git.iko.soy/Idris-dev
on 7d42ba2 help sign in
Idris-dev/src/Idris/IdeMode.hs
311 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 | PrintDef String
233 | ErrString Err
234 | ErrPPrint Err
235 | GetIdrisVersion
237sexpToCommand :: SExp -> Maybe IdeModeCommand
238sexpToCommand (SexpList (x:[])) = sexpToCommand x
239sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
240sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
241sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))
242sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)
243sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
244sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
245sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
246sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
247sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
248sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
249-- The Boolean in ProofSearch means "search recursively"
250-- If it's False, that means "refine", i.e. apply the name and fill in any
251-- arguments which can be done by unification.
252sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))
253 | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)
254 | [SexpList hintexp] <- rest
255 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)
256 | [SexpList hintexp, IntegerAtom depth] <- rest
257 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))
258 where getHints = mapM (\h -> case h of
259 StringAtom s -> Just s
260 _ -> Nothing)
261sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)
262sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)
263sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name Full)
264sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])
265 | Just w <- lookup s opts = Just (DocsFor name w)
266 where opts = [("overview", Overview), ("full", Full)]
267sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
268sexpToCommand (SymbolAtom "get-options") = Just GetOpts
269sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
270 | Just opt <- lookup s opts = Just (SetOpt opt b)
271 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
272sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
273sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
274sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
275sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
276 Just (TermNormalise bnd tm)
277sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
278 Just (TermShowImplicits bnd tm)
279sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
280 Just (TermNoImplicits bnd tm)
281sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
282sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
283sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded
284sexpToCommand (SymbolAtom "version") = Just GetIdrisVersion
285sexpToCommand _ = Nothing
287parseMessage :: String -> Either Err (SExp, Integer)
288parseMessage x = case receiveString x of
289 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
290 Right x -> Left . Msg $ "Invalid message " ++ show x
291 Left err -> Left err
293receiveString :: String -> Either Err SExp
294receiveString x =
295 case parseSExp x of
296 Failure _ -> Left . Msg $ "parse failure"
297 Success r -> Right r
299convSExp :: SExpable a => String -> a -> Integer -> String
300convSExp pre s id =
301 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
302 let str = sExpToString sex in
303 (getHexLength str) ++ str
305getHexLength :: String -> String
306getHexLength s = printf "%06x" (1 + (length s))
308-- | The version of the IDE mode command set. Increment this when you
309-- change it so clients can adapt.
310ideModeEpoch :: Int
311ideModeEpoch = 1