Merge branch 'experiments' into mono-experiments

17 files changed, 277 insertions, 154 deletions

diff --git a/src/Makefile b/src/Makefile
index 6cfcf874..1bac0b71 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -177,7 +177,7 @@ _build/cheri_embed_types_sequential.lem: $(CHERI_SAILS) ./sail.native
 
 _build/Cheri_embed_sequential.thy: _build/cheri_embed_types_sequential.lem
 	cd _build ;\
-	lem -isa -outdir . ../lem_interp/sail_impl_base.lem ../gen_lib/state.lem $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
+	lem -isa -outdir . -lib ../lem_interp -lib ../gen_lib $(MIPS_SAIL_DIR)/mips_extras_embed_sequential.lem cheri_embed_types_sequential.lem cheri_embed_sequential.lem
 
 _build/mips_all.sail: $(MIPS_SAILS)
 	cat $(MIPS_SAILS) > $@
diff --git a/src/ast_util.ml b/src/ast_util.ml
index aef1a05d..2f630021 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -618,6 +618,22 @@ let rec simplify_nexp (Nexp_aux (nexp, l)) =
   | Nexp_exp of nexp (* exponential *)
   | Nexp_neg of nexp (* For internal use *) *)
 
+let rec lexp_to_exp (LEXP_aux (lexp_aux, annot) as le) =
+  let rewrap e_aux = E_aux (e_aux, annot) in
+  match lexp_aux with
+  | LEXP_id id | LEXP_cast (_, id) -> rewrap (E_id id)
+  | LEXP_tup les ->
+    let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
+      | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
+      | _ ->
+        raise (Reporting_basic.err_unreachable l
+          ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
+    rewrap (E_tuple (List.map get_id les))
+  | LEXP_vector (lexp, e) -> rewrap (E_vector_access (lexp_to_exp lexp, e))
+  | LEXP_vector_range (lexp, e1, e2) -> rewrap (E_vector_subrange (lexp_to_exp lexp, e1, e2))
+  | LEXP_field (lexp, id) -> rewrap (E_field (lexp_to_exp lexp, id))
+  | LEXP_memory (id, exps) -> rewrap (E_app (id, exps))
+
 let rec is_number (Typ_aux (t,_)) =
   match t with
   | Typ_app (Id_aux (Id "range", _),_)
@@ -625,6 +641,10 @@ let rec is_number (Typ_aux (t,_)) =
   | Typ_app (Id_aux (Id "atom", _),_) -> true
   | _ -> false
 
+let is_reftyp (Typ_aux (typ_aux, _)) = match typ_aux with
+  | Typ_app (id, _) -> string_of_id id = "register" || string_of_id id = "reg"
+  | _ -> false
+
 let rec is_vector_typ = function
   | Typ_aux (Typ_app (Id_aux (Id "vector",_), [_;_;_;_]), _) -> true
   | Typ_aux (Typ_app (Id_aux (Id "register",_), [Typ_arg_aux (Typ_arg_typ rtyp,_)]), _) ->
diff --git a/src/ast_util.mli b/src/ast_util.mli
index e6823ee9..246e0ebd 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -44,6 +44,8 @@
 
 open Ast
 
+val no_annot : unit annot
+
 val mk_id : string -> id
 val mk_kid : string -> kid
 val mk_ord : order_aux -> order
@@ -201,7 +203,10 @@ val nexp_identical : nexp -> nexp -> bool
 val is_nexp_constant : nexp -> bool
 val simplify_nexp : nexp -> nexp
 
+val lexp_to_exp : 'a lexp -> 'a exp
+
 val is_number : typ -> bool
+val is_reftyp : typ -> bool
 val is_vector_typ : typ -> bool
 val is_bit_typ : typ -> bool
 val is_bitvector_typ : typ -> bool
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 74faba25..1f7840d0 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -44,6 +44,8 @@ open Ast
 open Util
 open Ast_util
 
+let opt_undefined_gen = ref false
+
 module Envmap = Finite_map.Fmap_map(String)
 module Nameset' = Set.Make(String)
 module Nameset = struct
@@ -1008,7 +1010,7 @@ let initial_kind_env =
   ]
 
 let typschm_of_string order str =
-  let typschm = Parser2.typschm Lexer2.token (Lexing.from_string str) in
+  let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
@@ -1055,14 +1057,14 @@ let generate_undefineds vs_ids (Defs defs) =
     if (IdSet.mem id vs_ids) then [] else [val_spec_of_string dec_ord id str]
   in
   let undefined_builtins = List.concat
-    [gen_vs (mk_id "internal_pick") "forall 'a:Type. list('a) -> 'a effect {undef}";
+    [gen_vs (mk_id "internal_pick") "forall ('a:Type). list('a) -> 'a effect {undef}";
      gen_vs (mk_id "undefined_bool") "unit -> bool effect {undef}";
      gen_vs (mk_id "undefined_bit") "unit -> bit effect {undef}";
      gen_vs (mk_id "undefined_int") "unit -> int effect {undef}";
      gen_vs (mk_id "undefined_string") "unit -> string effect {undef}";
      gen_vs (mk_id "undefined_range") "forall 'n 'm. (atom('n), atom('m)) -> range('n,'m) effect {undef}";
      (* FIXME: How to handle inc/dec order correctly? *)
-     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_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_td = function
@@ -1079,6 +1081,12 @@ let generate_undefineds vs_ids (Defs defs) =
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             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) ->
+       [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id));
+        mk_fundef [mk_funcl (prepend_id "undefined_" id)
+                            (mk_pat (P_lit (mk_lit L_unit)))
+                            (mk_exp (E_app (mk_id "internal_pick",
+                                            [])))]]
     | _ -> []
   in
   let rec undefined_defs = function
@@ -1110,6 +1118,11 @@ let generate_initialize_registers vs_ids (Defs defs) =
 
 let process_ast order defs =
   let (ast, _, _) = to_ast Nameset.empty initial_kind_env order defs in
-  let vs_ids = val_spec_ids ast in
-  let ast = generate_undefineds vs_ids ast in
-  generate_initialize_registers vs_ids ast
+  if not !opt_undefined_gen
+  then ast
+  else
+    begin
+      let vs_ids = val_spec_ids ast in
+      let ast = generate_undefineds vs_ids ast in
+      generate_initialize_registers vs_ids ast
+    end
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 86b5ca3b..feb9cb83 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -43,6 +43,8 @@
 open Ast
 open Ast_util
 
+val opt_undefined_gen : bool ref
+
 val process_ast : order -> Parse_ast.defs -> unit defs
 
 val val_spec_ids : 'a defs -> IdSet.t
diff --git a/src/lexer2.mll b/src/lexer2.mll
index f5350ea8..a1717d62 100644
--- a/src/lexer2.mll
+++ b/src/lexer2.mll
@@ -235,8 +235,6 @@ rule token = parse
       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) ()
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 8b88a07e..2509f8ef 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -88,7 +88,13 @@ let ocaml_lit (L_aux (lit_aux, _)) =
 
 let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
   match pat_aux with
-  | P_id id -> zencode ctx id
+  | P_id id ->
+     begin
+       match Env.lookup_id id (pat_env_of pat) with
+       | Local (Immutable, _) | Unbound -> zencode ctx id
+       | Enum _ -> zencode_upper ctx id
+       | _ -> failwith "Ocaml: Cannot pattern match on mutable variable or register"
+     end
   | P_lit lit -> ocaml_lit lit
   | P_typ (_, pat) -> ocaml_pat ctx pat
   | P_tup pats -> parens (separate_map (comma ^^ space) (ocaml_pat ctx) pats)
@@ -110,7 +116,7 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   | E_block [] -> string "()"
   | E_block exps -> begin_end (ocaml_block ctx exps)
   | E_field (exp, id) -> ocaml_atomic_exp ctx exp ^^ dot ^^ zencode ctx id
-  | E_exit exp -> string "failwith" ^^ space ^^ dquotes (string (String.escaped (string_of_exp exp)))
+  | E_exit exp -> string "exit 0"
   | E_case (exp, pexps) ->
      begin_end (separate space [string "match"; ocaml_atomic_exp ctx exp; string "with"]
                 ^/^ ocaml_pexps ctx pexps)
@@ -218,12 +224,12 @@ let rec ocaml_funcl_matches ctx = function
 let ocaml_funcls ctx = function
   | [] -> failwith "Ocaml: empty function"
   | [FCL_aux (FCL_Funcl (id, pat, exp),_)] ->
-     separate space [string "let"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"]
+     separate space [string "let rec"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"]
      ^//^ ocaml_exp ctx exp
      ^^ rparen
   | funcls ->
      let id = funcls_id funcls in
-     separate space [string "let"; zencode ctx id; equals; string "function"]
+     separate space [string "let rec"; zencode ctx id; equals; string "function"]
      ^//^ ocaml_funcl_matches ctx funcls
 
 let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
@@ -311,8 +317,10 @@ let ocaml_defs (Defs defs) =
 
 let ocaml_main spec =
   concat [separate space [string "open"; string (String.capitalize spec)] ^^ ocaml_def_end;
+          separate space [string "open"; string "Elf_loader"] ^^ ocaml_def_end;
           separate space [string "let"; string "()"; equals]
           ^//^ (string "Random.self_init ();"
+                ^/^ string "load_elf ();"
                 ^/^ string "initialize_registers ();"
                 ^/^ string "zmain ()")
          ]
@@ -328,20 +336,23 @@ let ocaml_compile spec defs =
   if Sys.file_exists "_sbuild" then () else Unix.mkdir "_sbuild" 0o775;
   let cwd = Unix.getcwd () in
   Unix.chdir "_sbuild";
-  let _ = Unix.system ("cp " ^ sail_lib_dir ^ "/sail_lib.ml .") in
+  let _ = Unix.system ("cp -r " ^ sail_lib_dir ^ "/ocaml_rts/. .") in
   let out_chan = open_out (spec ^ ".ml") in
   ocaml_pp_defs out_chan defs;
   close_out out_chan;
   if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
   then
-    let out_chan = open_out "main.ml" in
-    ToChannel.pretty 1. 80 out_chan (ocaml_main spec);
-    close_out out_chan;
-    let _ = Unix.system "ocamlbuild -lib nums main.native" in
-    let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in
-    ()
+    begin
+      print_endline "Generating main";
+      let out_chan = open_out "main.ml" in
+      ToChannel.pretty 1. 80 out_chan (ocaml_main spec);
+      close_out out_chan;
+      let _ = Unix.system "ocamlbuild -pkg zarith -pkg uint main.native" in
+      let _ = Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec) in
+      ()
+    end
   else
-    let _ = Unix.system ("ocamlbuild -lib nums " ^ spec ^ ".cmo") in
+    let _ = Unix.system ("ocamlbuild -pkg zarith -pkg uint " ^ spec ^ ".cmo") in
     ();
   Unix.chdir cwd
 
diff --git a/src/parser2.mly b/src/parser2.mly
index 42e13721..02a8f09c 100644
--- a/src/parser2.mly
+++ b/src/parser2.mly
@@ -139,7 +139,7 @@ let rec desugar_rchain chain s e =
 
 /*Terminals with content*/
 
-%token <string> Id TyVar Decl TyDecl
+%token <string> Id TyVar
 %token <int> Num
 %token <string> String Bin Hex Real
 
@@ -153,9 +153,8 @@ let rec desugar_rchain chain s e =
 %token <string> Op0r Op1r Op2r Op3r Op4r Op5r Op6r Op7r Op8r Op9r
 
 %start file
-%start typschm
-%type <Parse_ast.typschm> typschm
-%type <Parse_ast.defs> defs
+%start typschm_eof
+%type <Parse_ast.typschm> typschm_eof
 %type <Parse_ast.defs> file
 
 %%
@@ -233,10 +232,6 @@ op7r: Op7r { mk_id (Id $1) $startpos $endpos }
 op8r: Op8r { mk_id (Id $1) $startpos $endpos }
 op9r: Op9r { mk_id (Id $1) $startpos $endpos }
 
-decl:
-  | Decl
-    { mk_id (Id $1) $startpos $endpos }
-
 id_list:
   | id
     { [$1] }
@@ -247,10 +242,6 @@ kid:
   | TyVar
     { mk_kid $1 $startpos $endpos }
 
-tydecl:
-  | TyDecl
-    { mk_kid $1 $startpos $endpos }
-
 kid_list:
   | kid
     { [$1] }
@@ -515,8 +506,6 @@ 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
@@ -589,6 +578,10 @@ typschm:
   | Forall typquant Dot typ MinusGt typ Effect effect_set
     { (fun s e -> mk_typschm $2 (mk_typ (ATyp_fn ($4, $6, $8)) s e) s e) $startpos $endpos }
 
+typschm_eof:
+  | typschm Eof
+    { $1 }
+
 pat:
   | atomic_pat
     { $1 }
@@ -612,14 +605,10 @@ atomic_pat:
     { mk_pat (P_id $1) $startpos $endpos }
   | kid
     { mk_pat (P_var $1) $startpos $endpos }
-  | tydecl typ
-    { mk_pat (P_typ ($2, mk_pat (P_var $1) $startpos $endpos($1))) $startpos $endpos }
   | id Lparen pat_list Rparen
     { mk_pat (P_app ($1, $3)) $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 }
 
@@ -646,27 +635,21 @@ lit:
     { mk_lit (L_string $1) $startpos $endpos }
 
 exp:
-  | cast_exp Colon typ
-    { mk_exp (E_cast ($3, $1)) $startpos $endpos }
-  | cast_exp
-    { $1 }
-
-cast_exp:
   | exp0
     { $1 }
-  | atomic_exp Eq cast_exp
+  | atomic_exp Eq exp
     { mk_exp (E_assign ($1, $3)) $startpos $endpos }
-  | Let_ letbind In cast_exp
+  | Let_ letbind In exp
     { mk_exp (E_let ($2, $4)) $startpos $endpos }
   | Lcurly block Rcurly
     { mk_exp (E_block $2) $startpos $endpos }
-  | Return cast_exp
+  | Return exp
     { mk_exp (E_return $2) $startpos $endpos }
-  | Throw cast_exp
+  | Throw exp
     { mk_exp (E_throw $2) $startpos $endpos }
-  | If_ exp Then cast_exp Else cast_exp
+  | If_ exp Then exp Else exp
     { mk_exp (E_if ($2, $4, $6)) $startpos $endpos }
-  | If_ exp Then cast_exp
+  | If_ exp Then exp
     { mk_exp (E_if ($2, $4, mk_lit_exp L_unit $endpos($4) $endpos($4))) $startpos $endpos }
   | Match exp Lcurly case_list Rcurly
     { mk_exp (E_case ($2, $4)) $startpos $endpos }
@@ -856,12 +839,14 @@ block:
     { LB_aux (LB_val_implicit ($1, $3), loc $startpos $endpos) }
 
 atomic_exp:
+  | atomic_exp Colon atomic_typ
+    { mk_exp (E_cast ($3, $1)) $startpos $endpos }
   | lit
     { mk_exp (E_lit $1) $startpos $endpos }
-  | decl atomic_typ
-    { mk_exp (E_cast ($2, mk_exp (E_id $1) $startpos $endpos($1))) $startpos $endpos }
   | id
     { mk_exp (E_id $1) $startpos $endpos }
+  | kid
+    { mk_exp (E_sizeof (mk_typ (ATyp_var $1) $startpos $endpos)) $startpos $endpos }
   | id Unit
     { mk_exp (E_app ($1, [mk_lit_exp L_unit $startpos($2) $endpos])) $startpos $endpos }
   | id Lparen exp_list Rparen
@@ -922,8 +907,6 @@ enum:
     { $1 :: $3 }
 
 struct_field:
-  | decl typ
-    { ($2, $1) }
   | id Colon typ
     { ($3, $1) }
 
@@ -936,8 +919,6 @@ 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
@@ -960,14 +941,10 @@ let_def:
     { $2 }
 
 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 }
 
 register_def:
-  | Register decl typ
-    { mk_reg_dec (DEC_reg ($3, $2)) $startpos $endpos }
   | Register id Colon typ
     { mk_reg_dec (DEC_reg ($4, $2)) $startpos $endpos }
 
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 70f5b749..02cc3574 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -212,7 +212,7 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
     | Nexp_var v -> doc_var v
     | Nexp_id i  -> braces (doc_id i)
-    | Nexp_constant i -> doc_int i
+    | Nexp_constant i -> if i < 0 then parens(doc_int i) else doc_int i
     | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
       group (parens (nexp ne))
 
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 5e0d39a0..1bfb19aa 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -418,10 +418,21 @@ let doc_exp_lem, doc_let_lem =
                    (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                      parens (string "update_reg_field_bit" ^/^ field_ref ^/^ expY e2) ^/^ expY e)))
             | _ ->
-               liftR ((prefix 2 1)
-                 (string "update_reg")
-                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
-                   parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e))
+               (match le with
+                 | LEXP_aux (_, (_, Some (_, Typ_aux (Typ_app (vector, [_; _; _; Typ_arg_aux (Typ_arg_typ etyp, _)]), _), _)))
+                   when is_reftyp etyp && string_of_id vector = "vector" ->
+                   (* Special case vectors of register references *)
+                   let deref =
+                     parens (separate space [
+                       string "access";
+                       expY (lexp_to_exp le);
+                       expY e2
+                       ]) in
+                   liftR ((prefix 2 1) (string "write_reg") (deref ^/^ expY e))
+                 | _ ->
+                   liftR ((prefix 2 1) (string "update_reg")
+                   (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
+                     parens (string "update_reg_bit" ^/^ expY e2) ^/^ expY e)))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
@@ -519,14 +530,19 @@ let doc_exp_lem, doc_let_lem =
             if contains_bitvector_typ t && not (contains_t_pp_var t)
             then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
             else (epp, aexp_needed) in
-          if aexp_needed then parens (align taepp) else taepp
+          if aexp_needed then parens (align taepp) else taepp*)
        | Id_aux (Id "length",_) ->
+          (* Another temporary hack: The sizeof rewriting introduces calls to
+             "length", and the disambiguation between the length function on
+             bitvectors and vectors of other element types should be done by
+             the type checker, but type checking after rewriting steps is
+             currently broken. *)
           let [arg] = args in
           let targ = typ_of arg in
-          let call = if is_bitvector_typ targ then "bvlength" else "length" in
+          let call = if mwords && is_bitvector_typ targ then "bvlength" else "length" in
           let epp = separate space [string call;expY arg] in
           if aexp_needed then parens (align epp) else epp
-       | Id_aux (Id "bool_not", _) ->
+       (*)| Id_aux (Id "bool_not", _) ->
           let [a] = args in
           let epp = align (string "~" ^^ expY a) in
           if aexp_needed then parens (align epp) else epp *)
@@ -698,7 +714,9 @@ let doc_exp_lem, doc_let_lem =
         | _ -> parens (separate_map comma expN exps))
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
        let recordtyp = match annot with
-         | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+         | Some (env, Typ_aux (Typ_id tid,_), _)
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+           when Env.is_record tid env ->
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        let epp = anglebars (space ^^ (align (separate_map
@@ -706,9 +724,11 @@ let doc_exp_lem, doc_let_lem =
                                           (doc_fexp sequential mwords early_ret recordtyp) fexps)) ^^ space) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-       let (E_aux (_, (_, eannot))) = e in
-       let recordtyp = match eannot with
-         | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
+       (* let (E_aux (_, (_, eannot))) = e in *)
+       let recordtyp = match annot with
+         | Some (env, Typ_aux (Typ_id tid,_), _)
+         | Some (env, Typ_aux (Typ_app (tid, _), _), _)
+           when Env.is_record tid env ->
            tid
          | _ ->  raise (report l ("cannot get record type from annot " ^ string_of_annot annot ^ " of exp " ^ string_of_exp full_exp)) in
        anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 5edf9d12..73f06d1a 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -208,9 +208,9 @@ and pp_format_effects_lem (Effect_aux(e,l)) =
 and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) =
   "(Typ_arg_aux " ^
   (match t with
-  | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
-  | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
-  | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")");
+   | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
+   | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
+   | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")") ^ " " ^
   (pp_format_l_lem l) ^ ")"
 and pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
   "(NC_aux " ^
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index 69c5c084..2bd5d5bc 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -87,19 +87,48 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-let format_pos ff p = (
-  Format.fprintf ff "File \"%s\", line %d, character %d:\n"
-    p.Lexing.pos_fname p.Lexing.pos_lnum (p.Lexing.pos_cnum - p.Lexing.pos_bol);
-  Format.pp_print_flush ff ())
-
-
-let format_pos2 ff p1 p2 = (
-  Format.fprintf ff "File \"%s\", line %d, character %d to line %d, character %d"
-    p1.Lexing.pos_fname 
-    p1.Lexing.pos_lnum (p1.Lexing.pos_cnum - p1.Lexing.pos_bol + 1)
-    p2.Lexing.pos_lnum (p2.Lexing.pos_cnum - p2.Lexing.pos_bol);
-  Format.pp_print_flush ff ()
-)
+let format_pos ff p =
+  let open Lexing in
+  begin
+    Format.fprintf ff "file \"%s\", line %d, character %d:\n"
+                   p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol);
+    Format.pp_print_flush ff ()
+  end
+
+let rec skip_lines in_chan = function
+  | n when n <= 0 -> ()
+  | n -> input_line in_chan; skip_lines in_chan (n - 1)
+
+let termcode n = "\x1B[" ^ string_of_int n ^ "m"
+
+let print_code ff fname lnum1 cnum1 cnum2 =
+  try
+    let in_chan = open_in fname in
+    begin
+      try
+        skip_lines in_chan (lnum1 - 1);
+        let line = input_line in_chan in
+        Format.fprintf ff "%s%s%s%s%s"
+                       (Str.string_before line cnum1)
+                       (termcode 41)
+                       (Str.string_before (Str.string_after line cnum1) (cnum2 - cnum1))
+                       (termcode 49)
+                       (Str.string_after line cnum2);
+        close_in in_chan
+      with e -> (close_in_noerr in_chan; print_endline (Printexc.to_string e))
+    end
+  with _ -> ()
+
+let format_pos2 ff p1 p2 =
+  let open Lexing in
+  begin
+    Format.fprintf ff "file \"%s\", line %d, character %d to line %d, character %d\n\n"
+                   p1.pos_fname
+                   p1.pos_lnum (p1.pos_cnum - p1.pos_bol + 1)
+                   p2.pos_lnum (p2.pos_cnum - p2.pos_bol);
+    print_code ff p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) (p2.pos_cnum - p2.pos_bol);
+    Format.pp_print_flush ff ()
+  end
 
 (* reads the part between p1 and p2 from the file *)
 
@@ -171,12 +200,12 @@ let loc_to_string l =
 type pos_or_loc = Loc of Parse_ast.l | LocD of Parse_ast.l * Parse_ast.l | Pos of Lexing.position
 
 let print_err_internal fatal verb_loc p_l m1 m2 =
+  Format.eprintf "%s at " m1;
   let _ = (match p_l with Pos p -> print_err_pos p
                         | Loc l -> print_err_loc l
                         | LocD (l1,l2) ->
                           print_err_loc l1; Format.fprintf Format.err_formatter " and "; print_err_loc l2) in
-  let m12 = if String.length m2 = 0 then "" else ": " in
-  Format.eprintf "  %s%s%s\n" m1 m12 m2;
+  Format.eprintf "%s\n" m2;
   if verb_loc then (match p_l with Loc l ->
       format_loc_source Format.err_formatter l;
       Format.pp_print_newline Format.err_formatter (); | _ -> ());
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 2b096609..fed8408d 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -2209,29 +2209,20 @@ let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match annot with
   | Some (_, _, eff) -> effectful_effs eff
   | _ -> false
 
-let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) = match lexp with
-  | LEXP_id id | LEXP_cast (_, id) ->
-    (le, E_aux (E_id id, annot), (fun exp -> exp))
-  | LEXP_tup les ->
-    let get_id (LEXP_aux(lexp,((l,_) as annot)) as le) = match lexp with
-      | LEXP_id id | LEXP_cast (_, id) -> E_aux (E_id id, annot)
-      | _ ->
-        raise (Reporting_basic.err_unreachable l
-          ("Unsupported sub-lexp " ^ string_of_lexp le ^ " in tuple")) in
-    (le, E_aux (E_tuple (List.map get_id les), annot), (fun exp -> exp))
+let rec rewrite_local_lexp ((LEXP_aux(lexp,((l,_) as annot))) as le) =
+  match lexp with
+  | LEXP_id _ | LEXP_cast (_, _) | LEXP_tup _ -> (le, (fun exp -> exp))
   | LEXP_vector (lexp, e) ->
-    let (lexp, access, rexp) = rewrite_local_lexp lexp in
-    (lexp, E_aux (E_vector_access (access, e), annot),
-    (fun exp -> rexp (E_aux (E_vector_update (access, e, exp), annot))))
+    let (lhs, rhs) = rewrite_local_lexp lexp in
+    (lhs, (fun exp -> rhs (E_aux (E_vector_update (lexp_to_exp lexp, e, exp), annot))))
   | LEXP_vector_range (lexp, e1, e2) ->
-    let (lexp, access, rexp) = rewrite_local_lexp lexp in
-    (lexp, E_aux (E_vector_subrange (access, e1, e2), annot),
-    (fun exp -> rexp (E_aux (E_vector_update_subrange (access, e1, e2, exp), annot))))
+    let (lhs, rhs) = rewrite_local_lexp lexp in
+    (lhs, (fun exp -> rhs (E_aux (E_vector_update_subrange (lexp_to_exp lexp, e1, e2, exp), annot))))
   | LEXP_field (lexp, id) ->
-    let (lexp, access, rexp) = rewrite_local_lexp lexp in
+    let (lhs, rhs) = rewrite_local_lexp lexp in
+    let (LEXP_aux (_, recannot)) = lexp in
     let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
-    (lexp, E_aux (E_field (access, id), annot),
-    (fun exp -> rexp (E_aux (E_record_update (access, field_update exp), annot))))
+    (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), recannot))))
   | _ -> raise (Reporting_basic.err_unreachable l ("Unsupported lexp: " ^ string_of_lexp le))
 
 (*Expects to be called after rewrite_defs; thus the following should not appear:
@@ -2250,7 +2241,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
       | [] -> []
       | (E_aux(E_assign(le,e), ((l, Some (env,typ,eff)) as annot)) as exp)::exps
         when lexp_is_local_intro le env && not (lexp_is_effectful le) ->
-        let (le', _, re') = rewrite_local_lexp le in
+        let (le', re') = rewrite_local_lexp le in
         let e' = re' (rewrite_base e) in
         let exps' = walker exps in
         let effects = union_eff_exps exps' in
@@ -2303,7 +2294,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
     rewrap (E_block (walker exps))
   | E_assign(le,e)
     when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
-    let (le', _, re') = rewrite_local_lexp le in
+    let (le', re') = rewrite_local_lexp le in
     let e' = re' (rewrite_base e) in
     let block = E_aux (E_block [], simple_annot l unit_typ) in
     fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))
@@ -2530,7 +2521,7 @@ let rewrite_undefined =
   let rewrite_e_aux (E_aux (e_aux, _) as exp) =
     match e_aux with
     | E_lit (L_aux (L_undef, l)) ->
-       check_exp (env_of exp) (undefined_of_typ (typ_of exp)) (typ_of exp)
+       check_exp (env_of exp) (undefined_of_typ (Env.expand_synonyms (env_of exp) (typ_of exp))) (typ_of exp)
     | _ -> exp
   in
   let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
@@ -2635,7 +2626,7 @@ let rewrite_simple_assignments defs =
     let env = env_of_annot annot in
     match e_aux with
     | E_assign (lexp, exp) ->
-       let (lexp, _, rhs) = rewrite_local_lexp lexp in
+       let (lexp, rhs) = rewrite_local_lexp lexp in
        let assign = mk_exp (E_assign (strip_lexp lexp, strip_exp (rhs exp))) in
        check_exp env assign unit_typ
     | _ -> E_aux (e_aux, annot)
@@ -2956,6 +2947,18 @@ let rewrite_defs_letbind_effects  =
       let _ = reset_fresh_name_counter () in
       FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot)
     in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),fdannot) in
+  let rewrite_def rewriters = function
+    | DEF_val (LB_aux (lb, annot)) ->
+      let rewrap lb = DEF_val (LB_aux (lb, annot)) in
+      begin
+        match lb with
+        | LB_val_implicit (pat, exp) ->
+          rewrap (LB_val_implicit (pat, n_exp_term (effectful exp) exp))
+        | LB_val_explicit (ts, pat, exp) ->
+          rewrap (LB_val_explicit (ts, pat, n_exp_term (effectful exp) exp))
+      end
+    | DEF_fundef fdef -> DEF_fundef (rewrite_fun rewriters fdef)
+    | d -> d in
   rewrite_defs_base
     {rewrite_exp = rewrite_exp
     ; rewrite_pat = rewrite_pat
@@ -2977,9 +2980,9 @@ let rewrite_defs_effectful_let_expressions =
   let e_let (lb,body) =
     match lb with
     | LB_aux (LB_val_implicit (P_aux (P_wild, _), E_aux (E_assign ((LEXP_aux (_, annot) as le), exp), _)), _)
-      when lexp_is_local le (env_of_annot annot) ->
+      when lexp_is_local le (env_of_annot annot) && not (lexp_is_effectful le) ->
       (* Rewrite assignments to local variables into let bindings *)
-      let (lhs, _, rhs) = rewrite_local_lexp le in
+      let (lhs, rhs) = rewrite_local_lexp le in
       E_let (LB_aux (LB_val_implicit (pat_of_local_lexp lhs, rhs exp), annot), body)
     | LB_aux (LB_val_explicit (_,pat,exp'),annot')
     | LB_aux (LB_val_implicit (pat,exp'),annot') ->
@@ -3023,28 +3026,28 @@ let eqidtyp (id1,_) (id2,_) =
   name1 = name2
 
 let find_introduced_vars exp =
-  let lEXP_aux ((ids,lexp),annot) =
-    let ids = match lexp, annot with
-    | LEXP_id id, (_, Some (env, _, _))
-    | LEXP_cast (_, id), (_, Some (env, _, _))
+  let e_aux ((ids,e_aux),annot) =
+    let ids = match e_aux, annot with
+    | E_internal_let (LEXP_aux (LEXP_id id, _), _, _), (_, Some (env, _, _))
+    | E_internal_let (LEXP_aux (LEXP_cast (_, id), _), _, _), (_, Some (env, _, _))
       when id_is_unbound id env -> IdSet.add id ids
     | _ -> ids in
-    (ids, LEXP_aux (lexp, annot)) in
+    (ids, E_aux (e_aux, annot)) in
   fst (fold_exp
-    { (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
+    { (compute_exp_alg IdSet.empty IdSet.union) with e_aux = e_aux } exp)
 
 let find_updated_vars exp =
   let intros = find_introduced_vars exp in
-  let lEXP_aux ((ids,lexp),annot) =
-    let ids = match lexp, annot with
-    | LEXP_id id, (_, Some (env, _, _))
-    | LEXP_cast (_, id), (_, Some (env, _, _))
+  let e_aux ((ids,e_aux),annot) =
+    let ids = match e_aux, annot with
+    | E_assign (LEXP_aux (LEXP_id id, _), _), (_, Some (env, _, _))
+    | E_assign (LEXP_aux (LEXP_cast (_, id), _), _), (_, Some (env, _, _))
       when id_is_local_var id env && not (IdSet.mem id intros) ->
       (id, annot) :: ids
     | _ -> ids in
-    (ids, LEXP_aux (lexp, annot)) in
+    (ids, E_aux (e_aux, annot)) in
   dedup eqidtyp (fst (fold_exp
-    { (compute_exp_alg [] (@)) with lEXP_aux = lEXP_aux } exp))
+    { (compute_exp_alg [] (@)) with e_aux = e_aux } exp))
 
 let swaptyp typ (l,tannot) = match tannot with
   | Some (env, typ', eff) -> (l, Some (env, typ, eff))
@@ -3426,7 +3429,7 @@ let rewrite_defs_remove_e_assign =
 let recheck_defs defs = fst (check initial_env defs)
 
 let rewrite_defs_lem =[
-  (* top_sort_defs; *)
+  top_sort_defs;
   rewrite_trivial_sizeof;
   rewrite_sizeof;
   rewrite_defs_remove_vector_concat;
diff --git a/src/sail.ml b/src/sail.ml
index 04e1a6fd..312a3c7c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -65,7 +65,7 @@ let options = Arg.align ([
     Arg.Set opt_print_lem,
     " output a Lem translated version of the input");
   ( "-ocaml",
-    Arg.Set opt_print_ocaml,
+    Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
     " output an OCaml translated version of the input");
   ( "-lem_lib",
     Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem),
@@ -102,7 +102,7 @@ let options = Arg.align ([
     " (experimental) use new parser");
   ( "-just_check",
     Arg.Set opt_just_check,
-    " (experimental) terminate immediately after typechecking, implies -new_typecheck");
+    " (experimental) terminate immediately after typechecking");
   ( "-ddump_tc_ast",
     Arg.Set opt_ddump_tc_ast,
     " (debug) dump the typechecked ast to stdout");
@@ -118,6 +118,9 @@ let options = Arg.align ([
   ( "-no_effects",
     Arg.Set Type_check.opt_no_effects,
     " turn off effect checking");
+  ( "-undefined-gen",
+    Arg.Set Initial_check.opt_undefined_gen,
+    " generate undefined_type functions for types in the specification");
   ( "-v",
     Arg.Set opt_print_version,
     " print version");
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 5281ef27..d349037e 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -350,6 +350,7 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
     b,used,set
   | E_exit e -> fv_of_exp consider_var bound used set e
   | E_assert(c,m) -> list_fv bound used set [c;m]
+  | E_return e -> fv_of_exp consider_var bound used set e
   | _ -> bound,used,set
 
 and fv_of_pes consider_var bound used set pes =
diff --git a/src/type_check.ml b/src/type_check.ml
index 4eb0688b..f952d0d6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -65,9 +65,47 @@ let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ m) el
 
 let typ_warning m = prerr_endline ("Warning: " ^ m)
 
-exception Type_error of l * string;;
+type type_error =
+  (* First parameter is the error that caused us to start doing type
+     coercions, the second is the errors encountered by all possible
+     coerctions *)
+  | Err_no_casts of type_error * type_error list
+  | Err_subtype of typ * typ * n_constraint list
+  | Err_other of string
+
+let pp_type_error err =
+  let open PPrint in
+  let rec pp_err = function
+    | Err_no_casts (trigger, []) ->
+       (string "Tried performing type coercion because" ^//^ pp_err trigger)
+       ^/^ string "No possible coercions"
+    | Err_no_casts (trigger, errs) ->
+       (string "Tried performing type coerction because" ^//^ pp_err trigger)
+    | Err_subtype (typ1, typ2, []) ->
+       separate space [ string (string_of_typ typ1);
+                        string "is not a subtype of";
+                        string (string_of_typ typ2) ]
+    | Err_subtype (typ1, typ2, constrs) ->
+       separate space [ string (string_of_typ typ1);
+                        string "is not a subtype of";
+                        string (string_of_typ typ2) ]
+       ^/^ string "in context"
+       ^//^ string (string_of_list ", " string_of_n_constraint constrs)
+    | Err_other str -> string str
+  in
+  pp_err err
+
+let rec string_of_type_error err =
+  let open PPrint in
+  let b = Buffer.create 20 in
+  ToBuffer.pretty 1. 120 b (pp_type_error err);
+  "\n" ^ Buffer.contents b
+
+exception Type_error of l * type_error;;
 
-let typ_error l m = raise (Type_error (l, m))
+let typ_error l m = raise (Type_error (l, Err_other m))
+
+let typ_raise l err = raise (Type_error (l, err))
 
 let deinfix = function
   | Id_aux (Id v, l) -> Id_aux (DeIid v, l)
@@ -1447,9 +1485,7 @@ let rec subtyp l env typ1 typ2 =
   | _, None ->
      if subtyp_tnf env (normalize_typ env typ1) (normalize_typ env typ2)
      then ()
-     else typ_error l (string_of_typ typ1
-                       ^ " is not a subtype of " ^ string_of_typ typ2
-                       ^ " in context " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
+     else typ_raise l (Err_subtype (typ1, typ2, Env.get_constraints env))
 
 let typ_equality l env typ1 typ2 =
   subtyp l env typ1 typ2; subtyp l env typ2 typ1
@@ -1573,6 +1609,8 @@ let env_of (E_aux (_, (l, tannot))) = env_of_annot (l, tannot)
 
 let pat_typ_of (P_aux (_, (l, tannot))) = typ_of_annot (l, tannot)
 
+let pat_env_of (P_aux (_, (l, tannot))) = env_of_annot (l, tannot)
+
 (* Flow typing *)
 
 let rec big_int_of_nexp (Nexp_aux (nexp, _)) = match nexp with
@@ -1780,7 +1818,7 @@ let crule r env exp typ =
     let checked_exp = r env exp typ in
     decr depth; checked_exp
   with
-  | Type_error (l, m) -> decr depth; typ_error l m
+  | Type_error (l, err) -> decr depth; typ_raise l err
 
 let irule r env exp =
   incr depth;
@@ -1790,7 +1828,7 @@ let irule r env exp =
     decr depth;
     inferred_exp
   with
-  | Type_error (l, m) -> decr depth; typ_error l m
+  | Type_error (l, err) -> decr depth; typ_raise l err
 
 let strip_exp : 'a exp -> unit exp = function exp -> map_exp_annot (fun (l, _) -> (l, ())) exp
 let strip_pat : 'a pat -> unit pat = function pat -> map_pat_annot (fun (l, _) -> (l, ())) pat
@@ -1926,7 +1964,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        | (f :: fs) -> begin
            typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")");
            try crule check_exp env (E_aux (E_app (f, xs), (l, ()))) typ with
-           | Type_error (_, m) -> typ_print ("Error : " ^ m); try_overload fs
+           | Type_error (_, err) -> typ_print ("Error : " ^ string_of_type_error err); try_overload fs
          end
      in
      try_overload (Env.get_overloads f env)
@@ -1989,15 +2027,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
 and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
-  let rec try_casts m = function
-    | [] -> typ_error l ("No valid casts:\n" ^ m)
+  let rec try_casts trigger errs = function
+    | [] -> typ_raise l (Err_no_casts (trigger, errs))
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " to " ^ string_of_typ typ);
         try
           let checked_cast = crule check_exp (Env.no_casts env) (strip (E_app (cast, [annotated_exp]))) typ in
           annot_exp (E_cast (typ, checked_cast)) typ
         with
-        | Type_error (_, m) -> try_casts m casts
+        | Type_error (_, err) -> try_casts trigger (err :: errs) casts
       end
   in
   begin
@@ -2005,10 +2043,10 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
       typ_debug ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ);
       subtyp l env (typ_of annotated_exp) typ; annotated_exp
     with
-    | Type_error (_, m) when Env.allow_casts env ->
+    | Type_error (_, trigger) when Env.allow_casts env ->
        let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
-       try_casts "" casts
-    | Type_error (l, m) -> typ_error l ("Subtype error " ^ m)
+       try_casts trigger [] casts
+    | Type_error (l, err) -> typ_error l "Subtype error"
   end
 
 (* type_coercion_unify env exp typ attempts to coerce exp to a type
@@ -2019,8 +2057,8 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ =
 and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
   let strip exp_aux = strip_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))) in
   let annot_exp exp typ = E_aux (exp, (l, Some (env, typ, no_effect))) in
-  let rec try_casts m = function
-    | [] -> unify_error l ("No valid casts resulted in unification:\n" ^ m)
+  let rec try_casts = function
+    | [] -> unify_error l "No valid casts resulted in unification"
     | (cast :: casts) -> begin
         typ_print ("Casting with " ^ string_of_id cast ^ " expression " ^ string_of_exp annotated_exp ^ " for unification");
         try
@@ -2028,8 +2066,8 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
           let ityp = typ_of inferred_cast in
           annot_exp (E_cast (ityp, inferred_cast)) ityp, unify l env typ ityp
         with
-        | Type_error (_, m) -> try_casts m casts
-        | Unification_error (_, m) -> try_casts m casts
+        | Type_error (_, err) -> try_casts casts
+        | Unification_error (_, err) -> try_casts casts
       end
   in
   begin
@@ -2039,7 +2077,7 @@ and type_coercion_unify env (E_aux (_, (l, _)) as annotated_exp) typ =
     with
     | Unification_error (_, m) when Env.allow_casts env ->
        let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in
-       try_casts "" casts
+       try_casts casts
   end
 
 and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ) =
@@ -2495,7 +2533,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        | (f :: fs) -> begin
            typ_print ("Overload: " ^ string_of_id f ^ "(" ^ string_of_list ", " string_of_exp xs ^ ")");
            try irule infer_exp env (E_aux (E_app (f, xs), (l, ()))) with
-           | Type_error (_, m) -> typ_print ("Error: " ^ m); try_overload fs
+           | Type_error (_, err) -> typ_print ("Overload error"); try_overload fs
          end
      in
      try_overload (Env.get_overloads f env)
@@ -3123,7 +3161,7 @@ let mk_synonym typq typ =
        typ_subst_typ (kopt_kid kopt) (unaux_typ arg) typ, ncs
     | kopt :: kopts, Typ_arg_aux (Typ_arg_order arg, _) :: args when is_order_kopt kopt ->
        let typ, ncs = subst_args kopts args in
-       typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs     
+       typ_subst_order (kopt_kid kopt) (unaux_order arg) typ, ncs
     | [], [] -> typ, ncs
     | _, Typ_arg_aux (_, l) :: _ -> typ_error l "Synonym applied to bad arguments"
     | _, _ -> typ_error Parse_ast.Unknown "Synonym applied to bad arguments"
@@ -3191,4 +3229,4 @@ let rec check' env (Defs defs) =
 
 let check env defs =
   try check' env defs with
-  | Type_error (l, m) -> raise (Reporting_basic.err_typ l m)
+  | Type_error (l, err) -> raise (Reporting_basic.err_typ l (string_of_type_error err))
diff --git a/src/type_check.mli b/src/type_check.mli
index 857e0019..ca2fb90c 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -47,7 +47,9 @@ open Ast_util
 val opt_tc_debug : int ref
 val opt_no_effects : bool ref
 
-exception Type_error of l * string;;
+type type_error
+
+exception Type_error of l * type_error;;
 
 type mut = Immutable | Mutable
 
@@ -201,6 +203,7 @@ val typ_of : tannot exp -> typ
 val typ_of_annot : Ast.l * tannot -> typ
 
 val pat_typ_of : tannot pat -> typ
+val pat_env_of : tannot pat -> Env.t
 
 val effect_of : tannot exp -> effect
 val effect_of_annot : tannot -> effect