0 | module Syntax.StringDiagram.Util
  1 |
  2 | import Language.Reflection
  3 |
  4 | %default total
  5 | %language ElabReflection
  6 |
  7 | export infix 0 -<
  8 | export prefix 0 =<
  9 |
 10 | parseList : TTImp -> Elab (List String)
 11 | parseList = go [<]
 12 |   where
 13 |     go : SnocList String -> TTImp -> Elab (List String)
 14 |     go res `(~(IVar _ $ UN $ Basic var) :: ~t) = go (res :< var) t
 15 |     go res t@`(~(IVar _ $ UN Underscore) :: ~_) = failAt (getFC t) "Underscores are not allowed here"
 16 |     go res t@`(~(Implicit _ True) :: ~_) = failAt (getFC t) "Underscores are not allowed here"
 17 |     go res t@`(~_ :: ~_) = failAt (getFC t) "Could not read list"
 18 |     go res `(Nil) = pure (res <>> [])
 19 |     go res t = failAt (getFC t) "Not in proper list form"
 20 |
 21 | parseSingle : TTImp -> Elab (List String)
 22 | parseSingle (IVar _ $ UN $ Basic var) = pure [var]
 23 | parseSingle t@(IVar _ $ UN Underscore) = failAt (getFC t) "Underscores are not allowed here"
 24 | parseSingle t@(Implicit _ True) = failAt (getFC t) "Underscores are not allowed here"
 25 | parseSingle t = failAt (getFC t) "Not in proper list form"
 26 |
 27 | export
 28 | parseListOrSing : TTImp -> Elab (List String)
 29 | parseListOrSing t = parseList t <|> parseSingle t
 30 |
 31 | parseListPat : TTImp -> Elab (List (Maybe String))
 32 | parseListPat = go [<]
 33 |   where
 34 |     go : SnocList (Maybe String) -> TTImp -> Elab (List (Maybe String))
 35 |     go res `(~(IBindVar _ $ UN $ Basic var) :: ~t) = go (res :< Just var) t
 36 |     go res `(~(IBindVar _ $ UN Underscore) :: ~t) = go (res :< Nothing) t
 37 |     go res `(~(Implicit _ True) :: ~t) = go (res :< Nothing) t
 38 |     go res t@`(~_ :: ~_) = failAt (getFC t) "Could not read list"
 39 |     go res `(Nil) = pure (res <>> [])
 40 |     go res t = failAt (getFC t) "Not in proper list form"
 41 |
 42 | parseSinglePat : TTImp -> Elab (List (Maybe String))
 43 | parseSinglePat (IBindVar _ $ UN $ Basic var) = pure [Just var]
 44 | parseSinglePat t@(IBindVar _ $ UN Underscore) = pure [Nothing]
 45 | parseSinglePat t@(Implicit _ True) = pure [Nothing]
 46 | parseSinglePat t = failAt (getFC t) "Not in proper list form"
 47 |
 48 | export
 49 | parseListOrSingPat : TTImp -> Elab (List (Maybe String))
 50 | parseListOrSingPat t = parseListPat t <|> parseSinglePat t
 51 |
 52 | export
 53 | parseLam : TTImp -> Elab (List (Maybe String), TTImp)
 54 | parseLam
 55 |   t@(ILam _ MW ExplicitArg (Just _) _
 56 |     (ICase _ [] (IVar _ _) _ [PatClause _ ls exp])) = (,exp) <$> parseListOrSingPat ls
 57 | parseLam (ILam _ MW ExplicitArg (Just $ UN $ Basic var) _ exp) = pure ([Just var], exp)
 58 | parseLam (ILam _ MW ExplicitArg (Just $ UN Underscore) _ exp) = pure ([Nothing], exp)
 59 | parseLam (ILam _ MW ExplicitArg Nothing _ exp) = pure ([Nothing], exp)
 60 | parseLam t@(ILam {}) = failAt (getFC t) "Invalid string pattern"
 61 | parseLam t = failAt (getFC t) "Expected string pattern"
 62 |
 63 |
 64 | public export
 65 | record SDiagramStep where
 66 |   constructor MkSDStep
 67 |   inputs : List String
 68 |   mor : TTImp
 69 |   outputs : List (Maybe String)
 70 |
 71 | public export
 72 | record SDiagram where
 73 |   constructor MkSDiagram
 74 |   inputs : List (Maybe String)
 75 |   steps : List SDiagramStep
 76 |   outputs : List String
 77 |
 78 |
 79 | export
 80 | parseDiagram : TTImp -> Elab SDiagram
 81 | parseDiagram t = do
 82 |   (inp, rest) <- parseLam t
 83 |   let Nothing = findDup (catMaybes inp)
 84 |     | Just n => failAt (getFC t) "Duplicate string name '\{n}'"
 85 |   (steps, out) <- parseDiagram' [<] (catMaybes inp) rest
 86 |   pure $ MkSDiagram inp steps out
 87 |   where
 88 |     findDup : Eq a => List a -> Maybe a
 89 |     findDup [] = Nothing
 90 |     findDup (s :: ss) =
 91 |       if elem s ss
 92 |       then Just s
 93 |       else findDup ss
 94 |
 95 |     parseDiagram' : SnocList SDiagramStep -> List String -> TTImp -> Elab (List SDiagramStep, List String)
 96 |     parseDiagram' steps names t@`((~(mor) -< ~(inp)) >>= ~(pat)) = do
 97 |       (inp',o,names',rest) <- do
 98 |         inp' <- parseListOrSing inp
 99 |         (o, rest) <- parseLam pat
100 |         let onames = catMaybes o
101 |         let Nothing = findDup onames
102 |           | Just n => failAt (getFC pat) "Duplicate string name '\{n}'"
103 |         let names' = filter (\n => not $ elem n onames) names
104 |         pure (inp',o,onames ++ names',rest)
105 |       parseDiagram' (steps :< MkSDStep inp' mor o) names' (assert_smaller t rest)
106 |     parseDiagram' steps names t@`((~(mor) -< ~(inp)) >> ~(rest)) = do
107 |       inp' <- parseListOrSing inp
108 |       parseDiagram' (steps :< MkSDStep inp' mor []) names (assert_smaller t rest)
109 |     parseDiagram' steps names t@`(~(mor) >>= ~(pat)) = do
110 |       (o,names',rest) <- do
111 |         (o, rest) <- parseLam pat
112 |         let onames = catMaybes o
113 |         let Nothing = findDup onames
114 |           | Just n => failAt (getFC pat) "Duplicate string name '\{n}'"
115 |         let names' = filter (\n => not $ elem n onames) names
116 |         pure (o,onames ++ names',rest)
117 |       parseDiagram' (steps :< MkSDStep [] mor o) names' (assert_smaller t rest)
118 |     parseDiagram' steps names t@`(~(mor) >> ~(rest)) =
119 |       parseDiagram' (steps :< MkSDStep [] mor []) names (assert_smaller t rest)
120 |     parseDiagram' steps names `(=< ~(out)) = do
121 |       out' <- parseListOrSing out
122 |       pure (steps <>> [], out')
123 |     parseDiagram' _ _ t = failAt (getFC t) "Could not parse expression as string diagram"
124 |