///|
pub fn Plan::to_markdown(self : Plan) -> String {
  let out = StringBuilder::new()
  out.write_string("# FlipSpec repair plan: \{self.policy_name}\n\n")
  out.write_string("- Current outcome: **\{self.baseline.render()}**\n")
  out.write_string("- Target outcome: **\{self.target.render()}**\n")
  out.write_string("- Assignments evaluated: \{self.evaluated}\n")
  out.write_string("- Search truncated: \{self.truncated}\n\n")
  if self.repairs.is_empty() {
    out.write_string(
      "No feasible repair was found inside the declared domains.\n",
    )
    return out.to_string()
  }
  for index, repair in self.repairs {
    out.write_string("## Repair \{index + 1} — cost \{repair.cost}\n\n")
    for change in repair.changes {
      out.write_string(
        "- `\{change.feature}`: \{change.from.render()} → \{change.to.render()} (cost \{change.cost})\n",
      )
    }
    out.write_string("\nResult: **\{repair.result.render()}**\n\n")
  }
  out.to_string()
}

///|
pub fn Plan::to_json(self : Plan) -> String {
  let out = StringBuilder::new()
  out.write_string("{")
  out.write_string("\"policy\":\"\{json_escape(self.policy_name)}\",")
  out.write_string("\"baseline\":\"\{self.baseline.render()}\",")
  out.write_string("\"target\":\"\{self.target.render()}\",")
  out.write_string("\"evaluated\":\{self.evaluated},")
  out.write_string("\"truncated\":\{self.truncated},")
  out.write_string("\"repairs\":[")
  for index, repair in self.repairs {
    if index > 0 {
      out.write_char(',')
    }
    out.write_string(
      "{\"cost\":\{repair.cost},\"result\":\"\{repair.result.render()}\",\"changes\":[",
    )
    for change_index, change in repair.changes {
      if change_index > 0 {
        out.write_char(',')
      }
      out.write_string("{")
      out.write_string("\"feature\":\"\{json_escape(change.feature)}\",")
      out.write_string("\"from\":\"\{json_escape(change.from.plain())}\",")
      out.write_string("\"to\":\"\{json_escape(change.to.plain())}\",")
      out.write_string("\"cost\":\{change.cost}")
      out.write_char('}')
    }
    out.write_string("]}")
  }
  out.write_string("]}")
  out.to_string()
}

///|
pub fn PlanCertificate::to_markdown(self : PlanCertificate) -> String {
  let out = StringBuilder::new()
  out.write_string("# FlipSpec minimality certificate: \{self.policy_name}\n\n")
  out.write_string("- Status: **\{self.status}**\n")
  out.write_string("- Current outcome: **\{self.baseline.render()}**\n")
  out.write_string("- Target outcome: **\{self.target.render()}**\n")
  out.write_string("- Domain assignments: \{self.domain_points}\n")
  out.write_string("- Assignments evaluated: \{self.assignments_evaluated}\n")
  out.write_string("- Search exhaustive: \{self.search_exhaustive}\n")
  out.write_string("- Output truncated: \{self.output_truncated}\n")
  if self.has_repair {
    out.write_string("- Best repair cost: \{self.best_cost}\n")
  } else {
    out.write_string("- Best repair cost: none\n")
  }
  out.write_string(
    "- Lower-cost repair excluded: \{self.lower_cost_excluded}\n\n",
  )
  if self.status == "minimum-certified" {
    out.write_string(
      "Every declared assignment was evaluated, and no lower-cost assignment flipped the decision.\n",
    )
  } else if self.status == "no-feasible-repair" {
    out.write_string(
      "Every declared assignment was evaluated, and none reached the target outcome.\n",
    )
  } else if self.status == "policy-mismatch" {
    out.write_string(
      "The plan does not match the policy used for certification. Recompute the plan before reviewing it.\n",
    )
  } else {
    out.write_string(
      "The result is useful as a bounded search artifact, but minimality is not certified.\n",
    )
  }
  out.to_string()
}

///|
pub fn PlanCertificate::to_json(self : PlanCertificate) -> String {
  let out = StringBuilder::new()
  out.write_string("{")
  out.write_string("\"policy\":\"\{json_escape(self.policy_name)}\",")
  out.write_string("\"status\":\"\{json_escape(self.status)}\",")
  out.write_string("\"baseline\":\"\{self.baseline.render()}\",")
  out.write_string("\"target\":\"\{self.target.render()}\",")
  out.write_string("\"domain_points\":\{self.domain_points},")
  out.write_string("\"assignments_evaluated\":\{self.assignments_evaluated},")
  out.write_string("\"search_exhaustive\":\{self.search_exhaustive},")
  out.write_string("\"output_truncated\":\{self.output_truncated},")
  out.write_string("\"has_repair\":\{self.has_repair},")
  out.write_string("\"best_cost\":\{self.best_cost},")
  out.write_string("\"lower_cost_excluded\":\{self.lower_cost_excluded}")
  out.write_string("}")
  out.to_string()
}

///|
pub fn Trace::to_mermaid(self : Trace) -> String {
  let out = StringBuilder::new()
  out.write_string("flowchart TD\n")
  let counter = [0]
  append_mermaid_trace(self, out, counter, -1)
  out.to_string()
}

///|
fn append_mermaid_trace(
  trace : Trace,
  out : StringBuilder,
  counter : Array[Int],
  parent : Int,
) -> Unit {
  let id = counter[0]
  counter[0] = counter[0] + 1
  let label = json_escape("\{trace.truth.render()}: \{trace.expression}")
  out.write_string("  n\{id}[\"\{label}\"]\n")
  if parent >= 0 {
    out.write_string("  n\{parent} --> n\{id}\n")
  }
  for child in trace.children {
    append_mermaid_trace(child, out, counter, id)
  }
}

///|
fn json_escape(text : String) -> String {
  let out = StringBuilder::new()
  for ch in text {
    match ch {
      '"' => out.write_string("\\\"")
      '\\' => out.write_string("\\\\")
      '\n' => out.write_string("\\n")
      '\r' => out.write_string("\\r")
      '\t' => out.write_string("\\t")
      _ => out.write_char(ch)
    }
  }
  out.to_string()
}