blob: bcc8f672c38e02fa95309bb3b95ab7b6979cfc4e (
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
|
(.require
[library
[lux (.except type)
[abstract
[equivalence (.only Equivalence)]
[order (.only Order)]
[enum (.only Enum)]]
[control
[parser
["<[0]>" code]]]
["[0]" macro (.only)
[syntax (.only syntax)]]
[math
[number
["i" int]]]]]
["[0]" // (.only)
[primitive (.except)]])
(primitive .public (Qty scale unit)
Int
(def .public quantity
(All (_ scale unit) (-> Int (Qty scale unit)))
(|>> abstraction))
(def .public number
(All (_ scale unit) (-> (Qty scale unit) Int))
(|>> representation))
(def .public equivalence
(All (_ scale unit) (Equivalence (Qty scale unit)))
(implementation
(def (= reference sample)
(i.= (representation reference) (representation sample)))))
(def .public order
(All (_ scale unit) (Order (Qty scale unit)))
(implementation
(def equivalence ..equivalence)
(def (< reference sample)
(i.< (representation reference) (representation sample)))))
(def .public enum
(All (_ scale unit) (Enum (Qty 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) (-> (Qty scale unit) (Qty scale unit) (Qty 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) (-> (Qty scale <p>) (Qty scale <s>) (Qty scale <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 Any a))
in)
(is (-> (Qty Any a) Int)
out)))
(def .public (unit _)
(Ex (_ a) (-> Any (Unit a)))
(implementation
(def in ..quantity)
(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 [<unit> <type>]
[(def .public <unit>
(..unit []))
(.type .public <type>
(~ (..type <unit>)))]
[gram Gram]
[meter Meter]
[litre Litre]
[second Second]
)
|
