diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.mli | 118 | ||||
| -rw-r--r-- | intf/notation_term.mli | 76 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 2 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
4 files changed, 197 insertions, 2 deletions
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 |