aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml6
-rw-r--r--proofs/clenvtac.ml28
-rw-r--r--proofs/evar_refiner.ml8
-rw-r--r--proofs/logic.ml22
-rw-r--r--proofs/logic.mli3
-rw-r--r--proofs/pfedit.ml58
-rw-r--r--proofs/pfedit.mli6
-rw-r--r--proofs/proof.ml37
-rw-r--r--proofs/proof_global.ml36
-rw-r--r--proofs/proof_type.mli1
-rw-r--r--proofs/redexpr.ml26
-rw-r--r--proofs/refine.ml56
-rw-r--r--proofs/refine.mli8
-rw-r--r--proofs/refiner.ml18
-rw-r--r--proofs/tacmach.ml21
-rw-r--r--proofs/tacmach.mli14
16 files changed, 231 insertions, 117 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 853410db8b..0a90e0dbd3 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -72,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
exception NotExtensibleClause
let clenv_push_prod cl =
- let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
+ let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
let rec clrec typ = match kind_of_term typ with
| Cast (t,_,_) -> clrec t
| Prod (na,t,u) ->
@@ -663,7 +663,7 @@ let evar_of_binder holes = function
try
let h = List.nth holes (pred n) in
h.hole_evar
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
errorlabstrm "" (str "No such binder.")
let define_with_type sigma env ev c =
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index da2eee32a2..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
@@ -125,5 +145,5 @@ let unify ?(flags=fail_quick_unif_flags) m =
try
let evd' = w_unify env evd CONV ~flags m n in
Proofview.Unsafe.tclEVARSADVANCE evd'
- with e when Errors.noncritical e -> Proofview.tclZERO e
+ with e when CErrors.noncritical e -> Proofview.tclZERO e
end }
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3192a6a29a..29cad06352 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Evd
@@ -46,16 +46,16 @@ 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
try Pretyping.understand_ltac flags
env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let loc = Glob_ops.loc_of_glob_constr rawc in
user_err_loc
(loc,"", str "Instance is not well-typed in the environment of " ++
- str (string_of_existential evk))
+ pr_existential_key sigma evk ++ str ".")
in
define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index fd8a70c650..65497c80dd 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -59,7 +59,7 @@ let is_unification_error = function
| _ -> false
let catchable_exception = function
- | Errors.UserError _ | TypeError _
+ | CErrors.UserError _ | TypeError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _
(* reduction errors *)
@@ -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
+
(**********************************************************************)
@@ -463,7 +468,7 @@ and mk_hdgoals sigma goal goalacc trm =
and mk_arggoals sigma goal goalacc funty allargs =
let foldmap (goalacc, funty, sigma) harg =
- let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in
+ let t = whd_all (Goal.V82.env sigma goal) sigma funty in
let rec collapse t = match kind_of_term t with
| LetIn (_, c1, _, b) -> collapse (subst1 c1 b)
| _ -> t
@@ -533,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
@@ -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 bf1da8ac05..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
@@ -39,7 +50,7 @@ let cook_this_proof p =
match p with
| { Proof_global.id;entries=[constr];persistence;universes } ->
(id,(constr,universes,persistence))
- | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
+ | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
let cook_proof () =
cook_this_proof (fst
@@ -59,9 +70,9 @@ let get_universe_binders () =
Proof_global.get_universe_binders ()
exception NoSuchGoal
-let _ = Errors.register_handler begin function
- | NoSuchGoal -> Errors.error "No such goal."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | NoSuchGoal -> CErrors.error "No such goal."
+ | _ -> raise CErrors.Unhandled
end
let get_nth_V82_goal i =
let p = Proof_global.give_me_the_proof () in
@@ -76,12 +87,12 @@ let get_goal_context_gen i =
let get_goal_context i =
try get_goal_context_gen i
- with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
- | NoSuchGoal -> Errors.error "No such goal."
+ with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+ | NoSuchGoal -> CErrors.error "No such goal."
let get_current_goal_context () =
try get_goal_context_gen 1
- with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+ with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
| NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
there is no accessible evar either *)
@@ -102,7 +113,7 @@ let get_current_context () =
let current_proof_statement () =
match Proof_global.V82.get_current_initial_conclusions () with
| (id,([concl],strength)) -> id,strength,concl
- | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
+ | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement")
let solve ?with_end_tac gi info_lvl tac pr =
try
@@ -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
@@ -127,11 +143,11 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
(p,status)
with
- | Proof_global.NoCurrentProof -> Errors.error "No focused proof"
+ | Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
| CList.IndexOutOfRange ->
match gi with
| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
- Errors.errorlabstrm "" msg
+ CErrors.errorlabstrm "" msg
| _ -> assert false
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -157,15 +173,16 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
delete_current_proof ();
const, status, fst univs
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
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
@@ -188,7 +205,7 @@ let refine_by_tactic env sigma ty tac =
try Proof.run_tactic env tac prf
with Logic_monad.TacticFailure e as src ->
(** Catch the inner error of the monad tactic *)
- let (_, info) = Errors.push src in
+ let (_, info) = CErrors.push src in
iraise (e, info)
in
(** Plug back the retrieved sigma *)
@@ -215,7 +232,7 @@ let refine_by_tactic env sigma ty tac =
(* Support for resolution of evars in tactic interpretation, including
resolution by application of tactics *)
-let implicit_tactic = ref None
+let implicit_tactic = Summary.ref None ~name:"implicit-tactic"
let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -228,10 +245,13 @@ let solve_by_implicit_tactic env sigma evk =
when
Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
(Environ.named_context env) ->
- let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in
+ let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
(try
- let (ans, _, _) =
- build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in
- ans
+ let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+ if Evarutil.has_undefined_evars sigma c then raise Exit;
+ let (ans, _, ctx) =
+ build_by_tactic env (Evd.evar_universe_context sigma) c tac in
+ 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 86af420dc4..5c963d53e7 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -64,17 +64,17 @@ exception NoSuchGoals of int * int
exception FullyUnfocused
-let _ = Errors.register_handler begin function
+let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- Errors.error "This proof is focused, but cannot be unfocused this way"
+ CErrors.error "This proof is focused, but cannot be unfocused this way"
| NoSuchGoals (i,j) when Int.equal i j ->
- Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+ CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
- Errors.errorlabstrm "Focus" Pp.(
+ CErrors.errorlabstrm "Focus" Pp.(
str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
)
- | FullyUnfocused -> Errors.error "The proof is not focused"
- | _ -> raise Errors.Unhandled
+ | FullyUnfocused -> CErrors.error "The proof is not focused"
+ | _ -> raise CErrors.Unhandled
end
let check_cond_kind c k =
@@ -300,12 +300,12 @@ exception UnfinishedProof
exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
-let _ = Errors.register_handler begin function
- | UnfinishedProof -> Errors.error "Some goals have not been solved."
- | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf."
- | HasGivenUpGoals -> Errors.error "Some goals have been given up."
- | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | UnfinishedProof -> CErrors.error "Some goals have not been solved."
+ | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
+ | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
+ | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+ | _ -> raise CErrors.Unhandled
end
let return p =
@@ -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)
@@ -397,9 +404,9 @@ module V82 = struct
let evl = Evarutil.non_instantiated sigma in
let evl = Evar.Map.bindings evl in
if (n <= 0) then
- Errors.error "incorrect existential variable index"
+ CErrors.error "incorrect existential variable index"
else if CList.length evl < n then
- Errors.error "not so many uninstantiated existential variables"
+ CErrors.error "not so many uninstantiated existential variables"
else
CList.nth evl (n-1)
in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 61fe347504..7605f63872 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -34,7 +34,7 @@ let proof_modes = Hashtbl.create 6
let find_proof_mode n =
try Hashtbl.find proof_modes n
with Not_found ->
- Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
+ CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
let register_proof_mode ({name = n} as m) =
Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -122,15 +122,15 @@ let push a l = l := a::!l;
update_proof_mode ()
exception NoSuchProof
-let _ = Errors.register_handler begin function
- | NoSuchProof -> Errors.error "No such proof."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | NoSuchProof -> CErrors.error "No such proof."
+ | _ -> raise CErrors.Unhandled
end
exception NoCurrentProof
-let _ = Errors.register_handler begin function
- | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
- | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+ | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+ | _ -> raise CErrors.Unhandled
end
(*** Proof Global manipulation ***)
@@ -190,7 +190,7 @@ let check_no_pending_proof () =
if not (there_are_pending_proofs ()) then
()
else begin
- Errors.error (Pp.string_of_ppcmds
+ CErrors.error (Pp.string_of_ppcmds
(str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
str"Use \"Abort All\" first or complete proof(s)."))
end
@@ -202,7 +202,7 @@ let discard (loc,id) =
let n = List.length !pstates in
discard_gen id;
if Int.equal (List.length !pstates) n then
- Errors.user_err_loc
+ CErrors.user_err_loc
(loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
let discard_current () =
@@ -296,7 +296,7 @@ let set_used_variables l =
| [] -> raise NoCurrentProof
| p :: rest ->
if not (Option.is_empty p.section_vars) then
- Errors.error "Used section variables can be declared only once";
+ CErrors.error "Used section variables can be declared only once";
pstates := { p with section_vars = Some ctx} :: rest;
ctx, to_clear
@@ -408,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
let evd =
let error s =
let prf = str " (in proof " ++ Id.print pid ++ str ")" in
- raise (Errors.UserError("last tactic before Qed",s ++ prf))
+ raise (CErrors.UserError("last tactic before Qed",s ++ prf))
in
try Proof.return proof with
| Proof.UnfinishedProof ->
@@ -515,12 +515,12 @@ module Bullet = struct
exception FailedBullet of t * suggestion
let _ =
- Errors.register_handler
+ CErrors.register_handler
(function
| FailedBullet (b,sugg) ->
let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
- Errors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
- | _ -> raise Errors.Unhandled)
+ CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+ | _ -> raise CErrors.Unhandled)
(* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
@@ -633,7 +633,7 @@ module Bullet = struct
current_behavior :=
try Hashtbl.find behaviors n
with Not_found ->
- Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+ CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
end
}
@@ -681,9 +681,9 @@ let parse_goal_selector = function
let err_msg = "The default selector must be \"all\" or a natural number." in
begin try
let i = int_of_string i in
- if i < 0 then Errors.error err_msg;
+ if i < 0 then CErrors.error err_msg;
Vernacexpr.SelectNth i
- with Failure _ -> Errors.error err_msg
+ with Failure _ -> CErrors.error err_msg
end
let _ =
@@ -712,7 +712,7 @@ type state = pstate list
let freeze ~marshallable =
match marshallable with
| `Yes ->
- Errors.anomaly (Pp.str"full marshalling of proof state not supported")
+ CErrors.anomaly (Pp.str"full marshalling of proof state not supported")
| `Shallow -> !pstates
| `No -> !pstates
let unfreeze s = pstates := s; update_proof_mode ()
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 13b5848a33..72cb05f1b6 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -17,7 +17,7 @@ open Genredexpr
open Pattern
open Reductionops
open Tacred
-open Closure
+open CClosure
open RedFlags
open Libobject
open Misctypes
@@ -29,17 +29,22 @@ let cbv_vm env sigma c =
error "vm_compute does not support existential variables.";
Vnorm.cbv_vm env c ctyp
+let warn_native_compute_disabled =
+ CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
+ (fun () ->
+ strbrk "native_compute disabled at configure time; falling back to vm_compute.")
+
let cbv_native env sigma c =
if Coq_config.no_native_compiler then
- let () = Feedback.msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
- cbv_vm env sigma c
+ (warn_native_compute_disabled ();
+ cbv_vm env sigma c)
else
let ctyp = Retyping.get_type_of env sigma c in
Nativenorm.native_norm env sigma c ctyp
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 =
@@ -141,7 +146,9 @@ let make_flag_constant = function
let make_flag env f =
let red = no_red in
let red = if f.rBeta then red_add red fBETA else red in
- let red = if f.rIota then red_add red fIOTA else red in
+ let red = if f.rMatch then red_add red fMATCH else red in
+ let red = if f.rFix then red_add red fFIX else red in
+ let red = if f.rCofix then red_add red fCOFIX else red in
let red = if f.rZeta then red_add red fZETA else red in
let red =
if f.rDelta then (* All but rConst *)
@@ -209,6 +216,11 @@ let contextualize f g = function
e_red (contextually b (l,c) (fun _ -> h))
| None -> e_red g
+let warn_simpl_unfolding_modifiers =
+ CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
+ (fun () ->
+ Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
+
let reduction_of_red_expr env =
let make_flag = make_flag env in
let rec reduction_of_red_expr = function
@@ -221,7 +233,7 @@ let reduction_of_red_expr env =
let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
let () =
if not (!simplIsCbn || List.is_empty f.rConst) then
- Feedback.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+ warn_simpl_unfolding_modifiers () in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
| Cbn f ->
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 76e2d7dc53..3f55270609 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -51,7 +51,25 @@ 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 ->
+(* 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
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
@@ -62,9 +80,13 @@ 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
+ (** 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
@@ -91,11 +113,20 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
(** Select the goals *)
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"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 }
+ 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
+ }
+
+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 *)
@@ -118,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 a9798b7040..a44632eff5 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 ->
@@ -40,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/refiner.ml b/proofs/refiner.ml
index 23433692cd..ea8543b02f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Evd
open Environ
@@ -221,7 +221,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
Feedback.msg_notice
(str (emacs_str "<infoH>")
++ (hov 0 (str s))
- ++ (str (emacs_str "</infoH>")) ++ fnl());
+ ++ (str (emacs_str "</infoH>")));
tclIDTAC goal;;
@@ -240,8 +240,8 @@ let tclORELSE0 t1 t2 g =
try
t1 g
with (* Breakpoint *)
- | e when Errors.noncritical e ->
- let e = Errors.push e in catch_failerror e; t2 g
+ | e when CErrors.noncritical e ->
+ let e = CErrors.push e in catch_failerror e; t2 g
(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
then applies t2 *)
@@ -253,8 +253,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
let tclORELSE_THEN t1 t2then t2else gls =
match
try Some(tclPROGRESS t1 gls)
- with e when Errors.noncritical e ->
- let e = Errors.push e in catch_failerror e; None
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in catch_failerror e; None
with
| None -> t2else gls
| Some sgl ->
@@ -284,12 +284,12 @@ let ite_gen tcal tac_if continue tac_else gl=
try
tac_else gl
with
- e' when Errors.noncritical e' -> iraise e in
+ e' when CErrors.noncritical e' -> iraise e in
try
tcal tac_if0 continue gl
with (* Breakpoint *)
- | e when Errors.noncritical e ->
- let e = Errors.push e in catch_failerror e; tac_else0 e gl
+ | e when CErrors.noncritical e ->
+ let e = CErrors.push e in catch_failerror e; tac_else0 e gl
(* Try the first tactic and, if it succeeds, continue with
the second one, and if it fails, use the third one *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8c0b4ba98a..330594af5c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,7 +84,7 @@ let pf_eapply f gls x =
let pf_reduce = pf_apply
let pf_e_reduce = pf_apply
-let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota
+let pf_whd_all = pf_reduce whd_all
let pf_hnf_constr = pf_reduce hnf_constr
let pf_nf = pf_reduce simpl
let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota)
@@ -101,7 +101,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env)
let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind
-let pf_hnf_type_of gls = pf_whd_betadeltaiota gls % pf_get_type_of gls
+let pf_hnf_type_of gls = pf_whd_all gls % pf_get_type_of gls
let pf_is_matching = pf_apply Constr_matching.is_matching_conv
let pf_matches = pf_apply Constr_matching.matches_conv
@@ -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 *)
@@ -175,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
@@ -191,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
@@ -219,7 +218,7 @@ module New = struct
let sigma = project gl in
nf_evar sigma concl
- let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+ let pf_whd_all gl t = pf_apply whd_all gl t
let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
@@ -228,11 +227,11 @@ module New = struct
let pf_hnf_constr gl t = pf_apply hnf_constr gl t
let pf_hnf_type_of gl t =
- pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+ pf_whd_all gl (pf_get_type_of gl t)
let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
- let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+ let pf_whd_all gl t = pf_apply whd_all gl t
let pf_compute gl t = pf_apply compute gl t
let pf_nf_evar gl t = nf_evar (project gl) t
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 182433cb3a..59f296f64e 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -63,7 +63,7 @@ val pf_e_reduce :
(env -> evar_map -> constr -> evar_map * constr) ->
goal sigma -> constr -> evar_map * constr
-val pf_whd_betadeltaiota : goal sigma -> constr -> constr
+val pf_whd_all : goal sigma -> constr -> constr
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
val pf_nf_betaiota : goal sigma -> constr -> constr
@@ -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
@@ -109,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
@@ -127,7 +135,7 @@ module New : sig
val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
- val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr
+ val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr
val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 18:48:04 +0000