Remove use of deprecated Applicable interface (#93)

Signed-off-by: Calvin Loncaric <[email protected]>

build.xml

@@ -31,6 +31,7 @@
 		<javac srcdir="${src}" destdir="${build}/modules" classpath="${tlc}/tla2tools.jar:${lib}/gson-2.8.6.jar:${lib}/jgrapht-core-1.5.1.jar:${lib}/jungrapht-layout-1.4-SNAPSHOT.jar:${lib}/slf4j-api-1.7.30.jar:${lib}/slf4j-nop-1.7.30.jar:${lib}/commons-lang3-3.12.0.jar:${lib}/commons-math3-3.6.1.jar"
            source="1.8"
            target="1.8"
+           deprecation="true"
            includeantruntime="false"/>
 	</target>
 

modules/tlc2/overrides/BagsExt.java

@@ -1,5 +1,6 @@
 /*******************************************************************************
  * Copyright (c) 2022 Inria. All rights reserved. 
+ * Copyright (c) 2023, Oracle and/or its affiliates.
  *
  * The MIT License (MIT)
  * 
@@ -64,7 +65,7 @@ public static Value foldBag(final OpValue op, final Value base, final Value bag)
 									+ Values.ppr(domain[i].toString()) + ":>" + Values.ppr(values[i].toString()) + ")" });
 			}
 			for (int j = 0; j < ((IntValue) values[i]).val; j++) {
-				acc[0] = op.apply(acc, EvalControl.Clear);
+				acc[0] = op.eval(acc, EvalControl.Clear);
 			}
 		}
 

modules/tlc2/overrides/FiniteSetsExt.java

@@ -1,5 +1,6 @@
 /*******************************************************************************
  * Copyright (c) 2020 Microsoft Research. All rights reserved. 
+ * Copyright (c) 2023, Oracle and/or its affiliates.
  *
  * The MIT License (MIT)
  * 
@@ -30,7 +31,6 @@
 import tlc2.tool.EvalException;
 import tlc2.value.IBoolValue;
 import tlc2.value.Values;
-import tlc2.value.impl.Applicable;
 import tlc2.value.impl.BoolValue;
 import tlc2.value.impl.Enumerable;
 import tlc2.value.impl.EnumerableValue;
@@ -49,25 +49,19 @@ private FiniteSetsExt() {
 	}
 
 	@TLAPlusOperator(identifier = "Quantify", module = "FiniteSetsExt", warn = false)
-	public static Value quantify(final Value set, final Value pred) {
+	public static Value quantify(final Value set, final OpValue test) {
 		if (!(set instanceof EnumerableValue)) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "first", "Quantify", "set", Values.ppr(set.toString()) });
 		}
-		if (!(pred instanceof Applicable)) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "second", "Quantify", "boolean-valued operator", Values.ppr(pred.toString()) });
-		}
-
 
 		int size = 0;
-		final Applicable test = (Applicable) pred;
 		final ValueEnumeration enumSet = ((SetEnumValue) set.toSetEnum()).elements();
         Value elem;
         final Value[] args = new Value[1];
 		while ((elem = enumSet.nextElement()) != null) {
 			args[0] = elem;
-			Value val = test.apply(args, EvalControl.Clear);
+			Value val = test.eval(args, EvalControl.Clear);
 			if (val instanceof IBoolValue) {
 				if (((BoolValue) val).val) {
 					size++;
@@ -112,10 +106,10 @@ public static Value foldSet(final OpValue op, final Value base, final Enumerable
 
 		final ValueEnumeration ve = set.elements();
 
-		Value v = null;
+		Value v;
 		while ((v = ve.nextElement()) != null) {
 			args[0] = v;
-			args[1] = op.apply(args, EvalControl.Clear);
+			args[1] = op.eval(args, EvalControl.Clear);
 		}
 
 		return args[1];

modules/tlc2/overrides/Functions.java

@@ -1,5 +1,6 @@
 /*******************************************************************************
  * Copyright (c) 2019 Microsoft Research. All rights reserved. 
+ * Copyright (c) 2023, Oracle and/or its affiliates.
  *
  * The MIT License (MIT)
  * 
@@ -31,10 +32,10 @@
 import tlc2.tool.EvalControl;
 import tlc2.tool.EvalException;
 import tlc2.value.Values;
-import tlc2.value.impl.Applicable;
 import tlc2.value.impl.BoolValue;
 import tlc2.value.impl.Enumerable;
 import tlc2.value.impl.FcnRcdValue;
+import tlc2.value.impl.FunctionValue;
 import tlc2.value.impl.OpValue;
 import tlc2.value.impl.SetOfRcdsValue;
 import tlc2.value.impl.TupleValue;
@@ -123,23 +124,23 @@ public static Value foldFunction(final OpValue op, final Value base, final Value
 		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
 		// make sure that the first parameter is a binary operator.
 
-		if (!(fun instanceof Applicable)) {
+		if (!(fun instanceof FunctionValue)) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "third", "FoldFunction", "function", Values.ppr(fun.toString()) });
 		}
-		return foldFunctionOnSet(op, base, fun, ((Applicable) fun).getDomain());
+		return foldFunctionOnSet(op, base, fun, ((FunctionValue) fun).getDomain());
 	}
 
 	@TLAPlusOperator(identifier = "FoldFunctionOnSet", module = "Functions", warn = false)
 	public static Value foldFunctionOnSet(final OpValue op, final Value base, final Value v3, final Value v4) {
 		// Can assume type of OpValue because tla2sany.semantic.Generator.java will
 		// make sure that the first parameter is a binary operator.
 
-		if (!(v3 instanceof Applicable)) {
+		if (!(v3 instanceof FunctionValue)) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "third", "FoldFunctionOnSet", "function", Values.ppr(v3.toString()) });
 		}
-		final Applicable fun = (Applicable) v3;
+		final FunctionValue fun = (FunctionValue) v3;
 		if (!(v4 instanceof Enumerable)) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "fourth", "FoldFunctionOnSet", "set", Values.ppr(v4.toString()) });
@@ -152,10 +153,10 @@ public static Value foldFunctionOnSet(final OpValue op, final Value base, final
 
 		final ValueEnumeration ve = subdomain.elements();
 
-		Value v = null;
+		Value v;
 		while ((v = ve.nextElement()) != null) {
-			args[0] = fun.select(v);
-			args[1] = op.apply(args, EvalControl.Clear);
+			args[0] = fun.apply(v, EvalControl.Clear);
+			args[1] = op.eval(args, EvalControl.Clear);
 		}
 
 		return args[1];

modules/tlc2/overrides/GraphViz.java

@@ -1,5 +1,6 @@
 /*******************************************************************************
  * Copyright (c) 2023 Microsoft Research. All rights reserved.
+ * Copyright (c) 2023, Oracle and/or its affiliates.
  *
  * The MIT License (MIT)
  *
@@ -27,7 +28,7 @@
 
 import tlc2.tool.EvalControl;
 import tlc2.util.FP64;
-import tlc2.value.impl.Applicable;
+import tlc2.value.impl.OpValue;
 import tlc2.value.impl.RecordValue;
 import tlc2.value.impl.SetEnumValue;
 import tlc2.value.impl.StringValue;
@@ -38,24 +39,12 @@
 public class GraphViz {
 
 	@TLAPlusOperator(identifier = "DotDiGraph", module = "GraphViz", warn = false)
-	public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) throws Exception {
+	public static Value dotDiGraph(final Value v1, final OpValue vl, final OpValue el) throws Exception {
 		if (!(v1 instanceof RecordValue) || v1.toRcd() == null) {
 			throw new Exception("An DiGraph must be a record. Value given is of type: " + v1.getClass().getName());
 		}
 		final RecordValue g = (RecordValue) v1.toRcd();
 
-		if (!(v2 instanceof Applicable)) {
-			throw new Exception(
-					"Second parameter must be an Applicable. Value given is of type: " + v2.getClass().getName());
-		}
-		final Applicable vl = (Applicable) v2;
-
-		if (!(v3 instanceof Applicable)) {
-			throw new Exception(
-					"Third parameter must be an Applicable. Value given is of type: " + v2.getClass().getName());
-		}
-		final Applicable el = (Applicable) v3;
-
 		String dotString = "digraph MyGraph {";
 
 		// Nodes
@@ -65,7 +54,7 @@ public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) t
 		Value val = null;
 		while ((val = elements.nextElement()) != null) {
 			dotString += String.format("%s[label=%s];", val.fingerPrint(FP64.New()),
-					vl.apply(new Value[] { val }, EvalControl.Clear));
+					vl.eval(new Value[] { val }, EvalControl.Clear));
 		}
 
 		// Edges
@@ -75,7 +64,7 @@ public static Value dotDiGraph(final Value v1, final Value v2, final Value v3) t
 		while ((val = elements.nextElement()) != null) {
 			TupleValue tv = (TupleValue) val.toTuple();
 			dotString += String.format("%s->%s[label=%s];", tv.elems[0].fingerPrint(FP64.New()),
-					tv.elems[1].fingerPrint(FP64.New()), el.apply(new Value[] { tv }, EvalControl.Clear));
+					tv.elems[1].fingerPrint(FP64.New()), el.eval(new Value[] { tv }, EvalControl.Clear));
 		}
 
 		dotString += "}";

modules/tlc2/overrides/SequencesExt.java

@@ -1,6 +1,7 @@
 package tlc2.overrides;
 /*******************************************************************************
  * Copyright (c) 2019 Microsoft Research. All rights reserved. 
+ * Copyright (c) 2023, Oracle and/or its affiliates.
  *
  * The MIT License (MIT)
  * 
@@ -40,7 +41,6 @@
 import tlc2.value.IBoolValue;
 import tlc2.value.IValue;
 import tlc2.value.Values;
-import tlc2.value.impl.Applicable;
 import tlc2.value.impl.BoolValue;
 import tlc2.value.impl.FcnRcdValue;
 import tlc2.value.impl.IntValue;
@@ -275,7 +275,7 @@ public static Value foldLeft(final OpValue op, final Value base, final Value val
 		final Value[] elems = tv.elems;
 		for (int i = 0; i < elems.length; i++) {
 			args[1] = elems[i];
-			args[0] = op.apply(args, EvalControl.Clear);
+			args[0] = op.eval(args, EvalControl.Clear);
 		}
 
 		return args[0];
@@ -299,7 +299,7 @@ public static Value foldRight(final OpValue op, final Value val, final Value bas
 		final Value[] elems = tv.elems;
 		for (int i = elems.length - 1; i >= 0; i--) {
 			args[0] = elems[i];
-			args[1] = op.apply(args, EvalControl.Clear);
+			args[1] = op.eval(args, EvalControl.Clear);
 		}
 
 		return args[1];
@@ -381,25 +381,20 @@ public static Value isPrefix(final Value v1, final Value v2) {
 	}
 
 	@TLAPlusOperator(identifier = "SelectInSeq", module = "SequencesExt", warn = false)
-	public static Value selectInSeq(final Value s, final Value test) {
+	public static Value selectInSeq(final Value s, final OpValue test) {
 		final TupleValue seq = (TupleValue) s.toTuple();
 		if (seq == null) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "first", "SelectInSeq", "sequence", Values.ppr(s.toString()) });
 		}
-		if (!(test instanceof Applicable)) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "third", "SelectInSeq", "function", Values.ppr(test.toString()) });
-		}
 		final int len = seq.size();
-		final Applicable ftest = (Applicable) test;
 		final Value[] args = new Value[1];
 		for (int i = 0; i < len; i++) {
 			args[0] = seq.elems[i];
-			final Value val = ftest.apply(args, EvalControl.Clear);
+			final Value val = test.eval(args, EvalControl.Clear);
 			if (!(val instanceof IBoolValue)) {
 				throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "SelectInSeq",
-						"boolean-valued function", Values.ppr(test.toString()) });
+						"boolean-valued operator", Values.ppr(test.toString()) });
 			}
 			if (((BoolValue) val).val) {
 				return IntValue.gen(i + 1);
@@ -409,7 +404,7 @@ public static Value selectInSeq(final Value s, final Value test) {
 	}
 
 	@TLAPlusOperator(identifier = "SelectInSubSeq", module = "SequencesExt", warn = false)
-	public static Value SelectInSubSeq(final Value s, final Value f, final Value t, final Value test) {
+	public static Value SelectInSubSeq(final Value s, final Value f, final Value t, final OpValue test) {
 		final TupleValue seq = (TupleValue) s.toTuple();
 		if (seq == null) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
@@ -423,10 +418,6 @@ public static Value SelectInSubSeq(final Value s, final Value f, final Value t,
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "third", "SelectInSubSeq", "natural", Values.ppr(t.toString()) });
 		}
-		if (!(test instanceof Applicable)) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "fourth", "SelectInSubSeq", "function", Values.ppr(test.toString()) });
-		}
 
 		int from = ((IntValue) f).val;
 		final int to = ((IntValue) t).val;
@@ -442,15 +433,14 @@ public static Value SelectInSubSeq(final Value s, final Value f, final Value t,
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_NOT_IN_DOMAIN,
 					new String[] { "third", "SelectInSubSeq", "first", Values.ppr(s.toString()), Values.ppr(t.toString()) });
 		}
-
-		final Applicable ftest = (Applicable) test;
+
 		final Value[] args = new Value[1];
 		for (; from <= to; from++) {
 			args[0] = seq.elems[from - 1];
-			final Value val = ftest.apply(args, EvalControl.Clear);
+			final Value val = test.eval(args, EvalControl.Clear);
 			if (!(val instanceof IBoolValue)) {
 				throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "fourth", "SelectInSubSeq",
-						"boolean-valued function", Values.ppr(test.toString()) });
+						"boolean-valued operator", Values.ppr(test.toString()) });
 			}
 			if (((BoolValue) val).val) {
 				return IntValue.gen(from);
@@ -460,22 +450,17 @@ public static Value SelectInSubSeq(final Value s, final Value f, final Value t,
 	}
 
 	@TLAPlusOperator(identifier = "SelectLastInSeq", module = "SequencesExt", warn = false)
-	public static Value selectLastInSeq(final Value s, final Value test) {
+	public static Value selectLastInSeq(final Value s, final OpValue test) {
 		final TupleValue seq = (TupleValue) s.toTuple();
 		if (seq == null) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "first", "SelectLastInSeq", "sequence", Values.ppr(s.toString()) });
 		}
-		if (!(test instanceof Applicable)) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "third", "SelectLastInSeq", "function", Values.ppr(test.toString()) });
-		}
 		int i = seq.size() - 1;
-		final Applicable ftest = (Applicable) test;
 		final Value[] args = new Value[1];
 		for (; i >= 0; i--) {
 			args[0] = seq.elems[i];
-			final Value val = ftest.apply(args, EvalControl.Clear);
+			final Value val = test.eval(args, EvalControl.Clear);
 			if (!(val instanceof IBoolValue)) {
 				throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "SelectLastInSeq",
 						"boolean-valued function", Values.ppr(test.toString()) });
@@ -488,7 +473,7 @@ public static Value selectLastInSeq(final Value s, final Value test) {
 	}
 
 	@TLAPlusOperator(identifier = "SelectLastInSubSeq", module = "SequencesExt", warn = false)
-	public static Value SelectLastInSubSeq(final Value s, final Value f, final Value t, final Value test) {
+	public static Value SelectLastInSubSeq(final Value s, final Value f, final Value t, final OpValue test) {
 		final TupleValue seq = (TupleValue) s.toTuple();
 		if (seq == null) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
@@ -502,10 +487,6 @@ public static Value SelectLastInSubSeq(final Value s, final Value f, final Value
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "third", "SelectLastInSubSeq", "natural", Values.ppr(t.toString()) });
 		}
-		if (!(test instanceof Applicable)) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "fourth", "SelectLastInSubSeq", "function", Values.ppr(test.toString()) });
-		}
 
 		final int from = ((IntValue) f).val;
 		int to = ((IntValue) t).val;
@@ -521,12 +502,11 @@ public static Value SelectLastInSubSeq(final Value s, final Value f, final Value
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_NOT_IN_DOMAIN,
 					new String[] { "third", "SelectLastInSubSeq", "first", Values.ppr(s.toString()), Values.ppr(t.toString()) });
 		}
-
-		final Applicable ftest = (Applicable) test;
+
 		final Value[] args = new Value[1];
 		for (; to >= from; to--) {
 			args[0] = seq.elems[to - 1];
-			final Value val = ftest.apply(args, EvalControl.Clear);
+			final Value val = test.eval(args, EvalControl.Clear);
 			if (!(val instanceof IBoolValue)) {
 				throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "fourth", "SelectLastInSubSeq",
 						"boolean-valued function", Values.ppr(test.toString()) });
@@ -561,17 +541,12 @@ public static Value removeFirst(final Value s, final Value e) {
 	}
 
 	@TLAPlusOperator(identifier = "RemoveFirstMatch", module = "SequencesExt", warn = false)
-	public static Value removeFirstMatch(final Value s, final Value test) {
+	public static Value removeFirstMatch(final Value s, final OpValue test) {
 		final TupleValue seq = (TupleValue) s.toTuple();
 		if (seq == null) {
 			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
 					new String[] { "first", "RemoveFirstMatch", "sequence", Values.ppr(s.toString()) });
 		}
-		if (!(test instanceof Applicable)) {
-			throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR,
-					new String[] { "second", "RemoveFirstMatch", "function", Values.ppr(test.toString()) });
-		}
-		final Applicable ftest = (Applicable) test;
 		final Value[] args = new Value[1];
 
 		final ArrayList<Value> val = new ArrayList<>(seq.elems.length);
@@ -580,7 +555,7 @@ public static Value removeFirstMatch(final Value s, final Value test) {
 		for (int i = 0; i < seq.elems.length; i++) {
 			if (!found) {
 				args[0] = seq.elems[i];
-				final Value bval = ftest.apply(args, EvalControl.Clear);
+				final Value bval = test.eval(args, EvalControl.Clear);
 				if (!(bval instanceof IBoolValue)) {
 					throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "second", "RemoveFirstMatch",
 							"boolean-valued function", Values.ppr(test.toString()) });