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
|
++ Contributed by Stephen Wilson.
)abbrev domain CWMMT CompWithMappingModeTest
CompWithMappingModeTest() : Exports == Implementation where
Exports == with
runTests : () -> Boolean
Implementation == add
REC ==> Record(field1 : Integer, field2 : String)
UN ==> Union(rec : REC, str : String)
-- The following function accepts a map as argument to test
-- compWithMappingMode.
mapper(fn : Integer -> Boolean, n: Integer) : Boolean == fn n
-- We use the following as a target for currying and to pass to
-- mapper above.
pred(x: Integer, y: Integer) : Boolean ==
x < y => true
true
test1(x : Integer) : Boolean ==
r : REC := [1, ""]
mapper(pred(r.field1, #1), 1)
test2(x : Integer) : Boolean ==
r : REC := [1, ""]
i : Integer := 1
mapper(pred(r.field1 + x, #1), 1)
test3(x : Integer) : Boolean ==
r : REC := [1, ""]
i : Integer := 1
mapper(pred(r.field1 + i, #1), 1)
test4(x : Integer) : Boolean ==
r : REC := [1, ""]
i : Integer := 1
mapper(pred((r.field1 + min(#(r.field2), i)), #1), 1)
test5(x : Integer) : Boolean ==
r : REC := [1, ""]
i : Integer := 1
mapper(pred((r.field1 + min(#(r.field2), i + x)), #1), 1)
test6(x : Integer) : Boolean ==
u : UN := [[1, ""]$REC]
mapper(pred(u.rec.field1, #1), 1)
test7(x : Integer) : Boolean ==
u : UN := [[1, ""]$REC]
i : Integer := 1
mapper(pred(u.rec.field1 + x, #1), 1)
test8(x : Integer) : Boolean ==
u : UN := [[1, ""]$REC]
i : Integer := 1
mapper(pred(u.rec.field1 + i, #1), 1)
test9(x : Integer) : Boolean ==
u : UN := [[1, ""]$REC]
i : Integer := 1
mapper(pred((u.rec.field1 + min(#(u.rec.field2), i)), #1), 1)
test10(x : Integer) : Boolean ==
u : UN := [[1, ""]$REC]
i : Integer := 1
mapper(pred((u.rec.field1 + min(#(u.rec.field2), i + x)), #1), 1)
runTests() : Boolean ==
test1(1) and test2(1) and test3(1) _
and test4(1) and test5(1) _
and test6(1) and test7(1) _
and test8(1) and test9(1) _
and test10(1)
|
