aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/class_tactics.ml472
-rw-r--r--tactics/rewrite.ml47
-rw-r--r--theories/Classes/RelationClasses.v8
-rw-r--r--toplevel/classes.ml23
4 files changed, 70 insertions, 40 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a5adb9169..a45d9a3b2 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -46,8 +46,6 @@ let typeclasses_db = "typeclass_instances"
let _ = Auto.auto_init := (fun () ->
Auto.create_hint_db false typeclasses_db full_transparent_state true)
-let run_on_evars_forward = ref (fun _ _ _ _ -> assert false)
-
exception Found of evar_map
let is_dependent ev evm =
@@ -109,11 +107,23 @@ let auto_unif_flags = {
use_evars_pattern_unification = true;
}
-let tac_on_evars p tac gl =
- let db = searchtable_map typeclasses_db in
- match !run_on_evars_forward [db] (Hint_db.transparent_state db) p (project gl) with
- | None -> tclIDTAC gl
- | Some evm' -> Refiner.tclEVARS evm' gl
+let rec eq_constr_mod_evars x y =
+ match kind_of_term x, kind_of_term y with
+ | Evar (e1, l1), Evar (e2, l2) when e1 <> e2 -> true
+ | _, _ -> compare_constr eq_constr_mod_evars x y
+
+let progress_evars t gl =
+ let concl = pf_concl gl in
+ let check gl' =
+ let newconcl = pf_concl gl' in
+ if eq_constr_mod_evars concl newconcl
+ then tclFAIL 0 (str"No progress made (modulo evars)") gl'
+ else tclIDTAC gl'
+ in tclTHEN t check gl
+
+TACTIC EXTEND progress_evars
+ [ "progress_evars" tactic(t) ] -> [ progress_evars (snd t) ]
+END
let unify_e_resolve flags (c,clenv) gls =
let clenv' = connect_clenv gls clenv in
@@ -329,8 +339,11 @@ let then_tac (first : atac) (second : atac) : atac =
let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
t.skft (fun x _ -> Some x) (fun _ -> None) gl
-let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : auto_result option =
- (then_list t (fun x _ -> Some x))
+
+type run_list_res = (auto_result * run_list_res fk) option
+
+let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
+ (then_list t (fun x fk -> Some (x, fk)))
(gl, fun s pfs -> valid goals p (ref s) pfs)
(fun _ -> None)
@@ -375,22 +388,24 @@ let make_autogoals ?(st=full_transparent_state) gs evm' =
let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
(gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
+let get_result r =
+ match r with
+ | None -> None
+ | Some ((gls, v), fk) ->
+ try ignore(v (sig_sig gls) []); assert(false)
+ with Found evm' -> Some (evm', fk)
+
let run_on_evars ?(st=full_transparent_state) p evm tac =
match evars_to_goals p evm with
- | None -> None
+ | None -> None (* This happens only because there's no evar having p *)
| Some (goals, evm') ->
- match run_list_tac tac p goals (make_autogoals ~st goals evm') with
- | None -> raise Not_found
- | Some (gls, v) ->
- try ignore(v (sig_sig gls) []); assert(false)
- with Found evm' ->
- Some (Evd.evars_reset_evd evm' evm)
-
+ let res = run_list_tac tac p goals (make_autogoals ~st goals evm') in
+ match get_result res with
+ | None -> raise Not_found
+ | Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints))
-let () = run_on_evars_forward := (fun hints st p evd -> run_on_evars ~st p evd (eauto_tac hints))
-
let eauto hints g =
let gl = { it = make_autogoal ~st:(Hint_db.transparent_state (List.hd hints)) g; sigma = project g } in
match run_tac (eauto_tac hints) gl with
@@ -399,11 +414,20 @@ let eauto hints g =
{it = List.map fst goals; sigma = s}, valid s
let real_eauto st hints p evd =
- let rec aux evd =
- match run_on_evars ~st p evd (eauto_tac hints) with
- | None -> evd
- | Some evd' -> aux evd'
- in aux evd
+ let rec aux evd fails =
+ let res, fails =
+ try run_on_evars ~st p evd (eauto_tac hints), fails
+ with Not_found ->
+ List.fold_right (fun fk (res, fails) ->
+ match res with
+ | Some r -> res, fk :: fails
+ | None -> get_result (fk ()), fails)
+ fails (None, [])
+ in
+ match res with
+ | None -> evd
+ | Some (evd', fk) -> aux evd' (fk :: fails)
+ in aux evd []
let resolve_all_evars_once debug (mode, depth) p evd =
let db = searchtable_map typeclasses_db in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1c48988c7..0884b3462 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -460,7 +460,8 @@ let resolve_subrelation env sigma car rel rel' res =
let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
let evars, morph_instance, proj, sigargs, m', args, args' =
- let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in
+ let first = try (array_find args' (fun i b -> b <> None))
+ with Not_found -> raise (Invalid_argument "resolve_morphism") in
let morphargs, morphobjs = array_chop first args in
let morphargs', morphobjs' = array_chop first args' in
let appm = mkApp(m, morphargs) in
@@ -741,10 +742,10 @@ module Strategies =
seq s (any s)
let bu (s : strategy) : strategy =
- fix (fun s' -> seq (choice (all_subterms s') s) (try_ s'))
+ fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))
let td (s : strategy) : strategy =
- fix (fun s' -> seq (choice s (all_subterms s')) (try_ s'))
+ fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))
let innermost (s : strategy) : strategy =
fix (fun ins -> choice (one_subterm ins) s)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0222ad115..bc25fe488 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -358,12 +358,14 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+Set Automatic Introduction.
+
Instance relation_equivalence_equivalence (A : Type) :
Equivalence (@relation_equivalence A).
-Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
-Instance relation_implication_preorder : PreOrder (@subrelation A).
-Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Instance relation_implication_preorder A : PreOrder (@subrelation A).
+Proof. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
(** *** Partial Order.
A partial order is a preorder which is additionally antisymmetric.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 50bcf589b..5633b7273 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -141,12 +141,15 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
| Explicit -> cl
in
let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
- let k, ctx', imps, subst =
- let c = Command.generalize_constr_expr tclass ctx in
- let imps, c' = interp_type_evars evars env c in
- let ctx, c = decompose_prod_assum c' in
- let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
- cl, ctx, imps, List.rev args
+ let k, ctx', len, imps, subst =
+ let (env', ctx), imps = interp_context_evars evars env ctx in
+ let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
+ let len = List.length ctx in
+ let imps = imps @ Impargs.lift_implicits len imps' in
+ let ctx', c = decompose_prod_assum c' in
+ let ctx' = ctx' @ ctx in
+ let cl, args = Typeclasses.dest_class_app (push_rel_context ctx' env) c in
+ cl, ctx', len, imps, List.rev args
in
let id =
match snd instid with
@@ -227,7 +230,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
let term = Termops.it_mkLambda_or_LetIn app ctx' in
evars := Evarutil.nf_evar_defs !evars;
let term = Evarutil.nf_isevar !evars term in
- let evm = (undefined_evars !evars) in
+ let evm = undefined_evars !evars in
Evarutil.check_evars env Evd.empty !evars termtype;
if Evd.is_empty evm then
declare_instance_constant k pri global imps ?hook id term termtype
@@ -238,9 +241,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
Command.start_proof id kind termtype
(fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
| _ -> assert false);
- if props <> [] then
- Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS !evars) *)
- (!refine_ref (evm, term));
+ if props <> [] then Pfedit.by (!refine_ref (evm, term))
+ else if Flags.is_auto_intros () then
+ Pfedit.by (Refiner.tclDO len Tactics.intro);
(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
id
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-07 15:49:28 +0000