# check_state.ludic — 0.S: what a state parameter allows. `h: mut Hiker` may change the state;
# `h: Hiker` may only read it - an assignment whose target starts at it (`h.hips = 1`,
# `h.list[i] = x`), a push onto something in it, or passing it where a `mut Hiker` is wanted is
# refused. A module-level `let` (and a const, a registry, a state's own instance) is immutable all
# the way down: the same writes starting at one are refused. A reference read out of either into a
# local (`let l = h.list`, `let r = TABLE[0]`) carries the same rule: a write through it is refused.
var ck_ro: []int = new []int            # parallel to ck_names: 1 for a read-only state
var ck_alias: []Node = new []Node       # parallel to ck_names: the global a local's reference came from
var ck_ro_st: []pointer = new []pointer # parallel to ck_names: the state that makes a local read-only
var ck_from_st: []pointer = new []pointer  # parallel to ck_names: the state a local's reference came out of, mut or not

function ck_set_ro(ro: bool) -> void {
  let k = ck_top - 1
  while len(ck_ro) < len(ck_names) { push(ck_ro, 0) }
  while len(ck_alias) < len(ck_names) { push(ck_alias, null) }
  while len(ck_ro_st) < len(ck_names) { push(ck_ro_st, null) }
  while len(ck_from_st) < len(ck_names) { push(ck_from_st, null) }
  if ro { ck_ro[k] = 1 } else { ck_ro[k] = 0 }
  ck_alias[k] = null
  ck_ro_st[k] = null
  ck_from_st[k] = null
  if is_state_ty(ck_tys[k]) { ck_from_st[k] = ck_tys[k] }
  if ro { ck_ro_st[k] = ck_tys[k] }
}
# the local just bound is read-only for the same state as local `li`
function ck_ro_like(li: int) -> void {
  let k = ck_top - 1
  ck_ro[k] = 1
  ck_ro_st[k] = ck_ro_st[li]
}
# a value, not a reference: nothing can be written through it
function ck_scalar(t: pointer) -> bool {
  if t == null or (t == "?") or (t == "int") or (t == "float") or (t == "fixed") or (t == "long") { return true }
  if (t == "bool") or (t == "string") or (t == "byte") or (t == "pointer") { return true }
  if is_fn_type(t) { return true }
  return find_enum(t) != null
}
# `let l = <e>` just bound at the top: a reference out of a read-only state is read-only, and one out
# of a global is that global's (a write through it writes the global)
function ck_let_from(e: Node, ty: pointer) -> void {
  if e == null or ck_scalar(ty) { return }
  let r = ck_chain_root(e)
  if r == null { return }
  let k = ck_top - 1
  let li = ck_local(r.s)
  if li >= 0 and li < k {
    if ck_is_ro(li) { ck_ro_like(li) }
    if li < len(ck_alias) { ck_alias[k] = ck_alias[li] }
    if li < len(ck_from_st) and k < len(ck_from_st) { ck_from_st[k] = ck_from_st[li] }
    return
  }
  if li >= 0 { return }
  var g = ck_global(r.s)
  if g == null { g = mg_field_var(r.s) }
  if g != null and g.kind == N_VAR { ck_alias[k] = g }
}
function ck_is_ro(li: int) -> bool {
  if li < 0 or li >= len(ck_ro) { return false }
  return ck_ro[li] == 1
}
# the name an assignment's target starts at: `a` in `a.b[c].d`
function ck_chain_root(t: Node) -> Node {
  var n = t
  while n != null and (n.kind == E_INDEX or n.kind == E_MEMBER) { n = n.a }
  if n == null or n.kind != E_ID { return null }
  return n
}
function ck_module_let(g: Node) -> bool {
  if g == null { return false }
  if g.kind == N_CONST { return true }
  if g.kind != N_VAR { return false }
  if g.uns == 1 { return true }
  return reg_find(g.s) >= 0
}
# a write into `t`: refused when it starts at a read-only state or at a module-level binding
function ck_write_check(t: Node, what: pointer) -> void {
  let r = ck_chain_root(t)
  if r == null { return }
  let li = ck_local(r.s)
  if li >= 0 {
    mg_local_write(ck_tys[li])                   # 0.S2 --migrate-prune: a state changed here
    if li < len(ck_ro_st) { mg_local_write(ck_ro_st[li]) }
    if li < len(ck_from_st) and ck_from_st[li] != null { mg_local_write(ck_from_st[li]) }   # through a local holding part of it
    if li < len(ck_alias) and ck_alias[li] != null {
      let ag = ck_alias[li]
      mg_write(t, ag)
      if ck_module_let(ag) { ck_err("state", t, `{what}: {r.s} holds part of {mg_src_name(ag.s)}, which is module-level and immutable all the way down`) }
    }
    if ck_is_ro(li) and g_migrate and g_mg_cur >= 0 and ck_ro_st[li] != null {
      mg_need(g_mg_cur, mg_state_named(ck_ro_st[li]), true)   # 0.S2: it becomes `mut`
      return
    }
    if ck_is_ro(li) and li < len(ck_ro_st) and ck_ro_st[li] != null and not (ck_ro_st[li] == ck_tys[li]) {
      ck_err("state", t, `{what}: {r.s} holds part of a read-only {ck_ro_st[li]}; take the state as mut {ck_ro_st[li]} to change it`)
      return
    }
    if ck_is_ro(li) {
      ck_err("state", t, `{what}: {r.s} is read-only here ({r.s}: {ck_tys[li]}); take it as {r.s}: mut {ck_tys[li]} to change it`)
    }
    return
  }
  var g = ck_global(r.s)
  if g == null { g = mg_field_var(r.s) }
  mg_write(t, g)
  if ck_module_let(g) {
    var name = r.s
    if is_state_ty(g.ty) and g.uns == 1 { name = `the state {g.ty}` }
    ck_err("state", t, `{what}: {name} is module-level and immutable all the way down; changing data belongs in a state, passed as a mut parameter`)
  }
}
# a function's parameters: `mut` is for a state (or a table's row, 27.3), and a state without it is
# read-only
function ck_bind_param(p: Node) -> void {
  ck_bind(p.s, p.ty)
  if p.uns == 1 and not is_state_ty(p.ty) and not rr_is_row_ty(p.ty) {
    ck_err("state", p, `{p.s}: mut {p.ty} - mut is for a state parameter (or a row, mut Row<T>), and {p.ty} is not a state`)
  }
  ck_set_ro(is_state_ty(p.ty) and p.uns == 0)
}
# a call's arguments against the function's state parameters: a read-only state is not a mut one
function ck_state_args(e: Node, f: Node) -> void {
  var k = 0
  var i = 0
  while i < len(f.kids) {
    let p = f.kids[i]
    if p.kind == N_PARAM {
      if p.uns == 1 and is_state_ty(p.ty) and k < len(e.kids) {
        let a = e.kids[k]
        if a.kind == E_ID {
          let li = ck_local(a.s)
          if li >= 0 and ck_is_ro(li) {
            ck_err("state", a, `{f.s} changes {p.ty} ({p.s}: mut {p.ty}), and {a.s} is read-only here`)
          }
        }
      }
      k += 1
    }
    i += 1
  }
}
# a C function is handed what it may change: a state an argument comes out of keeps the mutability
# it was declared with, so --tighten leaves the mut on a wrapper writing through a native handle
function ck_extern_writes(e: Node) -> void {
  var i = 0
  while i < len(e.kids) {
    var a = e.kids[i]
    if a.kind == E_FINIT { a = a.a }
    let r = ck_chain_root(a)
    if r != null {
      let li = ck_local(r.s)
      if li >= 0 and li < len(ck_from_st) and ck_from_st[li] != null and not ck_is_ro(li) { mg_local_write(ck_from_st[li]) }
    }
    i += 1
  }
}