@@ -15,6 +15,8 @@ import Util.DynamicLinker
1515import Paths_idris
1616
1717import System.Console.Haskeline
18+import System.Console.ANSI ( Color(..), ConsoleLayer(..), SGR(..), setSGRCode,
19+ ColorIntensity(..), Underlining(..), ConsoleIntensity(..) )
1820
1921import Control.Monad.Trans.State.Strict
2022
@@ -28,7 +30,7 @@ data IOption = IOption { opt_logLevel :: Int,
2830 opt_typecase :: Bool,
2931 opt_typeintype :: Bool,
3032 opt_coverage :: Bool,
31− opt_showimp :: Bool,
33+ opt_showimp :: Bool, -- ^^ show implicits
3234 opt_errContext :: Bool,
3335 opt_repl :: Bool,
3436 opt_verbose :: Bool,
@@ -788,8 +790,22 @@ expandNS syn n = case syn_namespace syn of
788790
789791--- Pretty printing declarations and terms
790792
793+-- Set the colour of a string using POSIX escape codes
794+colourise :: Color -> ColorIntensity -> String -> String
795+colourise c i str = let sgr = [SetColor Foreground i c]
796+ in setSGRCode sgr ++ str ++ setSGRCode [Reset]
797+
798+colouriseKwd :: String -> String
799+colouriseKwd kwd = setSGRCode [SetUnderlining SingleUnderline
800+ , SetConsoleIntensity BoldIntensity
801+ , SetColor Foreground Vivid Black
802+ ] ++ kwd ++ setSGRCode [Reset]
803+
804+colouriseBound :: String -> String
805+colouriseBound = colourise Magenta Vivid
806+
791807instance Show PTerm where
792− show tm = showImp False tm
808+ show tm = showImp False False tm
793809
794810instance Pretty PTerm where
795811 pretty = prettyImp False
@@ -804,8 +820,8 @@ instance Show PData where
804820 show d = showDImp False d
805821
806822showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
807−showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
808−showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
823+showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t False ty
824+showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t False ty
809825showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
810826showDeclImp _ (PData _ _ _ _ d) = show d
811827showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
@@ -814,24 +830,24 @@ showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
814830
815831showCImp :: Bool -> PClause -> String
816832showCImp impl (PClause _ n l ws r w)
817− = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
833+ = showImp impl False l ++ showWs ws ++ " = " ++ showImp impl False r
818834 ++ " where " ++ show w
819835 where
820836 showWs [] = ""
821− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
837+ showWs (x : xs) = " | " ++ showImp impl False x ++ showWs xs
822838showCImp impl (PWith _ n l ws r w)
823− = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
839+ = showImp impl False l ++ showWs ws ++ " with " ++ showImp impl False r
824840 ++ " { " ++ show w ++ " } "
825841 where
826842 showWs [] = ""
827− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
843+ showWs (x : xs) = " | " ++ showImp impl False x ++ showWs xs
828844
829845
830846showDImp :: Bool -> PData -> String
831847showDImp impl (PDatadecl n ty cons)
832− = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
848+ = "data " ++ show n ++ " : " ++ showImp impl False ty ++ " where\n\t"
833849 ++ showSep "\n\t| "
834− (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
850+ (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl False t) cons)
835851
836852getImps :: [PArg] -> [(Name, PTerm)]
837853getImps [] = []
@@ -851,7 +867,10 @@ getConsts (_ : xs) = getConsts xs
851867getAll :: [PArg] -> [PTerm]
852868getAll = map getTm
853869
854−prettyImp :: Bool -> PTerm -> Doc
870+-- | Pretty-print a high-level Idris term
871+prettyImp :: Bool -- ^^ whether to show implicits
872+ -> PTerm -- ^^ the term to pretty-print
873+ -> Doc
855874prettyImp impl = prettySe 10
856875 where
857876 prettySe p (PQuote r) =
@@ -1037,108 +1056,117 @@ prettyImp impl = prettySe 10
10371056 bracket outer inner doc
10381057 | inner > outer = lparen <> doc <> rparen
10391058 | otherwise = doc
1040−
1041−showImp :: Bool -> PTerm -> String
1042−showImp impl tm = se 10 tm where
1043− se p (PQuote r) = "![" ++ show r ++ "]"
1044− se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1045− se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1046− se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1047− else showbasic n
1048− where showbasic n@(UN _) = show n
1059+
1060+-- | Show Idris term
1061+showImp :: Bool -- ^^ whether to show implicits
1062+ -> Bool -- ^^ whether to colourise
1063+ -> PTerm -- ^^ the term to show
1064+ -> String
1065+showImp impl colour tm = se 10 [] tm where
1066+ perhapsColourise :: (String -> String) -> String -> String
1067+ perhapsColourise col str = if colour then col str else str
1068+
1069+ se :: Int -> [Name] -> PTerm -> String
1070+ se p bnd (PQuote r) = "![" ++ show r ++ "]"
1071+ se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1072+ se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1073+ se p bnd (PRef fc n) = if colour && n `elem` bnd then colouriseBound name else name
1074+ where name = if impl then show n else showbasic n
1075+ showbasic n@(UN _) = show n
10491076 showbasic (MN _ s) = s
10501077 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1051− se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1052− (if impl then " : " ++ se 10 ty else "") ++ " => "
1053− ++ se 10 sc
1054− se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1055− " in " ++ se 10 sc
1056− se p (PPi (Exp l s _) n ty sc)
1078+ se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1079+ (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1080+ ++ se 10 (n:bnd) sc
1081+ se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1082+ " = " ++ se 10 bnd v ++
1083+ " in " ++ se 10 (n:bnd) sc
1084+ se p bnd (PPi (Exp l s _) n ty sc)
10571085 | n `elem` allNamesIn sc || impl
10581086 = bracket p 2 $
1059− (if l then "|(" else "(") ++
1060− show n ++ " : " ++ se 10 ty ++
1087+ (if l then "|(" else "(") ++
1088+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
10611089 ") " ++ st ++
1062− "-> " ++ se 10 sc
1063− | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1090+ "-> " ++ se 10 (n:bnd) sc
1091+ | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
10641092 where st = case s of
10651093 Static -> "[static] "
10661094 _ -> ""
1067− se p (PPi (Imp l s _) n ty sc)
1068− | impl = bracket p 2 $ (if l then "|{" else "{") ++
1069− show n ++ " : " ++ se 10 ty ++
1070− "} " ++ st ++ "-> " ++ se 10 sc
1071− | otherwise = se 10 sc
1095+ se p bnd (PPi (Imp l s _) n ty sc)
1096+ | impl = bracket p 2 $ (if l then "|{" else "{") ++
1097+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1098+ "} " ++ st ++ "-> " ++ se 10 (n:bnd) sc
1099+ | otherwise = se 10 bnd sc
10721100 where st = case s of
10731101 Static -> "[static] "
10741102 _ -> ""
1075− se p (PPi (Constraint _ _ _) n ty sc)
1076− = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1077− se p (PPi (TacImp _ _ s _) n ty sc)
1078− = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1079− se p e
1080− | Just str <- slist p e = str
1103+ se p bnd (PPi (Constraint _ _ _) n ty sc)
1104+ = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
1105+ se p bnd (PPi (TacImp _ _ s _) n ty sc)
1106+ = bracket p 2 $
1107+ "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1108+ se 10 (n:bnd) sc
1109+ se p bnd e
1110+ | Just str <- slist p bnd e = str
10811111 | Just num <- snat p e = show num
1082− se p (PMatchApp _ f) = "match " ++ show f
1083− se p (PApp _ (PRef _ f) [])
1112+ se p bnd (PMatchApp _ f) = "match " ++ show f
1113+ se p bnd (PApp _ (PRef _ f) [])
10841114 | not impl = show f
1085− se p (PApp _ (PRef _ op@(UN (f:_))) args)
1115+ se p bnd (PApp _ (PRef _ op@(UN (f:_))) args)
10861116 | length (getExps args) == 2 && not impl && not (isAlpha f)
10871117 = let [l, r] = getExps args in
1088− bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1089− se p (PApp _ f as)
1118+ bracket p 1 $ se 1 bnd l ++ " " ++ show op ++ " " ++ se 0 bnd r
1119+ se p bnd (PApp _ f as)
10901120 = let args = getExps as in
1091− bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1092− else concatMap seArg args
1093− se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1094− where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1095− se p (PHidden tm) = "." ++ se 0 tm
1096− se p (PRefl _ t)
1121+ bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
1122+ else concatMap (seArg bnd) args
1123+ se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1124+ where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1125+ se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1126+ se p bnd (PRefl _ t)
10971127 | not impl = "refl"
1098− | otherwise = "refl {" ++ se 10 t ++ "}"
1099− se p (PResolveTC _) = "resolvetc"
1100− se p (PTrue _) = "()"
1101− se p (PFalse _) = "_|_"
1102− se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1103− se p (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r
1104− se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1105− se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1106− se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1107− se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1108− se p PType = "Type"
1109− se p (PConstant c) = show c
1110− se p (PProof ts) = "proof { " ++ show ts ++ "}"
1111− se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1112− se p (PMetavar n) = "?" ++ show n
1113− se p (PReturn f) = "return"
1114− se p PImpossible = "impossible"
1115− se p Placeholder = "_"
1116− se p (PDoBlock _) = "do block show not implemented"
1117− se p (PElabError s) = show s
1118− se p (PCoerced t) = se p t
1119− se p (PUnifyLog t) = "%unifyLog " ++ se p t
1120− se p (PGoal f t n sc) = "quoteGoal " ++ show n ++ " by " ++ se 10 t ++
1121− " in " ++ se 10 sc
1122−-- se p x = "Not implemented"
1123−
1124− slist' p (PApp _ (PRef _ nil) _)
1128+ | otherwise = "refl {" ++ se 10 bnd t ++ "}"
1129+ se p bnd (PResolveTC _) = "resolvetc"
1130+ se p bnd (PTrue _) = "()"
1131+ se p bnd (PFalse _) = "_|_"
1132+ se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ " = " ++ se 10 bnd r
1133+ se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
1134+ se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
1135+ se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
1136+ se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
1137+ se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
1138+ se p bnd PType = "Type"
1139+ se p bnd (PConstant c) = show c
1140+ se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
1141+ se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
1142+ se p bnd (PMetavar n) = "?" ++ show n
1143+ se p bnd (PReturn f) = "return"
1144+ se p bnd PImpossible = "impossible"
1145+ se p bnd Placeholder = "_"
1146+ se p bnd (PDoBlock _) = "do block show not implemented"
1147+ se p bnd (PElabError s) = show s
1148+ se p bnd (PCoerced t) = se p bnd t
1149+ se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
1150+-- se p bnd x = "Not implemented"
1151+
1152+ slist' p bnd (PApp _ (PRef _ nil) _)
11251153 | nsroot nil == UN "Nil" = Just []
1126− slist' p (PApp _ (PRef _ cons) args)
1154+ slist' p bnd (PApp _ (PRef _ cons) args)
11271155 | nsroot cons == UN "::",
11281156 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
11291157 all isImp imps,
1130− Just tl' <- slist' p tl
1158+ Just tl' <- slist' p bnd tl
11311159 = Just (hd:tl')
11321160 where
11331161 isImp (PImp {}) = True
11341162 isImp _ = False
1135− slist' _ _ = Nothing
1163+ slist' _ _ _ = Nothing
11361164
1137− slist p e | Just es <- slist' p e = Just $
1165+ slist p bnd e | Just es <- slist' p bnd e = Just $
11381166 case es of [] -> "[]"
1139− [x] -> "[" ++ se p x ++ "]"
1140− xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1141− slist _ _ = Nothing
1167+ [x] -> "[" ++ se p bnd x ++ "]"
1168+ xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
1169+ slist _ _ _ = Nothing
11421170
11431171 -- since Prelude is always imported, S & Z are unqualified iff they're the
11441172 -- Nat ones.
@@ -1152,15 +1180,15 @@ showImp impl tm = se 10 tm where
11521180
11531181 natns = "Prelude.Nat."
11541182
1155− sArg (PImp _ _ n tm _) = siArg (n, tm)
1156− sArg (PExp _ _ tm _) = seArg tm
1157− sArg (PConstraint _ _ tm _) = scArg tm
1158− sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)
1183+ sArg bnd (PImp _ _ n tm _) = siArg bnd (n, tm)
1184+ sArg bnd (PExp _ _ tm _) = seArg bnd tm
1185+ sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
1186+ sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
11591187
1160− seArg arg = " " ++ se 0 arg
1161− siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1162− scArg val = " {{" ++ se 10 val ++ "}}"
1163− stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1188+ seArg bnd arg = " " ++ se 0 bnd arg
1189+ siArg bnd (n, val) = " {" ++ show n ++ " = " ++ se 10 bnd val ++ "}"
1190+ scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
1191+ stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
11641192
11651193 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
11661194 | otherwise = str