Experimenting with alternate parser

3 files changed, 468 insertions, 1320 deletions

diff --git a/src/lexer2.mll b/src/lexer2.mll
index 561adcfd..ebd806c4 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -49,37 +49,50 @@ 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 mk_operator n op =
+  match n with
+  | 0 -> Op0 op
+  | 1 -> Op1 op
+  | 2 -> Op2 op
+  | 3 -> Op3 op
+  | 4 -> Op4 op
+  | 5 -> Op5 op
+  | 6 -> Op6 op
+  | 7 -> Op7 op
+  | 8 -> Op8 op
+  | 9 -> Op9 op
+
+let operators = ref M.empty
+
 let kw_table =
   List.fold_left
     (fun r (x,y) -> M.add x y r)
     M.empty
     [
      ("and",                     (fun _ -> And));
-     ("alias",                   (fun _ -> Alias));
      ("as",                      (fun _ -> As));
      ("assert",                  (fun _ -> Assert));
      ("bitzero",                 (fun _ -> Bitzero));
      ("bitone",                  (fun _ -> Bitone));
-     ("bits",                    (fun _ -> Bits));
      ("by",                      (fun _ -> By));
-     ("case",			 (fun _ -> Case));
+     ("match",			 (fun _ -> Match));
      ("clause",                  (fun _ -> Clause));
      ("const",			 (fun _ -> Const));
      ("dec",                     (fun _ -> Dec));
      ("def",                     (fun _ -> Def));
+     ("op",                      (fun _ -> Op));
      ("default",		 (fun _ -> Default));
      ("deinfix",                 (fun _ -> Deinfix));
      ("effect",                  (fun _ -> Effect));
      ("Effect",                  (fun _ -> EFFECT));
      ("end",                     (fun _ -> End));
-     ("enumerate",		 (fun _ -> Enumerate));
+     ("enum",		         (fun _ -> Enum));
      ("else",                    (fun _ -> Else));
      ("exit",                    (fun _ -> Exit));
      ("extern",                  (fun _ -> Extern));
      ("cast",                    (fun _ -> Cast));
      ("false",                   (fun _ -> False));
      ("forall",                  (fun _ -> Forall));
-     ("exist",                   (fun _ -> Exist));
      ("foreach",                 (fun _ -> Foreach));
      ("function",                (fun x -> Function_));
      ("overload",                (fun _ -> Overload));
@@ -89,8 +102,7 @@ let kw_table =
      ("IN",                      (fun x -> IN));
      ("let",                     (fun x -> Let_));
      ("member",                  (fun x -> Member));
-     ("Nat",                     (fun x -> Nat));
-     ("Num",                     (fun x -> NatNum));
+     ("Int",                     (fun x -> Int));
      ("Order",                   (fun x -> Order));
      ("pure",                    (fun x -> Pure));
      ("rec",			 (fun x -> Rec));
@@ -104,7 +116,7 @@ let kw_table =
      ("then",                    (fun x -> Then));
      ("true",                    (fun x -> True));
      ("Type",                    (fun x -> TYPE));
-     ("typedef",		 (fun x -> Typedef));
+     ("type",		         (fun x -> Typedef));
      ("undefined",               (fun x -> Undefined));
      ("union",			 (fun x -> Union));
      ("with",                    (fun x -> With));
@@ -160,158 +172,50 @@ rule token = parse
   | "\n"
     { Lexing.new_line lexbuf;
       token lexbuf }
-
   | "&"					{ (Amp(r"&")) }
-  | "@"					{ (At(r"@")) }
   | "|"                                 { Bar }
   | "^"					{ (Carrot(r"^")) }
   | ":"                                 { Colon(r ":") }
   | ","                                 { Comma }
   | "."                                 { Dot }
   | "="                                 { (Eq(r"=")) }
-  | "!"					{ (Excl(r"!")) }
   | ">"					{ (Gt(r">")) }
   | "-"					{ Minus }
   | "<"					{ (Lt(r"<")) }
   | "+"					{ (Plus(r"+")) }
   | ";"                                 { Semi }
   | "*"                                 { (Star(r"*")) }
-  | "~"					{ (Tilde(r"~")) }
   | "_"                                 { Under }
   | "{"                                 { Lcurly }
   | "}"                                 { Rcurly }
+  | "()"                                { Unit(r"()") }
   | "("                                 { Lparen }
   | ")"                                 { Rparen }
   | "["                                 { Lsquare }
   | "]"                                 { Rsquare }
-  | "&&" as i                           { (AmpAmp(r i)) }
-  | "||"                                { BarBar }
-  | "||]"                               { BarBarSquare }
-  | "|]"				{ BarSquare }
-  | "^^"				{ (CarrotCarrot(r"^^")) }
-  | "::" as i                           { (ColonColon(r i)) }
-  | ":="                                { ColonEq }
-  | ":>"                                { ColonGt }
-  | ":]"                                { ColonSquare }
-  | ".."				{ DotDot }
-  | "=="				{ (EqEq(r"==")) }
   | "!="				{ (ExclEq(r"!=")) }
-  | "!!"				{ (ExclExcl(r"!!")) }
   | ">="				{ (GtEq(r">=")) }
-  | ">=+"				{ (GtEqPlus(r">=+")) }
-  | ">>"				{ (GtGt(r">>")) }
-  | ">>>"				{ (GtGtGt(r">>>")) }
-  | ">+"				{ (GtPlus(r">+")) }
-  | "#>>"				{ (HashGtGt(r"#>>")) }
-  | "#<<"				{ (HashLtLt(r"#<<")) }
   | "->"                                { MinusGt }
-  | "<:"                                { LtColon }
+  | "=>"                                { EqGt(r "=>") }
   | "<="				{ (LtEq(r"<=")) }
-  | "<=+"				{ (LtEqPlus(r"<=+")) }
-  | "<>"				{ (LtGt(r"<>")) }
-  | "<<"				{ (LtLt(r"<<")) }
-  | "<<<"				{ (LtLtLt(r"<<<")) }
-  | "<+"				{ (LtPlus(r"<+")) }
-  | "**"				{ (StarStar(r"**")) }
-  | "[|"                                { SquareBar }
-  | "[||"                               { SquareBarBar }
-  | "[:"                                { SquareColon }
-  | "~^"				{ (TildeCarrot(r"~^")) }
-
-  | "+_s"                               { (PlusUnderS(r"+_s")) }
-  | "-_s"                               { (MinusUnderS(r"-_s")) }
-  | ">=_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"                               { (StarUnderS(r"*_s")) }
-  | "**_s"				{ (StarStarUnderS(r"**_s")) }
-  | "**_si"				{ (StarStarUnderSi(r"**_si")) }
-  | "*_u"				{ (StarUnderU(r"*_u")) }
-  | "*_ui"				{ (StarUnderUi(r"*_ui")) }
-  | "2^"				{ (TwoCarrot(r"2^")) }
-  | "2**"				{ TwoStarStar }
-
-
+  | "infix" ws (digit as p) ws (oper_char+ as op)
+    { operators := M.add op (mk_operator (int_of_string (Char.escaped p)) op) !operators;
+      token lexbuf }
+  | oper_char+ as op
+    { try M.find op !operators
+      with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
   | "(*"        { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
   | "*)"        { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
-
+  | (tyvar_start startident ident* as i) ":" { TyDecl(r i) }
+  | (startident ident* as i) ":"        { Decl(r i) }
   | tyvar_start startident ident* as i  { TyVar(r i) }
   | startident ident* as i              { if M.mem i kw_table then
                                             (M.find i kw_table) ()
-                                          else if
+					  (* else if
                                             List.mem i default_type_names ||
                                             List.mem i !custom_type_names then
-					    TyId(r i)
-                                          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		{ (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)) }
-
+					    TyId(r i) *)
+					  else Id(r i) }
   | (digit+ as i1) "." (digit+ as i2)     { (Real (i1 ^ "." ^ i2)) }
   | "-" (digit* as i1) "." (digit+ as i2) { (Real ("-" ^ i1 ^ "." ^ i2)) }
   | digit+ as i                           { (Num(int_of_string i)) }
diff --git a/src/parser2.mly b/src/parser2.mly
index d6da6e63..c3dde8d3 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -46,96 +46,83 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
 
 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 idl i = Id_aux(i, loc())
-
-let efl e = BE_aux(e, 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 tlocl t l1 l2 = ATyp_aux(t,locn l1 l2)
-let lloc l = L_aux(l,loc ())
-let ploc p = P_aux(p,loc ())
-let fploc p = FP_aux(p,loc ())
-
-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 tdloc td = TD_aux(td, loc())
-let kdloc kd = KD_aux(kd, loc())
-let funloc fn = FD_aux(fn, loc())
-let vloc v = VS_aux(v, loc ())
-let sdloc sd = SD_aux(sd, loc ())
-let dloc d = d
-
-let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
-let mk_rec i = (Rec_aux((Rec_rec), 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 = Effect_opt_aux((Effect_opt_effect(e)),(locn i i))
-let mk_eannotn _ = Effect_opt_aux(Effect_opt_pure,Unknown)
-let mk_namesectn _ = Name_sect_aux(Name_sect_none,Unknown)
-
-let make_range_sugar_bounded typ1 typ2 =
-  ATyp_app(Id_aux(Id("range"),Unknown),[typ1; typ2;])
-let make_range_sugar typ1 =
-  make_range_sugar_bounded (ATyp_aux(ATyp_constant(0), Unknown)) typ1
-let make_atom_sugar typ1 =
-  ATyp_app(Id_aux(Id("atom"),Unknown),[typ1])
-
-let make_r bot top =
-  match bot,top with
-    | ATyp_aux(ATyp_constant b,_),ATyp_aux(ATyp_constant t,l) ->
-      ATyp_aux(ATyp_constant ((t-b)+1),l)
-    | bot,(ATyp_aux(_,l) as top) ->
-      ATyp_aux((ATyp_sum ((ATyp_aux (ATyp_sum (top, ATyp_aux(ATyp_constant 1,Unknown)), Unknown)),
-			  (ATyp_aux ((ATyp_neg bot),Unknown)))), l)				   
-
-let make_vector_sugar_bounded order_set is_inc name typ typ1 typ2 = 
-  let (rise,ord,name) = 
-    if order_set 
-    then if is_inc 
-      then (make_r typ1 typ2,ATyp_inc,name) 
-      else (make_r typ2 typ1,ATyp_dec,name) 
-    else if name = "vector" 
-    then (typ2, ATyp_default_ord,"vector_sugar_tb") (* rise not calculated, but top and bottom came from specification *)
-    else (typ2, ATyp_default_ord,"vector_sugar_r") (* rise and base not calculated, rise only from specification *) in
-  ATyp_app(Id_aux(Id(name),Unknown),[typ1;rise;ATyp_aux(ord,Unknown);typ])
-let make_vector_sugar order_set is_inc typ typ1 =
-  let zero = (ATyp_aux(ATyp_constant 0,Unknown)) in
-  let (typ1,typ2) = match (order_set,is_inc,typ1) with
-    | (true,true,ATyp_aux(ATyp_constant t,l)) -> zero,ATyp_aux(ATyp_constant (t-1),l)
-    | (true,true,ATyp_aux(_, l)) -> zero,ATyp_aux (ATyp_sum (typ1,
-    ATyp_aux(ATyp_neg(ATyp_aux(ATyp_constant 1,Unknown)), Unknown)), l)
-    | (true,false,_) -> typ1,zero 
-    | (false,_,_) -> zero,typ1 in
-  make_vector_sugar_bounded order_set is_inc "vector_sugar_r" typ typ1 typ2
+let loc n m = Range (m, n)
+
+let mk_id i n m = Id_aux (i, loc m n)
+let mk_kid str n m = Kid_aux (Var str, loc n m)
+
+let deinfix (Id_aux (Id v, l)) = Id_aux (DeIid v, l)
+
+let mk_typ t n m = ATyp_aux (t, loc n m)
+let mk_pat p n m = P_aux (p, loc n m)
+let mk_pexp p n m = Pat_aux (p, loc n m)
+let mk_exp e n m = E_aux (e, loc n m)
+let mk_lit l n m = L_aux (l, loc n m)
+let mk_lit_exp l n m = mk_exp (E_lit (mk_lit l n m)) n m
+let mk_typschm tq t n m = TypSchm_aux (TypSchm_ts (tq, t), loc n m)
+let mk_nc nc n m = NC_aux (nc, loc n m)
+
+let mk_funcl f n m = FCL_aux (f, loc n m)
+let mk_fun fn n m = FD_aux (fn, loc n m)
+let mk_td t n m = TD_aux (t, loc n m)
+let mk_vs v n m = VS_aux (v, loc n m)
+
+let qi_id_of_kopt (KOpt_aux (kopt_aux, l) as kopt) = QI_aux (QI_id kopt, l)
+
+let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
+let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
+let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
+let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
+let mk_namesectn = Name_sect_aux(Name_sect_none,Unknown)
+
+type lchain =
+  LC_lt
+| LC_lteq
+| LC_nexp of atyp
+
+let rec desugar_lchain chain s e =
+  match chain with
+  | [LC_nexp n1; LC_lteq; LC_nexp n2] ->
+    mk_nc (NC_bounded_le (n1, n2)) s e
+  | [LC_nexp n1; LC_lt; LC_nexp n2] ->
+    mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant 1) s e)) s e, n2)) s e
+  | (LC_nexp n1 :: LC_lteq :: LC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_le (n1, n2)) s e in
+    mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e
+  | (LC_nexp n1 :: LC_lt :: LC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_le (mk_typ (ATyp_sum (n1, mk_typ (ATyp_constant 1) s e)) s e, n2)) s e in
+    mk_nc (NC_and (nc1, desugar_lchain (LC_nexp n2 :: chain) s e)) s e
+  | _ -> assert false
+
+type rchain =
+  RC_gt
+| RC_gteq
+| RC_nexp of atyp
+
+let rec desugar_rchain chain s e =
+  match chain with
+  | [RC_nexp n1; RC_gteq; RC_nexp n2] ->
+    mk_nc (NC_bounded_ge (n1, n2)) s e
+  | [RC_nexp n1; RC_gt; RC_nexp n2] ->
+    mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant 1) s e)) s e)) s e
+  | (RC_nexp n1 :: RC_gteq :: RC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_ge (n1, n2)) s e in
+    mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
+  | (RC_nexp n1 :: RC_gt :: RC_nexp n2 :: chain) ->
+    let nc1 = mk_nc (NC_bounded_ge (n1, mk_typ (ATyp_sum (n2, mk_typ (ATyp_constant 1) s e)) s e)) s e in
+    mk_nc (NC_and (nc1, desugar_rchain (RC_nexp n2 :: chain) s e)) s e
+  | _ -> assert false
 
 %}
 
 /*Terminals with no content*/
 
-%token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End 
-%token Enumerate Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Nat NatNum Order Cast
-%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef 
+%token And As Assert Bitzero Bitone Bits By Match Clause Const Dec Def Default Deinfix Effect EFFECT End Op
+%token Enum Else Exit Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
+%token Pure Rec Register Return Scattered Sizeof Struct Switch Then True TwoStarStar Type TYPE Typedef
 %token Undefined Union With When Val Constraint
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
-
-/* Avoid shift/reduce conflict - see right_atomic_exp rule */
 %nonassoc Then
 %nonassoc Else
 
@@ -148,1203 +135,459 @@ let make_vector_sugar order_set is_inc typ typ1 =
 
 /*Terminals with content*/
 
-%token <string> Id TyVar TyId
+%token <string> Id TyVar Decl TyDecl
 %token <int> Num
 %token <string> String Bin Hex Real
 
-%token <string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde
-%token <string> AmpAmp CarrotCarrot Colon ColonColon EqEq ExclEq ExclExcl
+%token <string> Amp At Carrot  Div Eq Excl Gt Lt Plus Star Tilde EqGt Unit
+%token <string> Colon ExclEq
 %token <string> GtEq GtEqPlus GtGt GtGtGt GtPlus HashGtGt HashLtLt
 %token <string> LtEq LtEqPlus LtGt LtLt LtLtLt LtPlus StarStar TildeCarrot
 
 %token <string> GtEqUnderS GtEqUnderSi GtEqUnderU GtEqUnderUi GtGtUnderU GtUnderS
 %token <string> GtUnderSi GtUnderU GtUnderUi LtEqUnderS LtEqUnderSi LtEqUnderU
 %token <string> LtEqUnderUi LtUnderS LtUnderSi LtUnderU LtUnderUi StarStarUnderS StarStarUnderSi StarUnderS
-%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS 
-
-%token <string> AmpI AtI CarrotI  DivI EqI ExclI GtI LtI PlusI StarI TildeI
-%token <string> AmpAmpI CarrotCarrotI ColonColonI EqEqI ExclEqI ExclExclI
-%token <string> GtEqI GtEqPlusI GtGtI GtGtGtI GtPlusI HashGtGtI HashLtLtI
-%token <string> LtEqI LtEqPlusI LtGtI LtLtI LtLtLtI LtPlusI StarStarI TildeCarrotI
-
-%token <string> GtEqUnderSI GtEqUnderSiI GtEqUnderUI GtEqUnderUiI GtGtUnderUI GtUnderSI
-%token <string> GtUnderSiI GtUnderUI GtUnderUiI LtEqUnderSI LtEqUnderSiI LtEqUnderUI
-%token <string> LtEqUnderUiI LtUnderSI LtUnderSiI LtUnderUI LtUnderUiI StarStarUnderSI StarStarUnderSiI StarUnderSI
-%token <string> StarUnderSiI StarUnderUI StarUnderUiI TwoCarrotI
+%token <string> StarUnderSi StarUnderU StarUnderUi TwoCarrot PlusUnderS MinusUnderS
 
+%token <string> Op0 Op1 Op2 Op3 Op4 Op5 Op6 Op7 Op8 Op9
 
-%start file nonempty_exp_list
+%start file
 %type <Parse_ast.defs> defs
-%type <Parse_ast.atyp> typ
-%type <Parse_ast.pat> pat
-%type <Parse_ast.exp> exp
-%type <Parse_ast.exp list> nonempty_exp_list
 %type <Parse_ast.defs> file
 
-
 %%
 
 id:
   | Id
-    { idl (Id($1)) }
-  | Tilde
-    { idl (Id($1)) }
-  | 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 Quot Rparen
-    { idl (DeIid("quot")) }
-  | Lparen Deinfix QuotUnderS Rparen
-    { idl (DeIid("quot_s")) }
-  | Lparen Deinfix Eq Rparen
-    { Id_aux(DeIid($3),loc ()) }
-  | Lparen Deinfix Excl Lparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Gt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Lt Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix GtUnderS Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix LtUnderS Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Minus Rparen
-    { idl (DeIid("-")) }
-  | Lparen Deinfix MinusUnderS Rparen
-    { idl (DeIid("-_s")) }
-  | Lparen Deinfix Mod Rparen
-    { idl (DeIid("mod")) }
-  | Lparen Deinfix Plus Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix PlusUnderS Rparen
-    { idl (DeIid("+_s")) }
-  | Lparen Deinfix Star Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix StarUnderS Rparen
-    { idl (DeIid("*_s")) }
-  | Lparen Deinfix AmpAmp Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Bar Rparen
-    { idl (DeIid("|")) }
-  | Lparen Deinfix BarBar Rparen
-    { idl (DeIid("||")) }
-  | Lparen Deinfix CarrotCarrot Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix Colon Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix ColonColon 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 GtEqUnderS 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 LtEqUnderS 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 Tilde Rparen
-    { idl (DeIid($3)) }
-  | Lparen Deinfix TildeCarrot Rparen
-    { idl (DeIid($3)) }
-
-tid:
-  | TyId
-    { (idl (Id($1))) }
-
-tyvar:
+    { mk_id (Id $1) $startpos $endpos }
+  | Op Op1
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op2
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op3
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op4
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op5
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op6
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op7
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op8
+    { mk_id (DeIid $2) $startpos $endpos }
+  | Op Op9
+    { mk_id (DeIid $2) $startpos $endpos }
+
+op0: Op0 { mk_id (Id $1) $startpos $endpos }
+op1: Op1 { mk_id (Id $1) $startpos $endpos }
+op2: Op2 { mk_id (Id $1) $startpos $endpos }
+op3: Op3 { mk_id (Id $1) $startpos $endpos }
+op4: Op4 { mk_id (Id $1) $startpos $endpos }
+op5: Op5 { mk_id (Id $1) $startpos $endpos }
+op6: Op6 { mk_id (Id $1) $startpos $endpos }
+op7: Op7 { mk_id (Id $1) $startpos $endpos }
+op8: Op8 { mk_id (Id $1) $startpos $endpos }
+op9: Op9 { mk_id (Id $1) $startpos $endpos }
+
+decl:
+  | Decl
+    { mk_id (Id $1) $startpos $endpos }
+
+kid:
   | TyVar
-    { (Kid_aux((Var($1)),loc ())) }
+    { mk_kid $1 $startpos $endpos }
+
+tydecl:
+  | TyDecl
+    { mk_kid $1 $startpos $endpos }
 
-tyvars:
-  | tyvar
+kid_list:
+  | kid
     { [$1] }
-  | tyvar tyvars
+  | kid kid_list
     { $1 :: $2 }
 
-atomic_kind:
-  | TYPE
-    { bkloc BK_type }
-  | Nat
-    { bkloc BK_nat }
-  | NatNum
-    { bkloc BK_nat }
-  | Order
-    { bkloc BK_order }
-  | EFFECT
-    { bkloc BK_effect }
+nc:
+  | nc Bar nc_and
+    { mk_nc (NC_or ($1, $3)) $startpos $endpos }
+  | nc_and
+    { $1 }
+
+nc_and:
+  | nc_and Amp atomic_nc
+    { mk_nc (NC_and ($1, $3)) $startpos $endpos }
+  | atomic_nc
+    { $1 }
 
-kind_help:
-  | atomic_kind
-    { [ $1 ] }
-  | atomic_kind MinusGt kind_help
-    { $1::$3 }
+atomic_nc:
+  | True
+    { mk_nc NC_true $startpos $endpos }
+  | False
+    { mk_nc NC_false $startpos $endpos }
+  | typ Eq typ
+    { mk_nc (NC_fixed ($1, $3)) $startpos $endpos }
+  | typ ExclEq typ
+    { mk_nc (NC_not_equal ($1, $3)) $startpos $endpos }
+  | nc_lchain
+    { desugar_lchain $1 $startpos $endpos }
+  | nc_rchain
+    { desugar_rchain $1 $startpos $endpos }
+  | Lparen nc Rparen
+    { $2 }
+  | kid In Lcurly num_list Rcurly
+    { mk_nc (NC_nat_set_bounded ($1, $4)) $startpos $endpos }
 
-kind:
-  | kind_help
-    { K_aux(K_kind($1), loc ()) }
-
-effect:
-  | Barr
-    { efl BE_barr }
-  | Depend
-    { efl BE_depend }
-  | Rreg 
-    { efl BE_rreg }
-  | Wreg
-    { efl BE_wreg }
-  | Rmem
-    { efl BE_rmem } 
-  | Rmemt
-    { efl BE_rmemt } 
-  | Wmem
-    { efl BE_wmem }
-  | Wmv
-    { efl BE_wmv }
-  | Wmvt
-    { efl BE_wmvt }
-  | Eamem
-    { efl BE_eamem }
-  | Exmem
-    { efl BE_exmem }
-  | Undef
-    { efl BE_undef }
-  | Unspec
-    { efl BE_unspec }
-  | Nondet
-      { efl BE_nondet }
-  | Escape
-      { efl BE_escape }
-
-effect_list:
-  | effect
-    { [$1] }
-  | effect Comma effect_list
-    { $1::$3 }
-
-effect_typ:
-  | Lcurly effect_list Rcurly
-    { tloc (ATyp_set($2)) }
-  | Pure
-    { tloc (ATyp_set([])) }
-
-vec_typ:
-  | tid Lsquare nexp_typ Rsquare
-      { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
-  | tid Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
-  | tid Lsquare nexp_typ LtColon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
-  | tid Lsquare nexp_typ ColonGt nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
-  | tyvar Lsquare nexp_typ Rsquare
-      { tloc (make_vector_sugar false false (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) }
-  | tyvar Lsquare nexp_typ Colon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded false false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
-  | tyvar Lsquare nexp_typ LtColon nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true true "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
-  | tyvar Lsquare nexp_typ ColonGt nexp_typ Rsquare
-      { tloc (make_vector_sugar_bounded true false "vector" (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) }
-
-app_typs:
-  | atomic_typ
+num_list:
+  | Num
     { [$1] }
-  | atomic_typ Comma app_typs
-    { $1::$3 }
+  | Num Comma num_list
+    { $1 :: $3 }
+
+nc_lchain:
+  | typ LtEq typ
+    { [LC_nexp $1; LC_lteq; LC_nexp $3] }
+  | typ Lt typ
+    { [LC_nexp $1; LC_lt; LC_nexp $3] }
+  | typ LtEq nc_lchain
+    { LC_nexp $1 :: LC_lteq :: $3 }
+  | typ Lt nc_lchain
+    { LC_nexp $1 :: LC_lt :: $3 }
+
+nc_rchain:
+  | typ GtEq typ
+    { [RC_nexp $1; RC_gteq; RC_nexp $3] }
+  | typ Gt typ
+    { [RC_nexp $1; RC_gt; RC_nexp $3] }
+  | typ GtEq nc_rchain
+    { RC_nexp $1 :: RC_gteq :: $3 }
+  | typ Gt nc_rchain
+    { RC_nexp $1 :: RC_gt :: $3 }
 
-atomic_typ:
-  | vec_typ
-    { $1 }
-  | range_typ
-    { $1 }
-  | nexp_typ
-    { $1 }
-  | Inc
-    { tloc (ATyp_inc) }
-  | Dec
-    { tloc (ATyp_dec) }
-  | tid Lt app_typs Gt
-    { tloc (ATyp_app($1,$3)) }
-  | Register Lt app_typs Gt
-    { tloc (ATyp_app(Id_aux(Id "register", locn 1 1),$3)) }
-
-range_typ:
-  | SquareBar nexp_typ BarSquare
-      { tloc (make_range_sugar $2) }
-  | SquareBar nexp_typ Colon nexp_typ BarSquare
-      { tloc (make_range_sugar_bounded $2 $4) }
-  | SquareColon nexp_typ ColonSquare
-      { tloc (make_atom_sugar $2) }
-
-nexp_typ:
-  | nexp_typ Plus nexp_typ2
-    { tloc (ATyp_sum ($1, $3)) }
-  | nexp_typ Minus nexp_typ2
-    { tloc (ATyp_minus ($1, $3)) }
-  | Minus nexp_typ2
-    { tloc (ATyp_neg $2) }
-  | nexp_typ2
+typ:
+  | typ0
     { $1 }
+  | Lparen typ Comma typ_list Rparen
+    { mk_typ (ATyp_tup ($2 :: $4)) $startpos $endpos }
+  | Lcurly kid_list Dot typ Rcurly
+    { mk_typ (ATyp_exist ($2, NC_aux (NC_true, loc $startpos $endpos), $4)) $startpos $endpos }
+  | Lcurly kid_list Comma nc Dot typ Rcurly
+    { mk_typ (ATyp_exist ($2, $4, $6)) $startpos $endpos }
 
-nexp_typ2:
-  | nexp_typ2 Star nexp_typ3
-    { tloc (ATyp_times ($1, $3)) }
-  | nexp_typ3
-    { $1 }
+typ0:
+  | typ1 op0 typ1 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ1 { $1 }
 
-nexp_typ3:
-  | TwoStarStar nexp_typ4
-     { tloc (ATyp_exp $2) }
-  | nexp_typ4
-     { $1 }
+typ1:
+  | typ2 op1 typ2 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ2 { $1 }
 
-nexp_typ4:
-  | Num
-    { tlocl (ATyp_constant $1) 1 1 }
-  | tid
-    { tloc (ATyp_id $1) }
-  | Lcurly id Rcurly
-    { tloc (ATyp_id $2) }
-  | tyvar
-    { tloc (ATyp_var $1) }
-  | Lparen exist_typ Rparen
-    { $2 }
+typ2:
+  | typ3 op2 typ3 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ3 { $1 }
 
-tup_typ_list:
-   | atomic_typ Comma atomic_typ
-       { [$1;$3] }
-   | atomic_typ Comma tup_typ_list
-       { $1::$3 }
-
-tup_typ:
-   | atomic_typ
-     { $1 }
-   | Lparen tup_typ_list Rparen
-     { tloc (ATyp_tup $2) }
-
-exist_typ:
-  | Exist tyvars Comma nexp_constraint Dot tup_typ
-    { tloc (ATyp_exist ($2, $4, $6)) }
-  | Exist tyvars Dot tup_typ
-    { tloc (ATyp_exist ($2, NC_aux (NC_true, loc ()), $4)) }
-  | tup_typ
-    { $1 }
+typ3:
+  | typ4 op3 typ4 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ4 { $1 }
 
-typ:
-  | exist_typ
-    { $1 }
-  | tup_typ MinusGt exist_typ Effect effect_typ
-    { tloc (ATyp_fn($1,$3,$5)) }
+typ4:
+  | typ5 op4 typ5 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ5 { $1 }
 
-lit:
-  | True
-    { lloc L_true }
-  | False
-    { lloc L_false }
-  | Num
-    { lloc (L_num $1) }
-  | String
-    { lloc (L_string $1) }
-  | Lparen Rparen
-    { lloc L_unit }
-  | Bin
-    { lloc (L_bin $1) }
-  | Hex
-    { lloc (L_hex $1) }
-  | Real
-    { lloc (L_real $1) }
-  | Undefined
-    { lloc L_undef }
-  | Bitzero
-    { lloc L_zero }
-  | Bitone
-    { lloc L_one }
+typ5:
+  | typ6 op5 typ6 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ6 { $1 }
 
-atomic_pat:
-  | lit
-    { ploc (P_lit $1) }
-  | Under
-    { ploc P_wild }
-  | Lparen pat As id Rparen
-    { ploc (P_as($2,$4)) }
-  | Lparen exist_typ Rparen atomic_pat
-    { ploc (P_typ($2,$4)) }
-  | id
-    { ploc (P_app($1,[])) }
-  | Lcurly fpats Rcurly
-    { ploc (P_record((fst $2, snd $2))) }
-  | Lsquare comma_pats Rsquare
-    { ploc (P_vector($2)) }
-  | Lsquare pat Rsquare
-    { ploc (P_vector([$2])) }
-  | Lsquare Rsquare
-    { ploc (P_vector []) }
-  | Lsquare npats Rsquare
-    { ploc (P_vector_indexed($2)) }
-  | Lparen comma_pats Rparen
-    { ploc (P_tup($2)) }
-  | SquareBarBar BarBarSquare
-    { ploc (P_list([])) }
-  | SquareBarBar pat BarBarSquare
-    { ploc (P_list([$2])) }
-  | SquareBarBar comma_pats BarBarSquare
-    { ploc (P_list($2)) }
-  | atomic_pat ColonColon pat
-    { ploc (P_cons ($1, $3)) }
-  | Lparen pat Rparen
-    { $2 }
+typ6:
+  | typ7 op6 typ7 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ7 { $1 }
 
-app_pat:
-  | atomic_pat
-    { $1 }
-  | id Lparen comma_pats Rparen
-    { ploc (P_app($1,$3)) }
-  | id Lparen pat Rparen
-    { ploc (P_app($1,[$3])) }
+typ7:
+  | typ8 op7 typ8 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ8 { $1 }
 
-pat_colons:
-  | atomic_pat Colon atomic_pat
-    { ([$1;$3]) }
-  | atomic_pat Colon pat_colons
-    { ($1::$3) }
+typ8:
+  | typ9 op8 typ9 { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | typ9 { $1 }
 
-pat:
-  | app_pat
-    { $1 }
-  | pat_colons
-    { ploc (P_vector_concat($1)) }
-
-comma_pats:
-  | atomic_pat Comma atomic_pat
-    { [$1;$3] }
-  | atomic_pat Comma comma_pats
-    { $1::$3 }
-
-fpat:
-  | id Eq pat
-    { fploc (FP_Fpat($1,$3)) }
-
-fpats:
-  | fpat
-    { ([$1], false) }
-  | fpat Semi
-    { ([$1], true) }
-  | fpat Semi fpats
-    { ($1::fst $3, snd $3) }
-
-npat:
-  | Num Eq pat
-    { ($1,$3) }
-
-npats:
-  | npat
-    { [$1] }
-  | npat Comma npats
-    { ($1::$3) }
+typ9:
+  | atomic_typ op9 atomic_typ { mk_typ (ATyp_app (deinfix $2, [$1; $3])) $startpos $endpos }
+  | atomic_typ { $1 }
 
-atomic_exp:
-  | Lcurly semi_exps Rcurly
-    { eloc (E_block $2) }
-  | Nondet Lcurly semi_exps Rcurly
-    { eloc (E_nondet $3) }
+atomic_typ:
   | id
-    { eloc (E_id($1)) }
-  | lit
-    { eloc (E_lit($1)) }
-  | Lparen exp Rparen
+    { mk_typ (ATyp_id $1) $startpos $endpos }
+  | kid
+    { mk_typ (ATyp_var $1) $startpos $endpos }
+  | Num
+    { mk_typ (ATyp_constant $1) $startpos $endpos }
+  | Dec
+    { mk_typ ATyp_dec $startpos $endpos }
+  | Inc
+    { mk_typ ATyp_inc $startpos $endpos }
+  | id Lparen typ_list Rparen
+    { mk_typ (ATyp_app ($1, $3)) $startpos $endpos }
+  | Lparen typ Rparen
     { $2 }
-  | Lparen exist_typ Rparen atomic_exp
-    { eloc (E_cast($2,$4)) }
-  | Lparen comma_exps Rparen
-    { eloc (E_tuple($2)) }
-  | Lcurly exp With semi_exps Rcurly
-    { eloc (E_record_update($2,$4)) } 
-  | Lsquare Rsquare
-    { eloc (E_vector([])) }
-  | Lsquare exp Rsquare
-    { eloc (E_vector([$2])) }
-  | Lsquare comma_exps Rsquare
-    { eloc (E_vector($2)) }
-  | Lsquare comma_exps Semi Default Eq exp Rsquare
-    { eloc (E_vector_indexed($2,(Def_val_aux(Def_val_dec $6, locn 3 6)))) }
-  | Lsquare exp With atomic_exp Eq exp Rsquare
-    { 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)) }
-  | SquareBarBar BarBarSquare
-      { eloc (E_list []) }
-  | SquareBarBar exp BarBarSquare
-      { eloc (E_list [$2]) }
-  | SquareBarBar comma_exps BarBarSquare
-    { eloc (E_list($2)) }
-  | Switch exp Lcurly case_exps Rcurly
-    { eloc (E_case($2,$4)) }
-  | Sizeof atomic_typ
-    { eloc (E_sizeof($2)) }
-  | Constraint Lparen nexp_constraint Rparen
-    { eloc (E_constraint $3) }
-  | Exit atomic_exp
-      { eloc (E_exit $2) }
-  | Return atomic_exp
-      { eloc (E_return $2) }
-  | Assert Lparen exp Comma exp Rparen
-      { eloc (E_assert ($3,$5)) }
-
-field_exp:
-  | atomic_exp
-    { $1 }
-  | atomic_exp Dot id
-    { eloc (E_field($1,$3)) }
 
-vaccess_exp:
-  | field_exp
-    { $1 }
-  | atomic_exp Lsquare exp Rsquare
-    { eloc (E_vector_access($1,$3)) }
-  | atomic_exp Lsquare exp DotDot exp Rsquare
-    { eloc (E_vector_subrange($1,$3,$5)) }
+typ_list:
+  | typ
+    { [$1] }
+  | typ Comma typ_list
+    { $1 :: $3 }
 
-app_exp:
-  | vaccess_exp
-    { $1 }
-  | id Lparen Rparen
-    { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) }
-  /* we wrap into a tuple here, but this is unwrapped in initial_check.ml */
-  | id Lparen exp Rparen
-    { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) }
-  | id Lparen comma_exps Rparen
-    { eloc (E_app($1,[E_aux (E_tuple $3,locn 3 3)])) }
-
-right_atomic_exp:
-  | If_ exp Then exp Else exp
-    { eloc (E_if($2,$4,$6)) }
-  | If_ exp Then exp
-    { eloc (E_if($2,$4, eloc (E_lit(lloc L_unit)))) }
-  | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp In typ Rparen exp
-    { if $4 <> "from" then
-       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $6 <> "to" then
-       raise (Parse_error_locn ((loc ()),"Missing \"to\" in foreach loop"));
-      eloc (E_for($3,$5,$7,$9,$11,$13)) }
-  | Foreach Lparen id Id atomic_exp Id atomic_exp By atomic_exp Rparen exp
-    { if $4 <> "from" then
-       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $6 <> "to" && $6 <> "downto" then
-       raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
-      let order =
-        if $6 = "to"
-        then ATyp_aux(ATyp_inc,(locn 6 6))
-        else ATyp_aux(ATyp_dec,(locn 6 6)) in
-      eloc (E_for($3,$5,$7,$9,order,$11)) }
-  | Foreach Lparen id Id atomic_exp Id atomic_exp Rparen exp
-    { if $4 <> "from" then
-       raise (Parse_error_locn ((loc ()),"Missing \"from\" in foreach loop"));
-      if $6 <> "to" && $6 <> "downto" then
-       raise (Parse_error_locn ((loc ()),"Missing \"to\" or \"downto\" in foreach loop"));
-      let step = eloc (E_lit(lloc (L_num 1))) in
-      let ord =
-        if $6 = "to"
-        then ATyp_aux(ATyp_inc,(locn 6 6))
-        else ATyp_aux(ATyp_dec,(locn 6 6)) in
-      eloc (E_for($3,$5,$7,step,ord,$9)) }
-  | letbind In exp
-    { eloc (E_let($1,$3)) }
-
-starstar_exp:
-  | app_exp
-    { $1 }
-  | starstar_exp StarStar app_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-/* this is where we diverge from the non-right_atomic path;
-   here we go directly to right_atomic whereas the other one
-   goes through app_exp, vaccess_exp and field_exp too. */
-starstar_right_atomic_exp:
-  | right_atomic_exp
-    { $1 }
-  | starstar_exp StarStar right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+base_kind:
+  | Int
+    { BK_aux (BK_nat, loc $startpos $endpos) }
+  | TYPE
+    { BK_aux (BK_type, loc $startpos $endpos) }
+  | Order
+    { BK_aux (BK_order, loc $startpos $endpos) }
 
-star_exp:
-  | starstar_exp
-    { $1 }
-  | star_exp Star starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div_ starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) }
-  | star_exp Quot starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) }
-  | star_exp QuotUnderS starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) }
-  | star_exp Rem starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
-  | star_exp Mod starstar_exp
-      { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
-  | star_exp ModUnderS starstar_exp
-      { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) }
-  | star_exp StarUnderS starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderSi starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderU starstar_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderUi starstar_exp
-    { 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,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp Div_ starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("div"), locn 2 2), $3)) }
-  | star_exp Quot starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot"), locn 2 2), $3)) }
-  | star_exp QuotUnderS starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("quot_s"), locn 2 2), $3)) }
-  | star_exp Rem starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("rem"), locn 2 2), $3)) }
-  | star_exp Mod starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("mod"), locn 2 2), $3)) }
-  | star_exp ModUnderS starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("mod_s"), locn 2 2), $3)) }
-  | star_exp StarUnderS starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderSi starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderU starstar_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | star_exp StarUnderUi starstar_right_atomic_exp
-    { 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,Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp PlusUnderS star_exp
-    { eloc (E_app_infix($1, Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp Minus star_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
-  | plus_exp MinusUnderS star_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-_s"),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,Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp Minus star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-"), locn 2 2), $3)) }
-  | plus_exp PlusUnderS star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | plus_exp MinusUnderS star_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("-_s"), locn 2 2), $3)) }
-
-shift_exp:
-  | plus_exp
-    { $1 }
-  | shift_exp GtGt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp GtGtGt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLtLt plus_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-shift_right_atomic_exp:
-  | plus_right_atomic_exp
-    { $1 }
-  | shift_exp GtGt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp GtGtGt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | shift_exp LtLtLt plus_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-
-cons_exp:
-  | shift_exp
-    { $1 }
-  | shift_exp ColonColon cons_exp
-    { eloc (E_cons($1,$3)) }
-  | shift_exp Colon cons_exp
-    { eloc (E_vector_append($1, $3)) }
+kind:
+  | base_kind
+    { K_aux (K_kind [$1], loc $startpos $endpos) }
+
+kopt:
+  | tydecl kind
+    { KOpt_aux (KOpt_kind ($2, $1), loc $startpos $endpos) }
+  | Lparen kid Colon kind Rparen
+    { KOpt_aux (KOpt_kind ($4, $2), loc $startpos $endpos) }
+  | kid
+    { KOpt_aux (KOpt_none $1, loc $startpos $endpos) }
+
+kopt_list:
+  | kopt
+    { [$1] }
+  | kopt kopt_list
+    { $1 :: $2 }
 
-cons_right_atomic_exp:
-  | shift_right_atomic_exp
-    { $1 }
-  | shift_exp ColonColon cons_right_atomic_exp
-    { eloc (E_cons($1,$3)) }
-  | shift_exp Colon cons_right_atomic_exp
-    { eloc (E_vector_append($1, $3)) }
+typquant:
+  | kopt_list Comma nc
+    { let qi_nc = QI_aux (QI_const $3, loc $startpos($3) $endpos($3)) in
+      TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1 @ [qi_nc]), loc $startpos $endpos) }
+  | kopt_list
+    { TypQ_aux (TypQ_tq (List.map qi_id_of_kopt $1), loc $startpos $endpos) }
+
+typschm:
+  | typ MinusGt typ
+    { (fun s e -> mk_typschm mk_typqn (mk_typ (ATyp_fn ($1, $3, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
+  | Forall typquant Dot typ MinusGt typ
+    { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, mk_typ (ATyp_set []) s e)) s e) s e) $startpos $endpos }
 
-at_exp:
-  | cons_exp
-    { $1 }
-  | cons_exp At at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp CarrotCarrot at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp Carrot at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp TildeCarrot at_exp
-    { 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,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp CarrotCarrot at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp Carrot at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | cons_exp TildeCarrot at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-
-eq_exp:
-  | at_exp
-    { $1 }
-  /* XXX check for consistency */
-  | eq_exp Eq at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp EqEq at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ExclEq at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEq at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderS at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderU at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Gt at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderS at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderU at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEq at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEqUnderS at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Lt at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderS at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderSi at_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderU at_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  /* XXX assignement should not have the same precedence as equal,
-  otherwise a := b > c requires extra parens... */
-  | eq_exp ColonEq at_exp
-    { eloc (E_assign($1,$3)) }
-
-eq_right_atomic_exp:
-  | at_right_atomic_exp
-    { $1 }
-  | eq_exp Eq at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp EqEq at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ExclEq at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEq at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderS at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtEqUnderU at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Gt at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderS at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp GtUnderU at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEq at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtEqUnderS at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp Lt at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderS at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderSi at_right_atomic_exp
-    { eloc (E_app_infix ($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp LtUnderU at_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp ColonEq at_right_atomic_exp
-    { eloc (E_assign($1,$3)) }
-
-and_exp:
-  | eq_exp
+pat:
+  | atomic_pat
     { $1 }
-  | eq_exp Amp and_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp AmpAmp and_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+  | atomic_pat As id
+    { mk_pat (P_as ($1, $3)) $startpos $endpos }
+  | Lparen pat Comma pat_list Rparen
+    { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
 
-and_right_atomic_exp:
-  | eq_right_atomic_exp
-    { $1 }
-  | eq_exp Amp and_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
-  | eq_exp AmpAmp and_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id($2), locn 2 2), $3)) }
+pat_list:
+  | pat
+    { [$1] }
+  | pat Comma pat_list
+    { $1 :: $3 }
 
-or_exp:
-  | and_exp
-    { $1 }
-  | and_exp Bar or_exp
-    { eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) }
-  | and_exp BarBar or_exp
-    { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
+atomic_pat:
+  | Under
+    { mk_pat (P_wild) $startpos $endpos }
+  | lit
+    { mk_pat (P_lit $1) $startpos $endpos }
+  | id
+    { mk_pat (P_id $1) $startpos $endpos }
+  | pat Colon typ
+    { mk_pat (P_typ ($3, $1)) $startpos $endpos }
+  | decl typ
+    { mk_pat (P_typ ($2, mk_pat (P_id $1) $startpos $endpos($1))) $startpos $endpos }
+  | Lparen pat Rparen
+    { $2 }
 
-or_right_atomic_exp:
-  | and_right_atomic_exp
-    { $1 }
-  | and_exp Bar or_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("|"), locn 2 2), $3)) }
-  | and_exp BarBar or_right_atomic_exp
-    { eloc (E_app_infix($1,Id_aux(Id("||"), locn 2 2), $3)) }
+lit:
+  | True
+    { mk_lit L_true $startpos $endpos }
+  | False
+    { mk_lit L_false $startpos $endpos }
+  | Unit
+    { mk_lit L_unit $startpos $endpos }
+  | Num
+    { mk_lit (L_num $1) $startpos $endpos }
+  | Undefined
+    { mk_lit L_undef $startpos $endpos }
 
 exp:
-  | or_exp
-    { $1 }
-  | or_right_atomic_exp
+  | cast_exp Colon typ
+    { mk_exp (E_cast ($3, $1)) $startpos $endpos }
+  | cast_exp
     { $1 }
 
-comma_exps:
-  | exp Comma exp
-    { [$1;$3] }
-  | exp Comma comma_exps
-    { $1::$3 }
+cast_exp:
+  | atomic_exp
+    { $1 }
+  | atomic_exp Eq cast_exp
+    { mk_exp (E_assign ($1, $3)) $startpos $endpos }
+  | Let_ letbind In cast_exp
+    { mk_exp (E_let ($2, $4)) $startpos $endpos }
+  | Lcurly block Rcurly
+    { mk_exp (E_block $2) $startpos $endpos }
+  | Return cast_exp
+    { mk_exp (E_return $2) $startpos $endpos }
+  | If_ exp Then cast_exp Else cast_exp
+    { mk_exp (E_if ($2, $4, $6)) $startpos $endpos }
+  | Match atomic_exp Lcurly case_list Rcurly
+    { mk_exp (E_case ($2, $4)) $startpos $endpos }
+  | Lparen exp Comma exp_list Rparen
+    { mk_exp (E_tuple ($2 :: $4)) $startpos $endpos }
+
+case:
+  | pat EqGt exp
+    { mk_pexp (Pat_exp ($1, $3)) $startpos $endpos }
+  | pat If_ exp EqGt exp
+    { mk_pexp (Pat_when ($1, $3, $5)) $startpos $endpos }
+
+case_list:
+  | case
+    { [$1] }
+  | case Comma case_list
+    { $1 :: $3 }
 
-semi_exps_help:
+block:
   | exp
     { [$1] }
-  | exp Semi
+  | If_ exp Then exp Semi block
+    { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $startpos($5) $endpos($5))) $startpos $endpos($5) :: $6 }
+  | Let_ letbind Semi block
+    { [mk_exp (E_let ($2, mk_exp (E_block $4) $startpos($4) $endpos)) $startpos $endpos] }
+  | exp Semi /* Allow trailing semicolon in block */
     { [$1] }
-  | exp Semi semi_exps_help
-    { $1::$3 }
+  | exp Semi block
+    { $1 :: $3 }
 
-semi_exps:
-  |
-    { [] }
-  | semi_exps_help
-    { $1 }
+%inline letbind:
+  | pat Eq exp
+    { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
 
-case_exp:
-  | Case patsexp
+atomic_exp:
+  | lit
+    { mk_exp (E_lit $1) $startpos $endpos }
+  | decl typ
+    { mk_exp (E_cast ($2, mk_exp (E_id $1) $startpos $endpos($1))) $startpos $endpos }
+  | id
+    { mk_exp (E_id $1) $startpos $endpos }
+  | id Unit
+    { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
+  | id Lparen exp_list Rparen
+    { mk_exp (E_app ($1, $3)) $startpos $endpos }
+  | Lparen exp Rparen
     { $2 }
 
-case_exps:
-  | case_exp
+exp_list:
+  | exp
     { [$1] }
-  | case_exp case_exps
-    { $1::$2 }
+  | exp Comma exp_list
+    { $1 :: $3 }
 
-patsexp:
-  | atomic_pat MinusGt exp
-    { peloc (Pat_exp($1,$3)) }
-  | atomic_pat When exp MinusGt exp
-    { peloc (Pat_when ($1, $3, $5)) }
-
-letbind:
-  | Let_ atomic_pat Eq exp
-    { lbloc (LB_val_implicit($2,$4)) }
-  | Let_ typquant atomic_typ atomic_pat Eq exp
-    { lbloc (LB_val_explicit((mk_typschm $2 $3 2 3),$4,$6)) }
-/* This introduces one shift reduce conflict, that basically points out that an atomic_pat with a type declared is the Same as this
-  | Let_ Lparen typ Rparen atomic_pat Eq exp 
-    { assert false (* lbloc (LB_val_explicit((mk_typschm (mk_typqn ()) $2 2 2),$3,$5)) *)} */
+cast_exp_list:
+  | cast_exp
+    { [$1] }
+  | cast_exp Comma exp_list
+    { $1 :: $3 }
 
 funcl:
-  | id atomic_pat Eq exp
-    { funclloc (FCL_Funcl($1,$2,$4)) }
+  | id pat Eq exp
+    { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
 
-funcl_ands:
-  | funcl
+type_def:
+  | Typedef id typquant Eq typ
+    { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm $3 $5 $startpos($3) $endpos)) $startpos $endpos }
+  | Typedef id Eq typ
+    { mk_td (TD_abbrev ($2, mk_namesectn, mk_typschm mk_typqn $4 $startpos($4) $endpos)) $startpos $endpos }
+  | Struct id typquant Eq Lcurly struct_fields Rcurly
+    { mk_td (TD_record ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+  | Enum id Eq enum_bar
+    { mk_td (TD_enum ($2, mk_namesectn, $4, false)) $startpos $endpos }
+  | Enum id Eq Lcurly enum Rcurly
+    { mk_td (TD_enum ($2, mk_namesectn, $5, false)) $startpos $endpos }
+  | Union id typquant Eq Lcurly type_unions Rcurly
+    { mk_td (TD_variant ($2, mk_namesectn, $3, $6, false)) $startpos $endpos }
+
+enum_bar:
+  | id
     { [$1] }
-  | funcl And funcl_ands
-    { $1::$3 }
+  | id Bar enum_bar
+    { $1 :: $3 }
 
-/* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/
-fun_def:
-  | Function_ Rec typquant typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) }
-  | Function_ Rec typquant typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) }
-  | Function_ Rec Effect effect_typ funcl_ands 
-    { funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $4 4, $5)) }
-  | Function_ Rec typ funcl_ands
-    { funloc (FD_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
-  | Function_ Rec funcl_ands
-    { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) }
-  | Function_ typquant typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) }
-  | Function_ typquant typ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) }
-  | Function_ typ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) }
-  | Function_ Effect effect_typ funcl_ands
-    { funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $3 3, $4)) }
-  | Function_ typ funcl_ands
-    { funloc (FD_function(mk_recn (),mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
-  | Function_ funcl_ands
-    { funloc (FD_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
-
-
-val_spec:
-  | Val typquant typ id
-    { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
-  | Val typ id
-    { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
-  | Val Cast typquant typ id
-    { vloc (VS_cast_spec (mk_typschm $3 $4 3 4,$5)) }
-  | Val Cast typ id
-    { vloc (VS_cast_spec (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
-  | Val Extern typquant typ id
-    { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
-  | Val Extern typ id
-    { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
-  | Val Extern typquant typ id Eq String
-    { vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
-  | Val Extern typ id Eq String
-    { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
-
-kinded_id:
-  | tyvar
-    { kiloc (KOpt_none $1) }
-  | kind tyvar
-    { kiloc (KOpt_kind($1,$2))}
-
-/*kinded_ids:
-  | kinded_id
+enum:
+  | id
     { [$1] }
-  | kinded_id kinded_ids
-    { $1::$2 }*/
+  | id Comma enum
+    { $1 :: $3 }
 
-nums:
-  | Num
-    { [$1] }
-  | Num Comma nums
-    { $1::$3 }
+struct_field:
+  | decl typ
+    { ($2, $1) }
+  | id Colon typ
+    { ($3, $1) }
 
-nexp_constraint:
-  | nexp_constraint1
-    { $1 }
-  | nexp_constraint1 Bar nexp_constraint
-    { NC_aux (NC_or ($1, $3), loc ()) }
-
-nexp_constraint1:
-  | nexp_constraint2
-    { $1 }
-  | nexp_constraint2 Amp nexp_constraint1
-    { NC_aux (NC_and ($1, $3), loc ()) }
-
-nexp_constraint2:
-  | nexp_typ Eq nexp_typ
-    { NC_aux(NC_fixed($1,$3), loc () ) }
-  | nexp_typ ExclEq nexp_typ
-    { NC_aux (NC_not_equal ($1, $3), loc ()) }
-  | nexp_typ GtEq nexp_typ
-    { NC_aux(NC_bounded_ge($1,$3), loc () ) }
-  | nexp_typ LtEq nexp_typ
-    { NC_aux(NC_bounded_le($1,$3), loc () ) }
-  | tyvar In Lcurly nums Rcurly
-    { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
-  | tyvar IN Lcurly nums Rcurly
-    { NC_aux(NC_nat_set_bounded($1,$4), loc ()) }
-  | True
-    { NC_aux (NC_true, loc ()) }
-  | False
-    { NC_aux (NC_false, loc ()) }
-  | Lparen nexp_constraint Rparen
-    { $2 }
+struct_fields:
+  | struct_field
+    { [$1] }
+  | struct_field Comma
+    { [$1] }
+  | struct_field Comma struct_fields
+    { $1 :: $3 }
+
+type_union:
+  | decl typ
+    { Tu_aux (Tu_ty_id ($2, $1), loc $startpos $endpos) }
+  | id Colon typ
+    { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) }
+  | id
+    { Tu_aux (Tu_id $1, loc $startpos $endpos) }
 
-id_constraint:
-  | nexp_constraint
-      { QI_aux((QI_const $1), loc())}
-  | kinded_id
-      { QI_aux((QI_id $1), loc()) }
+type_unions:
+  | type_union
+    { [$1] }
+  | type_union Comma
+    { [$1] }
+  | type_union Comma type_unions
+    { $1 :: $3 }
 
-id_constraints:
-  | id_constraint
-      { [$1] }
-  | id_constraint Comma id_constraints
-      { $1::$3 }
+fun_def:
+  | Function_ funcl
+    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
 
-typquant:
-  | Forall id_constraints Dot
-    { typql(TypQ_tq($2)) }
-
-name_sect:
-  | Lsquare Id Eq String Rsquare
-    {
-      if $2 <> "name" then
-       raise (Parse_error_locn ((loc ()),"Unexpected id \""^$2^"\" in name_sect (should be \"name\")"));
-      Name_sect_aux(Name_sect_some($4), loc ()) }
-
-c_def_body:
-  | typ id
-    { [($1,$2)],false }
-  | typ id Semi
-    { [($1,$2)],true }
-  | typ id Semi c_def_body
-    { ($1,$2)::(fst $4), snd $4 }
-
-union_body:
-  | id
-    { [Tu_aux( Tu_id $1, loc())],false }
-  | typ id
-    { [Tu_aux( Tu_ty_id ($1,$2), loc())],false }
-  | id Semi
-    { [Tu_aux( Tu_id $1, loc())],true }
-  | 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 }
-  | 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)) }
-  | Num DotDot Num
-    { irloc (BF_range($1,$3)) }
-  | Lparen index_range Rparen
+let_def:
+  | Let_ letbind
     { $2 }
 
-enum_body:
-  | id
-  { [$1] }
-  | id Semi
-  { [$1] }
-  | id Semi enum_body
-  { $1::$3 }
-
-index_range:
-  | index_range_atomic
-    { $1 }
-  | index_range_atomic Comma index_range
-    { irloc(BF_concat($1,$3)) }
-
-r_id_def:
-  | index_range Colon id
-    { $1,$3 }
+val_spec_def:
+  | Val decl typschm
+    { mk_vs (VS_val_spec ($3, $2)) $startpos $endpos }
+  | Val id Colon typschm
+    { mk_vs (VS_val_spec ($4, $2)) $startpos $endpos }
 
-r_def_body:
-  | r_id_def
-    { [$1] }
-  | r_id_def Semi
-    { [$1] }
-  | r_id_def Semi r_def_body
-    { $1::$3 }
-
-type_def:
-  | Typedef tid name_sect Eq typquant typ
-    { tdloc (TD_abbrev($2,$3,mk_typschm $5 $6 5 6)) }
-  | Typedef tid name_sect Eq typ
-    { tdloc (TD_abbrev($2,$3,mk_typschm (mk_typqn ()) $5 5 5)) }
-  | Typedef tid Eq typquant typ
-    { tdloc (TD_abbrev($2,mk_namesectn (), mk_typschm $4 $5 4 5))}
-  | Typedef tid Eq typ
-    { tdloc (TD_abbrev($2,mk_namesectn (),mk_typschm (mk_typqn ()) $4 4 4)) }
-  /* The below adds 4 shift/reduce conflicts. Due to c_def_body and confusions in id id and parens  */
-  | Typedef tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2,$3,$7,fst $9, snd $9)) }
-  | Typedef tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2,$3,(mk_typqn ()), fst $8, snd $8)) }
-  | Typedef tid Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
-  | Typedef tid Eq Const Struct Lcurly c_def_body Rcurly
-    { tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
-  | Typedef tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
-    { tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) }
-  | Typedef tid Eq Const Union typquant Lcurly union_body Rcurly
-    { tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) }
-  | Typedef tid name_sect Eq Const Union Lcurly union_body Rcurly
-    { tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) }
-  | Typedef tid Eq Const Union Lcurly union_body Rcurly
-    { tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
-  | Typedef tid Eq Enumerate Lcurly enum_body Rcurly
-    { tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
-  | Typedef tid name_sect Eq Enumerate Lcurly enum_body Rcurly
-    { tdloc (TD_enum($2,$3,$7,false)) }
-  | Typedef tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
-    { tdloc (TD_register($2, $7, $9, $12)) }
-
-default_typ:
-  | Default atomic_kind tyvar
-    { defloc (DT_kind($2,$3)) }
-  | Default atomic_kind Inc
-    { defloc (DT_order($2, tloc (ATyp_inc))) }
-  | Default atomic_kind Dec
-    { defloc (DT_order($2, tloc (ATyp_dec))) }
-  | Default typquant typ id
-    { defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) }
-  | Default typ id
-    { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) }
-
-scattered_def:
-  | Function_ Rec typquant typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $6 6, $7)) }
-  | Function_ Rec typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $5 5, $6)) }
-  | Function_ Rec typquant typ id
-    { sdloc (SD_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) }
-  | Function_ Rec Effect effect_typ id
-    { sdloc (SD_scattered_function (mk_rec 2, mk_tannotn (), mk_eannot $4 4, $5)) }
-  | Function_ Rec typ id
-    { sdloc (SD_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) }
-  | Function_ Rec id
-    { sdloc (SD_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) }
-  | Function_ typquant typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $5 5, $6)) }
-  | Function_ typ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $4 4, $5)) }
-  | Function_ typquant typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) }
-  | Function_ Effect effect_typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $3 3, $4)) }
-  | Function_ typ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannotn (), $3)) }
-  | Function_ id
-    { sdloc (SD_scattered_function(mk_recn (), mk_tannotn (), mk_eannotn (), $2)) }
-  | Typedef tid name_sect Eq Const Union typquant
-    { sdloc (SD_scattered_variant($2,$3,$7)) }
-  | Typedef tid Eq Const Union typquant
-    { sdloc (SD_scattered_variant($2,(mk_namesectn ()),$6)) }
-  | Typedef tid name_sect Eq Const Union
-    { sdloc (SD_scattered_variant($2,$3,mk_typqn ())) }
-  | Typedef tid Eq Const Union
-    { sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
-
-ktype_def:
-  | Def kind tid name_sect Eq typquant typ
-    { kdloc (KD_abbrev($2,$3,$4,mk_typschm $6 $7 6 7)) }
-  | Def kind tid name_sect Eq typ
-    { kdloc (KD_abbrev($2,$3,$4,mk_typschm (mk_typqn ()) $6 6 6)) }
-  | Def kind tid Eq typquant typ
-    { kdloc (KD_abbrev($2,$3,mk_namesectn (), mk_typschm $5 $6 5 6)) }
-  | Def kind tid Eq typ
-    { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) $5 5 5)) }
-  | Def kind tid Eq Num
-    { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) (tlocl (ATyp_constant $5) 5 5) 5 5)) }
-  | Def kind tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,$4,$8,fst $10, snd $10)) }
-  | Def kind tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,$4,(mk_typqn ()), fst $9, snd $9)) }
-  | Def kind tid Eq Const Struct typquant Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
-  | Def kind tid Eq Const Struct Lcurly c_def_body Rcurly
-    { kdloc (KD_record($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
-  | Def kind tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3,$4, $8, fst $10, snd $10)) }
-  | Def kind tid Eq Const Union typquant Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
-  | Def kind tid name_sect Eq Const Union Lcurly union_body Rcurly
-    { kdloc (KD_variant($2, $3,$4, mk_typqn (), fst $9, snd $9)) }
-  | Def kind tid Eq Const Union Lcurly union_body Rcurly
-    { kdloc (KD_variant($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
-  | Def kind tid Eq Enumerate Lcurly enum_body Rcurly
-    { kdloc (KD_enum($2,$3, mk_namesectn (), $7,false)) }
-  | Def kind tid name_sect Eq Enumerate Lcurly enum_body Rcurly
-    { kdloc (KD_enum($2,$3,$4,$8,false)) }
-  | Def kind tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
-    { kdloc (KD_register($2,$3, $8, $10, $13)) }
-
-    
 def:
-  | type_def
-      { dloc (DEF_type($1)) }
-  | ktype_def
-      { dloc (DEF_kind($1)) }
   | fun_def
-    { dloc (DEF_fundef($1)) }
-  | letbind
-    { dloc (DEF_val($1)) }
-  | val_spec
-    { dloc (DEF_spec($1)) }
-  | default_typ
-    { dloc (DEF_default($1)) }
-  | Overload id Lsquare enum_body Rsquare
-    { dloc (DEF_overload($2,$4)) }
-  | Register typ id
-    { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
-  | Register Alias id Eq exp
-    { dloc (DEF_reg_dec(DEC_aux(DEC_alias($3,$5),loc ()))) }
-  | Register Alias typ id Eq exp
-    { dloc (DEF_reg_dec(DEC_aux(DEC_typ_alias($3,$4,$6), loc ()))) }
-  | Scattered scattered_def
-    { dloc (DEF_scattered $2) }
-  | Function_ Clause funcl
-    { dloc (DEF_scattered (sdloc (SD_scattered_funcl($3)))) }
-  | Union tid Member typ id
-    { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_ty_id($4,$5), locn 4 5))))) }
-  | Union tid Member id
-    { dloc (DEF_scattered (sdloc (SD_scattered_unioncl($2,Tu_aux(Tu_id($4), locn 4 4))))) }
-  | End id
-    { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
-  | End tid
-    { dloc (DEF_scattered (sdloc (SD_scattered_end($2)))) }
-
-defs_help:
+    { DEF_fundef $1 }
+  | val_spec_def
+    { DEF_spec $1 }
+  | type_def
+    { DEF_type $1 }
+  | let_def
+    { DEF_val $1 }
+
+defs_list:
   | def
     { [$1] }
-  | def defs_help
+  | def defs_list
     { $1::$2 }
 
 defs:
-  | defs_help
+  | defs_list
     { (Defs $1) }
 
 file:
   | defs Eof
     { $1 }
 
-nonempty_exp_list:
-  | semi_exps_help Eof { $1 }
-
diff --git a/src/process_file.mli b/src/process_file.mli
index 1cf710bc..7972c689 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -72,3 +72,4 @@ val output :
     files existed before. If it is set to [false] and an output file already exists,
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
+