6e13c82 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Support presentations of abstract names in output

When Idris sends strings over the IDE protocol, it includes out-of-band semantic information that allows regions of the string to _represent_ their underlying data. In particular, terms are serialized and sent with their representations, allowing things like interactive error messages in IDE clients. This patch adds a similar capability for names. Now, serialized datatypes are sent with names, allowing names that don't have syntax to be the subjects of commands. This is very convenient when working with metaprogramming or debugging the compiler. The change is backwards-compatible, because it has to be enabled in each IDE client, and if they aren't sent serialized names, then they don't act differently from today.

commit6e13c82c379de8361b764da34b6626fc776354c8 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 22 May 2017, 00:52 (9 years ago) parentffd2db0

3 files changed+26−1

compare with master

unifiedsplit

CHANGELOG.md+4 src/Idris/IdeMode.hs+8−1 src/Idris/REPL.hs+14

CHANGELOG.md+4

@@ -1,3 +1,7 @@

1++ Names are now annotated with their representations over the IDE

2+ protocol, which allows IDEs to provide commands that work on special

3+ names that don't have syntax, such as case block names.

15# New in 1.0

37+ It's about time

src/Idris/IdeMode.hs+8−1

@@ -128,7 +128,8 @@ namespaceOf _ = Nothing

128128

129129instance SExpable OutputAnnotation where

130130 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

131− (SymbolAtom "implicit", BoolAtom False)] ++

131+ (SymbolAtom "implicit", BoolAtom False),

132+ (SymbolAtom "key", StringAtom (encodeName n))] ++

132133 maybeProps [("decor", ty)] ++

133134 maybeProps [("doc-overview", d), ("type", t)] ++

134135 maybeProps [("namespace", namespaceOf n)]

@@ -172,6 +173,12 @@ instance SExpable OutputAnnotation where

172173 toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]

173174 toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]

174175

176+encodeName :: Name -> String

177+encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

178+

179+decodeName :: String -> Name

180+decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

181+

175182encodeTerm :: [(Name, Bool)] -> Term -> String

176183encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

177184 (bnd, tm)

src/Idris/REPL.hs+14

@@ -26,6 +26,10 @@ import Control.Monad

2626import Control.Monad.Trans (lift)

2727import Control.Monad.Trans.Except (runExceptT)

2828import Control.Monad.Trans.State.Strict (evalStateT, get, put)

29+import qualified Data.Binary as Binary

30+import qualified Data.ByteString.Base64 as Base64

31+import qualified Data.ByteString.Lazy as Lazy

32+import qualified Data.ByteString.UTF8 as UTF8

2933import Data.Char

3034import Data.Either (partitionEithers)

3135import Data.List hiding (group)

@@ -582,6 +586,16 @@ ideModeForceTermImplicits h id bnd impl tm =

582586 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

583587

584588splitName :: String -> Either String Name

589+splitName s | "{{{{{" `isPrefixOf` s =

590+ decode $ drop 5 $ reverse $ drop 5 $ reverse s

591+ where decode x =

592+ case Base64.decode (UTF8.fromString x) of

593+ Left err -> Left err

594+ Right ok ->

595+ case Binary.decodeOrFail (Lazy.fromStrict ok) of

596+ Left _ -> Left "Bad binary instance for Name"

597+ Right (_, _, n) -> Right n

598+

585599splitName s = case reverse $ splitOn "." s of

586600 [] -> Left ("Didn't understand name '" ++ s ++ "'")

587601 [n] -> Right . sUN $ unparen n