b762f14 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Basic colourisation in REPL

commitb762f14915b0bd14f521d6be81968269664df182 authorDavid Christiansen <david@davidchristiansen.dk> dateThu 15 Aug 2013, 16:09 (13 years ago) parentffb9ea9

7 files changed+110−77

compare with master

unifiedsplit

src/Core/Evaluate.hs+12−3 src/Idris/AbsSyntax.hs+2−2 src/Idris/AbsSyntaxTree.hs+49−25 src/Idris/Coverage.hs+2−2 src/Idris/Delaborate.hs+9−9 src/Idris/ElabDecls.hs+25−25 src/Idris/REPL.hs+11−11

src/Core/Evaluate.hs+12−3

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

99 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

12− lookupTotal, lookupTyEnv, isConName, isFnName,

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

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

1414

1515import Debug.Trace

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

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

726726

727727isConName :: 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

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

730733 case tfst def of

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

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

733735 _ -> return False

734736

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+

735744isFnName :: Name -> Context -> Bool

736745isFnName n ctxt

737746 = 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

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

11711171

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

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

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

11741174 let (ns, ss) = fs tm in

11751175 runState (pos ns ss tm) []

11761176 where fs (PPi p n t sc)

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

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

12021202

12031203dumpDecl (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

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

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

12071207dumpDecl (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

804804colouriseBound :: String -> String

805805colouriseBound = colourise Magenta Vivid

806806

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+

807816instance Show PTerm where

808− show tm = showImp False False tm

817+ show tm = showImp Nothing False False tm

809818

810819instance Pretty PTerm where

811820 pretty = prettyImp False

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

820829 show d = showDImp False d

821830

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

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

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

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

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

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

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

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

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

830839

831840showCImp :: Bool -> PClause -> String

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

834843 ++ " where " ++ show w

835844 where

836845 showWs [] = ""

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

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

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

840849 ++ " { " ++ show w ++ " } "

841850 where

842851 showWs [] = ""

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

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

844853

845854

846855showDImp :: Bool -> PData -> String

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

849858 ++ 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)

851860

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

853862getImps [] = []

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

10581067 | otherwise = doc

10591068

10601069-- | Show Idris term

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

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

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

10621072 -> Bool -- ^^ whether to colourise

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

10641074 -> String

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

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

10661076 perhapsColourise :: (String -> String) -> String -> String

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

1068−

1078+

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

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

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

10721082 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

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

10751085 showbasic n@(UN _) = show n

10761086 showbasic (MN _ s) = s

10771087 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

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

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

10801099 ++ se 10 (n:bnd) sc

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

11081127 se 10 (n:bnd) sc

11091128 se p bnd e

11101129 | 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)

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

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

1114− | not impl = show f

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

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

1133+ | not impl = se p bnd hd

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

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

11171136 = 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

11191138 se p bnd (PApp _ f as)

11201139 = let args = getExps as in

11211140 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

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

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

11261145 se p bnd (PRefl _ t)

1127− | not impl = "refl"

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

1146+ | not impl = perhapsColourise colouriseData "refl"

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

11291148 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

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

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

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

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

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

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

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

11371156 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

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

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

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

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

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

src/Idris/Coverage.hs+2−2

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

53+ showSep "\n" (map (\t -> showImp Nothing True False (delab' i t 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

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

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

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

6464 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)

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

6767 return new

6868-- 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 ++

100100 "Please consider reporting at " ++ bugaddr

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

102102 = let imps = opt_showimp (idris_options i) in

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

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

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

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

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

106106 case e of

107107 Msg "" -> ""

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

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

110110pshow i (CantConvert x y env)

111111 = let imps = opt_showimp (idris_options i) in

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

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

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

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

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

115115pshow i (UnifyScope n out tm env)

116116 = let imps = opt_showimp (idris_options i) in

117117 "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 ++

119119 " is not in scope" ++

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

121121pshow i (CantInferType t)

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

123123pshow i (NonFunctionType f ty)

124124 = let imps = opt_showimp (idris_options i) in

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

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

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

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

127127pshow i (CantIntroduce ty)

128128 = 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)

130130pshow i (InfiniteUnify x tm env)

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

132132 " would lead to infinite value" ++

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

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

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

140140pshow 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)

142142pshow i UniverseError = "Universe inconsistency"

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

144144pshow 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

5151 do checkUndefined fc n

5252 ctxt <- getContext

5353 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'

5555 ty' <- addUsingConstraints syn fc ty'

5656 ty' <- implicit syn n ty'

5757 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

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

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

6161 ds <- checkDef fc defer

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

482482 i <- getIState

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

484484 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

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

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

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

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

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

590590 let clhs = map getLHS pdef

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

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

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

593593 "\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))

595595 -- filter out anything in missing' which is

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

597597 -- unification may force a variable to take a

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

711711 = do ctxt <- getContext

712712 i <- getIState

713713 let tm = addImpl i tm_in

714− logLvl 10 (showImp True False tm)

714+ logLvl 10 (showImp Nothing True False tm)

715715 -- try:

716716 -- * ordinary elaboration

717717 -- * elaboration as a Type

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

776776 _ -> []

777777 let params = getParamsInType i [] fn_is fn_ty

778778 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)

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

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

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

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

806806 mapM_ (elabDecl' EAll info) wbefore

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

808808 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))

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

811811 (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

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

814814 logLvl 5 "STARTING CHECK"

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

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

911911 -- pattern bindings

912912 i <- getIState

913913 let lhs = addImplPat i lhs_in

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

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

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

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

917917 (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)

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

924924 let bargs = getPBtys lhs_tm

925925 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)

927927 -- Elaborate wval in this context

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

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

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

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

981981 pexp wval :

982982 (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)

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

985985 i <- getIState

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

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

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

10101010 = do i <- getIState

10111011 let tm = addImplPat i tm_in

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

1013− showImp True False toplhs)

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

1013+ showImp Nothing True False toplhs)

10141014 case matchClause i toplhs tm of

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

10161016 Right mvars ->

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

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

10211021 = do i <- getIState

10221022 let tm = addImplPat i tm_in

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

1024− showImp True False toplhs)

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

1024+ showImp Nothing True False toplhs)

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

10261026 case matchClause i toplhs tm of

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

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

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

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

11201120 = 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'

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

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

11241124 (n, (syn, o, t) ) )

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

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

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

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

1155− iLOG (showImp True False ty)

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

1155+ iLOG (showImp Nothing True False ty)

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

11571157 i <- getIState

11581158 let conn = case con of

11591159 PRef _ n -> n

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

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

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

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

1180− iLOG (showImp True False ty)

1180+ iLOG (showImp Nothing True False ty)

11811181 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)

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

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

11851185

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

15201520

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

15221522checkInferred fc inf user =

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

1524− showImp True False user

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

1524+ showImp Nothing True False user

15251525 logLvl 10 $ "Checking match"

15261526 i <- getIState

15271527 tclift $ case matchClause' True i user inf of

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

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

15391539inferredDiff fc inf user =

15401540 do i <- getIState

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

1542− showImp True False user

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

1542+ showImp Nothing True False user

15431543 tclift $ case matchClause' True i user inf of

15441544 Right vs -> return False

15451545 Left (x, y) -> return True

src/Idris/REPL.hs+11−11

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

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

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

306306 imp <- impShow

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

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

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

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

309309process fn (ExecVal t)

310310 = do ctxt <- getContext

311311 ist <- getIState

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

314314 let ty' = normaliseAll ctxt [] ty

315315 res <- execute tm

316316 imp <- impShow

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

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

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

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

319319process fn (Check (PRef _ n))

320320 = do ctxt <- getContext

321321 ist <- getIState

322322 imp <- impShow

323323 case lookupNames n ctxt of

324324 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

326326 iResult ""

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

328328process fn (Check t)

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

333333 let ty' = normaliseC ctxt [] ty

334334 case tm of

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

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

337− showImp imp True (delab ist ty))

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

337+ showImp (Just ist) imp True (delab ist ty))

338338

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

340340 case lookupCtxtName n (idris_docstrings i) of

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

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

365365 _ -> return ()

366366 where printCase i (_, lhs, rhs)

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

368− showImp True False (delab i rhs))

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

368+ showImp (Just i) True False (delab i rhs))

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

370370 case lookupTotal n (tt_ctxt i) of

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

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

505505 case lookupCtxt n (idris_patdefs i) of

506506 [] -> return ()

507507 [(_, tms)] ->

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

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

509509 _ -> iFail $ "Ambiguous name"

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

511511 let lib = trim l

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

553553 ctxt <- getContext

554554 imp <- impShow

555555 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

557557

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

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