import Base
import ./lib.bend as P

# pure places x and leaves the input untouched.
law pure_id:
  for -A: Type
  for x: A
  for s: String
  { P.Parse.pure(A, x, s) == Some{(x, s)} : Maybe<&1, A & String> }

# fail always returns None.
law fail_none:
  for -A: Type
  for s: String
  { P.Parse.fail(A, s) == None{} : Maybe<&1, A & String> }

# map id on a concrete pure result (definitional).
law map_id_pure:
  for s: String
  {
    P.Parse.map(U32, U32, (x => x), P.Parse.pure(U32, 7, s))
      == Some{(7, s)}
    : Maybe<&1, U32 & String>
  }

# or(fail, char) degenerates to char on the same input.
law or_fail_left_char:
  for +c: Char
  for +s: String
  {
    P.Parse.or(Char, P.Parse.fail(Char), P.Parse.char(c), s)
      == P.Parse.char(c, s)
    : Maybe<&1, Char & String>
  }

# or(char, fail) keeps a hit on a matching singleton (concrete char).
law or_fail_right_char_hit:
  {
    P.Parse.or(Char, P.Parse.char('a'), P.Parse.fail(Char), SCon{'a', SNil{}})
      == Some{('a', SNil{})}
    : Maybe<&1, Char & String>
  }

# char matches the head and returns the tail (concrete char; is_eq needs it).
law char_match:
  for t: String
  { P.Parse.char('a', SCon{'a', t}) == Some{('a', t)} : Maybe<&1, Char & String> }

# char fails on empty input.
law char_fail_empty:
  for +c: Char
  { P.Parse.char(c, SNil{}) == None{} : Maybe<&1, Char & String> }

# char fails when the head differs (concrete distinct chars).
law char_fail_mismatch:
  {
    P.Parse.char('a', SCon{'b', SNil{}}) == None{}
    : Maybe<&1, Char & String>
  }

# string literal: empty pattern always matches (case-split on s in the proof).
law string_empty:
  for s: String
  { P.Parse.string(SNil{}, s) == Some{(SNil{}, s)} : Maybe<&1, String & String> }

# map over fail is None.
law map_fail:
  for s: String
  {
    P.Parse.map(U32, U32, (x => x), P.Parse.fail(U32, s))
      == None{}
    : Maybe<&1, U32 & String>
  }

# string literal hit consumes the prefix.
law string_lit_hit:
  {
    P.Parse.string(SCon{'a', SNil{}}, SCon{'a', SCon{'b', SNil{}}})
      == Some{(SCon{'a', SNil{}}, SCon{'b', SNil{}})}
    : Maybe<&1, String & String>
  }

# string literal miss fails.
law string_lit_miss:
  {
    P.Parse.string(SCon{'a', SNil{}}, SCon{'b', SNil{}})
      == None{}
    : Maybe<&1, String & String>
  }