diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 130 |
1 files changed, 70 insertions, 60 deletions
diff --git a/language/l2.lem b/language/l2.lem index 51bad620..90974dfc 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -32,20 +32,16 @@ val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) -type base_kind = (* base kind *) - | BK_type (* kind of types *) - | BK_nat (* kind of natural number size expressions *) - | BK_order (* kind of vector order specifications *) - | BK_effects (* kind of effect sets *) - - type id = (* Identifier *) | Id of x | DeIid of x (* remove infix status *) -type kind = (* kinds *) - | K_kind of list base_kind +type base_kind = (* base kind *) + | BK_type (* kind of types *) + | BK_nat (* kind of natural number size expressions *) + | BK_order (* kind of vector order specifications *) + | BK_effects (* kind of effect sets *) type nexp = (* expression of kind $Nat$, for vector sizes and origins *) @@ -56,6 +52,10 @@ type nexp = (* expression of kind $Nat$, for vector sizes and origins *) | Nexp_exp of nexp (* exponential *) +type kind = (* kinds *) + | K_kind of list base_kind + + type efct = (* effect *) | Effect_rreg (* read register *) | Effect_wreg (* write register *) @@ -66,11 +66,6 @@ type efct = (* effect *) | Effect_nondet (* nondeterminism from intra-instruction parallelism *) -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - type nexp_constraint = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -78,6 +73,11 @@ type nexp_constraint = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of id * list num +type kinded_id = (* optionally kind-annotated identifier *) + | KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) + + type order = (* vector order specifications, of kind $Order$ *) | Ord_id of id (* identifier *) | Ord_inc (* increasing (little-endian) *) @@ -94,6 +94,15 @@ type quant_item = (* Either a kinded identifier or a nexp constraint for a typq | QI_const of nexp_constraint (* A constraint for this type *) +type ne = (* internal numeric expressions *) + | Ne_var of id + | Ne_const of num + | Ne_mult of ne * ne + | Ne_add of list ne + | Ne_exp of ne + | Ne_unary of ne + + type typ = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_var of id (* Type variable *) @@ -108,6 +117,11 @@ and typ_arg = (* Type constructor arguments of all kinds *) | Typ_arg_effects of effects +type typquant = (* type quantifiers and constraints *) + | TypQ_tq of list quant_item + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + + type lit = (* Literal constant *) | L_unit (* $() : unit$ *) | L_zero (* $bitzero : bit$ *) @@ -121,9 +135,14 @@ type lit = (* Literal constant *) | L_string of string (* string constant *) -type typquant = (* type quantifiers and constraints *) - | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +type nec = (* Numeric expression constraints *) + | Nec_lteq of ne * ne + | Nec_eq of ne * ne + | Nec_gteq of ne * ne + + +type typschm = (* type scheme *) + | TypSchm_ts of typquant * typ type pat = (* Pattern *) @@ -144,19 +163,6 @@ and fpat = (* Field pattern *) | FP_Fpat of id * pat -type typschm = (* type scheme *) - | TypSchm_ts of typquant * typ - - -type ne = (* internal numeric expressions *) - | Ne_var of id - | Ne_const of num - | Ne_mult of ne * ne - | Ne_add of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - type exp = (* Expression *) | E_block of list exp (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) @@ -203,18 +209,15 @@ and letbind = (* Let binding *) | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) -type k = (* Internal kinds *) - | Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_val (* Representing values, for use in identifier checks *) - | Ki_ctor of list k * k - | Ki_infer (* Representing an unknown kind, inferred by context *) +type index_range = (* index specification, for bitfields in register types *) + | BF_single of num (* single index *) + | BF_range of num * num (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) -type tannot_opt = (* Optional type annotation for functions *) - | Typ_annot_opt_some of typquant * typ +type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) + | Name_sect_none + | Name_sect_some of string type effects_opt = (* Optional effect annotation for functions *) @@ -227,23 +230,31 @@ type rec_opt = (* Optional recursive annotation for functions *) | Rec_rec (* recursive *) +type tannot_opt = (* Optional type annotation for functions *) + | Typ_annot_opt_some of typquant * typ + + type funcl = (* Function clause *) | FCL_Funcl of id * pat * exp -type index_range = (* index specification, for bitfields in register types *) - | BF_single of num (* single index *) - | BF_range of num * num (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) +type k = (* Internal kinds *) + | Ki_typ + | Ki_nat + | Ki_ord + | Ki_efct + | Ki_val (* Representing values, for use in identifier checks *) + | Ki_ctor of list k * k + | Ki_infer (* Representing an unknown kind, inferred by context *) -type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) - | Name_sect_none - | Name_sect_some of string +type default_typing_spec = (* Default kinding or typing assumption *) + | DT_kind of base_kind * id + | DT_typ of typschm * id -type fundef = (* Function definition *) - | FD_function of rec_opt * tannot_opt * effects_opt * list funcl +type val_spec = (* Value type specification *) + | VS_val_spec of typschm * id type type_def = (* Type definition body *) @@ -254,13 +265,8 @@ type type_def = (* Type definition body *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) -type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * id - | DT_typ of typschm * id - - -type val_spec = (* Value type specification *) - | VS_val_spec of typschm * id +type fundef = (* Function definition *) + | FD_function of rec_opt * tannot_opt * effects_opt * list funcl type def = (* Top-level definition *) @@ -277,6 +283,14 @@ type def = (* Top-level definition *) | DEF_scattered_end of id (* scattered definition end *) +type ts = + | Ts_lst of list t + + +type defs = (* Definition sequence *) + | Defs of list def + + type typ_lib = (* library types and syntactic sugar for them *) | Typ_lib_unit (* unit type with value $()$ *) | Typ_lib_bool (* booleans $true$ and $false$ *) @@ -294,8 +308,4 @@ type typ_lib = (* library types and syntactic sugar for them *) | Typ_lib_reg of typ (* mutable register components holding typ *) -type defs = (* Definition sequence *) - | Defs of list def - - |