Add CSV!CSVRead operator.

[Feature]

Author: lemmy

modules/CSV.tla

@@ -13,6 +13,15 @@ CSVWrite(template, val, file) ==
     *)
    TRUE
 
+CSVRead(columns, delimiter, file) == 
+   (*
+       CSVRead(<<"C1", "C2", "C3">>, "#", "/tmp/out.csv")
+       
+       << [ C1 |-> "\"abc\"", C2 |-> "42", C3 |-> "{"\"x\"", "\"y\""}" ] >>
+    *)
+   TRUE
+
+
 CSVRecords(file) == 
    (* The number of records in the given file (including headers if any). *)
    CHOOSE n : n \in Nat

modules/tlc2/overrides/CSV.java

@@ -32,16 +32,20 @@
 import java.nio.file.Paths;
 import java.nio.file.StandardOpenOption;
 import java.util.Arrays;
+import java.util.List;
+import java.util.stream.Collectors;
 import java.util.stream.Stream;
 
 import tlc2.output.EC;
 import tlc2.tool.EvalException;
 import tlc2.value.Values;
 import tlc2.value.impl.BoolValue;
 import tlc2.value.impl.IntValue;
+import tlc2.value.impl.RecordValue;
 import tlc2.value.impl.StringValue;
 import tlc2.value.impl.TupleValue;
 import tlc2.value.impl.Value;
+import util.UniqueString;
 
 public class CSV {
 
@@ -61,6 +65,36 @@ public static Value write(final StringValue template, final Value parameter, fin
 		return BoolValue.ValTrue;
 	}
 
+	@TLAPlusOperator(identifier = "CSVRead", module = "CSV", minLevel = 1, warn = false)
+	public static Value read(final Value columns, final StringValue delim, final StringValue absolutePath)
+			throws IOException {
+		
+		final TupleValue tv = (TupleValue) columns.toTuple();
+		if (tv == null) {
+			throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR,
+					new String[] { "CSVRead", "sequence", Values.ppr(columns.toString()) });
+		}
+
+		final Path path = Paths.get(absolutePath.val.toString());
+		if (!path.toFile().exists()) {
+			// There are zero records in a file that doesn't exist.
+			return TupleValue.EmptyTuple;
+		}
+		
+		final UniqueString[] names = Arrays.asList(tv.elems).stream().map(v -> ((StringValue) v).val)
+				.collect(Collectors.toList()).toArray(UniqueString[]::new);
+
+		final List<String> lines = Files.readAllLines(path);
+		final Value[] records = new Value[lines.size()];
+		for (int i = 0; i < lines.size(); i++) {
+			StringValue[] values = Arrays.asList(lines.get(i).split(delim.val.toString())).stream()
+					.map(s -> new StringValue(s)).collect(Collectors.toList()).toArray(StringValue[]::new);
+			records[i] = new RecordValue(names, values, false);
+		}
+
+		return new TupleValue(records);
+	}
+
 	@TLAPlusOperator(identifier = "CSVRecords", module = "CSV", minLevel = 1, warn = false)
 	public static Value records(final StringValue absolutePath)
 			throws IOException {

tests/CSVTests.tla

@@ -1,5 +1,5 @@
 ---------------------------- MODULE CSVTests ----------------------------
-EXTENDS CSV, TLC, Sequences, IOUtils
+EXTENDS CSV, TLC, Sequences, IOUtils, TLCExt
 
 ASSUME LET T == INSTANCE TLC IN T!PrintT("CSVTests")
 
@@ -14,11 +14,13 @@ ToFile ==
     "build/tests/CSVWriteTest-" \o ToString(JavaTime) \o ".csv"
 
 \* Write Value to ToFile then check success by reading with IOExec. 
-ASSUME(
+ASSUME
   CSVWrite(Template, Value, ToFile) 
     => 
-      /\ IOExec(<< "cat", ToFile >>).stdout = "42#\"abc\"#[a |-> \"a\", b |-> \"b\"]\n")
       /\ CSVRecords(ToFile) = 1
+      \* Skip the third (record) element because it would come back as a string.
+      /\ LET in == Head(CSVRead(<<"a", "b", "c">>, "#", ToFile))
+         IN in.a = "42" /\ in.b = "\"abc\"" /\ in.c = "[a |-> \"a\", b |-> \"b\"]"
 
 ASSUME
   CSVRecords("DoesNotExistNowhere.tla") = 0