ffb9ea9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Semantic colouring of identifiers in REPL

ffb9ea9David Christiansen13 years ago

idris.cabal+1−1

compare with master

unifiedsplit

@@ -278,7 +278,7 @@ Executable idris

278 containers, process, transformers, filepath,

279 directory, binary, bytestring, text, pretty,

280 language-java>=0.2.2, libffi,

281− vector, vector-binary-instances

281+ vector, vector-binary-instances, ansi-terminal

282

283 Extensions: MultiParamTypeClasses, FunctionalDependencies,

284 FlexibleInstances, TemplateHaskell

src/Idris/AbsSyntax.hs+2−2

@@ -1170,7 +1170,7 @@ mkPApp fc a f as = let rest = drop a as in

1170-- FIXME: It's possible that this really has to happen after elaboration

1171

1172findStatics :: IState -> PTerm -> (PTerm, [Bool])

1173−findStatics ist tm = trace (showImp True tm) $

1173+findStatics ist tm = trace (showImp True False tm) $

1174 let (ns, ss) = fs tm in

1175 runState (pos ns ss tm) []

1176 where fs (PPi p n t sc)

@@ -1201,7 +1201,7 @@ dumpDecls [] = ""

1201dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

1202

1203dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

1204−dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

1204+dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True False t

1205dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

1206dumpDecl (PData _ _ _ _ d) = showDImp True d

1207dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

src/Idris/AbsSyntaxTree.hs+122−94

@@ -15,6 +15,8 @@ import Util.DynamicLinker

15import Paths_idris

17import System.Console.Haskeline

18+import System.Console.ANSI ( Color(..), ConsoleLayer(..), SGR(..), setSGRCode,

19+ ColorIntensity(..), Underlining(..), ConsoleIntensity(..) )

19import Control.Monad.Trans.State.Strict

21import Control.Monad.Trans.State.Strict

@@ -28,7 +30,7 @@ data IOption = IOption { opt_logLevel :: Int,

28 opt_typecase :: Bool,

30 opt_typecase :: Bool,

29 opt_typeintype :: Bool,

31 opt_typeintype :: Bool,

30 opt_coverage :: Bool,

32 opt_coverage :: Bool,

31− opt_showimp :: Bool,

33+ opt_showimp :: Bool, -- ^^ show implicits

32 opt_errContext :: Bool,

34 opt_errContext :: Bool,

33 opt_repl :: Bool,

35 opt_repl :: Bool,

34 opt_verbose :: Bool,

36 opt_verbose :: Bool,

@@ -788,8 +790,22 @@ expandNS syn n = case syn_namespace syn of

788

790

789--- Pretty printing declarations and terms

791--- Pretty printing declarations and terms

790

792

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+

791instance Show PTerm where

807instance Show PTerm where

792− show tm = showImp False tm

808+ show tm = showImp False False tm

793

809

794instance Pretty PTerm where

810instance Pretty PTerm where

795 pretty = prettyImp False

811 pretty = prettyImp False

@@ -804,8 +820,8 @@ instance Show PData where

804 show d = showDImp False d

820 show d = showDImp False d

805

821

806showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

822showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

807−showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

823+showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t False ty

808−showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty

824+showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t False ty

809showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

825showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

810showDeclImp _ (PData _ _ _ _ d) = show d

826showDeclImp _ (PData _ _ _ _ d) = show d

811showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

827showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

@@ -814,24 +830,24 @@ showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

814

830

815showCImp :: Bool -> PClause -> String

831showCImp :: Bool -> PClause -> String

816showCImp impl (PClause _ n l ws r w)

832showCImp 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

818 ++ " where " ++ show w

834 ++ " where " ++ show w

819 where

835 where

820 showWs [] = ""

836 showWs [] = ""

821− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs

837+ showWs (x : xs) = " | " ++ showImp impl False x ++ showWs xs

822showCImp impl (PWith _ n l ws r w)

838showCImp 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

824 ++ " { " ++ show w ++ " } "

840 ++ " { " ++ show w ++ " } "

825 where

841 where

826 showWs [] = ""

842 showWs [] = ""

827− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs

843+ showWs (x : xs) = " | " ++ showImp impl False x ++ showWs xs

828

844

829

845

830showDImp :: Bool -> PData -> String

846showDImp :: Bool -> PData -> String

831showDImp impl (PDatadecl n ty cons)

847showDImp 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"

833 ++ showSep "\n\t| "

849 ++ showSep "\n\t| "

834− (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)

850+ (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl False t) cons)

835

851

836getImps :: [PArg] -> [(Name, PTerm)]

852getImps :: [PArg] -> [(Name, PTerm)]

837getImps [] = []

853getImps [] = []

@@ -851,7 +867,10 @@ getConsts (_ : xs) = getConsts xs

851getAll :: [PArg] -> [PTerm]

867getAll :: [PArg] -> [PTerm]

852getAll = map getTm

868getAll = map getTm

853

869

870+-- | Pretty-print a high-level Idris term

854−prettyImp :: Bool -> PTerm -> Doc

871+prettyImp :: Bool -- ^^ whether to show implicits

872+ -> PTerm -- ^^ the term to pretty-print

873+ -> Doc

855prettyImp impl = prettySe 10

874prettyImp impl = prettySe 10

856 where

875 where

857 prettySe p (PQuote r) =

876 prettySe p (PQuote r) =

@@ -1037,108 +1056,117 @@ prettyImp impl = prettySe 10

1037 bracket outer inner doc

1056 bracket outer inner doc

1038 | inner > outer = lparen <> doc <> rparen

1057 | inner > outer = lparen <> doc <> rparen

1039 | otherwise = doc

1058 | otherwise = doc

1040−

1059+

1060+-- | Show Idris term

1061+showImp :: Bool -- ^^ whether to show implicits

1062+ -> Bool -- ^^ whether to colourise

1063+ -> PTerm -- ^^ the term to show

1041−showImp :: Bool -> PTerm -> String

1064+ -> String

1042−showImp impl tm = se 10 tm where

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

1043− se p (PQuote r) = "![" ++ show r ++ "]"

1070+ se p bnd (PQuote r) = "![" ++ show r ++ "]"

1044− se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n

1071+ se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n

1045− se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

1072+ se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"

1046− se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"

1073+ se p bnd (PRef fc n) = if colour && n `elem` bnd then colouriseBound name else name

1047− else showbasic n

1074+ where name = if impl then show n else showbasic n

1048− where showbasic n@(UN _) = show n

1075+ showbasic n@(UN _) = show n

1049 showbasic (MN _ s) = s

1076 showbasic (MN _ s) = s

1050 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

1077 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

1051− se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++

1078+ se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++

1052− (if impl then " : " ++ se 10 ty else "") ++ " => "

1079+ (if impl then " : " ++ se 10 bnd ty else "") ++ " => "

1053− ++ se 10 sc

1080+ ++ se 10 (n:bnd) sc

1054− se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++

1081+ se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++

1082+ " = " ++ se 10 bnd v ++

1055− " in " ++ se 10 sc

1083+ " in " ++ se 10 (n:bnd) sc

1056− se p (PPi (Exp l s _) n ty sc)

1084+ se p bnd (PPi (Exp l s _) n ty sc)

1057 | n `elem` allNamesIn sc || impl

1085 | n `elem` allNamesIn sc || impl

1058 = bracket p 2 $

1086 = bracket p 2 $

1059− (if l then "|(" else "(") ++

1087+ (if l then "|(" else "(") ++

1060− show n ++ " : " ++ se 10 ty ++

1088+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1061 ") " ++ st ++

1089 ") " ++ st ++

1062− "-> " ++ se 10 sc

1090+ "-> " ++ se 10 (n:bnd) sc

1063− | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc

1091+ | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc

1064 where st = case s of

1092 where st = case s of

1065 Static -> "[static] "

1093 Static -> "[static] "

1066 _ -> ""

1094 _ -> ""

1067− se p (PPi (Imp l s _) n ty sc)

1095+ se p bnd (PPi (Imp l s _) n ty sc)

1068− | impl = bracket p 2 $ (if l then "|{" else "{") ++

1096+ | impl = bracket p 2 $ (if l then "|{" else "{") ++

1069− show n ++ " : " ++ se 10 ty ++

1097+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1070− "} " ++ st ++ "-> " ++ se 10 sc

1098+ "} " ++ st ++ "-> " ++ se 10 (n:bnd) sc

1071− | otherwise = se 10 sc

1099+ | otherwise = se 10 bnd sc

1072 where st = case s of

1100 where st = case s of

1073 Static -> "[static] "

1101 Static -> "[static] "

1074 _ -> ""

1102 _ -> ""

1075− se p (PPi (Constraint _ _ _) n ty sc)

1103+ se p bnd (PPi (Constraint _ _ _) n ty sc)

1076− = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc

1104+ = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc

1077− se p (PPi (TacImp _ _ s _) n ty sc)

1105+ se p bnd (PPi (TacImp _ _ s _) n ty sc)

1078− = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc

1106+ = bracket p 2 $

1107+ "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++

1108+ se 10 (n:bnd) sc

1079− se p e

1109+ se p bnd e

1080− | Just str <- slist p e = str

1110+ | Just str <- slist p bnd e = str

1081 | Just num <- snat p e = show num

1111 | Just num <- snat p e = show num

1082− se p (PMatchApp _ f) = "match " ++ show f

1112+ se p bnd (PMatchApp _ f) = "match " ++ show f

1083− se p (PApp _ (PRef _ f) [])

1113+ se p bnd (PApp _ (PRef _ f) [])

1084 | not impl = show f

1114 | not impl = show f

1085− se p (PApp _ (PRef _ op@(UN (f:_))) args)

1115+ se p bnd (PApp _ (PRef _ op@(UN (f:_))) args)

1086 | length (getExps args) == 2 && not impl && not (isAlpha f)

1116 | length (getExps args) == 2 && not impl && not (isAlpha f)

1087 = let [l, r] = getExps args in

1117 = let [l, r] = getExps args in

1088− bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

1118+ bracket p 1 $ se 1 bnd l ++ " " ++ show op ++ " " ++ se 0 bnd r

1089− se p (PApp _ f as)

1119+ se p bnd (PApp _ f as)

1090 = let args = getExps as in

1120 = let args = getExps as in

1091− bracket p 1 $ se 1 f ++ if impl then concatMap sArg as

1121+ bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as

1092− else concatMap seArg args

1122+ else concatMap (seArg bnd) args

1093− se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)

1123+ se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)

1094− where sc (l, r) = se 10 l ++ " => " ++ se 10 r

1124+ where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r

1095− se p (PHidden tm) = "." ++ se 0 tm

1125+ se p bnd (PHidden tm) = "." ++ se 0 bnd tm

1096− se p (PRefl _ t)

1126+ se p bnd (PRefl _ t)

1097 | not impl = "refl"

1127 | not impl = "refl"

1098− | otherwise = "refl {" ++ se 10 t ++ "}"

1128+ | otherwise = "refl {" ++ se 10 bnd t ++ "}"

1099− se p (PResolveTC _) = "resolvetc"

1129+ se p bnd (PResolveTC _) = "resolvetc"

1100− se p (PTrue _) = "()"

1130+ se p bnd (PTrue _) = "()"

1101− se p (PFalse _) = "_|_"

1131+ se p bnd (PFalse _) = "_|_"

1102− se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

1132+ se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ " = " ++ se 10 bnd r

1103− se p (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r

1133+ se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r

1104− se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"

1134+ se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"

1105− se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

1135+ se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"

1106− se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

1136+ se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"

1107− se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"

1137+ se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"

1108− se p PType = "Type"

1138+ se p bnd PType = "Type"

1109− se p (PConstant c) = show c

1139+ se p bnd (PConstant c) = show c

1110− se p (PProof ts) = "proof { " ++ show ts ++ "}"

1140+ se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"

1111− se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

1141+ se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"

1112− se p (PMetavar n) = "?" ++ show n

1142+ se p bnd (PMetavar n) = "?" ++ show n

1113− se p (PReturn f) = "return"

1143+ se p bnd (PReturn f) = "return"

1114− se p PImpossible = "impossible"

1144+ se p bnd PImpossible = "impossible"

1115− se p Placeholder = "_"

1145+ se p bnd Placeholder = "_"

1116− se p (PDoBlock _) = "do block show not implemented"

1146+ se p bnd (PDoBlock _) = "do block show not implemented"

1117− se p (PElabError s) = show s

1147+ se p bnd (PElabError s) = show s

1118− se p (PCoerced t) = se p t

1148+ se p bnd (PCoerced t) = se p bnd t

1119− se p (PUnifyLog t) = "%unifyLog " ++ se p t

1149+ se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd 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"

1150+-- se p bnd x = "Not implemented"

1123−

1151+

1124− slist' p (PApp _ (PRef _ nil) _)

1152+ slist' p bnd (PApp _ (PRef _ nil) _)

1125 | nsroot nil == UN "Nil" = Just []

1153 | nsroot nil == UN "Nil" = Just []

1126− slist' p (PApp _ (PRef _ cons) args)

1154+ slist' p bnd (PApp _ (PRef _ cons) args)

1127 | nsroot cons == UN "::",

1155 | nsroot cons == UN "::",

1128 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1156 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1129 all isImp imps,

1157 all isImp imps,

1130− Just tl' <- slist' p tl

1158+ Just tl' <- slist' p bnd tl

1131 = Just (hd:tl')

1159 = Just (hd:tl')

1132 where

1160 where

1133 isImp (PImp {}) = True

1161 isImp (PImp {}) = True

1134 isImp _ = False

1162 isImp _ = False

1135− slist' _ _ = Nothing

1163+ slist' _ _ _ = Nothing

1136

1164

1137− slist p e | Just es <- slist' p e = Just $

1165+ slist p bnd e | Just es <- slist' p bnd e = Just $

1138 case es of [] -> "[]"

1166 case es of [] -> "[]"

1139− [x] -> "[" ++ se p x ++ "]"

1167+ [x] -> "[" ++ se p bnd x ++ "]"

1140− xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"

1168+ xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"

1141− slist _ _ = Nothing

1169+ slist _ _ _ = Nothing

1142

1170

1143 -- since Prelude is always imported, S & Z are unqualified iff they're the

1171 -- since Prelude is always imported, S & Z are unqualified iff they're the

1144 -- Nat ones.

1172 -- Nat ones.

@@ -1152,15 +1180,15 @@ showImp impl tm = se 10 tm where

1152

1180

1153 natns = "Prelude.Nat."

1181 natns = "Prelude.Nat."

1154

1182

1155− sArg (PImp _ _ n tm _) = siArg (n, tm)

1183+ sArg bnd (PImp _ _ n tm _) = siArg bnd (n, tm)

1156− sArg (PExp _ _ tm _) = seArg tm

1184+ sArg bnd (PExp _ _ tm _) = seArg bnd tm

1157− sArg (PConstraint _ _ tm _) = scArg tm

1185+ sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

1158− sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)

1186+ sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)

1159

1187

1160− seArg arg = " " ++ se 0 arg

1188+ seArg bnd arg = " " ++ se 0 bnd arg

1161− siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"

1189+ siArg bnd (n, val) = " {" ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1162− scArg val = " {{" ++ se 10 val ++ "}}"

1190+ scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"

1163− stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"

1191+ stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"

1164

1192

1165 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

1193 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

1166 | otherwise = str

1194 | otherwise = str

src/Idris/Coverage.hs+2−2

@@ -50,7 +50,7 @@ genClauses fc n xs given

50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

51 logLvl 10 $ show argss ++ "\n" ++ show all_args

52 logLvl 10 $ "Original: \n" ++

53− showSep "\n" (map (\t -> showImp True (delab' i t True)) xs)

53+ showSep "\n" (map (\t -> showImp True False (delab' i t True)) xs)

54 -- add an infinite supply of explicit arguments to update the possible

55 -- cases for (the return type may be variadic, or function type, sp

56 -- there may be more case splitting that the idris_implicits record

@@ -62,7 +62,7 @@ genClauses fc n xs given

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63 let new = filter (noMatch i) (mnub i tryclauses)

64 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

65− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

65+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp True False) new)

66-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

67 return new

68-- return (map (\t -> PClause n t [] PImpossible []) new)

src/Idris/Delaborate.hs+10−10

@@ -100,33 +100,33 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

100 "Please consider reporting at " ++ bugaddr

101pshow i (CantUnify _ x y e sc s)

102 = let imps = opt_showimp (idris_options i) in

103− "Can't unify " ++ showImp imps (delab i x)

103+ "Can't unify " ++ showImp imps False (delab i x)

104− ++ " with " ++ showImp imps (delab i y) ++

104+ ++ " with " ++ showImp imps False (delab i y) ++

105−-- " (" ++ showEnvDbg [] x ++ " and " ++ showEnvDbg [] y ++ ") " ++

105+-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

106 case e of

107 Msg "" -> ""

108 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

109 if (opt_errContext (idris_options i)) then showSc i sc else ""

110pshow i (CantConvert x y env)

111 = let imps = opt_showimp (idris_options i) in

112− "Can't convert " ++ showImp imps (delab i x) ++ " with "

112+ "Can't convert " ++ showImp imps False (delab i x) ++ " with "

113− ++ showImp imps (delab i y) ++

113+ ++ showImp imps False (delab i y) ++

114 if (opt_errContext (idris_options i)) then showSc i env else ""

115pshow i (UnifyScope n out tm env)

116 = let imps = opt_showimp (idris_options i) in

117 "Can't unify " ++ show n ++ " with "

118− ++ showImp imps (delab i tm) ++ " as " ++ show out ++

118+ ++ showImp imps False (delab i tm) ++ " as " ++ show out ++

119 " is not in scope" ++

120 if (opt_errContext (idris_options i)) then showSc i env else ""

121pshow i (CantInferType t)

122 = "Can't infer type for " ++ t

123pshow i (NonFunctionType f ty)

124 = let imps = opt_showimp (idris_options i) in

125− showImp imps (delab i f) ++ " does not have a function type ("

125+ showImp imps False (delab i f) ++ " does not have a function type ("

126− ++ showImp imps (delab i ty) ++ ")"

126+ ++ showImp imps False (delab i ty) ++ ")"

127pshow i (CantIntroduce ty)

128 = let imps = opt_showimp (idris_options i) in

129− "Can't use lambda here: type is " ++ showImp imps (delab i ty)

129+ "Can't use lambda here: type is " ++ showImp imps False (delab i ty)

130pshow i (InfiniteUnify x tm env)

131 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

132 " would lead to infinite value" ++

@@ -138,7 +138,7 @@ pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

138pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

139pshow i (NoTypeDecl n) = "No type declaration for " ++ show n

140pshow i (NoSuchVariable n) = "No such variable " ++ show n

141−pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp True (delab i t)

141+pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp True False (delab i t)

142pshow i UniverseError = "Universe inconsistency"

143pshow i ProgramLineComment = "Program line next to comment"

144pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

src/Idris/ElabDecls.hs+25−25

@@ -51,11 +51,11 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

51 do checkUndefined fc n

52 ctxt <- getContext

53 i <- getIState

54− logLvl 3 $ show n ++ " pre-type " ++ showImp True ty'

54+ logLvl 3 $ show n ++ " pre-type " ++ showImp True False ty'

55 ty' <- addUsingConstraints syn fc ty'

56 ty' <- implicit syn n ty'

57 let ty = addImpl i ty'

58− logLvl 2 $ show n ++ " type " ++ showImp True ty

58+ logLvl 2 $ show n ++ " type " ++ showImp True False ty

59 ((tyT, defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

60 (erun fc (build i info False n ty))

61 ds <- checkDef fc defer

@@ -482,7 +482,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)

482 i <- getIState

483 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

484 let t = addImpl i t_in

485− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

485+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True False t

486 ((t', defer, is), log) <- tclift $ elaborate ctxt n (TType (UVal 0)) []

487 (erun fc (build i info False n t))

488 logLvl 2 $ "Rechecking " ++ show t'

@@ -589,9 +589,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

589 missing' <- filterM (checkPossible info fc True n) missing

590 let clhs = map getLHS pdef

591 logLvl 2 $ "Must be unreachable:\n" ++

592− showSep "\n" (map (showImp True) missing') ++

592+ showSep "\n" (map (showImp True False) missing') ++

593 "\nAgainst: " ++

594− showSep "\n" (map (\t -> showImp True (delab ist t)) (map getLHS pdef))

594+ showSep "\n" (map (\t -> showImp True False (delab ist t)) (map getLHS pdef))

595 -- filter out anything in missing' which is

596 -- matched by any of clhs. This might happen since

597 -- unification may force a variable to take a

@@ -711,7 +711,7 @@ elabVal info aspat tm_in

711 = do ctxt <- getContext

712 i <- getIState

713 let tm = addImpl i tm_in

714− logLvl 10 (showImp True tm)

714+ logLvl 10 (showImp True False tm)

715 -- try:

716 -- * ordinary elaboration

717 -- * elaboration as a Type

@@ -776,7 +776,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

776 _ -> []

777 let params = getParamsInType i [] fn_is fn_ty

778 let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))

779− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)

779+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True False lhs)

780 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

781 ((lhs', dlhs, []), _) <-

782 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

@@ -806,10 +806,10 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

806 mapM_ (elabDecl' EAll info) wbefore

807 -- Now build the RHS, using the type of the LHS as the goal.

808 i <- getIState -- new implicits from where block

809− logLvl 5 (showImp True (expandParams decorate newargs defs (defs \\ decls) rhs_in))

809+ logLvl 5 (showImp True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))

810 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

811 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

812− logLvl 2 $ "RHS: " ++ showImp True rhs

812+ logLvl 2 $ "RHS: " ++ showImp True False rhs

813 ctxt <- getContext -- new context with where block added

814 logLvl 5 "STARTING CHECK"

815 ((rhs', defer, is), _) <-

@@ -911,7 +911,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

911 -- pattern bindings

912 i <- getIState

913 let lhs = addImplPat i lhs_in

914− logLvl 5 ("LHS: " ++ showImp True lhs)

914+ logLvl 5 ("LHS: " ++ showImp True False lhs)

915 ((lhs', dlhs, []), _) <-

916 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

917 (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

@@ -923,7 +923,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

923 logLvl 5 ("Checked " ++ show clhs)

924 let bargs = getPBtys lhs_tm

925 let wval = addImplBound i (map fst bargs) wval_in

926− logLvl 5 ("Checking " ++ showImp True wval)

926+ logLvl 5 ("Checking " ++ showImp True False wval)

927 -- Elaborate wval in this context

928 ((wval', defer, is), _) <-

929 tclift $ elaborate ctxt (MN 0 "withRHS")

@@ -980,7 +980,7 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

980 (map (pexp . (PRef fc) . fst) bargs_pre ++

981 pexp wval :

982 (map (pexp . (PRef fc) . fst) bargs_post))

983− logLvl 5 ("New RHS " ++ showImp True rhs)

983+ logLvl 5 ("New RHS " ++ showImp True False rhs)

984 ctxt <- getContext -- New context with block added

985 i <- getIState

986 ((rhs', defer, is), _) <-

@@ -1009,8 +1009,8 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

1009 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

1010 = do i <- getIState

1011 let tm = addImplPat i tm_in

1012− logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

1012+ logLvl 2 ("Matching " ++ showImp True False tm ++ " against " ++

1013− showImp True toplhs)

1013+ showImp True False toplhs)

1014 case matchClause i toplhs tm of

1015 Left f -> fail $ show fc ++ ":with clause does not match top level"

1016 Right mvars ->

@@ -1020,8 +1020,8 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

1020 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

1021 = do i <- getIState

1022 let tm = addImplPat i tm_in

1023− logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

1023+ logLvl 2 ("Matching " ++ showImp True False tm ++ " against " ++

1024− showImp True toplhs)

1024+ showImp True False toplhs)

1025 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

1026 case matchClause i toplhs tm of

1027 Left _ -> fail $ show fc ++ "with clause does not match top level"

@@ -1118,7 +1118,7 @@ elabClass info syn doc fc constraints tn ps ds

1118 getMName (PTy _ _ _ _ n _) = nsroot n

1119 tdecl allmeths (PTy doc syn _ o n t)

1120 = do t' <- implicit' syn allmeths n t

1121− logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True t'

1121+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp True False t'

1122 return ( (n, (toExp (map fst ps) Exp t')),

1123 (n, (doc, o, (toExp (map fst ps) Imp t'))),

1124 (n, (syn, o, t) ) )

@@ -1152,8 +1152,8 @@ elabClass info syn doc fc constraints tn ps ds

1152 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1153 let rhs = PResolveTC (FC "HACK" 0)

1154 let ty = PPi constraint (MN 0 "pc") c con

1155− iLOG (showImp True ty)

1155+ iLOG (showImp True False ty)

1156− iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

1156+ iLOG (showImp True False lhs ++ " = " ++ showImp True False rhs)

1157 i <- getIState

1158 let conn = case con of

1159 PRef _ n -> n

@@ -1177,9 +1177,9 @@ elabClass info syn doc fc constraints tn ps ds

1177 let anames = map (\x -> MN x "arg") [0..]

1178 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1179 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1180− iLOG (showImp True ty)

1180+ iLOG (showImp True False ty)

1181 iLOG (show (m, ty', capp, margs))

1182− iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

1182+ iLOG (showImp True False lhs ++ " = " ++ showImp True False rhs)

1183 return [PTy doc syn fc o m ty',

1184 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1185

@@ -1520,8 +1520,8 @@ elabCaseBlock info d@(PClauses f o n ps)

1520

1521checkInferred :: FC -> PTerm -> PTerm -> Idris ()

1522checkInferred fc inf user =

1523− do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n\nFROM\n\n" ++

1523+ do logLvl 6 $ "Checked to\n" ++ showImp True False inf ++ "\n\nFROM\n\n" ++

1524− showImp True user

1524+ showImp True False user

1525 logLvl 10 $ "Checking match"

1526 i <- getIState

1527 tclift $ case matchClause' True i user inf of

@@ -1538,8 +1538,8 @@ checkInferred fc inf user =

1538inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

1539inferredDiff fc inf user =

1540 do i <- getIState

1541− logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

1541+ logLvl 6 $ "Checked to\n" ++ showImp True False inf ++ "\n" ++

1542− showImp True user

1542+ showImp True False user

1543 tclift $ case matchClause' True i user inf of

1544 Right vs -> return False

1545 Left (x, y) -> return True

src/Idris/REPL.hs+11−11

@@ -304,8 +304,8 @@ process fn (Eval t)

304 logLvl 3 $ "Raw: " ++ show (tm', ty')

305 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

306 imp <- impShow

307− iResult (showImp imp (delab ist tm') ++ " : " ++

307+ iResult (showImp imp True (delab ist tm') ++ " : " ++

308− showImp imp (delab ist ty'))

308+ showImp imp True (delab ist ty'))

309process fn (ExecVal t)

310 = do ctxt <- getContext

311 ist <- getIState

@@ -314,15 +314,15 @@ process fn (ExecVal t)

314 let ty' = normaliseAll ctxt [] ty

315 res <- execute tm

316 imp <- impShow

317− iResult (showImp imp (delab ist res) ++ " : " ++

317+ iResult (showImp imp True (delab ist res) ++ " : " ++

318− showImp imp (delab ist ty'))

318+ showImp imp True (delab ist ty'))

319process fn (Check (PRef _ n))

320 = do ctxt <- getContext

321 ist <- getIState

322 imp <- impShow

323 case lookupNames n ctxt of

324 ts@(_:_) -> do mapM_ (\n -> iputStrLn $ show n ++ " : " ++

325− showImp imp (delabTy ist n)) ts

325+ showImp imp True (delabTy ist n)) ts

326 iResult ""

327 [] -> iFail $ "No such variable " ++ show n

328process fn (Check t)

@@ -333,8 +333,8 @@ process fn (Check t)

333 let ty' = normaliseC ctxt [] ty

334 case tm of

335 TType _ -> iResult ("Type : Type 1")

336− _ -> iResult (showImp imp (delab ist tm) ++ " : " ++

336+ _ -> iResult (showImp imp True (delab ist tm) ++ " : " ++

337− showImp imp (delab ist ty))

337+ showImp imp True (delab ist ty))

338

339process fn (DocStr n) = do i <- getIState

340 case lookupCtxtName n (idris_docstrings i) of

@@ -364,8 +364,8 @@ process fn (Defn n) = do i <- getIState

364 [t] -> iputStrLn (showTotal t i)

365 _ -> return ()

366 where printCase i (_, lhs, rhs)

367− = do iputStrLn (showImp True (delab i lhs) ++ " = " ++

367+ = do iputStrLn (showImp True False (delab i lhs) ++ " = " ++

368− showImp True (delab i rhs))

368+ showImp True False (delab i rhs))

369process fn (TotCheck n) = do i <- getIState

370 case lookupTotal n (tt_ctxt i) of

371 [t] -> iResult (showTotal t i)

@@ -505,7 +505,7 @@ process fn (Missing n)

505 case lookupCtxt n (idris_patdefs i) of

506 [] -> return ()

507 [(_, tms)] ->

508− iResult (showSep "\n" (map (showImp True) tms))

508+ iResult (showSep "\n" (map (showImp True False) tms))

509 _ -> iFail $ "Ambiguous name"

510process fn (DynamicLink l) = do i <- getIState

511 let lib = trim l

@@ -553,7 +553,7 @@ dumpInstance n = do i <- getIState

553 ctxt <- getContext

554 imp <- impShow

555 case lookupTy n ctxt of

556− ts -> mapM_ (\t -> iputStrLn $ showImp imp (delab i t)) ts

556+ ts -> mapM_ (\t -> iputStrLn $ showImp imp False (delab i t)) ts

557

558showTotal t@(Partial (Other ns)) i

559 = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)