Updated syntax with working examples

5 files changed, 256 insertions, 205 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 79cb82b3..da806b57 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -22,11 +22,6 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
 type base_kind =  (* base kind *)
  | BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
@@ -34,18 +29,28 @@ type base_kind =  (* base kind *)
  | BK_effects (* kind of effect sets *)
 
 
+type id =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type var =  (* variables with kind, ticked to differntiate from program variables *)
+ | Var of x
+
+
+type kind =  (* kinds *)
+ | K_kind of list base_kind
+
+
 type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
  | Nexp_id of id (* identifier *)
+ | Nexp_var of var (* variable *)
  | Nexp_constant of nat (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | 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 *)
@@ -56,6 +61,11 @@ type efct =  (* effect *)
  | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
+type kinded_id =  (* optionally kind-annotated identifier *)
+ | KOpt_none of var (* identifier *)
+ | KOpt_kind of kind * var (* kind-annotated variable *)
+
+
 type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
@@ -63,22 +73,19 @@ 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 *)
-
-
 type order =  (* vector order specifications, of kind $Order$ *)
  | Ord_id of id (* identifier *)
+ | Ord_var of var (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
+type effects =  (* effect set, of kind $Effects$ *)
+ | Effects_id of id
+ | Effects_var of var
+ | Effects_set of list efct (* effect set *)
+
+
 type quant_item =  (* Either a kinded identifier or a nexp constraint for a typquant *)
  | QI_id of kinded_id (* An optionally kinded identifier *)
  | QI_const of nexp_constraint (* A constraint for this type *)
@@ -99,7 +106,8 @@ type lit =  (* Literal constant *)
 
 type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
- | Typ_var of id (* Type variable *)
+ | Typ_id of id (* Defined type *)
+ | Typ_var of var (* Type variable *)
  | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *)
  | Typ_tup of list typ (* Tuple type *)
  | Typ_app of id * list typ_arg (* type constructor application *)
@@ -184,15 +192,15 @@ and letbind =  (* Let binding *)
  | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
 
 
-type funcl =  (* Function clause *)
- | FCL_Funcl of id * pat * exp
-
-
 type effects_opt =  (* Optional effect annotation for functions *)
  | Effects_opt_pure (* sugar for empty effect set *)
  | Effects_opt_effects of effects
 
 
+type funcl =  (* Function clause *)
+ | FCL_Funcl of id * pat * exp
+
+
 type rec_opt =  (* Optional recursive annotation for functions *)
  | Rec_nonrec (* non-recursive *)
  | Rec_rec (* recursive *)
@@ -218,21 +226,21 @@ type index_range =  (* index specification, for bitfields in register types *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
 
-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 default_typing_spec =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
+ | DT_kind of base_kind * var
  | 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 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 *)
@@ -264,7 +272,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 (* UTF8 strings *)
+ | Typ_lib_string of 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} *)
diff --git a/language/l2.ml b/language/l2.ml
index 6ecf3411..00c59136 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -20,8 +20,8 @@ base_kind_aux =  (* base kind *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
+var_aux =  (* variables with kind, ticked to differntiate from program variables *)
+   Var of x
 
 
 type 
@@ -31,8 +31,13 @@ id_aux =  (* Identifier *)
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
+base_kind = 
+   BK_aux of base_kind_aux * l
+
+
+type 
+var = 
+   Var_aux of var_aux * l
 
 
 type 
@@ -41,13 +46,14 @@ id =
 
 
 type 
-kind = 
-   K_aux of kind_aux * l
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
 
 
 type 
 nexp_aux =  (* expression of kind $_$, for vector sizes and origins *)
    Nexp_id of id (* identifier *)
+ | Nexp_var of var (* variable *)
  | Nexp_constant of int (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
@@ -58,9 +64,8 @@ and nexp =
 
 
 type 
-kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+kind = 
+   K_aux of kind_aux * l
 
 
 type 
@@ -72,6 +77,22 @@ nexp_constraint_aux =  (* constraint over kind $_$ *)
 
 
 type 
+kinded_id_aux =  (* optionally kind-annotated identifier *)
+   KOpt_none of var (* identifier *)
+ | KOpt_kind of kind * var (* kind-annotated variable *)
+
+
+type 
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -83,13 +104,9 @@ efct_aux =  (* effect *)
 
 
 type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
-
-
-type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
+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 nexp_constraint (* A constraint for this type *)
 
 
 type 
@@ -98,27 +115,29 @@ efct =
 
 
 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 nexp_constraint (* A constraint for this type *)
+quant_item = 
+   QI_aux of quant_item_aux * l
 
 
 type 
 effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
+   Effects_id of id
+ | Effects_var of var
  | Effects_set of (efct) list (* effect set *)
 
 
 type 
 order_aux =  (* vector order specifications, of kind $_$ *)
    Ord_id of id (* identifier *)
+ | Ord_var of var (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
 type 
-quant_item = 
-   QI_aux of quant_item_aux * l
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
@@ -132,12 +151,6 @@ order =
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type 
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)
@@ -152,9 +165,15 @@ lit_aux =  (* Literal constant *)
 
 
 type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
 typ_aux =  (* Type expressions, of kind $_$ *)
    Typ_wild (* Unspecified type *)
- | Typ_var of id (* Type variable *)
+ | Typ_id of id (* Defined type *)
+ | Typ_var of var (* Type variable *)
  | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *)
  | Typ_tup of (typ) list (* Tuple type *)
  | Typ_app of id * (typ_arg) list (* type constructor application *)
@@ -173,11 +192,6 @@ and typ_arg =
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
 lit = 
    L_aux of lit_aux * l
 
@@ -218,7 +232,38 @@ typschm =
 
 
 type 
-'a letbind_aux =  (* Let binding *)
+'a exp = 
+   E_aux of 'a exp_aux * 'a annot
+
+and 'a lexp_aux =  (* lvalue expression *)
+   LEXP_id of id (* identifier *)
+ | LEXP_memory of id * 'a exp (* memory write via function call *)
+ | 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 *)
+
+and 'a lexp = 
+   LEXP_aux of 'a lexp_aux * 'a annot
+
+and 'a fexp_aux =  (* Field-expression *)
+   FE_Fexp of id * 'a exp
+
+and 'a fexp = 
+   FE_aux of 'a fexp_aux * 'a annot
+
+and 'a fexps_aux =  (* Field-expression list *)
+   FES_Fexps of ('a fexp) list * bool
+
+and 'a fexps = 
+   FES_aux of 'a fexps_aux * 'a annot
+
+and 'a pexp_aux =  (* Pattern match *)
+   Pat_exp of 'a pat * 'a exp
+
+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) *)
 
@@ -250,42 +295,27 @@ and 'a exp_aux =  (* Expression *)
  | E_let of 'a letbind * 'a exp (* let expression *)
  | E_assign of 'a lexp * 'a exp (* imperative assignment *)
 
-and 'a exp = 
-   E_aux of 'a exp_aux * 'a annot
-
-and 'a lexp_aux =  (* lvalue expression *)
-   LEXP_id of id (* identifier *)
- | LEXP_memory of id * 'a exp (* memory write via function call *)
- | 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 *)
-
-and 'a lexp = 
-   LEXP_aux of 'a lexp_aux * 'a annot
-
-and 'a fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * 'a exp
 
-and 'a fexp = 
-   FE_aux of 'a fexp_aux * 'a annot
+type 
+'a effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
 
-and 'a fexps_aux =  (* Field-expression list *)
-   FES_Fexps of ('a fexp) list * bool
 
-and 'a fexps = 
-   FES_aux of 'a fexps_aux * 'a annot
+type 
+'a tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_some of typquant * typ
 
-and 'a pexp_aux =  (* Pattern match *)
-   Pat_exp of 'a pat * 'a exp
 
-and 'a pexp = 
-   Pat_aux of 'a pexp_aux * 'a annot
+type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-type_union_aux =  (* Type union constructors *)
-   Tu_id of id
- | Tu_ty_id of typ * id
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
@@ -295,25 +325,29 @@ naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for va
 
 
 type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+type_union_aux =  (* Type union constructors *)
+   Tu_id of id
+ | Tu_ty_id of typ * id
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
 
 
 type 
-'a tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_some of typquant * typ
+'a tannot_opt = 
+   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
 
 
 type 
-'a effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
+
+
+type 
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
 
 
 type 
@@ -327,40 +361,18 @@ and index_range =
 
 
 type 
-type_union = 
-   Tu_aux of type_union_aux * l
-
-
-type 
 naming_scheme_opt = 
    Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
-
-
-type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
-
-
-type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
-
-
-type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
+type_union = 
+   Tu_aux of type_union_aux * l
 
 
 type 
-'a val_spec_aux =  (* 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 *)
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
 
 
 type 
@@ -373,19 +385,21 @@ type
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * var
+ | DT_typ of typschm * id
 
 
 type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
+'a val_spec_aux =  (* 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 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
@@ -394,13 +408,13 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a default_typing_spec = 
+   DT_aux of 'a default_typing_spec_aux * 'a annot
 
 
 type 
-'a default_typing_spec = 
-   DT_aux of 'a default_typing_spec_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
 
 
 type 
@@ -424,7 +438,7 @@ type
  | Typ_lib_bool (* booleans $_$ and $_$ *)
  | Typ_lib_bit (* pure bit values (not mutable bits) *)
  | Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string (* UTF8 strings *)
+ | Typ_lib_string of 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} *)
diff --git a/language/l2.ott b/language/l2.ott
index e28e0271..9c801336 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -129,7 +129,11 @@ id :: '' ::=
 % We don't enforce a lexical convention on infix operators, as some of the 
 % targets use alphabetical infix operators. 
 
-
+var :: '' ::=
+  {{ com variables with kind, ticked to differntiate from program variables }}
+  {{ aux _ l }}
+  | ' x                       :: :: var
+ 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Kinds and Types                                              %
@@ -157,6 +161,7 @@ nexp :: 'Nexp_' ::=
   {{ com expression of kind $[[Nat]]$, for vector sizes and origins }}
   {{ aux _ l }}
   | id                                  :: :: id          {{ com identifier }}
+  | var                                 :: :: var         {{ com variable }}
   | num                                 :: :: constant     {{ com constant }}
   | nexp1 * nexp2                       :: :: times        {{ com product }}
 %{{ com must be linear after normalisation... except for the type of *, ahem }}
@@ -168,6 +173,7 @@ order :: 'Ord_' ::=
   {{ com vector order specifications, of kind $[[Order]]$}}
   {{ aux _ l }} 
   | id                                  :: :: id  {{ com identifier }}
+  | var                                 :: :: var {{ com variable }} 
   | inc                                 :: :: inc  {{ com increasing (little-endian) }}
   | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
   | ( order )                             :: S :: paren {{ ichlo [[order]] }}
@@ -187,7 +193,8 @@ efct :: 'Effect_' ::=
 effects :: 'Effects_' ::=
   {{ com effect set, of kind $[[Effects]]$ }}
   {{ aux _ l }}
- | effect id                                  :: :: var
+ | effect id                                  :: :: id
+ | effect var                                 :: :: var
  | effect { efct1 , .. , efctn }           :: :: set {{ com effect set }}
  | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ ichlo [] }}
  | effects1 u+ .. u+ effectsn                   :: M :: union {{ com meta operation for combining sets of effects }} {{ ichlo [] }}
@@ -199,7 +206,9 @@ typ :: 'Typ_' ::=
   {{ aux _ l }}
   | _                                           :: :: wild
     {{ com Unspecified type }}
-  | id                                         :: :: var
+  | id                                         :: :: id
+    {{ com Defined type }}
+  | var                                         :: :: var
     {{ com Type variable }}
   | typ1 -> typ2 effects                        :: :: fn
     {{ com Function type (first-order only in user code) }}
@@ -226,12 +235,12 @@ typ_lib :: 'Typ_lib_' ::=
   {{ com library types and syntactic sugar for them }}
   {{ aux _ l }} {{ auxparam 'a }}
 % boring base types:
-  | Unit :: :: unit {{ com unit type with value $()$ }}
-  | Bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
-  | Bit :: :: bit  {{ com pure bit values (not mutable bits) }}
+  | unit :: :: unit {{ com unit type with value $()$ }}
+  | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
+  | bit :: :: bit  {{ com pure bit values (not mutable bits) }}
 % experimentally trying with two distinct types of bool and bit ...
-  | Nat :: :: nat {{ com natural numbers 0,1,2,... }}
-  | String :: :: string {{ com UTF8 strings }}
+  | nat :: :: nat {{ com natural numbers 0,1,2,... }}
+  | string :: :: string {{ com UTF8 strings }}
 % finite subranges of nat
   | Enum nexp1 nexp2 order :: :: enum  {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }}
   | [ nexp ]             :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }}
@@ -275,8 +284,8 @@ nexp_constraint :: 'NC_' ::=
 kinded_id :: 'KOpt_' ::=
   {{ com optionally kind-annotated identifier }}
   {{ aux _ l }}
-  | id	 	    		   	      :: :: none {{ com identifier }}
-  | kind id				      :: :: kind {{ com kind-annotated variable }}
+  | var	 	    		   	      :: :: none {{ com identifier }}
+  | kind var				      :: :: kind {{ com kind-annotated variable }}
 
 quant_item :: 'QI_' ::=
   {{ com Either a kinded identifier or a nexp constraint for a typquant }}
@@ -763,7 +772,7 @@ val_spec :: 'VS_' ::=
 default_typing_spec :: 'DT_' ::=
   {{ com Default kinding or typing assumption }}
   {{ aux _ annot }} {{ auxparam 'a }}
-  | default base_kind id    :: :: kind
+  | default base_kind var    :: :: kind
   | default typschm id      :: :: typ
 % The intended semantics of these is that if an id in binding position
 % doesn't have a kind or type annotation, then we look through the
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index 990166c4..b196f007 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -25,6 +25,17 @@ base_kind_aux =  (* base kind *)
 
 
 type 
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type 
+var_aux =  (* variables with kind, ticked to differntiate from program variables *)
+   Var of x
+
+
+type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -36,24 +47,23 @@ efct_aux =  (* effect *)
 
 
 type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
+base_kind = 
+   BK_aux of base_kind_aux * l
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
+id = 
+   Id_aux of id_aux * l
 
 
 type 
-efct = 
-   Effect_aux of efct_aux * l
+var = 
+   Var_aux of var_aux * l
 
 
 type 
-id = 
-   Id_aux of id_aux * l
+efct = 
+   Effect_aux of efct_aux * l
 
 
 type 
@@ -64,6 +74,7 @@ kind_aux =  (* kinds *)
 type 
 atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *)
    ATyp_id of id (* identifier *)
+ | ATyp_var of var (* ticked variable *)
  | ATyp_constant of int (* constant *)
  | ATyp_times of atyp * atyp (* product *)
  | ATyp_sum of atyp * atyp (* sum *)
@@ -71,6 +82,7 @@ atyp_aux =  (* expressions of all kinds, to be translated to types, nats, orders
  | ATyp_inc (* increasing (little-endian) *)
  | ATyp_dec (* decreasing (big-endian) *)
  | ATyp_efid of id
+ | ATyp_efvar of var
  | ATyp_set of (efct) list (* effect set *)
  | ATyp_wild (* Unspecified type *)
  | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *)
@@ -96,8 +108,8 @@ nexp_constraint_aux =  (* constraint over kind $_$ *)
 
 type 
 kinded_id_aux =  (* optionally kind-annotated identifier *)
-   KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+   KOpt_none of var (* identifier *)
+ | KOpt_kind of kind * var (* kind-annotated variable *)
 
 
 type 
@@ -128,6 +140,11 @@ typquant_aux =  (* type quantifiers and constraints *)
 
 
 type 
+typquant = 
+   TypQ_aux of typquant_aux * l
+
+
+type 
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)
@@ -142,8 +159,8 @@ lit_aux =  (* Literal constant *)
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * atyp
 
 
 type 
@@ -152,8 +169,8 @@ lit =
 
 
 type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * atyp
+typschm = 
+   TypSchm_aux of typschm_aux * l
 
 
 type 
@@ -182,11 +199,6 @@ and fpat =
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
-
-
-type 
 exp_aux =  (* Expression *)
    E_block of (exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -242,27 +254,21 @@ and letbind =
 
 
 type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
-
-
-type 
 type_union_aux =  (* Type union constructors *)
    Tu_id of id
  | Tu_ty_id of atyp * id
 
 
 type 
-tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_none
- | Typ_annot_opt_some of typquant * atyp
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
 
 
 type 
-effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of atyp
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * atyp
 
 
 type 
@@ -277,8 +283,14 @@ funcl_aux =  (* Function clause *)
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of atyp
+
+
+type 
+type_union = 
+   Tu_aux of type_union_aux * l
 
 
 type 
@@ -292,8 +304,8 @@ and index_range =
 
 
 type 
-type_union = 
-   Tu_aux of type_union_aux * l
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
@@ -302,11 +314,6 @@ tannot_opt =
 
 
 type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
-
-
-type 
 rec_opt = 
    Rec_aux of rec_opt_aux * l
 
@@ -317,10 +324,8 @@ funcl =
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
@@ -334,7 +339,7 @@ type_def_aux =  (* Type definition body *)
 
 type 
 default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
+   DT_kind of base_kind * var
  | DT_typ of typschm * id
 
 
@@ -344,8 +349,10 @@ fundef_aux =  (* Function definition *)
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string
 
 
 type 
@@ -364,6 +371,11 @@ fundef =
 
 
 type 
+val_spec = 
+   VS_aux of val_spec_aux * l
+
+
+type 
 def_aux =  (* Top-level definition *)
    DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 6876fcfa..f96c3f99 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -118,6 +118,12 @@ id :: '' ::=
   | x                           :: :: id
   | ( deinfix x )                       :: :: deIid {{ com remove infix status }}
 
+
+var :: '' ::=
+  {{ com variables with kind, ticked to differntiate from program variables }}
+  {{ aux _ l }}
+  | ' x                       :: :: var
+
 % Note: we have just a single namespace. We don't want the same
 % identifier to be reused as a type name or variable, expression
 % variable, and field name.  We don't enforce any lexical convention
@@ -162,6 +168,7 @@ atyp :: 'ATyp_' ::=
   {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }}
   {{ aux _ l }}
   | id                                  :: :: id          {{ com identifier }}
+  | var                                 :: :: var         {{ com ticked variable }}
   | num                                 :: :: constant     {{ com constant }}
   | atyp1 * atyp2                       :: :: times        {{ com product }}
   | atyp1 + atyp2                       :: :: sum          {{ com sum }}
@@ -171,6 +178,7 @@ atyp :: 'ATyp_' ::=
   | inc                                 :: :: inc  {{ com increasing (little-endian) }}
   | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
   | effect id                            :: :: efid
+  | effect var                           :: :: efvar
   | effect { efct1 , .. , efctn }           :: :: set {{ com effect set }}
   | pure                                 :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }}
 
@@ -237,8 +245,8 @@ nexp_constraint :: 'NC_' ::=
 kinded_id :: 'KOpt_' ::=
   {{ com optionally kind-annotated identifier }}
   {{ aux _ l }}
-  | id	 	    		   	      :: :: none {{ com identifier }}
-  | kind id				      :: :: kind {{ com kind-annotated variable }}
+  | var	 	    		   	      :: :: none {{ com identifier }}
+  | kind var				      :: :: kind {{ com kind-annotated variable }}
 
 quant_item :: 'QI_' ::=
   {{ com Either a kinded identifier or a nexp constraint for a typquant }}
@@ -682,7 +690,7 @@ default_typing_spec :: 'DT_' ::=
   {{ com Default kinding or typing assumption }}
   {{ aux _ l }}
 %  {{ aux _ annot }} {{ auxparam 'a }}
-  | default base_kind id    :: :: kind
+  | default base_kind var    :: :: kind
   | default typschm id      :: :: typ
 % The intended semantics of these is that if an id in binding position
 % doesn't have a kind or type annotation, then we look through the