blob: e0b0af6380c1fa0fe0323cba7208fe6805f5c881 (
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)]]
["[0]" macro (.only)
[syntax (.only syntax)]]
[math
[number
["i" int]]]
[meta
["[0]" code
["<[1]>" \\parser]]]]]
["[0]" // (.only)
[primitive (.except)]])
(primitive .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 a)
(Interface
(is (-> Int (Measure Any a))
in)
(is (-> (Measure Any a) Int)
out)))
(def .public (unit _)
(Ex (_ a) (-> Any (Unit a)))
(implementation
(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 [<unit> <type>]
[(def .public <unit>
(..unit []))
(.type .public <type>
(, (..type <unit>)))]
[gram Gram]
[meter Meter]
[litre Litre]
[second Second]
)
|
