1 files changed, 42 insertions, 0 deletions
diff --git a/src/CC/Term/Pretty.idr b/src/CC/Term/Pretty.idr
new file mode 100644
index 0000000..04e3109
--- /dev/null
+++ b/src/CC/Term/Pretty.idr
@@ -0,0 +1,42 @@
+module CC.Term.Pretty
+
+import CC.Name
+import CC.Term
+
+import Text.PrettyPrint.Prettyprinter
+
+--------------------------------------------------------------------------------
+
+startPrec, leftAppPrec, appPrec : Prec
+startPrec = Open
+leftAppPrec = Backtick
+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