Add type checking.HEADmaster

Currently, there is Set in Set. Next step is to add universe levels.

1 files changed, 34 insertions, 24 deletions

diff --git a/src/CC/Term/Pretty.idr b/src/CC/Term/Pretty.idr
index 04e3109..2b56e16 100644
--- a/src/CC/Term/Pretty.idr
+++ b/src/CC/Term/Pretty.idr
@@ -7,36 +7,46 @@ import Text.PrettyPrint.Prettyprinter
 
 --------------------------------------------------------------------------------
 
-startPrec, leftAppPrec, appPrec : Prec
+startPrec, leftArrowPrec, leftAppPrec, appPrec : Prec
 startPrec = Open
-leftAppPrec = Backtick
+leftArrowPrec = Backtick
+leftAppPrec = Open
 appPrec = App
 
 prettyVar : (ctx : Context) -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Doc ann
 prettyVar (_ :< n) 0 (Here eq) = pretty n
 prettyVar (ctx :< _) (S k) (There prf) = prettyVar ctx k prf
 
-prettyTerm : {ctx : Context} -> Prec -> Term ctx -> Doc ann
-prettyTerm d (Var k _ prf) = prettyVar ctx k prf
-prettyTerm d (Abs n t) =
-  let (names, body) = mapFst (pretty n ::) $ getNames t in
-  parenthesise (d > startPrec) $ group $
-    backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++>
-    pretty "=>" <+> softline <+> body
-  where
-  getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann)
-  getNames (Abs n t) = mapFst (pretty n ::) (getNames t)
-  getNames t = ([], prettyTerm startPrec t)
-prettyTerm d (App t u) =
-  parenthesise (d >= appPrec) $ group $
-  prettyTerm leftAppPrec t <++> prettyTerm appPrec u
-prettyTerm d (Let n t u) =
-  parenthesise (d > startPrec) $ group $ align $
-    pretty "let" <++>
-    (group $ align $ hang 2 $ pretty n <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+>
-    pretty ";" <+> line <+>
-    prettyTerm startPrec u
-
 export
 {ctx : Context} -> Pretty (Term ctx) where
-  prettyPrec = prettyTerm
+  prettyPrec d (Var k n prf) = prettyVar ctx k prf
+  prettyPrec d (Let n Nothing val t) =
+    parenthesise (d > startPrec) $ group $ align $
+      pretty "let" <++>
+      (group $ align $ hang 2 $ pretty n <++> equals <+> line <+> pretty val) <+>
+      pretty ";" <+> line <+> pretty t
+  prettyPrec d (Let n (Just ty) val t) =
+    parenthesise (d > startPrec) $ group $ align $
+      pretty "let" <++>
+      (group $ align $ hang 2 $
+        pretty n <++> colon <++> pretty ty <++> equals <+> line <+> pretty val) <+>
+      pretty ";" <+> line <+> pretty t
+  prettyPrec d Set = pretty "Set"
+  prettyPrec d (Pi Nothing dom cod) =
+    parenthesise (d > startPrec) $ group $
+      prettyPrec leftArrowPrec dom <++> pretty "->" <++> pretty cod
+  prettyPrec d (Pi (Just n) dom cod) =
+    parenthesise (d > startPrec) $ group $
+      parens (pretty n <++> colon <++> pretty dom) <++> pretty "->" <+> softline <+> pretty cod
+  prettyPrec d (Abs n t) =
+    let (names, body) = mapFst (pretty n ::) $ getNames t in
+    parenthesise (d > startPrec) $ group $
+      backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++>
+      pretty "=>" <+> softline <+> body
+    where
+    getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann)
+    getNames (Abs n t) = mapFst (pretty n ::) (getNames t)
+    getNames t = ([], pretty t)
+  prettyPrec d (App t u) =
+    parenthesise (d >= appPrec) $ group $
+    prettyPrec leftAppPrec t <++> prettyPrec appPrec u