{-|
Module      : Idris.IdeMode
Description : Idris' IDE Mode

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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 = String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
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 Handle
h = do String
s <- Handle -> Int -> String -> IO String
getNChar Handle
h Int
6 String
""
              case ReadS Int
forall a. (Eq a, Num a) => ReadS a
readHex String
s of
                ((Int
num, String
""):[(Int, String)]
_) -> Either Err Int -> IO (Either Err Int)
forall a. a -> IO a
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
                [(Int, String)]
_             -> Either Err Int -> IO (Either Err Int)
forall a. a -> IO a
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
$ String
"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
$c== :: SExp -> SExp -> Bool
== :: SExp -> SExp -> Bool
$c/= :: SExp -> SExp -> Bool
/= :: 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
$cshowsPrec :: Int -> SExp -> String -> String
showsPrec :: Int -> SExp -> String -> String
$cshow :: SExp -> String
show :: SExp -> String
$cshowList :: [SExp] -> String -> String
showList :: [SExp] -> String -> String
Show )

sExpToString :: SExp -> String
sExpToString :: SExp -> String
sExpToString (StringAtom String
s)   = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
escape String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
sExpToString (BoolAtom Bool
True)  = String
":True"
sExpToString (BoolAtom Bool
False) = String
":False"
sExpToString (IntegerAtom Integer
i)  = String -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"%d" Integer
i
sExpToString (SymbolAtom String
s)   = String
":" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
sExpToString (SexpList [SExp]
l)     = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" " ((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]
++ 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 (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)


instance SExpable Name where
  toSExp :: Name -> SExp
toSExp 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 Maybe a
Nothing  = [SExp] -> SExp
SexpList [String -> SExp
SymbolAtom String
"Nothing"]
  toSExp (Just a
a) = [SExp] -> SExp
SexpList [String -> SExp
SymbolAtom String
"Just", a -> SExp
forall a. SExpable a => a -> SExp
toSExp a
a]

instance (SExpable a) => SExpable [a] where
  toSExp :: [a] -> SExp
toSExp [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 (a
l, 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 (a
l, b
m, 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 (a
l, b
m, c
n, 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 (a
l, b
m, c
n, d
o, 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 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, 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 ((String
n, Maybe a
Nothing):[(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
_) = 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) = String -> Maybe String
forall a. a -> Maybe a
Just (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ([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 Name
_         = Maybe String
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) = [(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 String
"name", String -> SExp
StringAtom (Name -> String
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))] [(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 [(String
"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 [(String
"doc-overview", Maybe String
d), (String
"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 [(String
"namespace", Name -> Maybe String
namespaceOf Name
n)]
  toSExp (AnnBoundName Name
n Bool
imp)    = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom String
"name", String -> SExp
StringAtom (Name -> String
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)            = [(SExp, SExp)] -> SExp
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 (Const -> String
forall a. Show a => a -> String
show Const
c))]
  toSExp (AnnData String
ty String
doc)        = [(SExp, SExp)] -> SExp
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)      = [(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 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)] [(SExp, SExp)] -> [(SExp, SExp)] -> [(SExp, SExp)]
forall a. [a] -> [a] -> [a]
++
                                             if Bool -> Bool
not (String -> Bool
forall a. [a] -> Bool
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              = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom String
"decor", String -> SExp
SymbolAtom String
"keyword")]
  toSExp (AnnFC FC
fc)      = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom String
"source-loc", FC -> SExp
forall a. SExpable a => a -> SExp
toSExp FC
fc)]
  toSExp (AnnTextFmt TextFormatting
fmt) = [(SExp, SExp)] -> SExp
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) = [(SExp, SExp)] -> SExp
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 = [(SExp, SExp)] -> SExp
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) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom String
"doc-overview",
      String -> SExp
StringAtom (String
"Result type is " String -> String -> String
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) = [(SExp, SExp)] -> SExp
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) =
    [(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 String
"namespace", String -> SExp
StringAtom (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ((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 String
"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 String
"module" else String
"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 [(String
"source-file", Maybe String
file)]
  toSExp OutputAnnotation
AnnQuasiquote = [(SExp, Bool)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom String
"quasiquotation", Bool
True)]
  toSExp OutputAnnotation
AnnAntiquote = [(SExp, Bool)] -> SExp
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 (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)] -> Term -> String
encodeTerm [(Name, Bool)]
bnd Term
tm = ByteString -> String
UTF8.toString (ByteString -> String)
-> (([(Name, Bool)], Term) -> ByteString)
-> ([(Name, Bool)], Term)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Base64.encode (ByteString -> ByteString)
-> (([(Name, Bool)], Term) -> ByteString)
-> ([(Name, Bool)], Term)
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
Lazy.toStrict (ByteString -> ByteString)
-> (([(Name, Bool)], Term) -> ByteString)
-> ([(Name, Bool)], Term)
-> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Name, Bool)], Term) -> ByteString
forall a. Binary a => a -> ByteString
Binary.encode (([(Name, Bool)], Term) -> String)
-> ([(Name, Bool)], Term) -> String
forall a b. (a -> b) -> a -> b
$
                    ([(Name, Bool)]
bnd, Term
tm)

decodeTerm :: String -> ([(Name, Bool)], Term)
decodeTerm :: String -> ([(Name, Bool)], Term)
decodeTerm = ByteString -> ([(Name, Bool)], Term)
forall a. Binary a => ByteString -> a
Binary.decode (ByteString -> ([(Name, Bool)], Term))
-> (String -> ByteString) -> String -> ([(Name, Bool)], Term)
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 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 String
f (Int
sl, Int
sc) (Int
el, Int
ec)) =
    ((SExp, SExp), (SExp, SExp, SExp), (SExp, SExp, SExp)) -> SExp
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 (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 String
"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 FC
NoFC = [String] -> SExp
forall a. SExpable a => a -> SExp
toSExp ([] :: [String])
  toSExp (FileFC String
f) = [(SExp, SExp)] -> SExp
forall a. SExpable a => a -> SExp
toSExp [(String -> SExp
SymbolAtom String
"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 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 ([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 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 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 Char
Token String
' '))
    Parser SExp -> Parser SExp -> Parser SExp
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
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 (Tokens String) -> Parser SExp
forall a b.
a -> ParsecT () String Identity b -> ParsecT () String Identity a
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 String
Tokens String
"nil"
   Parser SExp -> Parser SExp -> Parser SExp
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
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 Char
Token String
':' ParsecT () String Identity Char -> Parser SExp -> Parser SExp
forall a b.
ParsecT () String Identity a
-> ParsecT () String Identity b -> ParsecT () String Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser SExp
atomC
   Parser SExp -> Parser SExp -> Parser SExp
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
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 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 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 a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String
ints <- ParsecT () String Identity Char
-> ParsecT () String Identity String
forall a.
ParsecT () String Identity a -> ParsecT () String Identity [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT () String Identity Char
ParsecT () String Identity (Token String)
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
            ((Integer
num, String
""):[(Integer, String)]
_) -> SExp -> Parser SExp
forall a. a -> ParsecT () String Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> SExp
IntegerAtom (Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
num))
            [(Integer, String)]
_ -> SExp -> Parser SExp
forall a. a -> ParsecT () String Identity a
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 (Tokens String) -> Parser SExp
forall a b.
a -> ParsecT () String Identity b -> ParsecT () String Identity a
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 String
Tokens String
"True"
    Parser SExp -> Parser SExp -> Parser SExp
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> SExp
BoolAtom Bool
False SExp -> ParsecT () String Identity (Tokens String) -> Parser SExp
forall a b.
a -> ParsecT () String Identity b -> ParsecT () String Identity a
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 String
Tokens String
"False"
    Parser SExp -> Parser SExp -> Parser SExp
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
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 a.
ParsecT () String Identity a -> ParsecT () String Identity [a]
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 String
[Token String]
" \n\t\r\"()")

quotedChar :: Parser Char
quotedChar :: ParsecT () String Identity Char
quotedChar = ParsecT () String Identity Char -> ParsecT () String Identity Char
forall a.
ParsecT () String Identity a -> ParsecT () String Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char
'\\' Char
-> ParsecT () String Identity (Tokens String)
-> ParsecT () String Identity Char
forall a b.
a -> ParsecT () String Identity b -> ParsecT () String Identity a
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 String
Tokens String
"\\\\")
         ParsecT () String Identity Char
-> ParsecT () String Identity Char
-> ParsecT () String Identity Char
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT () String Identity Char -> ParsecT () String Identity Char
forall a.
ParsecT () String Identity a -> ParsecT () String Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char
'"' Char
-> ParsecT () String Identity (Tokens String)
-> ParsecT () String Identity Char
forall a b.
a -> ParsecT () String Identity b -> ParsecT () String Identity a
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 String
Tokens String
"\\\"")
         ParsecT () String Identity Char
-> ParsecT () String Identity Char
-> ParsecT () String Identity Char
forall a.
ParsecT () String Identity a
-> ParsecT () String Identity a -> ParsecT () String Identity a
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 String
[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
$cshowsPrec :: Int -> Opt -> String -> String
showsPrec :: Int -> Opt -> String -> String
$cshow :: Opt -> String
show :: Opt -> String
$cshowList :: [Opt] -> String -> String
showList :: [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) -- ^^ Recursive?, line, name, hints, depth
                    | MakeLemma Int String
                    | LoadFile String (Maybe Int)
                    | DocsFor String WhatDocs
                    | Apropos String
                    | GetOpts
                    | SetOpt Opt Bool
                    | Metavariables Int -- ^^ the Int is the column count for pretty-printing
                    | 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])                           = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
Interpret String
cmd)
sexpToCommand (SexpList [SymbolAtom String
"repl-completions", StringAtom String
prefix])                 = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
REPLCompletions String
prefix)
sexpToCommand (SexpList [SymbolAtom String
"load-file", StringAtom String
filename, IntegerAtom 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 String
"load-file", StringAtom 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 String
"type-of", StringAtom String
name])                            = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
TypeOf String
name)
sexpToCommand (SexpList [SymbolAtom String
"case-split", IntegerAtom Integer
line, StringAtom 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 String
"add-clause", IntegerAtom Integer
line, StringAtom 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 String
"add-proof-clause", IntegerAtom Integer
line, StringAtom 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 String
"add-missing", IntegerAtom Integer
line, StringAtom 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 String
"make-with", IntegerAtom Integer
line, StringAtom 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 String
"make-case", IntegerAtom Integer
line, StringAtom 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)
-- The Boolean in ProofSearch means "search recursively"
-- If it's False, that means "refine", i.e. apply the name and fill in any
-- arguments which can be done by unification.
sexpToCommand (SexpList (SymbolAtom String
"proof-search" : IntegerAtom Integer
line : StringAtom String
name : [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 [SExp]
hintexp] <- [SExp]
rest
  ,  Just [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 [SExp]
hintexp, IntegerAtom Integer
depth] <- [SExp]
rest
 , Just [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\SExp
h -> case SExp
h of
                                StringAtom String
s -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
                                SExp
_            -> Maybe String
forall a. Maybe a
Nothing)
sexpToCommand (SexpList [SymbolAtom String
"make-lemma", IntegerAtom Integer
line, StringAtom 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 String
"refine", IntegerAtom Integer
line, StringAtom String
name, StringAtom 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 String
"docs-for", StringAtom String
name])                       = IdeModeCommand -> Maybe IdeModeCommand
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 <- 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 = [(String
"overview", WhatDocs
Overview), (String
"full", WhatDocs
Full)]
sexpToCommand (SexpList [SymbolAtom String
"apropos", StringAtom String
search])                      = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
Apropos String
search)
sexpToCommand (SymbolAtom String
"get-options")                                                = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just IdeModeCommand
GetOpts
sexpToCommand (SexpList [SymbolAtom String
"set-option", SymbolAtom String
s, BoolAtom Bool
b])
  | Just 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 = [(String
"show-implicits", Opt
ShowImpl), (String
"error-context", Opt
ErrContext)] --TODO support more options. Issue #1611 in the Issue tracker. https://github.com/idris-lang/Idris-dev/issues/1611
sexpToCommand (SexpList [SymbolAtom String
"metavariables", IntegerAtom 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 String
"who-calls", StringAtom String
name])                      = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
WhoCalls String
name)
sexpToCommand (SexpList [SymbolAtom String
"calls-who", StringAtom String
name])                      = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
CallsWho String
name)
sexpToCommand (SexpList [SymbolAtom String
"browse-namespace", StringAtom String
ns])                 = IdeModeCommand -> Maybe IdeModeCommand
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
                                                                                          IdeModeCommand -> Maybe IdeModeCommand
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
                                                                                          IdeModeCommand -> Maybe IdeModeCommand
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
                                                                                          IdeModeCommand -> Maybe IdeModeCommand
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
                                                                                          IdeModeCommand -> Maybe IdeModeCommand
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])               = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just (String -> IdeModeCommand
PrintDef String
name)
sexpToCommand (SexpList [SymbolAtom String
"error-string", StringAtom 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 String
"error-pprint", StringAtom 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 String
"version")                                                    = IdeModeCommand -> Maybe IdeModeCommand
forall a. a -> Maybe a
Just IdeModeCommand
GetIdrisVersion
sexpToCommand SExp
_                                                                         = Maybe IdeModeCommand
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)]) -> (SExp, Integer) -> Either Err (SExp, Integer)
forall a b. b -> Either a b
Right (SExp
cmd, Integer
id)
                   Right 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
$ String
"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 -> 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 b c d. (b -> c) -> Either b d -> Either c d
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 String
"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 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, 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 String
s = String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"%06x" (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s))

-- | The version of the IDE mode command set. Increment this when you
-- change it so clients can adapt.
ideModeEpoch :: Int
ideModeEpoch :: Int
ideModeEpoch = Int
1