Source file script_comparable.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
open Alpha_context
open Script_typed_ir
let compare_address {destination = destination1; entrypoint = entrypoint1}
{destination = destination2; entrypoint = entrypoint2} =
let lres = Destination.compare destination1 destination2 in
if Compare.Int.(lres = 0) then Entrypoint.compare entrypoint1 entrypoint2
else lres
let compare_tx_rollup_l2_address = Tx_rollup_l2_address.Indexable.compare_values
type compare_comparable_cont =
| Compare_comparable :
'a comparable_ty * 'a * 'a * compare_comparable_cont
-> compare_comparable_cont
| Compare_comparable_return : compare_comparable_cont
let compare_comparable : type a. a comparable_ty -> a -> a -> int =
let rec compare_comparable :
type a. a comparable_ty -> compare_comparable_cont -> a -> a -> int =
fun kind k x y ->
match (kind, x, y) with
| (Unit_t, (), ()) -> (apply [@tailcall]) 0 k
| (Never_t, _, _) -> .
| (Signature_t, x, y) ->
(apply [@tailcall]) (Script_signature.compare x y) k
| (String_t, x, y) -> (apply [@tailcall]) (Script_string.compare x y) k
| (Bool_t, x, y) -> (apply [@tailcall]) (Compare.Bool.compare x y) k
| (Mutez_t, x, y) -> (apply [@tailcall]) (Tez.compare x y) k
| (Key_hash_t, x, y) ->
(apply [@tailcall]) (Signature.Public_key_hash.compare x y) k
| (Key_t, x, y) -> (apply [@tailcall]) (Signature.Public_key.compare x y) k
| (Int_t, x, y) -> (apply [@tailcall]) (Script_int.compare x y) k
| (Nat_t, x, y) -> (apply [@tailcall]) (Script_int.compare x y) k
| (Timestamp_t, x, y) ->
(apply [@tailcall]) (Script_timestamp.compare x y) k
| (Address_t, x, y) -> (apply [@tailcall]) (compare_address x y) k
| (Tx_rollup_l2_address_t, x, y) ->
(apply [@tailcall]) (compare_tx_rollup_l2_address x y) k
| (Bytes_t, x, y) -> (apply [@tailcall]) (Compare.Bytes.compare x y) k
| (Chain_id_t, x, y) -> (apply [@tailcall]) (Script_chain_id.compare x y) k
| (Pair_t (tl, tr, _, YesYes), (lx, rx), (ly, ry)) ->
(compare_comparable [@tailcall])
tl
(Compare_comparable (tr, rx, ry, k))
lx
ly
| (Union_t (tl, _, _, YesYes), L x, L y) ->
(compare_comparable [@tailcall]) tl k x y
| (Union_t _, L _, R _) -> -1
| (Union_t _, R _, L _) -> 1
| (Union_t (_, tr, _, YesYes), R x, R y) ->
(compare_comparable [@tailcall]) tr k x y
| (Option_t _, None, None) -> (apply [@tailcall]) 0 k
| (Option_t _, None, Some _) -> -1
| (Option_t _, Some _, None) -> 1
| (Option_t (t, _, Yes), Some x, Some y) ->
(compare_comparable [@tailcall]) t k x y
and apply ret k =
match (ret, k) with
| (0, Compare_comparable (ty, x, y, k)) ->
(compare_comparable [@tailcall]) ty k x y
| (0, Compare_comparable_return) -> 0
| (ret, _) ->
if Compare.Int.(ret > 0) then 1 else -1
in
fun t -> compare_comparable t Compare_comparable_return
[@@coq_axiom_with_reason "non top-level mutually recursive function"]