aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vmvalues.ml')
-rw-r--r--kernel/vmvalues.ml118
1 files changed, 54 insertions, 64 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index de604176cb..0678f37a0b 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -34,8 +34,6 @@ let crazy_val = (val_of_obj (Obj.repr 0))
type tag = int
-let accu_tag = 0
-
let type_atom_tag = 2
let max_atom_tag = 2
let proj_tag = 3
@@ -166,7 +164,6 @@ let cofix_upd_val v = (Obj.magic v : values)
type vm_env
type vm_global
let fun_env v = (Obj.magic v : vm_env)
-let fix_env v = (Obj.magic v : vm_env)
let cofix_env v = (Obj.magic v : vm_env)
let cofix_upd_env v = (Obj.magic v : vm_env)
type vstack = values array
@@ -207,13 +204,13 @@ type vswitch = {
(* dom : values, codom : vfun *)
(* *)
(* + Functions have two representations : *)
-(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *)
+(* - unapplied fun : vf = Ct_[ C | envofs=2 | fv1 | ... | fvn] *)
(* C:tcode, fvi : values *)
(* Remark : a function and its environment is the same value. *)
-(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *)
+(* - partially applied fun : Ct_[ Restart::C | envofs=2 | vf | arg1 | ... | argn] *)
(* *)
(* + Fixpoints : *)
-(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *)
+(* - Ct_[C1|envofs1=3*n-1 | Infix_t|C2|envofs2 | ... | Infix_t|Cn|envofsn=2 | fv1|...|fvn] *)
(* One single block to represent all of the fixpoints, each fixpoint *)
(* is the pointer to the field holding the pointer to its code, and *)
(* the infix tag is used to know where the block starts. *)
@@ -226,13 +223,12 @@ type vswitch = {
(* + Cofixpoints : see cbytegen.ml *)
(* *)
(* + vblock's encode (non constant) constructors as in Ocaml, but *)
-(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *)
-(* accumulators. *)
+(* starting from 0 up. *)
(* *)
(* + vm_env is the type of the machine environments (i.e. a function or *)
(* a fixpoint) *)
(* *)
-(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
+(* + Accumulators : At_[accumulate | envofs=2 | accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *)
(* -- 10_[accu|proj name] : a projection blocked by an accu *)
@@ -291,10 +287,10 @@ type whd =
| Vuniv_level of Univ.Level.t
(* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let nargs : arguments -> int = fun args -> Obj.size (Obj.repr args) - 3
let arg args i =
if 0 <= i && i < (nargs args) then
- val_of_obj (Obj.field (Obj.repr args) (i+2))
+ val_of_obj (Obj.field (Obj.repr args) (i + 3))
else invalid_arg
("Vm.arg size = "^(string_of_int (nargs args))^
" acces "^(string_of_int i))
@@ -329,9 +325,9 @@ let uni_lvl_val (v : values) : Univ.Level.t =
let rec whd_accu a stk =
let stk =
- if Int.equal (Obj.size a) 2 then stk
+ if Int.equal (Obj.size a) 3 then stk
else Zapp (Obj.obj a) :: stk in
- let at = Obj.field a 1 in
+ let at = Obj.field a 2 in
match Obj.tag at with
| i when Int.equal i type_atom_tag ->
begin match stk with
@@ -356,7 +352,7 @@ let rec whd_accu a stk =
| i when Int.equal i fix_app_tag ->
let fa = Obj.field at 1 in
let zfix =
- Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
+ Zfix (Obj.obj (Obj.field fa 2), Obj.obj fa) in
whd_accu (Obj.field at 0) (zfix :: stk)
| i when Int.equal i switch_tag ->
let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
@@ -392,29 +388,28 @@ external accumulate : unit -> tcode = "accumulate_code"
external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field"
let accumulate = accumulate ()
-let whd_val : values -> whd =
- fun v ->
- let o = Obj.repr v in
- if Obj.is_int o then Vconstr_const (Obj.obj o)
+let whd_val (v: values) =
+ let o = Obj.repr v in
+ if Obj.is_int o then Vconstr_const (Obj.obj o)
+ else
+ let tag = Obj.tag o in
+ if Int.equal tag 0 then
+ if Int.equal (Obj.size o) 1 then
+ Varray (Obj.obj o)
+ else Vprod (Obj.obj o)
+ else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then
+ whd_accu o []
+ else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then
+ (match kind_of_closure o with
+ | 0 -> Vfun(Obj.obj o)
+ | 1 -> Vfix(Obj.obj o, None)
+ | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o))
+ | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+ | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
+ else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+ else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
else
- let tag = Obj.tag o in
- if tag = accu_tag then
- if Int.equal (Obj.size o) 1 then
- Varray(Obj.obj o)
- else if is_accumulate (fun_code o) then whd_accu o []
- else Vprod(Obj.obj o)
- else
- if tag = Obj.closure_tag || tag = Obj.infix_tag then
- (match kind_of_closure o with
- | 0 -> Vfun(Obj.obj o)
- | 1 -> Vfix(Obj.obj o, None)
- | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
- | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
- | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
- else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
- else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
- else
- Vconstr_block(Obj.obj o)
+ Vconstr_block (Obj.obj o)
(**********************************************)
(* Constructors *******************************)
@@ -422,9 +417,10 @@ let whd_val : values -> whd =
let obj_of_atom : atom -> Obj.t =
fun a ->
- let res = Obj.new_block accu_tag 2 in
+ let res = Obj.new_block Obj.closure_tag 3 in
set_bytecode_field res 0 accumulate;
- Obj.set_field res 1 (Obj.repr a);
+ Obj.set_field res 1 (Obj.repr 2);
+ Obj.set_field res 2 (Obj.repr a);
res
(* obj_of_str_const : structured_constant -> Obj.t *)
@@ -516,29 +512,23 @@ external closure_arity : vfun -> int = "coq_closure_arity"
(* Functions over fixpoint *)
-external offset : Obj.t -> int = "coq_offset"
-external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
-external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
+external current_fix : vfix -> int = "coq_current_fix"
+external shift_fix : vfix -> int -> vfix = "coq_shift_fix"
+external last_fix : vfix -> vfix = "coq_last_fix"
external tcode_array : tcode_array -> tcode array = "coq_tcode_array"
-let first o = (offset_closure o (offset o))
-let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix)
+let first_fix o = shift_fix o (- current_fix o)
+let fix_env v = (Obj.magic (last_fix v) : vm_env)
let last o = (Obj.field o (Obj.size o - 1))
let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
-let current_fix vf = - (offset (Obj.repr vf) / 2)
-
-let unsafe_fb_code fb i =
- let off = (2 * i) * (Sys.word_size / 8) in
- Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off))
-
-let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
+let unsafe_rec_arg fb i = int_tcode (Obj.magic (shift_fix fb i)) 1
let rec_args vf =
- let fb = first (Obj.repr vf) in
- let size = Obj.size (last fb) in
+ let fb = first_fix vf in
+ let size = Obj.size (last (Obj.repr fb)) in
Array.init size (unsafe_rec_arg fb)
exception FALSE
@@ -547,10 +537,10 @@ let check_fix f1 f2 =
let i1, i2 = current_fix f1, current_fix f2 in
(* Checking starting point *)
if i1 = i2 then
- let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
- let n = Obj.size (last fb1) in
+ let fb1,fb2 = first_fix f1, first_fix f2 in
+ let n = Obj.size (last (Obj.repr fb1)) in
(* Checking number of definitions *)
- if n = Obj.size (last fb2) then
+ if n = Obj.size (last (Obj.repr fb2)) then
(* Checking recursive arguments *)
try
for i = 0 to n - 1 do
@@ -593,21 +583,23 @@ let relaccu_code i =
let mk_fix_body k ndef fb =
let e = Obj.dup (Obj.repr fb) in
+ let env = Obj.repr (fix_env (Obj.obj e)) in
for i = 0 to ndef - 1 do
- set_bytecode_field e (2 * i) (relaccu_code (k + i))
+ set_bytecode_field e (3 * i) (relaccu_code (k + i))
done;
let fix_body i =
- let c = offset_tcode (unsafe_fb_code fb i) 2 in
- let res = Obj.new_block Obj.closure_tag 2 in
+ let c = offset_tcode (Obj.magic (shift_fix fb i)) 2 in
+ let res = Obj.new_block Obj.closure_tag 3 in
set_bytecode_field res 0 c;
- Obj.set_field res 1 (offset_closure e (2*i));
+ Obj.set_field res 1 (Obj.repr 2);
+ Obj.set_field res 2 env;
((Obj.obj res) : vfun) in
Array.init ndef fix_body
(* Functions over vcofix *)
let get_fcofix vcf i =
- match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
+ match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+2))) with
| Vcofix(vcfi, _, _) -> vcfi
| _ -> assert false
@@ -628,7 +620,7 @@ let check_cofix vcf1 vcf2 =
let mk_cofix_body apply_varray k ndef vcf =
let e = Obj.dup (Obj.repr vcf) in
for i = 0 to ndef - 1 do
- Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
+ Obj.set_field e (i+2) (Obj.repr (val_of_rel (k+i)))
done;
let cofix_body i =
@@ -636,9 +628,7 @@ let mk_cofix_body apply_varray k ndef vcf =
let c = Obj.field (Obj.repr vcfi) 0 in
Obj.set_field e 0 c;
let atom = Obj.new_block cofix_tag 1 in
- let self = Obj.new_block accu_tag 2 in
- set_bytecode_field self 0 accumulate;
- Obj.set_field self 1 (Obj.repr atom);
+ let self = obj_of_atom (Obj.obj atom) in
apply_varray (Obj.obj e) [|Obj.obj self|] in
Array.init ndef cofix_body
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:49:42 +0000