blob: df550075b6c3200e4fecc49f4d4f9e99469365ca (
plain)
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
|
(.module:
[library
[lux {"-" [nat]}
[abstract
[equivalence {"+" [Equivalence]}]
[order {"+" [Order]}]]
[control
["[0]" try {"+" [Try]}]
["[0]" exception {"+" [exception:]}]]
[data
[text
["%" format {"+" [format]}]]
["[0]" format "_"
["[1]" binary {"+" [Writer]}]]]
[macro
["[0]" template]]
[math
[number
["n" nat]
["[0]" i64]]]
[type
abstract]]])
(abstract: .public (Unsigned brand)
Nat
[(def: .public value
(-> (Unsigned Any) Nat)
(|>> :representation))
(implementation: .public equivalence
(All (_ brand) (Equivalence (Unsigned brand)))
(def: (= reference sample)
(n.= (:representation reference)
(:representation sample))))
(implementation: .public order
(All (_ brand) (Order (Unsigned brand)))
(def: &equivalence ..equivalence)
(def: (< reference sample)
(n.< (:representation reference)
(:representation sample))))
(exception: .public (value_exceeds_the_maximum [type Name
value Nat
maximum (Unsigned Any)])
(exception.report
["Type" (%.name type)]
["Value" (%.nat value)]
["Maximum" (%.nat (:representation maximum))]))
(exception: .public [brand] (subtraction_cannot_yield_negative_value
[type Name
parameter (Unsigned brand)
subject (Unsigned brand)])
(exception.report
["Type" (%.name type)]
["Parameter" (%.nat (:representation parameter))]
["Subject" (%.nat (:representation subject))]))
(template [<bytes> <name> <size> <constructor> <maximum> <+> <-> <max>]
[(with_expansions [<raw> (template.identifier [<name> "'"])]
(abstract: .public <raw> Any [])
(type: .public <name> (Unsigned <raw>)))
(def: .public <size> <bytes>)
(def: .public <maximum>
<name>
(|> <bytes> (n.* i64.bits_per_byte) i64.mask :abstraction))
(def: .public (<constructor> value)
(-> Nat (Try <name>))
(if (n.> (:representation <maximum>) value)
(exception.except ..value_exceeds_the_maximum [(name_of <name>) value <maximum>])
(#try.Success (:abstraction value))))
(def: .public (<+> parameter subject)
(-> <name> <name> (Try <name>))
(<constructor>
(n.+ (:representation parameter)
(:representation subject))))
(def: .public (<-> parameter subject)
(-> <name> <name> (Try <name>))
(let [parameter' (:representation parameter)
subject' (:representation subject)]
(if (n.> subject' parameter')
(exception.except ..subtraction_cannot_yield_negative_value [(name_of <name>) parameter subject])
(#try.Success (:abstraction (n.- parameter' subject'))))))
(def: .public (<max> left right)
(-> <name> <name> <name>)
(:abstraction (n.max (:representation left)
(:representation right))))]
[1 U1 bytes/1 u1 maximum/1 +/1 -/1 max/1]
[2 U2 bytes/2 u2 maximum/2 +/2 -/2 max/2]
[4 U4 bytes/4 u4 maximum/4 +/4 -/4 max/4]
)
(template [<name> <from> <to>]
[(def: .public <name>
(-> <from> <to>)
(|>> :transmutation))]
[lifted/2 U1 U2]
[lifted/4 U2 U4]
)
(template [<writer_name> <type> <writer>]
[(def: .public <writer_name>
(Writer <type>)
(|>> :representation <writer>))]
[writer/1 U1 format.bits/8]
[writer/2 U2 format.bits/16]
[writer/4 U4 format.bits/32]
)]
)
|
