progress on lem backend: auto-generate read_register and write_register functions, and state definition

7 files changed, 494 insertions, 251 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 0d60efce..8048c676 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,52 +1,8 @@
 open import Pervasives
+open import State
+open import Vector
+open import Arch
 
-type M 's 'a  = <| runState : 's -> ('a * 's) |>
-
-val return : forall 's 'a. 'a -> M 's 'a
-let return a = <| runState = (fun s -> (a,s)) |>
-
-val bind : forall 's 'a 'b. M 's 'a -> ('a -> M 's 'b) -> M 's 'b
-let bind m f = <| runState = (fun s -> let (a,s) = m.runState s in (f a).runState s) |>
-
-let (>>=) = bind
-let (>>) m n = m >>= fun _ -> n
-
-(* only expected to be 0, 1, 2; 2 represents undef *)
-type bit = Zero | One | Undef
-let is_inc = true
-
-type register =
-  | CR | CR0 | CR1 
-  | CTR
-  | LR
-  | XER | XER_SO | XER_OV | XER_CA
-  | GPR0
-  | GPR1
-  | GPR2
-  | GPR3
-  | GPR4
-  | VRSAVE
-  | SPRG3
-
-type vector = Vector of list bit * nat
-
-(* auto-generate *)
-let GPR = [GPR0;GPR1;GPR2;GPR3;GPR4]
-
-(* auto-generate *)
-type state =
-  <| cr : vector;
-     ctr : vector;
-     lr : vector;
-     xer : vector;
-     gpr0 : vector;
-     gpr1 : vector;
-     gpr2 : vector;
-     gpr3 : vector;
-     gpr4 : vector;
-     vrsave : vector;
-     sprg3 : vector |>
-  
 let to_bool = function
   | Zero -> false
   | One  -> true
@@ -57,25 +13,6 @@ let get_blist (Vector bs _) = bs
 let get_start (Vector _ s) = s
 let length (Vector bs _) = length bs
 
-(* auto-generate *)
-let length_register : register -> nat = function
-  | CR -> 32
-  | CR0 -> 4
-  | CR1 -> 4
-  | CTR -> 64
-  | LR -> 64
-  | XER -> 64
-  | XER_SO -> 1
-  | XER_OV -> 1
-  | XER_CA -> 1
-  | GPR0 -> 64
-  | GPR1 -> 64
-  | GPR2 -> 64
-  | GPR3 -> 64
-  | GPR4 -> 64
-  | VRSAVE -> 32
-  | SPRG3 -> 64
-end
 
 let vector_access (Vector bs start) n =
   let (Just b) = if is_inc then List.index bs (n - start)
@@ -83,76 +20,13 @@ let vector_access (Vector bs start) n =
   b
 
 
-let read_vector_subrange (Vector bs start) n m =
-  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-  let (_,suffix) = List.splitAt offset bs in
-  let (subvector,_) = List.splitAt length suffix in
-  Vector subvector n
-
-let write_vector_subrange (Vector bs start) n m (Vector bs' _) =
-  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
-  let (prefix,_) = List.splitAt offset bs in
-  let (_,suffix) = List.splitAt (offset + length) bs in
-  Vector (prefix ++ (List.take length bs') ++ suffix) start
-
-(* auto-generate *)
-let read_register reg =
-  <| runState =
-     fun s ->
-     let v = match reg with
-       | CR -> s.cr
-       | CR0 -> read_vector_subrange s.cr 32 35
-       | CR1 -> read_vector_subrange s.cr 36 39
-       | CTR -> s.ctr
-       | LR -> s.lr
-       | XER -> s.xer
-       | XER_SO -> read_vector_subrange s.xer 32 32
-       | XER_OV -> read_vector_subrange s.xer 33 33
-       | XER_CA -> read_vector_subrange s.xer 34 34
-       | GPR0 -> s.gpr0
-       | GPR1 -> s.gpr1
-       | GPR2 -> s.gpr2
-       | GPR3 -> s.gpr3
-       | GPR4 -> s.gpr4
-       | VRSAVE -> s.vrsave
-       | SPRG3 -> s.sprg3
-     end in
-   (v,s)
-  |>
-
-    (* auto-generate *)
-let write_register reg v =
-  <| runState =
-     fun s ->
-     let s' = 
-       match reg with
-       | CR ->     <| s with cr = write_vector_subrange s.cr 32 64 v |>
-       | CR0 ->    <| s with cr = write_vector_subrange s.cr 32 35 v |>
-       | CR1 ->    <| s with cr = write_vector_subrange s.cr 36 39 v |>
-       | CTR ->    <| s with ctr = write_vector_subrange s.cr 0 64 v |>
-       | LR ->     <| s with lr = write_vector_subrange s.cr 0 64 v |>
-       | XER ->    <| s with xer = write_vector_subrange s.cr 0 64 v |>
-       | XER_SO -> <| s with xer = write_vector_subrange s.xer 32 32 v |>
-       | XER_OV -> <| s with xer = write_vector_subrange s.xer 33 33 v |>
-       | XER_CA -> <| s with xer = write_vector_subrange s.xer 34 34 v |>
-       | GPR0 ->   <| s with gpr0 = write_vector_subrange s.cr 0 64 v |>
-       | GPR1 ->   <| s with gpr1 = write_vector_subrange s.cr 0 64 v |>
-       | GPR2 ->   <| s with gpr2 = write_vector_subrange s.cr 0 64 v |>
-       | GPR3 ->   <| s with gpr3 = write_vector_subrange s.cr 0 64 v |>
-       | GPR4 ->   <| s with gpr4 = write_vector_subrange s.cr 0 64 v |>
-       | VRSAVE -> <| s with vrsave = write_vector_subrange s.vrsave 32 64 v |>
-       | SPRG3 -> <| s with sprg3 = write_vector_subrange s.vrsave 0 64 v |>
-     end in
-   ((),s')
-  |>
-
 let write_two_registers r1 r2 vec =
   let size = length_register r1 in
   let start = get_start vec in
   let vsize = length vec in
-  let r1_v = read_vector_subrange vec start ((if is_inc then size - start else start - size) - 1) in
+  let r1_v = read_vector_subrange is_inc vec start ((if is_inc then size - start else start - size) - 1) in
   let r2_v =
-    read_vector_subrange
+    read_vector_subrange is_inc
       vec (if is_inc then size - start else start - size)
       (if is_inc then vsize - start else start - vsize) in
   write_register r1 r1_v >> write_register r2 r2_v
@@ -399,15 +273,15 @@ let shift_op_vec op (((Vector bs start) as l),r) =
     match op with
      | LL (*"<<"*) ->
        let right_vec = Vector (List.replicate n Zero) 0 in
-       let left_vec = read_vector_subrange l n (if is_inc then len + start else start - len) in
+       let left_vec = read_vector_subrange is_inc l n (if is_inc then len + start else start - len) in
        vector_concat left_vec right_vec
      | RR (*">>"*) ->
-       let right_vec = read_vector_subrange l start n in
+       let right_vec = read_vector_subrange is_inc l start n in
        let left_vec = Vector (List.replicate n Zero) 0 in
        vector_concat left_vec right_vec 
      | LLL (*"<<<"*) ->
-       let left_vec = read_vector_subrange l n (if is_inc then len + start else start - len) in
-       let right_vec = read_vector_subrange l start n in
+       let left_vec = read_vector_subrange is_inc l n (if is_inc then len + start else start - len) in
+       let right_vec = read_vector_subrange is_inc l start n in
        vector_concat left_vec right_vec
      end
 
@@ -522,4 +396,3 @@ let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
 
 let neq (l,r) = bitwise_not_bit (eq (l,r))
 let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec (l,r))
-
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
new file mode 100644
index 00000000..462eeec2
--- /dev/null
+++ b/src/gen_lib/state.lem
@@ -0,0 +1,10 @@
+type M 's 'a  = <| runState : 's -> ('a * 's) |>
+
+val return : forall 's 'a. 'a -> M 's 'a
+let return a = <| runState = (fun s -> (a,s)) |>
+
+val bind : forall 's 'a 'b. M 's 'a -> ('a -> M 's 'b) -> M 's 'b
+let bind m f = <| runState = (fun s -> let (a,s) = m.runState s in (f a).runState s) |>
+
+let (>>=) = bind
+let (>>) m n = m >>= fun _ -> n
diff --git a/src/gen_lib/vector.lem b/src/gen_lib/vector.lem
new file mode 100644
index 00000000..e7b20aeb
--- /dev/null
+++ b/src/gen_lib/vector.lem
@@ -0,0 +1,16 @@
+open import Pervasives
+
+type bit = Zero | One | Undef
+type vector = Vector of list bit * nat
+
+let read_vector_subrange is_inc (Vector bs start) n m =
+  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+  let (_,suffix) = List.splitAt offset bs in
+  let (subvector,_) = List.splitAt length suffix in
+  Vector subvector n
+
+let write_vector_subrange is_inc (Vector bs start) n m (Vector bs' _) =
+  let (length,offset) = if is_inc then (m-n+1,n-start) else (n-m+1,start-n) in
+  let (prefix,_) = List.splitAt offset bs in
+  let (_,suffix) = List.splitAt (offset + length) bs in
+  Vector (prefix ++ (List.take length bs') ++ suffix) start
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 86bcb77f..db49989f 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1258,7 +1258,7 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml =
   | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
     (string "number")
   | Typ_app(id,args) ->
-      (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id)
+     (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id)
   | _ -> atomic_typ ty 
   and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_id id  -> doc_id_ocaml_type id
@@ -1791,25 +1791,149 @@ let pp_defs_ocaml f d top_line opens =
            (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ 
            (doc_defs_ocaml d))
 
+
+
 (****************************************************************************
  * PPrint-based sail-to-lem pretty printer
 ****************************************************************************)
 
+let langlebar = string "<|"
+let ranglebar = string "|>"
+let anglebars = enclose langlebar ranglebar
+
+
 let doc_id_lem (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "vbit" 
-  | Id i -> string (if i.[0] = '\'' || is_number(i.[0]) then "_" ^ i else i)
+  | Id i -> string (if i.[0] = '\'' || is_number(i.[0])
+                    then "_" ^ i else i)
   | DeIid x ->
-      (* add an extra space through empty to avoid a closing-comment
-       * token in case of x ending with star. *)
-      parens (separate space [colon; string x; empty])
+     (* add an extra space through empty to avoid a closing-comment
+      * token in case of x ending with star. *)
+     parens (separate space [colon; string x; empty])
+
+let doc_id_lem_type (Id_aux(i,_)) =
+  match i with
+  | Id("bit") -> string "vbit" 
+  | Id i -> string i
+  | DeIid x ->
+     (* add an extra space through empty to avoid a closing-comment
+      * token in case of x ending with star. *)
+     parens (separate space [colon; string x; empty])
+
+let doc_id_lem_ctor (Id_aux(i,_)) =
+  match i with
+  | Id("bit") -> string "vbit" 
+  | Id i -> string (String.capitalize i)
+  | DeIid x ->
+     (* add an extra space through empty to avoid a closing-comment
+      * token in case of x ending with star. *)
+     parens (separate space [colon; string (String.capitalize x); empty])
+
+let doc_typ_lem, doc_atomic_typ_lem =
+  (* following the structure of parser for precedence *)
+  let rec typ ty = fn_typ ty
+  and fn_typ ((Typ_aux (t, _)) as ty) = match t with
+  | Typ_fn(arg,ret,efct) ->
+      separate space [tup_typ arg; arrow; fn_typ ret]
+  | _ -> tup_typ ty
+  and tup_typ ((Typ_aux (t, _)) as ty) = match t with
+  | Typ_tup typs -> parens (separate_map star app_typ typs)
+  | _ -> app_typ ty
+  and app_typ ((Typ_aux (t, _)) 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 typ, _)]) ->
+    string "vector"
+  | Typ_app(Id_aux (Id "range", _), [
+    Typ_arg_aux(Typ_arg_nexp n, _);
+    Typ_arg_aux(Typ_arg_nexp m, _);]) ->
+    (string "number")
+  | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) ->
+    (string "number")
+  | Typ_app(id,args) ->
+      (doc_id_lem_type id) ^^ space ^^ (separate_map space doc_typ_arg_lem args)
+  | _ -> atomic_typ ty 
+  and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
+  | Typ_id id  -> doc_id_lem_type id
+  | Typ_var v  -> doc_var v
+  | Typ_wild -> underscore
+  | Typ_app _ | Typ_tup _ | Typ_fn _ ->
+      (* exhaustiveness matters here to avoid infinite loops
+       * if we add a new Typ constructor *)
+      group (parens (typ ty))
+  and doc_typ_arg_lem (Typ_arg_aux(t,_)) = match t with
+  | Typ_arg_typ t -> app_typ t
+  | Typ_arg_nexp n -> empty
+  | Typ_arg_order o -> empty
+  | Typ_arg_effect e -> empty
+  in typ, atomic_typ
+
+let doc_lit_lem in_pat (L_aux(l,_)) =
+  utf8string (match l with
+  | L_unit  -> "()"
+  | L_zero  -> "Zero"
+  | L_one   -> "One"
+  | L_true  -> "One"
+  | L_false -> "Zero"
+  | L_num i -> (* if in_pat then string_of_int i else "(big_int_of_int " ^ string_of_int i ^ ")" *) string_of_int i
+  | 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 -> "Undef"
+  | L_string s -> "\"" ^ s ^ "\"")
+
+(* typ_doc is the doc for the type being quantified *)
+let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc
+
+let doc_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  (doc_typquant tq (doc_typ_lem t))
+
+(*Note: vector concatenation, literal vectors, indexed vectors, and record should 
+  be removed prior to pp. The latter two have never yet been seen
+*)
+let doc_pat_lem =
+  let rec pat pa = app_pat pa
+  and app_pat ((P_aux(p,(l,annot))) as pa) = match p with
+    | P_app(id, ((_ :: _) as pats)) ->
+      (match annot with
+       | Base(_,Constructor _,_,_,_,_) ->
+         doc_unop (doc_id_lem_ctor id) (separate_map space pat pats)
+       | _ -> empty)
+  | P_lit lit  -> doc_lit_lem true lit
+  | P_wild -> underscore
+  | P_id id -> doc_id_lem id
+  | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_lem id])
+  | P_typ(typ,p) -> doc_op colon (pat p) (doc_typ_lem typ) 
+  | P_app(id,[]) ->
+    (match annot with
+     | Base(_,Constructor n,_,_,_,_) -> doc_id_lem_ctor id
+     | _ -> empty)
+  | P_vector pats ->
+    let non_bit_print () =
+      parens
+        (separate space [string "Vector";
+                         (separate space [squarebars (separate_map semi pat pats);
+                                          underscore;underscore])]) in
+    (match annot with
+     | Base(([],t),_,_,_,_,_) ->
+       if is_bit_vector t
+       then parens (separate space [string "Vector";
+                                    (separate space [squarebars (separate_map semi pat pats);
+                                                     underscore;underscore])])
+       else non_bit_print()
+     | _ -> non_bit_print ())
+  | P_tup pats  -> parens (separate_map comma_sp pat pats)
+  | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in lem*)
+  in pat
 
 let doc_exp_lem, doc_let_lem =
-  let rec top_exp read_registers (E_aux (e, (_,annot))) =
-    let exp = top_exp read_registers in
+  let rec top_exp (E_aux (e, (_,annot))) =
+    let exp = top_exp in
     match e with
     | E_assign((LEXP_aux(le_act,tannot) as le),e) ->
-       (match annot with
+      (match annot with
        | Base(_,(Emp_local | Emp_set),_,_,_,_) ->
          (match le_act with
           | LEXP_id _ | LEXP_cast _ ->
@@ -1818,7 +1942,7 @@ let doc_exp_lem, doc_let_lem =
           | LEXP_vector _ ->
             doc_op (string "<-") (doc_lexp_array_lem le) (exp e)
           | LEXP_vector_range _ ->
-             doc_lexp_rwrite le e)
+            doc_lexp_rwrite le e)
        | _ ->
          (match le_act with
           | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ ->
@@ -1827,14 +1951,12 @@ let doc_exp_lem, doc_let_lem =
     | E_vector_append(l,r) ->
       parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r))
     | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r)
-    | E_if(c,t,E_aux(E_block [], _)) ->
-      string "if" ^^ space ^^ string "to_bool" ^^  parens (exp c) ^/^
-      string "then" ^^ space ^^ (exp t)
     | E_if(c,t,e) ->
       parens (
-      string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^
-      string "then" ^^ space ^^ group (exp t) ^/^
-      string "else" ^^ space ^^ group (exp e))
+          (separate space [string "if";string "to_bool";parens (exp c)]) ^/^
+          (prefix 2 1 (string "then") (exp t)) ^/^
+          (prefix 2 1 (string "else") (exp e))
+        ) ^^ hardline
     | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) ->
       let var= doc_id_lem id in
       let (compare,next) = if order = Ord_inc then string "<=",string "+" else string ">=",string "-" in
@@ -1869,11 +1991,11 @@ let doc_exp_lem, doc_let_lem =
            if i >= stop then (body i; foreach_dec (i - by) stop by body) else ()
 
          *)*)
-    | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e)
+    | E_let(leb,e) -> (let_exp leb) ^^ space ^^ string "in"  ^/^ (exp e)
     | E_app(f,args) ->
       let call = match annot with
         | Base(_,External (Some n),_,_,_,_) -> string n
-        | Base(_,Constructor i,_,_,_,_) -> doc_id_ocaml_ctor i f
+        | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor f
         | _ -> doc_id_lem f in
       parens (doc_unop call (parens (separate_map comma exp args)))
     | E_vector_access(v,e) ->
@@ -1885,7 +2007,7 @@ let doc_exp_lem, doc_let_lem =
           | _ -> (string "vector_access")) in
       parens (call ^^ space ^^ exp v ^^ space ^^ exp e)
     | E_vector_subrange(v,e1,e2) ->
-      parens ((string "vector_subrange") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
+      parens ((string "read_vector_subrange") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
     | E_field((E_aux(_,(_,fannot)) as fexp),id) ->
       (match fannot with
        | Base((_,{t= Tapp("register",_)}),_,_,_,_,_) |
@@ -1905,11 +2027,11 @@ let doc_exp_lem, doc_let_lem =
       (match annot with
       | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_,_) ->
         doc_id_lem id
-      | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),_,_,_,_,_) ->
-        if read_registers
-        then string "(read_register " ^^ doc_id_lem id ^^ string ")"
-        else doc_id_lem id
-      | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_ocaml_ctor i id
+      | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),tag,_,_,_,_) ->
+         (match tag with
+          | External _ -> string "(read_register " ^^ doc_id_lem id ^^ string ")"
+          | _ -> doc_id_lem id)
+      | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor id
       | Base((_,t),Alias alias_info,_,_,_,_) ->
         (match alias_info with
          | Alias_field(reg,field) ->
@@ -1921,31 +2043,28 @@ let doc_exp_lem, doc_let_lem =
            if start = stop
            then parens (separate space [string "bit_vector_access";string reg;doc_int start])
            else parens
-               (separate space [string "vector_subrange"; string reg; doc_int start; doc_int stop])
+               (separate space [string "read_vector_subrange"; string reg; doc_int start; doc_int stop])
          | Alias_pair(reg1,reg2) ->
            parens (separate space [string "vector_concat"; string reg1; string reg2]))
       | _ -> doc_id_lem id)
-    | E_lit lit -> doc_lit_ocaml false lit
+    | E_lit lit -> doc_lit_lem false lit
     | E_cast(typ,e) ->
       (match annot with
-      | Base(_,External _,_,_,_,_) ->
-        if read_registers
-        then parens( string "read_register" ^^ space ^^ exp e)
-        else exp e
-      | _ -> (parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))))
+      | Base(_,External _,_,_,_,_) -> parens( string "read_register" ^^ space ^^ exp e)
+      | _ -> (parens (doc_op colon (group (exp e)) (doc_typ_lem typ))))
     | E_tuple exps ->
       parens (separate_map comma exp exps)
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-      braces (separate_map semi_sp doc_fexp fexps)
+      anglebars (separate_map semi_sp doc_fexp fexps)
     | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-      braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
+       anglebars (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
     | E_vector exps ->
       (match annot with
        | Base((_,t),_,_,_,_,_) ->
          match t.t with
          | Tapp("vector", [TA_nexp start; _; TA_ord order; _])
          | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) ->
-           let call = if is_bit_vector t then (string "Vvector") else (string "VvectorR") in
+           let call = string "Vector" in
            let dir,dir_out = match order.order with
              | Oinc -> true,"true"
              | _ -> false, "false" in
@@ -1996,7 +2115,7 @@ let doc_exp_lem, doc_let_lem =
   | E_list exps ->
       brackets (separate_map semi exp exps)
   | E_case(e,pexps) ->
-      let opening = separate space [string "("; string "match"; top_exp true e; string "with"] in
+      let opening = separate space [string "("; string "match"; top_exp e; string "with"] in
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rparen
   | E_exit e ->
@@ -2011,72 +2130,65 @@ let doc_exp_lem, doc_let_lem =
     separate space [string "let";
                     doc_lexp_lem true lexp; (*Rewriter/typecheck should ensure this is only cast or id*)
                     equals;
-                    string "ref";
                     exp eq_exp;
                     string "in";
                     exp in_exp]
 
   | E_internal_plet (pat,e1,e2) ->
-     (separate space [(exp e1); string ">>= fun"; doc_pat_ocaml pat;arrow]) ^/^
+     (separate space [exp e1; string ">>= fun"; doc_pat_lem pat;arrow]) ^/^
      exp e2
        
   | E_internal_return (e1) ->
      separate space [string "return"; exp e1;]
   and let_exp (LB_aux(lb,_)) = match lb with
-  | LB_val_explicit(ts,pat,e) ->
-      prefix 2 1
-        (separate space [string "let"; doc_pat_ocaml pat; equals])
-        (top_exp true e)
+  | LB_val_explicit(_,pat,e)
   | LB_val_implicit(pat,e) ->
       prefix 2 1
-        (separate space [string "let"; doc_pat_ocaml pat; equals])
-        (top_exp true e)
+        (separate space [string "let"; doc_pat_lem pat; equals])
+        (top_exp e)
 
-  and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp true e)
+  and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_lem id) (top_exp e)
 
   and doc_case (Pat_aux(Pat_exp(pat,e),_)) =
-    doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp true e))
+    doc_op arrow (separate space [pipe; doc_pat_lem pat]) (group (top_exp e))
 
   and doc_lexp_lem top_call ((LEXP_aux(lexp,(l,annot))) as le) =
-    let exp = top_exp true in
+    let exp = top_exp in
     match lexp with
-    | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (exp e)
+    | LEXP_vector(v,e) -> parens ((string "vector_access") ^^ space ^^ (doc_lexp_lem false v)) ^^ dot ^^ parens (exp e)
     | LEXP_vector_range(v,e1,e2) ->
-       parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_lem false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
-    | LEXP_field(v,id) -> (doc_lexp_lem false v) ^^ dot ^^ doc_id_ocaml id
-    | LEXP_id id
-    | LEXP_cast(_,id) ->
-       let name = doc_id_ocaml id in
-       match annot,top_call with
-       | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false
-       | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false ->
-          string "!" ^^ name
-       | _ -> name
-
+      parens ((string "read_vector_subrange") ^^ space ^^ (doc_lexp_lem false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2))
+    | LEXP_field(v,id) -> (doc_lexp_lem false v) ^^ dot ^^ doc_id_lem id
+    | LEXP_id id | LEXP_cast(_,id) ->
+      let name = doc_id_lem id in
+      match annot,top_call with
+      | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false ->
+        string "!" ^^ name
+      | _ -> name
                            
   and doc_lexp_array_lem ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with
     | LEXP_vector(v,e) ->
-       (match annot with
-        | Base((_,t),_,_,_,_,_) ->
-           let t_act = match t.t with | Tapp("reg",[TA_typ t]) | Tabbrev(_,{t=Tapp("reg",[TA_typ t])}) -> t | _ -> t in
-           (match t_act.t with
-            | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) ->
-                           parens ((string "get_barray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp false e)
-            | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp false e))
-        | _ ->
-           parens ((string "get_varray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp false e))
+      (match annot with
+       | Base((_,t),_,_,_,_,_) ->
+         let t_act = match t.t with | Tapp("reg",[TA_typ t]) | Tabbrev(_,{t=Tapp("reg",[TA_typ t])}) -> t | _ -> t in
+         (match t_act.t with
+          | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) ->
+            parens ((string "get_barray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp e)
+          | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp e))
+       | _ ->
+         parens ((string "get_varray") ^^ space ^^ doc_lexp_lem false v) ^^ dot ^^ parens (top_exp e))
     | _ -> empty
-             
+
   and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v =
-    let exp = top_exp true in
+    let exp = top_exp in
     let (is_bit,is_bitv) = match e_new_v with
       | E_aux(_,(_,Base((_,t),_,_,_,_,_))) ->
         (match t.t with
          | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) |
            Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) ->
-            (false,true)
-           | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false)
-           | _ -> (false,false))
+           (false,true)
+         | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (true,false)
+         | _ -> (false,false))
       | _ -> (false,false) in
     match lexp with
     | LEXP_vector(v,e) ->
@@ -2085,17 +2197,17 @@ let doc_exp_lem, doc_let_lem =
          dot ^^ parens (exp e))
         (exp e_new_v)
     | LEXP_vector_range(v,e1,e2) ->
-       parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^
-                 doc_lexp_lem false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
+      parens ((string (if is_bitv then "write_vector_subrange_bit" else "write_vector_subrange_v")) ^^ space ^^
+              doc_lexp_lem false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v)
     | LEXP_field(v,id) ->
-       parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^
-                 doc_lexp_lem false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v)
+      parens ((string (if is_bit then "write_register_field_bit" else "write_register_field_v")) ^^ space ^^
+              doc_lexp_lem false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v)
     | LEXP_id id | LEXP_cast (_,id) ->
       (match annot with
        | Base(_,Alias alias_info,_,_,_,_) ->
          (match alias_info with
           | Alias_field(reg,field) ->
-            parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^
+            parens ((if is_bit then string "write_register_field_bit" else string "write_register_field_v") ^^ space ^^
                     string reg ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v)
           | Alias_extract(reg,start,stop) ->
             if start = stop
@@ -2105,21 +2217,62 @@ let doc_exp_lem, doc_let_lem =
                  dot ^^ parens (doc_int start))
                 (exp e_new_v)
             else 
-              parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_v")) ^^ space ^^
+              parens ((string (if is_bitv then "write_vector_subrange_bit" else "write_vector_subrange_v")) ^^ space ^^
                       string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v)
           | Alias_pair(reg1,reg2) ->
-            parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v))              
+            parens ((string "write_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v))              
        | _ ->
-         parens (separate space [string "set_register"; doc_id_lem id; exp e_new_v]))
+         parens (separate space [string "write_register"; doc_id_lem id; exp e_new_v]))
 
   and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with
-    | LEXP_memory(id,args) -> doc_id_lem id ^^ parens (separate_map comma (top_exp true) (args@[e_new_v]))
+    | LEXP_memory(id,args) -> doc_id_lem id ^^ parens (separate_map comma top_exp (args@[e_new_v]))
 
   (* expose doc_exp and doc_let *)
-  in top_exp true, let_exp
+  in top_exp, let_exp
+
+(*TODO Upcase and downcase type and constructors as needed*)
+let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
+  | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of"; doc_typ_lem typ;]
+  | Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
+
+let rec doc_range_lem (BF_aux(r,_)) = match r with
+  | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i))
+  | 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 (TD_aux(td,_)) = match td with
+  | TD_abbrev(id,nm,typschm) ->
+      doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) (doc_typscm_lem typschm)
+  | TD_record(id,nm,typq,fs,_) ->
+      let f_pp (typ,id) = concat [doc_id_lem_type id; space; colon; doc_typ_lem typ; semi] in
+      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 fs_doc))
+  | TD_variant(id,nm,typq,ar,_) ->
+    let n = List.length ar in
+    let ar_doc = group (separate_map (break 1) doc_type_union_lem ar) in
+    doc_op equals
+      (concat [string "type"; space; doc_id_lem_type id;])
+      (if n > 246
+       then brackets (space ^^(doc_typquant_lem typq ar_doc))
+       else (doc_typquant_lem typq ar_doc))
+  | TD_enum(id,nm,enums,_) ->
+    let enums_doc = group (separate_map (break 1 ^^ pipe) doc_id_lem_ctor enums) in
+    doc_op equals
+      (concat [string "type"; space; doc_id_lem_type id;])
+      (enums_doc)
+  | TD_register(id,n1,n2,rs) -> failwith "TD_register shouldn't occur here"
+
+let doc_rec_lem (Rec_aux(r,_)) = match r with
+  | Rec_nonrec -> space
+  | Rec_rec -> space ^^ string "rec" ^^ space
+
+let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with
+  | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem typ)
 
 let doc_funcl_lem (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  group (doc_op arrow (doc_pat_ocaml pat) (doc_exp_lem exp))
+  group (doc_op arrow (doc_pat_lem pat) (doc_exp_lem exp))
 
 let get_id = function
   | [] -> failwith "FD_function with empty list"
@@ -2129,36 +2282,227 @@ let doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | [FCL_aux (FCL_Funcl(id,pat,exp),_)] ->
-     (separate space [(string "let"); (doc_rec_ocaml r); (doc_id_lem id); (doc_pat_ocaml pat); equals]) ^^ hardline ^^ (doc_exp_lem exp)
+     prefix 2 1
+            (separate space [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id);
+                             (doc_pat_lem pat);
+                             equals])
+            (doc_exp_lem exp)
   | _ ->
     let id = get_id fcls in
     let sep = hardline ^^ pipe ^^ space in
-    let clauses = separate_map sep doc_funcl_lem fcls in
-    separate space [string "let";
-                    doc_rec_ocaml r;
-                    doc_id_lem id;
-                    equals;
-                    (string "function");
-                    (hardline^^pipe);
-                    clauses]
+    let clauses = hardline ^^ pipe ^^ separate_map sep doc_funcl_lem fcls in
+    prefix 2 1
+           (separate space [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;
+                            equals;
+                            (string "function")]
+           )
+             clauses
+
 
+let doc_dec_lem (DEC_aux (reg,(l,annot))) =
+  match reg with
+  | DEC_reg(typ,id) -> failwith "DEC_reg shouldn't occur here"
+  | DEC_alias(id,alspec) -> empty (*
+        doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *)
+  | DEC_typ_alias(typ,id,alspec) -> empty (*
+        doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) *)
 
 let doc_def_lem def = group (match def with
   | DEF_default df -> empty
   | DEF_spec v_spec -> empty (*unless we want to have a separate pass to create mli files*)
-  | DEF_type t_def -> doc_typdef_ocaml t_def
+  | DEF_type t_def -> doc_typdef_lem t_def
   | DEF_fundef f_def -> doc_fundef_lem f_def
   | DEF_val lbind -> doc_let_lem lbind
-  | DEF_reg_dec dec -> doc_dec_ocaml dec
+  | DEF_reg_dec dec -> doc_dec_lem dec
   | DEF_scattered sdef -> empty (*shoulnd't still be here*)
   ) ^^ hardline
 
+
+let reg_decls defs = 
+
+  let (regtyps,typedregs,simpleregs,defs) =
+    List.fold_left
+      (fun (regtyps,typedregs,simpleregs,defs) def ->
+             match def with
+             | DEF_type (TD_aux(TD_register (Id_aux (Id name, _),n1,n2,rs),_)) ->
+                (regtyps @ [(name,(n1,n2,rs))],typedregs,simpleregs,defs)
+             | DEF_reg_dec (DEC_aux (DEC_reg(Typ_aux (Typ_id (Id_aux (Id typ,_)),_),Id_aux (Id name,_)),_)) ->
+                (regtyps,typedregs @ [(name,typ)],simpleregs,defs)
+             | DEF_reg_dec (DEC_aux (DEC_reg(_, Id_aux (Id name,_)),_)) ->
+                (regtyps,typedregs,simpleregs @ [name],defs)
+             | def -> (regtyps,typedregs,simpleregs,defs @ [def])
+      ) ([],[],[],[]) defs in
+  
+  let default name = (name,
+         Nexp_aux (Nexp_constant 0,Unknown),
+         Nexp_aux (Nexp_constant 63,Unknown),
+         name) in
+
+  let dirpp = separate space [string "let";string "is_inc";equals;string "true"] in
+
+  let reg_decls =
+    (List.map default simpleregs) @
+      List.fold_left
+      (fun acc (id,typ) ->
+       let (n1,n2,rs) = List.assoc typ regtyps in
+       let rs_decls =
+         List.map
+           (function
+             | (BF_aux (BF_range (i,j), _), Id_aux (Id name,_)) ->
+                (name, Nexp_aux (Nexp_constant i,Unknown), Nexp_aux (Nexp_constant j, Unknown),id)
+             | (BF_aux (BF_single i, _), Id_aux (Id name, _)) ->
+                (name, Nexp_aux (Nexp_constant i,Unknown), Nexp_aux (Nexp_constant i, Unknown),id)
+           ) rs in
+       acc @ ((id,n1,n2,id) :: rs_decls)
+      ) [] typedregs in
+
+  let proper_regs = (List.map snd typedregs) @ simpleregs in
+  let regs_and_fields = List.map (fun (x,_,_,_) -> x) reg_decls in
+  
+  let regspp =
+    prefix 2 1 
+           (separate space [string "type"; string "register";equals])
+           (separate_map space (fun reg -> pipe ^^ space ^^ string reg) regs_and_fields) in
+  
+  let statepp =
+    prefix 2 1
+           (separate space [string "type";string "state";equals])
+           (anglebars
+              (separate_map
+                 (semi ^^ break 1)
+                 (fun reg -> separate space [string (String.lowercase reg);colon;string "vector"])
+                 proper_regs
+              )) in
+  
+  let lengthpp = 
+    prefix 2 1
+           (separate space [string "let";string "length_register";colon;string "register";
+                            arrow;string "nat";equals;string "function"])
+           ((separate_map
+              (break 1)
+              (fun (id,n1,n2,_) ->
+               separate
+                 space
+                 [pipe;string id;arrow;
+                  string "natFromInteger" ^^
+                    parens (
+                        separate
+                          space [
+                            string "abs";
+                            parens (separate
+                                      space
+                                      [doc_nexp n2;
+                                       minus;
+                                       doc_nexp n1]);
+                            plus;string "1"]
+                      )
+                 ])
+              reg_decls
+           ) ^^ 
+           hardline ^^ 
+           string "end") in
+
+  let read_register_pp =
+    prefix
+      2 1
+      (separate space [string "let";string "read_register";string "reg";equals])
+      (enclose
+         (langlebar ^^ space) (ranglebar)
+         (prefix
+            2 1
+            (separate space [string "runState";equals])
+            (prefix 2 1
+                    ((separate space [string "fun"; string "s";arrow]) ^^ hardline ^^
+                    (separate space [string "let";string "v";equals;string "match reg with"]))
+                    ((separate_map
+                        (break 1)
+                        (fun (id,n1,n2,id2) ->
+                         separate
+                           space
+                           [pipe;
+                            string id;
+                            arrow;
+                            string "read_vector_subrange";
+                            string "is_inc";
+                            string "s." ^^ (string (String.lowercase id2));
+                            doc_nexp n1;
+                            doc_nexp n2])
+                        reg_decls
+                     ) ^^ 
+                       hardline ^^ 
+                         string "end in")
+            ) ^^ hardline ^^
+            string "(v,s)" ^^ hardline
+         )
+      )
+  in
+
+  let write_register_pp =
+    prefix
+      2 1
+      (separate space [string "let";string "write_register";string "reg";string "v";equals])
+      (enclose
+         (langlebar ^^ space) (ranglebar)
+         (prefix
+            2 1
+            (separate space [string "runState";equals])
+            (prefix 2 1
+                    ((separate space [string "fun"; string "s";arrow]) ^^ hardline ^^
+                    (separate space [string "let";string "s'";equals;string "match reg with"]))
+                    ((separate_map
+                        (break 1)
+                        (fun (id,n1,n2,id2) ->
+                         separate
+                           space
+                           [pipe;string id;arrow;
+                            (
+                              enclose
+                                (langlebar ^^ space) (space ^^ ranglebar)
+                                (separate
+                                   space
+                                   [string "s with";
+                                    string (String.lowercase id2);
+                                    equals;
+                                    string "write_vector_subrange";
+                                    string "is_inc";
+                                    string "s." ^^ string (String.lowercase id2);
+                                    doc_nexp n1;
+                                    doc_nexp n2;
+                                    string "v"])
+                            )
+                           ]
+                        )
+                        reg_decls
+                     ) ^^ 
+                       hardline ^^ 
+                         string "end in")
+            ) ^^ hardline ^^
+            string "((),s')" ^^ hardline
+         )
+      )
+  in
+
+  (separate (hardline ^^ hardline) [dirpp;regspp;statepp;lengthpp;read_register_pp;write_register_pp],defs)
+
+
 let doc_defs_lem (Defs(defs)) =
-  separate_map hardline doc_def_lem defs
-let pp_defs_lem f d top_line opens =
-  print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
-           (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ 
-           (doc_defs_lem d))
+  let (decls,defs) = reg_decls defs in
+  (decls,separate_map hardline doc_def_lem defs)
+
+
+let pp_defs_lem f_arch f d top_line opens =
+  let (decls,defs) = doc_defs_lem d in
+  print f
+        (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
+           (separate_map
+              hardline
+              (fun lib -> separate space [string "open import";string lib])
+              ("Vector" :: "State" :: "Arch" :: opens)) ^/^ defs);
+  print f_arch
+        (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
+           (separate_map
+              hardline
+              (fun lib -> separate space [string "open import";string lib]) ["Pervasives";"State";"Vector"]) ^/^ decls);
 
 
 
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 4b51db8a..43680643 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -10,4 +10,4 @@ val pat_to_string : tannot pat -> string
 val pp_lem_defs : Format.formatter -> tannot defs -> unit
 
 val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit
-val pp_defs_lem : out_channel -> tannot defs -> string -> string list -> unit
+val pp_defs_lem : out_channel -> out_channel -> tannot defs -> string -> string list -> unit
diff --git a/src/process_file.ml b/src/process_file.ml
index 135f0931..1a776cff 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -173,14 +173,21 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
 	  close_output_with_check ext_o
 	end
       | Lem_out None ->
-        let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in
-	begin Pretty_print.pp_defs_lem o defs (generated_line filename) ["Sail_values";];
-        close_output_with_check ext_o
-        end
+         let ((o1,_, _) as ext_o1) =
+           open_output_with_check_unformatted ("arch.lem") in
+         let ((o2,_, _) as ext_o2) =
+           open_output_with_check_unformatted (f' ^ "embed.lem") in
+         Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename) ["Sail_values"];
+         close_output_with_check ext_o1;
+         close_output_with_check ext_o2
       | Lem_out (Some lib) ->
-        let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in
-	Pretty_print.pp_defs_lem o defs (generated_line filename) ["Sail_values"; lib];
-        close_output_with_check ext_o
+         let ((o1,_, _) as ext_o1) =
+           open_output_with_check_unformatted ("arch.lem") in
+         let ((o2,_, _) as ext_o2) =
+           open_output_with_check_unformatted (f' ^ "embed.lem") in
+	 Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename) ["Sail_values"; lib];
+         close_output_with_check ext_o1;
+         close_output_with_check ext_o2
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
 	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"];
diff --git a/src/rewriter.ml b/src/rewriter.ml
index d6b1fb33..30b6b3fe 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -907,9 +907,6 @@ let gettype (E_aux (_,(_,a))) =
   | _ -> failwith "a_normalise doesn't support Overload"
 
     
-let dedup = List.fold_left (fun acc e -> if List.exists ((=) e) acc then acc else e :: acc) []
-
-
 let effectful_effs {effect = Eset effs} =
   List.exists
     (fun (BE_aux (be,_)) -> match be with BE_nondet | BE_unspec | BE_undef -> false | _ -> true)
@@ -919,10 +916,6 @@ let effectful eaux =
   effectful_effs (geteffs eaux)
 
 let eff_union e1 e2 = union_effects (geteffs e1) (geteffs e2)
-(*KATHY:CHANGE: Not sure why the more general effect union is bad here?*)
-(*  let {effect = Eset effs_e1} = geteffs e1 in 
-  let {effect = Eset effs_e2} = geteffs e2 in
-  {effect = Eset (dedup (effs_e1 @ effs_e2))}*)
 
 let remove_blocks_exp_alg =
 
@@ -1148,8 +1141,8 @@ and n_exp (exp : 'a exp) (k : 'a exp -> 'a exp) : 'a exp =
   | E_case (exp1,pexps) ->
      n_exp_name exp1 (fun exp1 -> 
      n_pexpL pexps (fun pexps ->
-     let geteffs (Pat_aux (_,(_,Base (_,_,_,_,{effect = Eset effs},_)))) = effs in
-     let effsum = {effect = Eset (dedup (List.flatten (List.map geteffs pexps)))} in
+     let geteffs (Pat_aux (_,(_,Base (_,_,_,_,eff,_)))) = eff in
+     let effsum = List.fold_left union_effects {effect = Eset []} (List.map geteffs pexps) in
      k (rewrap_effs effsum (E_case (exp1,pexps)))))
   | E_let (lb,body) ->
      n_lb lb (fun lb ->