Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 102 insertions, 68 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index eef6a0ee..521c5ed2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -1,14 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: auto.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Util
 open Names
 open Term
@@ -22,31 +19,52 @@ open Evd
 open Libnames
 open Vernacexpr
 open Mod_subst
-(*i*)
 
-type auto_tactic =
-  | Res_pf     of constr * clausenv    (* Hint Apply *)
-  | ERes_pf    of constr * clausenv    (* Hint EApply *)
+(** Auto and related automation tactics *)
+
+type 'a auto_tactic =
+  | Res_pf     of constr * 'a    (** Hint Apply *)
+  | ERes_pf    of constr * 'a    (** Hint EApply *)
   | Give_exact of constr
-  | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *)
-  | Unfold_nth of evaluable_global_reference          (* Hint Unfold *)
-  | Extern     of Tacexpr.glob_tactic_expr   (* Hint Extern *)
+  | Res_pf_THEN_trivial_fail of constr * 'a (** Hint Immediate *)
+  | Unfold_nth of evaluable_global_reference          (** Hint Unfold *)
+  | Extern     of Tacexpr.glob_tactic_expr   (** Hint Extern *)
 
-open Rawterm
+open Glob_term
 
-type pri_auto_tactic = {
-  pri   : int;            (* A number between 0 and 4, 4 = lower priority *)
-  pat   : constr_pattern option; (* A pattern for the concl of the Goal *)
-  code  : auto_tactic;    (* the tactic to apply when the concl matches pat *)
+type hints_path_atom = 
+  | PathHints of global_reference list
+  | PathAny
+
+type 'a gen_auto_tactic = {
+  pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
+  pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
+  name  : hints_path_atom; (** A potential name to refer to the hint *) 
+  code  : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
 }
 
-type stored_data = pri_auto_tactic
+type pri_auto_tactic = clausenv gen_auto_tactic
+
+type stored_data = int * clausenv gen_auto_tactic
 
 type search_entry
 
-(* The head may not be bound. *)
+(** The head may not be bound. *)
 
-type hint_entry = global_reference option * pri_auto_tactic
+type hint_entry = global_reference option * types gen_auto_tactic
+
+type hints_path =
+  | PathAtom of hints_path_atom
+  | PathStar of hints_path
+  | PathSeq of hints_path * hints_path
+  | PathOr of hints_path * hints_path
+  | PathEmpty
+  | PathEpsilon
+
+val normalize_path : hints_path -> hints_path
+val path_matches : hints_path -> hints_path_atom list -> bool
+val path_derivate : hints_path -> hints_path_atom -> hints_path
+val pp_hints_path : hints_path -> Pp.std_ppcmds
 
 module Hint_db :
   sig
@@ -58,12 +76,17 @@ module Hint_db :
     val map_auto : global_reference * constr -> t -> pri_auto_tactic list
     val add_one : hint_entry -> t -> t
     val add_list : (hint_entry) list -> t -> t
-    val iter : (global_reference option -> stored_data list -> unit) -> t -> unit
+    val remove_one : global_reference -> t -> t
+    val remove_list : global_reference list -> t -> t
+    val iter : (global_reference option -> pri_auto_tactic list -> unit) -> t -> unit
 
     val use_dn : t -> bool
     val transparent_state : t -> transparent_state
     val set_transparent_state : t -> transparent_state -> t
 
+    val add_cut : hints_path -> t -> t
+    val cut : t -> hints_path
+
     val unfolds : t -> Idset.t * Cset.t
   end
 
@@ -72,8 +95,9 @@ 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
+  | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list
+  | HintsImmediateEntry of (hints_path_atom * constr) list
+  | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -85,19 +109,23 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
-(* [create_hint_db local name st use_dn].
+(** [create_hint_db local name st use_dn].
    [st] is a transparency state for unification using this db
    [use_dn] switches the use of the discrimination net for all hints
    and patterns. *)
 
 val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
+val remove_hints : bool -> hint_db_name list -> global_reference list -> unit
+
 val current_db_names : unit -> hint_db_name list
 
 val interp_hints : hints_expr -> hints_entry
 
 val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
+val prepare_hint : env -> open_constr -> constr
+
 val print_searchtable : unit -> unit
 
 val print_applicable_hint : unit -> unit
@@ -108,13 +136,13 @@ val print_hint_db_by_name : hint_db_name -> unit
 
 val print_hint_db : Hint_db.t -> unit
 
-(* [make_exact_entry pri (c, ctyp)].
+(** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
 
-val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> ?name:hints_path_atom -> constr * constr -> hint_entry
 
-(* [make_apply_entry (eapply,verbose) pri (c,cty)].
+(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
    [hnf] should be true if we should expand the head of cty before searching for
    products;
@@ -122,21 +150,21 @@ val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
    [cty] is the type of [c]. *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> int option -> constr * constr
-      -> hint_entry
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> 
+  constr * constr -> hint_entry
 
-(* A constr which is Hint'ed will be:
-   (1) used as an Exact, if it does not start with a product
-   (2) used as an Apply, if its HNF starts with a product, and
-       has no missing arguments.
-   (3) used as an EApply, if its HNF starts with a product, and
-       has missing arguments. *)
+(** A constr which is Hint'ed will be:
+   - (1) used as an Exact, if it does not start with a product
+   - (2) used as an Apply, if its HNF starts with a product, and
+         has no missing arguments.
+   - (3) used as an EApply, if its HNF starts with a product, and
+         has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> constr ->
-      hint_entry list
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:hints_path_atom -> 
+  constr -> hint_entry list
 
-(* [make_resolve_hyp hname htyp].
+(** [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
    Never raises a user exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
@@ -144,7 +172,7 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-(* [make_extern pri pattern tactic_expr] *)
+(** [make_extern pri pattern tactic_expr] *)
 
 val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
@@ -161,11 +189,11 @@ val set_extern_subst_tactic :
   (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr)
   -> unit
 
-(* Create a Hint database from the pairs (name, constr).
+(** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
-val make_local_hint_db : bool -> constr list -> goal sigma -> hint_db
+val make_local_hint_db : ?ts:transparent_state -> bool -> open_constr list -> goal sigma -> hint_db
 
 val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
 
@@ -173,63 +201,69 @@ val default_search_depth : int ref
 
 val auto_unif_flags : Unification.unify_flags
 
-(* Try unification with the precompiled clause, then use registered Apply *)
+(** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : (constr * clausenv) -> tactic
 
 val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic
 
-(* [ConclPattern concl pat tacast]:
+(** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
 val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic
 
-(* The Auto tactic *)
+(** The Auto tactic *)
 
-val auto : int -> constr list -> hint_db_name list -> tactic
+(** The use of the "core" database can be de-activated by passing
+    "nocore" amongst the databases. *)
 
-(* Auto with more delta. *)
+val make_db_list : hint_db_name list -> hint_db list
 
-val new_auto : int -> constr list -> hint_db_name list -> tactic
+val auto : int -> open_constr list -> hint_db_name list -> tactic
 
-(* auto with default search depth and with the hint database "core" *)
+(** Auto with more delta. *)
+
+val new_auto : int -> open_constr list -> hint_db_name list -> tactic
+
+(** auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
 
-(* auto with all hint databases except the "v62" compatibility database *)
-val full_auto : int -> constr list -> tactic
+(** auto with all hint databases except the "v62" compatibility database *)
+val full_auto : int -> open_constr list -> tactic
 
-(* auto with all hint databases except the "v62" compatibility database
+(** auto with all hint databases except the "v62" compatibility database
    and doing delta *)
-val new_full_auto : int -> constr list -> tactic
+val new_full_auto : int -> open_constr list -> tactic
 
-(* auto with default search depth and with all hint databases
+(** auto with default search depth and with all hint databases
    except the "v62" compatibility database *)
 val default_full_auto : tactic
 
-(* The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : int option -> constr list -> hint_db_name list option -> tactic
+(** The generic form of auto (second arg [None] means all bases) *)
+val gen_auto : int option -> open_constr list -> hint_db_name list option -> tactic
 
-(* The hidden version of auto *)
-val h_auto   : int option -> constr list -> hint_db_name list option -> tactic
+(** The hidden version of auto *)
+val h_auto   : int option -> open_constr list -> hint_db_name list option -> tactic
 
-(* Trivial *)
-val trivial : constr list -> hint_db_name list -> tactic
-val gen_trivial : constr list -> hint_db_name list option -> tactic
-val full_trivial : constr list -> tactic
-val h_trivial : constr list -> hint_db_name list option -> tactic
+(** Trivial *)
+val trivial : open_constr list -> hint_db_name list -> tactic
+val gen_trivial : open_constr list -> hint_db_name list option -> tactic
+val full_trivial : open_constr list -> tactic
+val h_trivial : open_constr list -> hint_db_name list option -> tactic
 
-val pr_autotactic : auto_tactic -> Pp.std_ppcmds
+val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
 
-(*s The following is not yet up to date -- Papageno. *)
+(** {6 The following is not yet up to date -- Papageno. } *)
 
-(* DAuto *)
-val dauto : int option * int option -> constr list -> tactic
+(** DAuto *)
+val dauto : int option * int option -> open_constr list -> tactic
 val default_search_decomp : int ref
 val default_dauto : tactic
 
-val h_dauto : int option * int option -> constr list -> tactic
-(* SuperAuto *)
+val h_dauto : int option * int option -> open_constr list -> tactic
+
+(** SuperAuto *)
 
 type autoArguments =
   | UsingTDB
@@ -241,4 +275,4 @@ val superauto : int -> (identifier * constr) list -> autoArguments list -> tacti
 
 val h_superauto : int option -> reference list -> bool -> bool -> tactic
 
-val auto_init : (unit -> unit) ref
+val add_auto_init : (unit -> unit) -> unit