f1c3c75 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'color-repl' of https://github.com/david-christiansen/Idris-dev into david-christiansen-color-repl

f1c3c75Edwin Brady13 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -6,6 +6,7 @@ New in 0.9.10:

6* Add 'quoteGoal x by p in e' which makes x equal to p applied to the goal

7 in the scope e

8* At the REPL, "it" now refers to the previous expression

9+* Semantic colouring at the REPL. Turn this off with --nocolour.

10Internal changes

11Internal changes

idris.cabal+2−2

@@ -250,7 +250,7 @@ Executable idris

250 Core.ShellParser, Core.Unify, Core.Elaborate,

251 Core.CaseTree, Core.Constraints,

252

253− Idris.AbsSyntax, Idris.AbsSyntaxTree,

253+ Idris.AbsSyntax, Idris.AbsSyntaxTree, Idris.Colours,

254 Idris.Parser, Idris.Help, Idris.IdeSlave, Idris.REPL,

255 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

256 Idris.Delaborate, Idris.Primitives, Idris.Imports,

@@ -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/Core/Evaluate.hs+12−3

@@ -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

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

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

749

750isConName :: Name -> Context -> Bool

751−isConName n ctxt

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

752+

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

754+isTConName n ctxt

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

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

753 case tfst def of

756 case tfst def of

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

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

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

756 _ -> return False

758 _ -> return False

757

759

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

761+isDConName n ctxt

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

763+ case tfst def of

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

765+ _ -> return False

766+

758isFnName :: Name -> Context -> Bool

767isFnName :: Name -> Context -> Bool

759isFnName n ctxt

768isFnName n ctxt

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

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

src/Idris/AbsSyntax.hs+10−2

@@ -481,6 +481,14 @@ allImportDirs :: IState -> Idris [FilePath]

481allImportDirs i = do let optdirs = opt_importdirs (idris_options i)

482 return ("." : reverse optdirs)

483

484+colourise :: Idris Bool

485+colourise = do i <- getIState

486+ return $ idris_colourRepl i

487+

488+setColourise :: Bool -> Idris ()

489+setColourise b = do i <- getIState

490+ putIState $ i { idris_colourRepl = b }

491+

484impShow :: Idris Bool

492impShow :: Idris Bool

485impShow = do i <- getIState

493impShow = do i <- getIState

486 return (opt_showimp (idris_options i))

494 return (opt_showimp (idris_options i))

@@ -1170,7 +1178,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

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

1171

1179

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

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

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

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

1174 let (ns, ss) = fs tm in

1182 let (ns, ss) = fs tm in

1175 runState (pos ns ss tm) []

1183 runState (pos ns ss tm) []

1176 where fs (PPi p n t sc)

1184 where fs (PPi p n t sc)

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

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

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

1202

1210

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

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

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+145−102

@@ -12,10 +12,13 @@ import IRTS.CodegenCommon

12import Util.Pretty

13import Util.DynamicLinker

15+import Idris.Colours

16+

15import Paths_idris

17import Paths_idris

17import System.Console.Haskeline

19import System.Console.Haskeline

21+

19import Control.Monad.Trans.State.Strict

22import Control.Monad.Trans.State.Strict

21import Data.List

24import Data.List

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

28 opt_typecase :: Bool,

31 opt_typecase :: Bool,

29 opt_typeintype :: Bool,

32 opt_typeintype :: Bool,

30 opt_coverage :: Bool,

33 opt_coverage :: Bool,

31− opt_showimp :: Bool,

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

32 opt_errContext :: Bool,

35 opt_errContext :: Bool,

33 opt_repl :: Bool,

36 opt_repl :: Bool,

34 opt_verbose :: Bool,

37 opt_verbose :: Bool,

@@ -117,7 +120,8 @@ data IState = IState {

117 compiled_so :: Maybe String,

120 compiled_so :: Maybe String,

118 idris_dynamic_libs :: [DynamicLib],

121 idris_dynamic_libs :: [DynamicLib],

119 idris_language_extensions :: [LanguageExt],

122 idris_language_extensions :: [LanguageExt],

120− idris_outputmode :: OutputMode

123+ idris_outputmode :: OutputMode,

124+ idris_colourRepl :: Bool

121 }

125 }

122

126

123data SizeChange = Smaller | Same | Bigger | Unknown

127data SizeChange = Smaller | Same | Bigger | Unknown

@@ -174,6 +178,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

174 emptyContext emptyContext emptyContext emptyContext

178 emptyContext emptyContext emptyContext emptyContext

175 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []

179 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []

176 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

180 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

181+ True

177

182

178-- | The monad for the main REPL - reading and processing files and updating

183-- | The monad for the main REPL - reading and processing files and updating

179-- global state (hence the IO inner monad).

184-- global state (hence the IO inner monad).

@@ -232,6 +237,7 @@ data Opt = Filename String

232 | Ver

237 | Ver

233 | Usage

238 | Usage

234 | Quiet

239 | Quiet

240+ | ColourREPL Bool

235 | Ideslave

241 | Ideslave

236 | ShowLibs

242 | ShowLibs

237 | ShowLibdir

243 | ShowLibdir

@@ -245,8 +251,8 @@ data Opt = Filename String

245 | DefaultTotal

251 | DefaultTotal

246 | DefaultPartial

252 | DefaultPartial

247 | WarnPartial

253 | WarnPartial

248− | NoCoverage

254+ | NoCoverage

249− | ErrContext

255+ | ErrContext

250 | ShowImpl

256 | ShowImpl

251 | Verbose

257 | Verbose

252 | IBCSubDir String

258 | IBCSubDir String

@@ -789,7 +795,7 @@ expandNS syn n = case syn_namespace syn of

789--- Pretty printing declarations and terms

795--- Pretty printing declarations and terms

790

796

791instance Show PTerm where

797instance Show PTerm where

792− show tm = showImp False tm

798+ show tm = showImp Nothing False False tm

793

799

794instance Pretty PTerm where

800instance Pretty PTerm where

795 pretty = prettyImp False

801 pretty = prettyImp False

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

804 show d = showDImp False d

810 show d = showDImp False d

805

811

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

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

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

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

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

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

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

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

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

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

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

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

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

814

820

815showCImp :: Bool -> PClause -> String

821showCImp :: Bool -> PClause -> String

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

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

817− = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r

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

818 ++ " where " ++ show w

824 ++ " where " ++ show w

819 where

825 where

820 showWs [] = ""

826 showWs [] = ""

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

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

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

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

823− = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r

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

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

830 ++ " { " ++ show w ++ " } "

825 where

831 where

826 showWs [] = ""

832 showWs [] = ""

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

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

828

834

829

835

830showDImp :: Bool -> PData -> String

836showDImp :: Bool -> PData -> String

831showDImp impl (PDatadecl n ty cons)

837showDImp impl (PDatadecl n ty cons)

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

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

833 ++ showSep "\n\t| "

839 ++ showSep "\n\t| "

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

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

835

841

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

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

837getImps [] = []

843getImps [] = []

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

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

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

852getAll = map getTm

858getAll = map getTm

853

859

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

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

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

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

863+ -> Doc

855prettyImp impl = prettySe 10

864prettyImp impl = prettySe 10

856 where

865 where

857 prettySe p (PQuote r) =

866 prettySe p (PQuote r) =

@@ -1037,108 +1046,142 @@ prettyImp impl = prettySe 10

1037 bracket outer inner doc

1046 bracket outer inner doc

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

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

1039 | otherwise = doc

1048 | otherwise = doc

1040−

1049+

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

1050+-- | Show Idris name

1042−showImp impl tm = se 10 tm where

1051+showName :: Maybe IState -- ^^ the Idris state, for information about names

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

1052+ -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

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

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

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

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

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

1055+ -> Name -- ^^ the term to show

1056+ -> String

1057+showName ist bnd impl colour n = if colour then colourise n else showbasic n

1047− else showbasic n

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

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

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

1049− showbasic (MN _ s) = s

1060+ showbasic (MN _ s) = s

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

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

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

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

1064+ case ctxt' of

1065+ Nothing -> name

1066+ Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit name

1067+ else colouriseBound name

1068+ | isDConName n ctxt -> colouriseData name

1069+ | isFnName n ctxt -> colouriseFun name

1070+ | isTConName n ctxt -> colouriseType name

1071+ | otherwise -> name

1072+

1073+-- | Show Idris term

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

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

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

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

1078+ -> String

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

1080+ perhapsColourise :: (String -> String) -> String -> String

1081+ perhapsColourise col str = if colour then col str else str

1082+

1083+ se :: Int -> [(Name, Bool)] -> PTerm -> String

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

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

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

1087+ se p bnd (PRef fc n) = showName ist bnd impl colour n

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

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

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

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

1053− ++ se 10 sc

1090+ ++ se 10 ((n, False):bnd) sc

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

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

1092+ " = " ++ se 10 bnd v ++

1055− " in " ++ se 10 sc

1093+ " in " ++ se 10 ((n, False):bnd) sc

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

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

1057 | n `elem` allNamesIn sc || impl

1095 | n `elem` allNamesIn sc || impl

1058 = bracket p 2 $

1096 = bracket p 2 $

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

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

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

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

1061 ") " ++ st ++

1099 ") " ++ st ++

1062− "-> " ++ se 10 sc

1100+ "-> " ++ se 10 ((n, False):bnd) sc

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

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

1064 where st = case s of

1102 where st = case s of

1065 Static -> "[static] "

1103 Static -> "[static] "

1066 _ -> ""

1104 _ -> ""

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

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

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

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

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

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

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

1108+ "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1071− | otherwise = se 10 sc

1109+ | otherwise = se 10 ((n, True):bnd) sc

1072 where st = case s of

1110 where st = case s of

1073 Static -> "[static] "

1111 Static -> "[static] "

1074 _ -> ""

1112 _ -> ""

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

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

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

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

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

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

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

1116+ = bracket p 2 $

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

1118+ se 10 ((n, False):bnd) sc

1079− se p e

1119+ se p bnd e

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

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

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

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

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

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

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

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

1084− | not impl = show f

1124+ | not impl = se p bnd hd

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

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

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

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

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

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

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

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

1089− se p (PApp _ f as)

1129+ se p bnd (PApp _ f as)

1090 = let args = getExps as in

1130 = let args = getExps as in

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

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

1092− else concatMap seArg args

1132+ else concatMap (seArg bnd) args

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

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

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

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

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

1096− se p (PRefl _ t)

1136+ se p bnd (PRefl _ t)

1097− | not impl = "refl"

1137+ | not impl = perhapsColourise colouriseData "refl"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1108− se p PType = "Type"

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

1109− se p (PConstant c) = show c

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

1150+ where cfun (AType _) = colouriseType

1151+ cfun StrType = colouriseType

1152+ cfun PtrType = colouriseType

1153+ cfun VoidType = colouriseType

1154+ cfun _ = colouriseData

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

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

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

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

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

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

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

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

1114− se p PImpossible = "impossible"

1159+ se p bnd PImpossible = "impossible"

1115− se p Placeholder = "_"

1160+ se p bnd Placeholder = "_"

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

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

1117− se p (PElabError s) = show s

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

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

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

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

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

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

1123−

1166+

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

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

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

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

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

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

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

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

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

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

1129 all isImp imps,

1172 all isImp imps,

1130− Just tl' <- slist' p tl

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

1131 = Just (hd:tl')

1174 = Just (hd:tl')

1132 where

1175 where

1133 isImp (PImp {}) = True

1176 isImp (PImp {}) = True

1134 isImp _ = False

1177 isImp _ = False

1135− slist' _ _ = Nothing

1178+ slist' _ _ _ = Nothing

1136

1179

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

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

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

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

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

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

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

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

1141− slist _ _ = Nothing

1184+ slist _ _ _ = Nothing

1142

1185

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

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

1144 -- Nat ones.

1187 -- Nat ones.

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

1152

1195

1153 natns = "Prelude.Nat."

1196 natns = "Prelude.Nat."

1154

1197

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

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

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

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

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

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

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

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

1159

1202

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

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

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

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

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

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

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

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

1164

1207

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

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

1166 | otherwise = str

1209 | otherwise = str

src/Idris/Colours.hsnew file+32

@@ -0,0 +1,32 @@

1+module Idris.Colours where

3+import System.Console.ANSI

5+-- Set the colour of a string using POSIX escape codes

6+colourise :: Color -> ColorIntensity -> String -> String

7+colourise c i str = let sgr = [SetColor Foreground i c]

8+ in setSGRCode sgr ++ str ++ setSGRCode [Reset]

10+colouriseKwd :: String -> String

11+colouriseKwd kwd = setSGRCode [SetUnderlining SingleUnderline

12+ , SetConsoleIntensity BoldIntensity

13+ , SetColor Foreground Vivid Black

14+ ] ++ kwd ++ setSGRCode [Reset]

15+

16+colouriseBound :: String -> String

17+colouriseBound = colourise Magenta Vivid

18+

19+colouriseImplicit :: String -> String

20+colouriseImplicit str = let sgr = [ SetColor Foreground Vivid Magenta

21+ , SetUnderlining SingleUnderline

22+ ]

23+ in setSGRCode sgr ++ str ++ setSGRCode [Reset]

24+

25+colouriseFun :: String -> String

26+colouriseFun = colourise Green Vivid

27+

28+colouriseType :: String -> String

29+colouriseType = colourise Blue Vivid

30+

31+colouriseData :: String -> String

32+colouriseData = colourise Red Vivid

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 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) 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+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 Nothing imps False (delab i x)

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

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

113− ++ showImp imps (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 (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 (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 (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 (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 (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 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 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 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) missing') ++

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

593 "\nAgainst: " ++

594− showSep "\n" (map (\t -> showImp True (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

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

713 = do ctxt <- getContext

714 i <- getIState

715 let tm = addImpl i tm_in

716− logLvl 10 (showImp True tm)

716+ logLvl 10 (showImp Nothing True False tm)

717 -- try:

718 -- * ordinary elaboration

719 -- * elaboration as a Type

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

778 _ -> []

779 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

808 mapM_ (elabDecl' EAll info) wbefore

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

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

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

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

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

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

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

814+ logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs

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

816 logLvl 5 "STARTING CHECK"

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

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

913 -- pattern bindings

914 i <- getIState

915 let lhs = addImplPat i lhs_in

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

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

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

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

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

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

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

926 let bargs = getPBtys lhs_tm

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

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

928+ logLvl 5 ("Checking " ++ showImp Nothing True False wval)

929 -- Elaborate wval in this context

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

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

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

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

983 pexp wval :

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

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

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

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

987 i <- getIState

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

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

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

1012 = do i <- getIState

1013 let tm = addImplPat i tm_in

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

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

1015− showImp True toplhs)

1015+ showImp Nothing True False toplhs)

1016 case matchClause i toplhs tm of

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

1018 Right mvars ->

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

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

1023 = do i <- getIState

1024 let tm = addImplPat i tm_in

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

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

1026− showImp True toplhs)

1026+ showImp Nothing True False toplhs)

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

1028 case matchClause i toplhs tm of

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

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

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

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

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

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

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

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

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

1126 (n, (syn, o, t) ) )

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

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

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

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

1157− iLOG (showImp True ty)

1157+ iLOG (showImp Nothing True False ty)

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

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

1159 i <- getIState

1160 let conn = case con of

1161 PRef _ n -> n

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

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

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

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

1182− iLOG (showImp True ty)

1182+ iLOG (showImp Nothing True False ty)

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

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

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

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

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

1187

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

1522

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

1524checkInferred fc inf user =

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

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

1526− showImp True user

1526+ showImp Nothing True False user

1527 logLvl 10 $ "Checking match"

1528 i <- getIState

1529 tclift $ case matchClause' True i user inf of

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

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

1541inferredDiff fc inf user =

1542 do i <- getIState

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

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

1544− showImp True user

1544+ showImp Nothing True False user

1545 tclift $ case matchClause' True i user inf of

1546 Right vs -> return False

1547 Left (x, y) -> return True

src/Idris/REPL.hs+27−12

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

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

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

306 imp <- impShow

307+ c <- colourise

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

308+ iResult (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

308− showImp imp (delab ist ty'))

309+ showImp (Just ist) imp c (delab ist ty'))

309process fn (ExecVal t)

310process fn (ExecVal t)

310 = do ctxt <- getContext

311 = do ctxt <- getContext

311 ist <- getIState

312 ist <- getIState

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

314 let ty' = normaliseAll ctxt [] ty

315 let ty' = normaliseAll ctxt [] ty

315 res <- execute tm

316 res <- execute tm

316 imp <- impShow

317 imp <- impShow

318+ c <- colourise

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

319+ iResult (showImp (Just ist) imp c (delab ist res) ++ " : " ++

318− showImp imp (delab ist ty'))

320+ showImp (Just ist) imp c (delab ist ty'))

319process fn (Check (PRef _ n))

321process fn (Check (PRef _ n))

320 = do ctxt <- getContext

322 = do ctxt <- getContext

321 ist <- getIState

323 ist <- getIState

322 imp <- impShow

324 imp <- impShow

325+ c <- colourise

323 case lookupNames n ctxt of

326 case lookupNames n ctxt of

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

327+ ts@(_:_) -> do mapM_ (\n -> iputStrLn $ showName (Just ist) [] False c n ++ " : " ++

325− showImp imp (delabTy ist n)) ts

328+ showImp (Just ist) imp c (delabTy ist n)) ts

326 iResult ""

329 iResult ""

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

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

328process fn (Check t)

331process fn (Check t)

@@ -330,11 +333,12 @@ process fn (Check t)

330 ctxt <- getContext

333 ctxt <- getContext

331 ist <- getIState

334 ist <- getIState

332 imp <- impShow

335 imp <- impShow

336+ c <- colourise

333 let ty' = normaliseC ctxt [] ty

337 let ty' = normaliseC ctxt [] ty

334 case tm of

338 case tm of

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

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

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

340+ _ -> iResult (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

337− showImp imp (delab ist ty))

341+ showImp (Just ist) imp c (delab ist ty))

338

342

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

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

340 case lookupCtxtName n (idris_docstrings i) of

344 case lookupCtxtName n (idris_docstrings i) of

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

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

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

365 _ -> return ()

369 _ -> return ()

366 where printCase i (_, lhs, rhs)

370 where printCase i (_, lhs, rhs)

371+ = do c <- colourise

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

372+ iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

368− showImp True (delab i rhs))

373+ showImp (Just i) True c (delab i rhs))

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

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

370 case lookupTotal n (tt_ctxt i) of

375 case lookupTotal n (tt_ctxt i) of

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

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

@@ -502,10 +507,11 @@ process fn (Pattelab t)

502

507

503process fn (Missing n)

508process fn (Missing n)

504 = do i <- getIState

509 = do i <- getIState

510+ c <- colourise

505 case lookupCtxt n (idris_patdefs i) of

511 case lookupCtxt n (idris_patdefs i) of

506 [] -> return ()

512 [] -> return ()

507 [(_, tms)] ->

513 [(_, tms)] ->

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

514+ iResult (showSep "\n" (map (showImp (Just i) True c) tms))

509 _ -> iFail $ "Ambiguous name"

515 _ -> iFail $ "Ambiguous name"

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

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

511 let lib = trim l

517 let lib = trim l

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

553 ctxt <- getContext

559 ctxt <- getContext

554 imp <- impShow

560 imp <- impShow

555 case lookupTy n ctxt of

561 case lookupTy n ctxt of

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

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

557

563

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

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

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

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

@@ -627,6 +633,10 @@ parseArgs ("-O0":ns) = OptLevel 0 : parseArgs ns

627parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

633parseArgs ("-O":n:ns) = OptLevel (read n) : parseArgs ns

628parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

634parseArgs ("--target":n:ns) = TargetTriple n : parseArgs ns

629parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

635parseArgs ("--cpu":n:ns) = TargetCPU n : parseArgs ns

636+parseArgs ("--colour":ns) = ColourREPL True : parseArgs ns

637+parseArgs ("--color":ns) = ColourREPL True : parseArgs ns

638+parseArgs ("--nocolour":ns) = ColourREPL False : parseArgs ns

639+parseArgs ("--nocolor":ns) = ColourREPL False : parseArgs ns

630parseArgs (n:ns) = Filename n : (parseArgs ns)

640parseArgs (n:ns) = Filename n : (parseArgs ns)

631

641

632helphead =

642helphead =

@@ -740,6 +750,7 @@ idrisMain opts =

740 [expr] -> return (Just expr)

750 [expr] -> return (Just expr)

741 when (DefaultTotal `elem` opts) $ do i <- getIState

751 when (DefaultTotal `elem` opts) $ do i <- getIState

742 putIState (i { default_total = True })

752 putIState (i { default_total = True })

753+ setColourise $ not quiet && last (True : opt getColour opts)

743 mapM_ addLangExt (opt getLanguageExt opts)

754 mapM_ addLangExt (opt getLanguageExt opts)

744 setREPL runrepl

755 setREPL runrepl

745 setQuiet (quiet || isJust script)

756 setQuiet (quiet || isJust script)

@@ -876,6 +887,10 @@ getOptLevel :: Opt -> Maybe Int

876getOptLevel (OptLevel x) = Just x

887getOptLevel (OptLevel x) = Just x

877getOptLevel _ = Nothing

888getOptLevel _ = Nothing

878

889

890+getColour :: Opt -> Maybe Bool

891+getColour (ColourREPL b) = Just b

892+getColour _ = Nothing

893+

879opt :: (Opt -> Maybe a) -> [Opt] -> [a]

894opt :: (Opt -> Maybe a) -> [Opt] -> [a]

880opt = mapMaybe

895opt = mapMaybe

881

896

src/Main.hs+1

@@ -80,6 +80,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

80 "Usage: idris [input file] [options]\n" ++

81 "Options:\n" ++

82 "\t--quiet Quiet mode (for editors)\n" ++

83+ "\t--[no]colour Control REPL colour highlighting" ++

83 "\t--check Type check only\n" ++

84 "\t--check Type check only\n" ++

84 "\t-o [file] Specify output filename\n" ++

85 "\t-o [file] Specify output filename\n" ++

85 "\t-i [dir] Add directory to the list of import paths\n" ++

86 "\t-i [dir] Add directory to the list of import paths\n" ++