Skip to content
Snippets Groups Projects
Commit e574db0d authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add initial support for unknown and custom types.

Add support for both custom and unknown custom types.  For now, all unknown
types are simply treated as reals for generation purposes.  Custom types can
be registered with a particular VariableParser using any previously existing
type.  All the generation code ignores the new type name and continues as
before.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@11086 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 0a384c0a
No related branches found
No related tags found
No related merge requests found
......@@ -60,7 +60,13 @@ final public class VariableParser {
return listener.m_variableCollection;
}
private static class VariablesParserToVariables extends VariableParserParserBaseListener {
public void addCustomType(String typeName, VariableType type) {
m_customTypes.put(typeName, type);
}
private final Map<String, VariableType> m_customTypes = new HashMap<String, VariableType>();
private class VariablesParserToVariables extends VariableParserParserBaseListener {
private String currentName;
private VariableType currentType;
private limitingExpressionData currentLimitingExpression;
......@@ -85,6 +91,14 @@ final public class VariableParser {
currentType = new BooleanVariableType();
}
@Override
public void enterUnknown_type(@NotNull VariableParserParser.Unknown_typeContext ctx) {
currentType = m_customTypes.get(ctx.UNKNOWN_TYPE().getText());
if (currentType == null) { // Assume this unknown. For now, pretend a real is wanted.
currentType = new RealVariableType();
}
}
@Override
public void enterSubtype_var(@NotNull VariableParserParser.Subtype_varContext ctx) {
currentLimitingExpression = new limitingExpressionData();
......@@ -142,10 +156,11 @@ final public class VariableParser {
private Map<String, Variable> m_variables = new HashMap<String, Variable>();
public VariableCollection m_variableCollection;
private static class limitingExpressionData {
public String expression;
public String variableName;
}
private Map<String, limitingExpressionData> m_variableLimitingExpressions = new HashMap<String, limitingExpressionData>();
}
private static class limitingExpressionData {
public String expression;
public String variableName;
}
}
......@@ -20,6 +20,7 @@ COLON: ':';
BOOL_TYPE: 'bool';
REAL_TYPE: 'real';
FIXEDT: 'fixedt' -> pushMode(FIXED_TYPE);
UNKNOWN_TYPE: [a-zA-Z_]+;
OPEN_SUBTYPE: '{' -> pushMode(ID_FETCH);
PVS_EXPR_BEGIN: '|' -> pushMode(PVS_EXPR_MODE);
......
......@@ -19,7 +19,8 @@ pvs_expr: PVS_EXPR;
simple_type_info: bool_type
| real_type
| fixed_type ;
| fixed_type
| unknown_type;
bool_type: BOOL_TYPE;
......@@ -27,3 +28,5 @@ real_type: 'real';
fixed_type: 'fixedt' '(' NAT NAT_SEPARATOR NAT ')'
| 'fixedt' '(' NAT NAT_SEPARATOR NAT NAT_SEPARATOR NAT ')';
unknown_type: UNKNOWN_TYPE;
......@@ -141,5 +141,35 @@ public class VariableParserTest {
assertThat(vars.get("z").type().subtypePredicate().toString(), is("(z NotEquals c)"));
}
@Test
public void testCustomType() {
VariableParser variableParser = new VariableParser();
variableParser.addCustomType("myreal", new RealVariableType());
BooleanVariableType customBool = new BooleanVariableType();
customBool.setSubtypePredicate(new Variable("c", new BooleanVariableType()));
variableParser.addCustomType("mybool", customBool);
Map<String, Variable> vars = variableParser.parseVariables("a:myreal,b:mybool").getVariables();
assertThat(vars.size(), is(2));
assertThat(vars.get("a").name(), is("a"));
assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));
assertThat(vars.get("b").name(), is("b"));
assertThat(vars.get("b").type(), is((VariableType) new BooleanVariableType()));
assertThat(vars.get("b").type().subtypePredicate().toString(), is("c"));
}
@Test
public void testUnknownCustomType() {
VariableParser variableParser = new VariableParser();
Map<String, Variable> vars = variableParser.parseVariables("a:unknowntype").getVariables();
assertThat(vars.size(), is(1));
assertThat(vars.get("a").name(), is("a"));
assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));
}
CheckerGenerator generator = new CVC3Generator();
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment