git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit304fff15319073d46a35f6c87412dc5fe423475e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 4 May 2014, 13:28 (12 years ago) parentac617c10663f4d
20 files changed+217−154
compare with master
unifiedsplit
libs/effects/Effects.idr+2−2 libs/oldeffects/Effects.idr+1−1 libs/prelude/Prelude/Applicative.idr+5−2 libs/prelude/Prelude/Bool.idr+4−4 libs/prelude/Prelude/Either.idr+4−4 libs/prelude/Prelude/Foldable.idr+25−8 libs/prelude/Prelude/List.idr+2−2 libs/prelude/Prelude/Maybe.idr+10−3 libs/prelude/Prelude/Stream.idr+3−1 src/Idris/ASTUtils.hs+31−21 src/Idris/AbsSyntaxTree.hs+73−51 src/Idris/Core/TT.hs+3 src/Idris/Delaborate.hs+2−2 src/Idris/Docs.hs+9−9 src/Idris/ElabDecls.hs+3−3 src/Idris/IdrisDoc.hs+1−1 src/Idris/Output.hs+6−6 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+9−9 src/Idris/REPL.hs+23−24
libs/effects/Effects.idr+2−2
@@ -337,8 +337,8 @@ mapVE f [] = pure []
337337mapVE f (x :: xs) = [| f x :: mapVE f xs |]
338338
339339
340−when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
341−when True e = e
340+when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()
341+when True e = Force e
342342when False e = pure ()
343343
344344-- --------------------------------------------------------------------- [ EOF ]
libs/oldeffects/Effects.idr+1−1
@@ -303,6 +303,6 @@ mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
303303mapE f [] = pure []
304304mapE f (x :: xs) = [| f x :: mapE f xs |]
305305
306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
306+when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()
307307when True e = e
308308when False e = pure ()
libs/prelude/Prelude/Applicative.idr+5−2
@@ -38,8 +38,11 @@ class Applicative f => Alternative (f : Type -> Type) where
3838 empty : f a
3939 (<|>) : f a -> f a -> f a
4040
41+||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`
4142guard : Alternative f => Bool -> f ()
4243guard a = if a then pure () else empty
4344
44−when : Applicative f => Bool -> f () -> f ()
45−when a f = if a then f else pure ()
45+||| Conditionally execute an applicative expression
46+when : Applicative f => Bool -> Lazy (f ()) -> f ()
47+when True f = Force f
48+when False f = pure ()
libs/prelude/Prelude/Bool.idr+4−4
@@ -27,13 +27,13 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)
2727-- Boolean Operator Precedence
2828infixl 4 &&, ||
2929
30−||| Boolean OR
31−(||) : Bool -> Bool -> Bool
30+||| Boolean OR only evaluates the second argument if the first is `False`.
31+(||) : Bool -> Lazy Bool -> Bool
3232(||) False x = x
3333(||) True _ = True
3434
35−||| Boolean AND
36−(&&) : Bool -> Bool -> Bool
35+||| Boolean AND only evaluates the second argument if the first is `True`.
36+(&&) : Bool -> Lazy Bool -> Bool
3737(&&) True x = x
3838(&&) False _ = False
3939
libs/prelude/Prelude/Either.idr+4−4
@@ -39,9 +39,9 @@ choose False = Right oh
3939||| @ f the action to take on Left
4040||| @ g the action to take on Right
4141||| @ e the sum to analyze
42−either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c
43−either l r (Left x) = l x
44−either l r (Right x) = r x
42+either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c
43+either l r (Left x) = (Force l) x
44+either l r (Right x) = (Force r) x
4545
4646||| Keep the payloads of all Left constructors in a list of Eithers
4747lefts : List (Either a b) -> List a
@@ -74,7 +74,7 @@ fromEither (Right r) = r
7474
7575||| Convert a Maybe to an Either by using a default value in case of Nothing
7676||| @ e the default value
77−maybeToEither : (def : e) -> Maybe a -> Either e a
77+maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
7878maybeToEither def (Just j) = Right j
7979maybeToEither def Nothing = Left def
8080
libs/prelude/Prelude/Foldable.idr+25−8
@@ -14,27 +14,44 @@ class Foldable (t : Type -> Type) where
1414foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
1515foldl f z t = foldr (flip (.) . flip f) id t z
1616
17+||| Combine each element of a structure into a monoid
1718concat : (Foldable t, Monoid a) => t a -> a
1819concat = foldr (<+>) neutral
1920
21+||| Combine into a monoid the collective results of applying a function
22+||| to each element of a structure
2023concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
2124concatMap f = foldr ((<+>) . f) neutral
2225
23−and : Foldable t => t Bool -> Bool
24−and = foldr (&&) True
25−
26−or : Foldable t => t Bool -> Bool
27−or = foldr (||) False
28−
26+||| The conjunction of all elements of a structure containing
27+||| lazy boolean values. `and` short-circuits from left to right,
28+||| evaluating until either an element is `False` or no elements remain.
29+and : Foldable t => t (Lazy Bool) -> Bool
30+and = foldl (&&) True
31+
32+||| The disjunction of all elements of a structure containing
33+||| lazy boolean values. `or` short-circuits from left to right, evaluating
34+||| either until an element is `True` or no elements remain.
35+or : Foldable t => t (Lazy Bool) -> Bool
36+or = foldl (||) False
37+
38+||| The disjunction of the collective results of applying a
39+||| predicate to all elements of a structure. `any` short-circuits
40+||| from left to right.
2941any : Foldable t => (a -> Bool) -> t a -> Bool
30−any p = foldr ((||) . p) False
42+any p = foldl (\x => \y => x || p y) False
3143
44+||| The disjunction of the collective results of applying a
45+||| predicate to all elements of a structure. `all` short-circuits
46+||| from left to right.
3247all : Foldable t => (a -> Bool) -> t a -> Bool
33−all p = foldr ((&&) . p) True
48+all p = foldl (\x => \y => x && p y) True
3449
50+||| Add together all the elements of a structure
3551sum : (Foldable t, Num a) => t a -> a
3652sum = foldr (+) 0
3753
54+||| Multiply together all elements of a structure
3855product : (Foldable t, Num a) => t a -> a
3956product = foldr (*) 1
4057
libs/prelude/Prelude/List.idr+2−2
@@ -182,9 +182,9 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
182182||| @ nil what to return at the end of the list
183183||| @ cons what to do at each step of recursion
184184||| @ xs the list to recurse over
185−list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
185+list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b
186186list nil cons [] = nil
187−list nil cons (x::xs) = cons x xs
187+list nil cons (x::xs) = (Force cons) x xs
188188
189189--------------------------------------------------------------------------------
190190-- Building (bigger) lists
libs/prelude/Prelude/Maybe.idr+10−3
@@ -28,25 +28,32 @@ isJust (Just j) = True
2828-- Misc
2929--------------------------------------------------------------------------------
3030
31−maybe : Lazy b -> (a -> b) -> Maybe a -> b
31+maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
3232maybe n j Nothing = n
33−maybe n j (Just x) = j x
33+maybe n j (Just x) = (Force j) x
3434
35+||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
36+||| in the case that the `Maybe` value is `Nothing`.
3537fromMaybe : (Lazy a) -> Maybe a -> a
3638fromMaybe def Nothing = def
3739fromMaybe def (Just j) = j
3840
39−toMaybe : Bool -> a -> Maybe a
41+||| Returns `Just` the given value if the conditional is `True`
42+||| and `Nothing` if the conditional is `False`.
43+toMaybe : Bool -> Lazy a -> Maybe a
4044toMaybe True j = Just j
4145toMaybe False j = Nothing
4246
4347justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
4448justInjective refl = refl
4549
50+||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
51+||| that the `Maybe` value is `Nothing`.
4652lowerMaybe : Monoid a => Maybe a -> a
4753lowerMaybe Nothing = neutral
4854lowerMaybe (Just x) = x
4955
56+||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
5057raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
5158raiseToMaybe x = if x == neutral then Nothing else Just x
5259
libs/prelude/Prelude/Stream.idr+3−1
@@ -31,8 +31,10 @@ take : (n : Nat) -> (xs : Stream a) -> Vect n a
3131take Z _ = []
3232take (S n) (x :: xs) = x :: (take n xs)
3333
34+||| Drop the first n elements from the stream
35+||| @ n how many elements to drop
3436%assert_total
35−drop : Nat -> Stream a -> Stream a
37+drop : (n : Nat) -> Stream a -> Stream a
3638drop Z xs = xs
3739drop (S k) (x::xs) = drop k xs
3840
src/Idris/ASTUtils.hs+31−21
@@ -25,7 +25,11 @@ module Idris.ASTUtils where
2525-- fputState (detag n2) False
2626--
2727-- -- Note that all these operations handle missing items consistently
28−-- -- and transparently, as prescribed by the typeclass InitialValue.
28+-- -- and transparently, as prescribed by the default values included
29+-- -- in the definitions of the ist_* functions.
30+-- --
31+-- -- Especially, it's no longer necessary to have initial values of
32+-- -- data structures copied (possibly inconsistently) all over the compiler.
2933
3034import Control.Category
3135import Control.Applicative
@@ -57,20 +61,22 @@ fputState field x = fmodifyState field (const x)
5761fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()
5862fmodifyState field f = modify $ fmodify field f
5963
60−-- Until now, we'd have just ad-hoc empty lists and Falses thrown around
61−-- whenever a new instance of a record was to be created.
62−--
63−-- This class formalises the notion of an initial value for a record.
64−class InitialValue a where
65− initialValue :: a
66−
67−-- Exact-name context lookup; uses the initial value if needed.
68−ctxt_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a
69−ctxt_lookupExact n = Field
70− { fget = fromMaybe initialValue . lookupCtxtExact n
71− , fset = addDef n
64+-- Exact-name context lookup; uses Nothing for deleted values (read+write!).
65+--
66+-- Reading a non-existing value yields Nothing,
67+-- writing Nothing deletes the value (if it existed).
68+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)
69+ctxt_lookup n = Field
70+ { fget = lookupCtxtExact n
71+ , fset = \newVal -> case newVal of
72+ Just x -> addDef n x
73+ Nothing -> deleteDefExact n
7274 }
7375
76+-- Maybe-lens with a default value.
77+maybe_default :: a -> Field (Maybe a) a
78+maybe_default dflt = Field (fromMaybe dflt) (const . Just)
79+
7480
7581-----------------------------------
7682-- Individual records and fields --
@@ -83,12 +89,14 @@ ctxt_lookupExact n = Field
8389-- OptInfo
8490----------
8591
86−instance InitialValue OptInfo where
87− initialValue = Optimise [] False
88−
8992-- the optimisation record for the given (exact) name
9093ist_optimisation :: Name -> Field IState OptInfo
91−ist_optimisation n = ctxt_lookupExact n
94+ist_optimisation n =
95+ maybe_default Optimise
96+ { inaccessible = []
97+ , detaggable = False
98+ }
99+ . ctxt_lookup n
92100 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })
93101
94102-- two fields of the optimisation record
@@ -102,12 +110,14 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })
102110-- CGInfo
103111---------
104112
105−instance InitialValue CGInfo where
106− initialValue = CGInfo [] [] [] [] []
107−
108113-- callgraph record for the given (exact) name
109114ist_callgraph :: Name -> Field IState CGInfo
110−ist_callgraph n = ctxt_lookupExact n
115+ist_callgraph n =
116+ maybe_default CGInfo
117+ { argsdef = [], calls = [], scg = []
118+ , argsused = [], usedpos = []
119+ }
120+ . ctxt_lookup n
111121 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })
112122
113123-- some fields of the CGInfo record
src/Idris/AbsSyntaxTree.hs+73−51
@@ -95,6 +95,28 @@ defaultOpts = IOption { opt_logLevel = 0
9595 , opt_autoSolve = True
9696 }
9797
98+data PPOption = PPOption {
99+ ppopt_impl :: Bool -- ^^ whether to show implicits
100+} deriving (Show)
101+
102+-- | Pretty printing options with default verbosity.
103+defaultPPOption :: PPOption
104+defaultPPOption = PPOption { ppopt_impl = False }
105+
106+-- | Pretty printing options with the most verbosity.
107+verbosePPOption :: PPOption
108+verbosePPOption = PPOption { ppopt_impl = True }
109+
110+-- | Get pretty printing options from the big options record.
111+ppOption :: IOption -> PPOption
112+ppOption opt = PPOption {
113+ ppopt_impl = opt_showimp opt
114+}
115+
116+-- | Get pretty printing options from an idris state record.
117+ppOptionIst :: IState -> PPOption
118+ppOptionIst = ppOption . idris_options
119+
98120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
99121
100122-- | The output mode in use
@@ -1089,19 +1111,19 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
10891111-- could interfere with interactive editing, which calls "show".
10901112
10911113instance Show PTerm where
1092− showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm
1114+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
10931115
10941116instance Show PDecl where
1095− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d
1117+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d
10961118
10971119instance Show PClause where
1098− showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c
1120+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
10991121
11001122instance Show PData where
1101− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d
1123+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
11021124
11031125instance Pretty PTerm OutputAnnotation where
1104− pretty = prettyImp False
1126+ pretty = prettyImp defaultPPOption
11051127
11061128-- | Colourise annotations according to an Idris state. It ignores the names
11071129-- in the annotation, as there's no good way to show extended information on a
@@ -1129,23 +1151,23 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
11291151 colour ItalicText = IdrisColour Nothing True False False True
11301152
11311153-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1132−prettyImp :: Bool -- ^^ whether to show implicits
1154+prettyImp :: PPOption -- ^^ pretty printing options
11331155 -> PTerm -- ^^ the term to pretty-print
11341156 -> Doc OutputAnnotation
11351157prettyImp impl = pprintPTerm impl [] [] []
11361158
11371159-- | Do the right thing for rendering a term in an IState
11381160prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1139−prettyIst ist = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist)
1161+prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
11401162
11411163-- | Pretty-print a high-level Idris term in some bindings context with infix info
1142−pprintPTerm :: Bool -- ^^ whether to show implicits
1164+pprintPTerm :: PPOption -- ^^ pretty printing options
11431165 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
11441166 -> [Name] -- ^^ names to always show in pi, even if not used
11451167 -> [FixDecl] -- ^^ Fixity declarations
11461168 -> PTerm -- ^^ the term to pretty-print
11471169 -> Doc OutputAnnotation
1148−pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
1170+pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
11491171 where
11501172 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
11511173 prettySe p bnd (PQuote r) =
@@ -1154,7 +1176,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
11541176 prettySe p bnd e
11551177 | Just str <- slist p bnd e = str
11561178 | Just n <- snat p e = annotate AnnConstData (text (show n))
1157− prettySe p bnd (PRef fc n) = prettyName impl bnd n
1179+ prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n
11581180 prettySe p bnd (PLam n ty sc) =
11591181 bracket p 2 . group . align . hang 2 $
11601182 text "\\" <> bindingOf n False <+> text "=>" <$>
@@ -1165,7 +1187,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
11651187 prettySe 10 bnd v <+> kwd "in" </>
11661188 prettySe 10 ((n, False):bnd) sc
11671189 prettySe p bnd (PPi (Exp l s _) n ty sc)
1168− | n `elem` allNamesIn sc || impl || n `elem` docArgs =
1190+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
11691191 bracket p 2 . group $
11701192 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
11711193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
@@ -1178,7 +1200,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
11781200 Static -> text "[static]" <> space
11791201 _ -> empty
11801202 prettySe p bnd (PPi (Imp l s _) n ty sc)
1181− | impl =
1203+ | ppopt_impl ppo =
11821204 bracket p 2 $
11831205 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
11841206 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
@@ -1197,16 +1219,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
11971219 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
11981220 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
11991221 | UN nm <- basename f
1200− , not impl && null (getExps args) = if isAlpha (thead nm)
1201− then prettyName impl bnd f
1202− else enclose lparen rparen $
1203− prettyName impl bnd f
1222+ , not (ppopt_impl ppo) && null (getExps args) =
1223+ if isAlpha (thead nm)
1224+ then prettyName (ppopt_impl ppo) bnd f
1225+ else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f
12041226 prettySe p bnd (PAppBind _ (PRef _ f) [])
1205− | not impl = text "!" <> prettyName impl bnd f
1227+ | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f
12061228 prettySe p bnd (PApp _ (PRef _ op) args)
12071229 | UN nm <- basename op
12081230 , not (tnull nm) &&
1209− (not impl) && (not $ isAlpha (thead nm)) =
1231+ (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
12101232 case getExps args of
12111233 [] -> enclose lparen rparen opName
12121234 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))
@@ -1215,7 +1237,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
12151237 (l:r:rest) -> bracket p 1 $
12161238 enclose lparen rparen (inFix l r) <+>
12171239 align (group (vsep (map (prettyArgSe bnd) rest)))
1218− where opName = prettyName impl bnd op
1240+ where opName = prettyName (ppopt_impl ppo) bnd op
12191241 f = getFixity (opStr op)
12201242 left l = case f of
12211243 Nothing -> prettySe (-1) bnd l
@@ -1235,7 +1257,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
12351257 fp = prettySe 1 bnd f
12361258 in
12371259 bracket p 1 . group $
1238− if impl
1260+ if ppopt_impl ppo
12391261 then if null as
12401262 then fp
12411263 else fp <+> align (vsep (map (prettyArgS bnd) as))
@@ -1340,9 +1362,9 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd
13401362 basename n = n
13411363
13421364 slist' p bnd (PApp _ (PRef _ nil) _)
1343− | not impl && nsroot nil == sUN "Nil" = Just []
1365+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
13441366 slist' p bnd (PRef _ nil)
1345− | not impl && nsroot nil == sUN "Nil" = Just []
1367+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
13461368 slist' p bnd (PApp _ (PRef _ cons) args)
13471369 | nsroot cons == sUN "::",
13481370 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
@@ -1415,43 +1437,43 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im
14151437 strName other = show other
14161438
14171439
1418−showCImp :: Bool -> PClause -> Doc OutputAnnotation
1419−showCImp impl (PClause _ n l ws r w)
1420− = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r
1440+showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1441+showCImp ppo (PClause _ n l ws r w)
1442+ = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
14211443 <+> text "where" <+> text (show w)
14221444 where
14231445 showWs [] = empty
1424− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1425−showCImp impl (PWith _ n l ws r w)
1426− = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r
1446+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1447+showCImp ppo (PWith _ n l ws r w)
1448+ = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
14271449 <+> braces (text (show w))
14281450 where
14291451 showWs [] = empty
1430− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1452+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
14311453
14321454
1433−showDImp :: Bool -> PData -> Doc OutputAnnotation
1434−showDImp impl (PDatadecl n ty cons)
1435− = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>
1436− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))
1455+showDImp :: PPOption -> PData -> Doc OutputAnnotation
1456+showDImp ppo (PDatadecl n ty cons)
1457+ = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1458+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))
14371459
1438−showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
1439−showDecls i ds = vsep (map (showDeclImp i) ds)
1460+showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1461+showDecls o ds = vsep (map (showDeclImp o) ds)
14401462
14411463showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1442−showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t
1443−showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1444− indent 2 (vsep (map (showCImp i) cs))
1445−showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d
1446−showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)
1447−showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)
1464+showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1465+showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1466+ indent 2 (vsep (map (showCImp o) cs))
1467+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1468+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1469+showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
14481470showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1449−showDeclImp i (PClass _ _ _ cs n ps _ ds)
1450− = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds
1451−showDeclImp i (PInstance _ _ cs n _ t _ ds)
1452− = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds
1471+showDeclImp o (PClass _ _ _ cs n ps _ ds)
1472+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1473+showDeclImp o (PInstance _ _ cs n _ t _ ds)
1474+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
14531475showDeclImp _ _ = text "..."
1454−-- showDeclImp (PImport i) = "import " ++ i
1476+-- showDeclImp (PImport o) = "import " ++ o
14551477
14561478instance Show (Doc OutputAnnotation) where
14571479 show = flip (displayS . renderCompact) ""
@@ -1478,14 +1500,14 @@ getAll = map getTm
14781500-- | Show Idris name
14791501showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
14801502 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1481− -> Bool -- ^^ whether to show implicits
1503+ -> PPOption -- ^^ pretty printing options
14821504 -> Bool -- ^^ whether to colourise
14831505 -> Name -- ^^ the term to show
14841506 -> String
1485−showName ist bnd impl colour n = case ist of
1507+showName ist bnd ppo colour n = case ist of
14861508 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
14871509 Nothing -> showbasic n
1488− where name = if impl then show n else showbasic n
1510+ where name = if ppopt_impl ppo then show n else showbasic n
14891511 showbasic n@(UN _) = showCG n
14901512 showbasic (MN _ s) = str s
14911513 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
@@ -1509,11 +1531,11 @@ showTm :: IState -- ^^ the Idris state, for information about identifiers and co
15091531 -> String
15101532showTm ist = displayDecorated (consoleDecorate ist) .
15111533 renderPretty 0.8 100000 .
1512− prettyImp (opt_showimp (idris_options ist))
1534+ prettyImp (ppOptionIst ist)
15131535
15141536-- | Show a term with implicits, no colours
15151537showTmImpls :: PTerm -> String
1516−showTmImpls = flip (displayS . renderCompact . prettyImp True) ""
1538+showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
15171539
15181540
15191541instance Sized PTerm where
src/Idris/Core/TT.hs+3
@@ -426,6 +426,9 @@ lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
426426lookupCtxtExact :: Name -> Ctxt a -> Maybe a
427427lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
428428
429+deleteDefExact :: Name -> Ctxt a -> Ctxt a
430+deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)
431+
429432updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
430433updateDef n f ctxt
431434 = let ds = lookupCtxtName n ctxt in
src/Idris/Delaborate.hs+2−2
@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
138138pprintTerm ist = pprintTerm' ist []
139139
140140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
141−pprintTerm' ist bnd = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist)
141+pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm
142142
143143pprintErr :: IState -> Err -> Doc OutputAnnotation
144144pprintErr i err = pprintErr' i (fmap (errReverse i) err)
@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>
269269
270270
271271showqual :: IState -> Name -> String
272−showqual i n = showName (Just i) [] False False (dens n)
272+showqual i n = showName (Just i) [] (ppOptionIst i) { ppopt_impl = False } False (dens n)
273273 where
274274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of
275275 [_] -> n -- just one thing
src/Idris/Docs.hs+9−9
@@ -36,8 +36,8 @@ showDoc d | nullDocstring d = empty
3636
3737pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
3838pprintFD ist (FD n doc args ty f)
39− = nest 4 (prettyName imp [] n <+> colon <+>
40− pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args
39+ = nest 4 (prettyName (ppopt_impl ppo) [] n <+> colon <+>
40+ pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
4141 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
4242 renderDocstring doc <$>
4343 maybe empty (\f -> text (show f) <> line) f <>
@@ -46,23 +46,23 @@ pprintFD ist (FD n doc args ty f)
4646 then nest 4 $ text "Arguments:" <$> vsep argshow
4747 else empty)
4848
49− where imp = opt_showimp (idris_options ist)
49+ where ppo = ppOptionIst ist
5050 infixes = idris_infixes ist
5151 showArgs ((n, ty, Exp {}, Just d):args) bnd
5252 = bindingOf n False <+> colon <+>
53− pprintPTerm imp bnd [] infixes ty <>
53+ pprintPTerm ppo bnd [] infixes ty <>
5454 showDoc d <> line
5555 :
5656 showArgs args ((n, False):bnd)
5757 showArgs ((n, ty, Constraint {}, Just d):args) bnd
5858 = text "Class constraint" <+>
59− pprintPTerm imp bnd [] infixes ty <> showDoc d <> line
59+ pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line
6060 :
6161 showArgs args ((n, True):bnd)
6262 showArgs ((n, ty, Imp {}, Just d):args) bnd
6363 = text "(implicit)" <+>
6464 bindingOf n True <+> colon <+>
65− pprintPTerm imp bnd [] infixes ty <>
65+ pprintPTerm ppo bnd [] infixes ty <>
6666 showDoc d <> line
6767 :
6868 showArgs args ((n, True):bnd)
@@ -77,7 +77,7 @@ pprintDocs ist (DataDoc t args)
7777 nest 4 (text "Constructors:" <> line <>
7878 vsep (map (pprintFD ist) args))
7979pprintDocs ist (ClassDoc n doc meths params instances)
80− = nest 4 (text "Type class" <+> prettyName imp [] n <>
80+ = nest 4 (text "Type class" <+> prettyName (ppopt_impl ppo) [] n <>
8181 if nullDocstring doc then empty else line <> renderDocstring doc)
8282 <> line <$>
8383 nest 4 (text "Parameters:" <$> prettyParameters)
@@ -97,11 +97,11 @@ pprintDocs ist (ClassDoc n doc meths params instances)
9797
9898 pNames = map fst params
9999
100− imp = opt_showimp (idris_options ist)
100+ ppo = ppOptionIst ist
101101 infixes = idris_infixes ist
102102
103103 dumpInstance :: PTerm -> Doc OutputAnnotation
104− dumpInstance = pprintPTerm imp params' [] infixes
104+ dumpInstance = pprintPTerm ppo params' [] infixes
105105
106106 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm
107107 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)
src/Idris/ElabDecls.hs+3−3
@@ -393,7 +393,7 @@ elabEliminator paramPos n ty cons info = do
393393 elimLog elimSig
394394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
395395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
396− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
396+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
397397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
398398 -- Do not elaborate clauses if there aren't any
399399 case eliminatorClauses of
@@ -1863,7 +1863,7 @@ elabClass info syn doc fc constraints tn ps pDocs ds
18631863 constraint
18641864 let cons = [(emptyDocstring, [], cn, cty, fc, [])]
18651865 let ddecl = PDatadecl tn tty cons
1866− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
1866+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)
18671867 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl
18681868 -- for each constraint, build a top level function to chase it
18691869 logLvl 5 $ "Building functions"
@@ -2059,7 +2059,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
20592059 let wbTys = map mkTyDecl mtys
20602060 let wbVals = map (decorateid (decorate ns iname)) ds'
20612061 let wb = wbTys ++ wbVals
2062− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)
2062+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)
20632063 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
20642064 show (concat (nub wparams))
20652065
src/Idris/IdrisDoc.hs+1−1
@@ -457,7 +457,7 @@ genTypeHeader ist (FD n _ args ftype _) = do
457457
458458 where
459459 htmlSignature = displayDecorated decorator $ renderCompact signature
460− signature = pprintPTerm False [] names (idris_infixes ist) ftype
460+ signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype
461461 names = [ n | (n@(UN n'), _, _, _) <- args,
462462 not (T.isPrefixOf (txt "__") n') ]
463463
src/Idris/Output.hs+6−6
@@ -88,16 +88,16 @@ ihPrintTermWithType h tm ty = do ist <- getIState
8888-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
8989ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
9090ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
91−ihPrintFunTypes h bnd n overloads = do imp <- impShow
92− ist <- getIState
91+ihPrintFunTypes h bnd n overloads = do ist <- getIState
92+ let ppo = ppOptionIst ist
9393 let infixes = idris_infixes ist
94− let output = vsep (map (uncurry (ppOverload imp infixes)) overloads)
94+ let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)
9595 case idris_outputmode ist of
9696 RawOutput -> consoleDisplayAnnotated h output
9797 IdeSlave n -> ideSlaveReturnAnnotated n h output
9898 where fullName n = prettyName True bnd n
99− ppOverload imp infixes n tm =
100− fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)
99+ ppOverload ppo infixes n tm =
100+ fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)
101101
102102ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
103103ihRenderResult h d = do ist <- getIState
@@ -123,7 +123,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =
123123 out = displayS . renderPretty 1.0 50 $ renderDocstring o
124124 return (out "")
125125 getTy :: IState -> Name -> String -- fails if name not already extant!
126− getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist) $
126+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $
127127 delabTy ist n
128128 in (displayS . renderPretty 1.0 50 $ theTy) ""
129129fancifyAnnots _ annot = annot
src/Idris/Parser.hs+1−1
@@ -1248,7 +1248,7 @@ loadSource h lidr f
12481248 -- Parsing done, now process declarations
12491249
12501250 let ds = namespaces mname ds'
1251− logLvl 3 (show $ showDecls True ds)
1251+ logLvl 3 (show $ showDecls verbosePPOption ds)
12521252 i <- getIState
12531253 logLvl 10 (show (toAlist (idris_implicits i)))
12541254 logLvl 3 (show (idris_infixes i))
src/Idris/Prover.hs+9−9
@@ -110,9 +110,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
110110 iputGoal rendered
111111
112112 where
113− showImplicits = opt_showimp (idris_options ist)
113+ ppo = ppOptionIst ist
114114
115− tPretty bnd t = pprintPTerm showImplicits bnd [] (idris_infixes ist) $ delab ist t
115+ tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t
116116
117117 assumptionNames :: Env -> [Name]
118118 assumptionNames = map fst
@@ -237,16 +237,16 @@ ploop fn d prompt prf e h
237237 ctxt' = envCtxt env ctxt
238238 putIState ist { tt_ctxt = ctxt' }
239239 (tm, ty) <- elabVal toplevel False t
240− let imp = opt_showimp (idris_options ist)
240+ let ppo = ppOptionIst ist
241241 ty' = normaliseC ctxt [] ty
242242 h = idris_outh ist
243243 infixes = idris_infixes ist
244244 case tm of
245245 TType _ ->
246− ihPrintTermWithType h (prettyImp imp PType) type1Doc
246+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc
247247 _ -> let bnd = map (\x -> (fst x, False)) env in
248− ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))
249− (pprintPTerm imp bnd [] infixes (delab ist ty))
248+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))
249+ (pprintPTerm ppo bnd [] infixes (delab ist ty))
250250 putIState ist
251251 return (False, e, False, prf))
252252 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
@@ -262,10 +262,10 @@ ploop fn d prompt prf e h
262262 (tm, ty) <- elabVal toplevel False t
263263 let tm' = force (normaliseAll ctxt' env tm)
264264 ty' = force (normaliseAll ctxt' env ty)
265− imp = opt_showimp (idris_options ist')
265+ ppo = ppOption (idris_options ist')
266266 infixes = idris_infixes ist
267− tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')
268− tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')
267+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')
268+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')
269269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
270270 putIState ist
271271 return (False, e, False, prf))
src/Idris/REPL.hs+23−24
@@ -312,34 +312,34 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =
312312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
313313 do ist <- getIState
314314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
315− imp <- impShow
315+ let ppo = ppOptionIst ist
316316 let mvarTys = map (delabTy ist) mvs
317317 let res = (IdeSlave.SymbolAtom "ok",
318318 zipWith (\ n (prems, concl) -> (n, prems, concl))
319319 (map (IdeSlave.StringAtom . show) mvs)
320− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))
320+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
321321 runIO . putStrLn $ IdeSlave.convSExp "return" res id
322322 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
323323 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
324324 in ((n, t):prems, conc)
325325 getGoal tm = ([], tm)
326− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)
326+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
327327 -> ([(String, String, SpanList OutputAnnotation)],
328328 (String, SpanList OutputAnnotation))
329− sexpGoal ist cols imp ns ([], concl) =
329+ sexpGoal ist cols ppo ns ([], concl) =
330330 let infixes = idris_infixes ist
331331 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
332− pprintPTerm imp (zip ns (repeat False)) [] infixes concl
332+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
333333 in ([], concl')
334− sexpGoal ist cols imp ns ((n, t):ps, concl) =
334+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =
335335 let n' = case n of
336336 NS (UN nm) ns -> str nm
337337 UN nm | ('_':'_':_) <- str nm -> "_"
338338 | otherwise -> str nm
339339 _ -> "_"
340340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
341− pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t
342− rest = sexpGoal ist cols imp (n:ns) (ps, concl)
341+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
342+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
343343 in ((n', t', spans) : fst rest, snd rest)
344344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
345345 case splitName n of
@@ -581,21 +581,21 @@ process h fn (ExecVal t)
581581process h fn (Check (PRef _ n))
582582 = do ctxt <- getContext
583583 ist <- getIState
584− imp <- impShow
584+ let ppo = ppOptionIst ist
585585 case lookupNames n ctxt of
586586 ts@(t:_) ->
587587 case lookup t (idris_metavars ist) of
588588 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $
589− showMetavarInfo imp ist n i
589+ showMetavarInfo ppo ist n i
590590 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)
591591 [] -> ihPrintError h $ "No such variable " ++ show n
592592 where
593− showMetavarInfo imp ist n i
593+ showMetavarInfo ppo ist n i
594594 = case lookupTy n (tt_ctxt ist) of
595− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))
596− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
597− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc
598− putTy imp ist i bnd (PPi _ n t sc)
595+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
596+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
597+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
598+ putTy ppo ist i bnd (PPi _ n t sc)
599599 = let current = text " " <>
600600 (case n of
601601 MN _ _ -> text "_"
@@ -603,21 +603,21 @@ process h fn (Check (PRef _ n))
603603 _ -> bindingOf n False) <+>
604604 colon <+> align (tPretty bnd ist t) <> line
605605 in
606− current <> putTy imp ist (i-1) ((n,False):bnd) sc
607− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc
608− putGoal imp ist bnd g
606+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc
607+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
608+ putGoal ppo ist bnd g
609609 = text "--------------------------------------" <$>
610610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>
611611 align (tPretty bnd ist g)
612612
613− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t
613+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t
614614
615615
616616process h fn (Check t)
617617 = do (tm, ty) <- elabVal toplevel False t
618618 ctxt <- getContext
619619 ist <- getIState
620− let imp = opt_showimp (idris_options ist)
620+ let ppo = ppOptionIst ist
621621 ty' = normaliseC ctxt [] ty
622622 case tm of
623623 TType _ ->
@@ -664,8 +664,8 @@ process h fn (TotCheck n)
664664 [] -> ihPrintError h $ "Unknown operator " ++ show n
665665 ts -> do ist <- getIState
666666 c <- colourise
667− imp <- impShow
668− let showN = showName (Just ist) [] imp c
667+ let ppo = ppOptionIst ist
668+ let showN = showName (Just ist) [] ppo c
669669 ihPrintResult h . concat . intersperse "\n" .
670670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
671671 ts
@@ -825,7 +825,7 @@ process h fn (DoProofSearch updatefile rec l n hints)
825825 ctxt <- getContext
826826 i <- getIState
827827 return . flip displayS "" . renderPretty 1.0 80 $
828− pprintPTerm False [] [] (idris_infixes i)
828+ pprintPTerm defaultPPOption [] [] (idris_infixes i)
829829 (stripNS
830830 (dropCtxt envlen
831831 (delab i (specialise ctxt [] [(mn, 1)] tm)))))
@@ -958,7 +958,6 @@ process h fn (TestInline t)
958958 ctxt <- getContext
959959 ist <- getIState
960960 let tm' = inlineTerm ist tm
961− imp <- impShow
962961 c <- colourise
963962 iPrintResult (showTm ist (delab ist tm'))
964963process h fn Execute