From 88b6df5dd91c062a96e646e6e6b0ac5fd57b7c03 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 13:19:06 +0000
Subject: Add False type.

---
 src/Obs/Typing.idr | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

(limited to 'src/Obs/Typing.idr')

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)
-- 
cgit v1.2.3