🍃 Compare.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Char.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Int64.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.Q.
Require TezosOfOCaml.Environment.Structs.V0.String.
Require TezosOfOCaml.Environment.Structs.V0.Z.
Import Pervasives.Notations.
Module COMPARABLE.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
}.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.
Module S.
Record signature {t : Set} : Set := {
t := t;
op_eq : t → t → bool;
op_ltgt : t → t → bool;
op_lt : t → t → bool;
op_lteq : t → t → bool;
op_gteq : t → t → bool;
op_gt : t → t → bool;
compare : t → t → int;
equal : t → t → bool;
max : t → t → t;
min : t → t → t;
}.
End S.
Definition S := @S.signature.
Arguments S {_}.
Definition Make {P_t : Set} (P : COMPARABLE (t := P_t))
: S (t := P.(COMPARABLE.t)) :=
{|
S.op_eq x y := Z.eqb (P.(COMPARABLE.compare) x y) 0;
S.op_ltgt x y := negb (Z.eqb (P.(COMPARABLE.compare) x y) 0);
S.op_lt x y := Z.ltb (P.(COMPARABLE.compare) x y) 0;
S.op_lteq x y := Z.leb (P.(COMPARABLE.compare) x y) 0;
S.op_gteq x y := Z.geb (P.(COMPARABLE.compare) x y) 0;
S.op_gt x y := Z.gtb (P.(COMPARABLE.compare) x y) 0;
S.compare x y := P.(COMPARABLE.compare) x y;
S.equal x y := Z.eqb (P.(COMPARABLE.compare) x y) 0;
S.max x y :=
if Z.leb (P.(COMPARABLE.compare) x y) 0 then
y
else
x;
S.min x y :=
if Z.leb (P.(COMPARABLE.compare) x y) 0 then
x
else
y;
|}.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Char.
Require TezosOfOCaml.Environment.Structs.V0.Int32.
Require TezosOfOCaml.Environment.Structs.V0.Int64.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Require TezosOfOCaml.Environment.Structs.V0.Q.
Require TezosOfOCaml.Environment.Structs.V0.String.
Require TezosOfOCaml.Environment.Structs.V0.Z.
Import Pervasives.Notations.
Module COMPARABLE.
Record signature {t : Set} : Set := {
t := t;
compare : t → t → int;
}.
End COMPARABLE.
Definition COMPARABLE := @COMPARABLE.signature.
Arguments COMPARABLE {_}.
Module S.
Record signature {t : Set} : Set := {
t := t;
op_eq : t → t → bool;
op_ltgt : t → t → bool;
op_lt : t → t → bool;
op_lteq : t → t → bool;
op_gteq : t → t → bool;
op_gt : t → t → bool;
compare : t → t → int;
equal : t → t → bool;
max : t → t → t;
min : t → t → t;
}.
End S.
Definition S := @S.signature.
Arguments S {_}.
Definition Make {P_t : Set} (P : COMPARABLE (t := P_t))
: S (t := P.(COMPARABLE.t)) :=
{|
S.op_eq x y := Z.eqb (P.(COMPARABLE.compare) x y) 0;
S.op_ltgt x y := negb (Z.eqb (P.(COMPARABLE.compare) x y) 0);
S.op_lt x y := Z.ltb (P.(COMPARABLE.compare) x y) 0;
S.op_lteq x y := Z.leb (P.(COMPARABLE.compare) x y) 0;
S.op_gteq x y := Z.geb (P.(COMPARABLE.compare) x y) 0;
S.op_gt x y := Z.gtb (P.(COMPARABLE.compare) x y) 0;
S.compare x y := P.(COMPARABLE.compare) x y;
S.equal x y := Z.eqb (P.(COMPARABLE.compare) x y) 0;
S.max x y :=
if Z.leb (P.(COMPARABLE.compare) x y) 0 then
y
else
x;
S.min x y :=
if Z.leb (P.(COMPARABLE.compare) x y) 0 then
x
else
y;
|}.
A utility function built on top of [Make] to make it simpler to use.
Definition Make_with_compare {A : Set} (compare : A → A → int) : S (t := A) :=
Make {| COMPARABLE.compare := compare |}.
Definition Char : S (t := ascii) :=
Make_with_compare Char.compare.
Definition int_of_bool (b : bool) : int :=
if b then 1 else 0.
Definition Unit : S (t := unit) :=
Make_with_compare (fun '_ '_ ⇒ 0).
Definition Bool : S (t := bool) :=
Make_with_compare (fun x y ⇒
match x, y with
| false, false ⇒ 0
| false, true ⇒ -1
| true, false ⇒ 1
| true, true ⇒ 0
end
).
Definition Z : S (t := Z.t) :=
{|
S.op_eq := Z.eqb;
S.op_ltgt x y := negb (x =? y);
S.op_lt x y := x <? y;
S.op_lteq x y := x <=? y;
S.op_gteq x y := x >=? y;
S.op_gt x y := x >? y;
S.compare := Z.compare;
S.equal := Z.eqb;
S.max := Z.max;
S.min := Z.min;
|}.
Definition Int : S (t := int) := Z.
Module Int.
Definition t : Set := int.
Definition op_eq : int → int → bool := Int.(S.op_eq).
Definition op_ltgt : int → int → bool := Int.(S.op_ltgt).
Definition op_lt : int → int → bool := Int.(S.op_lt).
Definition op_gt : int → int → bool := Int.(S.op_gt).
Definition op_lteq : int → int → bool := Int.(S.op_lteq).
Definition op_gteq : int → int → bool := Int.(S.op_gteq).
Definition compare : int → int → int := Int.(S.compare).
Definition max : int → int → int := Int.(S.max).
Definition min : int → int → int := Int.(S.min).
Definition equal : int → int → bool := Int.(S.equal).
End Int.
Definition Int32 : S (t := int32) := Z.
Definition Uint32 : S (t := int32) := Z.
Definition Int64 : S (t := int64) := Z.
Definition Uint64 : S (t := int64) := Z.
Parameter Q : S (t := Q.t).
Definition String : S (t := string) :=
Make_with_compare String.compare.
Definition Bytes : S (t := bytes) :=
Make_with_compare String.compare.
Module List.
Parameter compare : ∀ {a : Set},
(a → a → int) → list a → list a → int.
End List.
Definition List {P_t : Set} (P : COMPARABLE (t := P_t))
: S (t := list P.(COMPARABLE.t)) :=
Make_with_compare (List.compare P.(COMPARABLE.compare)).
Module Option.
Definition compare {a : Set} (compare : a → a → int) (x y : option a)
: int :=
match x, y with
| None, None ⇒ 0
| None, Some _ ⇒ -1
| Some _, None ⇒ 1
| Some x, Some y ⇒ compare x y
end.
End Option.
Definition Option {P_t : Set} (P : COMPARABLE (t := P_t))
: S (t := option P.(COMPARABLE.t)) :=
Make_with_compare (Option.compare P.(COMPARABLE.compare)).
Parameter Result :
∀ {Ok_t Error_t : Set},
∀ (Ok : COMPARABLE (t := Ok_t)),
∀ (Error : COMPARABLE (t := Error_t)),
S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).
Module List_length_with.
Fixpoint op_eq {a : Set} (l : list a) (n : int) : bool :=
match l with
| [] ⇒ n =? 0
| _ :: l ⇒ op_eq l (n -i 1)
end.
Parameter op_ltgt : ∀ {a : Set}, list a → int → bool.
Parameter op_lt : ∀ {a : Set}, list a → int → bool.
Parameter op_lteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gt : ∀ {a : Set}, list a → int → bool.
Parameter compare : ∀ {a : Set}, list a → int → int.
Parameter equal : ∀ {a : Set}, list a → int → bool.
End List_length_with.
Module List_lengths.
Parameter op_eq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_ltgt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gt : ∀ {a b : Set}, list a → list b → bool.
Parameter compare : ∀ {a b : Set}, list a → list b → int.
Parameter equal : ∀ {a b : Set}, list a → list b → bool.
End List_lengths.
Parameter or_else : int → (unit → int) → int.
Definition lexicographic {a b : Set} (compare_a : a → a → int)
(compare_b : b → b → int) (x y : a × b) : int :=
let (x_a, x_b) := x in
let (y_a, y_b) := y in
let a_res := compare_a x_a y_a in
match a_res with
| 0 ⇒ compare_b x_b y_b
| _ ⇒ a_res
end.
Definition Pair {P1_t P2_t : Set}
(P1 : COMPARABLE (t := P1_t)) (P2 : COMPARABLE (t := P2_t))
: S (t := P1.(COMPARABLE.t) × P2.(COMPARABLE.t)) :=
Make_with_compare
(lexicographic P1.(COMPARABLE.compare) P2.(COMPARABLE.compare)).
Module Notations.
Infix "=i" := Int.op_eq
(at level 70, no associativity).
Infix "<>i" := Int.op_ltgt
(at level 70, no associativity).
Infix "<=i" := Int.op_lteq
(at level 70, no associativity).
Infix "<i" := Int.op_lt
(at level 70, no associativity).
Infix ">=i" := Int.op_gteq
(at level 70, no associativity).
Infix ">i" := Int.op_gt
(at level 70, no associativity).
Infix "=i32" := Int32.(S.op_eq)
(at level 70, no associativity).
Infix "<>i32" := Int32.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=i32" := Int32.(S.op_lteq)
(at level 70, no associativity).
Infix "<i32" := Int32.(S.op_lt)
(at level 70, no associativity).
Infix ">=i32" := Int32.(S.op_gteq)
(at level 70, no associativity).
Infix ">i32" := Int32.(S.op_gt)
(at level 70, no associativity).
Infix "=i64" := Int64.(S.op_eq)
(at level 70, no associativity).
Infix "<>i64" := Int64.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=i64" := Int64.(S.op_lteq)
(at level 70, no associativity).
Infix "<i64" := Int64.(S.op_lt)
(at level 70, no associativity).
Infix ">=i64" := Int64.(S.op_gteq)
(at level 70, no associativity).
Infix ">i64" := Int64.(S.op_gt)
(at level 70, no associativity).
Infix "=Z" := Z.(S.op_eq)
(at level 70, no associativity).
Infix "<>Z" := Z.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=Z" := Z.(S.op_lteq)
(at level 70, no associativity).
Infix "<Z" := Z.(S.op_lt)
(at level 70, no associativity).
Infix ">=Z" := Z.(S.op_gteq)
(at level 70, no associativity).
Infix ">Z" := Z.(S.op_gt)
(at level 70, no associativity).
Infix "=s" := String.(S.op_eq)
(at level 70, no associativity).
Infix "<>s" := String.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=s" := String.(S.op_lteq)
(at level 70, no associativity).
Infix "<s" := String.(S.op_lt)
(at level 70, no associativity).
Infix ">=s" := String.(S.op_gteq)
(at level 70, no associativity).
Infix ">s" := String.(S.op_gt)
(at level 70, no associativity).
End Notations.
#[global] Hint Unfold
Int.op_eq
Int.op_ltgt
Int.op_lt
Int.op_gt
Int.op_lteq
Int.op_gteq
Int.compare
Int.max
Int.min
Int.equal
: tezos_z.
Make {| COMPARABLE.compare := compare |}.
Definition Char : S (t := ascii) :=
Make_with_compare Char.compare.
Definition int_of_bool (b : bool) : int :=
if b then 1 else 0.
Definition Unit : S (t := unit) :=
Make_with_compare (fun '_ '_ ⇒ 0).
Definition Bool : S (t := bool) :=
Make_with_compare (fun x y ⇒
match x, y with
| false, false ⇒ 0
| false, true ⇒ -1
| true, false ⇒ 1
| true, true ⇒ 0
end
).
Definition Z : S (t := Z.t) :=
{|
S.op_eq := Z.eqb;
S.op_ltgt x y := negb (x =? y);
S.op_lt x y := x <? y;
S.op_lteq x y := x <=? y;
S.op_gteq x y := x >=? y;
S.op_gt x y := x >? y;
S.compare := Z.compare;
S.equal := Z.eqb;
S.max := Z.max;
S.min := Z.min;
|}.
Definition Int : S (t := int) := Z.
Module Int.
Definition t : Set := int.
Definition op_eq : int → int → bool := Int.(S.op_eq).
Definition op_ltgt : int → int → bool := Int.(S.op_ltgt).
Definition op_lt : int → int → bool := Int.(S.op_lt).
Definition op_gt : int → int → bool := Int.(S.op_gt).
Definition op_lteq : int → int → bool := Int.(S.op_lteq).
Definition op_gteq : int → int → bool := Int.(S.op_gteq).
Definition compare : int → int → int := Int.(S.compare).
Definition max : int → int → int := Int.(S.max).
Definition min : int → int → int := Int.(S.min).
Definition equal : int → int → bool := Int.(S.equal).
End Int.
Definition Int32 : S (t := int32) := Z.
Definition Uint32 : S (t := int32) := Z.
Definition Int64 : S (t := int64) := Z.
Definition Uint64 : S (t := int64) := Z.
Parameter Q : S (t := Q.t).
Definition String : S (t := string) :=
Make_with_compare String.compare.
Definition Bytes : S (t := bytes) :=
Make_with_compare String.compare.
Module List.
Parameter compare : ∀ {a : Set},
(a → a → int) → list a → list a → int.
End List.
Definition List {P_t : Set} (P : COMPARABLE (t := P_t))
: S (t := list P.(COMPARABLE.t)) :=
Make_with_compare (List.compare P.(COMPARABLE.compare)).
Module Option.
Definition compare {a : Set} (compare : a → a → int) (x y : option a)
: int :=
match x, y with
| None, None ⇒ 0
| None, Some _ ⇒ -1
| Some _, None ⇒ 1
| Some x, Some y ⇒ compare x y
end.
End Option.
Definition Option {P_t : Set} (P : COMPARABLE (t := P_t))
: S (t := option P.(COMPARABLE.t)) :=
Make_with_compare (Option.compare P.(COMPARABLE.compare)).
Parameter Result :
∀ {Ok_t Error_t : Set},
∀ (Ok : COMPARABLE (t := Ok_t)),
∀ (Error : COMPARABLE (t := Error_t)),
S (t := Pervasives.result Ok.(COMPARABLE.t) Error.(COMPARABLE.t)).
Module List_length_with.
Fixpoint op_eq {a : Set} (l : list a) (n : int) : bool :=
match l with
| [] ⇒ n =? 0
| _ :: l ⇒ op_eq l (n -i 1)
end.
Parameter op_ltgt : ∀ {a : Set}, list a → int → bool.
Parameter op_lt : ∀ {a : Set}, list a → int → bool.
Parameter op_lteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gteq : ∀ {a : Set}, list a → int → bool.
Parameter op_gt : ∀ {a : Set}, list a → int → bool.
Parameter compare : ∀ {a : Set}, list a → int → int.
Parameter equal : ∀ {a : Set}, list a → int → bool.
End List_length_with.
Module List_lengths.
Parameter op_eq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_ltgt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lt : ∀ {a b : Set}, list a → list b → bool.
Parameter op_lteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gteq : ∀ {a b : Set}, list a → list b → bool.
Parameter op_gt : ∀ {a b : Set}, list a → list b → bool.
Parameter compare : ∀ {a b : Set}, list a → list b → int.
Parameter equal : ∀ {a b : Set}, list a → list b → bool.
End List_lengths.
Parameter or_else : int → (unit → int) → int.
Definition lexicographic {a b : Set} (compare_a : a → a → int)
(compare_b : b → b → int) (x y : a × b) : int :=
let (x_a, x_b) := x in
let (y_a, y_b) := y in
let a_res := compare_a x_a y_a in
match a_res with
| 0 ⇒ compare_b x_b y_b
| _ ⇒ a_res
end.
Definition Pair {P1_t P2_t : Set}
(P1 : COMPARABLE (t := P1_t)) (P2 : COMPARABLE (t := P2_t))
: S (t := P1.(COMPARABLE.t) × P2.(COMPARABLE.t)) :=
Make_with_compare
(lexicographic P1.(COMPARABLE.compare) P2.(COMPARABLE.compare)).
Module Notations.
Infix "=i" := Int.op_eq
(at level 70, no associativity).
Infix "<>i" := Int.op_ltgt
(at level 70, no associativity).
Infix "<=i" := Int.op_lteq
(at level 70, no associativity).
Infix "<i" := Int.op_lt
(at level 70, no associativity).
Infix ">=i" := Int.op_gteq
(at level 70, no associativity).
Infix ">i" := Int.op_gt
(at level 70, no associativity).
Infix "=i32" := Int32.(S.op_eq)
(at level 70, no associativity).
Infix "<>i32" := Int32.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=i32" := Int32.(S.op_lteq)
(at level 70, no associativity).
Infix "<i32" := Int32.(S.op_lt)
(at level 70, no associativity).
Infix ">=i32" := Int32.(S.op_gteq)
(at level 70, no associativity).
Infix ">i32" := Int32.(S.op_gt)
(at level 70, no associativity).
Infix "=i64" := Int64.(S.op_eq)
(at level 70, no associativity).
Infix "<>i64" := Int64.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=i64" := Int64.(S.op_lteq)
(at level 70, no associativity).
Infix "<i64" := Int64.(S.op_lt)
(at level 70, no associativity).
Infix ">=i64" := Int64.(S.op_gteq)
(at level 70, no associativity).
Infix ">i64" := Int64.(S.op_gt)
(at level 70, no associativity).
Infix "=Z" := Z.(S.op_eq)
(at level 70, no associativity).
Infix "<>Z" := Z.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=Z" := Z.(S.op_lteq)
(at level 70, no associativity).
Infix "<Z" := Z.(S.op_lt)
(at level 70, no associativity).
Infix ">=Z" := Z.(S.op_gteq)
(at level 70, no associativity).
Infix ">Z" := Z.(S.op_gt)
(at level 70, no associativity).
Infix "=s" := String.(S.op_eq)
(at level 70, no associativity).
Infix "<>s" := String.(S.op_ltgt)
(at level 70, no associativity).
Infix "<=s" := String.(S.op_lteq)
(at level 70, no associativity).
Infix "<s" := String.(S.op_lt)
(at level 70, no associativity).
Infix ">=s" := String.(S.op_gteq)
(at level 70, no associativity).
Infix ">s" := String.(S.op_gt)
(at level 70, no associativity).
End Notations.
#[global] Hint Unfold
Int.op_eq
Int.op_ltgt
Int.op_lt
Int.op_gt
Int.op_lteq
Int.op_gteq
Int.compare
Int.max
Int.min
Int.equal
: tezos_z.
Polymorphic comparison operators
These operators cannot be implemented in Coq but are sometimes useful to translate the tests. They are not used in the protocol itself. See the corresponding Proofs file for the specification of these operators.
Polymorphic comparison, like in OCaml.