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