diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-18 13:19:06 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-18 13:19:06 +0000 |
| commit | 88b6df5dd91c062a96e646e6e6b0ac5fd57b7c03 (patch) | |
| tree | e87c9a32740d6d9038156b1339737e93b9d617a3 /src/Obs/NormalForm.idr | |
| parent | 97f4dfe968f55e115f61ef43c37b8e7a16b6c3fd (diff) | |
Add False type.
Diffstat (limited to 'src/Obs/NormalForm.idr')
| -rw-r--r-- | src/Obs/NormalForm.idr | 17 |
1 files changed, 14 insertions, 3 deletions
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 |