(.using
 [library
  [lux "*"
   ["[0]" meta]
   [abstract
    [monad {"+" Monad do}]
    [equivalence {"+" Equivalence}]
    [order {"+" Order}]
    [enum {"+" Enum}]]
   [control
    ["<>" parser ("[1]#[0]" monad)
     ["<[0]>" code {"+" Parser}]]]
   [data
    ["[0]" text
     ["%" format {"+" format}]]]
   [macro
    ["[0]" code]
    ["[0]" template]
    [syntax {"+" syntax:}
     ["|[0]|" export]]]
   [math
    [number
     ["n" nat]
     ["i" int]
     ["[0]" ratio {"+" Ratio}]]]
   [type
    [abstract {"-" pattern}]]]])

(abstract: .public (Qty unit)
  Int
  
  (def: in'
    (All (_ unit) (-> Int (Qty unit)))
    (|>> abstraction))

  (def: out'
    (All (_ unit) (-> (Qty unit) Int))
    (|>> representation))

  (template [<name> <op>]
    [(def: .public (<name> param subject)
       (All (_ unit) (-> (Qty unit) (Qty unit) (Qty unit)))
       (abstraction (<op> (representation param)
                          (representation subject))))]

    [+ i.+]
    [- i.-]
    )

  (template [<name> <op> <p> <s> <p*s>]
    [(def: .public (<name> param subject)
       (All (_ p s) (-> (Qty <p>) (Qty <s>) (Qty <p*s>)))
       (abstraction (<op> (representation param)
                          (representation subject))))]

    [* i.* p s [p s]]
    [/ i./ p [p s] s]
    )
  )

(type: .public (Unit a)
  (Interface
   (is (-> Int (Qty a))
       in)
   (is (-> (Qty a) Int)
       out)))

(type: .public (Scale s)
  (Interface
   (is (All (_ u) (-> (Qty u) (Qty (s u))))
       scale)
   (is (All (_ u) (-> (Qty (s u)) (Qty u)))
       de_scale)
   (is Ratio
       ratio)))

(type: .public Pure
  (Qty Any))

(def: .public pure
  (-> Int Pure)
  ..in')

(def: .public number
  (-> Pure Int)
  ..out')

(syntax: .public (unit: [[export_policy type_name unit_name]
                         (|export|.parser
                          (all <>.and
                               <code>.local
                               <code>.local))])
  (do meta.monad
    [@ meta.current_module_name
     .let [g!type (code.local type_name)]]
    (in (list (` (type: (~ export_policy) (~ g!type)
                   (Primitive (~ (code.text (%.symbol [@ type_name]))))))

              (` (implementation: (~ export_policy) (~ (code.local unit_name))
                   (..Unit (~ g!type))

                   (def: (~' in) (~! ..in'))
                   (def: (~' out) (~! ..out'))))
              ))))

(def: scaleP
  (Parser Ratio)
  (<code>.tuple (do <>.monad
                  [numerator <code>.nat
                   _ (<>.assertion (format "Numerator must be positive: " (%.nat numerator))
                                   (n.> 0 numerator))
                   denominator <code>.nat
                   _ (<>.assertion (format "Denominator must be positive: " (%.nat denominator))
                                   (n.> 0 denominator))]
                  (in [numerator denominator]))))

(syntax: .public (scale: [[export_policy type_name scale_name ratio]
                          (|export|.parser
                           (all <>.and
                                <code>.local
                                <code>.local
                                ..scaleP))])
  (do meta.monad
    [.let [(open "_[0]") ratio]
     @ meta.current_module_name
     .let [g!scale (code.local type_name)]]
    (in (list (` (type: (~ export_policy) ((~ g!scale) (~' u))
                   (Primitive (~ (code.text (%.symbol [@ type_name]))) [(~' u)])))
              
              (` (implementation: (~ export_policy) (~ (code.local scale_name))
                   (..Scale (~ g!scale))
                   
                   (def: (~' scale)
                     (|>> ((~! ..out'))
                          (i.* (~ (code.int (.int _#numerator))))
                          (i./ (~ (code.int (.int _#denominator))))
                          ((~! ..in'))))
                   (def: (~' de_scale)
                     (|>> ((~! ..out'))
                          (i.* (~ (code.int (.int _#denominator))))
                          (i./ (~ (code.int (.int _#numerator))))
                          ((~! ..in'))))
                   (def: (~' ratio)
                     [(~ (code.nat _#numerator))
                      (~ (code.nat _#denominator))])))
              ))))

(def: .public (re_scaled from to quantity)
  (All (_ si so u) (-> (Scale si) (Scale so) (Qty (si u)) (Qty (so u))))
  (let [[numerator denominator] (ratio./ (# from ratio)
                                         (# to ratio))]
    (|> quantity
        out'
        (i.* (.int numerator))
        (i./ (.int denominator))
        in')))

(syntax: (implementation_name [type_name <code>.local])
  (in (list (code.local (text.lower_cased type_name)))))

(template [<type> <from> <to>]
  [(`` (scale: .public <type>
         (~~ (implementation_name <type>))
         [<from> <to>]))]

  [Kilo 1         1,000]
  [Mega 1     1,000,000]
  [Giga 1 1,000,000,000]

  [Milli 1,000         1]
  [Micro 1,000,000     1]
  [Nano  1,000,000,000 1]
  )

(template [<type>]
  [(`` (unit: .public <type>
         (~~ (implementation_name <type>))))]

  [Gram]
  [Meter]
  [Litre]
  [Second]
  )

(implementation: .public equivalence
  (All (_ unit) (Equivalence (Qty unit)))
  
  (def: (= reference sample)
    (i.= (..out' reference) (..out' sample))))

(implementation: .public order
  (All (_ unit) (Order (Qty unit)))
  
  (def: equivalence ..equivalence)
  
  (def: (< reference sample)
    (i.< (..out' reference) (..out' sample))))

(implementation: .public enum
  (All (_ unit) (Enum (Qty unit)))
  
  (def: order ..order)
  (def: succ (|>> ..out' ++ ..in'))
  (def: pred (|>> ..out' -- ..in')))