open Values
open Contexts
open InterpreterUtils
open InterpreterLoopsCore

(** Repeat until we can't simplify the context anymore:
   - explore the fresh anonymous values and replace all the values which are not
     borrows/loans with ⊥
   - also end the borrows which appear in fresh anonymous values and don't contain loans
   - end the fresh region abstractions which can be ended (no loans)

   Inputs:
   - config
   - fixed ids (the fixeds ids are the ids we consider as non-fresh)
 *)
val cleanup_fresh_values_and_abs : config -> Meta.span -> ids_sets -> Cps.cm_fun

(** Prepare the shared loans in the abstractions by moving them to fresh
    abstractions.

    We use this to prepare an evaluation context before computing a fixed point.

    Because a loop iteration might lead to symbolic value expansions and create
    shared loans in shared values inside the *fixed* abstractions, which we want
    to leave unchanged, we introduce some reborrows in the following way:

    {[
      abs'0 { SL {l0, l1} s0 }
      l0 -> SB l0
      l1 -> SB l1

        ~~>

      abs'0 { SL {l0, l1} s0 }
      l0 -> SB l2
      l1 -> SB l3
      abs'2 { SB l0, SL {l2} s2 }
      abs'3 { SB l1, SL {l3} s3 }
    ]}

    This is sound but leads to information loss. This way, the fixed abstraction
    [abs'0] is never modified because [s0] is never accessed (and thus never
    expanded).

    We do this because it makes it easier to compute joins and fixed points.

    **REMARK**:
    As a side note, we only reborrow the loan ids whose corresponding borrows
    appear in values (i.e., not in abstractions).

    For instance, if we have:
    {[
      abs'0 {
        SL {l0} s0
        SL {l1} s1
      }
      abs'1 { SB l0 }
      x -> SB l1
    ]}

    we only introduce a fresh abstraction for [l1].
  *)
val prepare_ashared_loans : Meta.span -> loop_id option -> Cps.cm_fun

(** Compute a fixed-point for the context at the entry of the loop.
    We also return:
    - the sets of fixed ids
    - the map from region group id to the corresponding abstraction appearing
      in the fixed point (this is useful to compute the return type of the loop
      backward functions for instance).
      Note that this is a partial map: the loop doesn't necessarily introduce
      an abstraction for each input region of the function.

    Rem.: the list of symbolic values should be computable by simply exploring
    the fixed point environment and listing all the symbolic values we find.
    In the future, we might want to do something more precise, by listing only
    the values which are read or modified (some symbolic values may be ignored).
 *)
val compute_loop_entry_fixed_point :
  config ->
  Meta.span ->
  loop_id ->
  (* This function is the function to evaluate the loop body (eval_statement applied
     to the proper arguments). We need to take it as input because [compute_loop_entry_fixed_point]
     is mutually recursive with [eval_statement], but doesn't live in the same module. *)
  Cps.stl_cm_fun ->
  eval_ctx ->
  eval_ctx * ids_sets * AbstractionId.id SymbolicAst.region_group_id_map

(** For the abstractions in the fixed point, compute the correspondance between
    the borrows ids and the loans ids, if we want to introduce equivalent
    identity abstractions (i.e., abstractions which do nothing - the input
    borrows are exactly the output loans).

    **Context:**
    ============
    When we (re-enter) the loop, we want to introduce identity abstractions
    (i.e., abstractions which actually only introduce fresh identifiers for
    some borrows, to abstract away a bit the borrow graph) which have the same
    shape as the abstractions introduced for the fixed point (see the explanations
    for [match_ctx_with_target]). This allows us to transform the environment
    into a fixed point (again, see the explanations for [match_ctx_with_target]).

    In order to introduce those identity abstractions, we need to figure out,
    for those abstractions, which loans should be linked to which borrows.
    We do this in the following way.

    We match the fixed point environment with the environment upon first entry
    in the loop, and exploit the fact that the fixed point was derived by also
    joining this first entry environment: because of that, the borrows in the
    abstractions introduced for the fixed-point actually exist in this first
    environment (they are not fresh). For [list_nth_mut] (see the explanations
    at the top of the file) we have the following:

    {[
      // Environment upon first entry in the loop
      env0 = {
        abs@0 { ML l0 }
        ls -> MB l0 (s2 : loops::List<T>)
        i -> s1 : u32
      }

      // Fixed-point environment
      env_fp = {
        abs@0 { ML l0 }
        ls -> MB l1 (s3 : loops::List<T>)
        i -> s4 : u32
        abs@fp {
          MB l0 // this borrow appears in [env0]
          ML l1
        }
      }
    ]}

    We filter those environments to remove the non-fixed dummy variables,
    abstractions, etc. in a manner similar to [match_ctx_with_target]. We
    get:

    {[
      filtered_env0 = {
        abs@0 { ML l0 }
        ls -> MB l0 (s2 : loops::List<T>)
        i -> s1 : u32
      }

      filtered_env_fp = {
        abs@0 { ML l0 }
        ls -> MB l1 (s3 : loops::List<T>)
        i -> s@ : u32
        // removed abs@fp
      }
    ]}

    We then match [filtered_env_fp] with [filtered_env0], taking care to not
    consider loans and borrows in a disjoint manner, and ignoring the fixed
    values, abstractions, loans, etc. We get:
    {[
      borrows_map: { l1 -> l0 } // because we matched [MB l1 ...] with [MB l0 ...] in [ls]
      loans_map: {} // we ignore abs@0, which is "fixed"
    ]}

    From there we deduce that, if we want to introduce an identity abstraction with the
    shape of [abs@fp], we should link [l1] to [l0]. In other words, the value retrieved
    through the loan [l1] is actually the value which has to be given back to [l0].
 *)
val compute_fixed_point_id_correspondance :
  Meta.span -> ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp

(** Compute the set of "quantified" symbolic value ids in a fixed-point context.

    We compute:
    - the set of symbolic value ids that are freshly introduced
    - the list of input symbolic values
 *)
val compute_fp_ctx_symbolic_values :
  Meta.span ->
  eval_ctx ->
  eval_ctx ->
  symbolic_value_id_set * symbolic_value list