Add dependent sums.

1 files changed, 30 insertions, 0 deletions

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index a15c3c1..4b4fded 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -20,6 +20,8 @@ data Constructor : Nat -> Type where
   Sort   : Sort -> Constructor n
   Pi     : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
   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
   Top    : Constructor n
   Bottom : Constructor n
 
@@ -27,6 +29,8 @@ public export
 data Neutral : Nat -> Type where
   Var    : String -> Fin n -> Neutral n
   App    : Neutral n -> NormalForm n -> Neutral n
+  Fst    : Neutral n -> Neutral n
+  Snd    : Neutral n -> Neutral n
   Absurd : Neutral n
 
 public export
@@ -58,12 +62,16 @@ eqWhnf  : NormalForm n -> NormalForm n -> Bool
 eqCnstr (Sort s) (Sort s') = s == s'
 eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
 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 Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
 
 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 Absurd Absurd = True
 eqNtrl _ _ = False
 
@@ -111,6 +119,16 @@ prettyPrecCnstr d (Lambda var t) =
   backslash <+> pretty var <++>
   pretty "=>" <+> softline <+>
   prettyPrecWhnf Open t
+prettyPrecCnstr d (Sigma _ _ var a b) =
+  parenthesise (d > Open) $
+  group $
+  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
+  pretty "**" <+> softline <+>
+  prettyPrecWhnf Open b
+prettyPrecCnstr d (Pair t u) =
+  angles $
+  group $
+  neutral <++> prettyPrecWhnf Open t <+> comma <+> softline <+> prettyPrecWhnf Open u <++> neutral
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -119,6 +137,14 @@ prettyPrecNtrl d (App t u) =
   parenthesise (d >= App) $
   group $
   fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u]
+prettyPrecNtrl d (Fst t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "fst", prettyPrecNtrl App t]
+prettyPrecNtrl d (Snd t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "snd", prettyPrecNtrl App t]
 prettyPrecNtrl d Absurd = pretty "absurd"
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
@@ -160,11 +186,15 @@ renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 renameCnstr (Sort s) f = Sort s
 renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
 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 Top f = Top
 renameCnstr Bottom f = Bottom
 
 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 Absurd f = Absurd
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f