Syntax changes per discussions on Thursday.

First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)

10 files changed, 643 insertions, 308 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4d16fef4..772df3e9 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -323,7 +323,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
     | Parse_ast.E_id(id) -> E_id(to_ast_id id)
     | Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit)
     | Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env typ, to_ast_exp k_env exp)
-    | Parse_ast.E_app(f,args) -> E_app(to_ast_exp k_env f, List.map (to_ast_exp k_env) args)
+    | Parse_ast.E_app(f,args) -> E_app(to_ast_id f, List.map (to_ast_exp k_env) args)
     | Parse_ast.E_app_infix(left,op,right) -> E_app_infix(to_ast_exp k_env left, to_ast_id op, to_ast_exp k_env right)
     | Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env) exps)
     | Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3)
@@ -351,9 +351,9 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
   LEXP_aux(
     (match exp with
     | Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
-    | Parse_ast.E_app(Parse_ast.E_aux(f,l'),[exp]) -> 
+    | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) -> 
       (match f with
-      | Parse_ast.E_id(id) -> LEXP_memory(to_ast_id id,to_ast_exp k_env exp)
+      | 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)
     | 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)
@@ -466,7 +466,11 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
     let id = to_ast_id id in
     let key = id_to_string id in
     let typq,k_env,_ = to_ast_typquant k_env typq in
-    let arms = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) arms in (* Add check that all arms have unique names *)
+    let arms = List.map (fun (Parse_ast.Tu_aux(tu,l)) -> 
+                             match tu with
+                             | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l))
+                             | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) ) 
+               arms in (* Add check that all arms have unique names *)
     let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in
     let typ = (match (typquant_to_quantkinds k_env typq) with
       | [ ] -> {k = K_Typ}
@@ -595,7 +599,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
         (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@[typ,arm_id],false),tl)),dl),false);
+          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))
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 2e8af9d3..640f6b1d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -130,7 +130,7 @@ let rec to_data_constructors (Defs defs) =
     | DEF_type t ->
       match t with 
       | TD_variant id _ tq tid_list _ ->
-        (List.map (fun (x,y) -> (y,x)) tid_list)++(to_data_constructors (Defs defs))
+        (List.map (fun (Tu_ty_id x y) -> (y,x)) tid_list)++(to_data_constructors (Defs defs))
       | _ -> to_data_constructors (Defs defs) end
     | _ -> to_data_constructors (Defs defs) end
    end
@@ -268,7 +268,7 @@ let rec to_exp v =
         E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(List.length vals),[]) vals))
     | V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
     | V_list(vals) -> E_list (List.map to_exp vals)
-    | V_ctor id vals -> E_app (E_id id) [to_exp vals]
+    | V_ctor id vals -> E_app id [to_exp vals]
     end
 
 val find_type_def : defs -> id -> maybe type_def
@@ -634,7 +634,7 @@ and interp_main t_level l_env l_mem exp =
     | E_block(exps) -> interp_block t_level l_env l_env l_mem exps
     | E_app f args ->
       match (f,t_level) with
-      | (E_id(id),(defs,externs,regs,mems,ctors)) -> 
+      | (id,(defs,externs,regs,mems,ctors)) -> 
 	(match find_function defs id with
 	| Just(funcls) -> 
           resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
diff --git a/src/lexer.mll b/src/lexer.mll
index 3843a50b..b9336e2d 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -45,7 +45,7 @@
 (**************************************************************************)
 
 {
-open Parser
+open Pre_parser
 module M = Map.Make(String)
 exception LexError of string * Lexing.position
 
@@ -58,64 +58,69 @@ let kw_table =
     (fun r (x,y) -> M.add x y r)
     M.empty
     [
-     ("and",                     (fun _ -> And));
-     ("as",                      (fun _ -> As));
-     ("bits",                    (fun _ -> Bits));
-     ("by",                      (fun _ -> By));
-     ("case",			 (fun _ -> Case));
-     ("clause",                  (fun _ -> Clause));
-     ("const",			 (fun _ -> Const));
-     ("default",		 (fun _ -> Default));
-     ("effect",                  (fun _ -> Effect));
-     ("Effects",                 (fun _ -> Effects));
-     ("end",                     (fun _ -> End));
-     ("enumerate",		 (fun _ -> Enumerate));
-     ("else",                    (fun _ -> Else));
-     ("extern",                  (fun _ -> Extern));
-     ("false",                   (fun _ -> False));
-     ("forall",                  (fun _ -> Forall));
-     ("foreach",                  (fun _ -> Foreach));
-     ("function",                (fun x -> Function_));
-     ("if",                      (fun x -> If_));
-     ("in",			 (fun x -> In));
-     ("IN",                      (fun x -> IN));
-     ("let",                     (fun x -> Let_));
-     ("member",                  (fun x -> Member));
-     ("Nat",                     (fun x -> Nat));
-     ("Order",                   (fun x -> Order));
-     ("pure",                    (fun x -> Pure));
-     ("rec",			 (fun x -> Rec));
-     ("register",		 (fun x -> Register));
+     ("and",                     (fun _ -> Other));
+     ("as",                      (fun _ -> Other));
+     ("bits",                    (fun _ -> Other));
+     ("by",                      (fun _ -> Other));
+     ("case",			 (fun _ -> Other));
+     ("clause",                  (fun _ -> Other));
+     ("const",			 (fun _ -> Other));
+     ("dec",                     (fun _ -> Other));
+     ("default",		 (fun _ -> Other));
+     ("deinfix",                 (fun _ -> Other));
+     ("effect",                  (fun _ -> Other));
+     ("Effects",                 (fun _ -> Other));
+     ("end",                     (fun _ -> Other));
+     ("enumerate",		 (fun _ -> Other));
+     ("else",                    (fun _ -> Other));
+     ("extern",                  (fun _ -> Other));
+     ("false",                   (fun _ -> Other));
+     ("forall",                  (fun _ -> Other));
+     ("foreach",                 (fun _ -> Other));
+     ("function",                (fun x -> Other));
+     ("if",                      (fun x -> Other));
+     ("in",			 (fun x -> Other));
+     ("IN",                      (fun x -> Other));
+     ("Inc",                     (fun x -> Other));
+     ("let",                     (fun x -> Other));
+     ("member",                  (fun x -> Other));
+     ("Nat",                     (fun x -> Other));
+     ("Order",                   (fun x -> Other));
+     ("pure",                    (fun x -> Other));
+     ("rec",			 (fun x -> Other));
+     ("register",		 (fun x -> Other));
      ("scattered",               (fun x -> Scattered));
-     ("struct",                  (fun x -> Struct));
-     ("switch",			 (fun x -> Switch));
-     ("then",                    (fun x -> Then));
-     ("true",                    (fun x -> True));
-     ("Type",                    (fun x -> TYPE));
+     ("struct",                  (fun x -> Other));
+     ("switch",			 (fun x -> Other));
+     ("then",                    (fun x -> Other));
+     ("true",                    (fun x -> Other));
+     ("Type",                    (fun x -> Other));
      ("typedef",		 (fun x -> Typedef));
-     ("undefined",               (fun x -> Undefined));
-     ("union",			 (fun x -> Union));
-     ("with",                    (fun x -> With));
-     ("val",                     (fun x -> Val));
-
-     ("AND",			 (fun x -> AND));
-     ("div",			 (fun x -> Div_));
-     ("EOR",			 (fun x -> EOR));
-     ("mod",			 (fun x -> Mod));
-     ("OR",			 (fun x -> OR));
-     ("quot",			 (fun x -> Quot));
-     ("rem",			 (fun x -> Rem));
+     ("undefined",               (fun x -> Other));
+     ("union",			 (fun x -> Other));
+     ("with",                    (fun x -> Other));
+     ("val",                     (fun x -> Other));
+
+     ("AND",			 (fun x -> Other));
+     ("div",			 (fun x -> Other));
+     ("EOR",			 (fun x -> Other));
+     ("mod",			 (fun x -> Other));
+     ("OR",			 (fun x -> Other));
+     ("quot",			 (fun x -> Other));
+     ("rem",			 (fun x -> Other));
 ]
 
 }
 
 let ws = [' ''\t']+
+let lowerletter = ['a'-'z']
+let upperletter = ['A'-'Z']
 let letter = ['a'-'z''A'-'Z']
 let digit = ['0'-'9']
 let binarydigit = ['0'-'1']
 let hexdigit = ['0'-'9''A'-'F''a'-'f']
 let alphanum = letter|digit
-let startident = letter|'_'
+let startident = lowerletter|'_'
 let ident = alphanum|['_''\'']
 let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
 let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
@@ -127,84 +132,6 @@ rule token = parse
     { Lexing.new_line lexbuf;
       token lexbuf }
 
-  | "&"					{ (Amp(r"&")) }
-  | "@"					{ (At(r"@")) }
-  | "|"                                 { Bar }
-  | "^"					{ (Carrot(r"^")) }
-  | ":"                                 { Colon }
-  | ","                                 { Comma }
-  | "."                                 { Dot }
-  | "/"			                { (Div(r "/")) }
-  | "="                                 { (Eq(r"=")) }
-  | "!"					{ (Excl(r"!")) }
-  | ">"					{ (Gt(r">")) }
-  | "-"					{ Minus }
-  | "<"					{ (Lt(r"<")) }
-  | "+"					{ (Plus(r"+")) }
-  | ";"                                 { Semi }
-  | "*"                                 { (Star(r"*")) }
-  | "~"					{ (Tilde(r"~")) }
-  | "_"                                 { Under }
-  | "{"                                 { Lcurly }
-  | "}"                                 { Rcurly }
-  | "("                                 { Lparen }
-  | "(:"                                { LparenColon }
-  | ")"                                 { Rparen }
-  | "["                                 { Lsquare }
-  | "]"                                 { Rsquare }
-  | "&&" as i                           { (AmpAmp(r i)) }
-  | "||"                                { BarBar }
-  | "|>"                                { BarGt }
-  | "|]"				{ BarSquare }
-  | "^^"				{ (CarrotCarrot(r"^^")) }
-  | "::" as i                           { (ColonColon(r i)) }
-  | ":="                                { ColonEq }
-  | ".."				{ DotDot }
-  | "=/="				{ (EqDivEq(r"=/=")) }
-  | "=="				{ (EqEq(r"==")) }
-  | "!="				{ (ExclEq(r"!=")) }
-  | "!!"				{ (ExclExcl(r"!!")) }
-  | ">="				{ (GtEq(r">=")) }
-  | ">=+"				{ (GtEqPlus(r">=+")) }
-  | ">>"				{ (GtGt(r">>")) }
-  | ">>>"				{ (GtGtGt(r">>>")) }
-  | ">+"				{ (GtPlus(r">+")) }
-  | "#>>"				{ (HashGtGt(r"#>>")) }
-  | "#<<"				{ (HashLtLt(r"#<<")) }
-  | "->"                                { MinusGt }
-  | "<="				{ (LtEq(r"<=")) }
-  | "<=+"				{ (LtEqPlus(r"<=+")) }
-  | "<>"				{ (LtGt(r"<>")) }
-  | "<<"				{ (LtLt(r"<<")) }
-  | "<<<"				{ (LtLtLt(r"<<<")) }
-  | "<+"				{ (LtPlus(r"<+")) }
-  | "**"				{ (StarStar(r"**")) }
-  | "~^"				{ (TildeCarrot(r"~^")) }
-
-  | ">=_s"				{ (GtEqUnderS(r">=_s")) }
-  | ">=_si"				{ (GtEqUnderSi(r">=_si")) }
-  | ">=_u"				{ (GtEqUnderU(r">=_u")) }
-  | ">=_ui"				{ (GtEqUnderUi(r">=_ui")) }
-  | ">>_u"				{ (GtGtUnderU(r">>_u")) }
-  | ">_s"				{ (GtUnderS(r">_s")) }
-  | ">_si"				{ (GtUnderSi(r">_si")) }
-  | ">_u"				{ (GtUnderU(r">_u")) }
-  | ">_ui"				{ (GtUnderUi(r">_ui")) }
-  | "<=_s"				{ (LtEqUnderS(r"<=_s")) }
-  | "<=_si"				{ (LtEqUnderSi(r"<=_si")) }
-  | "<=_u"				{ (LtEqUnderU(r"<=_u")) }
-  | "<=_ui"				{ (LtEqUnderUi(r"<=_ui")) }
-  | "<_s"				{ (LtUnderS(r"<_s")) }
-  | "<_si"				{ (LtUnderSi(r"<_si")) }
-  | "<_u"				{ (LtUnderU(r"<_u")) }
-  | "<_ui"				{ (LtUnderUi(r"<_ui")) }
-  | "**_s"				{ (StarStarUnderS(r"**_s")) }
-  | "**_si"				{ (StarStarUnderSi(r"**_si")) }
-  | "*_u"				{ (StarUnderU(r"*_u")) }
-  | "*_ui"				{ (StarUnderUi(r"*_ui")) }
-  | "2^"				{ (TwoCarrot(r"2^")) }
-
-
   | "(*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
   | "*)"        { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
 
@@ -212,71 +139,13 @@ rule token = parse
                                             (M.find i kw_table) ()
                                           else
                                             Id(r i) }
-  | "&" oper_char+ as i                 { (AmpI(r i)) }
-  | "@" oper_char+ as i                 { (AtI(r i)) }
-  | "^" oper_char+ as i                 { (CarrotI(r i)) }
-  | "/" oper_char+ as i                 { (DivI(r i)) }
-  | "=" oper_char+ as i			{ (EqI(r i)) }
-  | "!" oper_char+ as i                 { (ExclI(r i)) }
-  | ">" oper_char+ as i                 { (GtI(r i)) }
-  | "<" oper_char+ as i			{ (LtI(r i)) }
-  | "+"	oper_char+ as i			{ (PlusI(r i)) }
-  | "*" oper_char+ as i                 { (StarI(r i)) }
-  | "~"	oper_char+ as i			{ (TildeI(r i)) }
-  | "&&" oper_char+ as i                { (AmpAmpI(r i)) }
-  | "^^" oper_char+ as i		{ (CarrotCarrotI(r i)) }
-  | "::" oper_char+ as i                { (ColonColonI(r i)) }
-  | "=/=" oper_char+ as i		{ (EqDivEqI(r i)) }
-  | "==" oper_char+ as i		{ (EqEqI(r i)) }
-  | "!=" oper_char+ as i		{ (ExclEqI(r i)) }
-  | "!!" oper_char+ as i		{ (ExclExclI(r i)) }
-  | ">=" oper_char+ as i		{ (GtEqI(r i)) }
-  | ">=+" oper_char+ as i		{ (GtEqPlusI(r i)) }
-  | ">>" oper_char+ as i		{ (GtGtI(r i)) }
-  | ">>>" oper_char+ as i		{ (GtGtGtI(r i)) }
-  | ">+" oper_char+ as i		{ (GtPlusI(r i)) }
-  | "#>>" oper_char+ as i		{ (HashGtGt(r i)) }
-  | "#<<" oper_char+ as i		{ (HashLtLt(r i)) }
-  | "<=" oper_char+ as i		{ (LtEqI(r i)) }
-  | "<=+" oper_char+ as i		{ (LtEqPlusI(r i)) }
-  | "<<" oper_char+ as i		{ (LtLtI(r i)) }
-  | "<<<" oper_char+ as i		{ (LtLtLtI(r i)) }
-  | "<+" oper_char+ as i		{ (LtPlusI(r i)) }
-  | "**" oper_char+ as i		{ (StarStarI(r i)) }
-  | "~^" oper_char+ as i		{ (TildeCarrot(r i)) }
-
-  | ">=_s" oper_char+ as i				{ (GtEqUnderSI(r i)) }
-  | ">=_si" oper_char+ as i				{ (GtEqUnderSiI(r i)) }
-  | ">=_u" oper_char+ as i				{ (GtEqUnderUI(r i)) }
-  | ">=_ui" oper_char+ as i				{ (GtEqUnderUiI(r i)) }
-  | ">>_u" oper_char+ as i				{ (GtGtUnderUI(r i)) }
-  | ">_s" oper_char+ as i				{ (GtUnderSI(r i)) }
-  | ">_si" oper_char+ as i				{ (GtUnderSiI(r i)) }
-  | ">_u" oper_char+ as i				{ (GtUnderUI(r i)) }
-  | ">_ui" oper_char+ as i				{ (GtUnderUiI(r i)) }
-  | "<=_s" oper_char+ as i				{ (LtEqUnderSI(r i)) }
-  | "<=_si" oper_char+ as i				{ (LtEqUnderSiI(r i)) }
-  | "<=_u" oper_char+ as i				{ (LtEqUnderUI(r i)) }
-  | "<=_ui" oper_char+ as i				{ (LtEqUnderUiI(r i)) }
-  | "<_s" oper_char+ as i				{ (LtUnderSI(r i)) }
-  | "<_si" oper_char+ as i				{ (LtUnderSiI(r i)) }
-  | "<_u" oper_char+ as i				{ (LtUnderUI(r i)) }
-  | "<_ui" oper_char+ as i				{ (LtUnderUiI(r i)) }
-  | "**_s" oper_char+ as i				{ (StarStarUnderSI(r i)) }
-  | "**_si" oper_char+ as i				{ (StarStarUnderSiI(r i)) }
-  | "*_u" oper_char+ as i				{ (StarUnderUI(r i)) }
-  | "*_ui" oper_char+ as i				{ (StarUnderUiI(r i)) }
-  | "2^" oper_char+ as i				{ (TwoCarrotI(r i)) }
-
-  | digit+ as i                         { (Num(int_of_string i)) }
-  | "0b" (binarydigit+ as i)		{ (Bin(i)) }
-  | "0x" (hexdigit+ as i) 		{ (Hex(i)) }
-  | '"'                                 { (String(
-                                           string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+  | oper_char+                          { Other }
+  | digit+ as i                         { Other }
+  | '"'                                 { let s =
+                                           string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf) in 
+                                           Other }
   | eof                                 { Eof }
-  | _  as c                             { raise (LexError(
-                                          Printf.sprintf "Unexpected character: %c" c,
-                                          Lexing.lexeme_start_p lexbuf)) }
+  | _  as c                             { Other }
 
 
 and comment pos depth = parse
diff --git a/src/parser.mly b/src/parser.mly
index 2ff88944..c5f82508 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -120,9 +120,9 @@ let star = "*"
 
 /*Terminals with no content*/
 
-%token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else Extern
+%token And As Bits By Case Clause Const Dec Default Deinfix Effect Effects End Enumerate Else Extern
 %token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
-%token Scattered Struct Switch Then True Type TYPE Typedef Undefined Union With Val
+%token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
 
 /* Avoid shift/reduce conflict - see right_atomic_exp rule */
 %nonassoc Then
@@ -132,11 +132,11 @@ let star = "*"
 
 %token Bar Colon Comma Dot Eof Minus Semi Under
 %token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token BarBar BarGt BarSquare DotDot ColonEq ColonGt MinusGt LtBar LparenColon SquareBar
+%token BarBar BarSquare BarBarSquare ColonEq DotDot ColonGt MinusGt LtBar SquareBar SquareBarBar
 
 /*Terminals with content*/
 
-%token <string> Id TickId
+%token <string> Id TickId TyId
 %token <int> Num
 %token <string> String Bin Hex
 
@@ -175,70 +175,74 @@ id:
     { idl (Id($1)) }
   | Tilde
     { idl (Id($1)) }
-  | LparenColon Amp Rparen
-    { idl (DeIid($2)) }
-  | LparenColon At Rparen
-    { idl (DeIid($2)) }
-  | LparenColon Carrot Rparen
-    { idl (DeIid($2)) }
-  | LparenColon Div Rparen
-    { idl (DeIid($2)) }
-  | LparenColon Eq Rparen
-    { Id_aux(DeIid($2),loc ()) }
-  | LparenColon Excl Lparen
-    { idl (DeIid($2)) }
-  | LparenColon Gt Lparen
-    { idl (DeIid($2)) }
-  | LparenColon Lt Lparen
-    { idl (DeIid($2)) }
-  | LparenColon Minus Lparen
+  | Lparen Deinfix Amp Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix At Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Carrot Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Div Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Eq Rparen
+    { Id_aux(DeIid($3),loc ()) }
+  | Lparen Deinfix Excl Lparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Gt Lparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Lt Lparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Minus Lparen
     { idl (DeIid("-")) }
-  | LparenColon Plus Rparen
-    { idl (DeIid($2)) }
-  | LparenColon Star Rparen
-    { idl (DeIid($2)) }
-  | LparenColon AmpAmp Rparen
-    { idl (DeIid($2)) }
-  | LparenColon BarBar Rparen
+  | Lparen Deinfix Plus Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix Star Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix AmpAmp Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix BarBar Rparen
     { idl (DeIid("||")) }
-  | LparenColon CarrotCarrot Rparen
-    { idl (DeIid($2)) }
-  | LparenColon ColonColon Rparen
-    { idl (DeIid($2)) }
-  | LparenColon EqDivEq Rparen
-    { idl (DeIid($2)) }
-  | LparenColon EqEq Rparen
-    { idl (DeIid($2)) }
-  | LparenColon ExclEq Rparen
-    { idl (DeIid($2)) }
-  | LparenColon ExclExcl Rparen
-    { idl (DeIid($2)) }
-  | LparenColon GtEq Rparen
-    { idl (DeIid($2)) }
-  | LparenColon GtEqPlus Rparen
-    { idl (DeIid($2)) }
-  | LparenColon GtGt Rparen
-    { idl (DeIid($2)) }
-  | LparenColon GtGtGt Rparen
-    { idl (DeIid($2)) }
-  | LparenColon GtPlus Rparen
-    { idl (DeIid($2)) }
-  | LparenColon HashGtGt Rparen
-    { idl (DeIid($2)) }
-  | LparenColon HashLtLt Rparen
-    { idl (DeIid($2)) }
-  | LparenColon LtEq Rparen
-    { idl (DeIid($2)) }
-  | LparenColon LtLt Rparen
-    { idl (DeIid($2)) }
-  | LparenColon LtLtLt Rparen
-    { idl (DeIid($2)) }
-  | LparenColon LtPlus Rparen
-    { idl (DeIid($2)) }
-  | LparenColon StarStar Rparen
-    { idl (DeIid($2)) }
-  | LparenColon TildeCarrot Rparen
-    { idl (DeIid($2)) }
+  | Lparen Deinfix CarrotCarrot Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix ColonColon Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix EqDivEq Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix EqEq Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix ExclEq Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix ExclExcl Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix GtEq Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix GtEqPlus Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix GtGt Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix GtGtGt Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix GtPlus Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix HashGtGt Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix HashLtLt Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix LtEq Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix LtLt Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix LtLtLt Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix LtPlus Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix StarStar Rparen
+    { idl (DeIid($3)) }
+  | Lparen Deinfix TildeCarrot Rparen
+    { idl (DeIid($3)) }
+
+tid:
+  | TyId
+    { (idl (Id($1))) }
 
 atomic_kind:
   | TYPE
@@ -283,7 +287,7 @@ effect_list:
     { $1::$3 }
 
 effect_typ:
-  | Effect id
+  | Effect tid
     { tloc (ATyp_efid($2)) }
   | Effect Lcurly effect_list Rcurly
     { tloc (ATyp_set($3)) }
@@ -291,7 +295,7 @@ effect_typ:
     { tloc (ATyp_set([])) }
 
 atomic_typ:
-  | id
+  | tid
     { tloc (ATyp_id $1) }
   | effect_typ
     { $1 }
@@ -299,32 +303,36 @@ atomic_typ:
     { tloc (ATyp_inc) }
   | Dec
     { tloc (ATyp_dec) } 
-  | Lparen typ Rparen
-    { $2 }
   | SquareBar nexp_typ BarSquare
       { tloc (make_enum_sugar $2) }
   | SquareBar nexp_typ Colon nexp_typ BarSquare
       { tloc (make_enum_sugar_bounded $2 $4) }
+  | Lparen typ Rparen
+    { $2 }
 
 vec_typ:
   | atomic_typ
       { $1 }
-  | atomic_typ Lsquare nexp_typ Rsquare
-      { tloc (make_vector_sugar $1 $3) }
-  | atomic_typ Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded $1 $3 $5) }
+  | tid Lsquare nexp_typ Rsquare
+      { 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) }
 
 app_typs:
   | vec_typ
     { [$1] }
+  | Num
+    { [tloc (ATyp_constant $1)] }
+  | Num app_typs
+    { (ATyp_aux((ATyp_constant $1),locn 1 1))::$2 }
   | vec_typ app_typs
     { $1::$2 }
 
 app_typ:
   | vec_typ
     { $1 }
-  | id app_typs
-    { tloc (ATyp_app($1,$2)) }
+  | tid Lt app_typs Gt
+    { tloc (ATyp_app($1,$3)) }
 
 star_typ_list:
   | app_typ
@@ -342,23 +350,23 @@ star_typ:
 exp_typ:
    | star_typ
      { $1 }
-   | Num StarStar typ
-     { if (2 = $1)
-       then tloc (ATyp_exp($3))
-       else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) }
+   | Num
+     { tloc (ATyp_constant $1) }
+   | TwoStarStar typ
+     { tloc (ATyp_exp($2)) }
 
 nexp_typ:
-  | Num
-    { tloc (ATyp_constant $1) }
    | exp_typ
      { $1 }
-   | atomic_typ Plus typ
+   | atomic_typ Plus nexp_typ
      { tloc (ATyp_sum($1,$3)) }
+   | Lparen atomic_typ Plus nexp_typ Rparen
+     { tloc (ATyp_sum($2,$4)) }
 
 typ:
-  | nexp_typ
+  | star_typ
     { $1 }
-  | star_typ MinusGt atomic_typ effect_typ
+  | star_typ MinusGt typ effect_typ
     { tloc (ATyp_fn($1,$3,$4)) }
 
 lit:
@@ -387,21 +395,25 @@ atomic_pat:
     { ploc P_wild }
   | Lparen pat As id Rparen
     { ploc (P_as($2,$4)) }
-  | Lt typ Gt atomic_pat
-    { ploc (P_typ($2,$4)) } 
+  | Lparen Lparen typ Rparen atomic_pat Rparen
+    { ploc (P_typ($3,$5)) } 
   | id
     { ploc (P_app($1,[])) }
   | Lcurly fpats Rcurly
     { ploc (P_record((fst $2, snd $2))) }
-  | Lsquare pat Rsquare
-    { ploc (P_vector([$2])) }
   | Lsquare comma_pats Rsquare
     { ploc (P_vector($2)) }
+  | Lsquare pat Rsquare
+    { ploc (P_vector([$2])) }
   | Lsquare npats Rsquare
     { ploc (P_vector_indexed($2)) }
   | Lparen comma_pats Rparen
     { ploc (P_tup($2)) }
-  | SquareBar comma_pats BarSquare
+  | SquareBarBar BarBarSquare
+    { ploc (P_list([])) }
+  | SquareBarBar pat BarBarSquare
+    { ploc (P_list([$2])) }
+  | SquareBarBar comma_pats BarBarSquare
     { ploc (P_list($2)) }
   | Lparen pat Rparen
     { $2 }
@@ -409,10 +421,10 @@ atomic_pat:
 app_pat:
   | atomic_pat
     { $1 }
-  | id Lparen pat Rparen
-    { ploc (P_app($1,[$3])) }
   | id Lparen comma_pats Rparen
     { ploc (P_app($1,$3)) }
+  | id Lparen pat Rparen
+    { ploc (P_app($1,[$3])) }
 
 pat_colons:
   | atomic_pat Colon atomic_pat
@@ -463,7 +475,7 @@ atomic_exp:
     { eloc (E_lit($1)) }
   | Lparen exp Rparen
     { $2 }
-  | Lt typ Gt atomic_exp 
+  | Lparen typ Rparen atomic_exp 
     { eloc (E_cast($2,$4)) }
   | Lparen comma_exps Rparen
     { eloc (E_tuple($2)) }
@@ -475,7 +487,7 @@ atomic_exp:
     { eloc (E_vector_update($2,$4,$6)) }
   | Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
     { eloc (E_vector_update_subrange($2,$4,$6,$8)) }
-  | SquareBar comma_exps BarSquare
+  | SquareBarBar comma_exps BarBarSquare
     { eloc (E_list($2)) }
   | Switch exp Lcurly case_exps Rcurly
     { eloc (E_case($2,$4)) }
@@ -498,11 +510,11 @@ app_exp:
   | vaccess_exp
     { $1 }
   | id Lparen Rparen
-    { eloc (E_app((E_aux((E_id $1), locn 1 1)), [eloc (E_lit (lloc L_unit))])) }
+    { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) }
   | id Lparen exp Rparen
-    { eloc (E_app((E_aux((E_id $1),locn 1 1)),[ E_aux((E_tuple [$3]),locn 3 3)])) }
+    { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) }
   | id Lparen comma_exps Rparen
-    { eloc (E_app((E_aux((E_id $1),locn 1 1)),[E_aux (E_tuple $3,locn 3 3)])) }
+    { eloc (E_app($1,[E_aux (E_tuple $3,locn 3 3)])) }
 
 right_atomic_exp:
   | If_ exp Then exp Else exp
@@ -863,15 +875,19 @@ val_spec:
     { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
   | Val atomic_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)) }
+  | Val Extern atomic_typ id
+    { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
   | Val Extern typquant atomic_typ id Eq String
     { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
   | Val Extern atomic_typ id Eq String
     { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
 
 kinded_id:
-  | id
+  | tid
     { kiloc (KOpt_none $1) }
-  | kind id
+  | kind tid
     { kiloc (KOpt_kind($1,$2))}
 
 /*kinded_ids:
@@ -924,6 +940,20 @@ c_def_body:
   | atomic_typ id Semi c_def_body
     { ($1,$2)::(fst $4), snd $4 }
 
+union_body:
+  | id
+    { [Tu_aux( Tu_id $1, loc())],false }
+  | atomic_typ id
+    { [Tu_aux( Tu_ty_id ($1,$2), loc())],false }
+  | id Semi
+    { [Tu_aux( Tu_id $1, loc())],true }
+  | atomic_typ id Semi
+    { [Tu_aux( Tu_ty_id ($1,$2),loc())],true }
+  | id Semi union_body
+    { (Tu_aux( Tu_id $1, loc()))::(fst $3), snd $3 }
+  | atomic_typ id Semi union_body
+    { (Tu_aux(Tu_ty_id($1,$2),loc()))::(fst $4), snd $4 }
+
 index_range_atomic:
   | Num
     { irloc (BF_single($1)) }
@@ -976,13 +1006,13 @@ type_def:
     { tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
   | Typedef id Eq Const Struct Lcurly c_def_body Rcurly
     { tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
-  | Typedef id name_sect Eq Const Union typquant Lcurly c_def_body Rcurly
+  | Typedef id name_sect Eq Const Union typquant Lcurly union_body Rcurly
     { tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) }
-  | Typedef id Eq Const Union typquant Lcurly c_def_body Rcurly
+  | Typedef id Eq Const Union typquant Lcurly union_body Rcurly
     { tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) }
-  | Typedef id name_sect Eq Const Union Lcurly c_def_body Rcurly
+  | Typedef id name_sect Eq Const Union Lcurly union_body Rcurly
     { tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) }
-  | Typedef id Eq Const Union Lcurly c_def_body Rcurly
+  | Typedef id Eq Const Union Lcurly union_body Rcurly
     { tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
   | Typedef id Eq Enumerate Lcurly enum_body Rcurly
     { tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
new file mode 100644
index 00000000..6955c7c3
--- /dev/null
+++ b/src/pre_lexer.mll
@@ -0,0 +1,319 @@
+(**************************************************************************)
+(*                        Lem                                             *)
+(*                                                                        *)
+(*          Dominic Mulligan, University of Cambridge                     *)
+(*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            *)
+(*          Gabriel Kerneis, University of Cambridge                      *)
+(*          Kathy Gray, University of Cambridge                           *)
+(*          Peter Boehm, University of Cambridge (while working on Lem)   *)
+(*          Peter Sewell, University of Cambridge                         *)
+(*          Scott Owens, University of Kent                               *)
+(*          Thomas Tuerk, University of Cambridge                         *)
+(*                                                                        *)
+(*  The Lem sources are copyright 2010-2013                               *)
+(*  by the UK authors above and Institut National de Recherche en         *)
+(*  Informatique et en Automatique (INRIA).                               *)
+(*                                                                        *)
+(*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   *)
+(*  are distributed under the license below.  The former are distributed  *)
+(*  under the LGPLv2, as in the LICENSE file.                             *)
+(*                                                                        *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*  notice, this list of conditions and the following disclaimer.         *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*  notice, this list of conditions and the following disclaimer in the   *)
+(*  documentation and/or other materials provided with the distribution.  *)
+(*  3. The names of the authors may not be used to endorse or promote     *)
+(*  products derived from this software without specific prior written    *)
+(*  permission.                                                           *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
+(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
+(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
+(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
+(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
+(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
+(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
+(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  *)
+(*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       *)
+(*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   *)
+(*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
+(**************************************************************************)
+
+{
+open Parser
+module M = Map.Make(String)
+exception LexError of string * Lexing.position
+
+let r = fun s -> s (* Ulib.Text.of_latin1 *)
+(* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
+let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
+
+let kw_table =
+  List.fold_left
+    (fun r (x,y) -> M.add x y r)
+    M.empty
+    [
+     ("and",                     (fun _ -> And));
+     ("as",                      (fun _ -> As));
+     ("bits",                    (fun _ -> Bits));
+     ("by",                      (fun _ -> By));
+     ("case",			 (fun _ -> Case));
+     ("clause",                  (fun _ -> Clause));
+     ("const",			 (fun _ -> Const));
+     ("dec",                     (fun _ -> Dec));
+     ("default",		 (fun _ -> Default));
+     ("deinfix",                 (fun _ -> Deinfix));
+     ("effect",                  (fun _ -> Effect));
+     ("Effects",                 (fun _ -> Effects));
+     ("end",                     (fun _ -> End));
+     ("enumerate",		 (fun _ -> Enumerate));
+     ("else",                    (fun _ -> Else));
+     ("extern",                  (fun _ -> Extern));
+     ("false",                   (fun _ -> False));
+     ("forall",                  (fun _ -> Forall));
+     ("foreach",                  (fun _ -> Foreach));
+     ("function",                (fun x -> Function_));
+     ("if",                      (fun x -> If_));
+     ("in",			 (fun x -> In));
+     ("IN",                      (fun x -> IN));
+     ("Inc",                     (fun x -> Inc));
+     ("let",                     (fun x -> Let_));
+     ("member",                  (fun x -> Member));
+     ("Nat",                     (fun x -> Nat));
+     ("Order",                   (fun x -> Order));
+     ("pure",                    (fun x -> Pure));
+     ("rec",			 (fun x -> Rec));
+     ("register",		 (fun x -> Register));
+     ("scattered",               (fun x -> Scattered));
+     ("struct",                  (fun x -> Struct));
+     ("switch",			 (fun x -> Switch));
+     ("then",                    (fun x -> Then));
+     ("true",                    (fun x -> True));
+     ("Type",                    (fun x -> TYPE));
+     ("typedef",		 (fun x -> Typedef));
+     ("undefined",               (fun x -> Undefined));
+     ("union",			 (fun x -> Union));
+     ("with",                    (fun x -> With));
+     ("val",                     (fun x -> Val));
+
+     ("AND",			 (fun x -> AND));
+     ("div",			 (fun x -> Div_));
+     ("EOR",			 (fun x -> EOR));
+     ("mod",			 (fun x -> Mod));
+     ("OR",			 (fun x -> OR));
+     ("quot",			 (fun x -> Quot));
+     ("rem",			 (fun x -> Rem));
+]
+
+}
+
+let ws = [' ''\t']+
+let lowerletter = ['a'-'z']
+let upperletter = ['A'-'Z']
+let letter = ['a'-'z''A'-'Z']
+let digit = ['0'-'9']
+let binarydigit = ['0'-'1']
+let hexdigit = ['0'-'9''A'-'F''a'-'f']
+let alphanum = letter|digit
+let startident = lowerletter|'_'
+let ident = alphanum|['_''\'']
+let starttident = upperletter
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
+let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
+
+rule token = parse
+  | ws
+    { token lexbuf }
+  | "\n"
+    { Lexing.new_line lexbuf;
+      token lexbuf }
+
+  | "2**"                               { TwoStarStar }
+  | "&"					{ (Amp(r"&")) }
+  | "@"					{ (At(r"@")) }
+  | "|"                                 { Bar }
+  | "^"					{ (Carrot(r"^")) }
+  | ":"                                 { Colon }
+  | ","                                 { Comma }
+  | "."                                 { Dot }
+  | "/"			                { (Div(r "/")) }
+  | "="                                 { (Eq(r"=")) }
+  | "!"					{ (Excl(r"!")) }
+  | ">"					{ (Gt(r">")) }
+  | "-"					{ Minus }
+  | "<"					{ (Lt(r"<")) }
+  | "+"					{ (Plus(r"+")) }
+  | ";"                                 { Semi }
+  | "*"                                 { (Star(r"*")) }
+  | "~"					{ (Tilde(r"~")) }
+  | "_"                                 { Under }
+  | "{"                                 { Lcurly }
+  | "}"                                 { Rcurly }
+  | "("                                 { Lparen }
+  | ")"                                 { Rparen }
+  | "["                                 { Lsquare }
+  | "]"                                 { Rsquare }
+  | "&&" as i                           { (AmpAmp(r i)) }
+  | "||"                                { BarBar }
+  | "|]"				{ BarSquare }
+  | "||]"                               { BarBarSquare }
+  | "^^"				{ (CarrotCarrot(r"^^")) }
+  | "::" as i                           { (ColonColon(r i)) }
+  | ":="                                { ColonEq }
+  | ".."				{ DotDot }
+  | "=/="				{ (EqDivEq(r"=/=")) }
+  | "=="				{ (EqEq(r"==")) }
+  | "!="				{ (ExclEq(r"!=")) }
+  | "!!"				{ (ExclExcl(r"!!")) }
+  | ">="				{ (GtEq(r">=")) }
+  | ">=+"				{ (GtEqPlus(r">=+")) }
+  | ">>"				{ (GtGt(r">>")) }
+  | ">>>"				{ (GtGtGt(r">>>")) }
+  | ">+"				{ (GtPlus(r">+")) }
+  | "#>>"				{ (HashGtGt(r"#>>")) }
+  | "#<<"				{ (HashLtLt(r"#<<")) }
+  | "->"                                { MinusGt }
+  | "<="				{ (LtEq(r"<=")) }
+  | "<=+"				{ (LtEqPlus(r"<=+")) }
+  | "<>"				{ (LtGt(r"<>")) }
+  | "<<"				{ (LtLt(r"<<")) }
+  | "<<<"				{ (LtLtLt(r"<<<")) }
+  | "<+"				{ (LtPlus(r"<+")) }
+  | "**"				{ (StarStar(r"**")) }
+  | "~^"				{ (TildeCarrot(r"~^")) }
+
+  | ">=_s"				{ (GtEqUnderS(r">=_s")) }
+  | ">=_si"				{ (GtEqUnderSi(r">=_si")) }
+  | ">=_u"				{ (GtEqUnderU(r">=_u")) }
+  | ">=_ui"				{ (GtEqUnderUi(r">=_ui")) }
+  | ">>_u"				{ (GtGtUnderU(r">>_u")) }
+  | ">_s"				{ (GtUnderS(r">_s")) }
+  | ">_si"				{ (GtUnderSi(r">_si")) }
+  | ">_u"				{ (GtUnderU(r">_u")) }
+  | ">_ui"				{ (GtUnderUi(r">_ui")) }
+  | "<=_s"				{ (LtEqUnderS(r"<=_s")) }
+  | "<=_si"				{ (LtEqUnderSi(r"<=_si")) }
+  | "<=_u"				{ (LtEqUnderU(r"<=_u")) }
+  | "<=_ui"				{ (LtEqUnderUi(r"<=_ui")) }
+  | "<_s"				{ (LtUnderS(r"<_s")) }
+  | "<_si"				{ (LtUnderSi(r"<_si")) }
+  | "<_u"				{ (LtUnderU(r"<_u")) }
+  | "<_ui"				{ (LtUnderUi(r"<_ui")) }
+  | "**_s"				{ (StarStarUnderS(r"**_s")) }
+  | "**_si"				{ (StarStarUnderSi(r"**_si")) }
+  | "*_u"				{ (StarUnderU(r"*_u")) }
+  | "*_ui"				{ (StarUnderUi(r"*_ui")) }
+  | "2^"				{ (TwoCarrot(r"2^")) }
+
+
+  | "(*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
+  | "*)"        { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
+
+  | startident ident* as i              { if M.mem i kw_table then
+                                            (M.find i kw_table) ()
+                                          else
+                                            Id(r i) }
+  | starttident ident* as i             { if M.mem i kw_table then
+                                             (M.find i kw_table) ()
+                                          else
+                                            TyId(r i) }
+  | "&" oper_char+ as i                 { (AmpI(r i)) }
+  | "@" oper_char+ as i                 { (AtI(r i)) }
+  | "^" oper_char+ as i                 { (CarrotI(r i)) }
+  | "/" oper_char+ as i                 { (DivI(r i)) }
+  | "=" oper_char+ as i			{ (EqI(r i)) }
+  | "!" oper_char+ as i                 { (ExclI(r i)) }
+  | ">" oper_char+ as i                 { (GtI(r i)) }
+  | "<" oper_char+ as i			{ (LtI(r i)) }
+  | "+"	oper_char+ as i			{ (PlusI(r i)) }
+  | "*" oper_char+ as i                 { (StarI(r i)) }
+  | "~"	oper_char+ as i			{ (TildeI(r i)) }
+  | "&&" oper_char+ as i                { (AmpAmpI(r i)) }
+  | "^^" oper_char+ as i		{ (CarrotCarrotI(r i)) }
+  | "::" oper_char+ as i                { (ColonColonI(r i)) }
+  | "=/=" oper_char+ as i		{ (EqDivEqI(r i)) }
+  | "==" oper_char+ as i		{ (EqEqI(r i)) }
+  | "!=" oper_char+ as i		{ (ExclEqI(r i)) }
+  | "!!" oper_char+ as i		{ (ExclExclI(r i)) }
+  | ">=" oper_char+ as i		{ (GtEqI(r i)) }
+  | ">=+" oper_char+ as i		{ (GtEqPlusI(r i)) }
+  | ">>" oper_char+ as i		{ (GtGtI(r i)) }
+  | ">>>" oper_char+ as i		{ (GtGtGtI(r i)) }
+  | ">+" oper_char+ as i		{ (GtPlusI(r i)) }
+  | "#>>" oper_char+ as i		{ (HashGtGt(r i)) }
+  | "#<<" oper_char+ as i		{ (HashLtLt(r i)) }
+  | "<=" oper_char+ as i		{ (LtEqI(r i)) }
+  | "<=+" oper_char+ as i		{ (LtEqPlusI(r i)) }
+  | "<<" oper_char+ as i		{ (LtLtI(r i)) }
+  | "<<<" oper_char+ as i		{ (LtLtLtI(r i)) }
+  | "<+" oper_char+ as i		{ (LtPlusI(r i)) }
+  | "**" oper_char+ as i		{ (StarStarI(r i)) }
+  | "~^" oper_char+ as i		{ (TildeCarrot(r i)) }
+
+  | ">=_s" oper_char+ as i				{ (GtEqUnderSI(r i)) }
+  | ">=_si" oper_char+ as i				{ (GtEqUnderSiI(r i)) }
+  | ">=_u" oper_char+ as i				{ (GtEqUnderUI(r i)) }
+  | ">=_ui" oper_char+ as i				{ (GtEqUnderUiI(r i)) }
+  | ">>_u" oper_char+ as i				{ (GtGtUnderUI(r i)) }
+  | ">_s" oper_char+ as i				{ (GtUnderSI(r i)) }
+  | ">_si" oper_char+ as i				{ (GtUnderSiI(r i)) }
+  | ">_u" oper_char+ as i				{ (GtUnderUI(r i)) }
+  | ">_ui" oper_char+ as i				{ (GtUnderUiI(r i)) }
+  | "<=_s" oper_char+ as i				{ (LtEqUnderSI(r i)) }
+  | "<=_si" oper_char+ as i				{ (LtEqUnderSiI(r i)) }
+  | "<=_u" oper_char+ as i				{ (LtEqUnderUI(r i)) }
+  | "<=_ui" oper_char+ as i				{ (LtEqUnderUiI(r i)) }
+  | "<_s" oper_char+ as i				{ (LtUnderSI(r i)) }
+  | "<_si" oper_char+ as i				{ (LtUnderSiI(r i)) }
+  | "<_u" oper_char+ as i				{ (LtUnderUI(r i)) }
+  | "<_ui" oper_char+ as i				{ (LtUnderUiI(r i)) }
+  | "**_s" oper_char+ as i				{ (StarStarUnderSI(r i)) }
+  | "**_si" oper_char+ as i				{ (StarStarUnderSiI(r i)) }
+  | "*_u" oper_char+ as i				{ (StarUnderUI(r i)) }
+  | "*_ui" oper_char+ as i				{ (StarUnderUiI(r i)) }
+  | "2^" oper_char+ as i				{ (TwoCarrotI(r i)) }
+
+  | digit+ as i                         { (Num(int_of_string i)) }
+  | "0b" (binarydigit+ as i)		{ (Bin(i)) }
+  | "0x" (hexdigit+ as i) 		{ (Hex(i)) }
+  | '"'                                 { (String(
+                                           string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+  | eof                                 { Eof }
+  | _  as c                             { raise (LexError(
+                                          Printf.sprintf "Unexpected character: %c" c,
+                                          Lexing.lexeme_start_p lexbuf)) }
+
+
+and comment pos depth = parse
+  | "(*"                                { comment pos (depth+1) lexbuf }
+  | "*)"                                { if depth = 0 then ()
+                                          else if depth > 0 then comment pos (depth-1) lexbuf
+                                          else assert false }
+  | "\n"                                { Lexing.new_line lexbuf;
+                                          comment pos depth lexbuf }
+  | '"'                                 { ignore(string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf);
+                                          comment pos depth lexbuf }
+  | _                                   { comment pos depth lexbuf }
+  | eof                                 { raise (LexError("Unbalanced comment", pos)) }
+
+and string pos b = parse
+  | ([^'"''\n''\\']*'\n' as i)          { Lexing.new_line lexbuf;
+                                          Buffer.add_string b i;
+                                          string pos b lexbuf }
+  | ([^'"''\n''\\']* as i)              { Buffer.add_string b i; string pos b lexbuf }
+  | escape_sequence as i                { Buffer.add_string b i; string pos b lexbuf }
+  | '\\' '\n' ws                        { Lexing.new_line lexbuf; string pos b lexbuf }
+  | '\\'                                { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+                                            "illegal backslash escape in string"*) }
+  | '"'                                 { let s = unescaped(Buffer.contents b) in
+                                          (*try Ulib.UTF8.validate s; s
+                                          with Ulib.UTF8.Malformed_code ->
+                                            raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+                                              "String literal is not valid utf8"))) *) s }
+  | eof                                 { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+                                            "String literal not terminated")))*) }
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
new file mode 100644
index 00000000..5d56738b
--- /dev/null
+++ b/src/pre_parser.mly
@@ -0,0 +1,86 @@
+/**************************************************************************/
+/*                        Lem                                             */
+/*                                                                        */
+/*          Dominic Mulligan, University of Cambridge                     */
+/*          Francesco Zappa Nardelli, INRIA Paris-Rocquencourt            */
+/*          Gabriel Kerneis, University of Cambridge                      */
+/*          Kathy Gray, University of Cambridge                           */
+/*          Peter Boehm, University of Cambridge (while working on Lem)   */
+/*          Peter Sewell, University of Cambridge                         */
+/*          Scott Owens, University of Kent                               */
+/*          Thomas Tuerk, University of Cambridge                         */
+/*                                                                        */
+/*  The Lem sources are copyright 2010-2013                               */
+/*  by the UK authors above and Institut National de Recherche en         */
+/*  Informatique et en Automatique (INRIA).                               */
+/*                                                                        */
+/*  All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli}   */
+/*  are distributed under the license below.  The former are distributed  */
+/*  under the LGPLv2, as in the LICENSE file.                             */
+/*                                                                        */
+/*                                                                        */
+/*  Redistribution and use in source and binary forms, with or without    */
+/*  modification, are permitted provided that the following conditions    */
+/*  are met:                                                              */
+/*  1. Redistributions of source code must retain the above copyright     */
+/*  notice, this list of conditions and the following disclaimer.         */
+/*  2. Redistributions in binary form must reproduce the above copyright  */
+/*  notice, this list of conditions and the following disclaimer in the   */
+/*  documentation and/or other materials provided with the distribution.  */
+/*  3. The names of the authors may not be used to endorse or promote     */
+/*  products derived from this software without specific prior written    */
+/*  permission.                                                           */
+/*                                                                        */
+/*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    */
+/*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     */
+/*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    */
+/*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       */
+/*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    */
+/*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     */
+/*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         */
+/*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER  */
+/*  IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR       */
+/*  OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN   */
+/*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         */
+/**************************************************************************/
+
+%{
+
+let r = fun x -> x (* Ulib.Text.of_latin1 *)
+
+%}
+
+/*Terminals with no content*/
+
+%token Scattered Typedef Other Eof
+
+%token <string> Id 
+%start file
+%type <list string> file
+
+%%
+
+id:
+  | Id
+    { $1 }
+
+scan:
+  | Typedef id
+    { $2 }
+  | Scattered Typedef id
+    { $3 }
+  | id scan
+    { $2 }
+  | Other scan
+    { $2 }
+
+scan_file:
+  | scan
+    { [$1] }
+  | scan scan_file
+    { $1::$2 }
+
+file:
+  | scan_file Eof
+    { $1 }
+
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 55d09dcb..dd5a792b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -211,7 +211,7 @@ and pp_exp ppf (E_aux(e,_)) =
   | E_id(id) -> pp_id ppf id
   | E_lit(lit) -> pp_lit ppf lit
   | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "<" pp_typ typ kwd ">" pp_exp exp 
-  | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_exp f (list_pp pp_exp pp_exp) args
+  | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_id f (list_pp pp_exp pp_exp) args
   | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
   | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
   | E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
@@ -288,8 +288,11 @@ let pp_typdef ppf (TD_aux(td,_)) =
     fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n" 
       kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "struct" pp_typquant typq kwd "{" (list_pp f_pp f_pp) fs kwd "}"
   | TD_variant(id,nm,typq,ar,_) ->
-    let a_pp ppf (typ,id) = 
-      fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in
+    let a_pp ppf (Tu_aux(typ_u,_)) = 
+      match typ_u with
+      | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" 
+      | Tu_id(id) -> fprintf ppf "@[<1>%a%a@]" pp_id id kwd ";"
+    in
     fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n" 
       kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "union" pp_typquant typq kwd "{" (list_pp a_pp a_pp) ar kwd "}"
   | TD_enum(id,ns,enums,_) ->
@@ -504,7 +507,7 @@ and pp_lem_exp ppf (E_aux(e,_)) =
   | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
   | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
   | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
-  | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_exp f (list_pp pp_semi_lem_exp pp_lem_exp) args
+  | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
   | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
   | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
   | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
@@ -584,8 +587,11 @@ let pp_lem_typdef ppf (TD_aux(td,_)) =
     fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
       kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
   | TD_variant(id,nm,typq,ar,_) ->
-    let a_pp ppf (typ,id) = 
-      fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
+    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
+    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 
   | TD_enum(id,ns,enums,_) ->
diff --git a/src/type_check.mli b/src/type_check.mli
new file mode 100644
index 00000000..25992725
--- /dev/null
+++ b/src/type_check.mli
@@ -0,0 +1,9 @@
+open Ast
+open Type_internal
+type kind = Type_internal.kind
+type typ = Type_internal.t
+
+type envs = Nameset.t * kind Envmap.t * typ Envmap.t
+type 'a envs_out = 'a * envs
+
+val check : Nameset.t -> kind Envmap.t -> typ Envmap.t -> tannot defs -> tannot defs
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 8ebb0b69..dabb8100 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -55,6 +55,12 @@ and t_arg =
   | TA_eft of effect
   | TA_ord of order 
 
+type tag =
+  | Emp
+  | External
+  | Default
+  | Constructor
+
 (* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
 type nexp_range =
   | LtEq of Parse_ast.l * nexp
@@ -62,7 +68,7 @@ type nexp_range =
   | GtEq of Parse_ast.l * nexp
   | In of Parse_ast.l * nexp * nexp list
 
-type tannot = (t * nexp_range list) option
+type tannot = (t * tag * nexp_range list) option
 
 let initial_kind_env = 
   Envmap.from_list [ 
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 9aa5b9d9..99b82075 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -52,6 +52,12 @@ and t_arg =
   | TA_eft of effect
   | TA_ord of order 
 
+type tag =
+  | Emp
+  | External
+  | Default
+  | Constructor
+
 (* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
 type nexp_range =
   | LtEq of Parse_ast.l * nexp
@@ -59,6 +65,6 @@ type nexp_range =
   | GtEq of Parse_ast.l * nexp
   | In of Parse_ast.l * nexp * nexp list
 
-type tannot = (t * nexp_range list) option
+type tannot = (t * tag * nexp_range list) option
 
 val initial_kind_env : kind Envmap.t