Add equality types and casts.

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) |]