diff --git a/AlgebraicDataflowArchitectureModel/models/JumpGame.model b/AlgebraicDataflowArchitectureModel/models/JumpGame.model index d8b002b..36ce9b7 100644 --- a/AlgebraicDataflowArchitectureModel/models/JumpGame.model +++ b/AlgebraicDataflowArchitectureModel/models/JumpGame.model @@ -3,8 +3,8 @@ out time(t:Double, gravity(y)) == t + 0.01 } channel CIO2 { - out move(v:Pair, moveX(x:Double)) == pair(x, snd(v)) - out move(v, moveY(y:Double)) == pair(fst(v), y) + out move(v:Pair, moveX(x:Double)) == pair(x, right(v)) + out move(v, moveY(y:Double)) == pair(left(v), y) } channel CIO3 { out mass(m:Double, setMass(x:Double)) == x @@ -17,34 +17,34 @@ ref onground(o, update1(f2, m2, o)) in force(f, update1(f2, m2, o)) == f2 in mass(m, update1(f2, m2, o)) == m2 - out acceleration(a:Pair, update1(f2, m2, o)) == if(o, pair(fst(f2) / m2, 0.0), pair(fst(f2) / m2, snd(f2) / m2)) + out acceleration(a:Pair, update1(f2, m2, o)) == if(o, pair(left(f2) / m2, 0.0), pair(left(f2) / m2, right(f2) / m2)) } channel C2 { ref onground(o, update3(a2, o)) in acceleration(a, update3(a2, o)) == a2 - out velocity(v:Pair, update3(a2, o)) == if(and(o, lt(snd(v), 0.0)), - pair(fst(v) + 0.01 * fst(a2), 0.0), - pair(fst(v) + 0.01 * fst(a2), snd(v) + 0.01 * snd(a2))) + out velocity(v:Pair, update3(a2, o)) == if(and(o, lt(right(v), 0.0)), + pair(left(v) + 0.01 * left(a2), 0.0), + pair(left(v) + 0.01 * left(a2), right(v) + 0.01 * right(a2))) } channel C3 { ref onground(o, update4(m2, o)) in move(m, update4(m2, o)) == m2 - out velocity(v:Pair, update4(m2, o)) == if(and(o, ge(snd(m2), 0.0)), m2, v) + out velocity(v:Pair, update4(m2, o)) == if(and(o, ge(right(m2), 0.0)), m2, v) } channel C4 { in velocity(v, update5(v2, g)) == v2 ref ground(g, update5(v2, g)) - out position(p:Pair, update5(v2, g)) == if(and(eq(g, true), lt(snd(p) + 0.01 * snd(v2), 0.0)), - pair(fst(p) + 0.01 * fst(v2), 0.0), - pair(fst(p) + 0.01 * fst(v2), snd(p) + 0.01 * snd(v2))) + out position(p:Pair, update5(v2, g)) == if(and(eq(g, true), lt(right(p) + 0.01 * right(v2), 0.0)), + pair(left(p) + 0.01 * left(v2), 0.0), + pair(left(p) + 0.01 * left(v2), right(p) + 0.01 * right(v2))) } channel C5 { in position(p, update2(p2, g2)) == p2 in ground(g, update2(p2, g2)) == g2 - out onground(o:Bool, update2(p2, g2)) == and(eq(g2, true), le(snd(p2), 0.0)) + out onground(o:Bool, update2(p2, g2)) == and(eq(g2, true), le(right(p2), 0.0)) } channel C6 { in position(p, update6(p2)) == p2 - out clear(c:Bool, update6(p2)) == if(gt(fst(p2), 100.0), true, false) - out gameover(go:Bool, update6(p2)) == if(lt(snd(p2), -1.0), true, false) + out clear(c:Bool, update6(p2)) == if(gt(left(p2), 100.0), true, false) + out gameover(go:Bool, update6(p2)) == if(lt(right(p2), -1.0), true, false) } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/models/Twitter.model b/AlgebraicDataflowArchitectureModel/models/Twitter.model index f02f134..57de3b3 100644 --- a/AlgebraicDataflowArchitectureModel/models/Twitter.model +++ b/AlgebraicDataflowArchitectureModel/models/Twitter.model @@ -1,11 +1,9 @@ channel a_Tweet { out a_tweets(l:List, a_tweet(t:Str, time:Long)) == cons(tuple(time, t), l) - out a_tweets(l, e) == l } channel a_Follow { out a_following(f:List, a_follow(u:Int)) == cons(u, f) - out a_following(f, e) == f } channel a_Home { @@ -18,12 +16,10 @@ channel b_Tweet { out b_tweets(l:List, b_tweet(t:Str, time:Long)) == cons(tuple(time, t), l) - out b_tweets(l, e) == l } channel b_Follow { out b_following(f:List, b_follow(u:Int)) == cons(u, f) - out b_following(f, e) == f } channel b_Home { @@ -36,12 +32,10 @@ channel c_Tweet { out c_tweets(l:List, c_tweet(t:Str, time:Long)) == cons(tuple(time, t), l) - out c_tweets(l, e) == l } channel c_Follow { out c_following(f:List, c_follow(u:Int)) == cons(u, f) - out c_following(f, e) == f } channel c_Home { diff --git a/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model b/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model index 02ea307..0a14140 100644 --- a/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model +++ b/AlgebraicDataflowArchitectureModel/models/WeatherObservationSystem.model @@ -1,7 +1,11 @@ -channel CIO { +channel CIO1 { out temp_f(p:Double, observe(x)) == x } +channel CIO2 { + out highest(h:Double, reset(v)) == v +} + channel C1{ in temp_f(q:Double, conversion(y)) == y out temp_c(r:Double, conversion(z)) == (z-32) / 1.8 @@ -9,5 +13,5 @@ channel C2{ in temp_f(q:Double, update(y)) == y - out highest(r:Double, update(z)) == if(gt(z, r), z, r) + out highest(h:Double, update(z)) == if(gt(z, h), z, h) } \ No newline at end of file diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/JavaCodeGenerator.java b/AlgebraicDataflowArchitectureModel/src/algorithms/JavaCodeGenerator.java index 7613052..821a517 100644 --- a/AlgebraicDataflowArchitectureModel/src/algorithms/JavaCodeGenerator.java +++ b/AlgebraicDataflowArchitectureModel/src/algorithms/JavaCodeGenerator.java @@ -258,8 +258,17 @@ if(isCreatedPair) continue; if(model.getType("Pair").isAncestorOf(rn.getIdentifierTemplate().getResourceStateType())) { TypeDeclaration type = new TypeDeclaration("Pair"); - type.addField(new FieldDeclaration(new Type("Double","T"), "first")); - type.addField(new FieldDeclaration(new Type("Double","T"), "second")); + type.addField(new FieldDeclaration(new Type("Double", "T"), "left")); + type.addField(new FieldDeclaration(new Type("Double", "T"), "right")); + + MethodDeclaration constructor = new MethodDeclaration("Pair", true); + constructor.addParameter(new VariableDeclaration(new Type("Double", "T"), "left")); + constructor.addParameter(new VariableDeclaration(new Type("Double", "T"), "right")); + Block block = new Block(); + block.addStatement("this.left = left;"); + block.addStatement("this.right = right;"); + constructor.setBody(block); + type.addMethod(constructor); for(FieldDeclaration field : type.getFields()) { MethodDeclaration getter = new MethodDeclaration( @@ -324,42 +333,11 @@ } else { String cons = "\t" + "private " + field.getType().getInterfaceTypeName() + " " + field.getName() + " = new " + field.getType().getTypeName() + "("; - for (TypeDeclaration tree : codeTree) { - if (field.getType().getTypeName() == tree.getTypeName()) { - for (VariableDeclaration var : tree.getConstructors()) { - cons += var.getName() + ","; - } - if (!tree.getConstructors().isEmpty()) - cons = cons.substring(0, cons.length() - 1); - break; - } - } cons += ");"; codes.add(cons); } } codes.add(""); - if (type.getTypeName() != mainTypeName) { - if (!type.getConstructors().isEmpty()) { - String cons = "\t" + "public " + type.getTypeName() + "("; - for (VariableDeclaration constructor : type.getConstructors()) { - cons += constructor.getType().getTypeName() + " " + constructor.getName() + ","; - } - if (!type.getConstructors().isEmpty()) - cons = cons.substring(0, cons.length() - 1); - cons += "){"; - codes.add(cons); - for (FieldDeclaration field : type.getFields()) { - for (VariableDeclaration vari : type.getConstructors()) { - if (field.getType().getTypeName().equals(vari.getType().getTypeName())) { - codes.add("\t\t" + "this." + field.getName() + " = " + field.getName() + ";"); - } - } - } - codes.add("\t" + "}"); - codes.add(""); - } - } for (MethodDeclaration method : type.getMethods()) { String varstr = "\t" + "public " + method.getReturnType().getInterfaceTypeName() + " " + method.getName() + "("; diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyCodeGenerator.java b/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyCodeGenerator.java index b3cef51..8c7a428 100644 --- a/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyCodeGenerator.java +++ b/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyCodeGenerator.java @@ -26,6 +26,7 @@ import models.dataConstraintModel.DataConstraintModel; import models.dataConstraintModel.IdentifierTemplate; import models.dataFlowModel.DataFlowModel; +import models.dataFlowModel.DataflowChannelGenerator; import models.dataFlowModel.DataflowChannelGenerator.IResourceStateAccessor; import models.dataFlowModel.PushPullAttribute; import models.dataFlowModel.PushPullValue; @@ -127,6 +128,24 @@ } } + // Declare a client field to connect to the source resource of reference transfer. + if (!bDeclareClientField) { + for (ChannelGenerator cg : model.getChannelGenerators()) { + DataflowChannelGenerator dcg = ((DataflowChannelGenerator) cg); + for (ChannelMember cm : dcg.getOutputChannelMembers()) { + if (cm.getIdentifierTemplate().getResourceName().equals(type.getTypeName().toLowerCase())) { + if (dcg.getReferenceChannelMembers().size() > 0) { + // If there exists one or more reference channel member. + type.addField(new FieldDeclaration(typeClient, "client", "ClientBuilder.newClient()")); + bDeclareClientField = true; + break; + } + } + } + if (bDeclareClientField) break; + } + } + // Declare input methods in resources. for (ChannelGenerator cg : model.getIOChannelGenerators()) { for (ChannelMember cm : cg.getChannelMembers()) { @@ -190,6 +209,42 @@ codes.add(cu); } + // Declare the Pair class. + boolean isCreatedPair = false; + for(Node n : resources) { + ResourceNode rn = (ResourceNode) n; + if(isCreatedPair) continue; + if(model.getType("Pair").isAncestorOf(rn.getIdentifierTemplate().getResourceStateType())) { + TypeDeclaration type = new TypeDeclaration("Pair"); + type.addField(new FieldDeclaration(new Type("Double", "T"), "left")); + type.addField(new FieldDeclaration(new Type("Double", "T"), "right")); + + MethodDeclaration constructor = new MethodDeclaration("Pair", true); + constructor.addParameter(new VariableDeclaration(new Type("Double", "T"), "left")); + constructor.addParameter(new VariableDeclaration(new Type("Double", "T"), "right")); + Block block = new Block(); + block.addStatement("this.left = left;"); + block.addStatement("this.right = right;"); + constructor.setBody(block); + type.addMethod(constructor); + + for(FieldDeclaration field : type.getFields()) { + MethodDeclaration getter = new MethodDeclaration( + "get" + field.getName().substring(0,1).toUpperCase() + field.getName().substring(1), + new Type("Double","T")); + getter.setBody(new Block()); + getter.getBody().addStatement("return " + field.getName() + ";"); + type.addMethod(getter); + } + + CompilationUnit cu = new CompilationUnit(type); + cu.addImport(new ImportDeclaration("java.util.*")); + codes.add(cu); + + isCreatedPair = true; + } + } + return codes; } @@ -208,42 +263,11 @@ } else { String cons = "\t" + "private " + field.getType().getInterfaceTypeName() + " " + field.getName() + " = new " + field.getType().getTypeName() + "("; - for (TypeDeclaration tree : codeTree) { - if (field.getType().getTypeName() == tree.getTypeName()) { - for (VariableDeclaration var : tree.getConstructors()) { - cons += var.getName() + ","; - } - if (!tree.getConstructors().isEmpty()) - cons = cons.substring(0, cons.length() - 1); - break; - } - } cons += ");"; codes.add(cons); } } codes.add(""); - if (type.getTypeName() != mainTypeName) { - if (!type.getConstructors().isEmpty()) { - String cons = "\t" + "public " + type.getTypeName() + "("; - for (VariableDeclaration constructor : type.getConstructors()) { - cons += constructor.getType().getTypeName() + " " + constructor.getName() + ","; - } - if (!type.getConstructors().isEmpty()) - cons = cons.substring(0, cons.length() - 1); - cons += "){"; - codes.add(cons); - for (FieldDeclaration field : type.getFields()) { - for (VariableDeclaration vari : type.getConstructors()) { - if (field.getType().getTypeName().equals(vari.getType().getTypeName())) { - codes.add("\t\t" + "this." + field.getName() + " = " + field.getName() + ";"); - } - } - } - codes.add("\t" + "}"); - codes.add(""); - } - } for (MethodDeclaration method : type.getMethods()) { String varstr = "\t" + "public " + method.getReturnType().getInterfaceTypeName() + " " + method.getName() + "("; diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyMethodBodyGenerator.java b/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyMethodBodyGenerator.java index 3606bed..a9788fb 100644 --- a/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyMethodBodyGenerator.java +++ b/AlgebraicDataflowArchitectureModel/src/algorithms/JerseyMethodBodyGenerator.java @@ -93,7 +93,7 @@ updateStatement = sideEffects[0] + "this.value = " + curState + ";"; } if (update.getBody() == null || !update.getBody().getStatements().contains(updateStatement)) { - // add an update statement of the statement of dst side resource. + // add an update statement of the state of dst side resource. update.addFirstStatement(updateStatement); if (d.getChannelGenerator().getReferenceChannelMembers().size() > 0) { // For each reference channel member, get the current state of the reference side resource by pull data transfer. @@ -163,7 +163,7 @@ srcResName = srcResourceName; } if (!chainedCalls.contains(srcUpdate)) { - srcUpdate.addStatement(getHttpMethodParamsStatement(srcType.getTypeName(), src.getIdentifierTemplate().getResourceStateType(), srcResourceName)); + srcUpdate.addStatement(getHttpMethodParamsStatement(srcType.getTypeName(), src.getIdentifierTemplate().getResourceStateType(), srcResourceName, "this.value")); srcUpdate.addStatement("String result = " + getHttpMethodCallStatement(baseURL, dstResourceName, srcResName, httpMethod)); chainedCalls.add(srcUpdate); } else { @@ -179,7 +179,7 @@ srcResName = srcResourceName; } if (!chainedCalls.contains(srcInput)) { - srcInput.addStatement(getHttpMethodParamsStatement(srcType.getTypeName(), src.getIdentifierTemplate().getResourceStateType(), srcResourceName)); + srcInput.addStatement(getHttpMethodParamsStatement(srcType.getTypeName(), src.getIdentifierTemplate().getResourceStateType(), srcResourceName, "this.value")); srcInput.addStatement("String result = " + getHttpMethodCallStatement(baseURL, dstResourceName, srcResName, httpMethod)); chainedCalls.add(srcInput); } else { @@ -318,15 +318,15 @@ return decoded; } - private static String getHttpMethodParamsStatement(String callerResourceName, Type paramType, String paramName) { + private static String getHttpMethodParamsStatement(String callerResourceName, Type paramType, String paramName, String value) { if (DataConstraintModel.typeList.isAncestorOf(paramType)) { Type compType = TypeInference.getListComponentType(paramType); String statements = "Form form = new Form();\n"; String wrapperType = DataConstraintModel.getWrapperType(compType); if (wrapperType == null) { - statements += "for (" + compType.getInterfaceTypeName() + " i: " + paramName + ") {\n"; + statements += "for (" + compType.getInterfaceTypeName() + " i: " + value + ") {\n"; } else { - statements += "for (" + wrapperType + " i: " + paramName + ") {\n"; + statements += "for (" + wrapperType + " i: " + value + ") {\n"; } if (DataConstraintModel.typeTuple.isAncestorOf(compType) || DataConstraintModel.typeList.isAncestorOf(compType)) { statements += "\tform.param(\"" + paramName + "\", new ObjectMapper().writeValueAsString(i));\n"; @@ -338,7 +338,7 @@ return statements; // return "Entity entity = Entity.entity(" + paramName + ".toString(), MediaType.APPLICATION_JSON);"; } - return "Entity
entity = Entity.entity(new Form().param(\"" + paramName + "\", " + CodeUtil.getToStringExp(paramType.getImplementationTypeName(), paramName) + "), MediaType.APPLICATION_FORM_URLENCODED_TYPE);"; + return "Entity entity = Entity.entity(new Form().param(\"" + paramName + "\", " + CodeUtil.getToStringExp(paramType.getImplementationTypeName(), value) + "), MediaType.APPLICATION_FORM_URLENCODED_TYPE);"; } private static String getHttpMethodCallStatement(String baseURL, String resourceName, String srcResName, String httpMethod) { diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java b/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java index 73f9ef3..5c1ebbf 100644 --- a/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java +++ b/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java @@ -517,6 +517,82 @@ updateExps.put(System.identityHashCode(arg), arg); } tuple.put(System.identityHashCode(tupleExps), argType); + } else if (symbol.equals(DataConstraintModel.left)) { + // If the root symbol of the term is left. + List pairExps = new ArrayList<>(); + Expression arg = t.getChildren().get(0); + pairExps.add(arg); + expToPair.put(System.identityHashCode(arg), pairExps); + pairExps.add(t); + expToPair.put(System.identityHashCode(t), pairExps); + pairExps.add(null); + Type argType = null; + if (arg instanceof Variable) { + argType = ((Variable) arg).getType(); + } else if (arg instanceof Term) { + argType = ((Term) arg).getType(); + } + Type newPairType = DataConstraintModel.typePair; + if (argType == DataConstraintModel.typePair && t.getType() != null) { + List compTypeList = new ArrayList<>(); + compTypeList.add(t.getType()); + compTypeList.add(null); + newPairType = pairTypes.get(compTypeList); + if (newPairType == null) { + // Create new tuple type; + newPairType = createNewTupleType(compTypeList, DataConstraintModel.typePair); + } + } + if (argType != newPairType && newPairType != null) { + if (arg instanceof Variable) { + ((Variable) arg).setType(newPairType); + argType = newPairType; + } else if (arg instanceof Term) { + ((Term) arg).setType(newPairType); + argType = newPairType; + } + Map updateExps = getUpdateSet(updateFromPair, pairExps); + updateExps.put(System.identityHashCode(arg), arg); + } + pair.put(System.identityHashCode(pairExps), argType); + } else if (symbol.equals(DataConstraintModel.right)) { + // If the root symbol of the term is right. + List pairExps = new ArrayList<>(); + Expression arg = t.getChildren().get(0); + pairExps.add(arg); + expToPair.put(System.identityHashCode(arg), pairExps); + pairExps.add(null); + pairExps.add(t); + expToPair.put(System.identityHashCode(t), pairExps); + Type argType = null; + if (arg instanceof Variable) { + argType = ((Variable) arg).getType(); + } else if (arg instanceof Term) { + argType = ((Term) arg).getType(); + } + Type newPairType = DataConstraintModel.typePair; + if (argType == DataConstraintModel.typePair && t.getType() != null) { + List compTypeList = new ArrayList<>(); + compTypeList.add(null); + compTypeList.add(t.getType()); + newPairType = pairTypes.get(compTypeList); + if (newPairType == null) { + // Create new tuple type; + newPairType = createNewTupleType(compTypeList, DataConstraintModel.typePair); + } + } + if (argType != newPairType && newPairType != null) { + if (arg instanceof Variable) { + ((Variable) arg).setType(newPairType); + argType = newPairType; + } else if (arg instanceof Term) { + ((Term) arg).setType(newPairType); + argType = newPairType; + } + Map updateExps = getUpdateSet(updateFromPair, pairExps); + updateExps.put(System.identityHashCode(arg), arg); + } + pair.put(System.identityHashCode(pairExps), argType); } else if (symbol.equals(DataConstraintModel.cond)) { // If the root symbol of the term is if function. Expression c1 = t.getChild(1); diff --git a/AlgebraicDataflowArchitectureModel/src/code/ast/ConstructorDeclaration.java b/AlgebraicDataflowArchitectureModel/src/code/ast/ConstructorDeclaration.java deleted file mode 100644 index 70bdc90..0000000 --- a/AlgebraicDataflowArchitectureModel/src/code/ast/ConstructorDeclaration.java +++ /dev/null @@ -1,21 +0,0 @@ -package code.ast; - -import models.algebra.Type; - -public class ConstructorDeclaration extends FieldDeclaration { - private VariableDeclaration constructor; - - public ConstructorDeclaration(Type type, String fieldName,VariableDeclaration constructor) { - super(type, fieldName); - this.setConstructor(constructor); - } - - public VariableDeclaration getConstructor() { - return constructor; - } - - public void setConstructor(VariableDeclaration constructor) { - this.constructor = constructor; - } - -} diff --git a/AlgebraicDataflowArchitectureModel/src/code/ast/TypeDeclaration.java b/AlgebraicDataflowArchitectureModel/src/code/ast/TypeDeclaration.java index 0d97782..1dc5cf3 100644 --- a/AlgebraicDataflowArchitectureModel/src/code/ast/TypeDeclaration.java +++ b/AlgebraicDataflowArchitectureModel/src/code/ast/TypeDeclaration.java @@ -9,7 +9,6 @@ public class TypeDeclaration extends AbstractTypeDeclaration implements IAnnotatable { private List fields = new ArrayList<>(); private List methods = new ArrayList<>(); - private List constructors = new ArrayList<>(); private Map annotations = new HashMap<>(); public TypeDeclaration(String typeName) { @@ -27,13 +26,6 @@ this.methods = methods; } - public TypeDeclaration(String typeName, List fields, List methods,List constructors) { - this.typeName = typeName; - this.fields = fields; - this.methods = methods; - this.constructors = constructors; - } - public void addField(FieldDeclaration field) { fields.add(field); } @@ -42,10 +34,6 @@ methods.add(method); } - public void addConstructors(VariableDeclaration constructor) { - this.constructors.add(constructor); - } - public List getFields() { return fields; } @@ -54,10 +42,6 @@ return methods; } - public List getConstructors() { - return constructors; - } - @Override public Annotation getAnnotation(String name) { return annotations.get(name); diff --git a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java index 14a121d..350a695 100644 --- a/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java +++ b/AlgebraicDataflowArchitectureModel/src/models/dataConstraintModel/DataConstraintModel.java @@ -105,6 +105,8 @@ }); public static final Symbol fst = new Symbol("fst", 1, Symbol.Type.PREFIX, "getKey", Symbol.Type.METHOD); public static final Symbol snd = new Symbol("snd", 1, Symbol.Type.PREFIX, "getValue", Symbol.Type.METHOD); + public static final Symbol left = new Symbol("left", 1, Symbol.Type.PREFIX, "getLeft", Symbol.Type.METHOD); + public static final Symbol right = new Symbol("right", 1, Symbol.Type.PREFIX, "getRight", Symbol.Type.METHOD); static { add.setInverses(new Symbol[] {sub, sub}); @@ -129,7 +131,9 @@ true_.setSignature(new Type[] {typeBoolean}); false_.setSignature(new Type[] {typeBoolean}); pair.setSignature(new Type[] {typePair,null,null}); - pair.setInverses(new Symbol[] {fst, snd}); + pair.setInverses(new Symbol[] {left, right}); + left.setSignature(new Type[] {null, typePair}); + right.setSignature(new Type[] {null, typePair}); tuple.setSignature(new Type[] {typeTuple, null, null}); tuple.setInverses(new Symbol[] {fst, snd}); fst.setSignature(new Type[] {null, typeTuple}); @@ -176,6 +180,8 @@ addSymbol(true_); addSymbol(false_); addSymbol(pair); + addSymbol(left); + addSymbol(right); addSymbol(tuple); addSymbol(fst); addSymbol(snd);