Extract term printer to new module.

3 files changed, 44 insertions, 40 deletions

diff --git a/obs.ipkg b/obs.ipkg
index c1db82f..c937214 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -12,6 +12,7 @@ main = Main
 modules
   = CC.Name
   , CC.Term
+  , CC.Term.Pretty
   , CC.Term.Raw
   , CC.Thinning
   , Main
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
diff --git a/src/Main.idr b/src/Main.idr
index 8d69017..a5ce09c 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -2,6 +2,7 @@ module Main
 
 import CC.Name
 import CC.Term
+import CC.Term.Pretty
 import CC.Term.Raw
 import CC.Thinning
 
@@ -211,46 +212,6 @@ parseStdin = do
 
 --------------------------------------------------------------------------------
 
-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 t@(Abs _ _) =
-  let (names ** t) = getNames t in
-  parenthesise (d > startPrec) $ group $
-    backslash <+> prettyNames names <++> pretty "=>" <+> softline <+>
-    (assert_total $ prettyTerm startPrec t)
-  where
-  getNames : forall ctx. Term ctx -> (local ** Term (ctx <>< local))
-  getNames (Abs n t) = let (names ** t) = getNames t in (n :: names ** t)
-  getNames t = ([] ** t)
-
-  prettyNames : List Name -> Doc ann
-  prettyNames [] = neutral
-  prettyNames [n] = pretty n
-  prettyNames (n :: ns) = pretty n <+> comma <+> line <+> prettyNames ns
-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
-
-{ctx : Context} -> Pretty (Term ctx) where
-  prettyPrec = prettyTerm
-
---------------------------------------------------------------------------------
-
 -- -- ("\\" works for lambda as well)
 -- ex = main' "nf" $ unlines [
 --   "let λ λ 1 (1 (1 (1 (1 0))));",    -- five = λ s z. s (s (s (s (s z))))