git.iko.soy/Idris-dev
on master help sign in
Add commands for working with serialised terms

In particular, IDEs can now request the implicit and explicit versions of previously-output terms. They can also request normalisation.

commitf50b357c9a5fbc79592d34cdfa2d5ec65080cd57 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 14 Jun 2014, 17:40 (12 years ago) parentd1a832a
2 files changed+43−2
compare with master
unifiedsplit
src/Idris/IdeSlave.hs+13−2 src/Idris/REPL.hs+30
src/Idris/IdeSlave.hs+13−2
@@ -132,8 +132,13 @@ instance SExpable OutputAnnotation where
132132 BoldText -> "bold"
133133 ItalicText -> "italic"
134134 UnderlineText -> "underline"
135− toSExp (AnnTerm tm) = toSExp [(SymbolAtom "tt-term", StringAtom encoded)]
136− where encoded = (UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode) tm
135+ toSExp (AnnTerm tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm tm))]
136+
137+encodeTerm :: Term -> String
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
137142
138143instance SExpable FC where
139144 toSExp (FC f (sl, sc) (el, ec)) =
@@ -191,6 +196,9 @@ data IdeSlaveCommand = REPLCompletions String
191196 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
192197 | WhoCalls String
193198 | CallsWho String
199+ | TermNormalise Term
200+ | TermShowImplicits Term
201+ | TermNoImplicits Term
194202
195203sexpToCommand :: SExp -> Maybe IdeSlaveCommand
196204sexpToCommand (SexpList (x:[])) = sexpToCommand x
@@ -227,6 +235,9 @@ sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
227235sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
228236sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
229237sexpToCommand (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))
230241sexpToCommand _ = Nothing
231242
232243parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+30
@@ -394,6 +394,36 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =
394394 renderPretty 0.9 1000 .
395395 fmap (fancifyAnnots ist) .
396396 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+
397427
398428splitName :: String -> Either String Name
399429splitName s = case reverse $ splitOn "." s of