blob: 4142534e7199e6583cf2f9e87022c29f4dae9f8d (
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
|
(.using
[library
[lux (.except type only)
[abstract
[predicate (.only Predicate)]]
[control
[parser
["<[0]>" code]]]
["[0]" macro
[syntax (.only syntax:)]]
["[0]" type
[primitive "*"]]]])
(primitive: .public (Refined t %)
(Record
[#value t
#predicate (Predicate t)])
(type: .public (Refiner t %)
(-> t (Maybe (Refined t %))))
(def: .public (refiner predicate)
(All (_ t)
(Ex (_ %)
(-> (Predicate t) (Refiner t %))))
(function (_ value)
(if (predicate value)
{.#Some (abstraction [#value value
#predicate predicate])}
{.#None})))
(template [<name> <output> <slot>]
[(def: .public <name>
(All (_ t %) (-> (Refined t %) <output>))
(|>> representation (the <slot>)))]
[value t #value]
[predicate (Predicate t) #predicate]
)
(def: .public (lifted transform)
(All (_ t %)
(-> (-> t t)
(-> (Refined t %) (Maybe (Refined t %)))))
(function (_ refined)
(let [(open "_[0]") (representation refined)
value' (transform _#value)]
(if (_#predicate value')
{.#Some (abstraction [..#value value'
..#predicate _#predicate])}
{.#None}))))
)
(def: .public (only refiner values)
(All (_ t %)
(-> (Refiner t %) (List t) (List (Refined t %))))
(case values
{.#End}
{.#End}
{.#Item head tail}
(case (refiner head)
{.#Some refined}
{.#Item refined (only refiner tail)}
{.#None}
(only refiner tail))))
(def: .public (partition refiner values)
(All (_ t %)
(-> (Refiner t %) (List t) [(List (Refined t %)) (List t)]))
(case values
{.#End}
[{.#End} {.#End}]
{.#Item head tail}
(let [[yes no] (partition refiner tail)]
(case (refiner head)
{.#Some refined}
[{.#Item refined yes}
no]
{.#None}
[yes
{.#Item head no}]))))
(syntax: .public (type [refiner <code>.any])
... TODO: Switch to the cleaner approach ASAP.
(macro.with_symbols [g!t g!% g!_ g!:refiner:]
(in (list (` (let [... (~ g!_) (.is (.Ex ((~ g!_) (~ g!t) (~ g!%))
... (..Refined (~ g!t) (~ g!%)))
... (~ refiner))
]
(.case (.type_of (~ refiner))
{.#Apply (~ g!%) {.#Apply (~ g!t) (~ g!:refiner:)}}
(.type (..Refined (~ g!t) (~ g!%)))
(~ g!_)
(.undefined))))
... (` ((~! type.by_example) [(~ g!t) (~ g!%)]
... (..Refiner (~ g!t) (~ g!%))
... (~ refiner)
... (..Refined (~ g!t) (~ g!%))))
))))
|
