Add the possibility of specifying constants to unfold for typeclass

resolution. Add [relation] and Setoid's [equiv] as such objects. 
Considerably simplify resolve_all_evars for typeclass resolution, adding
a further refinement (and hack): evars get classified as non-resolvable
(using the evar_extra dynamic field) if they are turned into a
goal. This makes it possible to perform nested typeclass resolution
without looping. We
take advantage of that in Classes/Morphisms where [subrelation_tac] is
added to the [Morphism] search procedure and calls the apply tactic which
itself triggers typeclass resolution. Having [subrelation_tac] as a tactic
instead of an instance, we can actually force that it is applied only
once in each search branch and avoid looping.
We could get rid of the hack when we have real goals-as-evars
functionality (hint hint).
Also fix some test-suite scripts which were still calling [refl] 
instead of [reflexivity].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10687 85f007b7-540e-0410-9357-904b9bb8a0f7

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 := *)