From 8c64e9c1f2ba4b95f73c7be24805c8766a5bc541 Mon Sep 17 00:00:00 2001 From: Dominic Mulligan Date: Tue, 28 Feb 2012 13:52:19 +0100 Subject: [PATCH] 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 | 2 +- src/Core/Elaborate.hs | 7 +- src/Core/ProofShell.hs | 6 +- src/Core/ProofState.hs | 43 ++++++++++++- src/Core/TT.hs | 143 ++++++++++++++++++++++++++++++++++++++++- src/Idris/AbsSyntax.hs | 40 +++++++++++- src/Idris/Prover.hs | 9 ++- src/Util/Pretty.hs | 17 ++++- 8 files changed, 256 insertions(+), 11 deletions(-) diff --git a/idris.cabal b/idris.cabal index 6bd3d1e1ea..008f6e47fb 100644 --- a/idris.cabal +++ b/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 diff --git a/src/Core/Elaborate.hs b/src/Core/Elaborate.hs index 1fa47a0263..d89de52d3a 100644 --- a/src/Core/Elaborate.hs +++ b/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 diff --git a/src/Core/ProofShell.hs b/src/Core/ProofShell.hs index ab9c38baf7..d837e45e92 100644 --- a/src/Core/ProofShell.hs +++ b/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 diff --git a/src/Core/ProofState.hs b/src/Core/ProofState.hs index 15222c256c..ef58abbda6 100644 --- a/src/Core/ProofState.hs +++ b/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 diff --git a/src/Core/TT.hs b/src/Core/TT.hs index 51c61c3ef6..a554fe9422 100644 --- a/src/Core/TT.hs +++ b/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 "" diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index 03d399280a..fb67c92d6a 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -5,7 +5,7 @@ module Idris.AbsSyntax where import Core.TT import Core.Evaluate -import Core.Elaborate +import Core.Elaborate hiding (Tactic(..)) import Core.Typecheck import System.Console.Haskeline @@ -576,6 +576,26 @@ data PTactic' t = Intro [Name] | Intros | Focus Name deriving instance Binary PTactic' !-} +instance Sized a => Sized (PTactic' a) where + size (Intro nms) = 1 + size nms + size Intros = 1 + size (Focus nm) = 1 + size nm + size (Refine nm bs) = 1 + size nm + length bs + size (Rewrite t) = 1 + size t + size (LetTac nm t) = 1 + size nm + size t + size (Exact t) = 1 + size t + size Compute = 1 + size Trivial = 1 + size Solve = 1 + size Attack = 1 + size ProofState = 1 + size ProofTerm = 1 + size Undo = 1 + size (Try l r) = 1 + size l + size r + size (TSeq l r) = 1 + size l + size r + size Qed = 1 + size Abandon = 1 + type PTactic = PTactic' PTerm data PDo' t = DoExp FC t @@ -588,6 +608,13 @@ data PDo' t = DoExp FC t deriving instance Binary PDo' !-} +instance Sized a => Sized (PDo' a) where + size (DoExp fc t) = 1 + size fc + size t + size (DoBind fc nm t) = 1 + size fc + size nm + size t + size (DoBindP fc l r) = 1 + size fc + size l + size r + size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r + size (DoLetP fc l r) = 1 + size fc + size l + size r + type PDo = PDo' PTerm -- The priority gives a hint as to elaboration order. Best to elaborate @@ -605,6 +632,13 @@ data PArg' t = PImp { priority :: Int, getScript :: t, getTm :: t } deriving (Show, Eq, Functor) + +instance Sized a => Sized (PArg' a) where + size (PImp p l nm trm) = 1 + size nm + size trm + size (PExp p l trm) = 1 + size trm + size (PConstraint p l trm) = 1 + size trm + size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm + {-! deriving instance Binary PArg' !-} @@ -886,7 +920,7 @@ instance Sized PTerm where size (PQuote rawTerm) = size rawTerm size (PRef fc name) = size name size (PLam name ty bdy) = 1 + size ty + size bdy - size (PPi name ty bdy) = 1 + size ty + size bdy + size (PPi plicity name ty bdy) = 1 + size ty + size bdy size (PLet name ty def bdy) = 1 + size ty + size def + size bdy size (PTyped trm ty) = 1 + size trm + size ty size (PApp fc name args) = 1 + size args @@ -897,7 +931,7 @@ instance Sized PTerm where size (PResolveTC fc) = 1 size (PEq fc left right) = 1 + size left + size right size (PPair fc left right) = 1 + size left + size right - size (PDPair fs left right) = 1 + size left + size right + size (PDPair fs left ty right) = 1 + size left + size ty + size right size (PAlternative alts) = 1 + size alts size (PHidden hidden) = size hidden size PSet = 1 diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs index 1c11cf2462..eed400fe80 100644 --- a/src/Idris/Prover.hs +++ b/src/Idris/Prover.hs @@ -17,6 +17,8 @@ import Idris.DataOpts import System.Console.Haskeline import Control.Monad.State +import Util.Pretty + prover :: Bool -> Name -> Idris () prover lit x = do ctxt <- getContext @@ -55,7 +57,11 @@ elabStep st e = do case runStateT e st of OK (a, st') -> return (a, st') Error a -> do i <- get fail (pshow i a) - + +dumpState :: IState -> ProofState -> IO () +dumpState _ pst = putStrLn . render . pretty $ pst + +{- dumpState :: IState -> ProofState -> IO () dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals" dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) @@ -80,6 +86,7 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) showG (Guess t v) = tshow t ++ " =?= " ++ tshow v showG b = tshow (binderTy b) +-} lifte :: ElabState [PDecl] -> ElabD a -> Idris a lifte st e = do (v, _) <- elabStep st e diff --git a/src/Util/Pretty.hs b/src/Util/Pretty.hs index c17402de0c..0b56ae481e 100644 --- a/src/Util/Pretty.hs +++ b/src/Util/Pretty.hs @@ -1,10 +1,12 @@ module Util.Pretty ( module Text.PrettyPrint.HughesPJ, - Sized(..), Pretty(..) + Sized(..), breakingSize, nestingSize, + Pretty(..) ) where import Text.PrettyPrint.HughesPJ +-- A rough notion of size for pretty printing various types. class Sized a where size :: a -> Int @@ -14,5 +16,18 @@ instance (Sized a, Sized b) => Sized (a, b) where instance Sized a => Sized [a] where size = sum . map size +-- The maximum size before we break on to another line. +breakingSize :: Int +breakingSize = 5 + +nestingSize :: Int +nestingSize = 2 + class Pretty a where pretty :: a -> Doc + +instance Pretty () where + pretty () = text "()" + +instance Pretty a => Pretty [a] where + pretty l = foldr (<+>) empty $ map pretty l