Skip to main content

🪙 Tez_repr.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.V8.

Definition id : string := "tez".

Definition name : string := "mutez".

Definition repr : Set := int64.

Inductive t : Set :=
| Tez_tag : repr t.

Definition zero : t := Tez_tag 0.

Definition one_mutez : t := Tez_tag 1.

Definition max_mutez : t := Tez_tag Int64.max_int.

Definition mul_int (function_parameter : t) : int64 t :=
  let 'Tez_tag tez := function_parameter in
  fun (i_value : int64) ⇒ Tez_tag (tez ×i64 i_value).

Definition one_cent : t := mul_int one_mutez 10000.

Definition fifty_cents : t := mul_int one_cent 50.

Definition one : t := mul_int one_cent 100.

Definition of_string (s_value : string) : option t :=
  let triplets (function_parameter : list string) : bool :=
    match function_parameter with
    | cons hd tl
      let len := String.length hd in
      (len i 3) &&
      ((len >i 0) &&
      (List.for_all (fun (s_value : string) ⇒ (String.length s_value) =i 3) tl))
    | []false
    end in
  let integers (s_value : string) : bool :=
    triplets (String.split_on_char "," % char s_value) in
  let decimals (s_value : string) : bool :=
    let l_value := String.split_on_char "," % char s_value in
    if Compare.List_length_with.op_gt l_value 2 then
      false
    else
      triplets (List.rev l_value) in
  let parse (_left : string) (_right : string) : option t :=
    let remove_commas (s_value : string) : string :=
      String.concat "" (String.split_on_char "," % char s_value) in
    let pad_to_six (s_value : string) : string :=
      let len := String.length s_value in
      String.init_value 6
        (fun (i_value : int) ⇒
          if i_value <i len then
            String.get s_value i_value
          else
            "0" % char) in
    let prepared :=
      Pervasives.op_caret (remove_commas _left)
        (pad_to_six (remove_commas _right)) in
    Option.map (fun (i_value : repr) ⇒ Tez_tag i_value)
      (Int64.of_string_opt prepared) in
  match String.split_on_char "." % char s_value with
  | cons _left (cons _right []) ⇒
    if String.contains s_value "," % char then
      if (integers _left) && (decimals _right) then
        parse _left _right
      else
        None
    else
      if ((String.length _right) >i 0) && ((String.length _right) i 6) then
        parse _left _right
      else
        None
  | cons _left []
    if
      (Pervasives.not (String.contains s_value "," % char)) || (integers _left)
    then
      parse _left ""
    else
      None
  | _None
  end.

#[bypass_check(guard)]
Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  let 'Tez_tag amount := function_parameter in
  let mult_int := 1000000 in
  let fix _left (ppf : Format.formatter) (amount : int64) {struct amount}
    : unit :=
    let '(d_value, r_value) := ((amount /i64 1000), (Int64.rem amount 1000)) in
    if d_value >i64 0 then
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
              (CamlinternalFormatBasics.Lit_padding
                CamlinternalFormatBasics.Zeros 3)
              CamlinternalFormatBasics.No_precision
              CamlinternalFormatBasics.End_of_format)) "%a%03Ld") _left d_value
        r_value
    else
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Int64 CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            CamlinternalFormatBasics.End_of_format) "%Ld") r_value in
  let _right (ppf : Format.formatter) (amount : int) : unit :=
    let triplet (ppf : Format.formatter) (v_value : int) : unit :=
      if (Pervasives._mod v_value 10) >i 0 then
        Format.fprintf ppf
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
              (CamlinternalFormatBasics.Lit_padding
                CamlinternalFormatBasics.Zeros 3)
              CamlinternalFormatBasics.No_precision
              CamlinternalFormatBasics.End_of_format) "%03d") v_value
      else
        if (Pervasives._mod v_value 100) >i 0 then
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                (CamlinternalFormatBasics.Lit_padding
                  CamlinternalFormatBasics.Zeros 2)
                CamlinternalFormatBasics.No_precision
                CamlinternalFormatBasics.End_of_format) "%02d") (v_value /i 10)
        else
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.No_precision
                CamlinternalFormatBasics.End_of_format) "%d") (v_value /i 100)
      in
    let '(hi, lo) := ((amount /i 1000), (Pervasives._mod amount 1000)) in
    if lo =i 0 then
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
          "%a") triplet hi
    else
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
            (CamlinternalFormatBasics.Lit_padding CamlinternalFormatBasics.Zeros
              3) CamlinternalFormatBasics.No_precision
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format)) "%03d%a") hi triplet lo
    in
  let '(ints, decs) :=
    ((amount /i64 mult_int), (Int64.to_int (Int64.rem amount mult_int))) in
  let '_ := _left ppf ints in
  if decs >i 0 then
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Char_literal "." % char
          (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
        ".%a") _right decs
  else
    tt.

Definition to_string (t_value : t) : string :=
  Format.asprintf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
      "%a") pp t_value.

Definition op_minusquestion (tez1 : t) (tez2 : t) : M? t :=
  let 'Tez_tag t1 := tez1 in
  let 'Tez_tag t2 := tez2 in
  if t2 i64 t1 then
    return? (Tez_tag (t1 -i64 t2))
  else
    Error_monad.error_value
      (Build_extensible "Subtraction_underflow" (t × t) (tez1, tez2)).

Definition sub_opt (function_parameter : t) : t option t :=
  let 'Tez_tag t1 := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag t2 := function_parameter in
    if t2 i64 t1 then
      Some (Tez_tag (t1 -i64 t2))
    else
      None.

Definition op_plusquestion (tez1 : t) (tez2 : t) : M? t :=
  let 'Tez_tag t1 := tez1 in
  let 'Tez_tag t2 := tez2 in
  let t_value := t1 +i64 t2 in
  if t_value <i64 t1 then
    Error_monad.error_value
      (Build_extensible "Addition_overflow" (t × t) (tez1, tez2))
  else
    return? (Tez_tag t_value).

Definition op_starquestion (tez : t) (m_value : int64) : M? t :=
  let 'Tez_tag t_value := tez in
  if m_value <i64 0 then
    Error_monad.error_value
      (Build_extensible "Negative_multiplicator" (t × int64) (tez, m_value))
  else
    if m_value =i64 0 then
      return? (Tez_tag 0)
    else
      if t_value >i64 (Int64.max_int /i64 m_value) then
        Error_monad.error_value
          (Build_extensible "Multiplication_overflow" (t × int64) (tez, m_value))
      else
        return? (Tez_tag (t_value ×i64 m_value)).

Definition op_divquestion (tez : t) (d_value : int64) : M? t :=
  let 'Tez_tag t_value := tez in
  if d_value i64 0 then
    Error_monad.error_value
      (Build_extensible "Invalid_divisor" (t × int64) (tez, d_value))
  else
    return? (Tez_tag (t_value /i64 d_value)).

Definition mul_exn (t_value : t) (m_value : int) : t :=
  match op_starquestion t_value (Int64.of_int m_value) with
  | Pervasives.Ok v_valuev_value
  | Pervasives.Error _Pervasives.invalid_arg "mul_exn"
  end.

Definition div_exn (t_value : t) (d_value : int) : t :=
  match op_divquestion t_value (Int64.of_int d_value) with
  | Pervasives.Ok v_valuev_value
  | Pervasives.Error _Pervasives.invalid_arg "div_exn"
  end.

Definition of_mutez (t_value : int64) : option t :=
  if t_value <i64 0 then
    None
  else
    Some (Tez_tag t_value).

Definition of_mutez_exn (x_value : int64) : t :=
  match of_mutez x_value with
  | NonePervasives.invalid_arg "Tez.of_mutez"
  | Some v_valuev_value
  end.

Definition to_mutez (function_parameter : t) : repr :=
  let 'Tez_tag t_value := function_parameter in
  t_value.

Definition encoding : Data_encoding.encoding t :=
  let decode (function_parameter : t) : Z.t :=
    let 'Tez_tag t_value := function_parameter in
    Z.of_int64 t_value in
  let encode :=
    Data_encoding.Json.wrap_error
      (fun (i_value : Z.t) ⇒ Tez_tag (Z.to_int64 i_value)) in
  Data_encoding.def name None None
    (Data_encoding.check_size 10
      (Data_encoding.conv decode encode None Data_encoding.n_value)).

Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      (Pervasives.op_caret id ".addition_overflow")
      (Pervasives.op_caret "Overflowing " (Pervasives.op_caret id " addition"))
      (Pervasives.op_caret "An addition of two "
        (Pervasives.op_caret id " amounts overflowed"))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : t × t) ⇒
            let '(opa, opb) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Overflowing addition of "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal " " % char
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal " and "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal " " % char
                              (CamlinternalFormatBasics.String
                                CamlinternalFormatBasics.No_padding
                                CamlinternalFormatBasics.End_of_format))))))))
                "Overflowing addition of %a %s and %a %s") pp opa id pp opb id))
      (Data_encoding.obj1
        (Data_encoding.req None None "amounts"
          (Data_encoding.tup2 encoding encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Addition_overflow" then
            let '(a_value, b_value) := cast (t × t) payload in
            Some (a_value, b_value)
          else None
        end)
      (fun (function_parameter : t × t) ⇒
        let '(a_value, b_value) := function_parameter in
        Build_extensible "Addition_overflow" (t × t) (a_value, b_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      (Pervasives.op_caret id ".subtraction_underflow")
      (Pervasives.op_caret "Underflowing "
        (Pervasives.op_caret id " subtraction"))
      (Pervasives.op_caret "A subtraction of two "
        (Pervasives.op_caret id
          " amounts underflowed (i.e., would have led to a negative amount)"))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : t × t) ⇒
            let '(opa, opb) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Underflowing subtraction of "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal " " % char
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal " and "
                          (CamlinternalFormatBasics.Alpha
                            (CamlinternalFormatBasics.Char_literal " " % char
                              (CamlinternalFormatBasics.String
                                CamlinternalFormatBasics.No_padding
                                CamlinternalFormatBasics.End_of_format))))))))
                "Underflowing subtraction of %a %s and %a %s") pp opa id pp opb
              id))
      (Data_encoding.obj1
        (Data_encoding.req None None "amounts"
          (Data_encoding.tup2 encoding encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Subtraction_underflow" then
            let '(a_value, b_value) := cast (t × t) payload in
            Some (a_value, b_value)
          else None
        end)
      (fun (function_parameter : t × t) ⇒
        let '(a_value, b_value) := function_parameter in
        Build_extensible "Subtraction_underflow" (t × t) (a_value, b_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      (Pervasives.op_caret id ".multiplication_overflow")
      (Pervasives.op_caret "Overflowing "
        (Pervasives.op_caret id " multiplication"))
      (Pervasives.op_caret "A multiplication of a "
        (Pervasives.op_caret id " amount by an integer overflowed"))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : t × int64) ⇒
            let '(opa, opb) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Overflowing multiplication of "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal " " % char
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal " and "
                          (CamlinternalFormatBasics.Int64
                            CamlinternalFormatBasics.Int_d
                            CamlinternalFormatBasics.No_padding
                            CamlinternalFormatBasics.No_precision
                            CamlinternalFormatBasics.End_of_format))))))
                "Overflowing multiplication of %a %s and %Ld") pp opa id opb))
      (Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
        (Data_encoding.req None None "multiplicator" Data_encoding.int64_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Multiplication_overflow" then
            let '(a_value, b_value) := cast (t × int64) payload in
            Some (a_value, b_value)
          else None
        end)
      (fun (function_parameter : t × int64) ⇒
        let '(a_value, b_value) := function_parameter in
        Build_extensible "Multiplication_overflow" (t × int64)
          (a_value, b_value)) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      (Pervasives.op_caret id ".negative_multiplicator")
      (Pervasives.op_caret "Negative " (Pervasives.op_caret id " multiplicator"))
      (Pervasives.op_caret "Multiplication of a "
        (Pervasives.op_caret id " amount by a negative integer"))
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : t × int64) ⇒
            let '(opa, opb) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Multiplication of "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal " " % char
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal
                          " by negative integer "
                          (CamlinternalFormatBasics.Int64
                            CamlinternalFormatBasics.Int_d
                            CamlinternalFormatBasics.No_padding
                            CamlinternalFormatBasics.No_precision
                            CamlinternalFormatBasics.End_of_format))))))
                "Multiplication of %a %s by negative integer %Ld") pp opa id opb))
      (Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
        (Data_encoding.req None None "multiplicator" Data_encoding.int64_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Negative_multiplicator" then
            let '(a_value, b_value) := cast (t × int64) payload in
            Some (a_value, b_value)
          else None
        end)
      (fun (function_parameter : t × int64) ⇒
        let '(a_value, b_value) := function_parameter in
        Build_extensible "Negative_multiplicator" (t × int64) (a_value, b_value))
    in
  Error_monad.register_error_kind Error_monad.Temporary
    (Pervasives.op_caret id ".invalid_divisor")
    (Pervasives.op_caret "Invalid " (Pervasives.op_caret id " divisor"))
    (Pervasives.op_caret "Multiplication of a "
      (Pervasives.op_caret id " amount by a non positive integer"))
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : t × int64) ⇒
          let '(opa, opb) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "Division of "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal " " % char
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.String_literal
                        " by non positive integer "
                        (CamlinternalFormatBasics.Int64
                          CamlinternalFormatBasics.Int_d
                          CamlinternalFormatBasics.No_padding
                          CamlinternalFormatBasics.No_precision
                          CamlinternalFormatBasics.End_of_format))))))
              "Division of %a %s by non positive integer %Ld") pp opa id opb))
    (Data_encoding.obj2 (Data_encoding.req None None "amount" encoding)
      (Data_encoding.req None None "divisor" Data_encoding.int64_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_divisor" then
          let '(a_value, b_value) := cast (t × int64) payload in
          Some (a_value, b_value)
        else None
      end)
    (fun (function_parameter : t × int64) ⇒
      let '(a_value, b_value) := function_parameter in
      Build_extensible "Invalid_divisor" (t × int64) (a_value, b_value)).

Definition tez : Set := t.

Definition compare (function_parameter : t) : t int :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    Compare.Int64.(Compare.S.compare) x_value y_value.

Definition op_eq (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    x_value =i64 y_value.

Definition op_ltgt (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    x_value i64 y_value.

Definition op_lt (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    x_value <i64 y_value.

Definition op_gt (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    x_value >i64 y_value.

Definition op_lteq (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    x_value i64 y_value.

Definition op_gteq (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    x_value i64 y_value.

Definition equal (function_parameter : t) : t bool :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    Compare.Int64.(Compare.S.equal) x_value y_value.

Definition max (function_parameter : t) : t t :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    Tez_tag (Compare.Int64.(Compare.S.max) x_value y_value).

Definition min (function_parameter : t) : t t :=
  let 'Tez_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'Tez_tag y_value := function_parameter in
    Tez_tag (Compare.Int64.(Compare.S.min) x_value y_value).