Add CSV!CSVWriteRecord as a convenience method to write a record

(optionally including its names as column headers).

[Feature]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

modules/CSV.tla

@@ -13,6 +13,13 @@ CSVWrite(template, val, file) ==
     *)
    TRUE
 
+CSVWriteRecord(record, delim, headers, file) == 
+   (*
+       CSVWriteRecord([foo |-> 42] @@ [bar |-> "frob"], 
+           CSVRecords("/tmp/out.csv") = 0, "#", "/tmp/out.csv")
+    *)
+   TRUE
+
 CSVRead(columns, delimiter, file) == 
    (*
        CSVRead(<<"C1", "C2", "C3">>, "#", "/tmp/out.csv")

modules/tlc2/overrides/CSV.java

@@ -49,6 +49,37 @@
 
 public class CSV {
 
+	@TLAPlusOperator(identifier = "CSVWriteRecord", module = "CSV", minLevel = 1, warn = false)
+	public static Value writeRecord(final Value parameter, final StringValue delim, final BoolValue headers,
+			final StringValue absolutePath) throws IOException {
+
+		final RecordValue tv = (RecordValue) parameter.toRcd();
+		if (tv == null) {
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "CSVWriteRecord", "record", Values.ppr(parameter.toString()) });
+		}
+
+		// Normalizing the input takes care of mapping subsequent invocations of the
+		// same record to the same columns.
+		tv.deepNormalize();
+
+		// Names/Headers
+		if (headers.val) {
+			final String s = Arrays.stream(tv.names).map(v -> v.toString())
+					.collect(Collectors.joining(delim.val.toString()));
+			Files.write(Paths.get(absolutePath.val.toString()), (s + System.lineSeparator()).getBytes("UTF-8"),
+					StandardOpenOption.CREATE, StandardOpenOption.APPEND);
+		}
+
+		// Values
+		final String s = Arrays.stream(tv.values).map(v -> v.toString())
+				.collect(Collectors.joining(delim.val.toString()));
+		Files.write(Paths.get(absolutePath.val.toString()), (s + System.lineSeparator()).getBytes("UTF-8"),
+				StandardOpenOption.CREATE, StandardOpenOption.APPEND);
+
+		return BoolValue.ValTrue;
+	}
+
 	@TLAPlusOperator(identifier = "CSVWrite", module = "CSV", minLevel = 1, warn = false)
 	public static Value write(final StringValue template, final Value parameter, final StringValue absolutePath)
 			throws IOException {