1562 lines
47 KiB
OCaml
1562 lines
47 KiB
OCaml
(***********************************************************************)
|
|
(* *)
|
|
(* Objective Caml *)
|
|
(* *)
|
|
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
|
|
(* *)
|
|
(* Copyright 1996 Institut National de Recherche en Informatique et *)
|
|
(* en Automatique. All rights reserved. This file is distributed *)
|
|
(* under the terms of the Q Public License version 1.0. *)
|
|
(* *)
|
|
(***********************************************************************)
|
|
|
|
(* $Id$ *)
|
|
|
|
(* Detection of partial matches and unused match cases. *)
|
|
|
|
open Misc
|
|
open Asttypes
|
|
open Types
|
|
open Typedtree
|
|
|
|
(*************************************)
|
|
(* Utilities for building patterns *)
|
|
(*************************************)
|
|
|
|
let make_pat desc ty tenv =
|
|
{pat_desc = desc; pat_loc = Location.none;
|
|
pat_type = ty ; pat_env = tenv }
|
|
|
|
let omega = make_pat Tpat_any Ctype.none Env.empty
|
|
|
|
let rec omegas i =
|
|
if i <= 0 then [] else omega :: omegas (i-1)
|
|
|
|
let omega_list l = List.map (fun _ -> omega) l
|
|
|
|
(***********************)
|
|
(* Compatibility check *)
|
|
(***********************)
|
|
|
|
(* p and q compatible means, there exists V that matches both *)
|
|
|
|
let is_absent tag row =
|
|
let row = Btype.row_repr row in
|
|
let field =
|
|
try Btype.row_field_repr (List.assoc tag row.row_fields)
|
|
with Not_found -> Rabsent
|
|
in field = Rabsent
|
|
|
|
let sort_fields args =
|
|
Sort.list
|
|
(fun (lbl1,_) (lbl2,_) -> lbl1.lbl_pos <= lbl2.lbl_pos)
|
|
args
|
|
|
|
let records_args l1 l2 =
|
|
let l1 = sort_fields l1
|
|
and l2 = sort_fields l2 in
|
|
let rec combine r1 r2 l1 l2 = match l1,l2 with
|
|
| [],[] -> r1,r2
|
|
| [],(_,p2)::rem2 -> combine (omega::r1) (p2::r2) [] rem2
|
|
| (_,p1)::rem1,[] -> combine (p1::r1) (omega::r2) rem1 []
|
|
| (lbl1,p1)::rem1, (lbl2,p2)::rem2 ->
|
|
if lbl1.lbl_pos < lbl2.lbl_pos then
|
|
combine (p1::r1) (omega::r2) rem1 l2
|
|
else if lbl1.lbl_pos > lbl2.lbl_pos then
|
|
combine (omega::r1) (p2::r2) l1 rem2
|
|
else (* same label on both sides *)
|
|
combine (p1::r1) (p2::r2) rem1 rem2 in
|
|
combine [] [] l1 l2
|
|
|
|
|
|
let rec compat p q =
|
|
match p.pat_desc,q.pat_desc with
|
|
| Tpat_alias (p,_),_ -> compat p q
|
|
| _,Tpat_alias (q,_) -> compat p q
|
|
| (Tpat_any|Tpat_var _),_ -> true
|
|
| _,(Tpat_any|Tpat_var _) -> true
|
|
| Tpat_or (p1,p2,_),_ -> compat p1 q || compat p2 q
|
|
| _,Tpat_or (q1,q2,_) -> compat p q1 || compat p q2
|
|
| Tpat_constant c1, Tpat_constant c2 -> c1=c2
|
|
| Tpat_tuple ps, Tpat_tuple qs -> compats ps qs
|
|
| Tpat_construct (c1,ps1), Tpat_construct (c2,ps2) ->
|
|
c1.cstr_tag = c2.cstr_tag && compats ps1 ps2
|
|
| Tpat_variant(l1,Some p1, r1), Tpat_variant(l2,Some p2,_) ->
|
|
l1=l2 && not (is_absent l1 r1) && compat p1 p2
|
|
| Tpat_variant (l1,None,r1), Tpat_variant(l2,None,_) ->
|
|
l1 = l2 && not (is_absent l1 r1)
|
|
| Tpat_variant (_, None, _), Tpat_variant (_,Some _, _) -> false
|
|
| Tpat_variant (_, Some _, _), Tpat_variant (_, None, _) -> false
|
|
| Tpat_record l1,Tpat_record l2 ->
|
|
let ps,qs = records_args l1 l2 in
|
|
compats ps qs
|
|
| Tpat_array ps, Tpat_array qs ->
|
|
List.length ps = List.length qs &&
|
|
compats ps qs
|
|
| _,_ ->
|
|
assert false
|
|
|
|
and compats ps qs = match ps,qs with
|
|
| [], [] -> true
|
|
| p::ps, q::qs -> compat p q && compats ps qs
|
|
| _,_ -> assert false
|
|
|
|
(****************************************)
|
|
(* Utilities for retrieving constructor *)
|
|
(* and record label names *)
|
|
(****************************************)
|
|
|
|
exception Empty (* Empty pattern *)
|
|
|
|
let get_type_descr ty tenv =
|
|
let ty = Ctype.repr (Ctype.expand_head tenv ty) in
|
|
match ty.desc with
|
|
| Tconstr (path,_,_) -> Env.find_type path tenv
|
|
| _ -> fatal_error "Parmatch.get_type_descr"
|
|
|
|
let get_type_path ty tenv =
|
|
let ty = Ctype.repr (Ctype.expand_head tenv ty) in
|
|
match ty.desc with
|
|
| Tconstr (path,_,_) -> path
|
|
| _ -> fatal_error "Parmatch.get_type_path"
|
|
|
|
let get_constr tag ty tenv =
|
|
match get_type_descr ty tenv with
|
|
| {type_kind=Type_variant constr_list} ->
|
|
Datarepr.find_constr_by_tag tag constr_list
|
|
| _ -> fatal_error "Parmatch.get_constr"
|
|
|
|
let find_label lbl lbls =
|
|
try
|
|
let name,_,_ = List.nth lbls lbl.lbl_pos in
|
|
name
|
|
with Failure "nth" -> "*Unkown label*"
|
|
|
|
let get_record_labels ty tenv =
|
|
match get_type_descr ty tenv with
|
|
| {type_kind = Type_record(lbls, rep)} -> lbls
|
|
| _ -> fatal_error "Parmatch.get_record_labels"
|
|
|
|
|
|
(*************************************)
|
|
(* Values as patterns pretty printer *)
|
|
(*************************************)
|
|
|
|
open Format
|
|
;;
|
|
|
|
let get_constr_name tag ty tenv = match tag with
|
|
| Cstr_exception path -> Path.name path
|
|
| _ ->
|
|
try
|
|
let name,_ = get_constr tag ty tenv in name
|
|
with
|
|
| Datarepr.Constr_not_found -> "*Unknown constructor*"
|
|
|
|
let is_cons tag v = match get_constr_name tag v.pat_type v.pat_env with
|
|
| "::" -> true
|
|
| _ -> false
|
|
|
|
|
|
let rec pretty_val ppf v = match v.pat_desc with
|
|
| Tpat_any -> fprintf ppf "_"
|
|
| Tpat_var x -> Ident.print ppf x
|
|
| Tpat_constant (Const_int i) -> fprintf ppf "%d" i
|
|
| Tpat_constant (Const_char c) -> fprintf ppf "%C" c
|
|
| Tpat_constant (Const_string s) -> fprintf ppf "%S" s
|
|
| Tpat_constant (Const_float f) -> fprintf ppf "%s" f
|
|
| Tpat_constant (Const_int32 i) -> fprintf ppf "%ldl" i
|
|
| Tpat_constant (Const_int64 i) -> fprintf ppf "%LdL" i
|
|
| Tpat_constant (Const_nativeint i) -> fprintf ppf "%ndn" i
|
|
| Tpat_tuple vs ->
|
|
fprintf ppf "@[(%a)@]" (pretty_vals ",") vs
|
|
| Tpat_construct ({cstr_tag=tag},[]) ->
|
|
let name = get_constr_name tag v.pat_type v.pat_env in
|
|
fprintf ppf "%s" name
|
|
| Tpat_construct ({cstr_tag=tag},[w]) ->
|
|
let name = get_constr_name tag v.pat_type v.pat_env in
|
|
fprintf ppf "@[<2>%s@ %a@]" name pretty_arg w
|
|
| Tpat_construct ({cstr_tag=tag},vs) ->
|
|
let name = get_constr_name tag v.pat_type v.pat_env in
|
|
begin match (name, vs) with
|
|
("::", [v1;v2]) ->
|
|
fprintf ppf "@[%a::@,%a@]" pretty_car v1 pretty_cdr v2
|
|
| _ ->
|
|
fprintf ppf "@[<2>%s@ @[(%a)@]@]" name (pretty_vals ",") vs
|
|
end
|
|
| Tpat_variant (l, None, _) ->
|
|
fprintf ppf "`%s" l
|
|
| Tpat_variant (l, Some w, _) ->
|
|
fprintf ppf "@[<2>`%s@ %a@]" l pretty_arg w
|
|
| Tpat_record lvs ->
|
|
fprintf ppf "@[{%a}@]"
|
|
(pretty_lvals (get_record_labels v.pat_type v.pat_env))
|
|
(List.filter
|
|
(function
|
|
| (_,{pat_desc=Tpat_any}) -> false (* do not show lbl=_ *)
|
|
| _ -> true) lvs)
|
|
| Tpat_array vs ->
|
|
fprintf ppf "@[[| %a |]@]" (pretty_vals " ;") vs
|
|
| Tpat_alias (v,x) ->
|
|
fprintf ppf "@[(%a@ as %a)@]" pretty_val v Ident.print x
|
|
| Tpat_or (v,w,_) ->
|
|
fprintf ppf "@[(%a|@,%a)@]" pretty_or v pretty_or w
|
|
|
|
and pretty_car ppf v = match v.pat_desc with
|
|
| Tpat_construct ({cstr_tag=tag}, [_ ; _])
|
|
when is_cons tag v ->
|
|
fprintf ppf "(%a)" pretty_val v
|
|
| _ -> pretty_val ppf v
|
|
|
|
and pretty_cdr ppf v = match v.pat_desc with
|
|
| Tpat_construct ({cstr_tag=tag}, [v1 ; v2])
|
|
when is_cons tag v ->
|
|
fprintf ppf "%a::@,%a" pretty_car v1 pretty_cdr v2
|
|
| _ -> pretty_val ppf v
|
|
|
|
and pretty_arg ppf v = match v.pat_desc with
|
|
| Tpat_construct (_,_::_) -> fprintf ppf "(%a)" pretty_val v
|
|
| _ -> pretty_val ppf v
|
|
|
|
and pretty_or ppf v = match v.pat_desc with
|
|
| Tpat_or (v,w,_) ->
|
|
fprintf ppf "%a|@,%a" pretty_or v pretty_or w
|
|
| _ -> pretty_val ppf v
|
|
|
|
and pretty_vals sep ppf = function
|
|
| [] -> ()
|
|
| [v] -> pretty_val ppf v
|
|
| v::vs ->
|
|
fprintf ppf "%a%s@ %a" pretty_val v sep (pretty_vals sep) vs
|
|
|
|
and pretty_lvals lbls ppf = function
|
|
| [] -> ()
|
|
| [lbl,v] ->
|
|
let name = find_label lbl lbls in
|
|
fprintf ppf "%s=%a" name pretty_val v
|
|
| (lbl,v)::rest ->
|
|
let name = find_label lbl lbls in
|
|
fprintf ppf "%s=%a;@ %a" name pretty_val v (pretty_lvals lbls) rest
|
|
|
|
let top_pretty ppf v =
|
|
fprintf ppf "@[%a@]@?" pretty_val v
|
|
|
|
|
|
let prerr_pat v =
|
|
top_pretty str_formatter v ;
|
|
prerr_string (flush_str_formatter ())
|
|
|
|
|
|
(****************************)
|
|
(* Utilities for matching *)
|
|
(****************************)
|
|
|
|
(* Check top matching *)
|
|
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_variant(l1, _, _), Tpat_variant(l2, _, _) ->
|
|
l1 = l2
|
|
| Tpat_constant(Const_float s1), Tpat_constant(Const_float s2) ->
|
|
float_of_string s1 = float_of_string s2
|
|
| Tpat_constant(c1), Tpat_constant(c2) -> c1 = c2
|
|
| Tpat_tuple _, Tpat_tuple _ -> true
|
|
| Tpat_record _ , Tpat_record _ -> true
|
|
| Tpat_array p1s, Tpat_array p2s -> List.length p1s = List.length p2s
|
|
| _, (Tpat_any | Tpat_var(_)) -> true
|
|
| _, _ -> false
|
|
|
|
|
|
|
|
|
|
(* extract record fields as a whole *)
|
|
let record_arg p = match p.pat_desc with
|
|
| Tpat_any -> []
|
|
| Tpat_record args -> args
|
|
| _ -> fatal_error "Parmatch.as_record"
|
|
|
|
|
|
(* Raise Not_found when pos is not present in arg *)
|
|
|
|
|
|
let get_field pos arg =
|
|
let _,p = List.find (fun (lbl,_) -> pos = lbl.lbl_pos) arg in
|
|
p
|
|
|
|
|
|
let extract_fields omegas arg =
|
|
List.map
|
|
(fun (lbl,_) ->
|
|
try
|
|
get_field lbl.lbl_pos arg
|
|
with Not_found -> omega)
|
|
omegas
|
|
|
|
|
|
|
|
let sort_record p = match p.pat_desc with
|
|
| Tpat_record args ->
|
|
make_pat
|
|
(Tpat_record (sort_fields args))
|
|
p.pat_type p.pat_env
|
|
| _ -> p
|
|
|
|
let all_record_args lbls = match lbls with
|
|
| ({lbl_all=lbl_all},_)::_ ->
|
|
let t =
|
|
Array.map
|
|
(fun lbl -> lbl,omega) lbl_all in
|
|
List.iter
|
|
(fun ((lbl,_) as x) -> t.(lbl.lbl_pos) <- x)
|
|
lbls ;
|
|
Array.to_list t
|
|
| _ -> fatal_error "Parmatch.all_record_args"
|
|
|
|
|
|
(* Build argument list when p2 >= p1, where p1 is a simple pattern *)
|
|
let rec simple_match_args p1 p2 = match p2.pat_desc with
|
|
| Tpat_alias (p2,_) -> simple_match_args p1 p2
|
|
| Tpat_construct(cstr, args) -> args
|
|
| Tpat_variant(lab, Some arg, _) -> [arg]
|
|
| Tpat_tuple(args) -> args
|
|
| Tpat_record(args) -> extract_fields (record_arg p1) args
|
|
| Tpat_array(args) -> args
|
|
| (Tpat_any | Tpat_var(_)) ->
|
|
begin match p1.pat_desc with
|
|
Tpat_construct(_, args) -> omega_list args
|
|
| Tpat_variant(_, Some _, _) -> [omega]
|
|
| Tpat_tuple(args) -> omega_list args
|
|
| Tpat_record(args) -> omega_list args
|
|
| Tpat_array(args) -> omega_list args
|
|
| _ -> []
|
|
end
|
|
| _ -> []
|
|
|
|
(*
|
|
Normalize a pattern ->
|
|
all arguments are omega (simple pattern) and no more variables
|
|
*)
|
|
|
|
let rec normalize_pat q = match q.pat_desc with
|
|
| Tpat_any | Tpat_constant _ -> q
|
|
| Tpat_var _ -> make_pat Tpat_any q.pat_type q.pat_env
|
|
| Tpat_alias (p,_) -> normalize_pat p
|
|
| Tpat_tuple (args) ->
|
|
make_pat (Tpat_tuple (omega_list args)) q.pat_type q.pat_env
|
|
| Tpat_construct (c,args) ->
|
|
make_pat (Tpat_construct (c,omega_list args)) q.pat_type q.pat_env
|
|
| Tpat_variant (l, arg, row) ->
|
|
make_pat (Tpat_variant (l, may_map (fun _ -> omega) arg, row))
|
|
q.pat_type q.pat_env
|
|
| Tpat_array (args) ->
|
|
make_pat (Tpat_array (omega_list args)) q.pat_type q.pat_env
|
|
| Tpat_record (largs) ->
|
|
make_pat (Tpat_record (List.map (fun (lbl,_) -> lbl,omega) largs))
|
|
q.pat_type q.pat_env
|
|
| Tpat_or _ -> fatal_error "Parmatch.normalize_pat"
|
|
|
|
|
|
(*
|
|
Build normalized (cf. supra) discriminating pattern,
|
|
in the non-data type case
|
|
*)
|
|
|
|
let discr_pat q pss =
|
|
|
|
let rec acc_pat acc pss = match pss with
|
|
({pat_desc = Tpat_alias (p,_)}::ps)::pss ->
|
|
acc_pat acc ((p::ps)::pss)
|
|
| ({pat_desc = Tpat_or (p1,p2,_)}::ps)::pss ->
|
|
acc_pat acc ((p1::ps)::(p2::ps)::pss)
|
|
| ({pat_desc = (Tpat_any | Tpat_var _)}::_)::pss ->
|
|
acc_pat acc pss
|
|
| (({pat_desc = Tpat_tuple _} as p)::_)::_ -> normalize_pat p
|
|
| (({pat_desc = Tpat_record largs} as p)::_)::pss ->
|
|
let new_omegas =
|
|
List.fold_left
|
|
(fun r (lbl,_) ->
|
|
try
|
|
let _ = get_field lbl.lbl_pos r in
|
|
r
|
|
with Not_found ->
|
|
(lbl,omega)::r)
|
|
(record_arg acc)
|
|
largs in
|
|
acc_pat
|
|
(make_pat (Tpat_record new_omegas) p.pat_type p.pat_env)
|
|
pss
|
|
| _ -> acc in
|
|
|
|
match normalize_pat q with
|
|
| {pat_desc= (Tpat_any | Tpat_record _)} as q ->
|
|
sort_record (acc_pat q pss)
|
|
| q -> q
|
|
|
|
(*
|
|
In case a matching value is found, set actual arguments
|
|
of the matching pattern.
|
|
*)
|
|
|
|
let rec read_args xs r = match xs,r with
|
|
| [],_ -> [],r
|
|
| _::xs, arg::rest ->
|
|
let args,rest = read_args xs rest in
|
|
arg::args,rest
|
|
| _,_ ->
|
|
fatal_error "Parmatch.read_args"
|
|
|
|
let set_args q r = match q with
|
|
| {pat_desc = Tpat_tuple omegas} ->
|
|
let args,rest = read_args omegas r in
|
|
make_pat (Tpat_tuple args) q.pat_type q.pat_env::rest
|
|
| {pat_desc = Tpat_record omegas} ->
|
|
let args,rest = read_args omegas r in
|
|
make_pat
|
|
(Tpat_record
|
|
(List.map2 (fun (lbl,_) arg -> lbl,arg) omegas args))
|
|
q.pat_type q.pat_env::
|
|
rest
|
|
| {pat_desc = Tpat_construct (c,omegas)} ->
|
|
let args,rest = read_args omegas r in
|
|
make_pat
|
|
(Tpat_construct (c,args)) q.pat_type q.pat_env::
|
|
rest
|
|
| {pat_desc = Tpat_variant (l, omega, row)} ->
|
|
let arg, rest =
|
|
match omega, r with
|
|
Some _, a::r -> Some a, r
|
|
| None, r -> None, r
|
|
| _ -> assert false
|
|
in
|
|
make_pat
|
|
(Tpat_variant (l, arg, row)) q.pat_type q.pat_env::
|
|
rest
|
|
| {pat_desc = Tpat_array omegas} ->
|
|
let args,rest = read_args omegas r in
|
|
make_pat
|
|
(Tpat_array args) q.pat_type q.pat_env::
|
|
rest
|
|
| {pat_desc=Tpat_constant _|Tpat_any} ->
|
|
q::r (* case any is used in matching.ml *)
|
|
| _ -> fatal_error "Parmatch.set_args"
|
|
|
|
|
|
(* filter pss acording to pattern 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
|
|
|
|
(*
|
|
Filter pss in the ``extra case''. This applies :
|
|
- According to an extra constructor (datatype case, non-complete signature).
|
|
- Acordinng to anything (all-variables case).
|
|
*)
|
|
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
|
|
|
|
(*
|
|
Pattern p0 is the discriminating pattern,
|
|
returns [(q0,pss0) ; ... ; (qn,pssn)]
|
|
where the qi's are simple patterns and the pssi's are
|
|
matched matrices.
|
|
|
|
NOTES
|
|
* (qi,[]) is impossible.
|
|
* In the case when matching is useless (all-variable case),
|
|
returns []
|
|
*)
|
|
|
|
let filter_all pat0 pss =
|
|
|
|
let rec insert q qs env =
|
|
match env with
|
|
[] ->
|
|
let q0 = normalize_pat q in
|
|
[q0, [simple_match_args q0 q @ qs]]
|
|
| ((q0,pss) as c)::env ->
|
|
if simple_match q0 q
|
|
then (q0, ((simple_match_args q0 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
|
|
|
|
|
|
(*
|
|
Check whether the first column of env makes up a complete signature or
|
|
not.
|
|
*)
|
|
|
|
let full_match tdefs force env = match env with
|
|
| ({pat_desc = Tpat_construct ({cstr_tag=Cstr_exception _},_)},_)::_ ->
|
|
false
|
|
| ({pat_desc = Tpat_construct(c,_)},_) :: _ ->
|
|
List.length env = c.cstr_consts + c.cstr_nonconsts
|
|
| ({pat_desc = Tpat_variant(_,_,row)},_) :: _ ->
|
|
let fields =
|
|
List.map
|
|
(function ({pat_desc = Tpat_variant (tag, _, _)}, _) -> tag
|
|
| _ -> assert false)
|
|
env
|
|
in
|
|
let row = Btype.row_repr row in
|
|
if force && not row.row_fixed then begin
|
|
(* force=true, we are called from check_partial, and must close *)
|
|
let (ok, nm) =
|
|
List.fold_left
|
|
(fun (ok,nm) (tag,f) ->
|
|
match Btype.row_field_repr f with
|
|
Rabsent -> (ok, nm)
|
|
| Reither(_, _, false, e) ->
|
|
(* m=false means that this tag is not explicitly matched *)
|
|
Btype.set_row_field e Rabsent;
|
|
(ok, None)
|
|
| Reither (_, _, true, _)
|
|
(* m=true, do not discard matched tags, rather warn *)
|
|
| Rpresent _ ->
|
|
(ok && List.mem tag fields, nm))
|
|
(true, row.row_name) row.row_fields in
|
|
if not row.row_closed || nm != row.row_name then
|
|
(* this unification cannot fail *)
|
|
Ctype.unify tdefs row.row_more
|
|
(Btype.newgenty
|
|
(Tvariant {row with row_fields = []; row_more = Btype.newgenvar();
|
|
row_closed = true; row_name = nm}));
|
|
ok
|
|
end else
|
|
row.row_closed &&
|
|
List.for_all
|
|
(fun (tag,f) ->
|
|
Btype.row_field_repr f = Rabsent || List.mem tag fields)
|
|
row.row_fields
|
|
| ({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
|
|
| ({pat_desc = Tpat_array(_)},_) :: _ -> false
|
|
| _ -> fatal_error "Parmatch.full_match"
|
|
|
|
let extendable_match env = match env with
|
|
| ({pat_desc = Tpat_construct ({cstr_tag=Cstr_exception _},_)},_)::_ -> false
|
|
| ({pat_desc = Tpat_construct(c,_)} as p,_) :: _ ->
|
|
let path = get_type_path p.pat_type p.pat_env in
|
|
not
|
|
(Path.same path Predef.path_bool ||
|
|
Path.same path Predef.path_list ||
|
|
Path.same path Predef.path_option)
|
|
| _ -> false
|
|
|
|
|
|
(* complement constructor tags *)
|
|
let complete_tags nconsts nconstrs tags =
|
|
let seen_const = Array.create nconsts false
|
|
and seen_constr = Array.create nconstrs false in
|
|
List.iter
|
|
(function
|
|
| Cstr_constant i -> seen_const.(i) <- true
|
|
| Cstr_block i -> seen_constr.(i) <- true
|
|
| _ -> assert false)
|
|
tags ;
|
|
let r = ref [] in
|
|
for i = 0 to nconsts-1 do
|
|
if not seen_const.(i) then
|
|
r := Cstr_constant i :: !r
|
|
done ;
|
|
for i = 0 to nconstrs-1 do
|
|
if not seen_constr.(i) then
|
|
r := Cstr_block i :: !r
|
|
done ;
|
|
!r
|
|
|
|
(* build a pattern from a constructor list *)
|
|
let pat_of_constr ex_pat cstr =
|
|
{ex_pat with pat_desc = Tpat_construct (cstr,omegas cstr.cstr_arity)}
|
|
|
|
let rec pat_of_constrs ex_pat = function
|
|
| [] -> raise Empty
|
|
| [cstr] -> pat_of_constr ex_pat cstr
|
|
| cstr::rem ->
|
|
{ex_pat with
|
|
pat_desc=
|
|
Tpat_or
|
|
(pat_of_constr ex_pat cstr,
|
|
pat_of_constrs ex_pat rem, None)}
|
|
|
|
(* Sends back a pattern that complements constructor tags all_tag *)
|
|
let complete_constrs p all_tags = match p.pat_desc with
|
|
| Tpat_construct (c,_) ->
|
|
begin try
|
|
let not_tags = complete_tags c.cstr_consts c.cstr_nonconsts all_tags in
|
|
List.map
|
|
(fun tag ->
|
|
let _,targs = get_constr tag p.pat_type p.pat_env in
|
|
{c with
|
|
cstr_tag = tag ;
|
|
cstr_args = targs ;
|
|
cstr_arity = List.length targs})
|
|
not_tags
|
|
with
|
|
| Datarepr.Constr_not_found ->
|
|
fatal_error "Parmatch.complete_constr: constr_not_found"
|
|
end
|
|
| _ -> fatal_error "Parmatch.complete_constr"
|
|
|
|
|
|
(* Auxiliary for build_other *)
|
|
|
|
let build_other_constant proj make first next p env =
|
|
let all = List.map (fun (p, _) -> proj p.pat_desc) env in
|
|
let rec try_const i =
|
|
if List.mem i all
|
|
then try_const (next i)
|
|
else make_pat (make i) p.pat_type p.pat_env
|
|
in try_const first
|
|
|
|
(*
|
|
Builds a pattern that is incompatible with all patterns in
|
|
in the first column of env
|
|
*)
|
|
|
|
let build_other env = match env with
|
|
| ({pat_desc = Tpat_construct ({cstr_tag=Cstr_exception _} as c,_)},_) as p
|
|
::_ ->
|
|
make_pat
|
|
(Tpat_construct
|
|
({c with
|
|
cstr_tag=(Cstr_exception
|
|
(Path.Pident (Ident.create "*exception*")))},
|
|
[]))
|
|
Ctype.none Env.empty
|
|
| ({pat_desc = Tpat_construct (_,_)} as p,_) :: _ ->
|
|
let get_tag = function
|
|
| {pat_desc = Tpat_construct (c,_)} -> c.cstr_tag
|
|
| _ -> fatal_error "Parmatch.get_tag" in
|
|
let all_tags = List.map (fun (p,_) -> get_tag p) env in
|
|
pat_of_constrs p (complete_constrs p all_tags)
|
|
| ({pat_desc = Tpat_variant(_,_,row)} as p,_) :: _ ->
|
|
let tags =
|
|
List.map
|
|
(function ({pat_desc = Tpat_variant (tag, _, _)}, _) -> tag
|
|
| _ -> assert false)
|
|
env
|
|
in
|
|
let row = Btype.row_repr row in
|
|
let make_other_pat tag const =
|
|
let arg = if const then None else Some omega in
|
|
make_pat (Tpat_variant(tag, arg, row)) p.pat_type p.pat_env in
|
|
begin match
|
|
List.fold_left
|
|
(fun others (tag,f) ->
|
|
if List.mem tag tags then others else
|
|
match Btype.row_field_repr f with
|
|
Rabsent (* | Reither _ *) -> others
|
|
(* This one is called after erasing pattern info *)
|
|
| Reither (c, _, _, _) -> make_other_pat tag c :: others
|
|
| Rpresent arg -> make_other_pat tag (arg = None) :: others)
|
|
[] row.row_fields
|
|
with [] -> assert false
|
|
| pat::other_pats ->
|
|
List.fold_left
|
|
(fun p_res pat ->
|
|
make_pat (Tpat_or (pat, p_res, None)) p.pat_type p.pat_env)
|
|
pat other_pats
|
|
end
|
|
| ({pat_desc = Tpat_constant(Const_char _)} as p,_) :: _ ->
|
|
let all_chars =
|
|
List.map
|
|
(fun (p,_) -> match p.pat_desc with
|
|
| Tpat_constant (Const_char c) -> c
|
|
| _ -> assert false)
|
|
env in
|
|
|
|
let rec find_other i imax =
|
|
if i > imax then raise Not_found
|
|
else
|
|
let ci = Char.chr i in
|
|
if List.mem ci all_chars then
|
|
find_other (i+1) imax
|
|
else
|
|
make_pat (Tpat_constant (Const_char ci)) p.pat_type p.pat_env in
|
|
let rec try_chars = function
|
|
| [] -> omega
|
|
| (c1,c2) :: rest ->
|
|
try
|
|
find_other (Char.code c1) (Char.code c2)
|
|
with
|
|
| Not_found -> try_chars rest in
|
|
|
|
try_chars
|
|
[ 'a', 'z' ; 'A', 'Z' ; '0', '9' ;
|
|
' ', '~' ; Char.chr 0 , Char.chr 255]
|
|
|
|
| ({pat_desc=(Tpat_constant (Const_int _))} as p,_) :: _ ->
|
|
build_other_constant
|
|
(function Tpat_constant(Const_int i) -> i | _ -> assert false)
|
|
(function i -> Tpat_constant(Const_int i))
|
|
0 succ p env
|
|
| ({pat_desc=(Tpat_constant (Const_int32 _))} as p,_) :: _ ->
|
|
build_other_constant
|
|
(function Tpat_constant(Const_int32 i) -> i | _ -> assert false)
|
|
(function i -> Tpat_constant(Const_int32 i))
|
|
0l Int32.succ p env
|
|
| ({pat_desc=(Tpat_constant (Const_int64 _))} as p,_) :: _ ->
|
|
build_other_constant
|
|
(function Tpat_constant(Const_int64 i) -> i | _ -> assert false)
|
|
(function i -> Tpat_constant(Const_int64 i))
|
|
0L Int64.succ p env
|
|
| ({pat_desc=(Tpat_constant (Const_nativeint _))} as p,_) :: _ ->
|
|
build_other_constant
|
|
(function Tpat_constant(Const_nativeint i) -> i | _ -> assert false)
|
|
(function i -> Tpat_constant(Const_nativeint i))
|
|
0n Nativeint.succ p env
|
|
| ({pat_desc=(Tpat_constant (Const_string _))} as p,_) :: _ ->
|
|
build_other_constant
|
|
(function Tpat_constant(Const_string s) -> String.length s
|
|
| _ -> assert false)
|
|
(function i -> Tpat_constant(Const_string(String.make i '*')))
|
|
0 succ p env
|
|
| ({pat_desc=(Tpat_constant (Const_float _))} as p,_) :: _ ->
|
|
build_other_constant
|
|
(function Tpat_constant(Const_float f) -> float_of_string f
|
|
| _ -> assert false)
|
|
(function f -> Tpat_constant(Const_float (string_of_float f)))
|
|
0.0 (fun f -> f +. 1.0) p env
|
|
|
|
| ({pat_desc = Tpat_array args} as p,_)::_ ->
|
|
let all_lengths =
|
|
List.map
|
|
(fun (p,_) -> match p.pat_desc with
|
|
| Tpat_array args -> List.length args
|
|
| _ -> assert false)
|
|
env in
|
|
let rec try_arrays l =
|
|
if List.mem l all_lengths then try_arrays (l+1)
|
|
else
|
|
make_pat
|
|
(Tpat_array (omegas l))
|
|
p.pat_type p.pat_env in
|
|
try_arrays 0
|
|
| [] -> omega
|
|
| _ -> omega
|
|
|
|
(*
|
|
Core function :
|
|
Is the last row of pattern matrix pss + qs satisfiable ?
|
|
That is :
|
|
Does there 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)
|
|
NOTE:
|
|
satisfiable assumes that any pattern has at least one
|
|
matching value (see first case)
|
|
quid of << absent >> variants ??
|
|
|
|
*)
|
|
|
|
let rec has_instance p = match p.pat_desc with
|
|
| Tpat_variant (l,_,r) when is_absent l r -> false
|
|
| Tpat_any | Tpat_var _ | Tpat_constant _ | Tpat_variant (_,None,_) -> true
|
|
| Tpat_alias (p,_) | Tpat_variant (_,Some p,_) -> has_instance p
|
|
| Tpat_or (p1,p2,_) -> has_instance p1 || has_instance p2
|
|
| Tpat_construct (_,ps) | Tpat_tuple ps | Tpat_array ps -> has_instances ps
|
|
| Tpat_record lps -> has_instances (List.map snd lps)
|
|
|
|
and has_instances = function
|
|
| [] -> true
|
|
| q::rem -> has_instance q && has_instances rem
|
|
|
|
let rec satisfiable pss qs = match pss with
|
|
| [] -> has_instances qs
|
|
| _ ->
|
|
match qs with
|
|
| [] -> false
|
|
| {pat_desc = Tpat_or(q1,q2,_)}::qs ->
|
|
satisfiable pss (q1::qs) || satisfiable pss (q2::qs)
|
|
| {pat_desc = Tpat_alias(q,_)}::qs ->
|
|
satisfiable pss (q::qs)
|
|
| {pat_desc = (Tpat_any | Tpat_var(_))}::qs ->
|
|
let q0 = discr_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 ->
|
|
(not (full_match Env.empty false constrs) &&
|
|
satisfiable (filter_extra pss) qs) ||
|
|
List.exists
|
|
(fun (p,pss) -> satisfiable pss (simple_match_args p omega @ qs))
|
|
constrs
|
|
end
|
|
| {pat_desc=Tpat_variant (l,_,r)}::_ when is_absent l r -> false
|
|
| q::qs ->
|
|
let q0 = discr_pat q pss in
|
|
satisfiable (filter_one q0 pss) (simple_match_args q0 q @ qs)
|
|
|
|
(*
|
|
Like satisfiable, looking for a matching value with an extra constructor.
|
|
That is, look for the situation where adding one constructor
|
|
would NOT yield a non-exhaustive matching.
|
|
*)
|
|
|
|
let relevant_location loc r = match r with
|
|
| None -> None
|
|
| Some rloc ->
|
|
if rloc = Location.none then
|
|
Some loc
|
|
else
|
|
r
|
|
|
|
let rec satisfiable_extra some pss qs = match qs with
|
|
| [] -> if pss = [] then some else None
|
|
| {pat_desc = Tpat_or(q1,q2,_)}::qs ->
|
|
let r1 = satisfiable_extra some pss (q1::qs) in
|
|
begin match r1 with
|
|
| Some _ -> r1
|
|
| None -> satisfiable_extra some pss (q2::qs)
|
|
end
|
|
| {pat_desc = Tpat_alias(q,_)}::qs ->
|
|
satisfiable_extra some pss (q::qs)
|
|
| {pat_desc = (Tpat_any | Tpat_var(_))} as q::qs ->
|
|
let q0 = discr_pat omega pss in
|
|
let r =
|
|
match filter_all q0 pss with
|
|
(* first column of pss is made of variables only *)
|
|
| [] -> satisfiable_extra some (filter_extra pss) qs
|
|
| constrs ->
|
|
if extendable_match constrs then
|
|
let rloc =
|
|
satisfiable_extra (Some q.pat_loc) (filter_extra pss) qs in
|
|
match rloc with
|
|
| Some loc -> rloc
|
|
| None -> try_many_extra some qs constrs
|
|
else
|
|
try_many_extra some qs constrs in
|
|
relevant_location q.pat_loc r
|
|
| q::qs ->
|
|
let q0 = discr_pat q pss in
|
|
relevant_location
|
|
q.pat_loc
|
|
(satisfiable_extra
|
|
some (filter_one q0 pss) (simple_match_args q0 q @ qs))
|
|
|
|
and try_many_extra some qs = function
|
|
| [] -> None
|
|
| (p,pss)::rem ->
|
|
let rloc = satisfiable_extra some pss (simple_match_args p omega @ qs) in
|
|
match rloc with
|
|
| Some _ -> rloc
|
|
| None -> try_many_extra some qs rem
|
|
|
|
|
|
(*
|
|
Now another satisfiable function that additionally
|
|
supplies an example of a matching value.
|
|
|
|
This function should be called for exhaustiveness check only.
|
|
It impacts variant typing
|
|
*)
|
|
|
|
type 'a result =
|
|
| Rnone (* No matching value *)
|
|
| Rsome of 'a (* This matching value *)
|
|
|
|
(* boolean argument ``variants'' is unused at present *)
|
|
let rec try_many variants f = function
|
|
| [] -> Rnone
|
|
| x::rest ->
|
|
begin match f x with
|
|
| Rnone -> try_many variants f rest
|
|
| r ->
|
|
if variants then ignore (try_many variants f rest);
|
|
r
|
|
end
|
|
|
|
let rec exhaust variants tdefs pss n = match pss with
|
|
| [] -> Rsome (omegas n)
|
|
| []::_ -> Rnone
|
|
| pss ->
|
|
let q0 = discr_pat omega pss in
|
|
begin match filter_all q0 pss with
|
|
(* first column of pss is made of variables only *)
|
|
[] ->
|
|
begin match exhaust variants tdefs (filter_extra pss) (n-1) with
|
|
| Rsome r -> Rsome (q0::r)
|
|
| r -> r
|
|
end
|
|
| constrs ->
|
|
let try_non_omega (p,pss) =
|
|
match
|
|
exhaust variants tdefs pss
|
|
(List.length (simple_match_args p omega) + n - 1)
|
|
with
|
|
| Rsome r -> Rsome (set_args p r)
|
|
| r -> r in
|
|
if full_match tdefs true constrs
|
|
then try_many variants try_non_omega constrs
|
|
else
|
|
match exhaust variants tdefs (filter_extra pss) (n-1) with
|
|
| Rnone -> try_many variants try_non_omega constrs
|
|
| Rsome r ->
|
|
(* try all constructors anyway, for variant typing ! *)
|
|
(* Note: it may impact dramatically on cost *)
|
|
if variants then
|
|
ignore (try_many variants try_non_omega constrs) ;
|
|
try
|
|
Rsome (build_other constrs::r)
|
|
with
|
|
(* cannot occur, since constructors don't make a full signature *)
|
|
| Empty -> fatal_error "Parmatch.exhaust"
|
|
|
|
end
|
|
|
|
|
|
(* Yet another satisfiable fonction *)
|
|
|
|
(*
|
|
This time every_satisfiable pss qs checks the
|
|
utility of every expansion of qs.
|
|
Expansion means expansion of or-patterns inside qs
|
|
*)
|
|
|
|
type answer =
|
|
| Used (* Useful pattern *)
|
|
| Unused (* Useless pattern *)
|
|
| Upartial of Typedtree.pattern list (* Neither, with list of useless pattern *)
|
|
|
|
|
|
let pretty_pat p =
|
|
top_pretty Format.str_formatter p ;
|
|
prerr_string (Format.flush_str_formatter ())
|
|
|
|
type matrix = pattern list list
|
|
|
|
let pretty_line ps =
|
|
List.iter
|
|
(fun p ->
|
|
top_pretty Format.str_formatter p ;
|
|
prerr_string " <" ;
|
|
prerr_string (Format.flush_str_formatter ()) ;
|
|
prerr_string ">")
|
|
ps
|
|
|
|
let pretty_matrix pss =
|
|
prerr_endline "begin matrix" ;
|
|
List.iter
|
|
(fun ps ->
|
|
pretty_line ps ;
|
|
prerr_endline "")
|
|
pss ;
|
|
prerr_endline "end matrix"
|
|
|
|
(* this row type enable column processing inside the matrix
|
|
- left -> elements not to be processed,
|
|
- right -> elements to be processed
|
|
*)
|
|
type 'a row = {no_ors : 'a list ; ors : 'a list ; active : 'a list}
|
|
|
|
|
|
let pretty_row {ors=ors ; no_ors=no_ors; active=active} =
|
|
pretty_line ors ; prerr_string " *" ;
|
|
pretty_line no_ors ; prerr_string " *" ;
|
|
pretty_line active
|
|
|
|
let pretty_rows rs =
|
|
prerr_endline "begin matrix" ;
|
|
List.iter
|
|
(fun r ->
|
|
pretty_row r ;
|
|
prerr_endline "")
|
|
rs ;
|
|
prerr_endline "end matrix"
|
|
|
|
(* Initial build *)
|
|
let make_row ps = {ors=[] ; no_ors=[]; active=ps}
|
|
|
|
let make_rows pss = List.map make_row pss
|
|
|
|
|
|
(* Useful to detect and expand or pats inside as pats *)
|
|
let rec unalias p = match p.pat_desc with
|
|
| Tpat_alias (p,_) -> unalias p
|
|
| _ -> p
|
|
|
|
|
|
let is_var p = match (unalias p).pat_desc with
|
|
| Tpat_any|Tpat_var _ -> true
|
|
| _ -> false
|
|
|
|
let is_var_column rs =
|
|
List.for_all
|
|
(fun r -> match r.active with
|
|
| p::_ -> is_var p
|
|
| [] -> assert false)
|
|
rs
|
|
|
|
(* Standard or-args for left-to-right matching *)
|
|
let rec or_args p = match p.pat_desc with
|
|
| Tpat_or (p1,p2,_) -> p1,p2
|
|
| Tpat_alias (p,_) -> or_args p
|
|
| _ -> assert false
|
|
|
|
(* Just remove current column *)
|
|
let remove r = match r.active with
|
|
| _::rem -> {r with active=rem}
|
|
| [] -> assert false
|
|
|
|
let remove_column rs = List.map remove rs
|
|
|
|
(* Current column has been processed *)
|
|
let push_no_or r = match r.active with
|
|
| p::rem -> { r with no_ors = p::r.no_ors ; active=rem}
|
|
| [] -> assert false
|
|
|
|
let push_or r = match r.active with
|
|
| p::rem -> { r with ors = p::r.ors ; active=rem}
|
|
| [] -> assert false
|
|
|
|
let push_or_column rs = List.map push_or rs
|
|
and push_no_or_column rs = List.map push_no_or rs
|
|
|
|
(* Those are adaptations of the previous homonymous functions that
|
|
work on the current column, instead of the first column
|
|
*)
|
|
|
|
let discr_pat q rs =
|
|
discr_pat q (List.map (fun r -> r.active) rs)
|
|
|
|
let filter_one q rs =
|
|
let rec filter_rec rs = match rs with
|
|
| [] -> []
|
|
| r::rem ->
|
|
match r.active with
|
|
| [] -> assert false
|
|
| {pat_desc = Tpat_alias(p,_)}::ps ->
|
|
filter_rec ({r with active = p::ps}::rem)
|
|
| {pat_desc = Tpat_or(p1,p2,_)}::ps ->
|
|
filter_rec
|
|
({r with active = p1::ps}::
|
|
{r with active = p2::ps}::
|
|
rem)
|
|
| p::ps ->
|
|
if simple_match q p then
|
|
{r with active=simple_match_args q p @ ps} :: filter_rec rem
|
|
else
|
|
filter_rec rem in
|
|
filter_rec rs
|
|
|
|
|
|
(* Back to normal matrices *)
|
|
let make_vector r = r.no_ors
|
|
|
|
let make_matrix rs = List.map make_vector rs
|
|
|
|
|
|
(* Standard union on answers *)
|
|
let union_res r1 r2 = match r1, r2 with
|
|
| (Unused,_)
|
|
| (_, Unused) -> Unused
|
|
| Used,_ -> r2
|
|
| _, Used -> r1
|
|
| Upartial u1, Upartial u2 -> Upartial (u1@u2)
|
|
|
|
(* propose or pats for expansion *)
|
|
let extract_elements qs =
|
|
let rec do_rec seen = function
|
|
| [] -> []
|
|
| q::rem ->
|
|
{no_ors= List.rev_append seen rem @ qs.no_ors ;
|
|
ors=[] ;
|
|
active = [q]}::
|
|
do_rec (q::seen) rem in
|
|
do_rec [] qs.ors
|
|
|
|
(* idem for matrices *)
|
|
let transpose rs = match rs with
|
|
| [] -> assert false
|
|
| r::rem ->
|
|
let i = List.map (fun x -> [x]) r in
|
|
List.fold_left
|
|
(List.map2 (fun r x -> x::r))
|
|
i rem
|
|
|
|
let extract_columns pss qs = match pss with
|
|
| [] -> List.map (fun _ -> []) qs.ors
|
|
| _ ->
|
|
let rows = List.map extract_elements pss in
|
|
transpose rows
|
|
|
|
(* Core function
|
|
The idea is to first look for or patterns (recursive case), then
|
|
check or-patterns argument usefulness (terminal case)
|
|
*)
|
|
|
|
let rec every_satisfiables pss qs = match qs.active with
|
|
| [] ->
|
|
(* qs is now partitionned, check usefulness *)
|
|
begin match qs.ors with
|
|
| [] -> (* no or-patterns *)
|
|
if satisfiable (make_matrix pss) (make_vector qs) then
|
|
Used
|
|
else
|
|
Unused
|
|
| _ -> (* n or-patterns -> 2n expansions *)
|
|
List.fold_right2
|
|
(fun pss qs r -> match r with
|
|
| Unused -> Unused
|
|
| _ ->
|
|
match qs.active with
|
|
| [q] ->
|
|
let q1,q2 = or_args q in
|
|
let r_loc = every_both pss qs q1 q2 in
|
|
union_res r r_loc
|
|
| _ -> assert false)
|
|
(extract_columns pss qs) (extract_elements qs)
|
|
Used
|
|
end
|
|
| q::rem ->
|
|
let uq = unalias q in
|
|
begin match uq.pat_desc with
|
|
| Tpat_any | Tpat_var _ ->
|
|
if is_var_column pss then
|
|
(* forget about ``all-variable'' columns now *)
|
|
every_satisfiables (remove_column pss) (remove qs)
|
|
else
|
|
(* otherwise this is direct food for satisfiable *)
|
|
every_satisfiables (push_no_or_column pss) (push_no_or qs)
|
|
| Tpat_or (q1,q2,_) ->
|
|
if
|
|
q1.pat_loc.Location.loc_ghost &&
|
|
q2.pat_loc.Location.loc_ghost
|
|
then
|
|
(* syntactically generated or-pats should not be expanded *)
|
|
every_satisfiables (push_no_or_column pss) (push_no_or qs)
|
|
else
|
|
(* this is a real or-pattern *)
|
|
every_satisfiables (push_or_column pss) (push_or qs)
|
|
| Tpat_variant (l,_,r) when is_absent l r -> (* Ah Jacques... *)
|
|
Unused
|
|
| _ ->
|
|
(* standard case, filter matrix *)
|
|
let q0 = discr_pat q pss in
|
|
every_satisfiables
|
|
(filter_one q0 pss)
|
|
{qs with active=simple_match_args q0 q @ rem}
|
|
end
|
|
|
|
(*
|
|
This function ``every_both'' performs the usefulness check
|
|
of or-pat q1|q2.
|
|
The trick is to call every_satisfied twice with
|
|
current active columns restricted to q1 and q2,
|
|
That way,
|
|
- others orpats in qs.ors will not get expanded.
|
|
- all matching work performed on qs.no_ors is not performed again.
|
|
*)
|
|
and every_both pss qs q1 q2 =
|
|
let qs1 = {qs with active=[q1]}
|
|
and qs2 = {qs with active=[q2]} in
|
|
let r1 = every_satisfiables pss qs1
|
|
and r2 = every_satisfiables (if compat q1 q2 then qs1::pss else pss) qs2 in
|
|
match r1 with
|
|
| Unused ->
|
|
begin match r2 with
|
|
| Unused -> Unused
|
|
| Used -> Upartial [q1]
|
|
| Upartial u2 -> Upartial (q1::u2)
|
|
end
|
|
| Used ->
|
|
begin match r2 with
|
|
| Unused -> Upartial [q2]
|
|
| _ -> r2
|
|
end
|
|
| Upartial u1 ->
|
|
begin match r2 with
|
|
| Unused -> Upartial (u1@[q2])
|
|
| Used -> r1
|
|
| Upartial u2 -> Upartial (u1 @ u2)
|
|
end
|
|
|
|
|
|
|
|
|
|
(* le_pat p q means, forall V, V matches q implies V matches p *)
|
|
let rec le_pat p q =
|
|
match (p.pat_desc, q.pat_desc) with
|
|
| (Tpat_var _|Tpat_any),_ -> true
|
|
(* Absent variants have no instance *)
|
|
| _, Tpat_variant (l,_,row) when is_absent l row -> true
|
|
| Tpat_alias(p,_), _ -> le_pat p q
|
|
| _, Tpat_alias(q,_) -> le_pat p 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_variant(l1,Some p1,_), Tpat_variant(l2,Some p2,_) ->
|
|
(l1 = l2 && le_pat p1 p2)
|
|
| Tpat_variant(l1,None,r1), Tpat_variant(l2,None,_) ->
|
|
l1 = l2
|
|
| Tpat_tuple(ps), Tpat_tuple(qs) -> le_pats ps qs
|
|
| Tpat_record l1, Tpat_record l2 ->
|
|
let ps,qs = records_args l1 l2 in
|
|
le_pats ps qs
|
|
| Tpat_array(ps), Tpat_array(qs) ->
|
|
List.length ps = List.length qs && le_pats ps qs
|
|
(* In all other cases, enumeration is performed *)
|
|
| _,_ ->
|
|
not (satisfiable [[p]] [q])
|
|
|
|
|
|
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 le ps =
|
|
let rec select_rec r = function
|
|
[] -> r
|
|
| p::ps ->
|
|
if List.exists (fun p0 -> le p0 p) ps
|
|
then select_rec r ps
|
|
else select_rec (p::r) ps in
|
|
select_rec [] (select_rec [] ps)
|
|
|
|
|
|
(*
|
|
lub p q is a pattern that matches all values matched by p and q
|
|
may raise Empty, when p and q and not compatible
|
|
*)
|
|
|
|
let rec lub p q = match p.pat_desc,q.pat_desc with
|
|
| Tpat_alias (p,_),_ -> lub p q
|
|
| _,Tpat_alias (q,_) -> lub p q
|
|
| (Tpat_any|Tpat_var _),_ -> q
|
|
| _,(Tpat_any|Tpat_var _) -> p
|
|
| Tpat_or (p1,p2,_),_ -> orlub p1 p2 q
|
|
| _,Tpat_or (q1,q2,_) -> orlub q1 q2 p (* Thanks god, lub is commutative *)
|
|
| Tpat_constant c1, Tpat_constant c2 when c1=c2 -> p
|
|
| Tpat_tuple ps, Tpat_tuple qs ->
|
|
let rs = lubs ps qs in
|
|
make_pat (Tpat_tuple rs) p.pat_type p.pat_env
|
|
| Tpat_construct (c1,ps1), Tpat_construct (c2,ps2)
|
|
when c1.cstr_tag = c2.cstr_tag ->
|
|
let rs = lubs ps1 ps2 in
|
|
make_pat (Tpat_construct (c1,rs)) p.pat_type p.pat_env
|
|
| Tpat_variant(l1,Some p1,row), Tpat_variant(l2,Some p2,_)
|
|
when l1=l2 && not (is_absent l1 row) ->
|
|
let r=lub p1 p2 in
|
|
make_pat (Tpat_variant (l1,Some r,row)) p.pat_type p.pat_env
|
|
| Tpat_variant (l1,None,row), Tpat_variant(l2,None,_)
|
|
when l1 = l2 && not (is_absent l1 row) -> p
|
|
| Tpat_record l1,Tpat_record l2 ->
|
|
let rs = record_lubs l1 l2 in
|
|
make_pat (Tpat_record rs) p.pat_type p.pat_env
|
|
| Tpat_array ps, Tpat_array qs
|
|
when List.length ps = List.length qs ->
|
|
let rs = lubs ps qs in
|
|
make_pat (Tpat_array rs) p.pat_type p.pat_env
|
|
| _,_ ->
|
|
raise Empty
|
|
|
|
and orlub p1 p2 q =
|
|
try
|
|
let r1 = lub p1 q in
|
|
try
|
|
{q with pat_desc=(Tpat_or (r1,lub p2 q,None))}
|
|
with
|
|
| Empty -> r1
|
|
with
|
|
| Empty -> lub p2 q
|
|
|
|
and record_lubs l1 l2 =
|
|
let l1 = sort_fields l1 and l2 = sort_fields l2 in
|
|
let rec lub_rec l1 l2 = match l1,l2 with
|
|
| [],_ -> l2
|
|
| _,[] -> l1
|
|
| (lbl1,p1)::rem1, (lbl2,p2)::rem2 ->
|
|
if lbl1.lbl_pos < lbl2.lbl_pos then
|
|
(lbl1,p1)::lub_rec rem1 l2
|
|
else if lbl2.lbl_pos < lbl1.lbl_pos then
|
|
(lbl2,p2)::lub_rec l1 rem2
|
|
else
|
|
(lbl1,lub p1 p2)::lub_rec rem1 rem2 in
|
|
lub_rec l1 l2
|
|
|
|
and lubs ps qs = match ps,qs with
|
|
| p::ps, q::qs -> lub p q :: lubs ps qs
|
|
| _,_ -> []
|
|
|
|
|
|
(******************************)
|
|
(* Entry points *)
|
|
(* - Partial match *)
|
|
(* - Unused match case *)
|
|
(******************************)
|
|
|
|
|
|
(*
|
|
A small cvs commit/commit discussion....
|
|
JG:
|
|
Exhaustiveness of matching MUST be checked, even
|
|
when the warning is excluded explicitely by user.
|
|
LM:
|
|
Why such a strange thing ?
|
|
JG:
|
|
Because the typing of variants depends on it.
|
|
LM:
|
|
Ok, note that by contrast, unused clause check still can be avoided at
|
|
user request.
|
|
*)
|
|
(*
|
|
Build up a working pattern matrix.
|
|
- Forget about guarded patterns
|
|
*)
|
|
|
|
let has_guard act = match act.exp_desc with
|
|
| Texp_when(_, _) -> true
|
|
| _ -> false
|
|
|
|
|
|
let rec initial_matrix = function
|
|
[] -> []
|
|
| (pat, act) :: rem ->
|
|
if has_guard act
|
|
then
|
|
initial_matrix rem
|
|
else
|
|
[pat] :: initial_matrix rem
|
|
|
|
(*
|
|
All the following ``*_all'' functions
|
|
check whether a given value [v] is matched by some row in pss.
|
|
They are used to whether the exhaustiveness exemple is
|
|
matched by a guarded clause
|
|
*)
|
|
|
|
|
|
exception NoGuard
|
|
|
|
let rec initial_all no_guard = function
|
|
| [] ->
|
|
if no_guard then
|
|
raise NoGuard
|
|
else
|
|
[]
|
|
| (pat, act) :: rem ->
|
|
([pat], pat.pat_loc) :: initial_all (no_guard && not (has_guard act)) rem
|
|
|
|
|
|
let rec do_filter_var = function
|
|
| (_::ps,loc)::rem -> (ps,loc)::do_filter_var rem
|
|
| _ -> []
|
|
|
|
let do_filter_one q pss =
|
|
let rec filter_rec = function
|
|
| ({pat_desc = Tpat_alias(p,_)}::ps,loc)::pss ->
|
|
filter_rec ((p::ps,loc)::pss)
|
|
| ({pat_desc = Tpat_or(p1,p2,_)}::ps,loc)::pss ->
|
|
filter_rec ((p1::ps,loc)::(p2::ps,loc)::pss)
|
|
| (p::ps,loc)::pss ->
|
|
if simple_match q p
|
|
then (simple_match_args q p @ ps, loc) :: filter_rec pss
|
|
else filter_rec pss
|
|
| _ -> [] in
|
|
filter_rec pss
|
|
|
|
let rec do_match pss qs = match qs with
|
|
| [] ->
|
|
begin match pss with
|
|
| ([],loc)::_ -> Some loc
|
|
| _ -> None
|
|
end
|
|
| q::qs -> match q with
|
|
| {pat_desc = Tpat_or (q1,q2,_)} ->
|
|
begin match do_match pss (q1::qs) with
|
|
| None -> do_match pss (q2::qs)
|
|
| r -> r
|
|
end
|
|
| {pat_desc = Tpat_any} ->
|
|
do_match (do_filter_var pss) qs
|
|
| _ ->
|
|
let q0 = normalize_pat q in
|
|
do_match (do_filter_one q0 pss) (simple_match_args q0 q @ qs)
|
|
|
|
|
|
let check_partial_all v casel =
|
|
try
|
|
let pss = initial_all true casel in
|
|
do_match pss [v]
|
|
with
|
|
| NoGuard -> None
|
|
|
|
(* look for variants *)
|
|
let rec look_variant p = match p.pat_desc with
|
|
| Tpat_variant (_,_,_) -> true
|
|
| Tpat_any | Tpat_var _ | Tpat_constant _ -> false
|
|
| Tpat_alias (p,_) -> look_variant p
|
|
| Tpat_or (p1,p2,_) -> look_variant p1 || look_variant p2
|
|
| Tpat_construct (_,ps) | Tpat_tuple ps | Tpat_array ps -> look_variants ps
|
|
| Tpat_record lps -> look_variants (List.map snd lps)
|
|
|
|
and look_variants = function
|
|
| [] -> false
|
|
| q::rem -> look_variant q || look_variants rem
|
|
|
|
|
|
let check_partial tdefs loc casel =
|
|
let variant_inside = List.exists (fun (p,_) -> look_variant p) casel in
|
|
let pss = initial_matrix casel in
|
|
let pss = get_mins le_pats pss in
|
|
match pss with
|
|
| [] ->
|
|
(*
|
|
This can occur
|
|
- For empty matches generated by ocamlp4 (no warning)
|
|
- when all patterns have guards (then, casel <> [])
|
|
(specific warning)
|
|
Then match MUST be considered non-exhaustive,
|
|
otherwise compilation of PM is broken.
|
|
*)
|
|
begin match casel with
|
|
| [] -> ()
|
|
| _ ->
|
|
Location.prerr_warning loc
|
|
(Warnings.Other
|
|
"Bad style, all clauses in this pattern-matching are guarded.")
|
|
end ;
|
|
Partial
|
|
| ps::_ ->
|
|
begin match exhaust variant_inside tdefs pss (List.length ps) with
|
|
| Rnone -> Total
|
|
| Rsome [v] ->
|
|
let errmsg =
|
|
try
|
|
let buf = Buffer.create 16 in
|
|
let fmt = formatter_of_buffer buf in
|
|
top_pretty fmt v;
|
|
begin match check_partial_all v casel with
|
|
| None -> ()
|
|
| Some _ ->
|
|
(* This is ``Some l'', where l is the location of
|
|
a possibly matching clause.
|
|
I forget about l, because printing two locations
|
|
is a pain in the top-level *)
|
|
Buffer.add_string buf
|
|
"\n(However, some guarded clause may match this value.)"
|
|
end ;
|
|
Buffer.contents buf
|
|
with _ ->
|
|
"" in
|
|
Location.prerr_warning loc (Warnings.Partial_match errmsg) ;
|
|
Partial
|
|
| _ ->
|
|
fatal_error "Parmatch.check_partial"
|
|
end
|
|
|
|
|
|
let location_of_clause = function
|
|
pat :: _ -> pat.pat_loc
|
|
| _ -> fatal_error "Parmatch.location_of_clause"
|
|
|
|
let seen_pat q pss = [q]::pss
|
|
|
|
(* Extra check
|
|
Will this clause match if someone adds a constructor somewhere
|
|
*)
|
|
|
|
let warn_fragile () = Warnings.is_active (Warnings.Fragile_pat "")
|
|
|
|
let check_used_extra pss qs =
|
|
if warn_fragile () then begin
|
|
match satisfiable_extra None pss qs with
|
|
| Some location ->
|
|
Location.prerr_warning
|
|
location
|
|
(Warnings.Fragile_pat "")
|
|
| None -> ()
|
|
end
|
|
|
|
|
|
|
|
let check_unused tdefs casel =
|
|
if Warnings.is_active Warnings.Unused_match then
|
|
let rec do_rec pref = function
|
|
| [] -> ()
|
|
| (q,act as clause)::rem ->
|
|
let qs = [q] in
|
|
begin try
|
|
let pss = get_mins le_pats (List.filter (compats qs) pref) in
|
|
let r = every_satisfiables (make_rows pss) (make_row qs) in
|
|
match r with
|
|
| Unused ->
|
|
Location.prerr_warning
|
|
(location_of_clause qs) Warnings.Unused_match
|
|
| Upartial ps ->
|
|
List.iter
|
|
(fun p ->
|
|
Location.prerr_warning
|
|
p.pat_loc Warnings.Unused_pat)
|
|
ps
|
|
| Used ->
|
|
check_used_extra pss qs
|
|
with e -> (* useless ? *)
|
|
Location.prerr_warning (location_of_clause qs)
|
|
(Warnings.Other "Fatal Error in Parmatch.check_unused") ;
|
|
raise e
|
|
end ;
|
|
|
|
if has_guard act then
|
|
do_rec pref rem
|
|
else
|
|
do_rec (seen_pat q pref) rem in
|
|
|
|
|
|
|
|
do_rec [] casel
|