diff options
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 51 |
1 files changed, 34 insertions, 17 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 54547352..2f4f667d 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: topconstr.mli,v 1.23.2.3 2005/01/21 17:14:10 herbelin Exp $ i*) +(*i $Id: topconstr.mli 8624 2006-03-13 17:38:17Z msozeau $ i*) (*i*) open Pp @@ -15,6 +15,7 @@ open Names open Libnames open Rawterm open Term +open Mod_subst (*i*) (*s This is the subtype of rawconstr allowed in syntactic extensions *) @@ -32,25 +33,28 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * aconstr option * + | ACases of aconstr option * (aconstr * (name * (inductive * name list) option)) list * (identifier list * cases_pattern list * aconstr) list - | AOrderedCase of case_style * aconstr option * aconstr * aconstr array | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr | AIf of aconstr * (name * aconstr option) * aconstr * aconstr | ASort of rawsort - | AHole of hole_kind + | AHole of Evd.hole_kind | APatVar of patvar - | ACast of aconstr * aconstr + | ACast of aconstr * cast_kind * aconstr val rawconstr_of_aconstr_with_binders : loc -> (identifier -> 'a -> identifier * 'a) -> ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr -val subst_aconstr : Names.substitution -> aconstr -> aconstr +val rawconstr_of_aconstr : loc -> aconstr -> rawconstr + +val subst_aconstr : substitution -> Names.identifier list -> aconstr -> aconstr val aconstr_of_rawconstr : identifier list -> rawconstr -> aconstr +val eq_rawconstr : rawconstr -> rawconstr -> bool + (* [match_aconstr metas] match a rawconstr against an aconstr with metavariables in [metas]; it raises [No_match] if the matching fails *) exception No_match @@ -59,7 +63,7 @@ type scope_name = string type interpretation = (identifier * (scope_name option * scope_name list)) list * aconstr -val match_aconstr : (*i scope_name option -> i*) rawconstr -> interpretation -> +val match_aconstr : rawconstr -> interpretation -> (rawconstr * (scope_name option * scope_name list)) list (*s Concrete syntax for terms *) @@ -70,12 +74,15 @@ type explicitation = ExplByPos of int | ExplByName of identifier 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 | CPatAtom of loc * reference option + | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_expr list - | CPatNumeral of loc * Bignat.bigint + | CPatPrim of loc * prim_token | CPatDelimiters of loc * string * cases_pattern_expr type constr_expr = @@ -89,11 +96,9 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CCases of loc * (constr_expr option * constr_expr option) * + | CCases of loc * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list * constr_expr) list - | COrderedCase of loc * case_style * constr_expr option * constr_expr - * constr_expr list | CLetTuple of loc * name list * (name option * constr_expr option) * constr_expr * constr_expr | CIf of loc * constr_expr * (name option * constr_expr option) @@ -102,18 +107,22 @@ type constr_expr = | CPatVar of loc * (bool * patvar) | CEvar of loc * existential_key | CSort of loc * rawsort - | CCast of loc * constr_expr * constr_expr + | CCast of loc * constr_expr * cast_kind * constr_expr | CNotation of loc * notation * constr_expr list - | CNumeral of loc * Bignat.bigint + | CPrim of loc * prim_token | CDelimiters of loc * string * constr_expr | CDynamic of loc * Dyn.t and fixpoint_expr = - identifier * int * local_binder list * constr_expr * constr_expr + identifier * (int * recursion_order_expr) * local_binder list * constr_expr * constr_expr and cofixpoint_expr = identifier * local_binder list * constr_expr * constr_expr +and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + and local_binder = | LocalRawDef of name located * constr_expr | LocalRawAssum of name located list * constr_expr @@ -134,11 +143,16 @@ val names_of_cases_indtype : constr_expr -> identifier list val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr -val mkCastC : constr_expr * constr_expr -> constr_expr +val mkCastC : constr_expr * cast_kind * constr_expr -> constr_expr val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * constr_expr * constr_expr -> constr_expr +val coerce_to_id : constr_expr -> identifier located + +val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr +val prod_constr_expr : constr_expr -> local_binder list -> constr_expr + (* For binders parsing *) (* Includes let binders *) @@ -147,6 +161,9 @@ val local_binders_length : local_binder list -> int (* Does not take let binders into account *) val names_of_local_assums : local_binder list -> name located list +(* With let binders *) +val names_of_local_binders : local_binder list -> name located list + (* Used in correctness and interface; absence of var capture not guaranteed *) (* in pattern-matching clauses and in binders of the form [x,y:T(x)] *) @@ -157,8 +174,8 @@ val map_constr_expr_with_binders : (* Concrete syntax for modules and modules types *) type with_declaration_ast = - | CWith_Module of identifier located * qualid located - | CWith_Definition of identifier located * constr_expr + | CWith_Module of identifier list located * qualid located + | CWith_Definition of identifier list located * constr_expr type module_type_ast = | CMTEident of qualid located |