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