aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/pfedit.ml26
-rw-r--r--proofs/pfedit.mli6
-rw-r--r--proofs/proof.ml9
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/refine.ml33
-rw-r--r--proofs/refine.mli5
-rw-r--r--proofs/tacmach.ml7
-rw-r--r--proofs/tacmach.mli9
10 files changed, 88 insertions, 13 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 5f0cc73d2c..29cad06352 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -46,7 +46,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
let sigma',typed_c =
let flags = {
Pretyping.use_typeclasses = true;
- Pretyping.use_unif_heuristics = true;
+ Pretyping.solve_unification_constraints = true;
Pretyping.use_hook = None;
Pretyping.fail_evar = false;
Pretyping.expand_evars = true } in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e4c833627a..65497c80dd 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -538,7 +538,7 @@ let prim_refiner r sigma goal =
nexthyp,
t,cl,sigma
else
- (if !check && mem_named_context id (named_context_of_val sign) then
+ (if !check && mem_named_context_val id sign then
errorlabstrm "Logic.prim_refiner"
(str "Variable " ++ pr_id id ++ str " is already declared.");
push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4bae20128..eddbf72a89 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -13,6 +13,17 @@ open Entries
open Environ
open Evd
+let use_unification_heuristics_ref = ref true
+let _ = Goptions.declare_bool_option {
+ Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optname = "Solve unification constraints at every \".\"";
+ Goptions.optkey = ["Solve";"Unification";"Constraints"];
+ Goptions.optread = (fun () -> !use_unification_heuristics_ref);
+ Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a);
+}
+
+let use_unification_heuristics () = !use_unification_heuristics_ref
+
let refining = Proof_global.there_are_pending_proofs
let check_no_pending_proofs = Proof_global.check_no_pending_proof
@@ -119,6 +130,11 @@ let solve ?with_end_tac gi info_lvl tac pr =
| Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
| Vernacexpr.SelectAll -> tac
in
+ let tac =
+ if use_unification_heuristics () then
+ Proofview.tclTHEN tac Refine.solve_constraints
+ else tac
+ in
let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
let () =
match info_lvl with
@@ -161,11 +177,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
delete_current_proof ();
iraise reraise
-let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
let gk = Global, poly, Proof Theorem in
- let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
+ let ce, status, univs =
+ build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
let ce =
if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
else { ce with
@@ -232,8 +249,9 @@ let solve_by_implicit_tactic env sigma evk =
(try
let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
if Evarutil.has_undefined_evars sigma c then raise Exit;
- let (ans, _, _) =
+ let (ans, _, ctx) =
build_by_tactic env (Evd.evar_universe_context sigma) c tac in
- ans
+ let sigma = Evd.set_universe_context sigma ctx in
+ sigma, ans
with e when Logic.catchable_exception e -> raise Exit)
| _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 666730e1af..ea604e08eb 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -167,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
val build_constant_by_tactic :
Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
types -> unit Proofview.tactic ->
- Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
+ Safe_typing.private_constants Entries.definition_entry * bool *
+ Evd.evar_universe_context
val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
types -> unit Proofview.tactic ->
@@ -189,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
val clear_implicit_tactic : unit -> unit
(* Raise Exit if cannot solve *)
-(* FIXME: interface: it may incur some new universes etc... *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr
+val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5fe29653d3..5c963d53e7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -351,7 +351,14 @@ let run_tactic env tac pr =
Proofview.apply env tac sp
in
let sigma = Proofview.return proofview in
- let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in
+ let to_shelve = undef sigma to_shelve in
+ let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
+ let proofview =
+ List.fold_left
+ Proofview.Unsafe.mark_as_unresolvable
+ 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)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7605f63872..e753e972da 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -617,7 +617,7 @@ module Bullet = struct
let _ = register_behavior strict
end
- (* Current bullet behavior, controled by the option *)
+ (* Current bullet behavior, controlled by the option *)
let current_behavior = ref Strict.strict
let _ =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index dc6f4cea10..3f55270609 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -51,6 +51,23 @@ let typecheck_proof c concl env sigma =
let (pr_constrv,pr_constr) =
Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
+(* Get the side-effect's constant declarations to update the monad's
+ * environmnent *)
+let add_if_undefined kn cb env =
+ try ignore(Environ.lookup_constant kn env); env
+ with Not_found -> Environ.add_constant kn cb env
+
+(* Add the side effects to the monad's environment, if not already done. *)
+let add_side_effect env = function
+ | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+ add_if_undefined kn cb env
+ | { Entries.eff = Entries.SEscheme (l,_) } ->
+ List.fold_left (fun env (_,kn,cb,eff_env) ->
+ add_if_undefined kn cb env) env l
+
+let add_side_effects env effects =
+ List.fold_left (fun env eff -> add_side_effect env eff) env effects
+
let make_refine_enter ?(unsafe = true) f =
{ enter = fun gl ->
let gl = Proofview.Goal.assume gl in
@@ -66,6 +83,10 @@ let make_refine_enter ?(unsafe = true) f =
let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
let evs = Evd.future_goals sigma in
let evkmain = Evd.principal_future_goal 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 unsafe then sigma else CList.fold_left fold sigma evs in
@@ -94,6 +115,7 @@ let make_refine_enter ?(unsafe = true) f =
let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv 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.tclUNIT v
@@ -127,3 +149,14 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
} in
refine ?unsafe f
end }
+
+(** {7 solve_constraints}
+
+ Ensure no remaining unification problems are left. Run at every "." by default. *)
+
+let solve_constraints =
+ let open Proofview in
+ tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
+ try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ Unsafe.tclEVARSADVANCE sigma
+ with e -> tclZERO e
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3d140f036b..a44632eff5 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -43,3 +43,8 @@ val with_type : Environ.env -> Evd.evar_map ->
val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
(** Like {!refine} except the refined term is coerced to the conclusion of the
current goal. *)
+
+(** {7 Unification constraint handling} *)
+
+val solve_constraints : unit tactic
+(** Solve any remaining unification problems, applying heuristics. *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b9330ff007..330594af5c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -171,6 +171,9 @@ module New = struct
let pf_unsafe_type_of gl t =
pf_apply unsafe_type_of gl t
+ let pf_get_type_of gl t =
+ pf_apply (Retyping.get_type_of ~lax:true) gl t
+
let pf_type_of gl t =
pf_apply type_of gl t
@@ -187,9 +190,9 @@ module New = struct
next_ident_away id ids
let pf_get_hyp id gl =
- let hyps = Proofview.Goal.hyps gl in
+ let hyps = Proofview.Goal.env gl in
let sign =
- try Context.Named.lookup id hyps
+ try Environ.lookup_named id hyps
with Not_found -> raise (RefinerError (NoSuchHyp id))
in
sign
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 727efcf6dc..59f296f64e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -108,7 +108,16 @@ module New : sig
val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
+ (** WRONG: To be avoided at all costs, it typechecks the term entirely but
+ forgets the universe constraints necessary to retypecheck it *)
val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+
+ (** This function does no type inference and expects an already well-typed term.
+ It recomputes its type in the fastest way possible (no conversion is ever involved) *)
+ val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+
+ (** This function entirely type-checks the term and computes its type
+ and the implied universe constraints. *)
val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:11:12 +0000