[api] Relocate `intf` modules according to dependency-order.

In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.

We move all the files in `intf` to the lowest place their dependencies
can accommodate:

- `Misctypes`: is used by Declaremod, thus it has to go in `library`
  or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
  proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
  also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
  the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
  could be fixed, as this module should be declared in `interp` which
  is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
  as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.

Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...

1 files changed, 153 insertions, 0 deletions

diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
new file mode 100644
index 000000000..fda31756a
--- /dev/null
+++ b/pretyping/constrexpr.ml
@@ -0,0 +1,153 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Libnames
+open Misctypes
+open Decl_kinds
+
+(** {6 Concrete syntax for terms } *)
+
+(** [constr_expr] is the abstract syntax tree produced by the parser *)
+
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+
+type ident_decl = lident * universe_decl_expr option
+type name_decl = lname * universe_decl_expr option
+
+type notation = string
+
+type explicitation =
+  | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
+  | ExplByName of Id.t
+
+type binder_kind =
+  | Default of binding_kind
+  | Generalized of binding_kind * binding_kind * bool
+      (** Inner binding, outer bindings, typeclass-specific flag
+	 for implicit generalization of superclasses *)
+
+type abstraction_kind = AbsLambda | AbsPi
+
+type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
+
+(** Representation of integer literals that appear in Coq scripts.
+    We now use raw strings of digits in base 10 (big-endian), and a separate
+    sign flag. Note that this representation is not unique, due to possible
+    multiple leading zeros, and -0 = +0 *)
+
+type sign = bool
+type raw_natural_number = string
+
+type prim_token =
+  | Numeral of raw_natural_number * sign
+  | String of string
+
+type instance_expr = Misctypes.glob_level list
+
+type cases_pattern_expr_r =
+  | CPatAlias of cases_pattern_expr * lname
+  | CPatCstr  of reference
+    * cases_pattern_expr list option * cases_pattern_expr list
+  (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *)
+  | CPatAtom of reference option
+  | CPatOr   of cases_pattern_expr list
+  | CPatNotation of notation * cases_pattern_notation_substitution
+    * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
+				  (notation n applied with substitution l1)
+				  applied to arguments l2 *)
+  | CPatPrim   of prim_token
+  | CPatRecord of (reference * cases_pattern_expr) list
+  | CPatDelimiters of string * cases_pattern_expr
+  | CPatCast   of cases_pattern_expr * constr_expr
+and cases_pattern_expr = cases_pattern_expr_r CAst.t
+
+and cases_pattern_notation_substitution =
+    cases_pattern_expr list *     (** for constr subterms *)
+    cases_pattern_expr list list  (** for recursive notations *)
+
+and constr_expr_r =
+  | CRef     of reference * instance_expr option
+  | CFix     of lident * fix_expr list
+  | CCoFix   of lident * cofix_expr list
+  | CProdN   of local_binder_expr list * constr_expr
+  | CLambdaN of local_binder_expr list * constr_expr
+  | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
+  | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
+  | CApp     of (proj_flag * constr_expr) *
+                (constr_expr * explicitation CAst.t option) list
+  | CRecord  of (reference * constr_expr) list
+
+  (* representation of the "let" and "match" constructs *)
+  | CCases of Constr.case_style   (* determines whether this value represents "let" or "match" construct *)
+            * constr_expr option  (* return-clause *)
+            * case_expr list
+            * branch_expr list    (* branches *)
+
+  | CLetTuple of lname list * (lname option * constr_expr option) *
+                 constr_expr * constr_expr
+  | CIf of constr_expr * (lname option * constr_expr option)
+         * constr_expr * constr_expr
+  | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
+  | CPatVar of patvar
+  | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
+  | CSort   of glob_sort
+  | CCast   of constr_expr * constr_expr cast_type
+  | CNotation of notation * constr_notation_substitution
+  | CGeneralization of binding_kind * abstraction_kind option * constr_expr
+  | CPrim of prim_token
+  | CDelimiters of string * constr_expr
+  | CProj of reference * constr_expr
+and constr_expr = constr_expr_r CAst.t
+
+and case_expr = constr_expr                 (* expression that is being matched *)
+              * lname option                (* as-clause *)
+	      * cases_pattern_expr option   (* in-clause *)
+
+and branch_expr =
+  (cases_pattern_expr list list * constr_expr) CAst.t
+
+and fix_expr =
+    lident * (lident option * recursion_order_expr) *
+      local_binder_expr list * constr_expr * constr_expr
+
+and cofix_expr =
+    lident * local_binder_expr list * constr_expr * constr_expr
+
+and recursion_order_expr =
+  | CStructRec
+  | CWfRec of constr_expr
+  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+
+(* Anonymous defs allowed ?? *)
+and local_binder_expr =
+  | CLocalAssum   of lname list * binder_kind * constr_expr
+  | CLocalDef     of lname * constr_expr * constr_expr option
+  | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
+
+and constr_notation_substitution =
+    constr_expr list *      (** for constr subterms *)
+    constr_expr list list * (** for recursive notations *)
+    cases_pattern_expr list *   (** for binders *)
+    local_binder_expr list list (** for binder lists (recursive notations) *)
+
+type constr_pattern_expr = constr_expr
+
+(** Concrete syntax for modules and module types *)
+
+type with_declaration_ast =
+  | CWith_Module of Id.t list CAst.t * qualid CAst.t
+  | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
+
+type module_ast_r =
+  | CMident of qualid
+  | CMapply of module_ast * module_ast
+  | CMwith  of module_ast * with_declaration_ast
+and module_ast = module_ast_r CAst.t