diff options
| -rw-r--r-- | pretyping/typeclasses.ml | 20 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 8 | ||||
| -rw-r--r-- | tactics/class_tactics.ml4 | 141 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1704.v | 2 | ||||
| -rw-r--r-- | test-suite/typeclasses/unification_delta.v | 6 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 102 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 3 |
7 files changed, 166 insertions, 116 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c18b0e045..47be84460 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -341,9 +341,27 @@ let class_of_constr c = App (c, _) -> extract_ind c | _ -> extract_ind c +(* To embed a boolean for resolvability status. + This is essentially a hack to mark which evars correspond to + goals and do not need to be resolved when we have nested [resolve_all_evars] + calls (e.g. when doing apply in an External hint in typeclass_instances). + Would be solved by having real evars-as-goals. *) + +let ((bool_in : bool -> Dyn.t), + (bool_out : Dyn.t -> bool)) = Dyn.create "bool" + +let is_resolvable evi = + match evi.evar_extra with + Some t -> if Dyn.tag t = "bool" then bool_out t else true + | None -> true + +let mark_unresolvable evi = + { evi with evar_extra = Some (bool_in false) } + let has_typeclasses evd = Evd.fold (fun ev evi has -> has || - (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None)) + (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None + && is_resolvable evi)) evd false let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c06006ad0..dba60234b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -65,6 +65,14 @@ val is_class : inductive -> bool val class_of_constr : constr -> typeclass option val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool + +(* Use evar_extra for marking resolvable evars. *) +val bool_in : bool -> Dyn.t +val bool_out : Dyn.t -> bool + +val is_resolvable : evar_info -> bool +val mark_unresolvable : evar_info -> evar_info + val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index f06e9112f..998e767f5 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -51,28 +51,22 @@ let e_give_exact c gl = let assumption id = e_give_exact (mkVar id) -let gen_constant dir s = Coqlib.gen_constant "Class_tactics" dir s -let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") - open Unification -let deltaset = lazy - (Cpred.singleton (destConst (Lazy.force coq_relation))) - -let auto_unif_flags = lazy { +let auto_unif_flags = ref { modulo_conv_on_closed_terms = true; use_metas_eagerly = true; - modulo_delta = Lazy.force deltaset; + modulo_delta = Cpred.empty; } let unify_e_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let clenv' = clenv_unique_resolver false ~flags:(Lazy.force auto_unif_flags) clenv' gls in + let clenv' = clenv_unique_resolver false ~flags:(!auto_unif_flags) clenv' gls in Clenvtac.clenv_refine true clenv' gls let unify_resolve (c,clenv) gls = let clenv' = connect_clenv gls clenv in - let clenv' = clenv_unique_resolver false ~flags:(Lazy.force auto_unif_flags) clenv' gls in + let clenv' = clenv_unique_resolver false ~flags:(!auto_unif_flags) clenv' gls in Clenvtac.clenv_refine false clenv' gls let rec e_trivial_fail_db db_list local_db goal = @@ -295,50 +289,41 @@ let full_eauto ~(tac:tactic) debug n lems gls = let db_list = List.map searchtable_map dbnames in e_search_auto ~tac debug n lems db_list gls -exception Found of evar_defs - -let valid evm p res_sigma l = - let evd' = - Evd.fold - (fun ev evi (gls, sigma) -> - if not (Evd.is_evar evm ev) then - match gls with - hd :: tl -> - if evi.evar_body = Evar_empty then - let cstr, obls = Refiner.extract_open_proof !res_sigma hd in - (tl, Evd.evar_define ev cstr sigma) - else (tl, sigma) - | [] -> ([], sigma) - else if not (Evd.is_defined evm ev) && p ev evi then - match gls with - hd :: tl -> - if evi.evar_body = Evar_empty then - let cstr, obls = Refiner.extract_open_proof !res_sigma hd in - (tl, Evd.evar_define ev cstr sigma) - else (tl, sigma) - | [] -> assert(false) - else (gls, sigma)) - !res_sigma (l, Evd.create_evar_defs !res_sigma) - in raise (Found (snd evd')) +exception Found of evar_map let default_evars_tactic = fun x -> raise (UserError ("default_evars_tactic", mt())) (* tclFAIL 0 (Pp.mt ()) *) +let valid goals p res_sigma l = + let evm = + List.fold_left2 + (fun sigma (ev, evi) prf -> + let cstr, obls = Refiner.extract_open_proof !res_sigma prf in + if not (Evd.is_defined sigma ev) then + Evd.define sigma ev cstr + else sigma) + !res_sigma goals l + in raise (Found evm) + let resolve_all_evars_once ?(tac=default_evars_tactic) debug (mode, depth) env p evd = let evm = Evd.evars_of evd in - let goals, evm = + let goals, evm' = Evd.fold (fun ev evi (gls, evm) -> - (if evi.evar_body = Evar_empty && p ev evi then evi :: gls else gls), - Evd.add evm ev evi) + if evi.evar_body = Evar_empty + && Typeclasses.is_resolvable evi + && p ev evi then ((ev,evi) :: gls, Evd.add evm ev (Typeclasses.mark_unresolvable evi)) else + (gls, Evd.add evm ev evi)) evm ([], Evd.empty) in - let gls = { it = List.rev goals; sigma = evm } in - let res_sigma = ref evm in - let gls', valid' = full_eauto ~tac debug (mode, depth) [] (gls, valid evm p res_sigma) in + let goals = List.rev goals in + let gls = { it = List.map snd goals; sigma = evm' } in + let res_sigma = ref evm' in + let gls', valid' = full_eauto ~tac debug (mode, depth) [] (gls, valid goals p res_sigma) in res_sigma := Evarutil.nf_evars (sig_sig gls'); - try ignore(valid' []); assert(false) with Found evd' -> Evarutil.nf_evar_defs evd' + try ignore(valid' []); assert(false) + with Found evm' -> Evarutil.nf_evar_defs (Evd.evars_reset_evd evm' evd) exception FoundTerm of constr @@ -361,6 +346,76 @@ let rec resolve_all_evars ~(tac:tactic) debug m env p evd = else evd in aux 3 evd +(** Handling of the state of unfolded constants. *) + +open Libobject + +let freeze () = !auto_unif_flags.modulo_delta + +let unfreeze delta = + auto_unif_flags := { !auto_unif_flags with modulo_delta = delta } + +let init () = + auto_unif_flags := { + modulo_conv_on_closed_terms = true; + use_metas_eagerly = true; + modulo_delta = Cpred.empty; + } + +let _ = + Summary.declare_summary "typeclasses_unfold" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = true } + +let cache_autounfold (_,unfoldlist) = + auto_unif_flags := { !auto_unif_flags with + modulo_delta = Cpred.union !auto_unif_flags.modulo_delta unfoldlist } + +let subst_autounfold (_,subst,(unfoldlist as obj)) = + let b, l' = Cpred.elements unfoldlist in + let l'' = list_smartmap (fun x -> fst (Mod_subst.subst_con subst x)) l' in + if l'' == l' then obj + else + let set = List.fold_right Cpred.add l'' Cpred.empty in + if not b then set + else Cpred.complement set + +let classify_autounfold (_,obj) = Substitute obj + +let export_autounfold obj = + Some obj + +let (inAutoUnfold,outAutoUnfold) = + declare_object + {(default_object "AUTOUNFOLD") with + cache_function = cache_autounfold; + load_function = (fun _ -> cache_autounfold); + subst_function = subst_autounfold; + classify_function = classify_autounfold; + export_function = export_autounfold } + +let cpred_of_list l = + List.fold_right Cpred.add l Cpred.empty + +VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings +| [ "Typeclasses" "unfold" constr_list(cl) ] -> [ + let csts = + List.map + (fun c -> + let c = Constrintern.interp_constr Evd.empty (Global.env ()) c in + match kind_of_term c with + | Const c -> c + | _ -> error "Not a constant reference") + cl + in + Lib.add_anonymous_leaf (inAutoUnfold (cpred_of_list csts)) + ] +END + + (** Typeclass-based rewriting. *) let morphism_class = lazy (class_info (id_of_string "Morphism")) @@ -395,7 +450,7 @@ let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence") let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation") -(* let coq_relation = lazy (gen_constant ["RelationClasses";"Relation_Definitions"] "relation") *) +let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation") let mk_relation a = mkApp (Lazy.force coq_relation, [| a |]) let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT") diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/shouldsucceed/1704.v index 81b221690..4b02d5f93 100644 --- a/test-suite/bugs/closed/shouldsucceed/1704.v +++ b/test-suite/bugs/closed/shouldsucceed/1704.v @@ -12,6 +12,6 @@ Axiom r : False -> 0 == 1. Goal 0 == 0. Proof. rewrite r. -refl. +reflexivity. admit. Qed. diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v index b8789f26e..663a837f3 100644 --- a/test-suite/typeclasses/unification_delta.v +++ b/test-suite/typeclasses/unification_delta.v @@ -7,15 +7,15 @@ Lemma bla : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y Proof. intros. rewrite H0. - refl. + reflexivity. Defined. Lemma bla' : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x. Proof. intros. - (* Need delta no [relation] to unify with the right lemmas. *) + (* Need delta on [relation] to unify with the right lemmas. *) rewrite <- H0. - refl. + reflexivity. Qed. Axiom euclid : nat -> { x : nat | x > 0 } -> nat. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1eec3a24a..fbe90a9a9 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -97,6 +97,10 @@ Program Instance not_iff_morphism : Implicit Arguments Morphism [A]. +(** We allow to unfold the relation definition while doing morphism search. *) + +Typeclasses unfold relation. + (** Leibniz *) (* Instance Morphism (eq ++> eq ++> iff) (eq (A:=A)). *) @@ -169,53 +173,9 @@ Ltac subrelation_tac := set(H:=did 1) ; eapply @subrelation_morphism end. -Hint Resolve @subrelation_morphism 4 : typeclass_instances. - -(* Hint Extern 4 (@Morphism _ (_ --> _) _) => subrelation_tac : typeclass_instances. *) - -(* Goal forall A, Morphism (eq ++> eq ++> impl) (@eq A). *) -(* Proof. *) -(* intros. *) -(* eauto with typeclass_instances. *) -(* Set Printing All. *) -(* Show Proof. *) - (* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *) -(* Program Instance `A` (R : relation A) `B` (R' : relation B) *) -(* [ ? Morphism (R ==> R' ==> iff) m ] => *) -(* iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *) - -(* Next Obligation. *) -(* Proof. *) -(* destruct respect with x y x0 y0 ; auto. *) -(* Qed. *) - -(* Program Instance `A` (R : relation A) `B` (R' : relation B) *) -(* [ ? Morphism (R ==> R' ==> iff) m ] => *) -(* iff_inverse_impl_binary_morphism : ? Morphism (R ==> R' ==> inverse impl) m. *) - -(* Next Obligation. *) -(* Proof. *) -(* destruct respect with x y x0 y0 ; auto. *) -(* Qed. *) - - -(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *) -(* iff_impl_morphism : ? Morphism (R ==> impl) m. *) - -(* Next Obligation. *) -(* Proof. *) -(* destruct respect with x y ; auto. *) -(* Qed. *) - -(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *) -(* iff_inverse_impl_morphism : ? Morphism (R ==> inverse impl) m. *) - -(* Next Obligation. *) -(* Proof. *) -(* destruct respect with x y ; auto. *) -(* Qed. *) +Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. (** Logical implication [impl] is a morphism for logical equivalence. *) @@ -224,7 +184,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl (* Typeclasses eauto := debug. *) Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => reflexive_impl_iff : Morphism (R ==> iff) m. - + Next Obligation. Proof. split ; apply respect ; [ auto | symmetry ] ; auto. @@ -292,18 +252,18 @@ Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) apply r ; auto. Qed. -Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) (C : Type) (R'' : relation C) - [ Morphism (R ++> R' ++> R'') m ] => - morphism_inverse_inverse_morphism : - Morphism (R --> R' --> inverse R'') m. +(* Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) (C : Type) (R'' : relation C) *) +(* [ Morphism (R ++> R' ++> R'') m ] => *) +(* morphism_inverse_inverse_morphism : *) +(* Morphism (R --> R' --> inverse R'') m. *) - Next Obligation. - Proof. - unfold inverse in *. - pose respect. - unfold respectful in r. - apply r ; auto. - Qed. +(* Next Obligation. *) +(* Proof. *) +(* unfold inverse in *. *) +(* pose respect. *) +(* unfold respectful in r. *) +(* apply r ; auto. *) +(* Qed. *) (** Every transitive relation gives rise to a binary morphism on [impl], @@ -514,14 +474,22 @@ Program Instance or_iff_morphism : (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) -Instance {A B : Type} (m : A -> B) => - any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. -Proof. - red ; intros. subst ; reflexivity. -Qed. +(* Instance {A B : Type} (m : A -> B) => *) +(* any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. *) +(* Proof. *) +(* red ; intros. subst ; reflexivity. *) +(* Qed. *) -Instance {A : Type} (m : A -> Prop) => - any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. -Proof. - red ; intros. subst ; split; trivial. -Qed. +(* Instance {A : Type} (m : A -> Prop) => *) +(* any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. *) +(* Proof. *) +(* red ; intros. subst ; split; trivial. *) +(* Qed. *) + +Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) => + eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. +Proof. simpl_relation. Qed. + +Instance (A B : Type) [ ! Reflexive B R' ] => + Reflexive (@Logic.eq A ==> R'). +Proof. simpl_relation. Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index b355c3c08..5cf33542c 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -8,7 +8,6 @@ (************************************************************************) (* Typeclass-based setoids, tactics and standard instances. - TODO: explain clrewrite, clsubstitute and so on. Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud @@ -32,6 +31,8 @@ Class Setoid A := equiv : relation A ; setoid_equiv :> Equivalence A equiv. +Typeclasses unfold @equiv. + (* Too dangerous instance *) (* Program Instance [ eqa : Equivalence A eqA ] => *) (* equivalence_setoid : Setoid A := *) |