1335 lines
41 KiB
OCaml
1335 lines
41 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_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 s) ->
|
|
fprintf ppf "%s" s
|
|
| 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 simple_match_args p1 p2 =
|
|
match p2.pat_desc with
|
|
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 *)
|
|
e := Some 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"
|
|
|
|
(* 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"
|
|
|
|
|
|
(*
|
|
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,_) :: _ ->
|
|
let all_ints =
|
|
List.map
|
|
(fun (p,_) -> match p.pat_desc with
|
|
| Tpat_constant (Const_int i) -> i
|
|
| _ -> assert false)
|
|
env in
|
|
let rec try_ints i =
|
|
if List.mem i all_ints then try_ints (i+1)
|
|
else
|
|
make_pat
|
|
(Tpat_constant (Const_int i)) p.pat_type p.pat_env in
|
|
try_ints 0
|
|
| ({pat_desc=(Tpat_constant (Const_string _))} as p,_) :: _ ->
|
|
let all_lengths =
|
|
List.map
|
|
(fun (p,_) -> match p.pat_desc with
|
|
| Tpat_constant (Const_string s) -> String.length s
|
|
| _ -> assert false)
|
|
env in
|
|
let rec try_strings i =
|
|
if List.mem i all_lengths then try_strings (i+1)
|
|
else
|
|
make_pat
|
|
(Tpat_constant (Const_string (String.make i '*')))
|
|
p.pat_type p.pat_env in
|
|
try_strings 0
|
|
| ({pat_desc=(Tpat_constant (Const_float _))} as p,_) :: _ ->
|
|
let all_floats =
|
|
List.map
|
|
(fun (p,_) -> match p.pat_desc with
|
|
| Tpat_constant (Const_float s) -> float_of_string s
|
|
| _ -> assert false)
|
|
env in
|
|
let rec try_floats f =
|
|
if List.mem f all_floats then try_floats (f +. 1.0)
|
|
else
|
|
make_pat
|
|
(Tpat_constant (Const_float (string_of_float f^".0")))
|
|
p.pat_type p.pat_env in
|
|
try_floats 0.0
|
|
| ({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)
|
|
|
|
|
|
(*
|
|
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 *)
|
|
|
|
let rec try_many f = function
|
|
| [] -> Rnone
|
|
| x::rest ->
|
|
begin match f x with
|
|
| Rnone -> try_many f rest
|
|
| r -> r
|
|
end
|
|
|
|
let rec exhaust tdefs pss qs = match pss with
|
|
| [] -> Rsome qs
|
|
| []::_ -> Rnone
|
|
| pss -> match qs with
|
|
| [] -> assert false
|
|
| _::qs ->
|
|
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 tdefs (filter_extra pss) qs with
|
|
| Rsome r -> Rsome (q0::r)
|
|
| r -> r
|
|
end
|
|
| constrs ->
|
|
let try_non_omega (p,pss) =
|
|
match
|
|
exhaust tdefs pss (simple_match_args p omega @ qs)
|
|
with
|
|
| Rsome r -> Rsome (set_args p r)
|
|
| r -> r in
|
|
if full_match tdefs true constrs
|
|
then try_many try_non_omega constrs
|
|
else
|
|
match exhaust tdefs (filter_extra pss) qs with
|
|
| Rnone -> try_many try_non_omega constrs
|
|
| Rsome r ->
|
|
(* try all constructors anyway, for variant typing ! *)
|
|
ignore (try_many 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 *)
|
|
|
|
(* Using location to spot supbatterns, strange hack ? *)
|
|
|
|
let sub_pat p1 p2 =
|
|
let loc1 = p1.pat_loc and loc2 = p2.pat_loc in
|
|
not (loc1.Location.loc_ghost || loc2.Location.loc_ghost) &&
|
|
loc2.Location.loc_start <= loc1.Location.loc_start &&
|
|
loc1.Location.loc_end <= loc2.Location.loc_end
|
|
|
|
(*
|
|
Compute the ``unused pattern'' in qs=(p1|p2)::ps.
|
|
Ie given a matrix pss compute the patterns that can be suppressed
|
|
from qs, whitout changing values matching the last row of
|
|
matrix pss@[qs]
|
|
|
|
ps1 and ps2 are the unused patterns in p1::ps and p2::ps respectively
|
|
Hence p is unused in (p1|p2)::ps when
|
|
- p is in ps1 and p occurs inside p1, or
|
|
- p is in ps2 and p occurs inside p2, or
|
|
- p is both in ps1 and ps2
|
|
*)
|
|
|
|
let inter_almost ps1 ps2 =
|
|
List.fold_left
|
|
(fun r p ->
|
|
if List.exists (fun q -> q.pat_loc = p.pat_loc) ps2 then
|
|
p::r
|
|
else
|
|
r)
|
|
[] ps1
|
|
|
|
let merge_almost p1 p2 ps1 ps2 =
|
|
let keep1, check1 = List.partition (fun p -> sub_pat p p1) ps1
|
|
and keep2, check2 = List.partition (fun p -> sub_pat p p2) ps2 in
|
|
match keep1@keep2@inter_almost check1 check2 with
|
|
| [] -> Used
|
|
| l -> Upartial l
|
|
|
|
|
|
let rec try_many r f = function
|
|
| [] -> r
|
|
| x::rem ->
|
|
begin match f x, r with
|
|
| Unused,_ -> try_many r f rem
|
|
| Used,_ -> Used
|
|
| _, Used -> Used
|
|
| Upartial lnow, Unused -> try_many (Upartial lnow) f rem
|
|
| Upartial lnow, Upartial lbef ->
|
|
begin match inter_almost lnow lbef with
|
|
| [] -> Used
|
|
| l -> try_many (Upartial l) f rem
|
|
end
|
|
end
|
|
|
|
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"
|
|
|
|
let rec every_satisfiable pss qs = match qs with
|
|
| [] -> begin match pss with [] -> Used | _ -> Unused end
|
|
| {pat_desc = Tpat_or(q1,q2,_); pat_loc = loc}::qs as all ->
|
|
if loc.Location.loc_ghost then begin
|
|
(* #t patterns, do not check unused pats *)
|
|
if satisfiable pss all then Used else Unused
|
|
end else if not (satisfiable pss (omega_list (omega::qs))) then
|
|
Unused
|
|
else
|
|
begin match every_satisfiable pss (q1::qs) with
|
|
| Unused ->
|
|
begin match every_satisfiable pss (q2::qs) with
|
|
| Used -> Upartial [q1]
|
|
| Upartial l2 -> Upartial (q1::l2)
|
|
| Unused -> Unused
|
|
end
|
|
| Used ->
|
|
begin
|
|
match
|
|
every_satisfiable
|
|
(if compat q1 q2 then (q1::qs)::pss else pss) (q2::qs)
|
|
with
|
|
| Used -> Used
|
|
| Upartial l2 -> merge_almost q1 q2 [] l2
|
|
| Unused -> Upartial [q2]
|
|
end
|
|
| Upartial l1 ->
|
|
begin
|
|
match
|
|
every_satisfiable
|
|
(if compat q1 q2 then (q1::qs)::pss else pss) (q2::qs)
|
|
with
|
|
| Used -> merge_almost q1 q2 l1 []
|
|
| Upartial l2 -> merge_almost q1 q2 l1 l2
|
|
| Unused -> Upartial (l1@[q2])
|
|
end
|
|
end
|
|
| {pat_desc = Tpat_alias(q,_)}::qs ->
|
|
every_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 *)
|
|
| [] -> every_satisfiable (filter_extra pss) qs
|
|
| constrs ->
|
|
let try_non_omega (p,pss) =
|
|
every_satisfiable pss (simple_match_args p omega @ qs) in
|
|
if full_match Env.empty false constrs
|
|
then try_many Unused try_non_omega constrs
|
|
else
|
|
match every_satisfiable (filter_extra pss) qs with
|
|
| Used -> Used
|
|
| r -> try_many r try_non_omega constrs
|
|
end
|
|
| {pat_desc=Tpat_variant (l,_,r)}::_ when is_absent l r -> Unused
|
|
| q::qs ->
|
|
let q0 = discr_pat q pss in
|
|
every_satisfiable (filter_one q0 pss) (simple_match_args q0 q @ qs)
|
|
|
|
|
|
let has_guard act =
|
|
match act.exp_desc with
|
|
Texp_when(_, _) -> true
|
|
| _ -> false
|
|
|
|
|
|
(* 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 _,_ -> true | 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
|
|
Exact
|
|
*)
|
|
|
|
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.
|
|
1- Retain minimal patterns (for optimizing when catch all's are here)
|
|
2- Forget about guarded patterns
|
|
*)
|
|
|
|
let rec initial_matrix = function
|
|
[] -> []
|
|
| (pat, act) :: rem ->
|
|
if has_guard act
|
|
then
|
|
initial_matrix rem
|
|
else
|
|
[pat] :: initial_matrix rem
|
|
|
|
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
|
|
|
|
(* Check whether value v can be matched, considering guarded clauses *)
|
|
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 =
|
|
get_mins
|
|
(fun (p,_) (q,_) -> le_pats p q)
|
|
(initial_all true casel) in
|
|
do_match pss [v]
|
|
with
|
|
| NoGuard -> None
|
|
|
|
let check_partial tdefs loc casel =
|
|
let pss = get_mins le_pats (initial_matrix casel) 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::_ ->
|
|
let r = exhaust tdefs pss (omega_list ps) in
|
|
match exhaust tdefs pss (omega_list 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 plain 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"
|
|
|
|
let location_of_clause = function
|
|
pat :: _ -> pat.pat_loc
|
|
| _ -> fatal_error "Parmatch.location_of_clause"
|
|
(*
|
|
let rec or_inside p = match p.pat_desc with
|
|
| Tpat_or (_,_,_) -> true
|
|
| Tpat_any | Tpat_var _ | Tpat_variant (_,None,_)|Tpat_constant _ -> false
|
|
| Tpat_alias (q,_) | Tpat_variant (_,Some q,_) -> or_inside q
|
|
| Tpat_tuple qs | Tpat_construct (_,qs) | Tpat_array qs -> or_insides qs
|
|
| Tpat_record lqs -> or_insides (List.map snd lqs)
|
|
|
|
and or_insides ps = List.exists or_inside ps
|
|
*)
|
|
|
|
let check_unused tdefs casel =
|
|
if Warnings.is_active Warnings.Unused_match then
|
|
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)) ->
|
|
try
|
|
let r = every_satisfiable pss 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 -> ()
|
|
with e ->
|
|
Location.prerr_warning (location_of_clause qs)
|
|
(Warnings.Other "Fatal Error in Parmatch.check_unused") ;
|
|
raise e)
|
|
prefs
|
|
|
|
|
|
|
|
|