Skip to main content

➗ Ratio_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.V7.

Module t.
  Record record : Set := Build {
    numerator : int;
    denominator : int;
  }.
  Definition with_numerator numerator (r : record) :=
    Build numerator r.(denominator).
  Definition with_denominator denominator (r : record) :=
    Build r.(numerator) denominator.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv_with_guard
    (fun (r_value : t) ⇒ (r_value.(t.numerator), r_value.(t.denominator)))
    (fun (function_parameter : int × int) ⇒
      let '(numerator, denominator) := function_parameter in
      if denominator >i 0 then
        return? {| t.numerator := numerator; t.denominator := denominator; |}
      else
        Pervasives.Error "The denominator must be greater than 0.") None
    (Data_encoding.obj2
      (Data_encoding.req None None "numerator" Data_encoding.uint16)
      (Data_encoding.req None None "denominator" Data_encoding.uint16)).

Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
  let '{| t.numerator := numerator; t.denominator := denominator |} :=
    function_parameter in
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
        CamlinternalFormatBasics.No_padding
        CamlinternalFormatBasics.No_precision
        (CamlinternalFormatBasics.Char_literal "/" % char
          (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
            CamlinternalFormatBasics.No_padding
            CamlinternalFormatBasics.No_precision
            CamlinternalFormatBasics.End_of_format))) "%d/%d") numerator
    denominator.