diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index d76a2a28e..8b7cedbdb 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -36,13 +36,14 @@ import java.util.Map; import java.util.Vector; +import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.lex.LexBooleanToken; import com.fujitsu.vdmj.in.INNode; import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression; import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; +import com.fujitsu.vdmj.lex.Dialect; import com.fujitsu.vdmj.mapper.ClassMapper; -import com.fujitsu.vdmj.messages.Console; import com.fujitsu.vdmj.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -53,8 +54,12 @@ import com.fujitsu.vdmj.tc.expressions.TCExistsExpression; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.tc.types.TCParameterType; +import com.fujitsu.vdmj.tc.types.TCRealType; +import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.util.GetResource; import com.fujitsu.vdmj.values.BooleanValue; +import com.fujitsu.vdmj.values.ParameterValue; import com.fujitsu.vdmj.values.Value; import com.fujitsu.vdmj.values.ValueList; @@ -247,6 +252,12 @@ public ProofObligationList getPOs(ProofObligationList all, List poList) } } + if (!all.isEmpty() && chosen.isEmpty()) + { + String m = (Settings.dialect == Dialect.VDM_SL) ? "module" : "class"; + println("No POs in current " + m + " (" + def + ")"); + } + return chosen; // No PO#s specified, so use default class/module's POs } else @@ -310,10 +321,11 @@ public Results getValues(ProofObligation po) INExpression exp = getINExpression(po); List binds = getINBindList(exp); long before = System.currentTimeMillis(); + Context ctxt = addTypeParams(po, Interpreter.getInstance().getInitialContext()); for (QCStrategy strategy: strategies) { - Results presults = strategy.getValues(po, exp, binds); + Results presults = strategy.getValues(po, exp, binds, ctxt); Map cexamples = presults.counterexamples; for (String bind: cexamples.keySet()) @@ -336,7 +348,6 @@ public Results getValues(ProofObligation po) if (!union.containsKey(bind.toString())) { // Generate some values for missing bindings, using the fixed method - RootContext ctxt = Interpreter.getInstance().getInitialContext(); ValueList list = new ValueList(); list.addAll(bind.getType().apply(new FixedRangeCreator(ctxt), 10)); union.put(bind.toString(), list); @@ -351,9 +362,9 @@ public void checkObligation(ProofObligation po, Results results) try { resetErrors(); // Only flag fatal errors - RootContext ctxt = Interpreter.getInstance().getInitialContext(); + Context ctxt = Interpreter.getInstance().getInitialContext(); INExpression poexp = getINExpression(po); - List bindings = getINBindList(poexp);; + List bindings = getINBindList(poexp); if (!po.isCheckable) { @@ -396,6 +407,9 @@ else if (results.proved && long before = System.currentTimeMillis(); Value result = new BooleanValue(false); + ContextException exception = null; + + ctxt = addTypeParams(po, ctxt); try { @@ -404,8 +418,6 @@ else if (results.proved && } catch (ContextException e) { - printf("PO #%d, Exception: %s\n", po.number, e.getMessage()); - if (e.rawMessage.equals("Execution cancelled")) { result = null; @@ -413,19 +425,7 @@ else if (results.proved && else { result = new BooleanValue(false); - - if (e.ctxt.outer != null) - { - e.ctxt.printStackFrames(Console.out); - } - else - { - println("In context of " + e.ctxt.title + " " + e.ctxt.location); - } - - println("----"); - printBindings(bindings); - println("----"); + exception = e; } } @@ -465,10 +465,15 @@ else if (result instanceof BooleanValue) { printf("PO #%d, FAILED %s: ", po.number, duration(before, after)); printFailPath(bindings); + + if (exception != null) + { + printf("Causes %s\n", exception.getMessage()); + } + println("----"); println(po); } - } } else @@ -506,6 +511,26 @@ else if (result instanceof BooleanValue) } } + private Context addTypeParams(ProofObligation po, Context ctxt) + { + if (po.typeParams != null) + { + Context params = new Context(po.location, "Type params", ctxt); + + for (TCType type: po.typeParams) + { + TCParameterType ptype = (TCParameterType)type; + params.put(ptype.name, new ParameterValue(new TCRealType(po.location))); + } + + return params; + } + else + { + return ctxt; + } + } + private void printBindings(List bindings) { int MAXVALUES = 10; diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index 495cd7d6c..b175c9d40 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -38,7 +38,6 @@ import com.fujitsu.vdmj.messages.InternalException; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.runtime.Context; -import com.fujitsu.vdmj.runtime.Interpreter; import com.fujitsu.vdmj.values.ValueList; import quickcheck.QuickCheck; @@ -122,7 +121,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); @@ -130,7 +129,6 @@ public Results getValues(ProofObligation po, INExpression exp, List readRangeFile(String filename) for (int i=0; i names = mtb.type.apply(new TCParameterCollector(), null); + + if (!names.isEmpty()) + { + TCDefinitionList defs = new TCDefinitionList(); + LexLocation location = mtb.type.location; + + for (String name: names) + { + TCNameToken tcname = new TCNameToken(location, module, name.substring(1)); + TCParameterType ptype = new TCParameterType(tcname); + TCDefinition p = new TCLocalDefinition(location, tcname, ptype); + p.markUsed(); + defs.add(p); + } + + penv = new FlatEnvironment(defs, env); + } + } + + TCType mbtype = mb.typeCheck(penv, NameScope.NAMESANDSTATE); TCSetType mbset = new TCSetType(mb.location, mbtype); tctypes.add(mbtype); TCExpression exp = tcexps.get(i); - TCType exptype = exp.typeCheck(env, null, NameScope.NAMESANDSTATE, null); + TCType exptype = exp.typeCheck(penv, null, NameScope.NAMESANDSTATE, null); if (TypeChecker.getErrorCount() > 0) { for (VDMError error: TypeChecker.getErrors()) { - println(exp); + println(mb + " = " + exp); println(error.toString()); errorCount++; } @@ -438,7 +472,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { Map values = new HashMap(); long before = System.currentTimeMillis(); diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java index a38e420c6..a0ad97ba2 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.runtime.Context; import quickcheck.QuickCheck; @@ -38,6 +39,6 @@ abstract public class QCStrategy abstract public boolean hasErrors(); abstract public boolean useByDefault(); abstract public boolean init(QuickCheck qc); - abstract public Results getValues(ProofObligation po, INExpression exp, List binds); + abstract public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt); abstract public String help(); } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java index 08c12caa2..3d0925f50 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java @@ -34,8 +34,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; -import com.fujitsu.vdmj.runtime.Interpreter; -import com.fujitsu.vdmj.runtime.RootContext; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.values.ValueList; import com.fujitsu.vdmj.values.ValueSet; @@ -128,15 +127,13 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); if (po.isCheckable && po.getCheckedExpression() != null) { - RootContext ctxt = Interpreter.getInstance().getInitialContext(); - for (INBindingSetter bind: binds) { RandomRangeCreator visitor = new RandomRangeCreator(ctxt, seed++); diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index c609730ee..bf76acf6d 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -32,6 +32,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.values.NameValuePair; import com.fujitsu.vdmj.values.NameValuePairList; import com.fujitsu.vdmj.values.ValueList; @@ -78,7 +79,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); diff --git a/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java b/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java index fa91c348b..f01c1e652 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java @@ -49,6 +49,7 @@ import com.fujitsu.vdmj.tc.types.TCNaturalOneType; import com.fujitsu.vdmj.tc.types.TCNaturalType; import com.fujitsu.vdmj.tc.types.TCOptionalType; +import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCProductType; import com.fujitsu.vdmj.tc.types.TCQuoteType; import com.fujitsu.vdmj.tc.types.TCRationalType; @@ -118,6 +119,12 @@ public ValueSet caseUnknownType(TCUnknownType node, Integer limit) // Anything... ? return caseBooleanType(new TCBooleanType(LexLocation.ANY), limit); } + + @Override + public ValueSet caseParameterType(TCParameterType node, Integer limit) + { + return realLimit(limit); // For now...! + } @Override public ValueSet caseBooleanType(TCBooleanType type, Integer limit) diff --git a/examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java b/examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java index 9131fdbe4..fdff9528b 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java @@ -45,6 +45,7 @@ import com.fujitsu.vdmj.tc.types.TCNaturalOneType; import com.fujitsu.vdmj.tc.types.TCNaturalType; import com.fujitsu.vdmj.tc.types.TCOptionalType; +import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCProductType; import com.fujitsu.vdmj.tc.types.TCQuoteType; import com.fujitsu.vdmj.tc.types.TCRationalType; @@ -72,6 +73,7 @@ import com.fujitsu.vdmj.values.NaturalOneValue; import com.fujitsu.vdmj.values.NaturalValue; import com.fujitsu.vdmj.values.NilValue; +import com.fujitsu.vdmj.values.ParameterValue; import com.fujitsu.vdmj.values.QuoteValue; import com.fujitsu.vdmj.values.RealValue; import com.fujitsu.vdmj.values.RecordValue; @@ -120,6 +122,13 @@ public ValueSet caseUnknownType(TCUnknownType node, Integer limit) // Anything... ? return caseBooleanType(new TCBooleanType(LexLocation.ANY), limit); } + + @Override + public ValueSet caseParameterType(TCParameterType node, Integer limit) + { + ParameterValue pv = (ParameterValue) ctxt.get(node.name); + return pv.type.apply(this, limit); + } @Override public ValueSet caseBooleanType(TCBooleanType type, Integer limit) diff --git a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java index f3c09b9d9..786d8d564 100644 --- a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -33,6 +33,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.values.ValueList; import quickcheck.QuickCheck; @@ -93,7 +94,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { Map values = new HashMap(); long before = System.currentTimeMillis(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java index 8930a3340..d2c8223cd 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java @@ -40,17 +40,18 @@ public class INMultipleTypeBind extends INMultipleBind implements INBindingSette { private static final long serialVersionUID = 1L; public final TCType type; - public final boolean hasTypeParams; private ValueList bindValues = null; private Context bindCounterexample = null; private boolean bindPermuted = false; + private boolean bindOverride = false; // True if forcing QC values + private boolean hasPolymorphic = false; public INMultipleTypeBind(INPatternList plist, TCType type) { super(plist); this.type = type; - this.hasTypeParams = !type.apply(new TCParameterCollector(), null).isEmpty(); + this.hasPolymorphic = !type.apply(new TCParameterCollector(), null).isEmpty(); } @Override @@ -65,11 +66,13 @@ public void setBindValues(ValueList values) if (values == null) { bindValues = null; + bindOverride = false; } else { bindValues = new ValueList(); bindValues.addAll(values); + bindOverride = true; } } @@ -107,7 +110,7 @@ public TCType getType() @Override public ValueList getBindValues(Context ctxt, boolean permuted) throws ValueException { - if (bindValues != null && bindPermuted == permuted && !hasTypeParams) + if (bindOverride || (bindValues != null && bindPermuted == permuted && !hasPolymorphic)) { return bindValues; // Should be exactly the same } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java index 5b2838184..a7168fced 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java @@ -136,13 +136,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment ProofObligationList obligations = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); - if (typeParams != null && !typeParams.isEmpty()) - { - return obligations; // Cannot generate POs for polymorphic fns (yet) - } - TCNameList pids = new TCNameList(); boolean matchNeeded = false; + boolean polymorphic = (typeParams != null && !typeParams.isEmpty()); for (POPatternList pl: paramPatternList) { @@ -157,6 +153,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment } } + if (polymorphic) + { + // Cannot generate POs for polymorphic fns (yet), so unchecked + // ctxt.push(new PONoCheckContext()); + } + if (type.hasTotal()) { ctxt.push(new POFunctionDefinitionContext(this, true)); @@ -205,6 +207,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment ctxt.pop(); + if (polymorphic) + { + // Cannot generate POs for polymorphic fns (yet), so unchecked + // ctxt.pop(); + } + if (annotations != null) annotations.poAfter(this, obligations, ctxt); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java index 7ec45fb98..acaa53987 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java @@ -135,6 +135,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); TCNameList pids = new TCNameList(); boolean matchNeeded = false; + boolean polymorphic = (typeParams != null && !typeParams.isEmpty()); for (POPatternListTypePair pltp: parameterPatterns) { @@ -148,6 +149,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment matchNeeded = true; } } + + if (polymorphic) + { + // Cannot generate POs for polymorphic fns (yet), so unchecked + // ctxt.push(new PONoCheckContext()); + } if (pids.hasDuplicates() || matchNeeded) { @@ -206,6 +213,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment ctxt.pop(); } + if (polymorphic) + { + // Cannot generate POs for polymorphic fns (yet), so unchecked + // ctxt.pop(); + } + if (annotations != null) annotations.poAfter(this, obligations, ctxt); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java index 08767ea30..1c937034c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java @@ -60,7 +60,7 @@ public String getContext() sb.append("exists "); sb.append(pattern.getMatchingExpression()); sb.append(":"); - sb.append(type); + sb.append(type.toExplicitString(pattern.location)); sb.append(" & "); POGetMatchingExpressionVisitor.init(); sb.append(pattern.getMatchingExpression()); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java index ca6d28cda..449d880f0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java @@ -33,16 +33,23 @@ import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; abstract public class POContext { - abstract public String getContext(); private Map knownTypes = new HashMap(); + abstract public String getContext(); + public String getName() { return ""; // Overridden in PONameContext } + + public TCTypeList getTypeParams() + { + return null; + } public boolean isScopeBoundary() { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java index 1ec83da07..22eaa9aac 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; @SuppressWarnings("serial") public class POContextStack extends Stack @@ -100,8 +101,22 @@ public String getObligation(String root) result.append(tail); result.append("\n"); - // Finally, we change any polymorphic types to "?" for now - return result.toString().replaceAll("@\\w+", "?"); + return result.toString(); + } + + public TCTypeList getTypeParams() + { + for (POContext ctxt: this) + { + TCTypeList params = ctxt.getTypeParams(); + + if (params != null && !params.isEmpty()) + { + return params; + } + } + + return null; } private String indentNewLines(String line, String indent) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java index 0baa0c915..d7999d712 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java @@ -35,11 +35,13 @@ import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCFunctionType; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; public class POFunctionDefinitionContext extends POContext { public final TCNameToken name; public final TCFunctionType deftype; + public final TCTypeList typeParams; public final List paramPatternList; public final boolean addPrecond; public final String precondition; @@ -49,6 +51,7 @@ public POFunctionDefinitionContext( { this.name = definition.name; this.deftype = definition.type; + this.typeParams = definition.typeParams; this.paramPatternList = definition.paramPatternList; this.addPrecond = precond; POGetMatchingExpressionVisitor.init(); @@ -60,6 +63,7 @@ public POFunctionDefinitionContext( { this.name = definition.name; this.deftype = definition.type; + this.typeParams = definition.typeParams; this.addPrecond = precond; this.paramPatternList = definition.getParamPatternList(); POGetMatchingExpressionVisitor.init(); @@ -114,4 +118,10 @@ public String getContext() return sb.toString(); } + + @Override + public TCTypeList getTypeParams() + { + return typeParams; + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONotCaseContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONotCaseContext.java index 9b43127a3..9a104312d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONotCaseContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONotCaseContext.java @@ -60,7 +60,7 @@ public String getContext() sb.append("not exists "); sb.append(pattern.getMatchingExpression()); sb.append(":"); - sb.append(type); + sb.append(type.toExplicitString(pattern.location)); sb.append(" & "); POGetMatchingExpressionVisitor.init(); sb.append(pattern.getMatchingExpression()); 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 24ebc487c..0cb1fd626 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; abstract public class ProofObligation implements Comparable { @@ -40,6 +41,7 @@ abstract public class ProofObligation implements Comparable public POStatus status; public POTrivialProof proof; public boolean isCheckable; + public TCTypeList typeParams; private int var = 1; private TCExpression checkedExpression = null; @@ -53,6 +55,7 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.proof = null; this.number = 0; this.isCheckable = ctxt.isCheckable(); // Set false for operation POs + this.typeParams = ctxt.getTypeParams(); if (!isCheckable) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 1b108f3d5..c9bebfc0f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -41,12 +41,17 @@ import com.fujitsu.vdmj.syntax.ExpressionReader; import com.fujitsu.vdmj.syntax.ParserException; import com.fujitsu.vdmj.tc.TCNode; +import com.fujitsu.vdmj.tc.definitions.TCDefinition; +import com.fujitsu.vdmj.tc.definitions.TCDefinitionList; +import com.fujitsu.vdmj.tc.definitions.TCLocalDefinition; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.modules.TCModule; import com.fujitsu.vdmj.tc.types.TCBooleanType; +import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; +import com.fujitsu.vdmj.typechecker.FlatEnvironment; import com.fujitsu.vdmj.typechecker.NameScope; import com.fujitsu.vdmj.typechecker.TypeChecker; @@ -159,9 +164,10 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env } TCExpression tcexp = ClassMapper.getInstance(TCNode.MAPPINGS).convert(ast); + Environment tcenv = addTypeParams(obligation, env); TypeChecker.clearErrors(); - TCType potype = tcexp.typeCheck(env, null, NameScope.NAMESANDANYSTATE, null); + TCType potype = tcexp.typeCheck(tcenv, null, NameScope.NAMESANDANYSTATE, null); if (!potype.isType(TCBooleanType.class, obligation.location)) { @@ -206,4 +212,26 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env obligation.setCheckedExpression(tcexp); } + + private Environment addTypeParams(ProofObligation obligation, Environment env) + { + if (obligation.typeParams != null && !obligation.typeParams.isEmpty()) + { + TCDefinitionList pdefs = new TCDefinitionList(); + + for (TCType ptype: obligation.typeParams) + { + TCParameterType param = (TCParameterType)ptype; + TCDefinition p = new TCLocalDefinition(param.location, param.name, param); + p.markUsed(); + pdefs.add(p); + } + + return new FlatEnvironment(pdefs, env); + } + else + { + return env; + } + } } diff --git a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java index a1b0236d3..f1979e732 100644 --- a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java +++ b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java @@ -82,11 +82,11 @@ protected void tearDown() throws Exception /* 15 */ "(forall a:int, b:int &\n pre_prepostf(a, b) => post_prepostf(a, b, (a + b)))\n", /* 16 */ "(forall mk_(a, b):(int) * (int), c:(int) * (int) &\n is_(pre_prepostfi(mk_(a, b), c), bool))\n", /* 17 */ "(forall mk_(a, b):(int) * (int), c:(int) * (int) &\n pre_prepostfi(mk_(a, b), c) => exists r:int & post_prepostfi(mk_(a, b), c, r))\n", - /* 18 */ "(forall x:seq of int &\n (exists [a]:seq1 of (int) & [a] = x ^ [-999] => let [a] = x ^ [-999] in\n a in set dom m))\n", - /* 19 */ "(forall x:seq of int &\n (not exists [a]:seq1 of (int) & [a] = x ^ [-999] =>\n (exists [a, b]:seq1 of (int) & [a, b] = x ^ [-999] => let [a, b] = x ^ [-999] in\n (a + b) in set dom m)))\n", - /* 20 */ "(forall x:seq of int &\n (not exists [a]:seq1 of (int) & [a] = x ^ [-999] =>\n (not exists [a, b]:seq1 of (int) & [a, b] = x ^ [-999] =>\n (exists [a] ^ [b]:seq1 of (int) & [a] ^ [b] = x ^ [-999] => let [a] ^ [b] = x ^ [-999] in\n (a + b) in set dom m))))\n", - /* 21 */ "(forall x:seq of int &\n (not exists [a]:seq1 of (int) & [a] = x ^ [-999] =>\n (not exists [a, b]:seq1 of (int) & [a, b] = x ^ [-999] =>\n (not exists [a] ^ [b]:seq1 of (int) & [a] ^ [b] = x ^ [-999] =>\n m(999) in set dom m))))\n", - /* 22 */ "(forall x:seq of int &\n (not exists [a]:seq1 of (int) & [a] = x ^ [-999] =>\n (not exists [a, b]:seq1 of (int) & [a, b] = x ^ [-999] =>\n (not exists [a] ^ [b]:seq1 of (int) & [a] ^ [b] = x ^ [-999] =>\n 999 in set dom m))))\n", + /* 18 */ "(forall x:seq of int &\n (exists [a]:seq1 of int & [a] = x ^ [-999] => let [a] = x ^ [-999] in\n a in set dom m))\n", + /* 19 */ "(forall x:seq of int &\n (not exists [a]:seq1 of int & [a] = x ^ [-999] =>\n (exists [a, b]:seq1 of int & [a, b] = x ^ [-999] => let [a, b] = x ^ [-999] in\n (a + b) in set dom m)))\n", + /* 20 */ "(forall x:seq of int &\n (not exists [a]:seq1 of int & [a] = x ^ [-999] =>\n (not exists [a, b]:seq1 of int & [a, b] = x ^ [-999] =>\n (exists [a] ^ [b]:seq1 of int & [a] ^ [b] = x ^ [-999] => let [a] ^ [b] = x ^ [-999] in\n (a + b) in set dom m))))\n", + /* 21 */ "(forall x:seq of int &\n (not exists [a]:seq1 of int & [a] = x ^ [-999] =>\n (not exists [a, b]:seq1 of int & [a, b] = x ^ [-999] =>\n (not exists [a] ^ [b]:seq1 of int & [a] ^ [b] = x ^ [-999] =>\n m(999) in set dom m))))\n", + /* 22 */ "(forall x:seq of int &\n (not exists [a]:seq1 of int & [a] = x ^ [-999] =>\n (not exists [a, b]:seq1 of int & [a, b] = x ^ [-999] =>\n (not exists [a] ^ [b]:seq1 of int & [a] ^ [b] = x ^ [-999] =>\n 999 in set dom m))))\n", /* 23 */ "(forall mk_(i, $any1):(int) * (int) &\n exists x in set {m(1), 2, 3} & (m(x) < i))\n", /* 24 */ "(forall mk_(i, $any1):(int) * (int) &\n 1 in set dom m)\n", /* 25 */ "(forall mk_(i, $any1):(int) * (int) &\n (forall x in set {m(1), 2, 3} &\n x in set dom m))\n",