diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 40 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 9 |
2 files changed, 1 insertions, 48 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1f61bcae2e..196bb16f32 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -374,46 +374,6 @@ let rec stack_args_size = function | Zupdate(_)::s -> stack_args_size s | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 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))) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None -let array_of_stack s = - let rec stackrec = function - | [] -> [] - | Zapp args :: s -> args :: (stackrec s) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> 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) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s -let rec stack_tail p s = - if Int.equal 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 - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> 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) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> 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. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c2d53eed47..46be1bb279 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -123,8 +123,7 @@ type fterm = (*********************************************************************** 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 *) + [append_stack] one array at a time *) type stack_member = | Zapp of fconstr array @@ -139,13 +138,7 @@ 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 val eta_expand_stack : stack -> stack (** To lazy reduce a constr, create a [clos_infos] with |