277 lines
8.9 KiB
OCaml
277 lines
8.9 KiB
OCaml
(***********************************************************************)
|
|
(* *)
|
|
(* 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
|