blob: da7c3802574ac6671ead6e0267142079c742bab3 (
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
|
(.using
[library
[lux (.except type)
[abstract
[equivalence (only Equivalence)]]
[control
[parser
["<[0]>" code]]]
[macro (.only with_symbols)
[syntax (.only syntax)]]
["[0]" type
[primitive (.except)]]]])
(primitive .public (Class t c %)
(-> t c)
(def: .public class
(All (_ t c)
(Ex (_ %)
(-> (-> t c) (Class t c %))))
(|>> abstraction))
(primitive .public (Quotient t c %)
(Record
[#value t
#label c])
(def: .public (quotient class value)
(All (_ t c %)
(-> (Class t c %) t
(Quotient t c %)))
(abstraction [#value value
#label ((representation Class class) value)]))
(with_template [<name> <output> <slot>]
[(def: .public <name>
(All (_ t c %) (-> (Quotient t c %) <output>))
(|>> representation (the <slot>)))]
[value t #value]
[label c #label]
)
)
)
(def: .public type
(syntax (_ [class <code>.any])
... TODO: Switch to the cleaner approach ASAP.
(with_symbols [g!t g!c g!% g!_ g!:quotient:]
(in (list (` (let [ ... (~ g!_) (.is (.Ex ((~ g!_) (~ g!t) (~ g!c) (~ g!%))
... (..Class (~ g!t) (~ g!c) (~ g!%)))
... (~ class))
]
(.case (.type_of (~ class))
{.#Apply (~ g!%) {.#Apply (~ g!c) {.#Apply (~ g!t) (~ g!:quotient:)}}}
(.type (..Quotient (~ g!t) (~ g!c) (~ g!%)))
(~ g!_)
(.undefined))))
... (` ((~! type.by_example) [(~ g!t) (~ g!c) (~ g!%)]
... (is (..Class (~ g!t) (~ g!c) (~ g!%))
... (~ class))
... (..Quotient (~ g!t) (~ g!c) (~ g!%))))
)))))
(def: .public (equivalence super)
(All (_ t c %) (-> (Equivalence c) (Equivalence (..Quotient t c %))))
(implementation
(def: (= reference sample)
(at super = (..label reference) (..label sample)))))
|
