🍬 Script_comparable.v
Translated 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.
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.