Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 601 insertions, 0 deletions

diff --git a/kernel/vm.ml b/kernel/vm.ml
new file mode 100644
index 00000000..c8be979e
--- /dev/null
+++ b/kernel/vm.ml
@@ -0,0 +1,601 @@
+open Obj
+open Names
+open Term
+open Conv_oracle
+open Cbytecodes
+
+
+external set_drawinstr : unit -> unit = "coq_set_drawinstr"
+
+(******************************************)
+(* Fonctions en plus du module Obj ********)
+(******************************************)
+
+external offset_closure : t -> int -> t = "coq_offset_closure"
+external offset : t -> int = "coq_offset"
+let first o = (offset_closure o (offset o))
+let last o = (field o (size o - 1))
+
+let accu_tag = 0
+
+(*******************************************)
+(* Initalisation de la machine abstraite ***)
+(*******************************************)
+
+external init_vm : unit -> unit = "init_coq_vm"
+
+let _ = init_vm ()
+
+external transp_values : unit -> bool = "get_coq_transp_value"
+external set_transp_values : bool -> unit = "coq_set_transp_value"
+
+(*******************************************)
+(* Le code machine  ************************)
+(*******************************************)
+
+type tcode 
+let tcode_of_obj v = ((obj v):tcode)
+let fun_code v = tcode_of_obj (field (repr v) 0)
+
+external mkAccuCode : int -> tcode = "coq_makeaccu"
+external mkPopStopCode : int -> tcode = "coq_pushpop"
+external mkAccuCond : int -> tcode = "coq_accucond"
+
+external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
+external int_tcode : tcode -> int -> int = "coq_int_tcode"
+
+external accumulate : unit -> tcode = "accumulate_code"
+let accumulate = accumulate ()
+
+external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
+
+let popstop_tbl =  ref (Array.init 30 mkPopStopCode) 
+
+let popstop_code i =
+  let len = Array.length !popstop_tbl in
+  if i < len then !popstop_tbl.(i) 
+  else
+    begin
+      popstop_tbl :=
+	Array.init (i+10)
+	  (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j);
+      !popstop_tbl.(i) 
+    end
+
+let stop = popstop_code 0
+  
+(******************************************************)
+(* Types de donnees abstraites et fonctions associees *)
+(******************************************************)
+
+(* Values of the abstract machine *)
+let val_of_obj v = ((obj v):values)
+let crasy_val = (val_of_obj (repr 0))
+
+
+(* Functions *)
+type vfun  
+(* v = [Tc | c | fv1 | ... | fvn ] *)
+(*         ^                       *)
+(* [Tc | (Restart : c) | v | a1 | ... an] *)
+(*              ^                         *)
+
+(* Products *)
+type vprod 
+(* [0 | dom : codom] *) 
+(*     ^              *)
+let dom : vprod -> values = fun p -> val_of_obj (field (repr p) 0) 
+let codom : vprod -> vfun = fun p -> (obj (field (repr p) 1))
+
+(* Arguments *)
+type arguments 
+(* arguments = [_ | _ | _ | a1 | ... | an] *)
+(*                ^                        *)
+let nargs : arguments -> int = fun args -> (size (repr args)) - 2
+
+let unsafe_arg : arguments -> int -> values =
+     fun args i ->  val_of_obj (field (repr args) (i+2))
+
+let arg args i = 
+  if  0 <= i && i < (nargs args) then unsafe_arg args i 
+  else raise (Invalid_argument 
+		("Vm.arg size = "^(string_of_int (nargs args))^
+		 " acces "^(string_of_int i)))
+
+(* Fixpoints *)
+type vfix
+
+(* [Tc|c0|Ti|c1|...|Ti|cn|fv1|...|fvn| [ct0|...|ctn]] *)
+(*          ^                                         *)
+type vfix_block 
+
+let fix_init : vfix -> int = fun vf -> (offset (repr vf)/2)
+
+let block_of_fix : vfix -> vfix_block = fun vf -> obj (first (repr vf))
+
+let fix_block_type : vfix_block -> tcode array =
+  fun fb -> (obj (last (repr fb)))
+
+let fix_block_ndef : vfix_block -> int = 
+  fun fb -> size (last (repr fb))
+
+let fix_ndef vf = fix_block_ndef (block_of_fix vf)
+
+let unsafe_fb_code : vfix_block -> int -> tcode =
+  fun fb i -> tcode_of_obj (field (repr fb) (2 * i))
+
+let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
+  
+let rec_args vf =
+  let fb = block_of_fix vf in
+  let size = fix_block_ndef fb in
+  Array.init size (unsafe_rec_arg fb)
+
+exception FALSE
+
+let check_fix f1 f2 = 
+  let i1, i2 = fix_init f1, fix_init f2 in
+  (* Verification du point de depart *)
+    if i1 = i2 then
+      let fb1,fb2 = block_of_fix f1, block_of_fix f2 in
+      let n = fix_block_ndef fb1 in
+    (* Verification du nombre de definition *)
+      if n = fix_block_ndef fb2 then
+      (* Verification des arguments recursifs *)
+	try
+	  for i = 0 to n - 1 do
+	    if not (unsafe_rec_arg fb1 i = unsafe_rec_arg fb2 i) then
+	      raise FALSE
+	  done;
+	  true
+	with FALSE -> false
+      else false 
+    else false
+
+(* Partials applications of Fixpoints *)
+type vfix_app
+let fix : vfix_app -> vfix = 
+  fun vfa -> ((obj (field (repr vfa) 1)):vfix)
+let args_of_fix : vfix_app -> arguments =
+  fun vfa -> ((magic  vfa) : arguments)
+
+(* CoFixpoints *)
+type vcofix 
+type vcofix_block
+let cofix_init : vcofix -> int = fun vcf -> (offset (repr vcf)/2)
+
+let block_of_cofix : vcofix -> vcofix_block = fun vcf -> obj (first (repr vcf))
+
+let cofix_block_ndef : vcofix_block -> int = 
+  fun fb -> size (last (repr fb))
+
+let cofix_ndef vcf= cofix_block_ndef (block_of_cofix vcf)
+
+let cofix_block_type : vcofix_block -> tcode array =
+  fun cfb -> (obj (last (repr cfb)))
+
+let check_cofix cf1 cf2 = 
+  cofix_init cf1 = cofix_init cf2 &&
+  cofix_ndef cf1 = cofix_ndef cf2 
+
+let cofix_arity c = int_tcode c 1
+
+let unsafe_cfb_code : vcofix_block -> int -> tcode =
+  fun cfb i -> tcode_of_obj (field (repr cfb) (2 * i))
+
+(* Partials applications of CoFixpoints *)
+type vcofix_app 
+let cofix : vcofix_app -> vcofix = 
+  fun vcfa -> ((obj (field (repr vcfa) 1)):vcofix)
+let args_of_cofix : vcofix_app -> arguments = 
+  fun vcfa -> ((magic  vcfa) : arguments)
+
+(* Blocks *)
+type vblock (* la representation Ocaml *)
+let btag : vblock -> int = fun b -> tag (repr b)
+let bsize : vblock -> int = fun b -> size (repr b)
+let bfield b i =
+  if 0 <= i && i < (bsize b) then
+    val_of_obj (field (repr b) i)
+  else raise (Invalid_argument "Vm.bfield")
+
+(* Accumulators and atoms *)
+
+type accumulator 
+(* [Ta | accumulate | at | a1 | ... | an ] *)
+
+type inv_rel_key = int
+
+type id_key = inv_rel_key tableKey
+
+type vstack = values array
+
+type vm_env 
+
+type vswitch = {
+    sw_type_code : tcode; 
+    sw_code : tcode; 
+    sw_annot : annot_switch;
+    sw_stk : vstack;
+    sw_env : vm_env
+  } 
+
+(* Ne pas changer ce type sans modifier le code C *)
+type atom = 
+  | Aid of id_key
+  | Aiddef of id_key * values
+  | Aind of inductive
+  | Afix_app of accumulator * vfix_app
+  | Aswitch of accumulator * vswitch
+
+let atom_of_accu : accumulator -> atom =
+  fun a -> ((obj (field (repr a) 1)) : atom)
+
+let args_of_accu : accumulator -> arguments = 
+  fun a -> ((magic a) : arguments)
+
+let nargs_of_accu a = nargs (args_of_accu a)
+
+(* Les zippers *)
+
+type zipper =
+  | Zapp of arguments
+  | Zfix of vfix_app
+  | Zswitch of vswitch
+
+type stack = zipper list
+
+type whd =
+  | Vsort of sorts
+  | Vprod of vprod 
+  | Vfun of vfun
+  | Vfix of vfix
+  | Vfix_app of vfix_app
+  | Vcofix of vcofix
+  | Vcofix_app of vcofix_app
+  | Vconstr_const of int
+  | Vconstr_block of vblock
+  | Vatom_stk of atom * stack
+(* Les atomes sont forcement Aid Aiddef Aind *)
+
+(**********************************************)
+(* Constructeurs ******************************)
+(**********************************************)
+(* obj_of_atom : atom -> t *)
+let obj_of_atom : atom -> t =
+  fun a -> 
+    let res = Obj.new_block accu_tag 2 in
+    set_field res 0 (repr accumulate);
+    set_field res 1 (repr a);
+    res 
+
+(* obj_of_str_const : structured_constant -> t *)
+let rec obj_of_str_const str =
+  match str with 
+  | Const_sorts s -> repr (Vsort s)
+  | Const_ind ind -> obj_of_atom (Aind ind)
+  | Const_b0 tag -> repr tag
+  | Const_bn(tag, args) ->
+      let len = Array.length args in
+      let res = new_block tag len in
+      for i = 0 to len - 1 do 
+	set_field res i (obj_of_str_const args.(i)) 
+      done;
+      res
+
+let val_of_obj o = ((obj o) : values)
+
+let val_of_str_const str = val_of_obj (obj_of_str_const str)
+
+let val_of_atom a = val_of_obj (obj_of_atom a)
+
+let idkey_tbl = Hashtbl.create 31
+
+let val_of_idkey key =
+  try Hashtbl.find idkey_tbl key 
+  with Not_found -> 
+    let v = val_of_atom (Aid key) in
+    Hashtbl.add idkey_tbl key v;
+    v
+
+let val_of_rel k = val_of_idkey (RelKey k)
+let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v))
+
+let val_of_named id = val_of_idkey (VarKey id)
+let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v))
+  
+let val_of_constant c = val_of_idkey (ConstKey c)
+let val_of_constant_def n c v = 
+  let res = Obj.new_block accu_tag 2 in
+  set_field res 0 (repr (mkAccuCond n));
+  set_field res 1 (repr (Aiddef(ConstKey c, v)));
+  val_of_obj res 
+
+
+
+(*************************************************)
+(* Destructors ***********************************)
+(*************************************************)
+
+
+let rec whd_accu a stk =
+  let stk = 
+    if nargs_of_accu a = 0 then stk
+    else Zapp (args_of_accu a) :: stk in
+  let at = atom_of_accu a in 
+  match at with
+  | Aid _ | Aiddef _ | Aind _ -> Vatom_stk(at, stk)
+  | Afix_app(a,fa) -> whd_accu a (Zfix fa :: stk)
+  | Aswitch(a,sw) -> whd_accu a (Zswitch sw :: stk)
+
+external kind_of_closure : t -> int = "coq_kind_of_closure"
+
+let whd_val : values -> whd =
+  fun v -> 
+    let o = repr v in 
+    if is_int o then Vconstr_const (obj o)
+    else 
+      let tag = tag o in
+      if tag = accu_tag then
+	if is_accumulate (fun_code o) then whd_accu (obj o) []
+	else 
+	  if size o = 1 then Vsort(obj (field o 0))
+	  else Vprod(obj o)
+      else 
+	if tag = closure_tag || tag = infix_tag then
+	  match kind_of_closure o with
+	  | 0 -> Vfun(obj o)
+	  | 1 -> Vfix(obj o)
+	  | 2 -> Vfix_app(obj o) 
+	  | 3 -> Vcofix(obj o)
+	  | 4 -> Vcofix_app(obj o)
+	  | 5 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+	  | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work"
+	else Vconstr_block(obj o)
+	
+
+
+(************************************************)
+(* La machine abstraite *************************)
+(************************************************)
+
+
+(* gestion de la pile *)
+external push_ra : tcode -> unit = "coq_push_ra"
+external push_val : values -> unit = "coq_push_val"
+external push_arguments : arguments -> unit = "coq_push_arguments"
+external push_vstack : vstack -> unit = "coq_push_vstack"
+
+
+(* interpreteur *)
+external interprete : tcode -> values -> vm_env -> int -> values =
+  "coq_interprete_ml"
+
+let apply_arguments vf vargs =
+  let n = nargs vargs in
+  if n = 0 then vf 
+  else
+   begin
+     push_ra stop;
+     push_arguments vargs;
+     interprete (fun_code vf) vf (magic vf) (n - 1)
+   end
+
+let apply_vstack vf vstk =
+  let n = Array.length vstk in
+  if n = 0 then vf
+  else 
+    begin
+      push_ra stop;
+      push_vstack vstk;
+      interprete (fun_code vf) vf (magic vf) (n - 1)
+    end
+
+let apply_fix_app vfa arg =
+  let vf = fix vfa in
+  let vargs = args_of_fix vfa in
+  push_ra stop;
+  push_val arg;
+  push_arguments vargs;
+  interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs)
+
+external set_forcable : unit -> unit = "coq_set_forcable"
+let force_cofix v =
+  match whd_val v with
+  | Vcofix _    | Vcofix_app _ ->
+      push_ra stop;
+      set_forcable ();
+      interprete (fun_code v) (magic v) (magic v) 0
+  | _ -> v
+  
+let apply_switch sw arg =
+  let arg = force_cofix arg in
+  let tc = sw.sw_annot.tailcall in
+  if tc then 
+    (push_ra stop;push_vstack sw.sw_stk)
+  else 
+    (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk)));
+  interprete sw.sw_code arg sw.sw_env 0
+
+let is_accu v = 
+  is_block (repr v) && tag (repr v) = accu_tag && 
+  fun_code v == accumulate 
+
+let rec whd_stack v stk =  
+  match stk with
+  | [] -> whd_val v
+  | Zapp a :: stkt -> whd_stack (apply_arguments v a) stkt
+  | Zfix fa :: stkt -> 
+      if is_accu v then whd_accu (magic v) stk
+      else whd_stack (apply_fix_app fa v) stkt
+  | Zswitch sw :: stkt -> 
+      if is_accu v then whd_accu (magic v) stk 
+      else whd_stack (apply_switch sw v) stkt 
+
+let rec force_whd v stk =
+  match whd_stack v stk with
+  | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
+  | res -> res
+
+	  
+
+(* Function *)
+external closure_arity : vfun -> int = "coq_closure_arity"
+
+(* [apply_rel v k arity] applique la valeurs [v] aux arguments 
+   [k],[k+1], ... , [k+arity-1] *)
+let mkrel_vstack k arity =
+  let max = k + arity - 1 in
+  Array.init arity (fun i -> val_of_rel (max - i))
+
+let body_of_vfun k vf =
+  let vargs = mkrel_vstack k 1 in
+  apply_vstack (magic vf) vargs
+
+let decompose_vfun2 k vf1 vf2 =
+  let arity = min (closure_arity vf1) (closure_arity vf2) in
+  assert (0 <= arity && arity < Sys.max_array_length);
+  let vargs = mkrel_vstack k arity in
+  let v1 = apply_vstack (magic vf1) vargs in
+  let v2 = apply_vstack (magic vf2) vargs in
+  arity, v1, v2
+    
+  
+(* Fix *)
+external atom_rel : unit -> atom array = "get_coq_atom_tbl"
+external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
+
+let relaccu_tbl =  
+  let atom_rel = atom_rel() in
+  let len = Array.length atom_rel in
+  for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
+  ref (Array.init len mkAccuCode) 
+
+let relaccu_code i =
+  let len = Array.length !relaccu_tbl in
+  if i < len then !relaccu_tbl.(i) 
+  else
+    begin
+      realloc_atom_rel i;
+      let atom_rel = atom_rel () in
+      let nl = Array.length atom_rel in
+      for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
+      relaccu_tbl :=
+	Array.init nl
+	  (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
+      !relaccu_tbl.(i) 
+    end
+
+let jump_grabrec c = offset_tcode c 2
+let jump_grabrecrestart c = offset_tcode c 3
+
+let bodies_of_fix k vf = 
+  let fb = block_of_fix vf in
+  let ndef = fix_block_ndef fb in
+  (* Construction de l' environnement des corps des points fixes *)
+  let e = dup (repr fb) in
+  for i = 0 to ndef - 1 do
+    set_field e (2 * i) (repr (relaccu_code (k + i)))
+  done;
+  let fix_body i =
+    let c = jump_grabrec (unsafe_fb_code fb i)  in
+    let res = Obj.new_block closure_tag 2 in
+    set_field res 0 (repr c);
+    set_field res 1 (offset_closure e (2*i));
+    ((obj res) : vfun)
+  in Array.init ndef fix_body
+ 
+let types_of_fix vf =
+  let fb = block_of_fix vf in
+  let type_code = fix_block_type fb in
+  let type_val c = interprete c crasy_val (magic fb) 0 in
+  Array.map type_val type_code
+
+ 
+(* CoFix *)
+let jump_cograb c = offset_tcode c 2
+let jump_cograbrestart c = offset_tcode c 3 
+
+let bodies_of_cofix k vcf =
+  let cfb = block_of_cofix vcf in
+  let ndef = cofix_block_ndef cfb in
+  (* Construction de l' environnement des corps des cofix *)
+  let e = dup (repr cfb) in
+  for i = 0 to ndef - 1 do
+    set_field e (2 * i) (repr (relaccu_code (k + i)))
+  done;
+  let cofix_body i =
+    let c = unsafe_cfb_code cfb i in 
+    let arity = int_tcode c 1 in
+    if arity = 0 then 
+      begin
+	push_ra stop;
+	interprete (jump_cograbrestart c) crasy_val 
+	  (obj (offset_closure e (2*i))) 0
+      end
+    else 
+      let res = Obj.new_block closure_tag 2 in
+      set_field res 0 (repr (jump_cograb c));
+      set_field res 1 (offset_closure e (2*i));
+      ((obj res) : values)
+  in Array.init ndef cofix_body
+
+let types_of_cofix vcf =
+  let cfb = block_of_cofix vcf in
+  let type_code = cofix_block_type cfb in
+  let type_val c = interprete c crasy_val (magic cfb) 0 in
+  Array.map type_val type_code
+
+(* Switch *)
+      
+let eq_tbl sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl 
+    
+let case_info sw = sw.sw_annot.ci
+    
+let type_of_switch sw = 
+  push_vstack sw.sw_stk;
+  interprete sw.sw_type_code crasy_val sw.sw_env 0 
+    
+let branch_arg k (tag,arity) = 
+  if arity = 0 then  ((magic tag):values)
+  else
+    let b = new_block tag arity in
+    for i = 0 to arity - 1 do
+      set_field b i (repr (val_of_rel (k+i)))
+    done;
+    val_of_obj b
+  
+      
+let branch_of_switch k sw =
+  let eval_branch (_,arity as ta) =
+    let arg = branch_arg k ta in
+    let v = apply_switch sw arg in
+    (arity, v)
+  in 
+  Array.map eval_branch sw.sw_annot.rtbl
+    
+
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+