Skip to main content

🍬 Script_int.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V7.

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.