From: Stephane Glondu Date: Wed, 10 Jul 2019 12:49:44 +0000 (+0200) Subject: New upstream version 4.06.1 X-Git-Tag: archive/raspbian/4.08.1-4+rpi1~2^2~17^2~5^2~4 X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=92730427b78a4c0e555a34e6e4c7b11b7b5aec0b;p=ocaml.git New upstream version 4.06.1 --- diff --git a/.gitattributes b/.gitattributes index ecff398c..0d7fefb0 100644 --- a/.gitattributes +++ b/.gitattributes @@ -147,6 +147,7 @@ testsuite/tests/docstrings/empty.ml text eol=lf testsuite/tests/functors/functors.ml text eol=lf testsuite/tests/translprim/module_coercion.ml text eol=lf testsuite/tests/warnings/w04.ml text eol=lf +testsuite/tests/warnings/w04_failure.ml text eol=lf testsuite/tests/warnings/w32.ml text eol=lf # These are forced to \n to allow the Cygwin testsuite to pass on a diff --git a/Changes b/Changes index 3f87e219..7128bbe8 100644 --- a/Changes +++ b/Changes @@ -1,3 +1,32 @@ +OCaml 4.06.1 (16 Feb 2018): +--------------------------- + +### Bug fixes + +- MPR#7661, GPR#1459: fix faulty compilation of patterns + using extensible variants constructors + (Luc Maranget, review by Thomas Refis and Gabriel Scherer, report + by Abdelraouf Ouadjaout and Thibault Suzanne) + +- MPR#7702, GPR#1553: refresh raise counts when inlining a function + (Vincent Laviron, Xavier Clerc, report by Cheng Sun) + +- MPR#7704, GPR#1559: Soundness issue with private rows and pattern-matching + (Jacques Garrigue, report by Jeremy Yallop, review by Thomas Refis) + +- MPR#7705, GPR#1558: add missing bounds check in Bigarray.Genarray.nth_dim. + (Nicolás Ojeda Bär, report by Jeremy Yallop, review by Gabriel Scherer) + +- MPR#7713, GPR#1587: Make pattern matching warnings more robust + to ill-typed columns; this is a backport of GPR#1550 from 4.07+dev + (Thomas Refis, review by Gabriel Scherer, report by Andreas Hauptmann) + +- GPR#1470: Don't commute negation with float comparison + (Leo White, review by Xavier Leroy) + +- GPR#1538: Make pattern matching compilation more robust to ill-typed columns + (Gabriel Scherer and Thomas Refis, review by Luc Maranget) + OCaml 4.06.0 (3 Nov 2017): -------------------------- @@ -28,7 +57,7 @@ OCaml 4.06.0 (3 Nov 2017): - GPR#1118: Support inherited field in object type expression type t = < m : int > type u = < n : int; t; k : int > - (Runhang Li, reivew by Jeremy Yallop, Leo White, Jacques Garrigue, + (Runhang Li, review by Jeremy Yallop, Leo White, Jacques Garrigue, and Florian Angeletti) * GPR#1232: Support Unicode character escape sequences in string @@ -92,20 +121,20 @@ OCaml 4.06.0 (3 Nov 2017): - MPR#1771, MPR#7309, GPR#1026: Add update to maps. Allows to update a binding in a map or create a new binding if the key had no binding val update: key -> ('a option -> 'a option) -> 'a t -> 'a t - (Sébastien Briais, review by Daniel Buenzli, Alain Frisch and + (Sébastien Briais, review by Daniel Bünzli, Alain Frisch and Gabriel Scherer) - MPR#7515, GPR#1147: Arg.align now optionally uses the tab character '\t' to separate the "unaligned" and "aligned" parts of the documentation string. If tab is not present, then space is used as a fallback. Allows to have spaces in the unaligned part, which is useful for Tuple options. - (Nicolas Ojeda Bar, review by Alain Frisch and Gabriel Scherer) + (Nicolás Ojeda Bär, review by Alain Frisch and Gabriel Scherer) * GPR#615: Format, add symbolic formatters that output symbolic pretty-printing items. New fields have been added to the formatter_out_functions record, thus this change will break any code building such record from scratch. - When building Format.formatter_out_functions values redefinining the out_spaces field, + When building Format.formatter_out_functions values redefining the out_spaces field, "{ fmt_out_funs with out_spaces = f; }" should be replaced by "{ fmt_out_funs with out_spaces = f; out_indent = f; }" to maintain the old behavior. (Richard Bonichon and Pierre Weis, review by Alain Frisch, original request by @@ -156,7 +185,7 @@ OCaml 4.06.0 (3 Nov 2017): - MPR#7564, GPR#1211: Allow forward slashes in the target of symbolic links created by Unix.symlink under Windows. - (Nicolas Ojeda Bar, review by David Allsopp) + (Nicolás Ojeda Bär, review by David Allsopp) * MPR#7640, GPR#1414: reimplementation of Unix.execvpe to fix issues with the 4.05 implementation. The main issue is that the current @@ -176,7 +205,7 @@ OCaml 4.06.0 (3 Nov 2017): - GPR#1217: Restrict Unix.environment in privileged contexts; add Unix.unsafe_environment. - (Jeremy Yallop, review by Mark Shinwell, Nicolas Ojeda Bar, + (Jeremy Yallop, review by Mark Shinwell, Nicolás Ojeda Bär, Damien Doligez and Hannes Mehnert) - GPR#1321: Reimplement Unix.isatty on Windows. It no longer returns true for @@ -248,8 +277,8 @@ OCaml 4.06.0 (3 Nov 2017): allocator represents a trade-off between worse generated code performance for higher compilation speed (especially interesting in some cases graph coloring is necessarily quadratic). - (Marcell Fischbach and Benedikt Meurer, adapted by Nicolas Ojeda - Bar, review by Nicolas Ojeda Bar and Alain Frisch) + (Marcell Fischbach and Benedikt Meurer, adapted by Nicolás Ojeda Bär, review + by Nicolás Ojeda Bär and Alain Frisch) - MPR#6927, GPR#988: On macOS, when compiling bytecode stubs, plugins, and shared libraries through -output-obj, generate dylibs instead of @@ -435,7 +464,7 @@ OCaml 4.06.0 (3 Nov 2017): * MPR#3771, GPR#153, GPR#1200, GPR#1357, GPR#1362, GPR#1363, GPR#1369, GPR#1398, GPR#1446, GPR#1448: Unicode support for the Windows runtime. - (ygrek, Nicolas Ojeda Bar, review by Alain Frisch, David Allsopp, Damien + (ygrek, Nicolás Ojeda Bär, review by Alain Frisch, David Allsopp, Damien Doligez) * MPR#7594, GPR#1274, GPR#1368: String_val now returns 'const char*', not @@ -464,7 +493,7 @@ OCaml 4.06.0 (3 Nov 2017): - GPR#1086: in Sys.getcwd, just fail instead of calling getwd() if HAS_GETCWD is not set. (Report and first fix by Sebastian Markbåge, final fix by Xavier Leroy, - review by MarK Shinwell) + review by Mark Shinwell) - GPR#1269: Remove 50ms delay at exit for programs using threads (Valentin Gatien-Baron, review by Stephen Dolan) @@ -953,7 +982,7 @@ OCaml 4.05.0 (13 Jul 2017): - GPR#1042: Fix escaping of command-line arguments in Unix.create_process{,_env} under Windows. Arguments with tabs should now be received verbatim by the child process. - (Nicolas Ojeda Bar, Andreas Hauptmann review by Xavier Leroy) + (Nicolás Ojeda Bär, Andreas Hauptmann review by Xavier Leroy) ### Debugging and profiling: @@ -1085,7 +1114,7 @@ OCaml 4.05.0 (13 Jul 2017): - GPR#803: new ocamllex-based tool to extract bytecode compiler opcode information from C headers. - (Nicolas Ojeda Bar) + (Nicolás Ojeda Bär) - GPR#827: install missing mli and cmti files, new make target install-compiler-sources for installation of compiler-libs ml files @@ -1739,7 +1768,7 @@ OCaml 4.04.0 (4 Nov 2016): cf. PR#7313, meaning that you may sometimes need to add type annotations to explicitly instantiate non-generalizable type variables. (Jacques Garrigue, following discussion with Jeremy Yallop, - Nicolas Ojeda Bar and Alain Frisch) + Nicolás Ojeda Bär and Alain Frisch) - PR#7112: Aliased arguments ignored for equality of module types (Jacques Garrigue, report by Leo White) @@ -1761,7 +1790,7 @@ OCaml 4.04.0 (4 Nov 2016): (Pierre Chambart, report by Reed Wilson, review by Mark Shinwell) - PR#7260: GADT + subtyping compile time crash - (Jacques Garrigue, report by Nicolas Ojeda Bar) + (Jacques Garrigue, report by Nicolás Ojeda Bär) - PR#7269: Segfault from conjunctive constraints in GADT (Jacques Garrigue, report by Stephen Dolan) @@ -1816,7 +1845,7 @@ OCaml 4.04.0 (4 Nov 2016): (Bogdan Tătăroiu, review by Thomas Braibant and Alain Frisch) - GPR#700: Fix maximum weak bucket size - (Nicolas Ojeda Bar, review by François Bobot) + (Nicolás Ojeda Bär, review by François Bobot) - GPR#708 Allow more module aliases in strengthening (Leo White) @@ -2141,7 +2170,7 @@ OCaml 4.03.0 (25 Apr 2016): - GPR#545: use reraise to preserve backtrace on `match .. with exception e -> raise e` - (Nicolas Ojeda Bar, review by Gabriel Scherer) + (Nicolás Ojeda Bär, review by Gabriel Scherer) ### Runtime system: diff --git a/VERSION b/VERSION index 1b7a77c8..33d444c9 100644 --- a/VERSION +++ b/VERSION @@ -1,4 +1,4 @@ -4.06.0 +4.06.1 # The version string is the first line of this file. # It must be in the format described in stdlib/sys.mli diff --git a/asmcomp/closure.ml b/asmcomp/closure.ml index e86ecb6b..4fdb3778 100644 --- a/asmcomp/closure.ml +++ b/asmcomp/closure.ml @@ -502,7 +502,8 @@ let simplif_prim fpc p (args, approxs as args_approxs) dbg = (* Substitute variables in a [ulambda] term (a body of an inlined function) and perform some more simplifications on integer primitives. Also perform alpha-conversion on let-bound identifiers to avoid - clashes with locally-generated identifiers. + clashes with locally-generated identifiers, and refresh raise counts + in order to avoid clashes with inlined code from other modules. The variables must not be assigned in the term. This is used to substitute "trivial" arguments for parameters during inline expansion, and also for the translation of let rec @@ -527,18 +528,18 @@ let subst_debuginfo loc dbg = else dbg -let rec substitute loc fpc sb ulam = +let rec substitute loc fpc sb rn ulam = match ulam with Uvar v -> begin try Tbl.find v sb with Not_found -> ulam end | Uconst _ -> ulam | Udirect_apply(lbl, args, dbg) -> let dbg = subst_debuginfo loc dbg in - Udirect_apply(lbl, List.map (substitute loc fpc sb) args, dbg) + Udirect_apply(lbl, List.map (substitute loc fpc sb rn) args, dbg) | Ugeneric_apply(fn, args, dbg) -> let dbg = subst_debuginfo loc dbg in - Ugeneric_apply(substitute loc fpc sb fn, - List.map (substitute loc fpc sb) args, dbg) + Ugeneric_apply(substitute loc fpc sb rn fn, + List.map (substitute loc fpc sb rn) args, dbg) | Uclosure(defs, env) -> (* Question: should we rename function labels as well? Otherwise, there is a risk that function labels are not globally unique. @@ -548,12 +549,12 @@ let rec substitute loc fpc sb ulam = - When we substitute offsets for idents bound by let rec in [close], case [Lletrec], we discard the original let rec body and use only the substituted term. *) - Uclosure(defs, List.map (substitute loc fpc sb) env) - | Uoffset(u, ofs) -> Uoffset(substitute loc fpc sb u, ofs) + Uclosure(defs, List.map (substitute loc fpc sb rn) env) + | Uoffset(u, ofs) -> Uoffset(substitute loc fpc sb rn u, ofs) | Ulet(str, kind, id, u1, u2) -> let id' = Ident.rename id in - Ulet(str, kind, id', substitute loc fpc sb u1, - substitute loc fpc (Tbl.add id (Uvar id') sb) u2) + Ulet(str, kind, id', substitute loc fpc sb rn u1, + substitute loc fpc (Tbl.add id (Uvar id') sb) rn u2) | Uletrec(bindings, body) -> let bindings1 = List.map (fun (id, rhs) -> (id, Ident.rename id, rhs)) bindings in @@ -563,17 +564,17 @@ let rec substitute loc fpc sb ulam = bindings1 sb in Uletrec( List.map - (fun (_id, id', rhs) -> (id', substitute loc fpc sb' rhs)) + (fun (_id, id', rhs) -> (id', substitute loc fpc sb' rn rhs)) bindings1, - substitute loc fpc sb' body) + substitute loc fpc sb' rn body) | Uprim(p, args, dbg) -> - let sargs = List.map (substitute loc fpc sb) args in + let sargs = List.map (substitute loc fpc sb rn) args in let dbg = subst_debuginfo loc dbg in let (res, _) = simplif_prim fpc p (sargs, List.map approx_ulam sargs) dbg in res | Uswitch(arg, sw, dbg) -> - let sarg = substitute loc fpc sb arg in + let sarg = substitute loc fpc sb rn arg in let action = (* Unfortunately, we cannot easily deal with the case of a constructed block (makeblock) bound to a local @@ -589,64 +590,79 @@ let rec substitute loc fpc sb ulam = | _ -> None in begin match action with - | Some u -> substitute loc fpc sb u + | Some u -> substitute loc fpc sb rn u | None -> Uswitch(sarg, { sw with us_actions_consts = - Array.map (substitute loc fpc sb) sw.us_actions_consts; + Array.map (substitute loc fpc sb rn) sw.us_actions_consts; us_actions_blocks = - Array.map (substitute loc fpc sb) sw.us_actions_blocks; + Array.map (substitute loc fpc sb rn) sw.us_actions_blocks; }, dbg) end | Ustringswitch(arg,sw,d) -> Ustringswitch - (substitute loc fpc sb arg, - List.map (fun (s,act) -> s,substitute loc fpc sb act) sw, - Misc.may_map (substitute loc fpc sb) d) + (substitute loc fpc sb rn arg, + List.map (fun (s,act) -> s,substitute loc fpc sb rn act) sw, + Misc.may_map (substitute loc fpc sb rn) d) | Ustaticfail (nfail, args) -> - Ustaticfail (nfail, List.map (substitute loc fpc sb) args) + let nfail = + match rn with + | Some rn -> + begin try + Tbl.find nfail rn + with Not_found -> + fatal_errorf "Closure.split_list: invalid nfail (%d)" nfail + end + | None -> nfail in + Ustaticfail (nfail, List.map (substitute loc fpc sb rn) args) | Ucatch(nfail, ids, u1, u2) -> + let nfail, rn = + match rn with + | Some rn -> + let new_nfail = next_raise_count () in + new_nfail, Some (Tbl.add nfail new_nfail rn) + | None -> nfail, rn in let ids' = List.map Ident.rename ids in let sb' = List.fold_right2 (fun id id' s -> Tbl.add id (Uvar id') s) ids ids' sb in - Ucatch(nfail, ids', substitute loc fpc sb u1, substitute loc fpc sb' u2) + Ucatch(nfail, ids', substitute loc fpc sb rn u1, substitute loc fpc sb' rn u2) | Utrywith(u1, id, u2) -> let id' = Ident.rename id in - Utrywith(substitute loc fpc sb u1, id', - substitute loc fpc (Tbl.add id (Uvar id') sb) u2) + Utrywith(substitute loc fpc sb rn u1, id', + substitute loc fpc (Tbl.add id (Uvar id') sb) rn u2) | Uifthenelse(u1, u2, u3) -> - begin match substitute loc fpc sb u1 with + begin match substitute loc fpc sb rn u1 with Uconst (Uconst_ptr n) -> - if n <> 0 then substitute loc fpc sb u2 else substitute loc fpc sb u3 + if n <> 0 then substitute loc fpc sb rn u2 else substitute loc fpc sb rn u3 | Uprim(Pmakeblock _, _, _) -> - substitute loc fpc sb u2 + substitute loc fpc sb rn u2 | su1 -> - Uifthenelse(su1, substitute loc fpc sb u2, substitute loc fpc sb u3) + Uifthenelse(su1, substitute loc fpc sb rn u2, substitute loc fpc sb rn u3) end | Usequence(u1, u2) -> - Usequence(substitute loc fpc sb u1, substitute loc fpc sb u2) + Usequence(substitute loc fpc sb rn u1, substitute loc fpc sb rn u2) | Uwhile(u1, u2) -> - Uwhile(substitute loc fpc sb u1, substitute loc fpc sb u2) + Uwhile(substitute loc fpc sb rn u1, substitute loc fpc sb rn u2) | Ufor(id, u1, u2, dir, u3) -> let id' = Ident.rename id in - Ufor(id', substitute loc fpc sb u1, substitute loc fpc sb u2, dir, - substitute loc fpc (Tbl.add id (Uvar id') sb) u3) + Ufor(id', substitute loc fpc sb rn u1, substitute loc fpc sb rn u2, dir, + substitute loc fpc (Tbl.add id (Uvar id') sb) rn u3) | Uassign(id, u) -> let id' = try match Tbl.find id sb with Uvar i -> i | _ -> assert false with Not_found -> id in - Uassign(id', substitute loc fpc sb u) + Uassign(id', substitute loc fpc sb rn u) | Usend(k, u1, u2, ul, dbg) -> let dbg = subst_debuginfo loc dbg in - Usend(k, substitute loc fpc sb u1, substitute loc fpc sb u2, - List.map (substitute loc fpc sb) ul, dbg) + Usend(k, substitute loc fpc sb rn u1, substitute loc fpc sb rn u2, + List.map (substitute loc fpc sb rn) ul, dbg) | Uunreachable -> Uunreachable @@ -662,7 +678,7 @@ let no_effects = function let rec bind_params_rec loc fpc subst params args body = match (params, args) with - ([], []) -> substitute loc fpc subst body + ([], []) -> substitute loc fpc subst (Some Tbl.empty) body | (p1 :: pl, a1 :: al) -> if is_simple_argument a1 then bind_params_rec loc fpc (Tbl.add p1 a1 subst) pl al body @@ -947,7 +963,7 @@ let rec close fenv cenv = function Tbl.add id (Uoffset(Uvar clos_ident, pos)) sb) infos Tbl.empty in (Ulet(Immutable, Pgenval, clos_ident, clos, - substitute Location.none !Clflags.float_const_prop sb ubody), + substitute Location.none !Clflags.float_const_prop sb None ubody), approx) end else begin (* General case: recursive definition of values *) diff --git a/asmcomp/cmmgen.ml b/asmcomp/cmmgen.ml index ad1e5853..483123f4 100644 --- a/asmcomp/cmmgen.ml +++ b/asmcomp/cmmgen.ml @@ -292,8 +292,6 @@ let mk_not dbg cmm = tag_int (Cop(Ccmpi (negate_comparison cmp), [c1; c2], dbg'')) dbg' | Cop(Ccmpa cmp, [c1; c2], dbg'') -> tag_int (Cop(Ccmpa (negate_comparison cmp), [c1; c2], dbg'')) dbg' - | Cop(Ccmpf cmp, [c1; c2], dbg'') -> - tag_int (Cop(Ccmpf (negate_comparison cmp), [c1; c2], dbg'')) dbg' | _ -> (* 0 -> 3, 1 -> 1 *) Cop(Csubi, [Cconst_int 3; Cop(Clsl, [c; Cconst_int 1], dbg)], dbg) diff --git a/boot/ocamlc b/boot/ocamlc index 95c6f59d..a73dfdea 100755 Binary files a/boot/ocamlc and b/boot/ocamlc differ diff --git a/boot/ocamldep b/boot/ocamldep index b59eabb3..feec830c 100755 Binary files a/boot/ocamldep and b/boot/ocamldep differ diff --git a/boot/ocamllex b/boot/ocamllex index 084dce87..36fe17f9 100755 Binary files a/boot/ocamllex and b/boot/ocamllex differ diff --git a/bytecomp/matching.ml b/bytecomp/matching.ml index 25a819cc..32e8043d 100644 --- a/bytecomp/matching.ml +++ b/bytecomp/matching.ml @@ -33,6 +33,18 @@ let dbg = false Now, see Lefessant-Maranget ``Optimizing Pattern-Matching'' ICFP'2001 *) +(* + Compatibility predicate that considers potential rebindings of constructors + of an extension type. + + "may_compat p q" returns false when p and q never admit a common instance; + returns true when they may have a common instance. +*) + +module MayCompat = + Parmatch.Compat (struct let equal = Types.may_equal_constr end) +let may_compat = MayCompat.compat +and may_compats = MayCompat.compats (* Many functions on the various data structures of the algorithm : @@ -43,6 +55,7 @@ let dbg = false - Jump summaries: mapping from exit numbers to contexts *) + let string_of_lam lam = Printlambda.lambda Format.str_formatter lam ; Format.flush_str_formatter () @@ -170,23 +183,13 @@ let ctx_matcher p = let p = normalize_pat p in match p.pat_desc with | Tpat_construct (_, cstr,omegas) -> - begin match cstr.cstr_tag with - | Cstr_extension _ -> - let nargs = List.length omegas in - (fun q rem -> match q.pat_desc with - | Tpat_construct (_, _cstr',args) - when List.length args = nargs -> - p,args @ rem - | Tpat_any -> p,omegas @ rem - | _ -> raise NoMatch) - | _ -> - (fun q rem -> match q.pat_desc with - | Tpat_construct (_, cstr',args) - when cstr.cstr_tag=cstr'.cstr_tag -> - p,args @ rem - | Tpat_any -> p,omegas @ rem - | _ -> raise NoMatch) - end + (fun q rem -> match q.pat_desc with + | Tpat_construct (_, cstr',args) +(* NB: may_constr_equal considers (potential) constructor rebinding *) + when Types.may_equal_constr cstr cstr' -> + p,args@rem + | Tpat_any -> p,omegas @ rem + | _ -> raise NoMatch) | Tpat_constant cst -> (fun q rem -> match q.pat_desc with | Tpat_constant cst' when const_compare cst cst' = 0 -> @@ -208,24 +211,29 @@ let ctx_matcher p = | Tpat_array omegas -> let len = List.length omegas in (fun q rem -> match q.pat_desc with - | Tpat_array args when List.length args=len -> - p,args @ rem + | Tpat_array args when List.length args = len -> p,args @ rem | Tpat_any -> p, omegas @ rem | _ -> raise NoMatch) | Tpat_tuple omegas -> + let len = List.length omegas in (fun q rem -> match q.pat_desc with - | Tpat_tuple args -> p,args @ rem - | _ -> p, omegas @ rem) - | Tpat_record (l,_) -> (* Records are normalized *) + | Tpat_tuple args when List.length args = len -> p,args @ rem + | Tpat_any -> p, omegas @ rem + | _ -> raise NoMatch) + | Tpat_record (((_, lbl, _) :: _) as l,_) -> (* Records are normalized *) + let len = Array.length lbl.lbl_all in (fun q rem -> match q.pat_desc with - | Tpat_record (l',_) -> + | Tpat_record (((_, lbl', _) :: _) as l',_) + when Array.length lbl'.lbl_all = len -> let l' = all_record_args l' in p, List.fold_right (fun (_, _,p) r -> p::r) l' rem - | _ -> p,List.fold_right (fun (_, _,p) r -> p::r) l rem) + | Tpat_any -> p,List.fold_right (fun (_, _,p) r -> p::r) l rem + | _ -> raise NoMatch) | Tpat_lazy omega -> (fun q rem -> match q.pat_desc with | Tpat_lazy arg -> p, (arg::rem) - | _ -> p, (omega::rem)) + | Tpat_any -> p, (omega::rem) + | _ -> raise NoMatch) | _ -> fatal_error "Matching.ctx_matcher" @@ -287,10 +295,7 @@ let ctx_lub p ctx = let ctx_match ctx pss = List.exists - (fun {right=qs} -> - List.exists - (fun ps -> compats qs ps) - pss) + (fun {right=qs} -> List.exists (fun ps -> may_compats qs ps) pss) ctx type jumps = (int * ctx list) list @@ -420,7 +425,10 @@ let pretty_def def = def ; prerr_endline "+++++++++++++++++++++" -let pretty_pm pm = pretty_cases pm.cases +let pretty_pm pm = + pretty_cases pm.cases ; + if pm.default <> [] then + pretty_def pm.default let rec pretty_precompiled = function @@ -538,37 +546,11 @@ let up_ok_action act1 act2 = with | Exit -> false -(* Nothing is known about exception/extension patterns, - because of potential rebind *) -let rec exc_inside p = match p.pat_desc with - | Tpat_construct (_,{cstr_tag=Cstr_extension _},_) -> true - | Tpat_any|Tpat_constant _|Tpat_var _ - | Tpat_construct (_,_,[]) - | Tpat_variant (_,None,_) - -> false - | Tpat_construct (_,_,ps) - | Tpat_tuple ps - | Tpat_array ps - -> exc_insides ps - | Tpat_variant (_, Some q,_) - | Tpat_alias (q,_,_) - | Tpat_lazy q - -> exc_inside q - | Tpat_record (lps,_) -> - List.exists (fun (_,_,p) -> exc_inside p) lps - | Tpat_or (p1,p2,_) -> exc_inside p1 || exc_inside p2 - -and exc_insides ps = List.exists exc_inside ps - let up_ok (ps,act_p) l = - if exc_insides ps then match l with [] -> true | _::_ -> false - else - List.for_all - (fun (qs,act_q) -> - up_ok_action act_p act_q || - not (Parmatch.compats ps qs)) - l - + List.for_all + (fun (qs,act_q) -> + up_ok_action act_p act_q || not (may_compats ps qs)) + l (* The simplify function normalizes the first column of the match @@ -663,16 +645,6 @@ let rec what_is_cases cases = match cases with (* A few operations on default environments *) let as_matrix cases = get_mins le_pats (List.map (fun (ps,_) -> ps) cases) -(* For extension matching, record no information in matrix *) -let as_matrix_omega cases = - get_mins le_pats - (List.map - (fun (ps,_) -> - match ps with - | [] -> assert false - | _::ps -> omega::ps) - cases) - let cons_default matrix raise_num default = match matrix with | [] -> default @@ -684,7 +656,7 @@ let default_compat p def = let qss = List.fold_right (fun qs r -> match qs with - | q::rem when Parmatch.compat p q -> rem::r + | q::rem when may_compat p q -> rem::r | _ -> r) pss [] in match qss with @@ -801,7 +773,7 @@ let is_or p = match p.pat_desc with | _ -> false (* Conditions for appending to the Or matrix *) -let conda p q = not (compat p q) +let conda p q = not (may_compat p q) and condb act ps qs = not (is_guarded act) && Parmatch.le_pats qs ps let or_ok p ps l = @@ -830,7 +802,7 @@ let insert_or_append p ps act ors no = let rec attempt seen = function | (q::qs,act_q) as cl::rem -> if is_or q then begin - if compat p q then + if may_compat p q then if IdentSet.is_empty (extract_vars IdentSet.empty p) && IdentSet.is_empty (extract_vars IdentSet.empty q) && @@ -841,7 +813,7 @@ let insert_or_append p ps act ors no = or_ok p ps not_e && (* check append condition for head of O *) List.for_all (* check insert condition for tail of O *) (fun cl -> match cl with - | (q::_,_) -> not (compat p q) + | (q::_,_) -> not (may_compat p q) | _ -> assert false) seen then (* insert *) @@ -948,7 +920,7 @@ and split_naive cls args def k = | [] -> let yes = List.rev yes in { me = Pm {cases=yes; args=args; default=def;} ; - matrix = as_matrix_omega yes ; + matrix = as_matrix yes ; top_default=def}, k | (p::_,_ as cl)::rem -> @@ -962,7 +934,7 @@ and split_naive cls args def k = let idef = next_raise_count () in let def = cons_default matrix idef def in { me = Pm {cases=yes; args=args; default=def} ; - matrix = as_matrix_omega yes ; + matrix = as_matrix yes ; top_default = def; }, (idef,next)::nexts else @@ -972,7 +944,7 @@ and split_naive cls args def k = let idef = next_raise_count () in let def = cons_default matrix idef def in { me = Pm {cases=yes; args=args; default=def} ; - matrix = as_matrix_omega yes ; + matrix = as_matrix yes ; top_default = def; }, (idef,next)::nexts | _ -> assert false @@ -1112,21 +1084,12 @@ and dont_precompile_var args cls def k = matrix=as_matrix cls ; top_default=def},k -and is_exc p = match p.pat_desc with -| Tpat_or (p1,p2,_) -> is_exc p1 || is_exc p2 -| Tpat_alias (p,_,_) -> is_exc p -| Tpat_construct (_,{cstr_tag=Cstr_extension _},_) -> true -| _ -> false - and precompile_or argo cls ors args def k = match ors with | [] -> split_constr cls args def k | _ -> let rec do_cases = function | ({pat_desc=Tpat_or _} as orp::patl, action)::rem -> - let do_opt = not (is_exc orp) in - let others,rem = - if do_opt then get_equiv orp rem - else [],rem in + let others,rem = get_equiv orp rem in let orpm = {cases = (patl, action):: @@ -1136,7 +1099,7 @@ and precompile_or argo cls ors args def k = match ors with | _ -> assert false) others ; args = (match args with _::r -> r | _ -> assert false) ; - default = default_compat (if do_opt then orp else omega) def} in + default = default_compat orp def} in let vars = IdentSet.elements (IdentSet.inter @@ -1149,19 +1112,18 @@ and precompile_or argo cls ors args def k = match ors with Lstaticraise (or_num, List.map (fun v -> Lvar v) vs) in - let do_optrec,body,handlers = do_cases rem in - do_opt && do_optrec, + let body,handlers = do_cases rem in explode_or_pat argo new_patl mk_new_action body vars [] orp, - let mat = if do_opt then [[orp]] else [[omega]] in + let mat = [[orp]] in ((mat, or_num, vars , orpm):: handlers) | cl::rem -> - let b,new_ord,new_to_catch = do_cases rem in - b,cl::new_ord,new_to_catch - | [] -> true,[],[] in + let new_ord,new_to_catch = do_cases rem in + cl::new_ord,new_to_catch + | [] -> [],[] in - let do_opt,end_body, handlers = do_cases ors in - let matrix = (if do_opt then as_matrix else as_matrix_omega) (cls@ors) + let end_body, handlers = do_cases ors in + let matrix = as_matrix (cls@ors) and body = {cases=cls@end_body ; args=args ; default=def} in {me = PmOr {body=body ; handlers=handlers ; or_matrix=matrix} ; matrix=matrix ; @@ -1302,18 +1264,23 @@ let get_args_constr p rem = match p with | {pat_desc=Tpat_construct (_, _, args)} -> args @ rem | _ -> assert false +(* NB: matcher_constr applies to default matrices. + + In that context, matching by constructors of extensible + types degrades to arity checking, due to potential rebinding. + This comparison is performed by Types.may_equal_constr. +*) + let matcher_constr cstr = match cstr.cstr_arity with | 0 -> let rec matcher_rec q rem = match q.pat_desc with | Tpat_or (p1,p2,_) -> begin - try - matcher_rec p1 rem - with - | NoMatch -> matcher_rec p2 rem + try matcher_rec p1 rem + with NoMatch -> matcher_rec p2 rem end - | Tpat_construct (_, cstr1, []) when cstr.cstr_tag = cstr1.cstr_tag -> - rem + | Tpat_construct (_, cstr',[]) + when Types.may_equal_constr cstr cstr' -> rem | Tpat_any -> rem | _ -> raise NoMatch in matcher_rec @@ -1333,16 +1300,16 @@ let matcher_constr cstr = match cstr.cstr_arity with rem | _, _ -> assert false end - | Tpat_construct (_, cstr1, [arg]) - when cstr.cstr_tag = cstr1.cstr_tag -> arg::rem + | Tpat_construct (_, cstr', [arg]) + when Types.may_equal_constr cstr cstr' -> arg::rem | Tpat_any -> omega::rem | _ -> raise NoMatch in matcher_rec | _ -> fun q rem -> match q.pat_desc with | Tpat_or (_,_,_) -> raise OrPat - | Tpat_construct (_, cstr1, args) - when cstr.cstr_tag = cstr1.cstr_tag -> args @ rem + | Tpat_construct (_,cstr',args) + when Types.may_equal_constr cstr cstr' -> args @ rem | Tpat_any -> Parmatch.omegas cstr.cstr_arity @ rem | _ -> raise NoMatch @@ -1465,8 +1432,10 @@ let get_arg_lazy p rem = match p with let matcher_lazy p rem = match p.pat_desc with | Tpat_or (_,_,_) -> raise OrPat -| Tpat_var _ -> get_arg_lazy omega rem -| _ -> get_arg_lazy p rem +| Tpat_any +| Tpat_var _ -> omega :: rem +| Tpat_lazy arg -> arg :: rem +| _ -> raise NoMatch (* Inlining the tag tests before calling the primitive that works on lazy blocks. This is also used in translcore.ml. @@ -1592,8 +1561,10 @@ let get_args_tuple arity p rem = match p with let matcher_tuple arity p rem = match p.pat_desc with | Tpat_or (_,_,_) -> raise OrPat -| Tpat_var _ -> get_args_tuple arity omega rem -| _ -> get_args_tuple arity p rem +| Tpat_any +| Tpat_var _ -> omegas arity @ rem +| Tpat_tuple args when List.length args = arity -> args @ rem +| _ -> raise NoMatch let make_tuple_matching loc arity def = function [] -> fatal_error "Matching.make_tuple_matching" @@ -1629,8 +1600,14 @@ let get_args_record num_fields p rem = match p with let matcher_record num_fields p rem = match p.pat_desc with | Tpat_or (_,_,_) -> raise OrPat -| Tpat_var _ -> get_args_record num_fields omega rem -| _ -> get_args_record num_fields p rem +| Tpat_any +| Tpat_var _ -> + record_matching_line num_fields [] @ rem +| Tpat_record ([], _) when num_fields = 0 -> rem +| Tpat_record ((_, lbl, _) :: _ as lbl_pat_list, _) + when Array.length lbl.lbl_all = num_fields -> + record_matching_line num_fields lbl_pat_list @ rem +| _ -> raise NoMatch let make_record_matching loc all_labels def = function [] -> fatal_error "Matching.make_record_matching" @@ -2553,7 +2530,8 @@ let compile_orhandlers compile_fun lambda1 total1 ctx to_catch = | (mat,i,vars,pm)::rem -> begin try let ctx = select_columns mat ctx in - let handler_i, total_i = compile_fun ctx pm in + let handler_i, total_i = + compile_fun ctx pm in match raw_action r with | Lstaticraise (j,args) -> if i=j then diff --git a/bytecomp/simplif.ml b/bytecomp/simplif.ml index 04176603..f07fbc04 100644 --- a/bytecomp/simplif.ml +++ b/bytecomp/simplif.ml @@ -494,7 +494,7 @@ let simplify_lets lam = | Llet(StrictOpt, kind, v, l1, l2) -> begin match count_var v with 0 -> simplif l2 - | _ -> mklet Alias kind v (simplif l1) (simplif l2) + | _ -> mklet StrictOpt kind v (simplif l1) (simplif l2) end | Llet(str, kind, v, l1, l2) -> mklet str kind v (simplif l1) (simplif l2) | Lletrec(bindings, body) -> diff --git a/otherlibs/bigarray/bigarray_stubs.c b/otherlibs/bigarray/bigarray_stubs.c index aa510268..9f89184c 100644 --- a/otherlibs/bigarray/bigarray_stubs.c +++ b/otherlibs/bigarray/bigarray_stubs.c @@ -471,7 +471,7 @@ CAMLprim value caml_ba_dim(value vb, value vn) { struct caml_ba_array * b = Caml_ba_array_val(vb); intnat n = Long_val(vn); - if (n >= b->num_dims) caml_invalid_argument("Bigarray.dim"); + if (n < 0 || n >= b->num_dims) caml_invalid_argument("Bigarray.dim"); return Val_long(b->dim[n]); } diff --git a/testsuite/tests/basic-float/float_compare.ml b/testsuite/tests/basic-float/float_compare.ml new file mode 100644 index 00000000..d5b7a9a1 --- /dev/null +++ b/testsuite/tests/basic-float/float_compare.ml @@ -0,0 +1,6 @@ + +let compare_nan () = + not (nan < 0.0) +[@@inline never] + +let x = print_endline (string_of_bool (compare_nan ())) diff --git a/testsuite/tests/basic-float/float_compare.reference b/testsuite/tests/basic-float/float_compare.reference new file mode 100644 index 00000000..27ba77dd --- /dev/null +++ b/testsuite/tests/basic-float/float_compare.reference @@ -0,0 +1 @@ +true diff --git a/testsuite/tests/basic-more/robustmatch.compilers.reference b/testsuite/tests/basic-more/robustmatch.compilers.reference new file mode 100644 index 00000000..2ccfe59b --- /dev/null +++ b/testsuite/tests/basic-more/robustmatch.compilers.reference @@ -0,0 +1,107 @@ +File "robustmatch.ml", line 33, characters 6-122: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(AB, MAB, A) +File "robustmatch.ml", line 54, characters 4-73: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, 1) +File "robustmatch.ml", line 64, characters 4-73: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, (B|C)) +File "robustmatch.ml", line 69, characters 4-73: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, (B|C)) +File "robustmatch.ml", line 74, characters 4-73: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, "") +File "robustmatch.ml", line 85, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, (B|C)) +File "robustmatch.ml", line 90, characters 4-87: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, (Y|Z)) +File "robustmatch.ml", line 96, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, (Y|Z)) +File "robustmatch.ml", line 107, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, (B|C)) +File "robustmatch.ml", line 129, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, B) +File "robustmatch.ml", line 151, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, B) +File "robustmatch.ml", line 156, characters 4-87: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, Y) +File "robustmatch.ml", line 162, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, Y) +File "robustmatch.ml", line 167, characters 4-66: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, A) +File "robustmatch.ml", line 176, characters 4-90: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, [| _ |]) +File "robustmatch.ml", line 182, characters 4-69: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, [| _ |]) +File "robustmatch.ml", line 187, characters 4-90: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, [| _ |]) +File "robustmatch.ml", line 200, characters 4-89: +Warning 4: this pattern-matching is fragile. +It will remain exhaustive when constructors are added to type repr. +File "robustmatch.ml", line 210, characters 4-75: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, 'a') +File "robustmatch.ml", line 219, characters 4-74: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, `B) +File "robustmatch.ml", line 228, characters 4-89: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, (3, "*")) +File "robustmatch.ml", line 239, characters 4-113: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, {x=3; y="*"}) +File "robustmatch.ml", line 244, characters 4-113: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, {a=1; b="coucou"; c='b'}) +File "robustmatch.ml", line 253, characters 4-72: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, (3, "*")) +File "robustmatch.ml", line 263, characters 4-82: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, {x=3; y="*"}) +File "robustmatch.ml", line 272, characters 4-71: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R1, R1, lazy 0) +File "robustmatch.ml", line 281, characters 4-99: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +(R2, R2, "") diff --git a/testsuite/tests/basic-more/robustmatch.ml b/testsuite/tests/basic-more/robustmatch.ml new file mode 100644 index 00000000..e4768d0a --- /dev/null +++ b/testsuite/tests/basic-more/robustmatch.ml @@ -0,0 +1,285 @@ +(* TEST + flags += "-w +4+8+9+11+12+52+56+57" + include testing +*) + +module GPR1493 = struct + type t1 = { x : int; y : string; } + type t2 = { a : int; b : string; c : string list; } + + type t = .. + type t += C1 of t1 | C2 of t2 + + let f (x : t) = + match x with + | C1 { x; y } -> () + | C2 { a;b;c } -> () + | _ -> () +end + +module Coherence_illustration = struct + type ab = A | B + + module M : sig + type mab = A | B + + type _ t = AB : ab t | MAB : mab t + end = struct + type mab = ab = A | B + + type _ t = AB : ab t | MAB : mab t + + let f (type x) (t1 : x t) (t2 : x t) (x : x) = + match t1, t2, x with + | AB, AB, A -> () + | MAB, _, A -> () + | _, AB, B -> () + | _, MAB, B -> () + end + + open M + + let f (type x) (t1 : x t) (t2 : x t) (x : x) = + match t1, t2, x with + | AB, AB, A -> () + | MAB, _, A -> () + | _, AB, B -> () + | _, MAB, B -> () +end + +module M1 = struct + type _ repr = R1 : int repr | R2 : string repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, 0 -> () + | _, R2, "coucou" -> () +end + +module M2 = struct + type c = A | B | C + type _ repr = R1 : c repr | R2 : string repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, "coucou" -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | _, R2, "coucou" -> () + | R1, _, A -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | _, R2, "coucou" -> () + | R1, _, _ -> () +end + +module M3 = struct + type c1 = A | B | C + type c2 = X | Y | Z + type _ repr = R1 : c1 repr | R2 : c2 repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + | R1, _, _ -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, _ -> () + | _, R2, X -> () +end + +module M3_gadt = struct + type c1 = A | B | C + type _ c2 = X : int c2 | Y : char c2 | Z : char c2 + type _ repr = R1 : c1 repr | R2 : int c2 repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + | R1, _, _ -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, _ -> () + | _, R2, X -> () +end + +module M3_gadt_bis = struct + type _ c1 = A : int c1 | B : int c1 | C : char c1 + type _ c2 = X : int c2 | Y : char c2 | Z : char c2 + type _ repr = R1 : int c1 repr | R2 : int c2 repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + | R1, _, B -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, _ -> () + | _, R2, X -> () +end + +module M3_gadt_bis_harder = struct + type _ c1 = A : int c1 | B : int c1 | C : char c1 + type _ c2 = X : int c2 | Y : char c2 | Z : char c2 + type _ repr = R1 : 'a c1 repr | R2 : 'a c2 repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, A -> () + | _, R2, X -> () + | R1, _, _ -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, _ -> () + | _, R2, X -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, C -> () + | _, R2, Y -> () +end + +module M4 = struct + type _ repr = R1 : int repr | R2 : int array repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | _, R1, 0 -> () + | R2, _, [||] -> () + | _, R1, 1 -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, _ -> () + | _, R2, [||] -> () + + let h (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | _, R2, [||] -> () + | R1, _, 0 -> () + | R1, _, _ -> () + + let i (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | _, R2, [||] -> () + | R1, _, 0 -> () + | R1, _, _ -> () + | _, R2, _ -> () + + let j (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | _, R2, [||] -> () + | R1, _, 0 -> () + | _, _, _ -> () +end + +module M5 = struct + type _ repr = R1 : char repr | R2 : string repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, 'c' -> () + | _, R2, "coucou" -> () +end + +module M6 = struct + type _ repr = R1 : [ `A | `B ] repr | R2 : string repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, `A -> () + | _, R2, "coucou" -> () +end + +module M7 = struct + type _ repr = R1 : (int * string) repr | R2 : (int * string * char) repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, (3, "") -> () + | _, R2, (1, "coucou", 'a') -> () +end + +module M8 = struct + type r1 = { x : int; y : string } + type r2 = { a : int; b : string; c : char } + type _ repr = R1 : r1 repr | R2 : r2 repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, { x = 3; y = "" } -> () + | _, R2, { a = 1; b = "coucou"; c = 'a' } -> () + + let g (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R2, _, { a = 1; b = "coucou"; c = 'a' } -> () + | _, R1, { x = 3; y = "" } -> () +end + +module M9 = struct + type _ repr = R1 : (int * string) repr | R2 : int repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, (3, "") -> () + | _, R2, 1 -> () +end + +module M10 = struct + type r = { x : int; y : string } + type _ repr = R1 : r repr | R2 : int repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, { x = 3; y = "" } -> () + | _, R2, 1 -> () +end + +module M11 = struct + type _ repr = R1 : int lazy_t repr | R2 : int repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, lazy 1 -> () + | _, R2, 1 -> () +end + +module M12 = struct + type _ repr = R1 : unit repr | R2 : string repr + + let f (type a) (r1 : a repr) (r2 : a repr) (a : a) = + match r1, r2, a with + | R1, _, () -> () + | _, R2, "coucou" -> () + | _, R2, "foo" -> () +end diff --git a/testsuite/tests/basic-more/robustmatch.reference b/testsuite/tests/basic-more/robustmatch.reference new file mode 100644 index 00000000..197c9280 --- /dev/null +++ b/testsuite/tests/basic-more/robustmatch.reference @@ -0,0 +1,2 @@ + +All tests succeeded. diff --git a/testsuite/tests/basic/patmatch.ml b/testsuite/tests/basic/patmatch.ml index 43026be2..c1c00239 100644 --- a/testsuite/tests/basic/patmatch.ml +++ b/testsuite/tests/basic/patmatch.ml @@ -1633,3 +1633,242 @@ end let () = GPR234HList.test () let () = printf "GPR#234=Ok\n%!" + +module MPR7761 = struct + + let zyva msg c r = + if r <> c then begin + Printf.printf "'%c' pas bon pour %s (should be '%c')\n%!"r msg c + end else + Printf.printf "%s -> '%c'\n%!" msg r + + module A = struct + type t = .. + type t += + | A + | B + + let f x y = match x, y with + | (A | B), A -> 'a' + | (A | B), B -> 'b' + | _, _ -> '_' + + let () = + zyva "f A A" 'a' (f A A) ; + zyva "f A B" 'b' (f A B) ; + printf "PR#7661-A=Ok\n%!" + end + + module B = struct + type t = .. + type t += + | A + | B + + type t += C + type t += D + + let f x y = match x, y with + | B, C -> 'x' + | (A | B), A -> 'a' + | (A | B), B -> 'b' + | (C | D), (A|B|C) -> 'c' + | _, _ -> '_' + + let g x y = match x, y with + | Some B, C -> 'x' + | (Some A | Some B), A -> 'a' + | (Some A | Some B), B -> 'b' + | (Some C | Some D), (A|B|C) -> 'c' + | _, _ -> '_' + + let () = + zyva "f B C" 'x' (f B C) ; + zyva "f A A" 'a' (f A A) ; + zyva "f B A" 'a' (f B A) ; + zyva "f A B" 'b' (f A B) ; + zyva "f B B" 'b' (f B B) ; + zyva "f C B" 'c' (f C B) ; + zyva "f D B" 'c' (f D B) ; + zyva "f C A" 'c' (f C A) ; + zyva "f D A" 'c' (f D A) ; + zyva "f C C" 'c' (f C C) ; + zyva "f D C" 'c' (f D C) ; + zyva "f A D" '_' (f A D) ; + zyva "f C D" '_' (f C D) ; +(***************) + zyva "g (Some B) C" 'x' (g (Some B) C) ; + zyva "g (Some A) A" 'a' (g (Some A) A) ; + zyva "g (Some B) A" 'a' (g (Some B) A) ; + zyva "g (Some A) B" 'b' (g (Some A) B) ; + zyva "g (Some B) B" 'b' (g (Some B) B) ; + zyva "g (Some C) B" 'c' (g (Some C) B) ; + zyva "g (Some D) B" 'c' (g (Some D) B) ; + zyva "g (Some C) A" 'c' (g (Some C) A) ; + zyva "g (Some D) A" 'c' (g (Some D) A) ; + zyva "g (Some C) C" 'c' (g (Some C) C) ; + zyva "g (Some D) C" 'c' (g (Some D) C) ; + zyva "g (Some A) D" '_' (g (Some A) D) ; + zyva "g (Some C) D" '_' (g (Some C) D) ; +(***************) + printf "PR#7661-B=Ok\n%!" + end + + module C = struct + type t = .. + type t += + | A + | B + + type t += C + type t += D=A + + let f x y = match x, y with + | B, C -> 'x' + | (A | B), A -> 'a' + | (A | B), B -> 'b' + | (C | D), (A|B|C) -> 'c' + | _, _ -> '_' + + let g x y = match x, y with + | Some B, C -> 'x' + | (Some A | Some B), A -> 'a' + | (Some A | Some B), B -> 'b' + | (Some C | Some D), (A|B|C) -> 'c' + | _, _ -> '_' + + let () = + zyva "f B C" 'x' (f B C) ; + zyva "f A A" 'a' (f A A) ; + zyva "f B A" 'a' (f B A) ; + zyva "f A B" 'b' (f A B) ; + zyva "f B B" 'b' (f B B) ; + zyva "f C B" 'c' (f C B) ; + zyva "f D B" 'b' (f D B) ; + zyva "f C A" 'c' (f C A) ; + zyva "f D A" 'a' (f D A) ; + zyva "f C C" 'c' (f C C) ; + zyva "f D C" 'c' (f D C) ; + zyva "f A D" 'a' (f A D) ; + zyva "f B D" 'a' (f B D) ; + zyva "f C D" 'c' (f C D) ; + zyva "f D D" 'a' (f D D) ; +(***************) + zyva "g (Some B) C" 'x' (g (Some B) C) ; + zyva "g (Some A) A" 'a' (g (Some A) A) ; + zyva "g (Some B) A" 'a' (g (Some B) A) ; + zyva "g (Some A) B" 'b' (g (Some A) B) ; + zyva "g (Some B) B" 'b' (g (Some B) B) ; + zyva "g (Some C) B" 'c' (g (Some C) B) ; + zyva "g (Some D) B" 'b' (g (Some D) B) ; + zyva "g (Some C) A" 'c' (g (Some C) A) ; + zyva "g (Some D) A" 'a' (g (Some D) A) ; + zyva "g (Some C) C" 'c' (g (Some C) C) ; + zyva "g (Some D) C" 'c' (g (Some D) C) ; + zyva "g (Some A) D" 'a' (g (Some A) D) ; + zyva "g (Some B) D" 'a' (g (Some B) D) ; + zyva "g (Some C) D" 'c' (g (Some C) D) ; + zyva "g (Some D) D" 'a' (g (Some D) D) ; +(***************) + printf "PR#7661-C=Ok\n%!" + end + + module D = struct + type t = .. + type t += A | B of int + type t += C=A + + let f x y = match x,y with + | true,A -> 'a' + | _,B _ -> 'b' + | false,A -> 'c' + | _,_ -> '_' + + let g x y = match x,y with + | true,A -> 'a' + | _,C -> 'b' + | false,A -> 'c' + | _,_ -> '_' + + let () = + zyva "f true A" 'a' (f true A) ; + zyva "f true (B 0)" 'b' (f true (B 0)) ; + zyva "f false A" 'c' (f false A) ; + zyva "g true A" 'a' (g true A) ; + zyva "g false A" 'b' (g false A) ; + zyva "g true (B 0)" '_' (g true (B 0)) ; +(***************) + printf "PR#7661-D=Ok\n%!" + end + + module E = struct + + module type S = sig + type t = .. + type t += A|B|C + type u = X|Y|Z + + val fAYX : char + val gAYX : char + val fAZY : char + val gAZY : char + end + + module Z(T:S) : sig end = struct + + open T + + let f x y z = match x,y,z with + | A,X,_ -> '1' + | _,X,X -> '2' + | B,_,X -> '3' + | C,_,X -> '4' + | C,_,Y -> '5' + | _,_,_ -> '_' + + let g x y z = match x,y,z with + | A,X,_ -> '1' + | _,X,X -> '2' + | (B|C),_,X -> '3' + | C,_,Y -> '5' + | _,_,_ -> '_' + + let () = + zyva "f A Y X" fAYX (f A Y X) ; + zyva "g A Y X" gAYX (g A Y X) ; + zyva "f A Z Y" fAZY (f A Z Y) ; + zyva "g A Z Y" gAZY (g A Z Y) ; + () + end + + module A = + Z + (struct + type t = .. + type t += A|B + type t += C=A + type u = X|Y|Z + + let fAYX = '4' + and gAYX = '3' + and fAZY = '5' + and gAZY = '5' + end) + + module B = + Z + (struct + type t = .. + type t += A|B + type t += C + type u = X|Y|Z + + let fAYX = '_' + and gAYX = '_' + and fAZY = '_' + and gAZY = '_' + end) + + let () = printf "PR#7661-E=Ok\n%!" + end +end diff --git a/testsuite/tests/basic/patmatch.reference b/testsuite/tests/basic/patmatch.reference index 11cd189a..79f68157 100644 --- a/testsuite/tests/basic/patmatch.reference +++ b/testsuite/tests/basic/patmatch.reference @@ -74,3 +74,80 @@ PR#6646=Ok PR#6676=Ok 48 GPR#234=Ok +f A A -> 'a' +f A B -> 'b' +PR#7661-A=Ok +f B C -> 'x' +f A A -> 'a' +f B A -> 'a' +f A B -> 'b' +f B B -> 'b' +f C B -> 'c' +f D B -> 'c' +f C A -> 'c' +f D A -> 'c' +f C C -> 'c' +f D C -> 'c' +f A D -> '_' +f C D -> '_' +g (Some B) C -> 'x' +g (Some A) A -> 'a' +g (Some B) A -> 'a' +g (Some A) B -> 'b' +g (Some B) B -> 'b' +g (Some C) B -> 'c' +g (Some D) B -> 'c' +g (Some C) A -> 'c' +g (Some D) A -> 'c' +g (Some C) C -> 'c' +g (Some D) C -> 'c' +g (Some A) D -> '_' +g (Some C) D -> '_' +PR#7661-B=Ok +f B C -> 'x' +f A A -> 'a' +f B A -> 'a' +f A B -> 'b' +f B B -> 'b' +f C B -> 'c' +f D B -> 'b' +f C A -> 'c' +f D A -> 'a' +f C C -> 'c' +f D C -> 'c' +f A D -> 'a' +f B D -> 'a' +f C D -> 'c' +f D D -> 'a' +g (Some B) C -> 'x' +g (Some A) A -> 'a' +g (Some B) A -> 'a' +g (Some A) B -> 'b' +g (Some B) B -> 'b' +g (Some C) B -> 'c' +g (Some D) B -> 'b' +g (Some C) A -> 'c' +g (Some D) A -> 'a' +g (Some C) C -> 'c' +g (Some D) C -> 'c' +g (Some A) D -> 'a' +g (Some B) D -> 'a' +g (Some C) D -> 'c' +g (Some D) D -> 'a' +PR#7661-C=Ok +f true A -> 'a' +f true (B 0) -> 'b' +f false A -> 'c' +g true A -> 'a' +g false A -> 'b' +g true (B 0) -> '_' +PR#7661-D=Ok +f A Y X -> '4' +g A Y X -> '3' +f A Z Y -> '5' +g A Z Y -> '5' +f A Y X -> '_' +g A Y X -> '_' +f A Z Y -> '_' +g A Z Y -> '_' +PR#7661-E=Ok diff --git a/testsuite/tests/raise-counts/a.ml b/testsuite/tests/raise-counts/a.ml new file mode 100644 index 00000000..323fe2af --- /dev/null +++ b/testsuite/tests/raise-counts/a.ml @@ -0,0 +1,12 @@ +let _unused _ = try () with _ -> () + +let trigger_bug x = + let ok = + match x with + | None + | Some "" -> true + | Some _ -> false + in + if x = Some "" && not ok then + failwith "impossible" +[@@inline always] diff --git a/testsuite/tests/raise-counts/b.ml b/testsuite/tests/raise-counts/b.ml new file mode 100644 index 00000000..e346c8b2 --- /dev/null +++ b/testsuite/tests/raise-counts/b.ml @@ -0,0 +1 @@ +let bug x = A.trigger_bug x diff --git a/testsuite/tests/raise-counts/main.ml b/testsuite/tests/raise-counts/main.ml new file mode 100644 index 00000000..b881b832 --- /dev/null +++ b/testsuite/tests/raise-counts/main.ml @@ -0,0 +1,9 @@ +(* TEST + modules = "a.ml b.ml" +*) + +(* PR#7702 *) + +let () = + B.bug (Some ""); + print_endline "OK." diff --git a/testsuite/tests/raise-counts/main.reference b/testsuite/tests/raise-counts/main.reference new file mode 100644 index 00000000..d5c32f4a --- /dev/null +++ b/testsuite/tests/raise-counts/main.reference @@ -0,0 +1 @@ +OK. diff --git a/testsuite/tests/raise-counts/ocamltests b/testsuite/tests/raise-counts/ocamltests new file mode 100644 index 00000000..d389d156 --- /dev/null +++ b/testsuite/tests/raise-counts/ocamltests @@ -0,0 +1 @@ +main.ml diff --git a/testsuite/tests/typing-misc/polyvars.ml b/testsuite/tests/typing-misc/polyvars.ml index 4cdbd804..cb99f4e7 100644 --- a/testsuite/tests/typing-misc/polyvars.ml +++ b/testsuite/tests/typing-misc/polyvars.ml @@ -72,3 +72,15 @@ type 'a foo = 'a constraint 'a = [< `Tag of & int];; [%%expect{| type 'a foo = 'a constraint 'a = [< `Tag of & int ] |}] + +(* PR#7704 *) +type t = private [> `A of string ];; +function (`A x : t) -> x;; +[%%expect{| +type t = private [> `A of string ] +Line _, characters 0-24: +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +` +- : t -> string = +|}] diff --git a/testsuite/tests/typing-poly/poly.ml b/testsuite/tests/typing-poly/poly.ml index 6e21e0f4..bc1990c7 100644 --- a/testsuite/tests/typing-poly/poly.ml +++ b/testsuite/tests/typing-poly/poly.ml @@ -914,7 +914,7 @@ type t = A | B Line _, characters 0-41: Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: -(`AnyExtraTag, `AnyExtraTag) +(`, `) - : [> `A | `B ] * [> `A | `B ] -> int = Line _, characters 0-29: Warning 8: this pattern-matching is not exhaustive. diff --git a/testsuite/tests/warnings/w04_failure.ml b/testsuite/tests/warnings/w04_failure.ml new file mode 100644 index 00000000..929226cd --- /dev/null +++ b/testsuite/tests/warnings/w04_failure.ml @@ -0,0 +1,28 @@ +type ab = A | B +type xy = X | Y + +type _ repr = AB : ab repr | XY : xy repr + +(* Correctly reports fragility w.r.t. [repr], [ab] and [xy]. *) + +let vocal_fragile (type t) (r1 : t repr) (r2 : t repr) (t : t) = + match r1, r2, t with + | AB, _, A -> () + | _, XY, X -> () + | _, _, _ -> () + +(* Fails to report fragility on [ab] and [xy]. *) + +let silent_fragile1 (type t) (r1 : t repr) (r2 : t repr) (t : t) = + match r1, r2, t with + | AB, _, A -> () + | _, XY, X -> () + | _, AB, _ -> () + | XY, _, _ -> () + +let silent_fragile2 (type t) (r1 : t repr) (r2 : t repr) (t : t) = + match r1, r2, t with + | AB, _, A -> () + | _, XY, X -> () + | AB, _, _ -> () + | _, XY, _ -> () diff --git a/testsuite/tests/warnings/w04_failure.reference b/testsuite/tests/warnings/w04_failure.reference new file mode 100644 index 00000000..8af70f40 --- /dev/null +++ b/testsuite/tests/warnings/w04_failure.reference @@ -0,0 +1,9 @@ +File "w04_failure.ml", line 9, characters 2-78: +Warning 4: this pattern-matching is fragile. +It will remain exhaustive when constructors are added to type repr. +File "w04_failure.ml", line 9, characters 2-78: +Warning 4: this pattern-matching is fragile. +It will remain exhaustive when constructors are added to type ab. +File "w04_failure.ml", line 9, characters 2-78: +Warning 4: this pattern-matching is fragile. +It will remain exhaustive when constructors are added to type xy. diff --git a/typing/parmatch.ml b/typing/parmatch.ml index a2e64f65..cb5e07b0 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -44,11 +44,215 @@ let omega_list l = List.map (fun _ -> omega) l let zero = make_pat (Tpat_constant (Const_int 0)) Ctype.none Env.empty +(*******************) +(* Coherence check *) +(*******************) + +(* For some of the operations we do in this module, we would like (because it + simplifies matters) to assume that patterns appearing on a given column in a + pattern matrix are /coherent/ (think "of the same type"). + Unfortunately that is not always true. + + Consider the following (well-typed) example: + {[ + type _ t = S : string t | U : unit t + + let f (type a) (t1 : a t) (t2 : a t) (a : a) = + match t1, t2, a with + | U, _, () -> () + | _, S, "" -> () + ]} + + Clearly the 3rd column contains incoherent patterns. + + On the example above, most of the algorithms will explore the pattern matrix + as illustrated by the following tree: + + {v + S + -------> | "" | + U | S, "" | __/ | () | + --------> | _, () | \ ¬ S + | U, _, () | __/ -------> | () | + | _, S, "" | \ + ---------> | S, "" | ----------> | "" | + ¬ U S + v} + + where following an edge labelled by a pattern P means "assuming the value I + am matching on is filtered by [P] on the column I am currently looking at, + then the following submatrix is still reachable". + + Notice that at any point of that tree, if the first column of a matrix is + incoherent, then the branch leading to it can only be taken if the scrutinee + is ill-typed. + In the example above the only case where we have a matrix with an incoherent + first column is when we consider [t1, t2, a] to be [U, S, ...]. However such + a value would be ill-typed, so we can never actually get there. + + Checking the first column at each step of the recursion and making the + concious decision of "aborting" the algorithm whenever the first column + becomes incoherent, allows us to retain the initial assumption in later + stages of the algorithms. + + --- + + N.B. two patterns can be considered coherent even though they might not be of + the same type. + + That's in part because we only care about the "head" of patterns and leave + checking coherence of subpatterns for the next steps of the algorithm: + ('a', 'b') and (1, ()) will be deemed coherent because they are both a tuples + of arity 2 (we'll notice at a later stage the incoherence of 'a' and 1). + + But also because it can be hard/costly to determine exactly whether two + patterns are of the same type or not (eg. in the example above with _ and S, + but see also the module [Coherence_illustration] in + testsuite/tests/basic-more/robustmatch.ml). + + For the moment our weak, loosely-syntactic, coherence check seems to be + enough and we leave it to each user to consider (and document!) what happens + when an "incoherence" is not detected by this check. +*) + + +let simplify_head_pat p k = + let rec simplify_head_pat p k = + match p.pat_desc with + | Tpat_alias (p,_,_) -> simplify_head_pat p k + | Tpat_var (_,_) -> omega :: k + | Tpat_or (p1,p2,_) -> simplify_head_pat p1 (simplify_head_pat p2 k) + | _ -> p :: k + in simplify_head_pat p k + +let rec simplified_first_col = function + | [] -> [] + | [] :: _ -> assert false (* the rows are non-empty! *) + | (p::_) :: rows -> + simplify_head_pat p (simplified_first_col rows) + +(* Given the simplified first column of a matrix, this function first looks for + a "discriminating" pattern on that column (i.e. a non-omega one) and then + check that every other head pattern in the column is coherent with that one. +*) +let all_coherent column = + let coherent_heads hp1 hp2 = + match hp1.pat_desc, hp2.pat_desc with + | (Tpat_var _ | Tpat_alias _ | Tpat_or _), _ + | _, (Tpat_var _ | Tpat_alias _ | Tpat_or _) -> + assert false + | Tpat_construct (_, c, _), Tpat_construct (_, c', _) -> + c.cstr_consts = c'.cstr_consts + && c.cstr_nonconsts = c'.cstr_nonconsts + | Tpat_constant c1, Tpat_constant c2 -> begin + match c1, c2 with + | Const_char _, Const_char _ + | Const_int _, Const_int _ + | Const_int32 _, Const_int32 _ + | Const_int64 _, Const_int64 _ + | Const_nativeint _, Const_nativeint _ + | Const_float _, Const_float _ + | Const_string _, Const_string _ -> true + | ( Const_char _ + | Const_int _ + | Const_int32 _ + | Const_int64 _ + | Const_nativeint _ + | Const_float _ + | Const_string _), _ -> false + end + | Tpat_tuple l1, Tpat_tuple l2 -> List.length l1 = List.length l2 + | Tpat_record ((_, lbl1, _) :: _, _), Tpat_record ((_, lbl2, _) :: _, _) -> + Array.length lbl1.lbl_all = Array.length lbl2.lbl_all + | Tpat_any, _ + | _, Tpat_any + | Tpat_record ([], _), Tpat_record (_, _) + | Tpat_record (_, _), Tpat_record ([], _) + | Tpat_variant _, Tpat_variant _ + | Tpat_array _, Tpat_array _ + | Tpat_lazy _, Tpat_lazy _ -> true + | _, _ -> false + in + match + List.find (fun head_pat -> + match head_pat.pat_desc with + | Tpat_var _ | Tpat_alias _ | Tpat_or _ -> assert false + | Tpat_any -> false + | _ -> true + ) column + with + | exception Not_found -> + (* only omegas on the column: the column is coherent. *) + true + | discr_pat -> + List.for_all (coherent_heads discr_pat) column + +let first_column simplified_matrix = + List.map fst simplified_matrix + (***********************) (* Compatibility check *) (***********************) -(* p and q compatible means, there exists V that matches both *) +(* Patterns p and q compatible means: + there exists value V that matches both, However.... + + The case of extension types is dubious, as constructor rebind permits + that different constructors are the same (and are thus compatible). + + Compilation must take this into account, consider: + + type t = .. + type t += A|B + type t += C=A + + let f x y = match x,y with + | true,A -> '1' + | _,C -> '2' + | false,A -> '3' + | _,_ -> '_' + + As C is bound to A the value of f false A is '2' (and not '3' as it would + be in the absence of rebinding). + + Not considering rebinding, patterns "false,A" and "_,C" are incompatible + and the compiler can swap the second and third clause, resulting in the + (more efficiently compiled) matching + + match x,y with + | true,A -> '1' + | false,A -> '3' + | _,C -> '2' + | _,_ -> '_' + + This is not correct: when C is bound to A, "f false A" returns '2' (not '3') + + + However, diagnostics do not take constructor rebinding into account. + Notice, that due to module abstraction constructor rebinding is hidden. + + module X : sig type t = .. type t += A|B end = struct + type t = .. + type t += A + type t += B=A + end + + open X + + let f x = match x with + | A -> '1' + | B -> '2' + | _ -> '_' + + The second clause above will NOT (and cannot) be flagged as useless. + + Finally, there are two compatibility fonction + compat p q ---> 'syntactic compatibility, used for diagnostics. + may_compat p q ---> a safe approximation of possible compat, + for compilation + +*) + let is_absent tag row = Btype.row_field tag !row = Rabsent @@ -80,38 +284,67 @@ let records_args l1 l2 = combine [] [] l1 l2 -let rec compat p q = - match p.pat_desc,q.pat_desc with + +module Compat + (Constr:sig + val equal : + Types.constructor_description -> + Types.constructor_description -> + bool + end) = struct + + let rec compat p q = match p.pat_desc,q.pat_desc with +(* Variables match any value *) + | ((Tpat_any|Tpat_var _),_) + | (_,(Tpat_any|Tpat_var _)) -> true +(* Structural induction *) | 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 -> const_compare c1 c2 = 0 + | Tpat_or (p1,p2,_),_ -> + (compat p1 q || compat p2 q) + | _,Tpat_or (q1,q2,_) -> + (compat p q1 || compat p q2) +(* Constructors, with special case for extension *) + | Tpat_construct (_, c1,ps1), Tpat_construct (_, c2,ps2) -> + Constr.equal c1 c2 && compats ps1 ps2 +(* More standard stuff *) + | Tpat_variant(l1,op1, _), Tpat_variant(l2,op2,_) -> + l1=l2 && ocompat op1 op2 + | Tpat_constant c1, Tpat_constant c2 -> + const_compare c1 c2 = 0 | Tpat_tuple ps, Tpat_tuple qs -> compats ps qs | Tpat_lazy p, Tpat_lazy q -> compat p q - | Tpat_construct (_, c1,ps1), Tpat_construct (_, c2,ps2) -> - Types.equal_tag c1.cstr_tag c2.cstr_tag && compats ps1 ps2 - | Tpat_variant(l1,Some p1, _r1), Tpat_variant(l2,Some p2,_) -> - l1=l2 && compat p1 p2 - | Tpat_variant (l1,None, _r1), Tpat_variant(l2,None,_) -> - l1 = l2 - | 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 + | _,_ -> false -and compats ps qs = match ps,qs with -| [], [] -> true -| p::ps, q::qs -> compat p q && compats ps qs -| _,_ -> assert false + and ocompat op oq = match op,oq with + | None,None -> true + | Some p,Some q -> compat p q + | (None,Some _)|(Some _,None) -> false + + and compats ps qs = match ps,qs with + | [], [] -> true + | p::ps, q::qs -> compat p q && compats ps qs + | _,_ -> false + +end + +module SyntacticCompat = + Compat + (struct + let equal c1 c2 = Types.equal_tag c1.cstr_tag c2.cstr_tag + end) + +let compat = SyntacticCompat.compat +and compats = SyntacticCompat.compats + +(* Due to (potential) rebinding, two extension constructors + of the same arity type may equal *) exception Empty (* Empty pattern *) @@ -288,9 +521,9 @@ let simple_match p1 p2 = | Tpat_variant(l1, _, _), Tpat_variant(l2, _, _) -> l1 = l2 | Tpat_constant(c1), Tpat_constant(c2) -> const_compare c1 c2 = 0 - | Tpat_tuple _, Tpat_tuple _ -> true | Tpat_lazy _, Tpat_lazy _ -> true | Tpat_record _ , Tpat_record _ -> true + | Tpat_tuple p1s, Tpat_tuple p2s | Tpat_array p1s, Tpat_array p2s -> List.length p1s = List.length p2s | _, (Tpat_any | Tpat_var(_)) -> true | _, _ -> false @@ -774,7 +1007,7 @@ let complete_constrs p all_tags = let constrs = get_variant_constructors p.pat_env c.cstr_res in let others = List.filter - (fun cnstr -> ConstructorTagHashtbl.mem not_tags cnstr.cstr_tag) + (fun cnstr -> ConstructorTagHashtbl.mem not_tags cnstr.cstr_tag) constrs in let const, nonconst = List.partition (fun cnstr -> cnstr.cstr_arity = 0) others in @@ -805,6 +1038,8 @@ let build_other_constant proj make first next p env = in the first column of env *) +let some_other_tag = "" + let build_other ext env = match env with | ({pat_desc = Tpat_construct (lid, {cstr_tag=Cstr_extension _},_)},_) :: _ -> (* let c = {c with cstr_name = "*extension*"} in *) (* PR#7330 *) @@ -840,7 +1075,7 @@ let build_other ext env = match env with [] row.row_fields with [] -> - make_other_pat "AnyExtraTag" true + make_other_pat some_other_tag true | pat::other_pats -> List.fold_left (fun p_res pat -> @@ -950,6 +1185,20 @@ and has_instances = function | [] -> true | q::rem -> has_instance q && has_instances rem +(* + In two places in the following function, we check the coherence of the first + column of (pss + qs). + If it is incoherent, then we exit early saying that (pss + qs) is not + satisfiable (which is equivalent to saying "oh, we shouldn't have considered + that branch, no good result came come from here"). + + But what happens if we have a coherent but ill-typed column? + - we might end up returning [false], which is equivalent to noticing the + incompatibility: clearly this is fine. + - if we end up returning [true] then we're saying that [qs] is useful while + it is not. This is sad but not the end of the world, we're just allowing dead + code to survive. +*) let rec satisfiable pss qs = match pss with | [] -> has_instances qs | _ -> @@ -960,26 +1209,36 @@ let rec satisfiable pss qs = match pss with | {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 -> - if full_match false constrs then - List.exists - (fun (p,pss) -> - not (is_absent_pat p) && - satisfiable pss (simple_match_args p omega @ qs)) - constrs - else - satisfiable (filter_extra pss) qs + if not (all_coherent (simplified_first_col pss)) then + false + else begin + let q0 = discr_pat omega pss in + match filter_all q0 pss with + (* first column of pss is made of variables only *) + | [] -> satisfiable (filter_extra pss) qs + | constrs -> + if full_match false constrs then + List.exists + (fun (p,pss) -> + not (is_absent_pat p) && + satisfiable pss (simple_match_args p omega @ qs)) + constrs + else + satisfiable (filter_extra pss) qs 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) + if not (all_coherent (q :: simplified_first_col pss)) then + false + else begin + let q0 = discr_pat q pss in + satisfiable (filter_one q0 pss) (simple_match_args q0 q @ qs) + end -(* Also return the remaining cases, to enable GADT handling *) +(* Also return the remaining cases, to enable GADT handling + + For considerations regarding the coherence check, see the comment on + [satisfiable] above. *) let rec satisfiables pss qs = match pss with | [] -> if has_instances qs then [qs] else [] | _ -> @@ -990,36 +1249,43 @@ let rec satisfiables pss qs = match pss with | {pat_desc = Tpat_alias(q,_,_)}::qs -> satisfiables pss (q::qs) | {pat_desc = (Tpat_any | Tpat_var(_))}::qs -> - let q0 = discr_pat omega pss in - let wild p = - List.map (fun qs -> p::qs) (satisfiables (filter_extra pss) qs) in - begin match filter_all q0 pss with - (* first column of pss is made of variables only *) - | [] -> - wild omega - | (p,_)::_ as constrs -> - let for_constrs () = - List.flatten ( - List.map - (fun (p,pss) -> - if is_absent_pat p then [] else - List.map (set_args p) - (satisfiables pss (simple_match_args p omega @ qs))) - constrs ) - in - if full_match false constrs then for_constrs () else - match p.pat_desc with - Tpat_construct _ -> - (* activate this code for checking non-gadt constructors *) - wild (build_other_constrs constrs p) @ for_constrs () - | _ -> - wild omega + if not (all_coherent (simplified_first_col pss)) then + [] + else begin + let q0 = discr_pat omega pss in + let wild p = + List.map (fun qs -> p::qs) (satisfiables (filter_extra pss) qs) in + match filter_all q0 pss with + (* first column of pss is made of variables only *) + | [] -> + wild omega + | (p,_)::_ as constrs -> + let for_constrs () = + List.flatten ( + List.map + (fun (p,pss) -> + if is_absent_pat p then [] else + List.map (set_args p) + (satisfiables pss (simple_match_args p omega @ qs))) + constrs ) + in + if full_match false constrs then for_constrs () else + match p.pat_desc with + Tpat_construct _ -> + (* activate this code for checking non-gadt constructors *) + wild (build_other_constrs constrs p) @ for_constrs () + | _ -> + wild omega end | {pat_desc=Tpat_variant (l,_,r)}::_ when is_absent l r -> [] | q::qs -> - let q0 = discr_pat q pss in - List.map (set_args q0) - (satisfiables (filter_one q0 pss) (simple_match_args q0 q @ qs)) + if not (all_coherent (q :: simplified_first_col pss)) then + [] + else begin + let q0 = discr_pat q pss in + List.map (set_args q0) + (satisfiables (filter_one q0 pss) (simple_match_args q0 q @ qs)) + end (* Now another satisfiable function that additionally @@ -1143,52 +1409,67 @@ let rec exhaust_gadt (ext:Path.t option) 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_gadt ext (filter_extra pss) (n-1) with - | Rsome r -> Rsome (List.map (fun row -> q0::row) r) - | r -> r - end - | constrs -> - let try_non_omega (p,pss) = - if is_absent_pat p then - Rnone - else - match - exhaust_gadt - ext pss (List.length (simple_match_args p omega) + n - 1) - with - | Rsome r -> Rsome (List.map (fun row -> (set_args p row)) r) - | r -> r in - let before = try_many_gadt try_non_omega constrs in - if - full_match false constrs && not (should_extend ext constrs) - then - before - else - (* - D = filter_extra pss is the default matrix - as it is included in pss, one can avoid - recursive calls on specialized matrices, - Essentially : - * D exhaustive => pss exhaustive - * D non-exhaustive => we have a non-filtered value - *) - let r = exhaust_gadt ext (filter_extra pss) (n-1) in - match r with - | Rnone -> before - | Rsome r -> - try - let p = build_other ext constrs in - let dug = List.map (fun tail -> p :: tail) r in - match before with - | Rnone -> Rsome dug - | Rsome x -> Rsome (x @ dug) + if not (all_coherent (simplified_first_col pss)) then + (* We're considering an ill-typed branch, we won't actually be able to + produce a well typed value taking that branch. *) + Rnone + else begin + (* Assuming the first column is ill-typed but considered coherent, we + might end up producing an ill-typed witness of non-exhaustivity + corresponding to the current branch. + + If [exhaust] has been called by [do_check_partial], then the witnesses + produced get typechecked and the ill-typed ones are discarded. + + If [exhaust] has been called by [do_check_fragile], then it is possible + we might fail to warn the user that the matching is fragile. See for + example testsuite/tests/warnings/w04_failure.ml. *) + let q0 = discr_pat omega pss in + match filter_all q0 pss with + (* first column of pss is made of variables only *) + | [] -> + begin match exhaust_gadt ext (filter_extra pss) (n-1) with + | Rsome r -> Rsome (List.map (fun row -> q0::row) r) + | r -> r + end + | constrs -> + let try_non_omega (p,pss) = + if is_absent_pat p then + Rnone + else + match + exhaust_gadt + ext pss (List.length (simple_match_args p omega) + n - 1) with - (* cannot occur, since constructors don't make a full signature *) - | Empty -> fatal_error "Parmatch.exhaust" + | Rsome r -> Rsome (List.map (fun row -> (set_args p row)) r) + | r -> r in + let before = try_many_gadt try_non_omega constrs in + if + full_match false constrs && not (should_extend ext constrs) + then + before + else + (* + D = filter_extra pss is the default matrix + as it is included in pss, one can avoid + recursive calls on specialized matrices, + Essentially : + * D exhaustive => pss exhaustive + * D non-exhaustive => we have a non-filtered value + *) + let r = exhaust_gadt ext (filter_extra pss) (n-1) in + match r with + | Rnone -> before + | Rsome r -> + try + let p = build_other ext constrs in + let dug = List.map (fun tail -> p :: tail) r in + match before with + | Rnone -> Rsome dug + | Rsome x -> Rsome (x @ dug) + with + (* cannot occur, since constructors don't make a full signature *) + | Empty -> fatal_error "Parmatch.exhaust" end let exhaust_gadt ext pss n = @@ -1223,35 +1504,38 @@ let rec pressure_variants tdefs = function | [] -> false | []::_ -> true | pss -> - let q0 = discr_pat omega pss in - begin match filter_all q0 pss with - [] -> pressure_variants tdefs (filter_extra pss) - | constrs -> - let rec try_non_omega = function - (_p,pss) :: rem -> - let ok = pressure_variants tdefs pss in - try_non_omega rem && ok - | [] -> true - in - if full_match (tdefs=None) constrs then - try_non_omega constrs - else if tdefs = None then - pressure_variants None (filter_extra pss) - else - let full = full_match true constrs in - let ok = - if full then try_non_omega constrs - else try_non_omega (filter_all q0 (mark_partial pss)) + if not (all_coherent (simplified_first_col pss)) then + true + else begin + let q0 = discr_pat omega pss in + match filter_all q0 pss with + [] -> pressure_variants tdefs (filter_extra pss) + | constrs -> + let rec try_non_omega = function + (_p,pss) :: rem -> + let ok = pressure_variants tdefs pss in + try_non_omega rem && ok + | [] -> true in - begin match constrs, tdefs with - ({pat_desc=Tpat_variant _} as p,_):: _, Some env -> - let row = row_of_pat p in - if Btype.row_fixed row - || pressure_variants None (filter_extra pss) then () - else close_variant env row - | _ -> () - end; - ok + if full_match (tdefs=None) constrs then + try_non_omega constrs + else if tdefs = None then + pressure_variants None (filter_extra pss) + else + let full = full_match true constrs in + let ok = + if full then try_non_omega constrs + else try_non_omega (filter_all q0 (mark_partial pss)) + in + begin match constrs, tdefs with + ({pat_desc=Tpat_variant _} as p,_):: _, Some env -> + let row = row_of_pat p in + if Btype.row_fixed row + || pressure_variants None (filter_extra pss) then () + else close_variant env row + | _ -> () + end; + ok end @@ -1370,7 +1654,7 @@ let filter_one q rs = (* Back to normal matrices *) -let make_vector r = r.no_ors +let make_vector r = List.rev r.no_ors let make_matrix rs = List.map make_vector rs @@ -1413,6 +1697,12 @@ let extract_columns pss qs = match pss with The idea is to first look for or patterns (recursive case), then check or-patterns argument usefulness (terminal case) *) +let rec simplified_first_usefulness_col = function + | [] -> [] + | row :: rows -> + match row.active with + | [] -> assert false (* the rows are non-empty! *) + | p :: _ -> simplify_head_pat p (simplified_first_usefulness_col rows) let rec every_satisfiables pss qs = match qs.active with | [] -> @@ -1461,10 +1751,16 @@ let rec every_satisfiables pss qs = match qs.active with 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} + (* The handling of incoherent matrices is kept in line with + [satisfiable] *) + if not (all_coherent (uq :: simplified_first_usefulness_col pss)) then + Unused + else begin + let q0 = discr_pat q pss in + every_satisfiables + (filter_one q0 pss) + {qs with active=simple_match_args q0 q @ rem} + end end (* @@ -1690,6 +1986,8 @@ let rec do_match pss qs = match qs with do_match (do_filter_var pss) qs | _ -> let q0 = normalize_pat q in + (* [pss] will (or won't) match [q0 :: qs] regardless of the coherence of + its first column. *) do_match (do_filter_one q0 pss) (simple_match_args q0 q @ qs) @@ -2245,13 +2543,25 @@ let rec do_stable rs = match rs with collect_stable rs | _ -> let rs = push_vars rs in - match filter_all rs with - | [] -> - do_stable (List.map snd rs) - | (_,rs)::env -> - List.fold_left - (fun xs (_,rs) -> IdSet.inter xs (do_stable rs)) - (do_stable rs) env + if not (all_coherent (first_column rs)) then begin + (* If the first column is incoherent, then all the variables of this + matrix are stable. *) + List.fold_left (fun acc (_, { seen; _ }) -> + List.fold_left IdSet.union acc seen + ) IdSet.empty rs + end else begin + (* If the column is ill-typed but deemed coherent, we might spuriously + warn about some variables being unstable. + As sad as that might be, the warning can be silenced by splitting the + or-pattern... *) + match filter_all rs with + | [] -> + do_stable (List.map snd rs) + | (_,rs)::env -> + List.fold_left + (fun xs (_,rs) -> IdSet.inter xs (do_stable rs)) + (do_stable rs) env + end let stable p = do_stable [{unseen=[p]; seen=[];}] diff --git a/typing/parmatch.mli b/typing/parmatch.mli index 0fb4f757..feecb0c5 100644 --- a/typing/parmatch.mli +++ b/typing/parmatch.mli @@ -35,8 +35,20 @@ val const_compare : constant -> constant -> int val le_pat : pattern -> pattern -> bool val le_pats : pattern list -> pattern list -> bool -val compat : pattern -> pattern -> bool -val compats : pattern list -> pattern list -> bool + +(* Exported compatibility functor, abstracted over constructor equality *) +module Compat : + functor + (Constr: sig + val equal : + Types.constructor_description -> + Types.constructor_description -> + bool + end) -> sig + val compat : pattern -> pattern -> bool + val compats : pattern list -> pattern list -> bool + end + exception Empty val lub : pattern -> pattern -> pattern val lubs : pattern list -> pattern list -> pattern list @@ -83,3 +95,6 @@ val inactive : partial:partial -> pattern -> bool (* Ambiguous bindings *) val check_ambiguous_bindings : case list -> unit + +(* The tag used for open polymorphic variant types *) +val some_other_tag : label diff --git a/typing/typecore.ml b/typing/typecore.ml index b4cfb8b0..bf86107c 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -1213,7 +1213,10 @@ and type_pat_aux ~constrs ~labels ~no_existentials ~mode ~explode ~env row_more = newvar (); row_fixed = false; row_name = None } in - unify_pat_types loc !env (newty (Tvariant row)) expected_ty; + (* PR#7404: allow some_other_tag blindly, as it would not unify with + the abstract row variable *) + if l = Parmatch.some_other_tag then assert (constrs <> None) + else unify_pat_types loc !env (newty (Tvariant row)) expected_ty; let k arg = rp k { pat_desc = Tpat_variant(l, arg, ref {row with row_more = newvar()}); diff --git a/typing/types.ml b/typing/types.ml index 51d58a9a..7ef6eaff 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -331,6 +331,10 @@ let equal_tag t1 t2 = Path.same path1 path2 && b1 = b2 | (Cstr_constant _|Cstr_block _|Cstr_unboxed|Cstr_extension _), _ -> false +let may_equal_constr c1 c2 = match c1.cstr_tag,c2.cstr_tag with +| Cstr_extension _,Cstr_extension _ -> c1.cstr_arity = c2.cstr_arity +| tag1,tag2 -> equal_tag tag1 tag2 + type label_description = { lbl_name: string; (* Short name *) lbl_res: type_expr; (* Type of the result *) diff --git a/typing/types.mli b/typing/types.mli index 633aa31d..28317b52 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -473,8 +473,13 @@ and constructor_tag = | Cstr_extension of Path.t * bool (* Extension constructor true if a constant false if a block*) +(* Constructors are the same *) val equal_tag : constructor_tag -> constructor_tag -> bool +(* Constructors may be the same, given potential rebinding *) +val may_equal_constr : + constructor_description -> constructor_description -> bool + type label_description = { lbl_name: string; (* Short name *) lbl_res: type_expr; (* Type of the result *)