From a8a4ef9933a1a07b6fbf2d257df2a5fb40b1e87d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Wed, 21 Dec 2022 20:32:56 +0000
Subject: Add sum types.

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

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

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index fd3a814..71b554c 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -23,6 +23,9 @@ data Constructor : Nat -> Type where
   Lambda : String -> NormalForm (S n) -> Constructor n
   Sigma  : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
   Pair   : NormalForm n -> NormalForm n -> Constructor n
+  Sum    : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n
+  Left   : NormalForm n -> Constructor n
+  Right  : NormalForm n -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
@@ -32,6 +35,7 @@ data Neutral : Nat -> Type where
   App    : Neutral n -> NormalForm n -> Neutral n
   Fst    : Neutral n -> Neutral n
   Snd    : Neutral n -> Neutral n
+  Case   : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
   Absurd : Neutral n
   Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
   EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
@@ -72,6 +76,9 @@ eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' &&
 eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
 eqCnstr (Sigma s s' _ a b) (Sigma l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
 eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
+eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
+eqCnstr (Left t) (Left t') = eqWhnf t t'
+eqCnstr (Right t) (Right t') = eqWhnf t t'
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
@@ -80,6 +87,7 @@ eqNtrl (Var _ i) (Var _ j) = i == j
 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 (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g'
 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'
@@ -144,6 +152,18 @@ prettyPrecCnstr d (Pair t u) =
   angles $
   group $
   neutral <++> prettyPrecWhnf Open t <+> comma <+> softline <+> prettyPrecWhnf Open u <++> neutral
+prettyPrecCnstr d (Sum _ _ a b) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Either", prettyPrecWhnf App a, prettyPrecWhnf App b]
+prettyPrecCnstr d (Left t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Left", prettyPrecWhnf App t]
+prettyPrecCnstr d (Right t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Right", prettyPrecWhnf App t]
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -160,6 +180,10 @@ prettyPrecNtrl d (Snd t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "snd", prettyPrecNtrl App t]
+prettyPrecNtrl d (Case t f g) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g]
 prettyPrecNtrl d Absurd = pretty "absurd"
 prettyPrecNtrl d (Equal _ t u) =
   parenthesise (d >= Equal) $
@@ -231,6 +255,9 @@ renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ l
 renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
 renameCnstr (Sigma s s' var a b) f = Sigma s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
 renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
+renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f)
+renameCnstr (Left t) f = Left (renameWhnf t f)
+renameCnstr (Right t) f = Right (renameWhnf t f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
@@ -238,6 +265,7 @@ renameNtrl (Var var i) f = Var var (f i)
 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 (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf 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)
-- 
cgit v1.2.3