Add False type.

6 files changed, 128 insertions, 49 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index fe00621..1b72965 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -37,9 +37,14 @@ abstractSyntax ctx (Var b str) = do
   let Just i = lookup str ctx
     | Nothing => report b "unbound variable: \{str}"
   pure (Var b i)
-abstractSyntax ctx (Sort b s)  = pure (Sort b s)
-abstractSyntax ctx (Top b)     = pure (Top b)
-abstractSyntax ctx (Point b)   = pure (Point b)
+abstractSyntax ctx (Sort b s) = pure (Sort b s)
+abstractSyntax ctx (Top b) = pure (Top b)
+abstractSyntax ctx (Point b) = pure (Point b)
+abstractSyntax ctx (Bottom b) = pure (Bottom b)
+abstractSyntax ctx (Absurd b a t) = do
+  a <- abstractSyntax ctx a
+  t <- abstractSyntax ctx t
+  pure (Absurd b a t)
 
 export
 abstractDefinition : Context n -> Definition -> Error (Definition n)
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index f930176..08354b4 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -17,12 +17,14 @@ data NormalForm  : Nat -> Type
 
 public export
 data Constructor : Nat -> Type where
-  Sort : Sort -> Constructor n
-  Top  : Constructor n
+  Sort   : Sort -> Constructor n
+  Top    : Constructor n
+  Bottom : Constructor n
 
 public export
 data Neutral : Nat -> Type where
-  Var : Fin n -> Neutral n
+  Var    : Fin n -> Neutral n
+  Absurd : Neutral n
 
 public export
 data NormalForm : Nat -> Type where
@@ -52,9 +54,12 @@ eqWhnf  : NormalForm n -> NormalForm n -> Bool
 
 eqCnstr (Sort s) (Sort s') = s == s'
 eqCnstr Top      Top       = True
+eqCnstr Bottom   Bottom    = True
 eqCnstr _ _ = False
 
 eqNtrl (Var i) (Var j) = i == j
+eqNtrl Absurd  Absurd  = True
+eqNtrl _ _ = False
 
 eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
 eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
@@ -81,8 +86,10 @@ prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
 
 prettyPrecCnstr d (Sort s) = prettyPrec d s
 prettyPrecCnstr d Top = pretty "()"
+prettyPrecCnstr d Bottom = pretty "Void"
 
 prettyPrecNtrl d (Var i) = pretty "$\{show i}"
+prettyPrecNtrl d Absurd = pretty "absurd"
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
 prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
@@ -122,8 +129,10 @@ renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 
 renameCnstr (Sort s) f = Sort s
 renameCnstr Top      f = Top
+renameCnstr Bottom   f = Bottom
 
 renameNtrl (Var i) f = Var (f i)
+renameNtrl Absurd  f = Absurd
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
 renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
@@ -149,8 +158,10 @@ substWhnf  : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m
 
 substCnstr (Sort s) f = Sort s
 substCnstr Top      f = Top
+substCnstr Bottom   f = Bottom
 
 substNtrl (Var i) f = f i
+substNtrl Absurd  f = Ntrl Absurd
 
 substWhnf (Ntrl t)  f = substNtrl t f
 substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
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)
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 056c86a..07c625b 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,12 +11,15 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var   : Bounds -> String -> Syntax
+  Var    : Bounds -> String -> Syntax
   -- Sorts
-  Sort  : Bounds -> Sort -> Syntax
+  Sort   : Bounds -> Sort -> Syntax
   -- True
-  Top   : Bounds -> Syntax
-  Point : Bounds -> Syntax
+  Top    : Bounds -> Syntax
+  Point  : Bounds -> Syntax
+  -- False
+  Bottom : Bounds -> Syntax
+  Absurd : Bounds -> Syntax -> Syntax -> Syntax
 
 public export
 record Definition where
@@ -31,9 +34,14 @@ record Definition where
 export
 Pretty Syntax where
   prettyPrec d (Var x str) = pretty str
-  prettyPrec d (Sort x s)  = prettyPrec d s
-  prettyPrec d (Top x)     = pretty "()"
-  prettyPrec d (Point x)   = pretty "_"
+  prettyPrec d (Sort x s) = prettyPrec d s
+  prettyPrec d (Top x) = pretty "()"
+  prettyPrec d (Point x) = pretty "_"
+  prettyPrec d (Bottom x) = pretty "Void"
+  prettyPrec d (Absurd x a t) =
+    parenthesise (d > Open) $
+    group $
+    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
 
 export
 Pretty Definition where
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 2cc2f93..62a22bc 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,12 +12,15 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var   : Bounds -> Fin n -> Term n
+  Var    : Bounds -> Fin n -> Term n
   -- Sorts
-  Sort  : Bounds -> Sort -> Term n
+  Sort   : Bounds -> Sort -> Term n
   -- True
-  Top   : Bounds -> Term n
-  Point : Bounds -> Term n
+  Top    : Bounds -> Term n
+  Point  : Bounds -> Term n
+  -- False
+  Bottom : Bounds -> Term n
+  Absurd : Bounds -> Term n -> Term n -> Term n
 
 public export
 record Definition (n : Nat) where
@@ -35,20 +38,27 @@ data Block : Nat -> Type where
 -- Operations ------------------------------------------------------------------
 
 export
-fullBounds : Term n -> Bounds
-fullBounds (Var x i)  = x
-fullBounds (Sort x s) = x
-fullBounds (Top x)     = x
-fullBounds (Point x)   = x
+fullBounds : Term n -> WithBounds (Term n)
+fullBounds tm@(Var x i)      = MkBounded tm False x
+fullBounds tm@(Sort x s)     = MkBounded tm False x
+fullBounds tm@(Top x)        = MkBounded tm False x
+fullBounds tm@(Point x)      = MkBounded tm False x
+fullBounds tm@(Bottom x)     = MkBounded tm False x
+fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
 
 -- Pretty Print ----------------------------------------------------------------
 
 export
 Pretty (Term n) where
-  prettyPrec d (Var x i)  = pretty "$\{show i}"
+  prettyPrec d (Var x i) = pretty "$\{show i}"
   prettyPrec d (Sort x s) = prettyPrec d s
-  prettyPrec d (Top x)    = pretty "()"
-  prettyPrec d (Point x)  = pretty "_"
+  prettyPrec d (Top x) = pretty "()"
+  prettyPrec d (Point x) = pretty "_"
+  prettyPrec d (Bottom x) = pretty "Void"
+  prettyPrec d (Absurd x a t) =
+    parenthesise (d > Open) $
+    group $
+    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
 
 export
 Pretty (Definition n) where
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 22994ec..e59de5d 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -20,12 +20,17 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 -- invariant: all definitions fully expanded
 -- invariant: m |- t, u <- a : s
 convert : (t, u, a : NormalForm n) -> Sort -> Bool
+-- In sort Prop
 convert Irrel Irrel a Prop = True
+-- In unknown type in set
 convert t u (Ntrl _) (Set k) = t == u
-convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort Prop)) (Set 0) = True
+-- In type Set
+convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = s' == s''
+convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = True
+convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = True
 convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = Ntrl t == u
 convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = t == Ntrl u
-convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort s)) (Set k) = s' == s''
+-- Default
 convert _ _ _ _ = False
 
 -- Typing Contexts -------------------------------------------------------------
@@ -61,7 +66,7 @@ check : Context n -> Term n -> NormalForm n -> Sort -> Error ann (NormalForm n)
 infer : Context n -> Term n -> Error ann (NormalForm n, NormalForm n, Sort)
 
 check ctx tm ty s = do
-  let bounds = fullBounds tm
+  let bounds = (fullBounds tm).bounds
   (tm, ty', s') <- infer ctx tm
   let True = s == s'
     | False => report bounds
@@ -75,13 +80,20 @@ infer ctx (Var b i) = pure $ index ctx i
 infer ctx (Sort b s) = pure $ (Cnstr (Sort s), Cnstr (Sort (suc s)), suc (suc s))
 infer ctx (Top b) = pure $ (Cnstr Top, Cnstr (Sort Prop), Set 0)
 infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
+infer ctx (Bottom b) = pure $ (Cnstr Bottom, Cnstr (Sort Prop), Set 0)
+infer ctx (Absurd b a t) = do
+  (a, Cnstr (Sort s), _) <- infer ctx a
+    | (_, ty, _) => report (fullBounds a).bounds
+      (pretty "type mismatch: expected sort" <+> comma <+> softline <+> "got" <++> pretty ty)
+  _ <- check ctx t (Cnstr Bottom) Prop
+  pure (Ntrl Absurd, a, s)
 
 -- Checking Definitions and Blocks ---------------------------------------------
 
 checkDef : Context n -> Term.Definition n -> Error ann (NormalForm.Definition n)
 checkDef ctx def = do
-  let tyBounds = fullBounds def.ty
-  let tmBounds = fullBounds def.tm
+  let tyBounds = (fullBounds def.ty).bounds
+  let tmBounds = (fullBounds def.tm).bounds
   (ty, Cnstr (Sort sort), _) <- infer ctx def.ty
     | (_, a, _) => report tyBounds
       (pretty "invalid declaration: expected sort" <+> comma <+> softline <+> "got" <++> pretty a)