blob: 523ad990e21aff9ef2159e202e757c10a61a7ac9 (
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
|
(.require
[lux (.except)
["_" test (.only Test)]
["[0]" ffi (.only import)]
[abstract
[monad (.only do)]]
[control
["[0]" pipe]
["[0]" maybe]
["[0]" try]]
[data
[number
["n" nat]
["i" int]]
["[0]" text (.use "[1]#[0]" equivalence)
["%" \\format (.only format)]]
[collection
["[0]" array (.only Array)]
["[0]" list (.use "[1]#[0]" functor)]]]
[math
["r" random]]
[meta
[compiler
["[0]" analysis]
["[0]" synthesis]]]]
[///
[common (.only Runner)]])
(import java/lang/Integer)
(def (variant run)
(-> Runner Test)
(do [! r.monad]
[num_tags (|> r.nat (at ! each (|>> (n.% 10) (n.max 2))))
tag_in (|> r.nat (at ! each (n.% num_tags)))
.let [last?_in (|> num_tags -- (n.= tag_in))]
value_in r.i64]
(_.property (%.symbol (symbol synthesis.variant))
(|> (synthesis.variant [analysis.#lefts (if last?_in
(-- tag_in)
tag_in)
analysis.#right? last?_in
analysis.#value (synthesis.i64 value_in)])
(run "variant")
(pipe.case
{try.#Success valueT}
(let [valueT (as (Array Any) valueT)]
(and (n.= 3 (array.size valueT))
(let [tag_out (as java/lang/Integer (maybe.trusted (array.read! 0 valueT)))
last?_out (array.read! 1 valueT)
value_out (as Any (maybe.trusted (array.read! 2 valueT)))
same_tag? (|> tag_out ffi.int_to_long (as Nat) (n.= tag_in))
same_flag? (case last?_out
{.#Some last?_out'}
(and last?_in (text#= "" (as Text last?_out')))
{.#None}
(not last?_in))
same_value? (|> value_out (as Int) (i.= value_in))]
(and same_tag?
same_flag?
same_value?))))
{try.#Failure _}
false)))))
(def (tuple run)
(-> Runner Test)
(do [! r.monad]
[size (|> r.nat (at ! each (|>> (n.% 10) (n.max 2))))
tuple_in (r.list size r.i64)]
(_.property (%.symbol (symbol synthesis.tuple))
(|> (synthesis.tuple (list#each (|>> synthesis.i64) tuple_in))
(run "tuple")
(pipe.case
{try.#Success tuple_out}
(let [tuple_out (as (Array Any) tuple_out)]
(and (n.= size (array.size tuple_out))
(list.every? (function (_ [left right])
(i.= left (as Int right)))
(list.zipped_2 tuple_in (array.list tuple_out)))))
{try.#Failure _}
false)))))
(def .public (spec runner)
(-> Runner Test)
(all _.and
(..variant runner)
(..tuple runner)
))
|
