diff options
| author | Alasdair Armstrong | 2018-02-06 00:46:33 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-02-06 00:46:33 +0000 |
| commit | 9a8abcb2a327e0ab3133b72c10959ca70bacd211 (patch) | |
| tree | 00ee7920cd375af2e47072a2ae16538d69827325 /src/parse_ast.ml | |
| parent | fc5ad2e3930b06a8bd382639361b31bd7407f395 (diff) | |
Improve destructuring existential types
Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:
val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
function test (() : unit) -> unit = {
let matrix as vector('width, _, 'height) = mk_square ();
_prove(constraint('width = 'height));
()
}
where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax
let vector as 'length = ...
or even
let 'vector = ...
still works under this new scheme in a uniform way, so this is backwards compatible
The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.
Diffstat (limited to 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 5eb8038a..ba948040 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -150,6 +150,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_default_ord (* default order for increasing or decreasing signficant bits *) | ATyp_set of (base_effect) list (* effect set *) | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) + | ATyp_wild | ATyp_tup of (atyp) list (* Tuple type *) | ATyp_app of id * (atyp) list (* type constructor application *) | ATyp_exist of kid list * n_constraint * atyp @@ -239,10 +240,9 @@ type pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) - | P_as of pat * id (* named pattern *) | P_typ of atyp * pat (* typed pattern *) | P_id of id (* identifier *) - | P_var of pat * kid (* bind pat to type variable *) + | P_var of pat * atyp (* bind pat to type variable *) | P_app of id * (pat) list (* union constructor pattern *) | P_record of (fpat) list * bool (* struct pattern *) | P_vector of (pat) list (* vector pattern *) |