git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' into liftDecls_js_backend
commitef9eac688b7b44d1615f561aa8edb567b9e7325f authorRui Barreiro <rui.barreiro@gmail.com> dateMon 22 May 2017, 13:34 (9 years ago) parent48f9a4b50b1b41
4 files changed+28−1
compare with master
unifiedsplit
CHANGELOG.md+5 src/Idris/Core/Evaluate.hs+1 src/Idris/IdeMode.hs+8−1 src/Idris/REPL.hs+14
CHANGELOG.md+5
@@ -3,6 +3,11 @@
33
44+ New javascript code generator that uses an higher level intermediate
55 representation.
6+
7++ Names are now annotated with their representations over the IDE
8+ protocol, which allows IDEs to provide commands that work on special
9+ names that don't have syntax, such as case block names
10+
611
712# New in 1.0
813
src/Idris/Core/Evaluate.hs+1
@@ -78,6 +78,7 @@ data Value = VP NameType Name Value
7878
7979canonical :: Value -> Bool
8080canonical (VP (DCon _ _ _) _ _) = True
81+canonical (VP (TCon _ _) _ _) = True
8182canonical (VApp f a) = canonical f
8283canonical (VConstant _) = True
8384canonical (VType _) = True
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