From 7d6662595fc3f7017b23459e99c92ba0199a4b76 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 25 Sep 2023 17:29:47 +0100 Subject: [PATCH] Merged with master --- .../src/main/java/quickcheck/QuickCheck.java | 42 ++----------------- .../strategies/FiniteQCStrategy.java | 4 +- .../strategies/FixedQCStrategy.java | 42 ++----------------- .../quickcheck/strategies/QCStrategy.java | 3 +- .../strategies/RandomQCStrategy.java | 7 +++- .../strategies/SearchQCStrategy.java | 3 +- .../visitors/FixedRangeCreator.java | 7 ---- .../visitors/RandomRangeCreator.java | 9 ---- .../quickcheck/example/ExampleQCStrategy.java | 3 +- .../vdmj/in/patterns/INMultipleTypeBind.java | 9 ++-- .../POExplicitFunctionDefinition.java | 18 +++----- .../POImplicitFunctionDefinition.java | 13 ------ .../java/com/fujitsu/vdmj/pog/POContext.java | 9 +--- .../com/fujitsu/vdmj/pog/POContextStack.java | 19 +-------- .../vdmj/pog/POFunctionDefinitionContext.java | 10 ----- .../com/fujitsu/vdmj/pog/ProofObligation.java | 3 -- .../fujitsu/vdmj/pog/ProofObligationList.java | 30 +------------ 17 files changed, 31 insertions(+), 200 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 8b7cedbdb..d113c69c1 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -36,13 +36,11 @@ 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.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; @@ -54,12 +52,8 @@ 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; @@ -252,12 +246,6 @@ 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 @@ -321,11 +309,10 @@ 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, ctxt); + Results presults = strategy.getValues(po, exp, binds); Map cexamples = presults.counterexamples; for (String bind: cexamples.keySet()) @@ -348,6 +335,7 @@ 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); @@ -362,9 +350,9 @@ public void checkObligation(ProofObligation po, Results results) try { resetErrors(); // Only flag fatal errors - Context ctxt = Interpreter.getInstance().getInitialContext(); + RootContext ctxt = Interpreter.getInstance().getInitialContext(); INExpression poexp = getINExpression(po); - List bindings = getINBindList(poexp); + List bindings = getINBindList(poexp);; if (!po.isCheckable) { @@ -409,8 +397,6 @@ else if (results.proved && Value result = new BooleanValue(false); ContextException exception = null; - ctxt = addTypeParams(po, ctxt); - try { verbose("PO #%d, starting...\n", po.number); @@ -511,26 +497,6 @@ 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 b175c9d40..495cd7d6c 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -38,6 +38,7 @@ 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; @@ -121,7 +122,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public Results getValues(ProofObligation po, INExpression exp, List binds) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); @@ -129,6 +130,7 @@ 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); + TCType mbtype = mb.typeCheck(env, NameScope.NAMESANDSTATE); TCSetType mbset = new TCSetType(mb.location, mbtype); tctypes.add(mbtype); TCExpression exp = tcexps.get(i); - TCType exptype = exp.typeCheck(penv, null, NameScope.NAMESANDSTATE, null); + TCType exptype = exp.typeCheck(env, null, NameScope.NAMESANDSTATE, null); if (TypeChecker.getErrorCount() > 0) { for (VDMError error: TypeChecker.getErrors()) { - println(mb + " = " + exp); + println(exp); println(error.toString()); errorCount++; } @@ -472,7 +438,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public Results getValues(ProofObligation po, INExpression exp, List binds) { 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 a0ad97ba2..a38e420c6 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java @@ -29,7 +29,6 @@ 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; @@ -39,6 +38,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, Context ctxt); + abstract public Results getValues(ProofObligation po, INExpression exp, List binds); 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 3d0925f50..08c12caa2 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java @@ -34,7 +34,8 @@ 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.runtime.Interpreter; +import com.fujitsu.vdmj.runtime.RootContext; import com.fujitsu.vdmj.values.ValueList; import com.fujitsu.vdmj.values.ValueSet; @@ -127,13 +128,15 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public Results getValues(ProofObligation po, INExpression exp, List binds) { 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 bf76acf6d..c609730ee 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -32,7 +32,6 @@ 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; @@ -79,7 +78,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public Results getValues(ProofObligation po, INExpression exp, List binds) { 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 f01c1e652..fa91c348b 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java @@ -49,7 +49,6 @@ 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; @@ -119,12 +118,6 @@ 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 fdff9528b..9131fdbe4 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/RandomRangeCreator.java @@ -45,7 +45,6 @@ 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; @@ -73,7 +72,6 @@ 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; @@ -122,13 +120,6 @@ 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 786d8d564..f3c09b9d9 100644 --- a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -33,7 +33,6 @@ 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; @@ -94,7 +93,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public Results getValues(ProofObligation po, INExpression exp, List binds) { 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 d2c8223cd..8930a3340 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,18 +40,17 @@ 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.hasPolymorphic = !type.apply(new TCParameterCollector(), null).isEmpty(); + this.hasTypeParams = !type.apply(new TCParameterCollector(), null).isEmpty(); } @Override @@ -66,13 +65,11 @@ public void setBindValues(ValueList values) if (values == null) { bindValues = null; - bindOverride = false; } else { bindValues = new ValueList(); bindValues.addAll(values); - bindOverride = true; } } @@ -110,7 +107,7 @@ public TCType getType() @Override public ValueList getBindValues(Context ctxt, boolean permuted) throws ValueException { - if (bindOverride || (bindValues != null && bindPermuted == permuted && !hasPolymorphic)) + if (bindValues != null && bindPermuted == permuted && !hasTypeParams) { 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 a7168fced..5b2838184 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,9 +136,13 @@ 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) { @@ -153,12 +157,6 @@ 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)); @@ -207,12 +205,6 @@ 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 acaa53987..7ec45fb98 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,7 +135,6 @@ 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) { @@ -149,12 +148,6 @@ 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) { @@ -213,12 +206,6 @@ 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/POContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java index 449d880f0..ca6d28cda 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java @@ -33,23 +33,16 @@ 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 { - private Map knownTypes = new HashMap(); - abstract public String getContext(); + private Map knownTypes = new HashMap(); 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 22eaa9aac..1ec83da07 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -30,7 +30,6 @@ 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 @@ -101,22 +100,8 @@ public String getObligation(String root) result.append(tail); result.append("\n"); - return result.toString(); - } - - public TCTypeList getTypeParams() - { - for (POContext ctxt: this) - { - TCTypeList params = ctxt.getTypeParams(); - - if (params != null && !params.isEmpty()) - { - return params; - } - } - - return null; + // Finally, we change any polymorphic types to "?" for now + return result.toString().replaceAll("@\\w+", "?"); } 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 d7999d712..0baa0c915 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java @@ -35,13 +35,11 @@ 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; @@ -51,7 +49,6 @@ public POFunctionDefinitionContext( { this.name = definition.name; this.deftype = definition.type; - this.typeParams = definition.typeParams; this.paramPatternList = definition.paramPatternList; this.addPrecond = precond; POGetMatchingExpressionVisitor.init(); @@ -63,7 +60,6 @@ public POFunctionDefinitionContext( { this.name = definition.name; this.deftype = definition.type; - this.typeParams = definition.typeParams; this.addPrecond = precond; this.paramPatternList = definition.getParamPatternList(); POGetMatchingExpressionVisitor.init(); @@ -118,10 +114,4 @@ public String getContext() return sb.toString(); } - - @Override - public TCTypeList getTypeParams() - { - return typeParams; - } } 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 0cb1fd626..24ebc487c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -28,7 +28,6 @@ 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 { @@ -41,7 +40,6 @@ 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; @@ -55,7 +53,6 @@ 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 c9bebfc0f..1b108f3d5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -41,17 +41,12 @@ 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; @@ -164,10 +159,9 @@ 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(tcenv, null, NameScope.NAMESANDANYSTATE, null); + TCType potype = tcexp.typeCheck(env, null, NameScope.NAMESANDANYSTATE, null); if (!potype.isType(TCBooleanType.class, obligation.location)) { @@ -212,26 +206,4 @@ 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; - } - } }