Skip to content

Commit

Permalink
Pattern completeness: Handle structures under union constructors
Browse files Browse the repository at this point in the history
The following now generates a correct counterexample:
```
enum E = {A, B}

struct Foo = { bar : E }

val main : unit -> unit

function main() = {
    let x : Foo = struct { bar = B };
    match Some(x) {
      Some(struct { bar = A }) => (),
      None()  => (),
    }
}
```
whereas previously it would just mark the pattern as potentially
incomplete and continue.
  • Loading branch information
Alasdair committed Sep 7, 2024
1 parent 8d4b9d8 commit b905e9b
Show file tree
Hide file tree
Showing 4 changed files with 38 additions and 1 deletion.
5 changes: 5 additions & 0 deletions src/lib/jib_compile.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1556,6 +1556,11 @@ module Make (C : CONFIG) = struct
let compile_funcl ctx def_annot id pat guard exp =
let debug_attr = get_def_attribute "jib_debug" def_annot in

if Option.is_some debug_attr then (
prerr_endline Util.("Rewritten source for " ^ string_of_id id ^ ":" |> yellow |> bold |> clear);
prerr_endline (Document.to_string (Pretty_print_sail.doc_exp (Type_check.strip_exp exp)))
);

(* Find the function's type. *)
let quant, Typ_aux (fn_typ, _) =
try Env.get_val_spec id ctx.local_env with Type_error.Type_error _ -> Env.get_val_spec id ctx.tc_env
Expand Down
10 changes: 9 additions & 1 deletion src/lib/pattern_completeness.ml
Original file line number Diff line number Diff line change
Expand Up @@ -488,7 +488,15 @@ module Make (C : Config) = struct
field_typs
in
(struct_id, field_typs)
| _ -> Reporting.unreachable l __POS__ "P_struct pattern with non-struct type"
| Some typ -> Reporting.unreachable l __POS__ ("P_struct pattern with non-struct type: " ^ string_of_typ typ)
| None ->
let struct_id =
match typ with
| Typ_aux (Typ_app (id, _), _) -> id
| Typ_aux (Typ_id id, _) -> id
| _ -> Reporting.unreachable l __POS__ ("P_struct pattern with non-struct type: " ^ string_of_typ typ)
in
(struct_id, [])
in
let field_typs = List.fold_left (fun m (typ, field) -> Bindings.add field typ m) Bindings.empty field_typs in
GP_struct
Expand Down
6 changes: 6 additions & 0 deletions test/pattern_completeness/warn_struct_under_option.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
Warning: Incomplete pattern match statement at warn_struct_under_option.sail:14.4-9:
14 | match Some(x) {
 | ^---^
 |
The following expression is unmatched: Some(struct { bar = B })

18 changes: 18 additions & 0 deletions test/pattern_completeness/warn_struct_under_option.sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
default Order dec

$include <prelude.sail>
$include <option.sail>

enum E = {A, B}

struct Foo = { bar : E }

val main : unit -> unit

function main() = {
let x : Foo = struct { bar = B };
match Some(x) {
Some(struct { bar = A }) => (),
None() => (),
}
}

0 comments on commit b905e9b

Please sign in to comment.