{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where
import Idris.Core.Binary ()
import Idris.Core.TT
import Control.Applicative hiding (Const)
import Control.Arrow (left)
import qualified Data.Binary as Binary
import qualified Data.ByteString.Base64 as Base64
import qualified Data.ByteString.Lazy as Lazy
import qualified Data.ByteString.UTF8 as UTF8
import Data.List
import Data.Maybe (isJust)
import qualified Data.Text as T
import Numeric
import System.IO
import qualified Text.Megaparsec as P
import qualified Text.Megaparsec.Char as P
import Text.Printf
getNChar :: Handle -> Int -> String -> IO (String)
getNChar :: Handle -> Int -> String -> IO String
getNChar _ 0 s :: String
s = String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
forall a. [a] -> [a]
reverse String
s)
getNChar h :: Handle
h n :: Int
n s :: String
s = do Char
c <- Handle -> IO Char
hGetChar Handle
h
Handle -> Int -> String -> IO String
getNChar Handle
h (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: String
s)
getLen :: Handle -> IO (Either Err Int)
getLen :: Handle -> IO (Either Err Int)
getLen h :: Handle
h = do String
s <- Handle -> Int -> String -> IO String
getNChar Handle
h 6 ""
case ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex String
s of
((num :: Int
num, ""):_) -> Either Err Int -> IO (Either Err Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Err Int -> IO (Either Err Int))
-> Either Err Int -> IO (Either Err Int)
forall a b. (a -> b) -> a -> b
$ Int -> Either Err Int
forall a b. b -> Either a b
Right Int
num
_ -> Either Err Int -> IO (Either Err Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Err Int -> IO (Either Err Int))
-> Either Err Int -> IO (Either Err Int)
forall a b. (a -> b) -> a -> b
$ Err -> Either Err Int
forall a b. a -> Either a b
Left (Err -> Either Err Int)
-> (String -> Err) -> String -> Either Err Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Either Err Int) -> String -> Either Err Int
forall a b. (a -> b) -> a -> b
$ "Couldn't read length " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
data SExp = SexpList [SExp]
| StringAtom String
| BoolAtom Bool
| IntegerAtom Integer
| SymbolAtom String
deriving ( SExp -> SExp -> Bool
(SExp -> SExp -> Bool) -> (SExp -> SExp -> Bool) -> Eq SExp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SExp -> SExp -> Bool
$c/= :: SExp -> SExp -> Bool
== :: SExp -> SExp -> Bool
$c== :: SExp -> SExp -> Bool
Eq, Int -> SExp -> String -> String
[SExp] -> String -> String
SExp -> String
(Int -> SExp -> String -> String)
-> (SExp -> String) -> ([SExp] -> String -> String) -> Show SExp
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SExp] -> String -> String
$cshowList :: [SExp] -> String -> String
show :: SExp -> String
$cshow :: SExp -> String
showsPrec :: Int -> SExp -> String -> String
$cshowsPrec :: Int -> SExp -> String -> String
Show )
sExpToString :: SExp -> String
sExpToString :: SExp -> String
sExpToString (StringAtom s :: String
s) = "\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
escape String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\""
sExpToString (BoolAtom True) = ":True"
sExpToString (BoolAtom False) = ":False"
sExpToString (IntegerAtom i :: Integer
i) = String -> Integer -> String
forall r. PrintfType r => String -> r
printf "%d" Integer
i
sExpToString (SymbolAtom s :: String
s) = ":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
sExpToString (SexpList l :: [SExp]
l) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " " ((SExp -> String) -> [SExp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExp -> String
sExpToString [SExp]
l) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
class SExpable a where
toSExp :: a -> SExp
instance SExpable SExp where
toSExp :: SExp -> SExp
toSExp a :: SExp
a = SExp
a
instance SExpable Bool where
toSExp :: Bool -> SExp
toSExp True = Bool -> SExp
BoolAtom Bool
True
toSExp False = Bool -> SExp
BoolAtom Bool
False
instance SExpable String where
toSExp :: String -> SExp
toSExp s :: String
s = String -> SExp
StringAtom String
s
instance SExpable Integer where
toSExp :: Integer -> SExp
toSExp n :: Integer
n = Integer -> SExp
IntegerAtom Integer
n
instance SExpable Int where
toSExp :: Int -> SExp
toSExp n :: Int
n = Integer -> SExp
IntegerAtom (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)
instance SExpable Name where
toSExp :: Name -> SExp
toSExp s :: Name
s = String -> SExp
StringAtom (Name -> String
forall a. Show a => a -> String
show Name
s)
instance (SExpable a) => SExpable (Maybe a) where
toSExp :: Maybe a -> SExp
toSExp Nothing = [SExp] -> SExp
SexpList [String -> SExp
SymbolAtom "Nothing"]
toSExp (Just a :: a
a) = [SExp] -> SExp
SexpList [String -> SExp
SymbolAtom "Just", a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
a]
instance (SExpable a) => SExpable [a] where
toSExp :: [a] -> SExp
toSExp l :: [a]
l = [SExp] -> SExp
SexpList ((a -> SExp) -> [a] -> [SExp]
forall a b. (a -> b) -> [a] -> [b]
map a -> SExp
forall a. SExpable a => a -> SExp
toSExp [a]
l)
instance (SExpable a, SExpable b) => SExpable (a, b) where
toSExp :: (a, b) -> SExp
toSExp (l :: a
l, r :: b
r) = [SExp] -> SExp
SexpList [a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
l, b -> SExp
forall a. SExpable a => a -> SExp
toSExp b
r]
instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
toSExp :: (a, b, c) -> SExp
toSExp (l :: a
l, m :: b
m, n :: c
n) = [SExp] -> SExp
SexpList [a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
l, b -> SExp
forall a. SExpable a => a -> SExp
toSExp b
m, c -> SExp
forall a. SExpable a => a -> SExp
toSExp c
n]
instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
toSExp :: (a, b, c, d) -> SExp
toSExp (l :: a
l, m :: b
m, n :: c
n, o :: d
o) = [SExp] -> SExp
SexpList [a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
l, b -> SExp
forall a. SExpable a => a -> SExp
toSExp b
m, c -> SExp
forall a. SExpable a => a -> SExp
toSExp c
n, d -> SExp
forall a. SExpable a => a -> SExp
toSExp d
o]
instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>
SExpable (a, b, c, d, e) where
toSExp :: (a, b, c, d, e) -> SExp
toSExp (l :: a
l, m :: b
m, n :: c
n, o :: d
o, p :: e
p) = [SExp] -> SExp
SexpList [a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
l, b -> SExp
forall a. SExpable a => a -> SExp
toSExp b
m, c -> SExp
forall a. SExpable a => a -> SExp
toSExp c
n, d -> SExp
forall a. SExpable a => a -> SExp
toSExp d
o, e -> SExp
forall a. SExpable a => a -> SExp
toSExp e
p]
instance SExpable NameOutput where
toSExp :: NameOutput -> SExp
toSExp TypeOutput = String -> SExp
SymbolAtom "type"
toSExp FunOutput = String -> SExp
SymbolAtom "function"
toSExp DataOutput = String -> SExp
SymbolAtom "data"
toSExp MetavarOutput = String -> SExp
SymbolAtom "metavar"
toSExp PostulateOutput = String -> SExp
SymbolAtom "postulate"
maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps :: [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [] = []
maybeProps ((n :: String
n, Just p :: a
p):ps :: [(String, Maybe a)]
ps) = (String -> SExp
SymbolAtom String
n, a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
p) (SExp, SExp) -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. a -> [a] -> [a]
: [(String, Maybe a)] -> [(SExp, SExp)]
forall a. SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [(String, Maybe a)]
ps
maybeProps ((n :: String
n, Nothing):ps :: [(String, Maybe a)]
ps) = [(String, Maybe a)] -> [(SExp, SExp)]
forall a. SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [(String, Maybe a)]
ps
constTy :: Const -> String
constTy :: Const -> String
constTy (I _) = "Int"
constTy (BI _) = "Integer"
constTy (Fl _) = "Double"
constTy (Ch _) = "Char"
constTy (Str _) = "String"
constTy (B8 _) = "Bits8"
constTy (B16 _) = "Bits16"
constTy (B32 _) = "Bits32"
constTy (B64 _) = "Bits64"
constTy _ = "Type"
namespaceOf :: Name -> Maybe String
namespaceOf :: Name -> Maybe String
namespaceOf (NS _ ns :: [Text]
ns) = String -> Maybe String
forall a. a -> Maybe a
Just (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
ns))
namespaceOf _ = Maybe String
forall a. Maybe a
Nothing
instance SExpable OutputAnnotation where
toSExp :: OutputAnnotation -> SExp
toSExp (AnnName n :: Name
n ty :: Maybe NameOutput
ty d :: Maybe String
d t :: Maybe String
t) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp ([(SExp, SExp)] -> SExp) -> [(SExp, SExp)] -> SExp
forall a b. (a -> b) -> a -> b
$ [(String -> SExp
SymbolAtom "name", String -> SExp
StringAtom (Name -> String
forall a. Show a => a -> String
show Name
n)),
(String -> SExp
SymbolAtom "implicit", Bool -> SExp
BoolAtom Bool
False),
(String -> SExp
SymbolAtom "key", String -> SExp
StringAtom (Name -> String
encodeName Name
n))] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
[(String, Maybe NameOutput)] -> [(SExp, SExp)]
forall a. SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [("decor", Maybe NameOutput
ty)] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
[(String, Maybe String)] -> [(SExp, SExp)]
forall a. SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [("doc-overview", Maybe String
d), ("type", Maybe String
t)] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
[(String, Maybe String)] -> [(SExp, SExp)]
forall a. SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [("namespace", Name -> Maybe String
namespaceOf Name
n)]
toSExp (AnnBoundName n :: Name
n imp :: Bool
imp) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "name", String -> SExp
StringAtom (Name -> String
forall a. Show a => a -> String
show Name
n)),
(String -> SExp
SymbolAtom "decor", String -> SExp
SymbolAtom "bound"),
(String -> SExp
SymbolAtom "implicit", Bool -> SExp
BoolAtom Bool
imp)]
toSExp (AnnConst c :: Const
c) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "decor",
String -> SExp
SymbolAtom (if Const -> Bool
constIsType Const
c then "type" else "data")),
(String -> SExp
SymbolAtom "type", String -> SExp
StringAtom (Const -> String
constTy Const
c)),
(String -> SExp
SymbolAtom "doc-overview", String -> SExp
StringAtom (Const -> String
constDocs Const
c)),
(String -> SExp
SymbolAtom "name", String -> SExp
StringAtom (Const -> String
forall a. Show a => a -> String
show Const
c))]
toSExp (AnnData ty :: String
ty doc :: String
doc) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "decor", String -> SExp
SymbolAtom "data"),
(String -> SExp
SymbolAtom "type", String -> SExp
StringAtom String
ty),
(String -> SExp
SymbolAtom "doc-overview", String -> SExp
StringAtom String
doc)]
toSExp (AnnType name :: String
name doc :: String
doc) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp ([(SExp, SExp)] -> SExp) -> [(SExp, SExp)] -> SExp
forall a b. (a -> b) -> a -> b
$ [(String -> SExp
SymbolAtom "decor", String -> SExp
SymbolAtom "type"),
(String -> SExp
SymbolAtom "type", String -> SExp
StringAtom "Type"),
(String -> SExp
SymbolAtom "doc-overview", String -> SExp
StringAtom String
doc)] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
if Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
name) then [(String -> SExp
SymbolAtom "name", String -> SExp
StringAtom String
name)] else []
toSExp AnnKeyword = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "decor", String -> SExp
SymbolAtom "keyword")]
toSExp (AnnFC fc :: FC
fc) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "source-loc", FC -> SExp
forall a. SExpable a => a -> SExp
toSExp FC
fc)]
toSExp (AnnTextFmt fmt :: TextFormatting
fmt) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "text-formatting", String -> SExp
SymbolAtom String
format)]
where format :: String
format = case TextFormatting
fmt of
BoldText -> "bold"
ItalicText -> "italic"
UnderlineText -> "underline"
toSExp (AnnLink url :: String
url) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "link-href", String -> SExp
StringAtom String
url)]
toSExp (AnnTerm bnd :: [(Name, Bool)]
bnd tm :: TT Name
tm)
| Int -> TT Name -> Bool
termSmallerThan 1000 TT Name
tm = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "tt-term", String -> SExp
StringAtom ([(Name, Bool)] -> TT Name -> String
encodeTerm [(Name, Bool)]
bnd TT Name
tm))]
| Bool
otherwise = [SExp] -> SExp
SexpList []
toSExp (AnnSearchResult ordr :: Ordering
ordr) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "doc-overview",
String -> SExp
StringAtom ("Result type is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
descr))]
where descr :: String
descr = case Ordering
ordr of
EQ -> "isomorphic"
LT -> "more general than searched type"
GT -> "more specific than searched type"
toSExp (AnnErr e :: Err
e) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "error", String -> SExp
StringAtom (Err -> String
encodeErr Err
e))]
toSExp (AnnNamespace ns :: [Text]
ns file :: Maybe String
file) =
[(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp ([(SExp, SExp)] -> SExp) -> [(SExp, SExp)] -> SExp
forall a b. (a -> b) -> a -> b
$ [(String -> SExp
SymbolAtom "namespace", String -> SExp
StringAtom (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "." ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack [Text]
ns)))] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
[(String -> SExp
SymbolAtom "decor", String -> SExp
SymbolAtom (String -> SExp) -> String -> SExp
forall a b. (a -> b) -> a -> b
$ if Maybe String -> Bool
forall a. Maybe a -> Bool
isJust Maybe String
file then "module" else "namespace")] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
[(String, Maybe String)] -> [(SExp, SExp)]
forall a. SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
maybeProps [("source-file", Maybe String
file)]
toSExp AnnQuasiquote = [(SExp, Bool)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "quasiquotation", Bool
True)]
toSExp AnnAntiquote = [(SExp, Bool)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "antiquotation", Bool
True)]
toSExp (AnnSyntax c :: String
c) = [SExp] -> SExp
SexpList []
encodeName :: Name -> String
encodeName :: Name -> String
encodeName n :: Name
n = ByteString -> String
UTF8.toString (ByteString -> String) -> (Name -> ByteString) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Base64.encode (ByteString -> ByteString)
-> (Name -> ByteString) -> Name -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.toStrict (ByteString -> ByteString)
-> (Name -> ByteString) -> Name -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> ByteString
forall a. Binary a => a -> ByteString
Binary.encode (Name -> String) -> Name -> String
forall a b. (a -> b) -> a -> b
$ Name
n
encodeTerm :: [(Name, Bool)] -> Term -> String
encodeTerm :: [(Name, Bool)] -> TT Name -> String
encodeTerm bnd :: [(Name, Bool)]
bnd tm :: TT Name
tm = ByteString -> String
UTF8.toString (ByteString -> String)
-> (([(Name, Bool)], TT Name) -> ByteString)
-> ([(Name, Bool)], TT Name)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Base64.encode (ByteString -> ByteString)
-> (([(Name, Bool)], TT Name) -> ByteString)
-> ([(Name, Bool)], TT Name)
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.toStrict (ByteString -> ByteString)
-> (([(Name, Bool)], TT Name) -> ByteString)
-> ([(Name, Bool)], TT Name)
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Name, Bool)], TT Name) -> ByteString
forall a. Binary a => a -> ByteString
Binary.encode (([(Name, Bool)], TT Name) -> String)
-> ([(Name, Bool)], TT Name) -> String
forall a b. (a -> b) -> a -> b
$
([(Name, Bool)]
bnd, TT Name
tm)
decodeTerm :: String -> ([(Name, Bool)], Term)
decodeTerm :: String -> ([(Name, Bool)], TT Name)
decodeTerm = ByteString -> ([(Name, Bool)], TT Name)
forall a. Binary a => ByteString -> a
Binary.decode (ByteString -> ([(Name, Bool)], TT Name))
-> (String -> ByteString) -> String -> ([(Name, Bool)], TT Name)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.fromStrict (ByteString -> ByteString)
-> (String -> ByteString) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Base64.decodeLenient (ByteString -> ByteString)
-> (String -> ByteString) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
UTF8.fromString
encodeErr :: Err -> String
encodeErr :: Err -> String
encodeErr e :: Err
e = ByteString -> String
UTF8.toString (ByteString -> String) -> (Err -> ByteString) -> Err -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Base64.encode (ByteString -> ByteString)
-> (Err -> ByteString) -> Err -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.toStrict (ByteString -> ByteString)
-> (Err -> ByteString) -> Err -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> ByteString
forall a. Binary a => a -> ByteString
Binary.encode (Err -> String) -> Err -> String
forall a b. (a -> b) -> a -> b
$ Err
e
decodeErr :: String -> Err
decodeErr :: String -> Err
decodeErr = ByteString -> Err
forall a. Binary a => ByteString -> a
Binary.decode (ByteString -> Err) -> (String -> ByteString) -> String -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.fromStrict (ByteString -> ByteString)
-> (String -> ByteString) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Base64.decodeLenient (ByteString -> ByteString)
-> (String -> ByteString) -> String -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
UTF8.fromString
instance SExpable FC where
toSExp :: FC -> SExp
toSExp (FC f :: String
f (sl :: Int
sl, sc :: Int
sc) (el :: Int
el, ec :: Int
ec)) =
((SExp, SExp), (SExp, SExp, SExp), (SExp, SExp, SExp)) -> SExp
forall a. SExpable a => a -> SExp
toSExp ((String -> SExp
SymbolAtom "filename", String -> SExp
StringAtom String
f),
(String -> SExp
SymbolAtom "start", Integer -> SExp
IntegerAtom (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
sl), Integer -> SExp
IntegerAtom (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
sc)),
(String -> SExp
SymbolAtom "end", Integer -> SExp
IntegerAtom (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
el), Integer -> SExp
IntegerAtom (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
ec)))
toSExp NoFC = [String] -> SExp
forall a. SExpable a => a -> SExp
toSExp ([] :: [String])
toSExp (FileFC f :: String
f) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom "filename", String -> SExp
StringAtom String
f)]
escape :: String -> String
escape :: String -> String
escape = (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
escapeChar
where
escapeChar :: Char -> String
escapeChar '\\' = "\\\\"
escapeChar '"' = "\\\""
escapeChar c :: Char
c = [Char
c]
type Parser a = P.Parsec () String a
sexp :: Parser SExp
sexp :: Parser SExp
sexp = [SExp] -> SExp
SexpList ([SExp] -> SExp)
-> ParsecT () String Identity [SExp] -> Parser SExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT () String Identity Char
-> ParsecT () String Identity Char
-> ParsecT () String Identity [SExp]
-> ParsecT () String Identity [SExp]
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
P.between (Token String -> ParsecT () String Identity (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
'(') (Token String -> ParsecT () String Identity (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
')') (Parser SExp
sexp Parser SExp
-> ParsecT () String Identity Char
-> ParsecT () String Identity [SExp]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`P.sepBy` (Token String -> ParsecT () String Identity (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
' '))
Parser SExp -> Parser SExp -> Parser SExp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser SExp
atom
atom :: Parser SExp
atom :: Parser SExp
atom = [SExp] -> SExp
SexpList [] SExp -> ParsecT () String Identity String -> Parser SExp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String -> ParsecT () String Identity (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string Tokens String
"nil"
Parser SExp -> Parser SExp -> Parser SExp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token String -> ParsecT () String Identity (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
':' ParsecT () String Identity Char -> Parser SExp -> Parser SExp
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser SExp
atomC
Parser SExp -> Parser SExp -> Parser SExp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> SExp
StringAtom (String -> SExp)
-> ParsecT () String Identity String -> Parser SExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT () String Identity Char
-> ParsecT () String Identity Char
-> ParsecT () String Identity String
-> ParsecT () String Identity String
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
P.between (Token String -> ParsecT () String Identity (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
'"') (Token String -> ParsecT () String Identity (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
'"') (ParsecT () String Identity Char
-> ParsecT () String Identity String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many ParsecT () String Identity Char
quotedChar)
Parser SExp -> Parser SExp -> Parser SExp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String
ints <- ParsecT () String Identity Char
-> ParsecT () String Identity String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT () String Identity Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
P.digitChar
case ReadS Integer
forall a. (Eq a, Num a) => ReadS a
readDec String
ints of
((num :: Integer
num, ""):_) -> SExp -> Parser SExp
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> SExp
IntegerAtom (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
num))
_ -> SExp -> Parser SExp
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SExp
StringAtom String
ints)
atomC :: Parser SExp
atomC :: Parser SExp
atomC = Bool -> SExp
BoolAtom Bool
True SExp -> ParsecT () String Identity String -> Parser SExp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String -> ParsecT () String Identity (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string Tokens String
"True"
Parser SExp -> Parser SExp -> Parser SExp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> SExp
BoolAtom Bool
False SExp -> ParsecT () String Identity String -> Parser SExp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String -> ParsecT () String Identity (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string Tokens String
"False"
Parser SExp -> Parser SExp -> Parser SExp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> SExp
SymbolAtom (String -> SExp)
-> ParsecT () String Identity String -> Parser SExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT () String Identity Char
-> ParsecT () String Identity String
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ([Token String] -> ParsecT () String Identity (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.noneOf [Token String]
" \n\t\r\"()")
quotedChar :: Parser Char
quotedChar :: ParsecT () String Identity Char
quotedChar = ParsecT () String Identity Char -> ParsecT () String Identity Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ('\\' Char
-> ParsecT () String Identity String
-> ParsecT () String Identity Char
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String -> ParsecT () String Identity (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string Tokens String
"\\\\")
ParsecT () String Identity Char
-> ParsecT () String Identity Char
-> ParsecT () String Identity Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT () String Identity Char -> ParsecT () String Identity Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ('"' Char
-> ParsecT () String Identity String
-> ParsecT () String Identity Char
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String -> ParsecT () String Identity (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
P.string Tokens String
"\\\"")
ParsecT () String Identity Char
-> ParsecT () String Identity Char
-> ParsecT () String Identity Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> ParsecT () String Identity (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
P.noneOf [Token String]
"\""
data Opt = ShowImpl | ErrContext deriving Int -> Opt -> String -> String
[Opt] -> String -> String
Opt -> String
(Int -> Opt -> String -> String)
-> (Opt -> String) -> ([Opt] -> String -> String) -> Show Opt
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Opt] -> String -> String
$cshowList :: [Opt] -> String -> String
show :: Opt -> String
$cshow :: Opt -> String
showsPrec :: Int -> Opt -> String -> String
$cshowsPrec :: Int -> Opt -> String -> String
Show
data WhatDocs = Overview | Full
data IdeModeCommand = REPLCompletions String
| Interpret String
| TypeOf String
| CaseSplit Int String
| AddClause Int String
| AddProofClause Int String
| AddMissing Int String
| MakeWithBlock Int String
| MakeCaseBlock Int String
| ProofSearch Bool Int String [String] (Maybe Int)
| MakeLemma Int String
| LoadFile String (Maybe Int)
| DocsFor String WhatDocs
| Apropos String
| GetOpts
| SetOpt Opt Bool
| Metavariables Int
| WhoCalls String
| CallsWho String
| BrowseNS String
| TermNormalise [(Name, Bool)] Term
| TermShowImplicits [(Name, Bool)] Term
| TermNoImplicits [(Name, Bool)] Term
| TermElab [(Name, Bool)] Term
| PrintDef String
| ErrString Err
| ErrPPrint Err
| GetIdrisVersion
sexpToCommand :: SExp -> Maybe IdeModeCommand
sexpToCommand :: SExp -> Maybe IdeModeCommand
sexpToCommand (SexpList ([x :: SExp
x])) = SExp -> Maybe IdeModeCommand
sexpToCommand SExp
x
sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd :: String
cmd]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
Interpret String
cmd)
sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix :: String
prefix]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
REPLCompletions String
prefix)
sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename :: String
filename, IntegerAtom line :: Integer
line]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> Maybe Int -> IdeModeCommand
LoadFile String
filename (Int -> Maybe Int
forall a. a -> Maybe a
Just (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line)))
sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename :: String
filename]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> Maybe Int -> IdeModeCommand
LoadFile String
filename Maybe Int
forall a. Maybe a
Nothing)
sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
TypeOf String
name)
sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
CaseSplit (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
AddClause (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
AddProofClause (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
AddMissing (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
MakeWithBlock (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
MakeCaseBlock (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line :: Integer
line : StringAtom name :: String
name : rest :: [SExp]
rest))
| [] <- [SExp]
rest = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Bool -> Int -> String -> [String] -> Maybe Int -> IdeModeCommand
ProofSearch Bool
True (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name [] Maybe Int
forall a. Maybe a
Nothing)
| [SexpList hintexp :: [SExp]
hintexp] <- [SExp]
rest
, Just hints :: [String]
hints <- [SExp] -> Maybe [String]
getHints [SExp]
hintexp = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Bool -> Int -> String -> [String] -> Maybe Int -> IdeModeCommand
ProofSearch Bool
True (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name [String]
hints Maybe Int
forall a. Maybe a
Nothing)
| [SexpList hintexp :: [SExp]
hintexp, IntegerAtom depth :: Integer
depth] <- [SExp]
rest
, Just hints :: [String]
hints <- [SExp] -> Maybe [String]
getHints [SExp]
hintexp = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Bool -> Int -> String -> [String] -> Maybe Int -> IdeModeCommand
ProofSearch Bool
True (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name [String]
hints (Int -> Maybe Int
forall a. a -> Maybe a
Just (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
depth)))
where getHints :: [SExp] -> Maybe [String]
getHints = (SExp -> Maybe String) -> [SExp] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\h :: SExp
h -> case SExp
h of
StringAtom s :: String
s -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
_ -> Maybe String
forall a. Maybe a
Nothing)
sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line :: Integer
line, StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> String -> IdeModeCommand
MakeLemma (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name)
sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line :: Integer
line, StringAtom name :: String
name, StringAtom hint :: String
hint]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Bool -> Int -> String -> [String] -> Maybe Int -> IdeModeCommand
ProofSearch Bool
False (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
line) String
name [String
hint] Maybe Int
forall a. Maybe a
Nothing)
sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> WhatDocs -> IdeModeCommand
DocsFor String
name WhatDocs
Full)
sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name :: String
name, SymbolAtom s :: String
s])
| Just w :: WhatDocs
w <- String -> [(String, WhatDocs)] -> Maybe WhatDocs
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s [(String, WhatDocs)]
opts = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> WhatDocs -> IdeModeCommand
DocsFor String
name WhatDocs
w)
where opts :: [(String, WhatDocs)]
opts = [("overview", WhatDocs
Overview), ("full", WhatDocs
Full)]
sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search :: String
search]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
Apropos String
search)
sexpToCommand (SymbolAtom "get-options") = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just IdeModeCommand
GetOpts
sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s :: String
s, BoolAtom b :: Bool
b])
| Just opt :: Opt
opt <- String -> [(String, Opt)] -> Maybe Opt
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
s [(String, Opt)]
opts = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Opt -> Bool -> IdeModeCommand
SetOpt Opt
opt Bool
b)
where opts :: [(String, Opt)]
opts = [("show-implicits", Opt
ShowImpl), ("error-context", Opt
ErrContext)]
sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols :: Integer
cols]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (Int -> IdeModeCommand
Metavariables (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
cols))
sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
WhoCalls String
name)
sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
CallsWho String
name)
sexpToCommand (SexpList [SymbolAtom "browse-namespace", StringAtom ns :: String
ns]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
BrowseNS String
ns)
sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded :: String
encoded]) = let (bnd :: [(Name, Bool)]
bnd, tm :: TT Name
tm) = String -> ([(Name, Bool)], TT Name)
decodeTerm String
encoded in
IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just ([(Name, Bool)] -> TT Name -> IdeModeCommand
TermNormalise [(Name, Bool)]
bnd TT Name
tm)
sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded :: String
encoded]) = let (bnd :: [(Name, Bool)]
bnd, tm :: TT Name
tm) = String -> ([(Name, Bool)], TT Name)
decodeTerm String
encoded in
IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just ([(Name, Bool)] -> TT Name -> IdeModeCommand
TermShowImplicits [(Name, Bool)]
bnd TT Name
tm)
sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded :: String
encoded]) = let (bnd :: [(Name, Bool)]
bnd, tm :: TT Name
tm) = String -> ([(Name, Bool)], TT Name)
decodeTerm String
encoded in
IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just ([(Name, Bool)] -> TT Name -> IdeModeCommand
TermNoImplicits [(Name, Bool)]
bnd TT Name
tm)
sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded :: String
encoded]) = let (bnd :: [(Name, Bool)]
bnd, tm :: TT Name
tm) = String -> ([(Name, Bool)], TT Name)
decodeTerm String
encoded in
IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just ([(Name, Bool)] -> TT Name -> IdeModeCommand
TermElab [(Name, Bool)]
bnd TT Name
tm)
sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name :: String
name]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
PrintDef String
name)
sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded :: String
encoded]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (IdeModeCommand -> Maybe IdeModeCommand)
-> (String -> IdeModeCommand) -> String -> Maybe IdeModeCommand
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> IdeModeCommand
ErrString (Err -> IdeModeCommand)
-> (String -> Err) -> String -> IdeModeCommand
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
decodeErr (String -> Maybe IdeModeCommand) -> String -> Maybe IdeModeCommand
forall a b. (a -> b) -> a -> b
$ String
encoded
sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded :: String
encoded]) = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (IdeModeCommand -> Maybe IdeModeCommand)
-> (String -> IdeModeCommand) -> String -> Maybe IdeModeCommand
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> IdeModeCommand
ErrPPrint (Err -> IdeModeCommand)
-> (String -> Err) -> String -> IdeModeCommand
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
decodeErr (String -> Maybe IdeModeCommand) -> String -> Maybe IdeModeCommand
forall a b. (a -> b) -> a -> b
$ String
encoded
sexpToCommand (SymbolAtom "version") = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just IdeModeCommand
GetIdrisVersion
sexpToCommand _ = Maybe IdeModeCommand
forall a. Maybe a
Nothing
parseMessage :: String -> Either Err (SExp, Integer)
parseMessage :: String -> Either Err (SExp, Integer)
parseMessage x :: String
x = case String -> Either Err SExp
receiveString String
x of
Right (SexpList [cmd :: SExp
cmd, (IntegerAtom id :: Integer
id)]) -> (SExp, Integer) -> Either Err (SExp, Integer)
forall a b. b -> Either a b
Right (SExp
cmd, Integer
id)
Right x :: SExp
x -> Err -> Either Err (SExp, Integer)
forall a b. a -> Either a b
Left (Err -> Either Err (SExp, Integer))
-> (String -> Err) -> String -> Either Err (SExp, Integer)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Either Err (SExp, Integer))
-> String -> Either Err (SExp, Integer)
forall a b. (a -> b) -> a -> b
$ "Invalid message " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExp -> String
forall a. Show a => a -> String
show SExp
x
Left err :: Err
err -> Err -> Either Err (SExp, Integer)
forall a b. a -> Either a b
Left Err
err
receiveString :: String -> Either Err SExp
receiveString :: String -> Either Err SExp
receiveString = (ParseErrorBundle String () -> Err)
-> Either (ParseErrorBundle String ()) SExp -> Either Err SExp
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left (Err -> ParseErrorBundle String () -> Err
forall a b. a -> b -> a
const (Err -> ParseErrorBundle String () -> Err)
-> Err -> ParseErrorBundle String () -> Err
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg "parse failure") (Either (ParseErrorBundle String ()) SExp -> Either Err SExp)
-> (String -> Either (ParseErrorBundle String ()) SExp)
-> String
-> Either Err SExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser SExp
-> String -> String -> Either (ParseErrorBundle String ()) SExp
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
P.parse Parser SExp
sexp "(unknown)"
convSExp :: SExpable a => String -> a -> Integer -> String
convSExp :: String -> a -> Integer -> String
convSExp pre :: String
pre s :: a
s id :: Integer
id =
let sex :: SExp
sex = [SExp] -> SExp
SexpList [String -> SExp
SymbolAtom String
pre, a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
s, Integer -> SExp
IntegerAtom Integer
id] in
let str :: String
str = SExp -> String
sExpToString SExp
sex in
(String -> String
getHexLength String
str) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str
getHexLength :: String -> String
getHexLength :: String -> String
getHexLength s :: String
s = String -> Int -> String
forall r. PrintfType r => String -> r
printf "%06x" (1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s))
ideModeEpoch :: Int
ideModeEpoch :: Int
ideModeEpoch = 1