aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/library/lux/target/jvm/encoding/unsigned.lux
blob: 795f30716aed9a5427cc787ad08007828d804395 (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
(.using
 [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 Symbol
                                                  value Nat
                                                  maximum (Unsigned Any)])
    (exception.report
     "Type" (%.symbol type)
     "Value" (%.nat value)
     "Maximum" (%.nat (:representation maximum))))

  (exception: .public [brand] (subtraction_cannot_yield_negative_value
                               [type Symbol
                                parameter (Unsigned brand)
                                subject (Unsigned brand)])
    (exception.report
     "Type" (%.symbol type)
     "Parameter" (%.nat (:representation parameter))
     "Subject" (%.nat (:representation subject))))

  (template [<bytes> <name> <size> <constructor> <maximum> <+> <-> <max>]
    [(with_expansions [<raw> (template.symbol [<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 [(symbol <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 [(symbol <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]
    )
  )