///|
/// Evaluate IfThenElse
fn eval_if_then_else(
  cond : Expr,
  then_expr : Expr,
  else_expr : Expr,
  input : Json,
  env : Env,
) -> Iter[Json] raise InterpreterError {
  // jq evaluates a branch for every output of the condition, so
  // `if empty then a else b end` produces nothing.
  let results : Array[Json] = []
  for c in eval_with_env(cond, input, env).collect() {
    let branch = if @ast_internal.is_truthy(c) { then_expr } else { else_expr }
    for v in eval_with_env(branch, input, env) {
      results.push(v)
    }
  }
  results.iter()
}

///|
/// Evaluate TryCatch
fn eval_try_catch(
  try_expr : Expr,
  catch_opt : Expr?,
  input : Json,
  env : Env,
) -> Iter[Json] raise InterpreterError {
  eval_with_env(try_expr, input, env) catch {
    _ =>
      match catch_opt {
        Some(catch_expr) => eval_with_env(catch_expr, input, env)
        None => Iter::empty()
      }
  }
}

///|
/// Evaluate Alternative
fn eval_alternative(
  left : Expr,
  right : Expr,
  input : Json,
  env : Env,
) -> Iter[Json] raise InterpreterError {
  // jq 1.7: `a // b` yields every output of `a` that is neither false nor
  // null, or the outputs of `b` if there are none. Errors raised by `a`
  // propagate (jq 1.7.1: `[error("x") // 3]` is an error).
  let left_results = eval_with_env(left, input, env).collect()
  let truthy = left_results.filter(@ast_internal.is_truthy)
  if truthy.is_empty() {
    eval_with_env(right, input, env)
  } else {
    truthy.iter()
  }
}

///|
/// Evaluate Limit
fn eval_limit(
  n : Int,
  expr : Expr,
  input : Json,
  env : Env,
) -> Iter[Json] raise InterpreterError {
  eval_with_env(expr, input, env).take(n)
}

///|
/// Evaluate Until
fn eval_until(
  cond_expr : Expr,
  update_expr : Expr,
  input : Json,
  env : Env,
) -> Iter[Json] raise InterpreterError {
  let result = for current = input {
    let cond_results = eval_with_env(cond_expr, current, env).collect()
    match cond_results {
      [] => break current
      [True, ..] => break current
      _ => {
        let update_results = eval_with_env(update_expr, current, env).collect()
        match update_results {
          [] => break current
          [next, ..] => continue next
        }
      }
    }
  } where {
    proof_invariant: true,
    proof_reasoning: (
      #|`current` is always the initial input or the first value produced by
      #|the update expression. Each iteration either breaks immediately or
      #|continues with that next value; jq `until` may intentionally diverge
      #|when neither the condition nor the update causes termination.
    ),
  }
  Iter::singleton(result)
}

///|
/// Evaluate While
fn eval_while(
  cond_expr : Expr,
  update_expr : Expr,
  input : Json,
  env : Env,
) -> Iter[Json] raise InterpreterError {
  let results : Array[Json] = []
  let mut current = input
  while true {
    let cond_results = eval_with_env(cond_expr, current, env).collect()
    match cond_results {
      [] => break
      [first, ..] =>
        if !@ast_internal.is_truthy(first) {
          break
        } else {
          results.push(current)
          let update_results = eval_with_env(update_expr, current, env).collect()
          match update_results {
            [] => break
            [next, ..] => current = next
          }
        }
    }
  }
  results.iter()
}