///|
/// The interpreter: Chapter 4's rules, rule by rule.
///
/// Every `///|` block below names the rules it implements, so that the spec
/// and the code can be read side by side.
///
/// The state is small on purpose. A run needs somewhere to put what `print`
/// writes, the program's modules, the argument vector, and one thing the spec
/// does not have: a cache of loaded modules. The spec says loading is
/// deterministic and needs no cache, which is true of the VALUES; it is not
/// true of the output, and a module that prints when it loads would print
/// twice under two imports of it. CPython prints once, and CPython is the
/// oracle for what a run prints, so the cache is here and changes nothing
/// else.
using @value {
  type Value,
  type Env,
  type Outcome,
  type StmtResult,
  type MatchResult,
  type Termination,
}

///|
pub struct Interp {
  tree : @program.SourceTree
  host : Host
  /// Module name to the environment it loaded to, for this run only.
  loaded : Map[String, Env]
  /// Module names being loaded, to name a cycle rather than hang. Program
  /// well-formedness rules cycles out, so this only fires when `run` is
  /// asked for a program nobody checked.
  loading : Array[String]
  /// How deep the call stack is, and how deep it may go.
  ///
  /// The semantics allows a program not to terminate, and an infinite
  /// recursion is one that does not; but an evaluator that recurses on the
  /// machine stack meets a stack overflow rather than running forever. The
  /// limit turns that into an answer -- an operation the semantics does not
  /// cover -- which a person can read.
  mut depth : Int
  max_depth : Int
  /// How many machine steps are left, and how many there were.
  ///
  /// `max_depth` bounds a runaway that recurses; this bounds one that does
  /// not. A comprehension over a long sequence is the shape that needs it:
  /// it loops without recursing, so nothing else stops it.
  mut fuel : Int
  max_steps : Int
  /// The superset of PurePy this run's program was accepted under.
  ///
  /// The evaluator reads it in one place: which values `builtins` loads to. A
  /// profile is not a mode the semantics is in -- every rule below applies to
  /// every run -- it decides what was in scope to be written in the first
  /// place, and the checker has to have agreed about the same set or a name
  /// would type-check and then not be there.
  profile : @profile.Profile
  /// The module whose source is running right now.
  ///
  /// Not the top of `loading`: that is the IMPORT stack, and during a call
  /// into an imported function it still names the importer. This is set from
  /// the module body being loaded and from the callee's closure, and restored
  /// after, so it always names the module the current expression was written
  /// in.
  mut in_module : String
  /// Where the run's first abort happened, once one has.
  ///
  /// First write wins, and nothing ever clears it. That is sound because
  /// `try`/`except` is not PurePy: an abort is never caught, so the first one
  /// constructed is the one the run ends with. It is read only when the run
  /// ends `Terminated`, which is why a pattern that swallows an abort into
  /// `MatchStuck` can leave a value here that nobody looks at.
  mut abort_at : Site?
}

///|
/// Where an abort happened: the module, and the span within it.
///
/// The specification says an implementation "must agree on which kind a run
/// yields, though how it reports one is not prescribed"
/// (`operational-semantics.tex`). This is reporting, then, and not semantics:
/// a `Site` never changes which `Termination` a run yields, and two runs that
/// abort at different places with the same kind still agree.
pub(all) struct Site {
  in_module : String
  span : @basic.Span
} derive(Eq, Debug)

///|
/// `module:line:col`, the site as a person reads it.
pub fn Site::to_display(self : Site) -> String {
  "\{self.in_module}:\{self.span.start.to_display()}"
}

///|
/// Record where an abort happened, if nothing earlier has.
///
/// First write wins, so the INNERMOST construct to abort claims the site and
/// nothing enclosing it can take the site away: in `a + f(b)`, the call and
/// not the sum. That is the expression a person would point at.
///
/// Callers test for an abort before they compute a span, so a construct that
/// yields a value costs one tag test and nothing else. That matters:
/// `eval_expr` is the hottest path there is.
fn Interp::record(self : Interp, span : @basic.Span) -> Unit {
  if self.abort_at is None && span != @basic.nowhere {
    self.abort_at = Some({ in_module: self.in_module, span, })
  }
}

///|
/// `record`, for an outcome that may or may not have aborted.
///
/// A span is computed only when there is an abort, so an expression that
/// yields a value costs one tag test.
fn Interp::sited(self : Interp, e : @ast.Expr, o : Outcome) -> Outcome {
  if o is Aborts(_) {
    self.record(e.span())
  }
  o
}

///|
pub fn Interp::new(
  tree : @program.SourceTree,
  host? : Host = Host::new(),
  max_depth? : Int = default_max_depth,
  profile? : @profile.Profile = @profile.core,
  max_steps? : Int = default_max_steps,
) -> Interp {
  {
    tree,
    host,
    loaded: Map([]),
    loading: [],
    depth: 0,
    max_depth,
    fuel: max_steps,
    max_steps,
    profile,
    in_module: "__main__",
    abort_at: None,
  }
}

///|
/// Charge `n` steps for something a single move is about to build.
///
/// The driver charges one step per move, which bounds a guest that loops. It
/// does not bound one that asks a single move to build a very large value --
/// `range(10 ** 9)`, `[0] * 10 ** 9` -- because those are one move each.
/// Cost is the size of what they build, and it is charged BEFORE they build
/// it, so the answer is a limit that was reached rather than a host that ran
/// out of memory.
///
/// Answers whether there was enough.
fn Interp::spend(self : Interp, n : BigInt) -> Bool {
  if n <= 0N {
    return true
  }
  if n > BigInt::from_int(self.fuel) {
    self.fuel = 0
    return false
  }
  self.fuel -= n.to_int()
  true
}

///|
fn Interp::write(self : Interp, text : String) -> Unit {
  (self.host.write)(text)
}

// ---------------------------------------------------------------------------
// The predefined modules (Figure 2.7)

///|
/// The environment a predefined module loads to, or `None` if `q` is not one.
///
/// `typing` exposes `Any` alone. Figure 2.7 also lists `Callable`; the
/// reference checker does not, and the signature and the environment have to
/// agree or a from-import would type-check and then fail to run.
///
/// The host's redefinitions are laid over the result and not mixed into it,
/// for which see `Interp::redefine`.
pub fn Interp::predefined(self : Interp, q : String) -> Env? {
  let entries : Array[(String, Value)] = [("__name__", Str(q))]
  match q {
    "builtins" => {
      entries.push(("print", Prim(Print)))
      entries.push(("len", Prim(Len)))
      entries.push(("range", Prim(Range)))
      // In the order of `@context.extra_builtin_names`, which the checker
      // reads. `predefined_wbtest.mbt` is what keeps the two from drifting.
      if self.profile.has(ExtraBuiltins) {
        for e in extra_builtins() {
          entries.push(e)
        }
      }
    }
    "math" => {
      entries.push(("pi", Float(3.141592653589793)))
      entries.push(("e", Float(2.718281828459045)))
      entries.push(("sqrt", Prim(Sqrt)))
      entries.push(("exp", Prim(Exp)))
      entries.push(("log", Prim(Log)))
      entries.push(("sin", Prim(Sin)))
      entries.push(("cos", Prim(Cos)))
      entries.push(("tan", Prim(Tan)))
      entries.push(("floor", Prim(MathFloor)))
      entries.push(("ceil", Prim(MathCeil)))
    }
    "sys" => {
      entries.push(("argv", List(self.host.argv.map(fn(a) { Value::Str(a) }))))
      entries.push(("exit", Prim(Exit)))
    }
    "typing" => entries.push(("Any", Prim(Opaque("Any"))))
    "dataclasses" => entries.push(("dataclass", Prim(Opaque("dataclass"))))
    _ => return None
  }
  Some(self.redefine(q, @value.env_of(entries)))
}

///|
/// What the host put in `q` instead of what the specification has.
///
/// Laid OVER the environment with `override_env`, and never appended to the
/// entries it was built from. `@value.env_of` resolves a duplicate key by
/// keeping the FIRST -- `hash_map_from_array_by_add` folds the array backwards
/// -- and past sixty-four entries builds by another path entirely, so a
/// redefinition pushed onto `entries` would lose, and lose differently on
/// either side of a length nobody would think to test. `override_env` is `add`
/// per key and says what it means.
///
/// A key that names no module, or a member the module does not have, binds a
/// name the checker has never heard of: no well-formed program can reach it,
/// so it is not an error here. `Host::unknown_redefinitions` is where a host
/// finds out.
fn Interp::redefine(self : Interp, q : String, env : Env) -> Env {
  if self.host.redefined.is_empty() {
    return env
  }
  let mine : Array[(String, Value)] = []
  for name, v in self.host.redefined {
    // No predefined module's name has a dot in it, so the first is the one.
    if name.split_once(".") is Some((mod_name, within)) && mod_name == q {
      mine.push((within.to_owned(), v))
    }
  }
  if mine.is_empty() {
    env
  } else {
    @value.override_env(env, @value.env_of(mine))
  }
}

///|
/// The values of `@context.extra_builtin_names`, in that order.
///
/// A free function and not a method: it depends on nothing about a run, and
/// keeping it beside `Interp::predefined` is what makes the two lists easy to
/// read against each other. `lib/eval/predefined_wbtest.mbt` is what makes
/// them stay that way.
fn extra_builtins() -> Array[(String, Value)] {
  [
    ("abs", Prim(Abs)),
    ("all", Prim(All)),
    ("any", Prim(Any)),
    ("divmod", Prim(DivMod)),
    ("enumerate", Prim(Enumerate)),
    ("float", Prim(ToFloat)),
    ("int", Prim(ToInt)),
    ("list", Prim(ToList)),
    ("max", Prim(Max)),
    ("min", Prim(Min)),
    ("repr", Prim(Repr)),
    ("reversed", Prim(Reversed)),
    ("round", Prim(Round)),
    ("sorted", Prim(Sorted)),
    ("str", Prim(ToStr)),
    ("sum", Prim(Sum)),
    ("tuple", Prim(ToTuple)),
    ("zip", Prim(Zip)),
  ]
}