diff options
| author | Peter Sewell | 2013-07-17 16:50:36 +0100 |
|---|---|---|
| committer | Peter Sewell | 2013-07-17 16:50:36 +0100 |
| commit | 9538d030494bdfb07bdbd5c99ebb64a8fffe55e7 (patch) | |
| tree | fd7d7eb0909f9d82bbe35633e8e7261e1ec6d64e /src | |
| parent | 80fd65368f2769a29ce657aaffef50f3c8f0455f (diff) | |
wib
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.ml | 168 | ||||
| -rw-r--r-- | src/parse_ast.ml | 126 |
2 files changed, 147 insertions, 147 deletions
@@ -59,19 +59,14 @@ base_kind_aux = (* base kind *) type -base_kind = - BK_aux of base_kind_aux * l - - -type id_aux = (* Identifier *) Id of x | DeIid of terminal * x * terminal (* remove infix status *) type -kind_aux = (* kinds *) - K_kind of (base_kind * terminal) list +base_kind = + BK_aux of base_kind_aux * l type @@ -80,6 +75,11 @@ id = type +kind_aux = (* kinds *) + K_kind of (base_kind * terminal) list + + +type effect_aux = (* effect *) Effect_rreg of terminal (* read register *) | Effect_wreg of terminal (* write register *) @@ -91,11 +91,6 @@ effect_aux = (* effect *) type -kind = - K_aux of kind_aux * l - - -type nexp_aux = (* expression of kind $_$, for vector sizes and origins *) Nexp_id of id (* identifier *) | Nexp_constant of terminal * int (* constant *) @@ -108,14 +103,13 @@ and nexp = type -effect = - Effect_aux of effect_aux * l +kind = + K_aux of kind_aux * l type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) +effect = + Effect_aux of effect_aux * l type @@ -127,6 +121,12 @@ type type +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) + + +type effects_aux = (* effect set, of kind $_$ *) Effects_var of id | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) @@ -140,13 +140,13 @@ order_aux = (* vector order specifications, of kind $_$ *) type -kinded_id = - KOpt_aux of kinded_id_aux * l +'a nexp_constraint = + NC_aux of 'a nexp_constraint_aux * 'a annot type -'a nexp_constraint = - NC_aux of 'a nexp_constraint_aux * 'a annot +kinded_id = + KOpt_aux of kinded_id_aux * l type @@ -167,19 +167,6 @@ type type -lit_aux = (* Literal constant *) - L_unit of terminal * terminal (* $() : _$ *) - | L_zero of terminal (* $_ : _$ *) - | L_one of terminal (* $_ : _$ *) - | L_true of terminal (* $_ : _$ *) - | L_false of terminal (* $_ : _$ *) - | L_num of terminal * int (* natural number constant *) - | L_hex of terminal * string (* bit vector constant, C-style *) - | L_bin of terminal * string (* bit vector constant, C-style *) - | L_string of terminal * string (* string constant *) - - -type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild of terminal (* Unspecified type *) | Typ_var of id (* Type variable *) @@ -206,8 +193,16 @@ type type -lit = - L_aux of lit_aux * l +lit_aux = (* Literal constant *) + L_unit of terminal * terminal (* $() : _$ *) + | L_zero of terminal (* $_ : _$ *) + | L_one of terminal (* $_ : _$ *) + | L_true of terminal (* $_ : _$ *) + | L_false of terminal (* $_ : _$ *) + | L_num of terminal * int (* natural number constant *) + | L_hex of terminal * string (* bit vector constant, C-style *) + | L_bin of terminal * string (* bit vector constant, C-style *) + | L_string of terminal * string (* string constant *) type @@ -216,6 +211,16 @@ type type +lit = + L_aux of lit_aux * l + + +type +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a annot + + +type 'a pat_aux = (* Pattern *) P_lit of lit (* literal constant pattern *) | P_wild of terminal (* wildcard *) @@ -241,15 +246,7 @@ and 'a fpat = type -'a typschm = - TypSchm_aux of 'a typschm_aux * 'a annot - - -type -'a letbind = - LB_aux of 'a letbind_aux * 'a annot - -and 'a exp_aux = (* Expression *) +'a exp_aux = (* Expression *) E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) @@ -307,6 +304,9 @@ and 'a letbind_aux = (* Let binding *) LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *) | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *) +and 'a letbind = + LB_aux of 'a letbind_aux * 'a annot + type naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) @@ -315,26 +315,31 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va type +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * typ + + +type rec_opt_aux = (* Optional recursive annotation for functions *) Rec_nonrec (* non-recursive *) | Rec_rec of terminal (* recursive *) type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * terminal * 'a exp +'a effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of terminal * typ +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * terminal * 'a exp type -'a effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type @@ -348,8 +353,8 @@ and index_range = 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 @@ -358,18 +363,19 @@ rec_opt = type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * 'a typschm * id type @@ -382,19 +388,18 @@ type type -'a val_spec_aux = (* Value type specification *) - VS_val_spec of terminal * 'a typschm * id +'a fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * base_kind * id - | DT_typ of terminal * 'a typschm * id +'a val_spec_aux = (* Value type specification *) + VS_val_spec of terminal * 'a typschm * id type -'a fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot type @@ -403,18 +408,13 @@ type type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot - - -type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type @@ -433,6 +433,11 @@ 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 of terminal (* unit type with value $()$ *) | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) @@ -456,8 +461,8 @@ type type -'a def = - DEF_aux of 'a def_aux * 'a annot +'a defs = (* Definition sequence *) + Defs of ('a def) list type @@ -470,9 +475,4 @@ type CT_aux of 'a ctor_def_aux * 'a annot -type -'a defs = (* Definition sequence *) - Defs of ('a def) list - - diff --git a/src/parse_ast.ml b/src/parse_ast.ml index b5f38aa4..2ecf279d 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -59,6 +59,12 @@ base_kind_aux = (* base kind *) type +id_aux = (* Identifier *) + Id of x + | DeIid of terminal * x * terminal (* remove infix status *) + + +type effect_aux = (* effect *) Effect_rreg of terminal (* read register *) | Effect_wreg of terminal (* write register *) @@ -70,24 +76,18 @@ effect_aux = (* effect *) type -id_aux = (* Identifier *) - Id of x - | DeIid of terminal * x * terminal (* remove infix status *) - - -type base_kind = BK_aux of base_kind_aux * l type -effect = - Effect_aux of effect_aux * l +id = + Id_aux of id_aux * l type -id = - Id_aux of id_aux * l +effect = + Effect_aux of effect_aux * l type @@ -151,6 +151,11 @@ type type +'a typquant = + TypQ_aux of 'a typquant_aux * 'a annot + + +type lit_aux = (* Literal constant *) L_unit of terminal * terminal (* $() : _$ *) | L_zero of terminal (* $_ : _$ *) @@ -164,8 +169,8 @@ lit_aux = (* Literal constant *) type -'a typquant = - TypQ_aux of 'a typquant_aux * 'a annot +'a typschm_aux = (* type scheme *) + TypSchm_ts of 'a typquant * atyp type @@ -174,8 +179,8 @@ lit = type -'a typschm_aux = (* type scheme *) - TypSchm_ts of 'a typquant * atyp +'a typschm = + TypSchm_aux of 'a typschm_aux * 'a annot type @@ -204,11 +209,6 @@ and 'a fpat = type -'a typschm = - TypSchm_aux of 'a typschm_aux * 'a annot - - -type 'a exp_aux = (* Expression *) E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -272,8 +272,15 @@ and 'a letbind = type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * terminal * 'a exp +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal + + +type +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of terminal * terminal type @@ -289,30 +296,23 @@ type type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of terminal * terminal - - -type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * terminal * 'a exp type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type -rec_opt = - Rec_aux of rec_opt_aux * l - +index_range_aux = (* 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 -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +and index_range = + BF_aux of index_range_aux * l type @@ -321,23 +321,18 @@ type type -index_range_aux = (* 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 *) - -and index_range = - BF_aux of index_range_aux * l +rec_opt = + Rec_aux of rec_opt_aux * l type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type -'a fundef_aux = (* Function definition *) - FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type @@ -350,9 +345,8 @@ type type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of terminal * base_kind * id - | DT_typ of terminal * 'a typschm * id +'a fundef_aux = (* Function definition *) + FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list type @@ -361,8 +355,9 @@ type type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of terminal * base_kind * id + | DT_typ of terminal * 'a typschm * id type @@ -371,8 +366,8 @@ type type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type @@ -381,6 +376,11 @@ type type +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot + + +type 'a def_aux = (* Top-level definition *) DEF_type of 'a type_def (* type definition *) | DEF_fundef of 'a fundef (* function definition *) @@ -396,11 +396,6 @@ 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 of terminal (* unit type with value $()$ *) | Typ_lib_bool of terminal (* booleans $_$ and $_$ *) @@ -424,8 +419,8 @@ type type -'a defs = (* Definition sequence *) - Defs of ('a def) list +'a def = + DEF_aux of 'a def_aux * 'a annot type @@ -438,4 +433,9 @@ type CT_aux of 'a ctor_def_aux * 'a annot +type +'a defs = (* Definition sequence *) + Defs of ('a def) list + + |
