diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 72 | ||||
| -rw-r--r-- | language/l2.ml | 236 | ||||
| -rw-r--r-- | language/l2.ott | 31 | ||||
| -rw-r--r-- | language/l2_parse.ml | 108 | ||||
| -rw-r--r-- | language/l2_parse.ott | 14 |
5 files changed, 256 insertions, 205 deletions
diff --git a/language/l2.lem b/language/l2.lem index 79cb82b3..da806b57 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -22,11 +22,6 @@ val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) -type id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - type base_kind = (* base kind *) | BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) @@ -34,18 +29,28 @@ type base_kind = (* base kind *) | 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 + + type nexp = (* expression of kind $Nat$, for vector sizes and origins *) | Nexp_id of id (* identifier *) + | Nexp_var of var (* variable *) | Nexp_constant of nat (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) -type kind = (* kinds *) - | K_kind of list base_kind - - type efct = (* effect *) | Effect_rreg (* read register *) | Effect_wreg (* write register *) @@ -56,6 +61,11 @@ type efct = (* effect *) | Effect_nondet (* nondeterminism from intra-instruction parallelism *) +type kinded_id = (* optionally kind-annotated identifier *) + | KOpt_none of var (* identifier *) + | KOpt_kind of kind * var (* kind-annotated variable *) + + type nexp_constraint = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -63,22 +73,19 @@ type nexp_constraint = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of id * list nat -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - -type effects = (* effect set, of kind $Effects$ *) - | Effects_var of id - | Effects_set of list efct (* effect set *) - - type order = (* vector order specifications, of kind $Order$ *) | Ord_id of id (* identifier *) + | Ord_var of var (* 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 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 *) @@ -99,7 +106,8 @@ type lit = (* Literal constant *) type typ = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) + | 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_tup of list typ (* Tuple type *) | Typ_app of id * list typ_arg (* type constructor application *) @@ -184,15 +192,15 @@ and letbind = (* Let binding *) | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) -type funcl = (* Function clause *) - | FCL_Funcl of id * pat * exp - - type effects_opt = (* Optional effect annotation for functions *) | Effects_opt_pure (* sugar for empty effect set *) | Effects_opt_effects of effects +type funcl = (* Function clause *) + | FCL_Funcl of id * pat * exp + + type rec_opt = (* Optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) @@ -218,21 +226,21 @@ type index_range = (* index specification, for bitfields in register types *) | BF_concat of index_range * index_range (* concatenation of index ranges *) -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 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 * id + | 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 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 *) @@ -264,7 +272,7 @@ type typ_lib = (* library types and syntactic sugar for them *) | 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 (* UTF8 strings *) + | 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} *) diff --git a/language/l2.ml b/language/l2.ml index 6ecf3411..00c59136 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -20,8 +20,8 @@ base_kind_aux = (* base kind *) type -base_kind = - BK_aux of base_kind_aux * l +var_aux = (* variables with kind, ticked to differntiate from program variables *) + Var of x type @@ -31,8 +31,13 @@ id_aux = (* Identifier *) type -kind_aux = (* kinds *) - K_kind of (base_kind) list +base_kind = + BK_aux of base_kind_aux * l + + +type +var = + Var_aux of var_aux * l type @@ -41,13 +46,14 @@ id = type -kind = - K_aux of kind_aux * l +kind_aux = (* kinds *) + K_kind of (base_kind) list type nexp_aux = (* expression of kind $_$, for vector sizes and origins *) Nexp_id of id (* identifier *) + | Nexp_var of var (* variable *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) @@ -58,9 +64,8 @@ and nexp = type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) +kind = + K_aux of kind_aux * l type @@ -72,6 +77,22 @@ nexp_constraint_aux = (* constraint over kind $_$ *) type +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of var (* identifier *) + | KOpt_kind of kind * var (* kind-annotated variable *) + + +type +nexp_constraint = + NC_aux of nexp_constraint_aux * l + + +type +kinded_id = + KOpt_aux of kinded_id_aux * l + + +type efct_aux = (* effect *) Effect_rreg (* read register *) | Effect_wreg (* write register *) @@ -83,13 +104,9 @@ efct_aux = (* effect *) type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +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 *) type @@ -98,27 +115,29 @@ efct = 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 *) +quant_item = + QI_aux of quant_item_aux * l type effects_aux = (* effect set, of kind $_$ *) - Effects_var of id + Effects_id of id + | Effects_var of var | Effects_set of (efct) list (* effect set *) type order_aux = (* vector order specifications, of kind $_$ *) Ord_id of id (* identifier *) + | Ord_var of var (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) type -quant_item = - QI_aux of quant_item_aux * l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type @@ -132,12 +151,6 @@ order = type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of (quant_item) list - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - -type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) | L_zero (* $_ : _$ *) @@ -152,9 +165,15 @@ lit_aux = (* Literal constant *) type +typquant = + TypQ_aux of typquant_aux * l + + +type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) + | 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_tup of (typ) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) @@ -173,11 +192,6 @@ and typ_arg = type -typquant = - TypQ_aux of typquant_aux * l - - -type lit = L_aux of lit_aux * l @@ -218,7 +232,38 @@ typschm = type -'a letbind_aux = (* Let binding *) +'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 = + LEXP_aux of 'a lexp_aux * 'a annot + +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of id * 'a exp + +and 'a fexp = + FE_aux of 'a fexp_aux * 'a annot + +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp) list * bool + +and 'a fexps = + FES_aux of 'a fexps_aux * 'a annot + +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * 'a exp + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +and 'a letbind_aux = (* Let binding *) LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) @@ -250,42 +295,27 @@ 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 (* 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 = - LEXP_aux of 'a lexp_aux * 'a annot - -and 'a fexp_aux = (* Field-expression *) - FE_Fexp of id * 'a exp -and 'a fexp = - FE_aux of 'a fexp_aux * 'a annot +type +'a effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects -and 'a fexps_aux = (* Field-expression list *) - FES_Fexps of ('a fexp) list * bool -and 'a fexps = - FES_aux of 'a fexps_aux * 'a annot +type +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_some of typquant * typ -and 'a pexp_aux = (* Pattern match *) - Pat_exp of 'a pat * 'a exp -and 'a pexp = - Pat_aux of 'a pexp_aux * 'a annot +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type -type_union_aux = (* Type union constructors *) - Tu_id of id - | Tu_ty_id of typ * id +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -295,25 +325,29 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * 'a exp +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of typ * id type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot type -'a effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type @@ -327,40 +361,18 @@ and index_range = type -type_union = - Tu_aux of type_union_aux * l - - -type naming_scheme_opt = Name_sect_aux of naming_scheme_opt_aux * l type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot - - -type -rec_opt = - Rec_aux of rec_opt_aux * l - - -type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot - - -type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +type_union = + Tu_aux of type_union_aux * l type -'a 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 (* 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 *) +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list type @@ -373,19 +385,21 @@ type type -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * var + | DT_typ of typschm * id type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id - | DT_typ of typschm * id +'a 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 (* 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 -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type @@ -394,13 +408,13 @@ type type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type @@ -424,7 +438,7 @@ type | 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 (* UTF8 strings *) + | 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} *) diff --git a/language/l2.ott b/language/l2.ott index e28e0271..9c801336 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -129,7 +129,11 @@ id :: '' ::= % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. - +var :: '' ::= + {{ com variables with kind, ticked to differntiate from program variables }} + {{ aux _ l }} + | ' x :: :: var + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Kinds and Types % @@ -157,6 +161,7 @@ nexp :: 'Nexp_' ::= {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} {{ aux _ l }} | id :: :: id {{ com identifier }} + | var :: :: var {{ com variable }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} %{{ com must be linear after normalisation... except for the type of *, ahem }} @@ -168,6 +173,7 @@ order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} {{ aux _ l }} | id :: :: id {{ com identifier }} + | var :: :: var {{ com variable }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ ichlo [[order]] }} @@ -187,7 +193,8 @@ efct :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} - | effect id :: :: var + | effect id :: :: id + | effect var :: :: var | effect { efct1 , .. , efctn } :: :: 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 [] }} @@ -199,7 +206,9 @@ typ :: 'Typ_' ::= {{ aux _ l }} | _ :: :: wild {{ com Unspecified type }} - | id :: :: var + | id :: :: id + {{ com Defined type }} + | var :: :: var {{ com Type variable }} | typ1 -> typ2 effects :: :: fn {{ com Function type (first-order only in user code) }} @@ -226,12 +235,12 @@ 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} }} @@ -275,8 +284,8 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} - | id :: :: none {{ com identifier }} - | kind id :: :: kind {{ com kind-annotated variable }} + | var :: :: none {{ com identifier }} + | kind var :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} @@ -763,7 +772,7 @@ val_spec :: 'VS_' ::= default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ annot }} {{ auxparam 'a }} - | default base_kind id :: :: kind + | default base_kind var :: :: 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 diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 990166c4..b196f007 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -25,6 +25,17 @@ base_kind_aux = (* base kind *) type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type +var_aux = (* variables with kind, ticked to differntiate from program variables *) + Var of x + + +type efct_aux = (* effect *) Effect_rreg (* read register *) | Effect_wreg (* write register *) @@ -36,24 +47,23 @@ efct_aux = (* effect *) type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) +base_kind = + BK_aux of base_kind_aux * l type -base_kind = - BK_aux of base_kind_aux * l +id = + Id_aux of id_aux * l type -efct = - Effect_aux of efct_aux * l +var = + Var_aux of var_aux * l type -id = - Id_aux of id_aux * l +efct = + Effect_aux of efct_aux * l type @@ -64,6 +74,7 @@ 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_constant of int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) @@ -71,6 +82,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | 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_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) @@ -96,8 +108,8 @@ nexp_constraint_aux = (* constraint over kind $_$ *) type kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) + KOpt_none of var (* identifier *) + | KOpt_kind of kind * var (* kind-annotated variable *) type @@ -128,6 +140,11 @@ typquant_aux = (* type quantifiers and constraints *) type +typquant = + TypQ_aux of typquant_aux * l + + +type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) | L_zero (* $_ : _$ *) @@ -142,8 +159,8 @@ lit_aux = (* Literal constant *) type -typquant = - TypQ_aux of typquant_aux * l +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * atyp type @@ -152,8 +169,8 @@ lit = type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * atyp +typschm = + TypSchm_aux of typschm_aux * l type @@ -182,11 +199,6 @@ and fpat = type -typschm = - TypSchm_aux of typschm_aux * l - - -type exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -242,27 +254,21 @@ and letbind = type -naming_scheme_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 -tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of typquant * atyp +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string type -effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of atyp +tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of typquant * atyp type @@ -277,8 +283,14 @@ funcl_aux = (* Function clause *) type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +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 type @@ -292,8 +304,8 @@ and index_range = type -type_union = - Tu_aux of type_union_aux * l +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type @@ -302,11 +314,6 @@ tannot_opt = type -effects_opt = - Effects_opt_aux of effects_opt_aux * l - - -type rec_opt = Rec_aux of rec_opt_aux * l @@ -317,10 +324,8 @@ funcl = 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 +effects_opt = + Effects_opt_aux of effects_opt_aux * l type @@ -334,7 +339,7 @@ type_def_aux = (* Type definition body *) type default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id + DT_kind of base_kind * var | DT_typ of typschm * id @@ -344,8 +349,10 @@ fundef_aux = (* Function definition *) type -val_spec = - VS_aux of val_spec_aux * l +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 @@ -364,6 +371,11 @@ 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 *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 6876fcfa..f96c3f99 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -118,6 +118,12 @@ id :: '' ::= | x :: :: id | ( deinfix x ) :: :: deIid {{ com remove infix status }} + +var :: '' ::= + {{ com variables with kind, ticked to differntiate from program variables }} + {{ aux _ l }} + | ' x :: :: var + % Note: we have just a single namespace. We don't want the same % identifier to be reused as a type name or variable, expression % variable, and field name. We don't enforce any lexical convention @@ -162,6 +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 }} | num :: :: constant {{ com constant }} | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} @@ -171,6 +178,7 @@ 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 }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} @@ -237,8 +245,8 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} - | id :: :: none {{ com identifier }} - | kind id :: :: kind {{ com kind-annotated variable }} + | var :: :: none {{ com identifier }} + | kind var :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} @@ -682,7 +690,7 @@ default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} - | default base_kind id :: :: kind + | default base_kind var :: :: 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 |