Add more program structure to normal forms.

1 files changed, 31 insertions, 13 deletions

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index a141d28..74e15c2 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -10,17 +10,31 @@ import Text.Bounded
 
 -- Definition ------------------------------------------------------------------
 
+data Syntax : Type
+
+public export
+record DeclForm where
+  constructor MkDecl
+  var : WithBounds String
+  type : WithBounds Syntax
+
+public export
+record LambdaForm where
+  constructor MkLambda
+  var : WithBounds String
+  body : WithBounds Syntax
+
 public export
 data Syntax : Type where
   Var : (var : String) -> Syntax
   -- Universes
   Universe : (s : Universe) -> Syntax
   -- Dependent Products
-  Pi : (var : WithBounds String) -> (domain, codomain : WithBounds Syntax) -> Syntax
-  Lambda : (var : WithBounds String) -> (body : WithBounds Syntax) -> Syntax
+  Pi : (domain : DeclForm) -> (codomain : WithBounds Syntax) -> Syntax
+  Lambda : (body : LambdaForm) -> Syntax
   App : (fun, arg : WithBounds Syntax) -> Syntax
   -- Dependent Sums
-  Sigma : (var : WithBounds String) -> (index, element : WithBounds Syntax) -> Syntax
+  Sigma : (index : DeclForm) -> (element : WithBounds Syntax) -> Syntax
   Pair : (first, second : WithBounds Syntax) -> Syntax
   First : (arg : WithBounds Syntax) -> Syntax
   Second : (arg : WithBounds Syntax) -> Syntax
@@ -28,9 +42,7 @@ data Syntax : Type where
   Bool : Syntax
   True : Syntax
   False : Syntax
-  If : (var : WithBounds String) ->
-    (returnType, discriminant, true, false : WithBounds Syntax) ->
-    Syntax
+  If : (returnType : LambdaForm) -> (discriminant, true, false : WithBounds Syntax) -> Syntax
   -- True
   Top : Syntax
   Point : Syntax
@@ -55,15 +67,21 @@ record Definition where
 
 prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
 
+prettyPrecDecl : DeclForm -> Doc ann
+prettyPrecDecl (MkDecl var type) = prettyDecl (Just var.val) (prettyPrecBounds Open type)
+
+prettyPrecLambda : Prec -> LambdaForm -> Doc ann
+prettyPrecLambda d (MkLambda var body) = prettyLambda d var.val (prettyPrecBounds Open body)
+
 prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrec d (Var {var}) = 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]
@@ -71,9 +89,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