diff options
Diffstat (limited to 'src/Obs/Parser.idr')
| -rw-r--r-- | src/Obs/Parser.idr | 72 |
1 files changed, 64 insertions, 8 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr index efe7857..95d8e96 100644 --- a/src/Obs/Parser.idr +++ b/src/Obs/Parser.idr @@ -27,6 +27,10 @@ data ObsTokenKind | OTPoint | OTVoid | OTAbsurd + | OTRefl + | OTTransp + | OTCast + | OTCastRefl -- Special symbols | OTUnit -- Grouping symbols @@ -40,6 +44,7 @@ data ObsTokenKind | OTFatArrow | OTProduct | OTComma + | OTTilde | OTEqual | OTColon @@ -55,6 +60,10 @@ Eq ObsTokenKind where OTPoint == OTPoint = True OTVoid == OTVoid = True OTAbsurd == OTAbsurd = True + OTRefl == OTRefl = True + OTTransp == OTTransp = True + OTCast == OTCast = True + OTCastRefl == OTCastRefl = True OTUnit == OTUnit = True OTPOpen == OTPOpen = True OTPClose == OTPClose = True @@ -65,6 +74,7 @@ Eq ObsTokenKind where OTFatArrow == OTFatArrow = True OTProduct == OTProduct = True OTComma == OTComma = True + OTTilde == OTTilde = True OTEqual == OTEqual = True OTColon == OTColon = True _ == _ = False @@ -85,6 +95,10 @@ TokenKind ObsTokenKind where tokValue OTPoint s = () tokValue OTVoid s = () tokValue OTAbsurd s = () + tokValue OTRefl s = () + tokValue OTTransp s = () + tokValue OTCast s = () + tokValue OTCastRefl s = () tokValue OTUnit s = () tokValue OTPOpen s = () tokValue OTPClose s = () @@ -95,6 +109,7 @@ TokenKind ObsTokenKind where tokValue OTFatArrow s = () tokValue OTProduct s = () tokValue OTComma s = () + tokValue OTTilde s = () tokValue OTEqual s = () tokValue OTColon s = () @@ -117,6 +132,10 @@ keywords = , ("tt", OTPoint) , ("Void", OTVoid) , ("absurd", OTAbsurd) + , ("refl", OTRefl) + , ("transp", OTTransp) + , ("cast", OTCast) + , ("castRefl", OTCastRefl) ] obsTokenMap : TokenMap ObsToken @@ -136,16 +155,20 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++ , (exact "\\", OTBackslash) , (exact "**", OTProduct) , (exact ",", OTComma) + , (exact "~", OTTilde) , (exact "=", OTEqual) , (exact ":", OTColon) ] +newlines : Grammar state ObsToken False () +newlines = map (\_ => ()) $ many (match OTNewline) + parens : {c : _} -> Grammar state ObsToken c a -> Grammar state ObsToken True a parens g = match OTPOpen *> - many (match OTNewline) *> + newlines *> g <* - many (match OTNewline) <* + newlines <* match OTPClose ident : Grammar state ObsToken True (WithBounds String) @@ -192,7 +215,7 @@ set = do lambda : Grammar state ObsToken True (Syntax -> Syntax) lambda = do - name <- bounds $ match OTBackslash *> commit *> ident <* match OTFatArrow + name <- bounds $ match OTBackslash *> commit *> ident <* newlines <* match OTFatArrow <* newlines pure (Lambda name.bounds name.val) projFst : Grammar state ObsToken True (Syntax -> Syntax) @@ -210,6 +233,26 @@ botElim = do absurd <- bounds $ match OTAbsurd <* commit pure (Absurd absurd.bounds) +refl : Grammar state ObsToken True (Syntax -> Syntax) +refl = do + refl <- bounds $ match OTRefl <* commit + pure (Refl refl.bounds) + +transp : Grammar state ObsToken True (Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax) +transp = do + transp <- bounds $ match OTTransp <* commit + pure (Transp transp.bounds) + +cast : Grammar state ObsToken True (Syntax -> Syntax -> Syntax -> Syntax) +cast = do + cast <- bounds $ match OTCast <* commit + pure (Cast cast.bounds) + +castRefl : Grammar state ObsToken True (Syntax -> Syntax) +castRefl = do + castRefl <- bounds $ match OTCastRefl <* commit + pure (CastId castRefl.bounds) + -- NOTE: these functions are all total. partial pi : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax) @@ -222,6 +265,8 @@ term : Grammar state ObsToken True Syntax partial precGteApp : Grammar state ObsToken True Syntax partial +precGteEqual : Grammar state ObsToken True Syntax +partial exp' : Grammar state ObsToken True Syntax partial exp : Grammar state ObsToken True Syntax @@ -229,22 +274,33 @@ partial decl : Grammar state ObsToken True (WithBounds String, Syntax) pi decl = do - _ <- match OTThinArrow <* commit + _ <- match OTThinArrow <* commit <* newlines Parser.Core.pure (uncurry (Pi decl.bounds) decl.val) sigma decl = do - _ <- match OTProduct <* commit + _ <- match OTProduct <* commit <* newlines Parser.Core.pure (uncurry (Sigma decl.bounds) decl.val) pair fst snd = do - pair <- bounds $ [| MkPair (match OTAOpen *> fst <* match OTComma) (snd <* match OTAClose) |] + pair <- bounds $ [| MkPair (match OTAOpen *> fst <* newlines <* match OTComma <* newlines) (snd <* newlines <* match OTAClose) |] pure (uncurry (Pair pair.bounds) pair.val) term = atomic <|> pair exp exp <|> parens exp precGteApp = atomicNoSet <|> set <|> pair exp exp <|> parens exp -exp' = precGteApp <|> (projFst <*> term) <|> (projSnd <*> term) <|> (botElim <*> term <*> term) +precGteEqual = + map (\ty => let (t, t') = ty.val in maybe t (Equal ty.bounds t) t') $ + bounds [| MkPair precGteApp (optional (newlines *> match OTTilde *> commit *> newlines *> precGteApp)) |] +exp' = + precGteEqual <|> + (projFst <*> term) <|> + (projSnd <*> term) <|> + (botElim <*> term <*> term) <|> + (refl <*> term) <|> + (transp <*> term <*> term <*> term <*> term <*> term) <|> + (Parser.cast <*> term <*> term <*> term) <|> + (castRefl <*> term) exp = - (bounds (parens decl) >>= (\decl => (pi decl <|> sigma decl) <*> exp)) <|> + (bounds (parens decl) <* many (match OTNewline) >>= (\decl => (pi decl <|> sigma decl) <*> exp)) <|> (lambda <*> exp) <|> (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |]) decl = [| MkPair ident (match OTColon *> commit *> exp) |] |