From 39d9c956a98a0aecb4e2913d3df0cc8eb0e78f69 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 25 Mar 2023 16:43:28 +0000
Subject: Extract term printer to new module.

---
 src/CC/Term/Pretty.idr | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 src/CC/Term/Pretty.idr

(limited to 'src/CC')

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
-- 
cgit v1.2.3