(.module:
  [library
   [lux (#- nat)
    [abstract
     [equivalence (#+ Equivalence)]
     [order (#+ Order)]]
    [control
     ["." try (#+ Try)]
     ["." exception (#+ exception:)]]
    [data
     [text
      ["%" format (#+ format)]]
     ["." format #_
      ["#" binary (#+ Writer)]]]
    [macro
     ["." template]]
    [math
     [number
      ["n" nat]
      ["." i64]]]
    [type
     abstract]]])

(abstract: #export (Unsigned brand)
  Nat

  (def: #export value
    (-> (Unsigned Any) Nat)
    (|>> :representation))

  (implementation: #export equivalence
    (All [brand] (Equivalence (Unsigned brand)))
    (def: (= reference sample)
      (n.= (:representation reference)
           (:representation sample))))

  (implementation: #export order
    (All [brand] (Order (Unsigned brand)))
    
    (def: &equivalence ..equivalence)
    (def: (< reference sample)
      (n.< (:representation reference)
           (:representation sample))))

  (exception: #export (value_exceeds_the_maximum {type Name}
                                                 {value Nat}
                                                 {maximum (Unsigned Any)})
    (exception.report
     ["Type" (%.name type)]
     ["Value" (%.nat value)]
     ["Maximum" (%.nat (:representation maximum))]))

  (exception: #export [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: #export <raw> Any)
       (type: #export <name> (Unsigned <raw>)))

     (def: #export <size> <bytes>)
     
     (def: #export <maximum>
       <name>
       (|> <bytes> (n.* i64.bits_per_byte) i64.mask :abstraction))
     
     (def: #export (<constructor> value)
       (-> Nat (Try <name>))
       (if (n.<= (:representation <maximum>) value)
         (#try.Success (:abstraction value))
         (exception.throw ..value_exceeds_the_maximum [(name_of <name>) value <maximum>])))

     (def: #export (<+> parameter subject)
       (-> <name> <name> (Try <name>))
       (<constructor>
        (n.+ (:representation parameter)
             (:representation subject))))

     (def: #export (<-> parameter subject)
       (-> <name> <name> (Try <name>))
       (let [parameter' (:representation parameter)
             subject' (:representation subject)]
         (if (n.<= subject' parameter')
           (#try.Success (:abstraction (n.- parameter' subject')))
           (exception.throw ..subtraction_cannot_yield_negative_value [(name_of <name>) parameter subject]))))

     (def: #export (<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: #export <name>
       (-> <from> <to>)
       (|>> :transmutation))]

    [lift/2 U1 U2]
    [lift/4 U2 U4]
    )

  (template [<writer_name> <type> <writer>]
    [(def: #export <writer_name>
       (Writer <type>)
       (|>> :representation <writer>))]

    [writer/1 U1 format.bits/8]
    [writer/2 U2 format.bits/16]
    [writer/4 U4 format.bits/32]
    )
  )