diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 39 |
1 files changed, 28 insertions, 11 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index f62953907..9ee7df14c 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -33,7 +33,7 @@ type entry = (Term.constr * Term.types) list let proofview p = p.comb , p.solution -let compact el { comb; solution } = +let compact el ({ solution } as pv) = let nf = Evarutil.nf_evar solution in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in @@ -46,7 +46,7 @@ let compact el { comb; solution } = let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); - new_el, { comb; solution = new_solution } + new_el, { pv with solution = new_solution; } (** {6 Starting and querying a proof view} *) @@ -63,7 +63,7 @@ let dependent_init = let src = (Loc.ghost,Evar_kinds.GoalEvar) in (* Main routine *) let rec aux = function - | TNil sigma -> [], { solution = sigma; comb = []; } + | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in @@ -71,7 +71,7 @@ let dependent_init = let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let (gl, _) = Term.destEvar econstr in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; } + entry, { solution = sol; comb = gl :: comb; shelf = [] } in fun t -> let entry, v = aux t in @@ -235,6 +235,9 @@ let apply env t sp = match ans with | Nil (e, info) -> iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> + let (status, gaveup) = status in + let status = (status, state.shelf, gaveup) in + let state = { state with shelf = [] } in r, state, status, Trace.to_tree info @@ -581,7 +584,7 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.put initial + Shelf.modify (fun gls -> gls @ initial) (** [contained_in_info e evi] checks whether the evar [e] appears in @@ -620,7 +623,7 @@ let shelve_unifiable = let (u,n) = partition_unifiable initial.solution initial.comb in Comb.set n >> InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.put u + Shelf.modify (fun gls -> gls @ u) (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) @@ -642,6 +645,20 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } +let with_shelf tac = + let open Proof in + Pv.get >>= fun pv -> + let { shelf; solution } = pv in + Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> + tac >>= fun ans -> + Pv.get >>= fun npv -> + let { shelf = gls; solution = sigma } = npv in + let gls' = Evd.future_goals sigma in + let fgoals = Evd.future_goals solution in + let pgoal = Evd.principal_future_goal solution in + let sigma = Evd.restore_future_goals sigma fgoals pgoal in + Pv.set { npv with shelf; solution = sigma } >> + tclUNIT (CList.rev_append gls' gls, ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -870,7 +887,7 @@ module Unsafe = struct let tclSETGOALS = Comb.set let tclEVARSADVANCE evd = - Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) + Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) let tclEVARUNIVCONTEXT ctx = Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) @@ -1121,7 +1138,7 @@ struct let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.set { solution = sigma; comb; } + Pv.modify (fun ps -> { ps with solution = sigma; comb; }) end } (** Useful definitions *) @@ -1204,7 +1221,7 @@ module V82 = struct let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >> - Pv.set { solution = evd; comb = sgs; } + Pv.set { ps with solution = evd; comb = sgs; } with e when catchable_exception e -> let (e, info) = Errors.push e in tclZERO ~info e @@ -1216,7 +1233,7 @@ module V82 = struct Pv.modify begin fun ps -> let map g s = GoalV82.nf_evar s g in let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { solution = evd; comb = goals; } + { ps with solution = evd; comb = goals; } end let has_unresolved_evar pv = @@ -1261,7 +1278,7 @@ module V82 = struct let of_tactic t gls = try - let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in + let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = final.comb } with Logic_monad.TacticFailure e as src -> |