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