(* 타입 표현과 지역 unification.

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

   TMeta는 호출 지점에서 제네릭을 인스턴스화할 때 생기는 미지수다. 함수 하나
   범위에서만 살고 전역으로 흐르지 않는다 (철학 2: 전역 추론 없음). *)

type t =
  | TUnknown
  | TInt
  | TBool
  | TString
  | TUnit
  | TVar of string
  | TCon of string * t list
  | TFn of { affine : bool; params : t list; ret : t }
  | TMeta of meta ref

and meta = Unbound of int | Bound of t

let counter = ref 0

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

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

let rec show t =
  match resolve t with
  | TUnknown -> "?"
  | 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; ret } -> (
      (if affine then "affine fn(" else "fn(")
      ^ String.concat ", " (List.map show params)
      ^ ")"
      ^ 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

(* 성공하면 true. 실패해도 예외를 던지지 않는다 — 호출자가 위치를 알고
   진단을 만든다. *)
let rec unify a b =
  match (resolve a, resolve b) with
  | TUnknown, _ | _, TUnknown -> 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 f.ret g.ret
  | _ -> false

(* 제네릭 인스턴스화: TVar를 주어진 대입으로 바꾼다 *)
let rec subst env t =
  match resolve t with
  | TVar v -> ( match List.assoc_opt v env with Some u -> u | None -> TVar v)
  | TCon (n, args) -> TCon (n, List.map (subst env) args)
  | TFn f ->
      TFn
        {
          affine = f.affine;
          params = List.map (subst env) f.params;
          ret = subst env f.ret;
        }
  | u -> u