git.iko.soy/Idris-dev
on master help sign in
Add commands for working with serialised terms
f50b357David Raymond Christiansen
src/Idris/IdeSlave.hs+13−2
compare with master
unifiedsplit
@@ -132,8 +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 encoded)]
135+ toSExp (AnnTerm tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm tm))]
136+
137+encodeTerm :: Term -> String
136− where encoded = (UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode) tm
138+encodeTerm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode
139+
140+decodeTerm :: String -> Term
141+decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
137
142
138instance SExpable FC where
143instance SExpable FC where
139 toSExp (FC f (sl, sc) (el, ec)) =
144 toSExp (FC f (sl, sc) (el, ec)) =
@@ -191,6 +196,9 @@ data IdeSlaveCommand = REPLCompletions String
191 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
196 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
192 | WhoCalls String
197 | WhoCalls String
193 | CallsWho String
198 | CallsWho String
199+ | TermNormalise Term
200+ | TermShowImplicits Term
201+ | TermNoImplicits Term
194
202
195sexpToCommand :: SExp -> Maybe IdeSlaveCommand
203sexpToCommand :: SExp -> Maybe IdeSlaveCommand
196sexpToCommand (SexpList (x:[])) = sexpToCommand x
204sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -227,6 +235,9 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
227sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
235sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
228sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
236sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
229sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
237sexpToCommand (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))
230sexpToCommand _ = Nothing
241sexpToCommand _ = Nothing
231
242
232parseMessage :: String -> Either Err (SExp, Integer)
243parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+30
@@ -394,6 +394,36 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
394 renderPretty 0.9 1000 .
394 renderPretty 0.9 1000 .
395 fmap (fancifyAnnots ist) .
395 fmap (fancifyAnnots ist) .
396 prettyName True []
396 prettyName True []
397+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise tm) =
398+ do ctxt <- getContext
399+ ist <- getIState
400+ let tm' = force (normaliseAll ctxt [] tm)
401+ ptm = annotate (AnnTerm tm')
402+ (pprintDelab ist tm')
403+ msg = (IdeSlave.SymbolAtom "ok",
404+ displaySpans .
405+ renderPretty 0.9 80 .
406+ fmap (fancifyAnnots ist) $ ptm)
407+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
408+runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits tm) =
409+ ideSlaveForceTermImplicits id True tm
410+runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits tm) =
411+ ideSlaveForceTermImplicits id False tm
412+
413+-- | Show a term for IDESlave with the specified implicitness
414+ideSlaveForceTermImplicits :: Integer -> Bool -> Term -> Idris ()
415+ideSlaveForceTermImplicits id impl tm =
416+ do ist <- getIState
417+ let expl = annotate (AnnTerm tm)
418+ (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
419+ [] [] (idris_infixes ist)
420+ (delab ist tm))
421+ msg = (IdeSlave.SymbolAtom "ok",
422+ displaySpans .
423+ renderPretty 0.9 80 .
424+ fmap (fancifyAnnots ist) $ expl)
425+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id
426+
397
427
398splitName :: String -> Either String Name
428splitName :: String -> Either String Name
399splitName s = case reverse $ splitOn "." s of
429splitName s = case reverse $ splitOn "." s of