diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | checker/analyze.ml | 34 | ||||
| -rw-r--r-- | checker/analyze.mli | 1 | ||||
| -rw-r--r-- | checker/validate.ml | 5 | ||||
| -rw-r--r-- | checker/values.ml | 12 | ||||
| -rw-r--r-- | checker/values.mli | 1 | ||||
| -rw-r--r-- | checker/votour.ml | 4 | ||||
| -rw-r--r-- | kernel/float64.ml | 11 | ||||
| -rw-r--r-- | kernel/float64.mli | 3 |
9 files changed, 64 insertions, 9 deletions
diff --git a/Makefile.build b/Makefile.build index ed4cde2b16..f9286c9635 100644 --- a/Makefile.build +++ b/Makefile.build @@ -566,7 +566,7 @@ $(FAKEIDEBYTE): $(FAKEIDECMO) | $(IDETOPBYTE) # votour: a small vo explorer (based on the checker) -VOTOURCMO:=clib/cObj.cmo kernel/uint63.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo +VOTOURCMO:=clib/cObj.cmo kernel/uint63.cmo kernel/float64.cmo checker/analyze.cmo checker/values.cmo checker/votour.cmo bin/votour: $(call bestobj, $(VOTOURCMO)) $(SHOW)'OCAMLBEST -o $@' diff --git a/checker/analyze.ml b/checker/analyze.ml index e145988b4f..4c06f1e250 100644 --- a/checker/analyze.ml +++ b/checker/analyze.ml @@ -107,6 +107,7 @@ end type repr = | RInt of int | RInt63 of Uint63.t +| RFloat64 of Float64.t | RBlock of (int * int) (* tag × len *) | RString of string | RPointer of int @@ -121,6 +122,7 @@ type data = type obj = | Struct of int * data array (* tag × data *) | Int63 of Uint63.t (* Primitive integer *) +| Float64 of Float64.t (* Primitive float *) | String of string module type Input = @@ -279,6 +281,25 @@ let input_intL chan : int64 = (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor (Int64.of_int p) +let input_double_big chan : float = + Int64.float_of_bits (input_intL chan) + +let input_double_little chan : float = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let ( lsl ) x y = Int64.(shift_left (of_int x) y) in + let ( lor ) = Int64.logor in + let bits = + (p lsl 56) lor (o lsl 48) lor (n lsl 40) lor (m lsl 32) lor + (l lsl 24) lor (k lsl 16) lor (j lsl 8) lor (Int64.of_int i) in + Int64.float_of_bits bits + let parse_object chan = let data = input_byte chan in if prefix_small_block <= data then @@ -326,9 +347,11 @@ let parse_object chan = | "_j" -> RInt63 (Uint63.of_int64 (input_intL chan)) | s -> Printf.eprintf "Unhandled custom code: %s" s; assert false end + | CODE_DOUBLE_BIG -> + RFloat64 (Float64.of_float (input_double_big chan)) + | CODE_DOUBLE_LITTLE -> + RFloat64 (Float64.of_float (input_double_little chan)) | CODE_DOUBLE_ARRAY32_LITTLE - | CODE_DOUBLE_BIG - | CODE_DOUBLE_LITTLE | CODE_DOUBLE_ARRAY8_BIG | CODE_DOUBLE_ARRAY8_LITTLE | CODE_DOUBLE_ARRAY32_BIG @@ -370,6 +393,11 @@ let parse chan = let () = LargeArray.set memory !current_object (Int63 i) in let () = incr current_object in data, None + | RFloat64 f -> + let data = Ptr !current_object in + let () = LargeArray.set memory !current_object (Float64 f) in + let () = incr current_object in + data, None in let rec fill block off accu = @@ -434,6 +462,7 @@ let instantiate (p, mem) = let obj = match LargeArray.get mem i with | Struct (tag, blk) -> Obj.new_block tag (Array.length blk) | Int63 i -> Obj.repr i + | Float64 f -> Obj.repr f | String str -> Obj.repr str in LargeArray.set ans i obj @@ -453,6 +482,7 @@ let instantiate (p, mem) = Obj.set_field obj k (get_data blk.(k)) done | Int63 _ + | Float64 _ | String _ -> () done; get_data p diff --git a/checker/analyze.mli b/checker/analyze.mli index 029f595959..e579f4896d 100644 --- a/checker/analyze.mli +++ b/checker/analyze.mli @@ -8,6 +8,7 @@ type data = type obj = | Struct of int * data array (* tag × data *) | Int63 of Uint63.t (* Primitive integer *) +| Float64 of Float64.t (* Primitive float *) | String of string module LargeArray : diff --git a/checker/validate.ml b/checker/validate.ml index 178bb4c527..678af9f2d5 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -87,6 +87,7 @@ let rec val_gen v ctx o = match v with | Dyn -> val_dyn ctx o | Proxy { contents = v } -> val_gen v ctx o | Uint63 -> val_uint63 ctx o + | Float64 -> val_float64 ctx o (* Check that an object is a tuple (or a record). vs is an array of value representation for each field. Its size corresponds to the @@ -138,6 +139,10 @@ and val_uint63 ctx o = if not (Uint63.is_uint63 o) then fail ctx o "not a 63-bit unsigned integer" +and val_float64 ctx o = + if not (Float64.is_float64 o) then + fail ctx o "not a 64-bit float" + let print_frame = function | CtxType t -> t | CtxAnnot t -> t diff --git a/checker/values.ml b/checker/values.ml index 9a2028a96b..0cd63566d7 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -35,6 +35,7 @@ type value = | Proxy of value ref | Uint63 + | Float64 let fix (f : value -> value) : value = let self = ref Any in @@ -147,7 +148,8 @@ let rec v_constr = [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) - [|Uint63|] (* Int *) + [|Uint63|]; (* Int *) + [|Float64|] (* Int *) |]) and v_prec = Tuple ("prec_declaration", @@ -226,7 +228,7 @@ let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] let v_primitive = - v_enum "primitive" 25 + v_enum "primitive" 41 (* Number of "Primitive" in Int63.v and PrimFloat.v *) let v_cst_def = v_sum "constant_def" 0 @@ -300,9 +302,11 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Opt v_bool; v_typing_flags|] -let v_prim_ind = v_enum "prim_ind" 4 +let v_prim_ind = v_enum "prim_ind" 6 +(* Number of "Register ... as kernel.ind_..." in Int63.v and PrimFloat.v *) -let v_prim_type = v_enum "prim_type" 1 +let v_prim_type = v_enum "prim_type" 2 +(* Number of constructors of prim_type in "kernel/cPrimitives.ml" *) let v_retro_action = v_sum "retro_action" 0 [| diff --git a/checker/values.mli b/checker/values.mli index db6b0be250..ec3b91d5dd 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -39,6 +39,7 @@ type value = (** Same as the inner value, used to define recursive types *) | Uint63 + | Float64 (** NB: List and Opt have their own constructors to make it easy to define eg [let rec foo = List foo]. *) diff --git a/checker/votour.ml b/checker/votour.ml index 97584831e5..fe6c487496 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -101,6 +101,7 @@ struct in fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size) | Int63 _ -> k 0 + | Float64 _ -> k 0 | String s -> let size = 2 + (String.length s / ws) in let () = LargeArray.set !sizes p size in @@ -118,6 +119,7 @@ struct match LargeArray.get !memory p with | Struct (tag, os) -> BLOCK (tag, os) | Int63 _ -> OTHER (* TODO: pretty-print int63 values *) + | Float64 _ -> OTHER (* TODO: pretty-print float64 values *) | String s -> STRING s let input ch = @@ -156,6 +158,7 @@ let rec get_name ?(extra=false) = function |Dyn -> "<dynamic>" | Proxy v -> get_name ~extra !v | Uint63 -> "Uint63" + | Float64 -> "Float64" (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) @@ -261,6 +264,7 @@ let rec get_children v o pos = match v with |Fail s -> raise Forbidden | Proxy v -> get_children !v o pos | Uint63 -> raise Exit + | Float64 -> raise Exit let get_children v o pos = try get_children v o pos diff --git a/kernel/float64.ml b/kernel/float64.ml index c0611f37a0..72f0d83359 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -35,6 +35,9 @@ let abs = abs_float type float_comparison = FEq | FLt | FGt | FNotComparable +(* inspired by lib/util.ml; see also #10471 *) +let pervasives_compare = compare + let compare x y = if x < y then FLt else @@ -137,5 +140,9 @@ let hash = let total_compare f1 f2 = (* pervasives_compare considers all NaNs as equal, which is fine here, but also considers -0. and +0. as equal *) - if f1 = 0. && f2 = 0. then Util.pervasives_compare (1. /. f1) (1. /. f2) - else Util.pervasives_compare f1 f2 + if f1 = 0. && f2 = 0. then pervasives_compare (1. /. f1) (1. /. f2) + else pervasives_compare f1 f2 + +let is_float64 t = + Obj.tag t = Obj.double_tag +[@@ocaml.inline always] diff --git a/kernel/float64.mli b/kernel/float64.mli index 1e6ea8bb96..927594115e 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -87,3 +87,6 @@ val hash : t -> int (** Total order relation over float values. Behaves like [Pervasives.compare].*) val total_compare : t -> t -> int + +val is_float64 : Obj.t -> bool +[@@ocaml.inline always] |