Add more program structure to normal forms.

1 files changed, 31 insertions, 14 deletions

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 95ed08b..8dad72c 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,21 +12,33 @@ import Text.Bounded
 
 -- Definition ------------------------------------------------------------------
 
+data Term : Nat -> Type
+
+public export
+record DeclForm (n : Nat) where
+  constructor MkDecl
+  var : WithBounds String
+  type : WithBounds (Term n)
+
+public export
+record LambdaForm (n : Nat) where
+  constructor MkLambda
+  var : WithBounds String
+  body : WithBounds (Term (S n))
+
 public export
 data Term : Nat -> Type where
   Var : (var : String) -> (i : Fin n) -> Term n
   -- Universes
   Universe : (s : Universe) -> Term n
   -- Dependent Product
-  Pi : (var : WithBounds String) ->
-    (domain : WithBounds (Term n)) ->
+  Pi : (domain : DeclForm n) ->
     (codomain : WithBounds (Term (S n))) ->
     Term n
-  Lambda : (var : WithBounds String) -> (body : WithBounds (Term (S n))) -> Term n
+  Lambda : (body : LambdaForm n) -> Term n
   App : (fun, arg : WithBounds (Term n)) -> Term n
   -- Dependent Sums
-  Sigma : (var : WithBounds String) ->
-    (index : WithBounds (Term n)) ->
+  Sigma : (index : DeclForm n) ->
     (element : WithBounds (Term (S n))) ->
     Term n
   Pair : (first, second : WithBounds (Term n)) -> Term n
@@ -36,8 +48,7 @@ data Term : Nat -> Type where
   Bool : Term n
   True : Term n
   False : Term n
-  If : (var : WithBounds String) ->
-    (returnType : WithBounds (Term (S n))) ->
+  If : (returnType : LambdaForm n) ->
     (discriminant, true, false : WithBounds (Term n)) ->
     Term n
   -- True
@@ -69,15 +80,21 @@ data Block : Nat -> Type where
 
 prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
 
+prettyPrecDecl : DeclForm n -> Doc ann
+prettyPrecDecl (MkDecl var type) = prettyDecl (Just var.val) (prettyPrecBounds Open type)
+
+prettyPrecLambda : Prec -> LambdaForm n -> Doc ann
+prettyPrecLambda d (MkLambda var body) = prettyLambda d var.val (prettyPrecBounds Open body)
+
 prettyPrec : Prec -> Term n -> Doc ann
 prettyPrec d (Var {var, i}) = pretty var
 prettyPrec d (Universe {s}) = prettyPrec d s
-prettyPrec d (Pi {var, domain, codomain}) =
-  prettyDeclForm d var.val (prettyPrecBounds Open domain) "->" (prettyPrecBounds Open codomain)
-prettyPrec d (Lambda {var, body}) = prettyLambda d var.val (prettyPrecBounds Open body)
+prettyPrec d (Pi {domain, codomain}) =
+  prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrecBounds Open codomain)
+prettyPrec d (Lambda {body}) = prettyPrecLambda d body
 prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg]
-prettyPrec d (Sigma {var, index, element}) =
-  prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
+prettyPrec d (Sigma {index, element}) =
+  prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrecBounds Open element)
 prettyPrec d (Pair {first, second}) =
   prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
@@ -85,9 +102,9 @@ prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App a
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
-prettyPrec d (If {var, returnType, discriminant, true, false}) =
+prettyPrec d (If {returnType, discriminant, true, false}) =
   prettyApp d (pretty "if") $
-  [ prettyLambda App var.val (prettyPrecBounds Open returnType)
+  [ prettyPrecLambda App returnType
   , prettyPrecBounds App discriminant
   , prettyPrecBounds App true
   , prettyPrecBounds App false