aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/closure.ml206
-rw-r--r--kernel/closure.mli63
-rw-r--r--kernel/reduction.ml46
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/reductionops.ml85
-rw-r--r--pretyping/reductionops.mli28
-rw-r--r--pretyping/tacred.ml2
7 files changed, 270 insertions, 162 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index abbc66077..c5a5b9ffa 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -394,90 +394,6 @@ let create mk_cl flgs env =
(**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
-
-type 'a stack_member =
- | Zapp of 'a list
- | Zcase of case_info * 'a * 'a array
- | Zfix of 'a * 'a stack
- | Zshift of int
- | Zupdate of 'a
-
-and 'a stack = 'a stack_member list
-
-let empty_stack = []
-let append_stack_list = function
- | ([],s) -> s
- | (l1, Zapp l :: s) -> Zapp (l1@l) :: s
- | (l1, s) -> Zapp l1 :: s
-let append_stack v s = append_stack_list (Array.to_list v, s)
-
-(* Collapse the shifts in the stack *)
-let zshift n s =
- match (n,s) with
- (0,_) -> s
- | (_,Zshift(k)::s) -> Zshift(n+k)::s
- | _ -> Zshift(n)::s
-
-let rec stack_args_size = function
- | Zapp l::s -> List.length l + stack_args_size s
- | Zshift(_)::s -> stack_args_size s
- | Zupdate(_)::s -> stack_args_size s
- | _ -> 0
-
-(* When used as an argument stack (only Zapp can appear) *)
-let rec decomp_stack = function
- | Zapp[v]::s -> Some (v, s)
- | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
- | Zapp [] :: s -> decomp_stack s
- | _ -> None
-let rec decomp_stackn = function
- | Zapp [] :: s -> decomp_stackn s
- | Zapp l :: s -> (Array.of_list l, s)
- | _ -> assert false
-let array_of_stack s =
- let rec stackrec = function
- | [] -> []
- | Zapp args :: s -> args :: (stackrec s)
- | _ -> assert false
- in Array.of_list (List.concat (stackrec s))
-let rec list_of_stack = function
- | [] -> []
- | Zapp args :: s -> args @ (list_of_stack s)
- | _ -> assert false
-let rec app_stack = function
- | f, [] -> f
- | f, (Zapp [] :: s) -> app_stack (f, s)
- | f, (Zapp args :: s) ->
- app_stack (applist (f, args), s)
- | _ -> assert false
-let rec stack_assign s p c = match s with
- | Zapp args :: s ->
- let q = List.length args in
- if p >= q then
- Zapp args :: stack_assign s (p-q) c
- else
- (match list_chop p args with
- (bef, _::aft) -> Zapp (bef@c::aft) :: s
- | _ -> assert false)
- | _ -> s
-let rec stack_tail p s =
- if p = 0 then s else
- match s with
- | Zapp args :: s ->
- let q = List.length args in
- if p >= q then stack_tail (p-q) s
- else Zapp (list_skipn p args) :: s
- | _ -> failwith "stack_tail"
-let rec stack_nth s p = match s with
- | Zapp args :: s ->
- let q = List.length args in
- if p >= q then stack_nth s (p-q)
- else List.nth args p
- | _ -> raise Not_found
-
-
-(**********************************************************************)
(* Lazy reduction: the one used in kernel operations *)
(* type of shared terms. fconstr and frterm are mutually recursive.
@@ -543,6 +459,81 @@ let update v1 (no,t) =
v1)
else {norm=no;term=t}
+(**********************************************************************)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
+
+type stack_member =
+ | Zapp of fconstr array
+ | Zcase of case_info * fconstr * fconstr array
+ | Zfix of fconstr * stack
+ | Zshift of int
+ | Zupdate of fconstr
+
+and stack = stack_member list
+
+let empty_stack = []
+let append_stack v s =
+ if Array.length v = 0 then s else
+ match s with
+ | Zapp l :: s -> Zapp (Array.append v l) :: s
+ | _ -> Zapp v :: s
+
+(* Collapse the shifts in the stack *)
+let zshift n s =
+ match (n,s) with
+ (0,_) -> s
+ | (_,Zshift(k)::s) -> Zshift(n+k)::s
+ | _ -> Zshift(n)::s
+
+let rec stack_args_size = function
+ | Zapp v :: s -> Array.length v + stack_args_size s
+ | Zshift(_)::s -> stack_args_size s
+ | Zupdate(_)::s -> stack_args_size s
+ | _ -> 0
+
+(* When used as an argument stack (only Zapp can appear) *)
+let rec decomp_stack = function
+ | Zapp v :: s ->
+ (match Array.length v with
+ 0 -> decomp_stack s
+ | 1 -> Some (v.(0), s)
+ | _ ->
+ Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
+ | _ -> None
+let rec decomp_stackn = function
+ | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
+ | _ -> assert false
+let array_of_stack s =
+ let rec stackrec = function
+ | [] -> []
+ | Zapp args :: s -> args :: (stackrec s)
+ | _ -> assert false
+ in Array.concat (stackrec s)
+let rec stack_assign s p c = match s with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if p >= q then
+ Zapp args :: stack_assign s (p-q) c
+ else
+ (let nargs = Array.copy args in
+ nargs.(p) <- c;
+ Zapp nargs :: s)
+ | _ -> s
+let rec stack_tail p s =
+ if p = 0 then s else
+ match s with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if p >= q then stack_tail (p-q) s
+ else Zapp (Array.sub args p (q-p)) :: s
+ | _ -> failwith "stack_tail"
+let rec stack_nth s p = match s with
+ | Zapp args :: s ->
+ let q = Array.length args in
+ if p >= q then stack_nth s (p-q)
+ else args.(p)
+ | _ -> raise Not_found
+
(* Lifting. Preserves sharing (useful only for cell with norm=Red).
lft_fconstr always create a new cell, while lift_fconstr avoids it
when the lift is 0. *)
@@ -568,7 +559,7 @@ let clos_rel e i =
| Inl(n,mt) -> lift_fconstr n mt
| Inr(k,None) -> {norm=Norm; term= FRel k}
| Inr(k,Some p) ->
- lift_fconstr (k-p) {norm=Norm;term=FFlex(RelKey p)}
+ lift_fconstr (k-p) {norm=Red;term=FFlex(RelKey p)}
(* since the head may be reducible, we might introduce lifts of 0 *)
let compact_stack head stk =
@@ -801,14 +792,12 @@ let rec fstrong unfreeze_fun lfts v =
let rec zip m stk =
match stk with
| [] -> m
- | Zapp args :: s ->
- let args = Array.of_list args in
- zip {norm=neutr m.norm; term=FApp(m, args)} s
+ | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s
| Zcase(ci,p,br)::s ->
let t = FCases(ci, p, m, br) in
zip {norm=neutr m.norm; term=t} s
| Zfix(fx,par)::s ->
- zip fx (par @ append_stack_list ([m], s))
+ zip fx (par @ append_stack [|m|] s)
| Zshift(n)::s ->
zip (lift_fconstr n m) s
| Zupdate(rf)::s ->
@@ -841,31 +830,30 @@ let strip_update_shift_app head stk =
strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
| (Zapp args :: s) ->
strip_rec (Zapp args :: rstk)
- {norm=h.norm;term=FApp(h,Array.of_list args)} depth s
+ {norm=h.norm;term=FApp(h,args)} depth s
| Zupdate(m)::s ->
strip_rec rstk (update m (h.norm,h.term)) depth s
| stk -> (depth,List.rev rstk, stk) in
strip_rec [] head 0 stk
-let rec get_nth_arg head n stk =
+let get_nth_arg head n stk =
assert (head.norm <> Red);
let rec strip_rec rstk h depth n = function
| Zshift(k) as e :: s ->
strip_rec (e::rstk) (lift_fconstr k h) (depth+k) n s
| Zapp args::s' ->
- let q = List.length args in
+ let q = Array.length args in
if n >= q
then
strip_rec (Zapp args::rstk)
- {norm=h.norm;term=FApp(h,Array.of_list args)} depth (n-q) s'
+ {norm=h.norm;term=FApp(h,args)} depth (n-q) s'
else
- (match list_chop n args with
- (bef, v::aft) ->
- let stk' =
- List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
- (Some (stk', v), append_stack_list (aft,s'))
- | _ -> assert false)
+ let bef = Array.sub args 0 n in
+ let aft = Array.sub args (n+1) (q-n-1) in
+ let stk' =
+ List.rev (if n = 0 then rstk else (Zapp bef :: rstk)) in
+ (Some (stk', args.(n)), append_stack aft s')
| Zupdate(m)::s ->
strip_rec rstk (update m (h.norm,h.term)) depth n s
| s -> (None, List.rev rstk @ s) in
@@ -887,17 +875,18 @@ let rec get_args n tys f e stk =
| Zshift k :: s ->
get_args n tys f (subs_shft (k,e)) s
| Zapp l :: s ->
- let na = List.length l in
+ let na = Array.length l in
if n == na then
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e l in
+ let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e l in
(Inl e',s)
else if n < na then (* more arguments *)
- let (args,eargs) = list_chop n l in
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e args in
+ let args = Array.sub l 0 n in
+ let eargs = Array.sub l n (na-n) in
+ let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e args in
(Inl e', Zapp eargs :: s)
else (* more lambdas *)
let (_,etys) = list_chop na tys in
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e l in
+ let e' = Array.fold_left (fun e arg -> subs_cons(arg,e)) e l in
get_args (n-na) etys f e' s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
@@ -907,7 +896,7 @@ let rec get_args n tys f e stk =
let rec reloc_rargs_rec depth stk =
match stk with
Zapp args :: s ->
- Zapp (lift_fconstr_list depth args) :: reloc_rargs_rec depth s
+ Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s
| Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
| _ -> stk
@@ -917,12 +906,12 @@ let reloc_rargs depth stk =
let rec drop_parameters depth n stk =
match stk with
Zapp args::s ->
- let q = List.length args in
+ let q = Array.length args in
if n > q then drop_parameters depth (n-q) s
else if n = q then reloc_rargs depth s
else
- let aft = list_skipn n args in
- reloc_rargs depth (append_stack_list (aft,s))
+ let aft = Array.sub args n (q-n) in
+ reloc_rargs depth (append_stack aft s)
| Zshift(k)::s -> drop_parameters (depth-k) n s
| [] -> assert (n=0); []
| _ -> assert false (* we know that n < stack_args_size(stk) *)
@@ -1055,7 +1044,6 @@ let rec zip_term zfun m stk =
match stk with
| [] -> m
| Zapp args :: s ->
- let args = Array.of_list args in
zip_term zfun (mkApp(m, Array.map zfun args)) s
| Zcase(ci,p,br)::s ->
let t = mkCase(ci, zfun p, m, Array.map zfun br) in
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 4c0f9d32e..88f9139e6 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -91,33 +91,6 @@ val info_flags: 'a infos -> reds
val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
(************************************************************************)
-(*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_member =
- | Zapp of 'a list
- | Zcase of case_info * 'a * 'a array
- | Zfix of 'a * 'a stack
- | Zshift of int
- | Zupdate of 'a
-
-and 'a stack = 'a stack_member list
-
-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
-val zip_term : ('a -> constr) -> constr -> 'a stack -> constr
-
-(************************************************************************)
(*s Lazy reduction. *)
(* [fconstr] is the type of frozen constr *)
@@ -146,17 +119,43 @@ type fterm =
| FCLOS of constr * fconstr subs
| FLOCKED
+(************************************************************************)
+(*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_member =
+ | Zapp of fconstr array
+ | Zcase of case_info * fconstr * fconstr array
+ | Zfix of fconstr * stack
+ | Zshift of int
+ | Zupdate of fconstr
+
+and stack = stack_member list
+
+val empty_stack : stack
+val append_stack : fconstr array -> stack -> stack
+
+val decomp_stack : stack -> (fconstr * stack) option
+val array_of_stack : stack -> fconstr array
+val stack_assign : stack -> int -> fconstr -> stack
+val stack_args_size : stack -> int
+val stack_tail : int -> stack -> stack
+val stack_nth : stack -> int -> fconstr
+val zip_term : (fconstr -> constr) -> constr -> stack -> constr
+
(* To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
a reduction function *)
val inject : constr -> fconstr
+(* mk_atom: prevents a term from being evaluated *)
+val mk_atom : constr -> fconstr
+
val fterm_of : fconstr -> fterm
val term_of_fconstr : fconstr -> constr
val destFLambda :
(fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
-(* mk_atom: prevents a term from being evaluated *)
-val mk_atom : constr -> fconstr
(* Global and local constant cache *)
type clos_infos
@@ -173,7 +172,7 @@ val whd_val : clos_infos -> fconstr -> constr
(* [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
- clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+ clos_infos -> fconstr -> stack -> fconstr * stack
(* Conversion auxiliary functions to do step by step normalisation *)
@@ -195,8 +194,8 @@ val mk_clos_deep :
(fconstr subs -> constr -> fconstr) ->
fconstr subs -> constr -> fconstr
-val kni: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
-val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+val kni: clos_infos -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4aa7c5753..e72942608 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -41,8 +41,8 @@ let compare_stack_shape stk1 stk2 =
([],[]) -> bal=0
| ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
| (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
- | (Zapp l1::s1, _) -> compare_rec (bal+List.length l1) s1 stk2
- | (_, Zapp l2::s2) -> compare_rec (bal-List.length l2) stk1 s2
+ | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
+ | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
| (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2
| (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
@@ -50,6 +50,16 @@ let compare_stack_shape stk1 stk2 =
| (_,_) -> false in
compare_rec 0 stk1 stk2
+type lft_constr_stack_elt =
+ Zlapp of (lift * fconstr) array
+ | Zlfix of (lift * fconstr) * lft_constr_stack
+ | Zlcase of case_info * lift * fconstr * fconstr array
+and lft_constr_stack = lft_constr_stack_elt list
+
+let rec zlapp v = function
+ Zlapp v2 :: s -> zlapp (Array.append v v2) s
+ | s -> Zlapp v :: s
+
let pure_stack lfts stk =
let rec pure_rec lfts stk =
match stk with
@@ -58,15 +68,13 @@ let pure_stack lfts stk =
(match (zi,pure_rec lfts s) with
(Zupdate _,lpstk) -> lpstk
| (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
- | (Zapp a1,(l,Zapp a2::pstk)) ->
- (l,Zapp (List.map (fun t -> (l,t)) a1 @ a2)::pstk)
| (Zapp a, (l,pstk)) ->
- (l,Zapp (List.map (fun t -> (l,t)) a)::pstk)
+ (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
| (Zfix(fx,a),(l,pstk)) ->
let (lfx,pa) = pure_rec l a in
- (l, Zfix((lfx,fx),pa)::pstk)
+ (l, Zlfix((lfx,fx),pa)::pstk)
| (Zcase(ci,p,br),(l,pstk)) ->
- (l,Zcase(ci,(l,p),Array.map (fun t -> (l,t)) br)::pstk)) in
+ (l,Zlcase(ci,l,p,br)::pstk)) in
snd (pure_rec lfts stk)
(****************************************************************************)
@@ -98,10 +106,10 @@ let whd_betadeltaiota_nolet env t =
let beta_appvect c v =
let rec stacklam env t stack =
- match (decomp_stack stack,kind_of_term t) with
- | Some (h,stacktl), Lambda (_,_,c) -> stacklam (h::env) c stacktl
- | _ -> app_stack (substl env t, stack) in
- stacklam [] c (append_stack v empty_stack)
+ match kind_of_term t, stack with
+ Lambda(_,_,c), arg::stacktl -> stacklam (arg::env) c stacktl
+ | _ -> applist (substl env t, stack) in
+ stacklam [] c (Array.to_list v)
(********************************************************************)
(* Conversion *)
@@ -117,17 +125,17 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
let rec cmp_rec pstk1 pstk2 cuniv =
match (pstk1,pstk2) with
| (z1::s1, z2::s2) ->
- let c1 = cmp_rec s1 s2 cuniv in
+ let cu1 = cmp_rec s1 s2 cuniv in
(match (z1,z2) with
- | (Zapp a1,Zapp a2) -> List.fold_right2 f a1 a2 c1
- | (Zfix(fx1,a1),Zfix(fx2,a2)) ->
- let c2 = f fx1 fx2 c1 in
- cmp_rec a1 a2 c2
- | (Zcase(ci1,p1,br1),Zcase(ci2,p2,br2)) ->
+ | (Zlapp a1,Zlapp a2) -> array_fold_right2 f a1 a2 cu1
+ | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
+ let cu2 = f fx1 fx2 cu1 in
+ cmp_rec a1 a2 cu2
+ | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
if not (fmind ci1.ci_ind ci2.ci_ind) then
raise NotConvertible;
- let c2 = f p1 p2 c1 in
- array_fold_right2 f br1 br2 c2
+ let cu2 = f (l1,p1) (l2,p2) cu1 in
+ array_fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2
| _ -> assert false)
| _ -> cuniv in
if compare_stack_shape stk1 stk2 then
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9f4f1def1..923903bdb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -11,9 +11,9 @@
open Util
open Names
open Term
+open Closure
open Reduction
open Reductionops
-open Closure
open Environ
open Typing
open Classops
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9a0125025..2a5fba859 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -23,6 +23,91 @@ open Reduction
exception Elimconst
+
+(**********************************************************************)
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts) *)
+
+type 'a stack_member =
+ | Zapp of 'a list
+ | Zcase of case_info * 'a * 'a array
+ | Zfix of 'a * 'a stack
+ | Zshift of int
+ | Zupdate of 'a
+
+and 'a stack = 'a stack_member list
+
+let empty_stack = []
+let append_stack_list = function
+ | ([],s) -> s
+ | (l1, Zapp l :: s) -> Zapp (l1@l) :: s
+ | (l1, s) -> Zapp l1 :: s
+let append_stack v s = append_stack_list (Array.to_list v, s)
+
+(* Collapse the shifts in the stack *)
+let zshift n s =
+ match (n,s) with
+ (0,_) -> s
+ | (_,Zshift(k)::s) -> Zshift(n+k)::s
+ | _ -> Zshift(n)::s
+
+let rec stack_args_size = function
+ | Zapp l::s -> List.length l + stack_args_size s
+ | Zshift(_)::s -> stack_args_size s
+ | Zupdate(_)::s -> stack_args_size s
+ | _ -> 0
+
+(* When used as an argument stack (only Zapp can appear) *)
+let rec decomp_stack = function
+ | Zapp[v]::s -> Some (v, s)
+ | Zapp(v::l)::s -> Some (v, (Zapp l :: s))
+ | Zapp [] :: s -> decomp_stack s
+ | _ -> None
+let rec decomp_stackn = function
+ | Zapp [] :: s -> decomp_stackn s
+ | Zapp l :: s -> (Array.of_list l, s)
+ | _ -> assert false
+let array_of_stack s =
+ let rec stackrec = function
+ | [] -> []
+ | Zapp args :: s -> args :: (stackrec s)
+ | _ -> assert false
+ in Array.of_list (List.concat (stackrec s))
+let rec list_of_stack = function
+ | [] -> []
+ | Zapp args :: s -> args @ (list_of_stack s)
+ | _ -> assert false
+let rec app_stack = function
+ | f, [] -> f
+ | f, (Zapp [] :: s) -> app_stack (f, s)
+ | f, (Zapp args :: s) ->
+ app_stack (applist (f, args), s)
+ | _ -> assert false
+let rec stack_assign s p c = match s with
+ | Zapp args :: s ->
+ let q = List.length args in
+ if p >= q then
+ Zapp args :: stack_assign s (p-q) c
+ else
+ (match list_chop p args with
+ (bef, _::aft) -> Zapp (bef@c::aft) :: s
+ | _ -> assert false)
+ | _ -> s
+let rec stack_tail p s =
+ if p = 0 then s else
+ match s with
+ | Zapp args :: s ->
+ let q = List.length args in
+ if p >= q then stack_tail (p-q) s
+ else Zapp (list_skipn p args) :: s
+ | _ -> failwith "stack_tail"
+let rec stack_nth s p = match s with
+ | Zapp args :: s ->
+ let q = List.length args in
+ if p >= q then stack_nth s (p-q)
+ else List.nth args p
+ | _ -> raise Not_found
+
+(**************************************************************)
(* The type of (machine) states (= lambda-bar-calculus' cuts) *)
type state = constr * constr stack
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index e19ab9aa4..915b5fb2c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -21,6 +21,34 @@ 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 'a stack_member =
+ | Zapp of 'a list
+ | Zcase of case_info * 'a * 'a array
+ | Zfix of 'a * 'a stack
+ | Zshift of int
+ | Zupdate of 'a
+
+and 'a stack = 'a stack_member list
+
+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
+
+(************************************************************************)
+
type state = constr * constr stack
type contextual_reduction_function = env -> evar_map -> constr -> constr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4e9a36f2e..d79295c0b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -18,8 +18,8 @@ open Termops
open Declarations
open Inductive
open Environ
-open Reductionops
open Closure
+open Reductionops
open Cbv
open Rawterm
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 00:21:45 +0000