From 392300a73bc4e57d2be865d9a8d77c608ef02f59 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:50 +0000
Subject: 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
---
 intf/constrexpr.mli    | 118 +++++++++++++++++++++++++++++++++++++++++++++++++
 intf/notation_term.mli |  76 +++++++++++++++++++++++++++++++
 intf/tacexpr.mli       |   2 +-
 intf/vernacexpr.mli    |   3 +-
 4 files changed, 197 insertions(+), 2 deletions(-)
 create mode 100644 intf/constrexpr.mli
 create mode 100644 intf/notation_term.mli

(limited to 'intf')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
new file mode 100644
index 0000000000..f6d274abb6
--- /dev/null
+++ b/intf/constrexpr.mli
@@ -0,0 +1,118 @@
+(************************************************************************)
+(*  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 Pp
+open Names
+open Libnames
+open Term
+open Misctypes
+open Decl_kinds
+
+(** {6 Concrete syntax for terms } *)
+
+(** [constr_expr] is the abstract syntax tree produced by the parser *)
+
+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
+
+(** 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
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
new file mode 100644
index 0000000000..2485fd7a69
--- /dev/null
+++ b/intf/notation_term.mli
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  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 Term
+open Libnames
+open Misctypes
+open Glob_term
+
+(** [notation_constr] *)
+
+(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
+    extensions (i.e. notations).
+    No location since intended to be substituted at any place of a text.
+    Complex expressions such as fixpoints and cofixpoints are excluded,
+    as well as non global expressions such as existential variables. *)
+
+type notation_constr =
+  (** Part common to [glob_constr] and [cases_pattern] *)
+  | NRef of global_reference
+  | NVar of identifier
+  | NApp of notation_constr * notation_constr list
+  | NHole of Evar_kinds.t
+  | NList of identifier * identifier * notation_constr * notation_constr * bool
+  (** Part only in [glob_constr] *)
+  | NLambda of name * notation_constr * notation_constr
+  | NProd of name * notation_constr * notation_constr
+  | NBinderList of identifier * identifier * notation_constr * notation_constr
+  | NLetIn of name * notation_constr * notation_constr
+  | NCases of case_style * notation_constr option *
+      (notation_constr * (name * (inductive * name list) option)) list *
+      (cases_pattern list * notation_constr) list
+  | NLetTuple of name list * (name * notation_constr option) *
+      notation_constr * notation_constr
+  | NIf of notation_constr * (name * notation_constr option) *
+      notation_constr * notation_constr
+  | NRec of fix_kind * identifier array *
+      (name * notation_constr option * notation_constr) list array *
+      notation_constr array * notation_constr array
+  | NSort of glob_sort
+  | NPatVar of patvar
+  | NCast of notation_constr * notation_constr cast_type
+
+(** Note concerning NList: first constr is iterator, second is terminator;
+    first id is where each argument of the list has to be substituted
+    in iterator and snd id is alternative name just for printing;
+    boolean is associativity *)
+
+(** Types concerning notations *)
+
+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 notation_constr: 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 notation_constr:
+    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 *
+    notation_constr
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d8e340d1e8..e70fc13086 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Names
-open Topconstr
+open Constrexpr
 open Libnames
 open Nametab
 open Genredexpr
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index fc3f949208..3223e80b87 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -10,7 +10,8 @@ open Pp
 open Names
 open Tacexpr
 open Misctypes
-open Topconstr
+open Constrexpr
+open Notation_term
 open Decl_kinds
 open Libnames
 
-- 
cgit v1.2.3