(***********************************************************************)
(*                                                                     *)
(*                           Objective Caml                            *)
(*                                                                     *)
(*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         *)
(*                                                                     *)
(*  Copyright 1996 Institut National de Recherche en Informatique et   *)
(*  Automatique.  Distributed only by permission.                      *)
(*                                                                     *)
(***********************************************************************)

(* $Id$ *)

(* Detection of partial matches and unused match cases. *)

open Misc
open Asttypes
open Types
open Typedtree

let make_pat desc ty =
  {pat_desc = desc; pat_loc = Location.none; pat_type = ty}

let omega = make_pat Tpat_any Ctype.none

let rec omegas i =
  if i <= 0 then [] else omega :: omegas (i-1)

let omega_list l = omegas(List.length l)

let has_guard act =
  match act.exp_desc with
    Texp_when(_, _) -> true
  | _ -> false

let simple_match p1 p2 = 
  match p1.pat_desc, p2.pat_desc with
    Tpat_construct(c1, _), Tpat_construct(c2, _) ->
      c1.cstr_tag = c2.cstr_tag
  | Tpat_constant(c1), Tpat_constant(c2) ->
      c1 = c2
  | Tpat_tuple(_), Tpat_tuple(_) -> true
  | Tpat_record(_), Tpat_record(_) -> true
  | _, (Tpat_any | Tpat_var(_)) -> true
  | _, _ -> false

(* Return the set of labels and number of fields for a record pattern. *)

let record_labels p =
  match p.pat_desc with
    Tpat_record((lbl1, pat1) :: rem) -> Array.to_list lbl1.lbl_all
  | _ -> fatal_error "Parmatch.record_labels"

let record_num_fields p =
  match p.pat_desc with
    Tpat_record((lbl1, pat1) :: rem) -> Array.length lbl1.lbl_all
  | _ -> fatal_error "Parmatch.record_num_fields"

let set_fields size l =
  let v = Array.create size omega in
  let rec change_rec l = match l with
    (lbl,p)::l ->  v.(lbl.lbl_pos) <- p ;  change_rec l 
  | [] -> () in
  change_rec l;
  Array.to_list v

let simple_match_args p1 p2 =
  match p2.pat_desc with
    Tpat_construct(cstr, args) -> args
  | Tpat_tuple(args)  -> args
  | Tpat_record(args) ->  set_fields (record_num_fields p1) args
  | (Tpat_any | Tpat_var(_)) ->
      begin match p1.pat_desc with
        Tpat_construct(_, args) -> omega_list args
      | Tpat_tuple(args) -> omega_list args
      | Tpat_record(args) ->  omega_list args
      | _ -> []
      end
  | _ -> []

(*
  Computes the discriminating pattern for matching by the first
  column of pss, that is:
     checks for a tuple or a record when q is a variable.
*)

let rec simple_pat q pss = match pss with
    ({pat_desc = Tpat_alias(p,_)}::ps)::pss -> 
        simple_pat q ((p::ps)::pss)
  | ({pat_desc = Tpat_or(p1,p2)}::ps)::pss ->
        simple_pat q ((p1::ps)::(p2::ps)::pss)
  | ({pat_desc = (Tpat_any | Tpat_var(_))}::_)::pss ->
        simple_pat q pss
  | (({pat_desc = Tpat_tuple(args)} as p)::_)::_ ->
        make_pat (Tpat_tuple(omega_list args)) p.pat_type
  | (({pat_desc = Tpat_record(args)} as p)::_)::pss ->
        make_pat (Tpat_record (List.map (fun lbl -> (lbl,omega)) (record_labels p)))
                 p.pat_type
  | _ -> q

let filter_one q pss =
  let rec filter_rec = function
      ({pat_desc = Tpat_alias(p,_)}::ps)::pss -> 
        filter_rec ((p::ps)::pss)
    | ({pat_desc = Tpat_or(p1,p2)}::ps)::pss ->
        filter_rec ((p1::ps)::(p2::ps)::pss)
    | (p::ps)::pss ->
        if simple_match q p
        then (simple_match_args q p @ ps) :: filter_rec pss
        else filter_rec pss
    | _ -> [] in
  filter_rec pss

let filter_extra pss =
  let rec filter_rec = function
      ({pat_desc = Tpat_alias(p,_)}::ps)::pss -> 
        filter_rec ((p::ps)::pss)
    | ({pat_desc = Tpat_or(p1,p2)}::ps)::pss ->
        filter_rec ((p1::ps)::(p2::ps)::pss)
    | ({pat_desc = (Tpat_any | Tpat_var(_))} :: qs) :: pss ->
        qs :: filter_rec pss
    | _::pss  -> filter_rec pss
    | [] -> [] in
  filter_rec pss

let filter_all pat0 pss =

  let rec insert q qs env =
    match env with
      [] -> [q, [simple_match_args q q @ qs]]
    | ((p,pss) as c)::env ->
        if simple_match q p
        then (p, ((simple_match_args p q @ qs) :: pss)) :: env
        else c :: insert q qs env in

  let rec filter_rec env = function
    ({pat_desc = Tpat_alias(p,_)}::ps)::pss ->
      filter_rec env ((p::ps)::pss)
  | ({pat_desc = Tpat_or(p1,p2)}::ps)::pss ->
      filter_rec env ((p1::ps)::(p2::ps)::pss)
  | ({pat_desc = (Tpat_any | Tpat_var(_))}::_)::pss ->
      filter_rec env pss
  | (p::ps)::pss ->
      filter_rec (insert p ps env) pss
  | _ -> env

  and filter_omega env = function
    ({pat_desc = Tpat_alias(p,_)}::ps)::pss ->
      filter_omega env ((p::ps)::pss)
  | ({pat_desc = Tpat_or(p1,p2)}::ps)::pss ->
      filter_omega env ((p1::ps)::(p2::ps)::pss)
  | ({pat_desc = (Tpat_any | Tpat_var(_))}::ps)::pss ->
      filter_omega
        (List.map (fun (q,qss) -> (q,(simple_match_args q omega @ ps) :: qss)) env)
        pss
  | _::pss -> filter_omega env pss
  | [] -> env in
        
  filter_omega
    (filter_rec
      (match pat0.pat_desc with
        (Tpat_record(_) | Tpat_tuple(_)) -> [pat0,[]]
      | _ -> [])
      pss)
    pss

      
let full_match env =
  match env with
    ({pat_desc = Tpat_construct(c,_)},_) :: _ ->
      List.length env = c.cstr_consts + c.cstr_nonconsts
  | ({pat_desc = Tpat_constant(Const_char _)},_) :: _ ->
      List.length env = 256
  | ({pat_desc = Tpat_constant(_)},_) :: _ -> false
  | ({pat_desc = Tpat_tuple(_)},_) :: _ -> true
  | ({pat_desc = Tpat_record(_)},_) :: _ -> true
  | _ -> fatal_error "Parmatch.full_match"

(*
  Is the last row of pattern matrix pss + qs satisfiable ?
        That is :
  Does there List.exists at least one value vector, es such that :
   1/ for all ps in pss ps # es (ps and es are not compatible)
   2/ qs <= es                  (es matches qs)
*)

let rec satisfiable pss qs =
  match pss with
    [] -> true
  | _ ->
    match qs with
      [] -> false
    | {pat_desc = Tpat_or(q1,q2)}::qs ->
        satisfiable pss (q1::qs) or satisfiable pss (q2::qs)
    | {pat_desc = Tpat_alias(q,_)}::qs ->
        satisfiable pss (q::qs)
    | {pat_desc = (Tpat_any | Tpat_var(_))}::qs ->
        let q0 = simple_pat omega pss in     
        begin match filter_all q0 pss with
          (* first column of pss is made of variables only *)
          [] -> satisfiable (filter_extra pss) qs 
        | constrs ->          
            let try_non_omega (p,pss) =
              satisfiable pss (simple_match_args p omega @ qs)  in
            if full_match constrs
            then List.exists try_non_omega constrs
            else satisfiable (filter_extra pss) qs or
                 List.exists try_non_omega constrs
        end
    | q::qs ->
        let q0 = simple_pat q pss in
        satisfiable (filter_one q0 pss) (simple_match_args q0 q @ qs)

let rec initial_matrix = function
    [] -> []
  | (pat, act) :: rem ->
       if has_guard act
       then initial_matrix rem
       else [pat] :: initial_matrix rem

let rec le_pat p q =
  match (p.pat_desc, q.pat_desc) with
    (Tpat_var _ | Tpat_any), _ -> true
  | Tpat_alias(p,_), _ -> le_pat p q
  | _, Tpat_alias(q,_) -> le_pat p q
  | Tpat_or(p1,p2), _ -> le_pat p1 q or le_pat p2 q
  | _, Tpat_or(q1,q2) -> le_pat p q1 & le_pat p q2
  | Tpat_constant(c1), Tpat_constant(c2) -> c1 = c2
  | Tpat_construct(c1,ps), Tpat_construct(c2,qs) ->
      c1.cstr_tag = c2.cstr_tag & le_pats ps qs
  | Tpat_tuple(ps), Tpat_tuple(qs) -> le_pats ps qs
  | Tpat_record(l1), Tpat_record(l2) ->
     let size = record_num_fields p in
     le_pats (set_fields size l1) (set_fields size l2)
  | _, _ -> false  

and le_pats ps qs =
  match ps,qs with
    p::ps, q::qs -> le_pat p q & le_pats ps qs
  | _, _         -> true

let get_mins ps =
  let rec select_rec r = function
    [] -> r
  | p::ps ->
      if List.exists (fun p0 -> le_pats p0 p) ps
      then select_rec r ps
      else select_rec (p::r) ps in
  select_rec [] (select_rec [] ps)

let check_partial loc casel =
  let pss = get_mins (initial_matrix casel) in
  if match pss with
      []     -> if casel = [] then false else true
    | ps::_  -> satisfiable pss (List.map (fun _ -> omega) ps)
  then Location.print_warning loc "this pattern-matching is not exhaustive"

let location_of_clause = function
    pat :: _ -> pat.pat_loc
  | _ -> fatal_error "Parmatch.location_of_clause"

let check_unused casel =
  let prefs =   
    List.fold_right
      (fun (pat,act as clause) r ->
         if has_guard act
         then ([], ([pat], act)) :: r
         else ([], ([pat], act)) :: 
              List.map (fun (pss,clause) -> [pat]::pss,clause) r)
      casel [] in
  List.iter
    (fun (pss, ((qs, _) as clause)) ->
      if not (satisfiable pss qs) then
        Location.print_warning (location_of_clause qs)
                                "this match case is unused.")
    prefs