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/NormalForm.idr | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

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

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