///|
pub fn apply_subst(self : Expression, subst : Subst) -> Expression {
  match self {
    Var(v) =>
      match subst._.get(v) {
        Some(v) => v.to_expr()
        None => Var(v)
      }
    Ctor(name, exp) => Ctor(name, exp.map(apply_subst(_, subst)))
    Default => Default
    Case(e, clauses~, default~) => {
      let clauses = clauses.map(fn {
        { pattern, expr } => { pattern, expr: expr.apply_subst(subst) }
      })
      Case(e.apply_subst(subst), clauses~, default=default.apply_subst(subst))
    }
  }
}

///|
fn to_expr(self : Value) -> Expression {
  guard self is VApp(name, vs)
  Ctor(name, vs.map(to_expr(_)))
}

///|
pub fn step(self : Expression) -> Result[Expression, Value]! {
  match self {
    Var(_) | Default => raise Step
    Ctor(cn, vs) => Err(VApp(cn, vs.map(fn { v => v.steps?().unwrap() })))
    Case(e, clauses~, default~) => {
      let v = e.steps()
      for clause in clauses {
        let pattern = clause.pattern
        let expr = clause.expr
        match pattern.matches?(v) {
          Ok(subst) => {
            let new_expr = expr.apply_subst(subst)
            break Ok(new_expr)
          }
          Err(_) => ()
        }
      } else {
        if clauses
          .iter()
          .map(fn { { pattern, .. } => pattern.not_matches?(v) })
          .all(Result::is_ok) {
          Ok(default)
        } else {
          raise Step // non-exhaustive pattern match
        }
      }
    }
  }
}

///|
pub fn steps(self : Expression) -> Value! {
  loop self.step() {
    Ok(e) => continue e.step!()
    Err(v) => v
  }
}

///|
pub fn nnfP(self : Pattern) -> Pattern {
  match self {
    PAnd(p1, p2) => PAnd(p1.nnfP(), p2.nnfP())
    POr(p1, p2) => POr(p1.nnfP(), p2.nnfP())
    PNot(p) => nnfN(p)
    PCtor(cn, vs) => PCtor(cn, vs.map(nnfP(_)))
    PTop | PBottom | PVar(_) => self
  }
}

///|
pub fn nnfN(self : Pattern) -> Pattern {
  match self {
    PAnd(p1, p2) => POr(p1.nnfN(), p2.nnfN())
    POr(p1, p2) => PAnd(p1.nnfN(), p2.nnfN())
    PNot(p) => p.nnfP()
    PCtor(cn, vs) => {
      let l = vs.length()
      let val = Array::make(l, PTop)
      guard l > 0 else { PNot(PCtor(cn, [])) }
      vs
      .mapi(fn(i, p) {
        let pa = val.copy()
        pa[i] = p.nnfN()
        PCtor(cn, pa)
      })
      .fold(init=PCtor(cn, val), fn(acc, p) { POr(acc, p) })
    }
    PTop => PBottom
    PBottom => PTop
    PVar(x) => PNot(PVar(x))
  }
}

///|
pub fn dnf(self : Pattern) -> Set[Pattern] {
  match self {
    PVar(_) | PNot(PVar(_)) | PTop | PBottom => Set::from_array([self])
    PNot(PCtor(_, vs)) if vs.iter().all(fn { p => p == PTop }) =>
      Set::from_array([self])
    PCtor(cn, vs) =>
      cartesian(vs.map(dnf(_)).map(Set::iter)).map(fn {
        c => PCtor(cn, Iter::collect(c))
      })
      |> Set::from_iter
    PAnd(p1, p2) =>
      cartesian([p1.dnf().iter(), p2.dnf().iter()]).map(fn {
        c => {
          guard c.collect() is [x, y]
          PAnd(x, y)
        }
      })
      |> Set::from_iter
    POr(p1, p2) => p1.dnf().union(p2.dnf())
    PNot(_) => abort("dnf: unexpected pattern, not in NNF")
  }
}

///|
test {
  let sat = CtorName::{ name: "sat", arity: 0 } |> PCtor([])
  let sun = CtorName::{ name: "sun", arity: 0 } |> PCtor([])
  let p1 = PAnd(PVar("x"), PNot(POr(sat, sun)))
  let p2 = PAnd(PVar("x"), POr(sat, sun))
  inspect!(p1, content="x & ¬(sat || sun)")
  inspect!(p1.nnfP(), content="x & ¬(sat) & ¬(sun)")
  inspect!(p2, content="x & sat || sun")
  inspect!(p2.nnfP(), content="x & sat || sun")
  inspect!(p1.nnfP().dnf(), content="{x & ¬(sat) & ¬(sun)}")
  inspect!(p2.nnfP().dnf(), content="{x & sat, x & sun}")
}

///|
test {
  let true_ = CtorName::{ name: "true", arity: 0 }
  let b_true = true_ |> Ctor(_, [])
  let false_ = CtorName::{ name: "false", arity: 0 }
  let b_false = false_ |> Ctor(_, [])
  let cons_ = CtorName::{ name: "cons", arity: 2 }
  let cons = fn { x, xs => cons_ |> Ctor(_, [x, xs]) }
  let nil_ = CtorName::{ name: "nil", arity: 0 }
  let nil = nil_ |> Ctor(_, [])
  let lst = cons(b_true, nil)
  let cases = Case(
    lst,
    clauses=[PCtor(nil_, [])[b_false], PNot(PCtor(nil_, []))[b_true]],
    default=b_false,
  )
  inspect!(cases.steps?(), content="Ok(VApp(true, []))")
  let cases = Case(
    b_true,
    clauses=[PCtor(false_, [])[b_true], PNot(PNot(PCtor(true_, [])))[b_false]],
    default=b_false,
  )
  inspect!(cases.steps?(), content="Ok(VApp(false, []))")
}