Merge remote-tracking branch 'origin/mono-experiments' into experiments

1 files changed, 243 insertions, 174 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 2619cc51..586773ca 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -160,7 +160,7 @@ let doc_typ_lem, doc_atomic_typ_lem =
          let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes 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, _)) as ty) = match t with
+    and app_typ regtypes 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, _);
@@ -168,19 +168,17 @@ let doc_typ_lem, doc_atomic_typ_lem =
           Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
          let tpp = match elem_typ with
            | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
-               let len = match m with
-                 | (Nexp_aux(Nexp_constant i,_)) -> string "ty" ^^ doc_int i
-                 | _ -> doc_nexp m in
-               string "bitvector" ^^ space ^^ len
+             (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
          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?
-            The former are represented in the Lem library using a type
-            "register" (without parameters), the latter just using the content
-            type (e.g. "bitvector ty64").  We assume the latter is meant here
-            and drop the "register" keyword. *)
-         fn_typ regtypes atyp_needed etyp
+         (* TODO: Better distinguish register names and contents? *)
+         (* fn_typ regtypes atyp_needed etyp *)
+         (string "register")
       | Typ_app(Id_aux (Id "range", _),_) ->
          (string "integer")
       | Typ_app(Id_aux (Id "implicit", _),_) ->
@@ -192,13 +190,13 @@ let doc_typ_lem, doc_atomic_typ_lem =
          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
-      | Typ_id (Id_aux (Id "bool",_)) -> string "bitU"
-      | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU"
+      | Typ_id (Id_aux (Id "bool",_)) -> string "bool"
+      | Typ_id (Id_aux (Id "boolean",_)) -> string "bool"
       | Typ_id (Id_aux (Id "bit",_)) -> string "bitU"
       | Typ_id (id) ->
-         if List.exists ((=) (string_of_id id)) regtypes
+         (*if List.exists ((=) (string_of_id id)) regtypes
          then string "register"
-         else doc_id_lem_type id
+         else*) doc_id_lem_type id
       | Typ_var v -> doc_var v
       | Typ_wild -> underscore
       | Typ_app _ | Typ_tup _ | Typ_fn _ ->
@@ -213,46 +211,86 @@ let doc_typ_lem, doc_atomic_typ_lem =
       | Typ_arg_effect e -> empty
   in typ', atomic_typ
 
+(* Check for variables in types that would be pretty-printed.
+   In particular, in case of vector types, only the element type and the
+   length argument are checked for variables, and the latter only if it is
+   a bitvector; for other types of vectors, the length is not pretty-printed
+   in the type, and the start index is never pretty-printed in vector types. *)
+let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
+  | Typ_wild -> true
+  | Typ_id _ -> false
+  | Typ_var _ -> true
+  | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
+  | Typ_tup ts -> List.exists contains_t_pp_var ts
+  | Typ_app (c,targs) ->
+      if Ast_util.is_number typ then false
+      else if is_bitvector_typ typ then
+        let (_,length,_,_) = vector_typ_args_of typ in
+        not (is_nexp_constant (simplify_nexp length))
+      else List.exists contains_t_arg_pp_var targs
+and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
+  | Typ_arg_typ t -> contains_t_pp_var t
+  | Typ_arg_nexp nexp -> not (is_nexp_constant (simplify_nexp nexp))
+  | _ -> false
+
 let doc_tannot_lem regtypes eff typ =
-  let ta = doc_typ_lem regtypes typ in
-  if eff then string " : M " ^^ parens ta
-  else string " : " ^^ ta
+  if contains_t_pp_var typ then empty
+  else
+    let ta = doc_typ_lem regtypes 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 in_pat (L_aux(lit,l)) a =
-  utf8string (match lit with
-  | L_unit  -> "()"
-  | L_zero  -> "B0"
-  | L_one   -> "B1"
-  | L_false -> "B0"
-  | L_true  -> "B1"
+let doc_lit_lem regtypes in_pat (L_aux(lit,l)) a =
+  match lit with
+  | L_unit  -> utf8string "()"
+  | L_zero  -> utf8string "B0"
+  | L_one   -> utf8string "B1"
+  | L_false -> utf8string "false"
+  | L_true  -> utf8string "true"
   | L_num i ->
      let ipp = string_of_int i in
-     if in_pat then "("^ipp^":nn)"
-     else if i < 0 then "((0"^ipp^"):ii)"
-     else "("^ipp^":ii)"
+     utf8string (
+       if in_pat then "("^ipp^":nn)"
+       else if i < 0 then "((0"^ipp^"):ii)"
+       else "("^ipp^":ii)")
   | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*)
   | L_undef ->
      (match a with
-       | Some (_, Typ_aux (t,_), _) ->
+       | Some (_, (Typ_aux (t,_) as typ), _) ->
          (match t with
           | Typ_id (Id_aux (Id "bit", _))
-          | Typ_app (Id_aux (Id "register", _),_) -> "UndefinedRegister 0"
-          | Typ_id (Id_aux (Id "string", _)) -> "\"\""
-          | _ -> "(failwith \"undefined value of unsupported type\")")
-       | _ -> "(failwith \"undefined value of unsupported type\")")
-  | L_string s -> "\"" ^ s ^ "\""
-  | L_real s -> s (* TODO What's the Lem syntax for reals? *))
+          | Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0"
+          | Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\""
+          | _ ->
+            parens
+              ((utf8string "(failwith \"undefined value of unsupported type\")") ^^
+              (doc_tannot_lem regtypes 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? *)
 
 (* typ_doc is the doc for the type being quantified *)
+let doc_quant_item (QI_aux (qi, _)) = match qi with
+| QI_id (KOpt_aux (KOpt_none kid, _))
+| QI_id (KOpt_aux (KOpt_kind (_, kid), _)) -> doc_var kid
+| _ -> empty
 
-let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc
+let doc_typquant_items_lem (TypQ_aux(tq,_)) = match tq with
+| TypQ_tq qs -> separate_map space doc_quant_item qs
+| _ -> empty
 
-let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  (doc_typquant_lem tq (doc_typ_lem regtypes t))
+let doc_typquant_lem (TypQ_aux(tq,_)) typ = match tq with
+| TypQ_tq ((_ :: _) as qs) ->
+  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 is_ctor env id = match Env.lookup_id id env with
 | Enum _ | Union _ -> true
@@ -267,14 +305,17 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w
                        (parens (separate_map comma (doc_pat_lem regtypes 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 true lit annot
+  | P_lit lit  -> doc_lit_lem regtypes 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_typ(typ,p) -> parens (doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ))
+  | P_typ(typ,p) ->
+    let doc_p = doc_pat_lem regtypes true p in
+    if contains_t_pp_var typ then doc_p
+    else parens (doc_op colon doc_p (doc_typ_lem regtypes typ))
   | P_vector pats ->
      let ppp =
        (separate space)
@@ -300,38 +341,23 @@ and contains_bitvector_typ_arg (Typ_arg_aux (targ, _)) = match targ with
   | Typ_arg_typ t -> contains_bitvector_typ t
   | _ -> false
 
-let const_nexp (Nexp_aux (nexp,_)) = match nexp with
-  | Nexp_constant _ -> true
-  | _ -> false
-
-(* Check for variables in types that would be pretty-printed.
-   In particular, in case of vector types, only the element type and the
-   length argument are checked for variables, and the latter only if it is
-   a bitvector; for other types of vectors, the length is not pretty-printed
-   in the type, and the start index is never pretty-printed in vector types. *)
-let rec contains_t_pp_var (Typ_aux (t,a) as typ) = match t with
-  | Typ_wild -> true
-  | Typ_id _ -> false
-  | Typ_var _ -> true
-  | Typ_fn (t1,t2,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
-  | Typ_tup ts -> List.exists contains_t_pp_var ts
-  | Typ_app (c,targs) ->
-      if is_bitvector_typ typ then
-        let (_,length,_,_) = vector_typ_args_of typ in
-        not (const_nexp ((*normalize_nexp*) length))
-      else List.exists contains_t_arg_pp_var targs
-and contains_t_arg_pp_var (Typ_arg_aux (targ, _)) = match targ with
-  | Typ_arg_typ t -> contains_t_pp_var t
-  | Typ_arg_nexp nexp -> not (const_nexp ((*normalize_nexp*) nexp))
-  | _ -> false
+let contains_early_return exp =
+  fst (fold_exp
+  { (Rewriter.compute_exp_alg false (||))
+    with e_return = (fun (_, r) -> (true, E_return r)) } exp)
 
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp regtypes (aexp_needed : bool) (E_aux (e, (l,annot)) as full_exp) =
-    let expY = top_exp regtypes true in
-    let expN = top_exp regtypes false in
-    let expV = top_exp regtypes in
+  let rec top_exp regtypes (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 liftR doc =
+      if early_ret && effectful (effect_of full_exp)
+      then separate space [string "liftR"; parens (doc)]
+      else doc in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le), e) ->
        (* can only be register writes *)
@@ -343,14 +369,14 @@ let doc_exp_lem, doc_let_lem =
                if is_bit_typ (typ_of_annot lannot) then
                  raise (report l "indexing a register's (single bit) bitfield not supported")
                else
-                 (prefix 2 1)
+                 liftR ((prefix 2 1)
                    (string "write_reg_field_range")
-                   (align (doc_lexp_deref_lem regtypes le ^^ space^^
-                             string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e))
+                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space^^
+                             string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e)))
             | _ ->
-               (prefix 2 1)
+               liftR ((prefix 2 1)
                  (string "write_reg_range")
-                 (align (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e))
+                 (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)))
            )
         | LEXP_vector (le,e2) when is_bit_typ t ->
            (match le with
@@ -358,23 +384,23 @@ let doc_exp_lem, doc_let_lem =
                if is_bit_typ (typ_of_annot lannot) then
                  raise (report l "indexing a register's (single bit) bitfield not supported")
                else
-                 (prefix 2 1)
+                 liftR ((prefix 2 1)
                    (string "write_reg_field_bit")
-                   (align (doc_lexp_deref_lem regtypes le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e))
+                   (align (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e)))
             | _ ->
-               (prefix 2 1)
+               liftR ((prefix 2 1)
                  (string "write_reg_bit")
-                 (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e)
+                 (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ expY e2 ^/^ expY e))
            )
         | LEXP_field (le,id) when is_bit_typ t ->
-           (prefix 2 1)
+           liftR ((prefix 2 1)
              (string "write_reg_bitfield")
-             (doc_lexp_deref_lem regtypes le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e)
+             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e))
         | LEXP_field (le,id) ->
-           (prefix 2 1)
+           liftR ((prefix 2 1)
              (string "write_reg_field")
-             (doc_lexp_deref_lem regtypes le ^^ space ^^
-                string_lit(doc_id_lem id) ^/^ expY e)
+             (doc_lexp_deref_lem regtypes early_ret le ^^ space ^^
+                string_lit(doc_id_lem id) ^/^ expY e))
         (* | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info ->
            (match alias_info with
             | Alias_field(reg,field) ->
@@ -389,9 +415,11 @@ let doc_exp_lem, doc_let_lem =
                string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^
                  string reg2 ^^ space ^^ expY e) *)
         | _ ->
-           (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e))
+           liftR ((prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes early_ret le ^/^ expY e)))
     | E_vector_append(le,re) ->
-       let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+      raise (Reporting_basic.err_unreachable l
+        "E_vector_access 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)
@@ -400,12 +428,12 @@ let doc_exp_lem, doc_let_lem =
          else ("vector_concat",empty,aexp_needed) in
        let epp =
          align (group (separate space [string call;expY le;expY re])) ^^ ta in
-       if aexp_needed then parens epp else epp
+       if aexp_needed then parens epp else epp *)
     | E_cons(le,re) -> doc_op (group (colon^^colon)) (expY le) (expY re)
     | E_if(c,t,e) ->
        let (E_aux (_,(_,cannot))) = c in
        let epp =
-         separate space [string "if";group (align (string "bitU_to_bool" ^//^ group (expY c)))] ^^
+         separate space [string "if";group (expY c)] ^^
            break 1 ^^
              (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^
                (prefix 2 1 (string "else") (expN e)) in
@@ -413,7 +441,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 leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in
+       let epp = let_exp regtypes 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
@@ -438,7 +466,7 @@ let doc_exp_lem, doc_let_lem =
                    (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body))
                 )
             )
-       | Id_aux (Id "append",_) ->
+       (* | Id_aux (Id "append",_) ->
           let [e1;e2] = args in
           let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in
           if aexp_needed then parens (align epp) else epp
@@ -464,7 +492,7 @@ let doc_exp_lem, doc_let_lem =
        | Id_aux (Id "bool_not", _) ->
           let [a] = args in
           let epp = align (string "~" ^^ expY a) in
-          if aexp_needed then parens (align epp) else epp
+          if aexp_needed then parens (align epp) else epp *)
        | _ ->
           begin match annot with
           | Some (env, _, _) when (is_ctor env f) ->
@@ -477,24 +505,28 @@ let doc_exp_lem, doc_let_lem =
                     parens (separate_map comma (expV false) args) in
              if aexp_needed then parens (align epp) else epp
           | _ ->
-             let call = (*match annot with
-               | Base(_,External (Some n),_,_,_,_) -> string n
-               | _ ->*) doc_id_lem f in
+             let call = match annot with
+               | Some (env, _, _) when Env.is_extern f env ->
+                 string (Env.get_extern f env)
+               | _ -> doc_id_lem f in
              let argspp = match args with
                | [arg] -> expV true arg
                | args -> parens (align (separate_map (comma ^^ break 0) (expV false) args)) in
              let epp = align (call ^//^ argspp) in
              let (taepp,aexp_needed) =
-               let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+               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)
+               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)
                else (epp, aexp_needed) in
-             if aexp_needed then parens (align taepp) else taepp
+             liftR (if aexp_needed then parens (align taepp) else taepp)
           end
        end
     | E_vector_access (v,e) ->
-       let eff = effect_of full_exp in
+      raise (Reporting_basic.err_unreachable l
+        "E_vector_access should have been rewritten before pretty-printing")
+       (* let eff = effect_of full_exp in
        let epp =
          if has_effect eff BE_rreg then
            separate space [string "read_reg_bit";expY v;expY e]
@@ -502,9 +534,11 @@ let doc_exp_lem, doc_let_lem =
            let tv = typ_of v in
            let call = if is_bitvector_typ tv then "bvaccess" else "access" in
            separate space [string call;expY v;expY e] in
-       if aexp_needed then parens (align epp) else epp
+       if aexp_needed then parens (align epp) else epp*)
     | E_vector_subrange (v,e1,e2) ->
-       let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+      raise (Reporting_basic.err_unreachable l
+        "E_vector_access 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
@@ -519,22 +553,22 @@ let doc_exp_lem, doc_let_lem =
              then (bepp ^^ doc_tannot_lem regtypes 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
+       if aexp_needed then parens (align epp) else epp *)
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
        let ft = typ_of_annot (l,fannot) in
        (match fannot with
-        | Some(env, ftyp, _) when is_regtyp ftyp env ->
-           let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
+        | Some(env, (Typ_aux (Typ_id tid, _)), _)
+        | Some(env, (Typ_aux (Typ_app (Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]), _)), _)
+          when Env.is_regtyp tid env ->
+           let t = (* Env.base_typ_of (env_of full_exp) *) (typ_of full_exp) in
            let eff = effect_of full_exp in
-           let field_f = string
-             (if is_bit_typ t
-             then "read_reg_bitfield"
-             else "read_reg_field") in
+           let field_f = string "get" ^^ underscore ^^
+             doc_id_lem tid ^^ underscore ^^ doc_id_lem id 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)
              else (empty, aexp_needed) in
-           let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in
+           let epp = field_f ^^ space ^^ (expY fexp) in
            if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
         | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env ->
            let fname =
@@ -554,9 +588,9 @@ let doc_exp_lem, doc_let_lem =
        let base_typ = Env.base_typ_of env typ in
        if has_effect eff BE_rreg then
          let epp = separate space [string "read_reg";doc_id_lem id] in
-         if contains_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
-         then parens (epp ^^ doc_tannot_lem regtypes true base_typ)
-         else epp
+         if is_bitvector_typ base_typ && not (contains_t_pp_var base_typ)
+         then liftR (parens (epp ^^ doc_tannot_lem regtypes true base_typ))
+         else liftR epp
        else if is_ctor env id then doc_id_lem_ctor id
        else doc_id_lem id
         (*| Base((_,t),Alias alias_info,_,eff,_,_) ->
@@ -592,7 +626,7 @@ let doc_exp_lem, doc_let_lem =
                     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 false lit annot
+    | E_lit lit -> doc_lit_lem regtypes false lit annot
     | E_cast(typ,e) ->
        expV aexp_needed e (*
        (match annot with
@@ -633,14 +667,14 @@ 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 recordtyp) fexps)) ^^ space) in
+                                          (doc_fexp regtypes early_ret recordtyp) fexps)) ^^ space) in
        if aexp_needed then parens epp else epp
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
        let recordtyp = match annot with
          | 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 recordtyp) fexps))
+       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes 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) =
@@ -653,7 +687,7 @@ let doc_exp_lem, doc_let_lem =
            | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])
              | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->*)
               let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
-              let start = match start with
+              let start = match simplify_nexp start with
                 | Nexp_aux (Nexp_constant i, _) -> string_of_int i
                 | _ -> if dir then "0" else string_of_int (List.length exps) in
               let expspp =
@@ -685,10 +719,10 @@ let doc_exp_lem, doc_let_lem =
         if is_vector_typ t then vector_typ_args_of t
         else raise (Reporting_basic.err_unreachable l "E_vector_indexed of non-vector type") in
        let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in
-       let start = match start with
+       let start = match simplify_nexp start with
          | Nexp_aux (Nexp_constant i, _) -> string_of_int i
          | _ -> if dir then "0" else string_of_int (List.length iexps) in
-       let size = match len with
+       let size = match simplify_nexp len with
          | Nexp_aux (Nexp_constant i, _)-> string_of_int i
          | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) ->
            string_of_int (Util.power 2 i)
@@ -769,10 +803,10 @@ 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) pexps) ^/^
+                  (separate_map (break 1) (doc_case regtypes early_ret) pexps) ^/^
                     (string "end")) in
        if aexp_needed then parens (align epp) else align epp
-    | E_exit e -> separate space [string "exit"; expY e;]
+    | E_exit e -> liftR (separate space [string "exit"; expY e;])
     | E_assert (e1,e2) ->
        let epp = separate space [string "assert'"; expY e1; expY e2] in
        if aexp_needed then parens (align epp) else align epp
@@ -889,46 +923,45 @@ let doc_exp_lem, doc_let_lem =
     | E_internal_return (e1) ->
        separate space [string "return"; expY e1;]
     | E_sizeof nexp ->
-      (match nexp with
-        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem false (L_aux (L_num i, l)) annot
+      (match simplify_nexp nexp with
+        | Nexp_aux (Nexp_constant i, _) -> doc_lit_lem regtypes false (L_aux (L_num i, l)) annot
         | _ ->
           raise (Reporting_basic.err_unreachable l
             "pretty-printing non-constant sizeof expressions to Lem not supported"))
-    | E_return _ ->
-      raise (Reporting_basic.err_todo l
-        "pretty-printing early return statements to Lem not yet supported")
+    | E_return r ->
+      align (string "early_return" ^//^ expV true r)
     | E_constraint _ | E_comment _ | E_comment_struc _ -> empty
     | 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 (LB_aux(lb,_)) = match lb with
+  and let_exp regtypes 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 false e)
+              (top_exp regtypes early_ret false e)
 
-  and doc_fexp regtypes recordtyp (FE_aux(FE_Fexp(id,e),_)) =
+  and doc_fexp regtypes 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 true e))
+    group (doc_op equals fname (top_exp regtypes early_ret true e))
 
-  and doc_case regtypes = function
+  and doc_case regtypes 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 false e)))
+                  (group (top_exp regtypes 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 ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
+  and doc_lexp_deref_lem regtypes early_ret ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_field (le,id) ->
-       parens (separate empty [doc_lexp_deref_lem regtypes le;dot;doc_id_lem id])
+       parens (separate empty [doc_lexp_deref_lem regtypes early_ret le;dot;doc_id_lem id])
     | LEXP_vector(le,e) ->
-       parens ((separate space) [string "access";doc_lexp_deref_lem regtypes le;
-                                 top_exp regtypes true e])
+       parens ((separate space) [string "access";doc_lexp_deref_lem regtypes early_ret le;
+                                 top_exp regtypes early_ret true e])
     | LEXP_id id -> doc_id_lem id
     | LEXP_cast (typ,id) -> doc_id_lem id
     | _ ->
@@ -947,10 +980,10 @@ 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,_)) = match td with
+let doc_typdef_lem regtypes (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 typschm)
+            (doc_typschm_lem regtypes false typschm)
   | TD_record(id,nm,typq,fs,_) ->
      let f_pp (typ,fid) =
        let fname = if prefix_recordtype
@@ -960,7 +993,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       let fs_doc = group (separate_map (break 1) f_pp fs) in
       doc_op equals
              (concat [string "type"; space; doc_id_lem_type id;])
-             (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space)))
+             ((*doc_typquant_lem typq*) (anglebars (space ^^ align fs_doc ^^ space)))
   | TD_variant(id,nm,typq,ar,_) ->
      (match id with
       | Id_aux ((Id "read_kind"),_) -> empty
@@ -971,13 +1004,14 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       | Id_aux ((Id "regfp"),_) -> empty
       | Id_aux ((Id "niafp"),_) -> empty
       | 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 typ_pp =
 
            (doc_op equals)
-             (concat [string "type"; space; doc_id_lem_type id;])
-             (doc_typquant_lem typq ar_doc) in
+             (concat [string "type"; space; doc_id_lem_type id; space; doc_typquant_items_lem typq])
+             ((*doc_typquant_lem typq*) ar_doc) in
          let make_id pat id =
            separate space [string "SIA.Id_aux";
                            parens (string "SIA.Id " ^^ string_lit (doc_id id));
@@ -1142,7 +1176,7 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
                 fromToInterpValuePP ^^ hardline
             else empty)
   | TD_register(id,n1,n2,rs) ->
-    match n1,n2 with
+    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
@@ -1153,25 +1187,64 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
            (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
-       (doc_op equals)
+       let vtyp = vector_typ (nconstant i1) (nconstant size) ord bit_typ in
+       let tannot = doc_tannot_lem regtypes false vtyp in
+       let doc_field (fr, fid) =
+         let i, j = match fr with
+         | BF_aux (BF_single i, _) -> (i, i)
+         | BF_aux (BF_range (i, j), _) -> (i, j)
+         | _ -> raise (Reporting_basic.err_unreachable l "unsupported field type") 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 get_"; doc_id_lem id; underscore; doc_id_lem fid;
+             space; parens (string "reg" ^^ tannot)]) (string get) ^^
+         hardline ^^
+         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)
+       ^^ 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 ^^
-         separate_map hardline doc_rfield rs *)
+       ^^ hardline ^^
+       doc_op equals
+         (concat [string "let";space;string "cast_";doc_id_lem id;space;string "reg"])
+         (string "reg")
+       ^^ hardline ^^
+       doc_op equals
+         (concat [string "let";space;string "cast_to_";doc_id_lem id;space;string "reg"])
+         (string "reg")
+       ^^ hardline ^^
+         separate_map hardline doc_field rs
 
 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)
+  | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem regtypes typ)
+
+let doc_fun_body_lem regtypes exp =
+  let early_ret = contains_early_return exp in
+  let doc_exp = doc_exp_lem regtypes 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_exp_lem regtypes false exp))
+    (doc_fun_body_lem regtypes exp))
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -1188,7 +1261,7 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
           [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
            (doc_pat_lem regtypes true pat);
            equals])
-       (doc_exp_lem regtypes false exp)
+       (doc_fun_body_lem regtypes exp)
   | _ ->
     let id = get_id fcls in
     (*    let sep = hardline ^^ pipe ^^ space in *)
@@ -1230,7 +1303,7 @@ 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 false lit a
+                 | P_lit lit -> doc_lit_lem regtypes false lit a
                  | P_id id -> doc_id_lem id
                  | _ -> string ("arg" ^ string_of_int idx) in
                let clauses =
@@ -1256,37 +1329,33 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
       
 
 
-let doc_dec_lem (DEC_aux (reg,(l,annot))) =
+let doc_dec_lem (DEC_aux (reg, ((l, _) as annot))) =
   match reg with
   | DEC_reg(typ,id) ->
+     let env = env_of_annot annot in
      (match typ with
-      | Typ_aux (Typ_app (r, [Typ_arg_aux (Typ_arg_typ rt, _)]), _)
-        when string_of_id r = "register" && is_vector_typ rt ->
-        let env = env_of_annot (l,annot) in
-        let (start, size, order, etyp) = vector_typ_args_of (Env.base_typ_of env rt) in
-        (match is_bit_typ (Env.base_typ_of env etyp), start, size with
-          | true, Nexp_aux (Nexp_constant start, _), Nexp_aux (Nexp_constant size, _) ->
-             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_int (size);
-                                       doc_int (start);
-                                       string o;
-                                       string "[]"]))
-                ^/^ hardline
-           | _ ->
-              let (Id_aux (Id name,_)) = id in
-              failwith ("can't deal with register " ^ name))
-      | Typ_aux (Typ_app(r, [Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id idt, _)), _)]), _)
-        when string_of_id r = "register" ->
-         separate space [string "let";doc_id_lem id;equals;
-                         string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
-      | Typ_aux (Typ_id idt, _) ->
-         separate space [string "let";doc_id_lem id;equals;
-                         string "build_" ^^ string (string_of_id idt);string_lit (doc_id_lem id)] ^/^ hardline
-      |_-> empty)
+      | 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)))
   | DEC_alias(id,alspec) -> empty
   | DEC_typ_alias(typ,id,alspec) -> empty
 
@@ -1306,7 +1375,7 @@ let rec doc_def_lem regtypes def = match def with
 
   | 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 lbind) ^/^ hardline)
+  | DEF_val lbind -> (empty,group (doc_let_lem regtypes false lbind) ^/^ hardline)
   | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
   | DEF_kind _ -> (empty,empty)