(* 타입과 effect 표현, 그리고 지역 unification.

   TUnknown이 핵심이다. 외부 모듈에서 오는 이름은 모듈 로딩이 없는 v0에서
   해소할 수 없다. 그런 타입은 TUnknown이 되고 무엇과도 맞는다 — 모르는 것을
   틀렸다고 말하지 않기 위해서다.

   effect는 순서 없는 집합이고 합성은 합집합이다. 변수는 집합 변수이며,
   호출 지점에서 결정 위치(파라미터의 effect 자리에 단독으로 선 변수)를 통해
   메타에 묶인다. 함수 하나 범위를 넘지 않는다. *)

type t =
  | TUnknown
  (* 값을 내지 않는 타입. panic의 타입이고 어떤 자리에도 놓일 수 있다.
     TUnknown과 다르다 — TUnknown은 "모른다"이고 TNever는 "돌아오지
     않는다"이다. 둘 다 무엇과도 맞지만 생기는 이유가 다르다. *)
  | TNever
  | TInt
  | TBool
  | TString
  | TUnit
  | TVar of string
  | TCon of string * t list
  | TFn of { affine : bool; params : t list; eff : eff; ret : t }
  | TMeta of meta ref

and meta = Unbound of int | Bound of t

(* effect 집합. 원소는 구체 이름, 집합 변수, 또는 호출 지점의 미지수다. *)
and eff = atom list

and atom =
  | A_name of string * string (* Cap.method *)
  | A_var of string
  | A_meta of emeta ref

and emeta = EUnbound of int | EBound of eff

let counter = ref 0

let fresh () =
  incr counter;
  TMeta (ref (Unbound !counter))

let fresh_eff () =
  incr counter;
  [ A_meta (ref (EUnbound !counter)) ]

let rec resolve t =
  match t with TMeta { contents = Bound u } -> resolve u | _ -> t

(* 묶인 메타를 펼치고 중복을 없앤다. 집합이므로 순서는 의미가 없다. *)
let rec eff_resolve (e : eff) : eff =
  let expand a =
    match a with
    | A_meta { contents = EBound inner } -> eff_resolve inner
    | _ -> [ a ]
  in
  let flat = List.concat_map expand e in
  let mem a acc =
    List.exists
      (fun b ->
        match (a, b) with
        | A_name (c1, m1), A_name (c2, m2) -> c1 = c2 && m1 = m2
        | A_var x, A_var y -> x = y
        | A_meta r, A_meta r' -> r == r'
        | _ -> false)
      acc
  in
  List.fold_left (fun acc a -> if mem a acc then acc else a :: acc) [] flat
  |> List.rev

let atom_show = function
  | A_name (c, m) -> c ^ "." ^ m
  | A_var v -> v
  | A_meta { contents = EUnbound n } -> Printf.sprintf "_e%d" n
  | A_meta { contents = EBound _ } -> "?"

let eff_show e =
  match eff_resolve e with
  | [] -> "{}"
  | atoms -> "{" ^ String.concat ", " (List.map atom_show atoms) ^ "}"

let atom_eq a b =
  match (a, b) with
  | A_name (c1, m1), A_name (c2, m2) -> c1 = c2 && m1 = m2
  | A_var x, A_var y -> x = y
  | A_meta r, A_meta r' -> r == r'
  | _ -> false

(* declared가 덮지 못하는 원소들. 미지수는 판정을 미룬다 —
   결정되지 않은 것을 위반이라고 말하지 않는다. *)
let eff_missing ~declared ~performed =
  let declared = eff_resolve declared in
  List.filter
    (fun a ->
      match a with
      | A_meta { contents = EUnbound _ } -> false
      | _ -> not (List.exists (atom_eq a) declared))
    (eff_resolve performed)

let rec show t =
  match resolve t with
  | TUnknown -> "?"
  | TNever -> "Never"
  | TInt -> "Int"
  | TBool -> "Bool"
  | TString -> "String"
  | TUnit -> "Unit"
  | TVar v -> v
  | TCon (n, []) -> n
  | TCon (n, args) -> n ^ "[" ^ String.concat ", " (List.map show args) ^ "]"
  | TFn { affine; params; eff; ret } -> (
      (if affine then "affine fn(" else "fn(")
      ^ String.concat ", " (List.map show params)
      ^ ")"
      ^ (match eff_resolve eff with [] -> "" | e -> " effects " ^ eff_show e)
      ^ match resolve ret with TUnit -> "" | r -> " -> " ^ show r)
  | TMeta { contents = Unbound n } -> Printf.sprintf "_%d" n
  | TMeta { contents = Bound _ } -> "?"

let rec occurs r t =
  match resolve t with
  | TMeta r' -> r == r'
  | TCon (_, args) -> List.exists (occurs r) args
  | TFn { params; ret; _ } -> List.exists (occurs r) params || occurs r ret
  | _ -> false

(* 결정 위치의 해소: 파라미터의 effect 자리에 단독으로 선 미지수만 묶는다.
   그 외에는 참을 돌려주고, 실제 포함 검사는 호출 지점에서 방향을 아는
   쪽이 한다 (진단 품질 때문에). *)
let unify_eff a b =
  match (eff_resolve a, eff_resolve b) with
  | [ A_meta ({ contents = EUnbound _ } as r) ], other ->
      r := EBound other;
      true
  | other, [ A_meta ({ contents = EUnbound _ } as r) ] ->
      r := EBound other;
      true
  | _ -> true

let rec unify a b =
  match (resolve a, resolve b) with
  | TUnknown, _ | _, TUnknown -> true
  (* Never는 어떤 타입 자리에도 놓인다. panic이 match 팔에 설 수 있는 이유다 *)
  | TNever, _ | _, TNever -> true
  | TMeta r, TMeta r' when r == r' -> true
  | TMeta r, t | t, TMeta r ->
      if occurs r t then false
      else (
        r := Bound t;
        true)
  | TInt, TInt | TBool, TBool | TString, TString | TUnit, TUnit -> true
  | TVar x, TVar y -> x = y
  | TCon (n, xs), TCon (m, ys) ->
      n = m && List.length xs = List.length ys && List.for_all2 unify xs ys
  | TFn f, TFn g ->
      (* affinity는 타입 동등성의 일부가 아니다. 값이 affine인지는 무엇을
         capture했는지로 정해지는 substructural 성질이고, move/affinity 검사가
         소유한다. 여기서 섞으면 두 검사가 서로의 결론을 앞질러 버린다. *)
      List.length f.params = List.length g.params
      && List.for_all2 unify f.params g.params
      && unify_eff f.eff g.eff && unify f.ret g.ret
  | _ -> false

(* 제네릭 인스턴스화: 타입 변수와 effect 변수를 동시에 바꾼다 *)
let rec subst tenv eenv t =
  match resolve t with
  | TVar v -> ( match List.assoc_opt v tenv with Some u -> u | None -> TVar v)
  | TCon (n, args) -> TCon (n, List.map (subst tenv eenv) args)
  | TFn f ->
      TFn
        {
          affine = f.affine;
          params = List.map (subst tenv eenv) f.params;
          eff = subst_eff eenv f.eff;
          ret = subst tenv eenv f.ret;
        }
  | u -> u

and subst_eff eenv (e : eff) : eff =
  eff_resolve
    (List.concat_map
       (fun a ->
         match a with
         | A_var v -> (
             match List.assoc_opt v eenv with Some s -> s | None -> [ a ])
         | _ -> [ a ])
       e)