Add False type.

1 files changed, 52 insertions, 19 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 2dd7052..7008950 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -27,6 +27,8 @@ data ObsTokenKind
   | OTProp
   | OTSet
   | OTNat
+  | OTVoid
+  | OTAbsurd
   -- Special symbols
   | OTUnit
   | OTPoint
@@ -46,6 +48,8 @@ Eq ObsTokenKind where
   OTNat     == OTNat     = True
   OTUnit    == OTUnit    = True
   OTPoint   == OTPoint   = True
+  OTVoid    == OTVoid    = True
+  OTAbsurd  == OTAbsurd  = True
   OTPOpen   == OTPOpen   = True
   OTPClose  == OTPClose  = True
   OTEqual   == OTEqual   = True
@@ -65,6 +69,8 @@ TokenKind ObsTokenKind where
   tokValue OTNat     s = stringToNatOrZ s
   tokValue OTUnit    s = ()
   tokValue OTPoint   s = ()
+  tokValue OTVoid    s = ()
+  tokValue OTAbsurd  s = ()
   tokValue OTPOpen   s = ()
   tokValue OTPClose  s = ()
   tokValue OTEqual   s = ()
@@ -84,6 +90,8 @@ keywords : List (String, ObsTokenKind)
 keywords =
   [ ("Set", OTSet)
   , ("Prop", OTProp)
+  , ("Void", OTVoid)
+  , ("absurd", OTAbsurd)
   ]
 
 obsTokenMap : TokenMap ObsToken
@@ -117,35 +125,60 @@ var = do
   id <- ident
   pure (Var id.bounds id.val)
 
-prop : Grammar state ObsToken True (WithBounds Sort)
+prop : Grammar state ObsToken True Syntax
 prop = do
-  p <- bounds $ match OTProp
-  pure (map (\_ => Prop) p)
+  prop <- bounds $ match OTProp
+  pure (Sort prop.bounds Prop)
 
-set : Grammar state ObsToken True (WithBounds Sort)
-set = do
-  s <- bounds $ match OTSet
-  i <- bounds $ option 0 (match OTNat)
-  pure (map Set $ mergeBounds s i)
-
-sort : Grammar state ObsToken True Syntax
-sort = do
-  sort <- prop <|> set
-  pure (Sort sort.bounds sort.val)
+set0 : Grammar state ObsToken True Syntax
+set0 = do
+  set <- bounds $ match OTSet
+  pure (Sort set.bounds (Set 0))
 
 top : Grammar state ObsToken True Syntax
-top = map (\v => Top v.bounds) $ bounds $ match OTUnit
+top = do
+  unit <- bounds $ match OTUnit
+  pure (Top unit.bounds)
 
 point : Grammar state ObsToken True Syntax
-point = map (\v => Point v.bounds) $ bounds $ match OTPoint
+point = do
+  point <- bounds $ match OTPoint
+  pure (Point point.bounds)
 
-partial
-exp  : Grammar state ObsToken True Syntax
+bottom : Grammar state ObsToken True Syntax
+bottom = do
+  void <- bounds $ match OTVoid
+  pure (Bottom void.bounds)
+
+atomicNoSet : Grammar state ObsToken True Syntax
+atomicNoSet = var <|> prop <|> top <|> point <|> bottom
+
+atomic : Grammar state ObsToken True Syntax
+atomic = atomicNoSet <|> set0
+
+set : Grammar state ObsToken True Syntax
+set = do
+  i <- [| mergeBounds (bounds $ match OTSet) (bounds $ map Set $ option 0 $ match OTNat) |]
+  pure (Sort i.bounds i.val)
+
+botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
+botElim = do
+  absurd <- bounds $ match OTAbsurd
+  pure (Absurd absurd.bounds)
+
+-- NOTE: these functions are all total.
 partial
 term : Grammar state ObsToken True Syntax
 
-exp = term
-term = var <|> sort <|> top <|> point <|> parens exp
+partial
+precGteApp : Grammar state ObsToken True Syntax
+
+partial
+exp : Grammar state ObsToken True Syntax
+
+term = atomic <|> parens exp
+precGteApp = atomicNoSet <|> set <|> parens exp
+exp = precGteApp <|> (botElim <*> term <*> term)
 
 partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)