From 9538d030494bdfb07bdbd5c99ebb64a8fffe55e7 Mon Sep 17 00:00:00 2001 From: Peter Sewell Date: Wed, 17 Jul 2013 16:50:36 +0100 Subject: wib --- src/parse_ast.ml | 126 +++++++++++++++++++++++++++---------------------------- 1 file changed, 63 insertions(+), 63 deletions(-) (limited to 'src/parse_ast.ml') 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 @@ -58,6 +58,12 @@ base_kind_aux = (* base kind *) | BK_effects of terminal (* kind of effect sets *) +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 *) @@ -69,25 +75,19 @@ effect_aux = (* effect *) | Effect_nondet of terminal (* nondeterminism from intra-instruction parallelism *) -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 @@ -150,6 +150,11 @@ type | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +type +'a typquant = + TypQ_aux of 'a typquant_aux * 'a annot + + type lit_aux = (* Literal constant *) L_unit of terminal * 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 @@ -203,11 +208,6 @@ and 'a fpat = FP_aux of 'a fpat_aux * 'a annot -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?) *) @@ -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 @@ -380,6 +375,11 @@ type VS_aux of 'a val_spec_aux * 'a annot +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 *) @@ -395,11 +395,6 @@ type | DEF_scattered_end of terminal * id (* scattered definition end *) -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 $()$ *) @@ -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 + + -- cgit v1.2.3