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, 118 insertions, 0 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
new file mode 100644
index 000000000..f6d274abb
--- /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