diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 11 | ||||
| -rw-r--r-- | proofs/clenv.mli | 8 | ||||
| -rw-r--r-- | proofs/goal.ml | 12 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/proof.ml | 105 | ||||
| -rw-r--r-- | proofs/proof.mli | 7 | ||||
| -rw-r--r-- | proofs/refine.ml | 27 |
7 files changed, 68 insertions, 104 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index db76d08736..31bc698830 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -618,9 +618,6 @@ let clenv_cast_meta clenv = in crec -let clenv_value_cast_meta clenv = - clenv_cast_meta clenv (clenv_value clenv) - let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in @@ -673,7 +670,7 @@ let fail_quick_core_unif_flags = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; @@ -716,12 +713,6 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function | NoBindings -> mk_clenv_from_env env sigma n (c,t) -let make_clenv_binding_env_apply env sigma n = - make_clenv_binding_gen true n env sigma - -let make_clenv_binding_env env sigma = - make_clenv_binding_gen false None env sigma - let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 43e808dac7..a72c8c5e1f 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -75,17 +75,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** the arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None *) -val make_clenv_binding_env_apply : - env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> - clausenv - val make_clenv_binding_apply : env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv -val make_clenv_binding_env : - env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv - val make_clenv_binding : env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv @@ -99,7 +92,6 @@ val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv -val clenv_value_cast_meta : clausenv -> constr (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.t diff --git a/proofs/goal.ml b/proofs/goal.ml index beeaa60433..e8f2ab5674 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Pp module NamedDecl = Context.Named.Declaration @@ -57,13 +56,12 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) - let prev_future_goals = Evd.save_future_goals evars in - let (evars, evk) = - Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false hyps evars concl + let evars = Evd.push_future_goals evars in + let inst = EConstr.identity_subst_val hyps in + let (evars,evk) = + Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl in - let evars = Evd.restore_future_goals evars prev_future_goals in - let ctxt = Environ.named_context_of_val hyps in - let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let _, evars = Evd.pop_future_goals evars in let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) diff --git a/proofs/goal.mli b/proofs/goal.mli index a3aa1e248f..e8439120c0 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -65,4 +65,4 @@ module V82 : sig end -module Set : sig include Set.S with type elt = goal end +module Set = Evar.Set diff --git a/proofs/proof.ml b/proofs/proof.ml index a183fa7797..d864aed25a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -24,8 +24,6 @@ the focus kind is actually stored inside the condition). To unfocus, one needs to know the focus kind, and the condition (for instance "no condition" or the proof under focused must be complete) must be met. - - Shelf: A list of goals which have been put aside during the proof. They can be - retrieved with the [Unshelve] command, or solved by side effects - Given up goals: as long as there is a given up goal, the proof is not completed. Given up goals cannot be retrieved, the user must go back where the tactic [give_up] was run and solve the goal there. @@ -113,10 +111,6 @@ type t = (** History of the focusings, provides information on how to unfocus the proof and the extra information stored while focusing. The list is empty when the proof is fully unfocused. *) - ; shelf : Goal.goal list - (** List of goals that have been shelved. *) - ; given_up : Goal.goal list - (** List of goals that have been given up *) ; name : Names.Id.t (** the name of the theorem whose proof is being constructed *) ; poly : bool @@ -137,9 +131,7 @@ let proof p = let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack in - let shelf = p.shelf in - let given_up = p.given_up in - (goals,stack,shelf,given_up,sigma) + (goals,stack,sigma) let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk @@ -155,8 +147,12 @@ let is_done p = (* spiwack: for compatibility with <= 8.2 proof engine *) let has_unresolved_evar p = Proofview.V82.has_unresolved_evar p.proofview -let has_shelved_goals p = not (CList.is_empty (p.shelf)) -let has_given_up_goals p = not (CList.is_empty (p.given_up)) +let has_shelved_goals p = + let (_goals,sigma) = Proofview.proofview p.proofview in + Evd.has_shelved sigma +let has_given_up_goals p = + let (_goals,sigma) = Proofview.proofview p.proofview in + Evd.has_given_up sigma let is_complete p = is_done p && not (has_unresolved_evar p) && @@ -217,13 +213,10 @@ let focus_id cond inf id pr = (* goal is already under focus *) _focus cond (Obj.repr inf) i i pr | None -> - if CList.mem_f Evar.equal ev pr.shelf then + if CList.mem_f Evar.equal ev (Evd.shelf evar_map) then (* goal is on the shelf, put it in focus *) let proofview = Proofview.unshelve [ev] pr.proofview in - let shelf = - CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf - in - let pr = { pr with proofview; shelf } in + let pr = { pr with proofview } in let (focused_goals, _) = Proofview.proofview pr.proofview in let i = (* Now we know that this will succeed *) @@ -291,8 +284,6 @@ let start ~name ~poly sigma goals = { proofview ; entry ; focus_stack = [] - ; shelf = [] - ; given_up = [] ; name ; poly } in @@ -304,8 +295,6 @@ let dependent_start ~name ~poly goals = { proofview ; entry ; focus_stack = [] - ; shelf = [] - ; given_up = [] ; name ; poly } in @@ -356,46 +345,53 @@ let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in { p with proofview; entry } +let update_sigma_univs ugraph p = + let proofview = Proofview.Unsafe.update_sigma_univs ugraph p.proofview in + { p with proofview } + (*** Function manipulation proof extra informations ***) (*** Tactics ***) let run_tactic env tac pr = let open Proofview.Notations in - let sp = pr.proofview in let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in let tac = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclEVARS (Evd.push_shelf sigma) >>= fun () -> tac >>= fun result -> Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - 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 retrieved, sigma = Evd.pop_future_goals sigma in + let retrieved = Evd.FutureGoals.filter (Evd.is_undefined sigma) retrieved in + let retrieved = List.rev retrieved.Evd.FutureGoals.comb in let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in + let to_shelve, sigma = Evd.pop_shelf sigma in Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT (result,retrieved) + Proofview.Unsafe.tclNEWSHELVED (retrieved@to_shelve) <*> + Proofview.tclUNIT (result,retrieved,to_shelve) in - let { name; poly } = pr in - let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) = - Proofview.apply ~name ~poly env tac sp + let { name; poly; proofview } = pr in + let proofview = Proofview.Unsafe.push_future_goals proofview in + let ((result,retrieved,to_shelve),proofview,status,info_trace) = + Proofview.apply ~name ~poly env tac proofview in let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in - let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in - let given_up = pr.given_up@give_up in - let proofview = Proofview.Unsafe.reset_future_goals proofview in - { pr with proofview ; shelf ; given_up },(status,info_trace),result + let proofview = Proofview.filter_shelf (Evd.is_undefined sigma) proofview in + { pr with proofview },(status,info_trace),result (*** Commands ***) (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) let unshelve p = - { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } + let sigma = Proofview.return p.proofview in + let shelf = Evd.shelf sigma in + let proofview = Proofview.unshelve shelf p.proofview in + { p with proofview } (*** Compatibility layer with <=v8.2 ***) module V82 = struct @@ -441,23 +437,23 @@ module V82 = struct end in let { name; poly } = pr in let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in - let shelf = - List.filter begin fun g -> + let proofview = Proofview.filter_shelf + begin fun g -> Evd.is_undefined (Proofview.return proofview) g - end pr.shelf + end proofview in - { pr with proofview ; shelf } + { pr with proofview } end let all_goals p = let add gs set = List.fold_left (fun s g -> Goal.Set.add g s) set gs in - let (goals,stack,shelf,given_up,_) = proof p in + let (goals,stack,sigma) = proof p in let set = add goals Goal.Set.empty in let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in - let set = add shelf set in - let set = add given_up set in + let set = add (Evd.shelf sigma) set in + let set = Goal.Set.union (Evd.given_up sigma) set in let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in add bgoals set @@ -470,17 +466,13 @@ type data = (** Entry for the proofview *) ; stack : (Evar.t list * Evar.t list) list (** A representation of the focus stack *) - ; shelf : Evar.t list - (** A representation of the shelf *) - ; given_up : Evar.t list - (** A representation of the given up goals *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) } -let data { proofview; focus_stack; entry; shelf; given_up; name; poly } = +let data { proofview; focus_stack; entry; name; poly } = let goals, sigma = Proofview.proofview proofview in (* spiwack: beware, the bottom of the stack is used by [Proof] internally, and should not be exposed. *) @@ -491,10 +483,10 @@ let data { proofview; focus_stack; entry; shelf; given_up; name; poly } = in let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in - { sigma; goals; entry; stack; shelf; given_up; name; poly } + { sigma; goals; entry; stack; name; poly } let pr_proof p = - let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in + let { goals=fg_goals; stack=bg_goals; sigma } = data p in Pp.( let pr_goal_list = prlist_with_sep spc Goal.pr_goal in let rec aux acc = function @@ -504,8 +496,8 @@ let pr_proof p = pr_goal_list after) stack in str "[" ++ str "focus structure: " ++ aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++ - str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++ - str "given up: " ++ pr_goal_list given_up ++ + str "shelved: " ++ pr_goal_list (Evd.shelf sigma) ++ str ";" ++ spc () ++ + str "given up: " ++ pr_goal_list (Evar.Set.elements @@ Evd.given_up sigma) ++ str "]" ) @@ -574,7 +566,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let eff = Evd.eval_side_effects sigma in let sigma = Evd.drop_side_effects sigma in (* Save the existing goals *) - let prev_future_goals = Evd.save_future_goals sigma in + let sigma = Evd.push_future_goals sigma in (* Start a proof *) let prf = start ~name ~poly sigma [env, ty] in let (prf, _, ()) = @@ -585,7 +577,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = Exninfo.iraise (e, info) in (* Plug back the retrieved sigma *) - let { goals; stack; shelf; given_up; sigma; entry } = data prf in + let { goals; stack; sigma; entry } = data prf in assert (stack = []); let ans = match Proofview.initial_goals entry with | [c, _] -> c @@ -598,15 +590,10 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let sigma = Evd.drop_side_effects sigma in let sigma = Evd.emit_side_effects eff sigma in (* Restore former goals *) - let sigma = Evd.restore_future_goals sigma prev_future_goals in + let _goals, sigma = Evd.pop_future_goals sigma 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 diff --git a/proofs/proof.mli b/proofs/proof.mli index 0e5bdaf07d..f487595dac 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -43,10 +43,6 @@ type data = (** Entry for the proofview *) ; stack : (Evar.t list * Evar.t list) list (** A representation of the focus stack *) - ; shelf : Evar.t list - (** A representation of the shelf *) - ; given_up : Evar.t list - (** A representation of the given up goals *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool; @@ -78,6 +74,9 @@ val partial_proof : t -> EConstr.constr list val compact : t -> t +(** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proof *) +val update_sigma_univs : UGraph.t -> t -> t + (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. Raises [HasShelvedGoals] if some goals are left on the shelf. diff --git a/proofs/refine.ml b/proofs/refine.ml index a10bbcbdd4..ac410a958f 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -51,19 +51,18 @@ 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.save_future_goals sigma in + let sigma = Evd.push_future_goals sigma in (* Create the refinement term *) - Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> + Proofview.Unsafe.tclEVARS sigma >>= fun () -> f >>= fun (v, c) -> - Proofview.tclEVARMAP >>= fun sigma -> + Proofview.tclEVARMAP >>= fun sigma' -> Proofview.V82.wrap_exceptions begin fun () -> - 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 privates_csts = Evd.eval_side_effects sigma' in let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in - let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in + let sigma = if typecheck then Evd.fold_future_goals fold sigma' else sigma' in (* Check that the refined term is typesafe *) let sigma = if typecheck then Typing.check env sigma c concl else sigma in (* Check that the goal itself does not appear in the refined term *) @@ -73,17 +72,18 @@ let generic_refine ~typecheck f gl = 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 + let future_goals, sigma = Evd.pop_future_goals sigma 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 + let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in + let shelf = Evd.shelf sigma in + let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ List.mem ev shelf) future_goals in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with | None -> (* Nothing to do, the goal has been solved by side-effect *) sigma | Some self -> - match evkmain with + match future_goals.Evd.FutureGoals.principal with | None -> Evd.define self c sigma | Some evk -> let id = Evd.evar_ident self sigma in @@ -93,17 +93,14 @@ let generic_refine ~typecheck f gl = | Some id -> Evd.rename evk id sigma in (* Mark goals *) - let sigma = Proofview.Unsafe.mark_as_goals sigma comb in - let sigma = Proofview.Unsafe.mark_unresolvables sigma shelf in - let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in + let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in + let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> 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 |