checker/src/common.ml at master · Cryptinterested/checker · GitHub

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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
open Error

(* Oracle data *)
let oracle_entrypoint : string = "%getPrice"

(* OPERATIONS ON int *)
let[@inline] int_zero = Ligo.int_from_literal "0"

let min_int (x: Ligo.int) (y: Ligo.int) = if Ligo.leq_int_int x y then x else y
let max_int (x: Ligo.int) (y: Ligo.int) = if Ligo.geq_int_int x y then x else y

let neg_int (x: Ligo.int) = Ligo.sub_int_int (Ligo.int_from_literal "0") x

(* Note that ligo is not happy with nested lets. Take out when ready, but
 * keep internal for now. *)
let rec pow_rec (y, x, n: Ligo.int * Ligo.int * Ligo.nat) : Ligo.int =
  if Ligo.eq_nat_nat n (Ligo.nat_from_literal "0n") then
    y
  else if Ligo.eq_nat_nat n (Ligo.nat_from_literal "1n") then
    Ligo.mul_int_int x y
  else
    match Ligo.ediv_nat_nat n (Ligo.nat_from_literal "2n") with
    (* Note: Ignoring coverage for this line because it is unreachable *)
    | None -> (Ligo.failwith internalError_PowRecImpossible : Ligo.int)
              [@coverage off]
    | Some quot_rem ->
      let (quot, rem) = quot_rem in
      if Ligo.eq_nat_nat rem (Ligo.nat_from_literal "0n") then
        pow_rec (y, Ligo.mul_int_int x x, quot)
      else
        pow_rec (Ligo.mul_int_int x y, Ligo.mul_int_int x x, quot)

let pow_int_nat (x: Ligo.int) (n: Ligo.nat) = pow_rec (Ligo.int_from_literal "1", x, n)

let cdiv_int_int (x: Ligo.int) (y: Ligo.int) =
  match Ligo.ediv_int_int x y with
  | None -> (Ligo.failwith internalError_CdivIntIntZeroDenominator : Ligo.int)
  | Some quot_rem ->
    let (quot, rem) = quot_rem in
    if Ligo.eq_nat_nat rem (Ligo.nat_from_literal "0n") then
      quot
    else if Ligo.lt_int_int y (Ligo.int_from_literal "0") then
      quot
    else
      Ligo.add_int_int quot (Ligo.int_from_literal "1")

let fdiv_int_int (x: Ligo.int) (y: Ligo.int) =
  match Ligo.ediv_int_int x y with
  | None -> (Ligo.failwith internalError_FdivIntIntZeroDenominator : Ligo.int)
  | Some quot_rem ->
    let (quot, rem) = quot_rem in
    if Ligo.eq_nat_nat rem (Ligo.nat_from_literal "0n") then
      quot
    else if Ligo.gt_int_int y (Ligo.int_from_literal "0") then
      quot
    else
      Ligo.sub_int_int quot (Ligo.int_from_literal "1")

let clamp_int (v: Ligo.int) (lower: Ligo.int) (upper: Ligo.int) : Ligo.int =
  assert (Ligo.leq_int_int lower upper);
  min_int upper (max_int v lower)

(* OPERATIONS ON tez *)
let tez_to_mutez (x: Ligo.tez) = Ligo.int (Ligo.div_tez_tez x (Ligo.tez_from_literal "1mutez"))

(* OPERATIONS ON nat *)
let min_nat (x: Ligo.nat) (y: Ligo.nat) = if Ligo.leq_nat_nat x y then x else y
let max_nat (x: Ligo.nat) (y: Ligo.nat) = if Ligo.geq_nat_nat x y then x else y

(* RATIOS AND OPERATIONS ON THEM *)

(** A rational is represented as a pair numerator/denominator, reduced to have
  * a positive denominator. This form is canonical. *)
type ratio = {
  num: Ligo.int; (** Numerator. *)
  den: Ligo.int; (** Denominator, > 0 *)
}

(* The denominator must be positive. *)
let[@inline] make_ratio (n: Ligo.int) (d: Ligo.int) : ratio =
  assert (Ligo.gt_int_int d (Ligo.int_from_literal "0"));
  { num = n; den = d; }

(* zero: 0/1 *)
let[@inline] zero_ratio : ratio = { num = Ligo.int_from_literal "0"; den = Ligo.int_from_literal "1"; }

(* one: 1/1 *)
let[@inline] one_ratio : ratio = { num = Ligo.int_from_literal "1"; den = Ligo.int_from_literal "1"; }

(* Floor a fraction to an amount of tez. NOTE: this function deals in tez, not
 * in mutez. So, for example, fraction_to_tez_floor (1/1) = 1tez and
 * fraction_to_tez_floor (1/3) = 333_333mutez. *)
let fraction_to_tez_floor (x_num: Ligo.int) (x_den: Ligo.int) : Ligo.tez =
  assert (Ligo.gt_int_int x_den (Ligo.int_from_literal "0"));
  match Ligo.is_nat x_num with
  | None -> (Ligo.failwith internalError_FractionToTezFloorNegative : Ligo.tez)
  | Some n ->
    let n = Ligo.mul_nat_nat n (Ligo.nat_from_literal "1_000_000n") in
    let d = Ligo.abs x_den in
    (match Ligo.ediv_nat_nat n d with
     (* Note: Ignoring coverage for the case below since the assertion above makes it unreachable in OCaml *)
     | None -> (Ligo.failwith internalError_FractionToTezFloorZeroDenominator : Ligo.tez)
               [@coverage off]
     | Some quot_and_rem ->
       let (quot, _) = quot_and_rem in
       Ligo.mul_nat_tez quot (Ligo.tez_from_literal "1mutez") (* ignore the remainder; we floor towards zero here *)
    )

(* Floor a fraction to a natural number. *)
let fraction_to_nat_floor (x_num: Ligo.int) (x_den: Ligo.int) : Ligo.nat =
  assert (Ligo.gt_int_int x_den (Ligo.int_from_literal "0"));
  match Ligo.is_nat x_num with
  | None -> (Ligo.failwith internalError_FractionToNatFloorNegative : Ligo.nat)
  | Some n ->
    (match Ligo.ediv_nat_nat n (Ligo.abs x_den) with
     (* Note: Ignoring coverage for the case below since the assertion above makes it unreachable in OCaml *)
     | None -> (Ligo.failwith internalError_FractionToNatFloorZeroDenominator : Ligo.nat)
               [@coverage off]
     | Some quot_and_rem ->
       let (quot, _) = quot_and_rem in
       quot (* ignore the remainder; we floor towards zero here *)
    )

(* BEGIN_OCAML *)
[@@@coverage off]
let compare_int (i: Ligo.int) (j: Ligo.int) : Int.t =
  if Ligo.gt_int_int i j then
    1
  else if Ligo.eq_int_int i j then
    0
  else
    -1

let compare_nat (i: Ligo.nat) (j: Ligo.nat) : Int.t =
  if Ligo.gt_nat_nat i j then
    1
  else if Ligo.eq_nat_nat i j then
    0
  else
    -1

let show_ratio n = (Ligo.string_of_int n.num) ^ "/" ^ (Ligo.string_of_int n.den)
let pp_ratio f x = Format.pp_print_string f (show_ratio x)
[@@@coverage on]
(* END_OCAML *)