Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
Interface with user-defined match monad?
if there's a __match
in scope, we use this as the match strategy, assuming it conforms to MatchStrategy as defined below:
Compute the type T implied for a value v
matched by a pattern pat
(with expected type pt
).
Compute the type T implied for a value v
matched by a pattern pat
(with expected type pt
).
Usually, this is the pattern's type because pattern matching implies instance-of checks.
However, Stable Identifier and Literal patterns are matched using ==
,
which does not imply a type for the binder that binds the matched value.
See SI-1503, SI-5024: don't cast binders to types we're not sure they have
TODO: update spec as follows (deviation between **
):
A pattern binder x@p consists of a pattern variable x and a pattern p. The type of the variable x is the static type T **IMPLIED BY** the pattern p. This pattern matches any value v matched by the pattern p **Deleted: , provided the run-time type of v is also an instance of T, ** and it binds the variable name to that value.
Addition:
A pattern p
_implies_ a type T
if the pattern matches only values of the type T
.