0 | module Syntax.StringDiagram.Symmetric
 1 |
 2 | import public Control.Category.Core
 3 | import public Control.Category.Functor
 4 | import public Control.Category.Monoidal
 5 | import public Control.Category.Braided
 6 | import public Data.Vect
 7 | import Data.Wrap0
 8 | import public Language.Reflection
 9 | import public Syntax.StringDiagram.Util
10 |
11 | %default total
12 | %language ElabReflection
13 |
14 | export infix 0 -<
15 | export prefix 0 =<
16 |
17 | ||| Expand shortened string diagram notation into a full expression.
18 | |||
19 | ||| This takes two additional parameters: `obj`, which is a wildcard
20 | ||| expression used when passing objects as parameters, and `impl`,
21 | ||| which is the `Braided` implementation the expansion will use.
22 | export
23 | stringImpl : (obj,impl : TTImp) -> TTImp -> Elab TTImp
24 | stringImpl obj impl t = do
25 |   MkSDiagram inp steps out <- parseDiagram t
26 |   let Just inp' = the (Maybe _) $ sequence inp
27 |     | Nothing => fail "Strings cannot be discarded"
28 |   brd <- genSym "brd"
29 |   mon <- genSym "mon"
30 |   cat <- genSym "cat"
31 |   ts <- stringImpl' [<] (IVar EmptyFC mon) inp' out steps
32 |   pure `(let Control.Category.Braided.MkMonSymmetric @{~(IBindVar EmptyFC brd)} {} = ~impl
33 |              Control.Category.Braided.MkBraided @{~(IBindVar EmptyFC mon)} {} = ~(IVar EmptyFC brd)
34 |              Control.Category.Monoidal.MkMonoidal @{~(IBindVar EmptyFC cat)} {} = ~(IVar EmptyFC mon)
35 |         in ~(composeImp (IVar EmptyFC cat) ts))
36 |   where
37 |     listImp : Nat -> TTImp
38 |     listImp Z = `(Prelude.Nil)
39 |     listImp (S n) = `(Prelude.(::) ~obj ~(listImp n))
40 |
41 |     permutation : List Integer -> TTImp
42 |     permutation [] = `(Data.Permutation.Nil)
43 |     permutation (x :: xs) =
44 |       `(Data.Permutation.(::) (Data.Fin.fromInteger ~(IPrimVal EmptyFC (BI x))) ~(permutation xs))
45 |
46 |     stringsToBack : Eq a => SnocList Integer -> Integer -> List a -> List a -> TTImp
47 |     stringsToBack xs _ _ [] = permutation (xs <>> [])
48 |     stringsToBack xs r inp (str :: strings) =
49 |       case findIndex (==str) inp of
50 |         Just i => stringsToBack (xs :< r + finToInteger i) r (filter (/=str) inp) strings
51 |         Nothing => stringsToBack (xs :< 0) (r - 1) inp strings
52 |
53 |
54 |     stringImpl' : SnocList TTImp -> TTImp ->
55 |                   List String -> List String -> List SDiagramStep -> Elab (SnocList TTImp)
56 |     stringImpl' ts mon strings out (step :: steps) = do
57 |       let Just o = the (Maybe _) $ sequence step.outputs
58 |         | Nothing => fail "Strings cannot be discarded"
59 |       let rest = filter (\n => not $ elem n step.inputs) strings
60 |       let False = any (`elem` rest) o
61 |         | True => fail "Cannot shadow string name"
62 |       let perm = stringsToBack [<] (natToInteger $ length rest) step.inputs strings
63 |       stringImpl' (ts :<
64 |         `(Control.Category.Braided.permute @{~impl} {xs = ~(listImp $ length strings)} ~perm) :<
65 |         `(Control.Category.Monoidal.applyAssoc @{~mon}
66 |           {xs = ~(listImp $ length rest), ys = ~(listImp $ length step.inputs),
67 |            ys' = ~(listImp $ length o), zs = Prelude.Nil} ~(step.mor)))
68 |         mon (rest ++ o) out steps
69 |     stringImpl' ts _ strings out [] = do
70 |       perm <- do
71 |         let Just is = for out $ \n =>
72 |                       findIndex (== n) strings
73 |           | Nothing => fail "Unrecognized string name"
74 |         let Just p = fromPermSeq =<< toVect (length strings) is
75 |           | Nothing => fail "Return strings violate linearity"
76 |         pure $ permutation $ natToInteger <$> toList p
77 |       pure $ ts :< `(Control.Category.Braided.permute @{~impl}
78 |                       {xs = ~(listImp $ length strings)} ~perm)
79 |
80 |     composeImp : TTImp -> SnocList TTImp -> TTImp
81 |     composeImp cat [<] = `(Control.Category.Core.id {a = ~obj})
82 |     composeImp cat [<t] = t
83 |     composeImp cat (ts :< t) =
84 |       `(Control.Category.Core.(.) @{~cat}
85 |         {a = ~obj, b = ~obj, c = ~obj}
86 |         ~t ~(composeImp cat ts))
87 |
88 | ||| Enter string diagram notation (for `MonSymmetric`).
89 | |||
90 | ||| This elaboration script must be specifically invoked with
91 | ||| `%runElab`. The category is inferred from the return type, but
92 | ||| the tensor product must be passed as an explicit argument.
93 | export
94 | string : {obj : _} -> {0 cat : Hom obj} -> (0 ten : obj -> obj -> obj) -> {0 i,a,b : obj} ->
95 |          MonSymmetric cat ten i => TTImp -> Elab (cat a b)
96 | string {obj = obj@(Wrap0 _)} _ @{impl} t = check !(stringImpl `(W0 _) !(quote impl) t)
97 | string {obj = _} @{impl} _ t = check !(stringImpl `(_) !(quote impl) t)
98 |