git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/IdeSlave.hs
289 lines 14 kB history raw
1{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
3module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where
5import Text.Printf
6import Numeric
7import Data.List
8import qualified Data.Binary as Binary
9import qualified Data.ByteString.Base64 as Base64
10import qualified Data.ByteString.Lazy as Lazy
11import qualified Data.ByteString.UTF8 as UTF8
12-- import qualified Data.Text as T
13import Text.Trifecta hiding (Err)
14import Text.Trifecta.Delta
15import System.IO
17import Idris.Core.TT
18import Idris.Core.Binary
20import Control.Applicative hiding (Const)
22getNChar :: Handle -> Int -> String -> IO (String)
23getNChar _ 0 s = return (reverse s)
24getNChar h n s = do c <- hGetChar h
25 getNChar h (n - 1) (c : s)
27getLen :: Handle -> IO (Either Err Int)
28getLen h = do s <- getNChar h 6 ""
29 case readHex s of
30 ((num, ""):_) -> return $ Right num
31 _ -> return $ Left . Msg $ "Couldn't read length " ++ s
33data SExp = SexpList [SExp]
34 | StringAtom String
35 | BoolAtom Bool
36 | IntegerAtom Integer
37 | SymbolAtom String
38 deriving ( Eq, Show )
40sExpToString :: SExp -> String
41sExpToString (StringAtom s) = "\"" ++ escape s ++ "\""
42sExpToString (BoolAtom True) = ":True"
43sExpToString (BoolAtom False) = ":False"
44sExpToString (IntegerAtom i) = printf "%d" i
45sExpToString (SymbolAtom s) = ":" ++ s
46sExpToString (SexpList l) = "(" ++ intercalate " " (map sExpToString l) ++ ")"
48class SExpable a where
49 toSExp :: a -> SExp
51instance SExpable SExp where
52 toSExp a = a
54instance SExpable Bool where
55 toSExp True = BoolAtom True
56 toSExp False = BoolAtom False
58instance SExpable String where
59 toSExp s = StringAtom s
61instance SExpable Integer where
62 toSExp n = IntegerAtom n
64instance SExpable Int where
65 toSExp n = IntegerAtom (toInteger n)
68instance SExpable Name where
69 toSExp s = StringAtom (show s)
72instance (SExpable a) => SExpable (Maybe a) where
73 toSExp Nothing = SexpList [SymbolAtom "Nothing"]
74 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]
76instance (SExpable a) => SExpable [a] where
77 toSExp l = SexpList (map toSExp l)
79instance (SExpable a, SExpable b) => SExpable (a, b) where
80 toSExp (l, r) = SexpList [toSExp l, toSExp r]
82instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
83 toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n]
85instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
86 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
88instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>
89 SExpable (a, b, c, d, e) where
90 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
92instance SExpable NameOutput where
93 toSExp TypeOutput = SymbolAtom "type"
94 toSExp FunOutput = SymbolAtom "function"
95 toSExp DataOutput = SymbolAtom "data"
96 toSExp MetavarOutput = SymbolAtom "metavar"
97 toSExp PostulateOutput = SymbolAtom "postulate"
99maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
100maybeProps [] = []
101maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps
102maybeProps ((n, Nothing):ps) = maybeProps ps
104constTy :: Const -> String
105constTy (I _) = "Int"
106constTy (BI _) = "Integer"
107constTy (Fl _) = "Float"
108constTy (Ch _) = "Char"
109constTy (Str _) = "String"
110constTy (B8 _) = "Bits8"
111constTy (B16 _) = "Bits16"
112constTy (B32 _) = "Bits32"
113constTy (B64 _) = "Bits64"
114constTy (B8V _) = "Bits8x16"
115constTy (B16V _) = "Bits16x8"
116constTy (B32V _) = "Bits32x4"
117constTy (B64V _) = "Bits64x2"
118constTy _ = "Type"
120instance SExpable OutputAnnotation where
121 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
122 (SymbolAtom "implicit", BoolAtom False)] ++
123 maybeProps [("decor", ty)] ++
124 maybeProps [("doc-overview", d), ("type", t)]
125 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
126 (SymbolAtom "decor", SymbolAtom "bound"),
127 (SymbolAtom "implicit", BoolAtom imp)]
128 toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",
129 SymbolAtom (if constIsType c then "type" else "data")),
130 (SymbolAtom "type", StringAtom (constTy c)),
131 (SymbolAtom "doc-overview", StringAtom (constDocs c)),
132 (SymbolAtom "name", StringAtom (show c))]
133 toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),
134 (SymbolAtom "type", StringAtom ty),
135 (SymbolAtom "doc-overview", StringAtom doc)]
136 toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"),
137 (SymbolAtom "type", StringAtom "Type"),
138 (SymbolAtom "doc-overview", StringAtom doc)] ++
139 if not (null name) then [(SymbolAtom "name", StringAtom name)] else []
140 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]
141 toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)]
142 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]
143 where format = case fmt of
144 BoldText -> "bold"
145 ItalicText -> "italic"
146 UnderlineText -> "underline"
147 toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
148 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
149 StringAtom ("Result type is " ++ descr))]
150 where descr = case ordr of
151 EQ -> "isomorphic"
152 LT -> "more general than searched type"
153 GT -> "more specific than searched type"
155encodeTerm :: [(Name, Bool)] -> Term -> String
156encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
157 (bnd, tm)
159decodeTerm :: String -> ([(Name, Bool)], Term)
160decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
162instance SExpable FC where
163 toSExp (FC f (sl, sc) (el, ec)) =
164 toSExp ((SymbolAtom "filename", StringAtom f),
165 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),
166 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))
168escape :: String -> String
169escape = concatMap escapeChar
170 where
171 escapeChar '\\' = "\\\\"
172 escapeChar '"' = "\\\""
173 escapeChar c = [c]
175pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
176 return (SexpList xs)
177 <|> atom
179atom = do string "nil"; return (SexpList [])
180 <|> do char ':'; x <- atomC; return x
181 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
182 <|> do ints <- some digit
183 case readDec ints of
184 ((num, ""):_) -> return (IntegerAtom (toInteger num))
185 _ -> return (StringAtom ints)
187atomC = do string "True"; return (BoolAtom True)
188 <|> do string "False"; return (BoolAtom False)
189 <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
191quotedChar = try (string "\\\\" >> return '\\')
192 <|> try (string "\\\"" >> return '"')
193 <|> noneOf "\""
195parseSExp :: String -> Result SExp
196parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
198data Opt = ShowImpl | ErrContext deriving Show
200data IdeSlaveCommand = REPLCompletions String
201 | Interpret String
202 | TypeOf String
203 | CaseSplit Int String
204 | AddClause Int String
205 | AddProofClause Int String
206 | AddMissing Int String
207 | MakeWithBlock Int String
208 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
209 | MakeLemma Int String
210 | LoadFile String (Maybe Int)
211 | DocsFor String
212 | Apropos String
213 | GetOpts
214 | SetOpt Opt Bool
215 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
216 | WhoCalls String
217 | CallsWho String
218 | TermNormalise [(Name, Bool)] Term
219 | TermShowImplicits [(Name, Bool)] Term
220 | TermNoImplicits [(Name, Bool)] Term
221 | PrintDef String
223sexpToCommand :: SExp -> Maybe IdeSlaveCommand
224sexpToCommand (SexpList (x:[])) = sexpToCommand x
225sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
226sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
227sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))
228sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)
229sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
230sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
231sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
232sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
233sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
234sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
235-- The Boolean in ProofSearch means "search recursively"
236-- If it's False, that means "refine", i.e. apply the name and fill in any
237-- arguments which can be done by unification.
238sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))
239 | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)
240 | [SexpList hintexp] <- rest
241 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)
242 | [SexpList hintexp, IntegerAtom depth] <- rest
243 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))
244 where getHints = mapM (\h -> case h of
245 StringAtom s -> Just s
246 _ -> Nothing)
247sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)
248sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)
249sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
250sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
251sexpToCommand (SymbolAtom "get-options") = Just GetOpts
252sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
253 | Just opt <- lookup s opts = Just (SetOpt opt b)
254 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more options. Issue #1611 in the Issue tracker. https://github.com/idris-lang/Idris-dev/issues/1611
255sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
256sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
257sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
258sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
259 Just (TermNormalise bnd tm)
260sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
261 Just (TermShowImplicits bnd tm)
262sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
263 Just (TermNoImplicits bnd tm)
264sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
265sexpToCommand _ = Nothing
267parseMessage :: String -> Either Err (SExp, Integer)
268parseMessage x = case receiveString x of
269 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
270 Right x -> Left . Msg $ "Invalid message " ++ show x
271 Left err -> Left err
273receiveString :: String -> Either Err SExp
274receiveString x =
275 case parseSExp x of
276 Failure _ -> Left . Msg $ "parse failure"
277 Success r -> Right r
279convSExp :: SExpable a => String -> a -> Integer -> String
280convSExp pre s id =
281 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
282 let str = sExpToString sex in
283 (getHexLength str) ++ str
285getHexLength :: String -> String
286getHexLength s = printf "%06x" (1 + (length s))
288ideSlaveEpoch :: Int
289ideSlaveEpoch = 1