///|
enum NDNF_K {
  KCtor(Set[Var], CtorName, Array[NDNF_K])
  KNot(Set[Var], Array[CtorName])
  KBottom(Set[Var])
} derive(Eq)

///|
pub fn norm_set(set : Set[Pattern]) -> Array[NDNF_K] {
  set.iter().map(norm(_)).collect()
}

///|
pub fn head(self : NDNF_K) -> Set[CtorName] {
  match self {
    KCtor(_, c, _) => Set::from_array([c])
    KNot(_, cs) => Set::from_array(cs)
    KBottom(_) => Set::new()
  }
}

///|
pub fn head_arr(s : Array[NDNF_K]) -> Set[CtorName] {
  s.iter().fold(init=Set::new(), fn(acc, k) { acc.union(k.head()) })
}

///|
pub fn norm(self : Pattern) -> NDNF_K {
  match self {
    PVar(v) => KNot(Set::from_array([v]), [])
    PTop => KNot(Set::new(), [])
    PBottom => KBottom(Set::new())
    PNot(PVar(_)) => KBottom(Set::new())
    PNot(PCtor(n, vs)) if vs.iter().all(fn { p => p == PTop }) =>
      KNot(Set::new(), [n])
    PNot(PCtor(n, vs)) => KCtor(Set::new(), n, vs.map(norm(_)))
    PAnd(p1, p2) => combine(norm(p1), norm(p2))
    _ => abort("norm: not a disjunctive normal form")
  }
}

///|
fn combine(self : NDNF_K, other : NDNF_K) -> NDNF_K {
  match (self, other) {
    (KBottom(s1), KBottom(s2)) => KBottom(s1.union(s2))
    (KBottom(s1), KCtor(s2, _, _)) => KBottom(s1.union(s2))
    (KBottom(s1), KNot(s2, _)) => KBottom(s1.union(s2))
    (KNot(s1, cs1), KNot(s2, cs2)) => KNot(s1.union(s2), cs1 + cs2)
    (KCtor(s1, c1, ks), KNot(s2, cs)) => {
      guard cs.contains(c1) else { KCtor(s1.union(s2), c1, ks) }
      KBottom(s1.union(s2))
    }
    (KCtor(s1, c1, n), KCtor(s2, c2, m)) => {
      guard c1 == c2 && n.length() == m.length() else { KBottom(s1.union(s2)) }
      KCtor(s1.union(s2), c1, n.zip(m).map(fn { (k1, k2) => combine(k1, k2) }))
    }
    _ => abort("combine: not a valid normalized disjunctive normal form")
  }
}