diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 11 | ||||
| -rw-r--r-- | kernel/environ.ml | 6 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 | ||||
| -rw-r--r-- | kernel/instantiate.ml | 4 | ||||
| -rw-r--r-- | kernel/instantiate.mli | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 194 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/term.ml | 104 | ||||
| -rw-r--r-- | kernel/term.mli | 30 | ||||
| -rw-r--r-- | kernel/typeops.ml | 5 |
10 files changed, 186 insertions, 180 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 948361690d..178e5a9de7 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -144,7 +144,7 @@ let const_value_cache info c = try Some (Hashtbl.find info.i_tab c) with Not_found -> - match const_abst_opt_value info.i_env info.i_evc c with + match const_evar_opt_value info.i_env info.i_evc c with | Some body -> let v = info.i_repr info body in Hashtbl.add info.i_tab c v; @@ -450,7 +450,6 @@ let rec norm_head info env t stack = (VAL(0, mkProd (x, cbv_norm_term info env t, cbv_norm_term info (subs_lift env) c)), stack) - | IsAbst (_,_) -> failwith "No longer implemented" (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak @@ -519,8 +518,8 @@ and apply_stack info t = function apply_stack info (applistc t (List.map (cbv_norm_value info) args)) st | CASE (ty,br,ci,env,st) -> apply_stack info - (mkMutCaseA ci (cbv_norm_term info env ty) t - (Array.map (cbv_norm_term info env) br)) + (mkMutCase (ci, cbv_norm_term info env ty, t, + Array.map (cbv_norm_term info env) br)) st @@ -883,7 +882,7 @@ and whnf_frterm info ft = { norm = uf.norm; term = FLIFT(k, uf) } | FOP2 (Cast,f,_) -> whnf_frterm info f (* remove outer casts *) | FOPN (AppL,appl) -> whnf_apply info appl.(0) (array_tl appl) - | FOPN ((Const _ | Evar _ | Abst _) as op,vars) -> + | FOPN ((Const _ | Evar _) as op,vars) -> if red_under info.i_flags (DELTA op) then let cst = DOPN(op, Array.map term_of_freeze vars) in (match const_value_cache info cst with @@ -953,7 +952,7 @@ and whnf_term info env t = | DOP1 (op, nt) -> { norm = false; term = FOP1 (op, freeze env nt) } | DOP2 (Cast,ct,c) -> whnf_term info env ct (* remove outer casts *) | DOP2 (_,_,_) -> assert false (* Lambda|Prod made explicit *) - | DOPN ((AppL | Const _ | Evar _ | Abst _ | MutCase _) as op, ve) -> + | DOPN ((AppL | Const _ | Evar _ | MutCase _) as op, ve) -> whnf_frterm info { norm = false; term = FOPN (op, freeze_vect env ve) } | DOPN ((MutInd _ | MutConstruct _) as op,v) -> { norm = (v=[||]); term = FOPN (op, freeze_vect env v) } diff --git a/kernel/environ.ml b/kernel/environ.ml index 4909e4444f..604d0aea36 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -262,7 +262,7 @@ let hdchar env c = | IsCoFix (i,(_,ln,_)) -> let id = match List.nth ln i with Name id -> id | _ -> assert false in lowercase_first_char id - | IsMeta _|IsXtra _|IsAbst (_, _)|IsEvar _|IsMutCase (_, _, _, _) -> "y" + | IsMeta _|IsXtra _|IsEvar _|IsMutCase (_, _, _, _) -> "y" in hdrec 0 c @@ -311,7 +311,7 @@ let make_all_name_different env = env (* Abstractions. *) - +(* let evaluable_abst env = function | DOPN (Abst _,_) -> true | _ -> invalid_arg "evaluable_abst" @@ -324,7 +324,7 @@ let abst_value env = function | DOPN(Abst sp, args) -> contract_abstraction (lookup_abst sp env) args | _ -> invalid_arg "abst_value" - +*) let defined_constant env = function | DOPN (Const sp, _) -> is_defined (lookup_constant sp env) | _ -> invalid_arg "defined_constant" diff --git a/kernel/environ.mli b/kernel/environ.mli index b99410bd3b..4b483c7dd9 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -144,11 +144,11 @@ val it_mkNamedProd_or_LetIn : constr -> var_context -> constr val lambda_create : env -> constr * constr -> constr val prod_create : env -> constr * constr -> constr - +(* val translucent_abst : env -> constr -> bool val evaluable_abst : env -> constr -> bool val abst_value : env -> constr -> constr - +*) val defined_constant : env -> constr -> bool val evaluable_constant : env -> constr -> bool diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 627f0d45c1..9b1d9289a5 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -72,7 +72,7 @@ let existential_value sigma (n,args) = | Evar_empty -> anomaly "a defined existential with no body" -let const_abst_opt_value env sigma c = +let const_evar_opt_value env sigma c = match c with | DOPN(Const sp,_) -> if evaluable_constant env c then Some (constant_value env c) else None @@ -81,7 +81,5 @@ let const_abst_opt_value env sigma c = Some (existential_value sigma (ev,args)) else None - | DOPN(Abst sp,_) -> - if evaluable_abst env c then Some (abst_value env c) else None | _ -> invalid_arg "const_abst_opt_value" diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index d3454f1ccc..0d8c2a3039 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -27,4 +27,4 @@ val constant_type : env -> 'a evar_map -> constant -> typed_type val existential_value : 'a evar_map -> existential -> constr val existential_type : 'a evar_map -> existential -> constr -val const_abst_opt_value : env -> 'a evar_map -> constr -> constr option +val const_evar_opt_value : env -> 'a evar_map -> constr -> constr option diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f0f7945d6e..352e41e382 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -25,7 +25,7 @@ type 'a contextual_stack_reduction_function = type 'a stack_reduction_function = 'a contextual_stack_reduction_function type local_stack_reduction_function = constr -> constr list -> constr * constr list - +(* type stack = | EmptyStack | ConsStack of constr array * int * stack @@ -36,6 +36,15 @@ let decomp_stack = function Some (v.(n), (if n+1 = Array.length v then s else ConsStack (v, n+1, s))) let append_stack v s = if Array.length v = 0 then s else ConsStack (v,0,s) +*) + +type stack = constr list + +let decomp_stack = function + | [] -> None + | v :: s -> Some (v,s) + +let append_stack v s = v@s (*************************************) (*** Reduction Functions Operators ***) @@ -160,7 +169,6 @@ let red_product env sigma c = | IsConst (_,_) when evaluable_constant env x -> constant_value env x | IsEvar (ev,args) when Evd.is_defined sigma ev -> existential_value sigma (ev,args) - | IsAbst (_,_) when evaluable_abst env x -> abst_value env x | IsCast (c,_) -> redrec c | IsProd (x,a,b) -> mkProd (x, a, redrec b) | _ -> error "Term not reducible" @@ -182,12 +190,6 @@ let rec substlin env name n ol c = else ((n+1),ol,c) - | IsAbst (_,_) when path_of_abst c = name -> - if List.hd ol = n then - (n+1, List.tl ol, abst_value env c) - else - (n+1,ol,c) - (* INEFFICIENT: OPTIMIZE *) | IsAppL (c1,cl) -> List.fold_left @@ -236,14 +238,14 @@ let rec substlin env name n ol c = in let (n1,ol1,p') = substlin env name n ol p in (* ATTENTION ERREUR *) (match ol1 with (* si P pas affiche *) - | [] -> (n1,[],mkMutCaseA ci p' d llf) + | [] -> (n1,[],mkMutCase (ci, p', d, llf)) | _ -> let (n2,ol2,d') = substlin env name n1 ol1 d in (match ol2 with - | [] -> (n2,[],mkMutCaseA ci p' d' llf) + | [] -> (n2,[],mkMutCase (ci, p', d', llf)) | _ -> let (n3,ol3,lf') = substlist n2 ol2 (Array.to_list llf) - in (n3,ol3,mkMutCase (ci, p', d', lf')))) + in (n3,ol3,mkMutCaseL (ci, p', d', lf')))) | IsCast (c1,c2) -> let (n1,ol1,c1') = substlin env name n ol c1 in @@ -260,14 +262,13 @@ let rec substlin env name n ol c = (warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ - |IsAbst (_, _)|IsEvar _|IsConst _ - |IsMutInd _|IsMutConstruct _) -> (n,ol,c) + |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c) let unfold env sigma name = let flag = (UNIFORM,{ r_beta = true; - r_delta = (fun op -> op=(Const name) or op=(Abst name)); + r_delta = (fun op -> op=(Const name)); r_iota = true }) in clos_norm_flags flag env sigma @@ -336,9 +337,9 @@ let beta_applist (c,l) = stacklam applist [] c l let whd_beta_stack x stack = let rec whrec (x, stack as s) = match x with | CLam (name,c1,c2) -> - (match stack with - | [] -> (x,[]) - | a1::rest -> stacklam whrec [a1] c2 rest) + (match decomp_stack stack with + | None -> (x,[]) + | Some (a1,rest) -> stacklam whrec [a1] c2 rest) | DOPN(AppL,cl) -> whrec (array_hd cl, array_app_tl cl stack) | DOP2(Cast,c,_) -> whrec (c, stack) @@ -362,15 +363,6 @@ let whd_const_stack namelist env sigma = else x,l - | (DOPN(Abst sp,_)) as c -> - if List.mem sp namelist then - if evaluable_abst env c then - whrec (abst_value env c) l - else - error "whd_const_stack" - else - x,l - | DOP2(Cast,c,_) -> whrec c l | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) | x -> x,l @@ -393,14 +385,9 @@ let whd_delta_stack env sigma = whrec (existential_value sigma (ev,args)) l else x,l - | (DOPN(Abst _,_)) as c -> - if evaluable_abst env c then - whrec (abst_value env c) l - else - x,l - | DOP2(Cast,c,_) -> whrec c l - | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) - | x -> x,l + | DOP2(Cast,c,_) -> whrec c l + | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l) + | x -> x,l in whrec @@ -420,19 +407,12 @@ let whd_betadelta_stack env sigma x l = whrec (existential_value sigma (ev,args), l) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) l - else - (x,l) -*) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,cl) -> whrec (f, cl@l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) | IsLambda (_,_,c) -> - (match l with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack l with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | x -> s in whrec (x, l) @@ -448,19 +428,12 @@ let whd_betaevar_stack env sigma x l = whrec (existential_value sigma (ev,args), l) else s -(* - | DOPN(Abst _,_) -> - if translucent_abst env x then - whrec (abst_value env x) l - else - (x,l) -*) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,cl) -> whrec (f, cl@l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) | IsLambda (_,_,c) -> - (match l with - | [] -> (x,l) - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack l with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | x -> s in whrec (x, l) @@ -480,18 +453,11 @@ let whd_betadeltaeta_stack env sigma x l = whrec (existential_value sigma (ev,args), l) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) l - else - (x,l) -*) | IsCast (c,_) -> whrec (c, l) - | IsAppL (f,cl) -> whrec (f, cl@l) + | IsAppL (f,cl) -> whrec (f, append_stack cl l) | IsLambda (_,_,c) -> - (match l with - | [] -> + (match decomp_stack l with + | None -> (match applist (whrec (c, [])) with | DOPN(AppL,cl) -> let napp = (Array.length cl) -1 in @@ -502,7 +468,7 @@ let whd_betadeltaeta_stack env sigma x l = in if noccurn 1 u then (pop u,[]) else s | _ -> s) | _ -> s) - | (a::m) -> stacklam whrec [a] c m) + | Some (a,m) -> stacklam whrec [a] c m) | x -> s in whrec (x, l) @@ -545,7 +511,7 @@ let reduce_mind_case mia = applist (mia.mlf.(i-1),real_cargs) | DOPN(CoFix _,_) as cofix -> let cofix_def = contract_cofix (destCoFix cofix) in - mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf + mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf) | _ -> assert false (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce @@ -595,18 +561,18 @@ let whd_betaiota_stack x l = let rec whrec (x,stack as s) = match kind_of_term x with | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | a::m -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in if reducible_mind_case c then whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with @@ -626,26 +592,19 @@ let whd_betaiotaevar_stack env sigma x l = whrec (existential_value sigma (ev,args), stack) else s -(* - | DOPN(Abst _,_) -> - if translucent_abst env x then - whrec (abst_value env x) stack - else - (x,stack) -*) | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in if reducible_mind_case c then whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' @@ -670,26 +629,19 @@ let whd_betadeltaiota_stack env sigma x l = whrec (existential_value sigma (ev,args), stack) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) stack - else - (x,stack) -*) | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in if reducible_mind_case c then whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' @@ -715,18 +667,11 @@ let whd_betadeltaiotaeta_stack env sigma x l = whrec (existential_value sigma (ev,args), stack) else s -(* - | DOPN(Abst _,_) -> - if evaluable_abst env x then - whrec (abst_value env x) stack - else - (x,stack) -*) | IsCast (c,_) -> whrec (c, stack) - | IsAppL (f,cl) -> whrec (f, cl@stack) + | IsAppL (f,cl) -> whrec (f, append_stack cl stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> + (match decomp_stack stack with + | None -> (match applist (whrec (c, [])) with | DOPN(AppL,cl) -> let napp = (Array.length cl) -1 in @@ -737,7 +682,7 @@ let whd_betadeltaiotaeta_stack env sigma x l = in if noccurn 1 u then (pop u,[]) else s | _ -> s) | _ -> s) - | (a::m) -> stacklam whrec [a] c m) + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> let (c,cargs) = whrec (d, []) in @@ -745,7 +690,7 @@ let whd_betadeltaiotaeta_stack env sigma x l = whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' @@ -882,31 +827,14 @@ and eqappr cv_pb infos appr1 appr2 = (lft1, fhnf_apply infos n1 def1 v1) appr2 | None -> fun _ -> raise NotConvertible)) - | (FOPN(Abst sp1,al1), FOPN(Abst sp2,al2)) -> - convert_or - (* try first intensional equality *) - (bool_and_convert (sp1 = sp2) - (convert_and - (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) al1 al2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) - v1 v2))) - (* else expand the second occurrence (arbitrary heuristic) *) - (match search_frozen_cst infos (Abst sp2) al2 with - | Some def2 -> - eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) - | None -> (match search_frozen_cst infos (Abst sp1) al2 with - | Some def1 -> eqappr cv_pb infos - (lft1, fhnf_apply infos n1 def1 v1) appr2 - | None -> fun _ -> raise NotConvertible)) - (* only one constant, existential or abstraction *) - | (FOPN((Const _ | Evar _ | Abst _) as op,al1), _) -> + | (FOPN((Const _ | Evar _) as op,al1), _) -> (match search_frozen_cst infos op al1 with | Some def1 -> eqappr cv_pb infos (lft1, fhnf_apply infos n1 def1 v1) appr2 | None -> fun _ -> raise NotConvertible) - | (_, FOPN((Const _ | Evar _ | Abst _) as op,al2)) -> + | (_, FOPN((Const _ | Evar _) as op,al2)) -> (match search_frozen_cst infos op al2 with | Some def2 -> eqappr cv_pb infos appr1 (lft2, fhnf_apply infos n2 def2 v2) @@ -1125,7 +1053,7 @@ let rec apprec env sigma c stack = match kind_of_term t with | IsMutCase (ci,p,d,lf) -> let (cr,crargs) = whd_betadeltaiota_stack env sigma d [] in - let rslt = mkMutCaseA ci p (applist(cr,crargs)) lf in + let rslt = mkMutCase (ci, p, applist(cr,crargs), lf) in if reducible_mind_case cr then apprec env sigma rslt stack else @@ -1152,9 +1080,9 @@ let whd_programs_stack env sigma x l = match kind_of_term x with | IsAppL (f,[c]) -> if occur_meta c then s else whrec (f, c::stack) | IsLambda (_,_,c) -> - (match stack with - | [] -> s - | (a::m) -> stacklam whrec [a] c m) + (match decomp_stack stack with + | None -> s + | Some (a,m) -> stacklam whrec [a] c m) | IsMutCase (ci,p,d,lf) -> if occur_meta d then s @@ -1164,7 +1092,7 @@ let whd_programs_stack env sigma x l = whrec (reduce_mind_case {mP=p; mconstr=c; mcargs=cargs; mci=ci; mlf=lf}, stack) else - (mkMutCaseA ci p (applist(c,cargs)) lf, stack) + (mkMutCase (ci, p, applist(c,cargs), lf), stack) | IsFix fix -> (match reduce_fix whrec fix stack with | Reduced s' -> whrec s' diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6b97c63ac6..68cd846b75 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -50,12 +50,6 @@ let rec execute mf env cstr = | IsVar id -> (make_judge cstr (lookup_var_type id env), cst0) - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - (* ATTENTION : faudra faire le typage du contexte des Const, MutInd et MutConstructsi un jour cela devient des constructions arbitraires et non plus des variables *) diff --git a/kernel/term.ml b/kernel/term.ml index 40feeaab12..1933483901 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -26,7 +26,7 @@ type 'a oper = (* DOP2 *) | Cast | Prod | Lambda (* DOPN *) - | AppL | Const of section_path | Abst of section_path + | AppL | Const of section_path | Evar of existential_key | MutInd of inductive_path | MutConstruct of constructor_path @@ -505,9 +505,6 @@ let mkConst (sp,a) = DOPN (Const sp, a) (* Constructs an existential variable *) let mkEvar (n,a) = DOPN (Evar n, a) -(* Constructs an abstract object *) -let mkAbst sp a = DOPN (Abst sp, a) - (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l) @@ -518,9 +515,9 @@ let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l) let mkMutConstruct (cstr_sp,l) = DOPN (MutConstruct cstr_sp,l) (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -let mkMutCase (ci, p, c, ac) = +let mkMutCaseL (ci, p, c, ac) = DOPN (MutCase ci, Array.append [|p;c|] (Array.of_list ac)) -let mkMutCaseA ci p c ac = +let mkMutCase (ci, p, c, ac) = DOPN (MutCase ci, Array.append [|p;c|] ac) (* If recindxs = [|i1,...in|] @@ -782,6 +779,7 @@ let num_of_evar = function | DOPN (Evar n, _) -> n | _ -> anomaly "num_of_evar called with bad args" +(* (* Destructs an abstract term *) let destAbst = function | DOPN (Abst sp, a) -> (sp, a) @@ -794,7 +792,7 @@ let path_of_abst = function let args_of_abst = function | DOPN(Abst _,args) -> args | _ -> anomaly "args_of_abst called with bad args" - +*) (* Destructs a (co)inductive type named sp *) let destMutInd = function | DOPN (MutInd ind_sp, l) -> (ind_sp,l) @@ -870,7 +868,6 @@ type 'ctxt reference = | RConst of section_path * 'ctxt | RInd of inductive_path * 'ctxt | RConstruct of constructor_path * 'ctxt - | RAbst of section_path | RVar of identifier | REVar of int * 'ctxt @@ -902,7 +899,6 @@ type kindOfTerm = | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr | IsAppL of constr * constr list - | IsAbst of section_path * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -932,7 +928,6 @@ let kind_of_term c = IsAppL (a.(0), List.tl (Array.to_list a)) | DOPN (Const sp, a) -> IsConst (sp,a) | DOPN (Evar sp, a) -> IsEvar (sp,a) - | DOPN (Abst sp, a) -> IsAbst (sp, a) | DOPN (MutInd ind_sp, l) -> IsMutInd (ind_sp,l) | DOPN (MutConstruct cstr_sp,l) -> IsMutConstruct (cstr_sp,l) | DOPN (MutCase ci,v) -> @@ -1709,7 +1704,6 @@ module Hoper = | XTRA s -> XTRA (hstr s) | Sort s -> Sort (hsort s) | Const sp -> Const (hsp sp) - | Abst sp -> Abst (hsp sp) | MutInd (sp,i) -> MutInd (hsp sp, i) | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j) | MutCase ci as t -> t (* TO DO: extract ind_sp *) @@ -1719,7 +1713,6 @@ module Hoper = | (XTRA s1, XTRA s2) -> s1==s2 | (Sort s1, Sort s2) -> s1==s2 | (Const sp1, Const sp2) -> sp1==sp2 - | (Abst sp1, Abst sp2) -> sp1==sp2 | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2 | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) -> sp1==sp2 & i1=i2 & j1=j2 @@ -1795,7 +1788,7 @@ type constr_operator = | OpSort of sorts | OpRel of int | OpVar of identifier | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpAppL | OpConst of section_path | OpAbst of section_path + | OpAppL | OpConst of section_path | OpEvar of existential_key | OpMutInd of inductive_path | OpMutConstruct of constructor_path @@ -1922,3 +1915,88 @@ let generic_fold_left f acc bl tl = | None -> f acc t | Some b -> f (f acc b) t) acc bl in Array.fold_left f acc tl + +let fold_constr f acc c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> acc + | IsCast (c,t) -> f (f acc c) t + | IsProd (_,t,c) -> f (f acc t) c + | IsLambda (_,t,c) -> f (f acc t) c + | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c + | IsAppL (c,l) -> List.fold_left f (f acc c) l + | IsEvar (_,l) -> Array.fold_left f acc l + | IsConst (_,l) -> Array.fold_left f acc l + | IsMutInd (_,l) -> Array.fold_left f acc l + | IsMutConstruct (_,l) -> Array.fold_left f acc l + | IsMutCase (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl + | IsFix (_,(tl,_,bl)) -> Array.fold_left f (Array.fold_left f acc tl) bl + | IsCoFix (_,(tl,_,bl)) -> Array.fold_left f (Array.fold_left f acc tl) bl + +let fold_constr_with_binders g f n acc c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> acc + | IsCast (c,t) -> f n (f n acc c) t + | IsProd (_,t,c) -> f (g n) (f n acc t) c + | IsLambda (_,t,c) -> f (g n) (f n acc t) c + | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c + | IsAppL (c,l) -> List.fold_left (f n) (f n acc c) l + | IsEvar (_,l) -> Array.fold_left (f n) acc l + | IsConst (_,l) -> Array.fold_left (f n) acc l + | IsMutInd (_,l) -> Array.fold_left (f n) acc l + | IsMutConstruct (_,l) -> Array.fold_left (f n) acc l + | IsMutCase (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | IsFix (_,(tl,_,bl)) -> + let n' = iterate g (Array.length tl) n in + Array.fold_left (f n') (Array.fold_left (f n) acc tl) bl + | IsCoFix (_,(tl,_,bl)) -> + let n' = iterate g (Array.length tl) n in + Array.fold_left (f n') (Array.fold_left (f n) acc tl) bl + +let iter_constr_with_binders g f n c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> () + | IsCast (c,t) -> f n c; f n t + | IsProd (_,t,c) -> f n t; f (g n) c + | IsLambda (_,t,c) -> f n t; f (g n) c + | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c + | IsAppL (c,l) -> f n c; List.iter (f n) l + | IsEvar (_,l) -> Array.iter (f n) l + | IsConst (_,l) -> Array.iter (f n) l + | IsMutInd (_,l) -> Array.iter (f n) l + | IsMutConstruct (_,l) -> Array.iter (f n) l + | IsMutCase (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl + | IsFix (_,(tl,_,bl)) -> + Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + | IsCoFix (_,(tl,_,bl)) -> + Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl + +let map_constr f c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsCast (c,t) -> mkCast (f c, f t) + | IsProd (na,t,c) -> mkProd (na, f t, f c) + | IsLambda (na,t,c) -> mkLambda (na, f t, f c) + | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c) + | IsAppL (c,l) -> applist (f c, List.map f l) + | IsEvar (e,l) -> mkEvar (e, Array.map f l) + | IsConst (c,l) -> mkConst (c, Array.map f l) + | IsMutInd (c,l) -> mkMutInd (c, Array.map f l) + | IsMutConstruct (c,l) -> mkMutConstruct (c, Array.map f l) + | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f p, f c, Array.map f bl) + | IsFix (ln,(tl,lna,bl)) -> mkFix (ln,(Array.map f tl,lna,Array.map f bl)) + | IsCoFix(ln,(tl,lna,bl)) -> mkCoFix (ln,(Array.map f tl,lna,Array.map f bl)) + +let map_constr_with_binders g f l c = match kind_of_term c with + | IsRel _ | IsMeta _ | IsVar _ | IsSort _ | IsXtra _ -> c + | IsCast (c,t) -> mkCast (f l c, f l t) + | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c) + | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c) + | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c) + | IsAppL (c,al) -> applist (f l c, List.map (f l) al) + | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al) + | IsConst (c,al) -> mkConst (c, Array.map (f l) al) + | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al) + | IsMutConstruct (c,al) -> mkMutConstruct (c, Array.map (f l) al) + | IsMutCase (ci,p,c,bl) -> mkMutCase (ci, f l p, f l c, Array.map (f l) bl) + | IsFix (ln,(tl,lna,bl)) -> + let l' = List.fold_right g lna l in + mkFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) + | IsCoFix(ln,(tl,lna,bl)) -> + let l' = List.fold_right g lna l in + mkCoFix (ln,(Array.map (f l) tl,lna,Array.map (f l') bl)) diff --git a/kernel/term.mli b/kernel/term.mli index 0eb1d645d7..e4e0e1df5c 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -42,7 +42,7 @@ type 'a oper = | Meta of int | Sort of 'a | Cast | Prod | Lambda - | AppL | Const of section_path | Abst of section_path + | AppL | Const of section_path | Evar of existential_key | MutInd of inductive_path | MutConstruct of constructor_path @@ -104,7 +104,6 @@ type 'ctxt reference = | RConst of section_path * 'ctxt | RInd of inductive_path * 'ctxt | RConstruct of constructor_path * 'ctxt - | RAbst of section_path | RVar of identifier | REVar of int * 'ctxt @@ -136,7 +135,6 @@ type kindOfTerm = | IsLambda of name * constr * constr | IsLetIn of name * constr * constr * constr | IsAppL of constr * constr list - | IsAbst of section_path * constr array | IsEvar of existential | IsConst of constant | IsMutInd of inductive @@ -230,9 +228,6 @@ val mkConst : constant -> constr (* Constructs an existential variable *) val mkEvar : existential -> constr -(* Constructs an abstract object *) -val mkAbst : section_path -> constr array -> constr - (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) val mkMutInd : inductive -> constr @@ -243,8 +238,8 @@ val mkMutInd : inductive -> constr val mkMutConstruct : constructor -> constr (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -val mkMutCase : case_info * constr * constr * constr list -> constr -val mkMutCaseA : case_info -> constr -> constr -> constr array -> constr +val mkMutCaseL : case_info * constr * constr * constr list -> constr +val mkMutCase : case_info * constr * constr * constr array -> constr (* If [recindxs = [|i1,...in|]] [typarray = [|t1,...tn|]] @@ -363,11 +358,12 @@ val args_of_const : constr -> constr array val destEvar : constr -> int * constr array val num_of_evar : constr -> int +(* (* Destructs an abstract term *) val destAbst : constr -> section_path * constr array val path_of_abst : constr -> section_path val args_of_abst : constr -> constr array - +*) (* Destructs a (co)inductive type *) val destMutInd : constr -> inductive val op_of_mind : constr -> inductive_path @@ -697,7 +693,7 @@ type constr_operator = | OpSort of sorts | OpRel of int | OpVar of identifier | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpAppL | OpConst of section_path | OpAbst of section_path + | OpAppL | OpConst of section_path | OpEvar of existential_key | OpMutInd of inductive_path | OpMutConstruct of constructor_path @@ -717,6 +713,20 @@ val generic_fold_left : ('a -> constr -> 'a) -> 'a -> (name * constr option * constr) list -> constr array -> 'a +val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + +val iter_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit + +val map_constr : (constr -> constr) -> constr -> constr + +val map_constr_with_binders : + (name -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr + + (*s Hash-consing functions for constr. *) val hcons_constr: diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4b22b0b6a8..37dfccf9ee 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -213,7 +213,7 @@ let type_of_case env sigma ci pj cj lfj = type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft); - { uj_val = mkMutCaseA ci pj.uj_val cj.uj_val (Array.map j_val_only lfj); + { uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val_only lfj); uj_type = make_typed rslty kind } (* Prop and Set *) @@ -636,7 +636,7 @@ let rec check_subterm_rec_meta env sigma vectn k def = | IsVar _ | IsSort _ -> List.for_all (check_rec_call n lst) l - | IsXtra _ | IsAbst _ -> List.for_all (check_rec_call n lst) l + | IsXtra _ -> List.for_all (check_rec_call n lst) l ) in @@ -856,7 +856,6 @@ let control_only_guard env sigma = | IsMutConstruct (_,cl) -> Array.iter control_rec cl | IsConst (_,cl) -> Array.iter control_rec cl | IsEvar (_,cl) -> Array.iter control_rec cl - | IsAbst (_,cl) -> Array.iter control_rec cl | IsAppL (_,cl) -> List.iter control_rec cl | IsCast (c1,c2) -> control_rec c1; control_rec c2 | IsProd (_,c1,c2) -> control_rec c1; control_rec c2 |