diff options
Diffstat (limited to 'kernel/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index fe3c76c960..5acdd964b1 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -76,6 +76,8 @@ let rec eq_structured_values v1 v2 = Int.equal (Obj.size o1) (Obj.size o2) then if Int.equal t1 Obj.custom_tag then Int64.equal (Obj.magic v1 : int64) (Obj.magic v2 : int64) + else if Int.equal t1 Obj.double_tag + then Float64.(equal (of_float (Obj.magic v1)) (of_float (Obj.magic v2))) else begin assert (t1 <= Obj.last_non_constant_constructor_tag && t2 <= Obj.last_non_constant_constructor_tag); @@ -289,6 +291,7 @@ type whd = | Vconstr_const of int | Vconstr_block of vblock | Vint64 of int64 + | Vfloat64 of float | Vatom_stk of atom * stack | Vuniv_level of Univ.Level.t @@ -320,6 +323,7 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vconstr_const _i -> str "Vconstr_const" | Vconstr_block _b -> str "Vconstr_block" | Vint64 _ -> str "Vint64" + | Vfloat64 _ -> str "Vfloat64" | Vatom_stk (_a,_stk) -> str "Vatom_stk" | Vuniv_level _ -> assert false in @@ -379,6 +383,8 @@ let rec whd_accu a stk = end | i when Int.equal i Obj.custom_tag -> Vint64 (Obj.magic i) + | i when Int.equal i Obj.double_tag -> + Vfloat64 (Obj.magic i) | tg -> CErrors.anomaly Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg ++ str ".") @@ -408,6 +414,7 @@ let whd_val : values -> whd = | 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) @@ -681,6 +688,7 @@ and pr_whd w = | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" | Vconstr_block _b -> str "Vconstr_block" | Vint64 i -> i |> Format.sprintf "Vint64(%LiL)" |> str + | Vfloat64 f -> str "Vfloat64(" ++ str (Float64.(to_string (of_float f))) ++ str ")" | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = |