blob: c51f0cced9a682daea3bde018a7f667f8b3b3a0d (
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
|
(.using
[lux "*"
["_" test {"+" Test}]
[abstract
[monad {"+" do}]]
[control
["[0]" pipe]
["[0]" io]
["[0]" try]]
[math
["r" random {"+" Random}]]
[macro
["[0]" code]]
[tool
[compiler
[analysis {"+" State+}]
["[0]" phase
[macro {"+" Expander}]
["[0]" analysis
["[1]/[0]" scope]
["[1]/[0]" type]]]]]])
(def: (check_success+ expander state extension params output_type)
(-> Expander State+ Text (List Code) Type Bit)
(|> (analysis/scope.with_scope ""
(analysis/type.with_type output_type
(analysis.phase expander (` ((~ (code.text extension)) (~+ params))))))
(phase.result state)
(pipe.case
{try.#Success _}
true
{try.#Failure _}
false)))
(def: check
(Random [Code Type Code])
(`` ($_ r.either
(~~ (template [<random> <type> <code>]
[(do r.monad
[value <random>]
(in [(` <type>)
<type>
(<code> value)]))]
[r.bit {0 #0 "#Bit" {0 #0}} code.bit]
[r.nat {0 #0 "#I64" {0 #1 {0 #0 "#Nat" {0 #0}} {0 #0}}} code.nat]
[r.int {0 #0 "#I64" {0 #1 {0 #0 "#Int" {0 #0}} {0 #0}}} code.int]
[r.rev {0 #0 "#I64" {0 #1 {0 #0 "#Rev" {0 #0}} {0 #0}}} code.rev]
[r.safe_frac {0 #0 "#Frac" {0 #0}} code.frac]
[(r.ascii/upper_alpha 5) {0 #0 "#Text" {0 #0}} code.text]
)))))
(def: .public (spec expander state)
(-> Expander State+ Test)
(do r.monad
[[typeC exprT exprC] ..check
[other_typeC other_exprT other_exprC] ..check]
($_ _.and
(_.test "lux check"
(check_success+ expander state "lux check" (list typeC exprC) exprT))
(_.test "lux coerce"
(check_success+ expander state "lux coerce" (list typeC other_exprC) exprT))
)))
|
