blob: 0c716dd3fb91d879693f7b91ac8cf9eb4f6ae4f3 (
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
|
(.module:
[lux (#- primitive)
[control
[monad (#+ do)]
pipe
["ex" exception (#+ exception:)]]
[data
["." error (#+ Error)]
[text
format]]
[math
["r" random ("#;." monad)]]
["." type ("#;." equivalence)]
[macro
["." code]]
[compiler
[default
["." init]
[evaluation (#+ Eval)]
["." phase
["." analysis (#+ Analysis Operation)
[".A" type]
["." expression]]
[extension
[".E" analysis]]]]]
test])
(def: #export phase
analysis.Phase
expression.compile)
(def: #export state
analysis.State+
[(analysisE.bundle (:coerce Eval [])) (init.compiler [])])
(def: unit
(r.Random Code)
(r;wrap (' [])))
(def: #export primitive
(r.Random [Type Code])
(`` ($_ r.either
(~~ (do-template [<type> <code-wrapper> <value-gen>]
[(r.and (r;wrap <type>) (r;map <code-wrapper> <value-gen>))]
[Any code.tuple (r.list 0 ..unit)]
[Bit code.bit r.bit]
[Nat code.nat r.nat]
[Int code.int r.int]
[Rev code.rev r.rev]
[Frac code.frac r.frac]
[Text code.text (r.unicode 5)]
)))))
(exception: (wrong-inference {expected Type} {inferred Type})
(ex.report ["Expected" (%type expected)]
["Inferred" (%type inferred)]))
(def: (infer-primitive expected-type analysis)
(-> Type (Operation Analysis) (Error Analysis))
(|> analysis
typeA.with-inference
(phase.run ..state)
(case> (#error.Success [inferred-type output])
(if (is? expected-type inferred-type)
(#error.Success output)
(ex.throw wrong-inference [expected-type inferred-type]))
(#error.Failure error)
(#error.Failure error))))
(context: "Primitives"
($_ seq
(test "Can analyse unit."
(|> (infer-primitive Any (..phase (' [])))
(case> (^ (#error.Success (#analysis.Primitive (#analysis.Unit output))))
(is? [] output)
_
#0)))
(<| (times 100)
(`` ($_ seq
(~~ (do-template [<desc> <type> <tag> <random> <constructor>]
[(do @
[sample <random>]
(test (format "Can analyse " <desc> ".")
(|> (infer-primitive <type> (..phase (<constructor> sample)))
(case> (#error.Success (#analysis.Primitive (<tag> output)))
(is? sample output)
_
#0))))]
["bit" Bit #analysis.Bit r.bit code.bit]
["nat" Nat #analysis.Nat r.nat code.nat]
["int" Int #analysis.Int r.int code.int]
["rev" Rev #analysis.Rev r.rev code.rev]
["frac" Frac #analysis.Frac r.frac code.frac]
["text" Text #analysis.Text (r.unicode 5) code.text]
)))))))
|
