~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x36062a6887f9a7dac4ca208d99d96105/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as C

Laws

law is_quote_true provedin PROOF.bendsource · line 5 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.is_quote('"') == True{} : Bool}

Character classification is explicit and definitional.

law is_quote_false provedin PROOF.bendsource · line 8 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.is_quote('a') == False{} : Bool}

law is_comma_true provedin PROOF.bendsource · line 11 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.is_comma(',') == True{} : Bool}

law is_comma_false provedin PROOF.bendsource · line 14 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.is_comma('a') == False{} : Bool}

law parse_line_empty provedin PROOF.bendsource · line 18 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("") == [""] : List<&2, String>}

Empty and one-field lines retain CSV's empty-field behavior.

law parse_line_one provedin PROOF.bendsource · line 21 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("a") == ["a"] : List<&2, String>}

law parse_line_two provedin PROOF.bendsource · line 24 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("a,b") == ["a", "b"] : List<&2, String>}

law parse_line_trailing_empty provedin PROOF.bendsource · line 30 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("a,") == ["a", ""] : List<&2, String>}

law parse_line_quoted_comma provedin PROOF.bendsource · line 37 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("\"a,b\"") == ["a,b"] : List<&2, String>}

Quotes protect commas, and doubled quotes become one quote.

law parse_line_quoted_empty provedin PROOF.bendsource · line 43 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("\"\"") == [""] : List<&2, String>}

law parse_line_doubled_quote provedin PROOF.bendsource · line 49 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse_line("\"a\"\"b\"") == ["a\"b"] : List<&2, String>}

law parse_empty provedin PROOF.bendsource · line 56 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse("") == [] : List<&2, List<&2, String>>}

Empty input is no document; newline splits physical records.

law parse_one_line provedin PROOF.bendsource · line 59 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse("a,b") == [["a", "b"]] : List<&2, List<&2, String>>}

law parse_two_lines provedin PROOF.bendsource · line 65 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse("a\nb") == [["a"], ["b"]] : List<&2, List<&2, String>>}

law parse_final_empty_line provedin PROOF.bendsource · line 71 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse("a\n") == [["a"], [""]] : List<&2, List<&2, String>>}

law encode_field_plain provedin PROOF.bendsource · line 78 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_field("a") == "a" : String}

Encoding quotes only when needed, and doubles embedded quotes.

law encode_field_comma provedin PROOF.bendsource · line 81 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_field("a,b") == "\"a,b\"" : String}

law encode_field_quote provedin PROOF.bendsource · line 84 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_field("a\"b") == "\"a\"\"b\"" : String}

law encode_field_empty provedin PROOF.bendsource · line 87 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_field("") == "" : String}

law encode_row_empty provedin PROOF.bendsource · line 90 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_row([]) == "" : String}

law encode_row_two provedin PROOF.bendsource · line 93 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_row(["a", "b"]) == "a,b" : String}

law encode_row_quoted provedin PROOF.bendsource · line 99 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode_row(["a,b", "c"]) == "\"a,b\",c" : String}

law encode_empty provedin PROOF.bendsource · line 105 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode([]) == "" : String}

law encode_two_rows provedin PROOF.bendsource · line 108 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode([["a"], ["b"]]) == "a\nb" : String}

law parse_encode_simple provedin PROOF.bendsource · line 115 · raw

{0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.parse(0x36062a6887f9a7dac4ca208d99d96105/lib.Csv.encode([["a", "b"]])) == [["a", "b"]] : List<&2, List<&2, String>>}

The simple unquoted case round-trips by direct reduction.