rems-project / sail

Sail architecture definition language
Other
624 stars 116 forks source link

Pattern completeness: Handle structures under union constructors #700

Closed Alasdair closed 2 months ago

Alasdair commented 2 months ago

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.

github-actions[bot] commented 2 months ago

Test Results

    9 files  ±0     21 suites  ±0   0s :stopwatch: ±0s   681 tests +1    681 :white_check_mark: +1  0 :zzz: ±0  0 :x: ±0  2 143 runs  +1  2 142 :white_check_mark: +1  1 :zzz: ±0  0 :x: ±0 

Results for commit b905e9bb. ± Comparison against base commit 8d4b9d8d.

:recycle: This comment has been updated with latest results.