⚗️ Liquidity_baking_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Inductive liquidity_baking_toggle_vote : Set :=
| LB_on : liquidity_baking_toggle_vote
| LB_off : liquidity_baking_toggle_vote
| LB_pass : liquidity_baking_toggle_vote.
Definition liquidity_baking_toggle_vote_encoding
: Data_encoding.encoding liquidity_baking_toggle_vote :=
let of_int8 (function_parameter : int)
: Pervasives.result liquidity_baking_toggle_vote string :=
match function_parameter with
| 0 ⇒ Pervasives.Ok LB_on
| 1 ⇒ Pervasives.Ok LB_off
| 2 ⇒ Pervasives.Ok LB_pass
| _ ⇒ Pervasives.Error "liquidity_baking_toggle_vote_of_int8"
end in
let to_int8 (function_parameter : liquidity_baking_toggle_vote) : int :=
match function_parameter with
| LB_on ⇒ 0
| LB_off ⇒ 1
| LB_pass ⇒ 2
end in
Data_encoding.def "liquidity_baking_toggle_vote" None None
(Data_encoding.splitted
(Data_encoding.string_enum
[ ("on", LB_on); ("off", LB_off); ("pass", LB_pass) ])
(Data_encoding.conv_with_guard to_int8 of_int8 None Data_encoding.int8)).
Module Toggle_EMA.
Definition t : Set := Int32.t.
Definition check_bounds (x_value : int32) : bool :=
(0 ≤i32 x_value) && (x_value ≤i32 2000000000).
Definition of_int32 (x_value : int32) : M? int32 :=
if check_bounds x_value then
return? x_value
else
Error_monad.tzfail
(Build_extensible "Liquidity_baking_toggle_ema_out_of_bound" int32
x_value).
Definition zero : int32 := Int32.zero.
Definition of_int32_for_encoding (x_value : int32)
: Pervasives.result int32 string :=
if check_bounds x_value then
Pervasives.Ok x_value
else
Pervasives.Error "out of bounds".
Definition to_int32 {A : Set} (ema : A) : A := ema.
Definition z_1999 : Z.t := Z.of_int 1999.
Definition z_2000 : Z.t := Z.of_int 2000.
Definition attenuate (z_value : Z.t) : Z.t := (z_1999 ×Z z_value) /Z z_2000.
Definition z_1_000_000_000 : Z.t := Z.of_int 1000000000.
Definition recenter (f_value : Z.t → Z.t) (ema : Z.t) : Z.t :=
z_1_000_000_000 +Z (f_value (ema -Z z_1_000_000_000)).
Definition z_500_000 : Z.t := Z.of_int 500000.
Definition update_ema_off (ema : int32) : int32 :=
let ema := Z.of_int32 ema in
Z.to_int32 (recenter (fun (ema : Z.t) ⇒ (attenuate ema) +Z z_500_000) ema).
Definition update_ema_on (ema : int32) : int32 :=
let ema := Z.of_int32 ema in
Z.to_int32 (recenter (fun (ema : Z.t) ⇒ (attenuate ema) -Z z_500_000) ema).
Definition op_lt : int32 → int32 → bool := Compare.Int32.(Compare.S.op_lt).
Definition encoding : Data_encoding.encoding int32 :=
Data_encoding.conv_with_guard to_int32 of_int32_for_encoding None
Data_encoding.int32_value.
End Toggle_EMA.
Definition compute_new_ema
(toggle_vote : liquidity_baking_toggle_vote) (ema : Toggle_EMA.t)
: Toggle_EMA.t :=
match toggle_vote with
| LB_pass ⇒ ema
| LB_off ⇒ Toggle_EMA.update_ema_off ema
| LB_on ⇒ Toggle_EMA.update_ema_on ema
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Inductive liquidity_baking_toggle_vote : Set :=
| LB_on : liquidity_baking_toggle_vote
| LB_off : liquidity_baking_toggle_vote
| LB_pass : liquidity_baking_toggle_vote.
Definition liquidity_baking_toggle_vote_encoding
: Data_encoding.encoding liquidity_baking_toggle_vote :=
let of_int8 (function_parameter : int)
: Pervasives.result liquidity_baking_toggle_vote string :=
match function_parameter with
| 0 ⇒ Pervasives.Ok LB_on
| 1 ⇒ Pervasives.Ok LB_off
| 2 ⇒ Pervasives.Ok LB_pass
| _ ⇒ Pervasives.Error "liquidity_baking_toggle_vote_of_int8"
end in
let to_int8 (function_parameter : liquidity_baking_toggle_vote) : int :=
match function_parameter with
| LB_on ⇒ 0
| LB_off ⇒ 1
| LB_pass ⇒ 2
end in
Data_encoding.def "liquidity_baking_toggle_vote" None None
(Data_encoding.splitted
(Data_encoding.string_enum
[ ("on", LB_on); ("off", LB_off); ("pass", LB_pass) ])
(Data_encoding.conv_with_guard to_int8 of_int8 None Data_encoding.int8)).
Module Toggle_EMA.
Definition t : Set := Int32.t.
Definition check_bounds (x_value : int32) : bool :=
(0 ≤i32 x_value) && (x_value ≤i32 2000000000).
Definition of_int32 (x_value : int32) : M? int32 :=
if check_bounds x_value then
return? x_value
else
Error_monad.tzfail
(Build_extensible "Liquidity_baking_toggle_ema_out_of_bound" int32
x_value).
Definition zero : int32 := Int32.zero.
Definition of_int32_for_encoding (x_value : int32)
: Pervasives.result int32 string :=
if check_bounds x_value then
Pervasives.Ok x_value
else
Pervasives.Error "out of bounds".
Definition to_int32 {A : Set} (ema : A) : A := ema.
Definition z_1999 : Z.t := Z.of_int 1999.
Definition z_2000 : Z.t := Z.of_int 2000.
Definition attenuate (z_value : Z.t) : Z.t := (z_1999 ×Z z_value) /Z z_2000.
Definition z_1_000_000_000 : Z.t := Z.of_int 1000000000.
Definition recenter (f_value : Z.t → Z.t) (ema : Z.t) : Z.t :=
z_1_000_000_000 +Z (f_value (ema -Z z_1_000_000_000)).
Definition z_500_000 : Z.t := Z.of_int 500000.
Definition update_ema_off (ema : int32) : int32 :=
let ema := Z.of_int32 ema in
Z.to_int32 (recenter (fun (ema : Z.t) ⇒ (attenuate ema) +Z z_500_000) ema).
Definition update_ema_on (ema : int32) : int32 :=
let ema := Z.of_int32 ema in
Z.to_int32 (recenter (fun (ema : Z.t) ⇒ (attenuate ema) -Z z_500_000) ema).
Definition op_lt : int32 → int32 → bool := Compare.Int32.(Compare.S.op_lt).
Definition encoding : Data_encoding.encoding int32 :=
Data_encoding.conv_with_guard to_int32 of_int32_for_encoding None
Data_encoding.int32_value.
End Toggle_EMA.
Definition compute_new_ema
(toggle_vote : liquidity_baking_toggle_vote) (ema : Toggle_EMA.t)
: Toggle_EMA.t :=
match toggle_vote with
| LB_pass ⇒ ema
| LB_off ⇒ Toggle_EMA.update_ema_off ema
| LB_on ⇒ Toggle_EMA.update_ema_on ema
end.