package smtml

  1. Overview
  2. Docs

Source file num.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by the Smtml programmers *)

type t =
  | F32 of int32
  | F64 of int64

let type_of (n : t) =
  match n with F32 _ -> Ty.(Ty_fp 32) | F64 _ -> Ty.(Ty_fp 64)

(* Optimized mixer (DJB2 variant). Inlines to simple arithmetic. *)
let[@inline] combine h v = (h * 33) + v

let hash = function
  | F32 n -> combine 1 (Int32.hash n)
  | F64 n -> combine 2 (Int64.hash n)

let compare n1 n2 =
  match (n1, n2) with
  | F32 i1, F32 i2 ->
    Float.compare (Int32.float_of_bits i1) (Int32.float_of_bits i2)
  | F64 i1, F64 i2 ->
    Float.compare (Int64.float_of_bits i1) (Int64.float_of_bits i2)
  | F32 _, F64 _ -> -1
  | F64 _, _ -> 1

let equal (n1 : t) (n2 : t) : bool = compare n1 n2 = 0

let pp_num fmt = function
  | F32 f -> Fmt.pf fmt "(f32 %F)" (Int32.float_of_bits f)
  | F64 f -> Fmt.pf fmt "(f64 %F)" (Int64.float_of_bits f)

let pp_hex fmt = function
  | F32 f -> Fmt.pf fmt "(f32 0x%08lx)" f
  | F64 f -> Fmt.pf fmt "(f64 0x%016Lx)" f

let pp_no_type fmt = function
  | F32 f -> Fmt.pf fmt "%F" (Int32.float_of_bits f)
  | F64 f -> Fmt.pf fmt "%F" (Int64.float_of_bits f)

let pp_with ~printer fmt v =
  match printer with
  | Ty.Without_type -> pp_no_type fmt v
  | With_type -> pp_num fmt v
  | With_type_and_hexa_float -> pp_hex fmt v

let pp fmt v = pp_with ~printer:Without_type fmt v

let pp_safe fmt v = pp_with ~printer:With_type_and_hexa_float fmt v

let to_string (n : t) : string = Fmt.str "%a" pp n

let of_string (cast : Ty.t) value =
  match cast with
  | Ty_fp 32 -> (
    match float_of_string_opt value with
    | None -> Fmt.error_msg "invalid value %s, expected float" value
    | Some n -> Ok (F32 (Int32.bits_of_float n)) )
  | Ty_fp 64 -> (
    match float_of_string_opt value with
    | None -> Fmt.error_msg "invalid value %s, expected float" value
    | Some n -> Ok (F64 (Int64.bits_of_float n)) )
  | _ -> Fmt.error_msg "invalid value, expected num"

let to_json (n : t) : Yojson.Safe.t = `String (Fmt.str "%a" pp_no_type n)