From cb4ec1e7c1551c1d28f00ba11b062daa78e8c4e3 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 20 Dec 2022 11:07:04 +0000
Subject: Add equality types and casts.

---
 src/Obs/NormalForm.idr | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

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

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 4b4fded..2caf733 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -32,6 +32,13 @@ data Neutral : Nat -> Type where
   Fst    : Neutral n -> Neutral n
   Snd    : Neutral n -> Neutral n
   Absurd : Neutral n
+  Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
+  EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
+  EqualR : Nat -> Constructor n -> Neutral n -> Neutral n
+  EqualU : Nat -> Constructor n -> Constructor n -> Neutral n
+  CastL  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
+  CastR  : Constructor n -> Neutral n -> NormalForm n -> Neutral n
+  CastU  : Constructor n -> Constructor n -> NormalForm n -> Neutral n
 
 public export
 data NormalForm : Nat -> Type where
@@ -73,6 +80,13 @@ eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
 eqNtrl (Fst t) (Fst t') = eqNtrl t t'
 eqNtrl (Snd t) (Snd t') = eqNtrl t t'
 eqNtrl Absurd Absurd = True
+eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
+eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
+eqNtrl (EqualR i t u) (EqualR j t' u') = i == j && eqCnstr t t' && eqNtrl u u'
+eqNtrl (EqualU i t u) (EqualU j t' u') = i == j && eqCnstr t t' && eqCnstr u u'
+eqNtrl (CastL a b t) (CastL a' b' t') = eqNtrl a a' && eqWhnf b b' && eqWhnf t t'
+eqNtrl (CastR a b t) (CastR a' b' t') = eqCnstr a a' && eqNtrl b b' && eqWhnf t t'
+eqNtrl (CastU a b t) (CastU a' b' t') = eqCnstr a a' && eqCnstr b b' && eqWhnf t t'
 eqNtrl _ _ = False
 
 eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
@@ -146,6 +160,34 @@ prettyPrecNtrl d (Snd t) =
   group $
   fillSep [pretty "snd", prettyPrecNtrl App t]
 prettyPrecNtrl d Absurd = pretty "absurd"
+prettyPrecNtrl d (Equal _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecWhnf Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
+prettyPrecNtrl d (EqualL _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecNtrl Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
+prettyPrecNtrl d (EqualR _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecNtrl Equal u
+prettyPrecNtrl d (EqualU _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecCnstr Equal u
+prettyPrecNtrl d (CastL a b t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecNtrl App a, prettyPrecWhnf App b, prettyPrecWhnf App t]
+prettyPrecNtrl d (CastR a b t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrecWhnf App t]
+prettyPrecNtrl d (CastU a b t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrecWhnf App t]
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
 prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
@@ -196,6 +238,13 @@ renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
 renameNtrl (Fst t) f = Fst (renameNtrl t f)
 renameNtrl (Snd t) f = Snd (renameNtrl t f)
 renameNtrl Absurd f = Absurd
+renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
+renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
+renameNtrl (EqualR i t u) f = EqualR i (renameCnstr t f) (renameNtrl u f)
+renameNtrl (EqualU i t u) f = EqualU i (renameCnstr t f) (renameCnstr u f)
+renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (renameWhnf b f) (renameWhnf t f)
+renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (renameWhnf t f)
+renameNtrl (CastU a b t) f = CastU (renameCnstr a f) (renameCnstr b f) (renameWhnf t f)
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
 renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
-- 
cgit v1.2.3