diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 163 | ||||
| -rw-r--r-- | language/l2.ml | 201 | ||||
| -rw-r--r-- | language/l2.ott | 153 | ||||
| -rw-r--r-- | language/l2_parse.ml | 174 | ||||
| -rw-r--r-- | language/l2_parse.ott | 124 | ||||
| -rw-r--r-- | language/l2_rules.ott | 20 |
6 files changed, 403 insertions, 432 deletions
diff --git a/language/l2.lem b/language/l2.lem index 177f73cc..8e56f69e 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -22,73 +22,70 @@ val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) +type kid = (* variables with kind, ticked to differntiate from program variables *) + | Var of x + + type base_kind = (* base kind *) | BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) - - -type id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - -type var = (* variables with kind, ticked to differntiate from program variables *) - | Var of x - - -type kind = (* kinds *) - | K_kind of list base_kind + | BK_effect (* kind of effect sets *) type nexp = (* expression of kind $Nat$, for vector sizes and origins *) - | Nexp_id of id (* identifier *) - | Nexp_var of var (* variable *) + | Nexp_var of kid (* variable *) | Nexp_constant of nat (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) -type efct = (* effect *) - | Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) +type kind = (* kinds *) + | K_kind of list base_kind -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of var (* identifier *) - | KOpt_kind of kind * var (* kind-annotated variable *) +type base_effect = (* effect *) + | BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) -type nexp_constraint = (* constraint over kind $Nat$ *) +type n_constraint = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of id * list nat + | NC_nat_set_bounded of kid * list nat + + +type kinded_id = (* optionally kind-annotated identifier *) + | KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type order = (* vector order specifications, of kind $Order$ *) - | Ord_id of id (* identifier *) - | Ord_var of var (* variable *) + | Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) -type effects = (* effect set, of kind $Effects$ *) - | Effects_id of id - | Effects_var of var - | Effects_set of list efct (* effect set *) +type effect = (* effect set, of kind $Effects$ *) + | Effect_var of kid + | Effect_set of list base_effect (* effect set *) + + +type id = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) + | QI_const of n_constraint (* A constraint for this type *) type lit = (* Literal constant *) @@ -107,8 +104,8 @@ type lit = (* Literal constant *) type typ = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) - | Typ_var of var (* Type variable *) - | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) + | Typ_var of kid (* Type variable *) + | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) | Typ_tup of list typ (* Tuple type *) | Typ_app of id * list typ_arg (* type constructor application *) @@ -116,7 +113,7 @@ and typ_arg = (* Type constructor arguments of all kinds *) | Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order - | Typ_arg_effects of effects + | Typ_arg_effect of effect type typquant = (* type quantifiers and constraints *) @@ -173,7 +170,7 @@ type exp = (* Expression *) and lexp = (* lvalue expression *) | LEXP_id of id (* identifier *) - | LEXP_memory of id * exp (* memory write via function call *) + | LEXP_memory of id * list exp (* memory write via function call *) | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) | LEXP_field of lexp * id (* struct field *) @@ -192,15 +189,25 @@ and letbind = (* Let binding *) | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) -type effects_opt = (* Optional effect annotation for functions *) - | Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +type type_union = (* Type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id type funcl = (* Function clause *) | FCL_Funcl of id * pat * exp +type effect_opt = (* Optional effect annotation for functions *) + | Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + +type name_scm_opt = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string + + type rec_opt = (* Optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) @@ -210,42 +217,41 @@ type tannot_opt = (* Optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ -type type_union = (* Type union constructors *) - | Tu_id of id - | Tu_ty_id of typ * id - - -type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string - - type index_range = (* index specification, for bitfields in register types *) | BF_single of nat (* single index *) | BF_range of nat * nat (* index range *) | BF_concat of index_range * index_range (* concatenation of index ranges *) -type fundef = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effects_opt * list funcl - - -type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * var - | DT_typ of typschm * id - - type val_spec = (* Value type specification *) | VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) +type scattered_def = (* Function and type union definitions that can be spread across + a file. Each one must end in $id$ *) + | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of funcl (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) + + +type fundef = (* Function definition *) + | FD_function of rec_opt * tannot_opt * effect_opt * list funcl + + +type default_spec = (* Default kinding or typing assumption *) + | DT_kind of base_kind * kid + | DT_typ of typschm * id + + type type_def = (* Type definition body *) - | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) @@ -254,34 +260,13 @@ type def = (* Top-level definition *) | DEF_fundef of fundef (* function definition *) | DEF_val of letbind (* value definition *) | DEF_spec of val_spec (* top-level type constraint *) - | DEF_default of default_typing_spec (* default kind and type assumptions *) + | DEF_default of default_spec (* default kind and type assumptions *) + | DEF_scattered of scattered_def (* scattered function and type definition *) | DEF_reg_dec of typ * id (* register declaration *) - | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) type defs = (* Definition sequence *) | Defs of list def -type typ_lib = (* library types and syntactic sugar for them *) - | Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $true$ and $false$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) - | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *) - | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *) - | Typ_lib_list of typ (* list of typ *) - | Typ_lib_set of typ (* finite set of typ *) - | Typ_lib_reg of typ (* mutable register components holding typ *) - - diff --git a/language/l2.ml b/language/l2.ml index 10b4fd7e..1ee2b64e 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -16,33 +16,22 @@ base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) + | BK_effect (* kind of effect sets *) type -var_aux = (* variables with kind, ticked to differntiate from program variables *) +kid_aux = (* variables with kind, ticked to differntiate from program variables *) Var of x type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) - - -type base_kind = BK_aux of base_kind_aux * l type -var = - Var_aux of var_aux * l - - -type -id = - Id_aux of id_aux * l +kid = + Kid_aux of kid_aux * l type @@ -52,8 +41,7 @@ kind_aux = (* kinds *) type nexp_aux = (* expression of kind $_$, for vector sizes and origins *) - Nexp_id of id (* identifier *) - | Nexp_var of var (* variable *) + Nexp_var of kid (* variable *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) @@ -69,22 +57,22 @@ kind = type -nexp_constraint_aux = (* constraint over kind $_$ *) +n_constraint_aux = (* constraint over kind $_$ *) NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of id * (int) list + | NC_nat_set_bounded of kid * (int) list type kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of var (* identifier *) - | KOpt_kind of kind * var (* kind-annotated variable *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +n_constraint = + NC_aux of n_constraint_aux * l type @@ -93,25 +81,25 @@ kinded_id = type -efct_aux = (* effect *) - Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) +base_effect_aux = (* effect *) + BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) + | QI_const of n_constraint (* A constraint for this type *) type -efct = - Effect_aux of efct_aux * l +base_effect = + BE_aux of base_effect_aux * l type @@ -120,29 +108,33 @@ quant_item = type -effects_aux = (* effect set, of kind $_$ *) - Effects_id of id - | Effects_var of var - | Effects_set of (efct) list (* effect set *) +effect_aux = (* effect set, of kind $_$ *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) type order_aux = (* vector order specifications, of kind $_$ *) - Ord_id of id (* identifier *) - | Ord_var of var (* variable *) + Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type typquant_aux = (* type quantifiers and constraints *) TypQ_tq of (quant_item) list | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type -effects = - Effects_aux of effects_aux * l +effect = + Effect_aux of effect_aux * l type @@ -151,6 +143,11 @@ order = type +id = + Id_aux of id_aux * l + + +type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) | L_zero (* $_ : _$ *) @@ -173,8 +170,8 @@ type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) - | Typ_var of var (* Type variable *) - | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) + | Typ_var of kid (* Type variable *) + | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *) | Typ_tup of (typ) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) @@ -185,7 +182,7 @@ and typ_arg_aux = (* Type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order - | Typ_arg_effects of effects + | Typ_arg_effect of effect and typ_arg = Typ_arg_aux of typ_arg_aux * l @@ -232,17 +229,7 @@ typschm = type -'a exp = - E_aux of 'a exp_aux * 'a annot - -and 'a lexp_aux = (* lvalue expression *) - LEXP_id of id (* identifier *) - | LEXP_memory of id * 'a exp (* memory write via function call *) - | LEXP_vector of 'a lexp * 'a exp (* vector element *) - | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) - | LEXP_field of 'a lexp * id (* struct field *) - -and 'a lexp = +'a lexp = LEXP_aux of 'a lexp_aux * 'a annot and 'a fexp_aux = (* Field-expression *) @@ -295,11 +282,21 @@ and 'a exp_aux = (* Expression *) | E_let of 'a letbind * 'a exp (* let expression *) | E_assign of 'a lexp * 'a exp (* imperative assignment *) +and 'a exp = + E_aux of 'a exp_aux * 'a annot + +and 'a lexp_aux = (* lvalue expression *) + LEXP_id of id (* identifier *) + | LEXP_memory of id * ('a exp) list (* memory write via function call *) + | LEXP_vector of 'a lexp * 'a exp (* vector element *) + | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) + | LEXP_field of 'a lexp * id (* struct field *) + type -'a effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +'a effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect type @@ -319,7 +316,7 @@ type type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) +name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) Name_sect_none | Name_sect_some of string @@ -331,8 +328,8 @@ type_union_aux = (* Type union constructors *) type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +'a effect_opt = + Effect_opt_aux of 'a effect_opt_aux * 'a annot type @@ -351,6 +348,16 @@ type type +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l + + +type +type_union = + Tu_aux of type_union_aux * l + + +type index_range_aux = (* index specification, for bitfields in register types *) BF_single of int (* single index *) | BF_range of int * int (* index range *) @@ -361,32 +368,32 @@ and index_range = type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l - - -type -type_union = - Tu_aux of type_union_aux * l +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * 'a tannot_opt * 'a effect_opt * ('a funcl) list type -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list +'a scattered_def_aux = (* Function and type union definitions that can be spread across + a file. Each one must end in $_$ *) + SD_scattered_function of rec_opt * 'a tannot_opt * 'a effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of 'a funcl (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) type 'a type_def_aux = (* Type definition body *) - TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * (type_union) list * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *) + TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * var +'a default_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * kid | DT_typ of typschm * id @@ -403,13 +410,18 @@ type type +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot + + +type 'a type_def = TD_aux of 'a type_def_aux * 'a annot type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a default_spec = + DT_aux of 'a default_spec_aux * 'a annot type @@ -423,31 +435,9 @@ type | DEF_fundef of 'a fundef (* function definition *) | DEF_val of 'a letbind (* value definition *) | DEF_spec of 'a val_spec (* top-level type constraint *) - | DEF_default of 'a default_typing_spec (* default kind and type assumptions *) + | DEF_default of 'a default_spec (* default kind and type assumptions *) + | DEF_scattered of 'a scattered_def (* scattered function and type definition *) | DEF_reg_dec of typ * id (* register declaration *) - | DEF_scattered_function of rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of 'a funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * typ * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) - - -type -'a typ_lib_aux = (* library types and syntactic sugar for them *) - Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $_$ and $_$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) - | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of nexp * nexp * order * typ (* vector of typ, indexed by natural range *) - | Typ_lib_vector2 of typ * nexp (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * nexp * nexp (* sugar for vector indexed by [ nexp..nexp ] *) - | Typ_lib_list of typ (* list of typ *) - | Typ_lib_set of typ (* finite set of typ *) - | Typ_lib_reg of typ (* mutable register components holding typ *) type @@ -456,11 +446,6 @@ type type -'a typ_lib = - Typ_lib_aux of 'a typ_lib_aux * l - - -type 'a defs = (* Definition sequence *) Defs of ('a def) list diff --git a/language/l2.ott b/language/l2.ott index 6b81b6e8..b3a3f8b8 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -116,7 +116,7 @@ id :: '' ::= | bit :: M :: bit {{ ichlo bit_id }} | unit :: M :: unit {{ ichlo unit_id }} | nat :: M :: nat {{ ichlo nat_id }} - | string :: M :: string {{ ichlo string_id }} + | string :: M :: string {{ tex \ottkw{string} }} {{ ichlo string_id }} | enum :: M :: enum {{ ichlo enum_id }} | vector :: M :: vector {{ ichlo vector_id }} | list :: M :: list {{ ichlo list_id }} @@ -129,7 +129,7 @@ id :: '' ::= % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. -var :: '' ::= +kid :: '' ::= {{ com variables with kind, ticked to differntiate from program variables }} {{ aux _ l }} | ' x :: :: var @@ -148,20 +148,18 @@ base_kind :: 'BK_' ::= | Type :: :: type {{ com kind of types }} | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} - | Effects :: :: effects {{ com kind of effect sets }} + | Effect :: :: effect {{ com kind of effect sets }} kind :: 'K_' ::= {{ com kinds}} {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat , .. Order , .. or Effects - nexp :: 'Nexp_' ::= {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} {{ aux _ l }} - | id :: :: id {{ com identifier }} - | var :: :: var {{ com variable }} + | kid :: :: var {{ com variable }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} %{{ com must be linear after normalisation... except for the type of *, ahem }} @@ -172,13 +170,12 @@ nexp :: 'Nexp_' ::= order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} {{ aux _ l }} - | id :: :: id {{ com identifier }} - | var :: :: var {{ com variable }} + | kid :: :: var {{ com variable }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ ichlo [[order]] }} -efct :: 'Effect_' ::= +base_effect :: 'BE_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -190,14 +187,13 @@ efct :: 'Effect_' ::= | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} -effects :: 'Effects_' ::= +effect :: 'Effect_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} - | effect id :: :: id - | effect var :: :: var - | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} + | kid :: :: var + | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ ichlo [] }} - | effects1 u+ .. u+ effectsn :: M :: union {{ com meta operation for combining sets of effects }} {{ ichlo [] }} + | effect1 u+ .. u+ effectn :: M :: union {{ com meta operation for combining sets of effects }} {{ ichlo [] }} % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. @@ -208,18 +204,36 @@ typ :: 'Typ_' ::= {{ com Unspecified type }} | id :: :: id {{ com Defined type }} - | var :: :: var + | kid :: :: var {{ com Type variable }} - | typ1 -> typ2 effects :: :: fn + | typ1 -> typ2 effectkw effect :: :: fn {{ com Function type (first-order only in user code) }} % TODO: build first-order restriction into AST or just into type rules? neither - see note % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. | typ1 * .... * typn :: :: tup {{ com Tuple type }} % TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker - | id < typ_arg1 .. typ_argn > :: :: app + | id < typ_arg1 , .. , typ_argn > :: :: app {{ com type constructor application }} | ( typ ) :: S :: paren {{ ichlo [[typ]] }} +% | enum < nexp1, nexp2, order> :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }} + | [| nexp |] :: S :: enum1 {{ichlo enum <[[nexp]], 0, inc> }} {{ com sugar for \texttt{enum nexp 0 inc} }} + | [| nexp : nexp' |] :: S :: enum2 {{ichlo enum <[[nexp]],[[nexp']],inc> }} {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} +% use .. not - to avoid ambiguity with nexp - +% total maps and vectors indexed by finite subranges of nat +% | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} +% probably some sugar for vector types, using [ ] similarly to enums: +% (but with .. not : in the former, to avoid confusion...) + | typ [ nexp ] :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} {{ com sugar for vector indexed by [ [[nexp]] ] }} + | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }} +% ...so bit [ nexp ] etc is just an instance of that +% | List < typ > :: :: list {{ com list of [[typ]] }} +% | Set < typ > :: :: set {{ com finite set of [[typ]] }} +% | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }} +% "reg t" is basically the ML "t ref" +% not sure how first-class it should be, though +% use "reg word32" etc for the types of vanilla registers + typ_arg :: 'Typ_arg_' ::= {{ com Type constructor arguments of all kinds }} @@ -227,38 +241,21 @@ typ_arg :: 'Typ_arg_' ::= | nexp :: :: nexp | typ :: :: typ | order :: :: order - | effects :: :: effects + | effect :: :: effect % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ -typ_lib :: 'Typ_lib_' ::= - {{ com library types and syntactic sugar for them }} - {{ aux _ l }} {{ auxparam 'a }} +%typ_lib :: 'Typ_lib_' ::= +% {{ com library types and syntactic sugar for them }} +% {{ aux _ l }} {{ auxparam 'a }} % boring base types: - | unit :: :: unit {{ com unit type with value $()$ }} - | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} - | bit :: :: bit {{ com pure bit values (not mutable bits) }} +%% | unit :: :: unit {{ com unit type with value $()$ }} +% | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} +% | bit :: :: bit {{ com pure bit values (not mutable bits) }} % experimentally trying with two distinct types of bool and bit ... - | nat :: :: nat {{ com natural numbers 0,1,2,... }} - | string :: :: string {{ com UTF8 strings }} +% | nat :: :: nat {{ com natural numbers 0,1,2,... }} +% | string :: :: string {{ com UTF8 strings }} % finite subranges of nat - | Enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }} - | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} - | [ nexp : nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} -% use .. not - to avoid ambiguity with nexp - -% total maps and vectors indexed by finite subranges of nat - | Vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} -% probably some sugar for vector types, using [ ] similarly to enums: -% (but with .. not : in the former, to avoid confusion...) - | typ [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }} - | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }} -% ...so bit [ nexp ] etc is just an instance of that - | List < typ > :: :: list {{ com list of [[typ]] }} - | Set < typ > :: :: set {{ com finite set of [[typ]] }} - | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }} -% "reg t" is basically the ML "t ref" -% not sure how first-class it should be, though -% use "reg word32" etc for the types of vanilla registers parsing @@ -270,13 +267,13 @@ Typ_fn <= Typ_tup grammar -nexp_constraint :: 'NC_' ::= +n_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le - | id 'IN' { num1 , ... , numn } :: :: nat_set_bounded + | kid 'IN' { num1 , ... , numn } :: :: nat_set_bounded % Note only id on the left and constants on the right in a % finite-set-bound, as we don't think we need anything more @@ -284,14 +281,14 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} - | var :: :: none {{ com identifier }} - | kind var :: :: kind {{ com kind-annotated variable }} + | kid :: :: none {{ com identifier }} + | kind kid :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} {{ aux _ l }} | kinded_id :: :: id {{ com An optionally kinded identifier }} - | nexp_constraint :: :: const {{ com A constraint for this type }} + | n_constraint :: :: const {{ com A constraint for this type }} typquant :: 'TypQ_' ::= {{ com type quantifiers and constraints}} @@ -332,7 +329,7 @@ grammar %% | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn :: :: variant %% {{ com Variant types }} %% - naming_scheme_opt :: 'Name_sect_' ::= + name_scm_opt :: 'Name_sect_' ::= {{ com Optional variable-naming-scheme specification for variables of defined type }} {{ aux _ l }} | :: :: none @@ -353,18 +350,18 @@ grammar type_def :: 'TD_' ::= {{ com Type definition body }} {{ aux _ annot }} {{ auxparam 'a }} - | typedef id naming_scheme_opt = typschm :: :: abbrev + | typedef id name_scm_opt = typschm :: :: abbrev {{ com type abbreviation }} {{ texlong }} - | typedef id naming_scheme_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record + | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record {{ com struct type definition }} {{ texlong }} % for specifying constructor result types of nat-indexed GADTs, we can % let the typi be function types (as constructors are not allowed to % take parameters of function types) % concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = - | typedef id naming_scheme_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant {{ com union type definition}} {{ texlong }} - | typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum {{ com enumeration type definition}} {{ texlong }} | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } @@ -521,9 +518,9 @@ exp :: 'E_' ::= | id ( exp1 , .. , expn ) :: :: app {{ com function application }} + | id exp :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} {{ com No extra parens needed when exp is a tuple }} + % Note: fully applied function application only -% We might restrict exp to be an identifier -% We might require expn to have outermost parentheses (but not two sets if it's a tuple) | exp1 id exp2 :: :: app_infix {{ com infix function application }} @@ -620,7 +617,8 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} - | id exp :: :: memory {{ com memory write via function call }} + | id ( exp1 , .. , expn ) :: :: memory {{ com memory write via function call }} + | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} | lexp [ exp ] :: :: vector {{ com vector element }} | lexp [ exp1 : exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too @@ -727,11 +725,11 @@ rec_opt :: 'Rec_' ::= | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} -effects_opt :: 'Effects_opt_' ::= +effect_opt :: 'Effect_opt_' ::= {{ com Optional effect annotation for functions }} {{ aux _ annot }} {{ auxparam 'a }} | :: :: pure {{ com sugar for empty effect set }} - | effects :: :: effects + | effectkw effect :: :: effect funcl :: 'FCL_' ::= {{ com Function clause }} @@ -742,7 +740,7 @@ funcl :: 'FCL_' ::= fundef :: 'FD_' ::= {{ com Function definition}} {{ aux _ annot }} {{ auxparam 'a }} - | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }} + | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} % {{ com function definition }} % TODO note that the typ in the tannot_opt is the *result* type, not % the type of the whole function. The argument type comes from the @@ -769,10 +767,10 @@ val_spec :: 'VS_' ::= | val extern typschm id = string :: :: extern_spec {{ com Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked }} -default_typing_spec :: 'DT_' ::= +default_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ annot }} {{ auxparam 'a }} - | default base_kind var :: :: kind + | default base_kind kid :: :: kind | 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 @@ -781,6 +779,22 @@ default_typing_spec :: 'DT_' ::= % Otherwise we try to infer. Perhaps warn if there are multiple matches. % For example, we might often have default Type ['alphanum] +scattered_def :: 'SD_' ::= + {{ com Function and type union definitions that can be spread across + a file. Each one must end in $[[end id]]$ }} + {{ aux _ annot }} {{ auxparam 'a }} + | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} + + | function clause funcl :: :: scattered_funcl +{{ com scattered function definition clause }} + + | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} + + | union id member type_union :: :: scattered_unioncl {{ com scattered union definition member }} + | end id :: :: scattered_end +{{ com scattered definition end }} + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -796,21 +810,13 @@ def :: 'DEF_' ::= {{ com value definition }} | val_spec :: :: spec {{ com top-level type constraint }} - | default_typing_spec :: :: default + | default_spec :: :: default {{ com default kind and type assumptions }} + | scattered_def :: :: scattered + {{ com scattered function and type definition }} | register typ id :: :: reg_dec {{ com register declaration }} - | scattered function rec_opt tannot_opt effects_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} - - | function clause funcl :: :: scattered_funcl -{{ com scattered function definition clause }} - - | scattered typedef id naming_scheme_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} - - | union id member typ id' :: :: scattered_unioncl {{ com scattered union definition member }} - | end id :: :: scattered_end -{{ com scattered definition end }} defs :: '' ::= {{ com Definition sequence }} @@ -886,6 +892,8 @@ terminals :: '' ::= {{ tex \ensuremath{\Rightarrow} }} | -- :: :: dashdash {{ tex \mbox{--} }} + | effectkw :: :: effectkw + {{ tex \ottkw{effect} }} | empty :: :: empty {{ tex \ensuremath{\epsilon} }} | consistent_increase :: :: ci @@ -894,3 +902,4 @@ terminals :: '' ::= {{ tex \ottkw{consistent\_decrease}~ }} + diff --git a/language/l2_parse.ml b/language/l2_parse.ml index b196f007..a6ada0ec 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -1,4 +1,4 @@ -(* generated by Ott 0.22 from: l2_parse.ott *) +(* generated by Ott 0.23 from: l2_parse.ott *) type text = string @@ -21,7 +21,7 @@ base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) + | BK_effect (* kind of effect sets *) type @@ -31,19 +31,19 @@ id_aux = (* Identifier *) type -var_aux = (* variables with kind, ticked to differntiate from program variables *) +kid_aux = (* identifiers with kind, ticked to differntiate from program variables *) Var of x type -efct_aux = (* effect *) - Effect_rreg (* read register *) - | Effect_wreg (* write register *) - | Effect_rmem (* read memory *) - | Effect_wmem (* write memory *) - | Effect_undef (* undefined-instruction exception *) - | Effect_unspec (* unspecified values *) - | Effect_nondet (* nondeterminism from intra-instruction parallelism *) +base_effect_aux = (* effect *) + BE_rreg (* read register *) + | BE_wreg (* write register *) + | BE_rmem (* read memory *) + | BE_wmem (* write memory *) + | BE_undef (* undefined-instruction exception *) + | BE_unspec (* unspecified values *) + | BE_nondet (* nondeterminism from intra-instruction parallelism *) type @@ -57,13 +57,13 @@ id = type -var = - Var_aux of var_aux * l +kid = + Kid_aux of kid_aux * l type -efct = - Effect_aux of efct_aux * l +base_effect = + BE_aux of base_effect_aux * l type @@ -74,17 +74,14 @@ kind_aux = (* kinds *) type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) ATyp_id of id (* identifier *) - | ATyp_var of var (* ticked variable *) + | ATyp_var of kid (* ticked variable *) | ATyp_constant of int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) | ATyp_exp of atyp (* exponential *) | ATyp_inc (* increasing (little-endian) *) | ATyp_dec (* decreasing (big-endian) *) - | ATyp_efid of id - | ATyp_efvar of var - | ATyp_set of (efct) list (* effect set *) - | ATyp_wild (* Unspecified type *) + | 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 *) | ATyp_app of id * (atyp) list (* type constructor application *) @@ -99,22 +96,22 @@ kind = type -nexp_constraint_aux = (* constraint over kind $_$ *) +n_constraint_aux = (* constraint over kind $_$ *) NC_fixed of atyp * atyp | NC_bounded_ge of atyp * atyp | NC_bounded_le of atyp * atyp - | NC_nat_set_bounded of id * (int) list + | NC_nat_set_bounded of kid * (int) list type kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of var (* identifier *) - | KOpt_kind of kind * var (* kind-annotated variable *) + KOpt_none of kid (* identifier *) + | KOpt_kind of kind * kid (* kind-annotated variable *) type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +n_constraint = + NC_aux of n_constraint_aux * l type @@ -125,7 +122,7 @@ kinded_id = type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) + | QI_const of n_constraint (* A constraint for this type *) type @@ -254,15 +251,21 @@ and letbind = type +name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string + + +type type_union_aux = (* Type union constructors *) Tu_id of id | Tu_ty_id of atyp * id type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type @@ -272,9 +275,9 @@ tannot_opt_aux = (* Optional type annotation for functions *) type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +effect_opt_aux = (* Optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of atyp type @@ -283,14 +286,8 @@ funcl_aux = (* Function clause *) type -effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of atyp - - -type -type_union = - Tu_aux of type_union_aux * l +name_scm_opt = + Name_sect_aux of name_scm_opt_aux * l type @@ -304,8 +301,13 @@ and index_range = type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +type_union = + Tu_aux of type_union_aux * l + + +type +rec_opt = + Rec_aux of rec_opt_aux * l type @@ -314,8 +316,8 @@ tannot_opt = type -rec_opt = - Rec_aux of rec_opt_aux * l +effect_opt = + Effect_opt_aux of effect_opt_aux * l type @@ -324,40 +326,55 @@ funcl = type -effects_opt = - Effects_opt_aux of effects_opt_aux * l +type_def_aux = (* Type definition body *) + TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) + | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *) + | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) type -type_def_aux = (* Type definition body *) - TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) - | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * (type_union) list * bool (* union type definition *) - | TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *) - | TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *) +scattered_def_aux = (* Function and type union definitions that can be spread across + a file. Each one must end in $_$ *) + SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) + | SD_scattered_funcl of funcl (* scattered function definition clause *) + | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *) + | SD_scattered_unioncl of id * type_union (* scattered union definition member *) + | SD_scattered_end of id (* scattered definition end *) + + +type +val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string type default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * var + DT_kind of base_kind * kid | DT_typ of typschm * id type fundef_aux = (* Function definition *) - FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list + FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list type -val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string +type_def = + TD_aux of type_def_aux * l type -type_def = - TD_aux of type_def_aux * l +scattered_def = + SD_aux of scattered_def_aux * l + + +type +val_spec = + VS_aux of val_spec_aux * l type @@ -371,23 +388,14 @@ fundef = type -val_spec = - VS_aux of val_spec_aux * l - - -type def_aux = (* Top-level definition *) DEF_type of type_def (* type definition *) | DEF_fundef of fundef (* function definition *) | DEF_val of letbind (* value definition *) | DEF_spec of val_spec (* top-level type constraint *) | DEF_default of default_typing_spec (* default kind and type assumptions *) + | DEF_scattered of scattered_def (* scattered definition *) | DEF_reg_dec of atyp * id (* register declaration *) - | DEF_scattered_function of rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) - | DEF_scattered_funcl of funcl (* scattered function definition clause *) - | DEF_scattered_variant of id * naming_scheme_opt * typquant (* scattered union definition header *) - | DEF_scattered_unioncl of id * atyp * id (* scattered union definition member *) - | DEF_scattered_end of id (* scattered definition end *) type @@ -396,26 +404,9 @@ def = type -typ_lib_aux = (* library types and syntactic sugar for them *) - Typ_lib_unit (* unit type with value $()$ *) - | Typ_lib_bool (* booleans $_$ and $_$ *) - | Typ_lib_bit (* pure bit values (not mutable bits) *) - | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) - | Typ_lib_enum (* natural numbers _ .. _+_-1, ordered by order *) - | Typ_lib_enum1 (* sugar for \texttt{enum nexp 0 inc} *) - | Typ_lib_enum2 (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of atyp (* vector of atyp, indexed by natural range *) - | Typ_lib_vector2 of atyp (* sugar for vector indexed by [ atyp ] *) - | Typ_lib_vector3 of atyp (* sugar for vector indexed by [ atyp.._ ] *) - | Typ_lib_list of atyp (* list of atyp *) - | Typ_lib_set of atyp (* finite set of atyp *) - | Typ_lib_reg of atyp (* mutable register components holding atyp *) - - -type lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) + | LEXP_mem of id * (exp) list | LEXP_vector of lexp * exp (* vector element *) | LEXP_vector_range of lexp * exp * exp (* subvector *) | LEXP_field of lexp * id (* struct field *) @@ -429,9 +420,4 @@ defs = (* Definition sequence *) Defs of (def) list -type -typ_lib = - Typ_lib_aux of typ_lib_aux * l - - diff --git a/language/l2_parse.ott b/language/l2_parse.ott index f96c3f99..af90abaa 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -119,8 +119,8 @@ id :: '' ::= | ( deinfix x ) :: :: deIid {{ com remove infix status }} -var :: '' ::= - {{ com variables with kind, ticked to differntiate from program variables }} +kid :: '' ::= + {{ com identifiers with kind, ticked to differntiate from program variables }} {{ aux _ l }} | ' x :: :: var @@ -145,7 +145,7 @@ base_kind :: 'BK_' ::= | Type :: :: type {{ com kind of types }} | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} - | Effects :: :: effects {{ com kind of effect sets }} + | Effect :: :: effect {{ com kind of effect sets }} kind :: 'K_' ::= {{ com kinds}} @@ -153,7 +153,7 @@ kind :: 'K_' ::= | base_kind1 -> ... -> base_kindn :: :: kind % we'll never use ...-> Nat -efct :: 'Effect_' ::= +base_effect :: 'BE_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -168,7 +168,7 @@ atyp :: 'ATyp_' ::= {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }} {{ aux _ l }} | id :: :: id {{ com identifier }} - | var :: :: var {{ com ticked variable }} + | kid :: :: var {{ com ticked variable }} | num :: :: constant {{ com constant }} | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} @@ -177,48 +177,43 @@ atyp :: 'ATyp_' ::= | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} - | effect id :: :: efid - | effect var :: :: efvar - | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} + | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} - - | _ :: :: wild - {{ com Unspecified type }} - | atyp1 -> atyp2 atyp3 :: :: fn + | atyp1 -> atyp2 effect atyp3 :: :: fn {{ com Function type (first-order only in user code), last atyp is an effect }} | atyp1 * .... * atypn :: :: tup {{ com Tuple type }} - | id < atyp1 .. atypn > :: :: app + | id < atyp1 , .. , atypn > :: :: app {{ com type constructor application }} % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ -typ_lib :: 'Typ_lib_' ::= - {{ com library types and syntactic sugar for them }} - {{ aux _ l }} %{{ auxparam 'a }} +%typ_lib :: 'Typ_lib_' ::= +% {{ com library types and syntactic sugar for them }} +% {{ aux _ l }} %{{ auxparam 'a }} % boring base types: - | unit :: :: unit {{ com unit type with value $()$ }} - | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} - | bit :: :: bit {{ com pure bit values (not mutable bits) }} +% | unit :: :: unit {{ com unit type with value $()$ }} +% | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }} +% | bit :: :: bit {{ com pure bit values (not mutable bits) }} % experimentally trying with two distinct types of bool and bit ... - | nat :: :: nat {{ com natural numbers 0,1,2,... }} - | string :: :: string {{ com UTF8 strings }} +% | nat :: :: nat {{ com natural numbers 0,1,2,... }} +% | string :: :: string {{ com UTF8 strings }} % finite subranges of nat - | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[atyp2]] .. [[atyp2]]+[[atyp1]]-1, ordered by order }} - | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} - | [ nexp : nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} +% | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[atyp2]] .. [[atyp2]]+[[atyp1]]-1, ordered by order }} +% | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} +% | [ nexp : nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} % use .. not - to avoid ambiguity with nexp - % total maps and vectors indexed by finite subranges of nat - | vector nexp1 nexp2 order atyp :: :: vector {{ com vector of [[atyp]], indexed by natural range }} +% | vector nexp1 nexp2 order atyp :: :: vector {{ com vector of [[atyp]], indexed by natural range }} % probably some sugar for vector types, using [ ] similarly to enums: % (but with .. not : in the former, to avoid confusion...) - | atyp [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[atyp]] ] }} - | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[atyp]]..[[atyp']] ] }} +% | atyp [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[atyp]] ] }} +% | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[atyp]]..[[atyp']] ] }} % ...so bit [ nexp ] etc is just an instance of that - | list atyp :: :: list {{ com list of [[atyp]] }} - | set atyp :: :: set {{ com finite set of [[atyp]] }} - | reg atyp :: :: reg {{ com mutable register components holding [[atyp]] }} +% | list atyp :: :: list {{ com list of [[atyp]] }} +% | set atyp :: :: set {{ com finite set of [[atyp]] }} +% | reg atyp :: :: reg {{ com mutable register components holding [[atyp]] }} % "reg t" is basically the ML "t ref" % not sure how first-class it should be, though % use "reg word32" etc for the types of vanilla registers @@ -231,13 +226,13 @@ ATyp_fn <= ATyp_tup grammar -nexp_constraint :: 'NC_' ::= +n_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} | atyp = atyp' :: :: fixed | atyp >= atyp' :: :: bounded_ge | atyp '<=' atyp' :: :: bounded_le - | id 'IN' { num1 , ... , numn } :: :: nat_set_bounded + | kid 'IN' { num1 , ... , numn } :: :: nat_set_bounded % Note only id on the left and constants on the right in a % finite-set-bound, as we don't think we need anything more @@ -245,14 +240,14 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} - | var :: :: none {{ com identifier }} - | kind var :: :: kind {{ com kind-annotated variable }} + | kid :: :: none {{ com identifier }} + | kind kid :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} {{ aux _ l }} | kinded_id :: :: id {{ com An optionally kinded identifier }} - | nexp_constraint :: :: const {{ com A constraint for this type }} + | n_constraint :: :: const {{ com A constraint for this type }} typquant :: 'TypQ_' ::= {{ com type quantifiers and constraints}} @@ -279,7 +274,7 @@ grammar % but we could get away with disallowing constraints in typschm, we % think - if it's useful to do that - naming_scheme_opt :: 'Name_sect_' ::= + name_scm_opt :: 'Name_sect_' ::= {{ com Optional variable-naming-scheme specification for variables of defined type }} {{ aux _ l }} | :: :: none @@ -294,16 +289,16 @@ type_union :: 'Tu_' ::= type_def :: 'TD_' ::= {{ com Type definition body }} {{ aux _ l }} - | typedef id naming_scheme_opt = typschm :: :: abbrev + | typedef id name_scm_opt = typschm :: :: abbrev {{ com type abbreviation }} {{ texlong }} - | typedef id naming_scheme_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record + | typedef id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record {{ com struct type definition }} {{ texlong }} - | typedef id naming_scheme_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant {{ com union type definition}} {{ texlong }} - | typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum {{ com enumeration type definition}} {{ texlong }} - | typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } + | typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} % also sugar [ nexp ] @@ -371,7 +366,7 @@ pat :: 'P_' ::= {{ com wildcard }} | ( pat as id ) :: :: as {{ com named pattern }} - | ( ( atyp ) pat ) :: :: typ + | ( atyp ) pat :: :: typ {{ com typed pattern }} | id :: :: id @@ -432,11 +427,11 @@ exp :: 'E_' ::= | ( atyp ) exp :: :: cast {{ com cast }} + + | id exp :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} {{ com No extra parens needed when exp is a tuple }} | id ( exp1 , .. , expn ) :: :: app {{ com function application }} % Note: fully applied function application only -% We might restrict exp to be an identifier -% We might require expn to have outermost parentheses (but not two sets if it's a tuple) | exp1 id exp2 :: :: app_infix {{ com infix function application }} @@ -532,6 +527,8 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} % {{ aux _ annot }} {{ auxparam 'a }} | id :: :: id {{ com identifier }} + | id ( exp1 , .. , expn ) :: :: mem + | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} | lexp [ exp ] :: :: vector {{ com vector element }} | lexp [ exp1 : exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too @@ -641,12 +638,12 @@ rec_opt :: 'Rec_' ::= | :: :: nonrec {{ com non-recursive }} | rec :: :: rec {{ com recursive }} -effects_opt :: 'Effects_opt_' ::= +effect_opt :: 'Effect_opt_' ::= {{ com Optional effect annotation for functions }} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} | :: :: pure {{ com sugar for empty effect set }} - | atyp :: :: effects + | effectkw atyp :: :: effect funcl :: 'FCL_' ::= {{ com Function clause }} @@ -659,7 +656,7 @@ fundef :: 'FD_' ::= {{ com Function definition}} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} - | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }} + | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }} % {{ com function definition }} % TODO note that the typ in the tannot_opt is the *result* type, not % the type of the whole function. The argument type comes from the @@ -690,7 +687,7 @@ default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} - | default base_kind var :: :: kind + | default base_kind kid :: :: kind | 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 @@ -699,6 +696,22 @@ default_typing_spec :: 'DT_' ::= % Otherwise we try to infer. Perhaps warn if there are multiple matches. % For example, we might often have default Type ['alphanum] +scattered_def :: 'SD_' ::= + {{ com Function and type union definitions that can be spread across + a file. Each one must end in $[[end id]]$ }} + {{ aux _ l }} + | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} + + | function clause funcl :: :: scattered_funcl +{{ com scattered function definition clause }} + + | scattered typedef id name_scm_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} + + | union id member type_union :: :: scattered_unioncl {{ com scattered union definition member }} + | end id :: :: scattered_end +{{ com scattered definition end }} + + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -717,20 +730,11 @@ def :: 'DEF_' ::= {{ com top-level type constraint }} | default_typing_spec :: :: default {{ com default kind and type assumptions }} + | scattered_def :: :: scattered + {{ com scattered definition }} | register atyp id :: :: reg_dec {{ com register declaration }} - | scattered function rec_opt tannot_opt effects_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} - - | function clause funcl :: :: scattered_funcl -{{ com scattered function definition clause }} - - | scattered typedef id naming_scheme_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} - - | union id member atyp id' :: :: scattered_unioncl {{ com scattered union definition member }} - | end id :: :: scattered_end -{{ com scattered definition end }} - defs :: '' ::= {{ com Definition sequence }} % {{ auxparam 'a }} @@ -1193,6 +1197,8 @@ terminals :: '' ::= {{ tex \mbox{--} }} | empty :: :: empty {{ tex \ensuremath{\epsilon} }} + | effectkw :: :: effectkw + {{ tex \ottkw{effect} }} formula :: formula_ ::= diff --git a/language/l2_rules.ott b/language/l2_rules.ott index fd546b0c..8287f77a 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -19,7 +19,7 @@ k :: 'Ki_' ::= t , u :: 'T_' ::= {{ phantom }} {{ com Internal types }} | id :: :: id - | var :: :: var + | 'id :: :: var | t1 -> t2 effects tag S_N :: :: fn {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }} | ( t1 * .... * tn ) :: :: tup | id t_args :: :: app @@ -36,7 +36,7 @@ tag :: 'Tag_' ::= {{ phantom }} ne :: 'Ne_' ::= {{ com internal numeric expressions }} - | id :: :: var + | 'id :: :: var | num :: :: const | ne1 * ne2 :: :: mult | ne1 + ... + nen :: :: add @@ -189,7 +189,7 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} tid :: 'tid_' ::= {{ com A type identifier or type variable }} | id :: :: id - | var :: :: var + | 'id :: :: var E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::= {{ phantom }} {{ hol (tid-> k) }} @@ -541,11 +541,11 @@ by E_k |- kind ~> k ----------------------------------------------------------- :: kind -<E_k,E_r,E_e> |- kind var ~> {var |-> k}, {} +<E_k,E_r,E_e> |- kind 'id ~> {'id |-> k}, {} -E_k(var) gives k +E_k('id) gives k ----------------------------------------------------------- :: nokind -<E_k,E_r,E_e> |- var ~> {var |-> k},{} +<E_k,E_r,E_e> |- 'id ~> {'id |-> k},{} |- nexp1 ~> ne1 |- nexp2 ~> ne2 @@ -585,9 +585,9 @@ E_d |- typ ~> t :: :: convert_typ :: convert_typ_ {{ com Convert source types to internal types }} by -E_k(var) gives K_Typ +E_k('id) gives K_Typ ------------------------------------------------------------ :: var -<E_k,E_r,E_e> |- :Typ_var: var ~> var +<E_k,E_r,E_e> |- :Typ_var: 'id ~> 'id E_k(id) gives K_Typ ------------------------------------------------------------ :: id @@ -623,7 +623,7 @@ defn by ------------------------------------------------------------ :: var -|- id ~> id +|- 'id ~> 'id ------------------------------------------------------------ :: num |- num ~> num @@ -1001,7 +1001,7 @@ E |- exp1 : enum ne1 ne2 order gives I1,E_t E |- exp2 : enum ne3 ne4 order gives I2,E_t E |- lexp : vector ne5 ne6 order t gives I3,E_t ---------------------------------------------------------- :: wslice -E |- lexp [exp1 : exp2] : vector :Ne_var: id1 :Ne_var: id2 order t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6, id1 <= ne1, id2 <= ne2+ne3+ne4},pure> ,E_t +E |- lexp [exp1 : exp2] : vector :Ne_var: 'id1 :Ne_var: 'id2 order t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6, 'id1 <= ne1, 'id2 <= ne2+ne3+ne4},pure> ,E_t E |- exp1 : enum ne1 ne2 order gives I1,E_t E |- exp2 : enum ne3 ne4 order gives I2,E_t |