import Base
import ./lib.bend as C

# Character classification is explicit and definitional.
law is_quote_true:
  { C.Csv.is_quote('"') == True{} : Bool }

law is_quote_false:
  { C.Csv.is_quote('a') == False{} : Bool }

law is_comma_true:
  { C.Csv.is_comma(',') == True{} : Bool }

law is_comma_false:
  { C.Csv.is_comma('a') == False{} : Bool }

# Empty and one-field lines retain CSV's empty-field behavior.
law parse_line_empty:
  { C.Csv.parse_line("") == SNil{} <> Nil{} : List<&2, String> }

law parse_line_one:
  { C.Csv.parse_line("a") == "a" <> Nil{} : List<&2, String> }

law parse_line_two:
  {
    C.Csv.parse_line("a,b") == "a" <> ("b" <> Nil{})
    : List<&2, String>
  }

law parse_line_trailing_empty:
  {
    C.Csv.parse_line("a,") == "a" <> (SNil{} <> Nil{})
    : List<&2, String>
  }

# Quotes protect commas, and doubled quotes become one quote.
law parse_line_quoted_comma:
  {
    C.Csv.parse_line("\"a,b\"") == "a,b" <> Nil{}
    : List<&2, String>
  }

law parse_line_quoted_empty:
  {
    C.Csv.parse_line("\"\"") == SNil{} <> Nil{}
    : List<&2, String>
  }

law parse_line_doubled_quote:
  {
    C.Csv.parse_line("\"a\"\"b\"") == "a\"b" <> Nil{}
    : List<&2, String>
  }

# Empty input is no document; newline splits physical records.
law parse_empty:
  { C.Csv.parse("") == Nil{} : List<&2, List<&2, String>> }

law parse_one_line:
  {
    C.Csv.parse("a,b") == ("a" <> ("b" <> Nil{})) <> Nil{}
    : List<&2, List<&2, String>>
  }

law parse_two_lines:
  {
    C.Csv.parse("a\nb") == ("a" <> Nil{}) <> (("b" <> Nil{}) <> Nil{})
    : List<&2, List<&2, String>>
  }

law parse_final_empty_line:
  {
    C.Csv.parse("a\n") == (("a" <> Nil{}) <> ((SNil{} <> Nil{}) <> Nil{}))
    : List<&2, List<&2, String>>
  }

# Encoding quotes only when needed, and doubles embedded quotes.
law encode_field_plain:
  { C.Csv.encode_field("a") == "a" : String }

law encode_field_comma:
  { C.Csv.encode_field("a,b") == "\"a,b\"" : String }

law encode_field_quote:
  { C.Csv.encode_field("a\"b") == "\"a\"\"b\"" : String }

law encode_field_empty:
  { C.Csv.encode_field("") == "" : String }

law encode_row_empty:
  { C.Csv.encode_row(Nil{}) == "" : String }

law encode_row_two:
  {
    C.Csv.encode_row("a" <> ("b" <> Nil{})) == "a,b"
    : String
  }

law encode_row_quoted:
  {
    C.Csv.encode_row("a,b" <> ("c" <> Nil{})) == "\"a,b\",c"
    : String
  }

law encode_empty:
  { C.Csv.encode(Nil{}) == "" : String }

law encode_two_rows:
  {
    C.Csv.encode(("a" <> Nil{}) <> (("b" <> Nil{}) <> Nil{})) == "a\nb"
    : String
  }

# The simple unquoted case round-trips by direct reduction.
law parse_encode_simple:
  {
    C.Csv.parse(C.Csv.encode(("a" <> ("b" <> Nil{})) <> Nil{}))
      == ("a" <> ("b" <> Nil{})) <> Nil{}
    : List<&2, List<&2, String>>
  }