aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/class_tactics.ml450
-rw-r--r--tactics/rewrite.ml42
-rw-r--r--theories/Classes/Morphisms.v57
3 files changed, 72 insertions, 37 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 222efb54e..890f3a086 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -205,7 +205,9 @@ let typeclasses_debug = ref false
type validation = evar_map -> proof_tree list -> proof_tree
-type autoinfo = { hints : Auto.hint_db; auto_depth: int; auto_last_tac: std_ppcmds }
+let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
+
+type autoinfo = { hints : Auto.hint_db; auto_depth: int list; auto_last_tac: std_ppcmds }
type autogoal = goal * autoinfo
type 'ans fk = unit -> 'ans
type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -254,34 +256,38 @@ let solve_tac (x : 'a tac) : 'a tac =
let hints_tac hints =
{ skft = fun sk fk {it = gl,info; sigma = s} ->
- if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac
- ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl);
+(* if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac *)
+(* ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl); *)
let possible_resolve ((lgls,v) as res, pri, pp) =
(pri, pp, res)
in
let tacs =
- let poss = e_possible_resolve hints info.hints (Evarutil.nf_evar s gl.evar_concl) in
+ let concl = Evarutil.nf_evar s gl.evar_concl in
+ let poss = e_possible_resolve hints info.hints concl in
let l =
Util.list_map_append (fun (tac, pri, pptac) ->
try [tac {it = gl; sigma = s}, pri, pptac] with e when catchable e -> [])
poss
in
+ if l = [] && !typeclasses_debug then
+ msgnl (pr_depth info.auto_depth ++ str": no match for " ++
+ Printer.pr_constr_env (Evd.evar_env gl) concl ++ int (List.length poss) ++ str" possibilities");
List.map possible_resolve l
in
let tacs = List.sort compare tacs in
- let info = { info with auto_depth = succ info.auto_depth } in
- let rec aux = function
+ let rec aux i = function
| (_, pp, ({it = gls; sigma = s}, v)) :: tl ->
- if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ pp
- ++ spc () ++ str"succeeded on" ++ spc () ++ pr_ev s gl);
+ if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ pp
+ ++ str" on" ++ spc () ++ pr_ev s gl);
let fk =
- (fun () -> if !typeclasses_debug then msgnl (str"backtracked after " ++ pp ++ spc () ++ str"failed");
- aux tl)
+ (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
+ aux (succ i) tl)
in
- let glsv = {it = List.map (fun g -> g, { info with auto_last_tac = pp }) gls; sigma = s}, fun _ -> v in
+ let glsv = {it = list_map_i (fun j g -> g,
+ { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
sk glsv fk
| [] -> fk ()
- in aux tacs }
+ in aux 1 tacs }
let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
let rec aux s (acc : (autogoal list * validation) list) fk = function
@@ -344,10 +350,12 @@ let make_autogoal ?(st=full_transparent_state) g =
let sign = pf_hyps g in
let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) None) sign in
let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in
- (g.it, { hints = hints ; auto_depth = 0; auto_last_tac = mt() })
+ (g.it, { hints = hints ; auto_depth = []; auto_last_tac = mt() })
let make_autogoals ?(st=full_transparent_state) gs evm' =
- { it = List.map (fun g -> make_autogoal ~st {it = snd g; sigma = evm'}) gs; sigma = evm' }
+ { it = list_map_i (fun i g ->
+ let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
+ (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
let run_on_evars ?(st=full_transparent_state) p evm tac =
match evars_to_goals p evm with
@@ -642,3 +650,17 @@ TACTIC EXTEND not_evar
| Evar _ -> tclFAIL 0 (str"Evar")
| _ -> tclIDTAC ]
END
+
+TACTIC EXTEND is_ground
+ [ "is_ground" constr(ty) ] -> [ fun gl ->
+ if Evarutil.is_ground_term (project gl) ty then tclIDTAC gl
+ else tclFAIL 0 (str"Not ground") gl ]
+END
+
+TACTIC EXTEND autoapply
+ [ "autoapply" constr(c) "using" preident(i) ] -> [ fun gl ->
+ let flags = flags_of_state (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
+ let cty = pf_type_of gl c in
+ let ce = mk_clenv_from gl (c,cty) in
+ unify_e_resolve flags (c,ce) gl ]
+END
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 216beab54..213f0d11e 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -581,7 +581,7 @@ let subterm all flags (s : strategy) : strategy =
| Lambda (n, t, b) when flags.under_lambdas ->
let env' = Environ.push_rel (n, None, t) env in
- let b' = aux env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in
+ let b' = s env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in
(match b' with
| Some (Some r) ->
Some (Some { r with
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8297b9bd3..ee3d7876d 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -118,15 +118,23 @@ Proof. firstorder. Qed.
(** The subrelation property goes through products as usual. *)
-Instance subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
+Lemma subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) :
subrelation (R₁ ==> S₁) (R₂ ==> S₂).
Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
(** And of course it is reflexive. *)
-Instance subrelation_refl : ! subrelation A R R.
+Lemma subrelation_refl A R : @subrelation A R R.
Proof. simpl_relation. Qed.
+Ltac class_apply c := autoapply c using typeclass_instances.
+
+Ltac subrelation_tac T U :=
+ (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
+ class_apply @subrelation_respectful || class_apply @subrelation_refl.
+
+Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
+
(** [Proper] is itself a covariant morphism for [subrelation]. *)
Lemma subrelation_proper `(mor : Proper A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
@@ -139,10 +147,10 @@ CoInductive apply_subrelation : Prop := do_subrelation.
Ltac proper_subrelation :=
match goal with
- [ H : apply_subrelation |- _ ] => clear H ; eapply @subrelation_proper
+ [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
end.
-Hint Extern 4 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
+Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
Instance proper_subrelation_proper :
Proper (subrelation ++> @eq _ ==> impl) (@Proper A).
@@ -188,7 +196,7 @@ Program Instance flip_proper
contravariant in the first argument, covariant in the second. *)
Program Instance trans_contra_co_morphism
- `(Transitive A R) : Proper (R --> R ++> impl) R | 6.
+ `(Transitive A R) : Proper (R --> R ++> impl) R.
Next Obligation.
Proof with auto.
@@ -245,7 +253,7 @@ Program Instance per_partial_app_morphism
to get an [R y z] goal. *)
Program Instance trans_co_eq_inv_impl_morphism
- `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 3.
+ `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2.
Next Obligation.
Proof with auto.
@@ -254,7 +262,7 @@ Program Instance trans_co_eq_inv_impl_morphism
(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
-Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 2.
+Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
Next Obligation.
Proof with auto.
@@ -322,8 +330,8 @@ Proof. firstorder. Qed.
Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x.
Proof. firstorder. Qed.
-Hint Extern 1 (ProperProxy _ _) => apply eq_proper_proxy || eapply @reflexive_proper_proxy : typeclass_instances.
-(* Hint Extern 2 (ProperProxy ?R _) => not_evar R ; eapply @proper_proper_proxy : typeclass_instances. *)
+Hint Extern 1 (ProperProxy _ _) => class_apply eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+Hint Extern 2 (ProperProxy ?R _) => not_evar R ; class_apply @proper_proper_proxy : typeclass_instances.
(** [R] is Reflexive, hence we can build the needed proof. *)
@@ -340,7 +348,7 @@ CoInductive normalization_done : Prop := did_normalization.
Ltac partial_application_tactic :=
let rec do_partial_apps H m :=
match m with
- | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
+ | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
| _ => idtac
end
in
@@ -368,10 +376,10 @@ Ltac partial_application_tactic :=
| [ |- @Proper ?T _ (?m ?x) ] =>
match goal with
| [ _ : PartialApplication |- _ ] =>
- eapply @Reflexive_partial_app_morphism
+ class_apply @Reflexive_partial_app_morphism
| _ =>
on_morphism (m x) ||
- (eapply @Reflexive_partial_app_morphism ;
+ (class_apply @Reflexive_partial_app_morphism ;
[ pose Build_PartialApplication | idtac ])
end
end.
@@ -407,8 +415,8 @@ Qed.
Ltac inverse :=
match goal with
- | [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow
- | _ => eapply @inverse_atom
+ | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow
+ | _ => class_apply @inverse_atom
end.
Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
@@ -422,18 +430,21 @@ Proof. firstorder. Qed.
Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
Proof. firstorder. Qed.
-Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
-Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances.
+Hint Extern 1 (subrelation (flip _) _) => class_apply @inverse1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances.
(** That's if and only if *)
-Instance eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
+
+Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
Proof. simpl_relation. Qed.
+Hint Extern 3 (subrelation (@eq _) ?R) => not_evar R ; class_apply eq_subrelation.
+
(** Once we have normalized, we will apply this instance to simplify the problem. *)
Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor.
-Hint Extern 2 (@Proper _ (flip _) _) => eapply @proper_inverse_proper : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances.
(** Bootstrap !!! *)
@@ -450,8 +461,9 @@ Qed.
Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.
Proof.
- intros A R0 m H R' H'.
- red in H, H'. setoid_rewrite H.
+ intros A R0 R1 H m H'.
+ red in H, H'.
+ setoid_rewrite H.
assumption.
Qed.
@@ -459,7 +471,7 @@ Ltac proper_normalization :=
match goal with
| [ _ : normalization_done |- _ ] => fail 1
| [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in
- set(H:=did_normalization) ; eapply @proper_normalizes_proper
+ set(H:=did_normalization) ; class_apply @proper_normalizes_proper
end.
Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances.
@@ -476,7 +488,8 @@ Proof. intros. apply reflexive_proper. Qed.
Ltac proper_reflexive :=
match goal with
| [ _ : normalization_done |- _ ] => fail 1
- | [ |- @Proper _ _ _ ] => apply proper_eq || eapply @reflexive_proper
+ | [ _ : apply_subrelation |- _ ] => class_apply proper_eq || class_apply @reflexive_proper
+ | _ => class_apply proper_eq
end.
Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 17:07:59 +0000