amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8793 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 115 insertions, 2 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 9f4f1def13..923903bdbe 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 9a01250250..2a5fba8595 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 e19ab9aa4f..915b5fb2c7 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 4e9a36f2ed..d79295c0b1 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