aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r--tactics/tactics.ml142
1 files changed, 74 insertions, 68 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d0ec3358a..58c62af85 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -128,14 +128,14 @@ let unsafe_intro env store decl b =
(sigma, mkNamedLambda_or_LetIn decl ev)
end
-let introduction ?(check=true) id =
+let introduction id =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let hyps = named_context_val (Proofview.Goal.env gl) in
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
- let () = if check && mem_named_context_val id hyps then
+ let () = if mem_named_context_val id hyps then
user_err ~hdr:"Tactics.introduction"
(str "Variable " ++ Id.print id ++ str " is already declared.")
in
@@ -198,32 +198,40 @@ end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+ | None -> mt ()
+ | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- Id.print id ++ str " is used in conclusion."
+ Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+ Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_clear_dependency env sigma id err =
- user_err (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+ user_err (clear_dependency_msg env sigma id err inglobal)
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
str "Cannot change " ++ Id.print id ++
- strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_replacing_dependency env sigma id err =
- user_err (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+ user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -239,13 +247,12 @@ let clear_gen fail = function
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
- let evdref = ref sigma in
- let (hyps, concl) =
- try clear_hyps_in_evi env evdref (named_context_val env) concl ids
- with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ let (sigma, hyps, concl) =
+ try clear_hyps_in_evi env sigma (named_context_val env) concl ids
+ with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
in
let env = reset_with_named_context hyps env in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun sigma ->
Evarutil.new_evar env sigma ~principal:true concl
end)
@@ -423,11 +430,10 @@ let get_previous_hyp_position env sigma id =
let clear_hyps2 env sigma ids sign t cl =
try
- let evdref = ref (Evd.clear_metas sigma) in
- let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
- (hyps, t, cl, !evdref)
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency env sigma id err
+ let sigma = Evd.clear_metas sigma in
+ Evarutil.clear_hyps2_in_evi env sigma sign t cl ids
+ with Evarutil.ClearDependencyError (id,err,inglobal) ->
+ error_replacing_dependency env sigma id err inglobal
let internal_cut_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
@@ -439,7 +445,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
let sign',t,concl,sigma =
if replace then
let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
- let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
+ let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in
sign',t,concl,sigma
else
@@ -557,15 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
end
end
-let fix ido n = match ido with
- | None ->
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_fix id n [] 0
- end
- | Some id ->
- mutual_fix id n [] 0
+let fix id n = mutual_fix id n [] 0
let rec check_is_mutcoind env sigma cl =
let b = whd_all env sigma cl in
@@ -608,15 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl ->
end
end
-let cofix ido = match ido with
- | None ->
- Proofview.Goal.enter begin fun gl ->
- let name = Proof_global.get_current_proof_name () in
- let id = new_fresh_id Id.Set.empty name gl in
- mutual_cofix id [] 0
- end
- | Some id ->
- mutual_cofix id [] 0
+let cofix id = mutual_cofix id [] 0
(**************************************************************)
(* Reduction and conversion tactics *)
@@ -965,6 +955,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
| LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
let name = find_name false (LocalDef (name,b,t)) name_flag gl in
build_intro_tac name move_flag tac
+ | Evar ev when force_flag ->
+ let sigma, t = Evardefine.define_evar_as_product sigma ev in
+ Tacticals.New.tclTHEN
+ (Proofview.Unsafe.tclEVARS sigma)
+ (intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
@@ -1258,7 +1253,6 @@ let cut c =
end
let error_uninstantiated_metas t clenv =
- let t = EConstr.Unsafe.to_constr t in
let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.")
in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".")
@@ -1268,7 +1262,7 @@ let check_unresolved_evars_of_metas sigma clenv =
(* Refiner.pose_all_metas_as_evars are resolved *)
List.iter (fun (mv,b) -> match b with
| Clval (_,(c,_),_) ->
- (match Constr.kind c.rebus with
+ (match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with
| Evar (evk,_) when Evd.is_undefined clenv.evd evk
&& not (Evd.mem sigma evk) ->
error_uninstantiated_metas (mkMeta mv) clenv
@@ -1445,9 +1439,7 @@ let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations
let find_ind_eliminator ind s gl =
let gr = lookup_eliminator ind s in
- let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in
- let c = EConstr.of_constr c in
- evd, c
+ Tacmach.New.pf_apply Evd.fresh_global gl gr
let find_eliminator c gl =
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
@@ -1918,8 +1910,8 @@ let cast_no_check cast c =
exact_no_check (mkCast (c, cast, concl))
end
-let vm_cast_no_check c = cast_no_check Term.VMcast c
-let native_cast_no_check c = cast_no_check Term.NATIVEcast c
+let vm_cast_no_check c = cast_no_check VMcast c
+let native_cast_no_check c = cast_no_check NATIVEcast c
let exact_proof c =
let open Tacmach.New in
@@ -1971,24 +1963,22 @@ let on_the_bodies = function
exception DependsOnBody of Id.t option
let check_is_type env sigma ty =
- let evdref = ref sigma in
try
- let _ = Typing.e_sort_of env evdref ty in
- !evdref
+ let sigma, _ = Typing.sort_of env sigma ty in
+ sigma
with e when CErrors.noncritical e ->
raise (DependsOnBody None)
let check_decl env sigma decl =
let open Context.Named.Declaration in
let ty = NamedDecl.get_type decl in
- let evdref = ref sigma in
try
- let _ = Typing.e_sort_of env evdref ty in
- let _ = match decl with
- | LocalAssum _ -> ()
- | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
+ let sigma, _ = Typing.sort_of env sigma ty in
+ let sigma = match decl with
+ | LocalAssum _ -> sigma
+ | LocalDef (_,c,_) -> Typing.check env sigma c ty
in
- !evdref
+ sigma
with e when CErrors.noncritical e ->
let id = NamedDecl.get_id decl in
raise (DependsOnBody (Some id))
@@ -2612,9 +2602,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
- let eq = EConstr.of_constr eq in
let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
- let refl = EConstr.of_constr refl in
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in
@@ -2668,9 +2656,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
- let eq = EConstr.of_constr eq in
let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in
- let refl = EConstr.of_constr refl in
let eq = applist (eq,args) in
let refl = applist (refl, [t;mkVar id]) in
let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
@@ -3008,8 +2994,24 @@ let unfold_body x =
end
end
+let warn_cannot_remove_as_expected =
+ CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+ (fun (id,inglobal) ->
+ let pp = match inglobal with
+ | None -> mt ()
+ | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+ str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+ Proofview.tclORELSE
+ (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+ (function
+ | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+ | e -> iraise e)
+
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+ Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
(*****************************)
(* High-level induction *)
@@ -3425,7 +3427,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
type elim_scheme = {
elimc: constr with_bindings option;
elimt: types;
- indref: global_reference option;
+ indref: GlobRef.t option;
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
nparams: int; (* number of parameters *)
predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
@@ -3787,7 +3789,10 @@ let specialize_eqs id =
let ty = Tacmach.New.pf_get_hyp_typ id gl in
let evars = ref (Proofview.Goal.sigma gl) in
let unif env evars c1 c2 =
- compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2
+ compare_upto_variables !evars c1 c2 &&
+ (match Evarconv.conv env !evars c1 c2 with
+ | Some sigma -> evars := sigma; true
+ | None -> false)
in
let rec aux in_eqs ctx acc ty =
match EConstr.kind !evars ty with
@@ -3812,7 +3817,8 @@ let specialize_eqs id =
| _ ->
if in_eqs then acc, in_eqs, ctx, ty
else
- let e = e_new_evar (push_rel_context ctx env) evars t in
+ let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
+ evars := sigma;
aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
| t -> acc, in_eqs, ctx, ty
in
@@ -4339,7 +4345,7 @@ let check_expected_type env sigma (elimc,bl) elimt =
let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
let sigma = solve_evar_clause env sigma true cl bl in
let (_,u,_) = destProd sigma cl.cl_concl in
- fun t -> Evarconv.e_cumul env (ref sigma) t u
+ fun t -> Option.has_some (Evarconv.cumul env sigma t u)
let check_enough_applied env sigma elim =
(* A heuristic to decide whether the induction arg is enough applied *)
@@ -4930,9 +4936,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let evd, ctx, concl =
(* FIXME: should be done only if the tactic succeeds *)
- let evd, nf = nf_evars_and_universes !evdref in
+ let evd = Evd.minimize_universes !evdref in
let ctx = Evd.universe_context_set evd in
- evd, ctx, nf concl
+ evd, ctx, Evarutil.nf_evars_universes evd concl
in
let concl = EConstr.of_constr concl in
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 17:42:45 +0000