git.iko.soy/Idris-dev
on 8697358 help sign in
Idris-dev/src/Idris/IdeMode.hs
306 lines 15 kB history raw
1{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
5module Idris.IdeMode(parseMessage, convSExp, 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 IdeModeCommand = REPLCompletions String
210 | Interpret String
211 | TypeOf String
212 | CaseSplit Int String
213 | AddClause Int String
214 | AddProofClause Int String
215 | AddMissing Int String
216 | MakeWithBlock Int String
217 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth
218 | MakeLemma Int String
219 | LoadFile String (Maybe Int)
220 | DocsFor String
221 | Apropos String
222 | GetOpts
223 | SetOpt Opt Bool
224 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
225 | WhoCalls String
226 | CallsWho String
227 | TermNormalise [(Name, Bool)] Term
228 | TermShowImplicits [(Name, Bool)] Term
229 | TermNoImplicits [(Name, Bool)] Term
230 | PrintDef String
231 | ErrString Err
232 | ErrPPrint Err
233 | GetIdrisVersion
235sexpToCommand :: SExp -> Maybe IdeModeCommand
236sexpToCommand (SexpList (x:[])) = sexpToCommand x
237sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
238sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
239sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))
240sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)
241sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
242sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
243sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
244sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
245sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
246sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
247-- The Boolean in ProofSearch means "search recursively"
248-- If it's False, that means "refine", i.e. apply the name and fill in any
249-- arguments which can be done by unification.
250sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))
251 | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)
252 | [SexpList hintexp] <- rest
253 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)
254 | [SexpList hintexp, IntegerAtom depth] <- rest
255 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))
256 where getHints = mapM (\h -> case h of
257 StringAtom s -> Just s
258 _ -> Nothing)
259sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)
260sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)
261sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
262sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
263sexpToCommand (SymbolAtom "get-options") = Just GetOpts
264sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
265 | Just opt <- lookup s opts = Just (SetOpt opt b)
266 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
267sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
268sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
269sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
270sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
271 Just (TermNormalise bnd tm)
272sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
273 Just (TermShowImplicits bnd tm)
274sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in
275 Just (TermNoImplicits bnd tm)
276sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)
277sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded
278sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded
279sexpToCommand (SymbolAtom "version") = Just GetIdrisVersion
280sexpToCommand _ = Nothing
282parseMessage :: String -> Either Err (SExp, Integer)
283parseMessage x = case receiveString x of
284 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
285 Right x -> Left . Msg $ "Invalid message " ++ show x
286 Left err -> Left err
288receiveString :: String -> Either Err SExp
289receiveString x =
290 case parseSExp x of
291 Failure _ -> Left . Msg $ "parse failure"
292 Success r -> Right r
294convSExp :: SExpable a => String -> a -> Integer -> String
295convSExp pre s id =
296 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
297 let str = sExpToString sex in
298 (getHexLength str) ++ str
300getHexLength :: String -> String
301getHexLength s = printf "%06x" (1 + (length s))
303-- | The version of the IDE mode command set. Increment this when you
304-- change it so clients can adapt.
305ideModeEpoch :: Int
306ideModeEpoch = 1