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