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
|
... 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/.
(.require
[library
[lux (.except only type)
[abstract
[monad (.only do)]]
[control
["?" parser]
[function
[predicate (.only Predicate)]]]
["[0]" meta (.only)
["[0]" code
["<[1]>" \\parser]]
["[0]" macro (.only)
[syntax (.only syntax)]]]]]
["[0]" // (.only)
["?[1]" \\parser]
["[0]" nominal (.except def)]])
(nominal.def .public (Refined super %)
(Record
[#value super
#predicate (Predicate super)])
(.type .public (Refiner super %)
(-> super
(Maybe (Refined super %))))
(def .public (refiner predicate)
(All (_ super)
(Ex (_ %)
(-> (Predicate super)
(Refiner super %))))
(function (_ value)
(if (predicate value)
{.#Some (abstraction [#value value
#predicate predicate])}
{.#None})))
(with_template [<name> <slot> <output>]
[(def .public <name>
(All (_ super %)
(-> (Refined super %)
<output>))
(|>> representation
(the <slot>)))]
[value #value super]
[predicate #predicate (Predicate super)]
)
(def .public (lifted transform)
(All (_ super %)
(-> (-> super super)
(-> (Refined super %)
(Maybe (Refined super %)))))
(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 (_ super %)
(-> (Refiner super %) (List super)
(List (Refined super %))))
(when values
{.#Item head tail}
(when (refiner head)
{.#Some refined}
{.#Item refined (only refiner tail)}
{.#None}
(only refiner tail))
{.#End}
{.#End}))
(def .public (partition refiner values)
(All (_ super %)
(-> (Refiner super %) (List super)
[(List (Refined super %))
(List super)]))
(when values
{.#Item head tail}
(let [[yes no] (partition refiner tail)]
(when (refiner head)
{.#Some refined}
[{.#Item refined yes}
no]
{.#None}
[yes
{.#Item head no}]))
{.#End}
[{.#End} {.#End}]))
(def .public type
(syntax (_ [it <code>.any])
(macro.with_symbols ['_ 'super '%]
(do meta.monad
[it (meta.eval Type (` (.type_of ((is (All ((, '_) (, 'super) (, '%))
(-> (..Refiner (, 'super) (, '%))
(..Refiner (, 'super) (, '%))))
(|>>))
(, it)))))
[super %] (|> (as Type it)
(?//.result (?//.applied (?.after (?//.exactly ..Refiner)
(all ?.and ?//.any ?//.any))))
meta.of_try)]
(in (list (` (.type_literal (..Refined (, (//.code super))
(, (//.code %)))))))))))
|
