blob: 0697e5338f48b10168d58e7ecc8e24185bd835de (
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
|
(.module:
[lux #*
["_" test (#+ Test)]
[abstract
[monad (#+ do)]]
[control
[pipe (#+ case>)]
["." try]]
[data
["." maybe]
[number
["n" nat]
["i" int]]
["." text ("#@." equivalence)
["%" format (#+ format)]]
[collection
["." array (#+ Array)]
["." list ("#@." functor)]]]
[math
["r" random]]
["." host (#+ import:)]
[tool
[compiler
["." analysis]
["." synthesis]]]]
[///
[common (#+ Runner)]])
(import: #long java/lang/Integer)
(def: (variant run)
(-> Runner Test)
(do r.monad
[num-tags (|> r.nat (:: @ map (|>> (n.% 10) (n.max 2))))
tag-in (|> r.nat (:: @ map (n.% num-tags)))
#let [last?-in (|> num-tags dec (n.= tag-in))]
value-in r.i64]
(_.test (%.name (name-of synthesis.variant))
(|> (synthesis.variant {#analysis.lefts (if last?-in
(dec tag-in)
tag-in)
#analysis.right? last?-in
#analysis.value (synthesis.i64 value-in)})
(run "variant")
(case> (#try.Success valueT)
(let [valueT (:coerce (Array Any) valueT)]
(and (n.= 3 (array.size valueT))
(let [tag-out (:coerce java/lang/Integer (maybe.assume (array.read 0 valueT)))
last?-out (array.read 1 valueT)
value-out (:coerce Any (maybe.assume (array.read 2 valueT)))
same-tag? (|> tag-out host.int-to-long (:coerce Nat) (n.= tag-in))
same-flag? (case last?-out
(#.Some last?-out')
(and last?-in (text@= "" (:coerce Text last?-out')))
#.None
(not last?-in))
same-value? (|> value-out (:coerce 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 (:: @ map (|>> (n.% 10) (n.max 2))))
tuple-in (r.list size r.i64)]
(_.test (%.name (name-of synthesis.tuple))
(|> (synthesis.tuple (list@map (|>> synthesis.i64) tuple-in))
(run "tuple")
(case> (#try.Success tuple-out)
(let [tuple-out (:coerce (Array Any) tuple-out)]
(and (n.= size (array.size tuple-out))
(list.every? (function (_ [left right])
(i.= left (:coerce Int right)))
(list.zip2 tuple-in (array.to-list tuple-out)))))
(#try.Failure _)
false)))))
(def: #export (spec runner)
(-> Runner Test)
($_ _.and
(..variant runner)
(..tuple runner)
))
|
