🍬 Script_int.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Inductive n : Set :=
| Natural_tag : n.
Inductive z : Set :=
| Integer_tag : z.
Definition repr : Set := Z.t.
Inductive num : Set :=
| Num_tag : repr → num.
Definition compare (function_parameter : num) : num → int :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Z.compare x_value y_value.
Definition zero : num := Num_tag Z.zero.
Definition zero_n : num := Num_tag Z.zero.
Definition one_n : num := Num_tag Z.one.
Definition to_string (function_parameter : num) : string :=
let 'Num_tag x_value := function_parameter in
Z.to_string x_value.
Definition of_string (s_value : string) : option num :=
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Num_tag (Z.of_string s_value)).
Definition of_int32 (n_value : int32) : num :=
Num_tag (Z.of_int64 (Int64.of_int32 n_value)).
Definition to_int64 (function_parameter : num) : option int64 :=
let 'Num_tag x_value := function_parameter in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Z.to_int64 x_value).
Definition of_int64 (n_value : int64) : num := Num_tag (Z.of_int64 n_value).
Definition to_int (function_parameter : num) : option int :=
let 'Num_tag x_value := function_parameter in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Z.to_int x_value).
Definition of_int (n_value : int) : num := Num_tag (Z.of_int n_value).
Definition of_zint (x_value : repr) : num := Num_tag x_value.
Definition to_zint (function_parameter : num) : repr :=
let 'Num_tag x_value := function_parameter in
x_value.
Definition add (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (x_value +Z y_value).
Definition sub (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (x_value -Z y_value).
Definition mul (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (x_value ×Z y_value).
Definition ediv (function_parameter : num) : num → option (num × num) :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
let ediv_tagged (x_value : Z.t) (y_value : Z.t) : num × num :=
let '(quo, rem) := Z.ediv_rem x_value y_value in
((Num_tag quo), (Num_tag rem)) in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
ediv_tagged x_value y_value).
Definition add_n : num → num → num := add.
Definition succ_n (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.succ x_value).
Definition mul_n : num → num → num := mul.
Definition ediv_n : num → num → option (num × num) := ediv.
Definition abs (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.abs x_value).
Definition is_nat (function_parameter : num) : option num :=
let 'Num_tag x_value := function_parameter in
if x_value <Z Z.zero then
None
else
Some (Num_tag x_value).
Definition neg (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.neg x_value).
Definition int_value (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag x_value.
Definition shift_left (function_parameter : num) : num → option num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
if (Z.compare y_value (Z.of_int 256)) >i 0 then
None
else
let y_value := Z.to_int y_value in
Some (Num_tag (Z.shift_left x_value y_value)).
Definition shift_right (function_parameter : num) : num → option num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
if (Z.compare y_value (Z.of_int 256)) >i 0 then
None
else
let y_value := Z.to_int y_value in
Some (Num_tag (Z.shift_right x_value y_value)).
Definition shift_left_n : num → num → option num := shift_left.
Definition shift_right_n : num → num → option num := shift_right.
Definition logor (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (Z.logor x_value y_value).
Definition logxor (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (Z.logxor x_value y_value).
Definition logand (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (Z.logand x_value y_value).
Definition lognot (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.lognot x_value).
Definition z_encoding : Data_encoding.encoding num :=
Data_encoding.conv
(fun (function_parameter : num) ⇒
let 'Num_tag z_value := function_parameter in
z_value) (fun (z_value : repr) ⇒ Num_tag z_value) None
Data_encoding.z_value.
Definition n_encoding : Data_encoding.encoding num :=
Data_encoding.conv
(fun (function_parameter : num) ⇒
let 'Num_tag n_value := function_parameter in
n_value) (fun (n_value : repr) ⇒ Num_tag n_value) None
Data_encoding.n_value.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Inductive n : Set :=
| Natural_tag : n.
Inductive z : Set :=
| Integer_tag : z.
Definition repr : Set := Z.t.
Inductive num : Set :=
| Num_tag : repr → num.
Definition compare (function_parameter : num) : num → int :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Z.compare x_value y_value.
Definition zero : num := Num_tag Z.zero.
Definition zero_n : num := Num_tag Z.zero.
Definition one_n : num := Num_tag Z.one.
Definition to_string (function_parameter : num) : string :=
let 'Num_tag x_value := function_parameter in
Z.to_string x_value.
Definition of_string (s_value : string) : option num :=
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Num_tag (Z.of_string s_value)).
Definition of_int32 (n_value : int32) : num :=
Num_tag (Z.of_int64 (Int64.of_int32 n_value)).
Definition to_int64 (function_parameter : num) : option int64 :=
let 'Num_tag x_value := function_parameter in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Z.to_int64 x_value).
Definition of_int64 (n_value : int64) : num := Num_tag (Z.of_int64 n_value).
Definition to_int (function_parameter : num) : option int :=
let 'Num_tag x_value := function_parameter in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Z.to_int x_value).
Definition of_int (n_value : int) : num := Num_tag (Z.of_int n_value).
Definition of_zint (x_value : repr) : num := Num_tag x_value.
Definition to_zint (function_parameter : num) : repr :=
let 'Num_tag x_value := function_parameter in
x_value.
Definition add (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (x_value +Z y_value).
Definition sub (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (x_value -Z y_value).
Definition mul (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (x_value ×Z y_value).
Definition ediv (function_parameter : num) : num → option (num × num) :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
let ediv_tagged (x_value : Z.t) (y_value : Z.t) : num × num :=
let '(quo, rem) := Z.ediv_rem x_value y_value in
((Num_tag quo), (Num_tag rem)) in
Option.catch None
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
ediv_tagged x_value y_value).
Definition add_n : num → num → num := add.
Definition succ_n (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.succ x_value).
Definition mul_n : num → num → num := mul.
Definition ediv_n : num → num → option (num × num) := ediv.
Definition abs (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.abs x_value).
Definition is_nat (function_parameter : num) : option num :=
let 'Num_tag x_value := function_parameter in
if x_value <Z Z.zero then
None
else
Some (Num_tag x_value).
Definition neg (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.neg x_value).
Definition int_value (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag x_value.
Definition shift_left (function_parameter : num) : num → option num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
if (Z.compare y_value (Z.of_int 256)) >i 0 then
None
else
let y_value := Z.to_int y_value in
Some (Num_tag (Z.shift_left x_value y_value)).
Definition shift_right (function_parameter : num) : num → option num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
if (Z.compare y_value (Z.of_int 256)) >i 0 then
None
else
let y_value := Z.to_int y_value in
Some (Num_tag (Z.shift_right x_value y_value)).
Definition shift_left_n : num → num → option num := shift_left.
Definition shift_right_n : num → num → option num := shift_right.
Definition logor (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (Z.logor x_value y_value).
Definition logxor (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (Z.logxor x_value y_value).
Definition logand (function_parameter : num) : num → num :=
let 'Num_tag x_value := function_parameter in
fun (function_parameter : num) ⇒
let 'Num_tag y_value := function_parameter in
Num_tag (Z.logand x_value y_value).
Definition lognot (function_parameter : num) : num :=
let 'Num_tag x_value := function_parameter in
Num_tag (Z.lognot x_value).
Definition z_encoding : Data_encoding.encoding num :=
Data_encoding.conv
(fun (function_parameter : num) ⇒
let 'Num_tag z_value := function_parameter in
z_value) (fun (z_value : repr) ⇒ Num_tag z_value) None
Data_encoding.z_value.
Definition n_encoding : Data_encoding.encoding num :=
Data_encoding.conv
(fun (function_parameter : num) ⇒
let 'Num_tag n_value := function_parameter in
n_value) (fun (n_value : repr) ⇒ Num_tag n_value) None
Data_encoding.n_value.