git.iko.soy/Idris-dev
on master help sign in
Merge pull request #801 from david-christiansen/semantic-pprint

Colour support in the prover + refactoring of pretty-printing vs show

commit1e3658921ea202b965562bca6d984a8a4631697c authorEdwin Brady <edwin.brady@gmail.com> dateTue 28 Jan 2014, 05:38 (13 years ago) parent50c2c539eb64f4
22 files changed+730−722
compare with master
unifiedsplit
idris.cabal+2 src/Idris/AbsSyntax.hs+56−89 src/Idris/AbsSyntaxTree.hs+361−351 src/Idris/CaseSplit.hs+3−3 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/ProofState.hs+12−12 src/Idris/Core/TT.hs+33−19 src/Idris/Coverage.hs+3−3 src/Idris/Delaborate.hs+109−103 src/Idris/ElabDecls.hs+32−32 src/Idris/IdeSlave.hs+17 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+28−23 src/Idris/REPL.hs+23−27 src/Util/Pretty.hs+5−8 test/reg007/expected+6−7 test/reg007/run+1−1 test/reg010/expected+6−7 test/reg023/expected+6−7 test/test020/expected+6−7 test/test030/expected+6−7 test/test037/expected+13−14
idris.cabal+2
@@ -434,6 +434,7 @@ Library
434434
435435 Build-depends: base >=4 && <5
436436 , Cabal
437+ , annotated-wl-pprint >= 0.5.3
437438 , ansi-terminal
438439 , ansi-wl-pprint
439440 , binary
@@ -463,6 +464,7 @@ Library
463464 , zlib
464465 Extensions: MultiParamTypeClasses
465466 , FunctionalDependencies
467+ , FlexibleContexts
466468 , FlexibleInstances
467469 , TemplateHaskell
468470
src/Idris/AbsSyntax.hs+56−89
@@ -397,6 +397,55 @@ ihPrintResult h s = do i <- getIState
397397 let good = SexpList [SymbolAtom "ok", toSExp s] in
398398 runIO $ hPutStrLn h $ convSExp "return" good n
399399
400+-- | Write a pretty-printed term to the console with semantic coloring
401+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
402+consoleDisplayAnnotated h output = do ist <- getIState
403+ runIO . hPutStrLn h .
404+ displayDecorated (consoleDecorate ist) .
405+ renderCompact $ output
406+
407+-- | Write pretty-printed output to IDESlave with semantic annotations
408+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
409+ideSlaveReturnAnnotated n h out = do ist <- getIState
410+ let (str, spans) = displaySpans .
411+ renderCompact .
412+ fmap (fancifyAnnots ist) $
413+ out
414+ good = [SymbolAtom "ok", toSExp str, toSExp spans]
415+ runIO . hPutStrLn h $ convSExp "return" good n
416+
417+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
418+ihPrintTermWithType h tm ty = do ist <- getIState
419+ let output = tm <+> colon <+> ty
420+ case idris_outputmode ist of
421+ RawOutput -> consoleDisplayAnnotated h output
422+ IdeSlave n -> ideSlaveReturnAnnotated n h output
423+
424+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
425+ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
426+ihPrintFunTypes h n [] = ihPrintError h $ "No such variable " ++ show n
427+ihPrintFunTypes h n overloads = do imp <- impShow
428+ ist <- getIState
429+ let output = vsep (map (uncurry (ppOverload imp)) overloads)
430+ case idris_outputmode ist of
431+ RawOutput -> consoleDisplayAnnotated h output
432+ IdeSlave n -> ideSlaveReturnAnnotated n h output
433+ where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
434+ ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm
435+
436+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
437+fancifyAnnots ist annot@(AnnName n _ _) =
438+ do let ctxt = tt_ctxt ist
439+ case () of
440+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
441+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
442+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
443+ _ | otherwise -> annot
444+fancifyAnnots _ annot = annot
445+
446+type1Doc :: Doc OutputAnnotation
447+type1Doc = (annotate AnnConstType $ text "Type 1")
448+
400449ihPrintError :: Handle -> String -> Idris ()
401450ihPrintError h s = do i <- getIState
402451 case idris_outputmode i of
@@ -425,11 +474,12 @@ ideslavePutSExp cmd info = do i <- getIState
425474 _ -> return ()
426475
427476-- this needs some typing magic and more structured output towards emacs
428−iputGoal :: String -> Idris ()
429−iputGoal s = do i <- getIState
477+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
478+iputGoal g = do i <- getIState
430479 case idris_outputmode i of
431− RawOutput -> runIO $ putStrLn s
432− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
480+ RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
481+ IdeSlave n -> runIO . putStrLn $
482+ convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
433483
434484isetPrompt :: String -> Idris ()
435485isetPrompt p = do i <- getIState
@@ -692,90 +742,6 @@ setTypeCase t = do i <- getIState
692742 putIState $ i { idris_options = opt' }
693743
694744
695−-- For inferring types of things
696−
697−bi = fileFC "builtin"
698−
699−inferTy = sMN 0 "__Infer"
700−inferCon = sMN 0 "__infer"
701−inferDecl = PDatadecl inferTy
702− PType
703− [("", inferCon, PPi impl (sMN 0 "iType") PType (
704− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
705− (PRef bi inferTy)), bi, [])]
706−inferOpts = []
707−
708−infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
709−infP = P (TCon 6 0) inferTy (TType (UVal 0))
710−
711−getInferTerm, getInferType :: Term -> Term
712−getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
713−getInferTerm (App (App _ _) tm) = tm
714−getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
715−
716−getInferType (Bind n b sc) = Bind n b $ getInferType sc
717−getInferType (App (App _ ty) _) = ty
718−
719−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
720−
721−primNames = [unitTy, unitCon,
722− falseTy, pairTy, pairCon,
723− eqTy, eqCon, inferTy, inferCon]
724−
725−unitTy = sMN 0 "__Unit"
726−unitCon = sMN 0 "__II"
727−unitDecl = PDatadecl unitTy PType
728− [("", unitCon, PRef bi unitTy, bi, [])]
729−unitOpts = [DefaultEliminator]
730−
731−falseTy = sMN 0 "__False"
732−falseDecl = PDatadecl falseTy PType []
733−falseOpts = []
734−
735−pairTy = sMN 0 "__Pair"
736−pairCon = sMN 0 "__MkPair"
737−pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
738− [("", pairCon, PPi impl (n "A") PType (
739− PPi impl (n "B") PType (
740− PPi expl (n "a") (PRef bi (n "A")) (
741− PPi expl (n "b") (PRef bi (n "B"))
742− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
743− pexp (PRef bi (n "B"))])))), bi, [])]
744− where n a = sMN 0 a
745−pairOpts = []
746−
747−eqTy = sUN "="
748−eqCon = sUN "refl"
749−eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
750− (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
751− PType)
752− [("", eqCon, PPi impl (n "A") PType (
753− PPi impl (n "x") (PRef bi (n "A"))
754− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
755− pimp (n "B") Placeholder False,
756− pexp (PRef bi (n "x")),
757− pexp (PRef bi (n "x"))])), bi, [])]
758− where n a = sMN 0 a
759−eqOpts = []
760−
761−elimName = sUN "__Elim"
762−elimMethElimTy = sUN "__elimTy"
763−elimMethElim = sUN "elim"
764−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
765− [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
766− PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
767−
768−-- Defined in builtins.idr
769−sigmaTy = sUN "Exists"
770−existsCon = sUN "Ex_intro"
771−
772−piBind :: [(Name, PTerm)] -> PTerm -> PTerm
773−piBind = piBindp expl
774−
775−piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
776−piBindp p [] t = t
777−piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
778−
779745-- Dealing with parameters
780746
781747expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
@@ -1442,7 +1408,7 @@ mkPApp fc a f as = let rest = drop a as in
14421408-- FIXME: It's possible that this really has to happen after elaboration
14431409
14441410findStatics :: IState -> PTerm -> (PTerm, [Bool])
1445−findStatics ist tm = trace (showImp Nothing True False tm) $
1411+findStatics ist tm = trace (show tm) $
14461412 let (ns, ss) = fs tm in
14471413 runState (pos ns ss tm) []
14481414 where fs (PPi p n t sc)
@@ -1726,3 +1692,4 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
17261692 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
17271693 mkUniq t = return t
17281694
1695+
src/Idris/AbsSyntaxTree.hs+361−351
@@ -30,6 +30,8 @@ import Data.Word (Word)
3030
3131import Debug.Trace
3232
33+import Text.PrettyPrint.Annotated.Leijen
34+
3335data IOption = IOption { opt_logLevel :: Int,
3436 opt_typecase :: Bool,
3537 opt_typeintype :: Bool,
@@ -908,275 +910,440 @@ expandNS syn n = case syn_namespace syn of
908910 xs -> sNS n xs
909911
910912
911−--- Pretty printing declarations and terms
913+-- For inferring types of things
912914
913−instance Show PTerm where
914− show tm = showImp Nothing False False tm
915+bi = fileFC "builtin"
915916
916−instance Pretty PTerm where
917− pretty = prettyImp False
917+inferTy = sMN 0 "__Infer"
918+inferCon = sMN 0 "__infer"
919+inferDecl = PDatadecl inferTy
920+ PType
921+ [("", inferCon, PPi impl (sMN 0 "iType") PType (
922+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
923+ (PRef bi inferTy)), bi, [])]
924+inferOpts = []
918925
919−instance Show PDecl where
920− show d = showDeclImp False d
926+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
927+infP = P (TCon 6 0) inferTy (TType (UVal 0))
921928
922−instance Show PClause where
923− show c = showCImp True c
929+getInferTerm, getInferType :: Term -> Term
930+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
931+getInferTerm (App (App _ _) tm) = tm
932+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
924933
925−instance Show PData where
926− show d = showDImp False d
934+getInferType (Bind n b sc) = Bind n b $ getInferType sc
935+getInferType (App (App _ ty) _) = ty
927936
928−showDecls :: Bool -> [PDecl] -> String
929−showDecls _ [] = ""
930−showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds
931937
932−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
933−showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t
934−showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)
935−showDeclImp _ (PData _ _ _ _ d) = showDImp True d
936−showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"
937−showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"
938−showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn
939−showDeclImp i (PClass _ _ _ cs n ps ds)
940− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds
941−showDeclImp i (PInstance _ _ cs n _ t _ ds)
942− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds
943−showDeclImp _ _ = "..."
944−-- showDeclImp (PImport i) = "import " ++ i
945938
939+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
946940
947−showCImp :: Bool -> PClause -> String
948−showCImp impl (PClause _ n l ws r w)
949− = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r
950− ++ " where " ++ show w
951− where
952− showWs [] = ""
953− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
954−showCImp impl (PWith _ n l ws r w)
955− = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r
956− ++ " { " ++ show w ++ " } "
957− where
958− showWs [] = ""
959− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
941+primNames = [unitTy, unitCon,
942+ falseTy, pairTy, pairCon,
943+ eqTy, eqCon, inferTy, inferCon]
960944
945+unitTy = sMN 0 "__Unit"
946+unitCon = sMN 0 "__II"
947+unitDecl = PDatadecl unitTy PType
948+ [("", unitCon, PRef bi unitTy, bi, [])]
949+unitOpts = [DefaultEliminator]
961950
962−showDImp :: Bool -> PData -> String
963−showDImp impl (PDatadecl n ty cons)
964− = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"
965− ++ showSep "\n\t| "
966− (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)
951+falseTy = sMN 0 "__False"
952+falseDecl = PDatadecl falseTy PType []
953+falseOpts = []
967954
968−getImps :: [PArg] -> [(Name, PTerm)]
969−getImps [] = []
970−getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs
971−getImps (_ : xs) = getImps xs
955+pairTy = sMN 0 "__Pair"
956+pairCon = sMN 0 "__MkPair"
957+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
958+ [("", pairCon, PPi impl (n "A") PType (
959+ PPi impl (n "B") PType (
960+ PPi expl (n "a") (PRef bi (n "A")) (
961+ PPi expl (n "b") (PRef bi (n "B"))
962+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
963+ pexp (PRef bi (n "B"))])))), bi, [])]
964+ where n a = sMN 0 a
965+pairOpts = []
972966
973−getExps :: [PArg] -> [PTerm]
974−getExps [] = []
975−getExps (PExp _ _ tm _ : xs) = tm : getExps xs
976−getExps (_ : xs) = getExps xs
967+eqTy = sUN "="
968+eqCon = sUN "refl"
969+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
970+ (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
971+ PType)
972+ [("", eqCon, PPi impl (n "A") PType (
973+ PPi impl (n "x") (PRef bi (n "A"))
974+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
975+ pimp (n "B") Placeholder False,
976+ pexp (PRef bi (n "x")),
977+ pexp (PRef bi (n "x"))])), bi, [])]
978+ where n a = sMN 0 a
979+eqOpts = []
977980
978−getConsts :: [PArg] -> [PTerm]
979−getConsts [] = []
980−getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
981−getConsts (_ : xs) = getConsts xs
981+elimName = sUN "__Elim"
982+elimMethElimTy = sUN "__elimTy"
983+elimMethElim = sUN "elim"
984+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
985+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
986+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
987+
988+-- Defined in builtins.idr
989+sigmaTy = sUN "Exists"
990+existsCon = sUN "Ex_intro"
991+
992+piBind :: [(Name, PTerm)] -> PTerm -> PTerm
993+piBind = piBindp expl
994+
995+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
996+piBindp p [] t = t
997+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
982998
983−getAll :: [PArg] -> [PTerm]
984−getAll = map getTm
985999
986−-- | Pretty-print a high-level Idris term
1000+-- Pretty-printing declarations and terms
1001+
1002+instance Show PTerm where
1003+ showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm
1004+
1005+instance Show PDecl where
1006+ showsPrec _ d = (displayS . renderCompact . showDeclImp False) d
1007+
1008+instance Show PClause where
1009+ showsPrec _ c = (displayS . renderCompact . showCImp True) c
1010+
1011+instance Show PData where
1012+ showsPrec _ d = (displayS . renderCompact . showDImp False) d
1013+
1014+instance Pretty PTerm OutputAnnotation where
1015+ pretty = prettyImp False
1016+
1017+-- | Colourise annotations according to an Idris state. It ignores the names
1018+-- in the annotation, as there's no good way to show extended information on a
1019+-- terminal.
1020+consoleDecorate :: IState -> OutputAnnotation -> String -> String
1021+consoleDecorate ist _ | not (idris_colourRepl ist) = id
1022+consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist
1023+ in colouriseData theme
1024+consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
1025+ in colouriseType theme
1026+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1027+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1028+consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist
1029+ theme = idris_colourTheme ist
1030+ in case () of
1031+ _ | isDConName n ctxt -> colouriseData theme
1032+ _ | isFnName n ctxt -> colouriseFun theme
1033+ _ | isTConName n ctxt -> colouriseType theme
1034+ _ | otherwise -> id -- don't colourise unknown names
1035+consoleDecorate ist (AnnFC _) = id
1036+
1037+-- | Pretty-print a high-level closed Idris term
9871038prettyImp :: Bool -- ^^ whether to show implicits
9881039 -> PTerm -- ^^ the term to pretty-print
989− -> Doc
990−prettyImp impl = prettySe 10
1040+ -> Doc OutputAnnotation
1041+prettyImp impl = pprintPTerm impl []
1042+
1043+-- | Pretty-print a high-level Idris term in some bindings context
1044+pprintPTerm :: Bool -- ^^ whether to show implicits
1045+ -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1046+ -> PTerm -- ^^ the term to pretty-print
1047+ -> Doc OutputAnnotation
1048+pprintPTerm impl bnd = prettySe 10 bnd
9911049 where
992− prettySe p (PQuote r) =
1050+ prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1051+ prettySe p bnd (PQuote r) =
9931052 if size r > breakingSize then
994− text "![" $$ pretty r <> text "]"
1053+ text "![" <> line <> pretty r <> text "]"
9951054 else
9961055 text "![" <> pretty r <> text "]"
997− prettySe p (PPatvar fc n) = pretty n
998− prettySe p (PRef fc n) =
999− if impl then
1000− pretty n
1001− else
1002− prettyBasic n
1003− where
1004− prettyBasic n@(UN _) = pretty n
1005− prettyBasic (MN _ s) = text (str s)
1006− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n
1007− prettyBasic (SN sn) = text (show sn)
1008− prettySe p (PLam n ty sc) =
1056+ prettySe p bnd (PPatvar fc n) = pretty n
1057+ prettySe p bnd e
1058+ | Just str <- slist p bnd e = str
1059+ | Just n <- snat p e = annotate AnnConstData (text (show n))
1060+ prettySe p bnd (PRef fc n) = prettyName impl bnd n
1061+ prettySe p bnd (PLam n ty sc) =
10091062 bracket p 2 $
10101063 if size sc > breakingSize then
1011− text "λ" <> pretty n <+> text "=>" $+$ pretty sc
1064+ text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc
10121065 else
1013− text "λ" <> pretty n <+> text "=>" <+> pretty sc
1014− prettySe p (PLet n ty v sc) =
1066+ text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc
1067+ prettySe p bnd (PLet n ty v sc) =
10151068 bracket p 2 $
10161069 if size sc > breakingSize then
1017− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
1018− nest nestingSize (prettySe 10 sc)
1070+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>
1071+ nest nestingSize (prettySe 10 ((n, False):bnd) sc)
10191072 else
1020− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
1021− prettySe 10 sc
1022− prettySe p (PPi (Exp l s _ _) n ty sc)
1073+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>
1074+ prettySe 10 ((n, False):bnd) sc
1075+ prettySe p bnd (PPi (Exp l s _ _) n ty sc)
10231076 | n `elem` allNamesIn sc || impl =
10241077 let open = if Lazy `elem` l then text "|" <> lparen else lparen in
10251078 bracket p 2 $
10261079 if size sc > breakingSize then
1027− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
1028− st <+> text "->" $+$ prettySe 10 sc
1080+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1081+ st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
10291082 else
1030− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
1031− st <+> text "->" <+> prettySe 10 sc
1083+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1084+ st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
10321085 | otherwise =
10331086 bracket p 2 $
10341087 if size sc > breakingSize then
1035− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
1088+ prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
10361089 else
1037− prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
1090+ prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
10381091 where
10391092 st =
10401093 case s of
1041− Static -> text "[static]"
1094+ Static -> text "[static]" <> space
10421095 _ -> empty
1043− prettySe p (PPi (Imp l s _ _) n ty sc)
1096+ prettySe p bnd (PPi (Imp l s _ _) n ty sc)
10441097 | impl =
10451098 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
10461099 bracket p 2 $
10471100 if size sc > breakingSize then
1048− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1049− st <+> text "->" <+> prettySe 10 sc
1101+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1102+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
10501103 else
1051− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1052− st <+> text "->" <+> prettySe 10 sc
1053− | otherwise = prettySe 10 sc
1104+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1105+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1106+ | otherwise = prettySe 10 ((n, True):bnd) sc
10541107 where
10551108 st =
10561109 case s of
1057− Static -> text $ "[static]"
1110+ Static -> text "[static]" <> space
10581111 _ -> empty
1059− prettySe p (PPi (Constraint _ _ _) n ty sc) =
1112+ prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =
10601113 bracket p 2 $
10611114 if size sc > breakingSize then
1062− prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
1115+ prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc
10631116 else
1064− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
1065− prettySe p (PPi (TacImp _ _ s _) n ty sc) =
1117+ prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc
1118+ prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =
10661119 bracket p 2 $
10671120 if size sc > breakingSize then
1068− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1069− rbrace <+> text "->" $+$ prettySe 10 sc
1121+ lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>
1122+ rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc
10701123 else
1071− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1072− rbrace <+> text "->" <+> prettySe 10 sc
1073− prettySe p (PApp _ (PRef _ f) [])
1074− | not impl = pretty f
1075− prettySe p (PAppBind _ (PRef _ f) [])
1076− | not impl = text "!" <+> pretty f
1077− prettySe p (PApp _ (PRef _ op@(UN nm)) args)
1078− | not (tnull nm) &&
1124+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1125+ rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc
1126+ prettySe p bnd (PApp _ (PRef _ f) [])
1127+ | not impl = prettyName impl bnd f
1128+ prettySe p bnd (PAppBind _ (PRef _ f) [])
1129+ | not impl = text "!" <> prettyName impl bnd f
1130+ prettySe p bnd (PApp _ (PRef _ op) args)
1131+ | UN nm <- basename op
1132+ , not (tnull nm) &&
10791133 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
10801134 let [l, r] = getExps args in
10811135 bracket p 1 $
10821136 if size r > breakingSize then
1083− prettySe 1 l <+> pretty op $+$ prettySe 0 r
1137+ prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r
10841138 else
1085− prettySe 1 l <+> pretty op <+> prettySe 0 r
1086− prettySe p (PApp _ f as) =
1087− let args = getExps as in
1139+ prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r
1140+ prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1141+ | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1142+ f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1143+ prettySe p bnd (PApp _ f as) =
1144+ let args = getExps as
1145+ fp = prettySe 1 bnd f
1146+ in
10881147 bracket p 1 $
1089− prettySe 1 f <+>
1090− if impl then
1091− foldl' fS empty as
1092− -- foldr (<+>) empty $ map prettyArgS as
1093− else
1094− foldl' fSe empty args
1095− -- foldr (<+>) empty $ map prettyArgSe args
1148+ hsep (if impl
1149+ then fp : map (prettyArgS bnd) as
1150+ else fp : map (prettyArgSe bnd) args)
1151+ prettySe p bnd (PCase _ scr opts) =
1152+ text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
10961153 where
1097− fS l r =
1098− if size r > breakingSize then
1099− l $+$ nest nestingSize (prettyArgS r)
1100− else
1101− l <+> prettyArgS r
1102−
1103− fSe l r =
1104− if size r > breakingSize then
1105− l $+$ nest nestingSize (prettyArgSe r)
1106− else
1107− l <+> prettyArgSe r
1108− prettySe p (PCase _ scr opts) =
1109− text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
1110− where
1111− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
1112−
1113− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
1114− prettySe p (PHidden tm) = text "." <> prettySe 0 tm
1115− prettySe p (PRefl _ _) = text "refl"
1116− prettySe p (PResolveTC _) = text "resolvetc"
1117− prettySe p (PTrue _) = text "()"
1118− prettySe p (PFalse _) = text "_|_"
1119− prettySe p (PEq _ l r) =
1154+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1155+
1156+ sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1157+ prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1158+ prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
1159+ prettySe p bnd (PResolveTC _) = text "resolvetc"
1160+ prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
1161+ prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
1162+ prettySe p bnd (PEq _ l r) =
11201163 bracket p 2 $
11211164 if size r > breakingSize then
1122− prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
1165+ prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)
11231166 else
1124− prettySe 10 l <+> text "=" <+> prettySe 10 r
1125− prettySe p (PRewrite _ l r _) =
1167+ prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r
1168+ where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
1169+ prettySe p bnd (PRewrite _ l r _) =
11261170 bracket p 2 $
11271171 if size r > breakingSize then
1128− text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)
1172+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)
11291173 else
1130− text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r
1131− prettySe p (PTyped l r) =
1132− lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
1133− prettySe p (PPair _ l r) =
1174+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1175+ prettySe p bnd (PTyped l r) =
1176+ lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1177+ prettySe p bnd (PPair _ l r) =
11341178 if size r > breakingSize then
1135− lparen <> prettySe 10 l <> text "," $+$
1136− prettySe 10 r <> rparen
1179+ lparen <> prettySe 10 bnd l <> text "," <>
1180+ line <> prettySe 10 bnd r <> rparen
11371181 else
1138− lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
1139− prettySe p (PDPair _ l t r) =
1182+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
1183+ prettySe p bnd (PDPair _ l t r) =
11401184 if size r > breakingSize then
1141− lparen <> prettySe 10 l <+> text "**" $+$
1142− prettySe 10 r <> rparen
1185+ lparen <> prettySe 10 bnd l <+> text "**" <>
1186+ line <> prettySe 10 bnd r <> rparen
11431187 else
1144− lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
1145− prettySe p (PAlternative a as) =
1188+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1189+ prettySe p bnd (PAlternative a as) =
11461190 lparen <> text "|" <> prettyAs <> text "|" <> rparen
11471191 where
11481192 prettyAs =
1149− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
1150− prettySe p PType = text "Type"
1151− prettySe p (PConstant c) = pretty c
1193+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1194+ prettySe p bnd PType = annotate AnnConstType $ text "Type"
1195+ prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))
1196+ where annot (AType _) = AnnConstType
1197+ annot StrType = AnnConstType
1198+ annot PtrType = AnnConstType
1199+ annot VoidType = AnnConstType
1200+ annot _ = AnnConstData
11521201 -- XXX: add pretty for tactics
1153− prettySe p (PProof ts) =
1154− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1155− prettySe p (PTactics ts) =
1156− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1157− prettySe p (PMetavar n) = text "?" <> pretty n
1158− prettySe p (PReturn f) = text "return"
1159− prettySe p PImpossible = text "impossible"
1160− prettySe p Placeholder = text "_"
1161− prettySe p (PDoBlock _) = text "do block pretty not implemented"
1162− prettySe p (PElabError s) = pretty s
1163−
1164− prettySe p _ = text "test"
1165−
1166− prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)
1167− prettyArgS (PExp _ _ tm _) = prettyArgSe tm
1168− prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
1169− prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
1170−
1171− prettyArgSe arg = prettySe 0 arg
1172− prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1173− prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1174− prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1202+ prettySe p bnd (PProof ts) =
1203+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1204+ prettySe p bnd (PTactics ts) =
1205+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1206+ prettySe p bnd (PMetavar n) = text "?" <> pretty n
1207+ prettySe p bnd (PReturn f) = text "return"
1208+ prettySe p bnd PImpossible = text "impossible"
1209+ prettySe p bnd Placeholder = text "_"
1210+ prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1211+ prettySe p bnd (PElabError s) = pretty s
1212+
1213+ prettySe p bnd _ = text "test"
1214+
1215+ prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)
1216+ prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm
1217+ prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm
1218+ prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)
1219+
1220+ prettyArgSe bnd arg = prettySe 0 bnd arg
1221+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1222+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1223+ prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1224+
1225+ basename :: Name -> Name
1226+ basename (NS n _) = basename n
1227+ basename n = n
1228+
1229+ slist' p bnd (PApp _ (PRef _ nil) _)
1230+ | not impl && nsroot nil == sUN "Nil" = Just []
1231+ slist' p bnd (PApp _ (PRef _ cons) args)
1232+ | nsroot cons == sUN "::",
1233+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1234+ all isImp imps,
1235+ Just tl' <- slist' p bnd tl
1236+ = Just (hd:tl')
1237+ where
1238+ isImp (PImp {}) = True
1239+ isImp _ = False
1240+ slist' _ _ _ = Nothing
1241+
1242+ slist p bnd e | Just es <- slist' p bnd e = Just $
1243+ case es of [] -> annotate AnnConstData $ text "[]"
1244+ [x] -> enclose left
1245+ right
1246+ (prettySe p bnd x)
1247+ xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs
1248+ where left = (annotate AnnConstData (text "["))
1249+ right = (annotate AnnConstData (text "]"))
1250+ comma = (annotate AnnConstData (text ","))
1251+ slist _ _ _ = Nothing
1252+
1253+ natns = "Prelude.Nat."
1254+
1255+ snat p (PRef _ z)
1256+ | show z == (natns++"Z") || show z == "Z" = Just 0
1257+ snat p (PApp _ s [PExp {getTm=n}])
1258+ | show s == (natns++"S") || show s == "S",
1259+ Just n' <- snat p n
1260+ = Just $ 1 + n'
1261+ snat _ _ = Nothing
11751262
11761263 bracket outer inner doc
11771264 | inner > outer = lparen <> doc <> rparen
11781265 | otherwise = doc
11791266
1267+-- | Pretty-printer helper for the binding site of a name
1268+bindingOf :: Name -- ^^ the bound name
1269+ -> Bool -- ^^ whether the name is implicit
1270+ -> Doc OutputAnnotation
1271+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1272+
1273+-- | Pretty-printer helper for names that attaches the correct annotations
1274+prettyName :: Bool -- ^^ whether to show namespaces
1275+ -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1276+ -> Name -- ^^ the name to pprint
1277+ -> Doc OutputAnnotation
1278+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
1279+ | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))
1280+ where strName (UN n) = T.unpack n
1281+ strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1282+ | otherwise = strName n
1283+ strName (MN i s) = T.unpack s
1284+ strName other = show other
1285+
1286+
1287+showCImp :: Bool -> PClause -> Doc OutputAnnotation
1288+showCImp impl (PClause _ n l ws r w)
1289+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r
1290+ <+> text "where" <+> text (show w)
1291+ where
1292+ showWs [] = empty
1293+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1294+showCImp impl (PWith _ n l ws r w)
1295+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r
1296+ <+> braces (text (show w))
1297+ where
1298+ showWs [] = empty
1299+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1300+
1301+
1302+showDImp :: Bool -> PData -> Doc OutputAnnotation
1303+showDImp impl (PDatadecl n ty cons)
1304+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>
1305+ (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))
1306+
1307+showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
1308+showDecls i ds = vsep (map (showDeclImp i) ds)
1309+
1310+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1311+showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t
1312+showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1313+ indent 2 (vsep (map (showCImp i) cs))
1314+showDeclImp _ (PData _ _ _ _ d) = showDImp True d
1315+showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)
1316+showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)
1317+showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1318+showDeclImp i (PClass _ _ _ cs n ps ds)
1319+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds
1320+showDeclImp i (PInstance _ _ cs n _ t _ ds)
1321+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds
1322+showDeclImp _ _ = text "..."
1323+-- showDeclImp (PImport i) = "import " ++ i
1324+
1325+instance Show (Doc OutputAnnotation) where
1326+ show = flip (displayS . renderCompact) ""
1327+
1328+getImps :: [PArg] -> [(Name, PTerm)]
1329+getImps [] = []
1330+getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs
1331+getImps (_ : xs) = getImps xs
1332+
1333+getExps :: [PArg] -> [PTerm]
1334+getExps [] = []
1335+getExps (PExp _ _ tm _ : xs) = tm : getExps xs
1336+getExps (_ : xs) = getExps xs
1337+
1338+getConsts :: [PArg] -> [PTerm]
1339+getConsts [] = []
1340+getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
1341+getConsts (_ : xs) = getConsts xs
1342+
1343+getAll :: [PArg] -> [PTerm]
1344+getAll = map getTm
1345+
1346+
11801347-- | Show Idris name
11811348showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
11821349 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
@@ -1206,171 +1373,14 @@ showName ist bnd impl colour n = case ist of
12061373 -- (like error messages). Thus, unknown vars are colourised as implicits.
12071374 | otherwise -> colouriseImplicit t name
12081375
1209−-- | Show Idris term
1210−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours
1211− -> Bool -- ^^ whether to show implicits
1212− -> Bool -- ^^ whether to colourise
1213− -> PTerm -- ^^ the term to show
1214− -> String
1215−showImp ist impl colour tm = se 10 [] tm where
1216− perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
1217− perhapsColourise col str = case ist of
1218− Just i -> if colour then col (idris_colourTheme i) str else str
1219− Nothing -> str
1220−
1221− se :: Int -> [(Name, Bool)] -> PTerm -> String
1222− se p bnd (PQuote r) = "![" ++ show r ++ "]"
1223− se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1224− se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1225− se p bnd e
1226− | Just str <- slist p bnd e = str
1227− | Just num <- snat p e = perhapsColourise colouriseData (show num)
1228− se p bnd (PRef fc n) = showName ist bnd impl colour n
1229− se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1230− (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1231− ++ se 10 ((n, False):bnd) sc
1232− se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1233− " = " ++ se 10 bnd v ++
1234− " in " ++ se 10 ((n, False):bnd) sc
1235− se p bnd (PPi (Exp l s _ param) n ty sc)
1236− | n `elem` allNamesIn sc || impl
1237− = bracket p 2 $
1238− (if Lazy `elem` l then "|(" else "(") ++
1239− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1240− ") " ++
1241− (if (impl && param) then "P" else "") ++
1242− st ++
1243− "-> " ++ se 10 ((n, False):bnd) sc
1244− | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
1245− where st = case s of
1246− Static -> "[static] "
1247− _ -> ""
1248− se p bnd (PPi (Imp l s _ _) n ty sc)
1249− | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++
1250− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1251− "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
1252− | otherwise = se 10 ((n, True):bnd) sc
1253− where st = case s of
1254− Static -> "[static] "
1255− _ -> ""
1256− se p bnd (PPi (Constraint _ _ _) n ty sc)
1257− = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
1258− se p bnd (PPi (TacImp _ _ s _) n ty sc)
1259− = bracket p 2 $
1260− "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1261− se 10 ((n, False):bnd) sc
1262− se p bnd (PMatchApp _ f) = "match " ++ show f
1263− se p bnd (PApp _ hd@(PRef fc f) [tm])
1264− | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1265− f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))
1266− se p bnd (PApp _ hd@(PRef _ f) [])
1267− | not impl = se p bnd hd
1268− se p bnd (PAppBind _ hd@(PRef _ f) [])
1269− | not impl = "!" ++ se p bnd hd
1270− se p bnd (PApp _ op@(PRef _ (UN nm)) args)
1271− | not (tnull nm) &&
1272− length (getExps args) == 2 && not impl && not (isAlpha (thead nm))
1273− = let [l, r] = getExps args in
1274− bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r
1275− se p bnd (PApp _ f as)
1276− = -- let args = getExps as in
1277− bracket p 1 $ se 1 bnd f ++
1278− if impl then concatMap (sArg bnd) as
1279− else concatMap (suiArg impl bnd) as
1280− se p bnd (PAppBind _ f as)
1281− = let args = getExps as in
1282− "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
1283− else concatMap (seArg bnd) args)
1284− se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1285− where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1286− se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1287− se p bnd (PRefl _ t)
1288− | not impl = perhapsColourise colouriseData "refl"
1289− | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
1290− se p bnd (PResolveTC _) = "resolvetc"
1291− se p bnd (PTrue _) = perhapsColourise colouriseType "()"
1292− se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"
1293− se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r
1294− se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
1295− se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
1296− se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
1297− se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
1298− se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
1299− se p bnd PType = perhapsColourise colouriseType "Type"
1300− se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)
1301− where cfun (AType _) = colouriseType
1302− cfun StrType = colouriseType
1303− cfun PtrType = colouriseType
1304− cfun VoidType = colouriseType
1305− cfun _ = colouriseData
1306− se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
1307− se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
1308− se p bnd (PMetavar n) = "?" ++ show n
1309− se p bnd (PReturn f) = "return"
1310− se p bnd PImpossible = "impossible"
1311− se p bnd Placeholder = "_"
1312− se p bnd (PDoBlock _) = "do block show not implemented"
1313− se p bnd (PElabError s) = show s
1314− se p bnd (PCoerced t) = se p bnd t
1315− se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
1316− se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t
1317− se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t
1318−-- se p bnd x = "Not implemented"
1319−
1320− slist' p bnd (PApp _ (PRef _ nil) _)
1321− | not impl && nsroot nil == sUN "Nil" = Just []
1322− slist' p bnd (PApp _ (PRef _ cons) args)
1323− | nsroot cons == sUN "::",
1324− (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1325− all isImp imps,
1326− Just tl' <- slist' p bnd tl
1327− = Just (hd:tl')
1328− where
1329− isImp (PImp {}) = True
1330− isImp _ = False
1331− slist' _ _ _ = Nothing
1332−
1333− slist p bnd e | Just es <- slist' p bnd e = Just $
1334− case es of [] -> "[]"
1335− [x] -> "[" ++ se p bnd x ++ "]"
1336− xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
1337− slist _ _ _ = Nothing
1338−
1339− -- since Prelude is always imported, S & Z are unqualified iff they're the
1340− -- Nat ones.
1341− snat p (PRef _ o)
1342− | show o == (natns++"Z") || show o == "Z" = Just 0
1343− snat p (PApp _ s [PExp {getTm=n}])
1344− | show s == (natns++"S") || show s == "S",
1345− Just n' <- snat p n
1346− = Just $ 1 + n'
1347− snat _ _ = Nothing
1348−
1349− natns = "Prelude.Nat."
1376+showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1377+ -> PTerm -- ^^ the term to show
1378+ -> String
1379+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))
13501380
1351− sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)
1352− sArg bnd (PExp _ _ tm _) = seArg bnd tm
1353− sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
1354− sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
1355−
1356− -- show argument, implicits given by the user also shown
1357− suiArg impl bnd (PImp _ mi _ n tm _)
1358− | impl || not mi = siArg bnd (n, tm)
1359− suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm
1360− suiArg impl bnd _ = ""
1361−
1362− seArg bnd arg = " " ++ se 0 bnd arg
1363− siArg bnd (n, val) =
1364− let n' = show n
1365− val' = se 10 bnd val in
1366− if (n' == val')
1367− then " {" ++ n' ++ "}"
1368− else " {" ++ n' ++ " = " ++ val' ++ "}"
1369− scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
1370− stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
1371−
1372− bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1373− | otherwise = str
1381+-- | Show a term with implicits, no colours
1382+showTmImpls :: PTerm -> String
1383+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""
13741384
13751385
13761386instance Sized PTerm where
src/Idris/CaseSplit.hs+3−3
@@ -62,11 +62,11 @@ split n t'
6262 Just ty ->
6363 do let splits = findPats ist ty
6464 iLOG ("New patterns " ++ showSep ", "
65− (map (showImp Nothing True False) splits))
65+ (map showTmImpls splits))
6666 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
6767 logLvl 4 ("Working from " ++ show t)
6868 logLvl 4 ("Trying " ++ showSep "\n"
69− (map (showImp Nothing True False) newPats_in))
69+ (map (showTmImpls) newPats_in))
7070 newPats <- mapM elabNewPat newPats_in
7171 logLvl 3 ("Original:\n" ++ show t)
7272 logLvl 3 ("Split:\n" ++
@@ -237,7 +237,7 @@ splitOnLine l n fn = do
237237-- let (before, later) = splitAt (l-1) (lines inp)
238238-- i <- getIState
239239 cl <- getInternalApp fn l
240− logLvl 3 ("Working with " ++ showImp Nothing True False cl)
240+ logLvl 3 ("Working with " ++ showTmImpls cl)
241241 tms <- split n cl
242242-- iputStrLn (showSep "\n" (map show tms))
243243 return tms -- "" -- not yet done...
src/Idris/Core/Elaborate.hs+1−1
@@ -24,7 +24,7 @@ import Data.Char
2424import Data.List
2525import Debug.Trace
2626
27−import Util.Pretty
27+import Util.Pretty hiding (fill)
2828
2929-- I don't really want this here, but it's useful for the test shell
3030data Command = Theorem Name Raw
src/Idris/Core/ProofState.hs+12−12
@@ -18,7 +18,7 @@ import Control.Applicative hiding (empty)
1818import Data.List
1919import Debug.Trace
2020
21−import Util.Pretty
21+import Util.Pretty hiding (fill)
2222
2323data ProofState = PS { thname :: Name,
2424 holes :: [Name], -- holes still to be solved
@@ -113,23 +113,23 @@ instance Show ProofState where
113113 " =?= " ++ showEnv ps v
114114 showG ps b = showEnv ps (binderTy b)
115115
116−instance Pretty ProofState where
116+instance Pretty ProofState OutputAnnotation where
117117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
118118 if size nm > breakingSize then
119− pretty nm <> colon $$ nest nestingSize (text " no more goals.")
119+ pretty nm <+> colon <+> nest nestingSize (text " no more goals.")
120120 else
121− pretty nm <> colon <+> text " no more goals."
121+ pretty nm <+> colon <+> text " no more goals."
122122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =
123123 let OK g = goal (Just h) tm in
124124 let wkEnv = premises g in
125− text "Other goals" <+> colon <+> pretty hs $$
126− prettyPs wkEnv (reverse wkEnv) $$
127− text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
125+ text "Other goals" <+> colon <+> pretty hs <+>
126+ prettyPs wkEnv (reverse wkEnv) <+>
127+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
128128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
129129 where
130130 prettyGoal ps (Guess t v) =
131131 if size v > breakingSize then
132− prettyEnv ps t <+> text "=?=" $$
132+ prettyEnv ps t <+> text "=?=" <+>
133133 nest nestingSize (prettyEnv ps v)
134134 else
135135 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
@@ -139,17 +139,17 @@ instance Pretty ProofState where
139139 prettyPs env ((n, Let t v):bs) =
140140 nest nestingSize (pretty n <+> colon <+>
141141 if size v > breakingSize then
142− prettyEnv env t <+> text "=" $$
143− nest nestingSize (prettyEnv env v) $$
142+ prettyEnv env t <+> text "=" <+>
143+ nest nestingSize (prettyEnv env v) <+>
144144 nest nestingSize (prettyPs env bs)
145145 else
146− prettyEnv env t <+> text "=" <+> prettyEnv env v $$
146+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
147147 nest nestingSize (prettyPs env bs))
148148 prettyPs env ((n, b):bs) =
149149 if size (binderTy b) > breakingSize then
150150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
151151 else
152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
152+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
153153 nest nestingSize (prettyPs env bs))
154154
155155same Nothing n = True
src/Idris/Core/TT.hs+33−19
@@ -77,6 +77,16 @@ instance Sized FC where
7777instance Show FC where
7878 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
7979
80+-- | Output annotation for pretty-printed name - decides colour
81+data NameOutput = TypeOutput | FunOutput | DataOutput
82+
83+-- | Output annotations for pretty-printing
84+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)
85+ | AnnBoundName Name Bool
86+ | AnnConstData
87+ | AnnConstType
88+ | AnnFC FC
89+
8090-- | Used for error reflection
8191data ErrorReportPart = TextPart String
8292 | NamePart Name
@@ -177,15 +187,15 @@ instance Show Err where
177187 show (At f e) = show f ++ ":" ++ show e
178188 show _ = "Error"
179189
180−instance Pretty Err where
190+instance Pretty Err OutputAnnotation where
181191 pretty (Msg m) = text m
182192 pretty (CantUnify _ l r e _ i) =
183193 if size l + size r > breakingSize then
184− text "Cannot unify" <+> colon $$
185− nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
194+ text "Cannot unify" <+> colon <+>
195+ nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>
186196 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
187197 else
188− text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
198+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
189199 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
190200 pretty (ProviderError msg) = text msg
191201 pretty err@(LoadingFailed _ _) = text (show err)
@@ -196,11 +206,11 @@ instance Error Err where
196206
197207type TC = TC' Err
198208
199−instance (Pretty a) => Pretty (TC a) where
209+instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
200210 pretty (OK ok) = pretty ok
201211 pretty (Error err) =
202212 if size err > breakingSize then
203− text "Error" <+> colon $$ (nest nestingSize $ pretty err)
213+ text "Error" <+> colon <+> (nest nestingSize $ pretty err)
204214 else
205215 text "Error" <+> colon <+> pretty err
206216
@@ -294,11 +304,15 @@ instance Sized Name where
294304 size (MN i n) = 1
295305 size _ = 1
296306
297−instance Pretty Name where
298− pretty (UN n) = text (T.unpack n)
299− pretty (NS n s) = pretty n
300− pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
301− pretty (SN s) = text (show s)
307+instance Pretty Name OutputAnnotation where
308+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')
309+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un
310+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $
311+ lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
312+ pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)
313+
314+instance Pretty [Name] OutputAnnotation where
315+ pretty = encloseSep empty empty comma . map pretty
302316
303317instance Show Name where
304318 show (UN n) = str n
@@ -417,7 +431,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
417431data NativeTy = IT8 | IT16 | IT32 | IT64
418432 deriving (Show, Eq, Ord, Enum)
419433
420−instance Pretty NativeTy where
434+instance Pretty NativeTy OutputAnnotation where
421435 pretty IT8 = text "Bits8"
422436 pretty IT16 = text "Bits16"
423437 pretty IT32 = text "Bits32"
@@ -435,7 +449,7 @@ deriving instance NFData NativeTy
435449deriving instance NFData ArithTy
436450!-}
437451
438−instance Pretty ArithTy where
452+instance Pretty ArithTy OutputAnnotation where
439453 pretty (ATInt ITNative) = text "Int"
440454 pretty (ATInt ITBig) = text "BigInt"
441455 pretty (ATInt ITChar) = text "Char"
@@ -471,7 +485,7 @@ deriving instance NFData Const
471485instance Sized Const where
472486 size _ = 1
473487
474−instance Pretty Const where
488+instance Pretty Const OutputAnnotation where
475489 pretty (I i) = text . show $ i
476490 pretty (BI i) = text . show $ i
477491 pretty (Fl f) = text . show $ f
@@ -503,7 +517,7 @@ instance Sized Raw where
503517 size (RForce raw) = 1 + size raw
504518 size (RConstant const) = size const
505519
506−instance Pretty Raw where
520+instance Pretty Raw OutputAnnotation where
507521 pretty = text . show
508522
509523{-!
@@ -621,7 +635,7 @@ deriving instance NFData NameType
621635instance Sized NameType where
622636 size _ = 1
623637
624−instance Pretty NameType where
638+instance Pretty NameType OutputAnnotation where
625639 pretty = text . show
626640
627641instance Eq NameType where
@@ -687,7 +701,7 @@ instance Sized a => Sized (TT a) where
687701 size Erased = 1
688702 size (TType u) = 1 + size u
689703
690−instance Pretty a => Pretty (TT a) where
704+instance Pretty a o => Pretty (TT a) o where
691705 pretty _ = text "test"
692706
693707type EnvTT n = [(n, Binder (TT n))]
@@ -1042,7 +1056,7 @@ prettyEnv env t = prettyEnv' env t False
10421056 prettySe p env (P nt n t) debug =
10431057 pretty n <+>
10441058 if debug then
1045− lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
1059+ lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket
10461060 else
10471061 empty
10481062 prettySe p env (V i) debug
@@ -1050,7 +1064,7 @@ prettyEnv env t = prettyEnv' env t False
10501064 if debug then
10511065 text . show . fst $ env!!i
10521066 else
1053− lbrack <+> text (show i) <+> rbrack
1067+ lbracket <+> text (show i) <+> rbracket
10541068 | otherwise = text "unbound" <+> text (show i) <+> text "!"
10551069 prettySe p env (Bind n b@(Pi t) sc) debug
10561070 | noOccurrence n sc && not debug =
src/Idris/Coverage.hs+3−3
@@ -50,7 +50,7 @@ genClauses fc n xs given
5050 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
5151 logLvl 10 $ show argss ++ "\n" ++ show all_args
5252 logLvl 10 $ "Original: \n" ++
53− showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)
53+ showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
5454 -- add an infinite supply of explicit arguments to update the possible
5555 -- cases for (the return type may be variadic, or function type, sp
5656 -- there may be more case splitting that the idris_implicits record
@@ -60,10 +60,10 @@ genClauses fc n xs given
6060 _ -> repeat (pexp Placeholder)
6161 let tryclauses = mkClauses parg all_args
6262 logLvl 2 $ show (length tryclauses) ++ " initially to check"
63− logLvl 5 $ showSep "\n" (map (showImp Nothing True False) tryclauses)
63+ logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)
6464 let new = filter (noMatch i) (nub tryclauses)
6565 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
66− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)
66+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
6767-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
6868 return new
6969-- return (map (\t -> PClause n t [] PImpossible []) new)
src/Idris/Delaborate.hs+109−103
@@ -1,10 +1,12 @@
11{-# LANGUAGE PatternGuards #-}
22
3−module Idris.Delaborate where
3+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where
44
55-- Convert core TT back into high level syntax, primarily for display
66-- purposes.
77
8+import Util.Pretty
9+
810import Idris.AbsSyntax
911import Idris.Core.TT
1012import Idris.Core.Evaluate
@@ -33,7 +35,7 @@ delab' :: IState -> Term -> Bool -> Bool -> PTerm
3335delab' i t f mvs = delabTy' i [] t f mvs
3436
3537delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
36− -> Term
38+ -> Term
3739 -> Bool -- ^ use full names
3840 -> Bool -- ^ Don't treat metavariables specially
3941 -> PTerm
@@ -50,8 +52,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
5052 | Just n' <- lookup n env = PRef un n'
5153 | otherwise
5254 = case lookup n (idris_metavars ist) of
53− Just (Just _, mi, _) -> mkMVApp (dens n) []
54− _ -> PRef un (dens n)
55+ Just (Just _, mi, _) -> mkMVApp n []
56+ _ -> PRef un n
5557 de env _ (Bind n (Lam ty) sc)
5658 = PLam n (de env [] ty) (de ((n,n):env) [] sc)
5759 de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)
@@ -96,9 +98,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
9698 deFn env (P _ n _) args | not mvs
9799 = case lookup n (idris_metavars ist) of
98100 Just (Just _, mi, _) ->
99− mkMVApp (dens n) (drop mi (map (de env []) args))
100− _ -> mkPApp (dens n) (map (de env []) args)
101− | otherwise = mkPApp (dens n) (map (de env []) args)
101+ mkMVApp n (drop mi (map (de env []) args))
102+ _ -> mkPApp n (map (de env []) args)
103+ | otherwise = mkPApp n (map (de env []) args)
102104 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
103105
104106 mkMVApp n []
@@ -115,105 +117,109 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
115117 imp (PConstraint p l _ d) arg = PConstraint p l arg d
116118 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
117119
120+-- | How far to indent sub-errors
121+errorIndent :: Int
122+errorIndent = 8
118123
119−indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
120− boxIt c text = (c:text) ++ if last text == c
121− then ""
122− else [c]
124+-- | Actually indent a sub-error - no line at end because a newline can end
125+-- multiple layers of indent
126+indented :: Doc a -> Doc a
127+indented = nest errorIndent . (line <>)
123128
124−pshow :: IState -> Err -> String
125−pshow i err = pshow' i (fmap (errReverse i) err)
126−
127−pshow' i (Msg s) = s
128−pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
129− "\nThis is probably a bug, or a missing error message.\n" ++
130− "Please consider reporting at " ++ bugaddr
131−pshow' i (CantUnify _ x y e sc s)
132− = let imps = opt_showimp (idris_options i) in
133− let colour = idris_colourRepl i in
134− "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
135− ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++
136−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
137− case e of
138− Msg "" -> ""
139− _ -> "\nSpecifically:" ++
140− indented (pshow' i e) ++
141− if (opt_errContext (idris_options i)) then showSc i sc else ""
142−pshow' i (CantConvert x y env)
143− = let imps = opt_showimp (idris_options i) in
144− let colour = idris_colourRepl i in
145− "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
146− ++ indented (showImp (Just i) imps colour (delab i y)) ++
147− if (opt_errContext (idris_options i)) then showSc i env else ""
148−pshow' i (CantSolveGoal x env)
149− = let imps = opt_showimp (idris_options i) in
150− let colour = idris_colourRepl i in
151− "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++
152− if (opt_errContext (idris_options i)) then showSc i env else ""
153−pshow' i (UnifyScope n out tm env)
154− = let imps = opt_showimp (idris_options i) in
155− let colour = idris_colourRepl i in
156− "Can't unify" ++ indented (show n) ++ "with"
157− ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
158− indented (show out) ++ "is not in scope" ++
159− if (opt_errContext (idris_options i)) then showSc i env else ""
160−pshow' i (CantInferType t)
161− = "Can't infer type for " ++ t
162−pshow' i (NonFunctionType f ty)
163− = let imps = opt_showimp (idris_options i) in
164− let colour = idris_colourRepl i in
165− showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
166− ++ showImp (Just i) imps colour (delab i ty) ++ ")"
167−pshow' i (NotEquality tm ty)
168− = let imps = opt_showimp (idris_options i) in
169− let colour = idris_colourRepl i in
170− showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("
171− ++ showImp (Just i) imps colour (delab i ty) ++ ")"
172−pshow' i (TooManyArguments f)
173− = "Too many arguments for " ++ show f
174−pshow' i (CantIntroduce ty)
175− = let imps = opt_showimp (idris_options i) in
176− let colour = idris_colourRepl i in
177− "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
178−pshow' i (InfiniteUnify x tm env)
179− = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
180− " would lead to infinite value" ++
181− if (opt_errContext (idris_options i)) then showSc i env else ""
182−pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
183− " when unifying " ++ show (delab i x) ++ " and " ++
184− show (delab i y)
185−pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
186−pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
187−pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n
188−pshow' i (NoSuchVariable n) = "No such variable " ++ show n
189−pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
190−pshow' i UniverseError = "Universe inconsistency"
191−pshow' i ProgramLineComment = "Program line next to comment"
192−pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
193−pshow' i (NonCollapsiblePostulate n)
194− = "The return type of postulate " ++ show n ++ " is not collapsible"
195−pshow' i (AlreadyDefined n) = show n ++ " is already defined"
196−pshow' i (ProofSearchFail e) = pshow' i e
197−pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
198−pshow' i (At f e) = show f ++ ":" ++ pshow' i e
199−pshow' i (Elaborating s n e) = "When elaborating " ++ s ++
200− showqual i n ++ ":\n" ++ pshow' i e
201−pshow' i (ProviderError msg) = "Type provider error: " ++ msg
202−pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e
203−pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
204− concat (intersperse "\n" parts') ++
205− "\nOriginal error:\n" ++ indented (pshow' i orig)
206− where showPart :: ErrorReportPart -> String
207− showPart (TextPart str) = str
208− showPart (NamePart n) = let colour = idris_colourRepl i in
209− showName (Just i) [] False colour n
210− showPart (TermPart tm) = let colour = idris_colourRepl i
211− in showImp (Just i) False colour (delab i tm)
212− showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
213−pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
214− indented (pshow' i err) ++
215− "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
129+pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
130+pprintTerm ist = prettyImp (opt_showimp (idris_options ist))
216131
132+pshow :: IState -> Err -> String
133+pshow ist err = displayDecorated (consoleDecorate ist) .
134+ renderPretty 1.0 80 .
135+ fmap (fancifyAnnots ist) $ pprintErr ist err
136+
137+pprintErr :: IState -> Err -> Doc OutputAnnotation
138+pprintErr i err = pprintErr' i (fmap (errReverse i) err)
139+
140+pprintErr' i (Msg s) = text s
141+pprintErr' i (InternalMsg s) =
142+ vsep [ text "INTERNAL ERROR:" <+> text s,
143+ text "This is probably a bug, or a missing error message.",
144+ text ("Please consider reporting at " ++ bugaddr)
145+ ]
146+pprintErr' i (CantUnify _ x y e sc s) =
147+ text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>
148+ text "with" <> indented (pprintTerm i (delab i y)) <>
149+ case e of
150+ Msg "" -> empty
151+ _ -> line <> line <> text "Specifically:" <>
152+ indented (pprintErr' i e) <>
153+ if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
154+pprintErr' i (CantConvert x y env) =
155+ text "Can't convert" <> indented (pprintTerm i (delab i x)) <>
156+ text "with" <> indented (pprintTerm i (delab i y)) <>
157+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty
158+pprintErr' i (UnifyScope n out tm env) =
159+ text "Can't unify" <> indented (annName n) <+>
160+ text "with" <> indented (pprintTerm i (delab i tm)) <+>
161+ text "as" <> indented (annName out) <> text "is not in scope" <>
162+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty
163+pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
164+pprintErr' i (NonFunctionType f ty) =
165+ pprintTerm i (delab i f) <+>
166+ text "does not have a function type" <+>
167+ parens (pprintTerm i (delab i ty))
168+pprintErr' i (NotEquality tm ty) =
169+ pprintTerm i (delab i tm) <+>
170+ text "does not have an equality type" <+>
171+ parens (pprintTerm i (delab i ty))
172+pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
173+pprintErr' i (CantIntroduce ty) =
174+ text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
175+pprintErr' i (InfiniteUnify x tm env) =
176+ text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
177+ text "would lead to infinite value" <>
178+ if (opt_errContext (idris_options i)) then text (showSc i env) else empty
179+pprintErr' i (NotInjective p x y) =
180+ text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
181+ text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
182+ pprintTerm i (delab i y)
183+pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
184+pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
185+ cat (punctuate comma (map text as))
186+pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
187+pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
188+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
189+pprintErr' i UniverseError = text "Universe inconsistency"
190+pprintErr' i ProgramLineComment = text "Program line next to comment"
191+pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
192+pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>
193+ annName n <+> text "is not collapsible"
194+pprintErr' i (AlreadyDefined n) = annName n<+>
195+ text "is already defined"
196+pprintErr' i (ProofSearchFail e) = pprintErr' i e
197+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)
198+pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
199+pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
200+ annName' n (showqual i n) <> colon <$>
201+ pprintErr' i e
202+pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)
203+pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+> pprintErr' i e
204+pprintErr' i (ReflectionError parts orig) =
205+ let parts' = map (hsep . map showPart) parts in
206+ vsep parts' <> line <> line <>
207+ text "Original error:" <$> indented (pprintErr' i orig)
208+ where showPart :: ErrorReportPart -> Doc OutputAnnotation
209+ showPart (TextPart str) = text str
210+ showPart (NamePart n) = annName n
211+ showPart (TermPart tm) = pprintTerm i (delab i tm)
212+ showPart (SubReport rs) = indented . hsep . map showPart $ rs
213+pprintErr' i (ReflectionFailed msg err) =
214+ text "When attempting to perform error reflection, the following internal error occurred:" <>
215+ indented (pprintErr' i err) <>
216+ text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
217+
218+annName :: Name -> Doc OutputAnnotation
219+annName n = annName' n (show n)
220+
221+annName' :: Name -> String -> Doc OutputAnnotation
222+annName' n str = annotate (AnnName n Nothing Nothing) (text str)
217223
218224showSc i [] = ""
219225showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))
src/Idris/ElabDecls.hs+32−32
@@ -67,12 +67,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
6767 ctxt <- getContext
6868 i <- getIState
6969
70− logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'
70+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
7171 ty' <- addUsingConstraints syn fc ty'
7272 ty' <- implicit syn n ty'
7373
7474 let ty = addImpl i ty'
75− logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
75+ logLvl 2 $ show n ++ " type " ++ showTmImpls ty
7676 ((tyT, defer, is), log) <-
7777 tclift $ elaborate ctxt n (TType (UVal 0)) []
7878 (errAt "type of " n (erun fc (build i info False [] n ty)))
@@ -326,10 +326,10 @@ elabEliminator paramPos n ty cons info = do
326326 let clauseConsElimArgs = map getPiName consTerms
327327 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
328328 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
329− let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy
329+ let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
330330 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
331331 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
332− elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
332+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
333333 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
334334 -- Do not elaborate clauses if there aren't any
335335 case eliminatorClauses of
@@ -814,7 +814,7 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
814814 i <- getIState
815815 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
816816 let t = addImpl i t_in
817− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
817+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
818818 ((t', defer, is), log) <-
819819 tclift $ elaborate ctxt n (TType (UVal 0)) []
820820 (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -959,9 +959,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
959959 missing' <- filterM (checkPossible info fc True n) missing
960960 let clhs = map getLHS pdef
961961 logLvl 2 $ "Must be unreachable:\n" ++
962− showSep "\n" (map (showImp Nothing True False) missing') ++
962+ showSep "\n" (map showTmImpls missing') ++
963963 "\nAgainst: " ++
964− showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
964+ showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
965965 -- filter out anything in missing' which is
966966 -- matched by any of clhs. This might happen since
967967 -- unification may force a variable to take a
@@ -1125,8 +1125,8 @@ elabPE info fc caller r =
11251125 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
11261126 showSep "\n"
11271127 (map (\ (lhs, rhs) ->
1128− (showImp Nothing True False lhs ++ " = " ++
1129− showImp Nothing True False rhs)) pats)
1128+ (showTmImpls lhs ++ " = " ++
1129+ showTmImpls rhs)) pats)
11301130 elabType info defaultSyntax "" fc opts newnm specTy
11311131 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
11321132 elabClauses info fc opts newnm def
@@ -1180,7 +1180,7 @@ elabValBind info aspat tm_in
11801180 = do ctxt <- getContext
11811181 i <- getIState
11821182 let tm = addImpl i tm_in
1183− logLvl 10 (showImp Nothing True False tm)
1183+ logLvl 10 (showTmImpls tm)
11841184 -- try:
11851185 -- * ordinary elaboration
11861186 -- * elaboration as a Type
@@ -1271,7 +1271,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12711271 let params = getParamsInType i [] fn_is fn_ty
12721272 let lhs = stripUnmatchable i $
12731273 addImplPat i (propagateParams params (stripLinear i lhs_in))
1274− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
1274+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
12751275 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
12761276
12771277 ((lhs', dlhs, []), _) <-
@@ -1286,7 +1286,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12861286 (clhs_c, clhsty) <- recheckC fc [] lhs_tm
12871287 let clhs = normalise ctxt [] clhs_c
12881288
1289− logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
1289+ logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
12901290
12911291 rep <- useREPL
12921292 when rep $ do
@@ -1312,10 +1312,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13121312 mapM_ (elabDecl' EAll info) wbefore
13131313 -- Now build the RHS, using the type of the LHS as the goal.
13141314 i <- getIState -- new implicits from where block
1315− logLvl 5 (showImp Nothing True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))
1315+ logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
13161316 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
13171317 (expandParams decorate newargs defs (defs \\ decls) rhs_in)
1318− logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
1318+ logLvl 2 $ "RHS: " ++ showTmImpls rhs
13191319 ctxt <- getContext -- new context with where block added
13201320 logLvl 5 "STARTING CHECK"
13211321 ((rhs', defer, is), _) <-
@@ -1468,7 +1468,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14681468 -- pattern bindings
14691469 i <- getIState
14701470 let lhs = addImplPat i (stripLinear i lhs_in)
1471− logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1471+ logLvl 5 ("LHS: " ++ showTmImpls lhs)
14721472 ((lhs', dlhs, []), _) <-
14731473 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
14741474 (errAt "left hand side of with in " fname
@@ -1481,7 +1481,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14811481 logLvl 5 ("Checked " ++ show clhs)
14821482 let bargs = getPBtys lhs_tm
14831483 let wval = addImplBound i (map fst bargs) wval_in
1484− logLvl 5 ("Checking " ++ showImp Nothing True False wval)
1484+ logLvl 5 ("Checking " ++ showTmImpls wval)
14851485 -- Elaborate wval in this context
14861486 ((wval', defer, is), _) <-
14871487 tclift $ elaborate ctxt (sMN 0 "withRHS")
@@ -1545,7 +1545,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15451545 (map (pexp . (PRef fc) . fst) bargs_pre ++
15461546 pexp wval :
15471547 (map (pexp . (PRef fc) . fst) bargs_post))
1548− logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)
1548+ logLvl 5 ("New RHS " ++ showTmImpls rhs)
15491549 ctxt <- getContext -- New context with block added
15501550 i <- getIState
15511551 ((rhs', defer, is), _) <-
@@ -1576,8 +1576,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15761576 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
15771577 = do i <- getIState
15781578 let tm = addImplPat i tm_in
1579− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
1580− showImp Nothing True False toplhs)
1579+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1580+ showTmImpls toplhs)
15811581 case matchClause i toplhs tm of
15821582 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")
15831583 Right mvars ->
@@ -1587,8 +1587,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15871587 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
15881588 = do i <- getIState
15891589 let tm = addImplPat i tm_in
1590− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
1591− showImp Nothing True False toplhs)
1590+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1591+ showTmImpls toplhs)
15921592 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
15931593 case matchClause i toplhs tm of
15941594 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
@@ -1655,7 +1655,7 @@ elabClass info syn doc fc constraints tn ps ds
16551655 constraint
16561656 let cons = [("", cn, cty, fc, [])]
16571657 let ddecl = PDatadecl tn tty cons
1658− logLvl 5 $ "Class data " ++ showDImp True ddecl
1658+ logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
16591659 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
16601660 -- for each constraint, build a top level function to chase it
16611661 logLvl 5 $ "Building functions"
@@ -1697,7 +1697,7 @@ elabClass info syn doc fc constraints tn ps ds
16971697 getMName (PTy _ _ _ _ n _) = nsroot n
16981698 tdecl allmeths (PTy doc syn _ o n t)
16991699 = do t' <- implicit' syn allmeths n t
1700− logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
1700+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
17011701 return ( (n, (toExp (map fst ps) Exp t')),
17021702 (n, (doc, o, (toExp (map fst ps) Imp t'))),
17031703 (n, (syn, o, t) ) )
@@ -1734,8 +1734,8 @@ elabClass info syn doc fc constraints tn ps ds
17341734 let lhs = PApp fc (PRef fc cfn) [pconst capp]
17351735 let rhs = PResolveTC (fileFC "HACK")
17361736 let ty = PPi constraint (sMN 0 "pc") c con
1737− iLOG (showImp Nothing True False ty)
1738− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1737+ iLOG (showTmImpls ty)
1738+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
17391739 i <- getIState
17401740 let conn = case con of
17411741 PRef _ n -> n
@@ -1759,9 +1759,9 @@ elabClass info syn doc fc constraints tn ps ds
17591759 let anames = map (\x -> sMN x "arg") [0..]
17601760 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
17611761 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
1762− iLOG (showImp Nothing True False ty)
1762+ iLOG (showTmImpls ty)
17631763 iLOG (show (m, ty', capp, margs))
1764− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1764+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
17651765 return [PTy doc syn fc o m ty',
17661766 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
17671767
@@ -1849,7 +1849,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
18491849 let wbTys = map mkTyDecl mtys
18501850 let wbVals = map (decorateid (decorate ns iname)) ds'
18511851 let wb = wbTys ++ wbVals
1852− logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)
1852+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)
18531853 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
18541854 show (concat (nub wparams))
18551855 let lhs = PRef fc iname
@@ -2156,8 +2156,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)
21562156
21572157checkInferred :: FC -> PTerm -> PTerm -> Idris ()
21582158checkInferred fc inf user =
2159− do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++
2160− showImp Nothing True False user
2159+ do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++
2160+ showTmImpls user
21612161 logLvl 10 $ "Checking match"
21622162 i <- getIState
21632163 tclift $ case matchClause' True i user inf of
@@ -2174,8 +2174,8 @@ checkInferred fc inf user =
21742174inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
21752175inferredDiff fc inf user =
21762176 do i <- getIState
2177− logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
2178− showImp Nothing True False user
2177+ logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++
2178+ showTmImpls user
21792179 tclift $ case matchClause' True i user inf of
21802180 Right vs -> return False
21812181 Left (x, y) -> return True
src/Idris/IdeSlave.hs+17
@@ -69,6 +69,23 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
6969instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
7070 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
7171
72+instance SExpable NameOutput where
73+ toSExp TypeOutput = SymbolAtom "type"
74+ toSExp FunOutput = SymbolAtom "function"
75+ toSExp DataOutput = SymbolAtom "data"
76+
77+instance SExpable OutputAnnotation where
78+ toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
79+ (SymbolAtom "implicit", BoolAtom False)]
80+ toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
81+ (SymbolAtom "decor", toSExp ty),
82+ (SymbolAtom "implicit", BoolAtom False)]
83+ toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
84+ (SymbolAtom "decor", SymbolAtom "bound"),
85+ (SymbolAtom "implicit", BoolAtom imp)]
86+ toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
87+ toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
88+
7289escape :: String -> String
7390escape = concatMap escapeChar
7491 where
src/Idris/Parser.hs+1−1
@@ -1062,7 +1062,7 @@ loadSource h lidr f
10621062 f file pos
10631063 unless (null ds') $ do
10641064 let ds = namespaces mname ds'
1065− logLvl 3 (showDecls True ds)
1065+ logLvl 3 (show $ showDecls True ds)
10661066 i <- getIState
10671067 logLvl 10 (show (toAlist (idris_implicits i)))
10681068 logLvl 3 (show (idris_infixes i))
src/Idris/Prover.hs+28−23
@@ -89,47 +89,52 @@ elabStep st e = do case runStateT e st of
8989
9090dumpState :: IState -> ProofState -> Idris ()
9191dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
92− iputGoal . render $ pretty nm <> colon <+> text "No more goals."
92+ iputGoal . renderPretty 0.7 breakingSize $
93+ prettyName False [] nm <> colon <+> text "No more goals."
9394dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
9495 let OK ty = goalAtFocus ps
9596 let OK env = envAtFocus ps
96− iputGoal . render $
97− prettyOtherGoals hs $$
98− prettyAssumptions env $$
99− prettyGoal ty
97+ iputGoal . renderPretty 0.7 breakingSize $
98+ prettyOtherGoals hs <> line <>
99+ prettyAssumptions env <> line <>
100+ prettyGoal (zip (assumptionNames env) (repeat False)) ty
100101 where
101102 -- XXX
102− tPretty t = pretty $ delab ist t
103+ tPretty bnd t = pprintPTerm True bnd $ delab ist t
103104
104− prettyPs [] = empty
105− prettyPs ((MN _ r, _) : bs)
106− | r == txt "rewrite_rule" = prettyPs bs
107− prettyPs ((n, Let t v) : bs) =
108− nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
109− tPretty t $$ prettyPs bs)
110− prettyPs ((n, b) : bs) =
111− pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
105+ assumptionNames :: Env -> [Name]
106+ assumptionNames = map fst
112107
113− prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
114− prettyG b = tPretty $ binderTy b
108+ prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
109+ prettyPs bnd [] = empty
110+ prettyPs bnd ((n@(MN _ r), _) : bs)
111+ | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
112+ prettyPs bnd ((n, Let t v) : bs) =
113+ nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
114+ tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
115+ prettyPs bnd ((n, b) : bs) =
116+ line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs
115117
116− prettyGoal ty =
117− text "---------- Goal: ----------" $$
118− pretty h <> colon $$ nest nestingSize (prettyG ty)
118+ prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
119+ prettyG bnd b = tPretty bnd $ binderTy b
120+
121+ prettyGoal bnd ty =
122+ text "---------- Goal: ----------" <$$>
123+ bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)
119124
120125 prettyAssumptions env =
121126 if length env == 0 then
122127 empty
123128 else
124− text "---------- Assumptions: ----------" $$
125− nest nestingSize (prettyPs $ reverse env)
129+ text "---------- Assumptions: ----------" <>
130+ nest nestingSize (prettyPs [] $ reverse env)
126131
127132 prettyOtherGoals hs =
128133 if length hs == 0 then
129134 empty
130135 else
131− text "---------- Other goals: ----------" $$
132− pretty hs
136+ text "---------- Other goals: ----------" <$$>
137+ nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
133138
134139lifte :: ElabState [PDecl] -> ElabD a -> Idris a
135140lifte st e = do (v, _) <- elabStep st e
src/Idris/REPL.hs+23−27
@@ -448,10 +448,11 @@ process h fn (Eval t)
448448 ist <- getIState
449449 logLvl 3 $ "Raw: " ++ show (tm', ty')
450450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
451− imp <- impShow
452− c <- colourise
453− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
454− showImp (Just ist) imp c (delab ist ty'))
451+ let imp = opt_showimp (idris_options ist)
452+ tmDoc = prettyImp imp (delab ist tm')
453+ tyDoc = prettyImp imp (delab ist ty')
454+ ihPrintTermWithType h tmDoc tyDoc
455+
455456process h fn (ExecVal t)
456457 = do ctxt <- getContext
457458 ist <- getIState
@@ -459,10 +460,8 @@ process h fn (ExecVal t)
459460-- let tm' = normaliseAll ctxt [] tm
460461 let ty' = normaliseAll ctxt [] ty
461462 res <- execute tm
462− imp <- impShow
463− c <- colourise
464− ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++
465− showImp (Just ist) imp c (delab ist ty'))
463+ ihPrintResult h (showTm ist (delab ist res) ++ " : " ++
464+ showTm ist (delab ist ty'))
466465process h fn (Check (PRef _ n))
467466 = do ctxt <- getContext
468467 ist <- getIState
@@ -472,9 +471,7 @@ process h fn (Check (PRef _ n))
472471 ts@(t:_) ->
473472 case lookup t (idris_metavars ist) of
474473 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
475− Nothing -> ihPrintResult h $
476− concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++
477− showImp (Just ist) imp c (delabTy ist n)) $ ts
474+ Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
478475 [] -> ihPrintError h $ "No such variable " ++ show n
479476 where
480477 showMetavarInfo c imp ist n i
@@ -487,27 +484,27 @@ process h fn (Check (PRef _ n))
487484 MN _ _ -> "_"
488485 UN nm | ('_':'_':_) <- str nm -> "_"
489486 _ -> showName (Just ist) [] False c n) ++
490− " : " ++ showImp (Just ist) imp c t ++ "\n"
487+ " : " ++ showTm ist t ++ "\n"
491488 in
492489 current ++ putTy c imp ist (i-1) sc
493490 putTy c imp ist _ sc = putGoal c imp ist sc
494491 putGoal c imp ist g
495492 = "--------------------------------------\n" ++
496493 showName (Just ist) [] False c n ++ " : " ++
497− showImp (Just ist) imp c g
494+ showTm ist g
498495
499496
500497process h fn (Check t)
501498 = do (tm, ty) <- elabVal toplevel False t
502499 ctxt <- getContext
503500 ist <- getIState
504− imp <- impShow
505− c <- colourise
506− let ty' = normaliseC ctxt [] ty
501+ let imp = opt_showimp (idris_options ist)
502+ ty' = normaliseC ctxt [] ty
507503 case tm of
508− TType _ -> ihPrintResult h ("Type : Type 1")
509− _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
510− showImp (Just ist) imp c (delab ist ty))
504+ TType _ ->
505+ ihPrintTermWithType h (prettyImp imp PType) type1Doc
506+ _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))
507+ (prettyImp imp (delab ist ty))
511508
512509process h fn (DocStr n)
513510 = do i <- getIState
@@ -540,9 +537,9 @@ process h fn (Defn n)
540537 [t] -> iputStrLn (showTotal t i)
541538 _ -> return ()
542539 where printCase i (_, lhs, rhs)
543− = do c <- colourise
544− iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++
545− showImp (Just i) True c (delab i rhs))
540+ = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
541+ in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
542+ showTm i' (delab i rhs))
546543process h fn (TotCheck n)
547544 = do i <- getIState
548545 case lookupNameTotal n (tt_ctxt i) of
@@ -848,7 +845,7 @@ process h fn (TestInline t)
848845 let tm' = inlineTerm ist tm
849846 imp <- impShow
850847 c <- colourise
851− iPrintResult (showImp (Just ist) imp c (delab ist tm'))
848+ iPrintResult (showTm ist (delab ist tm'))
852849process h fn Execute
853850 = do (m, _) <- elabVal toplevel False
854851 (PApp fc
@@ -876,11 +873,11 @@ process h fn (Pattelab t)
876873
877874process h fn (Missing n)
878875 = do i <- getIState
879− c <- colourise
876+ let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
880877 case lookupCtxt n (idris_patdefs i) of
881878 [] -> return ()
882879 [(_, tms)] ->
883− iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))
880+ iPrintResult (showSep "\n" (map (showTm i') tms))
884881 _ -> iPrintError $ "Ambiguous name"
885882process h fn (DynamicLink l)
886883 = do i <- getIState
@@ -949,9 +946,8 @@ dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
949946dumpInstance :: Name -> Idris ()
950947dumpInstance n = do i <- getIState
951948 ctxt <- getContext
952− imp <- impShow
953949 case lookupTy n ctxt of
954− ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
950+ ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts
955951
956952showTotal :: Totality -> IState -> String
957953showTotal t@(Partial (Other ns)) i
src/Util/Pretty.hs+5−8
@@ -1,10 +1,11 @@
11module Util.Pretty (
2− module Text.PrettyPrint.HughesPJ,
2+ module Text.PrettyPrint.Annotated.Leijen,
33 Sized(..), breakingSize, nestingSize,
44 Pretty(..)
55) where
66
7−import Text.PrettyPrint.HughesPJ
7+--import Text.PrettyPrint.HughesPJ
8+import Text.PrettyPrint.Annotated.Leijen
89
910-- A rough notion of size for pretty printing various types.
1011class Sized a where
@@ -23,11 +24,7 @@ breakingSize = 15
2324nestingSize :: Int
2425nestingSize = 1
2526
26−class Pretty a where
27− pretty :: a -> Doc
27+class Pretty a ty where
28+ pretty :: a -> Doc ty
2829
29−instance Pretty () where
30− pretty () = text "()"
3130
32−instance Pretty a => Pretty [a] where
33− pretty l = foldr ($$) empty $ map pretty l
test/reg007/expected+6−7
@@ -1,13 +1,12 @@
11reg007.lidr:8:1:A.n is already defined
22reg007.lidr:12:9:When elaborating right hand side of hurrah:
33Can't unify
4− n = lala
4+ n = lala
55with
6− 0 = 1
6+ 0 = 1
77
88Specifically:
9− Can't unify
10− 1
11− with
12− 0
13−
9+ Can't unify
10+ 1
11+ with
12+ 0
test/reg007/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
2−idris --check $@ reg007.lidr
2+idris --nocolour --check $@ reg007.lidr
33rm -f *.ibc
test/reg010/expected+6−7
@@ -1,12 +1,11 @@
11reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:
22Can't unify
3− P x
3+ P x
44with
5− P y
5+ P y
66
77Specifically:
8− Can't unify
9− P x
10− with
11− P y
12−
8+ Can't unify
9+ P x
10+ with
11+ P y
test/reg023/expected+6−7
@@ -1,12 +1,11 @@
11reg023.idr:7:5:When elaborating right hand side of bad:
22Can't unify
3− Nat
3+ Nat
44with
5− f Nat
5+ f Nat
66
77Specifically:
8− Can't unify
9− Nat
10− with
11− f Nat
12−
8+ Can't unify
9+ Nat
10+ with
11+ f Nat
test/test020/expected+6−7
@@ -1,14 +1,13 @@
11When elaborating right hand side of foo:
22test020a.idr:14:18:Can't unify
3− Vect n a
3+ Vect n a
44with
5− List a
5+ List a
66
77Specifically:
8− Can't unify
9− Vect n a
10− with
11− List a
12−
8+ Can't unify
9+ Vect n a
10+ with
11+ List a
1312[3, 2, 1]
1413"Number 42"
test/test030/expected+6−7
@@ -1,12 +1,11 @@
11test030a.idr:12:14:When elaborating right hand side of testReflect1:
22Can't unify
3− IsJust (Just x)
3+ IsJust (Just x)
44with
5− IsJust (prove (getProof x))
5+ IsJust (prove (getProof x))
66
77Specifically:
8− Can't unify
9− Just x
10− with
11− Nothing
12−
8+ Can't unify
9+ Just x
10+ with
11+ Nothing
test/test037/expected+13−14
@@ -1,18 +1,17 @@
11In file ErrorReflection.idr line 78 column 5
2− When elaborating right hand side of Main.bad :
3− DSL type error: (t'(504) => t'(504)) doesn't match ()
2+ When elaborating right hand side of Main.bad :
3+ DSL type error: (t'(504) => t'(504)) doesn't match ()
44
55Original error:
66
7− ErrorReflection.idr:78:5:When elaborating right hand side of bad:
8− Can't unify
9− Tm [] (Main.TFun t' t')
10− with
11− Tm [] Main.TUnit
12−
13− Specifically:
14− Can't unify
15− Main.TFun t' t'
16− with
17− Main.TUnit
18−
7+ ErrorReflection.idr:78:5:When elaborating right hand side of bad:
8+ Can't unify
9+ Tm [] (TFun t' t')
10+ with
11+ Tm [] TUnit
12+
13+ Specifically:
14+ Can't unify
15+ TFun t' t'
16+ with
17+ TUnit