git.iko.soy/Idris-dev
on master help sign in
Maintain pretty-printer bound vars

This means serialized terms, when normalized, will have correct colors for bound variables.

commite245d488007c32e1ab325dbbf24f41e26146f496 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 15 Jun 2014, 22:18 (12 years ago) parentda6ed85
6 files changed+37−28
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Core/TT.hs+1−1 src/Idris/Delaborate.hs+3−3 src/Idris/IdeSlave.hs+14−10 src/Idris/Prover.hs+1−1 src/Idris/REPL.hs+17−12
src/Idris/AbsSyntaxTree.hs+1−1
@@ -1164,7 +1164,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
11641164 where colour BoldText = IdrisColour Nothing True False True False
11651165 colour UnderlineText = IdrisColour Nothing True True False False
11661166 colour ItalicText = IdrisColour Nothing True False False True
1167−consoleDecorate ist (AnnTerm _) = id
1167+consoleDecorate ist (AnnTerm _ _) = id
11681168
11691169isPostulateName :: Name -> IState -> Bool
11701170isPostulateName 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
9999 | AnnKeyword
100100 | AnnFC FC
101101 | AnnTextFmt TextFormatting
102− | AnnTerm (TT Name)
102+ | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
103103
104104-- | Used for error reflection
105105data ErrorReportPart = TextPart String
src/Idris/Delaborate.hs+3−3
@@ -137,14 +137,14 @@ indented = nest errorIndent . (line <>)
137137
138138-- | Pretty-print a core term using delaboration
139139pprintDelab :: IState -> Term -> Doc OutputAnnotation
140−pprintDelab ist tm = annotate (AnnTerm tm)
140+pprintDelab ist tm = annotate (AnnTerm [] tm)
141141 (prettyIst ist (delab ist tm))
142142
143143-- | Pretty-print the type of some name
144144pprintDelabTy :: IState -> Name -> Doc OutputAnnotation
145145pprintDelabTy i n
146146 = case lookupTy n (tt_ctxt i) of
147− (ty:_) -> annotate (AnnTerm ty) . prettyIst i $
147+ (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $
148148 case lookupCtxt n (idris_implicits i) of
149149 (imps:_) -> delabTy' i imps ty False False
150150 _ -> delabTy' i [] ty False False
@@ -274,7 +274,7 @@ annName' :: Name -> String -> Doc OutputAnnotation
274274annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)
275275
276276annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation
277−annTm tm = annotate (AnnTerm tm)
277+annTm tm = annotate (AnnTerm [] tm)
278278
279279fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
280280fancifyAnnots ist annot@(AnnName n _ _ _) =
src/Idris/IdeSlave.hs+14−10
@@ -132,12 +132,13 @@ instance SExpable OutputAnnotation where
132132 BoldText -> "bold"
133133 ItalicText -> "italic"
134134 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))]
136136
137−encodeTerm :: Term -> String
138−encodeTerm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode
137+encodeTerm :: [(Name, Bool)] -> Term -> String
138+encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
139+ (bnd, tm)
139140
140−decodeTerm :: String -> Term
141+decodeTerm :: String -> ([(Name, Bool)], Term)
141142decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
142143
143144instance SExpable FC where
@@ -196,9 +197,9 @@ data IdeSlaveCommand = REPLCompletions String
196197 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
197198 | WhoCalls String
198199 | CallsWho String
199− | TermNormalise Term
200− | TermShowImplicits Term
201− | TermNoImplicits Term
200+ | TermNormalise [(Name, Bool)] Term
201+ | TermShowImplicits [(Name, Bool)] Term
202+ | TermNoImplicits [(Name, Bool)] Term
202203
203204sexpToCommand :: SExp -> Maybe IdeSlaveCommand
204205sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -235,9 +236,12 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
235236sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
236237sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
237238sexpToCommand (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 "show-term-implicits", StringAtom encoded]) = Just (TermShowImplicits (decodeTerm encoded))
240−sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = Just (TermNoImplicits (decodeTerm encoded))
239+sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
240+ Just (TermNormalise bnd tm)
241+sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
242+ Just (TermShowImplicits bnd tm)
243+sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
244+ Just (TermNoImplicits bnd tm)
241245sexpToCommand _ = Nothing
242246
243247parseMessage :: 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 _ _ _ _) =
121121 where
122122 ppo = ppOptionIst ist
123123
124− tPretty bnd t = annotate (AnnTerm t) .
124+ tPretty bnd t = annotate (AnnTerm bnd t) .
125125 pprintPTerm ppo bnd [] (idris_infixes ist) $
126126 delab ist t
127127
src/Idris/REPL.hs+17−12
@@ -385,7 +385,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
385385 displaySpans .
386386 renderPretty 0.9 cols .
387387 fmap (fancifyAnnots ist) .
388− annotate (AnnTerm t) $ prettyT
388+ annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $
389+ prettyT
389390
390391 -- | Juggle the bits of a premise to prepare for output.
391392 processPremise :: IState
@@ -422,29 +423,33 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
422423 renderPretty 0.9 1000 .
423424 fmap (fancifyAnnots ist) .
424425 prettyName True []
425−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise tm) =
426+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =
426427 do ctxt <- getContext
427428 ist <- getIState
428429 let tm' = force (normaliseAll ctxt [] tm)
429− ptm = annotate (AnnTerm tm')
430− (pprintDelab ist tm')
430+ ptm = annotate (AnnTerm bnd tm')
431+ (pprintPTerm (ppOptionIst ist)
432+ bnd
433+ []
434+ (idris_infixes ist)
435+ (delab ist tm'))
431436 msg = (IdeSlave.SymbolAtom "ok",
432437 displaySpans .
433438 renderPretty 0.9 80 .
434439 fmap (fancifyAnnots ist) $ ptm)
435440 runIO . putStrLn $ IdeSlave.convSExp "return" msg id
436−runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits tm) =
437− ideSlaveForceTermImplicits id True tm
438−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits tm) =
439− ideSlaveForceTermImplicits id False tm
441+runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =
442+ ideSlaveForceTermImplicits id bnd True tm
443+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
444+ ideSlaveForceTermImplicits id bnd False tm
440445
441446-- | Show a term for IDESlave with the specified implicitness
442−ideSlaveForceTermImplicits :: Integer -> Bool -> Term -> Idris ()
443−ideSlaveForceTermImplicits id impl tm =
447+ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
448+ideSlaveForceTermImplicits id bnd impl tm =
444449 do ist <- getIState
445− let expl = annotate (AnnTerm tm)
450+ let expl = annotate (AnnTerm [] tm)
446451 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
447− [] [] (idris_infixes ist)
452+ bnd [] (idris_infixes ist)
448453 (delab ist tm))
449454 msg = (IdeSlave.SymbolAtom "ok",
450455 displaySpans .