@@ -12,10 +12,13 @@ import IRTS.CodegenCommon
1212import Util.Pretty
1313import Util.DynamicLinker
1414
15+import Idris.Colours
16+
1517import Paths_idris
1618
1719import System.Console.Haskeline
1820
21+
1922import Control.Monad.Trans.State.Strict
2023
2124import Data.List
@@ -28,7 +31,7 @@ data IOption = IOption { opt_logLevel :: Int,
2831 opt_typecase :: Bool,
2932 opt_typeintype :: Bool,
3033 opt_coverage :: Bool,
31− opt_showimp :: Bool,
34+ opt_showimp :: Bool, -- ^^ show implicits
3235 opt_errContext :: Bool,
3336 opt_repl :: Bool,
3437 opt_verbose :: Bool,
@@ -117,7 +120,8 @@ data IState = IState {
117120 compiled_so :: Maybe String,
118121 idris_dynamic_libs :: [DynamicLib],
119122 idris_language_extensions :: [LanguageExt],
120− idris_outputmode :: OutputMode
123+ idris_outputmode :: OutputMode,
124+ idris_colourRepl :: Bool
121125 }
122126
123127data SizeChange = Smaller | Same | Bigger | Unknown
@@ -174,6 +178,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
174178 emptyContext emptyContext emptyContext emptyContext
175179 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []
176180 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput
181+ True
177182
178183-- | The monad for the main REPL - reading and processing files and updating
179184-- global state (hence the IO inner monad).
@@ -232,6 +237,7 @@ data Opt = Filename String
232237 | Ver
233238 | Usage
234239 | Quiet
240+ | ColourREPL Bool
235241 | Ideslave
236242 | ShowLibs
237243 | ShowLibdir
@@ -245,8 +251,8 @@ data Opt = Filename String
245251 | DefaultTotal
246252 | DefaultPartial
247253 | WarnPartial
248− | NoCoverage
249− | ErrContext
254+ | NoCoverage
255+ | ErrContext
250256 | ShowImpl
251257 | Verbose
252258 | IBCSubDir String
@@ -789,7 +795,7 @@ expandNS syn n = case syn_namespace syn of
789795--- Pretty printing declarations and terms
790796
791797instance Show PTerm where
792− show tm = showImp False tm
798+ show tm = showImp Nothing False False tm
793799
794800instance Pretty PTerm where
795801 pretty = prettyImp False
@@ -804,8 +810,8 @@ instance Show PData where
804810 show d = showDImp False d
805811
806812showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
807−showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
808−showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
813+showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty
814+showDeclImp t (PPostulate _ _ _ _ n ty) = show n ++ " : " ++ showImp Nothing t False ty
809815showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
810816showDeclImp _ (PData _ _ _ _ d) = show d
811817showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
@@ -814,24 +820,24 @@ showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
814820
815821showCImp :: Bool -> PClause -> String
816822showCImp 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
818824 ++ " where " ++ show w
819825 where
820826 showWs [] = ""
821− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
827+ showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
822828showCImp 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
824830 ++ " { " ++ show w ++ " } "
825831 where
826832 showWs [] = ""
827− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
833+ showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
828834
829835
830836showDImp :: Bool -> PData -> String
831837showDImp 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"
833839 ++ 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)
835841
836842getImps :: [PArg] -> [(Name, PTerm)]
837843getImps [] = []
@@ -851,7 +857,10 @@ getConsts (_ : xs) = getConsts xs
851857getAll :: [PArg] -> [PTerm]
852858getAll = map getTm
853859
854−prettyImp :: Bool -> PTerm -> Doc
860+-- | Pretty-print a high-level Idris term
861+prettyImp :: Bool -- ^^ whether to show implicits
862+ -> PTerm -- ^^ the term to pretty-print
863+ -> Doc
855864prettyImp impl = prettySe 10
856865 where
857866 prettySe p (PQuote r) =
@@ -1037,108 +1046,142 @@ prettyImp impl = prettySe 10
10371046 bracket outer inner doc
10381047 | inner > outer = lparen <> doc <> rparen
10391048 | otherwise = doc
1040−
1041−showImp :: Bool -> PTerm -> String
1042−showImp impl tm = se 10 tm where
1043− se p (PQuote r) = "![" ++ show r ++ "]"
1044− se p (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1045− se p (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1046− se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1047− else showbasic n
1048− where showbasic n@(UN _) = show n
1049− showbasic (MN _ s) = s
1050− showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1051− se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1052− (if impl then " : " ++ se 10 ty else "") ++ " => "
1053− ++ se 10 sc
1054− se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1055− " in " ++ se 10 sc
1056− se p (PPi (Exp l s _) n ty sc)
1049+
1050+-- | Show Idris name
1051+showName :: Maybe IState -- ^^ the Idris state, for information about names
1052+ -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1053+ -> Bool -- ^^ whether to show implicits
1054+ -> Bool -- ^^ whether to colourise
1055+ -> Name -- ^^ the term to show
1056+ -> String
1057+showName ist bnd impl colour n = if colour then colourise n else showbasic n
1058+ where name = if impl then show n else showbasic n
1059+ showbasic n@(UN _) = show n
1060+ showbasic (MN _ s) = s
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
1088+ se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1089+ (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1090+ ++ se 10 ((n, False):bnd) sc
1091+ se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1092+ " = " ++ se 10 bnd v ++
1093+ " in " ++ se 10 ((n, False):bnd) sc
1094+ se p bnd (PPi (Exp l s _) n ty sc)
10571095 | n `elem` allNamesIn sc || impl
10581096 = bracket p 2 $
1059− (if l then "|(" else "(") ++
1060− show n ++ " : " ++ se 10 ty ++
1097+ (if l then "|(" else "(") ++
1098+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
10611099 ") " ++ st ++
1062− "-> " ++ se 10 sc
1063− | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1100+ "-> " ++ se 10 ((n, False):bnd) sc
1101+ | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
10641102 where st = case s of
10651103 Static -> "[static] "
10661104 _ -> ""
1067− se p (PPi (Imp l s _) n ty sc)
1068− | impl = bracket p 2 $ (if l then "|{" else "{") ++
1069− show n ++ " : " ++ se 10 ty ++
1070− "} " ++ st ++ "-> " ++ se 10 sc
1071− | otherwise = se 10 sc
1105+ se p bnd (PPi (Imp l s _) n ty sc)
1106+ | impl = bracket p 2 $ (if l then "|{" else "{") ++
1107+ perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1108+ "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
1109+ | otherwise = se 10 ((n, True):bnd) sc
10721110 where st = case s of
10731111 Static -> "[static] "
10741112 _ -> ""
1075− se p (PPi (Constraint _ _ _) n ty sc)
1076− = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1077− se p (PPi (TacImp _ _ s _) n ty sc)
1078− = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1079− se p e
1080− | Just str <- slist p e = str
1081− | Just num <- snat p e = show num
1082− se p (PMatchApp _ f) = "match " ++ show f
1083− se p (PApp _ (PRef _ f) [])
1084− | not impl = show f
1085− se p (PApp _ (PRef _ op@(UN (f:_))) args)
1113+ se p bnd (PPi (Constraint _ _ _) n ty sc)
1114+ = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
1115+ se p bnd (PPi (TacImp _ _ s _) n ty sc)
1116+ = bracket p 2 $
1117+ "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1118+ se 10 ((n, False):bnd) sc
1119+ se p bnd e
1120+ | Just str <- slist p bnd e = str
1121+ | Just num <- snat p e = perhapsColourise colouriseData (show num)
1122+ se p bnd (PMatchApp _ f) = "match " ++ show f
1123+ se p bnd (PApp _ hd@(PRef _ f) [])
1124+ | not impl = se p bnd hd
1125+ se p bnd (PApp _ op@(PRef _ (UN (f:_))) args)
10861126 | length (getExps args) == 2 && not impl && not (isAlpha f)
10871127 = let [l, r] = getExps args in
1088− bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1089− se p (PApp _ f as)
1128+ bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r
1129+ se p bnd (PApp _ f as)
10901130 = let args = getExps as in
1091− bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1092− else concatMap seArg args
1093− se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1094− where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1095− se p (PHidden tm) = "." ++ se 0 tm
1096− se p (PRefl _ t)
1097− | not impl = "refl"
1098− | otherwise = "refl {" ++ se 10 t ++ "}"
1099− se p (PResolveTC _) = "resolvetc"
1100− se p (PTrue _) = "()"
1101− se p (PFalse _) = "_|_"
1102− se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1103− se p (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r
1104− se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1105− se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1106− se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1107− se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1108− se p PType = "Type"
1109− se p (PConstant c) = show c
1110− se p (PProof ts) = "proof { " ++ show ts ++ "}"
1111− se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1112− se p (PMetavar n) = "?" ++ show n
1113− se p (PReturn f) = "return"
1114− se p PImpossible = "impossible"
1115− se p Placeholder = "_"
1116− se p (PDoBlock _) = "do block show not implemented"
1117− se p (PElabError s) = show s
1118− se p (PCoerced t) = se p t
1119− se p (PUnifyLog t) = "%unifyLog " ++ se p t
1120− se p (PGoal f t n sc) = "quoteGoal " ++ show n ++ " by " ++ se 10 t ++
1121− " in " ++ se 10 sc
1122−-- se p x = "Not implemented"
1123−
1124− slist' p (PApp _ (PRef _ nil) _)
1131+ bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
1132+ else concatMap (seArg bnd) args
1133+ se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1134+ where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1135+ se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1136+ se p bnd (PRefl _ t)
1137+ | not impl = perhapsColourise colouriseData "refl"
1138+ | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
1139+ se p bnd (PResolveTC _) = "resolvetc"
1140+ se p bnd (PTrue _) = perhapsColourise colouriseType "()"
1141+ se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"
1142+ se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r
1143+ se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
1144+ se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
1145+ se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
1146+ se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
1147+ se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
1148+ se p bnd PType = perhapsColourise colouriseType "Type"
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
1155+ se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
1156+ se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
1157+ se p bnd (PMetavar n) = "?" ++ show n
1158+ se p bnd (PReturn f) = "return"
1159+ se p bnd PImpossible = "impossible"
1160+ se p bnd Placeholder = "_"
1161+ se p bnd (PDoBlock _) = "do block show not implemented"
1162+ se p bnd (PElabError s) = show s
1163+ se p bnd (PCoerced t) = se p bnd t
1164+ se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
1165+-- se p bnd x = "Not implemented"
1166+
1167+ slist' p bnd (PApp _ (PRef _ nil) _)
11251168 | nsroot nil == UN "Nil" = Just []
1126− slist' p (PApp _ (PRef _ cons) args)
1169+ slist' p bnd (PApp _ (PRef _ cons) args)
11271170 | nsroot cons == UN "::",
11281171 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
11291172 all isImp imps,
1130− Just tl' <- slist' p tl
1173+ Just tl' <- slist' p bnd tl
11311174 = Just (hd:tl')
11321175 where
11331176 isImp (PImp {}) = True
11341177 isImp _ = False
1135− slist' _ _ = Nothing
1178+ slist' _ _ _ = Nothing
11361179
1137− slist p e | Just es <- slist' p e = Just $
1180+ slist p bnd e | Just es <- slist' p bnd e = Just $
11381181 case es of [] -> "[]"
1139− [x] -> "[" ++ se p x ++ "]"
1140− xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1141− slist _ _ = Nothing
1182+ [x] -> "[" ++ se p bnd x ++ "]"
1183+ xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
1184+ slist _ _ _ = Nothing
11421185
11431186 -- since Prelude is always imported, S & Z are unqualified iff they're the
11441187 -- Nat ones.
@@ -1152,15 +1195,15 @@ showImp impl tm = se 10 tm where
11521195
11531196 natns = "Prelude.Nat."
11541197
1155− sArg (PImp _ _ n tm _) = siArg (n, tm)
1156− sArg (PExp _ _ tm _) = seArg tm
1157− sArg (PConstraint _ _ tm _) = scArg tm
1158− sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)
1198+ sArg bnd (PImp _ _ n tm _) = siArg bnd (n, tm)
1199+ sArg bnd (PExp _ _ tm _) = seArg bnd tm
1200+ sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
1201+ sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
11591202
1160− seArg arg = " " ++ se 0 arg
1161− siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1162− scArg val = " {{" ++ se 10 val ++ "}}"
1163− stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1203+ seArg bnd arg = " " ++ se 0 bnd arg
1204+ siArg bnd (n, val) = " {" ++ show n ++ " = " ++ se 10 bnd val ++ "}"
1205+ scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
1206+ stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
11641207
11651208 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
11661209 | otherwise = str