d581842 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1228 from david-christiansen/ideslave-makelemma

Add IDESlave support to :makelemma

commitd581842d1fafd6c02a07ffe467bc1449a7401b26 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 14 May 2014, 12:59 (12 years ago) parentf53580a 659e985

3 files changed+28−5

compare with master

unifiedsplit

src/Idris/IdeSlave.hs+2 src/Idris/Interactive.hs+22−5 src/Idris/REPL.hs+4

src/Idris/IdeSlave.hs+2

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

172172 | AddMissing Int String

173173 | MakeWithBlock Int String

174174 | ProofSearch Bool Int String [String]

175+ | MakeLemma Int String

175176 | LoadFile String

176177 | DocsFor String

177178 | Apropos String

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

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

200201 StringAtom s -> Just s

201202 _ -> Nothing)

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

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

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

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

src/Idris/Interactive.hs+22−5

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

1515import Idris.Error

1616import Idris.Delaborate

1717import Idris.Output

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

1819

1920import Util.Pretty

2021import Util.System

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

2324import System.Directory

2425import System.IO

2526import Data.Char

27+import Data.Maybe (fromMaybe)

2628

2729

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

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

254256 do let fb = fn ++ "~"

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

256258 runIO $ copyFile fb fn

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

259+ else case idris_outputmode i of

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+

258270 else do -- provisional definition

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

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

260272 " = ?" ++ show n ++ "_rhs"

261273 if updatefile then

262274 do let fb = fn ++ "~"

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

264276 runIO $ copyFile fb fn

265− else ihPrintResult h $ lem_app

277+ else case idris_outputmode i of

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

266285

267286 where getIndent s = length (takeWhile isSpace s)

268287

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

318337 unlines $ before ++ tyline :

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

320339 later_end)

321−

322−

src/Idris/REPL.hs+4

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

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

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

297297 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)

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

299303 process stdout fn (Apropos a)

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