wib

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