diff options
| -rw-r--r-- | language/l2.ott | 4 | ||||
| -rw-r--r-- | src/ast.ml | 156 |
2 files changed, 80 insertions, 80 deletions
diff --git a/language/l2.ott b/language/l2.ott index 18fb213b..e25d7547 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -881,8 +881,8 @@ val_spec :: 'VS_' ::= default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ l }} - | default base_kind regexp :: :: kind - | default typschm regexp :: :: typ + | default base_kind id :: :: 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 % default regexps (in order from the beginning) and pick the first @@ -49,6 +49,12 @@ type x = terminal * text (* identifier *) type ix = terminal * text (* infix identifier *) type +id_aux = (* Identifier *) + Id of x + | DeIid of terminal * x * terminal (* remove infix status *) + + +type base_kind_aux = (* base kind *) BK_type of terminal (* kind of types *) | BK_nat of terminal (* kind of natural number size expressions *) @@ -57,9 +63,8 @@ base_kind_aux = (* base kind *) type -id_aux = (* Identifier *) - Id of x - | DeIid of terminal * x * terminal (* remove infix status *) +id = + Id_aux of id_aux * l type @@ -68,13 +73,14 @@ base_kind = type -id = - Id_aux of id_aux * l - - -type -kind_aux = (* kinds *) - K_kind of (base_kind * terminal) list +effect_aux = (* effect *) + Effect_rreg of terminal (* read register *) + | Effect_wreg of terminal (* write register *) + | Effect_rmem of terminal (* read memory *) + | Effect_wmem of terminal (* write memory *) + | Effect_undef of terminal (* undefined-instruction exception *) + | Effect_unspec of terminal (* unspecified values *) + | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *) type @@ -90,19 +96,13 @@ and nexp = type -effect_aux = (* effect *) - Effect_rreg of terminal (* read register *) - | Effect_wreg of terminal (* write register *) - | Effect_rmem of terminal (* read memory *) - | Effect_wmem of terminal (* write memory *) - | Effect_undef of terminal (* undefined-instruction exception *) - | Effect_unspec of terminal (* unspecified values *) - | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *) +kind_aux = (* kinds *) + K_kind of (base_kind * terminal) list type -kind = - K_aux of kind_aux * l +effect = + Effect_aux of effect_aux * l type @@ -114,19 +114,14 @@ nexp_constraint_aux = (* constraint over kind $_$ *) type -effect = - Effect_aux of effect_aux * l - - -type -kinded_id = (* 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 -nexp_constraint = - NC_aux of nexp_constraint_aux * l +effects_aux = (* effect set, of kind $_$ *) + Effects_var of id + | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) type @@ -137,31 +132,31 @@ order_aux = (* vector order specifications, of kind $_$ *) type -effects_aux = (* effect set, of kind $_$ *) - Effects_var of id - | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) +nexp_constraint = + NC_aux of nexp_constraint_aux * l type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal - | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +kinded_id = (* optionally kind-annotated identifier *) + KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) type -order = - Ord_aux of order_aux * l +effects = + Effects_aux of effects_aux * l type -effects = - Effects_aux of effects_aux * l +order = + Ord_aux of order_aux * l type -typquant = - TypQ_aux of typquant_aux * l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal + | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type @@ -180,6 +175,11 @@ and typ_arg = (* Type constructor arguments of all kinds *) type +typquant = + TypQ_aux of typquant_aux * l + + +type typschm_aux = (* type scheme *) TypSchm_ts of typquant * typ @@ -288,30 +288,20 @@ and letbind = type -effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects - - -type -funcl_aux = (* Function clause *) - FCL_Funcl of id * pat * terminal * exp - - -type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec of terminal (* recursive *) type -effects_opt = - Effects_opt_aux of effects_opt_aux * l +effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects type -funcl = - FCL_aux of funcl_aux * l +funcl_aux = (* Function clause *) + FCL_Funcl of id * pat * terminal * exp type @@ -326,13 +316,13 @@ rec_opt = type -fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list +effects_opt = + Effects_opt_aux of effects_opt_aux * l type -val_spec_aux = (* Value type specification *) - VS_val_spec of terminal * typschm * id +funcl = + FCL_aux of funcl_aux * l type @@ -349,19 +339,19 @@ index_range = (* index specification, for bitfields in register types *) type -default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * base_kind * terminal * string - | DT_typ of terminal * typschm * terminal * string +fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list type -fundef = - FD_aux of fundef_aux * l +val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * typschm * id type -val_spec = - VS_aux of val_spec_aux * l +default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * typschm * id type @@ -374,6 +364,16 @@ type_def = (* Type definition body *) type +fundef = + FD_aux of fundef_aux * l + + +type +val_spec = + VS_aux of val_spec_aux * l + + +type default_typing_spec = DT_aux of default_typing_spec_aux * l @@ -394,11 +394,6 @@ def_aux = (* Top-level definition *) type -def = - DEF_aux of def_aux * l - - -type typ_lib_aux = (* library types and syntactic sugar for them *) Typ_lib_unit of terminal (* unit type with value $()$ *) | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) @@ -417,8 +412,13 @@ typ_lib_aux = (* library types and syntactic sugar for them *) type -defs = (* Definition sequence *) - Defs of (def) list +def = + DEF_aux of def_aux * l + + +type +typ_lib = + Typ_lib_aux of typ_lib_aux * l type @@ -427,8 +427,8 @@ ctor_def = (* Datatype constructor definition clause *) type -typ_lib = - Typ_lib_aux of typ_lib_aux * l +defs = (* Definition sequence *) + Defs of (def) list |