# bend-mathlib/maybe.bend: Maybe monad and map laws over &2.
import Base

# Left identity: binding a pure value applies the function.
law maybe_pure_bind:
  for ~A: Data
  for ~B: Data
  for -f: A -> Maybe<&2, B>
  for -x: A
  {Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) == f(x) : Maybe<&2, B>}

def maybe_pure_bind(A, B, f, x):
  {==}

# Right identity: binding pure is the identity.
law maybe_bind_pure:
  for ~A: Data
  for m: Maybe<&2, A>
  {Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) == m : Maybe<&2, A>}

def maybe_bind_pure(A, m):
  match m:
    case None{}:
      {==}
    case Some{x}:
      {==}

# Bind is associative.
law maybe_bind_assoc:
  for ~A: Data
  for ~B: Data
  for ~C: Data
  for -f: A -> Maybe<&2, B>
  for -g: B -> Maybe<&2, C>
  for m: Maybe<&2, A>
  {Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) == Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) : Maybe<&2, C>}

def maybe_bind_assoc(A, B, C, f, g, m):
  match m:
    case None{}:
      {==}
    case Some{x}:
      {==}

# Mapping a pure value is pure of the mapped value.
law maybe_map_pure:
  for ~A: Data
  for ~B: Data
  for -f: A -> B
  for -x: A
  {Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) == Maybe.pure(&2, B, f(x)) : Maybe<&2, B>}

def maybe_map_pure(A, B, f, x):
  {==}

# Mapping a composition maps the composition.
law maybe_map_compose:
  for ~A: Data
  for ~B: Data
  for ~C: Data
  for -f: A -> B
  for -g: B -> C
  for m: Maybe<&2, A>
  {Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) == Maybe.map(&2, A, C, x => g(f(x)), m) : Maybe<&2, C>}

def maybe_map_compose(A, B, C, f, g, m):
  match m:
    case None{}:
      {==}
    case Some{x}:
      {==}

# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---

# Left identity: binding a pure value applies the function, reversed to rewrite toward the simple side.
law maybe_pure_bind_sym:
  for ~A: Data
  for ~B: Data
  for -f: A -> Maybe<&2, B>
  for -x: A
  {f(x) == Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f) : Maybe<&2, B>}

def maybe_pure_bind_sym(A, B, f, x):
  Equal.sym(Maybe<&2, B>, Maybe.bind(&2, A, B, Maybe.pure(&2, A, x), f), f(x), maybe_pure_bind(~A, ~B, f, x))

# Right identity: binding pure is the identity, reversed to rewrite toward the simple side.
law maybe_bind_pure_sym:
  for ~A: Data
  for m: Maybe<&2, A>
  {m == Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)) : Maybe<&2, A>}

def maybe_bind_pure_sym(A, m):
  Equal.sym(Maybe<&2, A>, Maybe.bind(&2, A, A, m, x => Maybe.pure(&2, A, x)), m, maybe_bind_pure(~A, m))

# Bind is associative, reversed to rewrite toward the simple side.
law maybe_bind_assoc_sym:
  for ~A: Data
  for ~B: Data
  for ~C: Data
  for -f: A -> Maybe<&2, B>
  for -g: B -> Maybe<&2, C>
  for m: Maybe<&2, A>
  {Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)) == Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g) : Maybe<&2, C>}

def maybe_bind_assoc_sym(A, B, C, f, g, m):
  Equal.sym(Maybe<&2, C>, Maybe.bind(&2, B, C, Maybe.bind(&2, A, B, m, f), g), Maybe.bind(&2, A, C, m, x => Maybe.bind(&2, B, C, f(x), g)), maybe_bind_assoc(~A, ~B, ~C, f, g, m))

# Mapping a pure value is pure of the mapped value, reversed to rewrite toward the simple side.
law maybe_map_pure_sym:
  for ~A: Data
  for ~B: Data
  for -f: A -> B
  for -x: A
  {Maybe.pure(&2, B, f(x)) == Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)) : Maybe<&2, B>}

def maybe_map_pure_sym(A, B, f, x):
  Equal.sym(Maybe<&2, B>, Maybe.map(&2, A, B, f, Maybe.pure(&2, A, x)), Maybe.pure(&2, B, f(x)), maybe_map_pure(~A, ~B, f, x))

# Mapping a composition maps the composition, reversed to rewrite toward the simple side.
law maybe_map_compose_sym:
  for ~A: Data
  for ~B: Data
  for ~C: Data
  for -f: A -> B
  for -g: B -> C
  for m: Maybe<&2, A>
  {Maybe.map(&2, A, C, x => g(f(x)), m) == Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)) : Maybe<&2, C>}

def maybe_map_compose_sym(A, B, C, f, g, m):
  Equal.sym(Maybe<&2, C>, Maybe.map(&2, B, C, g, Maybe.map(&2, A, B, f, m)), Maybe.map(&2, A, C, x => g(f(x)), m), maybe_map_compose(~A, ~B, ~C, f, g, m))