Fixes for @Quickcheck object creation

nickbattle · Jan 5, 2024 · d63e79c · d63e79c
1 parent 4e4cbe0
commit d63e79c
Show file tree

Hide file tree

Showing 4 changed files with 39 additions and 20 deletions.
diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java
@@ -25,6 +25,8 @@
 package quickcheck;
 
 import static com.fujitsu.vdmj.plugins.PluginConsole.errorln;
+import static com.fujitsu.vdmj.plugins.PluginConsole.infof;
+import static com.fujitsu.vdmj.plugins.PluginConsole.infoln;
 import static com.fujitsu.vdmj.plugins.PluginConsole.println;
 import static quickcheck.commands.QCConsole.infof;
 import static quickcheck.commands.QCConsole.infoln;
@@ -45,8 +47,8 @@
 import com.fujitsu.vdmj.in.definitions.INClassDefinition;
 import com.fujitsu.vdmj.in.expressions.INBooleanLiteralExpression;
 import com.fujitsu.vdmj.in.expressions.INExpression;
-import com.fujitsu.vdmj.in.patterns.INBindingOverride;
 import com.fujitsu.vdmj.in.patterns.INBindingGlobals;
+import com.fujitsu.vdmj.in.patterns.INBindingOverride;
 import com.fujitsu.vdmj.lex.Dialect;
 import com.fujitsu.vdmj.mapper.ClassMapper;
 import com.fujitsu.vdmj.po.annotations.POAnnotation;
@@ -71,8 +73,8 @@
 import com.fujitsu.vdmj.values.Value;
 import com.fujitsu.vdmj.values.ValueList;
 
-import quickcheck.annotations.po.POQuickCheckAnnotation;
 import quickcheck.annotations.IterableContext;
+import quickcheck.annotations.po.POQuickCheckAnnotation;
 import quickcheck.strategies.FixedQCStrategy;
 import quickcheck.strategies.QCStrategy;
 import quickcheck.strategies.StrategyResults;
@@ -751,6 +753,10 @@ private Context addSelf(ProofObligation po, Context ctxt)
 		{
 			try
 			{
+				ClassInterpreter in = ClassInterpreter.getInstance();
+				INClassDefinition classdef = in.getDefaultClass();
+				ObjectValue object = null;
+
 				if (po.annotations != null)
 				{
 					for (POAnnotation a: po.annotations)
@@ -759,29 +765,39 @@ private Context addSelf(ProofObligation po, Context ctxt)
 						{
 							POQuickCheckAnnotation qca = (POQuickCheckAnnotation)a;
 
-							if (qca.qcConstructor != null)
+							if (qca.tc != null)
 							{
-								// create object and return it... how?
+								if (qca.newexp == null)		// cached
+								{
+									qca.newexp = ClassMapper.getInstance(INNode.MAPPINGS).convert(qca.tc.qcConstructor);
+								}
+
+								object = (ObjectValue) qca.newexp.eval(in.getInitialContext());
 								break;
 							}
 						}
 					}
 				}
 
-				ClassInterpreter in = ClassInterpreter.getInstance();
-				INClassDefinition classdef = in.getDefaultClass();
-				ObjectValue object = classdef.newInstance(null, null, ctxt);
-
-				ctxt = new ObjectContext(
-						classdef.name.getLocation(), classdef.name.getName() + "()",
-						ctxt, object);
-
+				if (object == null)
+				{
+					object = classdef.newInstance(null, null, ctxt);
+
+					ctxt = new ObjectContext(
+							classdef.name.getLocation(), classdef.name.getName() + "()",
+							ctxt, object);
+				}
+
 				ctxt.put(classdef.name.getSelfName(), object);
 			}
 			catch (ValueException e)
 			{
 				// Use ctxt unchanged?
 			}
+			catch (Exception e)
+			{
+				// Problem with "new"?
+			}
 		}
 
 		return ctxt;

diff --git a/quickcheck/src/main/java/quickcheck/annotations/po/POQuickCheckAnnotation.java b/quickcheck/src/main/java/quickcheck/annotations/po/POQuickCheckAnnotation.java
@@ -24,36 +24,39 @@
 
 package quickcheck.annotations.po;
 
+import com.fujitsu.vdmj.in.expressions.INNewExpression;
 import com.fujitsu.vdmj.po.annotations.POAnnotation;
-import com.fujitsu.vdmj.po.expressions.PONewExpression;
 import com.fujitsu.vdmj.tc.lex.TCIdentifierToken;
 import com.fujitsu.vdmj.tc.types.TCParameterType;
 import com.fujitsu.vdmj.tc.types.TCTypeList;
 import com.fujitsu.vdmj.util.Utils;
 
+import quickcheck.annotations.tc.TCQuickCheckAnnotation;
+
 public class POQuickCheckAnnotation extends POAnnotation
 {
 	private static final long serialVersionUID = 1L;
 
 	public final TCParameterType qcParam;
 	public final TCTypeList qcTypes;
-	public final PONewExpression qcConstructor;
+	public final TCQuickCheckAnnotation tc;
+	public INNewExpression newexp;
 
 	public POQuickCheckAnnotation(TCIdentifierToken name,
-		TCParameterType qcParam, TCTypeList qcTypes, PONewExpression qcConstructor)
+		TCParameterType qcParam, TCTypeList qcTypes, TCQuickCheckAnnotation tc)
 	{
 		super(name, null);
 		this.qcParam = qcParam;
 		this.qcTypes = qcTypes;
-		this.qcConstructor = qcConstructor;
+		this.tc = tc;
 	}
 
 	@Override
 	public String toString()
 	{
-		if (qcConstructor != null)
+		if (tc != null)
 		{
-			return "@" + name + " " + qcConstructor + ";";
+			return "@" + name + " " + tc.qcConstructor + ";";
 		}
 		else
 		{

diff --git a/quickcheck/src/main/java/quickcheck/annotations/tc/TCQuickCheckAnnotation.java b/quickcheck/src/main/java/quickcheck/annotations/tc/TCQuickCheckAnnotation.java
@@ -86,7 +86,7 @@ public void tcBefore(TCDefinition def, Environment env, NameScope scope)
 
 	private void checkConstructor(TCDefinition def, Environment env, NameScope scope)
 	{
-		// check?
+		qcConstructor.typeCheck(env, null, scope, null);
 	}
 
 	private void checkTypeParams(TCDefinition def, Environment env, NameScope scope)

diff --git a/quickcheck/src/main/resources/tc-po.mappings b/quickcheck/src/main/resources/tc-po.mappings
@@ -4,5 +4,5 @@
 
 # annotations
 package quickcheck.annotations.tc to quickcheck.annotations.po;
-map TCQuickCheckAnnotation{name, qcParam, qcTypes, qcConstructor} to POQuickCheckAnnotation(name, qcParam, qcTypes, qcConstructor);
+map TCQuickCheckAnnotation{name, qcParam, qcTypes} to POQuickCheckAnnotation(name, qcParam, qcTypes, this);