Improvements to menhir pretty printer and ocaml backend

Menhir pretty printer can now print enough sail to be useful with ASL parser

Fixity declarations are now preserved in the AST

Menhir parser now runs without the Pre-lexer

Ocaml backend now supports variant typedefs, as the machinery to
generate arbitrary instances of variant types has been added to the
-undefined_gen flag

11 files changed, 184 insertions, 70 deletions

diff --git a/src/ast.ml b/src/ast.ml
index 76c926bb..6f702a78 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -553,6 +553,7 @@ type
 'a dec_spec =
    DEC_aux of 'a dec_spec_aux * 'a annot
 
+type prec = Infix | InfixL | InfixR
 
 type
 'a dec_comm =  (* Top-level generated comments *)
@@ -565,6 +566,7 @@ and 'a def =  (* Top-level 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_fixity of prec * int * id (* fixity declaration *)
  | DEF_overload of id * id list (* operator overload specification *)
  | DEF_default of 'a default_spec (* default kind and type assumptions *)
  | DEF_scattered of 'a scattered_def (* scattered function and type definition *)
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 36b6478e..6a7a1b0a 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -765,12 +765,19 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
       | Parse_ast.DEC_typ_alias(typ,id,e) ->
 	DEC_typ_alias(to_ast_typ k_env def_ord typ,to_ast_id id,to_ast_alias_spec k_env def_ord e)
     ),(l,()))
-      
+
+let to_ast_prec = function
+  | Parse_ast.Infix -> Infix
+  | Parse_ast.InfixL -> InfixL
+  | Parse_ast.InfixR -> InfixR
+
 let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list = 
   let envs = (names,k_env,def_ord) in
   match def with
   | Parse_ast.DEF_overload(id,ids) ->
-    ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs
+     ((Finished(DEF_overload(to_ast_id id, List.map to_ast_id ids))),envs),partial_defs
+  | Parse_ast.DEF_fixity (prec, n, op) ->
+     ((Finished(DEF_fixity (to_ast_prec prec, n, to_ast_id op)),envs),partial_defs)
   | Parse_ast.DEF_kind(k_def) ->
     let kd,envs = to_ast_kdef envs k_def in
     ((Finished(DEF_kind(kd))),envs),partial_defs
@@ -913,7 +920,7 @@ let typschm_of_string order str =
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
-let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some str, false))
+let val_spec_of_string order id str = mk_val_spec (VS_val_spec (typschm_of_string order str, id, Some (string_of_id id), false))
 
 let val_spec_ids (Defs defs) =
   let val_spec_id (VS_aux (vs_aux, _)) =
@@ -965,6 +972,10 @@ let generate_undefineds vs_ids (Defs defs) =
      gen_vs (mk_id "undefined_vector") "forall 'n 'm ('a:Type). (atom('n), atom('m), 'a) -> vector('n, 'm, dec,'a) effect {undef}";
      gen_vs (mk_id "undefined_unit") "unit -> unit effect {undef}"]
   in
+  let undefined_tu = function
+    | Tu_aux (Tu_id id, _) -> mk_exp (E_id id)
+    | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
+  in
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
@@ -980,11 +991,12 @@ let generate_undefineds vs_ids (Defs defs) =
                             pat
                             (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
     | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
+       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, None, false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
-                            (mk_pat (P_lit (mk_lit L_unit)))
+                            pat
                             (mk_exp (E_app (mk_id "internal_pick",
-                                            [])))]]
+                                            [mk_exp (E_list (List.map undefined_tu tus))])))]]
     | _ -> []
   in
   let rec undefined_defs = function
diff --git a/src/lexer2.mll b/src/lexer2.mll
index 1ab5b98b..5b711287 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -42,6 +42,7 @@
 
 {
 open Parser2
+open Parse_ast
 module M = Map.Make(String)
 exception LexError of string * Lexing.position
 
@@ -49,8 +50,6 @@ 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)
 
-type prec = Infix | InfixL | InfixR
-
 let mk_operator prec n op =
   match prec, n with
   | Infix, 0 -> Op0 op
@@ -102,13 +101,14 @@ let kw_table =
      ("clause",                  (fun _ -> Clause));
      ("dec",                     (fun _ -> Dec));
      ("def",                     (fun _ -> Def));
-     ("op",                      (fun _ -> Op));
+     ("operator",                (fun _ -> Op));
      ("default",		 (fun _ -> Default));
      ("effect",                  (fun _ -> Effect));
      ("Effect",                  (fun _ -> EFFECT));
      ("end",                     (fun _ -> End));
      ("enum",		         (fun _ -> Enum));
      ("else",                    (fun _ -> Else));
+     ("exit",                    (fun _ -> Exit));
      ("extern",                  (fun _ -> Extern));
      ("cast",                    (fun _ -> Cast));
      ("false",                   (fun _ -> False));
@@ -172,8 +172,8 @@ let alphanum = letter|digit
 let startident = letter|'_'
 let ident = alphanum|['_''\'']
 let tyvar_start = '\''
-let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
-let operator = oper_char+ ('_' ident)?
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|']
+let operator = (oper_char+ ('_' ident)?)
 let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
 
 rule token = parse
@@ -190,6 +190,9 @@ rule token = parse
   | ","                                 { Comma }
   | ".."                                { DotDot }
   | "."                                 { Dot }
+  | "==" as op
+    { try M.find op !operators
+      with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, Lexing.lexeme_start_p lexbuf)) }
   | "="                                 { (Eq(r"=")) }
   | ">"					{ (Gt(r">")) }
   | "-"					{ Minus }
@@ -215,19 +218,20 @@ rule token = parse
   | "<="				{ (LtEq(r"<=")) }
   | "infix" ws (digit as p) ws (operator as op)
     { operators := M.add op (mk_operator Infix (int_of_string (Char.escaped p)) op) !operators;
-      token lexbuf }
+      Fixity (Infix, int_of_string (Char.escaped p), op) }
   | "infixl" ws (digit as p) ws (operator as op)
     { operators := M.add op (mk_operator InfixL (int_of_string (Char.escaped p)) op) !operators;
-      token lexbuf }
+      Fixity (InfixL, int_of_string (Char.escaped p), op) }
   | "infixr" ws (digit as p) ws (operator as op)
     { operators := M.add op (mk_operator InfixR (int_of_string (Char.escaped p)) op) !operators;
-      token lexbuf }
+      Fixity (InfixR, int_of_string (Char.escaped p), op) }
   | operator as op
     { try M.find op !operators
-      with Not_found -> raise (LexError ("Operator fixity undeclared", Lexing.lexeme_start_p lexbuf)) }
+      with Not_found -> raise (LexError ("Operator fixity undeclared " ^ op, 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  { TyVar(r i) }
+  | "~"                                 { Id(r"~") }
   | startident ident* as i              { if M.mem i kw_table then
                                             (M.find i kw_table) ()
 					  (* else if
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 38b3cc9d..dc8c056e 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -107,8 +107,13 @@ let begin_end doc = group (string "begin" ^^ nest 2 (break 1 ^^ doc) ^/^ string
 
 let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   match exp_aux with
+  | E_app (f, [x]) when Env.is_union_constructor f (env_of exp) -> zencode_upper ctx f ^^ space ^^ ocaml_atomic_exp ctx x
   | E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
-  | E_app (f, xs) -> zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+  | E_app (f, xs) when Env.is_union_constructor f (env_of exp) ->
+     zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+  | E_app (f, xs) ->
+     zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+  | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) [exp1; exp2; exp3])
   | E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
   | E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
   | E_cast (_, exp) -> ocaml_exp ctx exp
@@ -176,9 +181,8 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
      begin
        match Env.lookup_id id (env_of exp) with
        | Local (Immutable, _) | Unbound -> zencode ctx id
-       | Enum _ -> zencode_upper ctx id
+       | Enum _ | Union _ -> zencode_upper ctx id
        | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
-       | _ -> failwith ("Union constructor: " ^ zencode_string (string_of_id id))
      end
   | E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
   | E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
@@ -255,8 +259,8 @@ let rec ocaml_fields ctx =
 
 let rec ocaml_cases ctx =
   let ocaml_case = function
-    | Tu_aux (Tu_id id, _) -> separate space [bar; zencode ctx id]
-    | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode ctx id; string "of"; ocaml_typ ctx typ]
+    | Tu_aux (Tu_id id, _) -> separate space [bar; zencode_upper ctx id]
+    | Tu_aux (Tu_ty_id (typ, id), _) -> separate space [bar; zencode_upper ctx id; string "of"; ocaml_typ ctx typ]
   in
   function
   | [tu] -> ocaml_case tu
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 9532b858..cfd749ba 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -481,14 +481,18 @@ type
 scattered_def = 
    SD_aux of scattered_def_aux * l
 
+type prec = Infix | InfixL | InfixR
 
-type 
+type fixity_token = (prec * int * string)
+
+type
 def =  (* Top-level definition *)
    DEF_kind of kind_def (* definition of named kind identifiers *)
  | DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
  | DEF_val of letbind (* value definition *)
  | DEF_overload of id * id list (* operator overload specifications *)
+ | DEF_fixity of prec * int * id (* fixity declaration *)
  | DEF_spec of val_spec (* top-level type constraint *)
  | DEF_default of default_typing_spec (* default kind and type assumptions *)
  | DEF_scattered of scattered_def (* scattered definition *)
diff --git a/src/parser2.mly b/src/parser2.mly
index 59db84a1..a2fb3bfb 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -127,7 +127,7 @@ let rec desugar_rchain chain s e =
 %token And As Assert Bitzero Bitone Bits By Match Clause Dec Def Default Effect EFFECT End Op
 %token Enum Else Extern False Forall Exist Foreach Overload Function_ If_ In IN Inc Let_ Member Int Order Cast
 %token Pure Rec Register Return Scattered Sizeof Struct Then True TwoCaret Type TYPE Typedef
-%token Undefined Union With Val Constraint Throw Try Catch
+%token Undefined Union With Val Constraint Throw Try Catch Exit
 %token Barr Depend Rreg Wreg Rmem Rmemt Wmem Wmv Wmvt Eamem Exmem Undef Unspec Nondet Escape
 
 %nonassoc Then
@@ -152,6 +152,8 @@ let rec desugar_rchain chain s e =
 %token <string> Op0l Op1l Op2l Op3l Op4l Op5l Op6l Op7l Op8l Op9l
 %token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
+%token <Parse_ast.fixity_token> Fixity
+
 %start file
 %start typschm_eof
 %type <Parse_ast.typschm> typschm_eof
@@ -198,6 +200,14 @@ id:
   | Op Plus { mk_id (DeIid "+") $startpos $endpos }
   | Op Minus { mk_id (DeIid "-") $startpos $endpos }
   | Op Star { mk_id (DeIid "*") $startpos $endpos }
+  | Op ExclEq { mk_id (DeIid "!=") $startpos $endpos }
+  | Op Lt { mk_id (DeIid "<") $startpos $endpos }
+  | Op Gt { mk_id (DeIid ">") $startpos $endpos }
+  | Op LtEq { mk_id (DeIid "<=") $startpos $endpos }
+  | Op GtEq { mk_id (DeIid ">=") $startpos $endpos }
+  | Op Amp { mk_id (DeIid "&") $startpos $endpos }
+  | Op Bar { mk_id (DeIid "|") $startpos $endpos }
+  | Op Caret { mk_id (DeIid "^") $startpos $endpos }
 
 op0: Op0 { mk_id (Id $1) $startpos $endpos }
 op1: Op1 { mk_id (Id $1) $startpos $endpos }
@@ -585,12 +595,24 @@ typschm_eof:
   | typschm Eof
     { $1 }
 
-pat:
+pat1:
   | atomic_pat
     { $1 }
-  | atomic_pat As id
+  | atomic_pat At pat_concat
+    { mk_pat (P_vector_concat ($1 :: $3)) $startpos $endpos }
+
+pat_concat:
+  | atomic_pat
+    { [$1] }
+  | atomic_pat At pat_concat
+    { $1 :: $3 }
+
+pat:
+  | pat1
+    { $1 }
+  | pat1 As id
     { mk_pat (P_as ($1, $3)) $startpos $endpos }
-  | atomic_pat As kid
+  | pat1 As kid
     { mk_pat (P_var ($1, $3)) $startpos $endpos }
 
 pat_list:
@@ -610,12 +632,14 @@ atomic_pat:
     { mk_pat (P_var (mk_pat (P_id (id_of_kid $1)) $startpos $endpos, $1)) $startpos $endpos }
   | id Lparen pat_list Rparen
     { mk_pat (P_app ($1, $3)) $startpos $endpos }
-  | pat Colon typ
+  | atomic_pat Colon typ
     { mk_pat (P_typ ($3, $1)) $startpos $endpos }
   | Lparen pat Rparen
     { $2 }
   | Lparen pat Comma pat_list Rparen
     { mk_pat (P_tup ($2 :: $4)) $startpos $endpos }
+  | Lsquare pat_list Rsquare
+    { mk_pat (P_vector $2) $startpos $endpos }
 
 lit:
   | True
@@ -695,6 +719,7 @@ exp2:
   | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp2l op2l exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp3 { $1 }
 exp2l:
   | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -703,12 +728,14 @@ exp2l:
 exp2r:
   | exp3 op2 exp3 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp3 op2r exp2r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp3 Bar exp2r { mk_exp (E_app_infix ($1, mk_id (Id "|") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp3 { $1 }
 
 exp3:
   | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp3l op3l exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4 { $1 }
 exp3l:
   | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
@@ -717,10 +744,16 @@ exp3l:
 exp3r:
   | exp4 op3 exp4 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp4 op3r exp3r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp4 Amp exp3r { mk_exp (E_app_infix ($1, mk_id (Id "&") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4 { $1 }
 
 exp4:
   | exp5 op4 exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
+  | exp5 Lt exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 Gt exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 LtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "<=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 GtEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id ">=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
+  | exp5 ExclEq exp5 { mk_exp (E_app_infix ($1, mk_id (Id "!=") $startpos($2) $endpos($2), $3)) $startpos $endpos }
   | exp4l op4l exp5 { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 op4r exp4r { mk_exp (E_app_infix ($1, $2, $3)) $startpos $endpos }
   | exp5 { $1 }
@@ -845,6 +878,8 @@ atomic_exp:
     { mk_exp (E_cast ($3, $1)) $startpos $endpos }
   | lit
     { mk_exp (E_lit $1) $startpos $endpos }
+  | atomic_exp Dot id
+    { mk_exp (E_field ($1, $3)) $startpos $endpos }
   | id
     { mk_exp (E_id $1) $startpos $endpos }
   | kid
@@ -853,6 +888,8 @@ atomic_exp:
     { 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 }
+  | Exit Lparen exp Rparen
+    { mk_exp (E_exit $3) $startpos $endpos }
   | Sizeof Lparen typ Rparen
     { mk_exp (E_sizeof $3) $startpos $endpos }
   | Constraint Lparen nc Rparen
@@ -886,11 +923,19 @@ funcl:
   | id pat Eq exp
     { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos }
 
+funcls:
+  | id pat Eq exp
+    { [mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos] }
+  | id pat Eq exp And funcls
+    { mk_funcl (FCL_Funcl ($1, $2, $4)) $startpos $endpos :: $6 }
+
 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 Eq Lcurly struct_fields Rcurly
+    { mk_td (TD_record ($2, mk_namesectn, TypQ_aux (TypQ_tq [], loc $endpos($2) $startpos($3)), $5, false)) $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
@@ -939,8 +984,8 @@ type_unions:
     { $1 :: $3 }
 
 fun_def:
-  | Function_ funcl
-    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, [$2])) $startpos $endpos }
+  | Function_ funcls
+    { mk_fun (FD_function (mk_recn, mk_tannotn, mk_eannotn, $2)) $startpos $endpos }
 
 let_def:
   | Let_ letbind
@@ -977,6 +1022,8 @@ scattered_def:
 def:
   | fun_def
     { DEF_fundef $1 }
+  | Fixity
+    { let (prec, n, op) = $1 in DEF_fixity (prec, n, Id_aux (Id op, loc $startpos $endpos)) }
   | val_spec_def
     { DEF_spec $1 }
   | type_def
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 99263bc7..0f8e482a 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -526,6 +526,7 @@ let rec doc_def def = group (match def with
       string "overload" ^^ space ^^ doc_id id ^^ space ^^ brackets ids_doc
   | DEF_comm (DC_comm s) -> comment (string s)
   | DEF_comm (DC_comm_struct d) -> comment (doc_def d)
+  | DEF_fixity _ -> empty
   ) ^^ hardline
 
 let doc_defs (Defs(defs)) =
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index bb7aa3b4..23452813 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -8,7 +8,7 @@ let doc_op symb a b = infix 2 1 symb a b
 let doc_id (Id_aux (id_aux, _)) =
   string (match id_aux with
           | Id v -> v
-          | DeIid op -> "op " ^ op)
+          | DeIid op -> "operator " ^ op)
 
 let doc_kid kid = string (Ast_util.string_of_kid kid)
 
@@ -76,6 +76,8 @@ let rec doc_typ (Typ_aux (typ_aux, _)) =
   | Typ_app (id, []) -> doc_id id
   | Typ_app (Id_aux (DeIid str, _), [x; y]) ->
      separate space [doc_typ_arg x; doc_typ_arg y]
+  | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0->
+     string "bits" ^^ parens (doc_typ_arg len)
   | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
@@ -144,7 +146,7 @@ let doc_lit (L_aux(l,_)) =
   | L_undef -> "undefined"
   | L_string s -> "\"" ^ String.escaped s ^ "\"")
 
-let rec doc_pat (P_aux (p_aux, _)) =
+let rec doc_pat (P_aux (p_aux, _) as pat) =
   match p_aux with
   | P_id id -> doc_id id
   | P_tup pats -> lparen ^^ separate_map (comma ^^ space) doc_pat pats ^^ rparen
@@ -155,63 +157,85 @@ let rec doc_pat (P_aux (p_aux, _)) =
   | P_var (P_aux (P_id id, _), kid) when Id.compare (id_of_kid kid) id == 0 ->
      doc_kid kid
   | P_var (pat, kid) -> separate space [doc_pat pat; string "as"; doc_kid kid]
+  | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats)
   | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats
   | P_wild -> string "_"
-  | _ -> string "PAT"
+  | P_as (pat, id) -> separate space [doc_pat pat; string "as"; doc_id id]
+  | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats)
+  | _ -> string (string_of_pat pat)
 
 let rec doc_exp (E_aux (e_aux, _) as exp) =
- match e_aux with
+  match e_aux with
+  | E_block [exp] -> doc_exp exp
   | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace
   | E_nondet exps -> assert false
-  | E_id id -> doc_id id
-  | E_lit lit -> doc_lit lit
-  | E_cast (typ, exp) ->
-     separate space [doc_exp exp; colon; doc_typ typ]
-  (* Format a function with a unit argument as f() rather than f(()) *)
-  | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
-  | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
-  | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_exp x) (doc_exp y)
+  (* This is mostly for the -convert option *)
+  | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
+     separate space [doc_atomic_exp x; string "/"; doc_atomic_exp y]
+  | E_app_infix (x, id, y) -> doc_op (doc_id id) (doc_atomic_exp x) (doc_atomic_exp y)
   | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps)
-  | E_if (if_exp, then_exp, else_exp) -> string "E_if"
+  | E_if (if_exp, then_exp, else_exp) ->
+     group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp])
   | E_for (id, exp1, exp2, exp3, order, exp4) -> string "E_for"
-  | E_vector exps -> string "E_vector"
-  | E_vector_access (exp1, exp2) -> string "E_vector_access"
-  | E_vector_subrange (exp1, exp2, exp3) -> doc_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3])
-  | E_vector_update (exp1, exp2, exp3) -> string "E_vector_update"
-  | E_vector_update_subrange (exp1, exp2, exp3, exp4) -> string "E_vector_update_subrange"
   | E_list exps -> string "E_list"
   | E_cons (exp1, exp2) -> string "E_cons"
   | E_record fexps -> string "E_record"
   | E_record_update (exp, fexps) -> string "E_record_update"
-  | E_field (exp, id) -> string "E_field"
   | E_case (exp, pexps) ->
      separate space [string "match"; doc_exp exp; doc_pexps pexps]
   | E_let (LB_aux (LB_val (pat, binding), _), exp) ->
      separate space [string "let"; doc_pat pat; equals; doc_exp binding; string "in"; doc_exp exp]
   | E_assign (lexp, exp) ->
      separate space [doc_lexp lexp; equals; doc_exp exp]
+  (* Resugar an assert with an empty message *)
+  | E_throw exp -> assert false
+  | E_try (exp, pexps) -> assert false
+  | E_return exp -> string "return" ^^ parens (doc_exp exp)
+  | _ -> doc_atomic_exp exp
+and doc_atomic_exp (E_aux (e_aux, _) as exp) =
+  match e_aux with
+  | E_cast (typ, exp) ->
+     separate space [doc_atomic_exp exp; colon; doc_typ typ]
+  | E_lit lit -> doc_lit lit
+  | E_id id -> doc_id id
+  | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id
   | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid
   | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp)
+  (* Format a function with a unit argument as f() rather than f(()) *)
+  | E_app (id, [E_aux (E_lit (L_aux (L_unit, _)), _)]) -> doc_id id ^^ string "()"
+  | E_app (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
   | E_constraint nc -> string "constraint" ^^ parens (doc_nc nc)
-  | E_exit exp -> assert false
-  (* Resugar an assert with an empty message *)
   | E_assert (exp1, E_aux (E_lit (L_aux (L_string "", _)), _)) -> string "assert" ^^ parens (doc_exp exp1)
   | E_assert (exp1, exp2) -> string "assert" ^^ parens (doc_exp exp1 ^^ comma ^^ space ^^ doc_exp exp2)
-  | E_throw exp -> assert false
-  | E_try (exp, pexps) -> assert false
-  | E_return exp -> string "return" ^^ parens (doc_exp exp)
+  | E_exit exp -> string "exit" ^^ parens (doc_exp exp)
+  | E_vector_access (exp1, exp2) -> doc_atomic_exp exp1 ^^ brackets (doc_exp exp2)
+  | E_vector_subrange (exp1, exp2, exp3) -> doc_atomic_exp exp1 ^^ brackets (separate space [doc_exp exp2; string ".."; doc_exp exp3])
+  | E_vector exps -> brackets (separate_map (comma ^^ space) doc_exp exps)
+  | E_vector_update (exp1, exp2, exp3) ->
+     brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; equals; doc_exp exp3])
+  | E_vector_update_subrange (exp1, exp2, exp3, exp4) ->
+     brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
+  | _ -> parens (doc_exp exp)
 and doc_block = function
   | [] -> assert false
   | [E_aux (E_let (LB_aux (LB_val (pat, binding), _), E_aux (E_block exps, _)), _)] ->
      separate space [string "let"; doc_pat pat; equals; doc_exp binding] ^^ semi ^^ hardline ^^ doc_block exps
   | [exp] -> doc_exp exp
   | exp :: exps -> doc_exp exp ^^ semi ^^ hardline ^^ doc_block exps
-and doc_lexp (LEXP_aux (l_aux, _)) =
+and doc_lexp (LEXP_aux (l_aux, _) as lexp) =
+  match l_aux with
+  | LEXP_cast (typ, id) -> separate space [doc_id id; colon; doc_typ typ]
+  | _ -> doc_atomic_lexp lexp
+and doc_atomic_lexp (LEXP_aux (l_aux, _) as lexp) =
   match l_aux with
   | LEXP_id id -> doc_id id
   | LEXP_tup lexps -> lparen ^^ separate_map (comma ^^ space) doc_lexp lexps ^^ rparen
-  | _ -> string "LEXP"
-and doc_pexps pexps = surround 2 0 lbrace (separate_map (semi ^^ hardline) doc_pexp pexps) rbrace
+  | LEXP_field (lexp, id) -> doc_atomic_lexp lexp ^^ dot ^^ doc_id id
+  | LEXP_vector (lexp, exp) -> doc_atomic_lexp lexp ^^ brackets (doc_exp exp)
+  | LEXP_vector_range (lexp, exp1, exp2) -> doc_atomic_lexp lexp ^^ brackets (separate space [doc_exp exp1; string ".."; doc_exp exp2])
+  | LEXP_memory (id, exps) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_exp exps)
+  | _ -> parens (doc_lexp lexp)
+and doc_pexps pexps = surround 2 0 lbrace (separate_map (comma ^^ hardline) doc_pexp pexps) rbrace
 and doc_pexp (Pat_aux (pat_aux, _)) =
   match pat_aux with
   | Pat_exp (pat, exp) -> separate space [doc_pat pat; string "=>"; doc_exp exp]
@@ -246,8 +270,11 @@ let doc_dec (DEC_aux (reg,_)) =
   | DEC_alias(id,alspec) -> string "ALIAS"
   | DEC_typ_alias(typ,id,alspec) -> string "ALIAS"
 
+let doc_field (typ, id) =
+  separate space [doc_id id; colon; doc_typ typ]
+
 let doc_typdef (TD_aux(td,_)) = match td with
-  | TD_abbrev(id, _, typschm) ->
+  | TD_abbrev (id, _, typschm) ->
      begin
        match doc_typschm_quants typschm with
        | Some qdoc ->
@@ -255,6 +282,13 @@ let doc_typdef (TD_aux(td,_)) = match td with
        | None ->
           doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
      end
+  | TD_enum (id, _, ids, _) ->
+     separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
+  | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) ->
+     separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
+  | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) ->
+     separate space [string "struct"; doc_id id; doc_quants qs; equals;
+                     surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
   | _ -> string "TYPEDEF"
 
 let doc_spec (VS_aux(v,_)) =
@@ -289,7 +323,7 @@ let rec doc_def def = group (match def with
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> string "TOPLEVEL"
   | DEF_overload (id, ids) ->
-      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (semi ^^ break 1) doc_id ids) rbrace]
+      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
   | DEF_comm (DC_comm s) -> string "TOPLEVEL"
   | DEF_comm (DC_comm_struct d) -> string "TOPLEVEL"
   ) ^^ hardline
diff --git a/src/process_file.ml b/src/process_file.ml
index 1749bc03..f176f198 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -59,20 +59,25 @@ let get_lexbuf f =
   lexbuf, in_chan
 
 let parse_file (f : string) : Parse_ast.defs =
-  let scanbuf, in_chan = get_lexbuf f in
-  let type_names =
-    try
-      Pre_parser.file Pre_lexer.token scanbuf
-    with
+  if not !opt_new_parser
+  then
+    let scanbuf, in_chan = get_lexbuf f in
+    let type_names =
+      try
+        Pre_parser.file Pre_lexer.token scanbuf
+      with
       | Parsing.Parse_error ->
-          let pos = Lexing.lexeme_start_p scanbuf in
-           raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre")))
+         let pos = Lexing.lexeme_start_p scanbuf in
+         raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre")))
       | Parse_ast.Parse_error_locn(l,m) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
+         raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m)))
       | Lexer.LexError(s,p) ->
-          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in
-  let () = Lexer.custom_type_names := !Lexer.custom_type_names @ type_names in
-  close_in in_chan;
+         raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
+    in
+    close_in in_chan;
+    Lexer.custom_type_names := !Lexer.custom_type_names @ type_names
+  else ();
+
   let lexbuf, in_chan = get_lexbuf f in
     try
       let ast =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 1c02b161..82ebaec5 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -561,7 +561,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
   in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
 
 let rewrite_def rewriters d = match d with
-  | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ -> d
+  | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ | DEF_overload _ | DEF_fixity _ -> d
   | DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
   | DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters letbind)
   | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
diff --git a/src/type_check.ml b/src/type_check.ml
index 06083211..7f204fca 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1959,7 +1959,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           let tpat, env = bind_pat env pat (typ_of inferred_bind) in
           annot_exp (E_let (LB_aux (LB_val (tpat, inferred_bind), (let_loc, None)), crule check_exp env exp typ)) typ
      end
-  | E_app_infix (x, op, y), _ when List.length (Env.get_overloads (deinfix op) env) > 0 ->
+  | E_app_infix (x, op, y), _ ->
      check_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ()))) typ
   | E_app (f, [E_aux (E_constraint nc, _)]), _ when Id.compare f (mk_id "_prove") = 0 ->
      if prove env nc
@@ -2592,7 +2592,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
   | E_cast (typ, exp) ->
      let checked_exp = crule check_exp env exp typ in
      annot_exp (E_cast (typ, checked_exp)) typ
-  | E_app_infix (x, op, y) when List.length (Env.get_overloads (deinfix op) env) > 0 -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ())))
+  | E_app_infix (x, op, y) -> infer_exp env (E_aux (E_app (deinfix op, [x; y]), (l, ())))
   | E_app (f, xs) when List.length (Env.get_overloads f env) > 0 ->
      let rec try_overload = function
        | (errs, []) -> typ_raise l (Err_no_overloading (f, errs))
@@ -3275,6 +3275,7 @@ let rec check_def env def =
   match def with
   | DEF_kind kdef -> check_kinddef env kdef
   | DEF_type tdef -> check_typedef env tdef
+  | DEF_fixity (prec, n, op) -> [DEF_fixity (prec, n, op)], env
   | DEF_fundef fdef -> check_fundef env fdef
   | DEF_val letdef -> check_letdef env letdef
   | DEF_spec vs -> check_val_spec env vs