diff options
| -rw-r--r-- | language/l2.lem | 32 | ||||
| -rw-r--r-- | language/l2.ml | 32 | ||||
| -rw-r--r-- | language/l2.ott | 6 |
3 files changed, 36 insertions, 34 deletions
diff --git a/language/l2.lem b/language/l2.lem index 9691f21c..2d375340 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -138,9 +138,9 @@ type n_constraint = | NC_aux of n_constraint_aux * l -type quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) - | QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of n_constraint (* A constraint for this type *) +type quant_item_aux = (* kinded identifier or Nat constraint *) + | QI_id of kinded_id (* optionally kinded identifier *) + | QI_const of n_constraint (* Nat constraint *) type quant_item = @@ -149,7 +149,7 @@ type quant_item = type typquant_aux = (* type quantifiers and constraints *) | TypQ_tq of list quant_item - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + | TypQ_no_forall (* empty *) type lit_aux = (* Literal constant *) @@ -231,8 +231,8 @@ type reg_id_aux 'a = type exp_aux 'a = (* Expression *) - | E_block of list (exp 'a) (* block *) - | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *) + | E_block of list (exp 'a) (* sequential block *) + | E_nondet of list (exp 'a) (* nondeterministic block *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * (exp 'a) (* cast *) @@ -246,7 +246,7 @@ type exp_aux 'a = (* Expression *) | 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 *) - | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *) + | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update, with vector *) | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *) | E_list of list (exp 'a) (* list *) | E_cons of (exp 'a) * (exp 'a) (* cons *) @@ -256,10 +256,10 @@ type exp_aux 'a = (* Expression *) | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *) | E_let of (letbind 'a) * (exp 'a) (* let expression *) | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *) - | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) - | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) - | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) - | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) + | E_sizeof of nexp (* the value of nexp at run time *) + | E_return of (exp 'a) (* return (exp 'a) from current function *) + | E_exit of (exp 'a) (* halt all current execution *) + | E_assert of (exp 'a) * (exp 'a) (* halt with error (exp 'a) when not (exp 'a) *) | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of annot 'a (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *) @@ -276,8 +276,8 @@ and exp 'a = and lexp_aux 'a = (* lvalue expression *) | LEXP_id of id (* identifier *) | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *) - | LEXP_cast of typ * id - | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *) + | LEXP_cast of typ * id (* cast *) + | LEXP_tup of list (lexp 'a) (* multiple (non-memory) assignment *) | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *) | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *) | LEXP_field of (lexp 'a) * id (* struct field *) @@ -311,8 +311,8 @@ and pexp 'a = | Pat_aux of (pexp_aux 'a) * annot 'a and letbind_aux 'a = (* Let binding *) - | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *) - | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *) + | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *) + | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *) and letbind 'a = | LB_aux of (letbind_aux 'a) * annot 'a @@ -350,7 +350,7 @@ type tannot_opt_aux = (* Optional type annotation for functions *) | Typ_annot_opt_some of typquant * typ -type alias_spec_aux 'a = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) +type alias_spec_aux 'a = (* Register alias expression forms *) | AL_subreg of (reg_id 'a) * id | AL_bit of (reg_id 'a) * (exp 'a) | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a) diff --git a/language/l2.ml b/language/l2.ml index fff2e420..4043c8e6 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -141,9 +141,9 @@ n_constraint = type -quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) - QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of n_constraint (* A constraint for this type *) +quant_item_aux = (* kinded identifier or _ constraint *) + QI_id of kinded_id (* optionally kinded identifier *) + | QI_const of n_constraint (* _ constraint *) type @@ -154,7 +154,7 @@ quant_item = type typquant_aux = (* type quantifiers and constraints *) TypQ_tq of (quant_item) list - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) + | TypQ_no_forall (* empty *) type @@ -245,8 +245,8 @@ type 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 *) + E_block of ('a exp) list (* sequential block *) + | E_nondet of ('a exp) list (* nondeterministic block *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) | E_cast of typ * 'a exp (* cast *) @@ -260,7 +260,7 @@ type | E_vector_access of 'a exp * 'a exp (* vector access *) | E_vector_subrange of 'a exp * 'a exp * 'a exp (* subvector extraction *) | E_vector_update of 'a exp * 'a exp * 'a exp (* vector functional update *) - | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update (with vector) *) + | E_vector_update_subrange of 'a exp * 'a exp * 'a exp * 'a exp (* vector subrange update, with vector *) | E_vector_append of 'a exp * 'a exp (* vector concatenation *) | E_list of ('a exp) list (* list *) | E_cons of 'a exp * 'a exp (* cons *) @@ -270,10 +270,10 @@ type | E_case of 'a exp * ('a pexp) list (* pattern matching *) | E_let of 'a letbind * 'a exp (* let expression *) | E_assign of 'a lexp * 'a exp (* imperative assignment *) - | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *) - | E_exit of 'a exp (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *) - | E_return of 'a exp (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *) - | E_assert of 'a exp * 'a exp (* expression to halt with error, when the first expression is false, reporting the optional string as an error *) + | E_sizeof of nexp (* the value of nexp at run time *) + | E_return of 'a exp (* return 'a exp from current function *) + | E_exit of 'a exp (* halt all current execution *) + | E_assert of 'a exp * 'a exp (* halt with error 'a exp when not 'a exp *) | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *) @@ -290,8 +290,8 @@ and 'a exp = and 'a lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) | LEXP_memory of id * ('a exp) list (* memory or register write via function call *) - | LEXP_cast of typ * id - | LEXP_tup of ('a lexp) list (* set multiple at a time, a check will ensure it's not memory *) + | LEXP_cast of typ * id (* cast *) + | LEXP_tup of ('a lexp) list (* multiple (non-memory) assignment *) | LEXP_vector of 'a lexp * 'a exp (* vector element *) | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) | LEXP_field of 'a lexp * id (* struct field *) @@ -325,8 +325,8 @@ and 'a pexp = Pat_aux of 'a pexp_aux * 'a annot and 'a letbind_aux = (* Let binding *) - LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) - | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) + LB_val_explicit of typschm * 'a pat * 'a exp (* let, explicit type ('a pat must be total) *) + | LB_val_implicit of 'a pat * 'a exp (* let, implicit type ('a pat must be total) *) and 'a letbind = LB_aux of 'a letbind_aux * 'a annot @@ -372,7 +372,7 @@ tannot_opt_aux = (* Optional type annotation for functions *) type -'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *) +'a alias_spec_aux = (* Register alias expression forms *) 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 diff --git a/language/l2.ott b/language/l2.ott index f2603a05..a1690452 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -454,8 +454,8 @@ lit :: 'L_' ::= {{ com hex and bin are constant bit vectors, C-style }} | bin :: :: bin {{ com bit vector constant, C-style }} % Should undefined be of type bit[alpha] or alpha[beta] or just alpha? - | undefined :: :: undef {{ com constant representing undefined values }} | string :: :: string {{ com string constant }} + | undefined :: :: undef {{ com constant representing undefined values }} semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} {{ ocaml bool }} @@ -693,8 +693,10 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ com identifier }} | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }} | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} +{{ com sugared form of above where [[exp]] is an explicit tuple }} | ( typ ) id :: :: cast - | ( lexp0 , .. , lexpn ) :: :: tup {{ com set multiple at a time, a check will ensure it's not memory }} +{{ com cast }} + | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} | lexp [ exp ] :: :: vector {{ com vector element }} | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} % maybe comma-sep such lists too |