Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

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