(***********************************************************************) (* *) (* 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