-
Notifications
You must be signed in to change notification settings - Fork 0
/
u32.ya
107 lines (80 loc) · 3.26 KB
/
u32.ya
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
package u32
import bool
import is
import pair
import maybe
where
def U32: Type = #U32
def U32.MAX: U32 = #U32.max
def U32.MIN: U32 = #U32.min
def U32.eql: ∀ (x y: U32) -> Bool = #U32.eql
def U32.lte: ∀ (x y: U32) -> Bool = #U32.lte
def U32.lth: ∀ (x y: U32) -> Bool = #U32.lth
def U32.gte: ∀ (x y: U32) -> Bool = #U32.gte
def U32.gth: ∀ (x y: U32) -> Bool = #U32.gth
def U32.and: ∀ (x y: U32) -> Bool = #U32.and
def U32.xor: ∀ (x y: U32) -> Bool = #U32.xor
def U32.or: ∀ (x y: U32) -> Bool = #U32.or
def U32.neq (x y: U32): Bool = Bool.not (U32.eql x y)
def U32.add: ∀ (x y: U32) -> U32 = #U32.add
def U32.addSafe (x y: U32) (0 e: Is (U32.gte (#U32.add x y) x)): U32
= #U32.add x y
def U32.sub: ∀ (x y: U32) -> U32 = #U32.sub
def U32.subSafe (x y: U32) (0 e: Is (U32.lte y x)): U32 = #U32.sub x y
def U32.mul: ∀ (x y: U32) -> U32 = #U32.mul
def U32.SafeMul (x y: U32): Bool =
(case (U32.eql x 0u32)) (λ _ => Bool)
Bool.True
(U32.eql (#U32.div (#U32.mul x y) x) y)
def U32.mulSafe (x y: U32) (0 e: Is (U32.SafeMul x y)): U32 = #U32.mul x y
def U32.div (x y: U32): Maybe U32 =
(case (U32.neq y 0u32)) (λ _ => Maybe U32)
(Maybe.Some U32 (#U32.div x y))
(Maybe.None U32)
def U32.divSafe (x y: U32) (0 e: Is (U32.neq y 0)): U32 = #U32.div x y
def U32.mod (x y: U32): Maybe U32 =
(case (U32.neq y 0u32)) (λ _ => Maybe U32)
(Maybe.Some U32 (#U32.mod x y))
(Maybe.None U32)
def U32.modSafe (x y: U32) (0 e: Is (U32.neq y 0)): U32 = #U32.mod x y
def U32.pow: ∀ (x y: U32) -> U32 = #U32.pow
def U32.shl: ∀ (x y: U32) -> U32 = #U32.shl
def U32.shr: ∀ (x y: U32) -> U32 = #U32.shr
def U32.rol: ∀ (x y: U32) -> U32 = #U32.rol
def U32.ror: ∀ (x y: U32) -> U32 = #U32.ror
def U32.countZeros: ∀ (x: U32) -> U32 = #U32.count_zeros
def U32.countOnes: ∀ (x: U32) -> U32 = #U32.count_ones
def U32.toU8 (x: U32): Maybe #U8 =
(case (U32.lte x (#U8.to_U32 #U8.max))) (λ _ => Maybe #U8)
(Maybe.Some #U8 (#U32.to_U8 x))
(Maybe.None #U8)
def U32.toU8Safe (x: U32) (0 e: Is (U32.lte x (#U8.to_U32 #U8.max))): #U8
= #U32.to_U8 x
def U32.toU16 (x: U32): Maybe #U16 =
(case (U32.lte x (#U16.to_U32 #U16.max))) (λ _ => Maybe #U16)
(Maybe.Some #U16 (#U32.to_U16 x))
(Maybe.None #U16)
def U32.toU16Safe (x: U32) (0 e: Is (U32.lte x (#U16.to_U32 #U16.max))): #U16
= #U32.to_U16 x
def U32.toU64: ∀ (x: U32) -> #U64 = #U32.to_U64
def U32.toI8 (x: U32): Maybe #I8 =
(case (U32.lte x (#I8.to_U32 #I8.max))) (λ _ => Maybe #I8)
(Maybe.Some #I8 (#U32.to_I8 x))
(Maybe.None #I8)
def U32.toI8Safe (x: U32) (0 e: Is (U32.lte x (#I8.to_U32 #I8.max))): #I8
= #U32.to_I8 x
def U32.toI16 (x: U32): Maybe #I16 =
(case (U32.lte x (#I16.to_U32 #I16.max))) (λ _ => Maybe #I16)
(Maybe.Some #I16 (#U32.to_I16 x))
(Maybe.None #I16)
def U32.toI16Safe (x: U32) (0 e: Is (U32.lte x (#I16.to_U32 #I16.max))): #I16
= #U32.to_I16 x
def U32.toI32 (x: U32): Maybe #I32 =
(case (U32.lte x (#I32.to_U32 #I32.max))) (λ _ => Maybe #I32)
(Maybe.Some #I32 (#U32.to_I32 x))
(Maybe.None #I32)
def U32.toI32Safe (x: U32) (0 e: Is (U32.lte x (#I32.to_U32 #I32.max))): #I32
= #U32.to_I32 x
def U32.toI64: ∀ (x: U32) -> #I64 = #U32.to_I64
def U32.toNat: ∀ (x: U32) -> #Nat = #U32.to_Nat
def U32.toInt: ∀ (x: U32) -> #Int = #U32.to_Int