Updated syntax with working examples

14 files changed, 458 insertions, 325 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
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 772df3e9..18a853d9 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -10,8 +10,15 @@ type 'a envs_out = 'a * envs
 let id_to_string (Id_aux(id,l)) =
   match id with | Id(x) | DeIid(x) -> x
 
+let var_to_string (Var_aux(Var v,l)) = v
+
 (*placeholder, write in type_internal*)
-let kind_to_string _ = " kind pp place holder "
+let kind_to_string kind = match kind.k with
+  | K_Nat -> "Nat"
+  | K_Typ -> "Type"
+  | K_Ord -> "Order"
+  | K_Efct -> "Effects"
+  | _ -> " kind pp place holder "
 
 let typquant_to_quantkinds k_env typquant = 
   match typquant with
@@ -25,29 +32,33 @@ let typquant_to_quantkinds k_env typquant =
           | QI_const _ -> rst
           | QI_id(ki) -> begin
             match ki with 
-            | KOpt_aux(KOpt_none(id),l) | KOpt_aux(KOpt_kind(_,id),l) -> 
-              (match Envmap.apply k_env (id_to_string id) with
+            | KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) -> 
+              (match Envmap.apply k_env (var_to_string v) with
               | Some(typ) -> typ::rst
               | None -> raise (Reporting_basic.err_unreachable l "Envmap didn't get an entry during typschm processing"))
           end)
         qlist
         [])
 
-let typ_error l msg opt_id opt_kind =
+let typ_error l msg opt_id opt_var opt_kind =
   raise (Reporting_basic.err_typ 
            l
            (msg ^
-              (match opt_id, opt_kind with
-              | Some(id),Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind)
-              | Some(id),None -> ": " ^ (id_to_string id)
-              | None,Some(kind) -> " " ^ (kind_to_string kind)
-              | None,None -> "")))
+              (match opt_id, opt_var, opt_kind with
+              | Some(id),None,Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind)
+              | Some(id),None,None -> ": " ^ (id_to_string id)
+              | None,Some(v),Some(kind) -> "'" ^ (var_to_string v) ^ " of " ^ (kind_to_string kind)
+              | None,Some(v),None -> ": '" ^ (var_to_string v)
+              | None,None,Some(kind) -> " " ^ (kind_to_string kind)
+              | _ -> "")))
                 
 let to_ast_id (Parse_ast.Id_aux(id,l)) =
     Id_aux( (match id with
              | Parse_ast.Id(x) -> Id(x)
              | Parse_ast.DeIid(x) -> DeIid(x)) , l)
 
+let to_ast_var (Parse_ast.Var_aux(Parse_ast.Var v,l)) = Var_aux(Var v,l)
+
 let to_ast_base_kind (Parse_ast.BK_aux(k,l')) =
   match k with
   | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ}
@@ -65,7 +76,7 @@ let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst),
           let ret,args = List.hd reverse_typs, List.rev (List.tl reverse_typs) in
           match ret.k with
           | K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) }
-          | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None
+          | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None
 
 let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
   match t with
@@ -76,10 +87,19 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
                 let mk = Envmap.apply k_env (id_to_string id) in
                 (match mk with
                 | Some(k) -> (match k.k with
-                              | K_Typ -> Typ_var id
-                              | K_infer -> k.k <- K_Typ; Typ_var id
-                              | _ -> typ_error l "Required a variable with kind Type, encountered " (Some id) (Some k))
-                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+                              | K_Typ -> Typ_id id
+                              | K_infer -> k.k <- K_Typ; Typ_id id
+                              | _ -> typ_error l "Required an identifier with kind Type, encountered " (Some id) None (Some k))
+                | None -> typ_error l "Encountered an unbound identifier" (Some id) None None)
+              | Parse_ast.ATyp_var(v) -> 
+                let v = to_ast_var v in
+                let mk = Envmap.apply k_env (var_to_string v) in
+                (match mk with
+                | Some(k) -> (match k.k with
+                              | K_Typ -> Typ_var v
+                              | K_infer -> k.k <- K_Typ; Typ_var v
+                              | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
               | Parse_ast.ATyp_wild -> Typ_wild
               | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env arg),
                                                            (to_ast_typ k_env ret),
@@ -93,10 +113,10 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ =
 		    if ((List.length args) = (List.length typs))
 		      then
 		      Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env k a)) args typs))
-		    else typ_error l "Type constructor given incorrect number of arguments" (Some id) None
-                  | None -> typ_error l "Required a type constructor, encountered an unbound variable" (Some id) None
-                  | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None)
-              | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None
+		    else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None
+                  | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None
+                  | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None)
+              | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None
     ), l)
 
 and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
@@ -110,8 +130,17 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
                 | Some(k) -> Nexp_aux((match k.k with
                                       | K_Nat -> Nexp_id id
                                       | K_infer -> k.k <- K_Nat; Nexp_id id
-                                      | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) (Some k)),l)
-                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+                                      | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) None (Some k)),l)
+                | None -> typ_error l "Encountered an unbound variable" (Some id) None None)
+    | Parse_ast.ATyp_var(v) ->                 
+                let v = to_ast_var v in
+                let mk = Envmap.apply k_env (var_to_string v) in
+                (match mk with
+                | Some(k) -> Nexp_aux((match k.k with
+                                      | K_Nat -> Nexp_var v
+                                      | K_infer -> k.k <- K_Nat; Nexp_var v
+                                      | _ -> typ_error l "Required a variable with kind Nat, encountered " None (Some v) (Some k)),l)
+                | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
     | Parse_ast.ATyp_constant(i) -> Nexp_aux(Nexp_constant(i),l)
     | Parse_ast.ATyp_sum(t1,t2) ->
       let n1 = to_ast_nexp k_env t1 in
@@ -128,7 +157,7 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
                           (Nexp_aux((Nexp_times(n1,n2)),l)))  (*TODO This needs just a portion of the l, think about adding a way to split*)
       in
       times_loop typs false
-    | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None)
+    | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None)
     
 and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order =
   match o with
@@ -141,11 +170,20 @@ and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order =
                 | Some(k) -> (match k.k with
                               | K_Ord -> Ord_id id
                               | K_infer -> k.k <- K_Ord; Ord_id id
-                              | _ -> typ_error l "Required a variable with kind Order, encountered " (Some id) (Some k))
-                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+                              | _ -> typ_error l "Required an identifier with kind Order, encountered " (Some id) None (Some k))
+                | None -> typ_error l "Encountered an unbound identifier" (Some id) None None)
+               | Parse_ast.ATyp_var(v) -> 
+                let v = to_ast_var v in
+                let mk = Envmap.apply k_env (var_to_string v) in
+                (match mk with
+                | Some(k) -> (match k.k with
+                              | K_Ord -> Ord_var v
+                              | K_infer -> k.k <- K_Ord; Ord_var v
+                              | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
                | Parse_ast.ATyp_inc -> Ord_inc
                | Parse_ast.ATyp_dec -> Ord_dec
-               | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None
+               | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None None
     ), l)
 
 and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects =
@@ -157,10 +195,19 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects =
                 let mk = Envmap.apply k_env (id_to_string id) in
                 (match mk with
                 | Some(k) -> (match k.k with
-                              | K_Efct -> Effects_var id
-                              | K_infer -> k.k <- K_Efct; Effects_var id
-                              | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) (Some k))
-                | None -> typ_error l "Encountered an unbound variable" (Some id) None)
+                              | K_Efct -> Effects_id id
+                              | K_infer -> k.k <- K_Efct; Effects_id id
+                              | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) None (Some k))
+                | None -> typ_error l "Encountered an unbound variable" (Some id) None None)
+               | Parse_ast.ATyp_efvar(v) ->  
+                let v = to_ast_var v in
+                let mk = Envmap.apply k_env (var_to_string v) in
+                (match mk with
+                | Some(k) -> (match k.k with
+                              | K_Efct -> Effects_var v
+                              | K_infer -> k.k <- K_Efct; Effects_var v
+                              | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k))
+                | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
                | Parse_ast.ATyp_set(effects) ->
                  Effects_set( List.map 
                              (fun efct -> match efct with
@@ -174,7 +221,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects =
                                | Parse_ast.Effect_unspec -> Effect_unspec
                                | Parse_ast.Effect_nondet -> Effect_nondet),l))
                              effects)
-               | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None
+               | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None
     ), l)
 
 and to_ast_typ_arg (k_env : kind Envmap.t) (kind : kind) (arg : Parse_ast.atyp) : Ast.typ_arg =
@@ -211,26 +258,26 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constrain
 (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *)
 let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t * kind Envmap.t =
   let opt_kind_to_ast k_env local_names local_env (Parse_ast.KOpt_aux(ki,l)) =
-    let id, key, kind, ktyp =
+    let v, key, kind, ktyp =
       match ki with
-      | Parse_ast.KOpt_none(id) ->
-	let id = to_ast_id id in
-	let key = id_to_string id in
+      | Parse_ast.KOpt_none(v) ->
+	let v = to_ast_var v in
+	let key = var_to_string v in
 	let kind,ktyp = if (Envmap.in_dom key k_env) then None,(Envmap.apply k_env key) else None,(Some{ k = K_infer }) in
-	id,key,kind, ktyp
-      | Parse_ast.KOpt_kind(k,id) ->
-	let id = to_ast_id id in
-	let key = id_to_string id in
+	v,key,kind, ktyp
+      | Parse_ast.KOpt_kind(k,v) ->
+	let v = to_ast_var v in
+	let key = var_to_string v in
 	let kind,ktyp = to_ast_kind k_env k in
-	id,key,Some(kind),Some(ktyp)
+	v,key,Some(kind),Some(ktyp)
     in
     if (Nameset.mem key local_names)
-    then typ_error l "Encountered duplicate name in type scheme" (Some id) None
+    then typ_error l "Encountered duplicate name in type scheme" None (Some v) None
     else 
       let local_names = Nameset.add key local_names in
       let kopt,k_env,k_env_local = (match kind,ktyp with
-        | Some(k),Some(kt) -> KOpt_kind(k,id), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
-	| None, Some(kt) -> KOpt_none(id), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
+        | Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
+	| None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt))
 	| _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom is true but apply gives None")) in
       KOpt_aux(kopt,l),k_env,local_names,local_env
   in
@@ -354,11 +401,11 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) -> 
       (match f with
       | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',to_ast_exp k_env exp)
-      | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None)
+      | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None)
     | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp)
     | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
     | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id)
-    | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None)
+    | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None)
       , (l,None))
 
 and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp =
@@ -376,7 +423,7 @@ and to_ast_fexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_as
                     | _  -> None)
                   | None,Some(l,msg) -> 
                     if fail_on_error
-                    then typ_error l msg None None
+                    then typ_error l msg None None None
                     else None
                   | _ -> None)
 
@@ -399,11 +446,11 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe
   match default with
   | Parse_ast.DT_aux(df,l) ->
     (match df with 
-    | Parse_ast.DT_kind(bk,id) ->
+    | Parse_ast.DT_kind(bk,v) ->
       let k,k_typ = to_ast_base_kind bk in
-      let id = to_ast_id id in
-      let key = id_to_string id in
-      DT_aux(DT_kind(k,id),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env)
+      let v = to_ast_var v in
+      let key = var_to_string v in
+      DT_aux(DT_kind(k,v),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env)
     | Parse_ast.DT_typ(typschm,id) ->
       let tps,_,_ = to_ast_typschm k_env typschm in
       DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
@@ -418,7 +465,10 @@ let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec
       VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env)
     | Parse_ast.VS_extern_spec(ts,id,s) ->
       let typsch,_,_ = to_ast_typschm k_env ts in
-      VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,None)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *)
+      VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,None)),(names,k_env,t_env)
+    | Parse_ast.VS_extern_no_rename(ts,id) ->
+      let typsch,_,_ = to_ast_typschm k_env ts in
+       VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,None)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *)
     
 
 let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = 
@@ -567,21 +617,21 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
       (match (def_in_progress id partial_defs) with
       | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in
                 (No_def,envs),((id,(partial_def,k_local))::partial_defs)
-      | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None)
+      | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
     | Parse_ast.DEF_scattered_funcl(funcl) -> 
       (match funcl with
       | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
         let id = to_ast_id id in
         (match (def_in_progress id partial_defs) with
-        | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None
+        | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
         | Some(d,k) ->
           (match !d with
           | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> 
             let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
             d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false);
             (No_def,envs),partial_defs
-          | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None
-          | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None)))
+          | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
+          | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
     | Parse_ast.DEF_scattered_variant(id,naming_scheme_opt,typquant) -> 
       let id = to_ast_id id in
       let name = to_ast_namescm naming_scheme_opt in
@@ -589,24 +639,24 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
       (match (def_in_progress id partial_defs) with
       | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in
                 (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs
-      | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None)
+      | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
     | Parse_ast.DEF_scattered_unioncl(id,typ,arm_id) -> 
       let id = to_ast_id id in
       let arm_id = to_ast_id arm_id in
       (match (def_in_progress id partial_defs) with
-      | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None
+      | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
       | Some(d,k) ->
         (match !d with
         | (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> 
           let typ = to_ast_typ k typ in
           d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[Tu_aux(Tu_ty_id (typ,arm_id), l)],false),tl)),dl),false);
           (No_def,envs),partial_defs
-        | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None
-        | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None))
+        | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
+        | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
     | Parse_ast.DEF_scattered_end(id) ->
       let id = to_ast_id id in
       (match (def_in_progress id partial_defs) with
-      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None
+      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
       | Some(d,k) ->
         (match !d with
         | (DEF_aux(DEF_type(_),_) as def),false ->
@@ -616,7 +666,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
           d:= (def,true);
           ((Finished def), envs),partial_defs
         | _, true -> 
-          typ_error l "Scattered definition ended multiple times" (Some id) None
+          typ_error l "Scattered definition ended multiple times" (Some id) None None
         | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type")))
     )
 
@@ -633,14 +683,14 @@ let rec to_ast_defs_helper envs partial_defs = function
                 | Some(d,k) -> 
                   if (snd !d) 
                   then (fst !d) :: defs, envs, partial_defs
-                  else typ_error l "Scattered type definition never ended" (Some id) None))                
+                  else typ_error l "Scattered type definition never ended" (Some id) None None))                
 
 let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : t Envmap.t) (Parse_ast.Defs(defs)) =
   let defs,_,partial_defs = to_ast_defs_helper (default_names,kind_env,typ_env) [] defs in
   List.iter 
     (fun (id,(d,k)) -> 
       (match !d with
-      | (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None
+      | (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None None
       | (_, true) -> ()))
     partial_defs;
   (Defs defs)
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 940a43bb..622bdbaa 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -92,6 +92,6 @@ let run (name, test) =
       eprintf "%s: action returned %s\n" name (val_to_string return);
       loop env' (resume test s return)
   | Error e -> eprintf "%s: error: %s\n" name e in
-  let entry = E_app(E_id(Id "main"), [E_lit L_unit]) in
+  let entry = E_app((Id "main"), [E_lit L_unit]) in
   loop (Reg.empty, Mem.empty) (interp test entry)
 ;;
diff --git a/src/lexer.mll b/src/lexer.mll
index 52be6084..80fd06f4 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -66,6 +66,7 @@ let kw_table =
      ("clause",                  (fun _ -> Clause));
      ("const",			 (fun _ -> Const));
      ("default",		 (fun _ -> Default));
+     ("deinfix",                 (fun _ -> Deinfix));
      ("effect",                  (fun _ -> Effect));
      ("Effects",                 (fun _ -> Effects));
      ("end",                     (fun _ -> End));
diff --git a/src/parser.mly b/src/parser.mly
index ba796347..572408ea 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -243,8 +243,10 @@ id:
 tid:
   | TyId
     { (idl (Id($1))) }
+
+tyvar:
   | TyVar
-    { (idl (Id($1))) }
+    { (Var_aux((Var($1)),loc ())) }
 
 atomic_kind:
   | TYPE
@@ -299,6 +301,8 @@ effect_typ:
 atomic_typ:
   | tid
     { tloc (ATyp_id $1) }
+  | tyvar
+    { tloc (ATyp_var $1) }
   | effect_typ
     { $1 }
   | Inc
@@ -319,6 +323,10 @@ vec_typ:
       { tloc (make_vector_sugar (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
   | tid Lsquare nexp_typ Colon nexp_typ Rsquare
       { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
+  | tyvar Lsquare nexp_typ Rsquare
+      { tloc (make_vector_sugar (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) }
+  | tyvar Lsquare nexp_typ Colon nexp_typ Rsquare
+      { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
 
 app_typs:
   | vec_typ
@@ -397,8 +405,8 @@ atomic_pat:
     { ploc P_wild }
   | Lparen pat As id Rparen
     { ploc (P_as($2,$4)) }
-  | Lparen Lparen typ Rparen atomic_pat Rparen
-    { ploc (P_typ($3,$5)) } 
+  | Lparen typ Rparen atomic_pat
+    { ploc (P_typ($2,$4)) } 
   | id
     { ploc (P_app($1,[])) }
   | Lcurly fpats Rcurly
@@ -844,13 +852,13 @@ funcl_ands:
 
 /* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/
 fun_def:
-  | Function_ Rec typquant atomic_typ effect_typ funcl_ands
+  | Function_ Rec typquant typ effect_typ funcl_ands
     { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
-  | Function_ Rec typquant atomic_typ funcl_ands
+  | Function_ Rec typquant typ funcl_ands
     { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec atomic_typ effect_typ funcl_ands
+  | Function_ Rec typ effect_typ funcl_ands
     { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
-  | Function_ Rec atomic_typ funcl_ands
+  | Function_ Rec typ funcl_ands
     { match $3 with
       | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
         funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $3 3, $4))
@@ -860,9 +868,9 @@ fun_def:
     { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) }
 */  | Function_ typquant atomic_typ effect_typ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
-  | Function_ typquant atomic_typ funcl_ands
+  | Function_ typquant typ funcl_ands
     { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
-  | Function_ atomic_typ funcl_ands
+  | Function_ typ funcl_ands
     { match $2 with
       | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) ->
         funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
@@ -873,9 +881,9 @@ fun_def:
 */
 
 val_spec:
-  | Val typquant atomic_typ id
+  | Val typquant typ id
     { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
-  | Val atomic_typ id
+  | Val typ id
     { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
   | Val Extern typquant atomic_typ id
     { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
@@ -887,9 +895,9 @@ val_spec:
     { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
 
 kinded_id:
-  | tid
+  | tyvar
     { kiloc (KOpt_none $1) }
-  | kind tid
+  | kind tyvar
     { kiloc (KOpt_kind($1,$2))}
 
 /*kinded_ids:
@@ -1020,12 +1028,12 @@ type_def:
     { tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
   | Typedef id name_sect Eq Enumerate Lcurly enum_body Rcurly
     { tdloc (TD_enum($2,$3,$7,false)) }
-  | Typedef id Eq Register Bits Lsquare typ Colon typ Rsquare Lcurly r_def_body Rcurly
+  | Typedef id Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
     { tdloc (TD_register($2, $7, $9, $12)) }
 
 
 default_typ:
-  | Default atomic_kind id
+  | Default atomic_kind tyvar
     { defloc (DT_kind($2,$3)) }
   | Default typquant atomic_typ id
     { defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) }
@@ -1033,13 +1041,13 @@ default_typ:
     { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) }
 
 scattered_def:
-  | Function_ Rec typquant atomic_typ effect_typ id
+  | Function_ Rec typquant typ effect_typ id
     { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
-  | Function_ Rec atomic_typ effect_typ id
+  | Function_ Rec typ effect_typ id
     { (DEF_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
-  | Function_ Rec typquant atomic_typ id
+  | Function_ Rec typquant typ id
     { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec atomic_typ id
+  | Function_ Rec typ id
     { match $3 with
       | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
         (DEF_scattered_function(mk_rec 2, mk_tannotn (), mk_eannot $3 3, $4))
@@ -1047,13 +1055,13 @@ scattered_def:
         (DEF_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
   | Function_ Rec id
     { (DEF_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) }
-  | Function_ typquant atomic_typ effect_typ id
+  | Function_ typquant typ effect_typ id
     { (DEF_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
-  | Function_ atomic_typ effect_typ id
+  | Function_ typ effect_typ id
     { (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) }
-  | Function_ typquant atomic_typ id
+  | Function_ typquant typ id
     { (DEF_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
-  | Function_ atomic_typ id
+  | Function_ typ id
     { match $2 with
       | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) ->
         (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $2 2, $3))
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
index fe59603f..e9c38ebd 100644
--- a/src/pre_parser.mly
+++ b/src/pre_parser.mly
@@ -64,25 +64,29 @@ id:
   | Id
     { $1 }
 
-scan:
+id_found:
   | Typedef id
     { $2 }
-  | Scattered Typedef id
-    { $3 }
-  | id scan
-    { $2 }
-  | Other scan
-    { $2 }
+
+skip:
+  | Scattered
+    { () }
+  | id
+    { () }
+  | Other
+    { () }
 
 scan_file:
-  | scan
+  | id_found
     { [$1] }
-  | scan scan_file
+  | skip
+    { [] }
+  | id_found scan_file
     { $1::$2 }
+  | skip scan_file
+    { $2 }
 
 file:
   | scan_file Eof
     { $1 }
-  | Other Eof
-    { [] }
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index dd5a792b..083bd087 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -50,10 +50,14 @@ let pp_parens is_atomic format =
 let pp_format_id (Id_aux(i,_)) =
   match i with
   | Id(i) -> i
-  | DeIid(x) -> "(:" ^ x ^ ")"
+  | DeIid(x) -> "(deinfix " ^ x ^ ")"
 
 let pp_id ppf id = base ppf (pp_format_id id)
 
+let pp_format_var (Var_aux(Var v,_)) = "'" ^ v
+
+let pp_var ppf var = base ppf (pp_format_var var)
+
 let pp_format_bkind (BK_aux(k,_)) =
   match k with
   | BK_type -> "Type"
@@ -70,7 +74,8 @@ let pp_kind ppf k = base ppf (pp_format_kind k)
 
 let rec pp_format_typ (Typ_aux(t,_)) =
   match t with
-  | Typ_var(id) -> pp_format_id id
+  | Typ_id(id) -> pp_format_id id
+  | Typ_var(var) -> pp_format_var var
   | Typ_wild -> "_"
   | Typ_fn(arg,ret,efct) -> "(" ^ (parens is_atomic_typ pp_format_typ arg) ^ " -> " ^ 
                             (parens is_atomic_typ pp_format_typ ret) ^ " " ^
@@ -80,6 +85,7 @@ let rec pp_format_typ (Typ_aux(t,_)) =
 and pp_format_nexp (Nexp_aux(n,_)) = 
   match n with
   | Nexp_id(id) -> pp_format_id id
+  | Nexp_var(var) -> pp_format_var var
   | Nexp_constant(i) -> string_of_int i
   | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + " ^ (pp_format_nexp n2) ^ ")"
   | Nexp_times(n1,n2) -> "(" ^  (pp_format_nexp n1) ^ " * " ^ (pp_format_nexp n2) ^ ")"
@@ -87,11 +93,13 @@ and pp_format_nexp (Nexp_aux(n,_)) =
 and pp_format_ord (Ord_aux(o,_)) = 
   match o with
   | Ord_id(id) -> pp_format_id id
+  | Ord_var(var) -> pp_format_var var
   | Ord_inc -> "inc"
   | Ord_dec -> "dec"  
 and pp_format_effects (Effects_aux(e,_)) =
   match e with
-  | Effects_var(id) -> "effect " ^ pp_format_id id
+  | Effects_id(id) -> "effect " ^ pp_format_id id
+  | Effects_var(var) -> "effect " ^ pp_format_var var
   | Effects_set(efcts) ->
     if (efcts = []) 
     then "pure"
@@ -137,8 +145,8 @@ let pp_format_qi (QI_aux(qi,_)) =
   | QI_const(n_const) -> pp_format_nexp_constraint n_const
   | QI_id(KOpt_aux(ki,_)) ->
     (match ki with
-    | KOpt_none(id) -> pp_format_id id
-    | KOpt_kind(k,id) -> pp_format_kind k ^ " " ^ pp_format_id id)
+    | KOpt_none(var) -> pp_format_var var
+    | KOpt_kind(k,var) -> pp_format_kind k ^ " " ^ pp_format_var var)
 
 let pp_qi ppf qi = base ppf (pp_format_qi qi)
 
@@ -259,13 +267,14 @@ and pp_lexp ppf (LEXP_aux(lexp,_)) =
 
 let pp_default ppf (DT_aux(df,_)) =
   match df with
-  | DT_kind(bk,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_id id
+  | DT_kind(bk,var) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_var var
   | DT_typ(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_typscm ts pp_id id
 
 let pp_spec ppf (VS_aux(v,_)) =
   match v with
   | VS_val_spec(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id
   | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>%a %a %a %a %a \"%s\"@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id kwd "=" s
+  | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>%a %a %a %a@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id
 
 let pp_namescm ppf (Name_sect_aux(ns,_)) =
   match ns with
@@ -352,6 +361,10 @@ let pp_format_id_lem (Id_aux(i,_)) =
 
 let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
 
+let pp_format_var_lem (Var_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
+
+let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
+
 let pp_format_bkind_lem (BK_aux(k,_)) =
   match k with
   | BK_type -> "BK_type"
@@ -368,7 +381,8 @@ let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k)
 
 let rec pp_format_typ_lem (Typ_aux(t,_)) =
   match t with
-  | Typ_var(id) -> "(Typ_var " ^ pp_format_id_lem id ^ ")"
+  | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
+  | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
   | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ 
                              pp_format_typ_lem ret ^ " " ^
                             (pp_format_effects_lem efct) ^ ")"
@@ -378,6 +392,7 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) =
 and pp_format_nexp_lem (Nexp_aux(n,_)) = 
   match n with
   | Nexp_id(id) -> "(Nexp_id " ^ pp_format_id_lem id ^ ")"
+  | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
   | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
   | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
   | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
@@ -385,11 +400,13 @@ and pp_format_nexp_lem (Nexp_aux(n,_)) =
 and pp_format_ord_lem (Ord_aux(o,_)) = 
   match o with
   | Ord_id(id) -> "(Ord_id " ^ pp_format_id_lem id ^ ")"
+  | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
   | Ord_inc -> "Ord_inc"
   | Ord_dec -> "Ord_dec"  
 and pp_format_effects_lem (Effects_aux(e,_)) =
   match e with
-  | Effects_var(id) -> "(Effects_var " ^ pp_format_id id ^ ")"
+  | Effects_id(id) -> "(Effects_id " ^ pp_format_id id ^ ")"
+  | Effects_var(v) -> "(Effects_var " ^ pp_format_var v ^ ")"
   | Effects_set(efcts) ->
     "(Effects_set [" ^
       (list_format "; " 
@@ -434,8 +451,8 @@ let pp_format_qi_lem (QI_aux(qi,_)) =
   | QI_id(KOpt_aux(ki,_)) ->
     "(QI_id " ^
     (match ki with
-    | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id_lem id ^ ")"
-    | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_id_lem id ^ ")") ^ ")"
+    | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")"
+    | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ ")"
 
 let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
 
@@ -558,13 +575,14 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
 
 let pp_lem_default ppf (DT_aux(df,_)) =
   match df with
-  | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id
+  | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
   | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
 
 let pp_lem_spec ppf (VS_aux(v,_)) =
   match v with
   | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
   | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
+  | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
 
 let pp_lem_namescm ppf (Name_sect_aux(ns,_)) =
   match ns with
@@ -589,8 +607,8 @@ let pp_lem_typdef ppf (TD_aux(td,_)) =
   | TD_variant(id,nm,typq,ar,_) ->
     let a_pp ppf (Tu_aux(typ_u,_)) = 
       match typ_u with
-      | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a)@]" pp_lem_typ typ pp_lem_id id 
-      | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a)@]" pp_id id
+      | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a);@]" pp_lem_typ typ pp_lem_id id 
+      | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a);@]" pp_lem_id id
     in
     fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
       kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar 
diff --git a/src/process_file.ml b/src/process_file.ml
index 35a84b21..b07caca4 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -62,6 +62,7 @@ let get_lexbuf fn =
 
 let parse_file (f : string) : Parse_ast.defs =
   let scanbuf = get_lexbuf f in
+  let default_type_names = ["bool";"unit";"vector";"enum";"list";"bit";"nat"] in
   let type_names = 
     try
       Pre_parser.file Pre_lexer.token scanbuf
@@ -73,14 +74,14 @@ let parse_file (f : string) : Parse_ast.defs =
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
       | Lexer.LexError(s,p) ->
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in
-  let _ = Lexer.type_names != ref type_names in
+  let _ = Lexer.type_names := (default_type_names@type_names) in
   let lexbuf = get_lexbuf f in
     try
       Parser.file Lexer.token lexbuf
     with
       | Parsing.Parse_error ->
           let pos = Lexing.lexeme_start_p lexbuf in
-           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "")))
+           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main")))
       | Parse_ast.Parse_error_locn(l,m) ->
           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
       | Lexer.LexError(s,p) ->
diff --git a/src/test/test1.sail b/src/test/test1.sail
index e7828483..dfb8ac8f 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -1,14 +1,14 @@
-(*default Nat i
-default Order o
+default Nat 'i
+default Order 'o
 default bool b
-default forall 'a. (list 'a) b
+default forall 'a. (list<'a>) b
 val forall 'a, 'b . (('a * 'b) -> 'b pure) snd
 val forall Type 'i, 'b. (('i * 'b) -> 'i pure) fst
-typedef int_list [name = "il"] = list nat
+typedef int_list [name = "il"] = list<nat>
 typedef reco = const struct forall 'i, 'a, 'b. { ('a['i]) v; 'b w; }
-typedef maybe = const union forall 'a. { unit None; a Some; }
+typedef maybe = const union forall 'a. { Nne; 'a Sme; }
 typedef colors = enumerate { red; green; blue }
-typedef creg = register bits [5:i] { 5 : h ; 6..7 : j}
+typedef creg = register bits [5:'i] { 5 : h ; 6..7 : j}
 let bool e = true
 
-function unit main _ = ()*)
+function unit main _ = ()
\ No newline at end of file
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 4a216467..30513bc9 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -8,9 +8,9 @@ val ( ( nat * nat ) -> nat effect { wmem , rmem } ) MEM_SIZE
 
 (* extern functions *)
 val extern ( ( nat * nat ) -> nat pure ) add = "add"
-val extern ( ( nat * nat ) -> nat pure ) (: + ) = "add_infix"   (* infix plus *)
+val extern ( ( nat * nat ) -> nat pure ) (deinfix + ) = "add_infix"   (* infix plus *)
 
-function nat (: * ) ( < nat > x, < nat > y ) = 42
+function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
 function nat main _ = {
   (* left-hand side function call = memory write *)