diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 59 |
1 files changed, 44 insertions, 15 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index 0ccba86..acb1360 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -25,6 +25,10 @@ data ObsTokenKind | OTNat | OTFst | OTSnd + | OTEither + | OTLeft + | OTRight + | OTCase | OTPoint | OTVoid | OTAbsurd @@ -58,6 +62,10 @@ Eq ObsTokenKind where OTNat == OTNat = True OTFst == OTFst = True OTSnd == OTSnd = True + OTEither == OTEither = True + OTLeft == OTLeft = True + OTRight == OTRight = True + OTCase == OTCase = True OTPoint == OTPoint = True OTVoid == OTVoid = True OTAbsurd == OTAbsurd = True @@ -93,6 +101,10 @@ TokenKind ObsTokenKind where tokValue OTNat s = stringToNatOrZ s tokValue OTFst s = () tokValue OTSnd s = () + tokValue OTEither s = () + tokValue OTLeft s = () + tokValue OTRight s = () + tokValue OTCase s = () tokValue OTPoint s = () tokValue OTVoid s = () tokValue OTAbsurd s = () @@ -126,6 +138,10 @@ Show ObsToken where show (Tok OTNat s) = s show (Tok OTFst s) = "fst" show (Tok OTSnd s) = "snd" + show (Tok OTEither s) = "Either" + show (Tok OTLeft s) = "Left" + show (Tok OTRight s) = "Right" + show (Tok OTCase s) = "case" show (Tok OTPoint s) = "tt" show (Tok OTVoid s) = "Void" show (Tok OTAbsurd s) = "absurd" @@ -156,6 +172,10 @@ keywords = , ("Prop", OTProp) , ("fst", OTFst) , ("snd", OTSnd) + , ("Either", OTEither) + , ("Left", OTLeft) + , ("Right", OTRight) + , ("case", OTCase) , ("tt", OTPoint) , ("Void", OTVoid) , ("absurd", OTAbsurd) @@ -195,18 +215,26 @@ uncurry : (n : _) -> op a b n -> Vect n a -> b uncurry 0 f [] = f uncurry (S n) f (x :: xs) = uncurry n (f x) xs -headForms : List (ObsTokenKind, (n ** (Vect n (WithBounds Syntax) -> Syntax))) +termForms : List (ObsTokenKind, Syntax) +termForms = + [ (OTPoint, Point) + , (OTVoid, Bottom) + , (OTUnit, Top) + ] + +headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax))) headForms = - [ (OTFst, (1 ** uncurry 1 Fst)) - , (OTSnd, (1 ** uncurry 1 Snd)) - , (OTPoint, (0 ** uncurry 0 Point)) - , (OTVoid, (0 ** uncurry 0 Bottom)) - , (OTAbsurd, (2 ** uncurry 2 Absurd)) - , (OTRefl, (1 ** uncurry 1 Refl)) - , (OTTransp, (5 ** uncurry 5 Transp)) - , (OTCast, (3 ** uncurry 3 Cast)) - , (OTCastRefl, (1 ** uncurry 1 CastId)) - , (OTUnit, (0 ** uncurry 0 Top)) + [ (OTFst, (0 ** uncurry 1 Fst)) + , (OTSnd, (0 ** uncurry 1 Snd)) + , (OTEither, (1 ** uncurry 2 Sum)) + , (OTLeft, (0 ** uncurry 1 Left)) + , (OTRight, (0 ** uncurry 1 Right)) + , (OTCase, (4 ** uncurry 5 Case)) + , (OTAbsurd, (1 ** uncurry 2 Absurd)) + , (OTRefl, (0 ** uncurry 1 Refl)) + , (OTTransp, (4 ** uncurry 5 Transp)) + , (OTCast, (2 ** uncurry 3 Cast)) + , (OTCastRefl, (0 ** uncurry 1 CastId)) ] declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2)) @@ -265,7 +293,8 @@ exp : Grammar state ObsToken True (WithBounds Syntax) noSortsTerm = parens exp <|> var <|> - bounds (map (uncurry Pair) (pair exp)) + bounds (map (uncurry Pair) (pair exp)) <|> + bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms) term = noSortsTerm <|> map (map Sort) noArgSort @@ -274,7 +303,7 @@ head = map (map Sort) sort <|> bounds (choiceMap - (\(hd, (n ** f)) => match hd *> commit *> [| f (count n (whitespace *> term)) |]) + (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |]) headForms) spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $ @@ -306,7 +335,7 @@ partial fullDef : Grammar state ObsToken True Definition fullDef = seq - [| MkPair (decl exp) (optional whitespace *> match OTNewlines *> def) |] + [| MkPair (decl exp <* commit) (optional whitespace *> match OTNewlines *> def <* commit) |] (\((name, ty), (name', tm)) => if name.val == name'.val then pure (MkDefinition {name = name, ty, tm}) @@ -316,7 +345,7 @@ partial file : Grammar state ObsToken False (List Definition) file = optional (whitespace *> match OTNewlines) *> - sepEndBy (optional whitespace *> match OTNewlines) fullDef <* + sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) <* eof whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken |