Add more program structure to abstract terms.

Add more program structure to type inference and checking.

1 files changed, 4 insertions, 40 deletions

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index a8a468c..a141d28 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -1,10 +1,10 @@
 ||| Raw syntax for terms. This is before eliminating names.
 module Obs.Syntax
 
+import Obs.Pretty
 import Obs.Universe
 
 import Text.Bounded
-import Text.PrettyPrint.Prettyprinter
 
 %default total
 
@@ -53,33 +53,9 @@ record Definition where
 
 -- Pretty Print ----------------------------------------------------------------
 
-prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
-prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
-
-prettyDeclForm : (prec : Prec) ->
-  (name : String) ->
-  (ty : Doc ann) ->
-  (sep : String) ->
-  (tail : Doc ann) ->
-  Doc ann
-prettyDeclForm d name ty sep tail =
-  parenthesise (d > Open) $
-  group $
-  vsep $
-  [prettyDecl name ty <++> pretty sep, align tail]
-
-prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
-prettyLambda d name body =
-  parenthesise (d >= App) $
-  group $
-  backslash <+> pretty name <++> pretty "=>" <+> line <+> align body
-
-prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann
-prettyApp d head tail = parenthesise (d >= App) $ group $ vsep (align head :: map (hang 2) tail)
-
-prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
 
+prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrec d (Var {var}) = pretty var
 prettyPrec d (Universe {s}) = prettyPrec d s
 prettyPrec d (Pi {var, domain, codomain}) =
@@ -89,14 +65,7 @@ prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyP
 prettyPrec d (Sigma {var, index, element}) =
   prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
 prettyPrec d (Pair {first, second}) =
-  angles $
-  group $
-  neutral <++>
-  align (prettyPrecBounds Open first) <+>
-  comma <+>
-  line <+>
-  align (prettyPrecBounds Open second) <++>
-  neutral
+  prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
 prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
@@ -115,12 +84,7 @@ prettyPrec d Bottom = pretty "Void"
 prettyPrec d (Absurd {contradiction}) =
   prettyApp d (pretty "absurd") [prettyPrecBounds App contradiction]
 prettyPrec d (Equal {left, right}) =
-  parenthesise (d >= Equal) $
-  group $
-  align (prettyPrecBounds Equal left) <++>
-  pretty "~" <+>
-  line <+>
-  align (prettyPrecBounds Equal right)
+  prettyEqual d (prettyPrecBounds Equal left) (prettyPrecBounds Equal right)
 prettyPrec d (Refl {value}) = prettyApp d (pretty "refl") [prettyPrecBounds App value]
 prettyPrec d (Transp {indexedType, oldIndex, value, newIndex, equality}) =
   prettyApp d (pretty "transp") $