Got pretty printing partially working using the Pretty type class as …

…a replacement for Show. Now need to tweak it in order to make everything look nice, and to get terms printing correctly!

idris.cabal

@@ -67,7 +67,7 @@ Executable     idris
 
                Build-depends:   base>=4 && <5, parsec, mtl, Cabal, haskeline,
                                 containers, process, transformers, filepath, directory,
-                                binary, bytestring, epic>=0.9.3
+                                binary, bytestring, epic>=0.9.3, pretty
 
                Extensions:      MultiParamTypeClasses, FunctionalDependencies,
                                 FlexibleInstances, TemplateHaskell

src/Core/Elaborate.hs

@@ -21,6 +21,8 @@ import Data.Char
 import Data.List
 import Debug.Trace
 
+import Util.Pretty
+
 -- I don't really want this here, but it's useful for the test shell
 data Command = Theorem Name Raw
              | Eval Raw
@@ -29,7 +31,10 @@ data Command = Theorem Name Raw
              | Tac (Elab ())
 
 data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
-  deriving Show
+
+instance Pretty aux => Pretty (ElabState aux) where
+  pretty (ES (pState, aux) str _) = text "test"
+
 type Elab' aux a = StateT (ElabState aux) TC a
 type Elab a = Elab' () a
 

src/Core/ProofShell.hs

@@ -11,6 +11,8 @@ import Core.Elaborate
 import Control.Monad.State
 import System.Console.Haskeline
 
+import Util.Pretty
+
 data ShellState = ShellState 
                         { ctxt     :: Context,
                           prf      :: Maybe ProofState,
@@ -50,13 +52,13 @@ processCommand (Tac e)  state
                                                                      (pterm ps')
                                                                      (ptype ps')
                                                                      (context ps') }, resp)
-                                err -> (state, show err)
+                                err -> (state, show . render . pretty $ err)
     | otherwise = (state, "No proof in progress")
 
 runShell :: ShellState -> InputT IO ShellState
 runShell st = do (prompt, parser) <- 
                            maybe (return ("TT# ", parseCommand)) 
-                                 (\st -> do outputStrLn (show st)
+                                 (\st -> do outputStrLn . render . pretty $ st
                                             return (show (thname st) ++ "# ", parseTactic)) 
                                  (prf st)
                  x <- getInputLine prompt

src/Core/ProofState.hs

@@ -13,10 +13,12 @@ import Core.TT
 import Core.Unify
 
 import Control.Monad.State
-import Control.Applicative
+import Control.Applicative hiding (empty)
 import Data.List
 import Debug.Trace
 
+import Util.Pretty
+
 data ProofState = PS { thname   :: Name,
                        holes    :: [Name], -- holes still to be solved
                        nextname :: Int,    -- name supply
@@ -94,6 +96,45 @@ instance Show ProofState where
                                          " =?= " ++ showEnv ps v
                showG ps b = showEnv ps (binderTy b)
 
+instance Pretty ProofState where
+  pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =
+    if size nm > breakingSize then
+      pretty nm <> colon $$ nest nestingSize (text " no more goals.")
+    else
+      pretty nm <> colon <+> text " no more goals."
+  pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =
+    let OK g  = goal (Just h) tm in
+    let wkEnv = premises g in
+      text "Other goals" <+> colon <+> pretty hs $$
+      prettyPs wkEnv (reverse wkEnv) $$
+      text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
+      pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
+    where
+      prettyGoal ps (Guess t v) =
+        if size v > breakingSize then
+          prettyEnv ps t <+> text "=?=" $$
+            nest nestingSize (prettyEnv ps v)
+        else 
+          prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
+      prettyGoal ps b = prettyEnv ps $ binderTy b
+
+      prettyPs env [] = empty
+      prettyPs env ((n, Let t v):bs) =
+        nest nestingSize (pretty n <+> colon <+>
+          if size v > breakingSize then
+            prettyEnv env t <+> text "=" $$
+              nest nestingSize (prettyEnv env v) $$
+                nest nestingSize (prettyPs env bs)
+          else
+            prettyEnv env t <+> text "=" <+> prettyEnv env v $$
+              nest nestingSize (prettyPs env bs))
+      prettyPs env ((n, b):bs) =
+        if size (binderTy b) > breakingSize then
+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
+        else
+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
+            nest nestingSize (prettyPs env bs))
+
 same Nothing n  = True
 same (Just x) n = x == n
 

src/Core/TT.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, FlexibleInstances #-}
 
 module Core.TT where
 
@@ -36,6 +36,9 @@ data FC = FC { fc_fname :: String,
 deriving instance Binary FC 
 !-}
 
+instance Sized FC where
+  size (FC f l) = 1 + length f
+
 instance Show FC where
     show (FC f l) = f ++ ":" ++ show l
 
@@ -50,6 +53,17 @@ data Err = Msg String
          | At FC Err
   deriving Eq
 
+instance Sized Err where
+  size (Msg msg) = length msg
+  size (CantUnify left right err score) = size left + size right + size err
+  size (NoSuchVariable name) = size name
+  size (NotInjective l c r) = size l + size c + size r
+  size (CantResolve trm) = size trm
+  size (IncompleteTerm trm) = size trm
+  size UniverseError = 1
+  size ProgramLineComment = 1
+  size (At fc err) = size fc + size err
+
 score :: Err -> Int
 score (CantUnify _ _ m s) = s + score m
 score (CantResolve _) = 20
@@ -62,10 +76,30 @@ instance Show Err where
                                ++ show e ++ " " ++ show i
     show _ = "Error"
 
+instance Pretty Err where
+  pretty (Msg m) = text m
+  pretty (CantUnify l r e i) =
+    if size l + size r > breakingSize then
+      text "Cannot unify" <+> colon $$
+        nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
+        nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
+    else
+      text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
+        nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
+  pretty _ = text "Error"
+
 data TC a = OK a
           | Error Err
   deriving (Eq, Functor)
 
+instance Pretty a => Pretty (TC a) where
+  pretty (OK ok) = pretty ok
+  pretty (Error err) =
+    if size err > breakingSize then
+      text "Error" <+> colon $$ (nest nestingSize $ pretty err)
+    else
+      text "Error" <+> colon <+> pretty err
+
 instance Show a => Show (TC a) where
     show (OK x) = show x
     show (Error str) = "Error: " ++ show str
@@ -120,6 +154,16 @@ data Name = UN String
 deriving instance Binary Name 
 !-}
 
+instance Sized Name where
+  size (UN n)     = 1
+  size (NS n els) = 1 + length els
+  size (MN i n) = 1
+
+instance Pretty Name where
+  pretty (UN n) = text n
+  pretty (NS n s) = pretty n
+  pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace
+
 instance Show Name where
     show (UN n) = n
     show (NS n s) = showSep "." (reverse s) ++ "." ++ show n
@@ -192,6 +236,23 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
 deriving instance Binary Const 
 !-}
 
+instance Sized Const where
+  size _ = 1
+
+instance Pretty Const where
+  pretty (I i) = text . show $ i
+  pretty (BI i) = text . show $ i
+  pretty (Fl f) = text . show $ f
+  pretty (Ch c) = text . show $ c
+  pretty (Str s) = text s
+  pretty IType = text "Int"
+  pretty BIType = text "BigInt"
+  pretty FlType = text "Float"
+  pretty ChType = text "Char"
+  pretty StrType = text "String"
+  pretty PtrType = text "Ptr"
+  pretty Forgot = text "Forgot"
+
 data Raw = Var Name
          | RBind Name (Binder Raw) Raw
          | RApp Raw Raw
@@ -229,6 +290,17 @@ data Binder b = Lam   { binderTy  :: b }
 deriving instance Binary Binder 
 !-}
 
+instance Sized a => Sized (Binder a) where
+  size (Lam ty) = 1 + size ty
+  size (Pi ty) = 1 + size ty
+  size (Let ty val) = 1 + size ty + size val
+  size (NLet ty val) = 1 + size ty + size val
+  size (Hole ty) = 1 + size ty
+  size (GHole ty) = 1 + size ty
+  size (Guess ty val) = 1 + size ty + size val
+  size (PVar ty) = 1 + size ty
+  size (PVTy ty) = 1 + size ty
+
 fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
 fmapMB f (Let t v)   = liftM2 Let (f t) (f v)
 fmapMB f (NLet t v)  = liftM2 NLet (f t) (f v)
@@ -270,6 +342,9 @@ data UExp = UVar Int -- universe variable
           | UVal Int -- explicit universe level
   deriving (Eq, Ord)
 
+instance Sized UExp where
+  size _ = 1
+
 -- We assume that universe levels have been checked, so anything external
 -- can just have the same universe variable and we won't get any new
 -- cycles.
@@ -300,6 +375,12 @@ data NameType = Bound | Ref | DCon Int Int | TCon Int Int
 deriving instance Binary NameType 
 !-}
 
+instance Sized NameType where
+  size _ = 1
+
+instance Pretty NameType where
+  pretty = text . show
+
 instance Eq NameType where
     Bound    == Bound    = True
     Ref      == Ref      = True
@@ -319,6 +400,18 @@ data TT n = P NameType n (TT n) -- embed type
 deriving instance Binary TT 
 !-}
 
+instance Sized a => Sized (TT a) where
+  size (P name n trm) = 1 + size name + size n + size trm
+  size (V v) = 1
+  size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
+  size (App l r) = 1 + size l + size r
+  size (Constant c) = size c
+  size Erased = 1
+  size (Set u) = 1 + size u
+
+instance Pretty a => Pretty (TT a) where
+  pretty 
+
 type EnvTT n = [(n, Binder (TT n))]
 
 data Datatype n = Data { d_typename :: n,
@@ -507,6 +600,54 @@ instance Show Const where
 showEnv env t = showEnv' env t False
 showEnvDbg env t = showEnv' env t True
 
+prettyEnv env t = prettyEnv' env t False
+  where
+    prettyEnv' env t dbg = prettySe 10 env t dbg
+
+    bracket outer inner p
+      | inner > outer = lparen <> p <> rparen
+      | otherwise     = p
+
+    prettySe p env (P nt n t) debug =
+      pretty n <+> 
+        if debug then
+          lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
+        else
+          empty
+    prettySe p env (V i) debug
+      | i < length env =
+        if debug then
+          text . show . fst $ env!!i
+        else
+          lbrack <+> text (show i) <+> rbrack
+      | otherwise      = text "unbound" <+> text (show i) <+> text "!"
+    prettySe p env (Bind n b@(Pi t) sc) debug
+      | noOccurrence n sc && not debug =
+          bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
+    prettySe p env (Bind n b sc) debug =
+      bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
+    prettySe p env (App f a) debug =
+      bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
+    prettySe p env (Constant c) debug = pretty c
+    prettySe p env Erased debug = text "[_]"
+    prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)
+
+    prettySb env n (Lam t) = prettyB env "λ" "=>" n t
+    prettySb env n (Hole t) = prettyB env "?defer" "." n t
+    prettySb env n (Pi t) = prettyB env "(" ") ->" n t
+    prettySb env n (PVar t) = prettyB env "pat" "." n t
+    prettySb env n (PVTy t) = prettyB env "pty" "." n t
+    prettySb env n (Let t v) = prettyBv env "let" "in" n t v
+    prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
+
+    prettyB env op sc n t debug =
+      text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
+
+    prettyBv env op sc n t v debug =
+      text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
+        prettySe 10 env v debug <> text sc
+
+
 showEnv' env t dbg = se 10 env t where
     se p env (P nt n t) = show n 
                             ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""