diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 116 |
1 files changed, 56 insertions, 60 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index 7ce31c4..758b019 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -25,10 +25,10 @@ data ObsTokenKind | OTNat | OTFst | OTSnd - | OTEither - | OTLeft - | OTRight - | OTCase + | OTBool + | OTTrue + | OTFalse + | OTIf | OTContainer | OTTag | OTPosition @@ -70,10 +70,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 + OTBool == OTBool = True + OTTrue == OTTrue = True + OTFalse == OTFalse = True + OTIf == OTIf = True OTContainer == OTContainer = True OTTag == OTTag = True OTPosition == OTPosition = True @@ -117,10 +117,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 OTBool s = () + tokValue OTTrue s = () + tokValue OTFalse s = () + tokValue OTIf s = () tokValue OTContainer s = () tokValue OTTag s = () tokValue OTPosition s = () @@ -162,10 +162,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 OTBool s) = "Bool" + show (Tok OTTrue s) = "True" + show (Tok OTFalse s) = "False" + show (Tok OTIf s) = "if" show (Tok OTContainer s) = "Container" show (Tok OTTag s) = "tag" show (Tok OTPosition s) = "position" @@ -204,10 +204,10 @@ keywords = , ("Prop", OTProp) , ("fst", OTFst) , ("snd", OTSnd) - , ("Either", OTEither) - , ("Left", OTLeft) - , ("Right", OTRight) - , ("case", OTCase) + , ("Bool", OTBool) + , ("True", OTTrue) + , ("False", OTFalse) + , ("if", OTIf) , ("Container", OTContainer) , ("tag", OTTag) , ("position", OTPosition) @@ -256,7 +256,10 @@ uncurry (S n) f (x :: xs) = uncurry n (f x) xs termForms : List (ObsTokenKind, Syntax) termForms = - [ (OTPoint, Point) + [ (OTBool, Bool) + , (OTTrue, True) + , (OTFalse, False) + , (OTPoint, Point) , (OTVoid, Bottom) , (OTUnit, Top) ] @@ -265,22 +268,18 @@ headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax) headForms = [ (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)) - , (OTContainer, (2 ** uncurry 3 Container)) - , (OTTag, (0 ** uncurry 1 Tag)) - , (OTPosition, (0 ** uncurry 1 Position)) - , (OTNext, (0 ** uncurry 1 Next)) - , (OTSem, (2 ** uncurry 3 Sem)) - , (OTAbsurd, (1 ** uncurry 2 Absurd)) + , (OTAbsurd, (0 ** uncurry 1 Absurd)) , (OTRefl, (0 ** uncurry 1 Refl)) - , (OTTransp, (4 ** uncurry 5 Transp)) - , (OTCast, (2 ** uncurry 3 Cast)) + , (OTTransp, (4 ** (uncurry 5 Transp))) + , (OTCast, (3 ** uncurry 4 Cast)) , (OTCastRefl, (0 ** uncurry 1 CastId)) ] +headLambdaForms : List (ObsTokenKind, (n ** ((WithBounds String, WithBounds Syntax) -> Vect n (WithBounds Syntax) -> Syntax))) +headLambdaForms = + [ (OTIf, (3 ** (uncurry 3 . uncurry If))) + ] + declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2)) declForms = [(OTThinArrow, Pi), (OTProduct, Sigma)] @@ -321,6 +320,11 @@ pair p = (optional whitespace *> p <* optional whitespace) |] <* match OTAClose <* commit +lambda : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a) +lambda p = + match OTBackslash *> commit *> + [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |] + partial noSortsTerm : Grammar state ObsToken True (WithBounds Syntax) partial @@ -349,30 +353,25 @@ head = map (map Sort) sort <|> bounds (choiceMap + (\(hd, (n ** f)) => match hd *> commit *> + [| f (whitespace *> parens (lambda exp)) (count n (whitespace *> term))|]) + headLambdaForms) <|> + bounds + (choiceMap (\(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))) $ [| MkPair head (many (whitespace *> term)) |] -container = - map (\bounds@(MkBounded (t, u) _ _) => case u of - Nothing => t - Just (p, f) => map (\_ => MkContainer t p f) bounds) $ - bounds $ - [| MkPair spine - (optional - [| MkPair - (whitespace *> match OTTriangle *> commit *> whitespace *> spine) - (whitespace *> match OTSlash *> commit *> whitespace *> spine) - |]) - |] +container = spine equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $ [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |] exp = equals <|> + bounds (map (uncurry Lambda) $ lambda exp) <|> bounds (map (\((var, a), (b, f)) => f var a b) $ [| MkPair @@ -380,11 +379,7 @@ exp = (choiceMap (\(op, f) => match op *> commit *> whitespace *> [| MkPair exp (pure f) |]) declForms) - |]) <|> - bounds - (map (uncurry Lambda) $ - match OTBackslash *> commit *> - [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) exp |]) + |]) partial def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax) @@ -404,8 +399,8 @@ partial file : Grammar state ObsToken False (List Definition) file = optional (whitespace *> match OTNewlines) *> - sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) <* - eof + sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) + -- <* eof whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken whitespaceIrrelevant a = case (a.val.kind) of @@ -429,12 +424,7 @@ castErr : Either (List1 (ParsingError tok)) a -> Logging ann a castErr (Right x) = pure x castErr (Left errs) = do for_ {b = ()} errs - (\(Error msg bounds) => - error $ - maybe - (irrelevantBounds $ msg) - (\bounds => MkBounded msg False bounds) $ - bounds) + (\(Error msg bounds) => maybe id inBounds bounds $ error msg) abort partial @@ -442,8 +432,14 @@ export parse : String -> Logging ann (List Definition) parse str = do let (toks, _, _, "") = lex obsTokenMap str - | (_, l, c, rem) => inScope "lex" $ fatal "failed to lex input" + | (toks, l, c, rem) => inScope "lex" $ do + error "failed to lex input" + trace (map (\tok => show tok.val) toks) + trace (show rem) + abort let toks = preprocess toks (defs, []) <- inScope "parse" $ castErr $ parse file $ toks - | (_, ts) => inScope "parse" $ fatal "unparsed tokens" + | (_, ts) => inScope "parse" $ do + trace (map (show . val) ts) + fatal "unparsed tokens" pure defs |