Merged with master

nickbattle · Sep 25, 2023 · 7d66625 · 7d66625
1 parent 78988d2
commit 7d66625
Show file tree

Hide file tree

Showing 17 changed files with 31 additions and 200 deletions.
diff --git 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<Integer> 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<INBindingSetter> 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<String, ValueList> 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<INBindingSetter> bindings = getINBindList(poexp);
+			List<INBindingSetter> 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<INBindingSetter> 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
@@ -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,14 +122,15 @@ public boolean init(QuickCheck qc)
 	}
 
 	@Override
-	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
 	{
 		HashMap<String, ValueList> result = new HashMap<String, ValueList>();
 		long before = System.currentTimeMillis();
 		boolean proved = false;
 
 		if (po.isCheckable)
 		{
+			Context ctxt = Interpreter.getInstance().getInitialContext();
 			long product = 1;
 
 			for (INBindingSetter bind: binds)

diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java
@@ -58,32 +58,23 @@
 import com.fujitsu.vdmj.messages.InternalException;
 import com.fujitsu.vdmj.messages.VDMError;
 import com.fujitsu.vdmj.pog.ProofObligation;
-import com.fujitsu.vdmj.runtime.Context;
 import com.fujitsu.vdmj.runtime.ContextException;
 import com.fujitsu.vdmj.runtime.Interpreter;
 import com.fujitsu.vdmj.runtime.RootContext;
 import com.fujitsu.vdmj.syntax.BindReader;
 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.expressions.TCExpressionList;
-import com.fujitsu.vdmj.tc.lex.TCNameToken;
 import com.fujitsu.vdmj.tc.patterns.TCMultipleBind;
 import com.fujitsu.vdmj.tc.patterns.TCMultipleBindList;
-import com.fujitsu.vdmj.tc.patterns.TCMultipleTypeBind;
 import com.fujitsu.vdmj.tc.types.TCFunctionType;
 import com.fujitsu.vdmj.tc.types.TCNamedType;
-import com.fujitsu.vdmj.tc.types.TCParameterType;
 import com.fujitsu.vdmj.tc.types.TCSetType;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.tc.types.TCTypeList;
-import com.fujitsu.vdmj.tc.types.visitors.TCParameterCollector;
 import com.fujitsu.vdmj.typechecker.Environment;
-import com.fujitsu.vdmj.typechecker.FlatEnvironment;
 import com.fujitsu.vdmj.typechecker.NameScope;
 import com.fujitsu.vdmj.typechecker.TypeCheckException;
 import com.fujitsu.vdmj.typechecker.TypeChecker;
@@ -235,43 +226,18 @@ private Map<String, ValueList> readRangeFile(String filename)
 			for (int i=0; i<tcbinds.size(); i++)
 			{
 				TCMultipleBind mb = tcbinds.get(i);
-				Environment penv = env;
-
-				if (mb instanceof TCMultipleTypeBind)
-				{
-					TCMultipleTypeBind mtb = (TCMultipleTypeBind)mb;
-		    		List<String> 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<INBindingSetter> binds, Context ctxt)
+	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
 	{
 		Map<String, ValueList> values = new HashMap<String, ValueList>();
 		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
@@ -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<INBindingSetter> binds, Context ctxt);
+	abstract public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> 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
@@ -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<INBindingSetter> binds, Context ctxt)
+	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
 	{
 		HashMap<String, ValueList> result = new HashMap<String, ValueList>();
 		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
@@ -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<INBindingSetter> binds, Context ctxt)
+	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
 	{
 		HashMap<String, ValueList> result = new HashMap<String, ValueList>();
 		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
@@ -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
@@ -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
@@ -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<INBindingSetter> binds, Context ctxt)
+	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds)
 	{
 		Map<String, ValueList> values = new HashMap<String, ValueList>();
 		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
@@ -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
 		}