open Errors
module T = Types
module V = Values
module E = Expressions
module A = CfimAst
open SymbolicAst
open ValuesUtils
open InterpreterUtils

type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's

type ended_loan = (V.mvalue, V.mvalue list) ended

type ended_borrow = (V.mvalue, V.mvalue) ended

type ended_loan_or_borrow =
  | EndedLoan of ended_loan
  | EndedBorrow of ended_borrow

(** Return the list of the meta-values given to the top owned ended mutable
    loans/borrows of an abstraction
    
    We expect an abstraction where all the loans/borrows have ended.
 *)
let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list
    =
  (* The accumulator *)
  let acc = ref [] in
  let add x = acc := x :: !acc in
  let add_loan x = add (EndedLoan x) in
  let add_borrow x = add (EndedBorrow x) in
  let add_sloan x = add_loan (EndedSymbolic x) in
  let add_cloan x = add_loan (EndedConcrete x) in
  let add_sborrow x = add_borrow (EndedSymbolic x) in
  let add_cborrow x = add_borrow (EndedConcrete x) in

  (* The visitor *)
  let obj =
    object
      inherit [_] V.iter_abs as super

      method! visit_aproj env aproj =
        match aproj with
        | AEndedProjLoans (msv, []) ->
            (* The symbolic value was left unchanged *)
            add_sloan [ mk_typed_value_from_symbolic_value msv ]
        | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl)
        | AEndedProjBorrows mv -> add_sborrow mv
        | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
            failwith "Unreachable"

      method! visit_aloan_content env lc =
        match lc with
        | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable"
        | AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
            (* Add the meta-value and stop the exploration *)
            add_cloan given_back_meta
        | AEndedSharedLoan (_, _) ->
            (* We don't dive into shared loans: there is nothing to give back
             * inside (note that there could be a mutable borrow in the shared
             * value, pointing to a mutable loan in the child avalue, but this
             * borrow is in practice immutable *)
            ()
        | AIgnoredMutLoan (_, _) ->
            (* There can be *inner* mutable loans, but not outer ones *)
            failwith "Unreachable"
        | AEndedIgnoredMutLoan _ ->
            (* Dive in *)
            super#visit_aloan_content env lc
        | AIgnoredSharedLoan _ ->
            (* Ignore *)
            ()

      method! visit_aborrow_content env bc =
        match bc with
        | AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
            failwith "Unreachable"
        | AEndedMutBorrow (mv, _) ->
            (* Add the meta-value and stop the exploration *)
            add_cborrow mv
        | AEndedIgnoredMutBorrow _ ->
            (* Dive in *)
            super#visit_aborrow_content env bc
        | AProjSharedBorrow _ ->
            (* Ignore *)
            ()
    end
  in
  (* Apply *)
  obj#visit_abs () abs;
  (* Return the accumulated values *)
  List.rev !acc