{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-} module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..)) where import Text.Printf import Numeric import Data.List import qualified Data.Binary as Binary import qualified Data.ByteString.Base64 as Base64 import qualified Data.ByteString.Lazy as Lazy import qualified Data.ByteString.UTF8 as UTF8 -- import qualified Data.Text as T import Text.Trifecta hiding (Err) import Text.Trifecta.Delta import Idris.Core.TT import Idris.Core.Binary import Control.Applicative hiding (Const) data SExp = SexpList [SExp] | StringAtom String | BoolAtom Bool | IntegerAtom Integer | SymbolAtom String deriving ( Eq, Show ) sExpToString :: SExp -> String sExpToString (StringAtom s) = "\"" ++ escape s ++ "\"" sExpToString (BoolAtom True) = ":True" sExpToString (BoolAtom False) = ":False" sExpToString (IntegerAtom i) = printf "%d" i sExpToString (SymbolAtom s) = ":" ++ s sExpToString (SexpList l) = "(" ++ intercalate " " (map sExpToString l) ++ ")" class SExpable a where toSExp :: a -> SExp instance SExpable SExp where toSExp a = a instance SExpable Bool where toSExp True = BoolAtom True toSExp False = BoolAtom False instance SExpable String where toSExp s = StringAtom s instance SExpable Integer where toSExp n = IntegerAtom n instance SExpable Int where toSExp n = IntegerAtom (toInteger n) instance SExpable Name where toSExp s = StringAtom (show s) instance (SExpable a) => SExpable (Maybe a) where toSExp Nothing = SexpList [SymbolAtom "Nothing"] toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a] instance (SExpable a) => SExpable [a] where toSExp l = SexpList (map toSExp l) instance (SExpable a, SExpable b) => SExpable (a, b) where toSExp (l, r) = SexpList [toSExp l, toSExp r] instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n] instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o] instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) => SExpable (a, b, c, d, e) where toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p] instance SExpable NameOutput where toSExp TypeOutput = SymbolAtom "type" toSExp FunOutput = SymbolAtom "function" toSExp DataOutput = SymbolAtom "data" toSExp MetavarOutput = SymbolAtom "metavar" toSExp PostulateOutput = SymbolAtom "postulate" maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)] maybeProps [] = [] maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps maybeProps ((n, Nothing):ps) = maybeProps ps constTy :: Const -> String constTy (I _) = "Int" constTy (BI _) = "Integer" constTy (Fl _) = "Float" constTy (Ch _) = "Char" constTy (Str _) = "String" constTy (B8 _) = "Bits8" constTy (B16 _) = "Bits16" constTy (B32 _) = "Bits32" constTy (B64 _) = "Bits64" constTy (B8V _) = "Bits8x16" constTy (B16V _) = "Bits16x8" constTy (B32V _) = "Bits32x4" constTy (B64V _) = "Bits64x2" constTy _ = "Type" instance SExpable OutputAnnotation where toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)), (SymbolAtom "implicit", BoolAtom False)] ++ maybeProps [("decor", ty)] ++ maybeProps [("doc-overview", d), ("type", t)] toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)), (SymbolAtom "decor", SymbolAtom "bound"), (SymbolAtom "implicit", BoolAtom imp)] toSExp (AnnConst c) = toSExp [(SymbolAtom "decor", SymbolAtom (if constIsType c then "type" else "data")), (SymbolAtom "type", StringAtom (constTy c)), (SymbolAtom "doc-overview", StringAtom (constDocs c)), (SymbolAtom "name", StringAtom (show c))] toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"), (SymbolAtom "type", StringAtom ty), (SymbolAtom "doc-overview", StringAtom doc)] toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"), (SymbolAtom "type", StringAtom "Type"), (SymbolAtom "doc-overview", StringAtom doc)] ++ if not (null name) then [(SymbolAtom "name", StringAtom name)] else [] toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")] toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)] toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)] where format = case fmt of BoldText -> "bold" ItalicText -> "italic" UnderlineText -> "underline" toSExp (AnnTerm bnd tm) = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))] encodeTerm :: [(Name, Bool)] -> Term -> String encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ (bnd, tm) decodeTerm :: String -> ([(Name, Bool)], Term) decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString instance SExpable FC where toSExp (FC f (sl, sc) (el, ec)) = toSExp ((SymbolAtom "filename", StringAtom f), (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)), (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))) escape :: String -> String escape = concatMap escapeChar where escapeChar '\\' = "\\\\" escapeChar '"' = "\\\"" escapeChar c = [c] pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' ')) return (SexpList xs) <|> atom atom = do string "nil"; return (SexpList []) <|> do char ':'; x <- atomC; return x <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs) <|> do ints <- some digit case readDec ints of ((num, ""):_) -> return (IntegerAtom (toInteger num)) _ -> return (StringAtom ints) atomC = do string "True"; return (BoolAtom True) <|> do string "False"; return (BoolAtom False) <|> do xs <- many (noneOf " \n\t\r\"()"); return (SymbolAtom xs) quotedChar = try (string "\\\\" >> return '\\') <|> try (string "\\\"" >> return '"') <|> noneOf "\"" parseSExp :: String -> Result SExp parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0) data Opt = ShowImpl | ErrContext deriving Show data IdeSlaveCommand = REPLCompletions String | Interpret String | TypeOf String | CaseSplit Int String | AddClause Int String | AddProofClause Int String | AddMissing Int String | MakeWithBlock Int String | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth | MakeLemma Int String | LoadFile String (Maybe Int) | DocsFor String | Apropos String | GetOpts | SetOpt Opt Bool | Metavariables Int -- ^^ the Int is the column count for pretty-printing | WhoCalls String | CallsWho String | TermNormalise [(Name, Bool)] Term | TermShowImplicits [(Name, Bool)] Term | TermNoImplicits [(Name, Bool)] Term sexpToCommand :: SExp -> Maybe IdeSlaveCommand sexpToCommand (SexpList (x:[])) = sexpToCommand x sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd) sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix) sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line))) sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing) sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name) sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name) sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name) sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name) sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name) sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name) -- The Boolean in ProofSearch means "search recursively" -- If it's False, that means "refine", i.e. apply the name and fill in any -- arguments which can be done by unification. sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest)) | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing) | [SexpList hintexp] <- rest , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing) | [SexpList hintexp, IntegerAtom depth] <- rest , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth))) where getHints = mapM (\h -> case h of StringAtom s -> Just s _ -> Nothing) sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name) sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing) sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name) sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search) sexpToCommand (SymbolAtom "get-options") = Just GetOpts sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b]) | Just opt <- lookup s opts = Just (SetOpt opt b) where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols)) sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name) sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name) sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in Just (TermNormalise bnd tm) sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in Just (TermShowImplicits bnd tm) sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in Just (TermNoImplicits bnd tm) sexpToCommand _ = Nothing parseMessage :: String -> Either Err (SExp, Integer) parseMessage x = case receiveString x of Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id) Left err -> Left err receiveString :: String -> Either Err SExp receiveString x = case readHex (take 6 x) of ((num, ""):_) -> let msg = drop 6 x in if (length msg) /= (num - 1) then Left . Msg $ "bad input length" else (case parseSExp msg of Failure _ -> Left . Msg $ "parse failure" Success r -> Right r) _ -> Left . Msg $ "readHex failed" convSExp :: SExpable a => String -> a -> Integer -> String convSExp pre s id = let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in let str = sExpToString sex in (getHexLength str) ++ str getHexLength :: String -> String getHexLength s = printf "%06x" (1 + (length s))