Merge branch 'master' into highprecision

examples/quickcheck/src/main/java/quickcheck/QuickCheck.java

@@ -466,6 +466,10 @@ else if (results.provedBy != null)
 					{
 						execResult = null;
 					}
+					else if (e.number == 4024)	// 'not yet specified' expression reached
+					{
+						execResult = new BooleanValue(true);	// MAYBE, in effect
+					}
 					else
 					{
 						execResult = new BooleanValue(false);

vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java

@@ -147,9 +147,8 @@ public NameValuePairList getNamedValues(Context ctxt)
 
 		if (measureDef != null && measureDef.name.getName().startsWith("measure_"))
 		{
-			FunctionValue mfunc = new FunctionValue(measureDef, null, null, null);
-			mfunc.uninstantiated = (typeParams != null);
-			nvl.add(new NameValuePair(measureDef.name, mfunc));
+			// Add implicit measure_* functions and any pre_measure_*s too.
+			nvl.addAll(measureDef.getNamedValues(ctxt));
 		}
 
 		return nvl;

vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java

@@ -159,7 +159,8 @@ public NameValuePairList getNamedValues(Context ctxt)
 
 		if (measureDef != null && measureDef.name.getName().startsWith("measure_"))
 		{
-			nvl.add(new NameValuePair(measureDef.name, new FunctionValue(measureDef, null, null, null)));
+			// Add implicit measure_* functions and any pre_measure_*s too.
+			nvl.addAll(measureDef.getNamedValues(ctxt));
 		}
 
 		return nvl;

vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java

@@ -161,6 +161,15 @@ public final POPattern removeIgnorePatterns()
 		return apply(new PORemoveIgnoresVisitor(), null);
 	}
 
+	/**
+	 * Indicates that the pattern is associated with a maximal type, which may
+	 * affect the string representation - eg. mk_R!(...).
+	 */
+	public void setMaximal(boolean maximal)
+	{
+		return;		// Only used in PORecordPattern
+	}
+
 	/**
 	 * Implemented by all patterns to allow visitor processing.
 	 */

vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/PORecordPattern.java

@@ -35,6 +35,7 @@ public class PORecordPattern extends POPattern
 	public final TCNameToken typename;
 	public final POPatternList plist;
 	public final TCType type;
+	private boolean maximal = false;
 
 	public PORecordPattern(TCNameToken typename, POPatternList list, TCType type)
 	{
@@ -47,7 +48,7 @@ public PORecordPattern(TCNameToken typename, POPatternList list, TCType type)
 	@Override
 	public String toString()
 	{
-		return "mk_" + type.toExplicitString(location) + "(" + Utils.listToString(plist) + ")";
+		return "mk_" + type.toExplicitString(location) + (maximal ? "!(" : "(") + Utils.listToString(plist) + ")";
 	}
 
 	@Override
@@ -61,6 +62,12 @@ public boolean alwaysMatches()
 	{
 		return plist.alwaysMatches();
 	}
+
+	@Override
+	public void setMaximal(boolean maximal)
+	{
+		this.maximal = maximal;
+	}
 
 	@Override
 	public <R, S> R apply(POPatternVisitor<R, S> visitor, S arg)

vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java

@@ -120,6 +120,18 @@ public String toString()
 
 		return sb.toString();
 	}
+
+	@Override
+	public boolean equals(Object other)
+	{
+		if (other instanceof ProofObligation)
+		{
+			ProofObligation opo = (ProofObligation)other;
+			return kind == opo.kind && location == opo.location;
+		}
+
+		return false; 
+	}
 
 	protected String getVar(String root)
 	{

vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java

@@ -24,6 +24,7 @@
 
 package com.fujitsu.vdmj.pog;
 
+import java.util.Collection;
 import java.util.Iterator;
 import java.util.List;
 import java.util.Vector;
@@ -55,6 +56,30 @@
 public class ProofObligationList extends Vector<ProofObligation>
 {
 	// Convenience class to hold lists of POs.
+
+	@Override
+	public synchronized boolean add(ProofObligation e)
+	{
+		if (!this.contains(e))		// Eliminate duplicates
+		{
+			return super.add(e);
+		}
+
+		return false;
+	}
+
+	@Override
+	public synchronized boolean addAll(Collection<? extends ProofObligation> poList)
+	{
+		boolean changed = false;
+
+		for (ProofObligation po: poList)
+		{
+			changed = this.add(po) || changed;
+		}
+
+		return changed;
+	}
 
 	@Override
 	public String toString()

vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java

@@ -75,11 +75,16 @@ private String getContext(String name, POExplicitFunctionDefinition def)
 
     		for (POPatternList pl: def.paramPatternList)
     		{
+    			int param = 0;
+
     			for (POPattern p: pl)
     			{
     				fapply.append(sep);
-    				fapply.append(p.removeIgnorePatterns());
+    				POPattern p2 = p.removeIgnorePatterns();
+   					p2.setMaximal(ftype.parameters.get(param).isMaximal());
+    				fapply.append(p2);
 					sep = ", ";
+					param++;
     			}
 
     			if (ftype.result instanceof TCFunctionType)

vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java

@@ -396,14 +396,17 @@ private void setMeasureExp(Environment base, Environment local, NameScope scope)
 		TCPatternListList cpll = new TCPatternListList();
 		cpll.add(all);
 
+		// Note that the measure_f has the precondition of the function it measures.
+
 		TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, accessSpecifier, measureName,
-				typeParams, type.getMeasureType(isCurried, actual), cpll, measureExp, null, null, false, null);
+				typeParams, type.getMeasureType(isCurried, actual), cpll, measureExp, precondition, null, false, null);
 
 		def.classDefinition = classDefinition;
+		def.implicitDefinitions(base);
 		def.typeResolve(base);
+		def.typeCheck(base, scope);
+
 		measureDef = def;
-
-		measureDef.typeCheck(base, scope);
 	}
 
 	/**
@@ -620,9 +623,9 @@ public TCDefinition findName(TCNameToken sought, NameScope scope)
 			return postdef;
 		}
 
-		if (measureDef != null && measureDef.findName(sought, scope) != null)
+		if (measureDef != null)
 		{
-			return measureDef;
+			return measureDef.findName(sought, scope);	// eg. pre_measure_f
 		}
 
 		return null;

vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java

@@ -380,12 +380,14 @@ private void setMeasureExp(Environment base, Environment local, NameScope scope)
 		measureName = name.getMeasureName(measureExp.location);
 		checkMeasure(measureName, actual);
 
+		// Note that the measure_f has the precondition of the function it measures.
+
 		TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, accessSpecifier, measureName,
-				typeParams, type.getMeasureType(false, actual), getParamPatternList(), measureExp, null, null, false, null);
+				typeParams, type.getMeasureType(false, actual), getParamPatternList(), measureExp, precondition, null, false, null);
 
 		def.classDefinition = classDefinition;
+		def.implicitDefinitions(base);
 		def.typeResolve(base);
-
 		def.typeCheck(base, scope);
 
 		measureDef = def;