diff options
| -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 | ||||
| -rw-r--r-- | src/initial_check.ml | 213 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 83 | ||||
| -rw-r--r-- | src/lexer.mll | 11 | ||||
| -rw-r--r-- | src/parser.mly | 158 | ||||
| -rw-r--r-- | src/pretty_print.ml | 104 | ||||
| -rw-r--r-- | src/test/test1.sail | 4 | ||||
| -rw-r--r-- | src/test/test3.sail | 4 | ||||
| -rw-r--r-- | src/type_internal.ml | 2 | ||||
| -rw-r--r-- | src/type_internal.mli | 2 |
15 files changed, 673 insertions, 743 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 diff --git a/src/initial_check.ml b/src/initial_check.ml index 18a853d9..ef80efcc 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -10,14 +10,14 @@ type 'a envs_out = 'a * envs let id_to_string (Id_aux(id,l)) = match id with | Id(x) | DeIid(x) -> x -let var_to_string (Var_aux(Var v,l)) = v +let var_to_string (Kid_aux(Var v,l)) = v (*placeholder, write in type_internal*) let kind_to_string kind = match kind.k with | K_Nat -> "Nat" | K_Typ -> "Type" | K_Ord -> "Order" - | K_Efct -> "Effects" + | K_Efct -> "Effect" | _ -> " kind pp place holder " let typquant_to_quantkinds k_env typquant = @@ -57,14 +57,14 @@ let to_ast_id (Parse_ast.Id_aux(id,l)) = | Parse_ast.Id(x) -> Id(x) | Parse_ast.DeIid(x) -> DeIid(x)) , l) -let to_ast_var (Parse_ast.Var_aux(Parse_ast.Var v,l)) = Var_aux(Var v,l) +let to_ast_var (Parse_ast.Kid_aux(Parse_ast.Var v,l)) = Kid_aux(Var v,l) let to_ast_base_kind (Parse_ast.BK_aux(k,l')) = match k with | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ} | Parse_ast.BK_nat -> BK_aux(BK_nat,l'), { k = K_Nat } | Parse_ast.BK_order -> BK_aux(BK_order,l'), { k = K_Ord } - | Parse_ast.BK_effects -> BK_aux(BK_effects,l'), { k = K_Efct } + | Parse_ast.BK_effect -> BK_aux(BK_effect,l'), { k = K_Efct } let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),l)) : (Ast.kind * kind) = match klst with @@ -100,7 +100,6 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ = | K_infer -> k.k <- K_Typ; Typ_var v | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k)) | None -> typ_error l "Encountered an unbound variable" None (Some v) None) - | Parse_ast.ATyp_wild -> Typ_wild | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env arg), (to_ast_typ k_env ret), (to_ast_effects k_env efct)) @@ -123,15 +122,6 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = match n with | Parse_ast.ATyp_aux(t,l) -> (match t with - | Parse_ast.ATyp_id(id) -> - let id = to_ast_id id in - let mk = Envmap.apply k_env (id_to_string id) in - (match mk with - | Some(k) -> Nexp_aux((match k.k with - | K_Nat -> Nexp_id id - | K_infer -> k.k <- K_Nat; Nexp_id id - | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) None (Some k)),l) - | None -> typ_error l "Encountered an unbound variable" (Some id) None None) | Parse_ast.ATyp_var(v) -> let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in @@ -163,15 +153,6 @@ and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order = match o with | Parse_ast.ATyp_aux(t,l) -> Ord_aux( (match t with - | Parse_ast.ATyp_id(id) -> - let id = to_ast_id id in - let mk = Envmap.apply k_env (id_to_string id) in - (match mk with - | Some(k) -> (match k.k with - | K_Ord -> Ord_id id - | K_infer -> k.k <- K_Ord; Ord_id id - | _ -> typ_error l "Required an identifier with kind Order, encountered " (Some id) None (Some k)) - | None -> typ_error l "Encountered an unbound identifier" (Some id) None None) | Parse_ast.ATyp_var(v) -> let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in @@ -186,40 +167,31 @@ and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order = | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None None ), l) -and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects = +and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect = match e with | Parse_ast.ATyp_aux(t,l) -> - Effects_aux( (match t with - | Parse_ast.ATyp_efid(id) -> - let id = to_ast_id id in - let mk = Envmap.apply k_env (id_to_string id) in - (match mk with - | Some(k) -> (match k.k with - | K_Efct -> Effects_id id - | K_infer -> k.k <- K_Efct; Effects_id id - | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) None (Some k)) - | None -> typ_error l "Encountered an unbound variable" (Some id) None None) - | Parse_ast.ATyp_efvar(v) -> + Effect_aux( (match t with + | Parse_ast.ATyp_var(v) -> let v = to_ast_var v in let mk = Envmap.apply k_env (var_to_string v) in (match mk with | Some(k) -> (match k.k with - | K_Efct -> Effects_var v - | K_infer -> k.k <- K_Efct; Effects_var v + | K_Efct -> Effect_var v + | K_infer -> k.k <- K_Efct; Effect_var v | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k)) | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_set(effects) -> - Effects_set( List.map + Effect_set( List.map (fun efct -> match efct with - | Parse_ast.Effect_aux(e,l) -> - Effect_aux((match e with - | Parse_ast.Effect_rreg -> Effect_rreg - | Parse_ast.Effect_wreg -> Effect_wreg - | Parse_ast.Effect_rmem -> Effect_rmem - | Parse_ast.Effect_wmem -> Effect_wmem - | Parse_ast.Effect_undef -> Effect_undef - | Parse_ast.Effect_unspec -> Effect_unspec - | Parse_ast.Effect_nondet -> Effect_nondet),l)) + | Parse_ast.BE_aux(e,l) -> + BE_aux((match e with + | Parse_ast.BE_rreg -> BE_rreg + | Parse_ast.BE_wreg -> BE_wreg + | Parse_ast.BE_rmem -> BE_rmem + | Parse_ast.BE_wmem -> BE_wmem + | Parse_ast.BE_undef -> BE_undef + | Parse_ast.BE_unspec -> BE_unspec + | Parse_ast.BE_nondet -> BE_nondet),l)) effects) | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None ), l) @@ -231,11 +203,11 @@ and to_ast_typ_arg (k_env : kind Envmap.t) (kind : kind) (arg : Parse_ast.atyp) | K_Typ -> Typ_arg_typ (to_ast_typ k_env arg) | K_Nat -> Typ_arg_nexp (to_ast_nexp k_env arg) | K_Ord -> Typ_arg_order (to_ast_order k_env arg) - | K_Efct -> Typ_arg_effects (to_ast_effects k_env arg) + | K_Efct -> Typ_arg_effect (to_ast_effects k_env arg) | _ -> raise (Reporting_basic.err_unreachable l "To_ast_typ_arg received Lam kind or infer kind")), l) -let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constraint) : nexp_constraint = +let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.n_constraint) : n_constraint = match c with | Parse_ast.NC_aux(nc,l) -> NC_aux( (match nc with @@ -252,7 +224,7 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constrain let n2 = to_ast_nexp k_env t2 in NC_bounded_le(n1,n2) | Parse_ast.NC_nat_set_bounded(id,bounds) -> - NC_nat_set_bounded(to_ast_id id, bounds) + NC_nat_set_bounded(to_ast_var id, bounds) ), l) (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) @@ -398,9 +370,9 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) LEXP_aux( (match exp with | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id) - | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) -> + | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),args) -> (match f with - | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',to_ast_exp k_env exp) + | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',List.map (to_ast_exp k_env) args) | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp) | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2) @@ -442,7 +414,7 @@ and to_ast_record_try (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_as | _ -> None,Some(l, "Expected a field assignment to be identifier = expression") -let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_typing_spec) envs_out = +let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spec) : (tannot default_spec) envs_out = match default with | Parse_ast.DT_aux(df,l) -> (match df with @@ -486,6 +458,11 @@ let rec to_ast_range (Parse_ast.BF_aux(r,l)) = (* TODO add check that ranges are | Parse_ast.BF_concat(ir1,ir2) -> BF_concat( to_ast_range ir1, to_ast_range ir2)), l) +let to_ast_type_union k_env (Parse_ast.Tu_aux(tu,l)) = + match tu with + | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l)) + | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) + let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_def) envs_out = match td with | Parse_ast.TD_aux(td,l) -> @@ -516,11 +493,7 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de let id = to_ast_id id in let key = id_to_string id in let typq,k_env,_ = to_ast_typquant k_env typq in - let arms = List.map (fun (Parse_ast.Tu_aux(tu,l)) -> - match tu with - | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l)) - | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) ) - arms in (* Add check that all arms have unique names *) + let arms = List.map (to_ast_type_union k_env) arms in (* Add check that all arms have unique names *) let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in let typ = (match (typquant_to_quantkinds k_env typq) with | [ ] -> {k = K_Typ} @@ -555,10 +528,10 @@ let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l) let typq,k_env,k_local = to_ast_typquant k_env tq in Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env,k_local -let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effects_opt_aux(e,l)) : tannot effects_opt = +let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : tannot effect_opt = match e with - | Parse_ast.Effects_opt_pure -> Effects_opt_aux(Effects_opt_pure,(l,None)) - | Parse_ast.Effects_opt_effects(typ) -> Effects_opt_aux(Effects_opt_effects(to_ast_effects k_env typ),(l,None)) + | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,(l,None)) + | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),(l,None)) let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) = match fcl with @@ -609,65 +582,65 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * let t = to_ast_typ k_env typ in let id = to_ast_id id in ((Finished(DEF_aux(DEF_reg_dec(t,id),(l,None)))),envs),partial_defs (*If tracking types here, update tenv and None*) - | Parse_ast.DEF_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> - let rec_opt = to_ast_rec rec_opt in - let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in - let effects_opt = to_ast_effects_opt k_env' effects_opt in - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in - (No_def,envs),((id,(partial_def,k_local))::partial_defs) - | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None) - | Parse_ast.DEF_scattered_funcl(funcl) -> - (match funcl with - | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None - | Some(d,k) -> - (match !d with - | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> - let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in - d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false); - (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None - | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None))) - | Parse_ast.DEF_scattered_variant(id,naming_scheme_opt,typquant) -> - let id = to_ast_id id in - let name = to_ast_namescm naming_scheme_opt in - let typq, k_env',_ = to_ast_typquant k_env typquant in - (match (def_in_progress id partial_defs) with - | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in - (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs - | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None) - | Parse_ast.DEF_scattered_unioncl(id,typ,arm_id) -> - let id = to_ast_id id in - let arm_id = to_ast_id arm_id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None - | Some(d,k) -> - (match !d with - | (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> - let typ = to_ast_typ k typ in - d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[Tu_aux(Tu_ty_id (typ,arm_id), l)],false),tl)),dl),false); - (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None - | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None)) - | Parse_ast.DEF_scattered_end(id) -> - let id = to_ast_id id in - (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None - | Some(d,k) -> - (match !d with - | (DEF_aux(DEF_type(_),_) as def),false -> - d:= (def,true); - (No_def,envs),partial_defs - | (DEF_aux(DEF_fundef(_),_) as def),false -> - d:= (def,true); - ((Finished def), envs),partial_defs - | _, true -> - typ_error l "Scattered definition ended multiple times" (Some id) None None - | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))) + | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,_)) -> + (match sd with + | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) -> + let rec_opt = to_ast_rec rec_opt in + let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in + let effects_opt = to_ast_effects_opt k_env' effects_opt in + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in + (No_def,envs),((id,(partial_def,k_local))::partial_defs) + | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None) + | Parse_ast.SD_scattered_funcl(funcl) -> + (match funcl with + | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None + | Some(d,k) -> + (match !d with + | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> + let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in + d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false); + (No_def,envs),partial_defs + | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None + | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None))) + | Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> + let id = to_ast_id id in + let name = to_ast_namescm naming_scheme_opt in + let typq, k_env',_ = to_ast_typquant k_env typquant in + (match (def_in_progress id partial_defs) with + | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in + (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs + | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None) + | Parse_ast.SD_scattered_unioncl(id,tu) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None + | Some(d,k) -> + (match !d with + | (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> + d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),dl),false); + (No_def,envs),partial_defs + | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None + | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None)) + | Parse_ast.SD_scattered_end(id) -> + let id = to_ast_id id in + (match (def_in_progress id partial_defs) with + | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None + | Some(d,k) -> + (match !d with + | (DEF_aux(DEF_type(_),_) as def),false -> + d:= (def,true); + (No_def,envs),partial_defs + | (DEF_aux(DEF_fundef(_),_) as def),false -> + d:= (def,true); + ((Finished def), envs),partial_defs + | _, true -> + typ_error l "Scattered definition ended multiple times" (Some id) None None + | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))) ) let rec to_ast_defs_helper envs partial_defs = function diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 640f6b1d..c0fec8a1 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -80,14 +80,14 @@ and to_reg_ranges base_id base_reg ranges = | (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges) end -val has_memory_effect : list efct -> bool +val has_memory_effect : list base_effect -> bool let rec has_memory_effect efcts = match efcts with | [] -> false | e::efcts -> match e with - | Effect_wreg -> true - | Effect_wmem -> true + | BE_wreg -> true + | BE_wmem -> true | _ -> has_memory_effect efcts end end @@ -101,7 +101,7 @@ let rec to_memory_ops (Defs defs) = match def with | DEF_spec valsp -> match valsp with - | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effects_set eff)) as t)) id -> + | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id -> if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs)) | _ -> to_memory_ops (Defs defs) end | _ -> to_memory_ops (Defs defs) end @@ -633,44 +633,35 @@ and interp_main t_level l_env l_mem exp = (fun vals -> V_vector (List_extra.head indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps | E_block(exps) -> interp_block t_level l_env l_env l_mem exps | E_app f args -> - match (f,t_level) with - | (id,(defs,externs,regs,mems,ctors)) -> - (match find_function defs id with - | Just(funcls) -> - resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args)) - (fun argv lm le -> - (match find_funcl funcls argv with - | Nothing -> - let name = match id with Id s -> s | DeIid s -> s end in - (Error ("No matching pattern for function " (* XXX ^ name *)),lm,l_env) - | Just(env,exp) -> - resolve_outcome (interp_main t_level env lm exp) - (fun ret lm le -> (Value ret, lm,l_env)) - (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env lm stack))) - end)) - (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a])))) - | Nothing -> - (match in_ctors ctors id with - | Just(typ) -> - resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args)) - (fun argv lm le -> (Value (V_ctor id argv), lm, le)) - (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a])))) + (match (exp_list t_level (fun es -> E_app f es) V_tuple l_env l_mem [] args) with + | (Value v,lm,le) -> + (match (f,t_level) with + | (id,(defs,externs,regs,mems,ctors)) -> + (match find_function defs id with + | Just(funcls) -> + (match find_funcl funcls v with + | Nothing -> + let name = match id with Id s -> s | DeIid s -> s end in + (Error ("No matching pattern for function " (* XXX ^ name *)),l_mem,l_env) + | Just(env,exp) -> + resolve_outcome (interp_main t_level env l_mem exp) + (fun ret lm le -> (Value ret, lm,l_env)) + (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack))) + end) | Nothing -> - (match find_memory mems id with - | Just(typ) -> - resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args)) - (fun argv lm le -> (Action (Read_mem id argv Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)) - (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a])))) + (match in_ctors ctors id with + | Just(typ) -> (Value (V_ctor id v), lm, le) | Nothing -> - (match find_extern externs id with - | Just(str) -> - resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args)) - (fun argv lm le -> (Action (Call_extern str argv) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)) - (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a])))) - | Nothing -> (Error "Unknown function call",l_mem,l_env) end) - end) end) end) - | _ -> (Error "Application with expression other than identifier",l_mem,l_env) - end + (match find_memory mems id with + | Just(typ) -> + (Action (Read_mem id v Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le) + | Nothing -> + (match find_extern externs id with + | Just(str) -> + (Action (Call_extern str v) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le) + | Nothing -> (Error "Unknown function call",lm,le) end) + end) end) end) end) + | out -> out end) | E_app_infix l op r -> let op = match op with | Id x -> DeIid x @@ -751,12 +742,12 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp = else ((Error "Undefined id",l_mem,l_env),Nothing) end end - | LEXP_memory id exp -> - match (interp_main t_level l_env l_mem exp) with - | (Value t,lm,le) -> - let request = (Action (Write_mem id t Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in - if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (to_exp t)))) - | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_memory id e))) + | LEXP_memory id exps -> + match (exp_list t_level E_tuple V_tuple l_env l_mem [] exps) with + | (Value (V_tuple vs),lm,le) -> + let request = (Action (Write_mem id (V_tuple vs) Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in + if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (List.map to_exp vs)))) + | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_tuple es) -> (LEXP_memory id es))) | e -> (e,Nothing) end | LEXP_vector lexp exp -> match (interp_main t_level l_env l_mem exp) with diff --git a/src/lexer.mll b/src/lexer.mll index 80fd06f4..620ca7a5 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -68,7 +68,7 @@ let kw_table = ("default", (fun _ -> Default)); ("deinfix", (fun _ -> Deinfix)); ("effect", (fun _ -> Effect)); - ("Effects", (fun _ -> Effects)); + ("Effect", (fun _ -> EFFECT)); ("end", (fun _ -> End)); ("enumerate", (fun _ -> Enumerate)); ("else", (fun _ -> Else)); @@ -106,6 +106,15 @@ let kw_table = ("OR", (fun x -> OR)); ("quot", (fun x -> Quot)); ("rem", (fun x -> Rem)); + + ("rreg", (fun x -> Rreg)); + ("wreg", (fun x -> Wreg)); + ("rmem", (fun x -> Rmem)); + ("wmem", (fun x -> Wmem)); + ("undef", (fun x -> Undef)); + ("unspec", (fun x -> Unspec)); + ("nondet", (fun x -> Nondet)); + ] let type_names : string list ref = ref [] diff --git a/src/parser.mly b/src/parser.mly index 4050885f..6ef0a91e 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -55,6 +55,8 @@ let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n) let idl i = Id_aux(i, loc()) +let efl e = BE_aux(e, loc()) + let ploc p = P_aux(p,loc ()) let eloc e = E_aux(e,loc ()) let peloc pe = Pat_aux(pe,loc ()) @@ -76,6 +78,7 @@ let defloc df = DT_aux(df, loc()) let tdloc td = TD_aux(td, loc()) let funloc fn = FD_aux(fn, loc()) let vloc v = VS_aux(v, loc ()) +let sdloc sd = SD_aux(sd, loc ()) let dloc d = DEF_aux(d,loc ()) let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e)) @@ -84,8 +87,8 @@ let mk_recn _ = (Rec_aux((Rec_nonrec), Unknown)) let mk_typqn _ = (TypQ_aux(TypQ_no_forall,Unknown)) let mk_tannot tq t s e = Typ_annot_opt_aux(Typ_annot_opt_some(tq,t),(locn s e)) let mk_tannotn _ = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown) -let mk_eannot e i = Effects_opt_aux((Effects_opt_effects(e)),(locn i i)) -let mk_eannotn _ = Effects_opt_aux(Effects_opt_pure,Unknown) +let mk_eannot e i = Effect_opt_aux((Effect_opt_effect(e)),(locn i i)) +let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown) let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown) let make_enum_sugar_bounded typ1 typ2 = @@ -120,8 +123,9 @@ let star = "*" /*Terminals with no content*/ -%token And As Bits By Case Clause Const Dec Default Deinfix Effect Effects End Enumerate Else Extern +%token And As Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End Enumerate Else Extern %token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register +%token Rreg Wreg Rmem Wmem Undef Unspec Nondet %token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val /* Avoid shift/reduce conflict - see right_atomic_exp rule */ @@ -246,7 +250,7 @@ tid: tyvar: | TyVar - { (Var_aux((Var($1)),loc ())) } + { (Kid_aux((Var($1)),loc ())) } atomic_kind: | TYPE @@ -255,8 +259,8 @@ atomic_kind: { bkloc BK_nat } | Order { bkloc BK_order } - | Effects - { bkloc BK_effects } + | EFFECT + { bkloc BK_effect } kind_help: | atomic_kind @@ -269,20 +273,20 @@ kind: { K_aux(K_kind($1), loc ()) } effect: - | id - { (match $1 with - | Id_aux(Id(s),l) -> - Effect_aux - ((match s with - | "rreg" -> (Effect_rreg) - | "wreg" -> (Effect_wreg) - | "rmem" -> (Effect_rmem) - | "wmem" -> (Effect_wmem) - | "undef" -> (Effect_undef) - | "unspec" -> (Effect_unspec) - | "nondet" -> (Effect_nondet) - | _ -> raise (Parse_error_locn (l,"Invalid effect"))),l) - | _ -> raise (Parse_error_locn ((loc ()),"Invalid effect"))) } + | Rreg + { efl BE_rreg } + | Wreg + { efl BE_wreg } + | Rmem + { efl BE_rmem } + | Wmem + { efl BE_wmem } + | Undef + { efl BE_undef } + | Unspec + { efl BE_unspec } + | Nondet + { efl BE_nondet } effect_list: | effect @@ -291,10 +295,8 @@ effect_list: { $1::$3 } effect_typ: - | Effect tid - { tloc (ATyp_efid($2)) } - | Effect Lcurly effect_list Rcurly - { tloc (ATyp_set($3)) } + | Lcurly effect_list Rcurly + { tloc (ATyp_set($2)) } | Pure { tloc (ATyp_set([])) } @@ -329,14 +331,10 @@ vec_typ: { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) } app_typs: - | vec_typ + | nexp_typ { [$1] } - | Num - { [tloc (ATyp_constant $1)] } - | Num app_typs - { (ATyp_aux((ATyp_constant $1),locn 1 1))::$2 } - | vec_typ app_typs - { $1::$2 } + | nexp_typ Comma app_typs + { $1::$3 } app_typ: | vec_typ @@ -376,8 +374,8 @@ nexp_typ: typ: | star_typ { $1 } - | star_typ MinusGt typ effect_typ - { tloc (ATyp_fn($1,$3,$4)) } + | star_typ MinusGt typ Effect effect_typ + { tloc (ATyp_fn($1,$3,$5)) } lit: | True @@ -852,33 +850,29 @@ funcl_ands: /* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/ fun_def: - | Function_ Rec typquant typ effect_typ funcl_ands - { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) } + | Function_ Rec typquant typ Effect effect_typ funcl_ands + { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) } | Function_ Rec typquant typ funcl_ands { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } - | Function_ Rec typ effect_typ funcl_ands - { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) } + | Function_ Rec typ Effect effect_typ funcl_ands + { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) } + | Function_ Rec Effect effect_typ funcl_ands + { funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $4 4, $5)) } | Function_ Rec typ funcl_ands - { match $3 with - | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> - funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $3 3, $4)) - | _ -> - funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } -/* | Function_ Rec funcl_ands + { funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } + | Function_ Rec funcl_ands { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) } -*/ | Function_ typquant atomic_typ effect_typ funcl_ands + | Function_ typquant atomic_typ effect_typ funcl_ands { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) } | Function_ typquant typ funcl_ands { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) } + | Function_ Effect effect_typ funcl_ands + { funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $3 3, $4)) } | Function_ typ funcl_ands - { match $2 with - | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> - funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $2 2, $3)) - | _ -> - funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) } -/* | Function_ funcl_ands + { funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) } + | Function_ funcl_ands { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) } -*/ + val_spec: | Val typquant typ id @@ -919,7 +913,7 @@ nexp_constraint: { NC_aux(NC_bounded_ge($1,$3), loc () ) } | typ LtEq typ { NC_aux(NC_bounded_le($1,$3), loc () ) } - | id IN Lcurly nums Rcurly + | tyvar IN Lcurly nums Rcurly { NC_aux(NC_nat_set_bounded($1,$4), loc ()) } id_constraint: @@ -1041,42 +1035,38 @@ default_typ: { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) } scattered_def: - | Function_ Rec typquant typ effect_typ id - { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) } - | Function_ Rec typ effect_typ id - { (DEF_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) } + | Function_ Rec typquant typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) } + | Function_ Rec typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) } | Function_ Rec typquant typ id - { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } + { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } + | Function_ Rec Effect effect_typ id + { sdloc (SD_scattered_function (mk_rec 2, mk_tannotn (), mk_eannot $4 4, $5)) } | Function_ Rec typ id - { match $3 with - | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> - (DEF_scattered_function(mk_rec 2, mk_tannotn (), mk_eannot $3 3, $4)) - | _ -> - (DEF_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } + { sdloc (SD_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } | Function_ Rec id - { (DEF_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) } - | Function_ typquant typ effect_typ id - { (DEF_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) } - | Function_ typ effect_typ id - { (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) } + { sdloc (SD_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) } + | Function_ typquant typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) } + | Function_ typ Effect effect_typ id + { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) } | Function_ typquant typ id - { (DEF_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) } + { sdloc (SD_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) } + | Function_ Effect effect_typ id + { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $3 3, $4)) } | Function_ typ id - { match $2 with - | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> - (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $2 2, $3)) - | _ -> - (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) } + { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) } | Function_ id - { (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) } + { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) } | Typedef id name_sect Eq Const Union typquant - { (DEF_scattered_variant($2,$3,$7)) } + { sdloc (SD_scattered_variant($2,$3,$7)) } | Typedef id Eq Const Union typquant - { (DEF_scattered_variant($2,(mk_namesectn ()),$6)) } + { sdloc (SD_scattered_variant($2,(mk_namesectn ()),$6)) } | Typedef id name_sect Eq Const Union - { (DEF_scattered_variant($2,$3,mk_typqn ())) } + { sdloc (SD_scattered_variant($2,$3,mk_typqn ())) } | Typedef id Eq Const Union - { (DEF_scattered_variant($2,mk_namesectn (),mk_typqn ())) } + { sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) } def: | type_def @@ -1092,13 +1082,15 @@ def: | Register atomic_typ id { dloc (DEF_reg_dec($2,$3)) } | Scattered scattered_def - { dloc $2 } + { dloc (DEF_scattered $2) } | Function_ Clause funcl - { dloc (DEF_scattered_funcl($3)) } - | Union id Member atomic_typ id - { dloc (DEF_scattered_unioncl($2,$4,$5)) } + { dloc (DEF_scattered (sdloc (SD_scattered_funcl($3)))) } + | Union id Member typ id + { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_ty_id($4,$5), locn 4 5))))) } + | Union id Member id + { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_id($4), locn 4 4))))) } | End id - { dloc (DEF_scattered_end($2)) } + { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) } defs_help: | def diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 083bd087..a32db3b1 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -3,11 +3,11 @@ open Format let is_atomic_typ (Typ_aux(t,_)) = match t with - | Typ_var _ | Typ_tup _ -> true + | Typ_id _ | Typ_var _ | Typ_tup _ -> true | _ -> false let is_atomic_nexp (Nexp_aux(n,_)) = match n with - | Nexp_id _ | Nexp_constant _ | Nexp_exp _ -> true + | Nexp_var _ | Nexp_constant _ | Nexp_exp _ -> true | _ -> false let is_atomic_pat (P_aux(p,l)) = @@ -54,7 +54,7 @@ let pp_format_id (Id_aux(i,_)) = let pp_id ppf id = base ppf (pp_format_id id) -let pp_format_var (Var_aux(Var v,_)) = "'" ^ v +let pp_format_var (Kid_aux(Var v,_)) = "'" ^ v let pp_var ppf var = base ppf (pp_format_var var) @@ -63,7 +63,7 @@ let pp_format_bkind (BK_aux(k,_)) = | BK_type -> "Type" | BK_nat -> "Nat" | BK_order -> "Order" - | BK_effects -> "Effects" + | BK_effect -> "Effect" let pp_bkind ppf bk = base ppf (pp_format_bkind bk) @@ -78,13 +78,12 @@ let rec pp_format_typ (Typ_aux(t,_)) = | Typ_var(var) -> pp_format_var var | Typ_wild -> "_" | Typ_fn(arg,ret,efct) -> "(" ^ (parens is_atomic_typ pp_format_typ arg) ^ " -> " ^ - (parens is_atomic_typ pp_format_typ ret) ^ " " ^ + (parens is_atomic_typ pp_format_typ ret) ^ " effect " ^ (pp_format_effects efct) ^ ")" | Typ_tup(typs) -> "(" ^ (list_format " * " pp_format_typ typs) ^ ")" - | Typ_app(id,args) -> "(" ^ (pp_format_id id) ^ " " ^ (list_format " " pp_format_typ_arg args) ^ ")" + | Typ_app(id,args) -> "(" ^ (pp_format_id id) ^ "<" ^ (list_format ", " pp_format_typ_arg args) ^ ">)" and pp_format_nexp (Nexp_aux(n,_)) = match n with - | Nexp_id(id) -> pp_format_id id | Nexp_var(var) -> pp_format_var var | Nexp_constant(i) -> string_of_int i | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + " ^ (pp_format_nexp n2) ^ ")" @@ -92,35 +91,33 @@ and pp_format_nexp (Nexp_aux(n,_)) = | Nexp_exp(n1) -> "2** (" ^ (pp_format_nexp n1) ^ ")" and pp_format_ord (Ord_aux(o,_)) = match o with - | Ord_id(id) -> pp_format_id id | Ord_var(var) -> pp_format_var var | Ord_inc -> "inc" | Ord_dec -> "dec" -and pp_format_effects (Effects_aux(e,_)) = +and pp_format_effects (Effect_aux(e,_)) = match e with - | Effects_id(id) -> "effect " ^ pp_format_id id - | Effects_var(var) -> "effect " ^ pp_format_var var - | Effects_set(efcts) -> + | Effect_var(var) -> pp_format_var var + | Effect_set(efcts) -> if (efcts = []) then "pure" - else "effect {" ^ + else "{" ^ (list_format "," - (fun (Effect_aux(e,l)) -> + (fun (BE_aux(e,l)) -> match e with - | Effect_rreg -> "rreg" - | Effect_wreg -> "wreg" - | Effect_rmem -> "rmem" - | Effect_wmem -> "wmem" - | Effect_undef -> "undef" - | Effect_unspec -> "unspec" - | Effect_nondet -> "nondet") + | BE_rreg -> "rreg" + | BE_wreg -> "wreg" + | BE_rmem -> "rmem" + | BE_wmem -> "wmem" + | BE_undef -> "undef" + | BE_unspec -> "unspec" + | BE_nondet -> "nondet") efcts) ^ " }" and pp_format_typ_arg (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ(t) -> pp_format_typ t | Typ_arg_nexp(n) -> pp_format_nexp n | Typ_arg_order(o) -> pp_format_ord o - | Typ_arg_effects(e) -> pp_format_effects e + | Typ_arg_effect(e) -> pp_format_effects e let pp_typ ppf t = base ppf (pp_format_typ t) let pp_nexp ppf n = base ppf (pp_format_nexp n) @@ -132,8 +129,8 @@ let pp_format_nexp_constraint (NC_aux(nc,_)) = | NC_fixed(n1,n2) -> pp_format_nexp n1 ^ " = " ^ pp_format_nexp n2 | NC_bounded_ge(n1,n2) -> pp_format_nexp n1 ^ " >= " ^ pp_format_nexp n2 | NC_bounded_le(n1,n2) -> pp_format_nexp n1 ^ " <= " ^ pp_format_nexp n2 - | NC_nat_set_bounded(id,bounds) -> - pp_format_id id ^ + | NC_nat_set_bounded(var,bounds) -> + pp_format_var var ^ " In {" ^ list_format ", " string_of_int bounds ^ "}" @@ -185,7 +182,7 @@ let rec pp_format_pat (P_aux(p,l)) = | P_wild -> "_" | P_id(id) -> pp_format_id id | P_as(pat,id) -> "(" ^ pp_format_pat pat ^ " as " ^ pp_format_id id ^ ")" - | P_typ(typ,pat) -> "<" ^ pp_format_typ typ ^ "> " ^ pp_format_pat pat + | P_typ(typ,pat) -> "(" ^ pp_format_typ typ ^ ") " ^ pp_format_pat pat | P_app(id,pats) -> if (pats = []) then pp_format_id id else pp_format_id id ^ "(" ^ @@ -199,7 +196,7 @@ let rec pp_format_pat (P_aux(p,l)) = "[" ^ list_format "; " (fun (i,p) -> string_of_int i ^ " = " ^ pp_format_pat p) ipats ^ "]" | P_vector_concat(pats) -> list_format " ^ " pp_format_pat pats | P_tup(pats) -> "(" ^ (list_format ", " (parens is_atomic_pat pp_format_pat) pats) ^ ")" - | P_list(pats) -> "[|" ^ (list_format "; " (parens is_atomic_pat pp_format_pat) pats) ^ "|]" + | P_list(pats) -> "[||" ^ (list_format "; " (parens is_atomic_pat pp_format_pat) pats) ^ "||]" let pp_pat ppf p = base ppf (pp_format_pat p) let pp_pat_atomic ppf p = base ppf (parens is_atomic_pat pp_format_pat p) @@ -218,8 +215,8 @@ and pp_exp ppf (E_aux(e,_)) = kwd "}" | E_id(id) -> pp_id ppf id | E_lit(lit) -> pp_lit ppf lit - | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "<" pp_typ typ kwd ">" pp_exp exp - | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_id f (list_pp pp_exp pp_exp) args + | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp + | E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_exp pp_exp) args | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")" | E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e @@ -260,7 +257,7 @@ and pp_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = and pp_lexp ppf (LEXP_aux(lexp,_)) = match lexp with | LEXP_id(id) -> pp_id ppf id - | LEXP_memory(id,exp) -> fprintf ppf "@[%a %a@]" pp_id id pp_exp exp + | LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args | LEXP_vector(v,exp) -> fprintf ppf "@[%a %a %a %a@]" pp_lexp v kwd "[" pp_exp exp kwd "]" | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a %a %a %a %a %a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]" | LEXP_field(v,id) -> fprintf ppf "@[%a%a%a@]" pp_lexp v kwd "." pp_id id @@ -323,10 +320,10 @@ let pp_tannot_opt ppf (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> fprintf ppf "%a %a " pp_typquant tq pp_typ typ -let pp_effects_opt ppf (Effects_opt_aux(e,_)) = +let pp_effects_opt ppf (Effect_opt_aux(e,_)) = match e with - | Effects_opt_pure -> fprintf ppf "" - | Effects_opt_effects e -> pp_effects ppf e + | Effect_opt_pure -> fprintf ppf "effect pure" + | Effect_opt_effect e -> fprintf ppf "effect %a" pp_effects e let pp_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = fprintf ppf "@[<0>%a %a %a @[<1>%a@] @]@\n" pp_id id pp_pat_atomic pat kwd "=" pp_exp exp @@ -361,7 +358,7 @@ let pp_format_id_lem (Id_aux(i,_)) = let pp_lem_id ppf id = base ppf (pp_format_id_lem id) -let pp_format_var_lem (Var_aux(Var v,_)) = "(Var \"" ^ v ^ "\")" +let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")" let pp_lem_var ppf var = base ppf (pp_format_var_lem var) @@ -370,7 +367,7 @@ let pp_format_bkind_lem (BK_aux(k,_)) = | BK_type -> "BK_type" | BK_nat -> "BK_nat" | BK_order -> "BK_order" - | BK_effects -> "BK_effects" + | BK_effect -> "BK_effect" let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk) @@ -391,7 +388,6 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) = | Typ_wild -> "Typ_wild" and pp_format_nexp_lem (Nexp_aux(n,_)) = match n with - | Nexp_id(id) -> "(Nexp_id " ^ pp_format_id_lem id ^ ")" | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")" | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" @@ -399,33 +395,31 @@ and pp_format_nexp_lem (Nexp_aux(n,_)) = | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")" and pp_format_ord_lem (Ord_aux(o,_)) = match o with - | Ord_id(id) -> "(Ord_id " ^ pp_format_id_lem id ^ ")" | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")" | Ord_inc -> "Ord_inc" | Ord_dec -> "Ord_dec" -and pp_format_effects_lem (Effects_aux(e,_)) = +and pp_format_effects_lem (Effect_aux(e,_)) = match e with - | Effects_id(id) -> "(Effects_id " ^ pp_format_id id ^ ")" - | Effects_var(v) -> "(Effects_var " ^ pp_format_var v ^ ")" - | Effects_set(efcts) -> - "(Effects_set [" ^ + | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")" + | Effect_set(efcts) -> + "(Effect_set [" ^ (list_format "; " - (fun (Effect_aux(e,l)) -> + (fun (BE_aux(e,l)) -> match e with - | Effect_rreg -> "Effect_rreg" - | Effect_wreg -> "Effect_wreg" - | Effect_rmem -> "Effect_rmem" - | Effect_wmem -> "Effect_wmem" - | Effect_undef -> "Effect_undef" - | Effect_unspec -> "Effect_unspec" - | Effect_nondet -> "Effect_nondet") + | BE_rreg -> "BE_rreg" + | BE_wreg -> "BE_wreg" + | BE_rmem -> "BE_rmem" + | BE_wmem -> "BE_wmem" + | BE_undef -> "BE_undef" + | BE_unspec -> "BE_unspec" + | BE_nondet -> "BE_nondet") efcts) ^ " ])" and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")" - | Typ_arg_effects(e) -> "(Typ_arg_effects " ^ pp_format_effects_lem e ^ ")" + | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")" let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t) let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n) @@ -438,7 +432,7 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) = | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ - pp_format_id id ^ + pp_format_var_lem id ^ " [" ^ list_format "; " string_of_int bounds ^ "])" @@ -567,7 +561,7 @@ and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = and pp_lem_lexp ppf (LEXP_aux(lexp,_)) = match lexp with | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id - | LEXP_memory(id,exp) -> fprintf ppf "(%a %a %a)" kwd "LEXP_memory" pp_lem_id id pp_lem_exp exp + | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2 @@ -631,10 +625,10 @@ let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ -let pp_lem_effects_opt ppf (Effects_opt_aux(e,_)) = +let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) = match e with - | Effects_opt_pure -> fprintf ppf "Effects_opt_pure" - | Effects_opt_effects e -> fprintf ppf "(Effects_opt_effects %a)" pp_effects e + | Effect_opt_pure -> fprintf ppf "Effect_opt_pure" + | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effects %a)" pp_lem_effects e let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp diff --git a/src/test/test1.sail b/src/test/test1.sail index 128a4a99..5c29f258 100644 --- a/src/test/test1.sail +++ b/src/test/test1.sail @@ -2,8 +2,8 @@ default Nat 'i default Order 'o default bool b default forall 'a. list<'a> b -val forall 'a, 'b . ('a * 'b) -> 'b pure snd -val forall Type 'i, 'b. ('i * 'b) -> 'i pure fst +val forall 'a, 'b . ('a * 'b) -> 'b effect pure snd +val forall Type 'i, 'b. ('i * 'b) -> 'i effect pure fst typedef int_list [name = "il"] = list<nat> typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; } typedef maybe = const union forall 'a. { Nne; 'a Sme; } diff --git a/src/test/test3.sail b/src/test/test3.sail index e77e1b71..89c710bc 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -7,8 +7,8 @@ val nat -> nat effect { wmem , rmem } MEM_GPU val ( nat * nat ) -> nat effect { wmem , rmem } MEM_SIZE (* extern functions *) -val extern ( nat * nat ) -> nat pure add = "add" -val extern ( nat * nat ) -> nat pure (deinfix + ) = "add_infix" (* infix plus *) +val extern ( nat * nat ) -> nat effect pure add = "add" +val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add_infix" (* infix plus *) function nat (deinfix * ) ( (nat) x, (nat) y ) = 42 diff --git a/src/type_internal.ml b/src/type_internal.ml index dabb8100..b019624d 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -39,7 +39,7 @@ and n_uvar = { nindex : int; mutable nsubst : t option } and effect = { mutable effect : effect_aux } and effect_aux = | Evar of string - | Eset of Ast.efct_aux list + | Eset of Ast.base_effect list | Euvar of e_uvar and e_uvar = { eindex : int; mutable esubst : t option } and order = { mutable order : order_aux } diff --git a/src/type_internal.mli b/src/type_internal.mli index 99b82075..fedc5cc4 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -38,7 +38,7 @@ and nexp_aux = and effect = { mutable effect : effect_aux } and effect_aux = | Evar of string - | Eset of Ast.efct_aux list + | Eset of Ast.base_effect list | Euvar of e_uvar and order = { mutable order : order_aux } and order_aux = |