🧮 Saturation_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Definition t : Set := int.
Parameter mul_safe : Set.
Parameter may_saturate : Set.
Definition may_saturate_value (x_value : t) : t := x_value.
Definition to_int {A : Set} (x_value : A) : A := x_value.
Definition op_lt : t → t → bool := Compare.Int.op_lt.
Definition op_lteq : t → t → bool := Compare.Int.op_lteq.
Definition op_gt : t → t → bool := Compare.Int.op_gt.
Definition op_gteq : t → t → bool := Compare.Int.op_gteq.
Definition op_eq : t → t → bool := Compare.Int.op_eq.
Definition equal : t → t → bool := op_eq.
Definition op_ltgt : t → t → bool := Compare.Int.op_ltgt.
Definition max (x_value : t) (y_value : t) : t :=
if op_gteq x_value y_value then
x_value
else
y_value.
Definition min (x_value : t) (y_value : t) : t :=
if op_gteq x_value y_value then
y_value
else
x_value.
Definition compare : t → t → t := Compare.Int.compare.
Definition saturated : int := Pervasives.max_int.
Definition op_gtexclamation : t → int → bool := Compare.Int.op_gt.
Definition of_int_opt (t_value : int) : option int :=
if (op_gteq t_value 0) && (op_lt t_value saturated) then
Some t_value
else
None.
Definition of_z_opt (z_value : Z.t) : option int :=
let 'int_value := Z.to_int z_value in
of_int_opt int_value.
Definition to_z (x_value : int) : Z.t := Z.of_int x_value.
Definition saturate_if_undef (function_parameter : option int) : int :=
match function_parameter with
| None ⇒ saturated
| Some x_value ⇒ x_value
end.
Definition safe_int (x_value : int) : int :=
saturate_if_undef (of_int_opt x_value).
Definition numbits (x_value : int) : int :=
let x_value : Pervasives.ref int :=
Pervasives.ref_value x_value
in let n_value : Pervasives.ref int :=
Pervasives.ref_value 0 in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 32 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value
((Pervasives.op_exclamation n_value) +i 32) in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 16 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value
((Pervasives.op_exclamation n_value) +i 16) in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 8 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 8)
in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 4 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 4)
in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 2 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 2)
in
Pervasives.op_coloneq x_value y_value
else
tt in
if op_ltgt (Pervasives.lsr (Pervasives.op_exclamation x_value) 1) 0 then
(Pervasives.op_exclamation n_value) +i 2
else
(Pervasives.op_exclamation n_value) +i (Pervasives.op_exclamation x_value).
Definition zero : int := 0.
Definition one : int := 1.
Definition small_enough (z_value : int) : bool :=
op_eq (Pervasives.land z_value (-2147483648)) 0.
Definition mul_safe_value (x_value : int) : option int :=
if small_enough x_value then
Some x_value
else
None.
Definition mul_safe_exn (x_value : int) : int :=
if small_enough x_value then
x_value
else
Pervasives.failwith
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "mul_safe_exn: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" must be below 2147483648"
CamlinternalFormatBasics.End_of_format)))
"mul_safe_exn: %d must be below 2147483648") x_value).
Definition mul_safe_of_int_exn (x_value : int) : int :=
(fun (function_parameter : option int) ⇒
match function_parameter with
| None ⇒
Pervasives.failwith
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "mul_safe_of_int_exn: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" must be below 2147483648"
CamlinternalFormatBasics.End_of_format)))
"mul_safe_of_int_exn: %d must be below 2147483648") x_value)
| Some x_value ⇒ x_value
end) (Option.bind (of_int_opt x_value) mul_safe_value).
Definition shift_right (x_value : int) (y_value : int) : int :=
Pervasives.lsr x_value y_value.
Definition shift_left (x_value : int) (y_value : int) : int :=
if op_lt (shift_right saturated y_value) x_value then
saturated
else
Pervasives.lsl x_value y_value.
Definition mul (x_value : int) (y_value : int) : int :=
match x_value with
| 0 ⇒ 0
| x_value ⇒
if (small_enough x_value) && (small_enough y_value) then
x_value ×i y_value
else
if y_value >i (saturated /i x_value) then
saturated
else
x_value ×i y_value
end.
Definition mul_fast (x_value : int) (y_value : int) : int := x_value ×i y_value.
Definition scale_fast (x_value : int) (y_value : int) : int :=
if op_eq x_value 0 then
0
else
if small_enough y_value then
x_value ×i y_value
else
if y_value >i (saturated /i x_value) then
saturated
else
x_value ×i y_value.
Definition add (x_value : int) (y_value : int) : int :=
let z_value := x_value +i y_value in
if z_value ≥i 0 then
z_value
else
saturated.
Definition succ (x_value : int) : int := add one x_value.
Definition sub (x_value : int) (y_value : int) : int :=
Compare.Int.max (x_value -i y_value) 0.
Definition sub_opt (x_value : int) (y_value : int) : option int :=
let s_value := x_value -i y_value in
if s_value ≥i 0 then
Some s_value
else
None.
Definition erem (x_value : int) (y_value : int) : int :=
Pervasives._mod x_value y_value.
Definition ediv (x_value : int) (y_value : int) : int := x_value /i y_value.
Definition sqrt (x_value : int) : int :=
saturate_if_undef
(Option.map (fun (x_value : int) ⇒ Z.to_int (Z.sqrt (Z.of_int x_value)))
(of_int_opt x_value)).
Definition t_to_z_exn (z_value : Z.t) : int :=
match of_z_opt z_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert int false
| Some x_value ⇒ x_value
end.
Definition z_encoding : Data_encoding.encoding int :=
Data_encoding.check_size 9
(Data_encoding.conv to_z t_to_z_exn None Data_encoding.z_value).
Definition n_encoding : Data_encoding.encoding int :=
Data_encoding.check_size 9
(Data_encoding.conv to_z t_to_z_exn None Data_encoding.n_value).
Definition pp (fmt : Format.formatter) (x_value : int) : unit :=
Format.pp_print_int fmt x_value.
Module Syntax.
Definition log2 (x_value : int) : int := safe_int (1 +i (numbits x_value)).
Definition sqrt : int → int := sqrt.
Definition op_plus : int → int → int := add.
Definition op_minus : int → int → int := sub.
Definition op_star : int → int → int := mul.
Definition op_lt : t → t → bool := op_lt.
Definition op_eq : t → t → bool := op_eq.
Definition lsr : int → int → int := shift_right.
Definition lsl : int → int → int := shift_left.
End Syntax.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Definition t : Set := int.
Parameter mul_safe : Set.
Parameter may_saturate : Set.
Definition may_saturate_value (x_value : t) : t := x_value.
Definition to_int {A : Set} (x_value : A) : A := x_value.
Definition op_lt : t → t → bool := Compare.Int.op_lt.
Definition op_lteq : t → t → bool := Compare.Int.op_lteq.
Definition op_gt : t → t → bool := Compare.Int.op_gt.
Definition op_gteq : t → t → bool := Compare.Int.op_gteq.
Definition op_eq : t → t → bool := Compare.Int.op_eq.
Definition equal : t → t → bool := op_eq.
Definition op_ltgt : t → t → bool := Compare.Int.op_ltgt.
Definition max (x_value : t) (y_value : t) : t :=
if op_gteq x_value y_value then
x_value
else
y_value.
Definition min (x_value : t) (y_value : t) : t :=
if op_gteq x_value y_value then
y_value
else
x_value.
Definition compare : t → t → t := Compare.Int.compare.
Definition saturated : int := Pervasives.max_int.
Definition op_gtexclamation : t → int → bool := Compare.Int.op_gt.
Definition of_int_opt (t_value : int) : option int :=
if (op_gteq t_value 0) && (op_lt t_value saturated) then
Some t_value
else
None.
Definition of_z_opt (z_value : Z.t) : option int :=
let 'int_value := Z.to_int z_value in
of_int_opt int_value.
Definition to_z (x_value : int) : Z.t := Z.of_int x_value.
Definition saturate_if_undef (function_parameter : option int) : int :=
match function_parameter with
| None ⇒ saturated
| Some x_value ⇒ x_value
end.
Definition safe_int (x_value : int) : int :=
saturate_if_undef (of_int_opt x_value).
Definition numbits (x_value : int) : int :=
let x_value : Pervasives.ref int :=
Pervasives.ref_value x_value
in let n_value : Pervasives.ref int :=
Pervasives.ref_value 0 in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 32 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value
((Pervasives.op_exclamation n_value) +i 32) in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 16 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value
((Pervasives.op_exclamation n_value) +i 16) in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 8 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 8)
in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 4 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 4)
in
Pervasives.op_coloneq x_value y_value
else
tt in
let '_ :=
let y_value := Pervasives.lsr (Pervasives.op_exclamation x_value) 2 in
if op_ltgt y_value 0 then
let '_ :=
Pervasives.op_coloneq n_value ((Pervasives.op_exclamation n_value) +i 2)
in
Pervasives.op_coloneq x_value y_value
else
tt in
if op_ltgt (Pervasives.lsr (Pervasives.op_exclamation x_value) 1) 0 then
(Pervasives.op_exclamation n_value) +i 2
else
(Pervasives.op_exclamation n_value) +i (Pervasives.op_exclamation x_value).
Definition zero : int := 0.
Definition one : int := 1.
Definition small_enough (z_value : int) : bool :=
op_eq (Pervasives.land z_value (-2147483648)) 0.
Definition mul_safe_value (x_value : int) : option int :=
if small_enough x_value then
Some x_value
else
None.
Definition mul_safe_exn (x_value : int) : int :=
if small_enough x_value then
x_value
else
Pervasives.failwith
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "mul_safe_exn: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" must be below 2147483648"
CamlinternalFormatBasics.End_of_format)))
"mul_safe_exn: %d must be below 2147483648") x_value).
Definition mul_safe_of_int_exn (x_value : int) : int :=
(fun (function_parameter : option int) ⇒
match function_parameter with
| None ⇒
Pervasives.failwith
(Format.sprintf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "mul_safe_of_int_exn: "
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.String_literal
" must be below 2147483648"
CamlinternalFormatBasics.End_of_format)))
"mul_safe_of_int_exn: %d must be below 2147483648") x_value)
| Some x_value ⇒ x_value
end) (Option.bind (of_int_opt x_value) mul_safe_value).
Definition shift_right (x_value : int) (y_value : int) : int :=
Pervasives.lsr x_value y_value.
Definition shift_left (x_value : int) (y_value : int) : int :=
if op_lt (shift_right saturated y_value) x_value then
saturated
else
Pervasives.lsl x_value y_value.
Definition mul (x_value : int) (y_value : int) : int :=
match x_value with
| 0 ⇒ 0
| x_value ⇒
if (small_enough x_value) && (small_enough y_value) then
x_value ×i y_value
else
if y_value >i (saturated /i x_value) then
saturated
else
x_value ×i y_value
end.
Definition mul_fast (x_value : int) (y_value : int) : int := x_value ×i y_value.
Definition scale_fast (x_value : int) (y_value : int) : int :=
if op_eq x_value 0 then
0
else
if small_enough y_value then
x_value ×i y_value
else
if y_value >i (saturated /i x_value) then
saturated
else
x_value ×i y_value.
Definition add (x_value : int) (y_value : int) : int :=
let z_value := x_value +i y_value in
if z_value ≥i 0 then
z_value
else
saturated.
Definition succ (x_value : int) : int := add one x_value.
Definition sub (x_value : int) (y_value : int) : int :=
Compare.Int.max (x_value -i y_value) 0.
Definition sub_opt (x_value : int) (y_value : int) : option int :=
let s_value := x_value -i y_value in
if s_value ≥i 0 then
Some s_value
else
None.
Definition erem (x_value : int) (y_value : int) : int :=
Pervasives._mod x_value y_value.
Definition ediv (x_value : int) (y_value : int) : int := x_value /i y_value.
Definition sqrt (x_value : int) : int :=
saturate_if_undef
(Option.map (fun (x_value : int) ⇒ Z.to_int (Z.sqrt (Z.of_int x_value)))
(of_int_opt x_value)).
Definition t_to_z_exn (z_value : Z.t) : int :=
match of_z_opt z_value with
| None ⇒
(* ❌ Assert instruction is not handled. *)
assert int false
| Some x_value ⇒ x_value
end.
Definition z_encoding : Data_encoding.encoding int :=
Data_encoding.check_size 9
(Data_encoding.conv to_z t_to_z_exn None Data_encoding.z_value).
Definition n_encoding : Data_encoding.encoding int :=
Data_encoding.check_size 9
(Data_encoding.conv to_z t_to_z_exn None Data_encoding.n_value).
Definition pp (fmt : Format.formatter) (x_value : int) : unit :=
Format.pp_print_int fmt x_value.
Module Syntax.
Definition log2 (x_value : int) : int := safe_int (1 +i (numbits x_value)).
Definition sqrt : int → int := sqrt.
Definition op_plus : int → int → int := add.
Definition op_minus : int → int → int := sub.
Definition op_star : int → int → int := mul.
Definition op_lt : t → t → bool := op_lt.
Definition op_eq : t → t → bool := op_eq.
Definition lsr : int → int → int := shift_right.
Definition lsl : int → int → int := shift_left.
End Syntax.