3d6fc38 · Idris-dev · git.iko.soy

216 (f:_) -> f

217 _ -> ""

218 case IdeSlave.sexpToCommand sexp of

219− Just (IdeSlave.Interpret cmd) ->

219+ Just cmd -> runIdeSlaveCommand id orig fn mods cmd

220− do c <- colourise

221− case parseCmd i "(input)" cmd of

222− Failure err -> iPrintError $ show (fixColour c err)

223− Success (Prove n') -> do iPrintResult ""

224− idrisCatch

225− (process stdout fn (Prove n'))

226− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

227− isetPrompt (mkPrompt mods)

228− Success cmd -> idrisCatch

229− (ideslaveProcess fn cmd)

230− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

231− Just (IdeSlave.REPLCompletions str) ->

232− do (unused, compls) <- replCompletion (reverse str, "")

233− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

234− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

235− Just (IdeSlave.LoadFile filename) ->

236− do clearErr

237− putIState (orig { idris_options = idris_options i,

238− idris_outputmode = (IdeSlave id) })

239− loadInputs stdout [filename]

240− isetPrompt (mkPrompt [filename])

241− -- Report either success or failure

242− i <- getIState

243− case (errSpan i) of

244− Nothing -> iPrintResult $ "loaded " ++ filename

245− Just x -> iPrintError $ "didn't load " ++ filename

246− ideslave orig [filename]

247− Just (IdeSlave.TypeOf name) ->

248− case splitName name of

249− Left err -> iPrintError err

250− Right n -> process stdout "(ideslave)"

251− (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

252− Just (IdeSlave.DocsFor name) ->

253− case splitName name of

254− Left err -> iPrintError err

255− Right n -> process stdout "(ideslave)" (DocStr n)

256− Just (IdeSlave.CaseSplit line name) ->

257− process stdout fn (CaseSplitAt False line (sUN name))

258− Just (IdeSlave.AddClause line name) ->

259− process stdout fn (AddClauseFrom False line (sUN name))

260− Just (IdeSlave.AddProofClause line name) ->

261− process stdout fn (AddProofClauseFrom False line (sUN name))

262− Just (IdeSlave.AddMissing line name) ->

263− process stdout fn (AddMissing False line (sUN name))

264− Just (IdeSlave.MakeWithBlock line name) ->

265− process stdout fn (MakeWith False line (sUN name))

266− Just (IdeSlave.ProofSearch line name hints) ->

267− process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

268− Just (IdeSlave.Apropos a) ->

269− process stdout fn (Apropos a)

270− Just (IdeSlave.GetOpts) ->

271− do ist <- getIState

272− let opts = idris_options ist

273− let impshow = opt_showimp opts

274− let errCtxt = opt_errContext opts

275− let options = (IdeSlave.SymbolAtom "ok",

276− [(IdeSlave.SymbolAtom "show-implicits", impshow),

277− (IdeSlave.SymbolAtom "error-context", errCtxt)])

278− runIO . putStrLn $ IdeSlave.convSExp "return" options id

279− Just (IdeSlave.SetOpt IdeSlave.ShowImpl b) ->

280− do setImpShow b

281− let msg = (IdeSlave.SymbolAtom "ok", b)

282− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

283− Just (IdeSlave.SetOpt IdeSlave.ErrContext b) ->

284− do setErrContext b

285− let msg = (IdeSlave.SymbolAtom "ok", b)

286− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

287− Just (IdeSlave.Metavariables cols) ->

288− do ist <- getIState

289− let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

290− imp <- impShow

291− let mvarTys = map (delabTy ist) mvs

292− let res = (IdeSlave.SymbolAtom "ok",

293− zipWith (\ n (prems, concl) -> (n, prems, concl))

294− (map (IdeSlave.StringAtom . show) mvs)

295− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

296− runIO . putStrLn $ IdeSlave.convSExp "return" res id

297− Nothing -> do iPrintError "did not understand")

220+ Nothing -> iPrintError "did not understand" )

298 (\e -> do iPrintError $ show e))

221 (\e -> do iPrintError $ show e))

299 (\e -> do iPrintError $ show e)

222 (\e -> do iPrintError $ show e)

300 ideslave orig mods

223 ideslave orig mods

224+

225+-- | Run IDESlave commands

226+runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client

227+ -> IState -- ^^ The original IState

228+ -> FilePath -- ^^ The current open file

229+ -> [FilePath] -- ^^ The currently loaded modules

230+ -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

231+ -> Idris ()

232+runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

233+ do c <- colourise

234+ i <- getIState

235+ case parseCmd i "(input)" cmd of

236+ Failure err -> iPrintError $ show (fixColour c err)

237+ Success (Prove n') -> do iPrintResult ""

238+ idrisCatch

239+ (process stdout fn (Prove n'))

240+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

241+ isetPrompt (mkPrompt mods)

242+ Success cmd -> idrisCatch

243+ (ideslaveProcess fn cmd)

244+ (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

245+runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =

246+ do (unused, compls) <- replCompletion (reverse str, "")

247+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

248+ IdeSlave.toSExp (map replacement compls,

249+ reverse unused)]

250+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id

251+runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename) =

252+ do i <- getIState

253+ clearErr

254+ putIState (orig { idris_options = idris_options i,

255+ idris_outputmode = (IdeSlave id) })

256+ loadInputs stdout [filename]

257+ isetPrompt (mkPrompt [filename])

258+ -- Report either success or failure

259+ i <- getIState

260+ case (errSpan i) of

261+ Nothing -> iPrintResult $ "loaded " ++ filename

262+ Just x -> iPrintError $ "didn't load " ++ filename

263+ ideslave orig [filename]

264+runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

265+ case splitName name of

266+ Left err -> iPrintError err

267+ Right n -> process stdout "(ideslave)"

268+ (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

269+ where splitName :: String -> Either String Name

270+ splitName s = case reverse $ splitOn "." s of

271+ [] -> Left ("Didn't understand name '" ++ s ++ "'")

272+ [n] -> Right $ sUN n

273+ (n:ns) -> Right $ sNS (sUN n) ns

274+runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

275+ case splitName name of

276+ Left err -> iPrintError err

277+ Right n -> process stdout "(ideslave)" (DocStr n)

301 where splitName :: String -> Either String Name

278 where splitName :: String -> Either String Name

302 splitName s = case reverse $ splitOn "." s of

279 splitName s = case reverse $ splitOn "." s of

303 [] -> Left ("Didn't understand name '" ++ s ++ "'")

280 [] -> Left ("Didn't understand name '" ++ s ++ "'")

304 [n] -> Right $ sUN n

281 [n] -> Right $ sUN n

305 (n:ns) -> Right $ sNS (sUN n) ns

282 (n:ns) -> Right $ sNS (sUN n) ns

283+runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

284+ process stdout fn (CaseSplitAt False line (sUN name))

285+runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

286+ process stdout fn (AddClauseFrom False line (sUN name))

287+runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =

288+ process stdout fn (AddProofClauseFrom False line (sUN name))

289+runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

290+ process stdout fn (AddMissing False line (sUN name))

291+runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

292+ process stdout fn (MakeWith False line (sUN name))

293+runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch line name hints) =

294+ process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

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

296+ process stdout fn (Apropos a)

297+runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

298+ do ist <- getIState

299+ let opts = idris_options ist

300+ let impshow = opt_showimp opts

301+ let errCtxt = opt_errContext opts

302+ let options = (IdeSlave.SymbolAtom "ok",

303+ [(IdeSlave.SymbolAtom "show-implicits", impshow),

304+ (IdeSlave.SymbolAtom "error-context", errCtxt)])

305+ runIO . putStrLn $ IdeSlave.convSExp "return" options id

306+runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

307+ do setImpShow b

308+ let msg = (IdeSlave.SymbolAtom "ok", b)

309+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

310+runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

311+ do setErrContext b

312+ let msg = (IdeSlave.SymbolAtom "ok", b)

313+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

314+runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

315+ do ist <- getIState

316+ let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

317+ imp <- impShow

318+ let mvarTys = map (delabTy ist) mvs

319+ let res = (IdeSlave.SymbolAtom "ok",

320+ zipWith (\ n (prems, concl) -> (n, prems, concl))

321+ (map (IdeSlave.StringAtom . show) mvs)

322+ (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

323+ runIO . putStrLn $ IdeSlave.convSExp "return" res id

306− getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

324+ where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

307 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

325 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

308 in ((n, t):prems, conc)

326 in ((n, t):prems, conc)

309 getGoal tm = ([], tm)

327 getGoal tm = ([], tm)

325 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

343 rest = sexpGoal ist cols imp (n:ns) (ps, concl)

326 in ((n', t', spans) : fst rest, snd rest)

344 in ((n', t', spans) : fst rest, snd rest)

327

345

346+

328ideslaveProcess :: FilePath -> Command -> Idris ()

347ideslaveProcess :: FilePath -> Command -> Idris ()

329ideslaveProcess fn Help = process stdout fn Help

348ideslaveProcess fn Help = process stdout fn Help

330ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

349ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)