diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 16 | ||||
| -rw-r--r-- | proofs/proof.ml | 6 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 5 | ||||
| -rw-r--r-- | proofs/refine.ml | 20 |
5 files changed, 36 insertions, 16 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ed0d76f93a..ba7e458f3a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -62,8 +62,7 @@ module V82 = struct goals are restored to their initial value after the evar is created. *) let concl = EConstr.Unsafe.to_constr concl in - let prev_future_goals = Evd.future_goals evars in - let prev_principal_goal = Evd.principal_future_goal evars in + let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; @@ -74,7 +73,7 @@ module V82 = struct in let evi = Typeclasses.mark_unresolvable evi in let (evars, evk) = Evarutil.new_pure_evar_full evars evi in - let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in + let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in let ev = EConstr.mkEvar (evk,inst) in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 03babfede2..8725f51cd7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -170,6 +170,8 @@ let refine_by_tactic env sigma ty tac = ones created during the tactic invocation easily. *) let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in + (** Save the existing goals *) + let prev_future_goals = save_future_goals sigma in (** Start a proof *) let prf = Proof.start sigma [env, ty] in let (prf, _) = @@ -180,7 +182,8 @@ let refine_by_tactic env sigma ty tac = iraise (e, info) in (** Plug back the retrieved sigma *) - let sigma = Proof.in_proof prf (fun sigma -> sigma) in + let (goals,stack,shelf,given_up,sigma) = Proof.proof prf in + assert (stack = []); let ans = match Proof.initial_goals prf with | [c, _] -> c | _ -> assert false @@ -192,6 +195,17 @@ let refine_by_tactic env sigma ty tac = (** Reset the old side-effects *) let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in + (** Restore former goals *) + let sigma = restore_future_goals sigma prev_future_goals in + (** Push remaining goals as future_goals which is the only way we + have to inform the caller that there are goals to collect while + not being encapsulated in the monad *) + (** Goals produced by tactic "shelve" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in + (** Goals produced by tactic "give_up" *) + let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in + (** Other goals *) + let sigma = List.fold_right Evd.declare_future_goal goals sigma in (** Get rid of the fresh side-effects by internalizing them in the term itself. Note that this is unsound, because the tactic may have solved other goals that were already present during its invocation, so that diff --git a/proofs/proof.ml b/proofs/proof.ml index 24f570f01e..51e0a1d614 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -347,7 +347,11 @@ let run_tactic env tac pr = Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in + (* Check that retrieved given up is empty *) + if not (List.is_empty retrieved_given_up) then + CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d713b0999a..15f34ccc6b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -169,6 +169,7 @@ let with_current_proof f = let p = { p with proof = newpr } in pstates := p :: rest; ret + let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ()) let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) @@ -341,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let subst_evar k = Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in let nf = Universes.nf_evars_and_universes_opt_subst subst_evar - (Evd.evar_universe_context_subst universes) in + (UState.subst universes) in let make_body = if poly || now then let make_body t (c, eff) = @@ -436,7 +437,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) diff --git a/proofs/refine.ml b/proofs/refine.ml index 50fd1c4722..909556b1ee 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -78,22 +78,20 @@ let generic_refine ~typecheck f gl = let state = Proofview.Goal.state gl in (** Save the [future_goals] state to restore them after the refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in + let prev_future_goals = Evd.save_future_goals sigma in (** Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> Proofview.tclEVARMAP >>= fun sigma -> Proofview.V82.wrap_exceptions begin fun () -> - let evs = Evd.future_goals sigma in - let evkmain = Evd.principal_future_goal sigma in + let evs = Evd.save_future_goals sigma in (** Redo the effects in sigma in the monad's env *) let privates_csts = Evd.eval_side_effects sigma in let sideff = Safe_typing.side_effects_of_private_constants privates_csts in let env = add_side_effects env sideff in (** Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in - let sigma = if typecheck then CList.fold_left fold sigma evs else sigma in + let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in (** Check that the goal itself does not appear in the refined term *) @@ -102,6 +100,11 @@ let generic_refine ~typecheck f gl = if not (Evarutil.occur_evar_upto sigma self c) then () else Pretype_errors.error_occur_check env sigma self c in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals in + (** Select the goals *) + let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in + let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) let c = EConstr.Unsafe.to_constr c in let sigma = match Proofview.Unsafe.advance sigma self with @@ -118,10 +121,7 @@ let generic_refine ~typecheck f gl = | None -> sigma | Some id -> Evd.rename evk id sigma in - (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in - (** Select the goals *) - let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + (** Mark goals *) let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in @@ -129,6 +129,8 @@ let generic_refine ~typecheck f gl = Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.Unsafe.tclPUTSHELF shelf <*> + Proofview.Unsafe.tclPUTGIVENUP given_up <*> Proofview.tclUNIT v end |