New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr

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

1 files changed, 15 insertions, 160 deletions

diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 101c39eea..760ee14a5 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -15,66 +15,17 @@ open Term
 open Mod_subst
 open Misctypes
 open Decl_kinds
+open Constrexpr
+open Notation_term
 
-(** Topconstr: definitions of [aconstr] et [constr_expr] *)
-
-(** {6 aconstr } *)
-(** This is the subtype of glob_constr allowed in syntactic extensions 
-   No location since intended to be substituted at any place of a text 
-   Complex expressions such as fixpoints and cofixpoints are excluded, 
-   non global expressions such as existential variables also *)
-
-type aconstr =
-  (** Part common to [glob_constr] and [cases_pattern] *)
-  | ARef of global_reference
-  | AVar of identifier
-  | AApp of aconstr * aconstr list
-  | AHole of Evar_kinds.t
-  | AList of identifier * identifier * aconstr * aconstr * bool
-  (** Part only in [glob_constr] *)
-  | ALambda of name * aconstr * aconstr
-  | AProd of name * aconstr * aconstr
-  | ABinderList of identifier * identifier * aconstr * aconstr
-  | ALetIn of name * aconstr * aconstr
-  | ACases of case_style * aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
-      (cases_pattern list * aconstr) list
-  | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
-  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
-  | ARec of fix_kind * identifier array *
-      (name * aconstr option * aconstr) list array * aconstr array *
-      aconstr array
-  | ASort of glob_sort
-  | APatVar of patvar
-  | ACast of aconstr * aconstr cast_type
-
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-(** Type of the meta-variables of an aconstr: in a recursive pattern x..y,
-    x carries the sequence of objects bound to the list x..y  *)
-type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
-
-(** Type of variables when interpreting a constr_expr as an aconstr:
-    in a recursive pattern x..y, both x and y carry the individual type
-    of each element of the list x..y *)
-type notation_var_internalization_type =
-  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
-
-(** This characterizes to what a notation is interpreted to *)
-type interpretation =
-    (identifier * (subscopes * notation_var_instance_type)) list * aconstr
+(** Topconstr *)
 
 (** Translate a glob_constr into a notation given the list of variables
     bound by the notation; also interpret recursive patterns           *)
 
-val aconstr_of_glob_constr :
+val notation_constr_of_glob_constr :
   (identifier * notation_var_internalization_type) list ->
-  (identifier * identifier) list -> glob_constr -> aconstr
+  (identifier * identifier) list -> glob_constr -> notation_constr
 
 (** Name of the special identifier used to encode recursive notations  *)
 val ldots_var : identifier
@@ -84,23 +35,26 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool
 
 (** Re-interpret a notation as a glob_constr, taking care of binders     *)
 
-val glob_constr_of_aconstr_with_binders : loc ->
+val glob_constr_of_notation_constr_with_binders : loc ->
   ('a -> name -> 'a * name) ->
-  ('a -> aconstr -> glob_constr) -> 'a -> aconstr -> glob_constr
+  ('a -> notation_constr -> glob_constr) ->
+  'a -> notation_constr -> glob_constr
 
-val glob_constr_of_aconstr : loc -> aconstr -> glob_constr
+val glob_constr_of_notation_constr : loc -> notation_constr -> glob_constr
 
-(** [match_aconstr] matches a glob_constr against a notation interpretation;
+(** [match_notation_constr] matches a glob_constr against a notation interpretation;
     raise [No_match] if the matching fails   *)
 
 exception No_match
 
-val match_aconstr : bool -> glob_constr -> interpretation ->
+val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
       (glob_decl list * subscopes) list
 
-val match_aconstr_cases_pattern :  cases_pattern -> interpretation ->
-      ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
+val match_notation_constr_cases_pattern :
+  cases_pattern -> interpretation ->
+  ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
+    (cases_pattern list)
 
 val match_aconstr_ind_pattern : inductive -> cases_pattern  list -> interpretation ->
       ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
@@ -109,94 +63,6 @@ val match_aconstr_ind_pattern : inductive -> cases_pattern  list -> interpretati
 
 val subst_interpretation : substitution -> interpretation -> interpretation
 
-(** {6 Concrete syntax for terms }                                        *)
-
-type notation = string
-
-type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-
-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 *)
-
-type prim_token = Numeral of Bigint.bigint | String of string
-
-type cases_pattern_expr =
-  | CPatAlias of loc * cases_pattern_expr * identifier
-  | CPatCstr of loc * reference * cases_pattern_expr list
-  | CPatCstrExpl of loc * reference * cases_pattern_expr list
-  | CPatAtom of loc * reference option
-  | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_notation_substitution
-  | CPatPrim of loc * prim_token
-  | CPatRecord of loc * (reference * cases_pattern_expr) list
-  | CPatDelimiters of loc * string * cases_pattern_expr
-
-and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
-
-type constr_expr =
-  | CRef of reference
-  | CFix of loc * identifier located * fix_expr list
-  | CCoFix of loc * identifier located * cofix_expr list
-  | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLetIn of loc * name located * constr_expr * constr_expr
-  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
-  | CApp of loc * (proj_flag * constr_expr) *
-      (constr_expr * explicitation located option) list
-  | CRecord of loc * constr_expr option * (reference * constr_expr) list
-  | CCases of loc * case_style * constr_expr option *
-      (constr_expr * (name located option * cases_pattern_expr option)) list *
-      (loc * cases_pattern_expr list located list * constr_expr) list
-  | CLetTuple of loc * name located list * (name located option * constr_expr option) *
-      constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name located option * constr_expr option)
-      * constr_expr * constr_expr
-  | CHole of loc * Evar_kinds.t option
-  | CPatVar of loc * (bool * patvar)
-  | CEvar of loc * existential_key * constr_expr list option
-  | CSort of loc * glob_sort
-  | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_notation_substitution
-  | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
-  | CPrim of loc * prim_token
-  | CDelimiters of loc * string * constr_expr
-
-and fix_expr =
-    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
-
-and cofix_expr =
-    identifier located * local_binder 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 =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * binder_kind * constr_expr
-
-and constr_notation_substitution =
-    constr_expr list *      (** for constr subterms *)
-    constr_expr list list * (** for recursive notations *)
-    local_binder list list (** for binders subexpressions *)
-
-type typeclass_constraint = name located * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
-type constr_pattern_expr = constr_expr
-
 val oldfashion_patterns : bool ref
 
 (** Utilities on constr_expr                                           *)
@@ -259,17 +125,6 @@ val map_constr_expr_with_binders :
   (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
       'a -> constr_expr -> constr_expr
 
-(** Concrete syntax for modules and module types                       *)
-
-type with_declaration_ast =
-  | CWith_Module of identifier list located * qualid located
-  | CWith_Definition of identifier list located * constr_expr
-
-type module_ast =
-  | CMident of qualid located
-  | CMapply of loc * module_ast * module_ast
-  | CMwith of loc * module_ast * with_declaration_ast
-
 val ntn_loc :
   loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :