Extract term printer to new module.

1 files changed, 1 insertions, 40 deletions

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))))