summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /tactics
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml54
-rw-r--r--tactics/auto.mli9
-rw-r--r--tactics/autorewrite.ml15
-rw-r--r--tactics/class_tactics.ml67
-rw-r--r--tactics/contradiction.ml6
-rw-r--r--tactics/eauto.ml478
-rw-r--r--tactics/elim.ml4
-rw-r--r--tactics/elimschemes.ml26
-rw-r--r--tactics/eqdecide.ml46
-rw-r--r--tactics/eqschemes.ml27
-rw-r--r--tactics/eqschemes.mli4
-rw-r--r--tactics/equality.ml143
-rw-r--r--tactics/equality.mli2
-rw-r--r--tactics/extratactics.ml427
-rw-r--r--tactics/hints.ml292
-rw-r--r--tactics/hints.mli39
-rw-r--r--tactics/hipattern.ml42
-rw-r--r--tactics/inv.ml6
-rw-r--r--tactics/leminv.ml7
-rw-r--r--tactics/rewrite.ml350
-rw-r--r--tactics/rewrite.mli5
-rw-r--r--tactics/tacenv.ml46
-rw-r--r--tactics/tacenv.mli16
-rw-r--r--tactics/tacintern.ml29
-rw-r--r--tactics/tacinterp.ml53
-rw-r--r--tactics/tactic_matching.mli4
-rw-r--r--tactics/tacticals.ml26
-rw-r--r--tactics/tactics.ml377
-rw-r--r--tactics/tactics.mli1
-rw-r--r--tactics/tauto.ml44
-rw-r--r--tactics/term_dnet.ml4
31 files changed, 1079 insertions, 690 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46274f83..a6b53d76 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -72,27 +72,44 @@ let auto_flags_of_state st =
(* Try unification with the precompiled clause, then use registered Apply *)
-let unify_resolve_nodelta poly (c,clenv) =
+let connect_hint_clenv poly (c, _, ctx) clenv gl =
+ (** [clenv] has been generated by a hint-making function, so the only relevant
+ data in its evarmap is the set of metas. The [evar_reset_evd] function
+ below just replaces the metas of sigma by those coming from the clenv. *)
+ let sigma = Proofview.Goal.sigma gl in
+ let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
+ (** Still, we need to update the universes *)
+ let clenv, c =
+ if poly then
+ (** Refresh the instance of the hint *)
+ let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in
+ let map c = Vars.subst_univs_level_constr subst c in
+ let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ let clenv = { clenv with evd = evd ; env = Proofview.Goal.env gl } in
+ (** FIXME: We're being inefficient here because we substitute the whole
+ evar map instead of just its metas, which are the only ones
+ mentioning the old universes. *)
+ Clenv.map_clenv map clenv, map c
+ else
+ let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
+ in clenv, c
+
+let unify_resolve poly flags ((c : raw_hint), clenv) =
Proofview.Goal.nf_enter begin fun gl ->
- let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
- let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
- let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags:auto_unif_flags clenv' gl) gl in
- Clenvtac.clenv_refine false clenv''
+ let clenv, c = connect_hint_clenv poly c clenv gl in
+ let clenv = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv gl) gl in
+ Clenvtac.clenv_refine false clenv
end
-let unify_resolve poly flags (c,clenv) =
- Proofview.Goal.nf_enter begin fun gl ->
- let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
- let clenv' = Tacmach.New.of_old connect_clenv gl clenv' in
- let clenv'' = Tacmach.New.of_old (fun gl -> clenv_unique_resolver ~flags clenv' gl) gl in
- Clenvtac.clenv_refine false clenv''
- end
+let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
let unify_resolve_gen poly = function
| None -> unify_resolve_nodelta poly
| Some flags -> unify_resolve poly flags
let exact poly (c,clenv) =
+ let (c, _, _) = c in
let ctx, c' =
if poly then
let evd', subst = Evd.refresh_undefined_universes clenv.evd in
@@ -131,7 +148,7 @@ let conclPattern concl pat tac =
try
Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
with Constr_matching.PatternMatchingFailure ->
- Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
+ Tacticals.New.tclZEROMSG (str "conclPattern")
in
Proofview.Goal.enter (fun gl ->
let env = Proofview.Goal.env gl in
@@ -309,7 +326,8 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
let hyp = Context.map_named_declaration nf decl in
let hintl = make_resolve_hyp env sigma hyp
- in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
+ in trivial_fail_db dbg mod_delta db_list
+ (Hint_db.add_list env sigma hintl local_db)
end)
in
Proofview.Goal.enter begin fun gl ->
@@ -377,7 +395,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
| Extern tacast ->
conclPattern concl p tacast
in
- tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic)
+ tclLOG dbg (fun () -> pr_hint t) (run_hint t tactic)
and trivial_resolve dbg mod_delta db_list local_db cl =
try
@@ -438,7 +456,9 @@ let possible_resolve dbg mod_delta db_list local_db cl =
with Not_found -> []
let extend_local_db decl db gl =
- Hint_db.add_list (make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) decl) db
+ let env = Tacmach.New.pf_env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db
(* Introduce an hypothesis, then call the continuation tactic [kont]
with the hint db extended with the so-obtained hypothesis *)
@@ -458,7 +478,7 @@ let search d n mod_delta db_list local_db =
(* spiwack: the test of [n] to 0 must be done independently in
each goal. Hence the [tclEXTEND] *)
Proofview.tclEXTEND [] begin
- if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
+ if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
Tacticals.New.tclORELSE0 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
( Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0cc8a0b1..cae180ce 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -19,16 +19,19 @@ val extern_interp :
(** Auto and related automation tactics *)
-val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
+val priority : ('a * full_hint) list -> ('a * full_hint) list
val default_search_depth : int ref
val auto_flags_of_state : transparent_state -> Unification.unify_flags
+val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
+ [ `NF ] Proofview.Goal.t -> clausenv * constr
+
(** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> unit Proofview.tactic
+val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
-val unify_resolve : polymorphic -> Unification.unify_flags -> (constr * clausenv) -> unit Proofview.tactic
+val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
(** [ConclPattern concl pat tacast]:
if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4eb8a792..3a9d40de 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -66,7 +66,7 @@ let find_base bas =
try raw_find_base bas
with Not_found ->
errorlabstrm "AutoRewrite"
- (str ("Rewriting base "^(bas)^" does not exist."))
+ (str "Rewriting base " ++ str bas ++ str " does not exist.")
let find_rewrites bas =
List.rev_map snd (HintDN.find_all (find_base bas))
@@ -174,7 +174,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
if cl.concl_occs != AllOccurrences &&
cl.concl_occs != NoOccurrences
then
- Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic."))
+ Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
else
let compose_tac t1 t2 =
match cl.onhyps with
@@ -204,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
*)
gen_auto_multi_rewrite conds tac_main lbas cl
| _ ->
- Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion."))
+ Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
(* Functions necessary to the library object declaration *)
let cache_hintrewrite (_,(rbase,lrl)) =
@@ -263,7 +263,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
try
let others,(c1,c2) = split_last_two args in
let ty1, ty2 =
- Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2
+ Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2
in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
@@ -281,7 +281,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| None -> None
let find_applied_relation metas loc env sigma c left2right =
- let ctype = Typing.type_of env sigma c in
+ let ctype = Typing.unsafe_type_of env sigma c in
match decompose_applied_relation metas env sigma c ctype left2right with
| Some c -> c
| None ->
@@ -292,10 +292,13 @@ let find_applied_relation metas loc env sigma c left2right =
(* To add rewriting rules to a base *)
let add_rew_rules base lrul =
let counter = ref 0 in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
let lrul =
List.fold_left
(fun dn (loc,(c,ctx),b,t) ->
- let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in
+ let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
+ let info = find_applied_relation false loc env sigma c b in
let pat = if b then info.hyp_left else info.hyp_right in
let rul = { rew_lemma = c; rew_type = info.hyp_ty;
rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e11458c0..f3a48634 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -141,6 +141,7 @@ let progress_evars t =
let e_give_exact flags poly (c,clenv) gl =
+ let (c, _, _) = c in
let c, gl =
if poly then
let clenv', subst = Clenv.refresh_undefined_univs clenv in
@@ -149,36 +150,35 @@ let e_give_exact flags poly (c,clenv) gl =
c, {gl with sigma = clenv'.evd}
else c, gl
in
- let t1 = pf_type_of gl c in
+ let t1 = pf_unsafe_type_of gl c in
tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
let unify_e_resolve poly flags (c,clenv) gls =
- let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
- let clenv' = connect_clenv gls clenv' in
- let clenv' = clenv_unique_resolver ~flags clenv' gls in
- Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
+ let clenv', c = connect_hint_clenv poly c clenv gls in
+ let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+ Clenvtac.clenv_refine true ~with_classes:false clenv'
let unify_resolve poly flags (c,clenv) gls =
- let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
- let clenv' = connect_clenv gls clenv' in
- let clenv' = clenv_unique_resolver ~flags clenv' gls in
- Proofview.V82.of_tactic
- (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
+ let clenv', _ = connect_hint_clenv poly c clenv gls in
+ let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+ Clenvtac.clenv_refine false ~with_classes:false clenv'
-let clenv_of_prods poly nprods (c, clenv) gls =
+let clenv_of_prods poly nprods (c, clenv) gl =
+ let (c, _, _) = c in
if poly || Int.equal nprods 0 then Some clenv
else
- let ty = pf_type_of gls c in
+ let ty = Tacmach.New.pf_unsafe_type_of gl c in
let diff = nb_prod ty - nprods in
if Pervasives.(>=) diff 0 then
(* Was Some clenv... *)
- Some (mk_clenv_from_n gls (Some diff) (c,ty))
+ Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
else None
-let with_prods nprods poly (c, clenv) f gls =
- match clenv_of_prods poly nprods (c, clenv) gls with
- | None -> tclFAIL 0 (str"Not enough premisses") gls
- | Some clenv' -> f (c, clenv') gls
+let with_prods nprods poly (c, clenv) f =
+ Proofview.Goal.nf_enter (fun gl ->
+ match clenv_of_prods poly nprods (c, clenv) gl with
+ | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+ | Some clenv' -> f (c, clenv') gl)
(** Hack to properly solve dependent evars that are typeclasses *)
@@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal =
let d = pf_last_hyp g' in
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db db_list
- (Hint_db.add_list hintl local_db) g'))) ::
+ (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
(List.map (fun (x,_,_,_,_) -> x)
(e_trivial_resolve db_list local_db (project goal) (pf_concl goal)))
in
@@ -205,7 +205,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
if cl.cl_strict then
Evd.evars_of_term concl
else Evar.Set.empty
- with _ -> Evar.Set.empty
+ with e when Errors.noncritical e -> Evar.Set.empty
in
let hintl =
List.map_append
@@ -222,22 +222,23 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
let tac_of_hint =
fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
let tac = function
- | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
- | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+ | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
+ | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
| Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
| Res_pf_THEN_trivial_fail (term,cl) ->
- Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
- (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+ Proofview.V82.tactic (tclTHEN
+ (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags))))
+ (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
| Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
| Extern tacast -> conclPattern concl p tacast
in
- let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
+ let tac = Proofview.V82.of_tactic (run_hint t tac) in
let tac = if complete then tclCOMPLETE tac else tac in
- match repr_auto_tactic t with
- | Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+ match repr_hint t with
+ | Extern _ -> (tac,b,true, name, lazy (pr_hint t))
| _ ->
(* let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
- (tac,b,false, name, lazy (pr_autotactic t))
+ (tac,b,false, name, lazy (pr_hint t))
in List.map tac_of_hint hintl
and e_trivial_resolve db_list local_db sigma concl =
@@ -339,7 +340,7 @@ let make_hints g st only_classes sign =
(PathOr (paths, path), hint @ hints)
else (paths, hints))
(PathEmpty, []) sign
- in Hint_db.add_list hintlist (Hint_db.empty st true)
+ in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
let make_autogoal_hints =
let cache = ref (true, Environ.empty_named_context_val,
@@ -374,7 +375,7 @@ let intro_tac : atac =
let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
(true,false,false) info.only_classes None (List.hd context) in
- let ldb = Hint_db.add_list hint info.hints in
+ let ldb = Hint_db.add_list env s hint info.hints in
(g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
in {it = gls'; sigma = s;})
@@ -397,7 +398,7 @@ let is_unique env concl =
try
let (cl,u), args = dest_class_app env concl in
cl.cl_unique
- with _ -> false
+ with e when Errors.noncritical e -> false
let needs_backtrack env evd oev concl =
if Option.is_empty oev || is_Prop env evd concl then
@@ -490,6 +491,7 @@ let hints_tac hints =
let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
let rec aux s (acc : autogoal list list) fk = function
| (gl,info) :: gls ->
+ Control.check_for_interrupt ();
(match info.is_evar with
| Some ev when Evd.is_defined s ev -> aux s acc fk gls
| _ ->
@@ -842,6 +844,7 @@ let is_ground c gl =
let autoapply c i gl =
let flags = auto_unif_flags Evar.Set.empty
(Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
- let cty = pf_type_of gl c in
+ let cty = pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
- unify_e_resolve false flags (c,ce) gl
+ let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in
+ Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9b69481d..22f218b4 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -55,7 +55,7 @@ let contradiction_context =
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let rec seek_neg l = match l with
- | [] -> Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
+ | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
| (id,_,typ)::rest ->
let typ = nf_evar sigma typ in
let typ = whd_betadeltaiota env sigma typ in
@@ -90,7 +90,7 @@ let contradiction_term (c,lbind as cl) =
Proofview.Goal.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
- let type_of = Tacmach.New.pf_type_of gl in
+ let type_of = Tacmach.New.pf_unsafe_type_of gl in
let typ = type_of c in
let _, ccl = splay_prod env sigma typ in
if is_empty_type ccl then
@@ -107,7 +107,7 @@ let contradiction_term (c,lbind as cl) =
Proofview.tclZERO Not_found
end
begin function (e, info) -> match e with
- | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+ | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
| e -> Proofview.tclZERO ~info e
end
end
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 27c3569d..ee7b94b0 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -33,7 +33,8 @@ DECLARE PLUGIN "eauto"
let eauto_unif_flags = auto_flags_of_state full_transparent_state
-let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
+let e_give_exact ?(flags=eauto_unif_flags) c gl =
+ let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in
if occur_existential t1 || occur_existential t2 then
tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
else Proofview.V82.of_tactic (exact_check c) gl
@@ -94,7 +95,7 @@ let out_term = function
| IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
let prolog_tac l n gl =
- let l = List.map (fun x -> out_term (pf_apply (prepare_hint false) gl x)) l in
+ let l = List.map (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in
let n =
match n with
| ArgArg n -> n
@@ -116,14 +117,17 @@ open Unification
(***************************************************************************)
let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
-
-let unify_e_resolve poly flags (c,clenv) gls =
- let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv
- else clenv, Univ.empty_level_subst in
- let clenv' = connect_clenv gls clenv' in
- let clenv' = clenv_unique_resolver ~flags clenv' gls in
- tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
+
+let unify_e_resolve poly flags (c,clenv) =
+ Proofview.Goal.nf_enter begin
+ fun gl ->
+ let clenv', c = connect_hint_clenv poly c clenv gl in
+ Proofview.V82.tactic
+ (fun gls ->
+ let clenv' = clenv_unique_resolver ~flags clenv' gls in
+ tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+ (Proofview.V82.of_tactic (Tactics.Simple.eapply c)) gls)
+ end
let hintmap_of hdc concl =
match hdc with
@@ -134,6 +138,7 @@ let hintmap_of hdc concl =
(* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
let e_exact poly flags (c,clenv) =
+ let (c, _, _) = c in
let clenv', subst =
if poly then Clenv.refresh_undefined_univs clenv
else clenv, Univ.empty_level_subst
@@ -147,7 +152,7 @@ let rec e_trivial_fail_db db_list local_db goal =
let d = pf_last_hyp g' in
let hintl = make_resolve_hyp (pf_env g') (project g') d in
(e_trivial_fail_db db_list
- (Hint_db.add_list hintl local_db) g'))) ::
+ (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
(List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
in
tclFIRST (List.map tclCOMPLETE tacl) goal
@@ -164,16 +169,16 @@ and e_my_find_search db_list local_db hdc concl =
(b,
let tac = function
| Res_pf (term,cl) -> unify_resolve poly st (term,cl)
- | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
+ | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
| Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
| Res_pf_THEN_trivial_fail (term,cl) ->
- Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl))
+ Proofview.V82.tactic (tclTHEN (Proofview.V82.of_tactic (unify_e_resolve poly st (term,cl)))
(e_trivial_fail_db db_list local_db))
| Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
| Extern tacast -> conclPattern concl p tacast
in
- let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
- (tac, lazy (pr_autotactic t)))
+ let tac = Proofview.V82.of_tactic (run_hint t tac) in
+ (tac, lazy (pr_hint t)))
in
List.map tac_of_hint hintl
@@ -200,7 +205,8 @@ type search_state = {
last_tactic : std_ppcmds Lazy.t;
dblist : hint_db list;
localdb : hint_db list;
- prev : prev_search_state
+ prev : prev_search_state;
+ local_lemmas : Evd.open_constr list;
}
and prev_search_state = (* for info eauto *)
@@ -259,7 +265,7 @@ module SearchProblem = struct
List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
last_tactic = pp; dblist = s.dblist;
localdb = List.tl s.localdb;
- prev = ps}) l
+ prev = ps; local_lemmas = s.local_lemmas}) l
in
let intro_tac =
let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in
@@ -269,10 +275,12 @@ module SearchProblem = struct
let hintl =
make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
in
- let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+ let ldb = Hint_db.add_list (pf_env g') (project g')
+ hintl (List.hd s.localdb) in
{ depth = s.depth; priority = cost; tacres = lgls;
last_tactic = pp; dblist = s.dblist;
- localdb = ldb :: List.tl s.localdb; prev = ps })
+ localdb = ldb :: List.tl s.localdb; prev = ps;
+ local_lemmas = s.local_lemmas})
l
in
let rec_tacs =
@@ -284,7 +292,8 @@ module SearchProblem = struct
let nbgl' = List.length (sig_it lgls) in
if nbgl' < nbgl then
{ depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
- prev = ps; dblist = s.dblist; localdb = List.tl s.localdb }
+ prev = ps; dblist = s.dblist; localdb = List.tl s.localdb;
+ local_lemmas = s.local_lemmas }
else
let newlocal =
let hyps = pf_hyps g in
@@ -292,12 +301,13 @@ module SearchProblem = struct
let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
let hyps' = pf_hyps gls in
if hyps' == hyps then List.hd s.localdb
- else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true [])
+ else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas)
(List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
in
{ depth = pred s.depth; priority = cost; tacres = lgls;
dblist = s.dblist; last_tactic = pp; prev = ps;
- localdb = newlocal @ List.tl s.localdb })
+ localdb = newlocal @ List.tl s.localdb;
+ local_lemmas = s.local_lemmas })
l
in
List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
@@ -362,7 +372,7 @@ let pr_info dbg s =
(** Eauto main code *)
-let make_initial_state dbg n gl dblist localdb =
+let make_initial_state dbg n gl dblist localdb lems =
{ depth = n;
priority = 0;
tacres = tclIDTAC gl;
@@ -370,6 +380,7 @@ let make_initial_state dbg n gl dblist localdb =
dblist = dblist;
localdb = [localdb];
prev = if dbg == Info then Init else Unknown;
+ local_lemmas = lems;
}
let e_search_auto debug (in_depth,p) lems db_list gl =
@@ -383,7 +394,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
in
try
pr_dbg_header d;
- let s = tac (make_initial_state d p gl db_list local_db) in
+ let s = tac (make_initial_state d p gl db_list local_db lems) in
pr_info d s;
s.tacres
with Not_found ->
@@ -609,7 +620,7 @@ TACTIC EXTEND unify
match table with
| None ->
let msg = str "Hint table " ++ str base ++ str " not found" in
- Proofview.tclZERO (UserError ("", msg))
+ Tacticals.New.tclZEROMSG msg
| Some t ->
let state = Hint_db.transparent_state t in
unify ~state x y
@@ -621,12 +632,7 @@ TACTIC EXTEND convert_concl_no_check
| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
END
-
-let pr_hints_path_atom prc _ _ a =
- match a with
- | PathAny -> str"."
- | PathHints grs ->
- pr_sequence Printer.pr_global grs
+let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
ARGUMENT EXTEND hints_path_atom
TYPED AS hints_path_atom
@@ -635,15 +641,7 @@ ARGUMENT EXTEND hints_path_atom
| [ "*" ] -> [ PathAny ]
END
-let pr_hints_path prc prx pry c =
- let rec aux = function
- | PathAtom a -> pr_hints_path_atom prc prx pry a
- | PathStar p -> str"(" ++ aux p ++ str")*"
- | PathSeq (p, p') -> aux p ++ spc () ++ aux p'
- | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")"
- | PathEmpty -> str"ø"
- | PathEpsilon -> str"ε"
- in aux c
+let pr_hints_path prc prx pry c = Hints.pp_hints_path c
ARGUMENT EXTEND hints_path
TYPED AS hints_path
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 3cb4fa9c..4841d2c2 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -85,7 +85,7 @@ let up_to_delta = ref false (* true *)
let general_decompose recognizer c =
Proofview.Goal.enter begin fun gl ->
- let type_of = pf_type_of gl in
+ let type_of = pf_unsafe_type_of gl in
let typc = type_of c in
tclTHENS (cut typc)
[ tclTHEN (intro_using tmphyp_name)
@@ -139,7 +139,7 @@ let induction_trailer abs_i abs_j bargs =
(onLastHypId
(fun id ->
Proofview.Goal.nf_enter begin fun gl ->
- let idty = pf_type_of gl (mkVar id) in
+ let idty = pf_unsafe_type_of gl (mkVar id) in
let fvty = global_vars (pf_env gl) idty in
let possible_bring_hyps =
(List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 749e0d2b..8a6d93cf 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -21,7 +21,7 @@ open Ind_tables
(* Induction/recursion schemes *)
-let optimize_non_type_induction_scheme kind dep sort ind =
+let optimize_non_type_induction_scheme kind dep sort _ ind =
let env = Global.env () in
let sigma = Evd.from_env env in
if check_scheme kind ind then
@@ -51,8 +51,8 @@ let optimize_non_type_induction_scheme kind dep sort ind =
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
- let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
- (c, Evd.evar_universe_context sigma), Declareops.no_seff
+ let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
+ (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
let build_induction_scheme_in_type dep sort ind =
let env = Global.env () in
@@ -63,20 +63,20 @@ let build_induction_scheme_in_type dep sort ind =
let u = Univ.UContext.instance ctx in
let ctxset = Univ.ContextSet.of_context ctx in
let ectx = Evd.evar_universe_context_of ctxset in
- let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+ let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
c, Evd.evar_universe_context sigma
let rect_scheme_kind_from_type =
declare_individual_scheme_object "_rect_nodep"
- (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+ (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
let rect_scheme_kind_from_prop =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
- (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+ (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
let rect_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
- (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+ (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
let ind_scheme_kind_from_type =
declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
let case_scheme_kind_from_type =
declare_individual_scheme_object "_case_nodep"
- (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+ (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
let case_scheme_kind_from_prop =
declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
- (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+ (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
let case_dep_scheme_kind_from_type =
declare_individual_scheme_object "_case" ~aux:"_case_from_type"
- (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+ (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
let case_dep_scheme_kind_from_type_in_prop =
declare_individual_scheme_object "_casep_dep"
- (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+ (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
let case_dep_scheme_kind_from_prop =
declare_individual_scheme_object "_case_dep"
- (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+ (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
let case_dep_scheme_kind_from_prop_in_prop =
declare_individual_scheme_object "_casep"
- (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+ (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index c2cd9e47..4fb76bb8 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,22 +104,29 @@ let mkGenDecideEqGoal rectype g =
(mkDecideEqGoal true (build_coq_sumbool ())
rectype (mkVar xname) (mkVar yname))))
+let rec rewrite_and_clear hyps = match hyps with
+| [] -> Proofview.tclUNIT ()
+| id :: hyps ->
+ tclTHENLIST [
+ Equality.rewriteLR (mkVar id);
+ clear [id];
+ rewrite_and_clear hyps;
+ ]
+
let eqCase tac =
- (tclTHEN intro
- (tclTHEN (onLastHyp Equality.rewriteLR)
- (tclTHEN clear_last
- tac)))
+ tclTHEN intro (onLastHypId tac)
-let diseqCase eqonleft =
+let diseqCase hyps eqonleft =
let diseq = Id.of_string "diseq" in
let absurd = Id.of_string "absurd" in
(tclTHEN (intro_using diseq)
(tclTHEN (choose_noteq eqonleft)
+ (tclTHEN (rewrite_and_clear (List.rev hyps))
(tclTHEN (Proofview.V82.tactic red_in_concl)
(tclTHEN (intro_using absurd)
(tclTHEN (Simple.apply (mkVar diseq))
(tclTHEN (Extratactics.injHyp absurd)
- (full_trivial [])))))))
+ (full_trivial []))))))))
open Proofview.Notations
@@ -131,15 +138,24 @@ let match_eqdec c =
(* /spiwack *)
-let solveArg eqonleft op a1 a2 tac =
+let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+| [], [] ->
+ tclTHENLIST [
+ choose_eq eqonleft;
+ rewrite_and_clear (List.rev hyps);
+ intros_reflexivity;
+ ]
+| a1 :: largs, a2 :: rargs ->
Proofview.Goal.enter begin fun gl ->
- let rectype = pf_type_of gl a1 in
+ let rectype = pf_unsafe_type_of gl a1 in
let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
+ let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
let subtacs =
- if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
- else [diseqCase eqonleft;eqCase tac;default_auto] in
+ if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
+ else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
(tclTHENS (elim_type decide) subtacs)
end
+| _ -> invalid_arg "List.fold_right2"
let solveEqBranch rectype =
Proofview.tclORELSE
@@ -152,13 +168,11 @@ let solveEqBranch rectype =
let getargs l = List.skipn nparams (snd (decompose_app l)) in
let rargs = getargs rhs
and largs = getargs lhs in
- List.fold_right2
- (solveArg eqonleft op) largs rargs
- (tclTHEN (choose_eq eqonleft) intros_reflexivity)
+ solveArg [] eqonleft op largs rargs
end
end
begin function (e, info) -> match e with
- | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
+ | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
| e -> Proofview.tclZERO ~info e
end
@@ -186,7 +200,7 @@ let decideGralEquality =
end
begin function (e, info) -> match e with
| PatternMatchingFailure ->
- Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."))
+ Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")
| e -> Proofview.tclZERO ~info e
end
@@ -203,7 +217,7 @@ let decideEquality rectype =
let compare c1 c2 =
Proofview.Goal.enter begin fun gl ->
- let rectype = pf_type_of gl c1 in
+ let rectype = pf_unsafe_type_of gl c1 in
let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
(tclTHENS (cut decide)
[(tclTHEN intro
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 8643fe10..b2603315 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -191,9 +191,9 @@ let build_sym_scheme env ind =
let sym_scheme_kind =
declare_individual_scheme_object "_sym_internal"
- (fun ind ->
+ (fun _ ind ->
let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
- (c, ctx), Declareops.no_seff)
+ (c, ctx), Safe_typing.empty_private_constants)
(**********************************************************************)
(* Build the involutivity of symmetry for an inductive type *)
@@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind =
let sym_involutive_scheme_kind =
declare_individual_scheme_object "_sym_involutive"
- (fun ind ->
+ (fun _ ind ->
build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
(**********************************************************************)
@@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind =
[|main_body|])
else
main_body))))))
- in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff
+ in (c, Evd.evar_universe_context_of ctx),
+ Safe_typing.concat_private eff' eff
(**********************************************************************)
(* Build the left-to-right rewriting lemma for hypotheses associated *)
@@ -650,7 +651,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
(**********************************************************************)
let rew_l2r_dep_scheme_kind =
declare_individual_scheme_object "_rew_r_dep"
- (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
+ (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
(**********************************************************************)
(* Dependent rewrite from right-to-left in conclusion *)
@@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_dep_scheme_kind =
declare_individual_scheme_object "_rew_dep"
- (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+ (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
(**********************************************************************)
(* Dependent rewrite from right-to-left in hypotheses *)
@@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_dep"
- (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+ (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
(**********************************************************************)
(* Dependent rewrite from left-to-right in hypotheses *)
@@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind =
(**********************************************************************)
let rew_l2r_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_r_dep"
- (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
+ (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
(**********************************************************************)
(* Non-dependent rewrite from either left-to-right in conclusion or *)
@@ -693,8 +694,8 @@ let rew_l2r_forward_dep_scheme_kind =
(**********************************************************************)
let rew_l2r_scheme_kind =
declare_individual_scheme_object "_rew_r"
- (fun ind -> fix_r2l_forward_rew_scheme
- (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
+ (fun _ ind -> fix_r2l_forward_rew_scheme
+ (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants)
(**********************************************************************)
(* Non-dependent rewrite from either right-to-left in conclusion or *)
@@ -704,7 +705,7 @@ let rew_l2r_scheme_kind =
(**********************************************************************)
let rew_r2l_scheme_kind =
declare_individual_scheme_object "_rew"
- (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
+ (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants)
(* End of rewriting schemes *)
@@ -780,6 +781,6 @@ let build_congr env (eq,refl,ctx) ind =
in c, Evd.evar_universe_context_of ctx
let congr_scheme_kind = declare_individual_scheme_object "_congr"
- (fun ind ->
+ (fun _ ind ->
(* May fail if equality is not defined *)
- build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
+ build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 6bb84808..3fe33073 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family ->
constr Evd.in_evar_universe_context
val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family ->
- constr Evd.in_evar_universe_context * Declareops.side_effects
+ constr Evd.in_evar_universe_context * Safe_typing.private_constants
val build_r2l_forward_rew_scheme :
bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
val build_l2r_forward_rew_scheme :
@@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
val sym_scheme_kind : individual scheme_kind
val build_sym_involutive_scheme : env -> inductive ->
- constr Evd.in_evar_universe_context * Declareops.side_effects
+ constr Evd.in_evar_universe_context * Safe_typing.private_constants
val sym_involutive_scheme_kind : individual scheme_kind
(** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ab8d0c3..674c85af 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,7 +88,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
type orientation = bool
type conditions =
- | Naive (* Only try the first occurence of the lemma (default) *)
+ | Naive (* Only try the first occurrence of the lemma (default) *)
| FirstSolved (* Use the first match whose side-conditions are solved *)
| AllMatches (* Rewrite all matches whose side-conditions are solved *)
@@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
in List.map try_occ occs
let instantiate_lemma gl c ty l l2r concl =
- let ct = pf_type_of gl c in
- let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
- [eqclause]
+ let sigma, ct = pf_type_of gl c in
+ let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+ let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
+ [eqclause]
let rewrite_conv_closed_core_unif_flags = {
modulo_conv_on_closed_terms = Some full_transparent_state;
@@ -306,8 +306,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
let _ = Global.lookup_constant c1' in
c1'
with Not_found ->
- let rwr_thm = Label.to_string l' in
- error ("Cannot find rewrite principle "^rwr_thm^".")
+ errorlabstrm "Equality.find_elim"
+ (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
end
| _ -> destConstRef pr1
end
@@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
assert false
in
let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
- sigma, elim, Declareops.no_seff
+ sigma, elim, Safe_typing.empty_private_constants
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case *)
@@ -335,7 +335,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
| Ind (ind,u) ->
let c, eff = find_scheme scheme_name ind in
(* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
- let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+ let sigma, elim =
+ Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+ in
sigma, elim, eff
| _ -> assert false
@@ -454,7 +456,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
(* Otherwise, if we are told to rewrite in all hypothesis via the
syntax "* |-", we fail iff all the different rewrites fail *)
let rec do_hyps_atleastonce = function
- | [] -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Nothing to rewrite."))
+ | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
| id :: l ->
tclIFTHENTRYELSEMUST
(general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
@@ -540,7 +542,7 @@ let replace_core clause l2r eq =
if check_setoid clause
then init_setoid ();
tclTHENFIRST
- (assert_as false None eq)
+ (assert_as false None None eq)
(onLastHypId (fun id ->
tclTHEN
(tclTRY (general_rewrite_clause l2r false (mkVar id,NoBindings) clause))
@@ -874,7 +876,7 @@ let gen_absurdity id =
then
simplest_elim (mkVar id)
else
- Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
+ tclZEROMSG (str "Not the negation of an equality.")
end
(* Precondition: eq is leibniz equality
@@ -899,7 +901,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
let i = build_coq_I () in
let absurd_term = build_coq_False () in
let eq_elim, eff = ind_scheme_of_eq lbeq in
- let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in
+ let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
eff
@@ -936,7 +938,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let concl = Proofview.Goal.concl gl in
match find_positions env sigma t1 t2 with
| Inr _ ->
- Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
+ tclZEROMSG (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
let sort = pf_apply get_type_of gl concl in
discr_positions env sigma u eq_clause cpath dirn sort
@@ -944,7 +946,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let onEquality with_evars tac (c,lbindc) =
Proofview.Goal.nf_enter begin fun gl ->
- let type_of = pf_type_of gl in
+ let type_of = pf_unsafe_type_of gl in
let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
let t = type_of c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
@@ -968,7 +970,7 @@ let onNegatedEquality with_evars tac =
(onLastHypId (fun id ->
onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
- Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+ tclZEROMSG (str "Not a negated primitive equality.")
end
let discrSimpleClause with_evars = function
@@ -1019,7 +1021,7 @@ let find_sigma_data env s = build_sigma_type ()
let make_tuple env sigma (rterm,rty) lind =
assert (dependent (mkRel lind) rty);
let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
- let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in
+ let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
let (na,_,_) = lookup_rel lind env in
(* We move [lind] to [1] and lift other rels > [lind] by 1 *)
let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1053,7 +1055,7 @@ let minimal_free_rels_rec env sigma =
let rec minimalrec_free_rels_rec prev_rels (c,cty) =
let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
let combined_rels = Int.Set.union prev_rels direct_rels in
- let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
+ let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i)))
in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
in minimalrec_free_rels_rec Int.Set.empty
@@ -1099,7 +1101,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let rec sigrec_clausal_form siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
- let dflt_typ = type_of env sigma dflt in
+ let dflt_typ = unsafe_type_of env sigma dflt in
try
let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
@@ -1118,13 +1120,20 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
(destEvar ev)
with
| Some w ->
- let w_type = type_of env sigma w in
+ let w_type = unsafe_type_of env sigma w in
if Evarconv.e_cumul env evdref w_type a then
let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
else
error "Cannot solve a unification problem."
- | None -> anomaly (Pp.str "Not enough components to build the dependent tuple")
+ | None ->
+ (* This at least happens if what has been detected as a
+ dependency is not one; use an evasive error message;
+ even if the problem is upwards: unification should be
+ tried in the first place in make_iterated_tuple instead
+ of approximatively computing the free rels; then
+ unsolved evars would mean not binding rel *)
+ error "Cannot solve a unification problem."
in
let scf = sigrec_clausal_form siglen ty in
!evdref, Evarutil.nf_evar !evdref scf
@@ -1200,7 +1209,7 @@ let make_iterated_tuple env sigma dflt (z,zty) =
sigma, (tuple,tuplety,dfltval)
let rec build_injrec env sigma dflt c = function
- | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
+ | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c)
| ((sp,cnum),argnum)::l ->
try
let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in
@@ -1253,7 +1262,7 @@ let inject_if_homogenous_dependent_pair ty =
if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
- let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+ let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
@@ -1293,7 +1302,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
let injfun = mkNamedLambda e t injbody in
let sigma,congr = Evd.fresh_global env sigma eq.congr in
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
- let sigma, pf_typ = Typing.e_type_of env sigma pf in
+ let sigma, pf_typ = Typing.type_of env sigma pf in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta inj_clause in
let ty = simplify_args env sigma (clenv_type inj_clause) in
@@ -1303,7 +1312,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
in
let injectors = List.map_filter filter posns in
if List.is_empty injectors then
- Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
+ tclZEROMSG (str "Failed to decompose the equality.")
else
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
(Proofview.tclBIND
@@ -1319,12 +1328,12 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let env = eq_clause.env in
match find_positions env sigma t1 t2 with
| Inl _ ->
- Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal."))
+ tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
| Inr [] ->
let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
- Proofview.tclZERO (Errors.UserError ("Equality.inj",strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)))
+ tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
| Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
- Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
+ tclZEROMSG (str"Nothing to inject.")
| Inr posns ->
inject_at_positions env sigma l2r u eq_clause posns
(tac (clenv_value eq_clause))
@@ -1460,8 +1469,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
let expected_goal = nf_betaiota sigma expected_goal in
(* Retype to get universes right *)
- let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in
- let sigma, _ = Typing.e_type_of env sigma body in
+ let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
+ let sigma, _ = Typing.type_of env sigma body in
sigma,body,expected_goal
(* Like "replace" but decompose dependent equalities *)
@@ -1575,7 +1584,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
exception FoundHyp of (Id.t * constr * bool)
-(* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
+(* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *)
let is_eq_x gl x (id,_,c) =
try
let c = pf_nf_evar gl c in
@@ -1589,10 +1598,10 @@ let is_eq_x gl x (id,_,c) =
erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one dep_proof_ok x (hyp,rhs,dir) =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let hyps = Proofview.Goal.hyps gl in
- let concl = Proofview.Goal.concl gl in
+ let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+ let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
(* The set of hypotheses using x *)
let dephyps =
List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
@@ -1662,7 +1671,70 @@ let default_subst_tactic_flags () =
else
{ only_leibniz = true; rewrite_dependent_proof = false }
+let regular_subst_tactic = ref false
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "more regular behavior of tactic subst";
+ optkey = ["Regular";"Subst";"Tactic"];
+ optread = (fun () -> !regular_subst_tactic);
+ optwrite = (:=) regular_subst_tactic }
+
let subst_all ?(flags=default_subst_tactic_flags ()) () =
+
+ if !regular_subst_tactic then
+
+ (* First step: find hypotheses to treat in linear time *)
+ let find_equations gl =
+ let gl = Proofview.Goal.assume gl in
+ let env = Proofview.Goal.env gl in
+ let find_eq_data_decompose = find_eq_data_decompose gl in
+ let test (hyp,_,c) =
+ try
+ let lbeq,u,(_,x,y) = find_eq_data_decompose c in
+ let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
+ if flags.only_leibniz then restrict_to_eq_and_identity eq;
+ match kind_of_term x, kind_of_term y with
+ | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) ->
+ Some hyp
+ | _ ->
+ None
+ with Constr_matching.PatternMatchingFailure -> None
+ in
+ let hyps = Proofview.Goal.hyps gl in
+ List.rev (List.map_filter test hyps)
+ in
+
+ (* Second step: treat equations *)
+ let process hyp =
+ Proofview.Goal.enter begin fun gl ->
+ let gl = Proofview.Goal.assume gl in
+ let find_eq_data_decompose = find_eq_data_decompose gl in
+ let (_,_,c) = pf_get_hyp hyp gl in
+ let _,_,(_,x,y) = find_eq_data_decompose c in
+ (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+ if Term.eq_constr x y then Proofview.tclUNIT () else
+ match kind_of_term x, kind_of_term y with
+ | Var x', _ when not (occur_term x y) ->
+ subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
+ | _, Var y' when not (occur_term y x) ->
+ subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
+ | _ ->
+ Proofview.tclUNIT ()
+ end
+ in
+ Proofview.Goal.nf_enter begin fun gl ->
+ let ids = find_equations gl in
+ tclMAP process ids
+ end
+
+ else
+
+(* Old implementation, not able to manage configurations like a=b, a=t,
+ or situations like "a = S b, b = S a", or also accidentally unfolding
+ let-ins *)
Proofview.Goal.nf_enter begin fun gl ->
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
@@ -1674,8 +1746,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
if Term.eq_constr x y then failwith "caught";
match kind_of_term x with Var x -> x | _ ->
match kind_of_term y with Var y -> y | _ -> failwith "caught"
- with Constr_matching.PatternMatchingFailure -> failwith "caught"
- in
+ with Constr_matching.PatternMatchingFailure -> failwith "caught" in
let test p = try Some (test p) with Failure _ -> None in
let hyps = pf_hyps_types gl in
let ids = List.map_filter test hyps in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3e13ee57..840ede7d 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -23,7 +23,7 @@ type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
type orientation = bool
type conditions =
- | Naive (* Only try the first occurence of the lemma (default) *)
+ | Naive (* Only try the first occurrence of the lemma (default) *)
| FirstSolved (* Use the first match whose side-conditions are solved *)
| AllMatches (* Rewrite all matches whose side-conditions are solved *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 891e2dba..cab74968 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -262,16 +262,15 @@ TACTIC EXTEND rewrite_star
(* Hint Rewrite *)
let add_rewrite_hint bases ort t lcsr =
- let env = Global.env() and sigma = Evd.empty in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
let poly = Flags.is_universe_polymorphism () in
let f ce =
let c, ctx = Constrintern.interp_constr env sigma ce in
let ctx =
- if poly then
- Evd.evar_universe_context_set ctx
- else
- let cstrs = Evd.evar_universe_context_constraints ctx in
- (Global.add_constraints cstrs; Univ.ContextSet.empty)
+ let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
+ if poly then ctx
+ else (Global.push_context_set false ctx; Univ.ContextSet.empty)
in
Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in
let eqs = List.map f lcsr in
@@ -320,7 +319,7 @@ let project_hint pri l2r r =
Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
in
let ctx = Evd.universe_context_set sigma in
- let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in
+ let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
(pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
let add_hints_iff l2r lc n bl =
@@ -490,7 +489,9 @@ let inTransitivity : bool * constr -> obj =
(* Main entry points *)
let add_transitivity_lemma left lem =
- let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in
add_anonymous_leaf (inTransitivity (left,lem'))
(* Vernacular syntax *)
@@ -704,7 +705,7 @@ let refl_equal =
call it before it is defined. *)
let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.nf_enter begin fun gl ->
- let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in
+ let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
Proofview.Goal.nf_enter begin fun gl ->
@@ -750,12 +751,12 @@ let rec find_a_destructable_match t =
let destauto t =
try find_a_destructable_match t;
- Proofview.tclZERO (UserError ("", str"No destructable match found"))
+ Tacticals.New.tclZEROMSG (str "No destructable match found")
with Found tac -> tac
let destauto_in id =
Proofview.Goal.nf_enter begin fun gl ->
- let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in
+ let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
destauto ctype
@@ -772,7 +773,7 @@ END
let eq_constr x y =
Proofview.Goal.enter (fun gl ->
let evd = Proofview.Goal.sigma gl in
- if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT ()
+ if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT ()
else Tacticals.New.tclFAIL 0 (str "Not equal"))
TACTIC EXTEND constr_eq
@@ -966,7 +967,7 @@ let guard tst =
Proofview.tclUNIT ()
else
let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in
- Proofview.tclZERO (Errors.UserError("guard",msg))
+ Tacticals.New.tclZEROMSG msg
TACTIC EXTEND guard
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 55d62e15..5630d20b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
(* The Type of Constructions Autotactic Hints *)
(************************************************************************)
-type 'a auto_tactic_ast =
+type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
| Give_exact of 'a
@@ -92,23 +92,66 @@ type hint_term =
| IsGlobRef of global_reference
| IsConstr of constr * Univ.universe_context_set
-type 'a auto_tactic = 'a auto_tactic_ast
+type 'a with_uid = {
+ obj : 'a;
+ uid : KerName.t;
+}
+
+type raw_hint = constr * types * Univ.universe_context_set
-type 'a gen_auto_tactic = {
+type hint = (raw_hint * clausenv) hint_ast with_uid
+
+type 'a with_metadata = {
pri : int; (* A number lower is higher priority *)
poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *)
pat : constr_pattern option; (* A pattern for the concl of the Goal *)
name : hints_path_atom; (* A potential name to refer to the hint *)
- code : 'a (* the tactic to apply when the concl matches pat *)
+ code : 'a; (* the tactic to apply when the concl matches pat *)
}
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
type hint_entry = global_reference option *
- (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
-
-let run_auto_tactic tac k = k tac
-let repr_auto_tactic tac = tac
+ raw_hint hint_ast with_uid with_metadata
+
+type import_level = [ `LAX | `WARN | `STRICT ]
+
+let warn_hint : import_level ref = ref `LAX
+let read_warn_hint () = match !warn_hint with
+| `LAX -> "Lax"
+| `WARN -> "Warn"
+| `STRICT -> "Strict"
+
+let write_warn_hint = function
+| "Lax" -> warn_hint := `LAX
+| "Warn" -> warn_hint := `WARN
+| "Strict" -> warn_hint := `STRICT
+| _ -> error "Only the following flags are accepted: Lax, Warn, Strict."
+
+let _ =
+ Goptions.declare_string_option
+ { Goptions.optsync = true;
+ Goptions.optdepr = false;
+ Goptions.optname = "behavior of non-imported hints";
+ Goptions.optkey = ["Loose"; "Hint"; "Behavior"];
+ Goptions.optread = read_warn_hint;
+ Goptions.optwrite = write_warn_hint;
+ }
+
+let fresh_key =
+ let id = Summary.ref ~name:"HINT-COUNTER" 0 in
+ fun () ->
+ let cur = incr id; !id in
+ let lbl = Id.of_string ("_" ^ string_of_int cur) in
+ let kn = Lib.make_kn lbl in
+ let (mp, dir, _) = KerName.repr kn in
+ (** We embed the full path of the kernel name in the label so that the
+ identifier should be unique. This ensures that including two modules
+ together won't confuse the corresponding labels. *)
+ let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+ (ModPath.to_string mp) (DirPath.to_string dir) cur)
+ in
+ KerName.make mp dir (Label.of_id lbl)
let eq_hints_path_atom p1 p2 = match p1, p2 with
| PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -125,7 +168,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with
| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
| Unfold_nth _ | Extern _), _ -> false
-let eq_gen_auto_tactic t1 t2 =
+let eq_hint_metadata t1 t2 =
Int.equal t1.pri t2.pri &&
Option.equal constr_pattern_eq t1.pat t2.pat &&
eq_hints_path_atom t1.name t2.name &&
@@ -153,7 +196,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
- un discrimination net borné (Btermdn.t) constitué de tous les
patterns de la seconde liste de tactiques *)
-type stored_data = int * pri_auto_tactic
+type stored_data = int * full_hint
(* First component is the index of insertion in the table, to keep most recent first semantics. *)
module Bounded_net = Btermdn.Make(struct
@@ -175,21 +218,7 @@ let empty_se = {
sentry_mode = [];
}
-let eq_pri_auto_tactic (_, x) (_, y) =
- if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
- match x.code,y.code with
- | Res_pf (cstr,_),Res_pf (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | ERes_pf (cstr,_),ERes_pf (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | Give_exact (cstr,_),Give_exact (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | Res_pf_THEN_trivial_fail (cstr,_)
- ,Res_pf_THEN_trivial_fail (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | _,_ -> false
- else
- false
+let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid
let add_tac pat t st se =
match pat with
@@ -239,24 +268,24 @@ let strip_params env c =
| _ -> c)
| _ -> c
-let instantiate_hint p =
- let mk_clenv c cty ctx =
- let env = Global.env () in
- let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in
- let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in
+let instantiate_hint env sigma p =
+ let mk_clenv (c, cty, ctx) =
+ let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+ let cl = mk_clenv_from_env env sigma None (c,cty) in
{cl with templval =
{ cl.templval with rebus = strip_params env cl.templval.rebus };
env = empty_env}
in
- let code = match p.code with
- | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx)
- | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx)
- | Res_pf_THEN_trivial_fail (c, cty, ctx) ->
- Res_pf_THEN_trivial_fail (c, mk_clenv c cty ctx)
- | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx)
+ let code = match p.code.obj with
+ | Res_pf c -> Res_pf (c, mk_clenv c)
+ | ERes_pf c -> ERes_pf (c, mk_clenv c)
+ | Res_pf_THEN_trivial_fail c ->
+ Res_pf_THEN_trivial_fail (c, mk_clenv c)
+ | Give_exact c -> Give_exact (c, mk_clenv c)
| Unfold_nth e -> Unfold_nth e
| Extern t -> Extern t
- in { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code }
+ in
+ { p with code = { p.code with obj = code } }
let hints_path_atom_eq h1 h2 = match h1, h2 with
| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
@@ -353,15 +382,19 @@ let rec normalize_path h =
let path_derivate hp hint = normalize_path (path_derivate hp hint)
+let pp_hints_path_atom a =
+ match a with
+ | PathAny -> str"*"
+ | PathHints grs -> pr_sequence pr_global grs
+
let rec pp_hints_path = function
- | PathAtom (PathAny) -> str"."
- | PathAtom (PathHints grs) -> pr_sequence pr_global grs
- | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+ | PathAtom pa -> pp_hints_path_atom pa
+ | PathStar p -> str "!(" ++ pp_hints_path p ++ str")"
| PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
| PathOr (p, p') ->
str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
- | PathEmpty -> str"Ø"
- | PathEpsilon -> str"ε"
+ | PathEmpty -> str"emp"
+ | PathEpsilon -> str"eps"
let subst_path_atom subst p =
match p with
@@ -429,7 +462,9 @@ module Hint_db = struct
else List.exists (matches_mode args) modes
let merge_entry db nopat pat =
- let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in
+ let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
+ let h = List.merge pri_order_int h nopat in
+ let h = List.merge pri_order_int h pat in
List.map realize_tac h
let map_none db =
@@ -473,15 +508,14 @@ module Hint_db = struct
let idv = id, v in
let k = match gr with
| Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
- is_unfold v.code then None else Some gr
+ is_unfold v.code.obj then None else Some gr
| None -> None
in
let dnst = if db.use_dn then Some db.hintdb_state else None in
- let pat = if not db.use_dn && is_exact v.code then None else v.pat in
+ let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in
match k with
| None ->
- (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
- let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in
+ let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
if not (List.exists is_present db.hintdb_nopat) then
(** FIXME *)
{ db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
@@ -497,10 +531,10 @@ module Hint_db = struct
in
List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
- let add_one (k, v) db =
- let v = instantiate_hint v in
+ let add_one env sigma (k, v) db =
+ let v = instantiate_hint env sigma v in
let st',db,rebuild =
- match v.code with
+ match v.code.obj with
| Unfold_nth egr ->
let addunf (ids,csts) (ids',csts') =
match egr with
@@ -515,7 +549,7 @@ module Hint_db = struct
let db, id = next_hint_id db in
addkv k id v db
- let add_list l db = List.fold_left (fun db k -> add_one k db) db l
+ let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
let remove_sdl p sdl = List.smartfilter p sdl
@@ -534,7 +568,9 @@ module Hint_db = struct
let remove_one gr db = remove_list [gr] db
- let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat)
+ let get_entry se =
+ let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
+ List.map realize_tac h
let iter f db =
let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
@@ -586,6 +622,7 @@ let auto_init_db =
Hintdbmap.empty)
let searchtable : hint_db_table = ref auto_init_db
+let statustable = ref KNmap.empty
let searchtable_map name =
Hintdbmap.find name !searchtable
@@ -598,7 +635,7 @@ let current_pure_db () =
List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
let error_no_such_hint_database x =
- error ("No such Hint database: "^x^".")
+ errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
(**************************************************************************)
(* Definition of the summary *)
@@ -609,9 +646,10 @@ let add_hints_init f =
let init = !hints_init in
hints_init := (fun () -> init (); f ())
-let init () = searchtable := auto_init_db; !hints_init ()
-let freeze _ = !searchtable
-let unfreeze fs = searchtable := fs
+let init () =
+ searchtable := auto_init_db; statustable := KNmap.empty; !hints_init ()
+let freeze _ = (!searchtable, !statustable)
+let unfreeze (fs, st) = searchtable := fs; statustable := st
let _ = Summary.declare_summary "search"
{ Summary.freeze_function = freeze;
@@ -632,6 +670,8 @@ let try_head_pattern c =
try head_pattern_bound c
with BoundPattern -> error "Bound head variable."
+let with_uid c = { obj = c; uid = fresh_key () }
+
let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
let cty = strip_outer_cast cty in
match kind_of_term cty with
@@ -647,7 +687,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
poly = poly;
pat = Some pat;
name = name;
- code = Give_exact (c, cty, ctx) })
+ code = with_uid (Give_exact (c, cty, ctx)); })
let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
@@ -667,7 +707,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
poly = poly;
pat = Some pat;
name = name;
- code = Res_pf(c,cty,ctx) })
+ code = with_uid (Res_pf(c,cty,ctx)); })
else begin
if not eapply then failwith "make_apply_entry";
if verbose then
@@ -678,7 +718,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
poly = poly;
pat = Some pat;
name = name;
- code = ERes_pf(c,cty,ctx) })
+ code = with_uid (ERes_pf(c,cty,ctx)); })
end
| _ -> failwith "make_apply_entry"
@@ -724,7 +764,7 @@ let make_unfold eref =
poly = false;
pat = None;
name = PathHints [g];
- code = Unfold_nth eref })
+ code = with_uid (Unfold_nth eref) })
let make_extern pri pat tacast =
let hdconstr = Option.map try_head_pattern pat in
@@ -733,7 +773,7 @@ let make_extern pri pat tacast =
poly = false;
pat = pat;
name = PathAny;
- code = Extern tacast })
+ code = with_uid (Extern tacast) })
let make_mode ref m =
let ty = Global.type_of_global_unsafe ref in
@@ -749,14 +789,14 @@ let make_mode ref m =
let make_trivial env sigma poly ?(name=PathAny) r =
let c,ctx = fresh_global_or_constr env sigma poly r in
let sigma = Evd.merge_context_set univ_flexible sigma ctx in
- let t = hnf_constr env sigma (type_of env sigma c) in
+ let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
let hd = head_of_constr_reference (head_constr t) in
let ce = mk_clenv_from_env env sigma None (c,t) in
(Some hd, { pri=1;
poly = poly;
pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
name = name;
- code=Res_pf_THEN_trivial_fail(c,t,ctx) })
+ code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
@@ -771,9 +811,19 @@ let get_db dbname =
try searchtable_map dbname
with Not_found -> Hint_db.empty empty_transparent_state false
-let add_hint dbname hintlist =
+let add_hint dbname hintlist =
+ let check (_, h) =
+ let () = if KNmap.mem h.code.uid !statustable then
+ error "Conflicting hint keys. This can happen when including \
+ twice the same module."
+ in
+ statustable := KNmap.add h.code.uid false !statustable
+ in
+ let () = List.iter check hintlist in
let db = get_db dbname in
- let db' = Hint_db.add_list hintlist db in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let db' = Hint_db.add_list env sigma hintlist db in
searchtable_add (dbname,db')
let add_transparency dbname grs b =
@@ -816,7 +866,7 @@ type hint_obj = {
hint_action : hint_action;
}
-let cache_autohint (_, h) =
+let load_autohint _ (kn, h) =
let name = h.hint_name in
match h.hint_action with
| CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
@@ -826,6 +876,16 @@ let cache_autohint (_, h) =
| AddCut path -> add_cut name path
| AddMode (l, m) -> add_mode name l m
+let open_autohint i (kn, h) =
+ if Int.equal i 1 then match h.hint_action with
+ | AddHints hints ->
+ let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
+ List.iter add hints
+ | _ -> ()
+
+let cache_autohint (kn, obj) =
+ load_autohint 1 (kn, obj); open_autohint 1 (kn, obj)
+
let subst_autohint (subst, obj) =
let subst_key gr =
let (lab'', elab') = subst_global subst gr in
@@ -837,34 +897,36 @@ let subst_autohint (subst, obj) =
let subst_hint (k,data as hint) =
let k' = Option.smartmap subst_key k in
let pat' = Option.smartmap (subst_pattern subst) data.pat in
- let code' = match data.code with
+ let code' = match data.code.obj with
| Res_pf (c,t,ctx) ->
let c' = subst_mps subst c in
let t' = subst_mps subst t in
- if c==c' && t'==t then data.code else Res_pf (c', t',ctx)
+ if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx)
| ERes_pf (c,t,ctx) ->
let c' = subst_mps subst c in
let t' = subst_mps subst t in
- if c==c' && t'==t then data.code else ERes_pf (c',t',ctx)
+ if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
| Give_exact (c,t,ctx) ->
let c' = subst_mps subst c in
let t' = subst_mps subst t in
- if c==c' && t'== t then data.code else Give_exact (c',t',ctx)
+ if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
| Res_pf_THEN_trivial_fail (c,t,ctx) ->
let c' = subst_mps subst c in
let t' = subst_mps subst t in
- if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx)
+ if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx)
| Unfold_nth ref ->
let ref' = subst_evaluable_reference subst ref in
- if ref==ref' then data.code else Unfold_nth ref'
+ if ref==ref' then data.code.obj else Unfold_nth ref'
| Extern tac ->
let tac' = Tacsubst.subst_tactic subst tac in
- if tac==tac' then data.code else Extern tac'
+ if tac==tac' then data.code.obj else Extern tac'
in
let name' = subst_path_atom subst data.name in
+ let uid' = subst_kn subst data.code.uid in
let data' =
- if data.pat==pat' && data.name == name' && data.code==code' then data
- else { data with pat = pat'; name = name'; code = code' }
+ if data.code.uid == uid' && data.pat == pat' &&
+ data.name == name' && data.code.obj == code' then data
+ else { data with pat = pat'; name = name'; code = { obj = code'; uid = uid' } }
in
if k' == k && data' == data then hint else (k',data')
in
@@ -896,7 +958,8 @@ let classify_autohint obj =
let inAutoHint : hint_obj -> obj =
declare_object {(default_object "AUTOHINT") with
cache_function = cache_autohint;
- load_function = (fun _ -> cache_autohint);
+ load_function = load_autohint;
+ open_function = open_autohint;
subst_function = subst_autohint;
classify_function = classify_autohint; }
@@ -999,7 +1062,7 @@ let default_prepare_hint_ident = Id.of_string "H"
exception Found of constr * types
-let prepare_hint check env init (sigma,c) =
+let prepare_hint check (poly,local) env init (sigma,c) =
let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
(* We re-abstract over uninstantiated evars.
It is actually a bit stupid to generalize over evars since the first
@@ -1012,7 +1075,7 @@ let prepare_hint check env init (sigma,c) =
(* We skip the test whether args is the identity or not *)
let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
- if not (Int.Set.is_empty (free_rels t)) then
+ if not (closed0 c) then
error "Hints with holes dependent on a bound variable not supported.";
if occur_existential t then
(* Not clever enough to construct dependency graph of evars *)
@@ -1029,13 +1092,18 @@ let prepare_hint check env init (sigma,c) =
let c' = iter c in
if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
- IsConstr (c', diff)
+ if poly then IsConstr (c', diff)
+ else if local then IsConstr (c', diff)
+ else (Global.push_context_set false diff;
+ IsConstr (c', Univ.ContextSet.empty))
let interp_hints poly =
fun h ->
- let f c =
- let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in
- prepare_hint true (Global.env()) Evd.empty (evd,c) in
+ let env = (Global.env()) in
+ let sigma = Evd.from_env env in
+ let f poly c =
+ let evd,c = Constrintern.interp_open_constr env sigma c in
+ prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
let fref r =
let gr = global_with_alias r in
Dumpglob.add_glob (loc_of_reference r) gr;
@@ -1048,7 +1116,7 @@ let interp_hints poly =
| HintsReference c ->
let gr = global_with_alias c in
(PathHints [gr], poly, IsGlobRef gr)
- | HintsConstr c -> (PathAny, poly, f c)
+ | HintsConstr c -> (PathAny, poly, f poly c)
in
let fres (pri, b, r) =
let path, poly, gr = fi r in
@@ -1083,7 +1151,8 @@ let add_hints local dbnames0 h =
if String.List.mem "nocore" dbnames0 then
error "The hint database \"nocore\" is meant to stay empty.";
let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
- let env = Global.env() and sigma = Evd.empty in
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
match h with
| HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
| HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
@@ -1103,7 +1172,7 @@ let expand_constructor_hints env sigma lems =
(fun i -> IsConstr (mkConstructU ((ind,i+1),u),
Univ.ContextSet.empty))
| _ ->
- [prepare_hint false env sigma (evd,lem)]) lems
+ [prepare_hint false (false,true) env sigma (evd,lem)]) lems
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
@@ -1111,8 +1180,8 @@ let expand_constructor_hints env sigma lems =
let add_hint_lemmas env sigma eapply lems hint_db =
let lems = expand_constructor_hints env sigma lems in
let hintlist' =
- List.map_append (make_resolves env sigma (eapply,true,false) None true) lems in
- Hint_db.add_list hintlist' hint_db
+ List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in
+ Hint_db.add_list env sigma hintlist' hint_db
let make_local_hint_db env sigma ts eapply lems =
let sign = Environ.named_context env in
@@ -1122,7 +1191,7 @@ let make_local_hint_db env sigma ts eapply lems =
in
let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
add_hint_lemmas env sigma eapply lems
- (Hint_db.add_list hintlist (Hint_db.empty ts false))
+ (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
let make_local_hint_db =
if Flags.profile then
@@ -1146,13 +1215,14 @@ let make_db_list dbnames =
(* Functions for printing the hints *)
(**************************************************************************)
-let pr_autotactic =
- function
- | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
- | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
- | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c)
- | Res_pf_THEN_trivial_fail (c,clenv) ->
- (str"apply " ++ pr_constr c ++ str" ; trivial")
+let pr_hint_elt (c, _, _) = pr_constr c
+
+let pr_hint h = match h.obj with
+ | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c)
+ | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c)
+ | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
+ | Res_pf_THEN_trivial_fail (c, _) ->
+ (str"apply " ++ pr_hint_elt c ++ str" ; trivial")
| Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
| Extern tac ->
let env =
@@ -1163,11 +1233,11 @@ let pr_autotactic =
in
(str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
-let pr_hint (id, v) =
- (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+let pr_id_hint (id, v) =
+ (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
let pr_hint_list hintlist =
- (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
+ (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
let pr_hints_db (name,db,hintlist) =
(str "In the database " ++ str name ++ str ":" ++
@@ -1266,3 +1336,27 @@ let pr_searchtable () =
in
Hintdbmap.fold fold !searchtable (mt ())
+let print_mp mp =
+ try
+ let qid = Nametab.shortest_qualid_of_module mp in
+ str " from " ++ pr_qualid qid
+ with Not_found -> mt ()
+
+let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
+
+let warn h x =
+ let hint = pr_hint h in
+ let (mp, _, _) = KerName.repr h.uid in
+ let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
+ Proofview.tclUNIT x
+
+let run_hint tac k = match !warn_hint with
+| `LAX -> k tac.obj
+| `WARN ->
+ if is_imported tac then k tac.obj
+ else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
+| `STRICT ->
+ if is_imported tac then k tac.obj
+ else Proofview.tclZERO (UserError ("", (str "Tactic failure.")))
+
+let repr_hint h = h.obj
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 958cca1c..3a0521f6 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array
(** Pre-created hint databases *)
-type 'a auto_tactic_ast =
+type 'a hint_ast =
| Res_pf of 'a (* Hint Apply *)
| ERes_pf of 'a (* Hint EApply *)
| Give_exact of 'a
@@ -36,13 +36,14 @@ type 'a auto_tactic_ast =
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
| Extern of Tacexpr.glob_tactic_expr (* Hint Extern *)
-type 'a auto_tactic
+type hint
+type raw_hint = constr * types * Univ.universe_context_set
type hints_path_atom =
| PathHints of global_reference list
| PathAny
-type 'a gen_auto_tactic = private {
+type 'a with_metadata = private {
pri : int; (** A number between 0 and 4, 4 = lower priority *)
poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *)
pat : constr_pattern option; (** A pattern for the concl of the Goal *)
@@ -50,7 +51,7 @@ type 'a gen_auto_tactic = private {
code : 'a; (** the tactic to apply when the concl matches pat *)
}
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
type search_entry
@@ -69,6 +70,7 @@ type hints_path =
val normalize_path : hints_path -> hints_path
val path_matches : hints_path -> hints_path_atom list -> bool
val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds
val pp_hints_path : hints_path -> Pp.std_ppcmds
module Hint_db :
@@ -76,28 +78,28 @@ module Hint_db :
type t
val empty : transparent_state -> bool -> t
val find : global_reference -> t -> search_entry
- val map_none : t -> pri_auto_tactic list
+ val map_none : t -> full_hint list
(** All hints associated to the reference *)
- val map_all : global_reference -> t -> pri_auto_tactic list
+ val map_all : global_reference -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments, _not_ using the discrimination net. *)
- val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+ val map_existential : (global_reference * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments and using the discrimination net. *)
- val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+ val map_eauto : (global_reference * constr array) -> constr -> t -> full_hint list
(** All hints associated to the reference, respecting modes if evars appear in the
arguments. *)
- val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
+ val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list
- val add_one : hint_entry -> t -> t
- val add_list : (hint_entry) list -> t -> t
+ val add_one : env -> evar_map -> hint_entry -> t -> t
+ val add_list : env -> evar_map -> hint_entry list -> t -> t
val remove_one : global_reference -> t -> t
val remove_list : global_reference list -> t -> t
- val iter : (global_reference option -> bool array list -> pri_auto_tactic list -> unit) -> t -> unit
+ val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
val transparent_state : t -> transparent_state
@@ -151,8 +153,9 @@ val interp_hints : polymorphic -> hints_expr -> hints_entry
val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
-val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map ->
- open_constr -> hint_term
+val prepare_hint : bool (* Check no remaining evars *) ->
+ (bool * bool) (* polymorphic or monomorphic, local or global *) ->
+ env -> evar_map -> open_constr -> hint_term
(** [make_exact_entry pri (c, ctyp)].
[c] is the term given as an exact proof to solve the goal;
@@ -197,12 +200,12 @@ val make_extern :
int -> constr_pattern option -> Tacexpr.glob_tactic_expr
-> hint_entry
-val run_auto_tactic : 'a auto_tactic ->
- ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+val run_hint : hint ->
+ ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
(** This function is for backward compatibility only, not to use in newly
written code. *)
-val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+val repr_hint : hint -> (raw_hint * clausenv) hint_ast
val extern_intern_tac :
(patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
@@ -227,7 +230,7 @@ val pr_applicable_hint : unit -> std_ppcmds
val pr_hint_ref : global_reference -> std_ppcmds
val pr_hint_db_by_name : hint_db_name -> std_ppcmds
val pr_hint_db : Hint_db.t -> std_ppcmds
-val pr_autotactic : (constr * 'a) auto_tactic -> Pp.std_ppcmds
+val pr_hint : hint -> Pp.std_ppcmds
(** Hook for changing the initialization of auto *)
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 4b94f420..95f3af57 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -411,7 +411,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
let extract_eq_args gl = function
| MonomorphicLeibnizEq (e1,e2) ->
- let t = pf_type_of gl e1 in (t,e1,e2)
+ let t = pf_unsafe_type_of gl e1 in (t,e1,e2)
| PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
| HeterogenousEq (t1,e1,t2,e2) ->
if pf_conv_x gl t1 t2 then (t1,e1,e2)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5502356f..ef115aea 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl =
let refl_term = eqdata.Coqlib.refl in
let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in
let refl = mkApp (refl_term, [|eqnty; rhs|]) in
- let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in
+ let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in
let args = refl :: args in
build_concl eqns args (succ n) restlist
in
let (newconcl, args) = build_concl [] [] 0 realargs in
let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in
- let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in
+ let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in
(* OK - this predicate should now be usable by res_elimination_then to
do elimination on the conclusion. *)
predicate, args
@@ -437,7 +437,7 @@ let raw_inversion inv_kind id status names =
let concl = Proofview.Goal.concl gl in
let c = mkVar id in
let (ind, t) =
- try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c)
+ try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
with UserError _ ->
let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
Errors.errorlabstrm "" msg
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9a64b03f..8ca62217 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -124,7 +124,7 @@ let rec add_prods_sign env sigma t =
add_prods_sign (push_named (id,Some c1,t1) env) sigma b'
| _ -> (env,t)
-(* [dep_option] indicates wether the inversion lemma is dependent or not.
+(* [dep_option] indicates whether the inversion lemma is dependent or not.
If it is dependent and I is of the form (x_bar:T_bar)(I t_bar) then
the stated goal will be (x_bar:T_bar)(H:(I t_bar))(P t_bar H)
where P:(x_bar:T_bar)(H:(I x_bar))[sort].
@@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
errorlabstrm "lemma_inversion"
(str"Computed inversion goal was not closed in initial signature.");
*)
- let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in
+ let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
let pf =
fst (Proof.run_tactic env (
tclTHEN intro (onLastHypId inv_op)) pf)
@@ -229,7 +229,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let add_inversion_lemma name env sigma t sort dep inv_op =
let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
- let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in
+ let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
+ ~univs:(snd ctx) invProof in
let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
()
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index ac8b4923..e8a7c0f6 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -52,7 +52,7 @@ let try_find_global_reference dir s =
let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
try Nametab.global_of_path sp
with Not_found ->
- anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting"))
+ anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting")
let find_reference dir s =
let gr = lazy (try_find_global_reference dir s) in
@@ -76,25 +76,6 @@ let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
let coq_all = find_global ["Init"; "Logic"] "all"
let impl = find_global ["Program"; "Basics"] "impl"
-(* let coq_inverse = lazy (gen_constant ["Program"; "Basics"] "flip") *)
-
-(* let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |]) *)
-
-(* let forall_relation = lazy (gen_constant ["Classes"; "Morphisms"] "forall_relation") *)
-(* let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation") *)
-(* let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") *)
-(* let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation") *)
-(* let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation") *)
-(* let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation") *)
-(* let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation") *)
-(* let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") *)
-(* let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) *)
-
-(* let proper_type = lazy (Universes.constr_of_global (Lazy.force proper_class).cl_impl) *)
-(* let proper_proxy_type = lazy (Universes.constr_of_global (Lazy.force proper_proxy_class).cl_impl) *)
-
-
-
(** Bookkeeping which evars are constraints so that we can
remove them at the end of the tactic. *)
@@ -226,6 +207,7 @@ end) = struct
let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in
match kind_of_term t, l with
| Prod (na, ty, b), obj :: cstrs ->
+ let b = Reductionops.nf_betaiota (goalevars evars) b in
if noccurn 1 b (* non-dependent product *) then
let ty = Reductionops.nf_betaiota (goalevars evars) ty in
let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
@@ -380,7 +362,7 @@ end
let type_app_poly env env evd f args =
let evars, c = app_poly_nocheck env evd f args in
- let evd', t = Typing.e_type_of env (goalevars evars) c in
+ let evd', t = Typing.type_of env (goalevars evars) c in
(evd', cstrevars evars), c
module PropGlobal = struct
@@ -452,7 +434,6 @@ let convertible env evd x y =
Reductionops.is_conv_leq env evd x y
type hypinfo = {
- env : env;
prf : constr;
car : constr;
rel : constr;
@@ -472,7 +453,7 @@ let rec decompose_app_rel env evd t =
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
let (f', argl, argr) = decompose_app_rel env evd arg in
- let ty = Typing.type_of env evd argl in
+ let ty = Typing.unsafe_type_of env evd argl in
let f'' = mkLambda (Name default_dependent_ident, ty,
mkLambda (Name (Id.of_string "y"), lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
@@ -498,7 +479,7 @@ let decompose_applied_relation env sigma (c,l) =
let sort = sort_of_rel env sigma equiv in
let args = Array.map_of_list (fun h -> h.Clenv.hole_evar) holes in
let value = mkApp (c, args) in
- Some (sigma, { env=env; prf=value;
+ Some (sigma, { prf=value;
car=ty1; rel = equiv; sort = Sorts.is_prop sort;
c1=c1; c2=c2; holes })
in
@@ -510,10 +491,6 @@ let decompose_applied_relation env sigma (c,l) =
| Some c -> c
| None -> error "Cannot find an homogeneous relation to rewrite."
-let decompose_applied_relation_expr env sigma (is, (c,l)) =
- let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma (c,l) in
- decompose_applied_relation env sigma cbl
-
let rewrite_db = "rewrite"
let conv_transparent_state = (Id.Pred.empty, Cpred.full)
@@ -588,24 +565,12 @@ let general_rewrite_unif_flags () =
Unification.resolve_evars = true
}
-let refresh_hypinfo env sigma hypinfo c =
- let sigma, hypinfo = match hypinfo with
- | None ->
- decompose_applied_relation_expr env sigma c
- | Some hypinfo ->
- if hypinfo.env != env then
- (* If the lemma actually generates existential variables, we cannot
- use it here as it will polute the evar map with existential variables
- that might not ever get instantiated (e.g. if we rewrite under a
- binder and need to refresh [c] again) *)
- (* TODO: remove bindings in sigma corresponding to c *)
- decompose_applied_relation_expr env sigma c
- else sigma, hypinfo
- in
+let refresh_hypinfo env sigma (is, cb) =
+ let sigma, cbl = Tacinterp.interp_open_constr_with_bindings is env sigma cb in
+ let sigma, hypinfo = decompose_applied_relation env sigma cbl in
let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
sigma, (car, rel, prf, c1, c2, holes, sort)
-
(** FIXME: write this in the new monad interface *)
let solve_remaining_by env sigma holes by =
match by with
@@ -647,13 +612,19 @@ let poly_inverse sort =
type rewrite_proof =
| RewPrf of constr * constr
+ (** A Relation (R : rew_car -> rew_car -> Prop) and a proof of R rew_from rew_to *)
| RewCast of cast_kind
+ (** A proof of convertibility (with casts) *)
type rewrite_result_info = {
- rew_car : constr;
- rew_from : constr;
- rew_to : constr;
- rew_prf : rewrite_proof;
+ rew_car : constr ;
+ (** A type *)
+ rew_from : constr ;
+ (** A term of type rew_car *)
+ rew_to : constr ;
+ (** A term of type rew_car *)
+ rew_prf : rewrite_proof ;
+ (** A proof of rew_from == rew_to *)
rew_evars : evars;
}
@@ -662,9 +633,17 @@ type rewrite_result =
| Identity
| Success of rewrite_result_info
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
- (bool (* prop *) * constr option) -> evars ->
- 'a * rewrite_result
+type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
+ env : Environ.env ;
+ unfresh : Id.t list ; (* Unfresh names *)
+ term1 : constr ;
+ ty1 : types ; (* first term and its type (convertible to rew_from) *)
+ cstr : (bool (* prop *) * constr option) ;
+ evars : evars }
+
+type 'a pure_strategy = { strategy :
+ 'a strategy_input ->
+ 'a * rewrite_result (* the updated state and the "result" *) }
type strategy = unit pure_strategy
@@ -719,7 +698,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
let rew_prf = RewPrf (rel, prf) in
let rew = { rew_car = car; rew_from = c1; rew_to = c2; rew_prf; rew_evars; } in
let rew = if l2r then rew else symmetry env sort rew in
- Some ((), rew)
+ Some rew
with
| e when Class_tactics.catchable e -> None
| Reduction.NotConvertible -> None
@@ -763,7 +742,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
let morphargs, morphobjs = Array.chop first args in
let morphargs', morphobjs' = Array.chop first args' in
let appm = mkApp(m, morphargs) in
- let appmtype = Typing.type_of env (goalevars evars) appm in
+ let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in
let cstrs = List.map
(Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf))
(Array.to_list morphobjs')
@@ -829,42 +808,47 @@ let coerce env avoid cstr res =
let rel, prf = get_rew_prf res in
apply_constraint env avoid res.rew_car rel prf cstr res
-let apply_rule unify loccs : ('a * int) pure_strategy =
+let apply_rule unify loccs : int pure_strategy =
let (nowhere_except_in,occs) = convert_occs loccs in
let is_occ occ =
if nowhere_except_in
then List.mem occ occs
else not (List.mem occ occs)
in
- fun (hypinfo, occ) env avoid t ty cstr evars ->
- let unif = if isEvar t then None else unify hypinfo env evars t in
+ { strategy = fun { state = occ ; env ; unfresh ;
+ term1 = t ; ty1 = ty ; cstr ; evars } ->
+ let unif = if isEvar t then None else unify env evars t in
match unif with
- | None -> ((hypinfo, occ), Fail)
- | Some (hypinfo', rew) ->
+ | None -> (occ, Fail)
+ | Some rew ->
let occ = succ occ in
- if not (is_occ occ) then ((hypinfo, occ), Fail)
- else if eq_constr t rew.rew_to then ((hypinfo, occ), Identity)
+ if not (is_occ occ) then (occ, Fail)
+ else if eq_constr t rew.rew_to then (occ, Identity)
else
let res = { rew with rew_car = ty } in
let rel, prf = get_rew_prf res in
- let res = Success (apply_constraint env avoid rew.rew_car rel prf cstr res) in
- ((hypinfo', occ), res)
-
-let apply_lemma l2r flags oc by loccs : strategy =
- fun () env avoid t ty cstr (sigma, cstrs) ->
+ let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in
+ (occ, res)
+ }
+
+let apply_lemma l2r flags oc by loccs : strategy = { strategy =
+ fun ({ state = () ; env ; term1 = t ; evars = (sigma, cstrs) } as input) ->
let sigma, c = oc sigma in
let sigma, hypinfo = decompose_applied_relation env sigma c in
let { c1; c2; car; rel; prf; sort; holes } = hypinfo in
let rew = (car, rel, prf, c1, c2, holes, sort) in
let evars = (sigma, cstrs) in
- let unify () env evars t =
+ let unify env evars t =
let rew = unify_eqn rew l2r flags env evars by t in
match rew with
| None -> None
- | Some rew -> Some ((), rew)
+ | Some rew -> Some rew
in
- let _, res = apply_rule unify loccs ((), 0) env avoid t ty cstr evars in
+ let _, res = (apply_rule unify loccs).strategy { input with
+ state = 0 ;
+ evars } in
(), res
+ }
let e_app_poly env evars f args =
let evars', c = app_poly_nocheck env !evars f args in
@@ -944,7 +928,8 @@ let unfold_match env sigma sk app =
let is_rew_cast = function RewCast _ -> true | _ -> false
let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
- let rec aux state env avoid t ty (prop, cstr) evars =
+ let rec aux { state ; env ; unfresh ;
+ term1 = t ; ty1 = ty ; cstr = (prop, cstr) ; evars } =
let cstr' = Option.map (fun c -> (ty, Some c)) cstr in
match kind_of_term t with
| App (m, args) ->
@@ -956,7 +941,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
state, (None :: acc, evars, progress)
else
let argty = Retyping.get_type_of env (goalevars evars) arg in
- let state, res = s state env avoid arg argty (prop,None) evars in
+ let state, res = s.strategy { state ; env ;
+ unfresh ;
+ term1 = arg ; ty1 = argty ;
+ cstr = (prop,None) ;
+ evars } in
let res' =
match res with
| Identity ->
@@ -980,7 +969,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
| Some r -> not (is_rew_cast r.rew_prf)) args'
then
let evars', prf, car, rel, c1, c2 =
- resolve_morphism env avoid t m args args' (prop, cstr') evars'
+ resolve_morphism env unfresh t m args args' (prop, cstr') evars'
in
let res = { rew_car = ty; rew_from = c1;
rew_to = c2; rew_prf = RewPrf (rel, prf);
@@ -1008,7 +997,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
evars, Some cstr', m, mty, args, Array.of_list args
| None -> evars, None, m, mty, argsl, args
in
- let state, m' = s state env avoid m mty (prop, cstr') evars in
+ let state, m' = s.strategy { state ; env ; unfresh ;
+ term1 = m ; ty1 = mty ;
+ cstr = (prop, cstr') ; evars } in
match m' with
| Fail -> rewrite_args state None (* Standard path, try rewrite on arguments *)
| Identity -> rewrite_args state (Some false)
@@ -1031,7 +1022,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let res =
match prf with
| RewPrf (rel, prf) ->
- Success (apply_constraint env avoid res.rew_car
+ Success (apply_constraint env unfresh res.rew_car
rel prf (prop,cstr) res)
| _ -> Success res
in state, res
@@ -1045,7 +1036,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
else TypeGlobal.arrow_morphism
in
let (evars', mor), unfold = arr env evars tx tb x b in
- let state, res = aux state env avoid mor ty (prop,cstr) evars' in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = mor ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
let res =
match res with
| Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1075,7 +1068,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in
(app_poly_sort prop env evars forall [| dom; lam |]), TypeGlobal.unfold_forall
in
- let state, res = aux state env avoid app ty (prop,cstr) evars' in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = app ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars = evars' } in
let res =
match res with
| Success r -> Success { r with rew_to = unfold r.rew_to }
@@ -1111,11 +1106,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
(* | _ -> b') *)
| Lambda (n, t, b) when flags.under_lambdas ->
- let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in
+ let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
let env' = Environ.push_rel (n', None, t) env in
let bty = Retyping.get_type_of env' (goalevars evars) b in
let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
- let state, b' = s state env' avoid b bty (prop, unlift env evars cstr) evars in
+ let state, b' = s.strategy { state ; env = env' ; unfresh ;
+ term1 = b ; ty1 = bty ;
+ cstr = (prop, unlift env evars cstr) ;
+ evars } in
let res =
match b' with
| Success r ->
@@ -1140,13 +1138,15 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
let cty = Retyping.get_type_of env (goalevars evars) c in
let evars', eqty = app_poly_sort prop env evars coq_eq [| cty |] in
let cstr' = Some eqty in
- let state, c' = s state env avoid c cty (prop, cstr') evars' in
+ let state, c' = s.strategy { state ; env ; unfresh ;
+ term1 = c ; ty1 = cty ;
+ cstr = (prop, cstr') ; evars = evars' } in
let state, res =
match c' with
| Success r ->
let case = mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs) in
let res = make_leibniz_proof env case ty r in
- state, Success (coerce env avoid (prop,cstr) res)
+ state, Success (coerce env unfresh (prop,cstr) res)
| Fail | Identity ->
if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then
let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in
@@ -1156,7 +1156,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
if not (Option.is_empty found) then
(state, found, fun x -> lift 1 br :: acc x)
else
- let state, res = s state env avoid br ty (prop,cstr) evars in
+ let state, res = s.strategy { state ; env ; unfresh ;
+ term1 = br ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
match res with
| Success r -> (state, Some r, fun x -> mkRel 1 :: acc x)
| Fail | Identity -> (state, None, fun x -> lift 1 br :: acc x))
@@ -1171,7 +1173,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> state, c'
| Some (cst, _, t', eff (*FIXME*)) ->
- let state, res = aux state env avoid t' ty (prop,cstr) evars in
+ let state, res = aux { state ; env ; unfresh ;
+ term1 = t' ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } in
let res =
match res with
| Success prf ->
@@ -1185,11 +1189,11 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
match res with
| Success r ->
let rel, prf = get_rew_prf r in
- Success (apply_constraint env avoid r.rew_car rel prf (prop,cstr) r)
+ Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r)
| Fail | Identity -> res
in state, res
| _ -> state, Fail
- in aux
+ in { strategy = aux }
let all_subterms = subterm true default_flags
let one_subterm = subterm false default_flags
@@ -1197,11 +1201,13 @@ let one_subterm = subterm false default_flags
(** Requires transitivity of the rewrite step, if not a reduction.
Not tail-recursive. *)
-let transitivity state env avoid prop (res : rewrite_result_info) (next : 'a pure_strategy) :
+let transitivity state env unfresh prop (res : rewrite_result_info) (next : 'a pure_strategy) :
'a * rewrite_result =
let state, nextres =
- next state env avoid res.rew_to res.rew_car
- (prop, get_opt_rew_rel res.rew_prf) res.rew_evars
+ next.strategy { state ; env ; unfresh ;
+ term1 = res.rew_to ; ty1 = res.rew_car ;
+ cstr = (prop, get_opt_rew_rel res.rew_prf) ;
+ evars = res.rew_evars }
in
let res =
match nextres with
@@ -1238,15 +1244,16 @@ module Strategies =
struct
let fail : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- state, Fail
+ { strategy = fun { state } -> state, Fail }
let id : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- state, Identity
+ { strategy = fun { state } -> state, Identity }
let refl : 'a pure_strategy =
- fun state env avoid t ty (prop,cstr) evars ->
+ { strategy =
+ fun { state ; env ;
+ term1 = t ; ty1 = ty ;
+ cstr = (prop,cstr) ; evars } ->
let evars, rel = match cstr with
| None ->
let mkr = if prop then PropGlobal.mk_relation else TypeGlobal.mk_relation in
@@ -1265,38 +1272,43 @@ module Strategies =
let res = Success { rew_car = ty; rew_from = t; rew_to = t;
rew_prf = RewPrf (rel, proof); rew_evars = evars }
in state, res
+ }
- let progress (s : 'a pure_strategy) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = s state env avoid t ty cstr evars in
+ let progress (s : 'a pure_strategy) : 'a pure_strategy = { strategy =
+ fun input ->
+ let state, res = s.strategy input in
match res with
| Fail -> state, Fail
| Identity -> state, Fail
| Success r -> state, Success r
+ }
- let seq first snd : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = first state env avoid t ty cstr evars in
+ let seq first snd : 'a pure_strategy = { strategy =
+ fun ({ env ; unfresh ; cstr } as input) ->
+ let state, res = first.strategy input in
match res with
| Fail -> state, Fail
- | Identity -> snd state env avoid t ty cstr evars
- | Success res -> transitivity state env avoid (fst cstr) res snd
+ | Identity -> snd.strategy { input with state }
+ | Success res -> transitivity state env unfresh (fst cstr) res snd
+ }
- let choice fst snd : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
- let state, res = fst state env avoid t ty cstr evars in
+ let choice fst snd : 'a pure_strategy = { strategy =
+ fun input ->
+ let state, res = fst.strategy input in
match res with
- | Fail -> snd state env avoid t ty cstr evars
+ | Fail -> snd.strategy { input with state }
| Identity | Success _ -> state, res
+ }
let try_ str : 'a pure_strategy = choice str id
- let check_interrupt str s e l c t r ev =
+ let check_interrupt str input =
Control.check_for_interrupt ();
- str s e l c t r ev
-
+ str input
+
let fix (f : 'a pure_strategy -> 'a pure_strategy) : 'a pure_strategy =
- let rec aux state = f (fun state -> check_interrupt aux state) state in aux
+ let rec aux input = (f { strategy = fun input -> check_interrupt aux input }).strategy input in
+ { strategy = aux }
let any (s : 'a pure_strategy) : 'a pure_strategy =
fix (fun any -> try_ (seq s any))
@@ -1332,16 +1344,17 @@ module Strategies =
(List.map (fun hint -> (inj_open hint, hint.Autorewrite.rew_l2r,
hint.Autorewrite.rew_tac)) rules)
- let hints (db : string) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let hints (db : string) : 'a pure_strategy = { strategy =
+ fun ({ term1 = t } as input) ->
let rules = Autorewrite.find_matches db t in
let lemma hint = (inj_open hint, hint.Autorewrite.rew_l2r,
hint.Autorewrite.rew_tac) in
let lems = List.map lemma rules in
- lemmas lems state env avoid t ty cstr evars
+ (lemmas lems).strategy input
+ }
- let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy =
+ fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } ->
let rfn, ckind = Redexpr.reduction_of_red_expr env r in
let evars', t' = rfn env (goalevars evars) t in
if eq_constr t' t then
@@ -1350,9 +1363,10 @@ module Strategies =
state, Success { rew_car = ty; rew_from = t; rew_to = t';
rew_prf = RewCast ckind;
rew_evars = evars', cstrevars evars }
+ }
- let fold_glob c : 'a pure_strategy =
- fun state env avoid t ty cstr evars ->
+ let fold_glob c : 'a pure_strategy = { strategy =
+ fun { state ; env ; term1 = t ; ty1 = ty ; cstr ; evars } ->
(* let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
let sigma, c = Pretyping.understand_tcc env (goalevars evars) c in
let unfolded =
@@ -1367,23 +1381,23 @@ module Strategies =
rew_prf = RewCast DEFAULTcast;
rew_evars = (sigma, snd evars) }
with e when Errors.noncritical e -> state, Fail
+ }
end
-(** The strategy for a single rewrite, dealing with occurences. *)
+(** The strategy for a single rewrite, dealing with occurrences. *)
(** A dummy initial clauseenv to avoid generating initial evars before
even finding a first application of the rewriting lemma, in setoid_rewrite
mode *)
-let rewrite_with l2r flags c occs : strategy =
- fun () env avoid t ty cstr (sigma, cstrs) ->
- let hypinfo = None in
- let unify hypinfo env evars t =
+let rewrite_with l2r flags c occs : strategy = { strategy =
+ fun ({ state = () } as input) ->
+ let unify env evars t =
let (sigma, cstrs) = evars in
let ans =
- try Some (refresh_hypinfo env sigma hypinfo c)
+ try Some (refresh_hypinfo env sigma c)
with e when Class_tactics.catchable e -> None
in
match ans with
@@ -1392,19 +1406,22 @@ let rewrite_with l2r flags c occs : strategy =
let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in
match rew with
| None -> None
- | Some rew -> Some (None, rew) (** reset the hypinfo cache *)
+ | Some rew -> Some rew
in
let app = apply_rule unify occs in
let strat =
Strategies.fix (fun aux ->
Strategies.choice app (subterm true default_flags aux))
in
- let _, res = strat (hypinfo, 0) env avoid t ty cstr (sigma, cstrs) in
- ((), res)
+ let _, res = strat.strategy { input with state = 0 } in
+ ((), res)
+ }
-let apply_strategy (s : strategy) env avoid concl (prop, cstr) evars =
+let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
let ty = Retyping.get_type_of env (goalevars evars) concl in
- let _, res = s () env avoid concl ty (prop, Some cstr) evars in
+ let _, res = s.strategy { state = () ; env ; unfresh ;
+ term1 = concl ; ty1 = ty ;
+ cstr = (prop, Some cstr) ; evars } in
res
let solve_constraints env (evars,cstrs) =
@@ -1506,7 +1523,7 @@ let newfail n s =
let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let open Proofview.Notations in
- let treat sigma (res, is_hyp) =
+ let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None -> Proofview.tclUNIT ()
@@ -1514,7 +1531,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
- match is_hyp, prf with
+ match clause, prf with
| Some id, Some p ->
let tac = Proofview.Refine.refine ~unsafe:false (fun h -> (h, p)) <*> Proofview.Unsafe.tclNEWGOALS gls in
Proofview.Unsafe.tclEVARS undef <*>
@@ -1546,17 +1563,25 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let ty, is_hyp =
- match clause with
- | Some id -> Environ.named_type id env, Some id
- | None -> concl, None
+ let ty = match clause with
+ | None -> concl
+ | Some id -> Environ.named_type id env
+ in
+ let env = match clause with
+ | None -> env
+ | Some id ->
+ (** Only consider variables not depending on [id] *)
+ let ctx = Environ.named_context env in
+ let filter decl = not (occur_var_in_decl env id decl) in
+ let nctx = List.filter filter ctx in
+ Environ.reset_with_named_context (Environ.val_of_named_context nctx) env
in
try
let res =
- cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
+ cl_rewrite_clause_aux ?abs strat env [] sigma ty clause
in
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
- treat sigma (res, is_hyp) <*>
+ treat sigma res <*>
(** For compatibility *)
beta <*> opt_beta <*> Proofview.shelve_unifiable
with
@@ -1583,13 +1608,13 @@ let cl_rewrite_clause l left2right occs clause gl =
let strat = rewrite_with left2right (general_rewrite_unif_flags ()) l occs in
cl_rewrite_clause_strat strat clause gl
-let apply_glob_constr c l2r occs = (); fun () env avoid t ty cstr evars ->
+let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) ->
let c sigma =
let (sigma, c) = Pretyping.understand_tcc env sigma c in
(sigma, (c, NoBindings))
in
let flags = general_rewrite_unif_flags () in
- apply_lemma l2r flags c None occs () env avoid t ty cstr evars
+ (apply_lemma l2r flags c None occs).strategy input
let interp_glob_constr_list env =
let make c = (); fun sigma ->
@@ -1653,16 +1678,18 @@ let rec strategy_of_ast = function
| Compose -> Strategies.seq
| Choice -> Strategies.choice
in f' s' t'
- | StratConstr (c, b) -> apply_glob_constr (fst c) b AllOccurrences
+ | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences }
| StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id
- | StratTerms l ->
- (fun () env avoid t ty cstr evars ->
+ | StratTerms l -> { strategy =
+ (fun ({ state = () ; env } as input) ->
let l' = interp_glob_constr_list env (List.map fst l) in
- Strategies.lemmas l' () env avoid t ty cstr evars)
- | StratEval r ->
- (fun () env avoid t ty cstr evars ->
+ (Strategies.lemmas l').strategy input)
+ }
+ | StratEval r -> { strategy =
+ (fun ({ state = () ; env ; evars } as input) ->
let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in
- Strategies.reduce r_interp () env avoid t ty cstr (sigma,cstrevars evars))
+ (Strategies.reduce r_interp).strategy { input with
+ evars = (sigma,cstrevars evars) }) }
| StratFold c -> Strategies.fold_glob (fst c)
@@ -1751,11 +1778,13 @@ let proper_projection r ty =
it_mkLambda_or_LetIn app ctx
let declare_projection n instance_id r =
- let c,uctx = Universes.fresh_global_instance (Global.env()) r in
let poly = Global.is_polymorphic r in
- let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let evd,c = Evd.fresh_global env sigma r in
+ let ty = Retyping.get_type_of env sigma c in
let term = proper_projection c ty in
- let typ = Typing.type_of (Global.env ()) Evd.empty term in
+ let typ = Typing.unsafe_type_of env sigma term in
let ctx, typ = decompose_prod_assum typ in
let typ =
let n =
@@ -1777,18 +1806,19 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
+ let pl, ctx = Evd.universe_context sigma in
let cst =
- Declare.definition_entry ~types:typ ~poly ~univs:(Univ.ContextSet.to_context uctx)
- term
+ Declare.definition_entry ~types:typ ~poly ~univs:ctx term
in
ignore(Declare.declare_constant n
(Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
let build_morphism_signature m =
let env = Global.env () in
- let m,ctx = Constrintern.interp_constr env Evd.empty m in
- let sigma = Evd.from_env ~ctx env in
- let t = Typing.type_of env sigma m in
+ let sigma = Evd.from_env env in
+ let m,ctx = Constrintern.interp_constr env sigma m in
+ let sigma = Evd.from_ctx ctx in
+ let t = Typing.unsafe_type_of env sigma m in
let cstrs =
let rec aux t =
match kind_of_term t with
@@ -1798,7 +1828,7 @@ let build_morphism_signature m =
in aux t
in
let evars, t', sig_, cstrs =
- PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t cstrs None in
+ PropGlobal.build_signature (sigma, Evar.Set.empty) env t cstrs None in
let evd = ref evars in
let _ = List.iter
(fun (ty, rel) ->
@@ -1815,9 +1845,10 @@ let build_morphism_signature m =
let default_morphism sign m =
let env = Global.env () in
- let t = Typing.type_of env Evd.empty m in
+ let sigma = Evd.from_env env in
+ let t = Typing.unsafe_type_of env sigma m in
let evars, _, sign, cstrs =
- PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign)
+ PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
in
let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
@@ -1848,9 +1879,9 @@ let add_morphism_infer glob m n =
let poly = Flags.is_universe_polymorphism () in
let instance_id = add_suffix n "_Proper" in
let instance = build_morphism_signature m in
- let evd = Evd.empty (*FIXME *) in
+ let evd = Evd.from_env (Global.env ()) in
if Lib.is_modtype () then
- let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id
+ let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
(None,poly,(instance,Univ.UContext.empty),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
@@ -1967,13 +1998,14 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
(** Setoid rewriting when called with "rewrite" *)
let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in
- let unify () env evars t = unify_abs res l2r sort env evars t in
+ let unify env evars t = unify_abs res l2r sort env evars t in
let app = apply_rule unify occs in
let recstrat aux = Strategies.choice app (subterm true general_rewrite_flags aux) in
let substrat = Strategies.fix recstrat in
- let strat () env avoid t ty cstr evars =
- let _, res = substrat ((), 0) env avoid t ty cstr evars in
+ let strat = { strategy = fun ({ state = () } as input) ->
+ let _, res = substrat.strategy { input with state = 0 } in
(), res
+ }
in
let origsigma = project gl in
init_setoid ();
@@ -2011,7 +2043,7 @@ let setoid_proof ty fn fallback =
try
let rel, _, _ = decompose_app_rel env sigma concl in
let evm = sigma in
- let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
+ let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in
(try init_setoid () with _ -> raise Not_found);
fn env sigma car rel
with e -> Proofview.tclZERO e
@@ -2070,7 +2102,7 @@ let setoid_transitivity c =
let setoid_symmetry_in id =
Proofview.V82.tactic (fun gl ->
- let ctype = pf_type_of gl (mkVar id) in
+ let ctype = pf_unsafe_type_of gl (mkVar id) in
let binders,concl = decompose_prod_assum ctype in
let (equiv, args) = decompose_app concl in
let rec split_last_two = function
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index cae00f5a..40a18ac4 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -55,10 +55,7 @@ type rewrite_result =
| Identity
| Success of rewrite_result_info
-type 'a pure_strategy = 'a -> Environ.env -> Id.t list -> constr -> types ->
- (bool (* prop *) * constr option) -> evars -> 'a * rewrite_result
-
-type strategy = unit pure_strategy
+type strategy
val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 84c0a99b..09a98bc8 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -26,6 +26,8 @@ let interp_alias key =
try KNmap.find key !alias_map
with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
+let check_alias key = KNmap.mem key !alias_map
+
(** ML tactic extensions (TacML) *)
type ml_tactic =
@@ -43,7 +45,7 @@ end
module MLTacMap = Map.Make(MLName)
let pr_tacname t =
- t.mltac_plugin ^ "::" ^ t.mltac_tactic
+ str t.mltac_plugin ++ str "::" ++ str t.mltac_tactic
let tac_tab = ref MLTacMap.empty
@@ -52,9 +54,9 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
if MLTacMap.mem s !tac_tab then
if overwrite then
let () = tac_tab := MLTacMap.remove s !tac_tab in
- msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
+ msg_warning (str "Overwriting definition of tactic " ++ pr_tacname s)
else
- Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
+ Errors.anomaly (str "Cannot redeclare tactic " ++ pr_tacname s ++ str ".")
in
tac_tab := MLTacMap.add s t !tac_tab
@@ -63,7 +65,7 @@ let interp_ml_tactic s =
MLTacMap.find s !tac_tab
with Not_found ->
Errors.errorlabstrm ""
- (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
+ (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
(***************************************************************************)
(* Tactic registration *)
@@ -73,34 +75,48 @@ let interp_ml_tactic s =
open Nametab
open Libobject
+type ltac_entry = {
+ tac_for_ml : bool;
+ tac_body : glob_tactic_expr;
+ tac_redef : ModPath.t list;
+}
+
let mactab =
- Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t)
+ Summary.ref (KNmap.empty : ltac_entry KNmap.t)
~name:"tactic-definition"
-let interp_ltac r = snd (KNmap.find r !mactab)
+let ltac_entries () = !mactab
+
+let interp_ltac r = (KNmap.find r !mactab).tac_body
+
+let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
-let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
+let add kn b t =
+ let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+ mactab := KNmap.add kn entry !mactab
-(* Declaration of the TAC-DEFINITION object *)
-let add (kn,td) = mactab := KNmap.add kn td !mactab
+let replace kn path t =
+ let (path, _, _) = KerName.repr path in
+ let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
+ mactab := KNmap.modify kn entry !mactab
let load_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->
let () = if not local then Nametab.push_tactic (Until i) sp kn in
- add (kn, (b,t))
-| Some kn -> add (kn, (b,t))
+ add kn b t
+| Some kn0 -> replace kn0 kn t
let open_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->
let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
- add (kn, (b,t))
-| Some kn -> add (kn, (b,t))
+ add kn b t
+| Some kn0 -> replace kn0 kn t
let cache_md ((sp, kn), (local, id ,b, t)) = match id with
| None ->
let () = Nametab.push_tactic (Until 1) sp kn in
- add (kn, (b,t))
-| Some kn -> add (kn, (b,t))
+ add kn b t
+| Some kn0 -> replace kn0 kn t
let subst_kind subst id = match id with
| None -> None
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 29677fd4..2df6bb04 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit
val interp_alias : alias -> glob_tactic_expr
(** Recover the the body of an alias. Raises an anomaly if it does not exist. *)
+val check_alias : alias -> bool
+(** Returns [true] if an alias is defined, false otherwise. *)
+
(** {5 Coq tactic definitions} *)
val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
@@ -41,6 +44,19 @@ val interp_ltac : KerName.t -> glob_tactic_expr
(** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *)
val is_ltac_for_ml_tactic : KerName.t -> bool
+(** Whether the tactic is defined from ML-side *)
+
+type ltac_entry = {
+ tac_for_ml : bool;
+ (** Whether the tactic is defined from ML-side *)
+ tac_body : glob_tactic_expr;
+ (** The current body of the tactic *)
+ tac_redef : ModPath.t list;
+ (** List of modules redefining the tactic in reverse chronological order *)
+}
+
+val ltac_entries : unit -> ltac_entry KNmap.t
+(** Low-level access to all Ltac entries currently defined. *)
(** {5 ML tactic extensions} *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 5cc4c835..fb22da83 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -341,7 +341,7 @@ let intern_typed_pattern ist p =
let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let interp_ref r =
- try l, Inl (intern_evaluable ist r)
+ try Inl (intern_evaluable ist r)
with e when Logic.catchable_exception e ->
(* Compatibility. In practice, this means that the code above
is useless. Still the idea of having either an evaluable
@@ -356,19 +356,19 @@ let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let c = Constrintern.interp_reference sign r in
match c with
| GRef (_,r,None) ->
- l, Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+ Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
| GVar (_,id) ->
let r = evaluable_of_global_reference ist.genv (VarRef id) in
- l, Inl (ArgArg (r,None))
+ Inl (ArgArg (r,None))
| _ ->
- l, Inr ((c,None),dummy_pat) in
- match p with
+ Inr ((c,None),dummy_pat) in
+ (l, match p with
| Inl r -> interp_ref r
| Inr (CAppExpl(_,(None,r,None),[])) ->
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
- l, Inr (intern_typed_pattern ist c)
+ Inr (intern_typed_pattern ist c))
(* This seems fairly hacky, but it's the first way I've found to get proper
globalization of [unfold]. --adamc *)
@@ -809,11 +809,24 @@ let pr_ltac_fun_arg = function
let print_ltac id =
try
let kn = Nametab.locate_tactic id in
- let l,t = split_ltac_fun (Tacenv.interp_ltac kn) in
+ let entries = Tacenv.ltac_entries () in
+ let tac = KNmap.find kn entries in
+ let filter mp =
+ try Some (Nametab.shortest_qualid_of_module mp)
+ with Not_found -> None
+ in
+ let mods = List.map_filter filter tac.Tacenv.tac_redef in
+ let redefined = match mods with
+ | [] -> mt ()
+ | mods ->
+ let redef = prlist_with_sep fnl pr_qualid mods in
+ fnl () ++ str "Redefined by:" ++ fnl () ++ redef
+ in
+ let l,t = split_ltac_fun tac.Tacenv.tac_body in
hv 2 (
hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
- ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t)
+ ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
with
Not_found ->
errorlabstrm "print_ltac"
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f29680e1..355745d9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,8 +44,8 @@ open Proofview.Notations
let safe_msgnl s =
Proofview.NonLogical.catch
- (Proofview.NonLogical.print (s++fnl()))
- (fun _ -> Proofview.NonLogical.print (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
+ (Proofview.NonLogical.print_debug (s++fnl()))
+ (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl()))
type value = tlevel generic_argument
@@ -557,7 +557,9 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
ltac_vars = constr_context;
ltac_bound = Id.Map.domain ist.lfun;
} in
- intern_gen kind ~allow_patvar ~ltacvars env c
+ let kind_for_intern =
+ match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
+ intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
in
let trace =
push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist in
@@ -678,7 +680,19 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
let p = match a with
- | Inl b -> Inl (interp_evaluable ist env sigma b)
+ | Inl (ArgVar (loc,id)) ->
+ (* This is the encoding of an ltac var supposed to be bound
+ prioritary to an evaluable reference and otherwise to a constr
+ (it is an encoding to satisfy the "union" type given to Simpl) *)
+ let coerce_eval_ref_or_constr x =
+ try Inl (coerce_to_evaluable_ref env x)
+ with CannotCoerceTo _ ->
+ let c = coerce_to_closed_constr env x in
+ Inr (pi3 (pattern_of_constr env sigma c)) in
+ (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
+ with Not_found ->
+ error_global_not_found_loc loc (qualid_of_ident id))
+ | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
interp_occurrences ist occs, p
@@ -734,7 +748,7 @@ let interp_may_eval f ist env sigma = function
str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
- Typing.e_type_of ~refresh:true env sigma c_interp
+ Typing.type_of ~refresh:true env sigma c_interp
| ConstrTerm c ->
try
f ist env sigma c
@@ -971,10 +985,10 @@ let interp_induction_arg ist gl arg =
let try_cast_id id' =
if Tactics.is_quantified_hypothesis id' gl
then keep,ElimOnIdent (loc,id')
- else
- (try keep,ElimOnConstr (fun env sigma -> sigma,(constr_of_id env id',NoBindings))
+ else keep, ElimOnConstr (fun env sigma ->
+ try sigma, (constr_of_id env id', NoBindings)
with Not_found ->
- user_err_loc (loc,"",
+ user_err_loc (loc, "interp_induction_arg",
pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
in
try
@@ -1026,11 +1040,12 @@ let interp_context ctxt = in_gen (topwit wit_constr_context) ctxt
(* Reads a pattern by substituting vars of lfun *)
let use_types = false
-let eval_pattern lfun ist env sigma (_,pat as c) =
+let eval_pattern lfun ist env sigma ((glob,_),pat as c) =
+ let bound_names = bound_glob_vars glob in
if use_types then
- pi3 (interp_typed_pattern ist env sigma c)
+ (bound_names,pi3 (interp_typed_pattern ist env sigma c))
else
- instantiate_pattern env sigma lfun pat
+ (bound_names,instantiate_pattern env sigma lfun pat)
let read_pattern lfun ist env sigma = function
| Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
@@ -1040,8 +1055,8 @@ let read_pattern lfun ist env sigma = function
let cons_and_check_name id l =
if Id.List.mem id l then
user_err_loc (dloc,"read_match_goal_hyps",
- strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^
- " used twice in the same pattern."))
+ str "Hypothesis pattern-matching variable " ++ pr_id id ++
+ str " used twice in the same pattern.")
else id::l
let rec read_match_goal_hyps lfun ist env sigma lidh = function
@@ -1123,7 +1138,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
interp_message ist s >>= fun msg ->
return (hov 0 msg , hov 0 msg)
in
- let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print msgnl)) in
+ let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in
let log (msg,_) = Proofview.Trace.log (fun () -> msg) in
let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in
Ftactic.run msgnl begin fun msgnl ->
@@ -1492,11 +1507,11 @@ and tactic_of_value ist vle =
extra = TacStore.set ist.extra f_trace []; } in
let tac = name_if_glob appl (eval_tactic ist t) in
catch_error_tac trace tac
- | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
+ | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
eval_tactic ist tac
- else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
+ else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist llc u =
@@ -1752,10 +1767,8 @@ and interp_ltac_constr ist e : constr Ftactic.t =
Ftactic.return cresult
with CannotCoerceTo _ ->
let env = Proofview.Goal.env gl in
- Proofview.tclZERO (UserError ( "",
- errorlabstrm ""
- (str "Must evaluate to a closed term" ++ fnl() ++
- str "offending expression: " ++ fnl() ++ pr_inspect env e result)))
+ Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
+ str "offending expression: " ++ fnl() ++ pr_inspect env e result)
end
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
index abeb47c3..d8e6dd0a 100644
--- a/tactics/tactic_matching.mli
+++ b/tactics/tactic_matching.mli
@@ -32,7 +32,7 @@ val match_term :
Environ.env ->
Evd.evar_map ->
Term.constr ->
- (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+ (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
(** [match_goal env sigma hyps concl rules] matches the goal
@@ -45,5 +45,5 @@ val match_goal:
Evd.evar_map ->
Context.named_context ->
Term.constr ->
- (Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
+ (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9b16fe3f..bc82e9ef 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -420,7 +420,7 @@ module New = struct
(* Try the first tactic that does not fail in a list of tactics *)
let rec tclFIRST = function
- | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic."))
+ | [] -> tclZEROMSG (str"No applicable tactic.")
| t::rest -> tclORELSE0 t (tclFIRST rest)
let rec tclFIRST_PROGRESS_ON tac = function
@@ -430,10 +430,7 @@ module New = struct
let rec tclDO n t =
if n < 0 then
- tclZERO (Errors.UserError (
- "Refiner.tclDO",
- str"Wrong argument : Do needs a positive integer.")
- )
+ tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
else if n = 0 then tclUNIT ()
else if n = 1 then t
else tclTHEN t (tclDO (n-1) t)
@@ -456,7 +453,7 @@ module New = struct
let tclCOMPLETE t =
t >>= fun res ->
(tclINDEPENDENT
- (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
+ (tclZEROMSG (str"Proof is not complete."))
) <*>
tclUNIT res
@@ -596,12 +593,14 @@ module New = struct
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
isrec allnames tac predicate ind (c, t) =
- Proofview.Goal.nf_enter begin fun gl ->
- let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
- (** FIXME: evar leak. *)
+ Proofview.Goal.nf_enter
+ begin fun gl ->
let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Proofview.Goal.nf_enter begin fun gl ->
+ let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
(* applying elimination_scheme just a little modified *)
- let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in
+ let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in
let indmv =
match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
| Meta mv -> mv
@@ -618,7 +617,8 @@ module New = struct
| Var id -> string_of_id id
| _ -> "\b"
in
- error ("The elimination combinator " ^ name_elim ^ " is unknown.")
+ errorlabstrm "Tacticals.general_elim_then_using"
+ (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain indmv elimclause indclause in
let branchsigns = compute_construtor_signatures isrec ind in
@@ -649,11 +649,11 @@ module New = struct
Proofview.tclTHEN
(Clenvtac.clenv_refine false clenv')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
- end
+ end) end
let elimination_then tac c =
Proofview.Goal.nf_enter begin fun gl ->
- let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
| None -> true,gl_make_elim
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7484139c..2a46efd8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -109,6 +109,44 @@ let _ =
optread = (fun () -> !clear_hyp_by_default) ;
optwrite = (fun b -> clear_hyp_by_default := b) }
+(* Compatibility option useful in developments using apply intensively
+ in ltac code *)
+
+let universal_lemma_under_conjunctions = ref false
+
+let accept_universal_lemma_under_conjunctions () =
+ !universal_lemma_under_conjunctions
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "trivial unification in tactics applying under conjunctions";
+ optkey = ["Universal";"Lemma";"Under";"Conjunction"];
+ optread = (fun () -> !universal_lemma_under_conjunctions) ;
+ optwrite = (fun b -> universal_lemma_under_conjunctions := b) }
+
+(* The following boolean governs what "intros []" do on examples such
+ as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
+ if false, it behaves as "intro H; case H; clear H" for fresh H.
+ Kept as false for compatibility.
+ *)
+
+let bracketing_last_or_and_intro_pattern = ref false
+
+let use_bracketing_last_or_and_intro_pattern () =
+ !bracketing_last_or_and_intro_pattern
+ && Flags.version_strictly_greater Flags.V8_4
+
+let _ =
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "bracketing last or-and introduction pattern";
+ optkey = ["Bracketing";"Last";"Introduction";"Pattern"];
+ optread = (fun () -> !bracketing_last_or_and_intro_pattern) ;
+ optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) }
+
(*********************************************)
(* Tactics *)
(*********************************************)
@@ -139,7 +177,8 @@ let introduction ?(check=true) id =
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
let () = if check && mem_named_context id hyps then
- error ("Variable " ^ Id.to_string id ^ " is already declared.")
+ errorlabstrm "Tactics.introduction"
+ (str "Variable " ++ pr_id id ++ str " is already declared.")
in
match kind_of_term (whd_evar sigma concl) with
| Prod (_, t, b) -> unsafe_intro env store (id, None, t) b
@@ -157,7 +196,7 @@ let convert_concl ?(check=true) ty k =
Proofview.Refine.refine ~unsafe:true begin fun sigma ->
let sigma =
if check then begin
- ignore (Typing.type_of env sigma ty);
+ ignore (Typing.unsafe_type_of env sigma ty);
let sigma,b = Reductionops.infer_conv env sigma ty conclty in
if not b then error "Not convertible.";
sigma
@@ -184,8 +223,9 @@ let convert_hyp_no_check = convert_hyp ~check:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
try
- let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
- Proofview.Unsafe.tclEVARS sigma
+ let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
+ if b then Proofview.Unsafe.tclEVARS sigma
+ else Tacticals.New.tclFAIL 0 (str "Not convertible")
with (* Reduction.NotConvertible *) _ ->
(** FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
@@ -627,7 +667,7 @@ let change_on_subterm cv_pb deep t where env sigma c =
env sigma c in
if !mayneedglobalcheck then
begin
- try ignore (Typing.type_of env sigma c)
+ try ignore (Typing.unsafe_type_of env sigma c)
with e when catchable_exception e ->
error "Replacement would lead to an ill-typed term."
end;
@@ -687,12 +727,11 @@ let reduction_clause redexp cl =
let reduce redexp cl goal =
let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
let redexps = reduction_clause redexp cl in
+ let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
let tac = tclMAP (fun (where,redexp) ->
- e_reduct_option ~check:true
+ e_reduct_option ~check
(Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
- match redexp with
- | Fold _ | Pattern _ -> with_check tac goal
- | _ -> tac goal
+ if check then with_check tac goal else tac goal
(* Unfolding occurrences of a constant *)
@@ -751,8 +790,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
(intro_then_gen name_flag move_flag false dep_flag tac))
begin function (e, info) -> match e with
| RefinerError IntroNeedsProduct ->
- Proofview.tclZERO
- (Errors.UserError("Intro",str "No product even after head-reduction."))
+ Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
| e -> Proofview.tclZERO ~info e
end
end
@@ -800,16 +838,23 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
aux n []
let get_next_hyp_position id gl =
- let rec get_next_hyp_position id = function
+ let rec aux = function
| [] -> raise (RefinerError (NoSuchHyp id))
| (hyp,_,_) :: right ->
if Id.equal hyp id then
match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
else
- get_next_hyp_position id right
+ aux right
+ in
+ aux (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+
+let get_previous_hyp_position id gl =
+ let rec aux dest = function
+ | [] -> raise (RefinerError (NoSuchHyp id))
+ | (hyp,_,_) :: right ->
+ if Id.equal hyp id then dest else aux (MoveAfter hyp) right
in
- let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
- get_next_hyp_position id hyps
+ aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
let intro_replacing id =
Proofview.Goal.enter begin fun gl ->
@@ -979,7 +1024,7 @@ let cut c =
let is_sort =
try
(** Backward compat: ensure that [c] is well-typed. *)
- let typ = Typing.type_of env sigma c in
+ let typ = Typing.unsafe_type_of env sigma c in
let typ = whd_betadeltaiota env sigma typ in
match kind_of_term typ with
| Sort _ -> true
@@ -1224,7 +1269,7 @@ let find_ind_eliminator ind s gl =
evd, c
let find_eliminator c gl =
- let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in
+ let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in
if is_nonrec ind then raise IsNonrec;
let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
evd, {elimindex = None; elimbody = (c,NoBindings);
@@ -1332,7 +1377,7 @@ let make_projection env sigma params cstr sign elim i n c u =
(* to avoid surprising unifications, excludes flexible
projection types or lambda which will be instantiated by Meta/Evar *)
&& not (isEvar (fst (whd_betaiota_stack sigma t)))
- && not (isRel t && destRel t > n-i)
+ && (accept_universal_lemma_under_conjunctions () || not (isRel t))
then
let t = lift (i+1-n) t in
let abselim = beta_applist (elim,params@[t;branch]) in
@@ -1358,7 +1403,7 @@ let make_projection env sigma params cstr sign elim i n c u =
| None -> None
in elim
-let descend_in_conjunctions avoid tac exit c =
+let descend_in_conjunctions avoid tac (err, info) c =
Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
@@ -1392,9 +1437,8 @@ let descend_in_conjunctions avoid tac exit c =
(* Might be ill-typed due to forbidden elimination. *)
Tacticals.New.onLastHypId (tac (not isrec))]
end))
- | None ->
- raise Exit
- with RefinerError _|UserError _|Exit -> exit ()
+ | None -> Proofview.tclZERO ~info err
+ with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
end
(****************************************************)
@@ -1417,7 +1461,15 @@ let solve_remaining_apply_goals =
with Not_found -> Proofview.tclUNIT ()
else Proofview.tclUNIT ()
end
-
+
+let tclORELSEOPT t k =
+ Proofview.tclORELSE t
+ (fun e -> match k e with
+ | None ->
+ let (e, info) = e in
+ Proofview.tclZERO ~info e
+ | Some tac -> tac)
+
let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
@@ -1442,50 +1494,46 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
with UserError _ as exn ->
Proofview.tclZERO exn
in
- Proofview.tclORELSE
+ let rec try_red_apply thm_ty (exn0, info) =
+ try
+ (* Try to head-reduce the conclusion of the theorem *)
+ let red_thm = try_red_product env sigma thm_ty in
+ tclORELSEOPT
+ (try_apply red_thm concl_nprod)
+ (function (e, info) -> match e with
+ | PretypeError _|RefinerError _|UserError _|Failure _ ->
+ Some (try_red_apply red_thm (exn0, info))
+ | _ -> None)
+ with Redelimination ->
+ (* Last chance: if the head is a variable, apply may try
+ second order unification *)
+ let info = Loc.add_loc info loc in
+ let tac =
+ if with_destruct then
+ descend_in_conjunctions []
+ (fun b id ->
+ Tacticals.New.tclTHEN
+ (try_main_apply b (mkVar id))
+ (Proofview.V82.tactic (thin [id])))
+ (exn0, info) c
+ else
+ Proofview.tclZERO ~info exn0 in
+ if not (Int.equal concl_nprod 0) then
+ tclORELSEOPT
+ (try_apply thm_ty 0)
+ (function (e, info) -> match e with
+ | PretypeError _|RefinerError _|UserError _|Failure _->
+ Some tac
+ | _ -> None)
+ else
+ tac
+ in
+ tclORELSEOPT
(try_apply thm_ty0 concl_nprod)
(function (e, info) -> match e with
- | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
- let rec try_red_apply thm_ty =
- try
- (* Try to head-reduce the conclusion of the theorem *)
- let red_thm = try_red_product env sigma thm_ty in
- Proofview.tclORELSE
- (try_apply red_thm concl_nprod)
- (function (e, info) -> match e with
- | PretypeError _|RefinerError _|UserError _|Failure _ ->
- try_red_apply red_thm
- | exn -> iraise (exn, info))
- with Redelimination ->
- (* Last chance: if the head is a variable, apply may try
- second order unification *)
- let tac =
- if with_destruct then
- descend_in_conjunctions []
- (fun b id ->
- Tacticals.New.tclTHEN
- (try_main_apply b (mkVar id))
- (Proofview.V82.tactic (thin [id])))
- (fun _ ->
- let info = Loc.add_loc info loc in
- Proofview.tclZERO ~info exn0) c
- else
- let info = Loc.add_loc info loc in
- Proofview.tclZERO ~info exn0 in
- if not (Int.equal concl_nprod 0) then
- try
- Proofview.tclORELSE
- (try_apply thm_ty 0)
- (function (e, info) -> match e with
- | PretypeError _|RefinerError _|UserError _|Failure _->
- tac
- | exn -> iraise (exn, info))
- with UserError _ | Exit ->
- tac
- else
- tac
- in try_red_apply thm_ty0
- | exn -> iraise (exn, info))
+ | PretypeError _|RefinerError _|UserError _|Failure _ ->
+ Some (try_red_apply thm_ty0 (e, info))
+ | _ -> None)
end
in
Tacticals.New.tclTHENLIST [
@@ -1596,10 +1644,10 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
tac id
])
with e when with_destruct && Errors.noncritical e ->
- let e = Errors.push e in
+ let (e, info) = Errors.push e in
(descend_in_conjunctions [targetid]
(fun b id -> aux (id::idstoclear) b (mkVar id))
- (fun _ -> iraise e) c)
+ (e, info) c)
end
in
aux [] with_destruct d
@@ -1636,7 +1684,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
let cut_and_apply c =
Proofview.Goal.nf_enter begin fun gl ->
- match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with
+ match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with
| Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
let concl = Proofview.Goal.concl gl in
let env = Tacmach.New.pf_env gl in
@@ -1669,7 +1717,7 @@ let exact_check c =
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let sigma, ct = Typing.e_type_of env sigma c in
+ let sigma, ct = Typing.type_of env sigma c in
Proofview.Unsafe.tclEVARS sigma <*>
Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c)
end
@@ -1818,7 +1866,7 @@ let specialize (c,lbind) g =
let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
tclEVARS evd, nf_evar evd c
else
- let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in
+ let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in
let flags = { (default_unify_flags ()) with resolve_evars = true } in
let clause = clenv_unify_meta_types ~flags clause in
let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
@@ -1838,11 +1886,11 @@ let specialize (c,lbind) g =
| Var id when Id.List.mem id (pf_ids_of_hyps g) ->
tclTHEN tac
(tclTHENFIRST
- (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g)
+ (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g)
(exact_no_check term)) g
| _ -> tclTHEN tac
(tclTHENLAST
- (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g)
+ (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g)
(exact_no_check term)) g
(* Keeping only a few hypotheses *)
@@ -1871,8 +1919,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
if Int.equal i 0 then error "The constructors are numbered starting from 1.";
begin match expctdnumopt with
| Some n when not (Int.equal n nconstr) ->
- error ("Not an inductive goal with "^
- string_of_int n ^ String.plural n " constructor"^".")
+ errorlabstrm "Tactics.check_number_of_constructors"
+ (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
| _ -> ()
end;
if i > nconstr then error "Not enough constructors."
@@ -1977,7 +2025,7 @@ let my_find_eq_data_decompose gl t =
let intro_decomp_eq loc l thin tac id =
Proofview.Goal.nf_enter begin fun gl ->
let c = mkVar id in
- let t = Tacmach.New.pf_type_of gl c in
+ let t = Tacmach.New.pf_unsafe_type_of gl c in
let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
match my_find_eq_data_decompose gl t with
| Some (eq,u,eq_args) ->
@@ -1991,7 +2039,7 @@ let intro_decomp_eq loc l thin tac id =
let intro_or_and_pattern loc bracketed ll thin tac id =
Proofview.Goal.enter begin fun gl ->
let c = mkVar id in
- let t = Tacmach.New.pf_type_of gl c in
+ let t = Tacmach.New.pf_unsafe_type_of gl c in
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
let nv = constructors_nrealargs ind in
let ll = fix_empty_or_and_pattern (Array.length nv) ll in
@@ -2010,7 +2058,7 @@ let rewrite_hyp assert_style l2r id =
let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let type_of = Tacmach.New.pf_type_of gl in
+ let type_of = Tacmach.New.pf_unsafe_type_of gl in
let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
let t = whd_betadeltaiota (type_of (mkVar id)) in
match match_with_equality_type t with
@@ -2074,7 +2122,7 @@ let make_tmp_naming avoid l = function
case of IntroFresh, we should use check_thin_clash_then anyway to
prevent the case of an IntroFresh precisely using the wild_id *)
| IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
- | _ -> NamingAvoid(avoid@explicit_intro_names l)
+ | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l))
let fit_bound n = function
| None -> true
@@ -2088,6 +2136,21 @@ let exceed_bound n = function
to ensure that dependent hypotheses are cleared in the right
dependency order (see bug #1000); we use fresh names, not used in
the tactic, for the hyps to clear *)
+ (* In [intro_patterns_core b avoid ids thin destopt bound n tac patl]:
+ [b]: compatibility flag, if false at toplevel, do not complete incomplete
+ trailing toplevel or_and patterns (as in "intros []", see
+ [bracketing_last_or_and_intro_pattern])
+ [avoid]: names to avoid when creating an internal name
+ [ids]: collect introduced names for possible use by the [tac] continuation
+ [thin]: collect names to erase at the end
+ [destopt]: position in the context where to introduce the hypotheses
+ [bound]: number of pending intros to do in the current or-and pattern,
+ with remembering of [b] flag if at toplevel
+ [n]: number of introduction done in the current or-and pattern
+ [tac]: continuation tactic
+ [patl]: introduction patterns to interpret
+ *)
+
let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
| [] when fit_bound n bound ->
tac ids thin
@@ -2105,31 +2168,33 @@ let rec intro_patterns_core b avoid ids thin destopt bound n tac = function
(n+List.length ids) tac l)
| IntroAction pat ->
intro_then_gen (make_tmp_naming avoid l pat)
- MoveLast true false
+ destopt true false
(intro_pattern_action loc (b || not (List.is_empty l)) false pat thin
+ destopt
(fun thin bound' -> intro_patterns_core b avoid ids thin destopt bound' 0
(fun ids thin ->
intro_patterns_core b avoid ids thin destopt bound (n+1) tac l)))
| IntroNaming pat ->
- intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l
+ intro_pattern_naming loc b avoid ids pat thin destopt bound (n+1) tac l
+ (* Pi-introduction rule, used backwards *)
and intro_pattern_naming loc b avoid ids pat thin destopt bound n tac l =
match pat with
| IntroIdentifier id ->
check_thin_clash_then id thin avoid (fun thin ->
intro_then_gen (NamingMustBe (loc,id)) destopt true false
- (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l))
+ (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l))
| IntroAnonymous ->
intro_then_gen (NamingAvoid (avoid@explicit_intro_names l))
destopt true false
- (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+ (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
| IntroFresh id ->
(* todo: avoid thinned names to interfere with generation of fresh name *)
intro_then_gen (NamingBasedOn (id, avoid@explicit_intro_names l))
destopt true false
- (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound (n+1) tac l)
+ (fun id -> intro_patterns_core b avoid (id::ids) thin destopt bound n tac l)
-and intro_pattern_action loc b style pat thin tac id = match pat with
+and intro_pattern_action loc b style pat thin destopt tac id = match pat with
| IntroWildcard ->
tac ((loc,id)::thin) None []
| IntroOrAndPattern ll ->
@@ -2142,7 +2207,13 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
(rewrite_hyp style l2r id)
(tac thin None [])
| IntroApplyOn (f,(loc,pat)) ->
- let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
+ let naming,tac_ipat =
+ prepare_intros_loc loc (IntroIdentifier id) destopt pat in
+ let doclear =
+ if naming = NamingMustBe (loc,id) then
+ Proofview.tclUNIT () (* apply_in_once do a replacement *)
+ else
+ Proofview.V82.tactic (clear [id]) in
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
@@ -2151,36 +2222,31 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
(Tacticals.New.tclTHENFIRST
(* Skip the side conditions of the apply *)
(apply_in_once false true true true naming id
- (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
+ (None,(sigma,(c,NoBindings)))
+ (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
+ (tac thin None []))
sigma
end
-and prepare_intros_loc loc dft = function
+and prepare_intros_loc loc dft destopt = function
| IntroNaming ipat ->
prepare_naming loc ipat,
- (fun _ -> Proofview.tclUNIT ())
+ (fun id -> Proofview.V82.tactic (move_hyp id destopt))
| IntroAction ipat ->
prepare_naming loc dft,
(let tac thin bound =
- intro_patterns_core true [] [] thin MoveLast bound 0
+ intro_patterns_core true [] [] thin destopt bound 0
(fun _ l -> clear_wildcards l) in
- fun id -> intro_pattern_action loc true true ipat [] tac id)
+ fun id -> intro_pattern_action loc true true ipat [] destopt tac id)
| IntroForthcoming _ -> user_err_loc
(loc,"",str "Introduction pattern for one hypothesis expected.")
let intro_patterns_bound_to n destopt =
intro_patterns_core true [] [] [] destopt
- (Some (true,n)) 0 (fun _ -> clear_wildcards)
-
-(* The following boolean governs what "intros []" do on examples such
- as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]";
- if false, it behaves as "intro H; case H; clear H" for fresh H.
- Kept as false for compatibility.
- *)
-let bracketing_last_or_and_intro_pattern = false
+ (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
let intro_patterns_to destopt =
- intro_patterns_core bracketing_last_or_and_intro_pattern
+ intro_patterns_core (use_bracketing_last_or_and_intro_pattern ())
[] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
let intro_pattern_to destopt pat =
@@ -2197,23 +2263,24 @@ let intros_patterns = function
(* Forward reasoning *)
(**************************)
-let prepare_intros dft = function
+let prepare_intros dft destopt = function
| None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
- | Some (loc,ipat) -> prepare_intros_loc loc dft ipat
+ | Some (loc,ipat) -> prepare_intros_loc loc dft destopt ipat
let ipat_of_name = function
| Anonymous -> None
| Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
- let head_ident c =
+let head_ident c =
let c = fst (decompose_app ((strip_lam_assum c))) in
if isVar c then Some (destVar c) else None
-let assert_as first ipat c =
- let naming,tac = prepare_intros IntroAnonymous ipat in
- let repl = do_replace (head_ident c) naming in
- if first then assert_before_then_gen repl naming c tac
- else assert_after_then_gen repl naming c tac
+let assert_as first hd ipat t =
+ let naming,tac = prepare_intros IntroAnonymous MoveLast ipat in
+ let repl = do_replace hd naming in
+ let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
+ if first then assert_before_then_gen repl naming t tac
+ else assert_after_then_gen repl naming t tac
(* apply in as *)
@@ -2222,13 +2289,18 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
let tac (naming,lemma) tac id =
apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
naming id lemma tac in
- let naming,ipat_tac = prepare_intros (IntroIdentifier id) ipat in
+ Proofview.Goal.enter begin fun gl ->
+ let destopt =
+ if with_evars then MoveLast (* evars would depend on the whole context *)
+ else get_previous_hyp_position id gl in
+ let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
let lemmas_target, last_lemma_target =
let last,first = List.sep_last lemmas in
List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
in
(* We chain apply_in_once, ending with an intro pattern *)
List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
+ end
(*
if sidecond_first then
@@ -2287,7 +2359,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
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
- let sigma, _ = Typing.e_type_of env sigma term in
+ let sigma, _ = Typing.type_of env sigma term in
sigma, term,
Tacticals.New.tclTHEN
(intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false)
@@ -2373,16 +2445,17 @@ let forward b usetac ipat c =
match usetac with
| None ->
Proofview.Goal.enter begin fun gl ->
- let t = Tacmach.New.pf_type_of gl c in
- Tacticals.New.tclTHENFIRST (assert_as true ipat t)
+ let t = Tacmach.New.pf_unsafe_type_of gl c in
+ let hd = head_ident c in
+ Tacticals.New.tclTHENFIRST (assert_as true hd ipat t)
(Proofview.V82.tactic (exact_no_check c))
end
| Some tac ->
if b then
- Tacticals.New.tclTHENFIRST (assert_as b ipat c) tac
+ Tacticals.New.tclTHENFIRST (assert_as b None ipat c) tac
else
Tacticals.New.tclTHENS3PARTS
- (assert_as b ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
+ (assert_as b None ipat c) [||] tac [|Tacticals.New.tclIDTAC|]
let pose_proof na c = forward true None (ipat_of_name na) c
let assert_by na t tac = forward true (Some tac) (ipat_of_name na) t
@@ -2408,11 +2481,13 @@ let bring_hyps hyps =
else
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
+ let store = Proofview.Goal.extra gl in
let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
let args = Array.of_list (instance_from_named_context hyps) in
Proofview.Refine.refine begin fun sigma ->
- let (sigma, ev) = Evarutil.new_evar env sigma newcl in
+ let (sigma, ev) =
+ Evarutil.new_evar env sigma ~principal:true ~store newcl in
(sigma, (mkApp (ev, args)))
end
end
@@ -2456,7 +2531,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) =
mkProd_or_LetIn (na,b,t) cl', evd'
let generalize_goal gl i ((occs,c,b),na as o) cl =
- let t = pf_type_of gl c in
+ let t = pf_unsafe_type_of gl c in
let env = pf_env gl in
generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl
@@ -2517,7 +2592,7 @@ let new_generalize_gen_let lconstr =
let (newcl, sigma), args =
List.fold_right_i
(fun i ((_,c,b),_ as o) (cl, args) ->
- let t = Tacmach.New.pf_type_of gl c in
+ let t = Tacmach.New.pf_unsafe_type_of gl c in
let args = if Option.is_empty b then c :: args else args in
generalize_goal_gen env ids i o t cl, args)
0 lconstr ((concl, sigma), [])
@@ -2794,7 +2869,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
let id = match kind_of_term c with
| Var id -> id
| _ ->
- let type_of = Tacmach.New.pf_type_of gl in
+ let type_of = Tacmach.New.pf_unsafe_type_of gl in
id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
let x = fresh_id_in_env avoid id env in
Tacticals.New.tclTHEN
@@ -3043,7 +3118,7 @@ let make_up_names n ind_opt cname =
let error_ind_scheme s =
let s = if not (String.is_empty s) then s^" " else s in
- error ("Cannot recognize "^s^"an induction scheme.")
+ errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
let glob = Universes.constr_of_global
@@ -3178,7 +3253,7 @@ let is_defined_variable env id = match lookup_named id env with
| (_, Some _, _) -> true
let abstract_args gl generalize_vars dep id defined f args =
- let sigma = project gl in
+ let sigma = ref (project gl) in
let env = pf_env gl in
let concl = pf_concl gl in
let dep = dep || dependent (mkVar id) concl in
@@ -3195,11 +3270,12 @@ let abstract_args gl generalize_vars dep id defined f args =
*)
let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg =
let (name, _, ty), arity =
- let rel, c = Reductionops.splay_prod_n env sigma 1 prod in
+ let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in
List.hd rel, c
in
- let argty = pf_type_of gl arg in
- let ty = (* refresh_universes_strict *) ty in
+ let argty = pf_unsafe_type_of gl arg in
+ let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in
+ let () = sigma := sigma' in
let lenctx = List.length ctx in
let liftargty = lift lenctx argty in
let leq = constr_cmp Reduction.CUMUL liftargty ty in
@@ -3238,8 +3314,9 @@ let abstract_args gl generalize_vars dep id defined f args =
true, mkApp (f', before), after
in
if dogen then
+ let tyf' = pf_unsafe_type_of gl f' in
let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
- Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
+ Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
in
let args, refls = List.rev args, List.rev refls in
let vars =
@@ -3248,9 +3325,12 @@ let abstract_args gl generalize_vars dep id defined f args =
hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
else []
in
- let body, c' = if defined then Some c', typ_of ctxenv Evd.empty c' else None, c' in
- Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls,
- dep, succ (List.length ctx), vars)
+ let body, c' =
+ if defined then Some c', typ_of ctxenv !sigma c'
+ else None, c'
+ in
+ let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in
+ Some (term, !sigma, dep, succ (List.length ctx), vars)
else None
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
@@ -3272,20 +3352,26 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in
match newc with
| None -> Proofview.tclUNIT ()
- | Some (newc, dep, n, vars) ->
+ | Some (newc, sigma, dep, n, vars) ->
let tac =
if dep then
- Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
- Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
- else
- Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro]
+ Tacticals.New.tclTHENLIST
+ [Proofview.Unsafe.tclEVARS sigma;
+ Proofview.V82.tactic (refine newc);
+ rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro;
+ Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))]
+ else Tacticals.New.tclTHENLIST
+ [Proofview.Unsafe.tclEVARS sigma;
+ Proofview.V82.tactic (refine newc);
+ Proofview.V82.tactic (clear [id]);
+ Tacticals.New.tclDO n intro]
in
if List.is_empty vars then tac
else Tacticals.New.tclTHEN tac
(Tacticals.New.tclFIRST
[revert vars ;
Proofview.V82.tactic (fun gl -> tclMAP (fun id ->
- tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
+ tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)])
end
let rec compare_upto_variables x y =
@@ -3563,13 +3649,13 @@ let guess_elim isrec dep s hyp0 gl =
Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s
else
Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in
- let elimt = Tacmach.New.pf_type_of gl elimc in
+ let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in
evd, ((elimc, NoBindings), elimt), mkIndU mind
let given_elim hyp0 (elimc,lbind as e) gl =
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
- Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess
+ Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
type scheme_signature =
(Id.t list * (elim_arg_kind * bool * Id.t) list) array
@@ -3594,14 +3680,17 @@ let find_induction_type isrec elim hyp0 gl =
if Option.is_empty scheme.indarg then error "Cannot find induction type";
let indsign = compute_scheme_signature scheme hyp0 ind_guess in
let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
- scheme, ElimUsing (elim,indsign) in
- (Option.get scheme.indref,scheme.nparams, elim)
+ scheme, ElimUsing (elim,indsign)
+ in
+ match scheme.indref with
+ | None -> error_ind_scheme ""
+ | Some ref -> ref, scheme.nparams, elim
let get_elim_signature elim hyp0 gl =
compute_elim_signature (given_elim hyp0 elim gl) hyp0
let is_functional_induction elimc gl =
- let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in
+ let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in
(* The test is not safe: with non-functional induction on non-standard
induction scheme, this may fail *)
Option.is_empty scheme.indarg
@@ -3960,7 +4049,7 @@ let induction_gen_l isrec with_evars elim names lc =
| _ ->
Proofview.Goal.enter begin fun gl ->
- let type_of = Tacmach.New.pf_type_of gl in
+ let type_of = Tacmach.New.pf_unsafe_type_of gl in
let x =
id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
@@ -4222,7 +4311,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
let symmetry_in id =
Proofview.Goal.enter begin fun gl ->
- let ctype = Tacmach.New.pf_type_of gl (mkVar id) in
+ let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in
let sign,t = decompose_prod_assum ctype in
Proofview.tclORELSE
begin
@@ -4273,7 +4362,7 @@ let prove_transitivity hdcncl eq_kind t =
| HeterogenousEq (typ1,c1,typ2,c2) ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let type_of = Typing.type_of env sigma in
+ let type_of = Typing.unsafe_type_of env sigma in
let typt = type_of t in
(mkApp(hdcncl, [| typ1; c1; typt ;t |]),
mkApp(hdcncl, [| typt; t; typ2; c2 |]))
@@ -4374,13 +4463,13 @@ let abstract_subproof id gk tac =
let cd = Entries.DefinitionEntry const in
let decl = (cd, IsProof Lemma) in
(** ppedrot: seems legit to have abstracted subproofs as local*)
- let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
+ let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in
(* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
let evd = Evd.set_universe_context evd ectx in
- let open Declareops in
- let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
- let effs = cons_side_effects eff
+ let open Safe_typing in
+ let eff = private_con_of_con (Global.safe_env ()) cst in
+ let effs = add_private eff
Entries.(snd (Future.force const.const_entry_body)) in
let args = List.rev (instance_from_named_context sign) in
let solve =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 0069d100..ade89fc9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -348,6 +348,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic
val assert_after : Name.t -> types -> unit Proofview.tactic
val assert_as : (* true = before *) bool ->
+ (* optionally tell if a specialization of some hyp: *) identifier option ->
intro_pattern option -> constr -> unit Proofview.tactic
(** Implements the tactics assert, enough and pose proof; note that "by"
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4b03ff24..b4c7bffa 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -316,7 +316,7 @@ let tauto_intuitionistic flags =
(intuition_gen (default_ist ()) flags <:tactic<fail>>)
begin function (e, info) -> match e with
| Refiner.FailError _ | UserError _ ->
- Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
+ Tacticals.New.tclZEROMSG (str "tauto failed.")
| e -> Proofview.tclZERO ~info e
end
@@ -328,7 +328,7 @@ let tauto_classical flags nnpp =
Proofview.tclORELSE
(Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
begin function (e, info) -> match e with
- | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
+ | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.")
| e -> Proofview.tclZERO ~info e
end
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e79fc6dc..65239a5f 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -98,8 +98,8 @@ struct
| DSort, DSort -> 0
| DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
| DCtx (tl1, tr1), DCtx (tl2, tr2)
- | DLambda (tl1, tr1), DCtx (tl2, tr2)
- | DApp (tl1, tr1), DCtx (tl2, tr2) ->
+ | DLambda (tl1, tr1), DLambda (tl2, tr2)
+ | DApp (tl1, tr1), DApp (tl2, tr2) ->
let c = cmp tl1 tl2 in
if c = 0 then cmp tr1 tr2 else c
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 04:44:37 +0000