///|
pub(all) struct ExpressionStats {
  nodes : Int
  depth : Int
  comparisons : Int
  variables : Array[String]
} derive(Debug, Eq)

///|
pub fn Expr::stats(self : Expr) -> ExpressionStats {
  let variables : Array[String] = []
  collect_variables(self, variables)
  {
    nodes: expression_nodes(self),
    depth: expression_depth(self),
    comparisons: expression_comparisons(self),
    variables,
  }
}

///|
fn collect_variables(expression : Expr, variables : Array[String]) -> Unit {
  match expression {
    Constant(_) => ()
    Compare(name, _, _) | Present(name) =>
      if !variables.contains(name) {
        variables.push(name)
      }
    Not(inner) => collect_variables(inner, variables)
    And(left, right) | Or(left, right) => {
      collect_variables(left, variables)
      collect_variables(right, variables)
    }
  }
}

///|
fn expression_nodes(expression : Expr) -> Int {
  match expression {
    Constant(_) | Compare(_, _, _) | Present(_) => 1
    Not(inner) => 1 + expression_nodes(inner)
    And(left, right) | Or(left, right) =>
      1 + expression_nodes(left) + expression_nodes(right)
  }
}

///|
fn expression_depth(expression : Expr) -> Int {
  match expression {
    Constant(_) | Compare(_, _, _) | Present(_) => 1
    Not(inner) => 1 + expression_depth(inner)
    And(left, right) | Or(left, right) => {
      let left_depth = expression_depth(left)
      let right_depth = expression_depth(right)
      let max_depth = if left_depth > right_depth {
        left_depth
      } else {
        right_depth
      }
      1 + max_depth
    }
  }
}

///|
fn expression_comparisons(expression : Expr) -> Int {
  match expression {
    Constant(_) | Present(_) => 0
    Compare(_, _, _) => 1
    Not(inner) => expression_comparisons(inner)
    And(left, right) | Or(left, right) =>
      expression_comparisons(left) + expression_comparisons(right)
  }
}

///|
/// Fold boolean constants, duplicate branches, and double negation without
/// changing three-valued semantics.
pub fn Expr::simplify(self : Expr) -> Expr {
  match self {
    Constant(_) | Compare(_, _, _) | Present(_) => self
    Not(inner) => {
      let child = inner.simplify()
      match child {
        Constant(value) => Constant(value.not())
        Not(grandchild) => grandchild.simplify()
        _ => Not(child)
      }
    }
    And(left, right) => {
      let a = left.simplify()
      let b = right.simplify()
      if a == b {
        a
      } else {
        match (a, b) {
          (Constant(No), _) | (_, Constant(No)) => Constant(No)
          (Constant(Yes), other) | (other, Constant(Yes)) => other
          (Constant(Unknown), Constant(Unknown)) => Constant(Unknown)
          _ => And(a, b)
        }
      }
    }
    Or(left, right) => {
      let a = left.simplify()
      let b = right.simplify()
      if a == b {
        a
      } else {
        match (a, b) {
          (Constant(Yes), _) | (_, Constant(Yes)) => Constant(Yes)
          (Constant(No), other) | (other, Constant(No)) => other
          (Constant(Unknown), Constant(Unknown)) => Constant(Unknown)
          _ => Or(a, b)
        }
      }
    }
  }
}

///|
/// Convert to negation-normal form, leaving `not` only directly above atomic
/// predicates. This is useful for rule editors and visualizers.
pub fn Expr::to_nnf(self : Expr) -> Expr {
  push_negation(self, false).simplify()
}

///|
fn push_negation(expression : Expr, negated : Bool) -> Expr {
  match expression {
    Constant(value) => Constant(if negated { value.not() } else { value })
    Compare(_, _, _) | Present(_) =>
      if negated {
        Not(expression)
      } else {
        expression
      }
    Not(inner) => push_negation(inner, !negated)
    And(left, right) =>
      if negated {
        Or(push_negation(left, true), push_negation(right, true))
      } else {
        And(push_negation(left, false), push_negation(right, false))
      }
    Or(left, right) =>
      if negated {
        And(push_negation(left, true), push_negation(right, true))
      } else {
        Or(push_negation(left, false), push_negation(right, false))
      }
  }
}

///|
/// Partially evaluate all predicates that reference a supplied feature.
pub fn Expr::substitute(self : Expr, name : String, value : Value) -> Expr {
  match self {
    Constant(_) => self
    Compare(feature_name, op, expected) =>
      if feature_name == name {
        Constant(evaluate(self, [{ name, value }]).truth)
      } else {
        Compare(feature_name, op, expected)
      }
    Present(feature_name) =>
      if feature_name == name {
        Constant(Yes)
      } else {
        Present(feature_name)
      }
    Not(inner) => Not(inner.substitute(name, value)).simplify()
    And(left, right) =>
      And(left.substitute(name, value), right.substitute(name, value)).simplify()
    Or(left, right) =>
      Or(left.substitute(name, value), right.substitute(name, value)).simplify()
  }
}

///|
pub fn Policy::unused_features(self : Policy) -> Array[String] {
  let used = self.goal.stats().variables
  let result : Array[String] = []
  for item in self.features {
    if !used.contains(item.name) {
      result.push(item.name)
    }
  }
  result
}

///|
pub(all) enum LintSeverity {
  Info
  Warning
} derive(Debug, Eq)

///|
pub(all) struct LintFinding {
  code : String
  severity : LintSeverity
  message : String
  feature : String?
} derive(Debug, Eq)

///|
pub fn Policy::lint(
  self : Policy,
  table_limit? : Int = 1024,
) -> Array[LintFinding] {
  let findings : Array[LintFinding] = []
  for name in self.unused_features() {
    findings.push({
      code: "L_UNUSED_FEATURE",
      severity: Warning,
      message: "feature '\{name}' is declared but never referenced by the goal",
      feature: Some(name),
    })
  }
  for item in self.features {
    if item.locked && item.domain.length() > 1 {
      findings.push({
        code: "L_LOCKED_DOMAIN",
        severity: Info,
        message: "locked feature '\{item.name}' has alternatives that planning will not use",
        feature: Some(item.name),
      })
    }
    if !item.locked && item.cost == 0 && item.domain.length() > 1 {
      findings.push({
        code: "L_ZERO_COST",
        severity: Info,
        message: "mutable feature '\{item.name}' can change at zero cost",
        feature: Some(item.name),
      })
    }
    for index, value in item.domain {
      for previous in 0.. ()
    Ok(table) if !table.truncated =>
      if table.count(Yes) == 0 {
        findings.push({
          code: "L_NEVER_TRUE",
          severity: Warning,
          message: "goal is never true in the declared feasible domains",
          feature: None,
        })
      } else if table.count(No) == 0 && table.count(Unknown) == 0 {
        findings.push({
          code: "L_ALWAYS_TRUE",
          severity: Info,
          message: "goal is true for every feasible combination",
          feature: None,
        })
      }
    _ => ()
  }
  findings
}