diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 102 |
1 files changed, 58 insertions, 44 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index bd4139c..d0a9fb8 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -35,6 +35,11 @@ data ObsTokenKind -- Head Forms | OTFst | OTSnd + | OTMkContainer + | OTShape + | OTPosition + | OTNextIndex + | OTExtension | OTAbsurd | OTRefl | OTTransp @@ -45,6 +50,8 @@ data ObsTokenKind -- Decl Forms | OTThinArrow | OTProduct + -- Special Forms + | OTContainer -- Lambda Form | OTBackslash | OTFatArrow @@ -78,6 +85,11 @@ Eq ObsTokenKind where OTFst == OTFst = True OTSnd == OTSnd = True + OTMkContainer == OTMkContainer = True + OTShape == OTShape = True + OTPosition == OTPosition = True + OTNextIndex == OTNextIndex = True + OTExtension == OTExtension = True OTAbsurd == OTAbsurd = True OTRefl == OTRefl = True OTTransp == OTTransp = True @@ -89,6 +101,8 @@ Eq ObsTokenKind where OTThinArrow == OTThinArrow = True OTProduct == OTProduct = True + OTContainer == OTContainer = True + OTBackslash == OTBackslash = True OTFatArrow == OTFatArrow = True @@ -123,6 +137,11 @@ Show ObsTokenKind where show OTFst = "fst" show OTSnd = "snd" + show OTMkContainer = "MkContainer" + show OTShape = "Shape" + show OTPosition = "Position" + show OTNextIndex = "nextIndex" + show OTExtension = "extension" show OTAbsurd = "absurd" show OTRefl = "refl" show OTTransp = "transp" @@ -134,6 +153,8 @@ Show ObsTokenKind where show OTThinArrow = "->" show OTProduct = "**" + show OTContainer = "Container" + show OTBackslash = "\\" show OTFatArrow = "=>" @@ -170,6 +191,11 @@ TokenKind ObsTokenKind where tokValue OTFst s = () tokValue OTSnd s = () + tokValue OTMkContainer s = () + tokValue OTShape s = () + tokValue OTPosition s = () + tokValue OTNextIndex s = () + tokValue OTExtension s = () tokValue OTAbsurd s = () tokValue OTRefl s = () tokValue OTTransp s = () @@ -181,6 +207,8 @@ TokenKind ObsTokenKind where tokValue OTThinArrow s = () tokValue OTProduct s = () + tokValue OTContainer s = () + tokValue OTBackslash s = () tokValue OTFatArrow s = () @@ -198,47 +226,10 @@ ObsToken : Type ObsToken = Token ObsTokenKind Show ObsToken where - show (Tok OTNewlines s) = "\\n" - show (Tok OTSpaces s) = " " - show (Tok OTIdent s) = s - - show (Tok OTProp s) = "Prop" - show (Tok OTSet s) = "Set" show (Tok OTNat s) = s - show (Tok OTBool s) = "Bool" - show (Tok OTTrue s) = "True" - show (Tok OTFalse s) = "False" - show (Tok OTUnit s) = "()" - show (Tok OTPoint s) = "tt" - show (Tok OTVoid s) = "Void" - - show (Tok OTFst s) = "fst" - show (Tok OTSnd s) = "snd" - show (Tok OTAbsurd s) = "absurd" - show (Tok OTRefl s) = "refl" - show (Tok OTTransp s) = "transp" - show (Tok OTCast s) = "cast" - show (Tok OTCastRefl s) = "castRefl" - - show (Tok OTIf s) = "if" - - show (Tok OTThinArrow s) = "->" - show (Tok OTProduct s) = "**" - - show (Tok OTBackslash s) = "\\" - show (Tok OTFatArrow s) = "=>" - - show (Tok OTPOpen s) = "(" - show (Tok OTPClose s) = ")" - show (Tok OTAOpen s) = "<" - show (Tok OTAClose s) = ">" - - show (Tok OTComma s) = "," - show (Tok OTTilde s) = "~" - show (Tok OTEqual s) = "=" - show (Tok OTColon s) = ":" + show (Tok kind s) = show kind identifier : Lexer identifier = alpha <+> many alphaNum @@ -256,6 +247,11 @@ keywords = , ("fst", OTFst) , ("snd", OTSnd) + , ("MkContainer", OTMkContainer) + , ("Shape", OTShape) + , ("Position", OTPosition) + , ("nextIndex", OTNextIndex) + , ("extension", OTExtension) , ("absurd", OTAbsurd) , ("refl", OTRefl) , ("transp", OTTransp) @@ -263,6 +259,8 @@ keywords = , ("castRefl", OTCastRefl) , ("if", OTIf) + + , ("Container", OTContainer) ] obsTokenMap : TokenMap ObsToken @@ -313,6 +311,10 @@ headForms : List (ObsTokenKind, (n ** op (WithBounds Syntax) Syntax (S n))) headForms = [ (OTFst, (0 ** First)) , (OTSnd, (0 ** Second)) + , (OTMkContainer, (2 ** MkContainer)) + , (OTShape, (0 ** Shape)) + , (OTPosition, (0 ** Position)) + , (OTNextIndex, (0 ** Next)) , (OTAbsurd, (0 ** Absurd)) , (OTRefl, (0 ** Refl)) , (OTTransp, (4 ** Transp)) @@ -321,7 +323,7 @@ headForms = ] headLambdaForms : List (ObsTokenKind, (n ** (LambdaForm -> op (WithBounds Syntax) Syntax n))) -headLambdaForms = [(OTIf, (3 ** If))] +headLambdaForms = [(OTExtension, (1 ** Sem)), (OTIf, (3 ** If))] declForms : List (ObsTokenKind, (n ** op DeclForm (WithBounds Syntax -> Syntax) (S n))) declForms = @@ -363,14 +365,18 @@ universe = bounds $ map (const Prop) (match' OTProp <* commit) <|> map Set (match' OTSet *> commit *> option 0 (match' OTNat <* commit)) +termUniverse : Grammar state ObsToken True (WithBounds Universe) +termUniverse = noArgUniverse <|> parens universe + decl : Lazy (Grammar state ObsToken True (WithBounds Syntax)) -> Grammar state ObsToken True DeclForm decl p = [| MkDecl (ident <* whitespace <* match' OTColon <* whitespace) p |] -pair : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (a, a) -pair p = +pair : Lazy (Grammar state ObsToken True (WithBounds Syntax)) -> + Grammar state ObsToken True (WithBounds Syntax) +pair p = bounds $ match' OTAOpen *> commit *> - [| MkPair + [| Pair (optional whitespace *> p <* optional whitespace <* match' OTComma <* commit) (optional whitespace *> p <* optional whitespace) |] <* match' OTAClose <* commit @@ -397,7 +403,7 @@ exp : Grammar state ObsToken True (WithBounds Syntax) noUniversesTerm = parens exp <|> var <|> - bounds (map (uncurry Pair) (pair exp)) <|> + pair exp <|> bounds (choiceMap (\(k, s) => map (const s) (match' k)) termForms) term = noUniversesTerm <|> map (map Universe) noArgUniverse @@ -415,7 +421,15 @@ head = (choiceMap (\(hd, (n ** f)) => match' hd *> commit *> pure (uncurry (S n) f) <*> count (S n) (whitespace *> term)) - headForms) + headForms) <|> + bounds + (match OTContainer *> commit *> + [| Container + (whitespace *> term) + (whitespace *> term) + (whitespace *> termUniverse) + (whitespace *> termUniverse) + |]) spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $ [| MkPair head (many (whitespace *> term)) |] |