diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 43 |
1 files changed, 23 insertions, 20 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 97e11af6..22317b5f 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,v 1.47.2.5 2005/01/21 16:42:37 herbelin Exp $ i*) +(*i $Id: rawterm.mli 8624 2006-03-13 17:38:17Z msozeau $ i*) (*i*) open Util @@ -31,8 +31,6 @@ type patvar = identifier type rawsort = RProp of Term.contents | RType of Univ.universe option -type fix_kind = RFix of (int array * int) | RCoFix of int - type binder_kind = BProd | BLambda | BLetIn type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier @@ -46,14 +44,6 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings -type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) - | BinderType of name - | QuestionMark - | CasesType - | InternalHole - | TomatchTypeParameter of inductive * int - type rawconstr = | RRef of (loc * global_reference) | RVar of (loc * identifier) @@ -63,26 +53,27 @@ 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 option ref) * - (rawconstr * (name * (loc * inductive * name list) option) ref) list * + | RCases of loc * rawconstr option * + (rawconstr * (name * (loc * inductive * name list) option)) list * (loc * identifier list * cases_pattern list * rawconstr) list - | ROrderedCase of loc * case_style * rawconstr option * rawconstr * - rawconstr array * rawconstr option ref | RLetTuple of loc * name list * (name * rawconstr option) * rawconstr * rawconstr | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr | RRec of loc * fix_kind * identifier array * rawdecl list array * rawconstr array * rawconstr array | RSort of loc * rawsort - | RHole of (loc * hole_kind) - | RCast of loc * rawconstr * rawconstr + | RHole of (loc * Evd.hole_kind) + | RCast of loc * rawconstr * cast_kind * 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 + val cases_predicate_names : - (rawconstr * (name * (loc * inductive * name list) option) ref) list -> - name list + (rawconstr * (name * (loc * inductive * name list) option)) list -> 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 @@ -107,7 +98,18 @@ val occur_rawconstr : identifier -> rawconstr -> bool val loc_of_rawconstr : rawconstr -> loc -val subst_raw : Names.substitution -> rawconstr -> rawconstr +(**********************************************************************) +(* Conversion from rawconstr to cases pattern, if possible *) + +(* Take the current alias as parameter, raise Not_found if *) +(* translation is impossible *) + +val cases_pattern_of_rawconstr : name -> rawconstr -> cases_pattern + +val rawconstr_of_closed_cases_pattern : cases_pattern -> name * rawconstr + +(**********************************************************************) +(* Reduction expressions *) type 'a raw_red_flag = { rBeta : bool; @@ -131,6 +133,7 @@ type ('a,'b) red_expr_gen = | Fold of 'a list | Pattern of 'a occurrences list | ExtraRedExpr of string + | CbvVm type ('a,'b) may_eval = | ConstrTerm of 'a |