b762f14 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Basic colourisation in REPL

b762f14David Christiansen13 years ago

src/Core/Evaluate.hs+12−3

compare with master

unifiedsplit

@@ -9,7 +9,7 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

9 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

12− lookupTotal, lookupTyEnv, isConName, isFnName,

12+ lookupTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

13 Value(..), Quote(..), evalState, initEval) where

15import Debug.Trace

@@ -725,13 +725,22 @@ lookupTy n ctxt

725 (CaseOp _ ty _ _ _ _ _ _) -> return ty

726

727isConName :: Name -> Context -> Bool

728−isConName n ctxt

728+isConName n ctxt = isTConName n ctxt || isDConName n ctxt

729+

730+isTConName :: Name -> Context -> Bool

731+isTConName n ctxt

729 = or $ do def <- lookupCtxt n (definitions ctxt)

732 = or $ do def <- lookupCtxt n (definitions ctxt)

730 case tfst def of

733 case tfst def of

731− (TyDecl (DCon _ _) _) -> return True

732 (TyDecl (TCon _ _) _) -> return True

734 (TyDecl (TCon _ _) _) -> return True

733 _ -> return False

735 _ -> return False

734

736

737+isDConName :: Name -> Context -> Bool

738+isDConName n ctxt

739+ = or $ do def <- lookupCtxt n (definitions ctxt)

740+ case tfst def of

741+ (TyDecl (DCon _ _) _) -> return True

742+ _ -> return False

743+

735isFnName :: Name -> Context -> Bool

744isFnName :: Name -> Context -> Bool

736isFnName n ctxt

745isFnName n ctxt

737 = or $ do def <- lookupCtxt n (definitions ctxt)

746 = or $ do def <- lookupCtxt n (definitions ctxt)

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 False tm) $

1173+findStatics ist tm = trace (showImp Nothing 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 False t

1204+dumpDecl (PTy _ _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp Nothing 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+49−25

@@ -804,8 +804,17 @@ colouriseKwd kwd = setSGRCode [SetUnderlining SingleUnderline

804colouriseBound :: String -> String

805colouriseBound = colourise Magenta Vivid

806

807+colouriseFun :: String -> String

808+colouriseFun = colourise Green Vivid

809+

810+colouriseType :: String -> String

811+colouriseType = colourise Blue Vivid

812+

813+colouriseData :: String -> String

814+colouriseData = colourise Red Vivid

815+

807instance Show PTerm where

816instance Show PTerm where

808− show tm = showImp False False tm

817+ show tm = showImp Nothing False False tm

809

818

810instance Pretty PTerm where

819instance Pretty PTerm where

811 pretty = prettyImp False

820 pretty = prettyImp False

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

820 show d = showDImp False d

829 show d = showDImp False d

821

830

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

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

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

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

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

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

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

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

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

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

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

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

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

830

839

831showCImp :: Bool -> PClause -> String

840showCImp :: Bool -> PClause -> String

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

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

833− = showImp impl False l ++ showWs ws ++ " = " ++ showImp impl False r

842+ = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r

834 ++ " where " ++ show w

843 ++ " where " ++ show w

835 where

844 where

836 showWs [] = ""

845 showWs [] = ""

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

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

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

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

839− = showImp impl False l ++ showWs ws ++ " with " ++ showImp impl False r

848+ = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r

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

849 ++ " { " ++ show w ++ " } "

841 where

850 where

842 showWs [] = ""

851 showWs [] = ""

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

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

844

853

845

854

846showDImp :: Bool -> PData -> String

855showDImp :: Bool -> PData -> String

847showDImp impl (PDatadecl n ty cons)

856showDImp impl (PDatadecl n ty cons)

848− = "data " ++ show n ++ " : " ++ showImp impl False ty ++ " where\n\t"

857+ = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"

849 ++ showSep "\n\t| "

858 ++ showSep "\n\t| "

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

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

851

860

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

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

853getImps [] = []

862getImps [] = []

@@ -1058,23 +1067,33 @@ prettyImp impl = prettySe 10

1058 | otherwise = doc

1067 | otherwise = doc

1059

1068

1060-- | Show Idris term

1069-- | Show Idris term

1070+showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers

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

1071+ -> Bool -- ^^ whether to show implicits

1062 -> Bool -- ^^ whether to colourise

1072 -> Bool -- ^^ whether to colourise

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

1073 -> PTerm -- ^^ the term to show

1064 -> String

1074 -> String

1065−showImp impl colour tm = se 10 [] tm where

1075+showImp ist impl colour tm = se 10 [] tm where

1066 perhapsColourise :: (String -> String) -> String -> String

1076 perhapsColourise :: (String -> String) -> String -> String

1067 perhapsColourise col str = if colour then col str else str

1077 perhapsColourise col str = if colour then col str else str

1068−

1078+

1069 se :: Int -> [Name] -> PTerm -> String

1079 se :: Int -> [Name] -> PTerm -> String

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

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

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

1081 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 ++ "]"

1082 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

1083+ se p bnd (PRef fc n) = if colour then colourise n else showbasic n

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

1084 where name = if impl then show n else showbasic n

1075 showbasic n@(UN _) = show n

1085 showbasic n@(UN _) = show n

1076 showbasic (MN _ s) = s

1086 showbasic (MN _ s) = s

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

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

1088+ fst3 (x, _, _) = x

1089+ colourise n = let ctxt' = fmap tt_ctxt ist in

1090+ case ctxt' of

1091+ Nothing -> name

1092+ Just ctxt | n `elem` bnd -> colouriseBound name

1093+ | isDConName n ctxt -> colouriseData name

1094+ | isFnName n ctxt -> colouriseFun name

1095+ | isTConName n ctxt -> colouriseType name

1096+ | otherwise -> name

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

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

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

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

1080 ++ se 10 (n:bnd) sc

1099 ++ se 10 (n:bnd) sc

@@ -1108,14 +1127,14 @@ showImp impl colour tm = se 10 [] tm where

1108 se 10 (n:bnd) sc

1127 se 10 (n:bnd) sc

1109 se p bnd e

1128 se p bnd e

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

1129 | Just str <- slist p bnd e = str

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

1130+ | Just num <- snat p e = perhapsColourise colouriseData (show num)

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

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

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

1132+ se p bnd (PApp _ hd@(PRef _ f) [])

1114− | not impl = show f

1133+ | not impl = se p bnd hd

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

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

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

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

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

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

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

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

1119 se p bnd (PApp _ f as)

1138 se p bnd (PApp _ f as)

1120 = let args = getExps as in

1139 = let args = getExps as in

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

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

@@ -1124,19 +1143,24 @@ showImp impl colour tm = se 10 [] tm where

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

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

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

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

1126 se p bnd (PRefl _ t)

1145 se p bnd (PRefl _ t)

1127− | not impl = "refl"

1146+ | not impl = perhapsColourise colouriseData "refl"

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

1147+ | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"

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

1148 se p bnd (PResolveTC _) = "resolvetc"

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

1149+ se p bnd (PTrue _) = perhapsColourise colouriseType "()"

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

1150+ se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"

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

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

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

1152 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 ++ ")"

1153 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 ++ ")"

1154 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 ++ ")"

1155 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) ++ "|)"

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

1138− se p bnd PType = "Type"

1157+ se p bnd PType = perhapsColourise colouriseType "Type"

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

1158+ se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)

1159+ where cfun (AType _) = colouriseType

1160+ cfun StrType = colouriseType

1161+ cfun PtrType = colouriseType

1162+ cfun VoidType = colouriseType

1163+ cfun _ = colouriseData

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

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

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

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

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

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

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 False (delab' i t True)) xs)

53+ showSep "\n" (map (\t -> showImp Nothing 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 False) new)

65+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing 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+9−9

@@ -100,8 +100,8 @@ 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 False (delab i x)

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

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

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

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

106 case e of

107 Msg "" -> ""

@@ -109,24 +109,24 @@ pshow i (CantUnify _ x y e sc s)

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 False (delab i x) ++ " with "

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

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

113+ ++ showImp Nothing 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 False (delab i tm) ++ " as " ++ show out ++

118+ ++ showImp Nothing 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 False (delab i f) ++ " does not have a function type ("

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

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

126+ ++ showImp Nothing 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 False (delab i ty)

129+ "Can't use lambda here: type is " ++ showImp Nothing 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 False (delab i t)

141+pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing 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 False ty'

54+ logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing 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 False ty

58+ logLvl 2 $ show n ++ " type " ++ showImp Nothing 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 False t

485+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing 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 False) missing') ++

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

593 "\nAgainst: " ++

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

594+ showSep "\n" (map (\t -> showImp Nothing 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 False tm)

714+ logLvl 10 (showImp Nothing 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 False lhs)

779+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing 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 False (expandParams decorate newargs defs (defs \\ decls) rhs_in))

809+ logLvl 5 (showImp Nothing 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 False rhs

812+ logLvl 2 $ "RHS: " ++ showImp Nothing 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 False lhs)

914+ logLvl 5 ("LHS: " ++ showImp Nothing 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 False wval)

926+ logLvl 5 ("Checking " ++ showImp Nothing 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 False rhs)

983+ logLvl 5 ("New RHS " ++ showImp Nothing 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 False tm ++ " against " ++

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

1013− showImp True False toplhs)

1013+ showImp Nothing 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 False tm ++ " against " ++

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

1024− showImp True False toplhs)

1024+ showImp Nothing 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 False t'

1121+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing 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 False ty)

1155+ iLOG (showImp Nothing True False ty)

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

1156+ iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing 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 False ty)

1180+ iLOG (showImp Nothing True False ty)

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

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

1182+ iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing 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 False inf ++ "\n\nFROM\n\n" ++

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

1524− showImp True False user

1524+ showImp Nothing 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 False inf ++ "\n" ++

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

1542− showImp True False user

1542+ showImp Nothing 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 True (delab ist tm') ++ " : " ++

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

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

308+ showImp (Just ist) 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 True (delab ist res) ++ " : " ++

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

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

318+ showImp (Just ist) 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 True (delabTy ist n)) ts

325+ showImp (Just ist) 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 True (delab ist tm) ++ " : " ++

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

337− showImp imp True (delab ist ty))

337+ showImp (Just ist) 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 False (delab i lhs) ++ " = " ++

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

368− showImp True False (delab i rhs))

368+ showImp (Just i) 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 False) tms))

508+ iResult (showSep "\n" (map (showImp (Just i) 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 False (delab i t)) ts

556+ ts -> mapM_ (\t -> iputStrLn $ showImp Nothing 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)