Parser compiles and compiles some very small test programs.

Output is only given in the event of a parse or lex failure (with poor reporting for now)

There are still 10 shift/reduce conflicts that may need further investigating and a few syntax changes that need discussion.

6 files changed, 446 insertions, 398 deletions

diff --git a/src/ast.ml b/src/ast.ml
index f27c2a89..d09526c6 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -328,7 +328,7 @@ type
 type 
 'a tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_none
- | Typ_annot_opt_some of terminal * typ
+ | Typ_annot_opt_some of 'a typquant * typ
 
 
 type 
diff --git a/src/lexer.mll b/src/lexer.mll
index c637984f..df5725aa 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -49,8 +49,7 @@ open Parser
 module M = Map.Make(String)
 exception LexError of char * Lexing.position
 
-let (^^^) = Ulib.Text.(^^^)
-let r = Ulib.Text.of_latin1
+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)
 
@@ -75,7 +74,7 @@ let kw_table =
      ("function",                (fun x -> Function_(x)));
      ("if",                      (fun x -> If_(x)));
      ("in",			 (fun x -> In(x)));
-     ("IN",                      (fun x -> IN(x,r"IN")));     
+     ("IN",                      (fun x -> IN(x)));     
      ("let",                     (fun x -> Let_(x)));
      ("member",                  (fun x -> Member(x)));
      ("Nat",                     (fun x -> Nat(x)));
@@ -90,7 +89,7 @@ let kw_table =
      ("type",                    (fun x -> Type(x)));
      ("Type",                    (fun x -> TYPE(x)));
      ("typedef",		 (fun x -> Typedef(x)));
-     ("union",			 (fun x -> Union(x)))
+     ("union",			 (fun x -> Union(x)));
      ("with",                    (fun x -> With(x)));
      ("val",                     (fun x -> Val(x)));
 
@@ -122,10 +121,10 @@ let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digi
 
 rule token skips = parse
   | ws as i
-    { token (Ast.Ws(Ulib.Text.of_latin1 i)::skips) lexbuf }
+    { token (Parse_ast.Ws(r i)::skips) lexbuf }
   | "\n"
     { Lexing.new_line lexbuf;
-      token (Ast.Nl::skips) lexbuf } 
+      token (Parse_ast.Nl::skips) lexbuf } 
   
   | "&"					{ (Amp(Some(skips),r"&")) }
   | "@"					{ (At(Some(skips),r"@")) }
@@ -151,12 +150,12 @@ rule token skips = parse
   | ")"                                 { (Rparen(Some(skips))) }
   | "["                                 { (Lsquare(Some(skips))) }
   | "]"                                 { (Rsquare(Some(skips))) }
-  | "&&" as i                           { (AmpAmp(Some(skips),Ulib.Text.of_latin1 i)) }
+  | "&&" as i                           { (AmpAmp(Some(skips),r i)) }
   | "||"                                { (BarBar(Some(skips))) }
   | "|>"                                { (BarGt(Some(skips))) }
   | "|]"				{ (BarSquare(Some(skips))) }
   | "^^"				{ (CarrotCarrot(Some(skips),r"^^")) }
-  | "::" as i                           { (ColonColon(Some(skips),Ulib.Text.of_latin1 i)) }
+  | "::" as i                           { (ColonColon(Some(skips),r i)) }
   | ".."				{ (DotDot(Some(skips))) }  
   | "=/="				{ (EqDivEq(Some(skips),r"=/=")) }
   | "=="				{ (EqEq(Some(skips),r"==")) }
@@ -204,67 +203,67 @@ rule token skips = parse
 
 
   | "--"                           
-    { token (Ast.Com(Ast.Comment(comment lexbuf))::skips) lexbuf }
+    { token (Parse_ast.Com(Parse_ast.Comment(comment lexbuf))::skips) lexbuf }
 
   | startident ident* as i              { if M.mem i kw_table then
                                             (M.find i kw_table) (Some(skips))
                                           else
-                                            Id(Some(skips), Ulib.Text.of_latin1 i) }
-  | "&" oper_char+ as i                 { (AmpI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "@" oper_char+ as i                 { (AtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "^" oper_char+ as i                 { (CarrotI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "/" oper_char+ as i                 { (DivI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "=" oper_char+ as i			{ (EqI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "!" oper_char+ as i                 { (ExclI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">" oper_char+ as i                 { (GtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<" oper_char+ as i			{ (LtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "+"	oper_char+ as i			{ (PlusI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "*" oper_char+ as i                 { (StarI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "~"	oper_char+ as i			{ (TildeI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "&&" oper_char+ as i                { (AmpAmpI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "^^" oper_char+ as i		{ (CarrotCarrotI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "::" oper_char+ as i                { (ColonColonI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "=/=" oper_char+ as i		{ (EqDivEqI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "==" oper_char+ as i		{ (EqEqI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "!=" oper_char+ as i		{ (ExclEqI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "!!" oper_char+ as i		{ (ExclExclI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">=" oper_char+ as i		{ (GtEqI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">=+" oper_char+ as i		{ (GtEqPlusI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">>" oper_char+ as i		{ (GtGtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">>>" oper_char+ as i		{ (GtGtGtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">+" oper_char+ as i		{ (GtPlusI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "#>>" oper_char+ as i		{ (HashGtGt(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "#<<" oper_char+ as i		{ (HashLtLt(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<=" oper_char+ as i		{ (LtEqI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<=+" oper_char+ as i		{ (LtEqPlusI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<<" oper_char+ as i		{ (LtLtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<<<" oper_char+ as i		{ (LtLtLtI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<+" oper_char+ as i		{ (LtPlusI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "**" oper_char+ as i		{ (StarStarI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "~^" oper_char+ as i		{ (TildeCarrot(Some(skips),Ulib.Text.of_latin1 i)) }
+                                            Id(Some(skips), r i) }
+  | "&" oper_char+ as i                 { (AmpI(Some(skips),r i)) }
+  | "@" oper_char+ as i                 { (AtI(Some(skips),r i)) }
+  | "^" oper_char+ as i                 { (CarrotI(Some(skips),r i)) }
+  | "/" oper_char+ as i                 { (DivI(Some(skips),r i)) }
+  | "=" oper_char+ as i			{ (EqI(Some(skips),r i)) }
+  | "!" oper_char+ as i                 { (ExclI(Some(skips),r i)) }
+  | ">" oper_char+ as i                 { (GtI(Some(skips),r i)) }
+  | "<" oper_char+ as i			{ (LtI(Some(skips),r i)) }
+  | "+"	oper_char+ as i			{ (PlusI(Some(skips),r i)) }
+  | "*" oper_char+ as i                 { (StarI(Some(skips),r i)) }
+  | "~"	oper_char+ as i			{ (TildeI(Some(skips),r i)) }
+  | "&&" oper_char+ as i                { (AmpAmpI(Some(skips),r i)) }
+  | "^^" oper_char+ as i		{ (CarrotCarrotI(Some(skips),r i)) }
+  | "::" oper_char+ as i                { (ColonColonI(Some(skips),r i)) }
+  | "=/=" oper_char+ as i		{ (EqDivEqI(Some(skips),r i)) }
+  | "==" oper_char+ as i		{ (EqEqI(Some(skips),r i)) }
+  | "!=" oper_char+ as i		{ (ExclEqI(Some(skips),r i)) }
+  | "!!" oper_char+ as i		{ (ExclExclI(Some(skips),r i)) }
+  | ">=" oper_char+ as i		{ (GtEqI(Some(skips),r i)) }
+  | ">=+" oper_char+ as i		{ (GtEqPlusI(Some(skips),r i)) }
+  | ">>" oper_char+ as i		{ (GtGtI(Some(skips),r i)) }
+  | ">>>" oper_char+ as i		{ (GtGtGtI(Some(skips),r i)) }
+  | ">+" oper_char+ as i		{ (GtPlusI(Some(skips),r i)) }
+  | "#>>" oper_char+ as i		{ (HashGtGt(Some(skips),r i)) }
+  | "#<<" oper_char+ as i		{ (HashLtLt(Some(skips),r i)) }
+  | "<=" oper_char+ as i		{ (LtEqI(Some(skips),r i)) }
+  | "<=+" oper_char+ as i		{ (LtEqPlusI(Some(skips),r i)) }
+  | "<<" oper_char+ as i		{ (LtLtI(Some(skips),r i)) }
+  | "<<<" oper_char+ as i		{ (LtLtLtI(Some(skips),r i)) }
+  | "<+" oper_char+ as i		{ (LtPlusI(Some(skips),r i)) }
+  | "**" oper_char+ as i		{ (StarStarI(Some(skips),r i)) }
+  | "~^" oper_char+ as i		{ (TildeCarrot(Some(skips),r i)) }
 
-  | ">=_s" oper_char+ as i				{ (GtEqUnderSI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">=_si" oper_char+ as i				{ (GtEqUnderSiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">=_u" oper_char+ as i				{ (GtEqUnderUI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">=_ui" oper_char+ as i				{ (GtEqUnderUiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">>_u" oper_char+ as i				{ (GtGtUnderUI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">_s" oper_char+ as i				{ (GtUnderSI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">_si" oper_char+ as i				{ (GtUnderSiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">_u" oper_char+ as i				{ (GtUnderUI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | ">_ui" oper_char+ as i				{ (GtUnderUiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<=_s" oper_char+ as i				{ (LtEqUnderSI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<=_si" oper_char+ as i				{ (LtEqUnderSiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<=_u" oper_char+ as i				{ (LtEqUnderUI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<=_ui" oper_char+ as i				{ (LtEqUnderUiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<_s" oper_char+ as i				{ (LtUnderSI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<_si" oper_char+ as i				{ (LtUnderSiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<_u" oper_char+ as i				{ (LtUnderUI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "<_ui" oper_char+ as i				{ (LtUnderUiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "**_s" oper_char+ as i				{ (StarStarUnderSI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "**_si" oper_char+ as i				{ (StarStarUnderSiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "*_u" oper_char+ as i				{ (StarUnderUI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "*_ui" oper_char+ as i				{ (StarUnderUiI(Some(skips),Ulib.Text.of_latin1 i)) }
-  | "2^" oper_char+ as i				{ (TwoCarrotI(Some(skips),Ulib.Text.of_latin1 i)) }
+  | ">=_s" oper_char+ as i				{ (GtEqUnderSI(Some(skips),r i)) }
+  | ">=_si" oper_char+ as i				{ (GtEqUnderSiI(Some(skips),r i)) }
+  | ">=_u" oper_char+ as i				{ (GtEqUnderUI(Some(skips),r i)) }
+  | ">=_ui" oper_char+ as i				{ (GtEqUnderUiI(Some(skips),r i)) }
+  | ">>_u" oper_char+ as i				{ (GtGtUnderUI(Some(skips),r i)) }
+  | ">_s" oper_char+ as i				{ (GtUnderSI(Some(skips),r i)) }
+  | ">_si" oper_char+ as i				{ (GtUnderSiI(Some(skips),r i)) }
+  | ">_u" oper_char+ as i				{ (GtUnderUI(Some(skips),r i)) }
+  | ">_ui" oper_char+ as i				{ (GtUnderUiI(Some(skips),r i)) }
+  | "<=_s" oper_char+ as i				{ (LtEqUnderSI(Some(skips),r i)) }
+  | "<=_si" oper_char+ as i				{ (LtEqUnderSiI(Some(skips),r i)) }
+  | "<=_u" oper_char+ as i				{ (LtEqUnderUI(Some(skips),r i)) }
+  | "<=_ui" oper_char+ as i				{ (LtEqUnderUiI(Some(skips),r i)) }
+  | "<_s" oper_char+ as i				{ (LtUnderSI(Some(skips),r i)) }
+  | "<_si" oper_char+ as i				{ (LtUnderSiI(Some(skips),r i)) }
+  | "<_u" oper_char+ as i				{ (LtUnderUI(Some(skips),r i)) }
+  | "<_ui" oper_char+ as i				{ (LtUnderUiI(Some(skips),r i)) }
+  | "**_s" oper_char+ as i				{ (StarStarUnderSI(Some(skips),r i)) }
+  | "**_si" oper_char+ as i				{ (StarStarUnderSiI(Some(skips),r i)) }
+  | "*_u" oper_char+ as i				{ (StarUnderUI(Some(skips),r i)) }
+  | "*_ui" oper_char+ as i				{ (StarUnderUiI(Some(skips),r i)) }
+  | "2^" oper_char+ as i				{ (TwoCarrotI(Some(skips),r i)) }
   
   | digit+ as i                         { (Num(Some(skips),int_of_string i)) }
   | "0b" (binarydigit+ as i)		{ (Bin(Some(skips), i)) }
@@ -278,9 +277,9 @@ rule token skips = parse
 and comment = parse
   | (com_body "("* as i) "--"           { let c1 = comment lexbuf in
                                           let c2 = comment lexbuf in
-                                            Ast.Chars(Ulib.Text.of_latin1 i) :: Ast.Comment(c1) :: c2}
+                                            Parse_ast.Chars(r i) :: Parse_ast.Comment(c1) :: c2}
   | (com_body as i) "\n"                { Lexing.new_line lexbuf;
-                                          [Ast.Chars(Ulib.Text.of_latin1 i)] }
+                                          [Parse_ast.Chars(r i)] }
   | _  as c                             { raise (LexError(c, Lexing.lexeme_start_p lexbuf)) }
   | eof                                 { [] }
 
@@ -291,12 +290,12 @@ and string pos b = parse
   | ([^'"''\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 }
-  | '\\'                                { raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
-                                            "illegal backslash escape in string"))) }
+  | '\\'                                { 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
+                                          (*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"))) }
-  | eof                                 { raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
-                                            "String literal not terminated"))) }
+                                              "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/parse_ast.ml b/src/parse_ast.ml
index 948b8ab8..c58a7cd7 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -121,7 +121,7 @@ kind =
 
 
 type 
-'a nexp_constraint_aux =  (* constraint over kind $_$ *)
+nexp_constraint_aux =  (* constraint over kind $_$ *)
    NC_fixed of atyp * terminal * atyp
  | NC_bounded_ge of atyp * terminal * atyp
  | NC_bounded_le of atyp * terminal * atyp
@@ -135,8 +135,8 @@ kinded_id_aux =  (* optionally kind-annotated identifier *)
 
 
 type 
-'a nexp_constraint = 
-   NC_aux of 'a nexp_constraint_aux * 'a annot
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
 
 
 type 
@@ -145,8 +145,8 @@ kinded_id =
 
 
 type 
-'a typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of terminal * (kinded_id) list * terminal * ('a nexp_constraint * terminal) list * terminal
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal
  | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *)
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
@@ -165,8 +165,8 @@ lit_aux =  (* Literal constant *)
 
 
 type 
-'a typquant = 
-   TypQ_aux of 'a typquant_aux * 'a annot
+typquant = 
+   TypQ_aux of typquant_aux * l
 
 
 type 
@@ -175,106 +175,98 @@ lit =
 
 
 type 
-'a typschm_aux =  (* type scheme *)
-   TypSchm_ts of 'a typquant * atyp
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * atyp
 
 
 type 
-'a pat_aux =  (* Pattern *)
+pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild of terminal (* wildcard *)
- | P_as of terminal * 'a pat * terminal * id * terminal (* named pattern *)
- | P_typ of terminal * atyp * 'a pat * terminal (* typed pattern *)
+ | P_as of terminal * pat * terminal * id * terminal (* named pattern *)
+ | P_typ of terminal * atyp * pat * terminal (* typed pattern *)
  | P_id of id (* identifier *)
- | P_app of id * ('a pat) list (* union constructor pattern *)
- | P_record of terminal * ('a fpat * terminal) list * terminal * bool * terminal (* struct pattern *)
- | P_vector of terminal * ('a pat * terminal) list * terminal (* vector pattern *)
- | P_vector_indexed of terminal * (((terminal * int) * terminal * 'a pat) * terminal) list * terminal (* vector pattern (with explicit indices) *)
- | P_vector_concat of ('a pat * terminal) list (* concatenated vector pattern *)
- | P_tup of terminal * ('a pat * terminal) list * terminal (* tuple pattern *)
- | P_list of terminal * ('a pat * terminal) list * terminal (* list pattern *)
+ | P_app of id * (pat) list (* union constructor pattern *)
+ | P_record of terminal * (fpat * terminal) list * terminal * bool * terminal (* struct pattern *)
+ | P_vector of terminal * (pat * terminal) list * terminal (* vector pattern *)
+ | P_vector_indexed of terminal * (((terminal * int) * terminal * pat) * terminal) list * terminal (* vector pattern (with explicit indices) *)
+ | P_vector_concat of (pat * terminal) list (* concatenated vector pattern *)
+ | P_tup of terminal * (pat * terminal) list * terminal (* tuple pattern *)
+ | P_list of terminal * (pat * terminal) list * terminal (* list pattern *)
 
-and 'a pat = 
-   P_aux of 'a pat_aux * 'a annot
+and pat = 
+   P_aux of pat_aux * l
 
-and 'a fpat_aux =  (* Field pattern *)
-   FP_Fpat of id * terminal * 'a pat
+and fpat_aux =  (* Field pattern *)
+   FP_Fpat of id * terminal * pat
 
-and 'a fpat = 
-   FP_aux of 'a fpat_aux * 'a annot
+and fpat = 
+   FP_aux of fpat_aux * l
 
 
 type 
-'a typschm = 
-   TypSchm_aux of 'a typschm_aux * 'a annot
+typschm = 
+   TypSchm_aux of typschm_aux * l
 
 
 type 
-'a exp_aux =  (* Expression *)
-   E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
+exp_aux =  (* Expression *)
+   E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
- | E_cast of terminal * atyp * terminal * 'a exp (* cast *)
- | E_app of 'a exp * ('a exp) list (* function application *)
- | E_app_infix of 'a exp * id * 'a exp (* infix function application *)
- | E_tuple of terminal * ('a exp * terminal) list * terminal (* tuple *)
- | E_if of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp (* conditional *)
- | E_vector of terminal * ('a exp * terminal) list * terminal (* vector (indexed from 0) *)
- | E_vector_indexed of terminal * (((terminal * int) * terminal * 'a exp) * terminal) list * terminal (* vector (indexed consecutively) *)
- | E_vector_access of 'a exp * terminal * 'a exp * terminal (* vector access *)
- | E_vector_subrange of 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector extraction *)
- | E_vector_update of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector functional update *)
- | E_vector_update_subrange of terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal * 'a exp * terminal (* vector subrange update (with vector) *)
- | E_list of terminal * ('a exp * terminal) list * terminal (* list *)
- | E_cons of 'a exp * terminal * 'a exp (* cons *)
- | E_record of terminal * 'a fexps * terminal (* struct *)
- | E_record_update of terminal * 'a exp * terminal * 'a fexps * terminal (* functional update of struct *)
- | E_field of 'a exp * terminal * id (* field projection from struct *)
- | E_case of terminal * 'a exp * terminal * ((terminal * 'a pexp)) list * terminal (* pattern matching *)
- | E_let of 'a letbind * terminal * 'a exp (* let expression *)
- | E_assign of 'a lexp * terminal * '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_vector of 'a lexp * terminal * 'a exp * terminal (* vector element *)
- | LEXP_vector_range of 'a lexp * terminal * 'a exp * terminal * 'a exp * terminal (* subvector *)
- | LEXP_field of 'a lexp * terminal * id (* struct field *)
+ | E_cast of terminal * atyp * terminal * exp (* cast *)
+ | E_app of exp * (exp) list (* function application *)
+ | E_app_infix of exp * id * exp (* infix function application *)
+ | E_tuple of terminal * (exp * terminal) list * terminal (* tuple *)
+ | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *)
+ | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *)
+ | E_vector_indexed of terminal * (((terminal * int) * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *)
+ | E_vector_access of exp * terminal * exp * terminal (* vector access *)
+ | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *)
+ | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *)
+ | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *)
+ | E_list of terminal * (exp * terminal) list * terminal (* list *)
+ | E_cons of exp * terminal * exp (* cons *)
+ | E_record of terminal * fexps * terminal (* struct *)
+ | E_record_update of terminal * exp * terminal * fexps * terminal (* functional update of struct *)
+ | E_field of exp * terminal * id (* field projection from struct *)
+ | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *)
+ | E_let of letbind * terminal * exp (* let expression *)
+ | E_assign of exp * terminal * exp (* imperative assignment *)
 
-and 'a lexp = 
-   LEXP_aux of 'a lexp_aux * 'a annot
+and exp = 
+   E_aux of exp_aux * l
 
-and 'a fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * terminal * 'a exp
+and fexp_aux =  (* Field-expression *)
+   FE_Fexp of id * terminal * exp
 
-and 'a fexp = 
-   FE_aux of 'a fexp_aux * 'a annot
+and fexp = 
+   FE_aux of fexp_aux * l
 
-and 'a fexps_aux =  (* Field-expression list *)
-   FES_Fexps of ('a fexp * terminal) list * terminal * bool
+and fexps_aux =  (* Field-expression list *)
+   FES_Fexps of (fexp * terminal) list * terminal * bool
 
-and 'a fexps = 
-   FES_aux of 'a fexps_aux * 'a annot
+and fexps = 
+   FES_aux of fexps_aux * l
 
-and 'a pexp_aux =  (* Pattern match *)
-   Pat_exp of 'a pat * terminal * 'a exp
+and pexp_aux =  (* Pattern match *)
+   Pat_exp of pat * terminal * exp
 
-and 'a pexp = 
-   Pat_aux of 'a pexp_aux * 'a annot
+and pexp = 
+   Pat_aux of pexp_aux * l
 
-and 'a letbind_aux =  (* Let binding *)
-   LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *)
+and letbind_aux =  (* Let binding *)
+   LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *)
 
-and 'a letbind = 
-   LB_aux of 'a letbind_aux * 'a annot
+and letbind = 
+   LB_aux of letbind_aux * l
 
 
 type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * terminal * 'a exp
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal
 
 
 type 
@@ -284,125 +276,124 @@ rec_opt_aux =  (* Optional recursive annotation for functions *)
 
 
 type 
-'a effects_opt_aux =  (* Optional effect annotation for functions *)
-   Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of terminal
+tannot_opt_aux =  (* Optional type annotation for functions *)
+   Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * atyp
 
 
 type 
-'a tannot_opt_aux =  (* Optional type annotation for functions *)
-   Typ_annot_opt_none
- | Typ_annot_opt_some of terminal * terminal
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * terminal * exp
 
 
 type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of terminal * terminal * terminal * terminal * string * terminal
+effects_opt_aux =  (* Optional effect annotation for functions *)
+   Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of atyp
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
+index_range_aux =  (* index specification, for bitfields in register types *)
+   BF_single of (terminal * int) (* single index *)
+ | BF_range of (terminal * int) * terminal * (terminal * int) (* index range *)
+ | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *)
+
+and index_range = 
+   BF_aux of index_range_aux * l
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
-index_range_aux =  (* index specification, for bitfields in register types *)
-   BF_single of (terminal * int) (* single index *)
- | BF_range of (terminal * int) * terminal * (terminal * int) (* index range *)
- | BF_concat of index_range * terminal * index_range (* concatenation of index ranges *)
-
-and index_range = 
-   BF_aux of index_range_aux * l
+funcl = 
+   FCL_aux of funcl_aux * l
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list
+default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of terminal * base_kind * id
+ | DT_typ of terminal * typschm * id
 
 
 type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of terminal * id * naming_scheme_opt * terminal * 'a typschm (* type abbreviation *)
- | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
- | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* union type definition *)
+type_def_aux =  (* Type definition body *)
+   TD_abbrev of terminal * id * naming_scheme_opt * terminal * typschm (* type abbreviation *)
+ | TD_record of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* struct type definition *)
+ | TD_variant of terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant * terminal * ((atyp * id) * terminal) list * terminal * bool * terminal (* union type definition *)
  | TD_enum of terminal * id * naming_scheme_opt * terminal * terminal * terminal * (id * terminal) list * terminal * bool * terminal (* enumeration type definition *)
- | TD_register of terminal * id * terminal * terminal * terminal * terminal * terminal * terminal * terminal * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
+ | TD_register of terminal * id * terminal * terminal * terminal * terminal * atyp * terminal * atyp * terminal * terminal * ((index_range * terminal * id) * terminal) list * terminal (* register mutable bitfield type definition *)
 
 
 type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of terminal * base_kind * id
- | DT_typ of terminal * 'a typschm * id
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of terminal * typschm * id
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of terminal * 'a typschm * id
+fundef_aux =  (* Function definition *)
+   FD_function of terminal * rec_opt * tannot_opt * effects_opt * (funcl * terminal) list
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+type_def = 
+   TD_aux of type_def_aux * l
 
 
 type 
-'a default_typing_spec = 
-   DT_aux of 'a default_typing_spec_aux * 'a annot
+val_spec = 
+   VS_aux of val_spec_aux * l
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+fundef = 
+   FD_aux of fundef_aux * l
 
 
 type 
-'a def_aux =  (* Top-level definition *)
-   DEF_type of 'a type_def (* type definition *)
- | DEF_fundef of 'a fundef (* function definition *)
- | DEF_val of 'a letbind (* value definition *)
- | DEF_spec of 'a val_spec (* top-level type constraint *)
- | DEF_default of 'a default_typing_spec (* default kind and type assumptions *)
- | DEF_reg_dec of terminal * terminal * id (* register declaration *)
- | DEF_scattered_function of terminal * terminal * rec_opt * 'a tannot_opt * 'a effects_opt * id (* scattered function definition header *)
- | DEF_scattered_funcl of terminal * terminal * 'a funcl (* scattered function definition clause *)
- | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * 'a typquant (* scattered union definition header *)
- | DEF_scattered_unioncl of terminal * id * terminal * terminal * id (* scattered union definition member *)
+def_aux =  (* Top-level definition *)
+   DEF_type of type_def (* type definition *)
+ | DEF_fundef of fundef (* function definition *)
+ | DEF_val of letbind (* value definition *)
+ | DEF_spec of val_spec (* top-level type constraint *)
+ | DEF_default of default_typing_spec (* default kind and type assumptions *)
+ | DEF_reg_dec of terminal * atyp * id (* register declaration *)
+ | DEF_scattered_function of terminal * terminal * rec_opt * tannot_opt * effects_opt * id (* scattered function definition header *)
+ | DEF_scattered_funcl of terminal * terminal * funcl (* scattered function definition clause *)
+ | DEF_scattered_variant of terminal * terminal * id * naming_scheme_opt * terminal * terminal * terminal * typquant (* scattered union definition header *)
+ | DEF_scattered_unioncl of terminal * id * terminal * atyp * id (* scattered union definition member *)
  | DEF_scattered_end of terminal * id (* scattered definition end *)
 
 
 type 
-'a def = 
-   DEF_aux of 'a def_aux * 'a annot
+def = 
+   DEF_aux of def_aux * l
 
 
 type 
-'a typ_lib_aux =  (* library types and syntactic sugar for them *)
+typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit of terminal (* unit type with value $()$ *)
  | Typ_lib_bool of terminal (* booleans $_$ and $_$ *)
  | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *)
@@ -420,23 +411,34 @@ type
 
 
 type 
-'a ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * terminal * 'a typschm
+ctor_def_aux =  (* Datatype constructor definition clause *)
+   CT_ct of id * terminal * typschm
+
+
+type 
+lexp_aux =  (* lvalue expression *)
+   LEXP_id of id (* identifier *)
+ | LEXP_vector of lexp * terminal * exp * terminal (* vector element *)
+ | LEXP_vector_range of lexp * terminal * exp * terminal * exp * terminal (* subvector *)
+ | LEXP_field of lexp * terminal * id (* struct field *)
+
+and lexp = 
+   LEXP_aux of lexp_aux * l
 
 
 type 
-'a defs =  (* Definition sequence *)
-   Defs of ('a def) list
+defs =  (* Definition sequence *)
+   Defs of (def) list
 
 
 type 
-'a typ_lib = 
-   Typ_lib_aux of 'a typ_lib_aux * l
+typ_lib = 
+   Typ_lib_aux of typ_lib_aux * l
 
 
 type 
-'a ctor_def = 
-   CT_aux of 'a ctor_def_aux * 'a annot
+ctor_def = 
+   CT_aux of ctor_def_aux * l
 
 
 
diff --git a/src/parser.mly b/src/parser.mly
index d2669ea0..968151da 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -48,39 +48,45 @@
 
 let r = fun x -> x (* Ulib.Text.of_latin1 *)
 
-open Ast
+open Parse_ast
 
 let loc () = Range(Parsing.symbol_start_pos(),Parsing.symbol_end_pos())
 let locn m n = Range(Parsing.rhs_start_pos m,Parsing.rhs_end_pos n)
 
-let ploc p = Pat_l(p,loc ())
-let eloc e = Expr_l(e,loc ())
-let lbloc lb = Letbind(lb,loc ())
+let ploc p = P_aux(p,loc ())
+let eloc e = E_aux(e,loc ())
+let peloc pe = Pat_aux(pe,loc ())
+let lbloc lb = LB_aux(lb,loc ())
 
 let bkloc k = BK_aux(k,loc ())
 let kloc k = K_aux(k,loc ())
+let kiloc ki = KOpt_aux(ki,loc ())
 let tloc t = ATyp_aux(t,loc ())
 let lloc l = L_aux(l,loc ())
-let ploc p = P_aux(p,(None,loc ()))
-let fploc p = FP_aux(p,(None,loc ()))
+let ploc p = P_aux(p,loc ())
+let fploc p = FP_aux(p,loc ())
 
-let dloc d = DEF_aux(d,loc ())
-
-let pat_to_let p =
-  match p with
-    | Pat_l(P_app(Id([],v,_),(arg::args as a)),_) ->
-        Some((v,a))
-    | _ ->
-        None
+let funclloc f = FCL_aux(f,loc ())
+let typql t = TypQ_aux(t, loc())
+let irloc r = BF_aux(r, loc())
+let defloc df = DT_aux(df, loc())
 
-let pat_to_letfun p =
-  match p with
-    | Pat_l(P_app(Id([],v,_),(arg::args as a)),_) ->
-        (v,a)
-    | Pat_l(_,l) -> 
-        raise (Parse_error_locn(l,"Bad pattern for let binding of a function"))
+let tdloc td = TD_aux(td, loc())
+let funloc fn = FD_aux(fn, loc())
+let vloc v = VS_aux(v, loc ())
+let dloc d = DEF_aux(d,loc ())
 
-let build_fexp (Expr_l(e,_)) l =
+let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
+let mk_rec r i = (Rec_aux((Rec_rec (r)), locn i i))
+let mk_recn _ = (Rec_aux((Rec_nonrec), Unknown))
+let mk_typqn _ = (TypQ_aux(TypQ_no_forall,Unknown))
+let mk_tannot tq t s e = Typ_annot_opt_aux(Typ_annot_opt_some(tq,t),(locn s e))
+let mk_tannotn _ = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
+let mk_eannot e i = Effects_opt_aux((Effects_opt_effects(e)),(locn i i))
+let mk_eannotn _ = Effects_opt_aux(Effects_opt_pure,Unknown)
+let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
+
+(*let build_fexp (Expr_l(e,_)) l =
   match e with
     | Infix(Expr_l(Ident(i), l'),SymX_l((stx,op),l''),e2) when String.compare op (r"=") = 0 ->
         Fexp(i, stx, e2, l)
@@ -91,7 +97,7 @@ let mod_cap n =
   if not (Name.starts_with_upper_letter (Name.strip_lskip (Name.from_x n))) then
     raise (Parse_error_locn(Ast.xl_to_l n, "Module name must begin with an upper-case letter"))
   else
-    ()
+    ()*)
 
 let space = " "
 let star = "*"
@@ -112,73 +118,73 @@ let star = "*"
 
 /*Terminals with no content*/
 
-%token <Ast.terminal> And As Bits Case Clause Const Default Effect Effects End Enum Else False 
-%token <Ast.terminal> Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register  
-%token <Ast.terminal> Scattered Struct Switch Then True Type TYPE Typedef Union With Val
+%token <Parse_ast.terminal> And As Bits Case Clause Const Default Effect Effects End Enum Else False 
+%token <Parse_ast.terminal> Forall Function_ If_ In IN Let_ Member Nat Order Pure Rec Register  
+%token <Parse_ast.terminal> Scattered Struct Switch Then True Type TYPE Typedef Union With Val
 
-%token <Ast.terminal> AND Div_ EOR Mod OR Quot Rem 
+%token <Parse_ast.terminal> AND Div_ EOR Mod OR Quot Rem 
 
-%token <Ast.terminal> Bar Colon Comma Dot Eof Minus Semi Under
-%token <Ast.terminal> Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token <Ast.terminal> BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar 
+%token <Parse_ast.terminal> Bar Colon Comma Dot Eof Minus Semi Under
+%token <Parse_ast.terminal> Lcurly Rcurly Lparen Rparen Lsquare Rsquare
+%token <Parse_ast.terminal> BarBar BarGt BarSquare DotDot MinusGt LtBar SquareBar 
 
 /*Terminals with content*/
 
-%token <Ast.terminal * string> Id
-%token <Ast.terminal * int> Num
-%token <Ast.terminal * string> String Bin Hex
+%token <Parse_ast.terminal * string> Id
+%token <Parse_ast.terminal * int> Num
+%token <Parse_ast.terminal * string> String Bin Hex
 
-%token <Ast.terminal * string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde 
-%token <Ast.terminal * string> AmpAmp CarrotCarrot ColonColon ColonEq EqDivEq EqEq ExclEq ExclExcl  
-%token <Ast.terminal * string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt   
-%token <Ast.terminal * string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
+%token <Parse_ast.terminal * string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde 
+%token <Parse_ast.terminal * string> AmpAmp CarrotCarrot ColonColon ColonEq EqDivEq EqEq ExclEq ExclExcl  
+%token <Parse_ast.terminal * string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt   
+%token <Parse_ast.terminal * string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
 
-%token <Ast.terminal * string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS 
-%token <Ast.terminal * string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU 
-%token <Ast.terminal * string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarUnderS 
-%token <Ast.terminal * string> StarUnderSi StarUnderU StarUnderUi TwoCarrot
+%token <Parse_ast.terminal * string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS 
+%token <Parse_ast.terminal * string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU 
+%token <Parse_ast.terminal * string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS 
+%token <Parse_ast.terminal * string> StarUnderSi StarUnderU StarUnderUi TwoCarrot
 
-%token <Ast.terminal * string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <Ast.terminal * string> AmpAmpI CarrotCarrotI ColonColonI ColonEqI EqDivEqI EqEqI ExclEqI ExclExclI  
-%token <Ast.terminal * string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI  
-%token <Ast.terminal * string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
+%token <Parse_ast.terminal * string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
+%token <Parse_ast.terminal * string> AmpAmpI CarrotCarrotI ColonColonI ColonEqI EqDivEqI EqEqI ExclEqI ExclExclI  
+%token <Parse_ast.terminal * string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI  
+%token <Parse_ast.terminal * string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
 
-%token <Ast.terminal * string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI 
-%token <Ast.terminal * string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI 
-%token <Ast.terminal * string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarUnderSI 
-%token <Ast.terminal * string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
+%token <Parse_ast.terminal * string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI 
+%token <Parse_ast.terminal * string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI 
+%token <Parse_ast.terminal * string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI 
+%token <Parse_ast.terminal * string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
 
 %start file
-%type <Ast.defs> defs
-%type <Ast.typ> typ
-%type <Ast.pat> pat
-%type <Ast.exp> exp
-%type <Ast.defs * Ast.terminal> file
+%type <Parse_ast.defs> defs
+%type <Parse_ast.atyp> typ
+%type <Parse_ast.pat> pat
+%type <Parse_ast.exp> exp
+%type <Parse_ast.defs * Parse_ast.terminal> file
 
 
 %%
 
 id:
   | Id
-    { X_l($1, loc ()) }
+    { Id_aux(Id($1), loc ()) }
   | Lparen Eq Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
   | Lparen IN Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,($2,"In"),$3),loc ()) }
   | Lparen AmpAmp Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
   | Lparen BarBar Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,($2,"||"),$3),loc ()) }
   | Lparen ColonColon Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
   | Lparen Star Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
   | Lparen Plus Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
   | Lparen GtEq Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
   | Lparen At Rparen
-    { mk_pre_x_l $1 $2 $3 (loc ()) }
+    { Id_aux(DeIid($1,$2,$3),loc ()) }
 
 atomic_kind:
   | TYPE
@@ -190,16 +196,20 @@ atomic_kind:
   | Effects
     { bkloc (BK_effects($1)) }
 
-kind:
+kind_help:
   | atomic_kind
     { [ ($1,None) ] }
-  | atomic_kind MinusGt kind
+  | atomic_kind MinusGt kind_help
     { ($1,$2)::$3 }
 
+kind:
+  | kind_help
+    { K_aux(K_kind($1), loc ()) }
+
 effect:
   | id
-    { (match id with
-       | Id_aux(Id(s,t),l) ->
+    { (match $1 with
+       | Id_aux(Id(t,s),l) ->
 	 Effect_aux
 	   ((match s with
 	   | "rreg" -> (Effect_rreg t)
@@ -209,34 +219,38 @@ effect:
 	   | "undef" -> (Effect_undef t)
 	   | "unspec" -> (Effect_unspec t)
 	   | "nondet" -> (Effect_nondet t)
-	   | _ -> Parse_error_locn(l, "Invalid effect")),l)
-       | _ -> Parse_error_locn(loc () , "Invalid effect")) }
+	   | _ -> raise (Parse_error_locn (l,"Invalid effect"))),l)
+       | _ -> raise (Parse_error_locn ((loc ()),"Invalid effect"))) }
 
 effect_list:
   | effect
     { [($1,None)] }
   | effect Comma effect_list
-    { ($1,Some($2))::$3 }
+    { ($1,$2)::$3 }
 
 effect_typ:
   | Effect id
     { tloc (ATyp_efid($1,$2)) }
   | Effect Lcurly effect_list Rcurly
-    { tloc (ATyp_effects($1,$2,$3,$4)) }
+    { tloc (ATyp_set($1,$2,$3,$4)) }
   | Pure
-    { tloc (ATyp_effects($1,[],None)) }
+    { tloc (ATyp_set($1,None,[],None)) }
 
 atomic_typ:
   | id
-    { tloc (ATyp_var $1) }
+    { tloc (ATyp_id $1) }
   | Num
-    { tloc (ATyp_constant(fst $1, snd$1)) }
+    { tloc (ATyp_constant(fst $1, snd $1)) }
   | Under
     { tloc (ATyp_wild($1)) }
   | effect_typ
     { $1 }
   | Lparen typ Rparen
     { $2 }
+  | Lsquare nexp_typ Rsquare
+      { assert false }
+  | Lsquare nexp_typ Colon nexp_typ Rsquare
+      { assert false }
 
 atomic_typs:
   | atomic_typ
@@ -268,9 +282,9 @@ exp_typ:
    | star_typ
      { $1 }
    | Num StarStar typ
-     { if (2 = (fst $1))
-       then tloc (ATyp_exp((fst $1,snd $1),$2,$3))
-       else Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats") } 
+     { if (2 = (snd $1))
+       then tloc (ATyp_exp((fst $1),(fst $2),$3))
+       else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) } 
 
 nexp_typ:
    | exp_typ
@@ -278,10 +292,18 @@ nexp_typ:
    | atomic_typ Plus typ
      { tloc (ATyp_sum($1,fst $2,$3)) } 
 
+vtyp_typ:
+   | star_typ
+       { $1 }
+   | star_typ Lsquare nexp_typ Rsquare
+     { assert false }
+   | star_typ Lsquare nexp_typ Colon nexp_typ Rsquare
+     { assert false }
+
 typ:
   | nexp_typ
     { $1 }
-  | star_typ MinusGt atomic_typ effect_typ
+  | vtyp_typ MinusGt atomic_typ effect_typ
     { tloc (ATyp_fn($1,$2,$3,$4)) } 
 
 lit:
@@ -384,13 +406,13 @@ atomic_exp:
   | Lparen exp Rparen
     { $2 }
   | Lparen comma_exps Rparen
-    { eloc (E_tup($1,$2,$3)) }
+    { eloc (E_tuple($1,$2,$3)) }
   | Lsquare comma_exps Rsquare
     { eloc (E_vector($1,$2,$3)) }
   | Lsquare exp With exp Eq exp Rsquare
     { eloc (E_vector_update($1,$2,$3,$4,fst $5,$6,$7)) }
   | Lsquare exp With exp Colon exp Eq exp Rsquare
-    { eloc (E_vector_subrance($1,$2,$3,$4,$5,fst $6,$7,$8)) }
+    { eloc (E_vector_update_subrange($1,$2,$3,$4,$5,$6,fst $7,$8,$9)) }
   | SquareBar comma_exps BarSquare
     { eloc (E_list($1,$2,$3)) }
   | Switch exp Lcurly case_exps Rcurly
@@ -414,9 +436,9 @@ app_exp:
   | vaccess_exp
     { $1 }
   | id Lparen exp Rparen
-    { eloc (E_app($1,$2)) }
+    { eloc (E_app((E_aux((E_id $1),locn 1 1)),[$3])) }
   | id Lparen comma_exps Rparen
-    { eloc (E_app($1,$3)) }
+    { eloc (E_app((E_aux((E_id $1),locn 1 1)),[(E_aux((E_tuple($2,$3,$4)),locn 2 4))])) }
 
 right_atomic_exp:
   | If_ exp Then exp Else exp
@@ -428,37 +450,37 @@ starstar_exp:
   | app_exp
     { $1 }
   | starstar_exp StarStar app_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 starstar_right_atomic_exp:
   | right_atomic_exp
     { $1 }
   | starstar_exp StarStar right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 star_exp:
   | starstar_exp
     { $1 }
   | star_exp Star starstar_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 star_right_atomic_exp:
   | starstar_right_atomic_exp
     { $1 }
   | star_exp Star starstar_right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 plus_exp:
   | star_exp
     { $1 }
   | plus_exp Plus star_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 plus_right_atomic_exp:
   | star_right_atomic_exp
     { $1 }
   | plus_exp Plus star_right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 cons_exp:
   | plus_exp
@@ -476,57 +498,59 @@ at_exp:
   | cons_exp
     { $1 }
   | cons_exp At at_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 at_right_atomic_exp:
   | cons_right_atomic_exp
     { $1 }
   | cons_exp At at_right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 eq_exp:
   | at_exp
     { $1 }
   /* Adds one shift/reduce conflict */
   | eq_exp Eq at_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
   | eq_exp GtEq at_exp
-    { eloc (E_app_infix ($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
   | eq_exp IN at_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id(($2,"In")), locn 2 2), $3)) }
   | eq_exp ColonEq at_exp
-    { eloc (E_assign($1,$2,$3)) }
+    { eloc (E_assign($1,fst $2,$3)) }
 
 eq_right_atomic_exp:
   | at_right_atomic_exp
     { $1 }
   | eq_exp Eq at_right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+  | eq_exp ColonEq at_right_atomic_exp 
+    { eloc (E_assign($1,fst $2,$3)) }
 
 and_exp:
   | eq_exp
     { $1 }
   | eq_exp AmpAmp and_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 and_right_atomic_exp:
   | eq_right_atomic_exp
     { $1 }
   | eq_exp AmpAmp and_right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
 
 or_exp:
   | and_exp
     { $1 }
   | and_exp BarBar or_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id(($2,"||")), locn 2 2), $3)) }
 
 
 or_right_atomic_exp:
   | and_right_atomic_exp
     { $1 }
   | and_exp BarBar or_right_atomic_exp
-    { eloc (E_app_infix($1,SymX_l($2, locn 2 2), $3)) }
+    { eloc (E_app_infix($1,Id_aux(Id(($2,"||")), locn 2 2), $3)) }
 
 exp:
   | or_exp
@@ -543,15 +567,15 @@ comma_exps:
  
 semi_exps_help:
   | exp
-    { ([($1,None)], (None,false)) }
+    { [($1,None)] }
   | exp Semi
-    { ([($1,None)], ($2,true)) }
+    { [($1,$2)] }
   | exp Semi semi_exps_help
-    { (($1,$2)::fst $3, snd $3) }
+    { ($1,$2)::$3 }
 
 semi_exps:
   |
-    { ([], (None, false)) }
+    { [] }
   | semi_exps_help
     { $1 }
 
@@ -566,68 +590,70 @@ case_exps:
     { $1::$2 }
 
 patsexp:
-  | atomic_pats MinusGt exp
-    { Patsexp($1,$2,$3,loc ()) }
-
-atomic_pats:
-  | atomic_pat
-    { [$1] }
-  | atomic_pat atomic_pats
-    { $1::$2 } 
+  | atomic_pat MinusGt exp
+    { peloc (Pat_exp($1,$2,$3)) }
 
 letbind:
   | Let_ atomic_pat Eq exp
-    { }
+    { lbloc (LB_val_implicit($1,$2,fst $3,$4)) }
   | Let_ typquant atomic_typ atomic_pat Eq exp
-    { }
+    { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,fst $5,$6)) }
   /* This is ambiguous causing 4 shift/reduce and 5 reduce/reduce conflicts because the parser can't tell until the end of typ whether it was parsing a type or a pattern, and this seem to be too late. Solutions are to have a different keyword for this and the above solution besides let (while still absolutely having a keyword here) 
   | Let_ atomic_typ atomic_pat Eq exp
     { } */
 
 funcl: 
-  | id atomic_pats Eq exp
-    { reclloc (FCL_Funcl($1,$2,fst $3,$4)) }
+  | id atomic_pat Eq exp
+    { funclloc (FCL_Funcl($1,$2,fst $3,$4)) }
 
 funcl_ands:
   | funcl
-    { [$1] }
+    { [$1,None] }
   | funcl And funcl_ands
-    { $1::$3 }
+    { ($1,$2)::$3 }
 
 fun_def:
   | Function_ Rec typquant atomic_typ effect_typ funcl_ands
-    { $1,$2,$3,$4,$5 }
+    { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
   | Function_ Rec typquant atomic_typ funcl_ands
-    { $1,$2,$3,$4,$5 }  
+    { funloc (FD_function($1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }  
   | Function_ Rec atomic_typ effect_typ funcl_ands
-    { }
+    { funloc (FD_function($1,mk_rec $2 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
   | Function_ Rec atomic_typ funcl_ands
-    { $1,$2,$3,$4 }
+    { match $3 with
+      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> 
+        funloc (FD_function($1,mk_rec $2 2,mk_tannotn (), mk_eannot $3 3, $4))
+      | _ -> 
+        funloc (FD_function($1,mk_rec $2 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
   | Function_ Rec funcl_ands
-    { $1,$2,$3 }
+    { funloc (FD_function($1,mk_rec $2 2, mk_tannotn (), mk_eannotn (), $3)) }
   | Function_ typquant atomic_typ effect_typ funcl_ands
-    { $1,$2,$3,$4 }
+    { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
   | Function_ typquant atomic_typ funcl_ands
-    { $1,$2,$3 }
+    { funloc (FD_function($1,mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }  
   | Function_ atomic_typ funcl_ands
-    { $1,$2,$3 }
+    { match $2 with
+      | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> 
+        funloc (FD_function($1,mk_recn (),mk_tannotn (), mk_eannot $2 2, $3))
+      | _ -> 
+        funloc (FD_function($1,mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
   | Function_ funcl_ands
-    { $1,$2 }
+    { funloc (FD_function($1,mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
 
 
 val_spec:
   | Val typquant atomic_typ id
-    { Val_spec($1,$2,$3) }
+    { vloc (VS_val_spec($1,mk_typschm $2 $3 2 3,$4)) }
   | Val atomic_typ id
-    { Val_spec($1,$2,$3) }
+    { vloc (VS_val_spec($1,mk_typschm (mk_typqn ()) $2 2 2,$3)) }
 
 kinded_id:
   | id
-    { }
+    { kiloc (KOpt_none $1) }
   | kind id
-    { }
+    { kiloc (KOpt_kind($1,$2))}
   | Lparen kinded_id Rparen
-    { }
+    { $2 }
 
 kinded_ids:
   | kinded_id
@@ -649,7 +675,7 @@ nexp_constraint:
   | typ LtEq typ
     { NC_aux(NC_bounded_le($1,(fst $2),$3), loc () ) }
   | id IN Lcurly nums Rcurly
-    { NC_aux(NC_nat_set_bounded($1,$2,$3,$4,$5)) } 
+    { NC_aux(NC_nat_set_bounded($1,$2,$3,$4,$5), loc ()) } 
     
 nexp_constraints:
   | nexp_constraint
@@ -658,28 +684,29 @@ nexp_constraints:
     { ($1,$2)::$3 }
 
 typquant:
+  /* This is a syntactic change to avoid 6 significant shift/reduce conflicts in the Dot */
   | Forall kinded_ids Amp nexp_constraints Dot
-    { typql(TypQ_tq($1,$2,$3,$4,$5)) }
+    { typql(TypQ_tq($1,$2,fst $3,$4,$5)) }
   | Forall kinded_ids Dot
     { typql(TypQ_no_constraint($1,$2,$3)) }
 
 name_sect:
-  | Lsquare id Eq String Rsquare
-    { Name_sect_some($1,$2,fst $3,(fst $4),(snd $4),$5) }
+  | Lsquare Id Eq String Rsquare
+    { Name_sect_aux(Name_sect_some($1,(fst $2),fst $3,(fst $4),(snd $4),$5), loc ()) }
 
 c_def_body:
   | typ id
-    { [(($1,$2),None)] }
+    { [(($1,$2),None)],(None,false) }
   | typ id Semi
-    { [(($1,$2),Some)] }
+    { [(($1,$2),None)],($3,true) }
   | typ id Semi c_def_body
-    { (($1,$2)$3)::$4 } 
+    { (($1,$2),$3)::(fst $4), snd $4 } 
 
 index_range_atomic:
   | Num
-    { IR_Num($1) }
+    { irloc (BF_single($1)) }
   | Num DotDot Num
-    { IR_Range($1,$2,$3) }
+    { irloc (BF_range($1,$2,$3)) }
   | Lparen index_range Rparen
     { $2 }
 
@@ -687,77 +714,95 @@ index_range:
   | index_range_atomic
     { $1 }
   | index_range_atomic Comma index_range
-    { IR_concat($1,$2,$3) } 
+    { irloc(BF_concat($1,$2,$3)) } 
+
+r_id_def:
+  | index_range Colon id
+    { $1,$2,$3 }
 
 r_def_body:
-  | index_range
-    { [(1,None)] }
-  | index_range Semi
+  | r_id_def
+    { [($1,None)] }
+  | r_id_def Semi
     { [$1,$2] }
-  | index_range Semi r_def_body
+  | r_id_def Semi r_def_body
     { ($1,$2)::$3 }
 
 type_def:
   | Typedef id name_sect Eq typquant typ
-    {}
+    { tdloc (TD_abbrev($1,$2,$3,fst $4,mk_typschm $5 $6 5 6)) }
   | Typedef id name_sect Eq typ
-    { }
+    { tdloc (TD_abbrev($1,$2,$3,fst $4,mk_typschm (mk_typqn ()) $5 5 5)) }
   | Typedef id Eq typquant typ
-    { }
+    { tdloc (TD_abbrev($1,$2,mk_namesectn (),fst $3, mk_typschm $4 $5 4 5))}
   | Typedef id Eq typ
-    { }
+    { tdloc (TD_abbrev($1,$2,mk_namesectn (),fst $3,mk_typschm (mk_typqn ()) $4 4 4)) }
   /* The below adds 4 shift/reduce conflicts. Unclear why */
   | Typedef id name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_record($1,$2,$3,fst $4,$5,$6,$7,$8,fst $9, fst (snd $9), snd (snd $9), $10)) }
   | Typedef id name_sect Eq Const Struct Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_record($1,$2,$3,fst $4,$5,$6,(mk_typqn ()), $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
   | Typedef id Eq Const Struct typquant Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_record($1,$2,mk_namesectn (), fst $3, $4, $5, $6, $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
   | Typedef id Eq Const Struct Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_record($1,$2, mk_namesectn (), fst $3, $4, $5, mk_typqn (), $6, fst $7, fst (snd $7), snd (snd $7), $8)) }
   | Typedef id name_sect Eq Const Union typquant Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_variant($1,$2,$3,fst $4, $5, $6, $7, $8, fst $9, fst (snd $9), snd (snd $9), $10)) }
   | Typedef id Eq Const Union typquant Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_variant($1,$2,mk_namesectn (), fst $3, $4, $5, $6, $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
   | Typedef id name_sect Eq Const Union Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_variant($1, $2, $3, fst $4, $5, $6, mk_typqn (), $7, fst $8, fst (snd $8), snd (snd $8), $9)) }
   | Typedef id Eq Const Union Lcurly c_def_body Rcurly
-    {}
+    { tdloc (TD_variant($1,$2, mk_namesectn (), fst $3, $4, $5, mk_typqn (), $6, fst $7, fst (snd $7), snd (snd $7), $8)) }
   | Typedef id Eq Register Bits Lsquare typ Colon typ Rsquare Lcurly r_def_body Rcurly
-    {}
+    { tdloc (TD_register($1,$2,fst $3, $4, $5, $6, $7, $8, $9, $10, $11, $12, $13)) }
 
 
 default_typ:
   | Default atomic_kind id
-    { $1,$2,$3 } 
+    { defloc (DT_kind($1,$2,$3)) } 
+  | Default typquant atomic_typ id
+    { defloc (DT_typ($1,(mk_typschm $2 $3 2 3),$4)) }
   | Default atomic_typ id
-    { $1,$2,$3 }
+    { defloc (DT_typ($1,(mk_typschm (mk_typqn ()) $2 2 2),$3)) }
  
 scattered_def:
   | Function_ Rec typquant atomic_typ effect_typ id
-    { (DEF_scattered_function(None,$1,(Rec_rec ($2)),$3,$4,$5)) }
+    { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) }
   | Function_ Rec atomic_typ effect_typ id
-    { (DEF_scattered_function(None,$1,(Rec_rec ($2)),$3,$4,$5)) }
+    { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) }
+  | Function_ Rec typquant atomic_typ id
+    { (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
   | Function_ Rec atomic_typ id
-    { (DEF_scattered_function(None,$1,(Rec_rec ($2)),$3,$4)) }
+    { match $3 with
+      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> 
+        (DEF_scattered_function(None,$1,mk_rec $2 2, mk_tannotn (), mk_eannot $3 3, $4))
+      | _ ->
+        (DEF_scattered_function(None,$1,mk_rec $2 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
   | Function_ Rec id
-    { DEF_scattered_function(None,$1,$2,None,None,$3) }
+    { (DEF_scattered_function(None,$1,mk_rec $2 2,mk_tannotn (), mk_eannotn (),$3)) }
   | Function_ typquant atomic_typ effect_typ id
-    { (DEF_scattered_function(None,$1,(Rec_rec ()),$2,$3,$4)) }
+    { (DEF_scattered_function(None,$1,mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) }
   | Function_ atomic_typ effect_typ id
-    { (DEF_scattered_function(None,$1,(Rec_rec ($2)),$3,)) }
+    { (DEF_scattered_function(None,$1,mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) }
+  | Function_ typquant atomic_typ id
+    { (DEF_scattered_function(None,$1,mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
   | Function_ atomic_typ id
-    { (DEF_scattered_function(None,$1,(Rec_rec ($2)),$3,)) }
+    { match $2 with
+      | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> 
+        (DEF_scattered_function(None,$1,mk_recn (), mk_tannotn (), mk_eannot $2 2, $3))
+      | _ ->
+        (DEF_scattered_function(None,$1,mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
   | Function_ id
-    { DEF_scattered_function(None,$1,$2,None,None,) }
+    { (DEF_scattered_function(None,$1,mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
   | Typedef id name_sect Eq Const Union typquant
-    { dloc (DEF_scattered_variant(None,$1,$2,$3,$4,$5,$6,$7)) }
+    { (DEF_scattered_variant(None,$1,$2,$3,fst $4,$5,$6,$7)) }
   | Typedef id Eq Const Union typquant
-    { dloc (DEF_scattered_variant(None,$1,Name_sect_none,$2,$3,$4,$5,$6)) }
+    { (DEF_scattered_variant(None,$1,$2,(mk_namesectn ()),fst $3,$4,$5,$6)) }
   | Typedef id name_sect Eq Const Union
-    { dloc (DEF_scattered_variant(None,$1,$2,$3,$4,$5,$6,None)) }
+    { (DEF_scattered_variant(None,$1,$2,$3,fst $4,$5,$6,mk_typqn ())) }
   | Typedef id Eq Const Union
-    { dloc (DEF_scattered_variant(None,$1,Name_sect_none,$2,$3,$4,$5,None)) }
+    { (DEF_scattered_variant(None,$1,$2,mk_namesectn (),fst $3,$4,$5,mk_typqn ())) }
 
 def:
   | type_def
@@ -775,9 +820,10 @@ def:
   | Scattered scattered_def
     { dloc (match ($2) with
             | DEF_scattered_function(_,f,r,t,e,i) -> DEF_scattered_function($1,f,r,t,e,i)
-            | DEF_scattered_variant(_,t,i,n,e,c,u,ty) -> DEF_scattered_variant($1,t,i,n,e,c,u,ty)) }
+            | DEF_scattered_variant(_,t,i,n,e,c,u,ty) -> DEF_scattered_variant($1,t,i,n,e,c,u,ty)
+            | _ -> assert false) }
   | Function_ Clause funcl
-    { dloc (DEF_funcl($1,$2,$3)) }
+    { dloc (DEF_scattered_funcl($1,$2,$3)) }
   | Union id Member atomic_typ id
     { dloc (DEF_scattered_unioncl($1,$2,$3,$4,$5)) }
   | End id 
@@ -791,7 +837,7 @@ defs_help:
 
 defs:
   | defs_help
-    { Defs($1) }
+    { (Defs $1) }
 
 file:
   | defs Eof
diff --git a/src/process_file.ml b/src/process_file.ml
index 5c7e4680..fe164957 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -56,9 +56,10 @@ let get_lexbuf fn =
                                   Lexing.pos_cnum = 0; };
     lexbuf
 
-let parse_file (f : string) : (bool Ast.defs * Ast.lex_skips) =
+let parse_file (f : string) : (Parse_ast.defs * Parse_ast.lex_skips) =
   let lexbuf = get_lexbuf f in
-    try
+  Parser.file (Lexer.token []) lexbuf
+(*    try
       Parser.file (Lexer.token []) lexbuf
     with
       | Parsing.Parse_error ->
@@ -67,7 +68,7 @@ let parse_file (f : string) : (bool Ast.defs * Ast.lex_skips) =
       | Ast.Parse_error_locn(l,m) ->
           raise "Parse error 2" (*Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))*)
       | Lexer.LexError(c,p) ->
-          raise "Lex error" (*Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, c))*)
+          raise "Lex error" (*Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, c))*)*)
 
 (* type instances = Types.instance list Types.Pfmap.t
 
diff --git a/src/process_file.mli b/src/process_file.mli
index 1fb8ea2f..55dbc6d1 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -46,7 +46,7 @@
 
 (* open Typed_ast *)
 
-val parse_file : string -> bool Ast.defs * Ast.lex_skips
+val parse_file : string -> Parse_ast.defs * Parse_ast.lex_skips
 
 (* type instances = Types.instance list Types.Pfmap.t