src/Idris/IdeMode.hs · Idris-dev

1{-|

2Module : Idris.IdeMode

3Description : Idris' IDE Mode

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

9

10{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

11

12module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where

13

14import Idris.Core.Binary ()

15import Idris.Core.TT

16

17import Control.Applicative hiding (Const)

18import qualified Data.Binary as Binary

19import qualified Data.ByteString.Base64 as Base64

20import qualified Data.ByteString.Lazy as Lazy

21import qualified Data.ByteString.UTF8 as UTF8

22import Data.List

23import Data.Maybe (isJust)

24import qualified Data.Text as T

25import Numeric

26import System.IO

27import Text.Printf

28import qualified Text.Trifecta as P

29import qualified Text.Trifecta.Delta as P

30

31getNChar :: Handle -> Int -> String -> IO (String)

32getNChar _ 0 s = return (reverse s)

33getNChar h n s = do c <- hGetChar h

34 getNChar h (n - 1) (c : s)

35

36getLen :: Handle -> IO (Either Err Int)

37getLen h = do s <- getNChar h 6 ""

38 case readHex s of

39 ((num, ""):_) -> return $ Right num

40 _ -> return $ Left . Msg $ "Couldn't read length " ++ s

41

42data SExp = SexpList [SExp]

43 | StringAtom String

44 | BoolAtom Bool

45 | IntegerAtom Integer

46 | SymbolAtom String

47 deriving ( Eq, Show )

48

49sExpToString :: SExp -> String

50sExpToString (StringAtom s) = "\"" ++ escape s ++ "\""

51sExpToString (BoolAtom True) = ":True"

52sExpToString (BoolAtom False) = ":False"

53sExpToString (IntegerAtom i) = printf "%d" i

54sExpToString (SymbolAtom s) = ":" ++ s

55sExpToString (SexpList l) = "(" ++ intercalate " " (map sExpToString l) ++ ")"

56

57class SExpable a where

58 toSExp :: a -> SExp

59

60instance SExpable SExp where

61 toSExp a = a

62

63instance SExpable Bool where

64 toSExp True = BoolAtom True

65 toSExp False = BoolAtom False

66

67instance SExpable String where

68 toSExp s = StringAtom s

69

70instance SExpable Integer where

71 toSExp n = IntegerAtom n

72

73instance SExpable Int where

74 toSExp n = IntegerAtom (toInteger n)

75

76

77instance SExpable Name where

78 toSExp s = StringAtom (show s)

79

80

81instance (SExpable a) => SExpable (Maybe a) where

82 toSExp Nothing = SexpList [SymbolAtom "Nothing"]

83 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]

84

85instance (SExpable a) => SExpable [a] where

86 toSExp l = SexpList (map toSExp l)

87

88instance (SExpable a, SExpable b) => SExpable (a, b) where

89 toSExp (l, r) = SexpList [toSExp l, toSExp r]

90

91instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where

92 toSExp (l, m, n) = SexpList [toSExp l, toSExp m, toSExp n]

93

94instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where

95 toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]

96

97instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>

98 SExpable (a, b, c, d, e) where

99 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]

100

101instance SExpable NameOutput where

102 toSExp TypeOutput = SymbolAtom "type"

103 toSExp FunOutput = SymbolAtom "function"

104 toSExp DataOutput = SymbolAtom "data"

105 toSExp MetavarOutput = SymbolAtom "metavar"

106 toSExp PostulateOutput = SymbolAtom "postulate"

107

108maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

109maybeProps [] = []

110maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps

111maybeProps ((n, Nothing):ps) = maybeProps ps

112

113constTy :: Const -> String

114constTy (I _) = "Int"

115constTy (BI _) = "Integer"

116constTy (Fl _) = "Double"

117constTy (Ch _) = "Char"

118constTy (Str _) = "String"

119constTy (B8 _) = "Bits8"

120constTy (B16 _) = "Bits16"

121constTy (B32 _) = "Bits32"

122constTy (B64 _) = "Bits64"

123constTy _ = "Type"

124

125namespaceOf :: Name -> Maybe String

126namespaceOf (NS _ ns) = Just (intercalate "." $ reverse (map T.unpack ns))

127namespaceOf _ = Nothing

128

129instance SExpable OutputAnnotation where

130 toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

131 (SymbolAtom "implicit", BoolAtom False),

132 (SymbolAtom "key", StringAtom (encodeName n))] ++

133 maybeProps [("decor", ty)] ++

134 maybeProps [("doc-overview", d), ("type", t)] ++

135 maybeProps [("namespace", namespaceOf n)]

136 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

137 (SymbolAtom "decor", SymbolAtom "bound"),

138 (SymbolAtom "implicit", BoolAtom imp)]

139 toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",

140 SymbolAtom (if constIsType c then "type" else "data")),

141 (SymbolAtom "type", StringAtom (constTy c)),

142 (SymbolAtom "doc-overview", StringAtom (constDocs c)),

143 (SymbolAtom "name", StringAtom (show c))]

144 toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),

145 (SymbolAtom "type", StringAtom ty),

146 (SymbolAtom "doc-overview", StringAtom doc)]

147 toSExp (AnnType name doc) = toSExp $ [(SymbolAtom "decor", SymbolAtom "type"),

148 (SymbolAtom "type", StringAtom "Type"),

149 (SymbolAtom "doc-overview", StringAtom doc)] ++

150 if not (null name) then [(SymbolAtom "name", StringAtom name)] else []

151 toSExp AnnKeyword = toSExp [(SymbolAtom "decor", SymbolAtom "keyword")]

152 toSExp (AnnFC fc) = toSExp [(SymbolAtom "source-loc", toSExp fc)]

153 toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]

154 where format = case fmt of

155 BoldText -> "bold"

156 ItalicText -> "italic"

157 UnderlineText -> "underline"

158 toSExp (AnnLink url) = toSExp [(SymbolAtom "link-href", StringAtom url)]

159 toSExp (AnnTerm bnd tm)

160 | termSmallerThan 1000 tm = toSExp [(SymbolAtom "tt-term", StringAtom (encodeTerm bnd tm))]

161 | otherwise = SexpList []

162 toSExp (AnnSearchResult ordr) = toSExp [(SymbolAtom "doc-overview",

163 StringAtom ("Result type is " ++ descr))]

164 where descr = case ordr of

165 EQ -> "isomorphic"

166 LT -> "more general than searched type"

167 GT -> "more specific than searched type"

168 toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]

169 toSExp (AnnNamespace ns file) =

170 toSExp $ [(SymbolAtom "namespace", StringAtom (intercalate "." (map T.unpack ns)))] ++

171 [(SymbolAtom "decor", SymbolAtom $ if isJust file then "module" else "namespace")] ++

172 maybeProps [("source-file", file)]

173 toSExp AnnQuasiquote = toSExp [(SymbolAtom "quasiquotation", True)]

174 toSExp AnnAntiquote = toSExp [(SymbolAtom "antiquotation", True)]

175 toSExp (AnnSyntax c) = SexpList []

176

177encodeName :: Name -> String

178encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

179

180encodeTerm :: [(Name, Bool)] -> Term -> String

181encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

182 (bnd, tm)

183

184decodeTerm :: String -> ([(Name, Bool)], Term)

185decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

186

187encodeErr :: Err -> String

188encodeErr e = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ e

189

190decodeErr :: String -> Err

191decodeErr = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

192

193instance SExpable FC where

194 toSExp (FC f (sl, sc) (el, ec)) =

195 toSExp ((SymbolAtom "filename", StringAtom f),

196 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

197 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))

198 toSExp NoFC = toSExp ([] :: [String])

199 toSExp (FileFC f) = toSExp [(SymbolAtom "filename", StringAtom f)]

200

201escape :: String -> String

202escape = concatMap escapeChar

203 where

204 escapeChar '\\' = "\\\\"

205 escapeChar '"' = "\\\""

206 escapeChar c = [c]

207

208pSExp = SexpList <$> P.between (P.char '(') (P.char ')') (pSExp `P.sepBy` (P.char ' '))

209 <|> atom

210

211atom = SexpList [] <$ P.string "nil"

212 <|> P.char ':' *> atomC

213 <|> StringAtom <$> P.between (P.char '"') (P.char '"') (P.many quotedChar)

214 <|> do ints <- some P.digit

215 case readDec ints of

216 ((num, ""):_) -> return (IntegerAtom (toInteger num))

217 _ -> return (StringAtom ints)

218

219atomC = BoolAtom True <$ P.string "True"

220 <|> BoolAtom False <$ P.string "False"

221 <|> SymbolAtom <$> many (P.noneOf " \n\t\r\"()")

222

223quotedChar = P.try ('\\' <$ P.string "\\\\")

224 <|> P.try ('"' <$ P.string "\\\"")

225 <|> P.noneOf "\""

226

227parseSExp :: String -> P.Result SExp

228parseSExp = P.parseString pSExp (P.Directed (UTF8.fromString "(unknown)") 0 0 0 0)

229

230data Opt = ShowImpl | ErrContext deriving Show

231

232data WhatDocs = Overview | Full

233

234data IdeModeCommand = REPLCompletions String

235 | Interpret String

236 | TypeOf String

237 | CaseSplit Int String

238 | AddClause Int String

239 | AddProofClause Int String

240 | AddMissing Int String

241 | MakeWithBlock Int String

242 | MakeCaseBlock Int String

243 | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

244 | MakeLemma Int String

245 | LoadFile String (Maybe Int)

246 | DocsFor String WhatDocs

247 | Apropos String

248 | GetOpts

249 | SetOpt Opt Bool

250 | Metavariables Int -- ^^ the Int is the column count for pretty-printing

251 | WhoCalls String

252 | CallsWho String

253 | BrowseNS String

254 | TermNormalise [(Name, Bool)] Term

255 | TermShowImplicits [(Name, Bool)] Term

256 | TermNoImplicits [(Name, Bool)] Term

257 | TermElab [(Name, Bool)] Term

258 | PrintDef String

259 | ErrString Err

260 | ErrPPrint Err

261 | GetIdrisVersion

262

263sexpToCommand :: SExp -> Maybe IdeModeCommand

264sexpToCommand (SexpList ([x])) = sexpToCommand x

265sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

266sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

267sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))

268sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)

269sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

270sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

271sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

272sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

273sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

274sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

275sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name]) = Just (MakeCaseBlock (fromInteger line) name)

276-- The Boolean in ProofSearch means "search recursively"

277-- If it's False, that means "refine", i.e. apply the name and fill in any

278-- arguments which can be done by unification.

279sexpToCommand (SexpList (SymbolAtom "proof-search" : IntegerAtom line : StringAtom name : rest))

280 | [] <- rest = Just (ProofSearch True (fromInteger line) name [] Nothing)

281 | [SexpList hintexp] <- rest

282 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints Nothing)

283 | [SexpList hintexp, IntegerAtom depth] <- rest

284 , Just hints <- getHints hintexp = Just (ProofSearch True (fromInteger line) name hints (Just (fromInteger depth)))

285 where getHints = mapM (\h -> case h of

286 StringAtom s -> Just s

287 _ -> Nothing)

288sexpToCommand (SexpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom name]) = Just (MakeLemma (fromInteger line) name)

289sexpToCommand (SexpList [SymbolAtom "refine", IntegerAtom line, StringAtom name, StringAtom hint]) = Just (ProofSearch False (fromInteger line) name [hint] Nothing)

290sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name Full)

291sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name, SymbolAtom s])

292 | Just w <- lookup s opts = Just (DocsFor name w)

293 where opts = [("overview", Overview), ("full", Full)]

294sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

295sexpToCommand (SymbolAtom "get-options") = Just GetOpts

296sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

297 | Just opt <- lookup s opts = Just (SetOpt opt b)

298 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

299sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

300sexpToCommand (SexpList [SymbolAtom "who-calls", StringAtom name]) = Just (WhoCalls name)

301sexpToCommand (SexpList [SymbolAtom "calls-who", StringAtom name]) = Just (CallsWho name)

302sexpToCommand (SexpList [SymbolAtom "browse-namespace", StringAtom ns]) = Just (BrowseNS ns)

303sexpToCommand (SexpList [SymbolAtom "normalise-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

304 Just (TermNormalise bnd tm)

305sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

306 Just (TermShowImplicits bnd tm)

307sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

308 Just (TermNoImplicits bnd tm)

309sexpToCommand (SexpList [SymbolAtom "elaborate-term", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

310 Just (TermElab bnd tm)

311sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

312sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded

313sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded

314sexpToCommand (SymbolAtom "version") = Just GetIdrisVersion

315sexpToCommand _ = Nothing

316

317parseMessage :: String -> Either Err (SExp, Integer)

318parseMessage x = case receiveString x of

319 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)

320 Right x -> Left . Msg $ "Invalid message " ++ show x

321 Left err -> Left err

322

323receiveString :: String -> Either Err SExp

324receiveString x =

325 case parseSExp x of

326 P.Failure _ -> Left . Msg $ "parse failure"

327 P.Success r -> Right r

328

329convSExp :: SExpable a => String -> a -> Integer -> String

330convSExp pre s id =

331 let sex = SexpList [SymbolAtom pre, toSExp s, IntegerAtom id] in

332 let str = sExpToString sex in

333 (getHexLength str) ++ str

334

335getHexLength :: String -> String

336getHexLength s = printf "%06x" (1 + (length s))

337

338-- | The version of the IDE mode command set. Increment this when you

339-- change it so clients can adapt.

340ideModeEpoch :: Int

341ideModeEpoch = 1