304fff1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

304fff1Edwin Brady12 years ago

libs/effects/Effects.idr+2−2

compare with master

unifiedsplit

@@ -337,8 +337,8 @@ mapVE f [] = pure []

337mapVE f (x :: xs) = [| f x :: mapVE f xs |]

338

339

340−when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()

340+when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()

341−when True e = e

341+when True e = Force e

342when False e = pure ()

343

344-- --------------------------------------------------------------------- [ 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)

303mapE f [] = pure []

304mapE f (x :: xs) = [| f x :: mapE f xs |]

305

306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()

306+when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()

307when True e = e

308when False e = pure ()

libs/prelude/Prelude/Applicative.idr+5−2

@@ -38,8 +38,11 @@ class Applicative f => Alternative (f : Type -> Type) where

38 empty : f a

39 (<|>) : f a -> f a -> f a

41+||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`

41guard : Alternative f => Bool -> f ()

42guard : Alternative f => Bool -> f ()

42guard a = if a then pure () else empty

43guard a = if a then pure () else empty

45+||| Conditionally execute an applicative expression

44−when : Applicative f => Bool -> f () -> f ()

46+when : Applicative f => Bool -> Lazy (f ()) -> f ()

45−when a f = if a then f else pure ()

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)

27-- Boolean Operator Precedence

28infixl 4 &&, ||

30−||| Boolean OR

30+||| Boolean OR only evaluates the second argument if the first is `False`.

31−(||) : Bool -> Bool -> Bool

31+(||) : Bool -> Lazy Bool -> Bool

32(||) False x = x

33(||) True _ = True

35−||| Boolean AND

35+||| Boolean AND only evaluates the second argument if the first is `True`.

36−(&&) : Bool -> Bool -> Bool

36+(&&) : Bool -> Lazy Bool -> Bool

37(&&) True x = x

38(&&) False _ = False

libs/prelude/Prelude/Either.idr+4−4

@@ -39,9 +39,9 @@ choose False = Right oh

39||| @ f the action to take on Left

40||| @ g the action to take on Right

41||| @ e the sum to analyze

42−either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c

42+either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c

43−either l r (Left x) = l x

43+either l r (Left x) = (Force l) x

44−either l r (Right x) = r x

44+either l r (Right x) = (Force r) x

46||| Keep the payloads of all Left constructors in a list of Eithers

47lefts : List (Either a b) -> List a

@@ -74,7 +74,7 @@ fromEither (Right r) = r

75||| Convert a Maybe to an Either by using a default value in case of Nothing

76||| @ e the default value

77−maybeToEither : (def : e) -> Maybe a -> Either e a

77+maybeToEither : (def : Lazy e) -> Maybe a -> Either e a

78maybeToEither def (Just j) = Right j

79maybeToEither def Nothing = Left def

libs/prelude/Prelude/Foldable.idr+25−8

@@ -14,27 +14,44 @@ class Foldable (t : Type -> Type) where

14foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc

15foldl f z t = foldr (flip (.) . flip f) id t z

17+||| Combine each element of a structure into a monoid

17concat : (Foldable t, Monoid a) => t a -> a

18concat : (Foldable t, Monoid a) => t a -> a

18concat = foldr (<+>) neutral

19concat = foldr (<+>) neutral

21+||| Combine into a monoid the collective results of applying a function

22+||| to each element of a structure

20concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m

23concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m

21concatMap f = foldr ((<+>) . f) neutral

24concatMap f = foldr ((<+>) . f) neutral

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.

23−and : Foldable t => t Bool -> Bool

29+and : Foldable t => t (Lazy Bool) -> Bool

24−and = foldr (&&) True

30+and = foldl (&&) True

25−

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.

26−or : Foldable t => t Bool -> Bool

35+or : Foldable t => t (Lazy Bool) -> Bool

27−or = foldr (||) False

36+or = foldl (||) False

28−

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.

29any : Foldable t => (a -> Bool) -> t a -> Bool

41any : Foldable t => (a -> Bool) -> t a -> Bool

30−any p = foldr ((||) . p) False

42+any p = foldl (\x => \y => x || p y) False

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.

32all : Foldable t => (a -> Bool) -> t a -> Bool

47all : Foldable t => (a -> Bool) -> t a -> Bool

33−all p = foldr ((&&) . p) True

48+all p = foldl (\x => \y => x && p y) True

50+||| Add together all the elements of a structure

35sum : (Foldable t, Num a) => t a -> a

51sum : (Foldable t, Num a) => t a -> a

36sum = foldr (+) 0

52sum = foldr (+) 0

54+||| Multiply together all elements of a structure

38product : (Foldable t, Num a) => t a -> a

55product : (Foldable t, Num a) => t a -> a

39product = foldr (*) 1

56product = foldr (*) 1

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

182||| @ nil what to return at the end of the list

183||| @ cons what to do at each step of recursion

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

186list nil cons [] = nil

187−list nil cons (x::xs) = cons x xs

187+list nil cons (x::xs) = (Force cons) x xs

188

189--------------------------------------------------------------------------------

190-- Building (bigger) lists

libs/prelude/Prelude/Maybe.idr+10−3

@@ -28,25 +28,32 @@ isJust (Just j) = True

28-- Misc

29--------------------------------------------------------------------------------

31−maybe : Lazy b -> (a -> b) -> Maybe a -> b

31+maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

32maybe n j Nothing = n

33−maybe n j (Just x) = j x

33+maybe n j (Just x) = (Force j) x

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`.

35fromMaybe : (Lazy a) -> Maybe a -> a

37fromMaybe : (Lazy a) -> Maybe a -> a

36fromMaybe def Nothing = def

38fromMaybe def Nothing = def

37fromMaybe def (Just j) = j

39fromMaybe def (Just j) = j

41+||| Returns `Just` the given value if the conditional is `True`

42+||| and `Nothing` if the conditional is `False`.

39−toMaybe : Bool -> a -> Maybe a

43+toMaybe : Bool -> Lazy a -> Maybe a

40toMaybe True j = Just j

44toMaybe True j = Just j

41toMaybe False j = Nothing

45toMaybe False j = Nothing

43justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

47justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y

44justInjective refl = refl

48justInjective refl = refl

50+||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case

51+||| that the `Maybe` value is `Nothing`.

46lowerMaybe : Monoid a => Maybe a -> a

52lowerMaybe : Monoid a => Maybe a -> a

47lowerMaybe Nothing = neutral

53lowerMaybe Nothing = neutral

48lowerMaybe (Just x) = x

54lowerMaybe (Just x) = x

56+||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.

50raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

57raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

51raiseToMaybe x = if x == neutral then Nothing else Just x

58raiseToMaybe x = if x == neutral then Nothing else Just x

libs/prelude/Prelude/Stream.idr+3−1

@@ -31,8 +31,10 @@ take : (n : Nat) -> (xs : Stream a) -> Vect n a

31take Z _ = []

32take (S n) (x :: xs) = x :: (take n xs)

34+||| Drop the first n elements from the stream

35+||| @ n how many elements to drop

34%assert_total

36%assert_total

35−drop : Nat -> Stream a -> Stream a

37+drop : (n : Nat) -> Stream a -> Stream a

36drop Z xs = xs

38drop Z xs = xs

37drop (S k) (x::xs) = drop k xs

39drop (S k) (x::xs) = drop k xs

src/Idris/ASTUtils.hs+31−21

@@ -25,7 +25,11 @@ module Idris.ASTUtils where

25-- fputState (detag n2) False

26--

27-- -- 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.

30import Control.Category

34import Control.Category

31import Control.Applicative

35import Control.Applicative

@@ -57,20 +61,22 @@ fputState field x = fmodifyState field (const x)

57fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()

61fmodifyState :: MonadState s m => Field s a -> (a -> a) -> m ()

58fmodifyState field f = modify $ fmodify field f

62fmodifyState field f = modify $ fmodify field f

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.

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_lookupExact :: InitialValue a => Name -> Field (Ctxt a) a

68+ctxt_lookup :: Name -> Field (Ctxt a) (Maybe a)

69−ctxt_lookupExact n = Field

69+ctxt_lookup n = Field

70− { fget = fromMaybe initialValue . lookupCtxtExact n

70+ { fget = lookupCtxtExact n

71+ , fset = \newVal -> case newVal of

71− , fset = addDef n

72+ Just x -> addDef n x

73+ Nothing -> deleteDefExact n

72 }

74 }

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+

75-----------------------------------

81-----------------------------------

76-- Individual records and fields --

82-- Individual records and fields --

@@ -83,12 +89,14 @@ ctxt_lookupExact n = Field

83-- OptInfo

89-- OptInfo

84----------

90----------

86−instance InitialValue OptInfo where

87− initialValue = Optimise [] False

88−

89-- the optimisation record for the given (exact) name

92-- the optimisation record for the given (exact) name

90ist_optimisation :: Name -> Field IState OptInfo

93ist_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

92 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

100 . Field idris_optimisation (\v ist -> ist{ idris_optimisation = v })

101

94-- two fields of the optimisation record

102-- two fields of the optimisation record

@@ -102,12 +110,14 @@ opt_detaggable = Field detaggable (\v opt -> opt{ detaggable = v })

102-- CGInfo

110-- CGInfo

103---------

111---------

104

112

105−instance InitialValue CGInfo where

106− initialValue = CGInfo [] [] [] [] []

107−

108-- callgraph record for the given (exact) name

113-- callgraph record for the given (exact) name

109ist_callgraph :: Name -> Field IState CGInfo

114ist_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

111 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

121 . Field idris_callgraph (\v ist -> ist{ idris_callgraph = v })

112

122

113-- some fields of the CGInfo record

123-- some fields of the CGInfo record

src/Idris/AbsSyntaxTree.hs+73−51

@@ -95,6 +95,28 @@ defaultOpts = IOption { opt_logLevel = 0

95 , opt_autoSolve = True

96 }

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+

98data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

121

100-- | The output mode in use

122-- | The output mode in use

@@ -1089,19 +1111,19 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

1089-- could interfere with interactive editing, which calls "show".

1111-- could interfere with interactive editing, which calls "show".

1090

1112

1091instance Show PTerm where

1113instance 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

1093

1115

1094instance Show PDecl where

1116instance 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

1096

1118

1097instance Show PClause where

1119instance 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

1099

1121

1100instance Show PData where

1122instance 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

1102

1124

1103instance Pretty PTerm OutputAnnotation where

1125instance Pretty PTerm OutputAnnotation where

1104− pretty = prettyImp False

1126+ pretty = prettyImp defaultPPOption

1105

1127

1106-- | Colourise annotations according to an Idris state. It ignores the names

1128-- | Colourise annotations according to an Idris state. It ignores the names

1107-- in the annotation, as there's no good way to show extended information on a

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

1129 colour ItalicText = IdrisColour Nothing True False False True

1151 colour ItalicText = IdrisColour Nothing True False False True

1130

1152

1131-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

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

1133 -> PTerm -- ^^ the term to pretty-print

1155 -> PTerm -- ^^ the term to pretty-print

1134 -> Doc OutputAnnotation

1156 -> Doc OutputAnnotation

1135prettyImp impl = pprintPTerm impl [] [] []

1157prettyImp impl = pprintPTerm impl [] [] []

1136

1158

1137-- | Do the right thing for rendering a term in an IState

1159-- | Do the right thing for rendering a term in an IState

1138prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1160prettyIst :: 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)

1140

1162

1141-- | Pretty-print a high-level Idris term in some bindings context with infix info

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

1143 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1165 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1144 -> [Name] -- ^^ names to always show in pi, even if not used

1166 -> [Name] -- ^^ names to always show in pi, even if not used

1145 -> [FixDecl] -- ^^ Fixity declarations

1167 -> [FixDecl] -- ^^ Fixity declarations

1146 -> PTerm -- ^^ the term to pretty-print

1168 -> PTerm -- ^^ the term to pretty-print

1147 -> Doc OutputAnnotation

1169 -> Doc OutputAnnotation

1148−pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1170+pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1149 where

1171 where

1150 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1172 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1151 prettySe p bnd (PQuote r) =

1173 prettySe p bnd (PQuote r) =

@@ -1154,7 +1176,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1154 prettySe p bnd e

1176 prettySe p bnd e

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

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

1156 | Just n <- snat p e = annotate AnnConstData (text (show n))

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

1158 prettySe p bnd (PLam n ty sc) =

1180 prettySe p bnd (PLam n ty sc) =

1159 bracket p 2 . group . align . hang 2 $

1181 bracket p 2 . group . align . hang 2 $

1160 text "\\" <> bindingOf n False <+> text "=>" <$>

1182 text "\\" <> bindingOf n False <+> text "=>" <$>

@@ -1165,7 +1187,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1165 prettySe 10 bnd v <+> kwd "in" </>

1187 prettySe 10 bnd v <+> kwd "in" </>

1166 prettySe 10 ((n, False):bnd) sc

1188 prettySe 10 ((n, False):bnd) sc

1167 prettySe p bnd (PPi (Exp l s _) n ty sc)

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

1169 bracket p 2 . group $

1191 bracket p 2 . group $

1170 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1192 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1171 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

@@ -1178,7 +1200,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1178 Static -> text "[static]" <> space

1200 Static -> text "[static]" <> space

1179 _ -> empty

1201 _ -> empty

1180 prettySe p bnd (PPi (Imp l s _) n ty sc)

1202 prettySe p bnd (PPi (Imp l s _) n ty sc)

1181− | impl =

1203+ | ppopt_impl ppo =

1182 bracket p 2 $

1204 bracket p 2 $

1183 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1205 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1184 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1206 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1197,16 +1219,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1197 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1219 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1198 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1220 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1199 | UN nm <- basename f

1221 | UN nm <- basename f

1222+ , not (ppopt_impl ppo) && null (getExps args) =

1200− , not impl && null (getExps args) = if isAlpha (thead nm)

1223+ if isAlpha (thead nm)

1201− then prettyName impl bnd f

1224+ then prettyName (ppopt_impl ppo) bnd f

1202− else enclose lparen rparen $

1225+ else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f

1203− prettyName impl bnd f

1204 prettySe p bnd (PAppBind _ (PRef _ f) [])

1226 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

1206 prettySe p bnd (PApp _ (PRef _ op) args)

1228 prettySe p bnd (PApp _ (PRef _ op) args)

1207 | UN nm <- basename op

1229 | UN nm <- basename op

1208 , not (tnull nm) &&

1230 , not (tnull nm) &&

1209− (not impl) && (not $ isAlpha (thead nm)) =

1231+ (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1210 case getExps args of

1232 case getExps args of

1211 [] -> enclose lparen rparen opName

1233 [] -> enclose lparen rparen opName

1212 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1234 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

@@ -1215,7 +1237,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1215 (l:r:rest) -> bracket p 1 $

1237 (l:r:rest) -> bracket p 1 $

1216 enclose lparen rparen (inFix l r) <+>

1238 enclose lparen rparen (inFix l r) <+>

1217 align (group (vsep (map (prettyArgSe bnd) rest)))

1239 align (group (vsep (map (prettyArgSe bnd) rest)))

1218− where opName = prettyName impl bnd op

1240+ where opName = prettyName (ppopt_impl ppo) bnd op

1219 f = getFixity (opStr op)

1241 f = getFixity (opStr op)

1220 left l = case f of

1242 left l = case f of

1221 Nothing -> prettySe (-1) bnd l

1243 Nothing -> prettySe (-1) bnd l

@@ -1235,7 +1257,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1235 fp = prettySe 1 bnd f

1257 fp = prettySe 1 bnd f

1236 in

1258 in

1237 bracket p 1 . group $

1259 bracket p 1 . group $

1238− if impl

1260+ if ppopt_impl ppo

1239 then if null as

1261 then if null as

1240 then fp

1262 then fp

1241 else fp <+> align (vsep (map (prettyArgS bnd) as))

1263 else fp <+> align (vsep (map (prettyArgS bnd) as))

@@ -1340,9 +1362,9 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1340 basename n = n

1362 basename n = n

1341

1363

1342 slist' p bnd (PApp _ (PRef _ nil) _)

1364 slist' p bnd (PApp _ (PRef _ nil) _)

1343− | not impl && nsroot nil == sUN "Nil" = Just []

1365+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1344 slist' p bnd (PRef _ nil)

1366 slist' p bnd (PRef _ nil)

1345− | not impl && nsroot nil == sUN "Nil" = Just []

1367+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1346 slist' p bnd (PApp _ (PRef _ cons) args)

1368 slist' p bnd (PApp _ (PRef _ cons) args)

1347 | nsroot cons == sUN "::",

1369 | nsroot cons == sUN "::",

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

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

1415 strName other = show other

1437 strName other = show other

1416

1438

1417

1439

1418−showCImp :: Bool -> PClause -> Doc OutputAnnotation

1440+showCImp :: PPOption -> PClause -> Doc OutputAnnotation

1419−showCImp impl (PClause _ n l ws r w)

1441+showCImp ppo (PClause _ n l ws r w)

1420− = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

1442+ = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r

1421 <+> text "where" <+> text (show w)

1443 <+> text "where" <+> text (show w)

1422 where

1444 where

1423 showWs [] = empty

1445 showWs [] = empty

1424− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1446+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1425−showCImp impl (PWith _ n l ws r w)

1447+showCImp ppo (PWith _ n l ws r w)

1426− = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

1448+ = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

1427 <+> braces (text (show w))

1449 <+> braces (text (show w))

1428 where

1450 where

1429 showWs [] = empty

1451 showWs [] = empty

1430− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1452+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1431

1453

1432

1454

1433−showDImp :: Bool -> PData -> Doc OutputAnnotation

1455+showDImp :: PPOption -> PData -> Doc OutputAnnotation

1434−showDImp impl (PDatadecl n ty cons)

1456+showDImp ppo (PDatadecl n ty cons)

1435− = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1457+ = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>

1436− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1458+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))

1437

1459

1438−showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1460+showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

1439−showDecls i ds = vsep (map (showDeclImp i) ds)

1461+showDecls o ds = vsep (map (showDeclImp o) ds)

1440

1462

1441showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1463showDeclImp _ (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

1464+showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1443−showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1465+showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1444− indent 2 (vsep (map (showCImp i) cs))

1466+ indent 2 (vsep (map (showCImp o) cs))

1445−showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1467+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

1446−showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1468+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1447−showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1469+showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

1448showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1470showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1449−showDeclImp i (PClass _ _ _ cs n ps _ ds)

1471+showDeclImp o (PClass _ _ _ cs n ps _ ds)

1450− = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

1472+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1451−showDeclImp i (PInstance _ _ cs n _ t _ ds)

1473+showDeclImp o (PInstance _ _ cs n _ t _ ds)

1452− = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

1474+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1453showDeclImp _ _ = text "..."

1475showDeclImp _ _ = text "..."

1454−-- showDeclImp (PImport i) = "import " ++ i

1476+-- showDeclImp (PImport o) = "import " ++ o

1455

1477

1456instance Show (Doc OutputAnnotation) where

1478instance Show (Doc OutputAnnotation) where

1457 show = flip (displayS . renderCompact) ""

1479 show = flip (displayS . renderCompact) ""

@@ -1478,14 +1500,14 @@ getAll = map getTm

1478-- | Show Idris name

1500-- | Show Idris name

1479showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1501showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

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

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

1481− -> Bool -- ^^ whether to show implicits

1503+ -> PPOption -- ^^ pretty printing options

1482 -> Bool -- ^^ whether to colourise

1504 -> Bool -- ^^ whether to colourise

1483 -> Name -- ^^ the term to show

1505 -> Name -- ^^ the term to show

1484 -> String

1506 -> String

1485−showName ist bnd impl colour n = case ist of

1507+showName ist bnd ppo colour n = case ist of

1486 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1508 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1487 Nothing -> showbasic n

1509 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

1489 showbasic n@(UN _) = showCG n

1511 showbasic n@(UN _) = showCG n

1490 showbasic (MN _ s) = str s

1512 showbasic (MN _ s) = str s

1491 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

1513 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

1509 -> String

1531 -> String

1510showTm ist = displayDecorated (consoleDecorate ist) .

1532showTm ist = displayDecorated (consoleDecorate ist) .

1511 renderPretty 0.8 100000 .

1533 renderPretty 0.8 100000 .

1512− prettyImp (opt_showimp (idris_options ist))

1534+ prettyImp (ppOptionIst ist)

1513

1535

1514-- | Show a term with implicits, no colours

1536-- | Show a term with implicits, no colours

1515showTmImpls :: PTerm -> String

1537showTmImpls :: PTerm -> String

1516−showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

1538+showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

1517

1539

1518

1540

1519instance Sized PTerm where

1541instance Sized PTerm where

src/Idris/Core/TT.hs+3

@@ -426,6 +426,9 @@ lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)

426lookupCtxtExact :: Name -> Ctxt a -> Maybe a

427lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]

428

429+deleteDefExact :: Name -> Ctxt a -> Ctxt a

430+deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)

431+

429updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

432updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

430updateDef n f ctxt

433updateDef n f ctxt

431 = let ds = lookupCtxtName n ctxt in

434 = let ds = lookupCtxtName n ctxt in

src/Idris/Delaborate.hs+2−2

@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

138pprintTerm ist = pprintTerm' ist []

139

140pprintTerm' :: 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

142

143pprintErr :: IState -> Err -> Doc OutputAnnotation

144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>

269

270

271showqual :: 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)

273 where

274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of

275 [_] -> n -- just one thing

src/Idris/Docs.hs+9−9

@@ -36,8 +36,8 @@ showDoc d | nullDocstring d = empty

37pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

38pprintFD ist (FD n doc args ty f)

39− = nest 4 (prettyName imp [] n <+> colon <+>

39+ = nest 4 (prettyName (ppopt_impl ppo) [] n <+> colon <+>

40− pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args

40+ pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

41 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

42 renderDocstring doc <$>

43 maybe empty (\f -> text (show f) <> line) f <>

@@ -46,23 +46,23 @@ pprintFD ist (FD n doc args ty f)

46 then nest 4 $ text "Arguments:" <$> vsep argshow

47 else empty)

49− where imp = opt_showimp (idris_options ist)

49+ where ppo = ppOptionIst ist

50 infixes = idris_infixes ist

51 showArgs ((n, ty, Exp {}, Just d):args) bnd

52 = bindingOf n False <+> colon <+>

53− pprintPTerm imp bnd [] infixes ty <>

53+ pprintPTerm ppo bnd [] infixes ty <>

54 showDoc d <> line

55 :

56 showArgs args ((n, False):bnd)

57 showArgs ((n, ty, Constraint {}, Just d):args) bnd

58 = text "Class constraint" <+>

59− pprintPTerm imp bnd [] infixes ty <> showDoc d <> line

59+ pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line

60 :

61 showArgs args ((n, True):bnd)

62 showArgs ((n, ty, Imp {}, Just d):args) bnd

63 = text "(implicit)" <+>

64 bindingOf n True <+> colon <+>

65− pprintPTerm imp bnd [] infixes ty <>

65+ pprintPTerm ppo bnd [] infixes ty <>

66 showDoc d <> line

67 :

68 showArgs args ((n, True):bnd)

@@ -77,7 +77,7 @@ pprintDocs ist (DataDoc t args)

77 nest 4 (text "Constructors:" <> line <>

78 vsep (map (pprintFD ist) args))

79pprintDocs 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 <>

81 if nullDocstring doc then empty else line <> renderDocstring doc)

82 <> line <$>

83 nest 4 (text "Parameters:" <$> prettyParameters)

@@ -97,11 +97,11 @@ pprintDocs ist (ClassDoc n doc meths params instances)

98 pNames = map fst params

100− imp = opt_showimp (idris_options ist)

100+ ppo = ppOptionIst ist

101 infixes = idris_infixes ist

102

103 dumpInstance :: PTerm -> Doc OutputAnnotation

104− dumpInstance = pprintPTerm imp params' [] infixes

104+ dumpInstance = pprintPTerm ppo params' [] infixes

105

106 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

107 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

393 elimLog elimSig

394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

396− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

396+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

398 -- Do not elaborate clauses if there aren't any

399 case eliminatorClauses of

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

1863 constraint

1864 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

1865 let ddecl = PDatadecl tn tty cons

1866− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1866+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

1867 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

1868 -- for each constraint, build a top level function to chase it

1869 logLvl 5 $ "Building functions"

@@ -2059,7 +2059,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2059 let wbTys = map mkTyDecl mtys

2060 let wbVals = map (decorateid (decorate ns iname)) ds'

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

2063 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

2064 show (concat (nub wparams))

2065

src/Idris/IdrisDoc.hs+1−1

@@ -457,7 +457,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

457

458 where

459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names (idris_infixes ist) ftype

460+ signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype

461 names = [ n | (n@(UN n'), _, _, _) <- args,

462 not (T.isPrefixOf (txt "__") n') ]

463

src/Idris/Output.hs+6−6

@@ -88,16 +88,16 @@ ihPrintTermWithType h tm ty = do ist <- getIState

88-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

89ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

90ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

91−ihPrintFunTypes h bnd n overloads = do imp <- impShow

91+ihPrintFunTypes h bnd n overloads = do ist <- getIState

92− ist <- getIState

92+ let ppo = ppOptionIst ist

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

95 case idris_outputmode ist of

96 RawOutput -> consoleDisplayAnnotated h output

97 IdeSlave n -> ideSlaveReturnAnnotated n h output

98 where fullName n = prettyName True bnd n

99− ppOverload imp infixes n tm =

99+ ppOverload ppo infixes n tm =

100− fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)

100+ fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

101

102ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

103ihRenderResult h d = do ist <- getIState

@@ -123,7 +123,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

123 out = displayS . renderPretty 1.0 50 $ renderDocstring o

124 return (out "")

125 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) $

127 delabTy ist n

128 in (displayS . renderPretty 1.0 50 $ theTy) ""

129fancifyAnnots _ annot = annot

src/Idris/Parser.hs+1−1

@@ -1248,7 +1248,7 @@ loadSource h lidr f

1248 -- Parsing done, now process declarations

1249

1250 let ds = namespaces mname ds'

1251− logLvl 3 (show $ showDecls True ds)

1251+ logLvl 3 (show $ showDecls verbosePPOption ds)

1252 i <- getIState

1253 logLvl 10 (show (toAlist (idris_implicits i)))

1254 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 _ _ _ _) =

110 iputGoal rendered

111

112 where

113− showImplicits = opt_showimp (idris_options ist)

113+ ppo = ppOptionIst ist

114

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

116

117 assumptionNames :: Env -> [Name]

118 assumptionNames = map fst

@@ -237,16 +237,16 @@ ploop fn d prompt prf e h

237 ctxt' = envCtxt env ctxt

238 putIState ist { tt_ctxt = ctxt' }

239 (tm, ty) <- elabVal toplevel False t

240− let imp = opt_showimp (idris_options ist)

240+ let ppo = ppOptionIst ist

241 ty' = normaliseC ctxt [] ty

242 h = idris_outh ist

243 infixes = idris_infixes ist

244 case tm of

245 TType _ ->

246− ihPrintTermWithType h (prettyImp imp PType) type1Doc

246+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

247 _ -> let bnd = map (\x -> (fst x, False)) env in

248− ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))

248+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

249− (pprintPTerm imp bnd [] infixes (delab ist ty))

249+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

250 putIState ist

251 return (False, e, False, prf))

252 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -262,10 +262,10 @@ ploop fn d prompt prf e h

262 (tm, ty) <- elabVal toplevel False t

263 let tm' = force (normaliseAll ctxt' env tm)

264 ty' = force (normaliseAll ctxt' env ty)

265− imp = opt_showimp (idris_options ist')

265+ ppo = ppOption (idris_options ist')

266 infixes = idris_infixes ist

267− tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')

267+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

268− tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')

268+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

270 putIState ist

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

312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

313 do ist <- getIState

314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

315− imp <- impShow

315+ let ppo = ppOptionIst ist

316 let mvarTys = map (delabTy ist) mvs

317 let res = (IdeSlave.SymbolAtom "ok",

318 zipWith (\ n (prems, concl) -> (n, prems, concl))

319 (map (IdeSlave.StringAtom . show) mvs)

320− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

320+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))

321 runIO . putStrLn $ IdeSlave.convSExp "return" res id

322 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

323 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

324 in ((n, t):prems, conc)

325 getGoal tm = ([], tm)

326− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

326+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)

327 -> ([(String, String, SpanList OutputAnnotation)],

328 (String, SpanList OutputAnnotation))

329− sexpGoal ist cols imp ns ([], concl) =

329+ sexpGoal ist cols ppo ns ([], concl) =

330 let infixes = idris_infixes ist

331 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

333 in ([], concl')

334− sexpGoal ist cols imp ns ((n, t):ps, concl) =

334+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =

335 let n' = case n of

336 NS (UN nm) ns -> str nm

337 UN nm | ('_':'_':_) <- str nm -> "_"

338 | otherwise -> str nm

339 _ -> "_"

340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

341− pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t

341+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t

342− rest = sexpGoal ist cols imp (n:ns) (ps, concl)

342+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)

343 in ((n', t', spans) : fst rest, snd rest)

344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

345 case splitName n of

@@ -581,21 +581,21 @@ process h fn (ExecVal t)

581process h fn (Check (PRef _ n))

582 = do ctxt <- getContext

583 ist <- getIState

584− imp <- impShow

584+ let ppo = ppOptionIst ist

585 case lookupNames n ctxt of

586 ts@(t:_) ->

587 case lookup t (idris_metavars ist) of

588 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

589− showMetavarInfo imp ist n i

589+ showMetavarInfo ppo ist n i

590 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

591 [] -> ihPrintError h $ "No such variable " ++ show n

592 where

593− showMetavarInfo imp ist n i

593+ showMetavarInfo ppo ist n i

594 = case lookupTy n (tt_ctxt ist) of

595− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))

595+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

596− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

596+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

597− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

597+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

598− putTy imp ist i bnd (PPi _ n t sc)

598+ putTy ppo ist i bnd (PPi _ n t sc)

599 = let current = text " " <>

600 (case n of

601 MN _ _ -> text "_"

@@ -603,21 +603,21 @@ process h fn (Check (PRef _ n))

603 _ -> bindingOf n False) <+>

604 colon <+> align (tPretty bnd ist t) <> line

605 in

606− current <> putTy imp ist (i-1) ((n,False):bnd) sc

606+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc

607− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

607+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc

608− putGoal imp ist bnd g

608+ putGoal ppo ist bnd g

609 = text "--------------------------------------" <$>

610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

611 align (tPretty bnd ist g)

612

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

614

615

616process h fn (Check t)

617 = do (tm, ty) <- elabVal toplevel False t

618 ctxt <- getContext

619 ist <- getIState

620− let imp = opt_showimp (idris_options ist)

620+ let ppo = ppOptionIst ist

621 ty' = normaliseC ctxt [] ty

622 case tm of

623 TType _ ->

@@ -664,8 +664,8 @@ process h fn (TotCheck n)

664 [] -> ihPrintError h $ "Unknown operator " ++ show n

665 ts -> do ist <- getIState

666 c <- colourise

667− imp <- impShow

667+ let ppo = ppOptionIst ist

668− let showN = showName (Just ist) [] imp c

668+ let showN = showName (Just ist) [] ppo c

669 ihPrintResult h . concat . intersperse "\n" .

670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

671 ts

@@ -825,7 +825,7 @@ process h fn (DoProofSearch updatefile rec l n hints)

825 ctxt <- getContext

826 i <- getIState

827 return . flip displayS "" . renderPretty 1.0 80 $

828− pprintPTerm False [] [] (idris_infixes i)

828+ pprintPTerm defaultPPOption [] [] (idris_infixes i)

829 (stripNS

830 (dropCtxt envlen

831 (delab i (specialise ctxt [] [(mn, 1)] tm)))))

@@ -958,7 +958,6 @@ process h fn (TestInline t)

958 ctxt <- getContext

959 ist <- getIState

960 let tm' = inlineTerm ist tm

961− imp <- impShow

962 c <- colourise

961 c <- colourise

963 iPrintResult (showTm ist (delab ist tm'))

962 iPrintResult (showTm ist (delab ist tm'))

964process h fn Execute

963process h fn Execute