ef9eac6 · Idris-dev · git.iko.soy

CHANGELOG.md+5

compare with master

unifiedsplit

@@ -3,6 +3,11 @@

3

4+ New javascript code generator that uses an higher level intermediate

5 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+

6

11

7# New in 1.0

12# New in 1.0

8

13

src/Idris/Core/Evaluate.hs+1

@@ -78,6 +78,7 @@ data Value = VP NameType Name Value

78

79canonical :: Value -> Bool

80canonical (VP (DCon _ _ _) _ _) = True

81+canonical (VP (TCon _ _) _ _) = True

81canonical (VApp f a) = canonical f

82canonical (VApp f a) = canonical f

82canonical (VConstant _) = True

83canonical (VConstant _) = True

83canonical (VType _) = True

84canonical (VType _) = True

src/Idris/IdeMode.hs+8−1

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

128

129instance SExpable OutputAnnotation where

130 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))] ++

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

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

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

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

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

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

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

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

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

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

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

174

175

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+

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

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

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

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

177 (bnd, tm)

184 (bnd, tm)

src/Idris/REPL.hs+14

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

26import Control.Monad.Trans (lift)

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

28import 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

29import Data.Char

33import Data.Char

30import Data.Either (partitionEithers)

34import Data.Either (partitionEithers)

31import Data.List hiding (group)

35import Data.List hiding (group)

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

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

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

583

587

584splitName :: String -> Either String Name

588splitName :: 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+

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

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

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

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

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

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