# Parse — tiny String parser combinators for Bend.
# Publish entry for this package. Depends only on Base.
#
# Encoding: a Parser for A is String → Maybe (A & remainder).
# One-shot combinators (bind/or/optional/map) take ordinary Parser functions
# (affine closures are fine — each is used at most once). Predicates for
# satisfy/take_while are templates (~) so they may fire on many chars.
# Tradeoff: a Parser closure is not reusable; rebuild with top-level defs or
# lambdas at each site. String is Data, so `or`/`optional` take +s to retry.
import Base

# Parser(A) ≅ String → Maybe<&1, A & String> (&1 keeps A : Type).
law Parser:
  for -A: Type
  Type

def Parser(A):
  String -> Maybe<&1, A & String>

# Always succeed with x, consuming nothing.
def Parse.pure(-A: Type, x: A, s: String) -> Maybe<&1, A & String>:
  Some{(x, s)}

# Always fail.
def Parse.fail(-A: Type, s: String) -> Maybe<&1, A & String>:
  None{}

# Map over a successful parse payload (value only; remainder unchanged).
def Parse.map(
  -A: Type, -B: Type, f: A -> B, m: Maybe<&1, A & String>
) -> Maybe<&1, B & String>:
  match m:
    case None{}:
      None{}
    case Some{(x, s)}:
      Some{(f(x), s)}

# Run p, then continue with f(value, remainder). Helpers avoid matching on p(s).
def Parse.bind.cont(
  -A: Type, -B: Type, f: A -> String -> Maybe<&1, B & String>,
  m: Maybe<&1, A & String>
) -> Maybe<&1, B & String>:
  match m:
    case None{}:
      None{}
    case Some{(x, s2)}:
      f(x, s2)

def Parse.bind(
  -A: Type, -B: Type, p: Parser(A), f: A -> String -> Maybe<&1, B & String>,
  s: String
) -> Maybe<&1, B & String>:
  Parse.bind.cont(A, B, f, p(s))

# Alias: and_then = bind.
def Parse.and_then(
  -A: Type, -B: Type, p: Parser(A), f: A -> String -> Maybe<&1, B & String>,
  s: String
) -> Maybe<&1, B & String>:
  Parse.bind(A, B, p, f, s)

# Prefer p; on failure try q on the same input (+s copies; String is Data).
def Parse.or.cont(
  -A: Type, q: Parser(A), +s: String, m: Maybe<&1, A & String>
) -> Maybe<&1, A & String>:
  match m:
    case Some{r}:
      Some{r}
    case None{}:
      q(s)

def Parse.or(
  -A: Type, p: Parser(A), q: Parser(A), +s: String
) -> Maybe<&1, A & String>:
  Parse.or.cont(A, q, s, p(s))

# Next char if pred holds. ~pred is a template (reusable, closed).
def Parse.satisfy.go(
  +h: Char, t: String, ok: Bool
) -> Maybe<&1, Char & String>:
  match ok:
    case False{}:
      None{}
    case True{}:
      Some{(h, t)}

def Parse.satisfy(~pred: Char -> Bool, s: String) -> Maybe<&1, Char & String>:
  match s:
    case SNil{}:
      None{}
    case SCon{+h, t}:
      Parse.satisfy.go(h, t, pred(h))

# Exact character.
def Parse.char.go(
  +expected: Char, +h: Char, t: String, ok: Bool
) -> Maybe<&1, Char & String>:
  match ok:
    case False{}:
      None{}
    case True{}:
      Some{(h, t)}

def Parse.char(+expected: Char, s: String) -> Maybe<&1, Char & String>:
  match s:
    case SNil{}:
      None{}
    case SCon{+h, t}:
      Parse.char.go(expected, h, t, Char.is_eq(h, expected))

# Exact string prefix; value is the matched prefix, rest is the suffix.
def Parse.string.go(
  +p: String, +s: String, ok: Bool
) -> Maybe<&1, String & String>:
  match ok:
    case False{}:
      None{}
    case True{}:
      Some{(p, String.drop(s, String.length(p)))}

def Parse.string(+p: String, +s: String) -> Maybe<&1, String & String>:
  Parse.string.go(p, s, String.starts_with(s, p))

# take_while: one self-recursive template with Nat fuel (2 steps per char).
# step=False → inspect s; step=True → inspect ok (h is the candidate char).
# Avoids mutual template recursion (Bend: templates may only call those above).
def Parse.take_while.go(
  ~pred: Char -> Bool, n: Nat, s: String, acc: String, step: Bool, +h: Char,
  ok: Bool
) -> String & String:
  match n s step ok:
    case 0n s2 _ _:
      (String.reverse(acc), s2)
    case 1n+p SNil{} False{} _:
      (String.reverse(acc), SNil{})
    case 1n+p SCon{+h2, t} False{} _:
      Parse.take_while.go(~pred, p, t, acc, True{}, h2, pred(h2))
    case 1n+p s2 True{} False{}:
      (String.reverse(acc), SCon{h, s2})
    case 1n+p s2 True{} True{}:
      Parse.take_while.go(~pred, p, s2, SCon{h, acc}, False{}, h, False{})
    case 1n+p s2 False{} _:
      (String.reverse(acc), s2)

# Longest prefix whose chars all satisfy pred. Always succeeds (may be empty).
def Parse.take_while(~pred: Char -> Bool, +s: String) -> Maybe<&1, String & String>:
  Some{
    Parse.take_while.go(
      ~pred, Nat.add(String.length(s), String.length(s)), s, SNil{}, False{},
      Char.from_u32(0), False{}
    )
  }

# Optional: always succeeds; value is Maybe A.
def Parse.optional.cont(
  -A: Type, +s: String, m: Maybe<&1, A & String>
) -> Maybe<&1, Maybe<&1, A> & String>:
  match m:
    case Some{(x, rest)}:
      Some{(Some{x}, rest)}
    case None{}:
      Some{(None{}, s)}

def Parse.optional(
  -A: Type, p: Parser(A), +s: String
) -> Maybe<&1, Maybe<&1, A> & String>:
  Parse.optional.cont(A, s, p(s))

# Run parser (identity application).
def Parse.run(-A: Type, p: Parser(A), s: String) -> Maybe<&1, A & String>:
  p(s)

# Succeed only if the whole input is consumed.
def Parse.run_full.rest(-A: Type, x: A, rest: String) -> Maybe<&1, A>:
  match rest:
    case SNil{}:
      Some{x}
    case SCon{h, t}:
      None{}

def Parse.run_full.go(-A: Type, m: Maybe<&1, A & String>) -> Maybe<&1, A>:
  match m:
    case None{}:
      None{}
    case Some{(x, rest)}:
      Parse.run_full.rest(A, x, rest)

def Parse.run_full(-A: Type, p: Parser(A), s: String) -> Maybe<&1, A>:
  Parse.run_full.go(A, p(s))