Skip to content

Commit

Permalink
handle negative rows in ambiguous variable check
Browse files Browse the repository at this point in the history
  • Loading branch information
@gasche
gasche committed Jan 3, 2018
1 parent c375625 commit 801a2d5
Show file tree
Hide file tree
Showing 3 changed files with 162 additions and 79 deletions.
47 changes: 47 additions & 0 deletions testsuite/tests/typing-warnings/ambiguous_guarded_disjunction.ml
View file
Expand Up @@ -218,3 +218,50 @@ let not_ambiguous__as_disjoint_on_second_column_split = function
| ((Some a, (1 as b)) | (Some b, (2 as a))) when a = 0 -> ignore a; ignore b
| _ -> ()
;;

let () = print_endline "no warning below";;
(* we check for the ambiguous case first, so there
is no warning *)
let solved_ambiguity_typical_example = function
| (Val x, Val y) ->
if x < 0 || y < 0
then ()
else ()
| ((Val x, _) | (_, Val x)) when x < 0 -> ()
| (_, Rest) -> ()
| (_, Val x) ->
(* the reader can expect *)
assert (x >= 0);
(* to hold here. *)
()
;;

let () = print_endline "yet a warning below";;
(* if the check for the ambiguous case is guarded,
there is still a warning *)
let guarded_ambiguity = function
| (Val x, Val y) when x < 0 || y < 0 -> ()
| ((Val y, _) | (_, Val y)) when y < 0 -> ()
| (_, Rest) -> ()
| (_, Val x) ->
(* the reader can expect *)
assert (x >= 0);
(* to hold here. *)
()
;;

(* see GPR#1552 *)
type a = A1 | A2;;

type 'a alg =
| Val of 'a
| Binop of 'a alg * 'a alg;;

let () = print_endline "warning below";;
let cmp (pred : a -> bool) (x : a alg) (y : a alg) =
match x, y with
| Val A1, Val A1 -> ()
| ((Val x, _) | (_, Val x)) when pred x -> ()
(* below: silence exhaustiveness/fragility warnings *)
| (Val (A1 | A2) | Binop _), _ -> ()
;;
18 changes: 18 additions & 0 deletions testsuite/tests/typing-warnings/ambiguous_guarded_disjunction.ml.reference
View file
Expand Up @@ -139,4 +139,22 @@ val ambiguous_xy_but_not_ambiguous_z : (int -> int -> bool) -> t2 -> int =
<fun>
# * * * * * * * * val not_ambiguous__as_disjoint_on_second_column_split :
int option * int -> unit = <fun>
# no warning below
# * val solved_ambiguity_typical_example : expr * expr -> unit = <fun>
# yet a warning below
# * Characters 164-189:
| ((Val y, _) | (_, Val y)) when y < 0 -> ()
^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 57: Ambiguous or-pattern variables under guard;
variable y may match different arguments. (See manual section 9.5)
val guarded_ambiguity : expr * expr -> unit = <fun>
# type a = A1 | A2
# type 'a alg = Val of 'a | Binop of 'a alg * 'a alg
# warning below
# Characters 100-125:
| ((Val x, _) | (_, Val x)) when pred x -> ()
^^^^^^^^^^^^^^^^^^^^^^^^^
Warning 57: Ambiguous or-pattern variables under guard;
variable x may match different arguments. (See manual section 9.5)
val cmp : (a -> bool) -> a alg -> a alg -> unit = <fun>
#
176 changes: 97 additions & 79 deletions typing/parmatch.ml
View file
Expand Up @@ -2263,23 +2263,9 @@ let pattern_vars p = IdSet.of_list (Typedtree.pat_bound_idents p)
All rows of a (sub)matrix have rows of the same length,
but also varsets of the same length.
*)

type amb_row = { row : pattern list ; varsets : IdSet.t list; }

(* Given a matrix of non-empty rows
p1 :: r1...
p2 :: r2...
p3 :: r3...
Simplify the first column [p1 p2 p3] by splitting all or-patterns and
collecting the head-bound variables (the varset). The result is a list of
couples
(simple head pattern, rest of row)
where a "simple head pattern" starts with either the catch-all pattern omega
(_) or a head constructor, and the "rest of the row" has the head-bound
variables pushed as a new varset.
Varsets are populated when simplifying the first column
-- the variables of the head pattern are collected in a new varset.
For example,
{ row = x :: r1; varsets = s1 }
{ row = (Some _) as y :: r2; varsets = s2 }
Expand All @@ -2288,31 +2274,61 @@ type amb_row = { row : pattern list ; varsets : IdSet.t list; }
becomes
(_, { row = r1; varsets = {x} :: s1 })
(Some _, { row = r2; varsets = {y} :: s2 })
(None, { row = r3; varsets = s3 ++ {x, y} })
(None, { row = r3; varsets = {x, y} :: s3 })
(Some x, { row = r4; varsets = {} :: s4 })
(None, { row = r4; varsets = {x} :: s4 })
*)
*)
type amb_row = { row : pattern list ; varsets : IdSet.t list; }

(*
To accurately report ambiguous variables, one must consider
that previous clauses have already matched some values.
Consider for example:
| (Foo x, Foo y) -> ...
| ((Foo x, _) | (_, Foo x)) when bar x -> ...
The second line taken in isolation uses an unstable variable,
but the discriminating values, of the shape [(Foo v1, Foo v2)],
would all be filtered by the line above.
To track this information, the matrices we analyze contain both *positive* rows,
that describe the rows currently being analyzed (of type amb_row, so that their
varsets are tracked) and *negative rows*, that describe the cases already
matched against. A variable is stable if, for any value not matched
by any of the negative rows, the environment captured by any of the
matching positive rows is identical.
*)
type ('a, 'b) signed = Positive of 'a | Negative of 'b

let rec simplify_first_amb_col = function
| [] -> []
| { row = [] } :: _ -> assert false
| { row = p::ps; varsets; }::rem ->
simplify_head_amb_pat IdSet.empty p ps varsets
| (Negative [] | Positive { row = []; _ }) :: _ -> assert false
| Negative (n :: ns) :: rem ->
simplify_head_amb_pat_neg n ns
(simplify_first_amb_col rem)
| Positive { row = p::ps; varsets; }::rem ->
simplify_head_amb_pat_pos IdSet.empty p ps varsets
(simplify_first_amb_col rem)

and simplify_head_amb_pat head_bound_variables p ps varsets k =
and simplify_head_amb_pat_neg p ps k =
Misc.map_end (fun (n, ns) -> (n, Negative ns))
(simplify_head_pat p ps []) k

and simplify_head_amb_pat_pos head_bound_variables p ps varsets k =
match p.pat_desc with
| Tpat_alias (p,x,_) ->
simplify_head_amb_pat (IdSet.add x head_bound_variables) p ps varsets k
simplify_head_amb_pat_pos (IdSet.add x head_bound_variables) p ps varsets k
| Tpat_var (x,_) ->
let rest_of_the_row =
{ row = ps; varsets = IdSet.add x head_bound_variables :: varsets; }
in
(omega, rest_of_the_row) :: k
(omega, Positive rest_of_the_row) :: k
| Tpat_or (p1,p2,_) ->
simplify_head_amb_pat head_bound_variables p1 ps varsets
(simplify_head_amb_pat head_bound_variables p2 ps varsets k)
simplify_head_amb_pat_pos head_bound_variables p1 ps varsets
(simplify_head_amb_pat_pos head_bound_variables p2 ps varsets k)
| _ ->
(p, { row = ps; varsets = head_bound_variables :: varsets; }) :: k
(p, Positive { row = ps; varsets = head_bound_variables :: varsets; }) :: k

(* Compute stable bindings *)

Expand All @@ -2328,53 +2344,54 @@ let reduce f = function
| [] -> invalid_arg "reduce"
| x::xs -> List.fold_left f x xs

let rec matrix_stable_vars rs = match rs with
| [] -> All
| { row = []; _ } :: _ ->
(* All rows have the same number of columns;
if the first row is empty, they all are. *)
List.iter (fun {row; _} -> assert (row = [])) rs;

(* A variable is stable in a given varset if, in each row, it
appears in this varset -- rather than in another position in
the list of binding sets. We can thus compute the stable
variables of each varset by pairwise intersection. *)
let rows_varsets = List.map (fun { varsets; _ } -> varsets) rs in
let stables_in_varsets = reduce (List.map2 IdSet.inter) rows_varsets in

(* The stable variables are those stable at any position *)
Vars (List.fold_left IdSet.union IdSet.empty stables_in_varsets)
| rs ->
let rs = simplify_first_amb_col rs in
if not (all_coherent (first_column rs))
then All
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...
*)
let extend_row columns r =
{ r with row = columns @ r.row } in
let q0 = discr_pat omega rs in
match build_specialized_submatrices ~extend_row q0 rs with
| { default; constrs = [] } ->
(* the first column contains no head constructor;
they are all _ after simplification, so it can be dropped *)
matrix_stable_vars default
| { default = _; constrs } ->
(* A stable variable must be stable in each submatrix.
If the first column contains some head constructors, there
is no need to look at stability for the default matrix: all
other submatrices contain the default matrix, so they have
less stable variables. *)
let submatrices = List.map snd constrs in
let submat_stable = List.map matrix_stable_vars submatrices in
List.fold_left stable_inter All submat_stable
end
let rec matrix_stable_vars m = match m with
| [] -> All
| ((Positive {row = []; _} | Negative []) :: _) as empty_rows ->
let exception Has_negative in
(* if at least one row is negative, the matrix matches no value *)
let get_varsets = function
| Negative n ->
(* All rows have the same number of columns;
if the first row is empty, they all are. *)
assert (n = []);
raise Has_negative
| Positive p ->
assert (p.row = []);
p.varsets in
begin match List.map get_varsets empty_rows with
| exception Has_negative -> All
| rows_varsets ->
let stables_in_varsets =
reduce (List.map2 IdSet.inter) rows_varsets in
(* The stable variables are those stable at any position *)
Vars (List.fold_left IdSet.union IdSet.empty stables_in_varsets)
end
| m ->
let m = simplify_first_amb_col m in
if not (all_coherent (first_column m))
then All
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...
*)
let submatrices =
let extend_row columns = function
| Negative r -> Negative (columns @ r)
| Positive r -> Positive { r with row = columns @ r.row } in
let q0 = discr_pat omega m in
let { default; constrs } =
build_specialized_submatrices ~extend_row q0 m in
default :: List.map snd constrs in
(* A stable variable must be stable in each submatrix. *)
let submat_stable = List.map matrix_stable_vars submatrices in
List.fold_left stable_inter All submat_stable
end

let pattern_stable_vars p = matrix_stable_vars [{varsets = []; row = [p]}]
let pattern_stable_vars ns p =
matrix_stable_vars
(Positive {varsets = []; row = [p]} :: (List.map (fun n -> Negative n) ns))

(* All identifier paths that appear in an expression that occurs
as a clause right hand side or guard.
Expand Down Expand Up @@ -2433,14 +2450,13 @@ let check_ambiguous_bindings =
let warn0 = Ambiguous_pattern [] in
fun cases ->
if is_active warn0 then
List.iter
(fun case -> match case with
| { c_guard=None ; _} -> ()
let check_case ns case = match case with
| { c_lhs = p; c_guard=None ; _} -> [p]::ns
| { c_lhs=p; c_guard=Some g; _} ->
let all =
IdSet.inter (pattern_vars p) (all_rhs_idents g) in
if not (IdSet.is_empty all) then begin
match pattern_stable_vars p with
match pattern_stable_vars ns p with
| All -> ()
| Vars stable ->
let ambiguous = IdSet.diff all stable in
Expand All @@ -2449,5 +2465,7 @@ let check_ambiguous_bindings =
let warn = Ambiguous_pattern pps in
Location.prerr_warning p.pat_loc warn
end
end)
cases
end;
ns
in
ignore (List.fold_left check_case [] cases)

0 comments on commit 801a2d5

Please sign in to comment.