git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/src/Idris/IdeMode.hs
314 lines 16 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
5module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where
7import Text.Printf
8import Numeric
9import Data.List
10import qualified Data.Binary as Binary
11import qualified Data.ByteString.Base64 as Base64
12import qualified Data.ByteString.Lazy as Lazy
13import qualified Data.ByteString.UTF8 as UTF8
14-- import qualified Data.Text as T
15import Text.Trifecta hiding (Err)
16import Text.Trifecta.Delta
17import System.IO
19import Idris.Core.TT
20import Idris.Core.Binary
22import Control.Applicative hiding (Const)
24getNChar :: Handle -> Int -> String -> IO (String)
25getNChar _ 0 s = return (reverse s)
26getNChar h n s = do c <- hGetChar h
27 getNChar h (n - 1) (c : s)
29getLen :: Handle -> IO (Either Err Int)
30getLen h = do s <- getNChar h 6 ""
31 case readHex s of
32 ((num, ""):_) -> return $ Right num
33 _ -> return $ Left . Msg $ "Couldn't read length " ++ s
35data SExp = SexpList [SExp]
36 | StringAtom String
37 | BoolAtom Bool
38 | IntegerAtom Integer
39 | SymbolAtom String
40 deriving ( Eq, Show )
42sExpToString :: SExp -> String
43sExpToString (StringAtom s) = "\"" ++ escape s ++ "\""
44sExpToString (BoolAtom True) = ":True"
45sExpToString (BoolAtom False) = ":False"
46sExpToString (IntegerAtom i) = printf "%d" i
47sExpToString (SymbolAtom s) = ":" ++ s
48sExpToString (SexpList l) = "(" ++ intercalate " " (map sExpToString l) ++ ")"
50class SExpable a where
51 toSExp :: a -> SExp
53instance SExpable SExp where
54 toSExp a = a
56instance SExpable Bool where
57 toSExp True = BoolAtom True
58 toSExp False = BoolAtom False
60instance SExpable String where
61 toSExp s = StringAtom s
63instance SExpable Integer where
64 toSExp n = IntegerAtom n
66instance SExpable Int where
67 toSExp n = IntegerAtom (toInteger n)
70instance SExpable Name where
71 toSExp s = StringAtom (show s)
74instance (SExpable a) => SExpable (Maybe a) where
75 toSExp Nothing = SexpList [SymbolAtom "Nothing"]
76 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]
78instance (SExpable a) => SExpable [a] where
79 toSExp l = SexpList (map toSExp l)
81instance (SExpable a, SExpable b) => SExpable (a, b) where
82 toSExp (l, r) = SexpList [toSExp l, toSExp r]
84instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
85 toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n]
87instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
88 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
90instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>
91 SExpable (a, b, c, d, e) where
92 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
94instance SExpable NameOutput where
95 toSExp TypeOutput = SymbolAtom "type"
96 toSExp FunOutput = SymbolAtom "function"
97 toSExp DataOutput = SymbolAtom "data"
98 toSExp MetavarOutput = SymbolAtom "metavar"
99 toSExp PostulateOutput = SymbolAtom "postulate"
101maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
102maybeProps [] = []
103maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps
104maybeProps ((n, Nothing):ps) = maybeProps ps
106constTy :: Const -> String
107constTy (I _) = "Int"
108constTy (BI _) = "Integer"
109constTy (Fl _) = "Float"
110constTy (Ch _) = "Char"
111constTy (Str _) = "String"
112constTy (B8 _) = "Bits8"
113constTy (B16 _) = "Bits16"
114constTy (B32 _) = "Bits32"
115constTy (B64 _) = "Bits64"
116constTy (B8V _) = "Bits8x16"
117constTy (B16V _) = "Bits16x8"
118constTy (B32V _) = "Bits32x4"
119constTy (B64V _) = "Bits64x2"
120constTy _ = "Type"
122instance SExpable OutputAnnotation where
123 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
124 (SymbolAtom "implicit", BoolAtom False)] ++
125 maybeProps [("decor", ty)] ++
126 maybeProps [("doc-overview", d), ("type", t)]
127 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
128 (SymbolAtom "decor", SymbolAtom "bound"),
129 (SymbolAtom "implicit", BoolAtom imp)]
130 toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",
131 SymbolAtom (if constIsType c then "type" else "data")),
132 (SymbolAtom "type", StringAtom (constTy c)),
133 (SymbolAtom "doc-overview", StringAtom (constDocs c)),
134 (SymbolAtom "name", StringAtom (show c))]
135 toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),
136 (SymbolAtom "type", StringAtom ty),
137 (SymbolAtom "doc-overview", StringAtom doc)]
138 toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"),
139 (SymbolAtom "type", StringAtom "Type"),
140 (SymbolAtom "doc-overview", StringAtom doc)] ++
141 if not (null name) then [(SymbolAtom "name", StringAtom name)] else []
142 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]
143 toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)]
144 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]
145 where format = case fmt of
146 BoldText -> "bold"
147 ItalicText -> "italic"
148 UnderlineText -> "underline"
149 toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
150 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
151 StringAtom ("Result type is " ++ descr))]
152 where descr = case ordr of
153 EQ -> "isomorphic"
154 LT -> "more general than searched type"
155 GT -> "more specific than searched type"
156 toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]
158encodeTerm :: [(Name, Bool)] -> Term -> String
159encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
160 (bnd, tm)
162decodeTerm :: String -> ([(Name, Bool)], Term)
163decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
165encodeErr :: Err -> String
166encodeErr e = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ e
168decodeErr :: String -> Err
169decodeErr = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
171instance SExpable FC where
172 toSExp (FC f (sl, sc) (el, ec)) =
173 toSExp ((SymbolAtom "filename", StringAtom f),
174 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),
175 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))
177escape :: String -> String
178escape = concatMap escapeChar
179 where
180 escapeChar '\\' = "\\\\"
181 escapeChar '"' = "\\\""
182 escapeChar c = [c]
184pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
185 return (SexpList xs)
186 <|> atom
188atom = do string "nil"; return (SexpList [])
189 <|> do char ':'; x <- atomC; return x
190 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
191 <|> do ints <- some digit
192 case readDec ints of
193 ((num, ""):_) -> return (IntegerAtom (toInteger num))
194 _ -> return (StringAtom ints)
196atomC = do string "True"; return (BoolAtom True)
197 <|> do string "False"; return (BoolAtom False)
198 <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
200quotedChar = try (string "\\\\" >> return '\\')
201 <|> try (string "\\\"" >> return '"')
202 <|> noneOf "\""
204parseSExp :: String -> Result SExp
205parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
207data Opt = ShowImpl | ErrContext deriving Show
209data WhatDocs = Overview | Full
211data IdeModeCommand = REPLCompletions String
212 | Interpret String
213 | TypeOf String
214 | CaseSplit Int String
215 | AddClause Int String
216 | AddProofClause Int String
217 | AddMissing Int String
218 | MakeWithBlock Int String
219 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
220 | MakeLemma Int String
221 | LoadFile String (Maybe Int)
222 | DocsFor String WhatDocs
223 | Apropos String
224 | GetOpts
225 | SetOpt Opt Bool
226 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
227 | WhoCalls String
228 | CallsWho String
229 | TermNormalise [(Name, Bool)] Term
230 | TermShowImplicits [(Name, Bool)] Term
231 | TermNoImplicits [(Name, Bool)] Term
232 | TermElab [(Name, Bool)] Term
233 | PrintDef String
234 | ErrString Err
235 | ErrPPrint Err
236 | GetIdrisVersion
238sexpToCommand :: SExp -> Maybe IdeModeCommand
239sexpToCommand (SexpList (x:[])) = sexpToCommand x
240sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
241sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
242sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))
243sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)
244sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
245sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
246sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
247sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
248sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
249sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
250-- The Boolean in ProofSearch means "search recursively"
251-- If it's False, that means "refine", i.e. apply the name and fill in any
252-- arguments which can be done by unification.
253sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))
254 | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)
255 | [SexpList hintexp] <- rest
256 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)
257 | [SexpList hintexp, IntegerAtom depth] <- rest
258 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))
259 where getHints = mapM (\h -> case h of
260 StringAtom s -> Just s
261 _ -> Nothing)
262sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)
263sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)
264sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name Full)
265sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])
266 | Just w <- lookup s opts = Just (DocsFor name w)
267 where opts = [("overview", Overview), ("full", Full)]
268sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
269sexpToCommand (SymbolAtom "get-options") = Just GetOpts
270sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
271 | Just opt <- lookup s opts = Just (SetOpt opt b)
272 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
273sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
274sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
275sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
276sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
277 Just (TermNormalise bnd tm)
278sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
279 Just (TermShowImplicits bnd tm)
280sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
281 Just (TermNoImplicits bnd tm)
282sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
283 Just (TermElab bnd tm)
284sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
285sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
286sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded
287sexpToCommand (SymbolAtom "version") = Just GetIdrisVersion
288sexpToCommand _ = Nothing
290parseMessage :: String -> Either Err (SExp, Integer)
291parseMessage x = case receiveString x of
292 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
293 Right x -> Left . Msg $ "Invalid message " ++ show x
294 Left err -> Left err
296receiveString :: String -> Either Err SExp
297receiveString x =
298 case parseSExp x of
299 Failure _ -> Left . Msg $ "parse failure"
300 Success r -> Right r
302convSExp :: SExpable a => String -> a -> Integer -> String
303convSExp pre s id =
304 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
305 let str = sExpToString sex in
306 (getHexLength str) ++ str
308getHexLength :: String -> String
309getHexLength s = printf "%06x" (1 + (length s))
311-- | The version of the IDE mode command set. Increment this when you
312-- change it so clients can adapt.
313ideModeEpoch :: Int
314ideModeEpoch = 1