Begin refactoring Sail library

- Add back support for bit list representation of bit vectors, for backwards
  compatibility in order to ease integration with the interpreter.  For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors.  Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.

- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
  library.  The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.

- Add early return support to the free monad, using a new constructor "Return
  of 'r".  As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.

1 files changed, 230 insertions, 195 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2971081e..7671c26b 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -148,44 +148,47 @@ let doc_nexp_lem (Nexp_aux (nexp, l) as full_nexp) = match nexp with
 
 let doc_typ_lem, doc_atomic_typ_lem =
   (* following the structure of parser for precedence *)
-  let rec typ regtypes ty = fn_typ regtypes true ty
-    and typ' regtypes ty = fn_typ regtypes false ty
-    and fn_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+  let rec typ sequential mwords ty = fn_typ sequential mwords true ty
+    and typ' sequential mwords ty = fn_typ sequential mwords false ty
+    and fn_typ (sequential : bool) (mwords : bool) atyp_needed ((Typ_aux (t, _)) as ty) = match t with
       | Typ_fn(arg,ret,efct) ->
          (*let exc_typ = string "string" in*)
          let ret_typ =
            if effectful efct
-           then separate space [string "M";(*parens exc_typ;*) fn_typ regtypes true ret]
-           else separate space [fn_typ regtypes false ret] in
-         let tpp = separate space [tup_typ regtypes true arg; arrow;ret_typ] in
+           then separate space [string "M";(*parens exc_typ;*) fn_typ sequential mwords true ret]
+           else separate space [fn_typ sequential mwords false ret] in
+         let tpp = separate space [tup_typ sequential mwords true arg; arrow;ret_typ] in
          (* once we have proper excetions we need to know what the exceptions type is *)
          if atyp_needed then parens tpp else tpp
-      | _ -> tup_typ regtypes atyp_needed ty
-    and tup_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+      | _ -> tup_typ sequential mwords atyp_needed ty
+    and tup_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
       | Typ_tup typs ->
-         let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in
+         let tpp = separate_map (space ^^ star ^^ space) (app_typ sequential mwords false) typs in
          if atyp_needed then parens tpp else tpp
-      | _ -> app_typ regtypes atyp_needed ty
-    and app_typ regtypes atyp_needed ((Typ_aux (t, l)) as ty) = match t with
+      | _ -> app_typ sequential mwords atyp_needed ty
+    and app_typ sequential mwords atyp_needed ((Typ_aux (t, l)) as ty) = match t with
       | Typ_app(Id_aux (Id "vector", _), [
           Typ_arg_aux (Typ_arg_nexp n, _);
           Typ_arg_aux (Typ_arg_nexp m, _);
           Typ_arg_aux (Typ_arg_order ord, _);
           Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
          let tpp = match elem_typ with
-           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
+           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) when mwords ->
              string "bitvector " ^^ doc_nexp_lem (simplify_nexp m)
              (* (match simplify_nexp m with
                | (Nexp_aux(Nexp_constant i,_)) -> string "bitvector ty" ^^ doc_int i
                | (Nexp_aux(Nexp_var _, _)) -> separate space [string "bitvector"; doc_nexp m]
                | _ -> raise (Reporting_basic.err_unreachable l
                  "cannot pretty-print bitvector type with non-constant length")) *)
-           | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in
+           | _ -> string "vector" ^^ space ^^ typ sequential mwords elem_typ in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
          (* TODO: Better distinguish register names and contents? *)
          (* fn_typ regtypes atyp_needed etyp *)
-         let tpp = (string "register_ref regstate " ^^ typ regtypes etyp) in
+         let tpp =
+           if sequential
+           then string "register_ref regstate " ^^ typ sequential mwords etyp
+           else string "register" in
          if atyp_needed then parens tpp else tpp
       | Typ_app(Id_aux (Id "range", _),_) ->
          (string "integer")
@@ -194,10 +197,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
          (string "integer")
       | Typ_app(id,args) ->
-         let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in
+         let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem sequential mwords) args) in
          if atyp_needed then parens tpp else tpp
-      | _ -> atomic_typ regtypes atyp_needed ty
-    and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with
+      | _ -> atomic_typ sequential mwords atyp_needed ty
+    and atomic_typ sequential mwords atyp_needed ((Typ_aux (t, _)) as ty) = match t with
       | Typ_id (Id_aux (Id "bool",_)) -> string "bool"
       | Typ_id (Id_aux (Id "boolean",_)) -> string "bool"
       | Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
@@ -210,10 +213,10 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_app _ | Typ_tup _ | Typ_fn _ ->
          (* exhaustiveness matters here to avoid infinite loops
           * if we add a new Typ constructor *)
-         let tpp = typ regtypes ty in
+         let tpp = typ sequential mwords ty in
          if atyp_needed then parens tpp else tpp
-    and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with
-      | Typ_arg_typ t -> app_typ regtypes true t
+    and doc_typ_arg_lem sequential mwords (Typ_arg_aux(t,_)) = match t with
+      | Typ_arg_typ t -> app_typ sequential mwords true t
       | Typ_arg_nexp n -> doc_nexp_lem (simplify_nexp n)
       | Typ_arg_order o -> empty
   in typ', atomic_typ
@@ -240,17 +243,17 @@ and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
   | Typ_arg_nexp nexp -> not (is_nexp_constant (simplify_nexp nexp))
   | _ -> false
 
-let doc_tannot_lem regtypes eff typ =
+let doc_tannot_lem sequential mwords eff typ =
   (* if contains_t_pp_var typ then empty
   else *)
-    let ta = doc_typ_lem regtypes typ in
+    let ta = doc_typ_lem sequential mwords typ in
     if eff then string " : _M " ^^ parens ta
     else string " : " ^^ ta
 
 (* doc_lit_lem gets as an additional parameter the type information from the
  * expression around it: that's a hack, but how else can we distinguish between
  * undefined values of different types ? *)
-let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a =
+let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
   match lit with
   | L_unit  -> utf8string "()"
   | L_zero  -> utf8string "B0"
@@ -275,7 +278,7 @@ let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a =
           | _ ->
             parens
               ((utf8string "(failwith \"undefined value of unsupported type\")") ^^
-              (doc_tannot_lem regtypes false typ)))
+              (doc_tannot_lem sequential mwords false typ)))
        | _ -> utf8string "(failwith \"undefined value of unsupported type\")")
   | L_string s -> utf8string ("\"" ^ s ^ "\"")
   | L_real s -> utf8string s (* TODO What's the Lem syntax for reals? *)
@@ -295,9 +298,9 @@ let doc_typquant_lem (TypQ_aux(tq,_)) typ = match tq with
   string "forall " ^^ separate_map space doc_quant_item qs ^^ string ". " ^^ typ
 | _ -> empty
 
-let doc_typschm_lem regtypes quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  if quants then (doc_typquant_lem tq (doc_typ_lem regtypes t))
-  else doc_typ_lem regtypes t
+let doc_typschm_lem sequential mwords quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  if quants then (doc_typquant_lem tq (doc_typ_lem sequential mwords t))
+  else doc_typ_lem sequential mwords t
 
 let is_ctor env id = match Env.lookup_id id env with
 | Enum _ | Union _ -> true
@@ -306,37 +309,37 @@ let is_ctor env id = match Env.lookup_id id env with
 (*Note: vector concatenation, literal vectors, indexed vectors, and record should
   be removed prior to pp. The latter two have never yet been seen
 *)
-let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+let rec doc_pat_lem sequential mwords apat_needed (P_aux (p,(l,annot)) as pa) = match p with
   | P_app(id, ((_ :: _) as pats)) ->
     let ppp = doc_unop (doc_id_lem_ctor id)
-                       (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in
+                       (parens (separate_map comma (doc_pat_lem sequential mwords true) pats)) in
     if apat_needed then parens ppp else ppp
   | P_app(id,[]) -> doc_id_lem_ctor id
-  | P_lit lit  -> doc_lit_lem regtypes true lit annot
+  | P_lit lit  -> doc_lit_lem sequential mwords true lit annot
   | P_wild -> underscore
   | P_id id ->
      begin match id with
      | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
      | _ -> doc_id_lem id end
-  | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id])
+  | P_as(p,id) -> parens (separate space [doc_pat_lem sequential mwords true p; string "as"; doc_id_lem id])
   | P_typ(typ,p) ->
-    let doc_p = doc_pat_lem regtypes true p in
+    let doc_p = doc_pat_lem sequential mwords true p in
     if contains_t_pp_var typ then doc_p
-    else parens (doc_op colon doc_p (doc_typ_lem regtypes typ))
+    else parens (doc_op colon doc_p (doc_typ_lem sequential mwords typ))
   | P_vector pats ->
      let ppp =
        (separate space)
-         [string "Vector";brackets (separate_map semi (doc_pat_lem regtypes true) pats);underscore;underscore] in
+         [string "Vector";brackets (separate_map semi (doc_pat_lem sequential mwords true) pats);underscore;underscore] in
      if apat_needed then parens ppp else ppp
   | P_vector_concat pats ->
      raise (Reporting_basic.err_unreachable l
        "vector concatenation patterns should have been removed before pretty-printing")
   | P_tup pats  ->
      (match pats with
-      | [p] -> doc_pat_lem regtypes apat_needed p
-      | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats))
-  | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*)
-  | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem regtypes true p) (doc_pat_lem regtypes true p')
+      | [p] -> doc_pat_lem sequential mwords apat_needed p
+      | _ -> parens (separate_map comma_sp (doc_pat_lem sequential mwords false) pats))
+  | P_list pats -> brackets (separate_map semi (doc_pat_lem sequential mwords false) pats) (*Never seen but easy in lem*)
+  | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem sequential mwords true p) (doc_pat_lem sequential mwords true p')
   | P_record (_,_) | P_vector_indexed _ -> empty (* TODO *)
 
 let rec contains_bitvector_typ (Typ_aux (t,_) as typ) = match t with
@@ -363,11 +366,11 @@ let typ_id_of (Typ_aux (typ, l)) = match typ with
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp regtypes (early_ret : bool) (aexp_needed : bool)
+  let rec top_exp sequential mwords (early_ret : bool) (aexp_needed : bool)
     (E_aux (e, (l,annot)) as full_exp) =
-    let expY = top_exp regtypes early_ret true in
-    let expN = top_exp regtypes early_ret false in
-    let expV = top_exp regtypes early_ret in
+    let expY = top_exp sequential mwords early_ret true in
+    let expN = top_exp sequential mwords early_ret false in
+    let expV = top_exp sequential mwords early_ret in
     let liftR doc =
       if early_ret && effectful (effect_of full_exp)
       then separate space [string "liftR"; parens (doc)]
@@ -389,12 +392,12 @@ let doc_exp_lem, doc_let_lem =
                    doc_id_lem id in
                  liftR ((prefix 2 1)
                    (string "write_reg_field_range")
-                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space^^
                              field_ref ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
                  (string "write_reg_range")
-                 (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
+                 (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
            )
         | LEXP_vector (le,e2) when is_bit_typ t ->
            (match le with
@@ -408,16 +411,16 @@ let doc_exp_lem, doc_let_lem =
                    doc_id_lem id in
                  liftR ((prefix 2 1)
                    (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
+                   (align (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ field_ref ^/^ expY e2 ^/^ expY e)))
             | _ ->
                liftR ((prefix 2 1)
                  (string "write_reg_bit")
-                 (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e))
+                 (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ expY e2 ^/^ expY e))
            )
         (* | LEXP_field (le,id) when is_bit_typ t ->
            liftR ((prefix 2 1)
              (string "write_reg_bitfield")
-             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *)
+             (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)) *)
         | LEXP_field ((LEXP_aux (_, lannot) as le),id) ->
           let field_ref =
             doc_id_lem (typ_id_of (typ_of_annot lannot)) ^^
@@ -425,7 +428,7 @@ let doc_exp_lem, doc_let_lem =
             doc_id_lem id in
            liftR ((prefix 2 1)
              (string "write_reg_field")
-             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^
+             (doc_lexp_deref_lem sequential mwords early_ret le ^^ space ^^
                 field_ref ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
            (match alias_info with
@@ -441,15 +444,15 @@ let doc_exp_lem, doc_let_lem =
                string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
                  string reg2 ^^ space ^^ expY e) *)
         | _ ->
-           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes early_ret le ^/^ expY e)))
+           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem sequential mwords early_ret le ^/^ expY e)))
     | E_vector_append(le,re) ->
       raise (Reporting_basic.err_unreachable l
-        "E_vector_access should have been rewritten before pretty-printing")
+        "E_vector_append should have been rewritten before pretty-printing")
        (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let (call,ta,aexp_needed) =
          if is_bitvector_typ t then
            if not (contains_t_pp_var t)
-           then ("bitvector_concat", doc_tannot_lem regtypes false t, true)
+           then ("bitvector_concat", doc_tannot_lem sequential mwords false t, true)
            else ("bitvector_concat", empty, aexp_needed)
          else ("vector_concat",empty,aexp_needed) in
        let epp =
@@ -467,7 +470,7 @@ let doc_exp_lem, doc_let_lem =
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
        raise (report l "E_for should have been removed till now")
     | E_let(leb,e) ->
-       let epp = let_exp regtypes early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+       let epp = let_exp sequential mwords early_ret leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
        if aexp_needed then parens epp else epp
     | E_app(f,args) ->
        begin match f with
@@ -506,7 +509,7 @@ let doc_exp_lem, doc_let_lem =
             let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
             let eff = effect_of full_exp in
             if contains_bitvector_typ t && not (contains_t_pp_var t)
-            then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
+            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
        | Id_aux (Id "length",_) ->
@@ -544,7 +547,7 @@ let doc_exp_lem, doc_let_lem =
                let eff = effect_of full_exp in
                if contains_bitvector_typ (Env.base_typ_of (env_of full_exp) t) &&
                   not (contains_t_pp_var t)
-               then (align epp ^^ (doc_tannot_lem regtypes (effectful eff) t), true)
+               then (align epp ^^ (doc_tannot_lem sequential mwords (effectful eff) t), true)
                else (epp, aexp_needed) in
              liftR (if aexp_needed then parens (align taepp) else taepp)
           end
@@ -563,20 +566,20 @@ let doc_exp_lem, doc_let_lem =
        if aexp_needed then parens (align epp) else epp*)
     | E_vector_subrange (v,e1,e2) ->
       raise (Reporting_basic.err_unreachable l
-        "E_vector_access should have been rewritten before pretty-printing")
+        "E_vector_subrange should have been rewritten before pretty-printing")
        (* let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let eff = effect_of full_exp in
        let (epp,aexp_needed) =
          if has_effect eff BE_rreg then
            let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
            if contains_bitvector_typ t && not (contains_t_pp_var t)
-           then (epp ^^ doc_tannot_lem regtypes true t, true)
+           then (epp ^^ doc_tannot_lem sequential mwords true t, true)
            else (epp, aexp_needed)
          else
            if is_bitvector_typ t then
              let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in
              if not (contains_t_pp_var t)
-             then (bepp ^^ doc_tannot_lem regtypes false t, true)
+             then (bepp ^^ doc_tannot_lem sequential mwords false t, true)
              else (bepp, aexp_needed)
            else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in
        if aexp_needed then parens (align epp) else epp *)
@@ -591,7 +594,7 @@ let doc_exp_lem, doc_let_lem =
            let field_f = doc_id_lem tid ^^ underscore ^^ doc_id_lem id ^^ dot ^^ string "get_field" in
            let (ta,aexp_needed) =
              if contains_bitvector_typ t && not (contains_t_pp_var t)
-             then (doc_tannot_lem regtypes (effectful eff) t, true)
+             then (doc_tannot_lem sequential mwords (effectful eff) t, true)
              else (empty, aexp_needed) in
            let epp = field_f ^^ space ^^ (expY fexp) in
            if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
@@ -614,7 +617,7 @@ let doc_exp_lem, doc_let_lem =
        if has_effect eff BE_rreg then
          let epp = separate space [string "read_reg";doc_id_lem id] in
          if is_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
-         then liftR (parens (epp ^^ doc_tannot_lem regtypes true base_typ))
+         then liftR (parens (epp ^^ doc_tannot_lem sequential mwords true base_typ))
          else liftR epp
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
@@ -626,7 +629,7 @@ let doc_exp_lem, doc_let_lem =
                   | _ -> "read_reg_field" in
                 let ta =
                   if contains_bitvector_typ t && not (contains_t_pp_var t)
-                  then doc_tannot_lem regtypes true t else empty in
+                  then doc_tannot_lem sequential mwords true t else empty in
                 let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
             | Alias_pair(reg1,reg2) ->
@@ -634,7 +637,7 @@ let doc_exp_lem, doc_let_lem =
                   if has_effect eff BE_rreg then
                     let ta =
                       if contains_bitvector_typ t && not (contains_t_pp_var t)
-                      then doc_tannot_lem regtypes true t else empty in
+                      then doc_tannot_lem sequential mwords true t else empty in
                     ("read_two_regs", ta)
                   else
                     ("RegisterPair", empty) in
@@ -647,11 +650,11 @@ let doc_exp_lem, doc_let_lem =
                   else
                     let ta =
                       if contains_bitvector_typ t && not (contains_t_pp_var t)
-                      then doc_tannot_lem regtypes true t else empty in
+                      then doc_tannot_lem sequential mwords true t else empty in
                     separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
                 if aexp_needed then parens (align epp) else epp
            )*)
-    | E_lit lit -> doc_lit_lem regtypes false lit annot
+    | E_lit lit -> doc_lit_lem sequential mwords false lit annot
     | E_cast(typ,e) ->
        expV aexp_needed e (*
        (match annot with
@@ -659,7 +662,7 @@ let doc_exp_lem, doc_let_lem =
            (* TODO: Does this case still exist with the new type checker? *)
            let epp = string "read_reg" ^^ space ^^ expY e in
            if contains_bitvector_typ t && not (contains_t_pp_var t)
-           then parens (epp ^^ doc_tannot_lem regtypes true t) else epp
+           then parens (epp ^^ doc_tannot_lem sequential mwords true t) else epp
         | Base((_,t),_,_,_,_,_) ->
            (match typ with
             | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) ->
@@ -692,7 +695,7 @@ let doc_exp_lem, doc_let_lem =
          | _ ->  raise (report l "cannot get record type") in
        let epp = anglebars (space ^^ (align (separate_map
                                           (semi_sp ^^ break 1)
-                                          (doc_fexp regtypes early_ret recordtyp) fexps)) ^^ space) in
+                                          (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
@@ -700,7 +703,7 @@ let doc_exp_lem, doc_let_lem =
          | Some (env, Typ_aux (Typ_id tid,_), _) when Env.is_record tid env ->
            tid
          | _ ->  raise (report l "cannot get record type") in
-       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes early_ret recordtyp) fexps))
+       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp sequential mwords early_ret recordtyp) fexps))
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let (start, len, order, etyp) =
@@ -731,11 +734,11 @@ let doc_exp_lem, doc_let_lem =
               let epp =
                 group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
               let (epp,aexp_needed) =
-                if is_bit_typ etyp then
+                if is_bit_typ etyp && mwords then
                   let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
                   if contains_t_pp_var t
                   then (bepp, aexp_needed)
-                  else (bepp ^^ doc_tannot_lem regtypes false t, true)
+                  else (bepp ^^ doc_tannot_lem sequential mwords false t, true)
                 else (epp,aexp_needed) in
               if aexp_needed then parens (align epp) else epp
        (* *)
@@ -792,18 +795,24 @@ let doc_exp_lem, doc_let_lem =
          align (group (call ^//^ brackets expspp ^/^
                          separate space [default_string;string start;string size;string dir_out])) in
        let (bepp, aexp_needed) =
-         if is_bitvector_typ t
-         then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem regtypes false t, true)
+         if is_bitvector_typ t && mwords
+         then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem sequential mwords false t, true)
          else (epp, aexp_needed) in
        if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
        let t = typ_of full_exp in
-       let call = if is_bitvector_typ t then "bvupdate_pos" else "update_pos" in
+       let call =
+         if is_bitvector_typ t (*&& mwords*)
+         then "bitvector_update_pos"
+         else "update_pos" in
        let epp = separate space [string call;expY v;expY e1;expY e2] in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
        let t = typ_of full_exp in
-       let call = if is_bitvector_typ t then "bvupdate" else "update" in
+       let call =
+         if is_bitvector_typ t (*&& mwords*)
+         then "bitvector_update"
+         else "update" in
        let epp = align (string call ^//^
                           group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
                             group (expY e3)) in
@@ -829,7 +838,7 @@ let doc_exp_lem, doc_let_lem =
         pattern-matching on integers *)
        let epp =
          group ((separate space [string "match"; only_integers e; string "with"]) ^/^
-                  (separate_map (break 1) (doc_case regtypes early_ret) pexps) ^/^
+                  (separate_map (break 1) (doc_case sequential mwords early_ret) pexps) ^/^
                     (string "end")) in
        if aexp_needed then parens (align epp) else align epp
     | E_exit e -> liftR (separate space [string "exit"; expY e;])
@@ -919,7 +928,7 @@ let doc_exp_lem, doc_let_lem =
                    string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
            let (epp,aexp_needed) =
              if contains_bitvector_typ t && not (contains_t_pp_var t)
-             then (parens epp ^^ doc_tannot_lem regtypes false t, true)
+             then (parens epp ^^ doc_tannot_lem sequential mwords false t, true)
              else (epp, aexp_needed) in
            if aexp_needed then parens (align epp) else epp
         | _ ->
@@ -944,13 +953,13 @@ let doc_exp_lem, doc_let_lem =
             (separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2
          | _ ->
             (separate space [expV b e1; string ">>= fun";
-                             doc_pat_lem regtypes true pat;arrow]) ^^ hardline ^^ expN e2 in
+                             doc_pat_lem sequential mwords true pat;arrow]) ^^ hardline ^^ expN e2 in
        if aexp_needed then parens (align epp) else epp
     | E_internal_return (e1) ->
        separate space [string "return"; expY e1;]
     | E_sizeof nexp ->
       (match simplify_nexp nexp with
-        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem regtypes false (L_aux (L_num i, l)) annot
+        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem sequential mwords false (L_aux (L_num i, l)) annot
         | _ ->
           raise (Reporting_basic.err_unreachable l
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
@@ -960,34 +969,34 @@ let doc_exp_lem, doc_let_lem =
     | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
       raise (Reporting_basic.err_unreachable l
         "unsupported internal expression encountered while pretty-printing")
-  and let_exp regtypes early_ret (LB_aux(lb,_)) = match lb with
+  and let_exp sequential mwords early_ret (LB_aux(lb,_)) = match lb with
     | LB_val_explicit(_,pat,e)
       | LB_val_implicit(pat,e) ->
        prefix 2 1
-              (separate space [string "let"; doc_pat_lem regtypes true pat; equals])
-              (top_exp regtypes early_ret false e)
+              (separate space [string "let"; doc_pat_lem sequential mwords true pat; equals])
+              (top_exp sequential mwords early_ret false e)
 
-  and doc_fexp regtypes early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+  and doc_fexp sequential mwords early_ret recordtyp (FE_aux(FE_Fexp(id,e),_)) =
     let fname =
       if prefix_recordtype
       then (string (string_of_id recordtyp ^ "_")) ^^ doc_id_lem id
       else doc_id_lem id in
-    group (doc_op equals fname (top_exp regtypes early_ret true e))
+    group (doc_op equals fname (top_exp sequential mwords early_ret true e))
 
-  and doc_case regtypes early_ret = function
+  and doc_case sequential mwords early_ret = function
   | Pat_aux(Pat_exp(pat,e),_) ->
-    group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow])
-                  (group (top_exp regtypes early_ret false e)))
+    group (prefix 3 1 (separate space [pipe; doc_pat_lem sequential mwords false pat;arrow])
+                  (group (top_exp sequential mwords early_ret false e)))
   | Pat_aux(Pat_when(_,_,_),(l,_)) ->
     raise (Reporting_basic.err_unreachable l
       "guarded pattern expression should have been rewritten before pretty-printing")
 
-  and doc_lexp_deref_lem regtypes early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+  and doc_lexp_deref_lem sequential mwords early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
-       parens (separate empty [doc_lexp_deref_lem regtypes early_ret le;dot;doc_id_lem id])
+       parens (separate empty [doc_lexp_deref_lem sequential mwords early_ret le;dot;doc_id_lem id])
     | LEXP_vector(le,e) ->
-       parens ((separate space) [string "access";doc_lexp_deref_lem regtypes early_ret le;
-                                 top_exp regtypes early_ret true e])
+       parens ((separate space) [string "access";doc_lexp_deref_lem sequential mwords early_ret le;
+                                 top_exp sequential mwords early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
     | _ ->
@@ -996,9 +1005,9 @@ let doc_exp_lem, doc_let_lem =
   in top_exp, let_exp
 
 (*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem regtypes (Tu_aux(typ_u,_)) = match typ_u with
+let doc_type_union_lem sequential mwords (Tu_aux(typ_u,_)) = match typ_u with
   | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
-                                        parens (doc_typ_lem regtypes typ)]
+                                        parens (doc_typ_lem sequential mwords typ)]
   | Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
 
 let rec doc_range_lem (BF_aux(r,_)) = match r with
@@ -1006,16 +1015,16 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2))
   | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
 
-let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
+let doc_typdef_lem sequential mwords (TD_aux(td, (l, _))) = match td with
   | TD_abbrev(id,nm,typschm) ->
      doc_op equals (concat [string "type"; space; doc_id_lem_type id])
-            (doc_typschm_lem regtypes false typschm)
+            (doc_typschm_lem sequential mwords false typschm)
   | TD_record(id,nm,typq,fs,_) ->
     let fname fid = if prefix_recordtype
                     then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
                     else doc_id_lem_type fid in
     let f_pp (typ,fid) =
-      concat [fname fid;space;colon;space;doc_typ_lem regtypes typ; semi] in
+      concat [fname fid;space;colon;space;doc_typ_lem sequential mwords typ; semi] in
     let rectyp = match typq with
       | TypQ_aux (TypQ_tq qs, _) ->
         let quant_item = function
@@ -1032,7 +1041,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
         mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
           [mk_typ_arg (Typ_arg_typ rectyp);
            mk_typ_arg (Typ_arg_typ ftyp)])) in
-      let rfannot = doc_tannot_lem regtypes false reftyp in
+      let rfannot = doc_tannot_lem sequential mwords false reftyp in
       let get, set =
         string "rec_val" ^^ dot ^^ fname fid,
         anglebars (space ^^ string "rec_val with " ^^
@@ -1040,12 +1049,14 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
       doc_op equals
         (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
         (anglebars (concat [space;
+          doc_op equals (string "field_name") (string_lit (doc_id_lem fid)); semi_sp;
           doc_op equals (string "get_field") (parens (doc_op arrow (string "fun rec_val") get)); semi_sp;
           doc_op equals (string "set_field") (parens (doc_op arrow (string "fun rec_val v") set)); space])) in
     doc_op equals
            (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq])
            ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space))) ^^ hardline ^^
-    separate_map hardline doc_field fs
+    if sequential && string_of_id id = "regstate" then empty
+    else separate_map hardline doc_field fs
   | TD_variant(id,nm,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
@@ -1058,7 +1069,7 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
       | Id_aux ((Id "diafp"),_) -> empty
       | Id_aux ((Id "option"),_) -> empty
       | _ ->
-         let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
+         let ar_doc = group (separate_map (break 1) (doc_type_union_lem sequential mwords) ar) in
          let typ_pp =
 
            (doc_op equals)
@@ -1230,20 +1241,16 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
   | TD_register(id,n1,n2,rs) ->
     match n1, n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
-       let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
-                                                       doc_range_lem r;]) in
-       let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
-       (*let doc_rfield (_,id) =
-         (doc_op equals)
-           (string "let" ^^ space ^^ doc_id_lem id)
-           (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
        let dir_b = i1 < i2 in
        let dir = string (if dir_b then "true" else "false") in
        let dir_suffix = (if dir_b then "_inc" else "_dec") in
        let ord = Ord_aux ((if dir_b then Ord_inc else Ord_dec), Parse_ast.Unknown) in
        let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in
        let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
-       let tannot = doc_tannot_lem regtypes false vtyp in
+       let tannot = doc_tannot_lem sequential mwords false vtyp in
+       let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id);
+                                                       doc_range_lem r;]) in
+       let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
        let doc_field (fr, fid) =
          let i, j = match fr with
          | BF_aux (BF_single i, _) -> (i, i)
@@ -1255,32 +1262,21 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
            mk_typ (Typ_app (Id_aux (Id "field_ref", Parse_ast.Unknown),
              [mk_typ_arg (Typ_arg_typ (mk_id_typ id));
               mk_typ_arg (Typ_arg_typ ftyp)])) in
-         let rfannot = doc_tannot_lem regtypes false reftyp in
+         let rfannot = doc_tannot_lem sequential mwords false reftyp in
          let get, set =
            "bitvector_subrange" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ")",
            "bitvector_update" ^ dir_suffix ^ " (reg, " ^ string_of_int i ^ ", " ^ string_of_int j ^ ", v)" in
          doc_op equals
            (concat [string "let "; parens (concat [doc_id_lem id; underscore; doc_id_lem fid; rfannot])])
            (concat [
-             space; langlebar; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline;
+             space; langlebar; string " field_name = \"" ^^ doc_id_lem fid ^^ string "\";"; hardline;
+             space; space; space; string (" get_field = (fun reg -> " ^ get ^ ");"); hardline;
              space; space; space; string (" set_field = (fun reg v -> " ^ set ^ ") "); ranglebar])
-             (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^
-         string ("  get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^
-         string ("  set_field = (fun reg v -> " ^ set ^") |>") *)
-         (* doc_op equals
-           (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid;
-             space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *)
        in
        doc_op equals
          (concat [string "type";space;doc_id_lem id])
-         (doc_typ_lem regtypes vtyp)
+         (doc_typ_lem sequential mwords vtyp)
        ^^ hardline ^^
-       (* doc_op equals
-         (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
-         (string "Register" ^^ space ^^
-            align (separate space [string "regname"; doc_int size; doc_int i1; dir;
-                                   break 0 ^^ brackets (align doc_rids)]))
-       ^^ hardline ^^ *)
        doc_op equals
          (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
          (string "reg")
@@ -1289,25 +1285,54 @@ let doc_typdef_lem regtypes (TD_aux(td, (l, _))) = match td with
          (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
          (string "reg")
        ^^ hardline ^^
-         separate_map hardline doc_field rs
+       (* if sequential then *)
+               (* string " = <|" (*; parens (string "reg" ^^ tannot) *)]) ^^ hardline ^^
+           string ("  get_field = (fun reg -> " ^ get ^ ");") ^^ hardline ^^
+           string ("  set_field = (fun reg v -> " ^ set ^") |>") *)
+           (* doc_op equals
+             (concat [string "let set_"; doc_id_lem id; underscore; doc_id_lem fid;
+               space; parens (separate comma_sp [parens (string "reg" ^^ tannot); string "v"])]) (string set) *)
+         (* in *)
+         (* doc_op equals
+           (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
+           (string "Register" ^^ space ^^
+              align (separate space [string "regname"; doc_int size; doc_int i1; dir;
+                                     break 0 ^^ brackets (align doc_rids)]))
+         ^^ hardline ^^ *)
+           separate_map hardline doc_field rs
+       ^^ hardline ^^
+       (* else *)
+         (*let doc_rfield (_,id) =
+           (doc_op equals)
+             (string "let" ^^ space ^^ doc_id_lem id)
+             (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*)
+         doc_op equals
+           (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"])
+           (string "Register" ^^ space ^^
+              align (separate space [string "regname"; doc_int size; doc_int i1; dir;
+                                     break 0 ^^ brackets (align doc_rids)]))
+         (*^^ hardline ^^
+           separate_map hardline doc_field rs*)
+    | _ -> raise (Reporting_basic.err_unreachable l "register with non-constant indices")
+
 
 let doc_rec_lem (Rec_aux(r,_)) = match r with
   | Rec_nonrec -> space
   | Rec_rec -> space ^^ string "rec" ^^ space
 
-let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with
-  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem regtypes typ)
+let doc_tannot_opt_lem sequential mwords (Typ_annot_opt_aux(t,_)) = match t with
+  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem sequential mwords typ)
 
-let doc_fun_body_lem regtypes exp =
+let doc_fun_body_lem sequential mwords exp =
   let early_ret = contains_early_return exp in
-  let doc_exp = doc_exp_lem regtypes early_ret false exp in
+  let doc_exp = doc_exp_lem sequential mwords early_ret false exp in
   if early_ret
   then align (string "catch_early_return" ^//^ parens (doc_exp))
   else doc_exp
 
-let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow)
-    (doc_fun_body_lem regtypes exp))
+let doc_funcl_lem sequential mwords (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+  group (prefix 3 1 ((doc_pat_lem sequential mwords false pat) ^^ space ^^ arrow)
+    (doc_fun_body_lem sequential mwords exp))
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -1315,20 +1340,21 @@ let get_id = function
 
 module StringSet = Set.Make(String)
 
-let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
+let rec doc_fundef_lem sequential mwords (FD_aux(FD_function(r, typa, efa, fcls),fannot)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
-  | [FCL_aux (FCL_Funcl(id,pat,exp),_)] ->
+  | [FCL_aux (FCL_Funcl(id,pat,exp),_)]
+    when not (Env.is_extern id (env_of exp)) ->
      (prefix 2 1)
        ((separate space)
           [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
-           (doc_pat_lem regtypes true pat);
+           (doc_pat_lem sequential mwords true pat);
            equals])
-       (doc_fun_body_lem regtypes exp)
-  | _ ->
-    let id = get_id fcls in
+       (doc_fun_body_lem sequential mwords exp)
+  | FCL_aux (FCL_Funcl(id,_,exp),_) :: _
+    when not (Env.is_extern id (env_of exp)) ->
     (*    let sep = hardline ^^ pipe ^^ space in *)
-    match id with
+    (match id with
     | Id_aux (Id fname,idl)
       when fname = "execute" || fname = "initial_analysis" ->
       let (_,auxiliary_functions,clauses) = 
@@ -1354,7 +1380,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
                                              P_aux (P_tup argspat,pannot),exp),annot) in
                let auxiliary_functions = 
                   auxiliary_functions ^^ hardline ^^ hardline ^^
-                    doc_fundef_lem regtypes (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
+                    doc_fundef_lem sequential mwords (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
                (* Bind complex patterns to names so that we can pass them to the
                   auxiliary function *)
                let name_pat idx (P_aux (p,a)) = match p with
@@ -1366,13 +1392,13 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
                let named_pat = P_aux (P_app (Id_aux (Id ctor,l),named_argspat),pannot) in
                let doc_arg idx (P_aux (p,(l,a))) = match p with
                  | P_as (pat,id) -> doc_id_lem id
-                 | P_lit lit -> doc_lit_lem regtypes false lit a
+                 | P_lit lit -> doc_lit_lem sequential mwords false lit a
                  | P_id id -> doc_id_lem id
                  | _ -> string ("arg" ^ string_of_int idx) in
                let clauses =
                  clauses ^^ (break 1) ^^
                    (separate space
-                      [pipe;doc_pat_lem regtypes false named_pat;arrow;
+                      [pipe;doc_pat_lem sequential mwords false named_pat;arrow;
                        string aux_fname;
                        parens (separate comma (List.mapi doc_arg named_argspat))]) in
                (already_used_fnames,auxiliary_functions,clauses)
@@ -1385,73 +1411,75 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
     | _ ->
       let clauses =
         (separate_map (break 1))
-          (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in
+          (fun fcl -> separate space [pipe;doc_funcl_lem sequential mwords fcl]) fcls in
       (prefix 2 1)
         ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"])
-        (clauses ^/^ string "end")
-      
+        (clauses ^/^ string "end"))
+  | _ -> empty
 
 
-let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
+
+let doc_dec_lem sequential (DEC_aux (reg, ((l, _) as annot))) =
   match reg with
   | DEC_reg(typ,id) ->
-     empty
-     (* let env = env_of_annot annot in
-     (match typ with
-      | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env ->
-        separate space [string "let";doc_id_lem id;equals;
-                        string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
-      | _ ->
-        let rt = Env.base_typ_of env typ in
-        if is_vector_typ rt then
-          let (start, size, order, etyp) = vector_typ_args_of rt in
-          if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
-            let o = if is_order_inc order then "true" else "false" in
-            (doc_op equals)
-            (string "let" ^^ space ^^ doc_id_lem id)
-            (string "Register" ^^ space ^^
-               align (separate space [string_lit(doc_id_lem id);
-                                      doc_nexp (size);
-                                      doc_nexp (start);
-                                      string o;
-                                      string "[]"]))
-               ^/^ hardline
+     if sequential then empty
+     else
+       let env = env_of_annot annot in
+       (match typ with
+        | Typ_aux (Typ_id idt, _) when Env.is_regtyp idt env ->
+          separate space [string "let";doc_id_lem id;equals;
+                          string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
+        | _ ->
+          let rt = Env.base_typ_of env typ in
+          if is_vector_typ rt then
+            let (start, size, order, etyp) = vector_typ_args_of rt in
+            if is_bit_typ etyp && is_nexp_constant start && is_nexp_constant size then
+              let o = if is_order_inc order then "true" else "false" in
+              (doc_op equals)
+              (string "let" ^^ space ^^ doc_id_lem id)
+              (string "Register" ^^ space ^^
+                 align (separate space [string_lit(doc_id_lem id);
+                                        doc_nexp (size);
+                                        doc_nexp (start);
+                                        string o;
+                                        string "[]"]))
+                 ^/^ hardline
+            else raise (Reporting_basic.err_unreachable l
+              ("can't deal with register type " ^ string_of_typ typ))
           else raise (Reporting_basic.err_unreachable l
-            ("can't deal with register type " ^ string_of_typ typ))
-        else raise (Reporting_basic.err_unreachable l
-          ("can't deal with register type " ^ string_of_typ typ))) *)
+            ("can't deal with register type " ^ string_of_typ typ)))
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
-let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
+let doc_spec_lem mwords (VS_aux (valspec,annot)) =
   match valspec with
   | VS_extern_no_rename _
   | VS_extern_spec _ -> empty (* ignore these at the moment *)
   | VS_val_spec (typschm,id) | VS_cast_spec (typschm,id) -> empty
-(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *)
+(* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem mwords typschm] ^/^ hardline *)
 
 
-let rec doc_def_lem regtypes def = match def with
-  | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty)
+let rec doc_def_lem sequential mwords def = match def with
+  | DEF_spec v_spec -> (doc_spec_lem mwords v_spec,empty)
   | DEF_overload _ -> (empty,empty)
-  | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty)
-  | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
+  | DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
+  | DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
 
   | DEF_default df -> (empty,empty)
-  | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline)
-  | DEF_val lbind -> (empty,group (doc_let_lem regtypes false lbind) ^/^ hardline)
+  | DEF_fundef f_def -> (empty,group (doc_fundef_lem sequential mwords f_def) ^/^ hardline)
+  | DEF_val lbind -> (empty,group (doc_let_lem sequential mwords false lbind) ^/^ hardline)
   | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
   | DEF_kind _ -> (empty,empty)
 
   | DEF_comm (DC_comm s) -> (empty,comment (string s))
   | DEF_comm (DC_comm_struct d) ->
-     let (typdefs,vdefs) = doc_def_lem regtypes d in
+     let (typdefs,vdefs) = doc_def_lem sequential mwords d in
      (empty,comment (typdefs ^^ hardline ^^ vdefs))
 
 
-let doc_defs_lem regtypes (Defs defs) =
-  let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
+let doc_defs_lem sequential mwords (Defs defs) =
+  let (typdefs,valdefs) = List.split (List.map (doc_def_lem sequential mwords) defs) in
   (separate empty typdefs,separate empty valdefs)
 
 let find_regtypes (Defs defs) =
@@ -1470,7 +1498,7 @@ let find_registers (Defs defs) =
       | _ -> acc
     ) [] defs
 
-let doc_regstate_lem regtypes registers =
+let doc_regstate_lem mwords registers =
   let l = Parse_ast.Unknown in
   let annot = (l, None) in
   let regstate = match registers with
@@ -1487,25 +1515,26 @@ let doc_regstate_lem regtypes registers =
         registers,
         false) in
   concat [
-    doc_typdef_lem regtypes (TD_aux (regstate, annot)); hardline;
+    doc_typdef_lem true mwords (TD_aux (regstate, annot)); hardline;
     hardline;
     string "type _M 'a = M regstate 'a"
   ]
 
-let doc_register_refs_lem regtypes registers =
+let doc_register_refs_lem registers =
   let doc_register_ref (typ, id) =
     let idd = doc_id_lem id in
     let field = if prefix_recordtype then string "regstate_" ^^ idd else idd in
     concat [string "let "; idd; string " = <|"; hardline;
+      string "  reg_name = \""; idd; string "\";"; hardline;
       string "  read_from = (fun s -> s."; field; string ");"; hardline;
       string "  write_to = (fun s v -> (<| s with "; field; string " = v |>)) |>"] in
   separate_map hardline doc_register_ref registers
 
-let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line =
-  let regtypes = find_regtypes d in
-  let (typdefs,valdefs) = doc_defs_lem regtypes d in
-  let regstate_def = doc_regstate_lem regtypes (find_registers d) in
-  let register_refs = doc_register_refs_lem regtypes (find_registers d) in
+let pp_defs_lem sequential mwords (types_file,types_modules) (defs_file,defs_modules) d top_line =
+  (* let regtypes = find_regtypes d in *)
+  let (typdefs,valdefs) = doc_defs_lem sequential mwords d in
+  let regstate_def = doc_regstate_lem mwords (find_registers d) in
+  let register_refs = doc_register_refs_lem (find_registers d) in
   (print types_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
@@ -1523,8 +1552,16 @@ let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (p
              string "module SIA = Interp_ast"; hardline;
              hardline]
         else empty;
-        typdefs]);
-  (print types_seq_file)
+        typdefs; hardline;
+        hardline;
+        if sequential then
+          concat [regstate_def; hardline;
+          hardline;
+          register_refs]
+        else
+          concat [string "type _M 'a = M 'a"; hardline]
+        ]);
+  (* (print types_seq_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
@@ -1541,24 +1578,22 @@ let pp_defs_lem (types_file,types_modules) (types_seq_file,types_seq_modules) (p
              string "module SIA = Interp_ast"; hardline;
              hardline]
         else empty;
-        typdefs;
-        hardline;
+        typdefs_seq; hardline;
         hardline;
-        regstate_def;
+        regstate_def; hardline;
         hardline;
-        hardline;
-        register_refs]);
-  (print prompt_file)
+        register_refs]); *)
+  (print defs_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
-          (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline;
+          (fun lib -> separate space [string "open import";string lib]) defs_modules;hardline;
         hardline;
         valdefs]);
-  (print state_file)
+  (* (print state_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
           (fun lib -> separate space [string "open import";string lib]) state_modules;hardline;
         hardline;
-        valdefs]);
+        valdefs_seq]); *)