diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.lem | 87 | ||||
| -rw-r--r-- | language/l2.ml | 118 | ||||
| -rw-r--r-- | language/l2.ott | 130 | ||||
| -rw-r--r-- | language/l2_parse.ml | 68 | ||||
| -rw-r--r-- | language/l2_parse.ott | 32 |
5 files changed, 203 insertions, 232 deletions
diff --git a/language/l2.lem b/language/l2.lem index 926706a0..79cb82b3 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -1,4 +1,5 @@ (* generated by Ott 0.22 from: l2.ott *) +open import Pervasives open import Map open import Maybe @@ -21,20 +22,16 @@ val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) -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 kind = (* kinds *) - | K_kind of list base_kind +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 nexp = (* expression of kind $Nat$, for vector sizes and origins *) @@ -45,6 +42,10 @@ type nexp = (* expression of kind $Nat$, for vector sizes and origins *) | 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 *) @@ -55,11 +56,6 @@ type efct = (* effect *) | Effect_nondet (* nondeterminism from intra-instruction parallelism *) -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - type nexp_constraint = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -67,6 +63,11 @@ 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 *) @@ -83,6 +84,19 @@ type quant_item = (* Either a kinded identifier or a nexp constraint for a typq | QI_const of nexp_constraint (* A constraint for this type *) +type lit = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of nat (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) + + type typ = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_var of id (* Type variable *) @@ -97,19 +111,6 @@ and typ_arg = (* Type constructor arguments of all kinds *) | Typ_arg_effects of effects -type lit = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of nat (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) - - type typquant = (* type quantifiers and constraints *) | TypQ_tq of list quant_item | TypQ_no_forall (* sugar, omitting quantifier and constraints *) @@ -142,7 +143,7 @@ type exp = (* Expression *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * exp (* cast *) - | E_app of exp * list exp (* function application *) + | E_app of id * list exp (* function application *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of list exp (* tuple *) | E_if of exp * exp * exp (* conditional *) @@ -183,10 +184,6 @@ and letbind = (* Let binding *) | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) -type tannot_opt = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ - - type funcl = (* Function clause *) | FCL_Funcl of id * pat * exp @@ -201,6 +198,15 @@ type rec_opt = (* Optional recursive annotation for functions *) | Rec_rec (* recursive *) +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 @@ -212,24 +218,25 @@ type index_range = (* index specification, for bitfields in register types *) | BF_concat of index_range * index_range (* concatenation of index ranges *) -type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * id - | 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 fundef = (* Function definition *) | FD_function of rec_opt * tannot_opt * effects_opt * list funcl -type val_spec = (* Value type specification *) - | VS_val_spec 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 default_typing_spec = (* Default kinding or typing assumption *) + | DT_kind of base_kind * id + | 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 (typ * id) * bool (* union 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_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) @@ -257,7 +264,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 of string (* UTF8 strings *) + | Typ_lib_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 664ace51..6ecf3411 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -218,7 +218,11 @@ typschm = type -'a letbind = +'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) *) + +and 'a letbind = LB_aux of 'a letbind_aux * 'a annot and 'a exp_aux = (* Expression *) @@ -226,7 +230,7 @@ and 'a exp_aux = (* Expression *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * 'a exp (* cast *) - | E_app of 'a exp * ('a exp) list (* function application *) + | E_app of id * ('a exp) list (* function application *) | E_app_infix of 'a exp * id * 'a exp (* infix function application *) | E_tuple of ('a exp) list (* tuple *) | E_if of 'a exp * 'a exp * 'a exp (* conditional *) @@ -277,25 +281,22 @@ and 'a pexp_aux = (* Pattern match *) 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) *) - type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of typ * id type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * 'a exp +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string type -'a effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -305,75 +306,81 @@ rec_opt_aux = (* Optional recursive annotation for functions *) type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_some of typquant * typ type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot +'a effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * l type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +type_union = + Tu_aux of type_union_aux * l type -rec_opt = - Rec_aux of rec_opt_aux * l +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_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 *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot -and index_range = - BF_aux of index_range_aux * l + +type +rec_opt = + Rec_aux of rec_opt_aux * l type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id - | DT_typ of typschm * id +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot 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 *) type -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list - - -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 * ((typ * id)) list * bool (* union 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 * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list + + +type +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * id + | DT_typ of typschm * id type @@ -382,13 +389,18 @@ type type +'a type_def = + TD_aux of 'a type_def_aux * 'a annot + + +type 'a fundef = FD_aux of 'a fundef_aux * 'a annot type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot type @@ -407,17 +419,12 @@ type type -'a def = - DEF_aux of 'a def_aux * 'a annot - - -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_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} *) @@ -430,8 +437,8 @@ type type -'a defs = (* Definition sequence *) - Defs of ('a def) list +'a def = + DEF_aux of 'a def_aux * 'a annot type @@ -439,4 +446,9 @@ type 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 1e39aaff..e28e0271 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -111,13 +111,7 @@ id :: '' ::= {{ com Identifier }} {{ aux _ l }} | x :: :: id - | ( x ) :: :: deIid {{ com remove infix status }} -% 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 -% on type variables (or variables of other kinds) -% We don't enforce a lexical convention on infix operators, as some of the -% targets use alphabetical infix operators. + | ( deinfix x ) :: :: deIid {{ com remove infix status }} | bool :: M :: bool {{ com Built in type identifiers }} {{ ichlo bool_id }} | bit :: M :: bit {{ ichlo bit_id }} | unit :: M :: unit {{ ichlo unit_id }} @@ -128,6 +122,13 @@ id :: '' ::= | list :: M :: list {{ ichlo list_id }} | set :: M :: set {{ ichlo set_id }} | reg :: M :: reg {{ ichlo reg_id }} +% 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 +% on type variables (or variables of other kinds) +% We don't enforce a lexical convention on infix operators, as some of the +% targets use alphabetical infix operators. + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -137,74 +138,6 @@ id :: '' ::= grammar - -% a :: 'A_' ::= -% {{ aux _ l }} -% {{ ocaml terminal * text }} -% {{ lem terminal * string }} -% {{ hol string }} -% {{ com Type variables }} -% | ' x :: :: A -% {{ ichlo [[x]] }} -% -% N :: 'N_' ::= -% {{ aux _ l }} -% {{ ocaml terminal * text }} -% {{ lem terminal * string }} -% {{ hol string }} -% {{ com numeric variables }} -% | ' ' x :: :: N -% {{ ichlo [[x]] }} -% -% EN :: 'EN_' ::= -% {{ aux _ l }} -% {{ ocaml terminal * text }} -% {{ lem terminal * string }} -% {{ hol string }} -% {{ com endianness variables }} -% | ' ' ' x :: :: EN -% {{ ichlo [[x]] }} -% -% EFF :: 'EFF_' ::= -% {{ aux _ l }} -% {{ ocaml terminal * text }} -% {{ lem terminal * string }} -% {{ hol string }} -% {{ com effect set variables }} -% | ' ' ' ' x :: :: EFF -% {{ ichlo [[x]] }} -% % TODO: better concrete syntax!!!! -% -% -% tnvar :: '' ::= -% {{ com variables of the base kinds }} -% | a :: :: Av -% | N :: :: Nv -% | EN :: :: ENv -% | EFF :: :: EFFv -% -% tnvars :: '' ::= {{ phantom }} -% {{ hol tnvar list }} -% {{ ocaml tnvar list }} -% {{ lem list tnvar }} -% {{ com Type variable lists }} -% | tnvar1 .. tnvarn :: :: Tvars -% {{ hol [[tnvar1..tnvarn]] }} -% {{ ocaml [[tnvar1..tnvarn]] }} -% {{ lem [[tnvar1..tnvarn]] }} -% -% -% ids :: '' ::= {{ phantom }} -% {{ hol id list }} -% {{ ocaml id list }} -% {{ lem list id }} -% {{ com Type variable lists }} -% | id1 .. idn :: :: Tvars -% {{ hol [[id1..idn]] }} -% {{ ocaml [[id1..idn]] }} -% {{ lem [[id1..idn]] }} - - base_kind :: 'BK_' ::= {{ com base kind}} {{ aux _ l }} @@ -217,7 +150,7 @@ kind :: 'K_' ::= {{ com kinds}} {{ aux _ l }} | base_kind1 -> ... -> base_kindn :: :: kind -% we'll never use ...-> Nat +% we'll never use ...-> Nat , .. Order , .. or Effects nexp :: 'Nexp_' ::= @@ -228,7 +161,7 @@ nexp :: 'Nexp_' ::= | nexp1 * nexp2 :: :: times {{ com product }} %{{ com must be linear after normalisation... except for the type of *, ahem }} | nexp1 + nexp2 :: :: sum {{ com sum }} - | 2 ** nexp :: :: exp {{ com exponential }} + | 2** nexp :: :: exp {{ com exponential }} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= @@ -275,7 +208,7 @@ typ :: 'Typ_' ::= | 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]] }} @@ -293,27 +226,27 @@ 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]] }} + | 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 }} + | 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]] }} + | 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 @@ -419,7 +352,7 @@ type_def :: 'TD_' ::= % 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 { typ1 id1 ; ... ; typn idn semi_opt } :: :: variant + | typedef id naming_scheme_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 @@ -430,6 +363,11 @@ type_def :: 'TD_' ::= % also sugar [ nexp ] +type_union :: 'Tu_' ::= + {{ com Type union constructors }} + {{ aux _ l }} + | id :: :: id + | typ id :: :: ty_id index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} {{ aux _ l }} @@ -498,15 +436,14 @@ pat :: 'P_' ::= % | ( pat : typ ) :: :: typ % {{ com Typed patterns }} % C-style -% XXX < > are necessary to make the grammar non ambiguous - | ( < typ > pat ) :: :: typ + | ( ( typ ) pat ) :: :: typ {{ com typed pattern }} | id :: :: id {{ com identifier }} % - | id pat1 .. patn :: :: app + | id ( pat1 , .. , patn ) :: :: app {{ com union constructor pattern }} % OR? do we invent something ghastly including a union keyword? Perhaps not... @@ -532,14 +469,12 @@ pat :: 'P_' ::= | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} - | [| pat1 , .. , patn |] :: :: list + | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren {{ ichlo [[pat]] }} % | pat1 '::' pat2 :: :: cons % {{ com Cons patterns }} -% | id '+' num :: :: num_add -% {{ com constant addition patterns }} % XXX Is this still useful? fpat :: 'FP_' ::= @@ -575,7 +510,7 @@ exp :: 'E_' ::= | ( typ ) exp :: :: cast {{ com cast }} - | exp exp1 ... expn :: :: app + | id ( exp1 , .. , expn ) :: :: app {{ com function application }} % Note: fully applied function application only % We might restrict exp to be an identifier @@ -627,7 +562,7 @@ exp :: 'E_' ::= % lists - | [| exp1 , .. , expn |] :: :: list + | [|| exp1 , .. , expn ||] :: :: list {{ com list }} | exp1 '::' exp2 :: :: cons {{ com cons }} @@ -821,6 +756,7 @@ val_spec :: 'VS_' ::= {{ com Value type specification }} {{ aux _ annot }} {{ auxparam 'a }} | val typschm id :: :: val_spec + | val extern typschm id :: :: extern_no_rename | 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 }} diff --git a/language/l2_parse.ml b/language/l2_parse.ml index c6153f89..990166c4 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -192,7 +192,7 @@ exp_aux = (* Expression *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of atyp * exp (* cast *) - | E_app of exp * (exp) list (* function application *) + | E_app of id * (exp) list (* function application *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of (exp) list (* tuple *) | E_if of exp * exp * exp (* conditional *) @@ -248,9 +248,9 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of atyp * id type @@ -260,14 +260,25 @@ tannot_opt_aux = (* Optional type annotation for functions *) type +effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of atyp + + +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) + + +type funcl_aux = (* Function clause *) FCL_Funcl of id * pat * exp type -effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of atyp +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type @@ -281,49 +292,50 @@ 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 +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * l type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * l +effects_opt = + Effects_opt_aux of effects_opt_aux * l type -funcl = - FCL_aux of funcl_aux * l +rec_opt = + Rec_aux of rec_opt_aux * l type -effects_opt = - Effects_opt_aux of effects_opt_aux * l +funcl = + FCL_aux of funcl_aux * l type -default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id - | DT_typ of typschm * id +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 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 * ((atyp * id)) list * bool (* union 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 *) type -val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_spec of typschm * id * string +default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * id + | DT_typ of typschm * id type @@ -332,8 +344,8 @@ fundef_aux = (* Function definition *) type -default_typing_spec = - DT_aux of default_typing_spec_aux * l +val_spec = + VS_aux of val_spec_aux * l type @@ -342,8 +354,8 @@ type_def = type -val_spec = - VS_aux of val_spec_aux * l +default_typing_spec = + DT_aux of default_typing_spec_aux * l type diff --git a/language/l2_parse.ott b/language/l2_parse.ott index c2cbe50d..6876fcfa 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -116,7 +116,8 @@ id :: '' ::= {{ com Identifier }} {{ aux _ l }} | x :: :: id - | ( x ) :: :: deIid {{ com remove infix status }} + | ( deinfix x ) :: :: deIid {{ com remove infix status }} + % 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 @@ -132,8 +133,6 @@ id :: '' ::= grammar - - base_kind :: 'BK_' ::= {{ com base kind}} {{ aux _ l }} @@ -166,7 +165,7 @@ atyp :: 'ATyp_' ::= | num :: :: constant {{ com constant }} | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} - | 2 ** atyp :: :: exp {{ com exponential }} + | 2** atyp :: :: exp {{ com exponential }} | ( atyp ) :: S :: paren {{ icho [[atyp]] }} | inc :: :: inc {{ com increasing (little-endian) }} @@ -181,7 +180,7 @@ atyp :: 'ATyp_' ::= {{ 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 }} @@ -278,6 +277,12 @@ grammar | :: :: none | [ name = regexp ] :: :: some +type_union :: 'Tu_' ::= + {{ com Type union constructors }} + {{ aux _ l }} + | id :: :: id + | atyp id :: :: ty_id + type_def :: 'TD_' ::= {{ com Type definition body }} {{ aux _ l }} @@ -285,7 +290,7 @@ type_def :: 'TD_' ::= {{ com type abbreviation }} {{ texlong }} | typedef id naming_scheme_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record {{ com struct type definition }} {{ texlong }} - | typedef id naming_scheme_opt = const union typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: variant + | typedef id naming_scheme_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 {{ com enumeration type definition}} {{ texlong }} @@ -358,13 +363,13 @@ pat :: 'P_' ::= {{ com wildcard }} | ( pat as id ) :: :: as {{ com named pattern }} - | ( < atyp > pat ) :: :: typ + | ( ( atyp ) pat ) :: :: typ {{ com typed pattern }} | id :: :: id {{ com identifier }} - | id pat1 .. patn :: :: app + | id ( pat1 , .. , patn ) :: :: app {{ com union constructor pattern }} | { fpat1 ; ... ; fpatn semi_opt } :: :: record @@ -381,7 +386,7 @@ pat :: 'P_' ::= | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} - | [| pat1 , .. , patn |] :: :: list + | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren {{ ichlo [[pat]] }} @@ -419,7 +424,7 @@ exp :: 'E_' ::= | ( atyp ) exp :: :: cast {{ com cast }} - | exp exp1 ... expn :: :: app + | id ( exp1 , .. , expn ) :: :: app {{ com function application }} % Note: fully applied function application only % We might restrict exp to be an identifier @@ -471,7 +476,7 @@ exp :: 'E_' ::= % lists - | [| exp1 , .. , expn |] :: :: list + | [|| exp1 , .. , expn ||] :: :: list {{ com list }} | exp1 '::' exp2 :: :: cons {{ com cons }} @@ -505,8 +510,6 @@ exp :: 'E_' ::= | switch exp { case pexp1 ... case pexpn } :: :: case {{ com pattern matching }} -% | ( typ ) exp :: :: Typed -% {{ com Type-annotated expressions }} | letbind in exp :: :: let {{ com let expression }} @@ -661,7 +664,7 @@ letbind :: 'LB_' ::= {{ com Let binding }} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} - | typschm pat = exp :: :: val_explicit + | let typschm pat = exp :: :: val_explicit {{ com value binding, explicit type ([[pat]] must be total)}} | let pat = exp :: :: val_implicit {{ com value binding, implicit type ([[pat]] must be total)}} @@ -672,6 +675,7 @@ val_spec :: 'VS_' ::= {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} | val typschm id :: :: val_spec + | val extern typschm id :: :: extern_no_rename | val extern typschm id = string :: :: extern_spec default_typing_spec :: 'DT_' ::= |