659e985 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add IDESlave support to :makelemma

659e985David Raymond Christiansen12 years ago

src/Idris/IdeSlave.hs+2

compare with master

unifiedsplit

@@ -172,6 +172,7 @@ data IdeSlaveCommand = REPLCompletions String

172 | AddMissing Int String

173 | MakeWithBlock Int String

174 | ProofSearch Bool Int String [String]

175+ | MakeLemma Int String

175 | LoadFile String

176 | LoadFile String

176 | DocsFor String

177 | DocsFor String

177 | Apropos String

178 | Apropos String

@@ -199,6 +200,7 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

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

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

200 StringAtom s -> Just s

201 StringAtom s -> Just s

201 _ -> Nothing)

202 _ -> Nothing)

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

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

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

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

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

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

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

src/Idris/Interactive.hs+22−5

@@ -15,6 +15,7 @@ import Idris.ElabDecls

15import Idris.Error

16import Idris.Delaborate

17import Idris.Output

18+import Idris.IdeSlave hiding (IdeSlaveCommand(..))

19import Util.Pretty

20import Util.Pretty

20import Util.System

21import Util.System

@@ -23,6 +24,7 @@ import System.FilePath

23import System.Directory

24import System.Directory

24import System.IO

25import System.IO

25import Data.Char

26import Data.Char

27+import Data.Maybe (fromMaybe)

28caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

30caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

@@ -254,15 +256,32 @@ makeLemma h fn updatefile l n

254 do let fb = fn ++ "~"

256 do let fb = fn ++ "~"

255 runIO $ writeFile fb (addLem before tyline lem lem_app later)

257 runIO $ writeFile fb (addLem before tyline lem lem_app later)

256 runIO $ copyFile fb fn

258 runIO $ copyFile fb fn

259+ else case idris_outputmode i of

257− else ihPrintResult h $ lem ++ "\n" ++ lem_app

260+ RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app

261+ IdeSlave n ->

262+ let good = SexpList [SymbolAtom "ok",

263+ SexpList [SymbolAtom "metavariable-lemma",

264+ SexpList [SymbolAtom "replace-metavariable",

265+ StringAtom lem_app],

266+ SexpList [SymbolAtom "definition-type",

267+ StringAtom lem]]]

268+ in runIO . hPutStrLn h $ convSExp "return" good n

269+

258 else do -- provisional definition

270 else do -- provisional definition

259− let lem_app = show n ++ appArgs [] mty ++

271+ let lem_app = show n ++ appArgs [] mty ++

260 " = ?" ++ show n ++ "_rhs"

272 " = ?" ++ show n ++ "_rhs"

261 if updatefile then

273 if updatefile then

262 do let fb = fn ++ "~"

274 do let fb = fn ++ "~"

263 runIO $ writeFile fb (addProv before tyline lem_app later)

275 runIO $ writeFile fb (addProv before tyline lem_app later)

264 runIO $ copyFile fb fn

276 runIO $ copyFile fb fn

277+ else case idris_outputmode i of

265− else ihPrintResult h $ lem_app

278+ RawOutput -> ihPrintResult h $ lem_app

279+ IdeSlave n ->

280+ let good = SexpList [SymbolAtom "ok",

281+ SexpList [SymbolAtom "provisional-definition-lemma",

282+ SexpList [SymbolAtom "definition-clause",

283+ StringAtom lem_app]]]

284+ in runIO . hPutStrLn h $ convSExp "return" good n

266

285

267 where getIndent s = length (takeWhile isSpace s)

286 where getIndent s = length (takeWhile isSpace s)

268

287

@@ -318,5 +337,3 @@ makeLemma h fn updatefile l n

318 unlines $ before ++ tyline :

337 unlines $ before ++ tyline :

319 (later_bef ++ [blankline, lem_app, blankline] ++

338 (later_bef ++ [blankline, lem_app, blankline] ++

320 later_end)

339 later_end)

321−

322−

src/Idris/REPL.hs+4

@@ -295,6 +295,10 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

295 process stdout fn (MakeWith False line (sUN name))

296runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints) =

297 process stdout fn (DoProofSearch False r line (sUN name) (map sUN hints))

298+runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

299+ case splitName name of

300+ Left err -> iPrintError err

301+ Right n -> process stdout fn (MakeLemma False line n)

298runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

302runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

299 process stdout fn (Apropos a)

303 process stdout fn (Apropos a)

300runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

304runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =