open Errors
open Identifiers

open Types
(** Pretty-printing for types *)

module Types = struct
  let type_var_to_string (tv : type_var) : string = tv.tv_name

  let region_var_to_string (rv : region_var) : string =
    match rv.rv_name with
    | Some name -> name
    | None -> RegionVarId.to_string rv.rv_index

  let region_to_string (rid_to_string : 'rid -> string) (r : 'rid region) :
      string =
    match r with Static -> "'static" | Var rid -> rid_to_string rid

  let erased_region_to_string (_ : erased_region) : string = "'_"

  let ref_kind_to_string (rk : ref_kind) : string =
    match rk with Mut -> "Mut" | Shared -> "Shared"

  let assumed_ty_to_string (_ : assumed_ty) : string = "Box"

  (* TODO: This is probably not the most OCaml-like way of doing this *)
  type 'r type_formatter = {
    r_to_string : 'r -> string;
    (* TODO: remove this and put the name everywhere instead? *)
    type_var_id_to_string : TypeVarId.id -> string;
    (* TODO: remove this and put the name everywhere instead? *)
    type_def_id_to_string : TypeDefId.id -> string;
  }

  type etype_formatter = erased_region type_formatter

  type rtype_formatter = RegionVarId.id region type_formatter

  let integer_type_to_string = function
    | Isize -> "isize"
    | I8 -> "i8"
    | I16 -> "i16"
    | I32 -> "i32"
    | I64 -> "i64"
    | I128 -> "i128"
    | Usize -> "usize"
    | U8 -> "u8"
    | U16 -> "u16"
    | U32 -> "u32"
    | U64 -> "u64"
    | U128 -> "u128"

  let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r ty) : string =
    match ty with
    | Adt (id, regions, tys) ->
        let params = params_to_string fmt regions tys in
        fmt.type_def_id_to_string id ^ params
    | TypeVar tv -> fmt.type_var_id_to_string tv
    | Bool -> "bool"
    | Char -> "char"
    | Never -> "⊥"
    | Integer int_ty -> integer_type_to_string int_ty
    | Str -> "str"
    | Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]"
    | Slice sty -> "[" ^ ty_to_string fmt sty ^ "]"
    | Ref (r, rty, ref_kind) -> (
        match ref_kind with
        | Mut -> "&" ^ fmt.r_to_string r ^ " mut (" ^ ty_to_string fmt rty ^ ")"
        | Shared -> "&" ^ fmt.r_to_string r ^ " (" ^ ty_to_string fmt rty ^ ")")
    | Tuple tys ->
        "(" ^ String.concat ",  " (List.map (ty_to_string fmt) tys) ^ ")"
    | Assumed (aty, regions, tys) -> (
        let params = params_to_string fmt regions tys in
        match aty with Box -> "std::boxed::Box" ^ params)

  and params_to_string fmt (regions : 'r list) (types : 'r ty list) : string =
    if List.length regions + List.length types > 0 then
      let regions = List.map fmt.r_to_string regions in
      let types = List.map (ty_to_string fmt) types in
      let params = String.concat ", " (List.append regions types) in
      "<" ^ params ^ ">"
    else ""

  let rty_to_string fmt (ty : rty) : string = ty_to_string fmt ty

  let ety_to_string fmt (ty : ety) : string = ty_to_string fmt ty

  let field_to_string fmt (f : field) : string =
    f.field_name ^ " : " ^ ty_to_string fmt f.field_ty

  let variant_to_string fmt (v : variant) : string =
    v.variant_name ^ "("
    ^ String.concat ", "
        (List.map (field_to_string fmt) (FieldId.vector_to_list v.fields))
    ^ ")"

  let name_to_string (name : name) : string = String.concat "::" name

  let type_def_to_string (type_def_id_to_string : TypeDefId.id -> string)
      (def : type_def) : string =
    let regions : region_var list =
      RegionVarId.vector_to_list def.region_params
    in
    let types : type_var list = TypeVarId.vector_to_list def.type_params in
    let rid_to_string rid =
      match List.find_opt (fun rv -> rv.rv_index = rid) regions with
      | Some rv -> region_var_to_string rv
      | None -> failwith "Unreachable"
    in
    let r_to_string = region_to_string rid_to_string in
    let type_var_id_to_string id =
      match List.find_opt (fun tv -> tv.tv_index = id) types with
      | Some tv -> type_var_to_string tv
      | None -> failwith "Unreachable"
    in
    let fmt = { r_to_string; type_var_id_to_string; type_def_id_to_string } in
    let name = name_to_string def.name in
    let params =
      if List.length regions + List.length types > 0 then
        let regions = List.map region_var_to_string regions in
        let types = List.map type_var_to_string types in
        let params = String.concat ", " (List.append regions types) in
        "<" ^ params ^ ">"
      else ""
    in
    match def.kind with
    | Struct fields ->
        let fields = FieldId.vector_to_list fields in
        if List.length fields > 0 then
          let fields =
            String.concat ","
              (List.map (fun f -> "\n  " ^ field_to_string fmt f) fields)
          in
          "struct " ^ name ^ params ^ "{" ^ fields ^ "}"
        else "struct" ^ name ^ params ^ "{}"
    | Enum variants ->
        let variants = VariantId.vector_to_list variants in
        let variants =
          List.map (fun v -> "|  " ^ variant_to_string fmt v) variants
        in
        let variants = String.concat "\n" variants in
        "enum " ^ name ^ params ^ " =\n" ^ variants
end

(** Pretty-printing for values *)

open Values

module Values = struct
  open Types (* local module *)

  type value_formatter = {
    r_to_string : RegionVarId.id -> string;
    type_var_id_to_string : TypeVarId.id -> string;
    type_def_id_to_string : TypeDefId.id -> string;
    type_def_id_variant_id_to_string : TypeDefId.id -> VariantId.id -> string;
    var_id_to_string : VarId.id -> string;
  }

  let value_to_etype_formatter (fmt : value_formatter) : etype_formatter =
    {
      Types.r_to_string = erased_region_to_string;
      Types.type_var_id_to_string = fmt.type_var_id_to_string;
      Types.type_def_id_to_string = fmt.type_def_id_to_string;
    }

  let value_to_rtype_formatter (fmt : value_formatter) : rtype_formatter =
    {
      Types.r_to_string = region_to_string fmt.r_to_string;
      Types.type_var_id_to_string = fmt.type_var_id_to_string;
      Types.type_def_id_to_string = fmt.type_def_id_to_string;
    }

  let var_id_to_string (id : VarId.id) : string = "var@" ^ VarId.to_string id

  let var_to_string (v : var) : string =
    let id = var_id_to_string v.index in
    match v.name with None -> id | Some name -> name ^ "(" ^ id ^ ")"

  let big_int_to_string (bi : big_int) : string = Z.to_string bi

  let scalar_value_to_string (sv : scalar_value) : string =
    big_int_to_string sv.value ^ ": " ^ integer_type_to_string sv.int_ty

  let constant_value_to_string (cv : constant_value) : string =
    match cv with
    | Scalar sv -> scalar_value_to_string sv
    | Bool b -> Bool.to_string b
    | Char c -> String.make 1 c
    | String s -> s

  let symbolic_value_id_to_string (id : SymbolicValueId.id) : string =
    "s@" ^ SymbolicValueId.to_string id

  let symbolic_value_to_string (fmt : rtype_formatter) (sv : symbolic_value) :
      string =
    symbolic_value_id_to_string sv.sv_id ^ " : " ^ ty_to_string fmt sv.sv_ty

  let region_id_to_string (rid : RegionId.id) : string =
    "r@" ^ RegionId.to_string rid

  let symbolic_proj_comp_to_string (fmt : rtype_formatter)
      (sp : symbolic_proj_comp) : string =
    let regions = RegionId.set_to_string sp.rset_ended in
    "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")"

  let rec typed_value_to_string (fmt : value_formatter) (v : typed_value) :
      string =
    match v.value with
    | Concrete cv -> constant_value_to_string cv
    | Adt av ->
        let adt_ident =
          match av.variant_id with
          | Some vid -> fmt.type_def_id_variant_id_to_string av.def_id vid
          | None -> fmt.type_def_id_to_string av.def_id
        in
        let field_values = FieldId.vector_to_list av.field_values in
        if List.length field_values > 0 then
          let field_values =
            String.concat " "
              (List.map (typed_value_to_string fmt) field_values)
          in
          adt_ident ^ " " ^ field_values
        else adt_ident
    | Tuple values ->
        let values = FieldId.vector_to_list values in
        let values =
          String.concat ", " (List.map (typed_value_to_string fmt) values)
        in
        "(" ^ values ^ ")"
    | Bottom -> "⊥"
    | Assumed av -> (
        match av with Box bv -> "@Box(" ^ typed_value_to_string fmt bv ^ ")")
    | Borrow bc -> borrow_content_to_string fmt bc
    | Loan lc -> loan_content_to_string fmt lc
    | Symbolic sp ->
        symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) sp

  and borrow_content_to_string (fmt : value_formatter) (bc : borrow_content) :
      string =
    match bc with
    | SharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋"
    | MutBorrow (bid, tv) ->
        "&mut@" ^ BorrowId.to_string bid ^ " ("
        ^ typed_value_to_string fmt tv
        ^ ")"
    | InactivatedMutBorrow bid ->
        "⌊inactivated_mut@" ^ BorrowId.to_string bid ^ "⌋"

  and loan_content_to_string (fmt : value_formatter) (lc : loan_content) :
      string =
    match lc with
    | SharedLoan (loans, v) ->
        let loans = BorrowId.set_to_string loans in
        "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")"
    | MutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋"

  let symbolic_value_proj_to_string (fmt : value_formatter)
      (sv : symbolic_value) (rty : rty) : string =
    symbolic_value_id_to_string sv.sv_id
    ^ " : "
    ^ ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty
    ^ " <: "
    ^ ty_to_string (value_to_rtype_formatter fmt) rty

  let rec abstract_shared_borrows_to_string (fmt : value_formatter)
      (abs : abstract_shared_borrows) : string =
    match abs with
    | AsbSet bs -> BorrowId.set_to_string bs
    | AsbProjReborrows (sv, rty) ->
        "{" ^ symbolic_value_proj_to_string fmt sv rty ^ "}"
    | AsbUnion (asb1, asb2) ->
        abstract_shared_borrows_to_string fmt asb1
        ^ " U "
        ^ abstract_shared_borrows_to_string fmt asb2

  let rec typed_avalue_to_string (fmt : value_formatter) (v : typed_avalue) :
      string =
    match v.avalue with
    | AConcrete cv -> constant_value_to_string cv
    | AAdt av ->
        let adt_ident =
          match av.avariant_id with
          | Some vid -> fmt.type_def_id_variant_id_to_string av.adef_id vid
          | None -> fmt.type_def_id_to_string av.adef_id
        in
        let field_values = FieldId.vector_to_list av.afield_values in
        if List.length field_values > 0 then
          let field_values =
            String.concat " "
              (List.map (typed_avalue_to_string fmt) field_values)
          in
          adt_ident ^ " " ^ field_values
        else adt_ident
    | ATuple values ->
        let values = FieldId.vector_to_list values in
        let values =
          String.concat ", " (List.map (typed_avalue_to_string fmt) values)
        in
        "(" ^ values ^ ")"
    | ABottom -> "⊥"
    | ALoan lc -> aloan_content_to_string fmt lc
    | ABorrow bc -> aborrow_content_to_string fmt bc
    | AAssumed av -> (
        match av with ABox bv -> "@Box(" ^ typed_avalue_to_string fmt bv ^ ")")
    | AProj pv -> aproj_to_string fmt pv

  and aloan_content_to_string (fmt : value_formatter) (lc : aloan_content) :
      string =
    match lc with
    | AMutLoan (bid, av) ->
        "⌊mut@" ^ BorrowId.to_string bid ^ ", "
        ^ typed_avalue_to_string fmt av
        ^ "⌋"
    | ASharedLoan (loans, v, av) ->
        let loans = BorrowId.set_to_string loans in
        "@shared_loan(" ^ loans ^ ", "
        ^ typed_value_to_string fmt v
        ^ ", "
        ^ typed_avalue_to_string fmt av
        ^ ")"
    | AEndedMutLoan ml ->
        "@ended_mut_loan{ given_back="
        ^ typed_value_to_string fmt ml.given_back
        ^ "; child="
        ^ typed_avalue_to_string fmt ml.child
        ^ " }"
    | AEndedSharedLoan (v, av) ->
        "@ended_shared_loan("
        ^ typed_value_to_string fmt v
        ^ ", "
        ^ typed_avalue_to_string fmt av
        ^ ")"
    | AIgnoredMutLoan (bid, av) ->
        "@ignored_mut_loan(" ^ BorrowId.to_string bid ^ ", "
        ^ typed_avalue_to_string fmt av
        ^ ")"
    | AIgnoredSharedLoan asb ->
        "@ignored_shared_loan("
        ^ abstract_shared_borrows_to_string fmt asb
        ^ ")"

  and aborrow_content_to_string (fmt : value_formatter) (bc : aborrow_content) :
      string =
    match bc with
    | AMutBorrow (bid, av) ->
        "&mut@" ^ BorrowId.to_string bid ^ " ("
        ^ typed_avalue_to_string fmt av
        ^ ")"
    | ASharedBorrow bid -> "⌊shared@" ^ BorrowId.to_string bid ^ "⌋"
    | AIgnoredMutBorrow av ->
        "@ignored_mut_borrow(" ^ typed_avalue_to_string fmt av ^ ")"
    | AEndedIgnoredMutLoan ml ->
        "@ended_ignored_mut_borrow{ given_back="
        ^ typed_avalue_to_string fmt ml.given_back
        ^ "; child: "
        ^ typed_avalue_to_string fmt ml.child
        ^ "}"
    | AIgnoredSharedBorrow sb ->
        "@ignored_shared_borrow("
        ^ abstract_shared_borrows_to_string fmt sb
        ^ ")"

  and aproj_to_string (fmt : value_formatter) (pv : aproj) : string =
    match pv with
    | AProjLoans sv ->
        "proj_loans ("
        ^ symbolic_value_to_string (value_to_rtype_formatter fmt) sv
        ^ ")"
    | AProjBorrows (sv, rty) ->
        "proj_borrows (" ^ symbolic_value_proj_to_string fmt sv rty ^ ")"

  let abs_to_string (fmt : value_formatter) (abs : abs) : string =
    let avs =
      List.map (fun av -> "  " ^ typed_avalue_to_string fmt av) abs.avalues
    in
    let avs = String.concat ",\n" avs in
    "abs@"
    ^ AbstractionId.to_string abs.abs_id
    ^ "{parents="
    ^ AbstractionId.set_to_string abs.parents
    ^ "}" ^ "{regions="
    ^ RegionId.set_to_string abs.regions
    ^ "}" ^ " {\n" ^ avs ^ "\n}"
end

open Contexts
(** Pretty-printing for contexts *)

module Contexts = struct
  open Values (* local module *)

  open Contexts

  let env_value_to_string (fmt : value_formatter) (ev : env_value) : string =
    match ev with
    | Var (vid, tv) ->
        var_id_to_string vid ^ " -> " ^ typed_value_to_string fmt tv
    | Abs abs -> abs_to_string fmt abs

  let env_to_string (fmt : value_formatter) (env : env) : string =
    "{\n"
    ^ String.concat ";\n"
        (List.map (fun ev -> "  " ^ env_value_to_string fmt ev) env)
    ^ "\n}"

  type ctx_formatter = value_formatter

  let eval_ctx_to_ctx_formatter (ctx : eval_ctx) : ctx_formatter =
    (* We shouldn't use r_to_string *)
    let r_to_string _ = failwith "Unreachable" in
    let type_var_id_to_string vid =
      let v = lookup_type_var ctx vid in
      v.tv_name
    in
    let type_def_id_to_string def_id =
      let def = TypeDefId.nth ctx.type_context def_id in
      Types.name_to_string def.name
    in
    let type_def_id_variant_id_to_string def_id variant_id =
      let def = TypeDefId.nth ctx.type_context def_id in
      match def.kind with
      | Struct _ -> failwith "Unreachable"
      | Enum variants ->
          let variant = VariantId.nth variants variant_id in
          Types.name_to_string def.name ^ "::" ^ variant.variant_name
    in
    let var_id_to_string vid =
      let v = VarId.Map.find vid ctx.vars in
      var_to_string v
    in
    {
      r_to_string;
      type_var_id_to_string;
      type_def_id_to_string;
      type_def_id_variant_id_to_string;
      var_id_to_string;
    }

  let frame_to_string (fmt : ctx_formatter) (ctx : eval_ctx)
      (frame : stack_frame) : string =
    let var_binding_to_string (vid : VarId.id) : string =
      let var = ctx_lookup_var ctx vid in
      let v = ctx_lookup_var_value ctx vid in
      let var_name =
        match var.name with Some name -> "(" ^ name ^ ")" | None -> ""
      in
      "  @" ^ VarId.to_string var.index ^ var_name ^ " --> "
      ^ typed_value_to_string fmt v
    in
    let vars =
      String.concat ",\n" (List.map var_binding_to_string frame.vars)
    in
    "[\n" ^ vars ^ "\n]"

  let eval_ctx_to_string (ctx : eval_ctx) : string =
    let fmt = eval_ctx_to_ctx_formatter ctx in
    let num_frames = List.length ctx.frames in
    let frames =
      List.mapi
        (fun i f ->
          "\n# Frame " ^ string_of_int i ^ ":\n" ^ frame_to_string fmt ctx f
          ^ "\n")
        ctx.frames
    in
    let frames = List.rev frames in
    "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames
end