diff --git a/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java b/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java index 1a8cadd..f57b895 100644 --- a/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java +++ b/AlgebraicDataflowArchitectureModel/src/algorithms/TypeInference.java @@ -149,143 +149,160 @@ Collection channels = new HashSet<>(model.getInputChannels()); channels.addAll(model.getChannels()); for (Channel ch : channels) { - for (ChannelMember cm : ch.getChannelMembers()) { - StateTransition st = cm.getStateTransition(); - ResourceHierarchy res = cm.getResource().getResourceHierarchy(); - - // 1.1 Group expressions by resources. - List identicalResources = resources.get(res); - if (identicalResources == null) { - identicalResources = new ArrayList<>(); - resources.put(res, identicalResources); - } - identicalResources.add(st.getCurStateExpression()); - expToResource.put(System.identityHashCode(st.getCurStateExpression()), identicalResources); - if (st.getNextStateExpression() != null) { - identicalResources.add(st.getNextStateExpression()); - expToResource.put(System.identityHashCode(st.getNextStateExpression()), identicalResources); - } - Map updatedExps = getUpdateSet(updateFromResource, identicalResources); - Type resType = res.getResourceStateType(); - Expression exp = st.getCurStateExpression(); - Type expType = getExpTypeIfUpdatable(resType, exp); - if (expType != null) { - res.setResourceStateType(expType); - for (Expression resExp : identicalResources) { - if (resExp != exp) { - if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) { - ((Variable) resExp).setType(expType); - updatedExps.put(System.identityHashCode(resExp), resExp); - } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) { - ((Term) resExp).setType(expType); - updatedExps.put(System.identityHashCode(resExp), resExp); - } + // 1.1 Group expressions by resources. + IGroupExpressionsByResource groupExpressionsByResource = new IGroupExpressionsByResource() { + public void groupForChannel(Channel ch) { + for (ChannelMember cm : ch.getChannelMembers()) { + StateTransition st = cm.getStateTransition(); + ResourceHierarchy res = cm.getResource().getResourceHierarchy(); + List identicalResources = resources.get(res); + if (identicalResources == null) { + identicalResources = new ArrayList<>(); + resources.put(res, identicalResources); } - } - } else if (exp instanceof Variable) { - if (compareTypes(((Variable) exp).getType(), resType)) { - ((Variable) exp).setType(resType); - updatedExps.put(System.identityHashCode(exp), exp); - } - } else if (exp instanceof Term) { - if (compareTypes(((Term) exp).getType(), resType)) { - ((Term) exp).setType(resType); - updatedExps.put(System.identityHashCode(exp), exp); - } - } - resType = res.getResourceStateType(); - exp = st.getNextStateExpression(); - if (exp != null) { - expType = getExpTypeIfUpdatable(resType, exp); - if (expType != null) { - res.setResourceStateType(expType); - for (Expression resExp : identicalResources) { - if (resExp != exp) { - if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) { - ((Variable) resExp).setType(expType); - updatedExps.put(System.identityHashCode(resExp), resExp); - } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) { - ((Term) resExp).setType(expType); - updatedExps.put(System.identityHashCode(resExp), resExp); - } - } + identicalResources.add(st.getCurStateExpression()); + expToResource.put(System.identityHashCode(st.getCurStateExpression()), identicalResources); + if (st.getNextStateExpression() != null) { + identicalResources.add(st.getNextStateExpression()); + expToResource.put(System.identityHashCode(st.getNextStateExpression()), identicalResources); } - } else if (exp instanceof Variable) { - if (compareTypes(((Variable) exp).getType(), resType)) { - ((Variable) exp).setType(resType); - updatedExps.put(System.identityHashCode(exp), exp); - } - } else if (exp instanceof Term) { - if (compareTypes(((Term) exp).getType(), resType)) { - ((Term) exp).setType(resType); - updatedExps.put(System.identityHashCode(exp), exp); - } - } - } - - // 1.2 Group expressions by variable. - Map> locals = new HashMap<>(); - Map localTypes = new HashMap<>(); - List allVariables = new ArrayList<>(); - allVariables.addAll(st.getCurStateExpression().getVariables().values()); - allVariables.addAll(st.getMessageExpression().getVariables().values()); - if (st.getNextStateExpression() != null) { - allVariables.addAll(st.getNextStateExpression().getVariables().values()); - } - for (Selector s: ch.getSelectors()) { // add channel selectors - if (s.getExpression() instanceof Variable) { - allVariables.add((Variable) s.getExpression()); - } - } - ResourcePath resPath = cm.getResource(); - for (Expression param: resPath.getPathParams()) { // add path parameters - if (param instanceof Variable) { - allVariables.add((Variable) param); - } else if (param instanceof Term) { - allVariables.addAll(((Term) param).getVariables().values()); - } - } - for (Variable var : allVariables) { - List sameVariable = locals.get(var.getName()); - if (sameVariable == null) { - sameVariable = new ArrayList<>(); - sameVariable.add(var); - expToVariable.put(System.identityHashCode(var), sameVariable); - locals.put(var.getName(), sameVariable); - localTypes.put(var.getName(), var.getType()); - } else { - sameVariable.add(var); - expToVariable.put(System.identityHashCode(var), sameVariable); - Type varType = localTypes.get(var.getName()); - Map updatedVars = getUpdateSet(updateFromVariable, sameVariable); - if (compareTypes(varType, var.getType())) { - localTypes.put(var.getName(), var.getType()); - for (Expression v : sameVariable) { - if (v != var) { - if (compareTypes(((Variable) v).getType(), var.getType())) { - ((Variable) v).setType(var.getType()); - updatedVars.put(System.identityHashCode(v), v); + Map updatedExps = getUpdateSet(updateFromResource, identicalResources); + Type resType = res.getResourceStateType(); + Expression exp = st.getCurStateExpression(); + Type expType = getExpTypeIfUpdatable(resType, exp); + if (expType != null) { + res.setResourceStateType(expType); + for (Expression resExp : identicalResources) { + if (resExp != exp) { + if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) { + ((Variable) resExp).setType(expType); + updatedExps.put(System.identityHashCode(resExp), resExp); + } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) { + ((Term) resExp).setType(expType); + updatedExps.put(System.identityHashCode(resExp), resExp); } } } - } else if (compareTypes(var.getType(), varType)) { - var.setType(varType); - updatedVars.put(System.identityHashCode(var), var); + } else if (exp instanceof Variable) { + if (compareTypes(((Variable) exp).getType(), resType)) { + ((Variable) exp).setType(resType); + updatedExps.put(System.identityHashCode(exp), exp); + } + } else if (exp instanceof Term) { + if (compareTypes(((Term) exp).getType(), resType)) { + ((Term) exp).setType(resType); + updatedExps.put(System.identityHashCode(exp), exp); + } + } + resType = res.getResourceStateType(); + exp = st.getNextStateExpression(); + if (exp != null) { + expType = getExpTypeIfUpdatable(resType, exp); + if (expType != null) { + res.setResourceStateType(expType); + for (Expression resExp : identicalResources) { + if (resExp != exp) { + if (resExp instanceof Variable && compareTypes(((Variable) resExp).getType(), expType)) { + ((Variable) resExp).setType(expType); + updatedExps.put(System.identityHashCode(resExp), resExp); + } else if (resExp instanceof Term && compareTypes(((Term) resExp).getType(), expType)) { + ((Term) resExp).setType(expType); + updatedExps.put(System.identityHashCode(resExp), resExp); + } + } + } + } else if (exp instanceof Variable) { + if (compareTypes(((Variable) exp).getType(), resType)) { + ((Variable) exp).setType(resType); + updatedExps.put(System.identityHashCode(exp), exp); + } + } else if (exp instanceof Term) { + if (compareTypes(((Term) exp).getType(), resType)) { + ((Term) exp).setType(resType); + updatedExps.put(System.identityHashCode(exp), exp); + } + } } } + for (Channel childCh: ch.getChildren()) { + groupForChannel(childCh); + } } - for (String varName : locals.keySet()) { - variables.put(System.identityHashCode(locals.get(varName)), localTypes.get(varName)); - } + }; + groupExpressionsByResource.groupForChannel(ch); - // 1.3 Group expressions by message. - Expression message = st.getMessageExpression(); - if (message instanceof Variable) { - IRecurseForMessageVariable resurceForVar = new IRecurseForMessageVariable() { - public void recurse(Channel rootCh, Channel ch, Expression message, - Map, Type>>> messages, - Map> expToMessage, - Map> updateFromMessage) { + // 1.2 Group expressions by variable. + IGroupExpressionsByVariable groupExpressionsByVariable = new IGroupExpressionsByVariable() { + public void groupForChannel(Channel ch) { + for (ChannelMember cm : ch.getChannelMembers()) { + StateTransition st = cm.getStateTransition(); + Map> locals = new HashMap<>(); + Map localTypes = new HashMap<>(); + List allVariables = new ArrayList<>(); + allVariables.addAll(st.getCurStateExpression().getVariables().values()); + allVariables.addAll(st.getMessageExpression().getVariables().values()); + if (st.getNextStateExpression() != null) { + allVariables.addAll(st.getNextStateExpression().getVariables().values()); + } + for (Selector s: ch.getAllSelectors()) { // add channel selectors + if (s.getExpression() instanceof Variable) { + allVariables.add((Variable) s.getExpression()); + } + } + ResourcePath resPath = cm.getResource(); + for (Expression param: resPath.getPathParams()) { // add path parameters + if (param instanceof Variable) { + allVariables.add((Variable) param); + } else if (param instanceof Term) { + allVariables.addAll(((Term) param).getVariables().values()); + } + } + for (Variable var : allVariables) { + List sameVariable = locals.get(var.getName()); + if (sameVariable == null) { + sameVariable = new ArrayList<>(); + sameVariable.add(var); + expToVariable.put(System.identityHashCode(var), sameVariable); + locals.put(var.getName(), sameVariable); + localTypes.put(var.getName(), var.getType()); + } else { + sameVariable.add(var); + expToVariable.put(System.identityHashCode(var), sameVariable); + Type varType = localTypes.get(var.getName()); + Map updatedVars = getUpdateSet(updateFromVariable, sameVariable); + if (compareTypes(varType, var.getType())) { + localTypes.put(var.getName(), var.getType()); + for (Expression v : sameVariable) { + if (v != var) { + if (compareTypes(((Variable) v).getType(), var.getType())) { + ((Variable) v).setType(var.getType()); + updatedVars.put(System.identityHashCode(v), v); + } + } + } + } else if (compareTypes(var.getType(), varType)) { + var.setType(varType); + updatedVars.put(System.identityHashCode(var), var); + } + } + } + for (String varName : locals.keySet()) { + variables.put(System.identityHashCode(locals.get(varName)), localTypes.get(varName)); + } + } + for (Channel childCh: ch.getChildren()) { + groupForChannel(childCh); + } + } + }; + groupExpressionsByVariable.groupForChannel(ch); + + // 1.3 Group expressions by message. + IGroupExpressionsByMessage groupExpressionsByMessage = new IGroupExpressionsByMessage() { + public void groupForChannel(Channel rootCh, Channel ch) { + for (ChannelMember cm : ch.getChannelMembers()) { + Expression message = cm.getStateTransition().getMessageExpression(); + if (message instanceof Variable) { Type msgType = ((Variable) message).getType(); Map, Type>> msgTypeMap = messages.get(rootCh); if (msgTypeMap == null) { @@ -318,21 +335,7 @@ updateExps.put(System.identityHashCode(message), message); } } - for (Channel childCh: ch.getChildren()) { - for (ChannelMember cm: childCh.getChannelMembers()) { - Expression childMessage = cm.getStateTransition().getMessageExpression(); - recurse(rootCh, childCh, childMessage, messages, expToMessage, updateFromMessage); - } - } - } - }; - resurceForVar.recurse(ch, ch, message, messages, expToMessage, updateFromMessage); - } else if (message instanceof Term) { - IRecurseForMessageTerm resurceForTerm = new IRecurseForMessageTerm() { - public void recurse(Channel rootCh, Channel ch, Expression message, - Map, Type>>> messages, - Map> expToMessage, - Map> updateFromMessage) { + } else if (message instanceof Term) { Map, Type>> msgTypeMap = messages.get(rootCh); if (msgTypeMap == null) { msgTypeMap = new HashMap<>(); @@ -380,853 +383,871 @@ } } } - for (Channel childCh: ch.getChildren()) { - for (ChannelMember cm: childCh.getChannelMembers()) { - Expression childMessage = cm.getStateTransition().getMessageExpression(); - recurse(rootCh, childCh, childMessage, messages, expToMessage, updateFromMessage); - } - } } - }; - resurceForTerm.recurse(ch, ch, message, messages, expToMessage, updateFromMessage); + } + for (Channel childCh: ch.getChildren()) { + groupForChannel(rootCh, childCh); + } } - // 1.4 Extract constraints on expressions in each term. - List terms = new ArrayList<>(); - if (st.getCurStateExpression() instanceof Term) { - Map subTerms = ((Term) st.getCurStateExpression()).getSubTerms(Term.class); - terms.addAll(subTerms.values()); - } - if (st.getMessageExpression() instanceof Term) { - Map subTerms = ((Term) st.getMessageExpression()).getSubTerms(Term.class); - terms.addAll(subTerms.values()); - } - if (st.getNextStateExpression() != null && st.getNextStateExpression() instanceof Term) { - Map subTerms = ((Term) st.getNextStateExpression()).getSubTerms(Term.class); - terms.addAll(subTerms.values()); - } - for (Term t : terms) { - Symbol symbol = t.getSymbol(); - if (symbol.equals(DataConstraintModel.cons) || symbol.equals(DataConstraintModel.set) || symbol.equals(DataConstraintModel.append)) { - // If the root symbol of the term is cons or set. - List consExps = new ArrayList<>(); - consExps.add(t); // list term - updateExpressionBelonging(expToConsOrSet, t, consExps); - if (symbol.equals(DataConstraintModel.cons)) { - // If the root symbol of the term is cons. - for (Expression e : t.getChildren()) { - consExps.add(e); - updateExpressionBelonging(expToConsOrSet, e, consExps); - } - } else if (symbol.equals(DataConstraintModel.append)) { - // If the root symbol of the term is append. - Expression e = t.getChildren().get(1); - consExps.add(e); // list element - updateExpressionBelonging(expToConsOrSet, e, consExps); - e = t.getChildren().get(0); - consExps.add(e); // list argument - updateExpressionBelonging(expToConsOrSet, e, consExps); - } else { - // If the root symbol of the term is set. - Expression e = t.getChildren().get(2); - consExps.add(e); // list element - updateExpressionBelonging(expToConsOrSet, e, consExps); - e = t.getChildren().get(0); - consExps.add(e); // list argument - updateExpressionBelonging(expToConsOrSet, e, consExps); + }; + groupExpressionsByMessage.groupForChannel(ch, ch); + + // 1.4 Extract constraints on expressions in each term. + IExtractConstraintsOnExpressionsInTerm extractConstraintsOnExpressionsInTerm = new IExtractConstraintsOnExpressionsInTerm() { + public void extractForChannel(Channel ch) { + for (ChannelMember cm : ch.getChannelMembers()) { + StateTransition st = cm.getStateTransition(); + List terms = new ArrayList<>(); + if (st.getCurStateExpression() instanceof Term) { + Map subTerms = ((Term) st.getCurStateExpression()).getSubTerms(Term.class); + terms.addAll(subTerms.values()); } - Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2)); - if (newType != null) { - // If the type of the 2nd argument of cons (1st argument of set/append) is more concrete than the type of the term. - t.setType(newType); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(t), t); - } else { - Type arg2Type = null; - if (consExps.get(2) != null && consExps.get(2) instanceof Variable) { - arg2Type = ((Variable) consExps.get(2)).getType(); - if (compareTypes(arg2Type, t.getType())) { - // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set/append). - ((Variable) consExps.get(2)).setType(t.getType()); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); - } - } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) { - arg2Type = ((Term) consExps.get(2)).getType(); - if (compareTypes(arg2Type, t.getType())) { - // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set/append). - ((Term) consExps.get(2)).setType(t.getType()); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); - } - } + if (st.getMessageExpression() instanceof Term) { + Map subTerms = ((Term) st.getMessageExpression()).getSubTerms(Term.class); + terms.addAll(subTerms.values()); } - Type newCompType = getExpTypeIfUpdatable(listComponentTypes.get(t.getType()), consExps.get(1)); - if (newCompType != null) { - // If the type of the 1st argument of cons (3rd argument of set) is more concrete than the type of list component. - Type newListType = listTypes.get(newCompType); - if (newListType == null) { - // Create new list type. - newListType = createNewListType(newCompType, DataConstraintModel.typeList); - } - t.setType(newListType); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(t), t); - if (consExps.get(2) != null && consExps.get(2) instanceof Variable) { - ((Variable) consExps.get(2)).setType(newListType); - updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); - } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) { - ((Term) consExps.get(2)).setType(newListType); - updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); - } + if (st.getNextStateExpression() != null && st.getNextStateExpression() instanceof Term) { + Map subTerms = ((Term) st.getNextStateExpression()).getSubTerms(Term.class); + terms.addAll(subTerms.values()); } - consOrSet.put(System.identityHashCode(consExps), t.getType()); - } else if (symbol.equals(DataConstraintModel.head) || symbol.equals(DataConstraintModel.get)) { - // If the root symbol of the term is head or get. - List consExps = new ArrayList<>(); - Expression e = t.getChildren().get(0); - consExps.add(e); // list argument - updateExpressionBelonging(expToConsOrSet, e, consExps); - consExps.add(t); // list's component - updateExpressionBelonging(expToConsOrSet, t, consExps); - consExps.add(null); - Type listType = listTypes.get(t.getType()); - if (listType == null && t.getType() != null) { - // Create a new list type. - listType = createNewListType(t.getType(), DataConstraintModel.typeList); - } - Type newListType = getExpTypeIfUpdatable(listType, consExps.get(0)); - if (newListType != null) { - // If the type of the component of the 1st argument is more concrete than the type of the term. - Type newCompType = listComponentTypes.get(newListType); - if (newCompType != null) { - t.setType(newCompType); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(t), t); - } - consOrSet.put(System.identityHashCode(consExps), newListType); - } else { - // If the type of the term is more concrete than the type of the component of the 1st argument. - if (consExps.get(0) != null && consExps.get(0) instanceof Variable) { - ((Variable) consExps.get(0)).setType(listType); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0)); - } else if (consExps.get(0) != null && consExps.get(0) instanceof Term) { - ((Term) consExps.get(0)).setType(listType); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0)); - } - consOrSet.put(System.identityHashCode(consExps), listType); - } - } else if (symbol.equals(DataConstraintModel.tail)) { - // If the root symbol of the term is tail. - List consExps = new ArrayList<>(); - consExps.add(t); // list term - updateExpressionBelonging(expToConsOrSet, t, consExps); - consExps.add(null); // list's component - Expression e = t.getChildren().get(0); - consExps.add(e); // list argument - updateExpressionBelonging(expToConsOrSet, e, consExps); - Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2)); - if (newType != null) { - // If the type of the argument is more concrete than the type of the term. - t.setType(newType); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(t), t); - } else { - Type argType = null; - if (consExps.get(2) != null && consExps.get(2) instanceof Variable) { - argType = ((Variable) consExps.get(2)).getType(); - if (compareTypes(argType, t.getType())) { - // If the type of the term is more concrete than the type of the argument. - ((Variable) consExps.get(2)).setType(t.getType()); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); - } - } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) { - argType = ((Term) consExps.get(2)).getType(); - if (compareTypes(argType, t.getType())) { - // If the type of the term is more concrete than the type of the argument. - ((Term) consExps.get(2)).setType(t.getType()); - Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); - updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); - } - } - } - consOrSet.put(System.identityHashCode(consExps), t.getType()); - } else if (symbol.equals(DataConstraintModel.tuple)) { - // If the root symbol of the term is tuple. - List tupleExps = new ArrayList<>(); - List newArgTypesList = new ArrayList<>(); - tupleExps.add(t); // tuple term - updateExpressionBelonging(expToTuple, t, tupleExps); - for (Expression e : t.getChildren()) { - tupleExps.add(e); // tuple's component - updateExpressionBelonging(expToTuple, e, tupleExps); - if (e instanceof Variable) { - newArgTypesList.add(((Variable) e).getType()); - } else if (e instanceof Term) { - newArgTypesList.add(((Term) e).getType()); - } else { - newArgTypesList.add(null); - } - } - if (t.getType() == DataConstraintModel.typeTuple) { - Type newTupleType = tupleTypes.get(newArgTypesList); - if (newTupleType == null) { - // Create new tuple type; - newTupleType = createNewTupleType(newArgTypesList, DataConstraintModel.typeTuple); - } - // Update the type of the tuple term and record the updated expression. - t.setType(newTupleType); - Map updateExps = getUpdateSet(updateFromTuple, tupleExps); - updateExps.put(System.identityHashCode(t), t); - } - tuple.put(System.identityHashCode(tupleExps), t.getType()); - } else if (symbol.equals(DataConstraintModel.pair)) { - // If the root symbol of the term is pair. - List pairExps = new ArrayList<>(); - pairExps.add(t); // pair - updateExpressionBelonging(expToPair, t, pairExps); - if (t.getType() == DataConstraintModel.typePair) { - for (Expression e : t.getChildren()) { - pairExps.add(e); // left/right - updateExpressionBelonging(expToPair, e, pairExps); - Type newArgType = null; - if (e instanceof Variable) { - newArgType = (((Variable) e).getType()); - - } else if (e instanceof Term) { - newArgType = (((Term) e).getType()); - } - - if (newArgType != null) { - Type newPairType = pairTypes.get(newArgType); - if (newPairType != null) { - t.setType(newPairType); - Map updateExps = getUpdateSet(updateFromPair, pairExps); - updateExps.put(System.identityHashCode(t), t); + for (Term t : terms) { + Symbol symbol = t.getSymbol(); + if (symbol.equals(DataConstraintModel.cons) || symbol.equals(DataConstraintModel.set) || symbol.equals(DataConstraintModel.append)) { + // If the root symbol of the term is cons or set. + List consExps = new ArrayList<>(); + consExps.add(t); // list term + updateExpressionBelonging(expToConsOrSet, t, consExps); + if (symbol.equals(DataConstraintModel.cons)) { + // If the root symbol of the term is cons. + for (Expression e : t.getChildren()) { + consExps.add(e); + updateExpressionBelonging(expToConsOrSet, e, consExps); } - } - } - pair.put(System.identityHashCode(pairExps), t.getType()); - - } - } else if (symbol.equals(DataConstraintModel.fst)) { - // If the root symbol of the term is fst. - List tupleExps = new ArrayList<>(); - Expression arg = t.getChildren().get(0); - tupleExps.add(arg); // tuple argument - updateExpressionBelonging(expToTuple, arg, tupleExps); - tupleExps.add(t); // first component - updateExpressionBelonging(expToTuple, t, tupleExps); - tupleExps.add(null); // second component - Type argType = null; - if (arg instanceof Variable) { - argType = ((Variable) arg).getType(); - } else if (arg instanceof Term) { - argType = ((Term) arg).getType(); - } - Type newTupleType = DataConstraintModel.typeTuple; - if (argType == DataConstraintModel.typeTuple && t.getType() != null) { - List newCompTypeList = new ArrayList<>(); - newCompTypeList.add(t.getType()); - newCompTypeList.add(null); - newTupleType = tupleTypes.get(newCompTypeList); - if (newTupleType == null) { - // Create new tuple type; - newTupleType = createNewTupleType(newCompTypeList, DataConstraintModel.typeTuple); - } - } - if (argType != newTupleType && newTupleType != null) { - // Update the type of the tuple argument and record the updated expression. - if (arg instanceof Variable) { - ((Variable) arg).setType(newTupleType); - argType = newTupleType; - } else if (arg instanceof Term) { - ((Term) arg).setType(newTupleType); - argType = newTupleType; - } - Map updateExps = getUpdateSet(updateFromTuple, tupleExps); - updateExps.put(System.identityHashCode(arg), arg); - } - tuple.put(System.identityHashCode(tupleExps), argType); - } else if (symbol.equals(DataConstraintModel.snd)) { - // If the root symbol of the term is snd. - List tupleExps = new ArrayList<>(); - Expression arg = t.getChildren().get(0); - tupleExps.add(arg); // tuple argument - updateExpressionBelonging(expToTuple, arg, tupleExps); - tupleExps.add(null); // first component - tupleExps.add(t); // second component - updateExpressionBelonging(expToTuple, t, tupleExps); - Type argType = null; - if (arg instanceof Variable) { - argType = ((Variable) arg).getType(); - } else if (arg instanceof Term) { - argType = ((Term) arg).getType(); - } - Type newTupleType = DataConstraintModel.typeTuple; - if (argType == DataConstraintModel.typeTuple && t.getType() != null) { - List newCompTypeList = new ArrayList<>(); - newCompTypeList.add(null); - if (DataConstraintModel.typeTuple.isAncestorOf(t.getType())) { - List sndTypes = tupleComponentTypes.get(t.getType()); - if (sndTypes != null) { - for (Type t2: sndTypes) { - newCompTypeList.add(t2); - } + } else if (symbol.equals(DataConstraintModel.append)) { + // If the root symbol of the term is append. + Expression e = t.getChildren().get(1); + consExps.add(e); // list element + updateExpressionBelonging(expToConsOrSet, e, consExps); + e = t.getChildren().get(0); + consExps.add(e); // list argument + updateExpressionBelonging(expToConsOrSet, e, consExps); } else { - newCompTypeList.add(t.getType()); + // If the root symbol of the term is set. + Expression e = t.getChildren().get(2); + consExps.add(e); // list element + updateExpressionBelonging(expToConsOrSet, e, consExps); + e = t.getChildren().get(0); + consExps.add(e); // list argument + updateExpressionBelonging(expToConsOrSet, e, consExps); } - } else { - newCompTypeList.add(t.getType()); - } - newTupleType = tupleTypes.get(newCompTypeList); - if (newTupleType == null) { - // Create new tuple type; - newTupleType = createNewTupleType(newCompTypeList, DataConstraintModel.typeTuple); - } - } - if (argType != newTupleType && newTupleType != null) { - // Update the type of the tuple argument and record the updated expression. - if (arg instanceof Variable) { - ((Variable) arg).setType(newTupleType); - argType = newTupleType; - } else if (arg instanceof Term) { - ((Term) arg).setType(newTupleType); - argType = newTupleType; - } - Map updateExps = getUpdateSet(updateFromTuple, tupleExps); - 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); // pair - updateExpressionBelonging(expToPair, arg, pairExps); - pairExps.add(t); // left - updateExpressionBelonging(expToPair, t, pairExps); - pairExps.add(null); // right - 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 newCompTypeList = new ArrayList<>(); - newCompTypeList.add(t.getType()); - newCompTypeList.add(null); - newPairType = pairTypes.get(newCompTypeList); - if (newPairType == null) { - // Create new tuple type; - newPairType = createNewTupleType(newCompTypeList, 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); // pair - updateExpressionBelonging(expToPair, arg, pairExps); - pairExps.add(null); // left - pairExps.add(t); // right - updateExpressionBelonging(expToPair, 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 newCompTypeList = new ArrayList<>(); - newCompTypeList.add(null); - newCompTypeList.add(t.getType()); - newPairType = pairTypes.get(newCompTypeList); - if (newPairType == null) { - // Create new tuple type; - newPairType = createNewTupleType(newCompTypeList, 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.lookup)) { - // If the root symbol of the term is lookup. - List mapExps = new ArrayList<>(); - Expression arg1 = t.getChildren().get(0); // map - mapExps.add(arg1); - updateExpressionBelonging(expToMap, arg1, mapExps); - Expression arg2 = t.getChildren().get(1); // key - mapExps.add(arg2); - updateExpressionBelonging(expToMap, arg2, mapExps); - mapExps.add(t); // value - updateExpressionBelonging(expToMap, t, mapExps); - Type arg1Type = null; - if (arg1 instanceof Variable) { - arg1Type = ((Variable) arg1).getType(); - } else if (arg1 instanceof Term) { - arg1Type = ((Term) arg1).getType(); - } - List newCompTypeList = new ArrayList<>(); - if (arg2 instanceof Variable) { - newCompTypeList.add(((Variable) arg2).getType()); - } else if (arg2 instanceof Term) { - newCompTypeList.add(((Term) arg2).getType()); - } else { - newCompTypeList.add(null); - } - newCompTypeList.add(t.getType()); - if (arg1Type == DataConstraintModel.typeMap || arg1Type == null) { - Type newMapType = mapTypes.get(newCompTypeList); - if (newMapType == null) { - // Create new tuple type; - newMapType = createNewMapType(newCompTypeList, DataConstraintModel.typeMap); - } - // Update the type of the map argument and record the updated expression. - if (arg1 instanceof Variable) { - ((Variable) arg1).setType(newMapType); - arg1Type = newMapType; - } else if (arg1 instanceof Term) { - ((Term) arg1).setType(newMapType); - arg1Type = newMapType; - } - Map updateExps = getUpdateSet(updateFromMap, mapExps); - updateExps.put(System.identityHashCode(arg1), arg1); - } - map.put(System.identityHashCode(mapExps), arg1Type); - } else if (symbol.equals(DataConstraintModel.insert)) { - // If the root symbol of the term is insert. - List mapExps = new ArrayList<>(); - mapExps.add(t); // map - updateExpressionBelonging(expToMap, t, mapExps); - Expression arg1 = t.getChildren().get(1); // key - mapExps.add(arg1); - updateExpressionBelonging(expToMap, arg1, mapExps); - Expression arg2 = t.getChildren().get(2); // value - mapExps.add(arg2); - updateExpressionBelonging(expToMap, arg2, mapExps); - Expression arg0 = t.getChildren().get(0); // map - mapExps.add(arg0); - updateExpressionBelonging(expToMap, arg0, mapExps); - Type termType = t.getType(); - List newCompTypeList = new ArrayList<>(); - if (arg1 instanceof Variable) { - newCompTypeList.add(((Variable) arg1).getType()); - } else if (arg1 instanceof Term) { - newCompTypeList.add(((Term) arg1).getType()); - } else { - newCompTypeList.add(null); - } - if (arg2 instanceof Variable) { - newCompTypeList.add(((Variable) arg2).getType()); - } else if (arg2 instanceof Term) { - newCompTypeList.add(((Term) arg2).getType()); - } else { - newCompTypeList.add(null); - } - Type newTermType = getExpTypeIfUpdatable(termType, mapExps.get(3)); - if (newTermType != null) { - // If the type of the 1st argument of insert is more concrete than the type of the term. - t.setType(newTermType); - termType = newTermType; - Map updateExps = getUpdateSet(updateFromMap, mapExps); - updateExps.put(System.identityHashCode(t), t); - } else { - Type arg3Type = null; - if (mapExps.get(3) != null && mapExps.get(3) instanceof Variable) { - arg3Type = ((Variable) mapExps.get(3)).getType(); - if (compareTypes(arg3Type, t.getType())) { - // If the type of the term is more concrete than the type of the 1st argument of insert. - ((Variable) mapExps.get(3)).setType(t.getType()); - Map updateExps = getUpdateSet(updateFromMap, mapExps); - updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); - } - } else if (mapExps.get(3) != null && mapExps.get(3) instanceof Term) { - arg3Type = ((Term) mapExps.get(3)).getType(); - if (compareTypes(arg3Type, t.getType())) { - // If the type of the term is more concrete than the type of the 1st argument of insert. - ((Term) mapExps.get(3)).setType(t.getType()); - Map updateExps = getUpdateSet(updateFromMap, mapExps); - updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); - } - } - } - if (termType == DataConstraintModel.typeMap || termType == null) { - Type newMapType = mapTypes.get(newCompTypeList); - if (newMapType == null) { - // Create new tuple type; - newMapType = createNewMapType(newCompTypeList, DataConstraintModel.typeMap); - } - // Update the type of the map term and record the updated expression. - t.setType(newMapType); - Map updateExps = getUpdateSet(updateFromMap, mapExps); - updateExps.put(System.identityHashCode(t), t); - if (mapExps.get(3) != null && mapExps.get(3) instanceof Variable) { - ((Variable) mapExps.get(3)).setType(newMapType); - updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); - } else if (mapExps.get(3) != null && mapExps.get(3) instanceof Term) { - ((Term) mapExps.get(3)).setType(newMapType); - updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); - } - termType = newMapType; - } - map.put(System.identityHashCode(mapExps), termType); - } else if (symbol.equals(DataConstraintModel.addMember)) { - // If the root symbol of the term is addMember (addMember(json, key, value)). - List dotExps = new ArrayList<>(); - Expression jsonArg = t.getChildren().get(0); - Expression keyArg = t.getChildren().get(1); - Expression valueArg = t.getChildren().get(2); - dotExps.add(t); // json - updateExpressionBelonging(expToJson, t, dotExps); - dotExps.add(keyArg); // key - updateExpressionBelonging(expToJson, keyArg, dotExps); - dotExps.add(valueArg); // value - updateExpressionBelonging(expToJson, valueArg, dotExps); - dotExps.add(jsonArg); // json - updateExpressionBelonging(expToJson, jsonArg, dotExps); - Type jsonType = t.getType(); - Type valueType = null; - if (valueArg instanceof Variable) { - valueType = ((Variable) valueArg).getType(); - } else if (valueArg instanceof Term) { - valueType = ((Term) valueArg).getType(); - } - String keyName = null; - if (keyArg instanceof Constant) { - keyName = ((Constant) keyArg).getSymbol().getName(); - } - Type jsonArgType = null; - if (jsonArg instanceof Variable) { - jsonArgType = ((Variable) jsonArg).getType(); - } else if (jsonArg instanceof Term) { - jsonArgType = ((Term) jsonArg).getType(); - } - Type newJsonType = DataConstraintModel.typeJson; - if (jsonType == DataConstraintModel.typeJson && jsonArgType != null && keyName != null) { - Map newMemberTypes = new HashMap<>(((JsonType) jsonArgType).getMemberTypes()); - newMemberTypes.put(keyName, valueType); - newJsonType = jsonTypes.get(newMemberTypes); - if (newJsonType == null) { - // Create new json type; - newJsonType = createNewJsonType(newMemberTypes, DataConstraintModel.typeJson); - } - } - if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) { - // Update the type of the json term and record the updated expression. - t.setType(newJsonType); - jsonType = newJsonType; - Map updateExps = getUpdateSet(updateFromJson, dotExps); - updateExps.put(System.identityHashCode(t), t); - } - json.put(System.identityHashCode(dotExps), jsonType); - } else if (symbol.equals(DataConstraintModel.dot)) { - // If the root symbol of the term is dot (json.property). - List dotExps = new ArrayList<>(); - Expression jsonArg = t.getChildren().get(0); - Expression keyArg = t.getChildren().get(1); - dotExps.add(jsonArg); // json - updateExpressionBelonging(expToJson, jsonArg, dotExps); - dotExps.add(keyArg); // key - updateExpressionBelonging(expToJson, keyArg, dotExps); - dotExps.add(t); // value - updateExpressionBelonging(expToJson, t, dotExps); - dotExps.add(null); // json - Type jsonType = null; - if (jsonArg instanceof Variable) { - jsonType = ((Variable) jsonArg).getType(); - } else if (jsonArg instanceof Term) { - jsonType = ((Term) jsonArg).getType(); - } - String keyName = null; - if (keyArg instanceof Constant) { - keyName = ((Constant) keyArg).getSymbol().getName(); - } - Type newJsonType = DataConstraintModel.typeJson; - if (jsonType == DataConstraintModel.typeJson && t.getType() != null && keyName != null) { - Map newMemberTypes = new HashMap<>(); - newMemberTypes.put(keyName, t.getType()); - newJsonType = jsonTypes.get(newMemberTypes); - if (newJsonType == null) { - // Create new json type; - newJsonType = createNewJsonType(newMemberTypes, DataConstraintModel.typeJson); - } - } - if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) { - // Update the type of the json argument and record the updated expression. - if (jsonArg instanceof Variable) { - ((Variable) jsonArg).setType(newJsonType); - jsonType = newJsonType; - } else if (jsonArg instanceof Term) { - ((Term) jsonArg).setType(newJsonType); - jsonType = newJsonType; - } - Map updateExps = getUpdateSet(updateFromJson, dotExps); - updateExps.put(System.identityHashCode(jsonArg), jsonArg); - } - json.put(System.identityHashCode(dotExps), jsonType); - } else if (symbol.equals(DataConstraintModel.dotParam)) { - // If the root symbol of the term is dot (json.{param}). - List dotExps = new ArrayList<>(); - Expression jsonArg = t.getChildren().get(0); - Expression keyArg = t.getChildren().get(1); - dotExps.add(jsonArg); // json (list/map) - updateExpressionBelonging(expToJson, jsonArg, dotExps); - dotExps.add(null); // key - dotExps.add(t); // value - updateExpressionBelonging(expToJson, t, dotExps); - dotExps.add(null); // json - Type jsonType = null; - if (jsonArg instanceof Variable) { - jsonType = ((Variable) jsonArg).getType(); - } else if (jsonArg instanceof Term) { - jsonType = ((Term) jsonArg).getType(); - } - Type keyType = null; - if (keyArg instanceof Variable) { - keyType = ((Variable) keyArg).getType(); - } else if (keyArg instanceof Term) { - keyType = ((Term) keyArg).getType(); - } - Type newJsonType = null; - if (keyType == DataConstraintModel.typeInt) { - newJsonType = DataConstraintModel.typeList; - } else if (keyType == DataConstraintModel.typeString) { - newJsonType = DataConstraintModel.typeMap; - } - if (t.getType() != null) { - if ((jsonType == DataConstraintModel.typeList)) { - newJsonType = listTypes.get(t.getType()); - if (newJsonType == null) { - // Create new list type; - newJsonType = createNewListType(t.getType(), DataConstraintModel.typeList); - } - } else if (jsonType == DataConstraintModel.typeMap) { - List keyValueTypes = Arrays.asList(new Type[] {DataConstraintModel.typeString, t.getType()}); - newJsonType = mapTypes.get(keyValueTypes); - if (newJsonType == null) { - // Create new map type; - newJsonType = createNewMapType(keyValueTypes, DataConstraintModel.typeMap); - } - } - } - if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) { - // Update the type of the json argument and record the updated expression. - if (jsonArg instanceof Variable) { - ((Variable) jsonArg).setType(newJsonType); - jsonType = newJsonType; - } else if (jsonArg instanceof Term) { - ((Term) jsonArg).setType(newJsonType); - jsonType = newJsonType; - } - Map updateExps = getUpdateSet(updateFromJson, dotExps); - updateExps.put(System.identityHashCode(jsonArg), jsonArg); - } - json.put(System.identityHashCode(dotExps), jsonType); - } else if (symbol.equals(DataConstraintModel.cond)) { - // If the root symbol of the term is if function. - Expression c1 = t.getChild(1); - Expression c2 = t.getChild(2); - List condTerms = new ArrayList<>(); - condTerms.add(t); - condTerms.add(c1); - condTerms.add(c2); - expToVariable.put(System.identityHashCode(t), condTerms); - expToVariable.put(System.identityHashCode(c1), condTerms); - expToVariable.put(System.identityHashCode(c2), condTerms); - Type condType = t.getType(); - Map updatedVars = getUpdateSet(updateFromVariable, condTerms); - Type child1Type = getExpTypeIfUpdatable(condType, c1); - if (child1Type != null) { - condType = child1Type; - t.setType(child1Type); - updatedVars.put(System.identityHashCode(t), t); - } else { - if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), condType)) { - ((Variable) c1).setType(condType); - updatedVars.put(System.identityHashCode(c1), c1); - } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), condType)) { - ((Term) c1).setType(condType); - updatedVars.put(System.identityHashCode(c1), c1); - } - } - Type child2Type = getExpTypeIfUpdatable(condType, c2); - if (child2Type != null) { - condType = child2Type; - t.setType(child2Type); - updatedVars.put(System.identityHashCode(t), t); - if (c1 instanceof Variable) { - ((Variable) c1).setType(child2Type); - updatedVars.put(System.identityHashCode(c1), c1); - } else if (c1 instanceof Term) { - ((Term) c1).setType(child2Type); - updatedVars.put(System.identityHashCode(c1), c1); - } - } else { - if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), condType)) { - ((Variable) c2).setType(condType); - updatedVars.put(System.identityHashCode(c2), c2); - } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), condType)) { - ((Term) c2).setType(condType); - updatedVars.put(System.identityHashCode(c2), c2); - } - } - variables.put(System.identityHashCode(condTerms), condType); - } else if (symbol.equals(DataConstraintModel.add) || symbol.equals(DataConstraintModel.sub) - || symbol.equals(DataConstraintModel.mul) || symbol.equals(DataConstraintModel.div)) { - // If the root symbol of the term is arithmetic operators. - Expression c1 = t.getChild(0); - Expression c2 = t.getChild(1); - List operands = new ArrayList<>(); - operands.add(t); - operands.add(c1); - operands.add(c2); - expToVariable.put(System.identityHashCode(t), operands); - expToVariable.put(System.identityHashCode(c1), operands); - expToVariable.put(System.identityHashCode(c2), operands); - Type opType = t.getType(); - Map updatedVars = getUpdateSet(updateFromVariable, operands); - Type child1Type = getExpTypeIfUpdatable(opType, c1); - if (child1Type != null) { - opType = child1Type; - t.setType(child1Type); - updatedVars.put(System.identityHashCode(t), t); - } else { - if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), opType)) { - ((Variable) c1).setType(opType); - updatedVars.put(System.identityHashCode(c1), c1); - } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), opType)) { - ((Term) c1).setType(opType); - updatedVars.put(System.identityHashCode(c1), c1); - } - } - Type child2Type = getExpTypeIfUpdatable(opType, c2); - if (child2Type != null) { - opType = child2Type; - t.setType(child2Type); - updatedVars.put(System.identityHashCode(t), t); - if (c1 instanceof Variable) { - ((Variable) c1).setType(child2Type); - updatedVars.put(System.identityHashCode(c1), c1); - } else if (c1 instanceof Term) { - ((Term) c1).setType(child2Type); - updatedVars.put(System.identityHashCode(c1), c1); - } - } else { - if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), opType)) { - ((Variable) c2).setType(opType); - updatedVars.put(System.identityHashCode(c2), c2); - } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), opType)) { - ((Term) c2).setType(opType); - updatedVars.put(System.identityHashCode(c2), c2); - } - } - variables.put(System.identityHashCode(operands), opType); - } else if (symbol.getSignature() != null - && symbol.getSignature()[0] == DataConstraintModel.typeList) { - // If the root symbol of the term is the list type (except for the cons - // function). - List consExps = new ArrayList<>(); - consExps.add(t); - expToVariable.put(System.identityHashCode(t), consExps); - Type condType = t.getType(); - Map updatedVars = getUpdateSet(updateFromVariable, consExps); - for (int i = 1; i < symbol.getSignature().length; i++) { - Type tc = symbol.getSignature()[i]; - if (tc == DataConstraintModel.typeList) { - Expression e = t.getChildren().get(i - 1); - Type newType = getExpTypeIfUpdatable(condType, e); + Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2)); if (newType != null) { - condType = newType; - for (Expression e2 : consExps) { - if (e2 instanceof Variable) { - ((Variable) e2).setType(newType); - updatedVars.put(System.identityHashCode(e2), e2); - } else if (e2 instanceof Term) { - ((Term) e2).setType(newType); - updatedVars.put(System.identityHashCode(e2), e2); + // If the type of the 2nd argument of cons (1st argument of set/append) is more concrete than the type of the term. + t.setType(newType); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(t), t); + } else { + Type arg2Type = null; + if (consExps.get(2) != null && consExps.get(2) instanceof Variable) { + arg2Type = ((Variable) consExps.get(2)).getType(); + if (compareTypes(arg2Type, t.getType())) { + // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set/append). + ((Variable) consExps.get(2)).setType(t.getType()); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); + } + } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) { + arg2Type = ((Term) consExps.get(2)).getType(); + if (compareTypes(arg2Type, t.getType())) { + // If the type of the term is more concrete than the type of the 2nd argument of cons (1st argument of set/append). + ((Term) consExps.get(2)).setType(t.getType()); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); } } - } else { - if (e instanceof Variable && compareTypes(((Variable) e).getType(), condType)) { - ((Variable) e).setType(condType); - updatedVars.put(System.identityHashCode(e), e); - } else if (e instanceof Term && compareTypes(((Term) e).getType(), condType)) { - ((Term) e).setType(condType); - updatedVars.put(System.identityHashCode(e), e); + } + Type newCompType = getExpTypeIfUpdatable(listComponentTypes.get(t.getType()), consExps.get(1)); + if (newCompType != null) { + // If the type of the 1st argument of cons (3rd argument of set) is more concrete than the type of list component. + Type newListType = listTypes.get(newCompType); + if (newListType == null) { + // Create new list type. + newListType = createNewListType(newCompType, DataConstraintModel.typeList); + } + t.setType(newListType); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(t), t); + if (consExps.get(2) != null && consExps.get(2) instanceof Variable) { + ((Variable) consExps.get(2)).setType(newListType); + updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); + } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) { + ((Term) consExps.get(2)).setType(newListType); + updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); } } - consExps.add(e); - expToVariable.put(System.identityHashCode(e), consExps); + consOrSet.put(System.identityHashCode(consExps), t.getType()); + } else if (symbol.equals(DataConstraintModel.head) || symbol.equals(DataConstraintModel.get)) { + // If the root symbol of the term is head or get. + List consExps = new ArrayList<>(); + Expression e = t.getChildren().get(0); + consExps.add(e); // list argument + updateExpressionBelonging(expToConsOrSet, e, consExps); + consExps.add(t); // list's component + updateExpressionBelonging(expToConsOrSet, t, consExps); + consExps.add(null); + Type listType = listTypes.get(t.getType()); + if (listType == null && t.getType() != null) { + // Create a new list type. + listType = createNewListType(t.getType(), DataConstraintModel.typeList); + } + Type newListType = getExpTypeIfUpdatable(listType, consExps.get(0)); + if (newListType != null) { + // If the type of the component of the 1st argument is more concrete than the type of the term. + Type newCompType = listComponentTypes.get(newListType); + if (newCompType != null) { + t.setType(newCompType); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(t), t); + } + consOrSet.put(System.identityHashCode(consExps), newListType); + } else { + // If the type of the term is more concrete than the type of the component of the 1st argument. + if (consExps.get(0) != null && consExps.get(0) instanceof Variable) { + ((Variable) consExps.get(0)).setType(listType); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0)); + } else if (consExps.get(0) != null && consExps.get(0) instanceof Term) { + ((Term) consExps.get(0)).setType(listType); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(consExps.get(0)), consExps.get(0)); + } + consOrSet.put(System.identityHashCode(consExps), listType); + } + } else if (symbol.equals(DataConstraintModel.tail)) { + // If the root symbol of the term is tail. + List consExps = new ArrayList<>(); + consExps.add(t); // list term + updateExpressionBelonging(expToConsOrSet, t, consExps); + consExps.add(null); // list's component + Expression e = t.getChildren().get(0); + consExps.add(e); // list argument + updateExpressionBelonging(expToConsOrSet, e, consExps); + Type newType = getExpTypeIfUpdatable(t.getType(), consExps.get(2)); + if (newType != null) { + // If the type of the argument is more concrete than the type of the term. + t.setType(newType); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(t), t); + } else { + Type argType = null; + if (consExps.get(2) != null && consExps.get(2) instanceof Variable) { + argType = ((Variable) consExps.get(2)).getType(); + if (compareTypes(argType, t.getType())) { + // If the type of the term is more concrete than the type of the argument. + ((Variable) consExps.get(2)).setType(t.getType()); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); + } + } else if (consExps.get(2) != null && consExps.get(2) instanceof Term) { + argType = ((Term) consExps.get(2)).getType(); + if (compareTypes(argType, t.getType())) { + // If the type of the term is more concrete than the type of the argument. + ((Term) consExps.get(2)).setType(t.getType()); + Map updateCons = getUpdateSet(updateFromConsOrSet, consExps); + updateCons.put(System.identityHashCode(consExps.get(2)), consExps.get(2)); + } + } + } + consOrSet.put(System.identityHashCode(consExps), t.getType()); + } else if (symbol.equals(DataConstraintModel.tuple)) { + // If the root symbol of the term is tuple. + List tupleExps = new ArrayList<>(); + List newArgTypesList = new ArrayList<>(); + tupleExps.add(t); // tuple term + updateExpressionBelonging(expToTuple, t, tupleExps); + for (Expression e : t.getChildren()) { + tupleExps.add(e); // tuple's component + updateExpressionBelonging(expToTuple, e, tupleExps); + if (e instanceof Variable) { + newArgTypesList.add(((Variable) e).getType()); + } else if (e instanceof Term) { + newArgTypesList.add(((Term) e).getType()); + } else { + newArgTypesList.add(null); + } + } + if (t.getType() == DataConstraintModel.typeTuple) { + Type newTupleType = tupleTypes.get(newArgTypesList); + if (newTupleType == null) { + // Create new tuple type; + newTupleType = createNewTupleType(newArgTypesList, DataConstraintModel.typeTuple); + } + // Update the type of the tuple term and record the updated expression. + t.setType(newTupleType); + Map updateExps = getUpdateSet(updateFromTuple, tupleExps); + updateExps.put(System.identityHashCode(t), t); + } + tuple.put(System.identityHashCode(tupleExps), t.getType()); + } else if (symbol.equals(DataConstraintModel.pair)) { + // If the root symbol of the term is pair. + List pairExps = new ArrayList<>(); + pairExps.add(t); // pair + updateExpressionBelonging(expToPair, t, pairExps); + if (t.getType() == DataConstraintModel.typePair) { + for (Expression e : t.getChildren()) { + pairExps.add(e); // left/right + updateExpressionBelonging(expToPair, e, pairExps); + Type newArgType = null; + if (e instanceof Variable) { + newArgType = (((Variable) e).getType()); + + } else if (e instanceof Term) { + newArgType = (((Term) e).getType()); + } + + if (newArgType != null) { + Type newPairType = pairTypes.get(newArgType); + if (newPairType != null) { + t.setType(newPairType); + Map updateExps = getUpdateSet(updateFromPair, pairExps); + updateExps.put(System.identityHashCode(t), t); + } + } + } + pair.put(System.identityHashCode(pairExps), t.getType()); + + } + } else if (symbol.equals(DataConstraintModel.fst)) { + // If the root symbol of the term is fst. + List tupleExps = new ArrayList<>(); + Expression arg = t.getChildren().get(0); + tupleExps.add(arg); // tuple argument + updateExpressionBelonging(expToTuple, arg, tupleExps); + tupleExps.add(t); // first component + updateExpressionBelonging(expToTuple, t, tupleExps); + tupleExps.add(null); // second component + Type argType = null; + if (arg instanceof Variable) { + argType = ((Variable) arg).getType(); + } else if (arg instanceof Term) { + argType = ((Term) arg).getType(); + } + Type newTupleType = DataConstraintModel.typeTuple; + if (argType == DataConstraintModel.typeTuple && t.getType() != null) { + List newCompTypeList = new ArrayList<>(); + newCompTypeList.add(t.getType()); + newCompTypeList.add(null); + newTupleType = tupleTypes.get(newCompTypeList); + if (newTupleType == null) { + // Create new tuple type; + newTupleType = createNewTupleType(newCompTypeList, DataConstraintModel.typeTuple); + } + } + if (argType != newTupleType && newTupleType != null) { + // Update the type of the tuple argument and record the updated expression. + if (arg instanceof Variable) { + ((Variable) arg).setType(newTupleType); + argType = newTupleType; + } else if (arg instanceof Term) { + ((Term) arg).setType(newTupleType); + argType = newTupleType; + } + Map updateExps = getUpdateSet(updateFromTuple, tupleExps); + updateExps.put(System.identityHashCode(arg), arg); + } + tuple.put(System.identityHashCode(tupleExps), argType); + } else if (symbol.equals(DataConstraintModel.snd)) { + // If the root symbol of the term is snd. + List tupleExps = new ArrayList<>(); + Expression arg = t.getChildren().get(0); + tupleExps.add(arg); // tuple argument + updateExpressionBelonging(expToTuple, arg, tupleExps); + tupleExps.add(null); // first component + tupleExps.add(t); // second component + updateExpressionBelonging(expToTuple, t, tupleExps); + Type argType = null; + if (arg instanceof Variable) { + argType = ((Variable) arg).getType(); + } else if (arg instanceof Term) { + argType = ((Term) arg).getType(); + } + Type newTupleType = DataConstraintModel.typeTuple; + if (argType == DataConstraintModel.typeTuple && t.getType() != null) { + List newCompTypeList = new ArrayList<>(); + newCompTypeList.add(null); + if (DataConstraintModel.typeTuple.isAncestorOf(t.getType())) { + List sndTypes = tupleComponentTypes.get(t.getType()); + if (sndTypes != null) { + for (Type t2: sndTypes) { + newCompTypeList.add(t2); + } + } else { + newCompTypeList.add(t.getType()); + } + } else { + newCompTypeList.add(t.getType()); + } + newTupleType = tupleTypes.get(newCompTypeList); + if (newTupleType == null) { + // Create new tuple type; + newTupleType = createNewTupleType(newCompTypeList, DataConstraintModel.typeTuple); + } + } + if (argType != newTupleType && newTupleType != null) { + // Update the type of the tuple argument and record the updated expression. + if (arg instanceof Variable) { + ((Variable) arg).setType(newTupleType); + argType = newTupleType; + } else if (arg instanceof Term) { + ((Term) arg).setType(newTupleType); + argType = newTupleType; + } + Map updateExps = getUpdateSet(updateFromTuple, tupleExps); + 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); // pair + updateExpressionBelonging(expToPair, arg, pairExps); + pairExps.add(t); // left + updateExpressionBelonging(expToPair, t, pairExps); + pairExps.add(null); // right + 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 newCompTypeList = new ArrayList<>(); + newCompTypeList.add(t.getType()); + newCompTypeList.add(null); + newPairType = pairTypes.get(newCompTypeList); + if (newPairType == null) { + // Create new tuple type; + newPairType = createNewTupleType(newCompTypeList, 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); // pair + updateExpressionBelonging(expToPair, arg, pairExps); + pairExps.add(null); // left + pairExps.add(t); // right + updateExpressionBelonging(expToPair, 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 newCompTypeList = new ArrayList<>(); + newCompTypeList.add(null); + newCompTypeList.add(t.getType()); + newPairType = pairTypes.get(newCompTypeList); + if (newPairType == null) { + // Create new tuple type; + newPairType = createNewTupleType(newCompTypeList, 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.lookup)) { + // If the root symbol of the term is lookup. + List mapExps = new ArrayList<>(); + Expression arg1 = t.getChildren().get(0); // map + mapExps.add(arg1); + updateExpressionBelonging(expToMap, arg1, mapExps); + Expression arg2 = t.getChildren().get(1); // key + mapExps.add(arg2); + updateExpressionBelonging(expToMap, arg2, mapExps); + mapExps.add(t); // value + updateExpressionBelonging(expToMap, t, mapExps); + Type arg1Type = null; + if (arg1 instanceof Variable) { + arg1Type = ((Variable) arg1).getType(); + } else if (arg1 instanceof Term) { + arg1Type = ((Term) arg1).getType(); + } + List newCompTypeList = new ArrayList<>(); + if (arg2 instanceof Variable) { + newCompTypeList.add(((Variable) arg2).getType()); + } else if (arg2 instanceof Term) { + newCompTypeList.add(((Term) arg2).getType()); + } else { + newCompTypeList.add(null); + } + newCompTypeList.add(t.getType()); + if (arg1Type == DataConstraintModel.typeMap || arg1Type == null) { + Type newMapType = mapTypes.get(newCompTypeList); + if (newMapType == null) { + // Create new tuple type; + newMapType = createNewMapType(newCompTypeList, DataConstraintModel.typeMap); + } + // Update the type of the map argument and record the updated expression. + if (arg1 instanceof Variable) { + ((Variable) arg1).setType(newMapType); + arg1Type = newMapType; + } else if (arg1 instanceof Term) { + ((Term) arg1).setType(newMapType); + arg1Type = newMapType; + } + Map updateExps = getUpdateSet(updateFromMap, mapExps); + updateExps.put(System.identityHashCode(arg1), arg1); + } + map.put(System.identityHashCode(mapExps), arg1Type); + } else if (symbol.equals(DataConstraintModel.insert)) { + // If the root symbol of the term is insert. + List mapExps = new ArrayList<>(); + mapExps.add(t); // map + updateExpressionBelonging(expToMap, t, mapExps); + Expression arg1 = t.getChildren().get(1); // key + mapExps.add(arg1); + updateExpressionBelonging(expToMap, arg1, mapExps); + Expression arg2 = t.getChildren().get(2); // value + mapExps.add(arg2); + updateExpressionBelonging(expToMap, arg2, mapExps); + Expression arg0 = t.getChildren().get(0); // map + mapExps.add(arg0); + updateExpressionBelonging(expToMap, arg0, mapExps); + Type termType = t.getType(); + List newCompTypeList = new ArrayList<>(); + if (arg1 instanceof Variable) { + newCompTypeList.add(((Variable) arg1).getType()); + } else if (arg1 instanceof Term) { + newCompTypeList.add(((Term) arg1).getType()); + } else { + newCompTypeList.add(null); + } + if (arg2 instanceof Variable) { + newCompTypeList.add(((Variable) arg2).getType()); + } else if (arg2 instanceof Term) { + newCompTypeList.add(((Term) arg2).getType()); + } else { + newCompTypeList.add(null); + } + Type newTermType = getExpTypeIfUpdatable(termType, mapExps.get(3)); + if (newTermType != null) { + // If the type of the 1st argument of insert is more concrete than the type of the term. + t.setType(newTermType); + termType = newTermType; + Map updateExps = getUpdateSet(updateFromMap, mapExps); + updateExps.put(System.identityHashCode(t), t); + } else { + Type arg3Type = null; + if (mapExps.get(3) != null && mapExps.get(3) instanceof Variable) { + arg3Type = ((Variable) mapExps.get(3)).getType(); + if (compareTypes(arg3Type, t.getType())) { + // If the type of the term is more concrete than the type of the 1st argument of insert. + ((Variable) mapExps.get(3)).setType(t.getType()); + Map updateExps = getUpdateSet(updateFromMap, mapExps); + updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); + } + } else if (mapExps.get(3) != null && mapExps.get(3) instanceof Term) { + arg3Type = ((Term) mapExps.get(3)).getType(); + if (compareTypes(arg3Type, t.getType())) { + // If the type of the term is more concrete than the type of the 1st argument of insert. + ((Term) mapExps.get(3)).setType(t.getType()); + Map updateExps = getUpdateSet(updateFromMap, mapExps); + updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); + } + } + } + if (termType == DataConstraintModel.typeMap || termType == null) { + Type newMapType = mapTypes.get(newCompTypeList); + if (newMapType == null) { + // Create new tuple type; + newMapType = createNewMapType(newCompTypeList, DataConstraintModel.typeMap); + } + // Update the type of the map term and record the updated expression. + t.setType(newMapType); + Map updateExps = getUpdateSet(updateFromMap, mapExps); + updateExps.put(System.identityHashCode(t), t); + if (mapExps.get(3) != null && mapExps.get(3) instanceof Variable) { + ((Variable) mapExps.get(3)).setType(newMapType); + updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); + } else if (mapExps.get(3) != null && mapExps.get(3) instanceof Term) { + ((Term) mapExps.get(3)).setType(newMapType); + updateExps.put(System.identityHashCode(mapExps.get(3)), mapExps.get(3)); + } + termType = newMapType; + } + map.put(System.identityHashCode(mapExps), termType); + } else if (symbol.equals(DataConstraintModel.addMember)) { + // If the root symbol of the term is addMember (addMember(json, key, value)). + List dotExps = new ArrayList<>(); + Expression jsonArg = t.getChildren().get(0); + Expression keyArg = t.getChildren().get(1); + Expression valueArg = t.getChildren().get(2); + dotExps.add(t); // json + updateExpressionBelonging(expToJson, t, dotExps); + dotExps.add(keyArg); // key + updateExpressionBelonging(expToJson, keyArg, dotExps); + dotExps.add(valueArg); // value + updateExpressionBelonging(expToJson, valueArg, dotExps); + dotExps.add(jsonArg); // json + updateExpressionBelonging(expToJson, jsonArg, dotExps); + Type jsonType = t.getType(); + Type valueType = null; + if (valueArg instanceof Variable) { + valueType = ((Variable) valueArg).getType(); + } else if (valueArg instanceof Term) { + valueType = ((Term) valueArg).getType(); + } + String keyName = null; + if (keyArg instanceof Constant) { + keyName = ((Constant) keyArg).getSymbol().getName(); + } + Type jsonArgType = null; + if (jsonArg instanceof Variable) { + jsonArgType = ((Variable) jsonArg).getType(); + } else if (jsonArg instanceof Term) { + jsonArgType = ((Term) jsonArg).getType(); + } + Type newJsonType = DataConstraintModel.typeJson; + if (jsonType == DataConstraintModel.typeJson && jsonArgType != null && keyName != null) { + Map newMemberTypes = new HashMap<>(((JsonType) jsonArgType).getMemberTypes()); + newMemberTypes.put(keyName, valueType); + newJsonType = jsonTypes.get(newMemberTypes); + if (newJsonType == null) { + // Create new json type; + newJsonType = createNewJsonType(newMemberTypes, DataConstraintModel.typeJson); + } + } + if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) { + // Update the type of the json term and record the updated expression. + t.setType(newJsonType); + jsonType = newJsonType; + Map updateExps = getUpdateSet(updateFromJson, dotExps); + updateExps.put(System.identityHashCode(t), t); + } + json.put(System.identityHashCode(dotExps), jsonType); + } else if (symbol.equals(DataConstraintModel.dot)) { + // If the root symbol of the term is dot (json.property). + List dotExps = new ArrayList<>(); + Expression jsonArg = t.getChildren().get(0); + Expression keyArg = t.getChildren().get(1); + dotExps.add(jsonArg); // json + updateExpressionBelonging(expToJson, jsonArg, dotExps); + dotExps.add(keyArg); // key + updateExpressionBelonging(expToJson, keyArg, dotExps); + dotExps.add(t); // value + updateExpressionBelonging(expToJson, t, dotExps); + dotExps.add(null); // json + Type jsonType = null; + if (jsonArg instanceof Variable) { + jsonType = ((Variable) jsonArg).getType(); + } else if (jsonArg instanceof Term) { + jsonType = ((Term) jsonArg).getType(); + } + String keyName = null; + if (keyArg instanceof Constant) { + keyName = ((Constant) keyArg).getSymbol().getName(); + } + Type newJsonType = DataConstraintModel.typeJson; + if (jsonType == DataConstraintModel.typeJson && t.getType() != null && keyName != null) { + Map newMemberTypes = new HashMap<>(); + newMemberTypes.put(keyName, t.getType()); + newJsonType = jsonTypes.get(newMemberTypes); + if (newJsonType == null) { + // Create new json type; + newJsonType = createNewJsonType(newMemberTypes, DataConstraintModel.typeJson); + } + } + if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) { + // Update the type of the json argument and record the updated expression. + if (jsonArg instanceof Variable) { + ((Variable) jsonArg).setType(newJsonType); + jsonType = newJsonType; + } else if (jsonArg instanceof Term) { + ((Term) jsonArg).setType(newJsonType); + jsonType = newJsonType; + } + Map updateExps = getUpdateSet(updateFromJson, dotExps); + updateExps.put(System.identityHashCode(jsonArg), jsonArg); + } + json.put(System.identityHashCode(dotExps), jsonType); + } else if (symbol.equals(DataConstraintModel.dotParam)) { + // If the root symbol of the term is dot (json.{param}). + List dotExps = new ArrayList<>(); + Expression jsonArg = t.getChildren().get(0); + Expression keyArg = t.getChildren().get(1); + dotExps.add(jsonArg); // json (list/map) + updateExpressionBelonging(expToJson, jsonArg, dotExps); + dotExps.add(null); // key + dotExps.add(t); // value + updateExpressionBelonging(expToJson, t, dotExps); + dotExps.add(null); // json + Type jsonType = null; + if (jsonArg instanceof Variable) { + jsonType = ((Variable) jsonArg).getType(); + } else if (jsonArg instanceof Term) { + jsonType = ((Term) jsonArg).getType(); + } + Type keyType = null; + if (keyArg instanceof Variable) { + keyType = ((Variable) keyArg).getType(); + } else if (keyArg instanceof Term) { + keyType = ((Term) keyArg).getType(); + } + Type newJsonType = null; + if (keyType == DataConstraintModel.typeInt) { + newJsonType = DataConstraintModel.typeList; + } else if (keyType == DataConstraintModel.typeString) { + newJsonType = DataConstraintModel.typeMap; + } + if (t.getType() != null) { + if ((jsonType == DataConstraintModel.typeList)) { + newJsonType = listTypes.get(t.getType()); + if (newJsonType == null) { + // Create new list type; + newJsonType = createNewListType(t.getType(), DataConstraintModel.typeList); + } + } else if (jsonType == DataConstraintModel.typeMap) { + List keyValueTypes = Arrays.asList(new Type[] {DataConstraintModel.typeString, t.getType()}); + newJsonType = mapTypes.get(keyValueTypes); + if (newJsonType == null) { + // Create new map type; + newJsonType = createNewMapType(keyValueTypes, DataConstraintModel.typeMap); + } + } + } + if (jsonType != newJsonType && newJsonType != null && !newJsonType.isAncestorOf(jsonType)) { + // Update the type of the json argument and record the updated expression. + if (jsonArg instanceof Variable) { + ((Variable) jsonArg).setType(newJsonType); + jsonType = newJsonType; + } else if (jsonArg instanceof Term) { + ((Term) jsonArg).setType(newJsonType); + jsonType = newJsonType; + } + Map updateExps = getUpdateSet(updateFromJson, dotExps); + updateExps.put(System.identityHashCode(jsonArg), jsonArg); + } + json.put(System.identityHashCode(dotExps), jsonType); + } else if (symbol.equals(DataConstraintModel.cond)) { + // If the root symbol of the term is if function. + Expression c1 = t.getChild(1); + Expression c2 = t.getChild(2); + List condTerms = new ArrayList<>(); + condTerms.add(t); + condTerms.add(c1); + condTerms.add(c2); + expToVariable.put(System.identityHashCode(t), condTerms); + expToVariable.put(System.identityHashCode(c1), condTerms); + expToVariable.put(System.identityHashCode(c2), condTerms); + Type condType = t.getType(); + Map updatedVars = getUpdateSet(updateFromVariable, condTerms); + Type child1Type = getExpTypeIfUpdatable(condType, c1); + if (child1Type != null) { + condType = child1Type; + t.setType(child1Type); + updatedVars.put(System.identityHashCode(t), t); + } else { + if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), condType)) { + ((Variable) c1).setType(condType); + updatedVars.put(System.identityHashCode(c1), c1); + } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), condType)) { + ((Term) c1).setType(condType); + updatedVars.put(System.identityHashCode(c1), c1); + } + } + Type child2Type = getExpTypeIfUpdatable(condType, c2); + if (child2Type != null) { + condType = child2Type; + t.setType(child2Type); + updatedVars.put(System.identityHashCode(t), t); + if (c1 instanceof Variable) { + ((Variable) c1).setType(child2Type); + updatedVars.put(System.identityHashCode(c1), c1); + } else if (c1 instanceof Term) { + ((Term) c1).setType(child2Type); + updatedVars.put(System.identityHashCode(c1), c1); + } + } else { + if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), condType)) { + ((Variable) c2).setType(condType); + updatedVars.put(System.identityHashCode(c2), c2); + } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), condType)) { + ((Term) c2).setType(condType); + updatedVars.put(System.identityHashCode(c2), c2); + } + } + variables.put(System.identityHashCode(condTerms), condType); + } else if (symbol.equals(DataConstraintModel.add) || symbol.equals(DataConstraintModel.sub) + || symbol.equals(DataConstraintModel.mul) || symbol.equals(DataConstraintModel.div)) { + // If the root symbol of the term is arithmetic operators. + Expression c1 = t.getChild(0); + Expression c2 = t.getChild(1); + List operands = new ArrayList<>(); + operands.add(t); + operands.add(c1); + operands.add(c2); + expToVariable.put(System.identityHashCode(t), operands); + expToVariable.put(System.identityHashCode(c1), operands); + expToVariable.put(System.identityHashCode(c2), operands); + Type opType = t.getType(); + Map updatedVars = getUpdateSet(updateFromVariable, operands); + Type child1Type = getExpTypeIfUpdatable(opType, c1); + if (child1Type != null) { + opType = child1Type; + t.setType(child1Type); + updatedVars.put(System.identityHashCode(t), t); + } else { + if (c1 instanceof Variable && compareTypes(((Variable) c1).getType(), opType)) { + ((Variable) c1).setType(opType); + updatedVars.put(System.identityHashCode(c1), c1); + } else if (c1 instanceof Term && compareTypes(((Term) c1).getType(), opType)) { + ((Term) c1).setType(opType); + updatedVars.put(System.identityHashCode(c1), c1); + } + } + Type child2Type = getExpTypeIfUpdatable(opType, c2); + if (child2Type != null) { + opType = child2Type; + t.setType(child2Type); + updatedVars.put(System.identityHashCode(t), t); + if (c1 instanceof Variable) { + ((Variable) c1).setType(child2Type); + updatedVars.put(System.identityHashCode(c1), c1); + } else if (c1 instanceof Term) { + ((Term) c1).setType(child2Type); + updatedVars.put(System.identityHashCode(c1), c1); + } + } else { + if (c2 instanceof Variable && compareTypes(((Variable) c2).getType(), opType)) { + ((Variable) c2).setType(opType); + updatedVars.put(System.identityHashCode(c2), c2); + } else if (c2 instanceof Term && compareTypes(((Term) c2).getType(), opType)) { + ((Term) c2).setType(opType); + updatedVars.put(System.identityHashCode(c2), c2); + } + } + variables.put(System.identityHashCode(operands), opType); + } else if (symbol.getSignature() != null + && symbol.getSignature()[0] == DataConstraintModel.typeList) { + // If the root symbol of the term is the list type (except for the cons function). + List consExps = new ArrayList<>(); + consExps.add(t); + expToVariable.put(System.identityHashCode(t), consExps); + Type condType = t.getType(); + Map updatedVars = getUpdateSet(updateFromVariable, consExps); + for (int i = 1; i < symbol.getSignature().length; i++) { + Type tc = symbol.getSignature()[i]; + if (tc == DataConstraintModel.typeList) { + Expression e = t.getChildren().get(i - 1); + Type newType = getExpTypeIfUpdatable(condType, e); + if (newType != null) { + condType = newType; + for (Expression e2 : consExps) { + if (e2 instanceof Variable) { + ((Variable) e2).setType(newType); + updatedVars.put(System.identityHashCode(e2), e2); + } else if (e2 instanceof Term) { + ((Term) e2).setType(newType); + updatedVars.put(System.identityHashCode(e2), e2); + } + } + } else { + if (e instanceof Variable && compareTypes(((Variable) e).getType(), condType)) { + ((Variable) e).setType(condType); + updatedVars.put(System.identityHashCode(e), e); + } else if (e instanceof Term && compareTypes(((Term) e).getType(), condType)) { + ((Term) e).setType(condType); + updatedVars.put(System.identityHashCode(e), e); + } + } + consExps.add(e); + expToVariable.put(System.identityHashCode(e), consExps); + } + } + variables.put(System.identityHashCode(consExps), condType); } } - variables.put(System.identityHashCode(consExps), condType); + } + for (Channel childCh: ch.getChildren()) { + extractForChannel(childCh); } } + }; + extractConstraintsOnExpressionsInTerm.extractForChannel(ch); - // 1.5 Extract constraints on path parameters and resources. - ResourcePath rPath = cm.getResource(); - while (rPath != null) { - Expression param = rPath.getLastParam(); - if (param != null) { - ResourceHierarchy parent = rPath.getResourceHierarchy().getParent(); - if (parent != null) { - List pathParams = resourcePathParams.get(parent); - if (pathParams == null) { - pathParams = new ArrayList<>(); - resourcePathParams.put(parent, pathParams); - } - pathParams.add(param); - expToPathParams.put(System.identityHashCode(param), pathParams); - Type parentType = parent.getResourceStateType(); - Type paramType = null; - if (param instanceof Variable) { - paramType = ((Variable) param).getType(); - } else if (param instanceof Term) { - paramType = ((Term) param).getType(); - } - if (paramType != null && parentType == null) { - if (paramType.equals(DataConstraintModel.typeString)) { - parentType = DataConstraintModel.typeMap; - } else if (paramType.equals(DataConstraintModel.typeInt)) { - parentType = DataConstraintModel.typeList; - } - if (parentType != null) { - parent.setResourceStateType(parentType); - updateFromResourceOwnership.add(parent); + // 1.5 Extract constraints on path parameters and resources. + IExtractConstraintsOnPathParametersAndResources extractConstraintsOnPathParametersAndResources = new IExtractConstraintsOnPathParametersAndResources() { + public void extractForChannel(Channel ch) { + for (ChannelMember cm : ch.getChannelMembers()) { + ResourcePath rPath = cm.getResource(); + while (rPath != null) { + Expression param = rPath.getLastParam(); + if (param != null) { + ResourceHierarchy parent = rPath.getResourceHierarchy().getParent(); + if (parent != null) { + List pathParams = resourcePathParams.get(parent); + if (pathParams == null) { + pathParams = new ArrayList<>(); + resourcePathParams.put(parent, pathParams); + } + pathParams.add(param); + expToPathParams.put(System.identityHashCode(param), pathParams); + Type parentType = parent.getResourceStateType(); + Type paramType = null; + if (param instanceof Variable) { + paramType = ((Variable) param).getType(); + } else if (param instanceof Term) { + paramType = ((Term) param).getType(); + } + if (paramType != null && parentType == null) { + if (paramType.equals(DataConstraintModel.typeString)) { + parentType = DataConstraintModel.typeMap; + } else if (paramType.equals(DataConstraintModel.typeInt)) { + parentType = DataConstraintModel.typeList; + } + if (parentType != null) { + parent.setResourceStateType(parentType); + updateFromResourceOwnership.add(parent); + } + } } } + rPath = rPath.getParent(); } } - rPath = rPath.getParent(); + for (Channel childCh: ch.getChildren()) { + extractForChannel(childCh); + } } - } + }; + extractConstraintsOnPathParametersAndResources.extractForChannel(ch); } // 1.6 Extract constraints on resource hierarchies. @@ -2359,17 +2380,23 @@ return false; } - private static interface IRecurseForMessageVariable { - public void recurse(Channel rootCh, Channel ch, Expression message, - Map, Type>>> messages, - Map> expToMessage, - Map> updateFromMessage); + private static interface IGroupExpressionsByResource { + public void groupForChannel(Channel ch); } - private static interface IRecurseForMessageTerm { - public void recurse(Channel rootCh, Channel ch, Expression message, - Map, Type>>> messages, - Map> expToMessage, - Map> updateFromMessage); + private static interface IGroupExpressionsByVariable { + public void groupForChannel(Channel ch); + } + + private static interface IGroupExpressionsByMessage { + public void groupForChannel(Channel rootCh, Channel ch); + } + + private static interface IExtractConstraintsOnExpressionsInTerm { + public void extractForChannel(Channel ch); + } + + private static interface IExtractConstraintsOnPathParametersAndResources { + public void extractForChannel(Channel ch); } }