0 | module Syntax.StringDiagram.Cartesian
 1 |
 2 | import public Control.Category.Core
 3 | import public Control.Category.Functor
 4 | import public Control.Category.Monoidal
 5 | import public Control.Category.Cartesian
 6 | import public Data.Fin
 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 | usedInDiagram : List SDiagramStep -> List String -> String -> Bool
18 | usedInDiagram [] out n = elem n out
19 | usedInDiagram (step :: steps) out n =
20 |   elem n step.inputs ||
21 |     (not (elem (Just n) step.outputs) && usedInDiagram steps out n)
22 |
23 | ||| Expand shortened string diagram notation into a full expression.
24 | |||
25 | ||| This takes two additional parameters: `obj`, which is a wildcard
26 | ||| expression used when passing objects as parameters, and `impl`,
27 | ||| which is the `Cartesian` implementation the expansion will use.
28 | export
29 | stringImpl : (obj,impl : TTImp) -> TTImp -> Elab TTImp
30 | stringImpl obj impl t = do
31 |   MkSDiagram inp steps out <- parseDiagram t
32 |   mon <- genSym "mon"
33 |   cat <- genSym "cat"
34 |   ts <- stringImpl' [<] (IVar EmptyFC mon) inp out steps
35 |   pure `(let Control.Category.Cartesian.MkCartesian @{~(IBindVar EmptyFC mon)} {} = ~impl
36 |              Control.Category.Monoidal.MkMonoidal @{~(IBindVar EmptyFC cat)} {} = ~(IVar EmptyFC mon)
37 |         in ~(composeImp (IVar EmptyFC cat) ts))
38 |   where
39 |     listImp : Nat -> TTImp
40 |     listImp Z = `(Prelude.Nil)
41 |     listImp (S n) = `(Prelude.(::) ~obj ~(listImp n))
42 |
43 |     toFinList : List Integer -> TTImp
44 |     toFinList [] = `(Prelude.Nil)
45 |     toFinList (n :: ns) =
46 |       `(Prelude.(::) (Data.Fin.fromInteger ~(IPrimVal EmptyFC (BI n))) ~(toFinList ns))
47 |
48 |     stringImpl' : SnocList TTImp -> TTImp ->
49 |                   List (Maybe String) -> List String -> List SDiagramStep -> Elab (SnocList TTImp)
50 |     stringImpl' ts mon strings out (step :: steps) = do
51 |       let (us, used) = unzip $
52 |                         filter (\(_,name) => not (elem (Just name) step.outputs) &&
53 |                                               usedInDiagram steps out name) $
54 |                         mapMaybe (\(i,n) => (i,) <$> n) $
55 |                         zip [0..natToInteger (length strings) - 1] strings
56 |       let Just is = for step.inputs $ \n =>
57 |                       finToInteger <$> findIndex (== Just n) strings
58 |         | Nothing => fail "Unrecognized string name"
59 |       let sw = toFinList (us ++ is)
60 |       stringImpl'
61 |         (ts :<
62 |         `(Control.Category.Cartesian.swizzle @{~impl}
63 |         {xs = ~(listImp $ length strings)} ~sw) :<
64 |         `(Control.Category.Monoidal.applyAssoc @{~mon}
65 |           {xs = ~(listImp $ length us), ys = ~(listImp $ length step.inputs),
66 |            ys' = ~(listImp $ length step.outputs), zs = Prelude.Nil} ~(step.mor)))
67 |         mon
68 |         (map Just used ++ step.outputs)
69 |         out steps
70 |     stringImpl' ts _ strings out [] = do
71 |       let Just is = for out $ \n =>
72 |                       finToInteger <$> findIndex (== Just n) strings
73 |         | Nothing => fail "Unrecognized string name"
74 |       let sw = toFinList is
75 |       pure (ts :<
76 |         `(Control.Category.Cartesian.swizzle @{~impl}
77 |           {xs = ~(listImp $ length strings)} ~sw))
78 |       
79 |     composeImp : TTImp -> SnocList TTImp -> TTImp
80 |     composeImp cat [<] = `(Control.Category.Core.id {a = ~obj})
81 |     composeImp cat [<t] = t
82 |     composeImp cat (ts :< t) =
83 |       `(Control.Category.Core.(.) @{~cat}
84 |         {a = ~obj, b = ~obj, c = ~obj}
85 |         ~t ~(composeImp cat ts))
86 |
87 | ||| Enter string diagram notation (for `Cartesian`).
88 | |||
89 | ||| This elaboration script must be specifically invoked with
90 | ||| `%runElab`. The category is inferred from the return type, but
91 | ||| the tensor product must be passed as an explicit argument.
92 | export
93 | string : {obj : _} -> {0 cat : Hom obj} -> (0 ten : obj -> obj -> obj) -> {0 i,a,b : obj} ->
94 |          Cartesian cat ten i => TTImp -> Elab (cat a b)
95 | string {obj = obj@(Wrap0 _)} _ @{impl} t = check !(stringImpl `(W0 _) !(quote impl) t)
96 | string {obj = _} @{impl} _ t = check !(stringImpl `(_) !(quote impl) t)
97 |
98 |