[External] : Re: Pattern coverage

[Brian Goetz]

Right, in this model "default" clauses map to "any" patterns.  It 
doesn't (yet) deal with remainder, but that will come in a separate 
section.  This is all about static type checking.  Also, the last two 
rules probably leave out some of the generics support, but that's not 
essential to the model; we're mostly trying to make sure we understand 
what exhaustiveness is, in a way that it can be specified.



On 3/24/2022 1:56 PM, Remi Forax wrote:
> Thanks for sharing,
> in the text, they are several mentions of the default pattern but the 
> default pattern is not defined.
>
> Rémi
>
> ------------------------------------------------------------------------
>
>     *From: *"Brian Goetz" <brian.goetz at oracle.com>
>     *To: *"amber-spec-experts" <amber-spec-experts at openjdk.java.net>
>     *Sent: *Thursday, March 24, 2022 6:39:21 PM
>     *Subject: *Pattern coverage
>
>     I've put a document at
>
>     http://cr.openjdk.java.net/~briangoetz/eg-attachments/Coverage.pdf
>
>     which outlines a formal model for pattern coverage, including
>     record patterns and the effects of sealing. This refines the work
>     we did earlier.  The document may be a bit rough so please let me
>     know if you spot any errors.  The approach here should be more
>     amenable to specification than the previous approach.
>
>
>