Merge remote-tracking branch 'origin/ordering'

Conflicts:
	FJ-VDMJ4/documentation/MESSAGES
	FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/tc/definitions/TCTypeDefinition.java
	FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/tc/expressions/TCBinaryExpression.java
	FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/tc/expressions/TCEqualsExpression.java

FJ-VDMJ4/documentation/MESSAGES

@@ -44,6 +44,7 @@ as the expected and actual values.
 0067, "Exported type <name> not structured"
 0068, "Periodic threads overlapping"
 
+
 1000, "Malformed quoted character"
 1001, "Invalid char <ch> in base <n> number"
 1002, "Expecting '|->'"
@@ -57,6 +58,7 @@ as the expected and actual values.
 1010, "Expecting <digits>[.<digits>][e<+-><digits>]"
 1011, "Unterminated block comment"
 
+
 2000, "Expecting 'in set' or 'in seq' after pattern in set binding"
 2001, "Expecting 'in set' or 'in seq' in set bind"
 2002, "Expecting ':' in type bind"
@@ -379,6 +381,10 @@ as the expected and actual values.
 2328, "Sequence binds are not available in classic"
 2329, "Duplicate <keyword> keyword"
 2330, "Tokens found after expression at <token>"
+2331, "Expecting inv, eq or ord clause"
+2332, "Duplicate inv clause"
+2333, "Type eq/ord clauses not available in classic"
+
 
 3000, "Expression does not match declared type"
 3001, "Class inherits thread definition from multiple supertypes"
@@ -519,8 +525,8 @@ as the expected and actual values.
 3136, "Left and right of '<>' different types"
 3137, "Not expression is not a boolean"
 3138, "Argument of 'not in set' is not a set"
-3139, "Left hand of <operator> is not numeric"
-3140, "Right hand of <operator> is not numeric"
+3139, "Left hand of <operator> is not ordered"
+3140, "Right hand of <operator> is not ordered"
 3141, "Right hand of '++' is not a map"
 3142, "Right hand of '++' is not a map"
 3143, "Domain of right hand of '++' must be nat1"
@@ -535,7 +541,7 @@ as the expected and actual values.
 3152, "Right of ':>' is not a set"
 3153, "Restriction of map should be set of <type>"
 3154, "<name> not in scope"
-3155, "List comprehension must define one numeric bind variable"
+3155, "List comprehension must define one ordered bind variable"
 3156, "Predicate is not boolean"
 3157, "Left hand of '^' is not a sequence"
 3158, "Right hand of '^' is not a sequence"
@@ -738,6 +744,7 @@ as the expected and actual values.
 3354, "Function argument must be instantiated"
 3355, "Cyclic dependency detected"
 
+
 4000, "Cannot instantiate abstract class <class>"
 4002, "Expression value is not in set|seq bind"
 4003, "Value <value> cannot be applied"
@@ -905,6 +912,7 @@ as the expected and actual values.
 4169, "Arithmetic overflow"
 4170, "Cannot convert empty set to set1"
 4171, "Cannot convert <function> to <function>"
+4172, "Values cannot be compared: <first>, <second>"
 
 
 5000, "Definition <name> not used"
@@ -925,3 +933,7 @@ as the expected and actual values.
 5015, "LaTeX source should start with %comment, \document, \section or \subsection"
 5016, "Some statements will not be reached"
 5017, "Pure operation call may not be referentially transparent"
+5018, "Field has ':-' for type with eq definition"
+5019, "Order of union member <name> will be overridden"
+5020, "Equality of union member <name> will be overridden"
+5021, "Multiple union members define eq clauses, <types>"

FJ-VDMJ4/pom.xml

@@ -4,7 +4,7 @@
 	<groupId>com.fujitsu</groupId>
 	<artifactId>vdmj</artifactId>
 	<name>VDMJ</name>
-	<version>4.0.0</version>
+	<version>4.1.0</version>
 
 	<properties>
 		<maven.build.timestamp.format>yyMMdd</maven.build.timestamp.format>

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/ast/definitions/ASTTypeDefinition.java

@@ -37,15 +37,30 @@ public class ASTTypeDefinition extends ASTDefinition
 	public final ASTInvariantType type;
 	public final ASTPattern invPattern;
 	public final ASTExpression invExpression;
+	public final ASTPattern eqPattern1;
+	public final ASTPattern eqPattern2;
+	public final ASTExpression eqExpression;
+	public final ASTPattern ordPattern1;
+	public final ASTPattern ordPattern2;
+	public final ASTExpression ordExpression;
 
 	public ASTTypeDefinition(LexNameToken name, ASTInvariantType type, ASTPattern invPattern,
-		ASTExpression invExpression)
+		ASTExpression invExpression, ASTPattern eqPattern1, ASTPattern eqPattern2, ASTExpression eqExpression,
+		ASTPattern ordPattern1, ASTPattern ordPattern2, ASTExpression ordExpression)
 	{
 		super(name.location, name);
 
 		this.type = type;
 		this.invPattern = invPattern;
 		this.invExpression = invExpression;
+
+		this.eqPattern1 = eqPattern1;
+		this.eqPattern2 = eqPattern2;
+		this.eqExpression = eqExpression;
+
+		this.ordPattern1 = ordPattern1;
+		this.ordPattern2 = ordPattern2;
+		this.ordExpression = ordExpression;
 	}
 
 	@Override
@@ -54,7 +69,11 @@ public String toString()
 		return accessSpecifier.ifSet(" ") +
 				name.name + " = " + type.toDetailedString() +
 				(invPattern == null ? "" :
-					"\n\tinv " + invPattern + " == " + invExpression);
+					"\n\tinv " + invPattern + " == " + invExpression) +
+        		(eqPattern1 == null ? "" :
+        			"\n\teq " + eqPattern1 + " = " + eqPattern2 + " == " + eqExpression) +
+        		(ordPattern1 == null ? "" :
+        			"\n\tord " + ordPattern1 + " < " + ordPattern2 + " == " + ordExpression);
 	}
 
 	@Override

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/definitions/INTypeDefinition.java

@@ -43,17 +43,27 @@ public class INTypeDefinition extends INDefinition
 	public final INPattern invPattern;
 	public final INExpression invExpression;
 	public final INExplicitFunctionDefinition invdef;
+	public final INExplicitFunctionDefinition eqdef;
+	public final INExplicitFunctionDefinition orddef;
+	public final INExplicitFunctionDefinition mindef;
+	public final INExplicitFunctionDefinition maxdef;
 
 	public INTypeDefinition(INAccessSpecifier accessSpecifier, TCNameToken name,
 			TCInvariantType type, INPattern invPattern, INExpression invExpression,
-			INExplicitFunctionDefinition invdef)
+			INExplicitFunctionDefinition invdef, INExplicitFunctionDefinition eqdef,
+			INExplicitFunctionDefinition orddef, INExplicitFunctionDefinition mindef,
+			INExplicitFunctionDefinition maxdef)
 	{
 		super(name.getLocation(), accessSpecifier, name);
 
 		this.type = type;
 		this.invPattern = invPattern;
 		this.invExpression = invExpression;
 		this.invdef = invdef;
+		this.eqdef = eqdef;
+		this.orddef = orddef;
+		this.mindef = mindef;
+		this.maxdef = maxdef;
 	}
 
 	@Override
@@ -77,6 +87,26 @@ public INDefinition findName(TCNameToken sought)
 			return invdef;
 		}
 
+		if (eqdef != null && eqdef.findName(sought) != null)
+		{
+			return eqdef;
+		}
+
+		if (orddef != null && orddef.findName(sought) != null)
+		{
+			return orddef;
+		}
+
+		if (mindef != null && mindef.findName(sought) != null)
+		{
+			return mindef;
+		}
+
+		if (maxdef != null && maxdef.findName(sought) != null)
+		{
+			return maxdef;
+		}
+
 		return null;
 	}
 
@@ -89,6 +119,30 @@ public INExpression findExpression(int lineno)
 			if (found != null) return found;
 		}
 
+		if (eqdef != null)
+		{
+			INExpression found = eqdef.findExpression(lineno);
+			if (found != null) return found;
+		}
+
+		if (orddef != null)
+		{
+			INExpression found = orddef.findExpression(lineno);
+			if (found != null) return found;
+		}
+
+		if (mindef != null)
+		{
+			INExpression found = mindef.findExpression(lineno);
+			if (found != null) return found;
+		}
+
+		if (maxdef != null)
+		{
+			INExpression found = maxdef.findExpression(lineno);
+			if (found != null) return found;
+		}
+
 		return null;
 	}
 
@@ -103,6 +157,30 @@ public NameValuePairList getNamedValues(Context ctxt)
 			nvl.add(new NameValuePair(invdef.name, invfunc));
 		}
 
+		if (eqdef != null)
+		{
+			FunctionValue eqfunc =	new FunctionValue(eqdef, null, null, ctxt);
+			nvl.add(new NameValuePair(eqdef.name, eqfunc));
+		}
+
+		if (orddef != null)
+		{
+			FunctionValue ordfunc =	new FunctionValue(orddef, null, null, ctxt);
+			nvl.add(new NameValuePair(orddef.name, ordfunc));
+		}
+
+		if (mindef != null)
+		{
+			FunctionValue minfunc =	new FunctionValue(mindef, null, null, ctxt);
+			nvl.add(new NameValuePair(mindef.name, minfunc));
+		}
+
+		if (maxdef != null)
+		{
+			FunctionValue maxfunc =	new FunctionValue(maxdef, null, null, ctxt);
+			nvl.add(new NameValuePair(maxdef.name, maxfunc));
+		}
+
 		return nvl;
 	}
 

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/expressions/INGreaterEqualExpression.java

@@ -25,7 +25,6 @@
 
 import com.fujitsu.vdmj.ast.lex.LexToken;
 import com.fujitsu.vdmj.runtime.Context;
-import com.fujitsu.vdmj.runtime.ValueException;
 import com.fujitsu.vdmj.values.BooleanValue;
 import com.fujitsu.vdmj.values.Value;
 
@@ -47,13 +46,16 @@ public Value eval(Context ctxt)
 		Value lv = left.eval(ctxt);
 		Value rv = right.eval(ctxt);
 
-		try
+		if (lv.isOrdered() && rv.isOrdered())
 		{
-			return new BooleanValue(lv.realValue(ctxt) >= rv.realValue(ctxt));
-        }
-        catch (ValueException e)
-        {
-        	return abort(e);
-        }
+			int cmp = lv.compareTo(rv);
+
+			if (cmp != Integer.MIN_VALUE)	// Indicates comparable
+			{
+				return new BooleanValue(cmp >= 0);
+			}
+		}
+
+		return abort(4172, "Values cannot be compared: " + lv + ", " + rv, ctxt);
 	}
 }

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/expressions/INGreaterExpression.java

@@ -25,7 +25,6 @@
 
 import com.fujitsu.vdmj.ast.lex.LexToken;
 import com.fujitsu.vdmj.runtime.Context;
-import com.fujitsu.vdmj.runtime.ValueException;
 import com.fujitsu.vdmj.values.BooleanValue;
 import com.fujitsu.vdmj.values.Value;
 
@@ -47,13 +46,16 @@ public Value eval(Context ctxt)
 		Value lv = left.eval(ctxt);
 		Value rv = right.eval(ctxt);
 
-		try
+		if (lv.isOrdered() && rv.isOrdered())
 		{
-			return new BooleanValue(lv.realValue(ctxt) > rv.realValue(ctxt));
-        }
-        catch (ValueException e)
-        {
-        	return abort(e);
-        }
+			int cmp = lv.compareTo(rv);
+
+			if (cmp != Integer.MIN_VALUE)	// Indicates comparable
+			{
+				return new BooleanValue(cmp > 0);
+			}
+		}
+
+		return abort(4172, "Values cannot be compared: " + lv + ", " + rv, ctxt);
 	}
 }

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/expressions/INLessEqualExpression.java

@@ -25,7 +25,6 @@
 
 import com.fujitsu.vdmj.ast.lex.LexToken;
 import com.fujitsu.vdmj.runtime.Context;
-import com.fujitsu.vdmj.runtime.ValueException;
 import com.fujitsu.vdmj.values.BooleanValue;
 import com.fujitsu.vdmj.values.Value;
 
@@ -47,13 +46,16 @@ public Value eval(Context ctxt)
 		Value lv = left.eval(ctxt);
 		Value rv = right.eval(ctxt);
 
-		try
+		if (lv.isOrdered() && rv.isOrdered())
 		{
-			return new BooleanValue(lv.realValue(ctxt) <= rv.realValue(ctxt));
+			int cmp = lv.compareTo(rv);
+
+			if (cmp != Integer.MIN_VALUE)	// Indicates comparable
+			{
+				return new BooleanValue(cmp <= 0);
+			}
 		}
-        catch (ValueException e)
-        {
-        	return abort(e);
-        }
+
+		return abort(4172, "Values cannot be compared: " + lv + ", " + rv, ctxt);
 	}
 }

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/expressions/INLessExpression.java

@@ -25,7 +25,6 @@
 
 import com.fujitsu.vdmj.ast.lex.LexToken;
 import com.fujitsu.vdmj.runtime.Context;
-import com.fujitsu.vdmj.runtime.ValueException;
 import com.fujitsu.vdmj.values.BooleanValue;
 import com.fujitsu.vdmj.values.Value;
 
@@ -46,14 +45,17 @@ public Value eval(Context ctxt)
 
 		Value lv = left.eval(ctxt);
 		Value rv = right.eval(ctxt);
-
-		try
+		
+		if (lv.isOrdered() && rv.isOrdered())
 		{
-			return new BooleanValue(lv.realValue(ctxt) < rv.realValue(ctxt));
+			int cmp = lv.compareTo(rv);
+
+			if (cmp != Integer.MIN_VALUE)	// Indicates comparable
+			{
+				return new BooleanValue(cmp < 0);
+			}
 		}
-        catch (ValueException e)
-        {
-        	return abort(e);
-        }
+
+		return abort(4172, "Values cannot be compared: " + lv + ", " + rv, ctxt);
 	}
 }

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/expressions/INSeqCompExpression.java

@@ -102,9 +102,9 @@ private Value evalSetBind(ValueList allValues, Context ctxt)
 
 				if (map.get(sortOn) == null)
 				{
-    				if (nvpl.size() != 1 || !sortOn.isNumeric())
+    				if (nvpl.size() != 1 || !sortOn.isOrdered())
     				{
-    					abort(4029, "Sequence comprehension bindings must be one numeric value", ctxt);
+    					abort(4029, "Sequence comprehension bindings must be one ordered value", ctxt);
     				}
 
     				evalContext.putList(nvpl);

FJ-VDMJ4/src/main/java/com/fujitsu/vdmj/in/expressions/INSetCompExpression.java

@@ -117,13 +117,13 @@ public Value eval(Context ctxt)
 					set.add(first.eval(evalContext));
 				}
 			}
+
+			return new SetValue(set);
 		}
 		catch (ValueException e)
 		{
 			return abort(e);
 		}
-
-		return new SetValue(set);
 	}
 
 	@Override