blob: 55aa3cdd7ef6cd3ca9b7ca3ded9c8ffa6e5488f2 (
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
|
(.module:
[lux #- Ref type]
(lux (control [predicate #+ Pred]
[monad #+ do]
["p" parser])
(data ["e" error #+ Error])
(lang [type "type/" Eq<Type>])
(type abstract)
[macro]
(macro ["s" syntax #+ syntax:]
[poly])))
(abstract: #export (Ref t r)
{#.doc "A refinement 'r' on type 't' based on a predicate."}
{#value t
#predicate (Pred t)}
(def: #export (refinement predicate)
(All [t]
(Ex [r]
(-> (Pred t) (-> t (Maybe (Ref 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] (-> (Ref t r) <output>))
(|> refined @representation (get@ <slot>)))]
[un-refine t #value]
[predicate (Pred t) #predicate]
)
(def: #export (lift transform)
(All [t r]
(-> (-> t t)
(-> (Ref t r) (Maybe (Ref t r)))))
(function [refined]
(let [[value predicate] (@representation refined)
value' (transform value)]
(if (predicate value')
(#.Some (@abstraction {#value value'
#predicate predicate}))
#.None))))
)
(def: (refinement-type constructor-type)
(-> Type (Error Type))
(<| (poly.run constructor-type)
(do p.Monad<Parser>
[[un-refinedT outputT] (poly.function poly.any poly.any)
refined-ex (<| (poly.local (list outputT))
poly.apply (p.after (poly.this .Maybe))
poly.apply (p.after (poly.this ..Ref))
(p.after (poly.this un-refinedT))
poly.existential)]
(wrap (.type (..Ref un-refinedT (#.Ex refined-ex)))))))
(syntax: #export (type [refinement s.symbol])
(do @
[constructorT (macro.find-type refinement)
refinementT (case (refinement-type constructorT)
(#e.Success refinementT)
(wrap refinementT)
(#e.Error error)
(p.fail error))]
(wrap (list (type.to-code refinementT)))))
|
