- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence

  as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
  uglily to be factorized by hand.
- Typography in RefMan-tac.tex.



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

7 files changed, 122 insertions, 87 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 907995c542..aceb5c5250 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -325,8 +325,8 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
     | e when Logic.catchable_exception e -> anomaly "make_resolve_hyp"
 
 (* REM : in most cases hintname = id *)
-let make_unfold (ref, eref) =
-  (Some ref,
+let make_unfold eref =
+  (Some (global_of_evaluable_reference eref),
    { pri = 4;
      pat = None;
      code = Unfold_nth eref })
@@ -522,57 +522,57 @@ let forward_intern_tac =
 
 let set_extern_intern_tac f = forward_intern_tac := f
 
-let add_hints local dbnames0 h =
-  let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
-  let env = Global.env() and sigma = Evd.empty in
-  let f = Constrintern.interp_constr sigma env in
+type hints_entry =
+  | HintsResolveEntry of (int option * bool * constr) list
+  | HintsImmediateEntry of constr list
+  | HintsUnfoldEntry of evaluable_global_reference list
+  | HintsTransparencyEntry of evaluable_global_reference list * bool
+  | HintsExternEntry of 
+      int * (patvar list * constr_pattern) option * glob_tactic_expr
+  | HintsDestructEntry of identifier * int * (bool,unit) location * 
+      (patvar list * constr_pattern) * glob_tactic_expr
+
+let interp_hints h =
+  let f = Constrintern.interp_constr Evd.empty (Global.env()) in
+  let fr r =
+    let gr = Syntax_def.global_with_alias r in
+    let r' = evaluable_of_global_reference (Global.env()) gr in
+    Dumpglob.add_glob (loc_of_reference r) gr;
+    r' in
+  let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
-  | HintsResolve lhints ->	
-      add_resolves env sigma (List.map (fun (pri, b, x) -> pri, b, f x) lhints) local dbnames
-  | HintsImmediate lhints ->
-      add_trivials env sigma (List.map f lhints) local dbnames
-  | HintsUnfold lhints ->
-      let f r =
-	let gr = Syntax_def.global_with_alias r in
-        let r' = match gr with
-         | ConstRef c -> EvalConstRef c
-         | VarRef c -> EvalVarRef c
-         | _ -> 
-           errorlabstrm "evalref_of_ref"
-            (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
-             str "to an evaluable reference.")
-        in
-	  Dumpglob.add_glob (loc_of_reference r) gr;
-	 (gr,r') in
-      add_unfolds (List.map f lhints) local dbnames
- | HintsTransparency (lhints, b) ->
-      let f r =
-	let gr = Syntax_def.global_with_alias r in
-        let r' = match gr with
-         | ConstRef c -> EvalConstRef c
-         | VarRef c -> EvalVarRef c
-         | _ -> 
-           errorlabstrm "evalref_of_ref"
-            (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
-             str "to an evaluable reference.")
-        in
-	  Dumpglob.add_glob (loc_of_reference r) gr;
-	  r' in
-      add_transparency (List.map f lhints) b local dbnames
+  | HintsResolve lhints -> HintsResolveEntry (List.map (on_pi3 f) lhints)
+  | HintsImmediate lhints -> HintsImmediateEntry (List.map f lhints)
+  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
+  | HintsTransparency (lhints, b) ->
+      HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
-      let add_one qid =
-        let env = Global.env() and sigma = Evd.empty in
+      let constr_hints_of_ind qid =
         let isp = inductive_of_reference qid in
         let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
-        let lcons = list_tabulate
-          (fun i -> None, true, mkConstruct (isp,i+1)) (Array.length consnames) in
-        add_resolves env sigma lcons local dbnames in
-      List.iter add_one lqid
+        list_tabulate (fun i -> None, true, mkConstruct (isp,i+1))
+	  (Array.length consnames) in
+	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Option.map (Constrintern.intern_constr_pattern Evd.empty (Global.env())) patcom in
+      let pat =	Option.map fp patcom in
       let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
-      add_externs pri pat tacexp local dbnames
+      HintsExternEntry (pri, pat, tacexp)
   | HintsDestruct(na,pri,loc,pat,code) ->
+      let (l,_ as pat) = fp pat in
+      HintsDestructEntry (na,pri,loc,pat,!forward_intern_tac l code)
+
+let add_hints local dbnames0 h =
+  let dbnames = if dbnames0 = [] then ["core"] else dbnames0 in
+  let env = Global.env() and sigma = Evd.empty in
+  match h with
+  | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
+  | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
+  | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
+  | HintsTransparencyEntry (lhints, b) ->
+      add_transparency lhints b local dbnames
+  | HintsExternEntry (pri, pat, tacexp) ->
+      add_externs pri pat tacexp local dbnames
+  | HintsDestructEntry (na,pri,loc,pat,code) ->
       if dbnames0<>[] then
         warn (str"Database selection not implemented for destruct hints");
       Dhyp.add_destructor_hint local na loc pat pri code
diff --git a/tactics/auto.mli b/tactics/auto.mli
index f893c9b15f..982a4e68ec 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -69,6 +69,16 @@ type hint_db_name = string
 
 type hint_db = Hint_db.t
 
+type hints_entry =
+  | HintsResolveEntry of (int option * bool * constr) list
+  | HintsImmediateEntry of constr list
+  | HintsUnfoldEntry of evaluable_global_reference list
+  | HintsTransparencyEntry of evaluable_global_reference list * bool
+  | HintsExternEntry of 
+      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+  | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location * 
+      (patvar list * constr_pattern) * Tacexpr.glob_tactic_expr
+
 val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
@@ -82,7 +92,9 @@ val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
 val current_db_names : unit -> hint_db_name list
 
-val add_hints : locality_flag -> hint_db_name list -> hints -> unit
+val interp_hints : hints_expr -> hints_entry
+
+val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
 val print_searchtable : unit -> unit
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 890f3a086e..e09ba93f8e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -480,13 +480,15 @@ let _ =
     
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, true))
+    add_hints false [typeclasses_db]
+      (interp_hints (Vernacexpr.HintsTransparency (cl, true)))
   ]
 END
 	
 VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
 | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db] (Vernacexpr.HintsTransparency (cl, false))
+    add_hints false [typeclasses_db]
+      (interp_hints (Vernacexpr.HintsTransparency (cl, false)))
   ]
 END
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index b37212d9d6..3d34a2d688 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -225,16 +225,10 @@ let (inDD,_) =
 		    classify_function = classify_dd;
                     export_function = export_dd }
 
-let forward_intern_tac = 
-  ref (fun _ -> failwith "intern_tac is not installed for DHyp")
-
-let set_extern_intern_tac f = forward_intern_tac := f
-
 let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
 let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
     
-let add_destructor_hint local na loc pat pri code =
-  let code = !forward_intern_tac code in
+let add_destructor_hint local na loc (_,pat) pri code =
   let code =
     begin match loc, code with
       | HypLocation _, TacFun ([id],body) -> (id,body)
@@ -243,8 +237,6 @@ let add_destructor_hint local na loc pat pri code =
 	  errorlabstrm "add_destructor_hint"
           (str "The tactic should be a function of the hypothesis name.") end
   in
-  let (_,pat) = Constrintern.intern_constr_pattern Evd.empty (Global.env()) pat
-  in
   let pat = match loc with
     | HypLocation b ->
 	HypLocation
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index c86102e935..3277fd2e67 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -17,7 +17,6 @@ open Tacexpr
 (* Programmable destruction of hypotheses and conclusions. *)
 
 val set_extern_interp : (glob_tactic_expr -> tactic) -> unit
-val set_extern_intern_tac : (raw_tactic_expr -> glob_tactic_expr) -> unit
 
 (*
 val dHyp : identifier -> tactic
@@ -29,4 +28,5 @@ val h_auto_tdb : int option -> tactic
 
 val add_destructor_hint :
   Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
-    Topconstr.constr_expr -> int -> raw_tactic_expr -> unit
+    Rawterm.patvar list * Pattern.constr_pattern -> int -> 
+      glob_tactic_expr -> unit
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 28e3888453..6bf3e34b02 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -204,6 +204,47 @@ VERNAC COMMAND EXTEND HintRewrite
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
     ":" preident(b) ] ->
   [ add_rewrite_hint b o t l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+  [ add_rewrite_hint "core" o (Tacexpr.TacId []) l ]
+| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+  [ add_rewrite_hint "core" o t l ]
+END
+
+open Term
+open Coqlib
+
+let project_hint pri l2r c =
+  let env = Global.env() in
+  let c = Constrintern.interp_constr Evd.empty env c in
+  let t = Retyping.get_type_of env Evd.empty c in
+  let t = 
+    Tacred.reduce_to_quantified_ref env Evd.empty (Lazy.force coq_iff_ref) t in
+  let sign,ccl = decompose_prod_assum t in
+  let (a,b) = match snd (decompose_app ccl) with
+    | [a;b] -> (a,b)
+    | _ -> assert false in
+  let p =
+    if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
+  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
+  let c = it_mkLambda_or_LetIn
+    (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
+  (pri,true,c)
+
+let add_hints_iff l2r lc n bl =
+  Auto.add_hints true bl
+    (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
+
+VERNAC COMMAND EXTEND HintResolveIff
+  [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n)
+    ":" preident_list(bl) ] ->
+  [ add_hints_iff true lc n bl ]
+| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n)
+    ":" preident_list(bl) ] ->
+  [ add_hints_iff false lc n bl ]
+| [ "Hint" "Resolve" "->" ne_constr_list(lc) natural_opt(n) ] ->
+  [ add_hints_iff true lc n ["core"] ]
+| [ "Hint" "Resolve" "<-" ne_constr_list(lc) natural_opt(n) ] ->
+  [ add_hints_iff false lc n ["core"] ]
 END
 
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 88692a13c5..8236f3e9e5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -174,11 +174,6 @@ let find_reference env qid =
 	-> VarRef id
     | _ -> Nametab.locate qid
 
-let error_not_evaluable s =
-  errorlabstrm "evalref_of_ref" 
-    (str "Cannot coerce" ++ spc ()  ++ s ++ spc () ++
-     str "to an evaluable reference.")
-
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
 let add_primitive_tactic s tac =
@@ -315,23 +310,23 @@ let coerce_to_tactic loc id = function
 
 (* We have identifier <| global_reference <| constr *)
 
-let find_ident id sign = 
-  List.mem id (fst sign.ltacvars) or 
-  List.mem id (ids_of_named_context (Environ.named_context sign.genv))
+let find_ident id ist = 
+  List.mem id (fst ist.ltacvars) or 
+  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
-let find_recvar qid sign = List.assoc qid sign.ltacrecvars
+let find_recvar qid ist = List.assoc qid ist.ltacrecvars
 
 (* a "var" is a ltac var or a var introduced by an intro tactic *)
-let find_var id sign = List.mem id (fst sign.ltacvars)
+let find_var id ist = List.mem id (fst ist.ltacvars)
 
 (* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
-let find_ctxvar id sign = List.mem id (snd sign.ltacvars)
+let find_ctxvar id ist = List.mem id (snd ist.ltacvars)
 
 (* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
-let find_ltacvar id sign = find_var id sign & not (find_ctxvar id sign)
+let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist)
 
-let find_hyp id sign =
-  List.mem id (ids_of_named_context (Environ.named_context sign.genv))
+let find_hyp id ist =
+  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
 (* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
 (* be fresh in which case it is binding later on *)
@@ -549,11 +544,6 @@ let intern_induction_arg ist = function
       else
 	ElimOnIdent (loc,id)
 
-let evaluable_of_global_reference = function
-  | ConstRef c -> EvalConstRef c
-  | VarRef c -> EvalVarRef c
-  | r -> error_not_evaluable (pr_global r)
-
 let short_name = function
   | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
   | _ -> None
@@ -566,21 +556,21 @@ let interp_global_reference r =
   | Ident (loc,id) when not !strict_check -> VarRef id
   | _ -> error_global_not_found_loc lqid
 
-let intern_evaluable_reference_or_by_notation = function
-  | AN r -> evaluable_of_global_reference (interp_global_reference r)
+let intern_evaluable_reference_or_by_notation ist = function
+  | AN r -> evaluable_of_global_reference ist.genv (interp_global_reference r)
   | ByNotation (loc,ntn,sc) ->
-      evaluable_of_global_reference
+      evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference loc
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
-(* Globalizes a reduction expression *)
+(* Globalize a reduction expression *)
 let intern_evaluable ist = function
   | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
   | AN (Ident (_,id)) when
       (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
       ArgArg (EvalVarRef id, None)
   | r ->
-      let e = intern_evaluable_reference_or_by_notation r in
+      let e = intern_evaluable_reference_or_by_notation ist r in
       let na = short_name r in
       ArgArg (e,na)
 
@@ -1331,7 +1321,7 @@ let interp_evaluable ist env = function
       (* Maybe [id] has been introduced by Intro-like tactics *)
       (try match Environ.lookup_named id env with
        | (_,Some _,_) -> EvalVarRef id
-       | _ -> error_not_evaluable (pr_id id)
+       | _ -> error_not_evaluable (VarRef id)
        with Not_found ->
        match r with
        | EvalConstRef _ -> r
@@ -2951,5 +2941,3 @@ let _ = Auto.set_extern_intern_tac
     (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
 let _ = Auto.set_extern_subst_tactic subst_tactic
 let _ = Dhyp.set_extern_interp eval_tactic
-let _ = Dhyp.set_extern_intern_tac
-  (fun t -> intern_tactic (make_empty_glob_sign()) t)