locus.mli for occurrences+clauses, misctypes.mli for various little things

 Corresponding operations in locusops.ml and miscops.ml

 The type of occurrences is now a clear algebraic one instead of
 a bool*list hard to understand.

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

4 files changed, 163 insertions, 5 deletions

diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 6ee6f707d8..d20bae0b55 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -8,9 +8,9 @@
 
 (** Informal mathematical status of declarations *)
 
-type locality =
-  | Local
-  | Global
+type locality = Local | Global
+
+type binding_kind = Explicit | Implicit
 
 type theorem_kind =
   | Theorem
diff --git a/intf/locus.mli b/intf/locus.mli
new file mode 100644
index 0000000000..b691175473
--- /dev/null
+++ b/intf/locus.mli
@@ -0,0 +1,88 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <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        *)
+(************************************************************************)
+
+open Names
+open Misctypes
+
+(** Locus : positions in hypotheses and goals *)
+
+(** {6 Occurrences} *)
+
+type 'a occurrences_gen =
+  | AllOccurrences
+  | AllOccurrencesBut of 'a list (** non-empty *)
+  | NoOccurrences
+  | OnlyOccurrences of 'a list (** non-empty *)
+
+type occurrences_expr = (int or_var) occurrences_gen
+type 'a with_occurrences = occurrences_expr * 'a
+
+type occurrences = int occurrences_gen
+
+
+(** {6 Locations}
+
+  Selecting the occurrences in body (if any), in type, or in both *)
+
+type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly
+
+
+(** {6 Abstract clauses expressions}
+
+  A [clause_expr] (and its instance [clause]) denotes occurrences and
+  hypotheses in a goal in an abstract way; in particular, it can refer
+  to the set of all hypotheses independently of the effective contents
+  of the current goal
+
+  Concerning the field [onhyps]:
+   - [None] means *on every hypothesis*
+   - [Some l] means on hypothesis belonging to l *)
+
+type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
+
+type 'id clause_expr =
+  { onhyps : 'id hyp_location_expr list option;
+    concl_occs : occurrences_expr }
+
+type clause = identifier clause_expr
+
+
+(** {6 Concrete view of occurrence clauses} *)
+
+(** [clause_atom] refers either to an hypothesis location (i.e. an
+   hypothesis with occurrences and a position, in body if any, in type
+   or in both) or to some occurrences of the conclusion *)
+
+type clause_atom =
+  | OnHyp of identifier * occurrences_expr * hyp_location_flag
+  | OnConcl of occurrences_expr
+
+(** A [concrete_clause] is an effective collection of occurrences
+    in the hypotheses and the conclusion *)
+
+type concrete_clause = clause_atom list
+
+
+(** {6 A weaker form of clause with no mention of occurrences} *)
+
+(** A [hyp_location] is an hypothesis together with a location *)
+
+type hyp_location = identifier * hyp_location_flag
+
+(** A [goal_location] is either an hypothesis (together with a location)
+    or the conclusion (represented by None) *)
+
+type goal_location = hyp_location option
+
+
+(** {6 Simple clauses, without occurrences nor location} *)
+
+(** A [simple_clause] is a set of hypotheses, possibly extended with
+   the conclusion (conclusion is represented by None) *)
+
+type simple_clause = identifier option list
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
new file mode 100644
index 0000000000..9d6820346d
--- /dev/null
+++ b/intf/misctypes.mli
@@ -0,0 +1,70 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <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        *)
+(************************************************************************)
+
+open Names
+open Libnames
+
+(** Basic types used both in [constr_expr] and in [glob_constr] *)
+
+(** Cases pattern variables *)
+
+type patvar = identifier
+
+(** Introduction patterns *)
+
+type intro_pattern_expr =
+  | IntroOrAndPattern of or_and_intro_pattern_expr
+  | IntroWildcard
+  | IntroRewrite of bool
+  | IntroIdentifier of identifier
+  | IntroFresh of identifier
+  | IntroForthcoming of bool
+  | IntroAnonymous
+and or_and_intro_pattern_expr = (Pp.loc * intro_pattern_expr) list list
+
+
+(** Sorts *)
+
+type glob_sort = GProp | GSet | GType of Univ.universe option
+
+(** Casts *)
+
+type 'a cast_type =
+  | CastConv of 'a
+  | CastVM of 'a
+  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+
+
+(** Bindings *)
+
+type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
+
+type 'a explicit_bindings = (Pp.loc * quantified_hypothesis * 'a) list
+
+type 'a bindings =
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_bindings
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a bindings
+
+
+(** Some utility types for parsing *)
+
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of Names.identifier Pp.located
+
+type 'a and_short_name = 'a * identifier Pp.located option
+
+type 'a or_by_notation =
+  | AN of 'a
+  | ByNotation of (Pp.loc * string * string option)
+
+(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
+   but this formulation avoids a useless dependency. *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 2384008060..fc3f949208 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -9,7 +9,7 @@
 open Pp
 open Names
 open Tacexpr
-open Genarg
+open Misctypes
 open Topconstr
 open Decl_kinds
 open Libnames
@@ -133,7 +133,7 @@ type option_ref_value =
   | StringRefValue of string
   | QualidRefValue of reference
 
-type sort_expr = Glob_term.glob_sort
+type sort_expr = glob_sort
 
 type definition_expr =
   | ProveBody of local_binder list * constr_expr