///|
fnalias @immut/hashmap.(singleton, new as empty)

///|
pub fn fv_even(self : Pattern) -> Set[Var] {
  let set = Set::new()
  fn go {
    PVar(v) => set.add(v)
    PCtor(_, ps) => ps.each(go)
    PTop | PBottom => ()
    PAnd(p1, p2) | POr(p1, p2) => {
      go(p1)
      go(p2)
    }
    PNot(p) => fv_odd(p).each(set.add(_))
  }

  go(self)
  set
}

///|
pub fn fv_odd(self : Pattern) -> Set[Var] {
  let set = Set::new()
  fn go {
    PCtor(_, ps) => ps.each(go)
    PVar(_) | PTop | PBottom => ()
    PAnd(p1, p2) | POr(p1, p2) => {
      go(p1)
      go(p2)
    }
    PNot(p) => fv_even(p).each(set.add(_))
  }

  go(self)
  set
}

///|
pub fn matches(self : Pattern, v : Value) -> Subst!Match {
  match self {
    PVar(x) => (singleton(x, v) : Subst)
    PTop => empty()
    PNot(p) => p.not_matches(v)
    PAnd(p1, p2) => p1.matches(v)._.union(p2.matches(v)._)
    POr(p1, p2) => p1.matches?(v).or(p2.matches(v))
    PCtor(name, ps) => {
      guard v is VApp(name2, vs) && name == name2 else { raise Match }
      let pvs = ps.zip(vs)
      loop empty(), pvs.length() {
        acc, 0 => acc
        acc, n => {
          let (p, v) = pvs[n - 1]
          continue acc.union(p.matches(v)._), n - 1
        }
      }
    }
    PBottom => raise Match
  }
}

///|
pub fn not_matches(self : Pattern, v : Value) -> Subst!Match {
  match self {
    PBottom => empty()
    PNot(p) => p.matches(v)
    PCtor(name, ps) => {
      guard v is VApp(name2, vs) && name == name2 else { empty() }
      let pvs = ps.zip(vs).map(fn { (p, v) => p.not_matches?(v) })
      match pvs.search_by(Result::is_ok) {
        Some(idx) => pvs[idx].unwrap()
        None => raise Match
      }
    }
    PAnd(p1, p2) => p1.not_matches?(v).or(p2.not_matches!(v))
    POr(p1, p2) => p1.not_matches(v)._.union(p2.not_matches(v)._)
    PTop | PVar(_) => raise Match
  }
}

///|
pub fn linP(self : Pattern) -> Bool {
  match self {
    PBottom | PTop | PVar(_) => true
    POr(p1, p2) => p1.linP() && p2.linP() && p1.fv_even() == p2.fv_even()
    PAnd(p1, p2) =>
      p1.linP() &&
      p2.linP() &&
      p1.fv_even().intersection(p2.fv_even()).is_empty()
    PNot(p) => p.linN()
    PCtor(_, ps) =>
      ps.iter().all(linP) &&
      ps
      .fold(init=Set::new(), fn(acc, pat) { acc.intersection(pat.fv_even()) })
      .is_empty()
  }
}

///|
pub fn linN(self : Pattern) -> Bool {
  match self {
    PBottom | PTop | PVar(_) => true
    POr(p1, p2) =>
      p1.linN() && p2.linN() && p1.fv_odd().intersection(p2.fv_odd()).is_empty()
    PAnd(p1, p2) => p1.linN() && p2.linN() && p1.fv_odd() == p2.fv_odd()
    PNot(p) => p.linP()
    PCtor(_, ps) =>
      ps.iter().all(linN) && ps.map(fv_odd).iter().all(Set::is_empty)
  }
}

///|
pub fn det(self : Pattern) -> Bool {
  match self {
    PTop | PBottom | PVar(_) => true
    PAnd(p1, p2) =>
      (p1.det() && p2.det()) &&
      (
        not(PNot(p1).overlap(PNot(p2))) ||
        (p1.fv_odd().is_empty() && p2.fv_odd().is_empty())
      )
    POr(p1, p2) =>
      (p1.det() && p2.det()) &&
      (
        not(p1.overlap(p2)) ||
        (p1.fv_even().is_empty() && p2.fv_even().is_empty())
      )
    PNot(p) => p.det()
    PCtor(_, ps) => ps.iter().all(det)
  }
}

///|
pub fn overlap(self : Pattern, _other : Pattern) -> Bool {
  abort("overlap: not implemented")
}

///|
pub fn op_get(self : Pattern, val : Expression) -> Clause {
  { pattern: self, expr: val }
}

///|
impl Show for Pattern with to_string(self) {
  match self {
    PVar(v) => v._
    PTop => "_"
    PBottom => "#"
    PAnd(p1, p2) => "\{p1} & \{p2}"
    POr(p1, p2) => "\{p1} || \{p2}"
    PNot(p) => "¬(\{p})"
    PCtor(cn, _ps) if cn.arity == 0 => cn.name
    PCtor(cn, ps) => cn.name + "(" + ps.map(Show::to_string(_)).join(", ") + ")"
  }
}

///|
impl Show for Pattern with output(self, logger) {
  logger.write_string(self.to_string())
}