diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 39 |
1 files changed, 26 insertions, 13 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 22317b5f..b29cc7b6 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: rawterm.mli 8624 2006-03-13 17:38:17Z msozeau $ i*) +(*i $Id: rawterm.mli 8878 2006-05-30 16:44:25Z herbelin $ i*) (*i*) open Util @@ -44,6 +44,10 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings +type cast_type = + | CastConv of cast_kind + | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *) + type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -53,9 +57,7 @@ type rawconstr = | RLambda of loc * name * rawconstr * rawconstr | RProd of loc * name * rawconstr * rawconstr | RLetIn of loc * name * rawconstr * rawconstr - | RCases of loc * rawconstr option * - (rawconstr * (name * (loc * inductive * name list) option)) list * - (loc * identifier list * cases_pattern list * rawconstr) list + | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr @@ -63,17 +65,26 @@ type rawconstr = rawconstr array * rawconstr array | RSort of loc * rawsort | RHole of (loc * Evd.hole_kind) - | RCast of loc * rawconstr * cast_kind * rawconstr + | RCast of loc * rawconstr * cast_type * rawconstr | RDynamic of loc * Dyn.t and rawdecl = name * rawconstr option * rawconstr and fix_recursion_order = RStructRec | RWfRec of rawconstr -and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int +and fix_kind = + | RFix of ((int option * fix_recursion_order) array * int) + | RCoFix of int + +and predicate_pattern = + name * (loc * inductive * int * name list) option + +and tomatch_tuple = (rawconstr * predicate_pattern) list -val cases_predicate_names : - (rawconstr * (name * (loc * inductive * name list) option)) list -> name list +and cases_clauses = + (loc * identifier list * cases_pattern list * rawconstr) list + +val cases_predicate_names : tomatch_tuple -> name list (*i - if PRec (_, names, arities, bodies) is in env then arities are typed in env too and bodies are typed in env enriched by the @@ -121,22 +132,24 @@ type 'a raw_red_flag = { val all_flags : 'a raw_red_flag -type 'a occurrences = int list * 'a +type 'a or_var = ArgArg of 'a | ArgVar of identifier located + +type 'a with_occurrences = int or_var list * 'a type ('a,'b) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a occurrences option + | Simpl of 'a with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag - | Unfold of 'b occurrences list + | Unfold of 'b with_occurrences list | Fold of 'a list - | Pattern of 'a occurrences list + | Pattern of 'a with_occurrences list | ExtraRedExpr of string | CbvVm type ('a,'b) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a, 'b) red_expr_gen * 'a + | ConstrEval of ('a,'b) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a |