summaryrefslogtreecommitdiff
path: root/kernel/closure.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /kernel/closure.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'kernel/closure.ml')
-rw-r--r--kernel/closure.ml239
1 files changed, 108 insertions, 131 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 8e16a922..617611bf 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: closure.ml 8802 2006-05-10 20:47:28Z barras $ *)
open Util
open Pp
@@ -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. *)
@@ -554,7 +545,7 @@ let rec lft_fconstr n ft =
| FFix(fx,e) -> {norm=Cstr; term=FFix(fx,subs_shft(n,e))}
| FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))}
| FLIFT(k,m) -> lft_fconstr (n+k) m
- | FLOCKED -> anomaly "lft_constr found locked term"
+ | FLOCKED -> assert false
| _ -> {norm=ft.norm; term=FLIFT(n,ft)}
let lift_fconstr k f =
if k=0 then f else lft_fconstr k f
@@ -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 =
@@ -654,9 +645,9 @@ and compact_v acc s v k i =
let optimise_closure env c =
if is_subs_id env then (env,c) else
let (c',(_,s)) = compact_constr (0,[]) c 1 in
- let env' = List.fold_left
- (fun subs i -> subs_cons (clos_rel env i, subs)) (ESID 0) s in
- (env',c')
+ let env' =
+ Array.map (fun i -> clos_rel env i) (Array.of_list s) in
+ (subs_cons (env', ESID 0),c')
let mk_lambda env t =
let (env,t) = optimise_closure env t in
@@ -772,8 +763,7 @@ let rec to_constr constr_fun lfts v =
let fr = mk_clos2 env t in
let unfv = update v (fr.norm,fr.term) in
to_constr constr_fun lfts unfv
- | FLOCKED -> (*anomaly "Closure.to_constr: found locked term"*)
-mkVar(id_of_string"_LOCK_")
+ | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*)
(* This function defines the correspondance between constr and
fconstr. When we find a closure whose substitution is the identity,
@@ -802,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 ->
@@ -842,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
@@ -888,18 +875,15 @@ 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
- if n == na then
- let e' = List.fold_left (fun e arg -> subs_cons(arg,e)) e l in
- (Inl e',s)
+ let na = Array.length l in
+ if n == na then (Inl (subs_cons(l,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
- (Inl e', Zapp eargs :: s)
+ let args = Array.sub l 0 n in
+ let eargs = Array.sub l n (na-n) in
+ (Inl (subs_cons(args,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
- get_args (n-na) etys f e' s
+ let etys = list_skipn na tys in
+ get_args (n-na) etys f (subs_cons(l,e)) s
| _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk)
@@ -908,7 +892,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
@@ -918,12 +902,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) *)
@@ -949,15 +933,9 @@ let contract_fix_vect fix =
(bds.(i),
(fun j -> { norm = Cstr; term = FCoFix ((j,rdcl),env) }),
env, Array.length bds)
- | _ -> anomaly "Closure.contract_fix_vect: not a (co)fixpoint"
+ | _ -> assert false
in
- let rec subst_bodies_from_i i env =
- if i = nfix then
- (env, thisbody)
- else
- subst_bodies_from_i (i+1) (subs_cons (make_body i, env))
- in
- subst_bodies_from_i 0 env
+ (subs_cons(Array.init nfix make_body, env), thisbody)
(*********************************************************************)
@@ -969,7 +947,7 @@ let rec knh m stk =
match m.term with
| FLIFT(k,a) -> knh a (zshift k stk)
| FCLOS(t,e) -> knht e t (zupdate m stk)
- | FLOCKED -> anomaly "Closure.knh: found lock"
+ | FLOCKED -> assert false
| FApp(a,b) -> knh a (append_stack b (zupdate m stk))
| FCases(ci,p,t,br) -> knh t (Zcase(ci,p,br)::zupdate m stk)
| FFix(((ri,n),(_,_,_)),_) ->
@@ -1037,7 +1015,7 @@ let rec knr info m stk =
knit info fxe fxbd (args@stk')
| (_,args,s) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
- knit info (subs_cons(v,e)) bd stk
+ knit info (subs_cons([|v|],e)) bd stk
| _ -> (m,stk)
(* Computes the weak head normal form of a term *)
@@ -1056,7 +1034,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