diff options
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 74 |
1 files changed, 51 insertions, 23 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 3c359bd5..d4fef0dc 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 9976 2007-07-12 11:58:30Z msozeau $ i*) +(*i $Id: topconstr.mli 11024 2008-05-30 12:41:39Z msozeau $ i*) (*i*) open Pp @@ -33,11 +33,14 @@ type aconstr = | ALambda of name * aconstr * aconstr | AProd of name * aconstr * aconstr | ALetIn of name * aconstr * aconstr - | ACases of aconstr option * + | ACases of case_style * aconstr option * (aconstr * (name * (inductive * int * 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 rawsort | AHole of Evd.hole_kind | APatVar of patvar @@ -65,11 +68,6 @@ val rawconstr_of_aconstr_with_binders : loc -> val rawconstr_of_aconstr : loc -> aconstr -> rawconstr (**********************************************************************) -(* Substitution of kernel names, avoiding a list of bound identifiers *) - -val subst_aconstr : substitution -> identifier list -> aconstr -> aconstr - -(**********************************************************************) (* [match_aconstr metas] matches a rawconstr against an aconstr with *) (* metavariables in [metas]; raise [No_match] if the matching fails *) @@ -86,11 +84,18 @@ val match_aconstr : rawconstr -> interpretation -> (rawconstr * (tmp_scope_name option * scope_name list)) list (**********************************************************************) +(* Substitution of kernel names in interpretation data *) + +val subst_interpretation : substitution -> interpretation -> interpretation + +(**********************************************************************) (*s Concrete syntax for terms *) type notation = string -type explicitation = ExplByPos of int | ExplByName of identifier +type explicitation = ExplByPos of int * identifier option | ExplByName of identifier + +type binder_kind = Default of binding_kind | TypeClass of binding_kind type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) @@ -110,22 +115,22 @@ type constr_expr = | CFix of loc * identifier located * fixpoint_expr list | CCoFix of loc * identifier located * cofixpoint_expr list | CArrow of loc * constr_expr * constr_expr - | CProdN of loc * (name located list * constr_expr) list * constr_expr - | CLambdaN of loc * (name located list * constr_expr) list * constr_expr + | 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 - | CCases of loc * constr_expr option * + (constr_expr * explicitation located option) list + | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * - (loc * cases_pattern_expr list list * constr_expr) list + (loc * cases_pattern_expr list located list * 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) * constr_expr * constr_expr - | CHole of loc + | CHole of loc * Evd.hole_kind option | CPatVar of loc * (bool * patvar) - | CEvar of loc * existential_key + | CEvar of loc * existential_key * constr_expr list option | CSort of loc * rawsort | CCast of loc * constr_expr * constr_expr cast_type | CNotation of loc * notation * constr_expr list @@ -134,19 +139,24 @@ type constr_expr = | CDynamic of loc * Dyn.t and fixpoint_expr = - identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr + identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr and cofixpoint_expr = - identifier * local_binder list * constr_expr * constr_expr + identifier located * local_binder list * constr_expr * constr_expr and recursion_order_expr = | CStructRec | CWfRec of constr_expr | CMeasureRec of constr_expr +(** Anonymous defs allowed ?? *) and local_binder = | LocalRawDef of name located * constr_expr - | LocalRawAssum of name located list * constr_expr + | LocalRawAssum of name located list * binder_kind * constr_expr + +type typeclass_constraint = name located * binding_kind * constr_expr + +and typeclass_context = typeclass_constraint list (**********************************************************************) (* Utilities on constr_expr *) @@ -161,6 +171,8 @@ val replace_vars_constr_expr : val free_vars_of_constr_expr : constr_expr -> Idset.t val occur_var_constr_expr : identifier -> constr_expr -> bool +val default_binder_kind : binder_kind + (* Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : constr_expr -> identifier list @@ -168,15 +180,19 @@ 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 cast_type -> constr_expr -val mkLambdaC : name located list * constr_expr * constr_expr -> constr_expr +val mkLambdaC : name located list * binder_kind * 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 mkProdC : name located list * binder_kind * 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 +(* Same as [abstract_constr_expr] and [prod_constr_expr], with location *) +val mkCLambdaN : loc -> local_binder list -> constr_expr -> constr_expr +val mkCProdN : loc -> local_binder list -> constr_expr -> constr_expr + (* For binders parsing *) (* Includes let binders *) @@ -191,6 +207,11 @@ 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 typeclasses *) + +val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) -> + ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b + (* 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)] *) @@ -205,10 +226,17 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr -type module_type_ast = - | CMTEident of qualid located - | CMTEwith of module_type_ast * with_declaration_ast type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast + +type module_type_ast = + | CMTEident of qualid located + | CMTEapply of module_type_ast * module_ast + | CMTEwith of module_type_ast * with_declaration_ast + +type include_ast = + | CIMTE of module_type_ast + | CIME of module_ast + |