(* match exhaustiveness와 도달 불가 팔 검사 (Maranget의 usefulness 알고리즘).

   철학 1의 대표 항목이다. 그리고 interface hash가 enum 정의 본문을 입력으로
   삼는 이유이기도 하다 — upstream에 variant가 하나 늘면 downstream의 match가
   깨져야 하는데, 이 검사가 없으면 깨질 것이 없다.

   생성자 집합을 알 수 없는 타입(외부 타입, 미지수)은 검사하지 않는다.
   모르는 것을 위반이라고 말하지 않는다. *)

module T = Types

(* 패턴을 검사용 형태로 줄인다. 바인딩은 와일드카드와 같다 —
   무엇을 덮는가만 중요하다. *)
type cpat = CWild | CCtor of string * cpat list
type ctor = { c_name : string; c_args : T.t list }
type ctors = Finite of ctor list | Infinite

type env = {
  (* enum 이름 -> variant 목록. 제네릭은 인스턴스화해서 넘어온다 *)
  variants : string -> T.t list -> (string * T.t list) list option;
  is_ctor : string -> bool;
}

let ctors_of env (t : T.t) : ctors =
  match T.resolve t with
  | T.TBool ->
      Finite
        [ { c_name = "true"; c_args = [] }; { c_name = "false"; c_args = [] } ]
  | T.TUnit -> Finite [ { c_name = "unit"; c_args = [] } ]
  | T.TCon ("Option", [ a ]) ->
      Finite
        [
          { c_name = "Some"; c_args = [ a ] }; { c_name = "None"; c_args = [] };
        ]
  | T.TCon ("Result", [ a; b ]) ->
      Finite
        [
          { c_name = "Ok"; c_args = [ a ] }; { c_name = "Err"; c_args = [ b ] };
        ]
  | T.TCon (n, args) -> (
      match env.variants n args with
      | Some vs ->
          Finite
            (List.map (fun (name, tys) -> { c_name = name; c_args = tys }) vs)
      | None -> Infinite)
  | _ -> Infinite

let rec of_pattern env (p : Ast.pattern) : cpat =
  match p with
  | Ast.P_wild _ -> CWild
  | Ast.P_lit (Ast.L_bool true, _) -> CCtor ("true", [])
  | Ast.P_lit (Ast.L_bool false, _) -> CCtor ("false", [])
  (* 리터럴은 인자 없는 생성자다. 와일드카드로 바꾸면 모든 값을 덮는 것이 되어
     Int 리터럴 몇 개로 exhaustive가 되어버린다. 타입의 생성자 집합이 무한하므로
     리터럴만으로는 결코 완전해지지 않는다. *)
  | Ast.P_lit (Ast.L_int n, _) -> CCtor ("<" ^ n ^ ">", [])
  | Ast.P_lit (Ast.L_str v, _) -> CCtor ("<" ^ String.escaped v ^ ">", [])
  | Ast.P_bind (n, _) -> if env.is_ctor n then CCtor (n, []) else CWild
  | Ast.P_ctor { name; args; _ } ->
      if env.is_ctor name then CCtor (name, List.map (of_pattern env) args)
      else CWild

let wilds n = List.init n (fun _ -> CWild)

(* 행렬을 생성자 c로 특수화한다 *)
let specialize (c : ctor) (matrix : cpat list list) : cpat list list =
  let arity = List.length c.c_args in
  List.filter_map
    (fun row ->
      match row with
      | CCtor (n, args) :: rest ->
          if n = c.c_name then Some (args @ rest) else None
      | CWild :: rest -> Some (wilds arity @ rest)
      | [] -> None)
    matrix

let default_matrix (matrix : cpat list list) : cpat list list =
  List.filter_map
    (fun row ->
      match row with
      | CCtor _ :: _ -> None
      | CWild :: rest -> Some rest
      | [] -> None)
    matrix

let head_names (matrix : cpat list list) =
  List.filter_map
    (fun row -> match row with CCtor (n, _) :: _ -> Some n | _ -> None)
    matrix

(* 행렬이 덮지 못하는 반례 벡터를 찾는다. None이면 완전하다. *)
let rec witness env (matrix : cpat list list) (tys : T.t list) :
    cpat list option =
  match tys with
  | [] -> if matrix = [] then Some [] else None
  | th :: rest -> (
      let heads = head_names matrix in
      match ctors_of env th with
      | Finite cs
        when List.for_all (fun c -> List.mem c.c_name heads) cs && cs <> [] ->
          (* 모든 생성자가 나타났다: 각각으로 파고든다 *)
          let rec try_each = function
            | [] -> None
            | c :: more -> (
                let arity = List.length c.c_args in
                match witness env (specialize c matrix) (c.c_args @ rest) with
                | Some ws ->
                    let args = List.filteri (fun i _ -> i < arity) ws in
                    let tail = List.filteri (fun i _ -> i >= arity) ws in
                    Some (CCtor (c.c_name, args) :: tail)
                | None -> try_each more)
          in
          try_each cs
      | kind -> (
          (* 빠진 생성자가 있거나 집합이 무한하다 *)
          match witness env (default_matrix matrix) rest with
          | None -> None
          | Some ws ->
              let head =
                match kind with
                | Finite cs -> (
                    match
                      List.find_opt (fun c -> not (List.mem c.c_name heads)) cs
                    with
                    | Some c -> CCtor (c.c_name, wilds (List.length c.c_args))
                    | None -> CWild)
                | Infinite -> CWild
              in
              Some (head :: ws)))

let rec show_cpat = function
  | CWild -> "_"
  | CCtor (n, []) -> n
  | CCtor (n, args) ->
      n ^ "(" ^ String.concat ", " (List.map show_cpat args) ^ ")"

(* 행 q가 행렬 P에 대해 쓸모 있는가 = P가 덮지 못하는 값을 q가 덮는가 *)
let useful env (matrix : cpat list list) (q : cpat list) (tys : T.t list) : bool
    =
  let rec go matrix q tys =
    match (q, tys) with
    | [], [] -> matrix = []
    | qh :: qt, th :: tt -> (
        match qh with
        | CCtor (n, args) -> (
            match ctors_of env th with
            | Finite cs -> (
                match List.find_opt (fun c -> c.c_name = n) cs with
                | Some c -> go (specialize c matrix) (args @ qt) (c.c_args @ tt)
                | None -> go (default_matrix matrix) qt tt)
            | Infinite ->
                let c =
                  { c_name = n; c_args = List.map (fun _ -> T.TUnknown) args }
                in
                go (specialize c matrix) (args @ qt) (c.c_args @ tt))
        | CWild -> (
            let heads = head_names matrix in
            match ctors_of env th with
            | Finite cs
              when List.for_all (fun c -> List.mem c.c_name heads) cs
                   && cs <> [] ->
                List.exists
                  (fun c ->
                    go (specialize c matrix)
                      (wilds (List.length c.c_args) @ qt)
                      (c.c_args @ tt))
                  cs
            | _ -> go (default_matrix matrix) qt tt))
    | _ -> false
  in
  go matrix q tys

type result = {
  missing : string option; (* 빠진 경우의 반례 *)
  unreachable : int list; (* 도달할 수 없는 팔의 번호 (0부터) *)
}

let check env (scrutinee : T.t) (pats : Ast.pattern list) : result =
  match ctors_of env scrutinee with
  | Infinite when T.resolve scrutinee = T.TUnknown ->
      (* 생성자 집합을 모르면 검사하지 않는다 *)
      { missing = None; unreachable = [] }
  | _ ->
      let rows = List.map (fun p -> [ of_pattern env p ]) pats in
      let unreachable =
        let acc = ref [] in
        List.iteri
          (fun i row ->
            let before = List.filteri (fun j _ -> j < i) rows in
            if not (useful env before row [ scrutinee ]) then acc := i :: !acc)
          rows;
        List.rev !acc
      in
      let missing =
        (* 리터럴 패턴이 섞이면 정확한 반례를 만들 수 없다 — 그 열은 무한
           집합이므로 와일드카드가 없으면 불완전으로 본다 *)
        match witness env rows [ scrutinee ] with
        | Some ws -> (
            match ws with [ w ] -> Some (show_cpat w) | _ -> Some "_")
        | None -> None
      in
      { missing; unreachable }