///|
/// A recursively explainable evaluation node.
pub(all) struct Trace {
  expression : String
  truth : Truth
  reason : String
  children : Array[Trace]
} derive(Debug, Eq)

///|
pub(all) struct Evaluation {
  truth : Truth
  trace : Trace
} derive(Debug, Eq)

///|
pub fn evaluate(expression : Expr, environment : Environment) -> Evaluation {
  let trace = evaluate_trace(expression, environment)
  { truth: trace.truth, trace }
}

///|
pub fn Policy::evaluate(self : Policy) -> Evaluation {
  evaluate(self.goal, self.environment())
}

///|
fn evaluate_trace(expression : Expr, environment : Environment) -> Trace {
  match expression {
    Constant(value) =>
      {
        expression: value.render(),
        truth: value,
        reason: "literal truth value",
        children: [],
      }
    Present(name) => {
      let result = match environment_get(environment, name) {
        Some(_) => Yes
        None => No
      }
      {
        expression: "present(\{name})",
        truth: result,
        reason: if result == Yes {
          "feature is present"
        } else {
          "feature is missing"
        },
        children: [],
      }
    }
    Compare(name, op, expected) =>
      match environment_get(environment, name) {
        None =>
          {
            expression: expression.render(),
            truth: Unknown,
            reason: "feature '\{name}' is missing",
            children: [],
          }
        Some(actual) => {
          let result = compare_values(actual, op, expected)
          {
            expression: expression.render(),
            truth: result,
            reason: if result == Unknown {
              "cannot compare \{actual.kind()} with \{expected.kind()}"
            } else {
              "actual value is \{actual.render()}"
            },
            children: [],
          }
        }
      }
    Not(inner) => {
      let child = evaluate_trace(inner, environment)
      {
        expression: expression.render(),
        truth: child.truth.not(),
        reason: "logical negation",
        children: [child],
      }
    }
    And(left, right) => {
      let left_trace = evaluate_trace(left, environment)
      let right_trace = evaluate_trace(right, environment)
      let result = left_trace.truth.conjunction(right_trace.truth)
      {
        expression: expression.render(),
        truth: result,
        reason: and_reason(left_trace.truth, right_trace.truth),
        children: [left_trace, right_trace],
      }
    }
    Or(left, right) => {
      let left_trace = evaluate_trace(left, environment)
      let right_trace = evaluate_trace(right, environment)
      let result = left_trace.truth.disjunction(right_trace.truth)
      {
        expression: expression.render(),
        truth: result,
        reason: or_reason(left_trace.truth, right_trace.truth),
        children: [left_trace, right_trace],
      }
    }
  }
}

///|
fn and_reason(left : Truth, right : Truth) -> String {
  match (left, right) {
    (No, No) => "both requirements fail"
    (No, _) => "left requirement fails"
    (_, No) => "right requirement fails"
    (Yes, Yes) => "both requirements pass"
    _ => "at least one requirement is unknown"
  }
}

///|
fn or_reason(left : Truth, right : Truth) -> String {
  match (left, right) {
    (Yes, Yes) => "both alternatives pass"
    (Yes, _) => "left alternative passes"
    (_, Yes) => "right alternative passes"
    (No, No) => "both alternatives fail"
    _ => "no alternative passes and at least one is unknown"
  }
}

///|
fn compare_values(actual : Value, op : CompareOp, expected : Value) -> Truth {
  match (actual, expected) {
    (Integer(left), Integer(right)) => truth_from_order(left.compare(right), op)
    (Text(left), Text(right)) => truth_from_order(left.compare(right), op)
    (Boolean(left), Boolean(right)) => {
      let equal = left == right
      match op {
        Equal => if equal { Yes } else { No }
        NotEqual => if equal { No } else { Yes }
        _ => Unknown
      }
    }
    _ => Unknown
  }
}

///|
fn truth_from_order(order : Int, op : CompareOp) -> Truth {
  let result = match op {
    Equal => order == 0
    NotEqual => order != 0
    Less => order < 0
    LessEqual => order <= 0
    Greater => order > 0
    GreaterEqual => order >= 0
  }
  if result {
    Yes
  } else {
    No
  }
}

///|
/// A compact multi-line explanation suited to terminals and log files.
pub fn Trace::to_text(self : Trace) -> String {
  let out = StringBuilder::new()
  append_trace_text(self, out, 0)
  out.to_string()
}

///|
fn append_trace_text(trace : Trace, out : StringBuilder, depth : Int) -> Unit {
  out.write_string("  ".repeat(depth))
  out.write_string(
    "[\{trace.truth.render()}] \{trace.expression} — \{trace.reason}\n",
  )
  for child in trace.children {
    append_trace_text(child, out, depth + 1)
  }
}