git.iko.soy/Idris-dev
on master help sign in
Maintain pretty-printer bound vars
e245d48David Raymond Christiansen
src/Idris/AbsSyntaxTree.hs+1−1
compare with master
unifiedsplit
@@ -1164,7 +1164,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1164 where colour BoldText = IdrisColour Nothing True False True False
1164 where colour BoldText = IdrisColour Nothing True False True False
1165 colour UnderlineText = IdrisColour Nothing True True False False
1165 colour UnderlineText = IdrisColour Nothing True True False False
1166 colour ItalicText = IdrisColour Nothing True False False True
1166 colour ItalicText = IdrisColour Nothing True False False True
1167−consoleDecorate ist (AnnTerm _) = id
1167+consoleDecorate ist (AnnTerm _ _) = id
1168
1168
1169isPostulateName :: Name -> IState -> Bool
1169isPostulateName :: Name -> IState -> Bool
1170isPostulateName n ist = S.member n (idris_postulates ist)
1170isPostulateName n ist = S.member n (idris_postulates ist)
src/Idris/Core/TT.hs+1−1
@@ -99,7 +99,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St
99 | AnnKeyword
99 | AnnKeyword
100 | AnnFC FC
100 | AnnFC FC
101 | AnnTextFmt TextFormatting
101 | AnnTextFmt TextFormatting
102− | AnnTerm (TT Name)
102+ | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
103
103
104-- | Used for error reflection
104-- | Used for error reflection
105data ErrorReportPart = TextPart String
105data ErrorReportPart = TextPart String
src/Idris/Delaborate.hs+3−3
@@ -137,14 +137,14 @@ indented = nest errorIndent . (line <>)
137
137
138-- | Pretty-print a core term using delaboration
138-- | Pretty-print a core term using delaboration
139pprintDelab :: IState -> Term -> Doc OutputAnnotation
139pprintDelab :: IState -> Term -> Doc OutputAnnotation
140−pprintDelab ist tm = annotate (AnnTerm tm)
140+pprintDelab ist tm = annotate (AnnTerm [] tm)
141 (prettyIst ist (delab ist tm))
141 (prettyIst ist (delab ist tm))
142
142
143-- | Pretty-print the type of some name
143-- | Pretty-print the type of some name
144pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
144pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
145pprintDelabTy i n
145pprintDelabTy i n
146 = case lookupTy n (tt_ctxt i) of
146 = case lookupTy n (tt_ctxt i) of
147− (ty:_) -> annotate (AnnTerm ty) . prettyIst i $
147+ (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
148 case lookupCtxt n (idris_implicits i) of
148 case lookupCtxt n (idris_implicits i) of
149 (imps:_) -> delabTy' i imps ty False False
149 (imps:_) -> delabTy' i imps ty False False
150 _ -> delabTy' i [] ty False False
150 _ -> delabTy' i [] ty False False
@@ -274,7 +274,7 @@ annName' :: Name -> String -> Doc OutputAnnotation
274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
275
275
276annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
276annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
277−annTm tm = annotate (AnnTerm tm)
277+annTm tm = annotate (AnnTerm [] tm)
278
278
279fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
279fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
280fancifyAnnots ist annot@(AnnName n _ _ _) =
280fancifyAnnots ist annot@(AnnName n _ _ _) =
src/Idris/IdeSlave.hs+14−10
@@ -132,12 +132,13 @@ instance SExpable OutputAnnotation where
132 BoldText -> "bold"
132 BoldText -> "bold"
133 ItalicText -> "italic"
133 ItalicText -> "italic"
134 UnderlineText -> "underline"
134 UnderlineText -> "underline"
135− toSExp (AnnTerm tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm tm))]
135+ toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
136
136
137−encodeTerm :: Term -> String
137+encodeTerm :: [(Name, Bool)] -> Term -> String
138−encodeTerm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode
138+encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
139+ (bnd, tm)
139
140
140−decodeTerm :: String -> Term
141+decodeTerm :: String -> ([(Name, Bool)], Term)
141decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
142decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
142
143
143instance SExpable FC where
144instance SExpable FC where
@@ -196,9 +197,9 @@ data IdeSlaveCommand = REPLCompletions String
196 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
197 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
197 | WhoCalls String
198 | WhoCalls String
198 | CallsWho String
199 | CallsWho String
199− | TermNormalise Term
200+ | TermNormalise [(Name, Bool)] Term
200− | TermShowImplicits Term
201+ | TermShowImplicits [(Name, Bool)] Term
201− | TermNoImplicits Term
202+ | TermNoImplicits [(Name, Bool)] Term
202
203
203sexpToCommand :: SExp -> Maybe IdeSlaveCommand
204sexpToCommand :: SExp -> Maybe IdeSlaveCommand
204sexpToCommand (SexpList (x:[])) = sexpToCommand x
205sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -235,9 +236,12 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
235sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
236sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
236sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
237sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
237sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
238sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
238−sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = Just (TermNormalise (decodeTerm encoded))
239+sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
240+ Just (TermNormalise bnd tm)
239−sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = Just (TermShowImplicits (decodeTerm encoded))
241+sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
242+ Just (TermShowImplicits bnd tm)
240−sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = Just (TermNoImplicits (decodeTerm encoded))
243+sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
244+ Just (TermNoImplicits bnd tm)
241sexpToCommand _ = Nothing
245sexpToCommand _ = Nothing
242
246
243parseMessage :: String -> Either Err (SExp, Integer)
247parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/Prover.hs+1−1
@@ -121,7 +121,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
121 where
121 where
122 ppo = ppOptionIst ist
122 ppo = ppOptionIst ist
123
123
124− tPretty bnd t = annotate (AnnTerm t) .
124+ tPretty bnd t = annotate (AnnTerm bnd t) .
125 pprintPTerm ppo bnd [] (idris_infixes ist) $
125 pprintPTerm ppo bnd [] (idris_infixes ist) $
126 delab ist t
126 delab ist t
127
127
src/Idris/REPL.hs+17−12
@@ -385,7 +385,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
385 displaySpans .
385 displaySpans .
386 renderPretty 0.9 cols .
386 renderPretty 0.9 cols .
387 fmap (fancifyAnnots ist) .
387 fmap (fancifyAnnots ist) .
388− annotate (AnnTerm t) $ prettyT
388+ annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
389+ prettyT
389
390
390 -- | Juggle the bits of a premise to prepare for output.
391 -- | Juggle the bits of a premise to prepare for output.
391 processPremise :: IState
392 processPremise :: IState
@@ -422,29 +423,33 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
422 renderPretty 0.9 1000 .
423 renderPretty 0.9 1000 .
423 fmap (fancifyAnnots ist) .
424 fmap (fancifyAnnots ist) .
424 prettyName True []
425 prettyName True []
425−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise tm) =
426+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =
426 do ctxt <- getContext
427 do ctxt <- getContext
427 ist <- getIState
428 ist <- getIState
428 let tm' = force (normaliseAll ctxt [] tm)
429 let tm' = force (normaliseAll ctxt [] tm)
429− ptm = annotate (AnnTerm tm')
430+ ptm = annotate (AnnTerm bnd tm')
430− (pprintDelab ist tm')
431+ (pprintPTerm (ppOptionIst ist)
432+ bnd
433+ []
434+ (idris_infixes ist)
435+ (delab ist tm'))
431 msg = (IdeSlave.SymbolAtom "ok",
436 msg = (IdeSlave.SymbolAtom "ok",
432 displaySpans .
437 displaySpans .
433 renderPretty 0.9 80 .
438 renderPretty 0.9 80 .
434 fmap (fancifyAnnots ist) $ ptm)
439 fmap (fancifyAnnots ist) $ ptm)
435 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
440 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
436−runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits tm) =
441+runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
437− ideSlaveForceTermImplicits id True tm
442+ ideSlaveForceTermImplicits id bnd True tm
438−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits tm) =
443+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
439− ideSlaveForceTermImplicits id False tm
444+ ideSlaveForceTermImplicits id bnd False tm
440
445
441-- | Show a term for IDESlave with the specified implicitness
446-- | Show a term for IDESlave with the specified implicitness
442−ideSlaveForceTermImplicits :: Integer -> Bool -> Term -> Idris ()
447+ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
443−ideSlaveForceTermImplicits id impl tm =
448+ideSlaveForceTermImplicits id bnd impl tm =
444 do ist <- getIState
449 do ist <- getIState
445− let expl = annotate (AnnTerm tm)
450+ let expl = annotate (AnnTerm [] tm)
446 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
451 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
447− [] [] (idris_infixes ist)
452+ bnd [] (idris_infixes ist)
448 (delab ist tm))
453 (delab ist tm))
449 msg = (IdeSlave.SymbolAtom "ok",
454 msg = (IdeSlave.SymbolAtom "ok",
450 displaySpans .
455 displaySpans .