Skip to content

Commit 4fd1fcd

Browse files
phantamanta44phantamanta44
committed
Support auxiliary function and datatype declaration (closes #3, closes #4), clean up some deserialization code
1 parent 001b712 commit 4fd1fcd

File tree

10 files changed

+431
-96
lines changed

10 files changed

+431
-96
lines changed

‎src/main/java/org/semgus/java/event/EventParser.java‎

Lines changed: 134 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
import java.util.Map;
1717

1818
import static org.semgus.java.event.SemgusSpecEvent.*;
19+
import static org.semgus.java.event.SmtSpecEvent.*;
1920

2021
/**
2122
* Helper class that deserializes SemGuS parser events from their JSON representations.
@@ -117,8 +118,17 @@ public static SpecEvent parseEvent(String eventJson) throws ParseException, Dese
117118
public static SpecEvent parseEvent(JSONObject eventDto) throws DeserializationException {
118119
String eventType = JsonUtils.getString(eventDto, "$event");
119120
return switch (eventType) {
121+
// meta events
120122
case "set-info" -> parseSetInfo(eventDto);
121123
case "end-of-stream" -> new MetaSpecEvent.StreamEndEvent();
124+
125+
// smt events
126+
case "declare-function" -> parseDeclareFunction(eventDto);
127+
case "define-function" -> parseDefineFunction(eventDto);
128+
case "declare-datatype" -> parseDeclareDatatype(eventDto);
129+
case "define-datatype" -> parseDefineDatatype(eventDto);
130+
131+
// semgus events
122132
case "check-synth" -> new CheckSynthEvent();
123133
case "declare-term-type" -> parseDeclareTermType(eventDto);
124134
case "define-term-type" -> parseDefineTermType(eventDto);
@@ -137,14 +147,119 @@ public static SpecEvent parseEvent(JSONObject eventDto) throws DeserializationEx
137147
* @return The deserialized event.
138148
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "set-info" event.
139149
*/
140-
private static SpecEvent parseSetInfo(JSONObject eventDto) throws DeserializationException {
141-
String keyword = JsonUtils.getString(eventDto, "keyword");
142-
Object valueDtoRaw = JsonUtils.get(eventDto, "value");
150+
private static MetaSpecEvent.SetInfoEvent parseSetInfo(JSONObject eventDto) throws DeserializationException {
151+
return new MetaSpecEvent.SetInfoEvent(
152+
JsonUtils.getString(eventDto, "keyword"),
153+
AttributeValue.deserializeAt(eventDto, "value"));
154+
}
155+
156+
/**
157+
* Deserializes a "declare-function" event.
158+
*
159+
* @param eventDto The JSON representation of the event.
160+
* @return The deserialized event.
161+
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "declare-function" event.
162+
*/
163+
private static DeclareFunctionEvent parseDeclareFunction(JSONObject eventDto) throws DeserializationException {
164+
String name = JsonUtils.getString(eventDto, "name");
165+
JSONObject rankDto = JsonUtils.getObject(eventDto, "rank");
166+
167+
Identifier returnType;
168+
List<Identifier> argumentTypes;
169+
try {
170+
returnType = Identifier.deserializeAt(rankDto, "returnSort");
171+
JSONArray argumentTypesDto = JsonUtils.getArray(rankDto, "argumentSorts");
172+
try {
173+
argumentTypes = Identifier.deserializeList(argumentTypesDto);
174+
} catch (DeserializationException e) {
175+
throw e.prepend("argumentSorts");
176+
}
177+
} catch (DeserializationException e) {
178+
throw e.prepend("rank");
179+
}
180+
181+
return new DeclareFunctionEvent(name, returnType, argumentTypes);
182+
}
183+
184+
/**
185+
* Deserializes a "define-function" event.
186+
*
187+
* @param eventDto The JSON representation of the event.
188+
* @return The deserialized event.
189+
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "define-function" event.
190+
*/
191+
private static DefineFunctionEvent parseDefineFunction(JSONObject eventDto) throws DeserializationException {
192+
// extract the data shared with declare-function
193+
DeclareFunctionEvent declEvent = parseDeclareFunction(eventDto);
194+
195+
JSONObject defnDto = JsonUtils.getObject(eventDto, "definition");
196+
197+
TypedVar[] arguments = new TypedVar[declEvent.argumentTypes().size()];
198+
SmtTerm body;
143199
try {
144-
return new MetaSpecEvent.SetInfoEvent(keyword, AttributeValue.deserialize(valueDtoRaw));
200+
List<String> argNames = JsonUtils.getStrings(defnDto, "arguments");
201+
if (argNames.size() != arguments.length) {
202+
throw new DeserializationException(
203+
String.format(
204+
"Number of argument sorts and lambda arity differ %d != %d",
205+
arguments.length, argNames.size()),
206+
"arguments");
207+
}
208+
for (int i = 0; i < arguments.length; i++) {
209+
arguments[i] = new TypedVar(argNames.get(i), declEvent.argumentTypes().get(i));
210+
}
211+
212+
body = SmtTerm.deserializeAt(defnDto, "body");
145213
} catch (DeserializationException e) {
146-
throw e.prepend("value");
214+
throw e.prepend("definition");
215+
}
216+
217+
return new DefineFunctionEvent(declEvent.name(), declEvent.returnType(), Arrays.asList(arguments), body);
218+
}
219+
220+
/**
221+
* Deserializes a "declare-datatype" event.
222+
*
223+
* @param eventDto The JSON representation of the event.
224+
* @return The deserialized event.
225+
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "declare-datatype" event.
226+
*/
227+
private static DeclareDatatypeEvent parseDeclareDatatype(JSONObject eventDto) throws DeserializationException {
228+
return new DeclareDatatypeEvent(JsonUtils.getString(eventDto, "name")); // TODO arity is currently unused
229+
}
230+
231+
/**
232+
* Deserializes a "define-datatype" event.
233+
*
234+
* @param eventDto The JSON representation of the event.
235+
* @return The deserialized event.
236+
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "define-datatype" event.
237+
*/
238+
private static DefineDatatypeEvent parseDefineDatatype(JSONObject eventDto) throws DeserializationException {
239+
String name = JsonUtils.getString(eventDto, "name");
240+
List<JSONObject> constructorsDto = JsonUtils.getObjects(eventDto, "constructors");
241+
242+
DefineDatatypeEvent.Constructor[] constructors = new DefineDatatypeEvent.Constructor[constructorsDto.size()];
243+
for (int i = 0; i < constructors.length; i++) {
244+
JSONObject constructorDto = constructorsDto.get(i);
245+
try {
246+
String constructorName = JsonUtils.getString(constructorDto, "name");
247+
JSONArray argumentTypesDto = JsonUtils.getArray(constructorDto, "children");
248+
249+
List<Identifier> argumentTypes;
250+
try {
251+
argumentTypes = Identifier.deserializeList(argumentTypesDto);
252+
} catch (DeserializationException e) {
253+
throw e.prepend("children");
254+
}
255+
256+
constructors[i] = new DefineDatatypeEvent.Constructor(constructorName, argumentTypes);
257+
} catch (DeserializationException e) {
258+
throw e.prepend("constructors." + i);
259+
}
147260
}
261+
262+
return new DefineDatatypeEvent(name, Arrays.asList(constructors));
148263
}
149264

150265
/**
@@ -155,7 +270,7 @@ private static SpecEvent parseSetInfo(JSONObject eventDto) throws Deserializatio
155270
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "declare-term-type"
156271
* event.
157272
*/
158-
private static SpecEvent parseDeclareTermType(JSONObject eventDto) throws DeserializationException {
273+
private static DeclareTermTypeEvent parseDeclareTermType(JSONObject eventDto) throws DeserializationException {
159274
return new DeclareTermTypeEvent(JsonUtils.getString(eventDto, "name"));
160275
}
161276

@@ -166,7 +281,7 @@ private static SpecEvent parseDeclareTermType(JSONObject eventDto) throws Deseri
166281
* @return The deserialized event.
167282
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "define-term-type" event.
168283
*/
169-
private static SpecEvent parseDefineTermType(JSONObject eventDto) throws DeserializationException {
284+
private static DefineTermTypeEvent parseDefineTermType(JSONObject eventDto) throws DeserializationException {
170285
String name = JsonUtils.getString(eventDto, "name");
171286
List<JSONObject> constructorsDto = JsonUtils.getObjects(eventDto, "constructors");
172287

@@ -193,7 +308,7 @@ private static SpecEvent parseDefineTermType(JSONObject eventDto) throws Deseria
193308
* @return The deserialized event.
194309
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "chc" event.
195310
*/
196-
private static SpecEvent parseHornClause(JSONObject eventDto) throws DeserializationException {
311+
private static HornClauseEvent parseHornClause(JSONObject eventDto) throws DeserializationException {
197312
JSONObject constructorDto = JsonUtils.getObject(eventDto, "constructor");
198313

199314
// parse constructor specification
@@ -217,27 +332,19 @@ private static SpecEvent parseHornClause(JSONObject eventDto) throws Deserializa
217332
}
218333

219334
// parse constructor arg type identifiers
220-
Identifier[] constructorArgTypes = new Identifier[constructorArgTypesDto.size()];
221-
for (int i = 0; i < constructorArgTypes.length; i++) {
222-
try {
223-
constructorArgTypes[i] = Identifier.deserialize(constructorArgTypesDto.get(i));
224-
} catch (DeserializationException e) {
225-
throw e.prepend("constructor.argumentSorts." + i);
226-
}
335+
List<Identifier> constructorArgTypes;
336+
try {
337+
constructorArgTypes = Identifier.deserializeList(constructorArgTypesDto);
338+
} catch (DeserializationException e) {
339+
throw e.prepend("constructor.argumentSorts");
227340
}
228341
HornClauseEvent.Constructor constructor = new HornClauseEvent.Constructor(
229342
constructorName,
230-
TypedVar.fromNamesAndTypes(constructorArgs, Arrays.asList(constructorArgTypes)),
343+
TypedVar.fromNamesAndTypes(constructorArgs, constructorArgTypes),
231344
returnType);
232345

233346
// parse head relation
234-
JSONObject headDto = JsonUtils.getObject(eventDto, "head");
235-
RelationApp head;
236-
try {
237-
head = RelationApp.deserialize(headDto);
238-
} catch (DeserializationException e) {
239-
throw e.prepend("head");
240-
}
347+
RelationApp head = RelationApp.deserializeAt(eventDto, "head");
241348

242349
// parse body relations
243350
List<JSONObject> bodyRelationsDto = JsonUtils.getObjects(eventDto, "bodyRelations");
@@ -251,13 +358,7 @@ private static SpecEvent parseHornClause(JSONObject eventDto) throws Deserializa
251358
}
252359

253360
// parse semantic constraint
254-
Object constraintDtoRaw = JsonUtils.get(eventDto, "constraint");
255-
SmtTerm constraint;
256-
try {
257-
constraint = SmtTerm.deserialize(constraintDtoRaw);
258-
} catch (DeserializationException e) {
259-
throw e.prepend("constraint");
260-
}
361+
SmtTerm constraint = SmtTerm.deserializeAt(eventDto, "constraint");
261362

262363
// parse variable list
263364
List<String> variablesDto = JsonUtils.getStrings(eventDto, "variables");
@@ -324,13 +425,8 @@ private static SpecEvent parseHornClause(JSONObject eventDto) throws Deserializa
324425
* @return The deserialized event.
325426
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "constraint" event.
326427
*/
327-
private static SpecEvent parseConstraint(JSONObject eventDto) throws DeserializationException {
328-
Object constraintDtoRaw = JsonUtils.get(eventDto, "constraint");
329-
try {
330-
return new ConstraintEvent(SmtTerm.deserialize(constraintDtoRaw));
331-
} catch (DeserializationException e) {
332-
throw e.prepend("constraint");
333-
}
428+
private static ConstraintEvent parseConstraint(JSONObject eventDto) throws DeserializationException {
429+
return new ConstraintEvent(SmtTerm.deserializeAt(eventDto, "constraint"));
334430
}
335431

336432
/**
@@ -340,7 +436,7 @@ private static SpecEvent parseConstraint(JSONObject eventDto) throws Deserializa
340436
* @return The deserialized event.
341437
* @throws DeserializationException If {@code eventDto} is not a valid representation of a "synth-fun" event.
342438
*/
343-
private static SpecEvent parseSynthFun(JSONObject eventDto) throws DeserializationException {
439+
private static SynthFunEvent parseSynthFun(JSONObject eventDto) throws DeserializationException {
344440
String name = JsonUtils.getString(eventDto, "name");
345441
String termType = JsonUtils.getString(eventDto, "termType");
346442

‎src/main/java/org/semgus/java/event/SmtSpecEvent.java‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
package org.semgus.java.event;
2+
3+
import org.semgus.java.object.Identifier;
4+
import org.semgus.java.object.SmtTerm;
5+
import org.semgus.java.object.TypedVar;
6+
7+
import java.util.List;
8+
9+
/**
10+
* A SemGuS parser event of the "smt" type.
11+
*/
12+
public sealed interface SmtSpecEvent extends SpecEvent {
13+
14+
/**
15+
* A "declare-function" event declaring the signature of an auxiliary function.
16+
*
17+
* @param name The name of the function.
18+
* @param returnType The return type of the function.
19+
* @param argumentTypes The types of the arguments to the function.
20+
*/
21+
record DeclareFunctionEvent(
22+
String name,
23+
Identifier returnType,
24+
List<Identifier> argumentTypes
25+
) implements SmtSpecEvent {
26+
// NO-OP
27+
}
28+
29+
/**
30+
* A "define-function" event giving a definition for a previously-declared auxiliary function.
31+
*
32+
* @param name The name of the function.
33+
* @param returnType The return type of the function.
34+
* @param arguments The arguments to the function.
35+
* @param body The body of the function.
36+
*/
37+
record DefineFunctionEvent(
38+
String name,
39+
Identifier returnType,
40+
List<TypedVar> arguments,
41+
SmtTerm body
42+
) implements SmtSpecEvent {
43+
// NO-OP
44+
}
45+
46+
/**
47+
* A "declare-datatype" event declaring the signature of an auxiliary datatype.
48+
*
49+
* @param name The name of the datatype.
50+
*/
51+
record DeclareDatatypeEvent(String name) implements SmtSpecEvent {
52+
// NO-OP
53+
}
54+
55+
/**
56+
* A "define-datatype" event giving a definition for a previously-declared auxiliary datatype.
57+
*
58+
* @param name The name of the datatype.
59+
* @param constructors The constructors of the datatype.
60+
*/
61+
record DefineDatatypeEvent(String name, List<Constructor> constructors) implements SmtSpecEvent {
62+
63+
/**
64+
* A constructor for a datatype.
65+
*
66+
* @param name The name of the constructor.
67+
* @param argumentTypes The types of the arguments to the constructor.
68+
*/
69+
public record Constructor(String name, List<Identifier> argumentTypes) {
70+
// NO-OP
71+
}
72+
73+
}
74+
75+
}

‎src/main/java/org/semgus/java/event/SpecEvent.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@
33
/**
44
* Parent interface for all SemGuS parser events.
55
*/
6-
public sealed interface SpecEvent permits MetaSpecEvent, SemgusSpecEvent {
6+
public sealed interface SpecEvent permits MetaSpecEvent, SmtSpecEvent, SemgusSpecEvent {
77
// NO-OP
88
}

‎src/main/java/org/semgus/java/object/AttributeValue.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
package org.semgus.java.object;
22

33
import org.json.simple.JSONArray;
4+
import org.json.simple.JSONObject;
45
import org.semgus.java.util.DeserializationException;
6+
import org.semgus.java.util.JsonUtils;
57

68
import javax.annotation.Nullable;
79
import java.util.ArrayList;
@@ -39,6 +41,23 @@ static AttributeValue deserialize(@Nullable Object attrValDtoRaw) throws Deseria
3941
String.format("Could not deserialize attribute value \"%s\"", attrValDtoRaw));
4042
}
4143

44+
/**
45+
* Deserializes an attribute value from the SemGuS JSON format at a given key in a parent JSON object.
46+
*
47+
* @param parentDto The parent JSON object.
48+
* @param key The key whose value should be deserialized.
49+
* @return The deserialized attribute value.
50+
* @throws DeserializationException If the value at {@code key} is not a valid representation of an attribute value.
51+
*/
52+
static AttributeValue deserializeAt(JSONObject parentDto, String key) throws DeserializationException {
53+
Object attrValDto = JsonUtils.get(parentDto, key);
54+
try {
55+
return deserialize(attrValDto);
56+
} catch (DeserializationException e) {
57+
throw e.prepend(key);
58+
}
59+
}
60+
4261
/**
4362
* The value for a nullary attribute.
4463
*/

0 commit comments

Comments
 (0)