diff options
Diffstat (limited to 'language/l2.lem')
| -rw-r--r-- | language/l2.lem | 87 |
1 files changed, 47 insertions, 40 deletions
diff --git a/language/l2.lem b/language/l2.lem index 926706a0..79cb82b3 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -1,4 +1,5 @@ (* generated by Ott 0.22 from: l2.ott *) +open import Pervasives open import Map open import Maybe @@ -21,20 +22,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 *) @@ -45,6 +42,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 *) @@ -55,11 +56,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 @@ -67,6 +63,11 @@ type nexp_constraint = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of id * list nat +type kinded_id = (* optionally kind-annotated identifier *) + | KOpt_none of id (* identifier *) + | KOpt_kind of kind * id (* kind-annotated variable *) + + type effects = (* effect set, of kind $Effects$ *) | Effects_var of id | Effects_set of list efct (* effect set *) @@ -83,6 +84,19 @@ 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 lit = (* Literal constant *) + | L_unit (* $() : unit$ *) + | L_zero (* $bitzero : bit$ *) + | L_one (* $bitone : bit$ *) + | L_true (* $true : bool$ *) + | L_false (* $false : bool$ *) + | L_num of nat (* 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 = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) | Typ_var of id (* Type variable *) @@ -97,19 +111,6 @@ and typ_arg = (* Type constructor arguments of all kinds *) | Typ_arg_effects of effects -type lit = (* Literal constant *) - | L_unit (* $() : unit$ *) - | L_zero (* $bitzero : bit$ *) - | L_one (* $bitone : bit$ *) - | L_true (* $true : bool$ *) - | L_false (* $false : bool$ *) - | L_num of nat (* 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 typquant = (* type quantifiers and constraints *) | TypQ_tq of list quant_item | TypQ_no_forall (* sugar, omitting quantifier and constraints *) @@ -142,7 +143,7 @@ type exp = (* Expression *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * exp (* cast *) - | E_app of exp * list exp (* function application *) + | E_app of id * list exp (* function application *) | E_app_infix of exp * id * exp (* infix function application *) | E_tuple of list exp (* tuple *) | E_if of exp * exp * exp (* conditional *) @@ -183,10 +184,6 @@ and letbind = (* Let binding *) | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) -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 @@ -201,6 +198,15 @@ 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 type_union = (* Type union constructors *) + | Tu_id of id + | Tu_ty_id of typ * id + + type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *) | Name_sect_none | Name_sect_some of string @@ -212,24 +218,25 @@ type index_range = (* index specification, for bitfields in register types *) | BF_concat of index_range * index_range (* concatenation of index ranges *) -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 + | 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 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 - | 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 default_typing_spec = (* Default kinding or typing assumption *) + | DT_kind of base_kind * id + | DT_typ of typschm * id type type_def = (* Type definition body *) | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) - | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *) + | TD_variant of id * naming_scheme_opt * typquant * list type_union * bool (* union type definition *) | TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *) | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *) @@ -257,7 +264,7 @@ type typ_lib = (* library types and syntactic sugar for them *) | Typ_lib_bool (* booleans $true$ and $false$ *) | Typ_lib_bit (* pure bit values (not mutable bits) *) | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string of string (* UTF8 strings *) + | Typ_lib_string (* UTF8 strings *) | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) |