0 | module Syntax.StringDiagram.Monoidal
 1 |
 2 | import public Control.Category.Core
 3 | import public Control.Category.Functor
 4 | import public Control.Category.Monoidal
 5 | import Data.Wrap0
 6 | import public Language.Reflection
 7 | import public Syntax.StringDiagram.Util
 8 |
 9 | %default total
10 | %language ElabReflection
11 |
12 | export infix 0 -<
13 | export prefix 0 =<
14 |
15 | record MonDiagramStep where
16 |   constructor MkMDStep
17 |   l, c, c', r : Nat
18 |   mor : TTImp
19 |
20 | MonDiagram : Type
21 | MonDiagram = List MonDiagramStep
22 |
23 | findSublist : Eq a => (sub, full : List a) -> Maybe (List a, List a)
24 | findSublist [] full = Just ([], full)
25 | findSublist (_ :: _) [] = Nothing
26 | findSublist (s :: sub) (f :: full) =
27 |   if s == f
28 |   then findSublist sub full
29 |   else mapFst (f::) <$> findSublist (s :: sub) full
30 |
31 | ||| Check if this string diagram is valid in a monoidal category.
32 | checkDiagram : SDiagram -> Elab MonDiagram
33 | checkDiagram (MkSDiagram inp steps out) = do
34 |   let Just strings = the (Maybe _) $ sequence inp
35 |     | Nothing => fail "Strings cannot be discarded"
36 |   checkDiagram' [<] strings steps
37 |   where
38 |     checkDiagram' : SnocList MonDiagramStep -> List String -> List SDiagramStep -> Elab MonDiagram
39 |     checkDiagram' diag strings (MkSDStep i m o :: steps) = do
40 |       let Just o' = the (Maybe _) $ sequence o
41 |         | Nothing => fail "Strings cannot be discarded"
42 |       let False = any (\name => elem name strings) o'
43 |         | True => fail "Cannot shadow string name"
44 |       let Just (l,r) = findSublist i strings
45 |         | Nothing => fail "Strings are not contiguous"
46 |       checkDiagram'
47 |         (diag :< MkMDStep (length l) (length i) (length o) (length r) m)
48 |         (l ++ o' ++ r) steps
49 |     checkDiagram' diag strings [] =
50 |       if strings == out
51 |       then pure (diag <>> [])
52 |       else fail "Return strings are not contiguous"
53 |
54 | ||| Expand shortened string diagram notation into a full expression.
55 | |||
56 | ||| This takes two additional parameters: `obj`, which is a wildcard
57 | ||| expression used when passing objects as parameters, and `impl`,
58 | ||| which is the `Monoidal` implementation the expansion will use.
59 | export
60 | stringImpl : (obj,impl : TTImp) -> TTImp -> Elab TTImp
61 | stringImpl obj impl t = do
62 |   diag <- checkDiagram =<< parseDiagram t
63 |   cat <- genSym "cat"
64 |   ts <- for diag $ \(MkMDStep l c c' r mor) => do
65 |     pure `(
66 |       Control.Category.Monoidal.applyAssoc
67 |       @{~impl}
68 |       {xs = ~(listImp l), ys = ~(listImp c),
69 |        ys' = ~(listImp c'), zs = ~(listImp r)}
70 |        ~(mor))
71 |   pure `(let Control.Category.Monoidal.MkMonoidal @{~(IBindVar EmptyFC cat)} {} = ~impl
72 |          in ~(composeImp (IVar EmptyFC cat) ts))
73 |   where
74 |     listImp : Nat -> TTImp
75 |     listImp Z = `(Prelude.Nil)
76 |     listImp (S n) = `(Prelude.(::) ~obj ~(listImp n))
77 |
78 |     composeImp : TTImp -> List TTImp -> TTImp
79 |     composeImp cat [] =
80 |       `(Control.Category.Core.id @{~cat}
81 |         {a = ~obj})
82 |     composeImp _ [t] = t
83 |     composeImp cat (t :: ts) =
84 |       `(Control.Category.Core.(.) @{~cat}
85 |         {a = ~obj, b = ~obj, c = ~obj}
86 |         ~(composeImp cat ts) ~t)
87 |
88 | ||| Enter string diagram notation (for `Monoidal`).
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 |          Monoidal 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 |