--- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@@@@@@@@@ -39,16 +39,132 @@@@@@@@@@ let rec omegas i = if i <= 0 then [] else omega :: omegas (i-1) 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 first_column_is_coherent matrix = +| match +| List.find (fun (col1, _) -> +| match col1.pat_desc with +| | Tpat_var _ | Tpat_alias _ | Tpat_or _ -> assert false +| | Tpat_any -> false +| | _ -> true +| ) matrix +| with +| | exception Not_found -> +| (* only omegas on the first column: the column is coherent. *) +| true +| | (discr_pat, _) -> +| let same_kind (col1, _) = +| match discr_pat.pat_desc, col1.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 +| | _, _ -> 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_variant _, Tpat_variant _ +| | Tpat_array _, Tpat_array _ +| | Tpat_lazy _, Tpat_lazy _ -> true +| | _, _ -> false +| in +| List.for_all same_kind matrix +| (***********************) (* Compatibility check *) (***********************) (* 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 @@@@@@@@@@ -991,76 +1107,104 @@@@@@@@@@ (* Core function : Is the last row of pattern matrix pss + qs satisfiable ? That is : Does there exists at least one value vector, es such that : 1- for all ps in pss ps # es (ps and es are not compatible) 2- qs <= es (es matches qs) +| +| --- +| +| In two places in the following function, we check the coherence of the first +| column. +| 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 | _ -> match qs with | [] -> false | {pat_desc = Tpat_or(q1,q2,_)}::qs -> satisfiable pss (q1::qs) || satisfiable pss (q2::qs) | {pat_desc = Tpat_alias(q,_,_)}::qs -> satisfiable pss (q::qs) | {pat_desc = (Tpat_any | Tpat_var(_))}::qs -> let pss = simplify_first_col pss in +| if not (first_column_is_coherent pss) then ( +| false +| ) else ( let q0 = discr_pat omega pss in !| begin match build_specialized_submatrices ~extend_row:(@) q0 pss with | { default; constrs = [] } -> (* first column of pss is made of variables only *) satisfiable default qs | { default; 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 default qs -| end +| ) | {pat_desc=Tpat_variant (l,_,r)}::_ when is_absent l r -> false | q::qs -> let pss = simplify_first_col pss in let q0 = discr_pat q pss in +| if not (first_column_is_coherent pss) then ( +| false +| ) else ( satisfiable (build_specialized_submatrix ~extend_row:(@) q0 pss) (simple_match_args q0 q @ qs) +| ) (* While [satisfiable] only checks whether the last row of [pss + qs] is satisfiable, this function returns the (possibly empty) list of vectors [es] which verify: 1- for all ps in pss, ps # es (ps and es are not compatible) 2- qs <= es (es matches qs) !| This is done to enable GADT handling !| !| For considerations regarding the coherence check, see the comment on !| [satisfiable] above. *) let rec list_satisfying_vectors pss qs = match pss with | [] -> if has_instances qs then [qs] else [] | _ -> match qs with | [] -> [] | {pat_desc = Tpat_or(q1,q2,_)}::qs -> list_satisfying_vectors pss (q1::qs) @ list_satisfying_vectors pss (q2::qs) | {pat_desc = Tpat_alias(q,_,_)}::qs -> list_satisfying_vectors pss (q::qs) | {pat_desc = (Tpat_any | Tpat_var(_))}::qs -> let pss = simplify_first_col pss in +| if not (first_column_is_coherent pss) then ( +| [] +| ) else ( let q0 = discr_pat omega pss in let wild default_matrix p = List.map (fun qs -> p::qs) (list_satisfying_vectors default_matrix qs) in !| begin match build_specialized_submatrices ~extend_row:(@) q0 pss with | { default; constrs = [] } -> (* first column of pss is made of variables only *) wild default omega | { default; constrs = ((p,_)::_ as constrs) } -> let for_constrs () = List.flatten ( List.map (fun (p,pss) -> if is_absent_pat p then @@@@@@@@@@ -1073,28 +1217,33 @@@@@@@@@@ List.map (set_args p) witnesses ) 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 default (build_other_constrs constrs p) @ for_constrs () | _ -> wild default omega -| end +| ) | {pat_desc=Tpat_variant (l,_,r)}::_ when is_absent l r -> [] | q::qs -> let pss = simplify_first_col pss in +| if not (first_column_is_coherent pss) then ( +| [] +| ) else ( let q0 = discr_pat q pss in List.map (set_args q0) (list_satisfying_vectors (build_specialized_submatrix ~extend_row:(@) q0 pss) (simple_match_args q0 q @ qs)) +| ) (******************************************) (* Look for a row that matches some value *) (******************************************) (* Useful for seeing if the example of non-matched value can indeed be matched @@@@@@@@@@ -1113,19 +1262,21 @@@@@@@@@@ | {pat_desc = Tpat_any} -> let rec remove_first_column = function | (_::ps)::rem -> ps::remove_first_column rem | _ -> [] in do_match (remove_first_column pss) qs | _ -> let q0 = normalize_pat q in +| let pss = simplify_first_col pss in +| (* [pss] will (or won't) match [q0 :: qs] regardless of the coherence of +| its first column. *) do_match !| (build_specialized_submatrix ~extend_row:(@) q0 !| (simplify_first_col pss)) (simple_match_args q0 q @ qs) type 'a exhaust_result = | No_matching_value | Witnesses of 'a list let rappend r1 r2 = @@@@@@@@@@ -1168,18 +1319,33 @@@@@@@@@@ This function should be called for exhaustiveness check only. *) let rec exhaust (ext:Path.t option) pss n = match pss with | [] -> Witnesses [omegas n] | []::_ -> No_matching_value | pss -> let pss = simplify_first_col pss in +| if not (first_column_is_coherent pss) then +| (* We're considering an ill-typed branch, we won't actually be able to +| produce a well typed value taking that branch. *) +| No_matching_value +| else ( +| (* 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 !| begin match build_specialized_submatrices ~extend_row:(@) q0 pss with | { default; constrs = [] } -> (* first column of pss is made of variables only *) begin match exhaust ext default (n-1) with | Witnesses r -> Witnesses (List.map (fun row -> q0::row) r) | r -> r end | { default; constrs } -> let try_non_omega (p,pss) = @@@@@@@@@@ -1206,17 +1372,17 @@@@@@@@@@ let p = build_other ext constrs in let dug = List.map (fun tail -> p :: tail) r in match before with | No_matching_value -> Witnesses dug | Witnesses x -> Witnesses (x @ dug) with (* cannot occur, since constructors don't make a full signature *) | Empty -> fatal_error "Parmatch.exhaust" -| end +| ) let exhaust ext pss n = let ret = exhaust ext pss n in match ret with No_matching_value -> No_matching_value | Witnesses lst -> let singletons = List.map @@@@@@@@@@ -1239,18 +1405,21 @@@@@@@@@@ (even if it doesn't help in making the matching exhaustive). *) let rec pressure_variants tdefs = function | [] -> false | []::_ -> true | pss -> let pss = simplify_first_col pss in +| if not (first_column_is_coherent pss) then +| true +| else ( let q0 = discr_pat omega pss in !| begin match build_specialized_submatrices ~extend_row:(@) q0 pss with | { default; constrs = [] } -> pressure_variants tdefs default | { default; constrs } -> let rec try_non_omega = function | (_p,pss) :: rem -> let ok = pressure_variants tdefs pss in (* The order below matters : we want [pressure_variants] to be called on all the specialized submatrices because we might close some variant in any of them regardless of whether [ok] @@@@@@@@@@ -1279,17 +1448,17 @@@@@@@@@@ ({pat_desc=Tpat_variant _} as p,_):: _, Some env -> let row = row_of_pat p in if Btype.row_fixed row || pressure_variants None default then () else close_variant env row | _ -> () end; ok -| end +| ) (* Yet another satisfiable function *) (* This time every_satisfiable pss qs checks the utility of every expansion of qs. Expansion means expansion of or-patterns inside qs @@@@@@@@@@ -1388,17 +1557,17 @@@@@@@@@@ match p.pat_desc with | Tpat_alias (p,_,_) -> simplify_head_pat p ps k | Tpat_var (_,_) -> (omega, ps) :: k | Tpat_or (p1,p2,_) -> simplify_head_pat p1 ps (simplify_head_pat p2 ps k) | _ -> (p, ps) :: k (* Back to normal matrices *) !|let make_vector r = List.rev r.no_ors let make_matrix rs = List.map make_vector rs (* Standard union on answers *) let union_res r1 r2 = match r1, r2 with | (Unused,_) | (_, Unused) -> Unused @@@@@@@@@@ -1480,21 +1649,27 @@@@@@@@@@ else (* this is a real or-pattern *) every_satisfiables (push_or_column pss) (push_or qs) | Tpat_variant (l,_,r) when is_absent l r -> (* Ah Jacques... *) Unused | _ -> (* standard case, filter matrix *) let pss = simplify_first_col pss in +| (* The handling of incoherent matrices is kept in line with +| [satisfiable] *) +| if not (first_column_is_coherent pss) then +| Unused +| else ( let q0 = discr_pat q pss in every_satisfiables (build_specialized_submatrix q0 pss ~extend_row:(fun ps r -> { r with active = ps @ r.active })) {qs with active=simple_match_args q0 q @ rem} +| ) end (* This function ``every_both'' performs the usefulness check of or-pat q1|q2. The trick is to call every_satisfied twice with current active columns restricted to q1 and q2, That way, @@@@@@@@@@ -2162,21 +2337,36 @@@@@@@@@@ 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 *) List.fold_left IdSet.union IdSet.empty stables_in_varsets | rs -> -| let submatrices = split_rows (simplify_first_col rs) in +| let rs = simplify_first_col rs in +| if not (first_column_is_coherent rs) then ( +| (* If the first column is incoherent, then all the variables of this +| matrix are stable. *) +| List.fold_left (fun acc (_, { varsets; _ }) -> +| List.fold_left IdSet.union acc varsets +| ) IdSet.empty rs +| ) else ( +| (* 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 = split_rows rs in let submat_stable = List.map matrix_stable_vars submatrices in (* a stable variable must be stable in each submatrix; if the matrix has at least one row, there is at least one submatrix *) reduce IdSet.inter submat_stable +| ) let pattern_stable_vars p = matrix_stable_vars [{varsets = []; row = [p]}] (* All identifier paths that appear in an expression that occurs as a clause right hand side or guard. The function is rather complex due to the compilation of unpack patterns by introducing code in rhs expressions