diff options
-rw-r--r-- | kernel/closure.ml | 124 | ||||
-rw-r--r-- | kernel/closure.mli | 196 | ||||
-rw-r--r-- | kernel/reduction.ml | 93 | ||||
-rw-r--r-- | kernel/reduction.mli | 21 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 1 | ||||
-rw-r--r-- | pretyping/tacred.ml | 3 |
6 files changed, 240 insertions, 198 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 08b0cd065..e61f94939 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -412,10 +412,10 @@ let contract_cofixp env (i,(_,_,bds as bodies)) = * (APP (l,(APP ...))) forbidden *) -type stack = +type cbv_stack = | TOP - | APP of cbv_value list * stack - | CASE of constr * constr array * case_info * cbv_value subs * stack + | APP of cbv_value list * cbv_stack + | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack (* Adds an application list. Collapse APPs! *) let stack_app appl stack = @@ -717,6 +717,83 @@ let cbv_norm infos constr = (**** End of call by value ****) +(**********************************************************************) +(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) + +type 'a stack = + | EmptyStack + | ConsStack of 'a array * int * 'a stack + +let empty_stack = EmptyStack + +let decomp_stack = function + | EmptyStack -> None + | ConsStack (v, n, s) -> + 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) + +let rec app_stack = function + | f, EmptyStack -> f + | f, ConsStack (v, n, s) -> + let args = if n=0 then v else Array.sub v n (Array.length v - n) in + app_stack (appvect (f, args), s) + +let rec list_of_stack = function + | EmptyStack -> [] + | ConsStack (v, n, s) -> + let args = if n=0 then v else Array.sub v n (Array.length v - n) in + Array.fold_right (fun a l -> a::l) args (list_of_stack s) + +let array_of_stack s = + let rec stackrec = function + | EmptyStack -> [] + | ConsStack (v, n, s) -> + let args = if n=0 then v else Array.sub v n (Array.length v - n) in + args :: (stackrec s) + in Array.concat (stackrec s) + +let rec stack_assign s p c = match s with + | EmptyStack -> EmptyStack + | ConsStack (v, n, s) -> + let q = Array.length v - n in + if p >= q then + ConsStack (v, n, stack_assign s (p-q) c) + else + let v' = Array.sub v n q in + v'.(p) <- c; + ConsStack (v', 0, s) + +let rec stack_tail p s = + if p = 0 then s else + match s with + | EmptyStack -> failwith "stack_shop" + | ConsStack (v, n, s) -> + let q = Array.length v - n in + if p >= q then stack_tail (p-q) s + else ConsStack (v, n+p, s) + +let rec stack_nth s p = match s with + | EmptyStack -> raise Not_found + | ConsStack (v, n, s) -> + let q = Array.length v - n in + if p >= q then stack_nth s (p-q) + else v.(p+n) + +let rec stack_args_size = function + | EmptyStack -> 0 + | ConsStack (v, n, s) -> Array.length v - n + stack_args_size s + + +(* Version avec listes +type stack = constr list + +let decomp_stack = function + | [] -> None + | v :: s -> Some (v,s) + +let append_stack v s = v@s +*) (* Lazy reduction: the one used in kernel operations *) @@ -999,11 +1076,12 @@ let rec strip_frterm n v stack = match v.term with | FLIFT (k,f) -> strip_frterm (k+n) f stack | FApp (f,args) -> - strip_frterm n f ((Array.map (lift_freeze n) args)::stack) + strip_frterm n f + (append_stack (Array.map (lift_freeze n) args) stack) | FCast (f,_) -> (strip_frterm n f stack) - | _ -> (n, v, Array.concat stack) + | _ -> (n, v, stack) -let strip_freeze v = strip_frterm 0 v [] +let strip_freeze v = strip_frterm 0 v empty_stack (* Same as contract_fixp, but producing a freeze *) @@ -1038,9 +1116,9 @@ let copy_case ci p ft bl = (* Check if the case argument enables iota-reduction *) type case_status = - | CONSTRUCTOR of int * fconstr array + | CONSTRUCTOR of int * fconstr stack | COFIX of int * int * (fconstr array * name list * fconstr array) * - fconstr array * constr array * freeze subs + fconstr stack * constr array * freeze subs | IRREDUCTIBLE @@ -1048,14 +1126,14 @@ let constr_or_cofix env v = let (lft_hd, head, appl) = strip_freeze v in match head.term with | FConstruct ((indsp,i),_) -> - let args = snd (array_chop (mindsp_nparams env indsp) appl) in + let args = stack_tail (mindsp_nparams env indsp) appl in CONSTRUCTOR (i, args) | FCoFix (bnum, def, bds, env) -> COFIX (lft_hd,bnum,def,appl, bds, env) | _ -> IRREDUCTIBLE -let fix_reducible env unf_fun n appl = - if n < Array.length appl & n >= 0 (* e.g for Acc_rec: n = -2 *) then - let v = unf_fun appl.(n) in +let fix_reducible env unf_fun n stack = + if n < stack_args_size stack & n >= 0 (* e.g for Acc_rec: n = -2 *) then + let v = unf_fun (stack_nth stack n) in match constr_or_cofix env v with | CONSTRUCTOR _ -> true | _ -> false @@ -1083,7 +1161,7 @@ and whnf_frterm info ft = let uf = unfreeze info f in { norm = uf.norm; term = FLIFT(k, uf) } | FCast (f,_) -> whnf_frterm info f (* remove outer casts *) - | FApp (f,appl) -> whnf_apply info f appl + | FApp (f,appl) -> whnf_apply info f (append_stack appl empty_stack) | FFlex (FConst (sp,vars)) -> let cst = (sp, Array.map term_of_freeze vars) in if red_under info.i_flags (CONST [sp]) then @@ -1152,23 +1230,27 @@ and whnf_frterm info ft = | FFix _ | FCoFix _ | FInd _ | FConstruct _ | FLambda _ | FProd _ -> ft (* Weak head reduction: case of the application (head appl) *) -and whnf_apply info head appl = +and whnf_apply info head stack = let head = unfreeze info head in - if Array.length appl = 0 then + if stack = empty_stack then head else - let (lft_hd,whd,args) = strip_frterm 0 head [appl] in + let (lft_hd,whd,lstack) = strip_frterm 0 head stack in match whd.term with | FLambda (_,_,_,t,subs) when red_under info.i_flags BETA -> - let vbody = contract_subst lft_hd t subs args.(0) in - whnf_apply info vbody (array_tl args) + (match decomp_stack lstack with + | Some (c, stack') -> + let vbody = contract_subst lft_hd t subs c in + whnf_apply info vbody stack' + | None -> assert false) | FFix ((reci,bnum), _, _, _) as fx when red_under info.i_flags IOTA & fix_reducible info.i_env - (unfreeze (infos_under info)) reci.(bnum) args -> + (unfreeze (infos_under info)) reci.(bnum) lstack -> let fix = contract_fix_vect fx in - whnf_apply info (lift_freeze lft_hd fix) args - | _ -> + whnf_apply info (lift_freeze lft_hd fix) lstack + | _ -> + let appl = array_of_stack stack in { norm = (is_val head) & (array_for_all is_val appl); term = FApp (head, appl) } diff --git a/kernel/closure.mli b/kernel/closure.mli index c38c6aaa0..8bb25554b 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -82,7 +82,97 @@ type 'a subs = | SHIFT of int * 'a subs | LIFT of int * 'a subs -(*s Call by value functions *) +(*s A [stack] is a context of arguments, arguments are pushed by + [append_stack] one array at a time but popped with [decomp_stack] + one by one *) + +type 'a stack +val empty_stack : 'a stack +val append_stack : 'a array -> 'a stack -> 'a stack +val decomp_stack : 'a stack -> ('a * 'a stack) option +val list_of_stack : 'a stack -> 'a list +val array_of_stack : 'a stack -> 'a array +val stack_assign : 'a stack -> int -> 'a -> 'a stack +val stack_args_size : 'a stack -> int +val app_stack : constr * constr stack -> constr +val stack_tail : int -> 'a stack -> 'a stack +val stack_nth : 'a stack -> int -> 'a + +(***********************************************************************) +(*s Call-by-value reduction *) + +(* Entry point for cbv normalization of a constr *) +type 'a cbv_infos +val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos +val cbv_norm : 'a cbv_infos -> constr -> constr + +(*s Lazy reduction. *) + +(* [fconstr] is the type of frozen constr *) + +type fconstr + +(* [fconstr] can be accessed by using the function [frterm_of] and by + matching on type [frterm] *) + +type frterm = + | FRel of int + | FAtom of constr + | FCast of fconstr * fconstr + | FFlex of frreference + | FInd of inductive_path * fconstr array + | FConstruct of constructor_path * fconstr array + | FApp of fconstr * fconstr array + | FFix of (int array * int) * (fconstr array * name list * fconstr array) + * constr array * fconstr subs + | FCoFix of int * (fconstr array * name list * fconstr array) + * constr array * fconstr subs + | FCases of case_info * fconstr * fconstr * fconstr array + | FLambda of name * fconstr * fconstr * constr * fconstr subs + | FProd of name * fconstr * fconstr * constr * fconstr subs + | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs + | FLIFT of int * fconstr + | FFROZEN of constr * fconstr subs + +and frreference = + | FConst of section_path * fconstr array + | FEvar of (existential * fconstr subs) + | FVar of identifier + | FFarRel of int + +val frterm_of : fconstr -> frterm + +(* To lazy reduce a constr, create a ['a clos_infos] with + [create_cbv_infos], inject the term to reduce with [inject]; then use + a reduction function *) + +(* Global and local constant cache *) +type 'a clos_infos +val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos +val clos_infos_env : 'a clos_infos -> env + +val inject : constr -> fconstr + +(* Reduction function *) + +(* [norm_val] is for strong normalization *) +val norm_val : 'a clos_infos -> fconstr -> constr + +(* [whd_val] is for weak head normalization *) +val whd_val : 'a clos_infos -> fconstr -> constr + +(* [fhnf] and [fnf_apply] are for weak head normalization but staying + in [fcontr] world to perform step by step weak head normalization *) + +val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr stack +val fhnf_apply : 'a clos_infos -> + int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack + +(* [search_frozen_value] unfolds references in a [fconstr] *) +val search_frozen_value : 'a clos_infos -> frreference -> fconstr option + + +(*i This is for cbv debug *) type cbv_value = | VAL of int * constr | LAM of name * constr * constr * cbv_value subs @@ -92,75 +182,32 @@ type cbv_value = val shift_value : int -> cbv_value -> cbv_value -(*i Private ?? -val contract_fixp : cbv_value subs -> fixpoint -> cbv_value subs * constr -i*) - -type stack = +type cbv_stack = | TOP - | APP of cbv_value list * stack - | CASE of constr * constr array * case_info * cbv_value subs * stack + | APP of cbv_value list * cbv_stack + | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack -val stack_app : cbv_value list -> stack -> stack -val under_case_stack : stack -> bool -val strip_appl : cbv_value -> stack -> cbv_value * stack +val stack_app : cbv_value list -> cbv_stack -> cbv_stack +val under_case_stack : cbv_stack -> bool +val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack -val red_allowed : flags -> stack -> red_kind -> bool +val red_allowed : flags -> cbv_stack -> red_kind -> bool val reduce_const_body : - (cbv_value -> cbv_value) -> cbv_value -> stack -> cbv_value * stack -(*i Private ?? -val fixp_reducible : - (cbv_value -> cbv_value) -> flags -> fixpoint -> stack -> bool -i*) - -(* normalization of a constr: the two functions to know... *) -type 'a cbv_infos -val create_cbv_infos : flags -> env -> 'a evar_map -> 'a cbv_infos -val cbv_norm : 'a cbv_infos -> constr -> constr + (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack (* recursive functions... *) val cbv_stack_term : 'a cbv_infos -> - stack -> cbv_value subs -> constr -> cbv_value + cbv_stack -> cbv_value subs -> constr -> cbv_value val cbv_norm_term : 'a cbv_infos -> cbv_value subs -> constr -> constr val cbv_norm_more : 'a cbv_infos -> cbv_value subs -> cbv_value -> cbv_value val norm_head : 'a cbv_infos -> - cbv_value subs -> constr -> stack -> cbv_value * stack -val apply_stack : 'a cbv_infos -> constr -> stack -> constr + cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack +val apply_stack : 'a cbv_infos -> constr -> cbv_stack -> constr val cbv_norm_value : 'a cbv_infos -> cbv_value -> constr +(* End of cbv debug section i*) - -(*s Lazy reduction. *) - -type freeze = { - mutable norm: bool; - mutable term: frterm } - -and frterm = - | FRel of int - | FAtom of constr - | FCast of freeze * freeze - | FFlex of frreference - | FInd of inductive_path * freeze array - | FConstruct of constructor_path * freeze array - | FApp of freeze * freeze array - | FFix of (int array * int) * (freeze array * name list * freeze array) - * constr array * freeze subs - | FCoFix of int * (freeze array * name list * freeze array) - * constr array * freeze subs - | FCases of case_info * freeze * freeze * freeze array - | FLambda of name * freeze * freeze * constr * freeze subs - | FProd of name * freeze * freeze * constr * freeze subs - | FLetIn of name * freeze * freeze * freeze * constr * freeze subs - | FLIFT of int * freeze - | FFROZEN of constr * freeze subs - -and frreference = - | FConst of section_path * freeze array - | FEvar of (existential * freeze subs) - | FVar of identifier - | FFarRel of int - -val frterm_of : freeze -> frterm +(*i This is for lazy debug *) +type freeze = fconstr val is_val : freeze -> bool val lift_frterm : int -> freeze -> freeze @@ -181,44 +228,25 @@ val applist_of_freeze : freeze array -> constr list (* contract a substitution *) val contract_subst : int -> constr -> freeze subs -> freeze -> freeze -(* Global and local constant cache *) -type 'a clos_infos -val create_clos_infos : flags -> env -> 'a evar_map -> 'a clos_infos -val clos_infos_env : 'a clos_infos -> env - -(* Calculus of Constructions *) -type fconstr = freeze - -val inject : constr -> fconstr - val strip_frterm : - int -> fconstr -> fconstr array list -> int * fconstr * fconstr array -val strip_freeze : fconstr -> int * fconstr * fconstr array - + int -> fconstr -> fconstr stack -> int * fconstr * fconstr stack +val strip_freeze : fconstr -> int * fconstr * fconstr stack (* Auxiliary functions for (co)fixpoint reduction *) val contract_fix_vect : frterm -> fconstr val copy_case : case_info -> fconstr -> fconstr -> fconstr array -> fconstr - (* Iota analysis: reducible ? *) type case_status = - | CONSTRUCTOR of int * fconstr array + | CONSTRUCTOR of int * fconstr stack | COFIX of int * int * (fconstr array * name list * fconstr array) * - fconstr array * constr array * freeze subs + fconstr stack * constr array * freeze subs | IRREDUCTIBLE - -(* Reduction function *) -val norm_val : 'a clos_infos -> fconstr -> constr -val whd_val : 'a clos_infos -> fconstr -> constr -val fhnf: 'a clos_infos -> fconstr -> int * fconstr * fconstr array -val fhnf_apply : 'a clos_infos -> - int -> fconstr -> fconstr array -> int * fconstr * fconstr array -val search_frozen_value : 'a clos_infos -> frreference -> fconstr option - (* recursive functions... *) val unfreeze : 'a clos_infos -> fconstr -> fconstr val whnf_frterm : 'a clos_infos -> fconstr -> fconstr val whnf_term : 'a clos_infos -> fconstr subs -> constr -> fconstr -val whnf_apply : 'a clos_infos -> fconstr -> fconstr array -> fconstr +val whnf_apply : 'a clos_infos -> fconstr -> fconstr stack -> fconstr + +(* End of cbn debug section i*) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4df8de1a2..43a671536 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -14,13 +14,8 @@ open Closure exception Elimconst -(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) -type stack = - | EmptyStack - | ConsStack of constr array * int * stack - (* The type of (machine) states (= lambda-bar-calculus' cuts) *) -type state = constr * stack +type state = constr * constr stack type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr type 'a reduction_function = 'a contextual_reduction_function @@ -36,61 +31,6 @@ type 'a contextual_state_reduction_function = type 'a state_reduction_function = 'a contextual_state_reduction_function type local_state_reduction_function = state -> state -let empty_stack = EmptyStack - -let decomp_stack = function - | EmptyStack -> None - | ConsStack (v, n, s) -> - 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) - -let rec app_stack = function - | f, EmptyStack -> f - | f, ConsStack (v, n, s) -> - let args = if n=0 then v else Array.sub v n (Array.length v - n) in - app_stack (appvect (f, args), s) - -let rec list_of_stack = function - | EmptyStack -> [] - | ConsStack (v, n, s) -> - let args = if n=0 then v else Array.sub v n (Array.length v - n) in - Array.fold_right (fun a l -> a::l) args (list_of_stack s) - -let appterm_of_stack (f,s) = (f,list_of_stack s) - -let rec stack_assign s p c = match s with - | EmptyStack -> EmptyStack - | ConsStack (v, n, s) -> - let q = Array.length v - n in - if p >= q then - ConsStack (v, n, stack_assign s (p-q) c) - else - let v' = Array.sub v n q in - v'.(p) <- c; - ConsStack (v', 0, s) - -let rec stack_nth s p = match s with - | EmptyStack -> raise Not_found - | ConsStack (v, n, s) -> - let q = Array.length v - n in - if p >= q then stack_nth s (p-q) - else v.(p+n) - -let rec stack_args_size = function - | EmptyStack -> 0 - | ConsStack (v, n, s) -> Array.length v - n + stack_args_size s - - -(* Version avec listes -type stack = constr list - -let decomp_stack = function - | [] -> None - | v :: s -> Some (v,s) - -let append_stack v s = v@s -*) (*************************************) (*** Reduction Functions Operators ***) (*************************************) @@ -101,6 +41,8 @@ let rec whd_state (x, stack as s) = | IsCast (c,_) -> whd_state (c, stack) | _ -> s +let appterm_of_stack (f,s) = (f,list_of_stack s) + let whd_stack x = appterm_of_stack (whd_state (x, empty_stack)) let whd_castapp_stack = whd_stack @@ -204,7 +146,7 @@ let rec stacklam recfun env t stack = | _ -> recfun (substl env t, stack) let beta_applist (c,l) = - stacklam app_stack [] c (append_stack (Array.of_list l) EmptyStack) + stacklam app_stack [] c (append_stack (Array.of_list l) empty_stack) (* Iota reduction tools *) @@ -734,6 +676,9 @@ let convert_forall2 f v1 v2 c = then array_fold_left2 (fun c x y -> f x y c) c v1 v2 else raise NotConvertible +let convert_stacks f v1 v2 c = + convert_forall2 f (array_of_stack v1) (array_of_stack v2) c + (* Convertibility of sorts *) let sort_cmp pb s0 s1 = @@ -771,15 +716,15 @@ and eqappr cv_pb infos appr1 appr2 = (match kind_of_term a1, kind_of_term a2 with | (IsSort s1, IsSort s2) -> bool_and_convert - (Array.length v1 = 0 && Array.length v2 = 0) + (stack_args_size v1 = 0 && stack_args_size v2 = 0) (sort_cmp cv_pb s1 s2) | (IsMeta n, IsMeta m) -> bool_and_convert (n=m) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) | IsXtra s1, IsXtra s2 -> bool_and_convert (s1=s2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) | _ -> fun _ -> raise NotConvertible) @@ -787,14 +732,14 @@ and eqappr cv_pb infos appr1 appr2 = | (FRel n, FRel m) -> bool_and_convert (reloc_rel n el1 = reloc_rel m el2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) (* 2 constants, 2 existentials or 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> convert_or (* try first intensional equality *) (bool_and_convert (fl1 = fl2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) (* else expand the second occurrence (arbitrary heuristic) *) (fun u -> match search_frozen_value infos fl2 with @@ -820,7 +765,7 @@ and eqappr cv_pb infos appr1 appr2 = (* other constructors *) | (FLambda (_,c1,c2,_,_), FLambda (_,c'1,c'2,_,_)) -> bool_and_convert - (Array.length v1 = 0 && Array.length v2 = 0) + (stack_args_size v1 = 0 && stack_args_size v2 = 0) (convert_and (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) (ccnv (pb_equal cv_pb) infos (el_lift el1) (el_lift el2) c2 c'2)) @@ -829,7 +774,7 @@ and eqappr cv_pb infos appr1 appr2 = | (FProd (_,c1,c2,_,_), FProd (_,c'1,c'2,_,_)) -> bool_and_convert - (Array.length v1 = 0 && Array.length v2 = 0) + (stack_args_size v1 = 0 && stack_args_size v2 = 0) (convert_and (ccnv (pb_equal cv_pb) infos el1 el2 c1 c'1) (* Luo's system *) (ccnv cv_pb infos (el_lift el1) (el_lift el2) c2 c'2)) @@ -845,19 +790,19 @@ and eqappr cv_pb infos appr1 appr2 = (ccnv (pb_equal cv_pb) infos el1 el2 c1 c2) (convert_and (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2) )) | (FInd (op1,cl1), FInd(op2,cl2)) -> bool_and_convert (op1 = op2) (convert_and (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) | (FConstruct (op1,cl1), FConstruct(op2,cl2)) -> bool_and_convert (op1 = op2) (convert_and (convert_forall2 (ccnv (pb_equal cv_pb) infos el1 el2) cl1 cl2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2)) | (FFix (op1,(tys1,_,cl1),_,_), FFix(op2,(tys2,_,cl2),_,_)) -> let n = Array.length cl1 in bool_and_convert (op1 = op2) @@ -867,7 +812,7 @@ and eqappr cv_pb infos appr1 appr2 = (convert_forall2 (ccnv (pb_equal cv_pb) infos (el_liftn n el1) (el_liftn n el2)) cl1 cl2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))) | (FCoFix (op1,(tys1,_,cl1),_,_), FCoFix(op2,(tys2,_,cl2),_,_)) -> let n = Array.length cl1 in @@ -878,7 +823,7 @@ and eqappr cv_pb infos appr1 appr2 = (convert_forall2 (ccnv (pb_equal cv_pb) infos (el_liftn n el1) (el_liftn n el2)) cl1 cl2) - (convert_forall2 (ccnv (pb_equal cv_pb) infos lft1 lft2) + (convert_stacks (ccnv (pb_equal cv_pb) infos lft1 lft2) v1 v2))) | _ -> (fun _ -> raise NotConvertible) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7828ff940..600cdd823 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -14,20 +14,7 @@ open Closure exception Elimconst -(*s A [stack] is a context of arguments, arguments are pushed by - [append_stack] one array at a time but popped with [decomp_stack] - one by one *) - -type stack -val empty_stack : stack -val append_stack : constr array -> stack -> stack -val decomp_stack : stack -> (constr * stack) option -val list_of_stack : stack -> constr list -val stack_assign : stack -> int -> constr -> stack -val stack_args_size : stack -> int -val app_stack : constr * stack -> constr - -type state = constr * stack +type state = constr * constr stack type 'a contextual_reduction_function = env -> 'a evar_map -> constr -> constr type 'a reduction_function = 'a contextual_reduction_function @@ -58,7 +45,7 @@ val strong_prodspine : local_reduction_function -> local_reduction_function val stack_reduction_of_reduction : 'a reduction_function -> 'a state_reduction_function i*) -val stacklam : (state -> 'a) -> constr list -> constr -> stack -> 'a +val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a (*s Generic Optimized Reduction Function using Closures *) @@ -148,9 +135,9 @@ val whd_programs : 'a reduction_function type fix_reduction_result = NotReducible | Reduced of state -val fix_recarg : fixpoint -> stack -> (int * constr) option +val fix_recarg : fixpoint -> constr stack -> (int * constr) option val reduce_fix : local_state_reduction_function -> fixpoint - -> stack -> fix_reduction_result + -> constr stack -> fix_reduction_result (*s Conversion Functions (uses closures, lazy strategy) *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c90dcddb1..f0b50aa0d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -5,6 +5,7 @@ open Util open Names open Term open Reduction +open Closure open Instantiate open Environ open Typing diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1e162a4bd..715cb798a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -8,6 +8,7 @@ open Term open Inductive open Environ open Reduction +open Closure open Instantiate (************************************************************************) @@ -582,8 +583,6 @@ let rec substlin env name n ol c = | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c) -open Closure - let unfold env sigma name = clos_norm_flags (unfold_flags name) env sigma |