aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/library/lux/meta/type/unit.lux
blob: 0473ab18aeb1002f620b6cec8fed4bb14683e03b (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
122
123
124
125
126
127
128
129
130
131
132
133
... This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
... If a copy of the MPL was not distributed with this file, You can obtain one at https://mozilla.org/MPL/2.0/.

... https://en.wikipedia.org/wiki/Dimensional_analysis
(.require
 [library
  [lux (.except type)
   [abstract
    [equivalence (.only Equivalence)]
    [order (.only Order)]
    [enum (.only Enum)]]
   [data
    ["[0]" text (.only)
     ["%" \\format]]]
   [math
    [number
     ["i" int]]]
   [meta
    ["[0]" code
     ["<[1]>" \\parser]]
    ["[0]" macro (.only)
     [syntax (.only syntax)]]]]]
 ["[0]" // (.only)
  ["[0]" nominal (.except def)]])

(nominal.def .public (Measure scale unit)
  Int

  (def .public measure
    (All (_ scale unit)
      (-> Int
          (Measure scale unit)))
    (|>> abstraction))

  (def .public number
    (All (_ scale unit)
      (-> (Measure scale unit)
          Int))
    (|>> representation))

  (def .public equivalence
    (All (_ scale unit)
      (Equivalence (Measure scale unit)))
    (implementation
     (def (= reference sample)
       (i.= (representation reference) (representation sample)))))

  (def .public order
    (All (_ scale unit)
      (Order (Measure scale unit)))
    (implementation
     (def equivalence ..equivalence)
     
     (def (< reference sample)
       (i.< (representation reference) (representation sample)))))

  (def .public enum
    (All (_ scale unit)
      (Enum (Measure scale unit)))
    (implementation
     (def order ..order)
     (def succ (|>> representation ++ abstraction))
     (def pred (|>> representation -- abstraction))))

  (with_template [<name> <op>]
    [(def .public (<name> param subject)
       (All (_ scale unit)
         (-> (Measure scale unit) (Measure scale unit)
             (Measure scale unit)))
       (abstraction (<op> (representation param)
                          (representation subject))))]

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

  (with_template [<name> <op> <p> <s> <p*s>]
    [(def .public (<name> param subject)
       (All (_ scale p s)
         (-> (Measure scale <p>) (Measure scale <s>)
             (Measure scale <p*s>)))
       (abstraction (<op> (representation param)
                          (representation subject))))]

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

  (.type .public (Unit of)
    (Interface
     (is (-> (Measure Any of)
             Text)
         format)
     (is (-> Int
             (Measure Any of))
         in)
     (is (-> (Measure Any of)
             Int)
         out)))

  (def .public (unit descriptor)
    (Ex (_ of)
      (-> Text
          (Unit of)))
    (implementation
     (def format (|>> ..number %.int (text.suffix descriptor)))
     (def in ..measure)
     (def out ..number)))
  )

(def .public type
  (syntax (_ [it <code>.any])
    (macro.with_symbols [g!a]
      (in (list (` (//.by_example [(, g!a)]
                     (is (..Unit (, g!a))
                         (, it))
                     (, g!a))))))))

(with_template [<descriptor> <unit> <type>]
  [(def .public <unit>
     (..unit <descriptor>))
   
   (.def .public <type>
     (let [[module _] (symbol .._)
           [_ short] (symbol <type>)]
       {.#Named [module short]
                (..type <unit>)}))]

  ["g" gram Gram]
  ["m" meter Meter]
  ["l" litre Litre]
  ["s" second Second]
  )