git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/IdeSlave.hs
212 lines 10 kB history raw
1{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
3module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..)) where
5import Text.Printf
6import Numeric
7import Data.List
8import qualified Data.ByteString.UTF8 as UTF8
9-- import qualified Data.Text as T
10import Text.Trifecta hiding (Err)
11import Text.Trifecta.Delta
13import Idris.Core.TT
15import Control.Applicative
17data SExp = SexpList [SExp]
18 | StringAtom String
19 | BoolAtom Bool
20 | IntegerAtom Integer
21 | SymbolAtom String
22 deriving ( Eq, Show )
24sExpToString :: SExp -> String
25sExpToString (StringAtom s) = "\"" ++ escape s ++ "\""
26sExpToString (BoolAtom True) = ":True"
27sExpToString (BoolAtom False) = ":False"
28sExpToString (IntegerAtom i) = printf "%d" i
29sExpToString (SymbolAtom s) = ":" ++ s
30sExpToString (SexpList l) = "(" ++ intercalate " " (map sExpToString l) ++ ")"
32class SExpable a where
33 toSExp :: a -> SExp
35instance SExpable SExp where
36 toSExp a = a
38instance SExpable Bool where
39 toSExp True = BoolAtom True
40 toSExp False = BoolAtom False
42instance SExpable String where
43 toSExp s = StringAtom s
45instance SExpable Integer where
46 toSExp n = IntegerAtom n
48instance SExpable Int where
49 toSExp n = IntegerAtom (toInteger n)
52instance SExpable Name where
53 toSExp s = StringAtom (show s)
56instance (SExpable a) => SExpable (Maybe a) where
57 toSExp Nothing = SexpList [SymbolAtom "Nothing"]
58 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]
60instance (SExpable a) => SExpable [a] where
61 toSExp l = SexpList (map toSExp l)
63instance (SExpable a, SExpable b) => SExpable (a, b) where
64 toSExp (l, r) = SexpList [toSExp l, toSExp r]
66instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
67 toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n]
69instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
70 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
72instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>
73 SExpable (a, b, c, d, e) where
74 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
76instance SExpable NameOutput where
77 toSExp TypeOutput = SymbolAtom "type"
78 toSExp FunOutput = SymbolAtom "function"
79 toSExp DataOutput = SymbolAtom "data"
80 toSExp MetavarOutput = SymbolAtom "metavar"
82maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
83maybeProps [] = []
84maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps
85maybeProps ((n, Nothing):ps) = maybeProps ps
87instance SExpable OutputAnnotation where
88 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),
89 (SymbolAtom "implicit", BoolAtom False)] ++
90 maybeProps [("decor", ty)] ++
91 maybeProps [("doc-overview", d), ("type", t)]
92 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),
93 (SymbolAtom "decor", SymbolAtom "bound"),
94 (SymbolAtom "implicit", BoolAtom imp)]
95 toSExp AnnConstData = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
96 toSExp AnnConstType = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
97 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]
98 toSExp (AnnFC (FC f (sl, sc) (el, ec))) = toSExp [(SymbolAtom "source-loc",
99 ((SymbolAtom "filename", StringAtom f),
100 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),
101 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))))]
102 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]
103 where format = case fmt of
104 BoldText -> "bold"
105 ItalicText -> "italic"
106 UnderlineText -> "underline"
108escape :: String -> String
109escape = concatMap escapeChar
110 where
111 escapeChar '\\' = "\\\\"
112 escapeChar '"' = "\\\""
113 escapeChar c = [c]
115pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
116 return (SexpList xs)
117 <|> atom
119atom = do string "nil"; return (SexpList [])
120 <|> do char ':'; x <- atomC; return x
121 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
122 <|> do ints <- some digit
123 case readDec ints of
124 ((num, ""):_) -> return (IntegerAtom (toInteger num))
125 _ -> return (StringAtom ints)
127atomC = do string "True"; return (BoolAtom True)
128 <|> do string "False"; return (BoolAtom False)
129 <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
131quotedChar = try (string "\\\\" >> return '\\')
132 <|> try (string "\\\"" >> return '"')
133 <|> noneOf "\""
135parseSExp :: String -> Result SExp
136parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
138data Opt = ShowImpl | ErrContext deriving Show
140data IdeSlaveCommand = REPLCompletions String
141 | Interpret String
142 | TypeOf String
143 | CaseSplit Int String
144 | AddClause Int String
145 | AddProofClause Int String
146 | AddMissing Int String
147 | MakeWithBlock Int String
148 | ProofSearch Bool Int String [String]
149 | LoadFile String
150 | DocsFor String
151 | Apropos String
152 | GetOpts
153 | SetOpt Opt Bool
154 | Metavariables Int -- ^^ the Int is the column count for pretty-printing
155 | WhoCalls String
156 | CallsWho String
158sexpToCommand :: SExp -> Maybe IdeSlaveCommand
159sexpToCommand (SexpList (x:[])) = sexpToCommand x
160sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
161sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
162sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)
163sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
164sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
165sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
166sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
167sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
168sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
169-- The Boolean in ProofSearch means "search recursively"
170-- If it's False, that means "refine", i.e. apply the name and fill in any
171-- arguments which can be done by unification.
172sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints)
173 where getHints = mapM (\h -> case h of
174 StringAtom s -> Just s
175 _ -> Nothing)
176sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint])
177sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
178sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)
179sexpToCommand (SymbolAtom "get-options") = Just GetOpts
180sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])
181 | Just opt <- lookup s opts = Just (SetOpt opt b)
182 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more
183sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))
184sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)
185sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)
186sexpToCommand _ = Nothing
188parseMessage :: String -> Either Err (SExp, Integer)
189parseMessage x = case receiveString x of
190 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
191 Left err -> Left err
193receiveString :: String -> Either Err SExp
194receiveString x =
195 case readHex (take 6 x) of
196 ((num, ""):_) ->
197 let msg = drop 6 x in
198 if (length msg) /= (num - 1)
199 then Left . Msg $ "bad input length"
200 else (case parseSExp msg of
201 Failure _ -> Left . Msg $ "parse failure"
202 Success r -> Right r)
203 _ -> Left . Msg $ "readHex failed"
205convSExp :: SExpable a => String -> a -> Integer -> String
206convSExp pre s id =
207 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
208 let str = sExpToString sex in
209 (getHexLength str) ++ str
211getHexLength :: String -> String
212getHexLength s = printf "%06x" (1 + (length s))