diff options
| -rw-r--r-- | language/l2.ott | 84 | ||||
| -rw-r--r-- | src/ast.ml | 79 |
2 files changed, 84 insertions, 79 deletions
diff --git a/language/l2.ott b/language/l2.ott index 5002eb2b..0e0e3ce6 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -481,26 +481,26 @@ ctor_def :: 'CT_' ::= tdef :: 'TD_' ::= {{ com Type definition body }} | typedef id naming_scheme_opt = typschm :: :: abbrev - {{ com Type abbreviation }} {{ texlong }} + {{ com type abbreviation }} {{ texlong }} | typedef id naming_scheme_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record - {{ com Struct type definition }} {{ texlong }} + {{ 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 { typ1 id1 ; ... ; typn idn semi_opt } :: :: variant - {{ com Union type definition}} {{ texlong }} + {{ com union type definition}} {{ texlong }} | typedef id naming_scheme_opt = enum { id1 ; ... ; idn semi_opt } :: :: enum {{ com enumeration type definition}} {{ texlong }} | typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -:: :: register {{ com register mutable bitfield type }} {{ texlong }} +:: :: register {{ com register mutable bitfield type definition }} {{ texlong }} % also sugar [ nexp ] -index_range :: 'BF_' ::= {{ com index specification, e.g.~for bitfields }} +index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}} | num :: :: 'single' {{ com single index }} | num1 '..' num2 :: :: range {{ com index range }} | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }} @@ -553,6 +553,8 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} pat :: 'P_' ::= {{ com Pattern }} {{ aux _ l }} + | lit :: :: lit + {{ com literal constant pattern }} | _ :: :: wild {{ com wildcard }} | ( pat as id ) :: :: as @@ -589,20 +591,19 @@ pat :: 'P_' ::= {{ com vector pattern (with explicit indices) }} % cf ntoes for this - | pat1 : .. : patn :: :: vector_concat + | pat1 : .... : patn :: :: vector_concat {{ com concatenated vector pattern }} | ( pat1 , .... , patn ) :: :: tup {{ com tuple pattern }} | [| pat1 , .. , patn |] :: :: list {{ com list pattern }} - | ( pat ) :: :: paren + | ( pat ) :: S :: paren +{{ ichlo [[pat]] }} % | pat1 '::' pat2 :: :: cons % {{ com Cons patterns }} % | id '+' num :: :: num_add % {{ com constant addition patterns }} - | lit :: :: lit - {{ com literal constant pattern }} fpat :: 'FP_' ::= {{ com Field pattern }} @@ -625,7 +626,6 @@ exp :: 'E_' ::= {{ com Expression }} {{ aux _ l }} - | ( exp ) :: S :: paren {{ ichlo [[exp]] }} | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} | id :: :: id @@ -670,7 +670,7 @@ exp :: 'E_' ::= {{ com vector functional update }} | [ exp with exp1 : exp2 = exp3 ] :: :: vector_update_range - {{ com vector functional subrange update (with another vector)}} + {{ com vector subrange update (with vector)}} % do we want a functional update form with a comma-separated list of such? @@ -717,6 +717,9 @@ exp :: 'E_' ::= | lexp := exp :: :: assign {{ com imperative assignment }} + | ( exp ) :: S :: paren {{ ichlo [[exp]] }} + + lexp :: 'LEXP_' ::= {{ com lvalue expression }} | id :: :: id {{ com identifier }} @@ -727,17 +730,17 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} fexp :: 'FE_' ::= - {{ com field-expression }} + {{ com Field-expression }} {{ aux _ l }} | id = exp :: :: Fexp fexps :: 'FES_' ::= - {{ com field-expression list }} + {{ com Field-expression list }} {{ aux _ l }} | fexp1 ; ... ; fexpn semi_opt :: :: Fexps pexp :: 'Pat_' ::= - {{ com pattern match }} + {{ com Pattern match }} {{ aux _ l }} | pat -> exp :: :: exp % apparently could use -> or => for this. @@ -814,29 +817,31 @@ grammar %%%%% C-ish style %%%%%%%%%% tannot_opt :: 'Typ_annot_opt_' ::= - {{ com Optional type annotation }} + {{ com Optional type annotation for functions}} | :: :: none | typ_quant typ :: :: some +rec_opt :: 'Rec_' ::= + {{ aux _ l }} {{ com Optional recursive annotation for functions }} + | :: :: nonrec {{ com non-recursive }} + | rec :: :: rec {{ com recursive }} + +effects_opt :: 'Effects_opt_' ::= + {{ aux _ l }} {{ com Optional effect annotation for functions }} + | :: :: pure {{ com sugar for empty effect set }} + | effects :: :: effects + funcl :: 'FCL_' ::= {{ com Function clause }} {{ aux _ l }} | id pat = exp :: :: Funcl -rec_opt :: 'Rec_' ::= - {{ aux _ l }} - | :: :: nonrec - | rec :: :: rec - -effects_opt :: 'Effects_opt_' ::= - {{ aux _ l }} - | :: :: pure {{ com sugar for empty effect set }} - | effects :: :: nonpure fundef :: 'FD_' ::= {{ com Function definition}} {{ aux _ l }} - | function rec_opt tannot_opt effects_opt funcl1 and ... and funcln :: :: function {{ texlong }} {{ com function definition }} + | function rec_opt tannot_opt effects_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 % pattern in the funcl @@ -848,7 +853,7 @@ letbind :: 'LB_' ::= {{ com Let binding }} {{ aux _ l }} | typschm id = exp :: :: val_explicit - {{ com Value binding }} + {{ com value binding with explicit type }} | let id = exp :: :: val_implicit {{ com value binding with implicit type }} @@ -859,7 +864,7 @@ val_spec :: 'VS_' ::= | val typschm id :: :: val_spec default_typing_spec :: 'DT_' ::= - {{ com default kinding and typing assumption }} + {{ com Default kinding or typing assumption }} {{ aux _ l }} | default base_kind regexp :: :: kind | default typschm regexp :: :: typ @@ -878,30 +883,31 @@ def :: 'DEF_' ::= {{ com Top-level definition }} {{ aux _ l }} | type_def :: :: type - {{ com Type definition }} + {{ com type definition }} | fundef :: :: fundef - {{ com Function definition }} + {{ com function definition }} | letbind :: :: val - {{ com Value definition }} + {{ com value definition }} | val_spec :: :: spec - {{ com Top-level type constraint }} + {{ com top-level type constraint }} | default_typing_spec :: :: default {{ com default kind and type assumptions }} | register typ id :: :: reg_dec - {{ com Register declaration }} - - | split function rec_opt tannot_opt effects_opt id :: :: split_function {{ texlong }} + {{ com register declaration }} - | function clause funcl :: :: split_funcl + | scattered function rec_opt tannot_opt effects_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} - | end id :: :: split_end + | function clause funcl :: :: scattered_funcl +{{ com scattered function definition clause }} - | split typedef id naming_scheme_opt = const union typquant :: :: split_variant {{ texlong }} + | scattered typedef id naming_scheme_opt = const union typquant :: :: scattered_variant {{ texlong }} {{ com scattered union definition header }} - | union member id = typ id' :: :: split_unioncl + | union id member typ id' :: :: scattered_unioncl {{ com scattered union definition member }} + | end id :: :: scattered_end +{{ com scattered definition end }} defs :: '' ::= - {{ com Definition sequences }} + {{ com Definition sequence }} {{ aux _ l }} | def1 .. defn :: :: Defs @@ -204,7 +204,8 @@ typschm = type pat_aux = (* Pattern *) - P_wild of terminal (* wildcard *) + P_lit of lit (* literal constant pattern *) + | P_wild of terminal (* wildcard *) | P_as of terminal * pat * terminal * id * terminal (* named pattern *) | P_typ of terminal * typ * pat * terminal (* typed pattern *) | P_id of id (* identifier *) @@ -215,8 +216,6 @@ pat_aux = (* Pattern *) | P_vector_concat of (pat * terminal) list (* concatenated vector pattern *) | P_tup of terminal * (pat * terminal) list * terminal (* tuple pattern *) | P_list of terminal * (pat * terminal) list * terminal (* list pattern *) - | P_paren of terminal * pat * terminal - | P_lit of lit (* literal constant pattern *) and pat = P_aux of pat_aux * l @@ -242,7 +241,7 @@ exp_aux = (* Expression *) | E_vector_access of exp * terminal * exp * terminal (* vector access *) | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *) | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *) - | E_vector_update_range of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional subrange update (with another vector) *) + | E_vector_update_range of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *) | E_list of terminal * (exp * terminal) list * terminal (* list *) | E_cons of exp * terminal * exp (* cons *) | E_record of terminal * fexps * terminal (* struct *) @@ -261,26 +260,26 @@ and lexp = (* lvalue expression *) | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal (* subvector *) | LEXP_field of lexp * terminal * id (* struct field *) -and fexp_aux = (* field-expression *) +and fexp_aux = (* Field-expression *) FE_Fexp of id * terminal * exp and fexp = FE_aux of fexp_aux * l -and fexps_aux = (* field-expression list *) +and fexps_aux = (* Field-expression list *) FES_Fexps of (fexp * terminal) list * terminal * bool and fexps = FES_aux of fexps_aux * l -and pexp_aux = (* pattern match *) +and pexp_aux = (* Pattern match *) Pat_exp of pat * terminal * exp and pexp = Pat_aux of pexp_aux * l and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * id * terminal * exp (* Value binding *) + LB_val_explicit of typschm * id * terminal * exp (* value binding with explicit type *) | LB_val_implicit of terminal * id * terminal * exp (* value binding with implicit type *) and letbind = @@ -288,34 +287,29 @@ and letbind = type -funcl_aux = (* Function clause *) - FCL_Funcl of id * pat * terminal * exp +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec of terminal (* recursive *) type -rec_opt_aux = - Rec_nonrec - | Rec_rec of terminal +effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects type -effects_opt_aux = - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_nonpure of effects +funcl_aux = (* Function clause *) + FCL_Funcl of id * pat * terminal * exp type -tannot_opt = (* Optional type annotation *) +tannot_opt = (* Optional type annotation for functions *) Typ_annot_opt_none | Typ_annot_opt_some of terminal * typ type -funcl = - FCL_aux of funcl_aux * l - - -type rec_opt = Rec_aux of rec_opt_aux * l @@ -326,8 +320,13 @@ effects_opt = type +funcl = + FCL_aux of funcl_aux * l + + +type fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list (* function definition *) + FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list type @@ -336,7 +335,7 @@ val_spec_aux = (* Value type specification *) type -default_typing_spec_aux = (* default kinding and typing assumption *) +default_typing_spec_aux = (* Default kinding or typing assumption *) DT_kind of terminal * base_kind * terminal * string | DT_typ of terminal * typschm * terminal * string @@ -358,17 +357,17 @@ default_typing_spec = type def_aux = (* Top-level definition *) - DEF_type of terminal (* Type definition *) - | DEF_fundef of fundef (* Function definition *) - | DEF_val of letbind (* Value definition *) - | DEF_spec of val_spec (* Top-level type constraint *) + DEF_type of terminal (* 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_reg_dec of terminal * typ * id (* Register declaration *) - | DEF_split_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id - | DEF_split_funcl of terminal * terminal * funcl - | DEF_split_end of terminal * id - | DEF_split_variant of terminal * terminal * id * terminal * terminal * terminal * terminal * typquant - | DEF_split_unioncl of terminal * terminal * id * terminal * typ * id + | DEF_reg_dec of terminal * typ * id (* register declaration *) + | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *) + | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *) + | DEF_scattered_variant of terminal * terminal * id * terminal * terminal * terminal * terminal * typquant (* scattered union definition header *) + | DEF_scattered_unioncl of terminal * id * terminal * typ * id (* scattered union definition member *) + | DEF_scattered_end of terminal * id (* scattered definition end *) type @@ -395,14 +394,14 @@ typ_lib_aux = (* library types and syntactic sugar for them *) type -index_range = (* index specification, e.g.~for bitfields *) +index_range = (* index specification, for bitfields in register types *) BF_single of terminal * int (* single index *) | BF_range of terminal * int * terminal * terminal * int (* index range *) | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *) type -defs_aux = (* Definition sequences *) +defs_aux = (* Definition sequence *) Defs of (def) list @@ -418,11 +417,11 @@ ctor_def = (* Datatype constructor definition clause *) type tdef = (* Type definition body *) - TD_abbrev of terminal * id * terminal * terminal * typschm (* Type abbreviation *) - | TD_record of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Struct type definition *) - | TD_variant of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* Union type definition *) + TD_abbrev of terminal * id * terminal * terminal * typschm (* type abbreviation *) + | TD_record of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* struct type definition *) + | TD_variant of terminal * id * terminal * terminal * terminal * terminal * typquant * terminal * ((typ * id) * terminal) list * terminal * bool * terminal (* union type definition *) | TD_enum of terminal * id * terminal * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *) - | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type *) + | TD_register of terminal * id * terminal * terminal * terminal * terminal * nexp * terminal * nexp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *) type |