diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2_parse.ml | 4 | ||||
| -rw-r--r-- | language/l2_parse.ott | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/language/l2_parse.ml b/language/l2_parse.ml index d0c8f1a8..5aaf8086 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -88,6 +88,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_neg of atyp (* Internal (but not M as I want a datatype constructor) negative nexp *) | ATyp_inc (* increasing (little-endian) *) | ATyp_dec (* decreasing (big-endian) *) + | 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_tup of (atyp) list (* Tuple type *) @@ -376,8 +377,9 @@ val_spec_aux = (* Value type specification *) type -default_typing_spec_aux = (* Default kinding or typing assumption *) +default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *) DT_kind of base_kind * kid + | DT_order of base_kind * atyp | DT_typ of typschm * id diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 9785290f..74522150 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -174,6 +174,7 @@ atyp :: 'ATyp_' ::= | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} + | defaultOrd :: :: default_ord {{ com default order for increasing or decreasing signficant bits }} | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} | atyp1 -> atyp2 effect atyp3 :: :: fn @@ -694,10 +695,11 @@ val_spec :: 'VS_' ::= | val extern typschm id = string :: :: extern_spec default_typing_spec :: 'DT_' ::= - {{ com Default kinding or typing assumption }} + {{ com Default kinding or typing assumption, and default order for literal vectors and vector shorthands }} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} | default base_kind kid :: :: kind + | default base_kind atyp :: :: order | default typschm id :: :: typ % The intended semantics of these is that if an id in binding position % doesn't have a kind or type annotation, then we look through the |