diff options
Diffstat (limited to 'language/l2.ml')
| -rw-r--r-- | language/l2.ml | 62 |
1 files changed, 36 insertions, 26 deletions
diff --git a/language/l2.ml b/language/l2.ml index 60343397..a00e2f84 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -81,6 +81,12 @@ id_aux = (* Identifier *) type +effect_aux = (* effect set, of kind Effects *) + Effect_var of kid + | Effect_set of (base_effect) list (* effect set *) + + +type order_aux = (* vector order specifications, of kind Order *) Ord_var of kid (* variable *) | Ord_inc (* increasing (little-endian) *) @@ -88,24 +94,18 @@ order_aux = (* vector order specifications, of kind Order *) type -effect_aux = (* effect set, of kind Effects *) - Effect_var of kid - | Effect_set of (base_effect) list (* effect set *) - - -type id = Id_aux of id_aux * l type -order = - Ord_aux of order_aux * l +effect = + Effect_aux of effect_aux * l type -effect = - Effect_aux of effect_aux * l +order = + Ord_aux of order_aux * l type @@ -231,6 +231,11 @@ typschm = type +'a reg_id_aux = + RI_id of id + + +type 'a exp_aux = (* Expression *) E_block of ('a exp) list (* block *) | E_nondet of ('a exp) list (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) @@ -309,11 +314,8 @@ and 'a letbind = type -'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) - AL_subreg of id * id (* id must refer to a register, id' to a declared subregister of id *) - | AL_bit of id * 'a exp - | AL_slice of id * 'a exp * 'a exp - | AL_concat of id * id (* both id and id' must refer to a register *) +'a reg_id = + RI_aux of 'a reg_id_aux * 'a annot type @@ -351,8 +353,11 @@ rec_opt_aux = (* Optional recursive annotation for functions *) type -'a alias_spec = - AL_aux of 'a alias_spec_aux * 'a annot +'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) + AL_subreg of 'a reg_id * id + | AL_bit of 'a reg_id * 'a exp + | AL_slice of 'a reg_id * 'a exp * 'a exp + | AL_concat of 'a reg_id * 'a reg_id type @@ -396,10 +401,8 @@ and index_range = type -'a dec_spec_aux = (* Register declarations *) - DEC_reg of typ * id - | DEC_alias of id * 'a alias_spec - | DEC_typ_alias of typ * id * 'a alias_spec +'a alias_spec = + AL_aux of 'a alias_spec_aux * 'a annot type @@ -433,6 +436,13 @@ type type +'a dec_spec_aux = (* Register declarations *) + DEC_reg of typ * id + | DEC_alias of id * 'a alias_spec + | DEC_typ_alias of typ * id * 'a alias_spec + + +type 'a val_spec_aux = (* Value type specification *) VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id @@ -440,11 +450,6 @@ type type -'a dec_spec = - DEC_aux of 'a dec_spec_aux * 'a annot - - -type 'a scattered_def = SD_aux of 'a scattered_def_aux * 'a annot @@ -465,6 +470,11 @@ type type +'a dec_spec = + DEC_aux of 'a dec_spec_aux * 'a annot + + +type 'a val_spec = VS_aux of 'a val_spec_aux * 'a annot |