Merge remote-tracking branch 'origin/sail2' into polymorphic_variants

11 files changed, 408 insertions, 150 deletions

diff --git a/src/latex.ml b/src/latex.ml
index 39db43db..0520d074 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -126,7 +126,7 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) dir cmd no_loc ((l
     | Some l -> Printf.sprintf "\\label{%s}" l
   in
   let cmd = !opt_prefix_latex ^ prefix ^ cmd in
-  let lcmd = String.lowercase_ascii cmd in  (* lowercase to avoid file names differing only by case *)
+  let lcmd = String.lowercase cmd in  (* lowercase to avoid file names differing only by case *)
   if StringSet.mem lcmd !commands then
     latex_command ~label:label dir (cmd ^ "v") no_loc annot
   else
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index c17e879f..a5cb96ff 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -481,7 +481,7 @@ let rec instr_parms_to_string ps =
 let pad n s = if String.length s < n then s ^ String.make (n-String.length s) ' ' else s
 
 let instruction_to_string (name, parms) = 
-  ((*pad 5*) (String.lowercase_ascii name)) ^ " " ^ instr_parms_to_string parms 
+  ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms 
 
 let print_backtrace_compact printer (IState(stack,_)) =
   List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack)
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index adc4d6d2..ab6d9e2d 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -3167,13 +3167,15 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
     | None -> r
     | Some (tenv,typ,_) ->
        let typ = Env.base_typ_of tenv typ in
-       let env, typ =
+       let env, tenv, typ =
          match destruct_exist tenv typ with
-         | None -> env, typ
+         | None -> env, tenv, typ
          | Some (kids, nc, typ) ->
             { env with kid_deps =
                 List.fold_left (fun kds kid -> KBindings.add kid deps kds) env.kid_deps kids },
-            typ
+           Env.add_constraint nc
+             (List.fold_left (fun tenv kid -> Env.add_typ_var l kid BK_int tenv) tenv kids),
+           typ
        in
        if is_bitvector_typ typ then
          let size,_,_ = vector_typ_args_of typ in
@@ -3644,6 +3646,14 @@ let is_constant_vec_typ env typ =
 
 let rewrite_app env typ (id,args) =
   let is_append = is_id env (Id "append") in
+  let try_cast_to_typ (E_aux (e,_) as exp) =
+    let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
+    match size with
+    | Nexp_aux (Nexp_constant _,_) -> E_cast (typ,exp)
+    | _ -> match solve env size with
+      | Some c -> E_cast (vector_typ (nconstant c) order bittyp, exp)
+      | None -> e
+  in
   if is_append id then
     let is_subrange = is_id env (Id "vector_subrange") in
     let is_slice = is_id env (Id "slice") in
@@ -3661,14 +3671,23 @@ let rewrite_app env typ (id,args) =
           not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
-       let midsize = nminus size size1 in
-       let midtyp = vector_typ midsize order bittyp in
-       E_app (append,
-              [e1;
-               E_aux (E_cast (midtyp,
-                              E_aux (E_app (mk_id "subrange_subrange_concat",
-                                            [vector1; start1; end1; vector2; start2; end2]),
-                                     (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+       let midsize = nminus size size1 in begin
+         match solve env midsize with
+         | Some c ->
+            let midtyp = vector_typ (nconstant c) order bittyp in
+            E_app (append,
+                   [e1;
+                    E_aux (E_cast (midtyp,
+                                   E_aux (E_app (mk_id "subrange_subrange_concat",
+                                                 [vector1; start1; end1; vector2; start2; end2]),
+                                          (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+         | _ ->
+            E_app (append,
+                   [e1;
+                    E_aux (E_app (mk_id "subrange_subrange_concat",
+                                  [vector1; start1; end1; vector2; start2; end2]),
+                           (Unknown,empty_tannot))])
+       end
     | [E_aux (E_app (append,
               [e1;
                E_aux (E_app (slice1,
@@ -3680,14 +3699,23 @@ let rewrite_app env typ (id,args) =
           not (is_constant length1 || is_constant length2) ->
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
-       let midsize = nminus size size1 in
-       let midtyp = vector_typ midsize order bittyp in
-       E_app (append,
-              [e1;
-               E_aux (E_cast (midtyp,
-                              E_aux (E_app (mk_id "slice_slice_concat",
-                                            [vector1; start1; length1; vector2; start2; length2]),
-                                     (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+       let midsize = nminus size size1 in begin
+         match solve env midsize with
+         | Some c ->
+            let midtyp = vector_typ (nconstant c) order bittyp in
+            E_app (append,
+                   [e1;
+                    E_aux (E_cast (midtyp,
+                                   E_aux (E_app (mk_id "slice_slice_concat",
+                                                 [vector1; start1; length1; vector2; start2; length2]),
+                                          (Unknown,empty_tannot))),(Unknown,empty_tannot))])
+         | _ ->
+            E_app (append,
+                   [e1;
+                    E_aux (E_app (mk_id "slice_slice_concat",
+                                  [vector1; start1; length1; vector2; start2; length2]),
+                           (Unknown,empty_tannot))])
+       end
 
     (* variable-range @ variable-range *)
     | [E_aux (E_app (subrange1,
@@ -3696,10 +3724,10 @@ let rewrite_app env typ (id,args) =
                      [vector2; start2; end2]),_)]
         when is_subrange subrange1 && is_subrange subrange2 &&
           not (is_constant_range (start1, end1) || is_constant_range (start2, end2)) ->
-       E_cast (typ,
-               E_aux (E_app (mk_id "subrange_subrange_concat",
-                             [vector1; start1; end1; vector2; start2; end2]),
-                      (Unknown,empty_tannot)))
+       try_cast_to_typ
+         (E_aux (E_app (mk_id "subrange_subrange_concat",
+                        [vector1; start1; end1; vector2; start2; end2]),
+                 (Unknown,empty_tannot)))
 
     (* variable-slice @ variable-slice *)
     | [E_aux (E_app (slice1,
@@ -3708,9 +3736,9 @@ let rewrite_app env typ (id,args) =
                      [vector2; start2; length2]),_)]
         when is_slice slice1 && is_slice slice2 &&
           not (is_constant length1 || is_constant length2) ->
-       E_cast (typ,
-               E_aux (E_app (mk_id "slice_slice_concat",
-                             [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
+       try_cast_to_typ
+         (E_aux (E_app (mk_id "slice_slice_concat",
+                        [vector1; start1; length1; vector2; start2; length2]),(Unknown,empty_tannot)))
 
     | [E_aux (E_app (append1,
                      [e1;
@@ -3721,16 +3749,25 @@ let rewrite_app env typ (id,args) =
           not (is_constant length1 || is_constant length2) ->
        let (size,order,bittyp) = vector_typ_args_of (Env.base_typ_of env typ) in
        let (size1,_,_) = vector_typ_args_of (Env.base_typ_of env (typ_of e1)) in
-       let midsize = nminus size size1 in
-       let midtyp = vector_typ midsize order bittyp in
-       E_cast (typ,
-               E_aux (E_app (mk_id "append",
+       let midsize = nminus size size1 in begin
+         match solve env midsize with
+         | Some c ->
+            let midtyp = vector_typ (nconstant c) order bittyp in
+            try_cast_to_typ
+              (E_aux (E_app (mk_id "append",
                              [e1;
                               E_aux (E_cast (midtyp,
                                              E_aux (E_app (mk_id "slice_zeros_concat",
                                                            [vector1; start1; length1; length2]),(Unknown,empty_tannot))),(Unknown,empty_tannot))]),
                       (Unknown,empty_tannot)))
-
+         | _ ->
+            try_cast_to_typ
+              (E_aux (E_app (mk_id "append",
+                             [e1;
+                              E_aux (E_app (mk_id "slice_zeros_concat",
+                                            [vector1; start1; length1; length2]),(Unknown,empty_tannot))]),
+                      (Unknown,empty_tannot)))
+       end
     | _ -> E_app (id,args)
 
   else if is_id env (Id "eq_vec") id then
@@ -3875,7 +3912,7 @@ let simplify_size_nexp env quant_kids (Nexp_aux (_,l) as nexp) =
 (* These functions add cast functions across case splits, so that when a
    bitvector size becomes known in sail, the generated Lem code contains a
    function call to change mword 'n to (say) mword ty16, and vice versa. *)
-let make_bitvector_cast_fns env quant_kids src_typ target_typ =
+let make_bitvector_cast_fns cast_name env quant_kids src_typ target_typ =
   let genunk = Generated Unknown in
   let fresh =
     let counter = ref 0 in
@@ -3908,7 +3945,7 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
           P_aux (P_id var,(Generated src_l,src_ann)),
           E_aux
             (E_cast (tar_typ',
-                     E_aux (E_app (Id_aux (Id "bitvector_cast", genunk),
+                     E_aux (E_app (Id_aux (Id cast_name, genunk),
                                    [E_aux (E_id var, (genunk, src_ann))]), (genunk, tar_ann))),
              (genunk, tar_ann))
        | _ ->
@@ -3934,12 +3971,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
        (fun var exp ->
          let exp_ann = mk_tannot env (typ_of exp) (effect_of exp) in
          E_aux (E_let (LB_aux (LB_val (P_aux (P_typ (one_target_typ, P_aux (P_id var,(genunk,tar_ann))),(genunk,tar_ann)),
-                                       E_aux (E_app (Id_aux (Id "bitvector_cast",genunk),
+                                       E_aux (E_app (Id_aux (Id cast_name,genunk),
                                                      [E_aux (E_id var,(genunk,src_ann))]),(genunk,tar_ann))),(genunk,tar_ann)),
                        exp),(genunk,exp_ann))),
       (fun (E_aux (_,(exp_l,exp_ann)) as exp) ->
         E_aux (E_cast (one_target_typ,
-                       E_aux (E_app (Id_aux (Id "bitvector_cast", genunk), [exp]), (Generated exp_l,tar_ann))),
+                       E_aux (E_app (Id_aux (Id cast_name, genunk), [exp]), (Generated exp_l,tar_ann))),
                (Generated exp_l,tar_ann)))
     | _ ->
        (fun var exp ->
@@ -3954,12 +3991,12 @@ let make_bitvector_cast_fns env quant_kids src_typ target_typ =
 
 (* TODO: bound vars *)
 let make_bitvector_env_casts env quant_kids (kid,i) exp =
-  let mk_cast var typ exp = (fst (make_bitvector_cast_fns env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
+  let mk_cast var typ exp = (fst (make_bitvector_cast_fns "bitvector_cast_in" env quant_kids typ (subst_src_typ (KBindings.singleton kid (nconstant i)) typ))) var exp in
   let locals = Env.get_locals env in
   Bindings.fold (fun var (mut,typ) exp ->
     if mut = Immutable then mk_cast var typ exp else exp) locals exp
 
-let make_bitvector_cast_exp env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns env quant_kids typ target_typ)) exp
+let make_bitvector_cast_exp cast_name env quant_kids typ target_typ exp = (snd (make_bitvector_cast_fns cast_name env quant_kids typ target_typ)) exp
 
 let rec extract_value_from_guard var (E_aux (e,_)) =
   match e with
@@ -3986,6 +4023,12 @@ let fill_in_type env typ =
   subst_src_typ subst typ
 
 (* TODO: top-level patterns *)
+(* TODO: proper environment tracking for variables.  Currently we pretend that
+   we can print the type of a variable in the top-level environment, but in
+   practice they might be below a case split.  Note that we'd also need to
+   provide some way for the Lem pretty printer to know what to use; currently
+   we just use two names for the cast, bitvector_cast_in and bitvector_cast_out,
+   to let the pretty printer know whether to use the top-level environment. *)
 let add_bitvector_casts (Defs defs) =
   let rewrite_body id quant_kids top_env ret_typ exp =
     let rewrite_aux (e,ann) =
@@ -4002,13 +4045,13 @@ let add_bitvector_casts (Defs defs) =
              let body = match pat, guard with
                | P_aux (P_lit (L_aux (L_num i,_)),_), _ ->
                   let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in
-                  make_bitvector_cast_exp env quant_kids src_typ result_typ
+                  make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ
                     (make_bitvector_env_casts env quant_kids (kid,i) body)
                | P_aux (P_id var,_), Some guard ->
                   (match extract_value_from_guard var guard with
                   | Some i ->
                      let src_typ = subst_src_typ (KBindings.singleton kid (nconstant i)) result_typ in
-                     make_bitvector_cast_exp env quant_kids src_typ result_typ
+                     make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ
                        (make_bitvector_env_casts env quant_kids (kid,i) body)
                   | None -> body)
                | _ ->
@@ -4019,15 +4062,46 @@ let add_bitvector_casts (Defs defs) =
            E_aux (E_case (exp', List.map map_case cases),ann)
         | _ -> E_aux (e,ann)
       end
+      | E_if (e1,e2,e3) ->
+         let env = env_of_annot ann in
+         let result_typ = Env.base_typ_of env (typ_of_annot ann) in
+         let rec extract (E_aux (e,_)) =
+           match e with
+           | E_app (op,
+                    ([E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_); y] |
+                     [y; E_aux (E_sizeof (Nexp_aux (Nexp_var kid,_)),_)]))
+               when string_of_id op = "eq_atom" ->
+              (match destruct_atom_nexp (env_of y) (typ_of y) with
+              | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)]
+              | _ -> [])
+           | E_app (op, [x;y]) when string_of_id op = "and_bool" ->
+              extract x @ extract y
+           | _ -> []
+         in
+         let insts = extract e1 in
+         let e2' = List.fold_left (fun body inst ->
+           make_bitvector_env_casts env quant_kids inst body) e2 insts in
+         let insts = List.fold_left (fun insts (kid,i) ->
+           KBindings.add kid (nconstant i) insts) KBindings.empty insts in
+         let src_typ = subst_src_typ insts result_typ in
+         let e2' = make_bitvector_cast_exp "bitvector_cast_out" env quant_kids src_typ result_typ e2' in
+         E_aux (E_if (e1,e2',e3), ann)
       | E_return e' ->
-         E_aux (E_return (make_bitvector_cast_exp top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
-      (* TODO: (env_of_annot ann) isn't suitable, because it contains
-         constraints revealing the case splits involved; needs a more
-         subtle approach *)
+         E_aux (E_return (make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e')) ret_typ e'),ann)
       | E_assign (LEXP_aux (lexp,lexp_annot),e') ->
          E_aux (E_assign (LEXP_aux (lexp,lexp_annot),
-                          make_bitvector_cast_exp (env_of_annot ann) quant_kids (fill_in_type (env_of e') (typ_of e'))
+                          make_bitvector_cast_exp "bitvector_cast_out" top_env quant_kids (fill_in_type (env_of e') (typ_of e'))
                             (typ_of_annot lexp_annot) e'),ann)
+      | E_id id -> begin
+        let env = env_of_annot ann in
+        match Env.lookup_id id env with
+        | Local (Mutable, vtyp) ->
+           make_bitvector_cast_exp "bitvector_cast_in" top_env quant_kids
+             (fill_in_type (env_of_annot ann) (typ_of_annot ann))
+             vtyp
+             (E_aux (e,ann))
+        | _ -> E_aux (e,ann)
+      end
       | _ -> E_aux (e,ann)
     in
     let open Rewriter in
@@ -4052,7 +4126,7 @@ let add_bitvector_casts (Defs defs) =
     let body = rewrite_body id quant_kids body_env ret_typ body in
     (* Also add a cast around the entire function clause body, if necessary *)
     let body =
-      make_bitvector_cast_exp fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body
+      make_bitvector_cast_exp "bitvector_cast_out" fcl_env quant_kids (fill_in_type body_env (typ_of body)) ret_typ body
     in
     let pexp = construct_pexp (pat,guard,body,annot) in
     FCL_aux (FCL_Funcl (id,pexp),fcl_ann)
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 3e4dc650..236c4222 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -673,7 +673,7 @@ let ocaml_main spec sail_dir =
     with
     | End_of_file -> close_in chan; lines := List.rev !lines
   end;
-  (("open " ^ String.capitalize_ascii spec ^ ";;\n\n") :: !lines
+  (("open " ^ String.capitalize spec ^ ";;\n\n") :: !lines
    @ [ "  zinitializze_registers ();";
        if !opt_trace_ocaml then "  Sail_lib.opt_trace := true;" else "  ();";
        "  Printexc.record_backtrace true;";
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 713cfb34..d5aa7151 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -58,6 +58,7 @@ open Pretty_print_common
 module StringSet = Set.Make(String)
 
 let opt_undef_axioms = ref false
+let opt_debug_on : string list ref = ref []
 
 (****************************************************************************
  * PPrint-based sail-to-coq pprinter
@@ -69,6 +70,7 @@ type context = {
   kid_id_renames : id KBindings.t; (* tyvar -> argument renames *)
   bound_nexps : NexpSet.t;
   build_ex_return : bool;
+  debug : bool;
 }
 let empty_ctxt = {
   early_ret = false;
@@ -76,8 +78,20 @@ let empty_ctxt = {
   kid_id_renames = KBindings.empty;
   bound_nexps = NexpSet.empty;
   build_ex_return = false;
+  debug = false;
 }
 
+let debug_depth = ref 0
+
+let rec indent n = match n with
+  | 0 -> ""
+  | n -> "|   " ^ indent (n - 1)
+
+let debug ctxt m =
+  if ctxt.debug
+  then print_endline (indent !debug_depth ^ Lazy.force m)
+  else ()
+
 let langlebar = string "<|"
 let ranglebar = string "|>"
 let anglebars = enclose langlebar ranglebar
@@ -91,6 +105,11 @@ let is_number_char c =
   c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
   c = '6' || c = '7' || c = '8' || c = '9'
 
+let is_enum env id =
+  match Env.lookup_id id env with
+  | Enum _ -> true
+  | _ -> false
+
 let rec fix_id remove_tick name = match name with
   | "assert"
   | "lsl"
@@ -138,7 +157,6 @@ let doc_id id = string (string_id id)
 let doc_id_type (Id_aux(i,_)) =
   match i with
   | Id("int") -> string "Z"
-  | Id("nat") -> string "Z"
   | Id i -> string (fix_id false i)
   | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
@@ -296,37 +314,70 @@ let drop_duplicate_atoms kids ty =
     | Typ_app _ -> Some full_typ
   in aux_typ ty
 
-(* TODO: parens *)
-let rec doc_nc_prop ctx (NC_aux (nc,_)) =
+(* Follows Coq precedence levels *)
+let rec doc_nc_prop ctx nc =
+  let rec l85 (NC_aux (nc,_) as nc_full) =
+  match nc with
+  | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
+  | _ -> l80 nc_full
+  and l80 (NC_aux (nc,_) as nc_full) =
+  match nc with
+  | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
+  | _ -> l70 nc_full
+  and l70 (NC_aux (nc,_) as nc_full) =
   match nc with
   | NC_equal (ne1, ne2) -> doc_op equals (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_bounded_le (ne1, ne2) -> doc_op (string "<=") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
   | NC_not_equal (ne1, ne2) -> doc_op (string "<>") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_set (kid, is) -> (* TODO: is this a good translation? *)
+  | _ -> l10 nc_full
+  and l10 (NC_aux (nc,_) as nc_full) =
+  match nc with
+  | NC_set (kid, is) ->
      separate space [string "In"; doc_var_lem ctx kid;
                      brackets (separate (string "; ")
                                  (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
-  | NC_or (nc1, nc2) -> doc_op (string "\\/") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
-  | NC_and (nc1, nc2) -> doc_op (string "/\\") (doc_nc_prop ctx nc1) (doc_nc_prop ctx nc2)
   | NC_true -> string "True"
   | NC_false -> string "False"
-
-(* TODO: parens *)
-let rec doc_nc_exp ctx (NC_aux (nc,_)) =
-  match nc with
-  | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
-  | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2))
-  | NC_set (kid, is) -> (* TODO: is this a good translation? *)
-     separate space [string "member_Z_list"; doc_var_lem ctx kid;
-                     brackets (separate (string "; ")
-                                 (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
-  | NC_or (nc1, nc2) -> doc_op (string "||") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2)
-  | NC_and (nc1, nc2) -> doc_op (string "&&") (doc_nc_exp ctx nc1) (doc_nc_exp ctx nc2)
-  | NC_true -> string "true"
-  | NC_false -> string "false"
+  | NC_or _
+  | NC_and _
+  | NC_equal _
+  | NC_bounded_ge _
+  | NC_bounded_le _
+  | NC_not_equal _ -> parens (l85 nc_full)
+  in l85 nc
+
+(* Follows Coq precedence levels *)
+let doc_nc_exp ctx nc =
+  let rec l70 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_equal (ne1, ne2) -> doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+    | NC_bounded_ge (ne1, ne2) -> doc_op (string ">=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+    | NC_bounded_le (ne1, ne2) -> doc_op (string "<=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2)
+    | _ -> l50 nc_full
+  and l50 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_or (nc1, nc2) -> doc_op (string "||") (l50 nc1) (l40 nc2)
+    | _ -> l40 nc_full
+  and l40 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_and (nc1, nc2) -> doc_op (string "&&") (l40 nc1) (l10 nc2)
+    | _ -> l10 nc_full
+  and l10 (NC_aux (nc,_) as nc_full) =
+    match nc with
+    | NC_not_equal (ne1, ne2) -> string "negb" ^^ space ^^ parens (doc_op (string "=?") (doc_nexp ctx ne1) (doc_nexp ctx ne2))
+    | NC_set (kid, is) ->
+       separate space [string "member_Z_list"; doc_var_lem ctx kid;
+                       brackets (separate (string "; ")
+                                   (List.map (fun i -> string (Nat_big_num.to_string i)) is))]
+    | NC_true -> string "true"
+    | NC_false -> string "false"
+    | NC_equal _
+    | NC_bounded_ge _
+    | NC_bounded_le _
+    | NC_or _
+    | NC_and _ -> parens (l70 nc_full)
+  in l70 nc
 
 let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
   match typ with
@@ -337,6 +388,11 @@ let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) =
      let var = nvar kid in
      let nc = nc_and (nc_lteq low var) (nc_lteq var high) in
      Some (Typ_aux (Typ_exist ([kid], nc, atom_typ var),Parse_ast.Generated l))
+  | Typ_id (Id_aux (Id "nat",_)) ->
+     let kid = mk_kid "n" in
+     let var = nvar kid in
+     Some (Typ_aux (Typ_exist ([kid], nc_gteq var (nconstant Nat_big_num.zero), atom_typ var),
+                    Generated l))
   | _ -> None
 
 let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ)
@@ -381,7 +437,8 @@ let doc_typ, doc_atomic_typ =
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
          let tpp = string "register_ref regstate register_value " ^^ typ etyp in
          if atyp_needed then parens tpp else tpp
-      | Typ_app(Id_aux (Id "range", _), _) ->
+      | Typ_app(Id_aux (Id "range", _), _)
+      | Typ_id (Id_aux (Id "nat", _)) ->
          (match maybe_expand_range_type ty with
          | Some typ -> atomic_typ atyp_needed typ
          | None -> raise (Reporting_basic.err_unreachable l "Bad range type"))
@@ -758,17 +815,27 @@ let replace_atom_return_type ret_typ =
   | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) ->
      let kid = mk_kid "_retval" in (* TODO: collision avoidance *)
      true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l)
-  | Typ_aux (Typ_id (Id_aux (Id "nat",_)),l) ->
-     let kid = mk_kid "_retval" in
-     true, Typ_aux (Typ_exist ([kid], nc_gteq (nvar kid) (nconstant Nat_big_num.zero), atom_typ (nvar kid)),Generated l)
   | _ -> false, ret_typ
 
+let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) =
+  match argty, fnty with
+  | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),
+    Typ_app(Id_aux (Id "range", _), [Typ_arg_aux(Typ_arg_nexp low,_);
+                                     Typ_arg_aux(Typ_arg_nexp high,_)]) ->
+     Type_check.prove env (nc_and (nc_eq nexp low) (nc_eq nexp high))
+  | _ -> false
 
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
   let rec top_exp (ctxt : context) (aexp_needed : bool)
     (E_aux (e, (l,annot)) as full_exp) =
+    let top_exp c a e = 
+      let () = debug_depth := !debug_depth + 1 in
+      let r = top_exp c a e in
+      let () = debug_depth := !debug_depth - 1 in
+      r
+    in
     let expY = top_exp ctxt true in
     let expN = top_exp ctxt false in
     let expV = top_exp ctxt in
@@ -984,6 +1051,7 @@ let doc_exp_lem, doc_let_lem =
                    parens (separate_map comma (expV false) args) in
             if aexp_needed then parens (align epp) else epp
           else
+            let () = debug ctxt (lazy ("Function application " ^ string_of_id f)) in
             let call, is_extern =
               if Env.is_extern f env "coq"
               then string (Env.get_extern f env "coq"), true
@@ -996,33 +1064,44 @@ let doc_exp_lem, doc_let_lem =
                  | _ -> [arg_typ], ret_typ, eff)
               | _ -> raise (Reporting_basic.err_unreachable l "Function not a function type")
             in
+            let inst =
+              match instantiation_of_without_type full_exp with
+              | x -> x
+              (* Not all function applications can be inferred, so try falling back to the
+                 type inferred when we know the target type.
+                 TODO: there are probably some edge cases where this won't pick up a need
+                 to cast. *)
+              | exception _ -> instantiation_of full_exp
+            in
+            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
+
             (* Insert existential unpacking of arguments where necessary *)
             let doc_arg arg typ_from_fn =
               let arg_pp = expY arg in
-              let arg_ty = expand_range_type (Env.expand_synonyms (env_of arg) (typ_of arg)) in
-              let typ_from_fn = expand_range_type (Env.expand_synonyms (env_of arg) typ_from_fn) in
+              let arg_ty_plain = Env.expand_synonyms (env_of arg) (typ_of arg) in
+              let arg_ty = expand_range_type arg_ty_plain in
+              let typ_from_fn_plain = subst_unifiers inst typ_from_fn in
+              let typ_from_fn_plain = Env.expand_synonyms (env_of arg) typ_from_fn_plain in
+              let typ_from_fn = expand_range_type typ_from_fn_plain in
               (* TODO: more sophisticated check *)
+              let () =
+                debug ctxt (lazy (" arg type found    " ^ string_of_typ arg_ty_plain));
+                debug ctxt (lazy (" arg type expected " ^ string_of_typ typ_from_fn_plain))
+              in
               match destruct_exist env arg_ty, destruct_exist env typ_from_fn with
               | Some _, None -> parens (string "projT1 " ^^ arg_pp)
               (* Usually existentials have already been built elsewhere, but this
                  is useful for (e.g.) ranges *)
               | None, Some _ -> parens (string "build_ex " ^^ arg_pp)
+              | Some _, Some _ when is_range_from_atom (env_of arg) arg_ty_plain typ_from_fn_plain ->
+                 parens (string "to_range " ^^ parens (string "projT1 " ^^ arg_pp))
               | _, _ -> arg_pp
             in
             let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in
+
             (* Decide whether to unpack an existential result, pack one, or cast.
                To do this we compare the expected type stored in the checked expression
                with the inferred type. *)
-            let inst =
-              match instantiation_of_without_type full_exp with
-              | x -> x
-              (* Not all function applications can be inferred, so try falling back to the
-                 type inferred when we know the target type.
-                 TODO: there are probably some edge cases where this won't pick up a need
-                 to cast. *)
-              | exception _ -> instantiation_of full_exp
-            in
-            let inst = KBindings.fold (fun k u m -> KBindings.add (orig_kid k) u m) inst KBindings.empty in
             let ret_typ_inst =
                  subst_unifiers inst ret_typ
             in
@@ -1033,6 +1112,10 @@ let doc_exp_lem, doc_let_lem =
               let ret_typ_inst =
                 if is_no_Z_proof_fn env f then ret_typ_inst
                 else snd (replace_atom_return_type ret_typ_inst) in
+              let () = 
+                debug ctxt (lazy (" type returned " ^ string_of_typ ret_typ_inst));
+                debug ctxt (lazy (" type expected " ^ string_of_typ ann_typ))
+              in
               let unpack, build_ex, in_typ, out_typ =
                 match ret_typ_inst, ann_typ with
                 | Typ_aux (Typ_exist (_,_,t1),_), Typ_aux (Typ_exist (_,_,t2),_) ->
@@ -1053,10 +1136,13 @@ let doc_exp_lem, doc_let_lem =
                 | _ -> false
               in unpack,build_ex,autocast
             in
-            let autocast_id = if effectful eff then "autocast_m" else "autocast" in
-            let epp = if unpack then string "projT1" ^^ space ^^ parens epp else epp in
+            let autocast_id, proj_id, build_id =
+              if effectful eff
+              then "autocast_m", "projT1_m", "build_ex_m"
+              else "autocast",   "projT1",   "build_ex" in
+            let epp = if unpack then string proj_id ^^ space ^^ parens epp else epp in
             let epp = if autocast then string autocast_id ^^ space ^^ parens epp else epp in
-            let epp = if build_ex then string "build_ex" ^^ space ^^ parens epp else epp in
+            let epp = if build_ex then string build_id ^^ space ^^ parens epp else epp in
             liftR (if aexp_needed then parens (align epp) else epp)
        end
     | E_vector_access (v,e) ->
@@ -1231,12 +1317,16 @@ let doc_exp_lem, doc_let_lem =
             let epp =
               let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in
               let middle =
-                match fst (untyp_pat pat) with
+                match pat with
                 | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) ->
                    string ">>"
-                | P_aux (P_id id,_) ->
+                | P_aux (P_id id,_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) (typ_of e1)) &&
+                        not (is_enum (env_of e1) id) ->
                    separate space [string ">>= fun"; doc_id id; bigarrow]
-                | P_aux (P_typ (typ, P_aux (P_id id,_)),_) ->
+                | P_aux (P_typ (typ, P_aux (P_id id,_)),_)
+                   when Util.is_none (is_auto_decomposed_exist (env_of e1) typ) &&
+                        not (is_enum (env_of e1) id) ->
                    separate space [string ">>= fun"; doc_id id; colon; doc_typ ctxt typ; bigarrow]
                 | _ ->
                    separate space [string ">>= fun"; squote ^^ doc_pat ctxt true (pat, typ_of e1); bigarrow]
@@ -1290,12 +1380,14 @@ let doc_exp_lem, doc_let_lem =
     (* Prefer simple lets over patterns, because I've found Coq can struggle to
        work out return types otherwise *)
     | LB_val(P_aux (P_id id,_),e)
-      when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) ->
+      when Util.is_none (is_auto_decomposed_exist (env_of e) (typ_of e)) &&
+           not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; coloneq])
               (top_exp ctxt false e)
     | LB_val(P_aux (P_typ (typ,P_aux (P_id id,_)),_),e)
-      when Util.is_none (is_auto_decomposed_exist (env_of e) typ) ->
+      when Util.is_none (is_auto_decomposed_exist (env_of e) typ) &&
+           not (is_enum (env_of e) id) ->
        prefix 2 1
               (separate space [string "let"; doc_id id; colon; doc_typ ctxt typ; coloneq])
               (top_exp ctxt false e)
@@ -1535,10 +1627,6 @@ let rec atom_constraint ctxt (pat, typ) =
      | _ ->
         Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
                                   parens (doc_op equals (doc_id id) (doc_nexp ctxt nexp)))))
-  | P_aux (P_id id, _),
-        Typ_aux (Typ_id (Id_aux (Id "nat",_)),_) ->
-     Some (bquote ^^ braces (string "ArithFact" ^^ space ^^
-                                  parens (doc_op (string ">=") (doc_id id) (string "0"))))
   | P_aux (P_typ (_,p),_), _ -> atom_constraint ctxt (p, typ)
   | _ -> None
 
@@ -1639,6 +1727,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
       kid_id_renames = kid_to_arg_rename;
       bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ);
       build_ex_return = effectful eff && build_ex;
+      debug = List.mem (string_of_id id) (!opt_debug_on)
     } in
   (* Put the constraints after pattern matching so that any type variable that's
      been replaced by one of the term-level arguments is bound. *)
@@ -1650,7 +1739,9 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
     let exp_typ = Env.expand_synonyms env typ in
     match p with
     | P_id id
-    | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) ->
+    | P_typ (_,P_aux (P_id id,_))
+         when Util.is_none (is_auto_decomposed_exist env exp_typ) &&
+              not (is_enum env id) ->
        parens (separate space [doc_id id; colon; doc_typ ctxt typ])
     | _ ->
        (used_a_pattern := true;
@@ -1849,6 +1940,7 @@ let doc_val pat exp =
   in
   let env = env_of exp in
   let typ = expand_range_type (Env.expand_synonyms env (typ_of exp)) in
+  let ctxt = { empty_ctxt with debug  = List.mem (string_of_id id) (!opt_debug_on) } in
   let id, opt_unpack =
     match destruct_exist env typ with
     | None -> id, None
@@ -1863,7 +1955,7 @@ let doc_val pat exp =
   let idpp = doc_id id in
   let basepp =
     group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^
-             doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline
+             doc_exp_lem ctxt false exp ^^ dot) ^^ hardline
   in
   match opt_unpack with
   | None -> basepp ^^ hardline
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 75284418..d300f699 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -65,8 +65,9 @@ let opt_mwords = ref false
 type context = {
   early_ret : bool;
   bound_nexps : NexpSet.t;
+  top_env : Env.t
 }
-let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty }
+let empty_ctxt = { early_ret = false; bound_nexps = NexpSet.empty; top_env = Env.empty }
 
 let print_to_from_interp_value = ref false
 let langlebar = string "<|"
@@ -128,7 +129,7 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
   | Id("nat") -> string "integer"
   | Id("Some") -> string "Just"
   | Id("None") -> string "Nothing"
-  | Id i -> string (fix_id false (String.capitalize_ascii i))
+  | Id i -> string (fix_id false (String.capitalize i))
   | DeIid x -> string (Util.zencode_string ("op " ^ x))
 
 let deinfix = function
@@ -328,10 +329,9 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_arg_order o -> empty
   in typ', atomic_typ
 
-(* Check for variables in types that would be pretty-printed and are not
-   bound in the val spec of the function. *)
+(* Check for variables in types that would be pretty-printed. *)
 let contains_t_pp_var ctxt (Typ_aux (t,a) as typ) =
-  NexpSet.diff (lem_nexps_of_typ typ) ctxt.bound_nexps
+  lem_nexps_of_typ typ
   |> NexpSet.exists (fun nexp -> not (is_nexp_constant nexp))
 
 let replace_typ_size ctxt env (Typ_aux (t,a)) =
@@ -341,29 +341,32 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp = 
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       let is_equal nexp =
-         prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
-       in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
-       | nexp -> mk_typ nexp
-       | exception Not_found ->
-          match Type_check.solve env size with
-          | Some n -> mk_typ (nconstant n)
-          | None -> None
+       match Type_check.solve env size with
+       | Some n -> mk_typ (nconstant n)
+       | None ->
+          let is_equal nexp =
+            prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+          in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+          | nexp -> mk_typ nexp
+          | exception Not_found -> None
      end
   | _ -> None
 
-let doc_tannot_lem ctxt env eff typ =
-  let of_typ typ =
-    let ta = doc_typ_lem typ in
-    if eff then string " : M " ^^ parens ta
-    else string " : " ^^ ta
-  in
+let make_printable_type ctxt env typ =
   if contains_t_pp_var ctxt typ
   then
     match replace_typ_size ctxt env typ with
-    | None -> empty
-    | Some typ -> of_typ typ
-  else of_typ typ
+    | None -> None
+    | Some typ -> Some typ
+  else Some typ
+
+let doc_tannot_lem ctxt env eff typ =
+  match make_printable_type ctxt env typ with
+  | None -> empty
+  | Some typ ->
+     let ta = doc_typ_lem typ in
+     if eff then string " : M " ^^ parens ta
+     else string " : " ^^ ta
 
 let doc_lit_lem (L_aux(lit,l)) =
   match lit with
@@ -495,8 +498,9 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
      parens (separate comma_sp (List.map2 doc_elem typs pats))
   | P_typ(typ,p) ->
     let doc_p = doc_pat_lem ctxt true p in
-    if contains_t_pp_var ctxt typ then doc_p
-    else parens (doc_op colon doc_p (doc_typ_lem typ))
+    (match make_printable_type ctxt (env_of_annot (l,annot)) typ with
+    | None -> doc_p
+    | Some typ -> parens (doc_op colon doc_p (doc_typ_lem typ)))
   | P_vector pats ->
      let ppp = brackets (separate_map semi (doc_pat_lem ctxt true) pats) in
      if apat_needed then parens ppp else ppp
@@ -727,14 +731,16 @@ let doc_exp_lem, doc_let_lem =
             | [exp] ->
                let epp = separate space [string "early_return"; expY exp] in
                let aexp_needed, tepp =
-                 if contains_t_pp_var ctxt (typ_of exp) ||
-                    contains_t_pp_var ctxt (typ_of full_exp) then
-                   aexp_needed, epp
-                 else
-                   let tannot = separate space [string "MR";
-                     doc_atomic_typ_lem false (typ_of full_exp);
-                     doc_atomic_typ_lem false (typ_of exp)] in
-                   true, doc_op colon epp tannot in
+                 match Util.option_bind (make_printable_type ctxt ctxt.top_env)
+                                        (Env.get_ret_typ (env_of exp)),
+                       make_printable_type ctxt (env_of full_exp) (typ_of full_exp) with
+                   | Some typ, Some full_typ ->
+                     let tannot = separate space [string "MR";
+                       doc_atomic_typ_lem false full_typ;
+                       doc_atomic_typ_lem false typ] in
+                     true, doc_op colon epp tannot
+                   | _ -> aexp_needed, epp
+               in
                if aexp_needed then parens tepp else tepp
             | _ -> raise (Reporting_basic.err_unreachable l
                "Unexpected number of arguments for early_return builtin")
@@ -760,8 +766,12 @@ let doc_exp_lem, doc_let_lem =
                let env = env_of full_exp in
                let t = Env.expand_synonyms env (typ_of full_exp) in
                let eff = effect_of full_exp in
-               if typ_needs_printed t
-               then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true)
+               if typ_needs_printed t then
+                 if Id.compare f (mk_id "bitvector_cast_out") <> 0
+                 then (align (group (prefix 0 1 epp (doc_tannot_lem ctxt env (effectful eff) t))), true)
+                 (* TODO: coordinate with the code in monomorphise.ml to find the correct
+                    typing environment to use *)
+                 else (align (group (prefix 0 1 epp (doc_tannot_lem ctxt ctxt.top_env (effectful eff) t))), true)
                else (epp, aexp_needed) in
              liftR (if aexp_needed then parens (align taepp) else taepp)
           end
@@ -916,12 +926,15 @@ let doc_exp_lem, doc_let_lem =
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
     | E_return r ->
       let ta =
-        if contains_t_pp_var ctxt (typ_of full_exp) || contains_t_pp_var ctxt (typ_of r)
-        then empty
-        else separate space
-          [string ": MR";
-          parens (doc_typ_lem (typ_of full_exp));
-          parens (doc_typ_lem (typ_of r))] in
+        match Util.option_bind (make_printable_type ctxt ctxt.top_env) (Env.get_ret_typ (env_of full_exp)),
+              make_printable_type ctxt (env_of r) (typ_of r) with
+       | Some full_typ, Some r_typ ->
+          separate space
+            [string ": MR";
+            parens (doc_typ_lem full_typ);
+            parens (doc_typ_lem r_typ)]
+       | _ -> empty
+      in
       align (parens (string "early_return" ^//^ expV true r ^//^ ta))
     | E_constraint _ -> string "true"
     | E_internal_value _ ->
@@ -1255,7 +1268,8 @@ let doc_funcl_lem (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
   let ctxt =
     { early_ret = contains_early_return exp;
-      bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ) } in
+      bound_nexps = NexpSet.union (lem_nexps_of_typ typ) (typeclass_nexps typ);
+      top_env = env_of_annot annot } in
   let pats, bind = untuple_args_pat pat in
   let patspp = separate_map space (doc_pat_lem ctxt true) pats in
   let _ = match guard with
diff --git a/src/process_file.ml b/src/process_file.ml
index 5fdd3d24..96029587 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -271,14 +271,14 @@ let output_lem filename libs defs =
       operators_module
     ] @ monad_modules
   in
-  let isa_thy_name = String.capitalize_ascii filename ^ "_lemmas" in
+  let isa_thy_name = String.capitalize filename ^ "_lemmas" in
   let isa_lemmas =
     separate hardline [
       string ("theory " ^ isa_thy_name);
       string  "  imports";
       string  "    Sail.Sail2_values_lemmas";
       string  "    Sail.Sail2_state_lemmas";
-      string ("    " ^ String.capitalize_ascii filename);
+      string ("    " ^ String.capitalize filename);
       string  "begin";
       string  "";
       State.generate_isa_lemmas !Pretty_print_lem.opt_mwords defs;
@@ -292,7 +292,7 @@ let output_lem filename libs defs =
     open_output_with_check_unformatted (filename ^ ".lem") in
   (Pretty_print.pp_defs_lem
      (ot, base_imports)
-     (o, base_imports @ (String.capitalize_ascii types_module :: libs))
+     (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_o;
@@ -309,6 +309,7 @@ let output_coq filename libs defs =
   let base_imports = [
       "Sail2_instr_kinds";
       "Sail2_values";
+      "Sail2_string";
       operators_module
     ] @ monad_modules
   in
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 01ff62b1..6d88730d 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -266,7 +266,7 @@ let vector_string_to_bit_list l lit =
     | _ -> raise (Reporting_basic.err_unreachable l "hexchar_to_binlist given unrecognized character") in
 
   let s_bin = match lit with
-    | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase_ascii s_hex)))
+    | L_hex s_hex -> List.flatten (List.map hexchar_to_binlist (explode (String.uppercase s_hex)))
     | L_bin s_bin -> explode s_bin
     | _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in
 
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 3e582071..da4702b5 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -74,6 +74,8 @@ val rewrite_lexp : tannot rewriters -> tannot lexp -> tannot lexp
 
 val rewrite_pat : tannot rewriters -> tannot pat -> tannot pat
 
+val rewrite_pexp : tannot rewriters -> tannot pexp -> tannot pexp
+
 val rewrite_let : tannot rewriters -> tannot letbind -> tannot letbind
 
 val rewrite_def : tannot rewriters -> tannot def -> tannot def
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5ed174ea..47c7e923 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1084,9 +1084,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
   | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2
   | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) ->
     if id1 = id2 then Some []
-    else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound &&
-            Env.lookup_id aid2 (env_of_annot annot2) = Unbound
-           then Some [(id2,id1)] else None
+    else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound
+    then if Env.lookup_id aid2 (env_of_annot annot2) = Unbound
+      then Some [(id2,id1)]
+      else Some []
+    else None
   | P_id id1, _ ->
     if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None
   | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2
@@ -4043,7 +4045,18 @@ let rewrite_defs_realise_mappings (Defs defs) =
 
 
 (* Rewrite to make all pattern matches in Coq output exhaustive.
-   Assumes that guards, vector patterns, etc have been rewritten already. *)
+   Assumes that guards, vector patterns, etc have been rewritten already,
+   and the scattered functions have been merged.
+   Will add escape effect where a default is needed, so effects will
+   need recalculated afterwards.
+
+   Also detects and removes redundant wildcard patterns at the end of the match.
+   (We could do more, but this is sufficient to deal with the code generated by
+   the mappings rewrites.)
+
+   Note: if this naive implementation turns out to be too slow or buggy, we
+   could look at implementing Maranget JFP 17(3), 2007.
+ *)
 
 let opt_coq_warn_nonexhaustive = ref false
 
@@ -4261,12 +4274,38 @@ let process_pexp env =
      raise (Reporting_basic.err_unreachable l
               "Guarded pattern should have been rewritten away")
 
+(* We do some minimal redundancy checking to remove bogus wildcard patterns here *)
+let check_cases process is_wild loc_of cases =
+  let rec aux rps acc = function
+    | [] -> acc, rps
+    | [p] when is_wild p && match rps with [] -> true | _ -> false ->
+      let () = Reporting_basic.print_err false false
+        (loc_of p) "Match checking" "Redundant wildcard clause" in
+      acc, []
+    | h::t -> aux (process rps h) (h::acc) t
+  in
+  let cases, rps = aux [RP_any] [] cases in
+  List.rev cases, rps
+
+let pexp_is_wild = function
+  | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true
+  | _ -> false
+
+let pexp_loc = function
+  | (Pat_aux (Pat_exp (P_aux (_,(l,_)),_),_)) -> l
+  | (Pat_aux (Pat_when (P_aux (_,(l,_)),_,_),_)) -> l
+
+let funcl_is_wild = function
+  | (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp_is_wild pexp
+
+let funcl_loc (FCL_aux (_,(l,_))) = l
+
 let rewrite_case (e,ann) =
   match e with
   | E_case (e1,cases) ->
      begin
      let env = env_of_annot ann in
-     let rps = List.fold_left (process_pexp env) [RP_any] cases in
+     let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in
      match rps with
      | [] -> E_aux (E_case (e1,cases),ann)
      | (example::_) ->
@@ -4285,6 +4324,37 @@ let rewrite_case (e,ann) =
      end
   | _ -> E_aux (e,ann)
 
+let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
+  let id,fcl_ann =
+    match fcls with
+    | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann
+    | [] -> raise (Reporting_basic.err_unreachable (fst f_ann)
+                 "Empty function")
+  in
+  let env = env_of_annot fcl_ann in
+  let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in
+  let fcls, rps = check_cases process_funcl funcl_is_wild funcl_loc fcls in
+  let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) ->
+                                  FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann))
+                fcls in
+  match rps with
+  | [] -> FD_aux (FD_function (r,t,e,fcls'),f_ann)
+  | (example::_) ->
+     let _ =
+       if !opt_coq_warn_nonexhaustive
+       then Reporting_basic.print_err false false
+              (fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
+
+     let l = Parse_ast.Generated Parse_ast.Unknown in
+     let p = P_aux (P_wild, (l, empty_tannot)) in
+     let ann' = mk_tannot env (typ_of_annot fcl_ann) (mk_effect [BE_escape]) in
+     (* TODO: use an expression that specifically indicates a failed pattern match *)
+     let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in
+     let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in
+
+     FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann)
+  
+
 let rewrite =
   let alg = { id_exp_alg with e_aux = rewrite_case } in
   rewrite_defs_base
@@ -4381,6 +4451,8 @@ let rewrite_defs_lem = [
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
   ("fix_val_specs", rewrite_fix_val_specs);
+  (* early_return currently breaks the types *)
+  ("recheck_defs", recheck_defs);
   ("remove_blocks", rewrite_defs_remove_blocks);
   ("letbind_effects", rewrite_defs_letbind_effects);
   ("remove_e_assign", rewrite_defs_remove_e_assign);
diff --git a/src/sail.ml b/src/sail.ml
index e698090e..0b56ab21 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -146,6 +146,9 @@ let options = Arg.align ([
   ( "-dcoq_warn_nonex",
     Arg.Set Rewrites.opt_coq_warn_nonexhaustive,
     "Generate warnings for non-exhaustive pattern matches in the Coq backend");
+  ( "-dcoq_debug_on",
+    Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f::!Pretty_print_coq.opt_debug_on),
+    "<function> Produce debug messages for Coq output on given function");
   ( "-latex_prefix",
     Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix),
     " set a custom prefix for generated latex command (default sail)");