blob: 0881eb8eb394ba69d812c72c50d0845e70a20acd (
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
|
(.module:
[lux (#- type)
[control
[predicate (#+ Predicate)]
[monad (#+ do)]
["p" parser]]
[data
["." error (#+ Error)]]
["." type ("#/." equivalence)
abstract]
["." macro
["s" syntax (#+ syntax:)]
["." poly]]])
(abstract: #export (Refined t r)
{#.doc "A refined type 'r' of base type 't' using a predicate."}
{#value t
#predicate (Predicate t)}
(type: #export (Refiner t r)
(-> t (Maybe (Refined t r))))
(def: #export (refinement predicate)
(All [t]
(Ex [r]
(-> (Predicate t) (Refiner t r))))
(function (_ un-refined)
(if (predicate un-refined)
(#.Some (:abstraction {#value un-refined
#predicate predicate}))
#.None)))
(do-template [<name> <output> <slot>]
[(def: #export (<name> refined)
(All [t r] (-> (Refined t r) <output>))
(|> refined :representation (get@ <slot>)))]
[un-refine t #value]
[predicate (Predicate t) #predicate]
)
(def: #export (lift transform)
(All [t r]
(-> (-> t t)
(-> (Refined t r) (Maybe (Refined t r)))))
(function (_ refined)
(let [[value predicate] (:representation refined)
value' (transform value)]
(if (predicate value')
(#.Some (:abstraction {#value value'
#predicate predicate}))
#.None))))
)
(def: #export (filter refiner values)
(All [t r] (-> (Refiner t r) (List t) (List (Refined t r))))
(case values
#.Nil
#.Nil
(#.Cons head tail)
(case (refiner head)
(#.Some refined)
(#.Cons refined (filter refiner tail))
#.None
(filter refiner tail))))
(def: #export (partition refiner values)
(All [t r] (-> (Refiner t r) (List t) [(List (Refined t r)) (List t)]))
(case values
#.Nil
[#.Nil #.Nil]
(#.Cons head tail)
(let [[yes no] (partition refiner tail)]
(case (refiner head)
(#.Some refined)
[(#.Cons refined yes)
no]
#.None
[yes
(#.Cons head no)]))))
(def: (refinement-type constructor-type)
(-> Type (Error Type))
(<| (poly.run constructor-type)
(do p.monad
[[un-refinedT refined-ex] (poly.apply (p.after (poly.exactly ..Refiner)
(p.and poly.any poly.existential)))]
(wrap (.type (..Refined un-refinedT (#.Ex refined-ex)))))))
(syntax: #export (type {refinement s.identifier})
(do @
[constructorT (macro.find-type refinement)
refinementT (case (refinement-type constructorT)
(#error.Success refinementT)
(wrap refinementT)
(#error.Failure error)
(p.fail error))]
(wrap (list (type.to-code refinementT)))))
|
