Refactor printing to display the contents the [_] and to better format bit vectors

6 files changed, 186 insertions, 147 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 0633ad26..bafe8dd0 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -3,10 +3,10 @@ import Map
 import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
 import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
 open import String_extra (* for 'show' to convert nat to string) *)
+import Assert_extra (*For failwith when partiality is known to be unreachable*)
 
 open import Interp_ast
 open import Interp_utilities
-
 open import Instruction_extractor
 
 type tannot = Interp_utilities.tannot
@@ -63,7 +63,16 @@ let rec string_of_value v = match v with
     | L_string str-> "\"" ^ str ^ "\"" end)
   | V_tuple vals -> "(" ^ (list_to_string string_of_value "," vals) ^ ")"
   | V_list vals -> "[||" ^ (list_to_string string_of_value "," vals) ^ "||]"
-  | V_vector i inc vals -> "[" ^ (list_to_string string_of_value "," vals) ^ "]"
+  | V_vector i inc vals -> 
+    let default_format _ = "[" ^ (list_to_string string_of_value "," vals) ^ "]" in
+    let to_bin () = "0b" ^ (List.foldr (fun (V_lit (L_aux l _)) rst -> (match l with | L_one -> "1" | L_zero -> "0" end) ^rst) "" vals) in
+    match vals with
+      | [] -> default_format ()
+      | v::vs ->
+	match v with 
+	  | V_lit (L_aux L_zero _) -> to_bin()
+	  | V_lit (L_aux L_one _) -> to_bin()
+	  | _ -> default_format() end end
   | V_vector_sparse _ _ _ _ _ -> "sparse_vector"
   | V_record t vals ->
     "{" ^ (list_to_string (fun (id,v) -> (get_id id) ^ "=" ^ (string_of_value v)) ";" vals) ^ "}"
@@ -547,6 +556,13 @@ let rec set_in_context stack e =
     | Thunk_frame _ _ _ _ s -> set_in_context s e
 end
 
+let get_stack_state stack = 
+  match stack with
+    | Top -> Assert_extra.failwith "Top reached in extracting stack state"
+    | Hole_frame id exp top_level lenv lmem stack -> (lenv,lmem)
+    | Thunk_frame exp top_level lenv lmem stack -> (lenv,lmem)
+end
+
 let id_of_string s = (Id_aux (Id s) Unknown)
 
 (*functions for converting in progress evaluation back into expression for building current continuation*)
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 211dd015..6a72526a 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -58,6 +58,9 @@ let doc_unop symb a = prefix 2 1 symb a
 let arrow = string "->"
 let dotdot = string ".."
 let coloneq = string ":="
+let lsquarebar = string "[|"
+let rsquarebar = string "|]"
+let squarebars = enclose lsquarebar rsquarebar
 let lsquarebarbar = string "[||"
 let rsquarebarbar = string "||]"
 let squarebarbars = enclose lsquarebarbar rsquarebarbar
@@ -104,7 +107,19 @@ let doc_typ, doc_atomic_typ, doc_nexp =
   | Typ_app(id,args) ->
       (* trailing space to avoid >> token in case of nested app types *)
       (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space
-  | _ -> atomic_typ ty (* for simplicity, skip vec_typ - which is only sugar *)
+  | Typ_app(Id_aux (Id "vector", _), [
+    Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
+    Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _);
+    Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_inc, _)), _);
+    Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) ->
+    (doc_id id) ^^ 
+      (brackets (if eq_big_int n zero_big_int then doc_int m 
+	         else doc_op colon (doc_int n) (doc_int (add_big_int n (sub_big_int m unit_big_int)))))
+  | Typ_app(Id_aux (Id "range", _), [
+    Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _);
+    Typ_arg_aux(Typ_arg_nexp m, _);]) ->
+    (squarebars (if eq_big_int n zero_big_int then nexp m else doc_op colon (doc_int n) (nexp m))) 
+  | _ -> atomic_typ ty 
   and atomic_typ ((Typ_aux (t, _)) as ty) = match t with
   | Typ_id id  -> doc_id id
   | Typ_var v  -> doc_var v
@@ -222,139 +237,145 @@ let doc_pat, doc_atomic_pat =
   in pat, atomic_pat
 
 let doc_exp, doc_let =
-  let rec exp e = group (or_exp e)
-  and or_exp ((E_aux(e,_)) as expr) = match e with
+  let rec exp env e = group (or_exp env e)
+  and or_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) ->
-      doc_op (doc_id op) (and_exp l) (or_exp r)
-  | _ -> and_exp expr
-  and and_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (and_exp env l) (or_exp env r)
+  | _ -> and_exp env expr
+  and and_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) ->
-      doc_op (doc_id op) (eq_exp l) (and_exp r)
-  | _ -> eq_exp expr
-  and eq_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (eq_exp env l) (and_exp env r)
+  | _ -> eq_exp env expr
+  and eq_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
     (* XXX this is not very consistent - is the parser bogus here? *)
       "=" | "==" | "!="
     | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u"
     | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u"
     ),_) as op),r) ->
-      doc_op (doc_id op) (eq_exp l) (at_exp r)
+      doc_op (doc_id op) (eq_exp env l) (at_exp env r)
   (* XXX assignment should not have the same precedence as equal etc. *)
-  | E_assign(le,exp) -> doc_op coloneq (doc_lexp le) (at_exp exp)
-  | _ -> at_exp expr
-  and at_exp ((E_aux(e,_)) as expr) = match e with
+  | E_assign(le,exp) -> doc_op coloneq (doc_lexp env le) (at_exp env exp)
+  | _ -> at_exp env expr
+  and at_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) ->
-      doc_op (doc_id op) (cons_exp l) (at_exp r)
-  | _ -> cons_exp expr
-  and cons_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (cons_exp env l) (at_exp env r)
+  | _ -> cons_exp env expr
+  and cons_exp env ((E_aux(e,_)) as expr) = match e with
   | E_vector_append(l,r) ->
-      doc_op colon (shift_exp l) (cons_exp r)
+      doc_op colon (shift_exp env l) (cons_exp env r)
   | E_cons(l,r) ->
-      doc_op colon (shift_exp l) (cons_exp r)
-  | _ -> shift_exp expr
-  and shift_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op colon (shift_exp env l) (cons_exp env r)
+  | _ -> shift_exp env expr
+  and shift_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) ->
-      doc_op (doc_id op) (shift_exp l) (plus_exp r)
-  | _ -> plus_exp expr
-  and plus_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (shift_exp env l) (plus_exp env r)
+  | _ -> plus_exp env expr
+  and plus_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("+" | "-"),_) as op),r) ->
-      doc_op (doc_id op) (plus_exp l) (star_exp r)
-  | _ -> star_exp expr
-  and star_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (plus_exp env l) (star_exp env r)
+  | _ -> star_exp env expr
+  and star_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
       "*" | "/"
     | "div" | "quot" | "rem" | "mod"
     | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) ->
-      doc_op (doc_id op) (star_exp l) (starstar_exp r)
-  | _ -> starstar_exp expr
-  and starstar_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (star_exp env l) (starstar_exp env r)
+  | _ -> starstar_exp env expr
+  and starstar_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id "**",_) as op),r) ->
-      doc_op (doc_id op) (starstar_exp l) (app_exp r)
-  | E_if _ | E_for _ | E_let _ -> right_atomic_exp expr
-  | _ -> app_exp expr
-  and right_atomic_exp ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (starstar_exp env l) (app_exp env r)
+  | E_if _ | E_for _ | E_let _ -> right_atomic_exp env expr
+  | _ -> app_exp env expr
+  and right_atomic_exp env ((E_aux(e,_)) as expr) = match e with
   (* Special case: omit "else ()" when the else branch is empty. *)
   | E_if(c,t,E_aux(E_block [], _)) ->
-      string "if" ^^ space ^^ group (exp c) ^/^
-      string "then" ^^ space ^^ group (exp t)
+      string "if" ^^ space ^^ group (exp env c) ^/^
+      string "then" ^^ space ^^ group (exp env t)
   | E_if(c,t,e) ->
-      string "if" ^^ space ^^ group (exp c) ^/^
-      string "then" ^^ space ^^ group (exp t) ^/^
-      string "else" ^^ space ^^ group (exp e)
+      string "if" ^^ space ^^ group (exp env c) ^/^
+      string "then" ^^ space ^^ group (exp env t) ^/^
+      string "else" ^^ space ^^ group (exp env e)
   | E_for(id,exp1,exp2,exp3,order,exp4) ->
       string "foreach" ^^ space ^^
       group (parens (
         separate (break 1) [
           doc_id id;
-          string "from " ^^ atomic_exp exp1;
-          string "to " ^^ atomic_exp exp2;
-          string "by " ^^ atomic_exp exp3;
+          string "from " ^^ (atomic_exp env exp1);
+          string "to " ^^ (atomic_exp env exp2);
+          string "by " ^^ (atomic_exp env exp3);
           string "in " ^^ doc_ord order
         ]
       )) ^/^
-      exp exp4
-  | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e)
-  | _ -> group (parens (exp expr))
-  and app_exp ((E_aux(e,_)) as expr) = match e with
+	(exp env exp4)
+  | E_let(leb,e) -> doc_op (string "in") (let_exp env leb) (exp env e)
+  | _ -> group (parens (exp env expr))
+  and app_exp env ((E_aux(e,_)) as expr) = match e with
   | E_app(f,args) ->
-      doc_unop (doc_id f) (parens (separate_map comma exp args))
-  | _ -> vaccess_exp expr
-  and vaccess_exp ((E_aux(e,_)) as expr) = match e with
+      doc_unop (doc_id f) (parens (separate_map comma (exp env) args))
+  | _ -> vaccess_exp env expr
+  and vaccess_exp env ((E_aux(e,_)) as expr) = match e with
   | E_vector_access(v,e) ->
-      atomic_exp v ^^ brackets (exp e)
+    (atomic_exp env v) ^^ brackets (exp env e)
   | E_vector_subrange(v,e1,e2) ->
-      atomic_exp v ^^ brackets (doc_op dotdot (exp e1) (exp e2))
-  | _ -> field_exp expr
-  and field_exp ((E_aux(e,_)) as expr) = match e with
-  | E_field(fexp,id) -> atomic_exp fexp ^^ dot ^^ doc_id id
-  | _ -> atomic_exp expr
-  and atomic_exp ((E_aux(e,annot)) as expr) = match e with
-  (* Special case: an empty block is equivalent to unit, but { } would
-   * be parsed as a struct. *)
+    (atomic_exp env v) ^^ brackets (doc_op dotdot (exp env e1) (exp env e2))
+  | _ -> field_exp env expr
+  and field_exp env ((E_aux(e,_)) as expr) = match e with
+  | E_field(fexp,id) -> (atomic_exp env fexp) ^^ dot ^^ doc_id id
+  | _ -> atomic_exp env expr
+  and atomic_exp env ((E_aux(e,annot)) as expr) = match e with
+  (* Special case: an empty block is equivalent to unit, but { } is a syntactic struct *)
   | E_block [] -> string "()"
   | E_block exps ->
-      let exps_doc = separate_map (semi ^^ hardline) exp exps in
+      let exps_doc = separate_map (semi ^^ hardline) (exp env) exps in
       surround 2 1 lbrace exps_doc rbrace
   | E_nondet exps ->
-    let exps_doc = separate_map (semi ^^ hardline) exp exps in
+    let exps_doc = separate_map (semi ^^ hardline) (exp env) exps in
     string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
-  | E_id id -> doc_id id
+  | E_id id -> (*TODO, use env here*) doc_id id
   | E_lit lit -> doc_lit lit
   | E_cast(typ,e) ->
       if !ignore_casts then
-        atomic_exp e
+        atomic_exp env e
       else
-        prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e))
+        prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env e))
   | E_internal_cast(_,e) ->
       (* XXX ignore internal casts in the interpreter *)
-      atomic_exp e
+      atomic_exp env e
   | E_tuple exps ->
-      parens (separate_map comma exp exps)
+      parens (separate_map comma (exp env) exps)
   | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-      (* XXX E_record is not handled by parser currently
-         AAA I don't think the parser can handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *)
-      braces (separate_map semi_sp doc_fexp fexps)
+      braces (separate_map semi_sp (doc_fexp env) fexps)
   | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
-      braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps))
+      braces (doc_op (string "with") (exp env e) (separate_map semi_sp (doc_fexp env) fexps))
   | E_vector exps ->
-      brackets (separate_map comma exp exps)
+    let default_print _ = brackets (separate_map comma (exp env) exps) in
+    (match exps with
+      | [] -> default_print ()
+      | E_aux(e,_)::es ->
+	(match e with
+	  | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) ->
+	    utf8string
+	      ("0b" ^ 
+	       (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps "")) 
+	  | _ -> default_print ()))
   | E_vector_indexed (iexps, default) ->
       (* XXX TODO print default when it is non-empty *)
-      let iexp (i,e) = doc_op equals (doc_int i) (exp e) in
+      let iexp (i,e) = doc_op equals (doc_int i) (exp env e) in
       brackets (separate_map comma iexp iexps)
   | E_vector_update(v,e1,e2) ->
-      brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2)))
+      brackets (doc_op (string "with") (exp env v) (doc_op equals (atomic_exp env e1) (exp env e2)))
   | E_vector_update_subrange(v,e1,e2,e3) ->
       brackets (
-        doc_op (string "with") (exp v)
-        (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3)))
+        doc_op (string "with") (exp env v)
+        (doc_op equals ((atomic_exp env e1) ^^ colon ^^ (atomic_exp env e2)) (exp env e3)))
   | E_list exps ->
-      squarebarbars (separate_map comma exp exps)
+      squarebarbars (separate_map comma (exp env) exps)
   | E_case(e,pexps) ->
-      let opening = separate space [string "switch"; exp e; lbrace] in
-      let cases = separate_map (break 1) doc_case pexps in
+      let opening = separate space [string "switch"; exp env e; lbrace] in
+      let cases = separate_map (break 1) (doc_case env) pexps in
       surround 2 1 opening cases rbrace
-  | E_exit e -> separate space [string "exit"; exp e;]
+  | E_exit e -> separate space [string "exit"; exp env e;]
   (* adding parens and loop for lower precedence *)
   | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
   | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
@@ -376,10 +397,10 @@ let doc_exp, doc_let =
     | "*_s" | "*_si" | "*_u" | "*_ui"
     | "**"), _))
     , _) ->
-      group (parens (exp expr))
+      group (parens (exp env expr))
   (* XXX fixup deinfix into infix ones *)
   | E_app_infix(l, (Id_aux((DeIid op), annot')), r) ->
-      group (parens (exp (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot))))
+      group (parens (exp env (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot))))
   (* XXX default precedence for app_infix? *)
   | E_app_infix(l,op,r) ->
       failwith ("unexpected app_infix operator " ^ (pp_format_id op))
@@ -387,40 +408,40 @@ let doc_exp, doc_let =
   (* XXX missing case *)
   | E_internal_exp _ -> assert false
 
-  and let_exp (LB_aux(lb,_)) = match lb with
+  and let_exp env (LB_aux(lb,_)) = match lb with
   | LB_val_explicit(ts,pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals])
-        (exp e)
+        (exp env e)
   | LB_val_implicit(pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_atomic_pat pat; equals])
-        (exp e)
+        (exp env e)
 
-  and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e)
+  and doc_fexp env (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp env e)
 
-  and doc_case (Pat_aux(Pat_exp(pat,e),_)) =
-    doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp e))
+  and doc_case env (Pat_aux(Pat_exp(pat,e),_)) =
+    doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env e))
 
   (* lexps are parsed as eq_exp - we need to duplicate the precedence
    * structure for them *)
-  and doc_lexp le = app_lexp le
-  and app_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args)
-  | _ -> vaccess_lexp le
-  and vaccess_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_vector(v,e) -> atomic_lexp v ^^ brackets (exp e)
+  and doc_lexp env le = app_lexp env le
+  and app_lexp env ((LEXP_aux(lexp,_)) as le) = match lexp with
+  | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env) args)
+  | _ -> vaccess_lexp env le
+  and vaccess_lexp env ((LEXP_aux(lexp,_)) as le) = match lexp with
+  | LEXP_vector(v,e) -> (atomic_lexp env v) ^^ brackets (exp env e)
   | LEXP_vector_range(v,e1,e2) ->
-      atomic_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2)
-  | _ -> field_lexp le
-  and field_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_field(v,id) -> atomic_lexp v ^^ dot ^^ doc_id id
-  | _ -> atomic_lexp le
-  and atomic_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with
+      (atomic_lexp env v) ^^ brackets ((exp env e1) ^^ dotdot ^^ (exp env e2))
+  | _ -> field_lexp env le
+  and field_lexp env ((LEXP_aux(lexp,_)) as le) = match lexp with
+  | LEXP_field(v,id) -> (atomic_lexp env v) ^^ dot ^^ doc_id id
+  | _ -> atomic_lexp env le
+  and atomic_lexp env ((LEXP_aux(lexp,_)) as le) = match lexp with
   | LEXP_id id -> doc_id id
   | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id)
   | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _
-  | LEXP_field _ -> group (parens (doc_lexp le))
+  | LEXP_field _ -> group (parens (doc_lexp env le))
 
   (* expose doc_exp and doc_let *)
   in exp, let_exp
@@ -496,15 +517,15 @@ let doc_effects_opt (Effect_opt_aux(e,_)) = match e with
   | Effect_opt_pure -> string "pure"
   | Effect_opt_effect e -> doc_effects e
 
-let doc_funcl (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp exp))
+let doc_funcl env (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+  group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env exp))
 
-let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+let doc_fundef env (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | _ ->
       let sep = hardline ^^ string "and" ^^ space in
-      let clauses = separate_map sep doc_funcl fcls in
+      let clauses = separate_map sep (doc_funcl env) fcls in
       separate space [string "function";
         doc_rec r ^^ doc_tannot_opt typa;
         string "effect"; doc_effects_opt efa;
@@ -513,7 +534,7 @@ let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) =
 let doc_dec (DEC_aux(DEC_reg(typ,id),_)) =
   separate space [string "register"; doc_atomic_typ typ; doc_id id]
 
-let doc_scattered (SD_aux (sdef, _)) = match sdef with
+let doc_scattered env (SD_aux (sdef, _)) = match sdef with
  | SD_scattered_function (r, typa, efa, id) ->
      separate space [
        string "scattered function";
@@ -525,29 +546,29 @@ let doc_scattered (SD_aux (sdef, _)) = match sdef with
        (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns)
        (doc_typquant tq empty)
  | SD_scattered_funcl funcl ->
-     string "function clause" ^^ space ^^ doc_funcl funcl
+     string "function clause" ^^ space ^^ doc_funcl env funcl
  | SD_scattered_unioncl (id, tu) ->
      separate space [string "union"; doc_id id;
      string "member"; doc_type_union tu]
  | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id
 
-let doc_def def = group (match def with
+let doc_def env def = group (match def with
   | DEF_default df -> doc_default df
   | DEF_spec v_spec -> doc_spec v_spec
   | DEF_type t_def -> doc_typdef t_def
-  | DEF_fundef f_def -> doc_fundef f_def
-  | DEF_val lbind -> doc_let lbind
+  | DEF_fundef f_def -> doc_fundef env f_def
+  | DEF_val lbind -> doc_let env lbind
   | DEF_reg_dec dec -> doc_dec dec
-  | DEF_scattered sdef -> doc_scattered sdef
+  | DEF_scattered sdef -> doc_scattered env sdef
   ) ^^ hardline
 
-let doc_defs (Defs(defs)) =
-  separate_map hardline doc_def defs
+let doc_defs env (Defs(defs)) =
+  separate_map hardline (doc_def env) defs
 
 let print ?(len=80) channel doc = ToChannel.pretty 1. len channel doc
 let to_buf ?(len=80) buf doc = ToBuffer.pretty 1. len buf doc
 
-let pp_exp e =
+let pp_exp env e =
   let b = Buffer.create 20 in
-  to_buf b (doc_exp e);
+  to_buf b (doc_exp env e);
   Buffer.contents b
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 8aaf3ee9..b7334d17 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -124,12 +124,12 @@ let rec val_to_string_internal = function
  | Interp.V_unknown -> "unknown"
 ;;
 
-let rec top_frame_exp = function
+let rec top_frame_exp_state = function
   | Interp.Top -> raise (Invalid_argument "top_frame_exp")
-  | Interp.Hole_frame(_, e, _, _, _, Top)
-  | Interp.Thunk_frame(e, _, _, _, Top) -> e
+  | Interp.Hole_frame(_, e, _, env, mem, Top)
+  | Interp.Thunk_frame(e, _, env, mem, Top) -> (e,(env,mem))
   | Interp.Thunk_frame(_, _, _, _, s)
-  | Interp.Hole_frame(_, _, _, _, _, s) -> top_frame_exp s
+  | Interp.Hole_frame(_, _, _, _, _, s) -> top_frame_exp_state s
 
 let tunk = Unknown, None
 let ldots = E_aux(E_id (Id_aux (Id "...", Unknown)), tunk)
@@ -175,8 +175,8 @@ let rec compact_exp (E_aux (e, l)) =
  * the top of the stack is the head of the returned list. *)
 let rec compact_stack ?(acc=[]) = function
   | Interp.Top -> acc
-  | Interp.Hole_frame(_,e,_,_,_,s)
-  | Interp.Thunk_frame(e,_,_,_,s) -> compact_stack ~acc:((compact_exp e) :: acc) s
+  | Interp.Hole_frame(_,e,_,env,mem,s)
+  | Interp.Thunk_frame(e,_,env,mem,s) -> compact_stack ~acc:(((compact_exp e),(env,mem)) :: acc) s
 ;;  
 
 let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
@@ -218,16 +218,17 @@ let yellow = color true 3
 let blue = color true 4
 let grey = color false 7
 
-let exp_to_string e = Pretty_interp.pp_exp e
+let exp_to_string env e = Pretty_interp.pp_exp env e
 
 let get_loc (E_aux(_, (l, (_ : tannot)))) = loc_to_string l
-let print_exp printer e =
-  printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp e) ^ "\n")
+let print_exp printer env e =
+  printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env e) ^ "\n")
 
 let instruction_state_to_string stack =
-  List.fold_right (fun e es -> (exp_to_string e) ^ "\n" ^ es) (compact_stack stack) ""
+  let env = () in
+  List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env e) ^ "\n" ^ es) (compact_stack stack) ""
 
-let top_instruction_state_to_string stack = exp_to_string (top_frame_exp stack)
+let top_instruction_state_to_string stack = let (exp,(env,_)) = top_frame_exp_state stack in exp_to_string env exp
 
 let instr_parm_to_string (name, typ, value) = 
   name ^"="^
@@ -250,6 +251,6 @@ let rec instr_parms_to_string ps =
 let instruction_to_string (name, parms, base_effects) = 
   (String.lowercase name) ^ " " ^ instr_parms_to_string parms 
 
-let print_backtrace_compact printer stack = List.iter (print_exp printer) (compact_stack stack)
-let print_continuation printer stack = print_exp printer (top_frame_exp stack)
+let print_backtrace_compact printer stack = List.iter (fun (e,(env,mem)) -> print_exp printer env e) (compact_stack stack)
+let print_continuation printer stack = let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env e
 let print_instruction printer instr = printer (instruction_to_string instr)
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index c101ce83..73150f93 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -17,7 +17,7 @@ val reg_name_to_string : reg_name -> string
 (* format the register dependencies *)
 val dependencies_to_string : reg_name list -> string
 (* formats an expression, using interp_pretty *)
-val exp_to_string : tannot exp -> string
+val exp_to_string : Interp.lenv -> tannot exp -> string
 
 (* Functions to set the color of parts of the output *)
 val red : string -> string
@@ -29,7 +29,7 @@ val grey : string -> string
 
 (*Functions to modify the instruction state and expression used in printing and in run_model*)
 val compact_exp : tannot exp -> tannot exp
-val top_frame_exp : instruction_state -> tannot exp
+val top_frame_exp_state : instruction_state -> (tannot exp * (Interp.lenv*Interp.lmem))
 
 
 (*functions to format events and instruction_states to strings *)
@@ -43,7 +43,7 @@ val top_instruction_state_to_string : instruction_state -> string
 val instruction_to_string : instruction -> string
 
 (*Functions to take a print function and cause a print event for the above functions *)
-val print_exp : (string-> unit) -> tannot exp -> unit 
+val print_exp : (string-> unit) -> Interp.lenv -> tannot exp -> unit 
 val print_backtrace_compact : (string -> unit) -> instruction_state -> unit
 val print_continuation : (string -> unit) -> instruction_state -> unit
 val print_instruction : (string -> unit) -> instruction -> unit
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index a54dc6e1..c9244938 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -99,12 +99,12 @@ let rec val_to_string_internal = function
  | V_unknown -> "unknown"
 ;;
 
-let rec top_frame_exp = function
+let rec top_frame_exp_state = function
   | Top -> raise (Invalid_argument "top_frame_exp")
-  | Hole_frame(_, e, _, _, _, Top)
-  | Thunk_frame(e, _, _, _, Top) -> e
+  | Hole_frame(_, e, _, env, mem, Top) 
+  | Thunk_frame(e, _, env, mem, Top) -> (e,(env,mem))
   | Thunk_frame(_, _, _, _, s)
-  | Hole_frame(_, _, _, _, _, s) -> top_frame_exp s
+  | Hole_frame(_, _, _, _, _, s) -> top_frame_exp_state s
 
 let tunk = Unknown, None
 let ldots = E_aux(E_id (Id_aux (Id "...", Unknown)), tunk)
@@ -150,8 +150,8 @@ let rec compact_exp (E_aux (e, l)) =
  * the top of the stack is the head of the returned list. *)
 let rec compact_stack ?(acc=[]) = function
   | Top -> acc
-  | Hole_frame(_,e,_,_,_,s)
-  | Thunk_frame(e,_,_,_,s) -> compact_stack ~acc:((compact_exp e) :: acc) s
+  | Hole_frame(_,e,_,env,mem,s)
+  | Thunk_frame(e,_,env,mem,s) -> compact_stack ~acc:(((compact_exp e),(env,mem)) :: acc) s
 ;;  
 
 let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
@@ -324,8 +324,8 @@ let run
   ?mode
   (name, test) =
   let get_loc (E_aux(_, (l, _))) = loc_to_string l in
-  let print_exp  e =
-    debugf "%s: %s\n" (get_loc e) (Pretty_interp.pp_exp e) in
+  let print_exp env e =
+    debugf "%s: %s\n" (get_loc e) (Pretty_interp.pp_exp env e) in
   (* interactive loop for step-by-step execution *)
   let usage = "Usage:
     step    go to next action [default]
@@ -351,11 +351,12 @@ let run
         Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) mem;
         interact mode env stack
     | "bt" | "backtrace" | "stack" ->
-        List.iter print_exp (compact_stack stack);
+        List.iter (fun (e,(env,mem)) -> print_exp env e) (compact_stack stack);
         interact mode env stack
     | "c" | "cont" | "continuation" ->
         (* print not-compacted continuation *)
-        print_exp (top_frame_exp stack);
+      let (e,(lenv,lmem)) = top_frame_exp_state stack in
+        print_exp lenv e;
         interact mode env stack
     | "show_casts" ->
         Pretty_interp.ignore_casts := false;
@@ -372,12 +373,12 @@ let run
       debugf "%s: %s %s\n" (grey name) (blue "return") (val_to_string_internal v);
       true, mode, env
   | Action (a, s) ->
-      let top_exp = top_frame_exp s in
+      let (top_exp,(top_env,top_mem)) = top_frame_exp_state s in
       let loc = get_loc (compact_exp top_exp) in
       let return, env' = perform_action env a in
       let step ?(force=false) () =
         if mode = Step || force then begin
-          debugf "%s\n" (Pretty_interp.pp_exp top_exp);
+          debugf "%s\n" (Pretty_interp.pp_exp top_env top_exp);
           interact mode env s
        end else
          mode in
@@ -428,7 +429,7 @@ let run
   | Error(l, e) ->
       debugf "%s: %s: %s\n" (grey (loc_to_string l)) (red "error") e;
       false, mode, env in
-  debugf "%s: %s %s\n" (grey name) (blue "evaluate") (Pretty_interp.pp_exp entry);
+  debugf "%s: %s %s\n" (grey name) (blue "evaluate") (Pretty_interp.pp_exp Interp.eenv entry);
   let mode = match mode with
   | None -> if eager_eval then Run else Step
   | Some m -> m in
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index fe547201..f5f4b090 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -238,10 +238,10 @@ let run
     (false, mode, !track_dependencies, env) 
   | action ->
     let step ?(force=false) stack =
-      let top_exp = top_frame_exp stack in
+      let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in
       let loc = get_loc (compact_exp top_exp) in
       if mode = Step || force then begin
-        debugf "%s\n" (Pretty_interp.pp_exp top_exp);
+        debugf "%s\n" (Pretty_interp.pp_exp top_env top_exp);
         interact mode env stack
       end else
         mode in
@@ -313,8 +313,8 @@ let run
   let context = build_context spec in
   let initial_state = initial_instruction_state context main_func parameters in
   let imode = make_mode eager_eval !track_dependencies in
-  let top_exp = top_frame_exp initial_state in
-  debugf "%s: %s %s\n" (grey name) (blue "evaluate") (Pretty_interp.pp_exp top_exp);
+  let (top_exp,(top_env,top_mem)) = top_frame_exp_state initial_state in
+  debugf "%s: %s %s\n" (grey name) (blue "evaluate") (Pretty_interp.pp_exp top_env top_exp);
   try
     Printexc.record_backtrace true;
     loop mode (reg, mem) (interp0 imode initial_state)