diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 173 |
1 files changed, 90 insertions, 83 deletions
diff --git a/language/l2.lem b/language/l2.lem index 969a5bbf..4921c16b 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -75,6 +75,11 @@ type base_effect = | BE_aux of base_effect_aux * l +type id_aux = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) + + type effect_aux = (* effect set, of kind Effects *) | Effect_var of kid | Effect_set of list base_effect (* effect set *) @@ -86,9 +91,8 @@ type order_aux = (* vector order specifications, of kind Order *) | Ord_dec (* decreasing (big-endian) *) -type id_aux = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) +type id = + | Id_aux of id_aux * l type effect = @@ -98,10 +102,6 @@ type effect = type order = | Ord_aux of order_aux * l - -type id = - | Id_aux of id_aux * l - let effect_union e1 e2 = match (e1,e2) with | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l @@ -142,19 +142,6 @@ type typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* sugar, omitting quantifier and constraints *) -type lit_aux = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of integer (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_undef (* constant representing undefined values *) - | L_string of string (* string constant *) - - type typ_aux = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_id of id (* Defined type *) @@ -180,14 +167,31 @@ type typquant = | TypQ_aux of typquant_aux * l -type lit = - | L_aux of lit_aux * l +type lit_aux = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of integer (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_undef (* constant representing undefined values *) + | L_string of string (* string constant *) type typschm_aux = (* type scheme *) | TypSchm_ts of typquant * typ +type lit = + | L_aux of lit_aux * l + + +type typschm = + | TypSchm_aux of typschm_aux * l + + type pat_aux 'a = (* Pattern *) | P_lit of lit (* literal constant pattern *) | P_wild (* wildcard *) @@ -212,10 +216,6 @@ and fpat 'a = | FP_aux of (fpat_aux 'a) * annot 'a -type typschm = - | TypSchm_aux of typschm_aux * l - - type exp_aux 'a = (* Expression *) | E_block of list (exp 'a) (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -227,7 +227,7 @@ type exp_aux 'a = (* Expression *) | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *) | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *) | E_vector of list (exp 'a) (* vector (indexed from 0) *) - | E_vector_indexed of list (integer * (exp 'a)) (* vector (indexed consecutively) *) + | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *) | E_vector_access of (exp 'a) * (exp 'a) (* vector access *) | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *) | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *) @@ -269,6 +269,13 @@ and fexps_aux 'a = (* Field-expression list *) and fexps 'a = | FES_aux of (fexps_aux 'a) * annot 'a +and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *) + | Def_val_empty + | Def_val_dec of (exp 'a) + +and opt_default 'a = + | Def_val_aux of (opt_default_aux 'a) * annot 'a + and pexp_aux 'a = (* Pattern match *) | Pat_exp of (pat 'a) * (exp 'a) @@ -283,23 +290,14 @@ and letbind 'a = | LB_aux of (letbind_aux 'a) * annot 'a -type effect_opt_aux = (* Optional effect annotation for functions *) - | Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of effect - - type rec_opt_aux = (* Optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) -type funcl_aux 'a = (* Function clause *) - | FCL_Funcl of id * (pat 'a) * (exp 'a) - - -type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string +type effect_opt_aux = (* Optional effect annotation for functions *) + | Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect type type_union_aux = (* Type union constructors *) @@ -307,34 +305,43 @@ type type_union_aux = (* Type union constructors *) | Tu_ty_id of typ * id +type funcl_aux 'a = (* Function clause *) + | FCL_Funcl of id * (pat 'a) * (exp 'a) + + type tannot_opt_aux = (* Optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ -type effect_opt = - | Effect_opt_aux of effect_opt_aux * l +type name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string type rec_opt = | Rec_aux of rec_opt_aux * l -type funcl 'a = - | FCL_aux of (funcl_aux 'a) * l - - -type name_scm_opt = - | Name_sect_aux of name_scm_opt_aux * l +type effect_opt = + | Effect_opt_aux of effect_opt_aux * l type type_union = | Tu_aux of type_union_aux * l +type funcl 'a = + | FCL_aux of (funcl_aux 'a) * l + + type tannot_opt = | Typ_annot_opt_aux of tannot_opt_aux * l +type name_scm_opt = + | Name_sect_aux of name_scm_opt_aux * l + + type index_range_aux = (* index specification, for bitfields in register types *) | BF_single of integer (* single index *) | BF_range of integer * integer (* index range *) @@ -344,6 +351,10 @@ and index_range = | BF_aux of index_range_aux * l +type dec_spec_aux 'a = (* Register declarations *) + | DEC_reg of typ * id + + type scattered_def_aux 'a = (* Function and type union definitions that can be spread across a file. Each one must end in $id$ *) | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *) @@ -353,18 +364,6 @@ type scattered_def_aux 'a = (* Function and type union definitions that can be | SD_scattered_end of id (* scattered definition end *) -type type_def_aux 'a = (* Type definition body *) - | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) - | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) - | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) - | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) - - -type dec_spec_aux 'a = (* Register declarations *) - | DEC_reg of typ * id - - type fundef_aux 'a = (* Function definition *) | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a) @@ -374,24 +373,28 @@ type default_spec_aux 'a = (* Default kinding or typing assumption *) | DT_typ of typschm * id +type type_def_aux 'a = (* Type definition body *) + | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) + | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *) + | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *) + | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *) + | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) + + type val_spec_aux 'a = (* Value type specification *) | VS_val_spec of typschm * id | VS_extern_no_rename of typschm * id | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *) -type scattered_def 'a = - | SD_aux of (scattered_def_aux 'a) * annot 'a - - -type type_def 'a = - | TD_aux of (type_def_aux 'a) * annot 'a - - type dec_spec 'a = | DEC_aux of (dec_spec_aux 'a) * annot 'a +type scattered_def 'a = + | SD_aux of (scattered_def_aux 'a) * annot 'a + + type fundef 'a = | FD_aux of (fundef_aux 'a) * annot 'a @@ -400,6 +403,10 @@ type default_spec 'a = | DT_aux of (default_spec_aux 'a) * l +type type_def 'a = + | TD_aux of (type_def_aux 'a) * annot 'a + + type val_spec 'a = | VS_aux of (val_spec_aux 'a) * annot 'a @@ -440,6 +447,15 @@ let rec disjoint_all sets = end +type ne = (* internal numeric expressions *) + | Ne_var of x + | Ne_const of integer + | Ne_mult of ne * ne + | Ne_add of list ne + | Ne_exp of ne + | Ne_unary of ne + + type k = (* Internal kinds *) | Ki_typ | Ki_nat @@ -449,13 +465,11 @@ type k = (* Internal kinds *) | Ki_infer (* Representing an unknown kind, inferred by context *) -type ne = (* internal numeric expressions *) - | Ne_var of x - | Ne_const of integer - | Ne_mult of ne * ne - | Ne_add of list ne - | Ne_exp of ne - | Ne_unary of ne +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + | Nec_in of x * list integer type kinf = (* Whether a kind is default or from a local binding *) @@ -468,13 +482,6 @@ type tid = (* A type identifier or type variable *) | Tid_var of kid -type nec = (* Numeric expression constraints *) - | Nec_lteq of ne * ne - | Nec_eq of ne * ne - | Nec_gteq of ne * ne - | Nec_in of x * list integer - - type t = (* Internal types *) | T_id of x | T_var of x @@ -551,10 +558,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should -type I = inf +type E = env -type E = env +type I = inf |