git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/src/Idris/IdeMode.hs
310 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 _ = "Type"
118instance SExpable OutputAnnotation where
119 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
120 (SymbolAtom "implicit", BoolAtom False)] ++
121 maybeProps [("decor", ty)] ++
122 maybeProps [("doc-overview", d), ("type", t)]
123 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
124 (SymbolAtom "decor", SymbolAtom "bound"),
125 (SymbolAtom "implicit", BoolAtom imp)]
126 toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",
127 SymbolAtom (if constIsType c then "type" else "data")),
128 (SymbolAtom "type", StringAtom (constTy c)),
129 (SymbolAtom "doc-overview", StringAtom (constDocs c)),
130 (SymbolAtom "name", StringAtom (show c))]
131 toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),
132 (SymbolAtom "type", StringAtom ty),
133 (SymbolAtom "doc-overview", StringAtom doc)]
134 toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"),
135 (SymbolAtom "type", StringAtom "Type"),
136 (SymbolAtom "doc-overview", StringAtom doc)] ++
137 if not (null name) then [(SymbolAtom "name", StringAtom name)] else []
138 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]
139 toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)]
140 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]
141 where format = case fmt of
142 BoldText -> "bold"
143 ItalicText -> "italic"
144 UnderlineText -> "underline"
145 toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]
146 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",
147 StringAtom ("Result type is " ++ descr))]
148 where descr = case ordr of
149 EQ -> "isomorphic"
150 LT -> "more general than searched type"
151 GT -> "more specific than searched type"
152 toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]
154encodeTerm :: [(Name, Bool)] -> Term -> String
155encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $
156 (bnd, tm)
158decodeTerm :: String -> ([(Name, Bool)], Term)
159decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
161encodeErr :: Err -> String
162encodeErr e = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ e
164decodeErr :: String -> Err
165decodeErr = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString
167instance SExpable FC where
168 toSExp (FC f (sl, sc) (el, ec)) =
169 toSExp ((SymbolAtom "filename", StringAtom f),
170 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),
171 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))
173escape :: String -> String
174escape = concatMap escapeChar
175 where
176 escapeChar '\\' = "\\\\"
177 escapeChar '"' = "\\\""
178 escapeChar c = [c]
180pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
181 return (SexpList xs)
182 <|> atom
184atom = do string "nil"; return (SexpList [])
185 <|> do char ':'; x <- atomC; return x
186 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
187 <|> do ints <- some digit
188 case readDec ints of
189 ((num, ""):_) -> return (IntegerAtom (toInteger num))
190 _ -> return (StringAtom ints)
192atomC = do string "True"; return (BoolAtom True)
193 <|> do string "False"; return (BoolAtom False)
194 <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
196quotedChar = try (string "\\\\" >> return '\\')
197 <|> try (string "\\\"" >> return '"')
198 <|> noneOf "\""
200parseSExp :: String -> Result SExp
201parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
203data Opt = ShowImpl | ErrContext deriving Show
205data WhatDocs = Overview | Full
207data IdeModeCommand = REPLCompletions String
208 | Interpret String
209 | TypeOf String
210 | CaseSplit Int String
211 | AddClause Int String
212 | AddProofClause Int String
213 | AddMissing Int String
214 | MakeWithBlock Int String
215 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
216 | MakeLemma Int String
217 | LoadFile String (Maybe Int)
218 | DocsFor String WhatDocs
219 | Apropos String
220 | GetOpts
221 | SetOpt Opt Bool
222 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
223 | WhoCalls String
224 | CallsWho String
225 | TermNormalise [(Name, Bool)] Term
226 | TermShowImplicits [(Name, Bool)] Term
227 | TermNoImplicits [(Name, Bool)] Term
228 | TermElab [(Name, Bool)] Term
229 | PrintDef String
230 | ErrString Err
231 | ErrPPrint Err
232 | GetIdrisVersion
234sexpToCommand :: SExp -> Maybe IdeModeCommand
235sexpToCommand (SexpList (x:[])) = sexpToCommand x
236sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
237sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
238sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))
239sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)
240sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
241sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
242sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
243sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
244sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
245sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
246-- The Boolean in ProofSearch means "search recursively"
247-- If it's False, that means "refine", i.e. apply the name and fill in any
248-- arguments which can be done by unification.
249sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))
250 | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)
251 | [SexpList hintexp] <- rest
252 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)
253 | [SexpList hintexp, IntegerAtom depth] <- rest
254 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))
255 where getHints = mapM (\h -> case h of
256 StringAtom s -> Just s
257 _ -> Nothing)
258sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)
259sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)
260sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name Full)
261sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])
262 | Just w <- lookup s opts = Just (DocsFor name w)
263 where opts = [("overview", Overview), ("full", Full)]
264sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
265sexpToCommand (SymbolAtom "get-options") = Just GetOpts
266sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
267 | Just opt <- lookup s opts = Just (SetOpt opt b)
268 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
269sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
270sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
271sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
272sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
273 Just (TermNormalise bnd tm)
274sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
275 Just (TermShowImplicits bnd tm)
276sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
277 Just (TermNoImplicits bnd tm)
278sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
279 Just (TermElab bnd tm)
280sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
281sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
282sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded
283sexpToCommand (SymbolAtom "version") = Just GetIdrisVersion
284sexpToCommand _ = Nothing
286parseMessage :: String -> Either Err (SExp, Integer)
287parseMessage x = case receiveString x of
288 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
289 Right x -> Left . Msg $ "Invalid message " ++ show x
290 Left err -> Left err
292receiveString :: String -> Either Err SExp
293receiveString x =
294 case parseSExp x of
295 Failure _ -> Left . Msg $ "parse failure"
296 Success r -> Right r
298convSExp :: SExpable a => String -> a -> Integer -> String
299convSExp pre s id =
300 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
301 let str = sExpToString sex in
302 (getHexLength str) ++ str
304getHexLength :: String -> String
305getHexLength s = printf "%06x" (1 + (length s))
307-- | The version of the IDE mode command set. Increment this when you
308-- change it so clients can adapt.
309ideModeEpoch :: Int
310ideModeEpoch = 1