bf7d26c · Idris-dev · git.iko.soy

156 iputGoal rendered

157dumpState ist inElab menv ps | (h : hs) <- holes ps = do

158 let OK ty = goalAtFocus ps

159− let OK env = envAtFocus ps

159+ OK env = envAtFocus ps

160− let state = prettyOtherGoals hs <> line <>

160+ state = prettyOtherGoals hs <> line <>

161 prettyAssumptions inElab ty env <> line <>

162 prettyMetaValues (reverse menv) <>

163 prettyGoal (zip (assumptionNames env) (repeat False)) ty

215 bindingOf h False <+> colon <+> align (prettyG bnd ty)

216

217 prettyAssumptions inElab g env =

218− if length env == 0 then

218+ if null env then empty

219− empty

220 else

219 else

221 text "---------- Assumptions: ----------" <>

220 text "---------- Assumptions: ----------" <>

222 nest nestingSize (prettyPs inElab g [] $ reverse env)

221 nest nestingSize (prettyPs inElab g [] $ reverse env)

223

222

224 prettyOtherGoals hs =

223 prettyOtherGoals hs =

225− if length hs == 0 then

224+ if null hs then empty

226− empty

227 else

225 else

228 text "---------- Other goals: ----------" <$$>

226 text "---------- Other goals: ----------" <$$>

229− nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)

227+ nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)

230

228

231 freeEnvNames :: Env -> [Name]

229 freeEnvNames :: Env -> [Name]

232− freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))

230+ freeEnvNames = concatMap (\(n, b) -> freeNames (Bind n b Erased))

233

231

234lifte :: ElabState EState -> ElabD a -> Idris a

232lifte :: ElabState EState -> ElabD a -> Idris a

235lifte st e = do (v, _) <- elabStep st e

233lifte st e = do (v, _) <- elabStep st e

247 (sexp, id) <- case IdeMode.parseMessage l of

245 (sexp, id) <- case IdeMode.parseMessage l of

248 Left err -> ierror err

246 Left err -> ierror err

249 Right (sexp, id) -> return (sexp, id)

247 Right (sexp, id) -> return (sexp, id)

250− putIState $ i { idris_outputmode = (IdeMode id h) }

248+ putIState $ i { idris_outputmode = IdeMode id h }

251 case IdeMode.sexpToCommand sexp of

249 case IdeMode.sexpToCommand sexp of

252 Just (IdeMode.REPLCompletions prefix) ->

250 Just (IdeMode.REPLCompletions prefix) ->

253 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

251 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

309 Success (Left cmd') ->

307 Success (Left cmd') ->

310 case cmd' of

308 case cmd' of

311 EQED -> do hs <- lifte e get_holes

309 EQED -> do hs <- lifte e get_holes

312− when (not (null hs)) $ ifail "Incomplete proof"

310+ unless (null hs) $ ifail "Incomplete proof"

313 iputStrLn "Proof completed!"

311 iputStrLn "Proof completed!"

314 return (False, prev, e, True, prf, env, Right $ iPrintResult "")

312 return (False, prev, e, True, prf, env, Right $ iPrintResult "")

315 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev

313 EUndo -> do (prf', env', st', prev') <- undoElab prf env e prev

333 return (d', prev, st', done, prf', env, go)

331 return (d', prev, st', done, prf', env, go)

334 Success (Right cmd') ->

332 Success (Right cmd') ->

335 case cmd' of

333 case cmd' of

336− DoLetP _ _ _ -> ifail "Pattern-matching let not supported here"

334+ DoLetP {} -> ifail "Pattern-matching let not supported here"

337− DoBindP _ _ _ _ -> ifail "Pattern-matching <- not supported here"

335+ DoBindP {} -> ifail "Pattern-matching <- not supported here"

338 DoLet fc i ifc Placeholder expr ->

336 DoLet fc i ifc Placeholder expr ->

339 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

337 do (tm, ty) <- elabVal recinfo ERHS (inLets ist env expr)

340 ctxt <- getContext

338 ctxt <- getContext

380 else do ok

378 else do ok

381 elabloop fn d prompt prf' st prev' h' env'

379 elabloop fn d prompt prf' st prev' h' env'

382

380

383− where

381+ where

384 -- A bit of a hack: wrap the value up in a let binding, which will

382 -- A bit of a hack: wrap the value up in a let binding, which will

385 -- normalise away. It would be better to figure out how to call

383 -- normalise away. It would be better to figure out how to call

386 -- the elaborator with a custom environment here to avoid the

384 -- the elaborator with a custom environment here to avoid the

412 return (i, h)

410 return (i, h)

413 (cmd, step) <- case x of

411 (cmd, step) <- case x of

414 Nothing -> do iPrintError ""; ifail "Abandoned"

412 Nothing -> do iPrintError ""; ifail "Abandoned"

415− Just input -> do return (parseTactic i input, input)

413+ Just input -> return (parseTactic i input, input)

416 case cmd of

414 case cmd of

417 Success Abandon -> do iPrintError ""; ifail "Abandoned"

415 Success Abandon -> do iPrintError ""; ifail "Abandoned"

418 _ -> return ()

416 _ -> return ()

426 iputStrLn $ "TT: " ++ show tm ++ "\n"

424 iputStrLn $ "TT: " ++ show tm ++ "\n"

427 return (False, e, False, prf, Right $ iPrintResult "")

425 return (False, e, False, prf, Right $ iPrintResult "")

428 Success Qed -> do hs <- lifte e get_holes

426 Success Qed -> do hs <- lifte e get_holes

429− when (not (null hs)) $ ifail "Incomplete proof"

427+ unless (null hs) $ ifail "Incomplete proof"

430 iputStrLn "Proof completed!"

428 iputStrLn "Proof completed!"

431 return (False, e, True, prf, Right $ iPrintResult "")

429 return (False, e, True, prf, Right $ iPrintResult "")

432 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

430 Success (TCheck (PRef _ _ n)) -> checkNameType e prf n