blob: edf3cc14b8395dab6cdb1c212618da4d63632dfb (
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
|
(.require
[lux (.except)
["_" test (.only Test)]
[abstract
[monad (.only do)]]
[control
["[0]" pipe]
["[0]" io]
["[0]" try]]
[math
["r" random (.only Random)]]
[meta
["[0]" code]]
[tool
[compiler
[analysis (.only State+)]
["[0]" phase
[macro (.only 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])
(`` (all r.either
(,, (with_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.upper_case_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]
(all _.and
(_.property "lux check"
(check_success+ expander state "lux check" (list typeC exprC) exprT))
(_.property "lux coerce"
(check_success+ expander state "lux coerce" (list typeC other_exprC) exprT))
)))
|
