diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 239 |
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 |