diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 80f4527aa..2e59c983a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -38,8 +38,10 @@ import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.tc.expressions.TCExpression; +import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; +import com.fujitsu.vdmj.values.ParameterValue; abstract public class ProofObligation implements Comparable { @@ -259,10 +261,15 @@ private String launchExplicitFunction(POExplicitFunctionDefinition efd, Context StringBuilder callString = new StringBuilder(efd.name.getName()); PORemoveIgnoresVisitor.init(); + if (efd.typeParams != null) + { + callString.append(addTypeParams(efd.typeParams, ctxt)); + } + for (POPatternList pl: efd.paramPatternList) { - callString.append("("); String sep = ""; + callString.append("("); for (POPattern p: pl) { @@ -283,14 +290,20 @@ private String launchExplicitFunction(POExplicitFunctionDefinition efd, Context return callString.toString(); } - + private String launchImplicitFunction(POImplicitFunctionDefinition ifd, Context ctxt) { StringBuilder callString = new StringBuilder(ifd.name.getName()); - callString.append("("); - String sep = ""; PORemoveIgnoresVisitor.init(); + if (ifd.typeParams != null) + { + callString.append(addTypeParams(ifd.typeParams, ctxt)); + } + + String sep = ""; + callString.append("("); + for (POPatternListTypePair pl: ifd.parameterPatterns) { for (POPattern p: pl.patterns) @@ -313,6 +326,25 @@ private String launchImplicitFunction(POImplicitFunctionDefinition ifd, Context return callString.toString(); } + private String addTypeParams(TCTypeList params, Context ctxt) + { + StringBuilder callString = new StringBuilder(); + String sep = ""; + callString.append("["); + + for (TCType p: params) + { + TCParameterType param = (TCParameterType)p; + ParameterValue inst = (ParameterValue) ctxt.get(param.name); + callString.append(sep); + callString.append(inst.type); + sep = ", "; + } + + callString.append("]"); + return callString.toString(); + } + private String paramMatch(POPattern p, Context ctxt) { POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor();