diff options
Diffstat (limited to 'src/Inky/Term/Parser.idr')
| -rw-r--r-- | src/Inky/Term/Parser.idr | 27 |
1 files changed, 3 insertions, 24 deletions
diff --git a/src/Inky/Term/Parser.idr b/src/Inky/Term/Parser.idr index ee122bb..1c6eb58 100644 --- a/src/Inky/Term/Parser.idr +++ b/src/Inky/Term/Parser.idr @@ -38,7 +38,6 @@ data InkyKind | List | Suc | Map - | GetChildren | ParenOpen | ParenClose | BracketOpen @@ -75,7 +74,6 @@ export List == List = True Suc == Suc = True Map == Map = True - GetChildren == GetChildren = True ParenOpen == ParenOpen = True ParenClose == ParenClose = True BracketOpen == BracketOpen = True @@ -113,7 +111,6 @@ Interpolation InkyKind where interpolate List = "'List'" interpolate Suc = "'suc'" interpolate Map = "'map'" - interpolate GetChildren = "'getChildren'" interpolate ParenOpen = "'('" interpolate ParenClose = "')'" interpolate BracketOpen = "'['" @@ -154,7 +151,6 @@ TokenKind InkyKind where tokValue List = const () tokValue Suc = const () tokValue Map = const () - tokValue GetChildren = const () tokValue ParenOpen = const () tokValue ParenClose = const () tokValue BracketOpen = const () @@ -188,7 +184,6 @@ keywords = , ("List", List) , ("suc", Suc) , ("map", Map) - , ("getChildren", GetChildren) ] export @@ -281,7 +276,7 @@ TypeFun = ParseFun 1 Ty public export TermFun : Type -TermFun = ParseFun 2 (Term Bounds) +TermFun = ParseFun 2 (Term Sugar Bounds) public export TypeParser : SnocList String -> SnocList String -> Type @@ -431,7 +426,7 @@ AppTerm = , weaken (S Z) SuffixTerm ] , mkApp <$> Seq - [ OneOf {nils = [False, False, False]} + [ OneOf [ WithBounds SuffixTerm , mkMap <$> Seq [ WithBounds (match Map) @@ -444,16 +439,6 @@ AppTerm = , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType ] - , mkGetChildren <$> Seq - [ WithBounds (match GetChildren) - , enclose (match ParenOpen) (match ParenClose) $ Seq - [ match Backslash - , match TypeIdent - , match DoubleArrow - , rename Id (Drop Id) OpenType - ] - , sub [<"openType" :- rename Id (Drop Id) OpenType] [<] AtomType - ] ] , star (weaken (S Z) SuffixTerm) ] @@ -468,12 +453,6 @@ AppTerm = pure $ Map m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx) !(c.try tyCtx)) <$ m - mkGetChildren : HList [WithBounds (), HList [_, String, _, TypeFun], TypeFun] -> WithBounds TermFun - mkGetChildren [m, [_, x, _, a], b] = - MkParseFun (\tyCtx, tmCtx => - pure $ GetChildren m.bounds (x ** !(a.try (tyCtx :< x))) !(b.try tyCtx)) - <$ m - mkApp : HList [WithBounds TermFun, List TermFun] -> TermFun mkApp [t, []] = t.val mkApp [fun, (arg :: args)] = @@ -600,7 +579,7 @@ CaseTerm = mkBranch : HList [String, String, (), TermFun] -> - Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Bounds tyCtx (tmCtx :< x))) + Assoc (ParseFun 2 $ \tyCtx, tmCtx => (x ** Term Sugar Bounds tyCtx (tmCtx :< x))) mkBranch [tag, bound, _, branch] = tag :- MkParseFun (\tyCtx, tmCtx => pure (bound ** !(branch.try tyCtx (tmCtx :< bound)))) |