Skip to main content

🍬 Script_comparable.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.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Dependent_bool.
Require TezosOfOCaml.Proto_alpha.Script_int.
Require TezosOfOCaml.Proto_alpha.Script_string.
Require TezosOfOCaml.Proto_alpha.Script_timestamp.
Require TezosOfOCaml.Proto_alpha.Script_typed_ir.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.

Definition compare_address (function_parameter : Script_typed_ir.address)
  : Script_typed_ir.address int :=
  let '{|
    Script_typed_ir.address.destination := destination1;
      Script_typed_ir.address.entrypoint := entrypoint1
      |} := function_parameter in
  fun (function_parameter : Script_typed_ir.address) ⇒
    let '{|
      Script_typed_ir.address.destination := destination2;
        Script_typed_ir.address.entrypoint := entrypoint2
        |} := function_parameter in
    let lres := Alpha_context.Destination.compare destination1 destination2 in
    if lres =i 0 then
      Alpha_context.Entrypoint.compare entrypoint1 entrypoint2
    else
      lres.

Definition compare_tx_rollup_l2_address
  : Tx_rollup_l2_address.Indexable.value
  Tx_rollup_l2_address.Indexable.value int :=
  Tx_rollup_l2_address.Indexable.compare_values.

Inductive compare_comparable_cont : Set :=
| Compare_comparable : {a : Set},
  Script_typed_ir.comparable_ty a a compare_comparable_cont
  compare_comparable_cont
| Compare_comparable_return : compare_comparable_cont.

Module Compare_comparable.
  Reserved Notation "'apply".

  #[bypass_check(guard)]
  Fixpoint compare_comparable {a : Set}
    (kind_value : Script_typed_ir.comparable_ty)
    (k_value : compare_comparable_cont) (x_value : a) (y_value : a)
    {struct kind_value} : int :=
    let apply := 'apply in
    match (kind_value, x_value, y_value) with
    | (Script_typed_ir.Unit_t, _, _)apply 0 k_value
    | (Script_typed_ir.Signature_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Script_typed_ir.signature ** Script_typed_ir.signature]
          [y_value, x_value] in
      apply (Script_typed_ir.Script_signature.compare x_value y_value) k_value
    | (Script_typed_ir.String_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Script_string.t ** Script_string.t] [y_value, x_value] in
      apply (Script_string.compare x_value y_value) k_value
    | (Script_typed_ir.Bool_t, x_value, y_value)
      let '[y_value, x_value] := cast [bool ** bool] [y_value, x_value] in
      apply (Compare.Bool.(Compare.S.compare) x_value y_value) k_value
    | (Script_typed_ir.Mutez_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Alpha_context.Tez.t ** Alpha_context.Tez.t] [y_value, x_value] in
      apply (Alpha_context.Tez.compare x_value y_value) k_value
    | (Script_typed_ir.Key_hash_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Alpha_context.public_key_hash ** Alpha_context.public_key_hash]
          [y_value, x_value] in
      apply
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare) x_value
          y_value) k_value
    | (Script_typed_ir.Key_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Alpha_context.public_key ** Alpha_context.public_key]
          [y_value, x_value] in
      apply
        (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare) x_value y_value)
        k_value
    | (Script_typed_ir.Int_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Script_int.num ** Script_int.num] [y_value, x_value] in
      apply (Script_int.compare x_value y_value) k_value
    | (Script_typed_ir.Nat_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Script_int.num ** Script_int.num] [y_value, x_value] in
      apply (Script_int.compare x_value y_value) k_value
    | (Script_typed_ir.Timestamp_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Script_timestamp.t ** Script_timestamp.t] [y_value, x_value] in
      apply (Script_timestamp.compare x_value y_value) k_value
    | (Script_typed_ir.Address_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast [Script_typed_ir.address ** Script_typed_ir.address]
          [y_value, x_value] in
      apply (compare_address x_value y_value) k_value
    | (Script_typed_ir.Tx_rollup_l2_address_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast
          [Script_typed_ir.tx_rollup_l2_address **
            Script_typed_ir.tx_rollup_l2_address] [y_value, x_value] in
      apply (compare_tx_rollup_l2_address x_value y_value) k_value
    | (Script_typed_ir.Bytes_t, x_value, y_value)
      let '[y_value, x_value] := cast [bytes ** bytes] [y_value, x_value] in
      apply (Compare.Bytes.(Compare.S.compare) x_value y_value) k_value
    | (Script_typed_ir.Chain_id_t, x_value, y_value)
      let '[y_value, x_value] :=
        cast
          [Script_typed_ir.Script_chain_id.t **
            Script_typed_ir.Script_chain_id.t] [y_value, x_value] in
      apply (Script_typed_ir.Script_chain_id.compare x_value y_value) k_value
    | (Script_typed_ir.Pair_t tl tr _ Dependent_bool.YesYes, x_value, y_value)
      ⇒
      let 'existT _ [__0, __1] [y_value, x_value, tr, tl] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__0, __1]
            [__0 × __1 ** __0 × __1 ** Script_typed_ir.ty ** Script_typed_ir.ty])
          [y_value, x_value, tr, tl] in
      let '(lx, rx) := x_value in
      let '(ly, ry) := y_value in
      compare_comparable tl (Compare_comparable tr rx ry k_value) lx ly
    | (Script_typed_ir.Union_t tl tr _ Dependent_bool.YesYes, x_value, y_value)
      ⇒
      let 'existT _ [__2, __3] [y_value, x_value, tr, tl] :=
        cast_exists (Es := [Set ** Set])
          (fun '[__2, __3]
            [Script_typed_ir.union __2 __3 ** Script_typed_ir.union __2 __3 **
              Script_typed_ir.ty ** Script_typed_ir.ty])
          [y_value, x_value, tr, tl] in
      match (x_value, y_value) with
      | (Script_typed_ir.L x_value, Script_typed_ir.L y_value)
        compare_comparable tl k_value x_value y_value
      | (Script_typed_ir.L _, Script_typed_ir.R _) ⇒ (-1)
      | (Script_typed_ir.R _, Script_typed_ir.L _) ⇒ 1
      | (Script_typed_ir.R x_value, Script_typed_ir.R y_value)
        compare_comparable tr k_value x_value y_value
      end
    | (Script_typed_ir.Option_t t_value _ _, x_value, y_value)
      let 'existT _ __4 [y_value, x_value, t_value] :=
        cast_exists (Es := Set)
          (fun __4[option __4 ** option __4 ** Script_typed_ir.ty])
          [y_value, x_value, t_value] in
      match (x_value, y_value) with
      | (None, None)apply 0 k_value
      | (None, Some _) ⇒ (-1)
      | (Some _, None) ⇒ 1
      | (Some x_value, Some y_value)
        compare_comparable t_value k_value x_value y_value
      end
    | _unreachable_gadt_branch
    end
  
  where "'apply" :=
    (fun (ret_value : int) (k_value : compare_comparable_cont) ⇒
      match (ret_value, k_value) with
      | (0, Compare_comparable ty_value x_value y_value k_value)
        compare_comparable ty_value k_value x_value y_value
      | (0, Compare_comparable_return) ⇒ 0
      | (ret_value, _)
        if ret_value >i 0 then
          1
        else
          (-1)
      end).

  Definition apply := 'apply.
End Compare_comparable.

Definition compare_comparable {a : Set}
  (t_value : Script_typed_ir.comparable_ty) : a a int :=
  Compare_comparable.compare_comparable t_value Compare_comparable_return.