Skip to content

Commit

Permalink
Typecore.type_pat: refactor ppat_of_type and Need_backtrack in wildcards
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
garrigue authored and gasche committed Nov 4, 2019
1 parent e27120f commit da3295c
Show file tree
Hide file tree
Showing 5 changed files with 58 additions and 22 deletions.
5 changes: 5 additions & 0 deletions Changes
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion testsuite/tests/typing-warnings/exhaustiveness.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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>
|}]

Expand Down
26 changes: 20 additions & 6 deletions typing/parmatch.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
| [] ->
Expand Down
29 changes: 22 additions & 7 deletions typing/parmatch.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
18 changes: 10 additions & 8 deletions typing/typecore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand Down

0 comments on commit da3295c

Please sign in to comment.