From da3295c3aff40113f2ab073d837a61ecbfa0b02e Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Wed, 30 Oct 2019 14:32:48 +0100 Subject: [PATCH] Typecore.type_pat: refactor ppat_of_type and Need_backtrack in wildcards There is a small, desirable change of behavior in this PR: we do not backtrack on all wildcard pattern explosions, only on those where ppat_of_type knows there will be GADTs. As a result, some exhaustivity counter-examples have been improved with more cases (see testsuite for an example). --- Changes | 5 ++++ .../tests/typing-warnings/exhaustiveness.ml | 2 +- typing/parmatch.ml | 26 +++++++++++++---- typing/parmatch.mli | 29 ++++++++++++++----- typing/typecore.ml | 18 +++++++----- 5 files changed, 58 insertions(+), 22 deletions(-) diff --git a/Changes b/Changes index f871066db341..1c1a34ac2175 100644 --- a/Changes +++ b/Changes @@ -36,6 +36,11 @@ Working version - #9078: make all compilerlibs/ available to ocamltest. (Gabriel Scherer, review by Sébastien Hinderer) +- #9079: typecore/parmatch: refactor ppat_of_type and refine + the use of backtracking on wildcard patterns + (Florian Angeletti, Jacques Garrigue, Gabriel Scherer, + review by Thomas Refis) + ### Build system: ### Bug fixes: diff --git a/testsuite/tests/typing-warnings/exhaustiveness.ml b/testsuite/tests/typing-warnings/exhaustiveness.ml index e2eaeb11b805..1ed1aefc80f5 100644 --- a/testsuite/tests/typing-warnings/exhaustiveness.ml +++ b/testsuite/tests/typing-warnings/exhaustiveness.ml @@ -149,7 +149,7 @@ Line 1, characters 8-47: ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: -{left=Box 0; right=Box 0} +({left=Box 0; right=Box 0}|{left=Box 1; right=Box _}) val f : int box pair -> unit = |}] diff --git a/typing/parmatch.ml b/typing/parmatch.ml index 71b22b615ad3..18799abe3554 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -995,7 +995,8 @@ let pats_of_type ?(always=false) env ty = match ty'.desc with | Tconstr (path, _, _) -> begin try match (Env.find_type path env).type_kind with - | Type_variant cl when always || List.length cl = 1 || + | Type_variant cl when always || List.length cl <= 1 || + (* Only explode when all constructors are GADTs *) List.for_all (fun cd -> cd.Types.cd_res <> None) cl -> let cstrs = fst (Env.find_type_descrs path env) in List.map (pat_of_constr (make_pat Tpat_any ty env)) cstrs @@ -2070,14 +2071,27 @@ let contains_extension pat = | _ -> false) pat -(* Build an untyped or-pattern from its expected type *) +(* Build a pattern from its expected type *) +type pat_explosion = PE_single | PE_gadt_cases +type ppat_of_type = + | PT_empty + | PT_any + | PT_pattern of + pat_explosion * + Parsetree.pattern * + (string, constructor_description) Hashtbl.t * + (string, label_description) Hashtbl.t + let ppat_of_type env ty = match pats_of_type env ty with - | [] -> raise Empty - | [{pat_desc = Tpat_any}] -> - (Conv.mkpat Parsetree.Ppat_any, Hashtbl.create 0, Hashtbl.create 0) + | [] -> PT_empty + | [{pat_desc = Tpat_any}] -> PT_any + | [pat] -> + let (ppat, constrs, labels) = Conv.conv pat in + PT_pattern (PE_single, ppat, constrs, labels) | pats -> - Conv.conv (orify_many pats) + let (ppat, constrs, labels) = Conv.conv (orify_many pats) in + PT_pattern (PE_gadt_cases, ppat, constrs, labels) let do_check_partial ~pred loc casel pss = match pss with | [] -> diff --git a/typing/parmatch.mli b/typing/parmatch.mli index 549fad205c5d..2eb4b8758c97 100644 --- a/typing/parmatch.mli +++ b/typing/parmatch.mli @@ -82,13 +82,28 @@ val pat_of_constr : pattern -> constructor_description -> pattern val complete_constrs : pattern -> constructor_tag list -> constructor_description list -(** [ppat_of_type] builds an untyped or-pattern from its expected type. - May raise [Empty] when [type_expr] is an empty variant *) -val ppat_of_type : - Env.t -> type_expr -> - Parsetree.pattern * - (string, constructor_description) Hashtbl.t * - (string, label_description) Hashtbl.t +(** [ppat_of_type] builds an untyped pattern from its expected type, + for explosion of wildcard patterns in Typecore.type_pat. + + There are four interesting cases: + - the type is empty ([PT_empty]) + - no further explosion is necessary ([PT_any]) + - a single pattern is generated, from a record or tuple type + or a single-variant type ([PE_single]) + - an or-pattern is generated, in the case that all branches + are GADT constructors ([PE_gadt_cases]). + *) +type pat_explosion = PE_single | PE_gadt_cases +type ppat_of_type = + | PT_empty + | PT_any + | PT_pattern of + pat_explosion * + Parsetree.pattern * + (string, constructor_description) Hashtbl.t * + (string, label_description) Hashtbl.t + +val ppat_of_type: Env.t -> type_expr -> ppat_of_type val pressure_variants: Env.t -> pattern list -> unit diff --git a/typing/typecore.ml b/typing/typecore.ml index e5129600d87a..4e308b3e9c0e 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -1262,15 +1262,17 @@ and type_pat_aux | Counter_example {explosion_fuel; _} when explosion_fuel <= 0 -> k' Tpat_any | Counter_example ({explosion_fuel; _} as info) -> - begin match Parmatch.ppat_of_type !env expected_ty with - | exception Parmatch.Empty -> raise (Error (loc, !env, Empty_pattern)) - | (sp, constrs, labels) -> - if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any else - if must_backtrack_on_gadt then raise Need_backtrack else + let open Parmatch in + begin match ppat_of_type !env expected_ty with + | PT_empty -> raise (Error (loc, !env, Empty_pattern)) + | PT_any -> k' Tpat_any + | PT_pattern (explosion, sp, constrs, labels) -> let explosion_fuel = - match sp.ppat_desc with - Parsetree.Ppat_or _ -> explosion_fuel - 5 - | _ -> explosion_fuel - 1 + match explosion with + | PE_single -> explosion_fuel - 1 + | PE_gadt_cases -> + if must_backtrack_on_gadt then raise Need_backtrack; + explosion_fuel - 5 in let mode = Counter_example { info with explosion_fuel; constrs; labels }