Skip to content

Commit aaeba30

Browse files
geo2ageo2a
committed
Separate kore-rpc-dev and kore-rpc-booster responses for test-vacuous
1 parent 3635d1a commit aaeba30

File tree

3 files changed

+134
-18
lines changed

3 files changed

+134
-18
lines changed

‎booster/test/rpc-integration/test-vacuous/response-vacuous-at-branch.kore-rpc-dev‎

Lines changed: 100 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,100 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "vacuous",
6+
"depth": 0,
7+
"state": {
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "App",
13+
"name": "Lbl'-LT-'generatedTop'-GT-'",
14+
"sorts": [],
15+
"args": [
16+
{
17+
"tag": "App",
18+
"name": "Lbl'-LT-'k'-GT-'",
19+
"sorts": [],
20+
"args": [
21+
{
22+
"tag": "App",
23+
"name": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "inj",
29+
"sorts": [
30+
{
31+
"tag": "SortApp",
32+
"name": "SortState",
33+
"args": []
34+
},
35+
{
36+
"tag": "SortApp",
37+
"name": "SortKItem",
38+
"args": []
39+
}
40+
],
41+
"args": [
42+
{
43+
"tag": "DV",
44+
"sort": {
45+
"tag": "SortApp",
46+
"name": "SortState",
47+
"args": []
48+
},
49+
"value": "init"
50+
}
51+
]
52+
},
53+
{
54+
"tag": "App",
55+
"name": "dotk",
56+
"sorts": [],
57+
"args": []
58+
}
59+
]
60+
}
61+
]
62+
},
63+
{
64+
"tag": "App",
65+
"name": "Lbl'-LT-'int'-GT-'",
66+
"sorts": [],
67+
"args": [
68+
{
69+
"tag": "DV",
70+
"sort": {
71+
"tag": "SortApp",
72+
"name": "SortInt",
73+
"args": []
74+
},
75+
"value": "0"
76+
}
77+
]
78+
},
79+
{
80+
"tag": "App",
81+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
82+
"sorts": [],
83+
"args": [
84+
{
85+
"tag": "DV",
86+
"sort": {
87+
"tag": "SortApp",
88+
"name": "SortInt",
89+
"args": []
90+
},
91+
"value": "0"
92+
}
93+
]
94+
}
95+
]
96+
}
97+
}
98+
}
99+
}
100+
}

‎booster/test/rpc-integration/test-vacuous/response-vacuous-var-at-branch.json‎

Lines changed: 32 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -66,13 +66,13 @@
6666
"sorts": [],
6767
"args": [
6868
{
69-
"tag": "DV",
69+
"tag": "EVar",
70+
"name": "N",
7071
"sort": {
7172
"tag": "SortApp",
7273
"name": "SortInt",
7374
"args": []
74-
},
75-
"value": "0"
75+
}
7676
}
7777
]
7878
},
@@ -95,14 +95,14 @@
9595
]
9696
}
9797
},
98-
"substitution": {
98+
"predicate": {
9999
"format": "KORE",
100100
"version": 1,
101101
"term": {
102102
"tag": "Equals",
103103
"argSort": {
104104
"tag": "SortApp",
105-
"name": "SortInt",
105+
"name": "SortBool",
106106
"args": []
107107
},
108108
"sort": {
@@ -111,22 +111,38 @@
111111
"args": []
112112
},
113113
"first": {
114-
"tag": "EVar",
115-
"name": "N",
116-
"sort": {
117-
"tag": "SortApp",
118-
"name": "SortInt",
119-
"args": []
120-
}
121-
},
122-
"second": {
123114
"tag": "DV",
124115
"sort": {
125116
"tag": "SortApp",
126-
"name": "SortInt",
117+
"name": "SortBool",
127118
"args": []
128119
},
129-
"value": "0"
120+
"value": "true"
121+
},
122+
"second": {
123+
"tag": "App",
124+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
125+
"sorts": [],
126+
"args": [
127+
{
128+
"tag": "EVar",
129+
"name": "N",
130+
"sort": {
131+
"tag": "SortApp",
132+
"name": "SortInt",
133+
"args": []
134+
}
135+
},
136+
{
137+
"tag": "DV",
138+
"sort": {
139+
"tag": "SortApp",
140+
"name": "SortInt",
141+
"args": []
142+
},
143+
"value": "0"
144+
}
145+
]
130146
}
131147
}
132148
}

‎scripts/booster-integration-tests.sh‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,12 @@ for dir in $(ls -d test-*); do
2828
name=${dir##test-}
2929
echo "Running $name..."
3030
case "$name" in
31-
"a-to-f" | "diamond" | "substitutions")
31+
"a-to-f" | "diamond" | "substitutions" | "vacuous")
3232
SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
3333
SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
3434
SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@
3535
;;
36-
"vacuous" | "pathological-add-module")
36+
"pathological-add-module")
3737
SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
3838
SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@
3939
;;

0 commit comments

Comments
 (0)