git.iko.soy/Idris-dev
on e63fcef help sign in
Idris-dev/src/Idris/IdeSlave.hs
155 lines 6.2 kB history raw
1{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
3module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable) 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]
72escape :: String -> String
73escape = concatMap escapeChar
74 where
75 escapeChar '\\' = "\\\\"
76 escapeChar '"' = "\\\""
77 escapeChar c = [c]
79pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))
80 return (SexpList xs)
81 <|> atom
83atom = do string "nil"; return (SexpList [])
84 <|> do char ':'; x <- atomC; return x
85 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)
86 <|> do ints <- some digit
87 case readDec ints of
88 ((num, ""):_) -> return (IntegerAtom (toInteger num))
89 _ -> return (StringAtom ints)
91atomC = do string "True"; return (BoolAtom True)
92 <|> do string "False"; return (BoolAtom False)
93 <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs)
95quotedChar = try (string "\\\\" >> return '\\')
96 <|> try (string "\\\"" >> return '"')
97 <|> noneOf "\""
99parseSExp :: String -> Result SExp
100parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
102data IdeSlaveCommand = REPLCompletions String
103 | Interpret String
104 | TypeOf String
105 | CaseSplit Int String
106 | AddClause Int String
107 | AddProofClause Int String
108 | AddMissing Int String
109 | MakeWithBlock Int String
110 | ProofSearch Int String [String]
111 | LoadFile String
112 deriving Show
114sexpToCommand :: SExp -> Maybe IdeSlaveCommand
115sexpToCommand (SexpList (x:[])) = sexpToCommand x
116sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)
117sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)
118sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)
119sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)
120sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)
121sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)
122sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)
123sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)
124sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)
125sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch (fromInteger line) name hints)
126 where getHints = mapM (\h -> case h of
127 StringAtom s -> Just s
128 _ -> Nothing)
129sexpToCommand _ = Nothing
131parseMessage :: String -> Either Err (SExp, Integer)
132parseMessage x = case receiveString x of
133 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)
134 Left err -> Left err
136receiveString :: String -> Either Err SExp
137receiveString x =
138 case readHex (take 6 x) of
139 ((num, ""):_) ->
140 let msg = drop 6 x in
141 if (length msg) /= (num - 1)
142 then Left . Msg $ "bad input length"
143 else (case parseSExp msg of
144 Failure _ -> Left . Msg $ "parse failure"
145 Success r -> Right r)
146 _ -> Left . Msg $ "readHex failed"
148convSExp :: SExpable a => String -> a -> Integer -> String
149convSExp pre s id =
150 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in
151 let str = sExpToString sex in
152 (getHexLength str) ++ str
154getHexLength :: String -> String
155getHexLength s = printf "%06x" (1 + (length s))