Merge pull request ocaml#9079 from garrigue/refactor-ppat_of_type

Typecore.type_pat: refactor ppat_of_type and Need_backtrack in wildcards

Author: gasche

Changes

@@ -39,6 +39,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:

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 = <fun>
 |}]
 

typing/parmatch.ml

@@ -974,7 +974,7 @@ let complete_tags nconsts nconstrs tags =
 (* build a pattern from a constructor description *)
 let pat_of_constr ex_pat cstr =
   {ex_pat with pat_desc =
-   Tpat_construct (mknoloc (Longident.Lident "?pat_of_constr?"),
+   Tpat_construct (mknoloc (Longident.Lident cstr.cstr_name),
                    cstr, omegas cstr.cstr_arity)}
 
 let orify x y = make_pat (Tpat_or (x, y, None)) x.pat_type x.pat_env
@@ -995,15 +995,16 @@ 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
       | Type_record _ ->
           let labels = snd (Env.find_type_descrs path env) in
           let fields =
             List.map (fun ld ->
-              mknoloc (Longident.Lident "?pat_of_label?"), ld, omega)
+              mknoloc (Longident.Lident ld.lbl_name), ld, omega)
               labels
           in
           [make_pat (Tpat_record (fields, Closed)) ty env]
@@ -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
 | [] ->

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

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 }