aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenvtac.ml26
-rw-r--r--proofs/logic.ml14
-rw-r--r--proofs/logic.mli3
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/pfedit.mli6
-rw-r--r--proofs/proof_type.mli1
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/refine.ml21
-rw-r--r--proofs/refine.mli3
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli1
11 files changed, 59 insertions, 32 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 04a2eb4879..98b5bc8b05 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -59,6 +59,19 @@ let clenv_pose_dependent_evars with_evars clenv =
(RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
clenv_pose_metas_as_evars clenv dep_mvs
+(** Use our own fast path, more informative than from Typeclasses *)
+let check_tc evd =
+ let has_resolvable = ref false in
+ let check _ evi =
+ let res = Typeclasses.is_resolvable evi in
+ if res then
+ let () = has_resolvable := true in
+ Typeclasses.is_class_evar evd evi
+ else false
+ in
+ let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
+ (has_typeclass, !has_resolvable)
+
let clenv_refine with_evars ?(with_classes=true) clenv =
(** ppedrot: a Goal.enter here breaks things, because the tactic below may
solve goals by side effects, while the compatibility layer keeps those
@@ -67,9 +80,16 @@ let clenv_refine with_evars ?(with_classes=true) clenv =
let clenv = clenv_pose_dependent_evars with_evars clenv in
let evd' =
if with_classes then
- let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
- ~fail:(not with_evars) clenv.env clenv.evd
- in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+ let (has_typeclass, has_resolvable) = check_tc clenv.evd in
+ let evd' =
+ if has_typeclass then
+ Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+ ~fail:(not with_evars) clenv.env clenv.evd
+ else clenv.evd
+ in
+ if has_resolvable then
+ Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
+ else evd'
else clenv.evd
in
let clenv = { clenv with evd = evd' } in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index cc95de646e..65497c80dd 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -276,6 +276,11 @@ let move_hyp toleft (left,declfrom,right) hto =
List.fold_left (fun sign d -> push_named_context_val d sign)
right left
+let move_hyp_in_named_context hfrom hto sign =
+ let (left,right,declfrom,toleft) =
+ split_sign hfrom hto (named_context_of_val sign) in
+ move_hyp toleft (left,declfrom,right) hto
+
(**********************************************************************)
@@ -549,12 +554,3 @@ let prim_refiner r sigma goal =
let sgl = List.rev sgl in
let sigma = Goal.V82.partial_solution sigma goal oterm in
(sgl, sigma)
-
- | Move (hfrom, hto) ->
- let (left,right,declfrom,toleft) =
- split_sign hfrom hto (named_context_of_val sign) in
- let hyps' =
- move_hyp toleft (left,declfrom,right) hto in
- let (gl,ev,sigma) = mk_goal hyps' cl in
- let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
- ([gl], sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2764d28c02..0dba9ef1ee 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -56,3 +56,6 @@ val catchable_exception : exn -> bool
val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
Context.Named.Declaration.t -> Environ.named_context_val
+
+val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+ Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4bae20128..a3ece19134 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -161,11 +161,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 +233,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_type.mli b/proofs/proof_type.mli
index f7798a0edb..c120796220 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -22,7 +22,6 @@ open Misctypes
type prim_rule =
| Cut of bool * bool * Id.t * types
| Refine of constr
- | Move of Id.t * Id.t move_location
(** Nowadays, the only rules we'll consider are the primitive rules *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8a9ce4f944..72cb05f1b6 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -44,7 +44,7 @@ let cbv_native env sigma c =
let whd_cbn flags env sigma t =
let (state,_) =
- (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty))
+ (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
in Reductionops.Stack.zip ~refold:true state
let strong_cbn flags =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index af9be78974..dc6f4cea10 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -51,7 +51,8 @@ let typecheck_proof c concl env sigma =
let (pr_constrv,pr_constr) =
Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
-let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
+let make_refine_enter ?(unsafe = true) f =
+ { enter = fun gl ->
let gl = Proofview.Goal.assume gl in
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
@@ -62,7 +63,7 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
let prev_future_goals = Evd.future_goals sigma in
let prev_principal_goal = Evd.principal_future_goal sigma in
(** Create the refinement term *)
- let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
+ 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
(** Check that the introduced evars are well-typed *)
@@ -92,10 +93,18 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
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 ()) >>= fun () ->
- Proofview.Unsafe.tclEVARS sigma >>= fun () ->
- Proofview.Unsafe.tclSETGOALS comb
-end }
+ Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Proofview.Unsafe.tclSETGOALS comb <*>
+ Proofview.tclUNIT v
+ }
+
+let refine_one ?(unsafe = true) f =
+ Proofview.Goal.enter_one (make_refine_enter ~unsafe f)
+
+let refine ?(unsafe = true) f =
+ let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in
+ Proofview.Goal.enter (make_refine_enter ~unsafe f)
(** Useful definitions *)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index a9798b7040..3d140f036b 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -30,6 +30,9 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
tactic failures. If [unsafe] is [false] (default is [true]) [t] is
type-checked beforehand. *)
+val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+(** A generalization of [refine] which assumes exactly one goal under focus *)
+
(** {7 Helper functions} *)
val with_type : Environ.env -> Evd.evar_map ->
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index ba22db0830..2b129ad89c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -121,15 +121,11 @@ let internal_cut_rev_no_check replace id t gl =
let refine_no_check c gl =
refiner (Refine c) gl
-let move_hyp_no_check id1 id2 gl =
- refiner (Move (id1,id2)) gl
-
(* Versions with consistency checks *)
let internal_cut b d t = with_check (internal_cut_no_check b d t)
let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
let refine c = with_check (refine_no_check c)
-let move_hyp id id' = with_check (move_hyp_no_check id id')
(* Pretty-printers *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 100ed1522e..727efcf6dc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -92,7 +92,6 @@ val refine_no_check : constr -> tactic
val internal_cut : bool -> Id.t -> types -> tactic
val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
-val move_hyp : Id.t -> Id.t move_location -> tactic
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : goal sigma -> Pp.std_ppcmds
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:17:56 +0000