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
+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):
--------------------------
- 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
- 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
- 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
- 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
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
* 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
- 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)
- 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:
- 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
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)
(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)
(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)
- 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:
-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
(* 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
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.
- 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
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
| _ -> 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
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
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 *)
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)
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 :
- Jump summaries: mapping from exit numbers to contexts
*)
+
let string_of_lam lam =
Printlambda.lambda Format.str_formatter lam ;
Format.flush_str_formatter ()
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 ->
| 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"
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
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
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
(* 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
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
| _ -> 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 =
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) &&
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 *)
| [] ->
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 ->
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
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
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)::
| _ -> 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
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 ;
| {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
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
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.
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"
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"
| (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
| 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) ->
{
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]);
}
--- /dev/null
+
+let compare_nan () =
+ not (nan < 0.0)
+[@@inline never]
+
+let x = print_endline (string_of_bool (compare_nan ()))
--- /dev/null
+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, "")
--- /dev/null
+(* 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
--- /dev/null
+
+All tests succeeded.
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
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
--- /dev/null
+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]
--- /dev/null
+let bug x = A.trigger_bug x
--- /dev/null
+(* TEST
+ modules = "a.ml b.ml"
+*)
+
+(* PR#7702 *)
+
+let () =
+ B.bug (Some "");
+ print_endline "OK."
[%%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:
+`<some other tag>
+- : t -> string = <fun>
+|}]
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)
+(`<some other tag>, `<some other tag>)
- : [> `A | `B ] * [> `A | `B ] -> int = <fun>
Line _, characters 0-29:
Warning 8: this pattern-matching is not exhaustive.
--- /dev/null
+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, _ -> ()
--- /dev/null
+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.
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
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 *)
| 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
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
in the first column of env
*)
+let some_other_tag = "<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 *)
[] 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 ->
| [] -> 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
| _ ->
| {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 []
| _ ->
| {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
| [] -> 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 =
| [] -> 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
(* 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
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
| [] ->
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
(*
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)
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=[];}]
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
(* Ambiguous bindings *)
val check_ambiguous_bindings : case list -> unit
+
+(* The tag used for open polymorphic variant types *)
+val some_other_tag : label
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()});
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 *)
| 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 *)
projects / ocaml.git / commitdiff