interpreter: optionally print debugging traces

4 files changed, 421 insertions, 71 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b09991dc..58874fa6 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -45,6 +45,7 @@ import Map
 import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
 import Set_extra (* For 'to_list' because map only goes to set *)
 import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
+open import Show
 open import Show_extra (* for 'show' to convert nat to string) *)
 open import String_extra (* for chr *)
 import Assert_extra (*For failwith when partiality is known to be unreachable*)
@@ -54,6 +55,15 @@ open import Interp_ast
 open import Interp_utilities
 open import Instruction_extractor
 
+(* TODO: upstream into Lem *)
+val stringFromTriple : forall 'a 'b 'c. ('a -> string) -> ('b -> string) -> ('c -> string) -> ('a * 'b * 'c) -> string
+let stringFromTriple showX showY showZ (x,y,z) =
+  "(" ^ showX x ^ ", " ^ showY y ^ ", " ^ showZ z ^ ")"
+
+instance forall 'a 'b 'c. Show 'a, Show 'b, Show 'c => (Show ('a * 'b * 'c))
+  let show = stringFromTriple show show show
+end
+
 val debug_print : string -> unit
 declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
 
@@ -172,18 +182,21 @@ let rec debug_print_value v = match v with
   | V_record t vals ->
      let ppidval (id,v) = "(" ^ (get_id id) ^ "," ^ debug_print_value v ^ ")" in
      "V_record t [" ^ debug_print_value_list (List.map ppidval vals) ^ "]"
-  | V_ctor id t k vals ->
+  | V_ctor id t k v' ->
      "V_ctor " ^ (get_id id) ^ " t " ^
        (match k with | C_Enum n -> "(C_Enum " ^ show n ^ ")"
                      | C_Union -> "C_Union" end) ^
-         "(" ^ debug_print_value v ^ ")"
+         "(" ^ debug_print_value v' ^ ")"
   | V_unknown -> "V_unknown"
   | V_register r -> "V_register (" ^ string_of_reg_form r ^ ")"
   | V_register_alias _ _ -> "V_register_alias _ _"
   | V_track v rs -> "V_track (" ^ debug_print_value v ^ ") _"
   end
-                                   
-                                   
+
+instance (Show value)
+  let show v = debug_print_value v
+end
+
 let rec {coq;ocaml} id_value_eq strict (i, v) (i', v') = i = i' && value_eq strict v v'
 and value_eq strict left right =
   match (left, right) with
@@ -302,12 +315,20 @@ end
 let env_to_string (LEnv c env) =
   "(LEnv " ^ show c ^ " [" ^
   (list_to_string ", " (fun (k,v) -> k ^ " -> " ^ (string_of_value v)) (Map_extra.toList env)) ^
-  "])"
+    "])"
+
+instance (Show lenv)
+  let show env = env_to_string env
+end
 
 let mem_to_string (LMem f c mem _) =
   "(LMem " ^ f ^ " " ^ show c ^
   " [" ^ (list_to_string ", " (fun (k,v) -> show k ^ " -> " ^ (string_of_value v)) (Map_extra.toList mem)) ^ "])"
 
+instance (Show lmem)
+  let show mem = mem_to_string mem
+end
+
 type sub_reg_map = map string index_range
 
 (*top_level is a tuple of 
@@ -327,6 +348,7 @@ type top_level =
         * map string typ (*typedef union constructors *)
         * map string sub_reg_map (*sub register mappings*)
         * map string (alias_spec tannot) (*register aliases*)
+        * bool (* debug? *)
 
 type action = 
  | Read_reg of reg_form * maybe (nat * nat)
@@ -363,10 +385,246 @@ type outcome =
  | Action of action * stack
  | Error of l * string 
 
-type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool|>
+let string_of_id id' =
+  (match id' with
+   | Id_aux id _ ->
+      (match id with
+       | Id s -> s
+       | DeIid s -> s
+       end)
+   end)
+
+instance (Show id)
+  let show = string_of_id
+end
+
+let string_of_kid kid' =
+  (match kid' with
+   | Kid_aux kid _ ->
+     (match kid with
+      | Var s -> s
+      end)
+   end)
+
+instance (Show kid)
+  let show = string_of_kid
+end
+
+let string_of_reg_id (RI_aux (RI_id id ) _) = string_of_id id
+
+instance forall 'a. (Show reg_id 'a)
+  let show = string_of_reg_id
+end
+
+let rec string_of_typ typ' =
+  (match typ' with
+   | Typ_aux typ _ ->
+      (match typ with
+       | Typ_wild -> "(Typ_wild)"
+       | Typ_id id -> "(Typ_id " ^ (string_of_id id) ^ ")"
+       | Typ_var kid -> "(Typ_var " ^ (string_of_kid kid) ^ ")"
+       | Typ_fn typ1 typ2 eff -> "(Typ_fn _ _ _)"
+       | Typ_tup typs -> "(Typ_tup [" ^ String.concat "; " (List.map string_of_typ typs) ^ "])"
+       | Typ_app id args -> "(Typ_app " ^ string_of_id id ^ " _)"
+       end)
+   end)
+
+instance (Show typ)
+  let show = string_of_typ
+end
+
+let rec string_of_lexp l' =
+  (match l' with
+   | LEXP_aux l _ ->
+      (match l with
+       | LEXP_id id -> "(LEXP_id " ^ string_of_id id ^ ")"
+       | LEXP_memory id exps -> "(LEXP_memory " ^ string_of_id id ^ " _)"
+       | LEXP_cast typ id -> "(LEXP_cast " ^ string_of_typ typ ^ " " ^ string_of_id id ^ ")"
+       | LEXP_tup lexps -> "(LEXP_tup [" ^ String.concat "; " (List.map string_of_lexp lexps) ^ "])"
+       | LEXP_vector lexps exps -> "(LEXP_vector _ _)"
+       | LEXP_vector_range lexp exp1 exp2 -> "(LEXP_vector_range _ _ _)"
+       | LEXP_field lexp id -> "(LEXP_field " ^ string_of_lexp lexp ^ "." ^ string_of_id id ^ ")"
+       end)
+   end)
+
+instance forall 'a. (Show lexp 'a)
+  let show = string_of_lexp
+end
+
+let string_of_lit l' =
+  (match l' with
+   | L_aux l _ ->
+      (match l with
+       | L_unit -> "()"
+       | L_zero -> "0"
+       | L_one -> "1"
+       | L_true -> "true"
+       | L_false -> "false"
+       | L_num n -> "0d" ^ (show n)
+       | L_hex s -> "0x" ^ s
+       | L_bin s -> "0b" ^ s
+       | L_undef -> "undef"
+       | L_string s -> "\"" ^ s ^ "\""
+       end)
+   end)
+
+instance (Show lit)
+  let show = string_of_lit
+end
+
+let string_of_order o' =
+  (match o' with
+   | Ord_aux o _ ->
+      (match o with
+       | Ord_var kid -> string_of_kid kid
+       | Ord_inc -> "inc"
+       | Ord_dec -> "dec"
+       end)
+   end)
+
+instance (Show order)
+  let show = string_of_order
+end
+
+let rec string_of_exp e' =
+  (match e' with
+   | E_aux e _ ->
+      (match e with
+       | E_block exps -> "(E_block [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_nondet exps -> "(E_nondet [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_id id -> "(E_id \"" ^ string_of_id id ^ "\")"
+       | E_lit lit -> "(E_lit " ^ string_of_lit lit ^ ")"
+       | E_cast typ exp -> "(E_cast " ^ string_of_typ typ ^ " " ^ string_of_exp exp ^ ")"
+       | E_app id exps -> "(E_app " ^ string_of_id id ^ " [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_app_infix exp1 id exp2 -> "(E_app_infix " ^ string_of_exp exp1 ^ " " ^ string_of_id id ^ " " ^ string_of_exp exp2 ^ ")"
+       | E_tuple exps -> "(E_tuple [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_if cond thn els -> "(E_if " ^ (string_of_exp cond) ^ " ? " ^ (string_of_exp thn) ^ " : " ^ (string_of_exp els) ^ ")"
+       | E_for id from to_ by order exp -> "(E_for " ^ string_of_id id ^ " " ^ string_of_exp from ^ " " ^ string_of_exp to_ ^ " " ^ string_of_exp by ^ " " ^ string_of_order order ^ " " ^ string_of_exp exp ^ ")"
+       | E_vector exps -> "(E_vector [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_vector_indexed _ _ -> "(E_vector_indexed)"
+       | E_vector_access exp1 exp2 -> "(E_vector_access " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ ")"
+       | E_vector_subrange exp1 exp2 exp3 -> "(E_vector_subrange " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ " " ^ string_of_exp exp3 ^ ")"
+       | E_vector_update _ _ _ -> "(E_vector_update)"
+       | E_vector_update_subrange _ _ _ _ -> "(E_vector_update_subrange)"
+       | E_vector_append exp1 exp2 -> "(E_vector_append " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ ")"
+       | E_list exps -> "(E_list [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_cons exp1 exp2 -> "(E_cons " ^ string_of_exp exp1 ^ " :: " ^ string_of_exp exp2 ^ ")"
+       | E_record _ -> "(E_record)"
+       | E_record_update _ _ -> "(E_record_update)"
+       | E_field _ _ -> "(E_field)"
+       | E_case _ _ -> "(E_case)"
+       | E_let _ _ -> "(E_let)"
+       | E_assign lexp exp -> "(E_assign " ^ string_of_lexp lexp ^ " := " ^ string_of_exp exp ^ ")"
+       | E_sizeof _ -> "(E_sizeof _)"
+       | E_exit exp -> "(E_exit " ^ string_of_exp exp ^ ")"
+       | E_return exp -> "(E_return " ^ string_of_exp exp ^ ")"
+       | E_assert cond msg -> "(E_assert " ^ string_of_exp cond ^ " " ^ string_of_exp msg ^ ")"
+       | E_internal_cast _ _ -> "(E_internal_cast _ _)"
+       | E_internal_exp _ -> "(E_internal_exp _)"
+       | E_sizeof_internal _ -> "(E_size _)"
+       | E_internal_exp_user _ _ -> "(E_internal_exp_user _ _)"
+       | E_comment _ -> "(E_comment _)"
+       | E_comment_struc _ -> "(E_comment_struc _)"
+       | E_internal_let _ _ _ -> "(E_internal_let _ _ _)"
+       | E_internal_plet _ _ _ -> "(E_internal_plet _ _ _)"
+       | E_internal_return _ -> "(E_internal_return _)"
+       | E_internal_value value -> "(E_internal_value " ^ debug_print_value value ^ ")"
+       end)
+   end)
+
+instance forall 'a. (Show (exp 'a))
+  let show = string_of_exp
+end
+
+let string_of_alias_spec (AL_aux _as _) =
+  (match _as with
+   | AL_subreg reg_id id -> "(AL_subreg " ^ (show reg_id) ^ " " ^ (show id) ^ ")"
+   | AL_bit reg_id exp -> "(AL_bit " ^ (show reg_id) ^ " " ^ (show exp) ^ ")"
+   | AL_slice reg_id exp1 exp2 -> "(AL_slice " ^ (show reg_id) ^ " " ^ (show exp1) ^ " " ^ (show exp2) ^ ")"
+   | AL_concat reg_id1 reg_id2 -> "(AL_concat " ^ (show reg_id1) ^ " " ^ (show reg_id2) ^ ")"
+   end)
+
+instance forall 'a. (Show alias_spec 'a)
+  let show = string_of_alias_spec
+end
+
+let string_of_quant_item (QI_aux qi _) =
+  (match qi with
+   | QI_id kinded_id -> "(QI_id _)"
+   | QI_const nc -> "(QI_const _)"
+   end)
+
+instance (Show quant_item)
+  let show = string_of_quant_item
+end
+
+let string_of_typquant (TypQ_aux tq _) =
+  (match tq with
+   | TypQ_tq qis -> "(TypQ_tq [" ^ (String.concat "; " (List.map show qis)) ^ "]"
+   | TypQ_no_forall -> "TypQ_no_forall"
+   end)
+
+instance (Show typquant)
+  let show = string_of_typquant
+end
+
+let string_of_typschm (TypSchm_aux (TypSchm_ts typquant typ) _) =
+  "(TypSchm " ^ (show typquant) ^ " " ^ (show typ) ^ ")"
+
+instance (Show typschm)
+  let show = string_of_typschm
+end
+
+let rec string_of_pat (P_aux pat _) =
+  (match pat with
+   | P_lit lit -> "(P_lit " ^ show lit ^ ")"
+   | P_wild -> "P_wild"
+   | P_as pat' id -> "(P_as " ^ string_of_pat pat' ^ " " ^ show id ^ ")"
+   | P_typ typ pat' -> "(P_typ" ^ show typ ^ " " ^ string_of_pat pat' ^ ")"
+   | P_id id -> "(P_id " ^ show id ^ ")"
+   | P_app id pats -> "(P_app " ^ show id ^ " [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_record _ _ -> "(P_record _ _)"
+   | P_vector pats -> "(P_vector [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_vector_indexed _ -> "(P_vector_indexed _)"
+   | P_vector_concat pats -> "(P_vector_concat [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_tup pats -> "(P_tup [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_list pats -> "(P_list [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   end)
+
+instance forall 'a. (Show pat 'a)
+  let show = string_of_pat
+end
+
+let string_of_letbind (LB_aux lb _) =
+  (match lb with
+   | LB_val_explicit ts pat exp -> "(LB_val_explicit " ^ (show ts) ^ " " ^ (show pat) ^ " " ^ (show exp) ^ ")"
+   | LB_val_implicit pat exp -> "(LB_val_implicit " ^ (show pat) ^ " " ^ (show exp) ^ ")"
+   end)
+
+instance forall 'a. (Show letbind 'a)
+  let show = string_of_letbind
+end
+
+type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool; debug : bool; debug_indent : string |>
+
+let indent_mode mode = if mode.debug then <| mode with debug_indent = "  " ^ mode.debug_indent |> else mode
+
+val debug_fun_enter : interp_mode -> string -> list string -> unit
+let debug_fun_enter mode name args =
+  if mode.debug then
+    debug_print (mode.debug_indent ^ ":: " ^ name ^ " args: [" ^ (String.concat "; " args) ^ "]\n")
+  else
+    ()
+
+val debug_fun_exit : forall 'a. Show 'a => interp_mode -> string -> 'a -> unit
+let debug_fun_exit mode name retval =
+  if mode.debug then
+    debug_print (mode.debug_indent ^ "=> " ^ name ^ " returns: " ^ (show retval) ^ "\n")
+  else
+    ()
 
 (* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
-val to_top_env : (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
+val to_top_env : bool -> (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
 val get_default_direction : top_level -> i_direction
 
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value, a memory request, or other external action *)
@@ -1103,7 +1361,7 @@ end
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv
 let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
-  let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in 
+  let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   let (t,tag,cs) = match annot with
     | Just(t,tag,cs,e,_) -> (t,tag,cs)
     | Nothing -> (T_var "fresh",Tag_empty,[]) end in
@@ -1430,7 +1688,43 @@ let resolve_outcome to_match value_thunk action_thunk =
     | (Value v,lm,le) -> value_thunk v lm le
     | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
     | (Error l s,lm,le) -> (Error l s,lm,le)
-  end
+end
+
+let string_of_action a =
+  (match a with
+  | Read_reg r _ -> "(Read_reg " ^ string_of_reg_form r ^ " _)"
+  | Write_reg r _ _ -> "(Write_reg " ^ string_of_reg_form r ^ " _ _)"
+  | Read_mem id v _ -> "(Read_mem " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)"
+  | Read_mem_tagged id v _ -> "(Read_mem_tagged " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)"
+  | Write_mem _ _ _ _ -> "(Write_mem _ _ _ _)"
+  | Write_ea id v -> "(Write_ea " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)"
+  | Write_memv _ _ _ -> "(Write_memv _ _ _)"
+  | Excl_res id -> "(Excl_res " ^ string_of_id id ^ ")"
+  | Write_memv_tagged _ _ _ _ -> "(Write_memv_tagged _ _ _ _)"
+  | Barrier id v -> "(Barrier " ^ string_of_id id ^ " " ^ debug_print_value v ^ ")"
+  | Footprint id v -> "(Footprint " ^ string_of_id id ^ " " ^ debug_print_value v ^ ")"
+  | Nondet exps _ -> "(Nondet [" ^ String.concat "; " (List.map string_of_exp exps) ^ "] _)"
+  | Call_extern s v -> "(Call_extern \"" ^ s ^ "\" " ^ debug_print_value v ^ ")"
+  | Return v -> "(Return " ^ debug_print_value v ^ ")"
+  | Exit exp -> "(Exit " ^ string_of_exp exp ^ ")"
+  | Fail v -> "(Fail " ^ debug_print_value v ^ ")"
+  | Step _ _ _ -> "(Step _ _ _)"
+  end)
+
+instance (Show action)
+  let show action = string_of_action action
+end
+
+let string_of_outcome outcome =
+  (match outcome with
+  | Value v -> "(Value " ^ debug_print_value v ^ ")"
+  | Action a _ -> "(Action " ^ string_of_action a ^ " _)"
+  | Error _ s -> "(Error _ \"" ^ s ^ "\")"
+  end)
+
+instance (Show outcome)
+  let show outcome = string_of_outcome outcome
+end
 
 let update_stack o fn = match o  with
   | Action act stack -> Action act (fn stack)
@@ -1448,7 +1742,7 @@ let get_num v = match v with
   | _ -> 0 end
 
 (*Interpret a list of expressions, tracking local state but evaluating in the same scope (i.e. not tracking env) *)
-let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
+let rec __exp_list mode t_level build_e build_v l_env l_mem vals exps =
   match exps with
   | [ ] -> (Value (build_v vals), l_mem, l_env)
   | e::exps -> 
@@ -1461,8 +1755,14 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
                                                   (e,env''))))
   end
 
-and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in 
+and exp_list mode t_level build_e build_v l_env l_mem vals exps =
+  let _ = debug_fun_enter mode "exp_list" [show vals; show exps] in
+  let retval = __exp_list (indent_mode mode) t_level build_e build_v l_env l_mem vals exps in
+  let _ = debug_fun_exit mode "exp_list" retval in
+  retval
+
+and __interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
+  let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   let (typ,tag,ncs,effect,reffect) = match annot with 
     | Nothing ->
       (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
@@ -2283,8 +2583,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
   | _ -> (Error l "Internal expression escaped to interpreter", l_mem, l_env)
   end
 
+and interp_main mode t_level l_env l_mem exp =
+  let _ = debug_fun_enter mode "interp_main" [show exp] in
+  let retval = __interp_main (indent_mode mode) t_level l_env l_mem exp in
+  let _ = debug_fun_exit mode "interp_main" retval in
+  retval
+
 (*TODO shrink location information on recursive calls *)
- and interp_block mode t_level init_env local_env local_mem l tannot exps =
+and __interp_block mode t_level init_env local_env local_mem l tannot exps =
    match exps with
     | [] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
     | [exp] -> 
@@ -2299,12 +2605,18 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                         else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
                       (fun a -> update_stack a 
                         (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
-    end
+   end
 
-and create_write_message_or_update mode t_level value l_env l_mem is_top_level
+and interp_block mode t_level init_env local_env local_mem l tannot exps =
+  let _ = debug_fun_enter mode "interp_block" [show exps] in
+  let retval = __interp_block (indent_mode mode) t_level init_env local_env local_mem l tannot exps in
+  let _ = debug_fun_exit mode "interp_block" retval in
+  retval
+
+and __create_write_message_or_update mode t_level value l_env l_mem is_top_level
     ((LEXP_aux lexp (l,annot)):lexp tannot) 
     : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv)) * maybe value) =
-   let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
+   let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
    let (typ,tag,ncs,ef,efr) = match annot with 
      | Nothing -> (T_var "fresh_v", Tag_empty, [],
                    (Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
@@ -2963,7 +3275,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
      | e -> e end)
      end
 
-and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
+and create_write_message_or_update mode t_level value l_env l_mem is_top_level le =
+  let _ = debug_fun_enter mode "create_write_message_or_update" [show le] in
+  let retval = __create_write_message_or_update (indent_mode mode) t_level value l_env l_mem is_top_level le in
+  let _ = debug_fun_exit mode "create_write_message_or_update" "_" in
+  retval
+
+and __interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
   match lbind with
   | LB_val_explicit t pat exp ->
     match (interp_main mode t_level l_env l_mem exp) with
@@ -2981,10 +3299,16 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
       | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
     | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
     | e -> (e,Nothing) end
-end     
+end
+
+and interp_letbind mode t_level l_env l_mem lb =
+  let _ = debug_fun_enter mode "interp_letbind" [show lb] in
+  let retval = __interp_letbind (indent_mode mode) t_level l_env l_mem lb in
+  let _ = debug_fun_exit mode "interp_letbind" "_" in
+  retval
 
-and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
-  let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in 
+and __interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
+  let (Env defs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   let stack = Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem Top in
   let get_reg_typ_name typ =
     match typ with
@@ -3038,8 +3362,14 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
     | _ -> Assert_extra.failwith "alias spec not well formed"
 end
 
+and interp_alias_read mode t_level l_env l_mem al =
+  let _ = debug_fun_enter mode "interp_alias_read" [show al] in
+  let retval = __interp_alias_read (indent_mode mode) t_level l_env l_mem al in
+  let _ = debug_fun_exit mode "interp_alias_read" retval in
+  retval
+
 let rec eval_toplevel_let handle_action tlevel env mem lbind = 
-  match interp_letbind <|eager_eval=true; track_values=false; track_lmem=false|> tlevel env mem lbind with
+  match interp_letbind <| eager_eval=true; track_values=false; track_lmem=false; debug=false; debug_indent="" |> tlevel env mem lbind with
     | ((Value v, lm, (LEnv _ le)),_) -> Just le
     | ((Action a s,lm,le), Just le_builder) -> 
       (match handle_action (Action a s) with
@@ -3052,7 +3382,7 @@ let rec eval_toplevel_let handle_action tlevel env mem lbind =
     | _ -> Nothing end
 
 let rec to_global_letbinds handle_action (Defs defs) t_level =
-  let  (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
+  let  (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)), (emem "global_letbinds"), eenv),t_level)
   | def::defs ->
@@ -3062,10 +3392,10 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
         | Just le -> 
           to_global_letbinds handle_action
             (Defs defs) 
-            (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases)
+            (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases debug)
         | Nothing -> 
           to_global_letbinds handle_action (Defs defs) 
-                                           (Env fdefs instrs default_dir lets regs ctors subregs aliases) end
+                                           (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) end
     | DEF_type (TD_aux tdef _) ->
       match tdef with
       | TD_enum id ns ids _ -> 
@@ -3076,7 +3406,7 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
             (List.foldl (fun (c,rst) eid -> (1+c,(get_id eid,V_ctor eid typ (C_Enum c) unitv)::rst)) (0,[]) ids)) in
         to_global_letbinds 
           handle_action (Defs defs) 
-                        (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases)
+                        (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases debug)
       | _ -> to_global_letbinds handle_action (Defs defs) t_level end
     | _ -> to_global_letbinds handle_action (Defs defs) t_level
     end
@@ -3091,28 +3421,34 @@ let rec extract_default_direction (Defs defs) = match defs with
       | _ -> extract_default_direction (Defs defs) end end
 
 (*TODO Contemplate making execute environment variable instead of constant*)
-let to_top_env external_functions defs = 
+let to_top_env debug external_functions defs =
   let direction = (extract_default_direction defs) in
   let t_level = Env (to_fdefs defs) 
                     (extract_instructions "execute" defs) 
                     direction
                     Map.empty (* empty letbind and enum values, call below will fill in any *) 
                     (to_registers direction defs) 
-                    (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+                    (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) debug in
   let (o,t_level) = to_global_letbinds (external_functions direction) defs t_level in
   match o with
     | (Value _,_,_) -> (Nothing,t_level)
     | (o,_,_) -> (Just o,t_level)
   end
 
-let interp mode external_functions defs exp =
-  match (to_top_env external_functions defs) with
+let __interp mode external_functions defs exp =
+  match (to_top_env mode.debug external_functions defs) with
     | (Nothing,t_level) -> 
       interp_main mode t_level eenv (emem "top level") exp
     | (Just o,_) -> (o,(emem "top level error"),eenv) 
   end
 
-let rec resume_with_env mode stack value =
+let interp mode external_functions defs exp =
+  let _ = debug_fun_enter mode "interp" [show exp] in
+  let retval = __interp (indent_mode mode) external_functions defs exp in
+  let _ = debug_fun_exit mode "interp" retval in
+  retval
+
+let rec __resume_with_env mode stack value =
   match (stack,value) with
   | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume_with_env",eenv)
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
@@ -3139,10 +3475,17 @@ let rec resume_with_env mode stack value =
       match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end 
     | (Action action stack,e) -> (Action action (Thunk_frame exp t_level env mem stack),e)
     | (Error l s,e) -> (Error l s,e)
-    end  
+    end
   end
 
-let rec resume mode stack value =
+and resume_with_env mode stack value =
+  let _ = debug_fun_enter mode "resume_with_env" [show value] in
+  let retval = __resume_with_env (indent_mode mode) stack value in
+  let _ = debug_fun_exit mode "interp" retval in
+  retval
+
+
+let rec __resume mode stack value =
   match (stack,value) with
   | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume",(emem "top level error"),eenv)
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
@@ -3173,3 +3516,8 @@ let rec resume mode stack value =
     end  
   end
 
+and resume mode stack value =
+  let _ = debug_fun_enter mode "resume" [show value] in
+  let retval = __resume (indent_mode mode) stack value in
+  let _ = debug_fun_exit mode "resume" retval in
+  retval
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 69958109..fda9d5dd 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -59,16 +59,16 @@ val extern_vector_value: Interp_ast.value -> list byte_lifted
 val extern_mem_value :   Interp_ast.value -> memory_value
 val extern_reg : Interp_ast.reg_form -> maybe (nat * nat) -> reg_name
 
-let make_interpreter_mode eager_eval tracking_values = 
-  <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;;
+let make_interpreter_mode eager_eval tracking_values debug =
+  <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false; Interp.debug = debug; Interp.debug_indent = "" |>;;
 
-let make_mode eager_eval tracking_values =
-  <|internal_mode = make_interpreter_mode eager_eval tracking_values|>;;
-let make_mode_exhaustive =
-  <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true|> |>;;
+let make_mode eager_eval tracking_values debug =
+  <| internal_mode = make_interpreter_mode eager_eval tracking_values debug |>;;
+let make_mode_exhaustive debug =
+  <| internal_mode = <| Interp.eager_eval = true; Interp.track_values = true; Interp.track_lmem = true; Interp.debug = debug; Interp.debug_indent = "" |> |>;;
 let tracking_dependencies mode = mode.internal_mode.Interp.track_values
-let make_eager_mode mode = <| internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
-let make_default_mode = fun () -> <|internal_mode = make_interpreter_mode false false|>;;
+let make_eager_mode mode = <| internal_mode = <| mode.internal_mode with Interp.eager_eval = true |> |>;;
+let make_default_mode = fun () -> <| internal_mode = make_interpreter_mode false false false |>;;
 
 let bitl_to_ibit = function 
   | Bitl_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) 
@@ -355,7 +355,7 @@ type interp_value_return =
   | Ivh_value_after_exn of Interp_ast.value
   | Ivh_error of decode_error
 
-let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk =
+let rec interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen thunk =
   let errk_str = match ivh_mode with
     | Ivh_translate -> "translate"
     | Ivh_analysis -> "analysis"
@@ -363,7 +363,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
     | Ivh_unsupported -> "supported_instructions"
     | Ivh_illegal -> "illegal instruction" end in
   let events_out = match events with [] -> Nothing | _ -> Just events end in
-  let mode = (make_interpreter_mode true false) in
+  let mode = (make_interpreter_mode true false debug) in
   match thunk() with
     | (Interp.Value value,_,_) ->
       if exn_seen
@@ -384,13 +384,13 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
             | _ -> (Ivh_error (Interp_interface.Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
     | (Interp.Error l msg,_,_) -> (Ivh_error (Interp_interface.Internal_error msg), events_out)
     | (Interp.Action (Interp.Return value) stack,_,_) ->
-      interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
+      interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen
         (fun _ -> Interp.resume mode stack (Just value))
     | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
       match List.lookup i (Interp_lib.library_functions direction) with
         | Nothing -> (Ivh_error (Interp_interface.Internal_error ("External function not available " ^ i)), events_out)
         | Just f  ->
-          interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
+          interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen
                                  (fun _ -> Interp.resume mode stack (Just (f value)))
       end
     | (Interp.Action (Interp.Fail v) stack, _, _) ->
@@ -399,7 +399,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
         (Ivh_error (Interp_interface.Internal_error ("Assert failed: " ^ s)), events_out)
       | _ -> (Ivh_error (Interp_interface.Internal_error "Assert failed"), events_out) end
     | (Interp.Action (Interp.Exit exp) stack,_,_) ->
-      interp_to_value_helper arg ivh_mode err_str instr direction registers events true
+      interp_to_value_helper debug arg ivh_mode err_str instr direction registers events true
         (fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing)
     | (Interp.Action (Interp.Read_reg r slice) stack,_,_) ->
       let rname = match r with 
@@ -418,12 +418,12 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
             | Just v ->
               let value = intern_reg_value v in
 (*              let _ = Interp.debug_print ("Register read of " ^ rname ^ " returning value " ^ (Interp.string_of_value value) ^ "\n") in *)
-              interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
+              interp_to_value_helper debug arg ivh_mode err_str instr direction registers events exn_seen
                 (fun _ -> Interp.resume mode stack (Just value)) end end)      
     | (Interp.Action (Interp.Write_reg r slice value) stack,_,_) ->
       let ext_reg = extern_reg r slice in
       let reg_value = extern_reg_value ext_reg value in
-      interp_to_value_helper arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events)
+      interp_to_value_helper debug arg ivh_mode err_str instr direction registers ((E_write_reg ext_reg reg_value)::events)
         exn_seen (fun _ -> Interp.resume mode stack Nothing)
     | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
       (Ivh_error (Interp_interface.Internal_error ("Read memory request in a " ^ errk_str)), events_out)
@@ -450,25 +450,26 @@ let call_external_functions direction outcome =
         | Just f -> Just (f value) end
     | _ -> Nothing end
 
-let build_context defs reads writes write_eas write_vals barriers excl_res externs =
+let build_context debug defs reads writes write_eas write_vals barriers excl_res externs =
   (*TODO add externs to to_top_env*)
-  match Interp.to_top_env call_external_functions defs with 
-    | (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) -> 
+  match Interp.to_top_env debug call_external_functions defs with 
+    | (_,((Interp.Env _ _ dir _ _ _ _ _ debug) as context)) -> 
       Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing)
         reads writes write_eas write_vals barriers excl_res externs end
 
 
 let translate_address top_level end_flag thunk_name registers address =
   let (Address bytes i) = address in
-  let mode = make_mode true false in
-  let int_mode = mode.internal_mode in
   let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
+  let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
+  let mode = make_mode true false debug in
+  let int_mode = mode.internal_mode in
   let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (address_error,events) =
-    interp_to_value_helper (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction
+    interp_to_value_helper debug (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -504,15 +505,16 @@ let intern_instruction direction (name,parms) =
     (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms))
 
 let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
-  let mode = make_mode true false in
-  let int_mode = mode.internal_mode in
   let (Context top_env direction _ _ _ _ _ _ _ _ _) = top_level in
+  let (Interp.Env _ _ _ _ _ _ _ _ debug) = top_env in
+  let mode = make_mode true false debug in
+  let int_mode = mode.internal_mode in
   let intern_val = intern_instruction direction instruction in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (analysis_or_error,events) =
-    interp_to_value_helper Nothing Ivh_analysis val_str ("",[]) internal_direction
+    interp_to_value_helper debug Nothing Ivh_analysis val_str ("",[]) internal_direction
       registers [] false
       (fun _ -> Interp.resume 
         int_mode 
@@ -646,7 +648,7 @@ end
 
 
 let interp_value_to_instr_external top_level instr = 
-  let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _) = top_level in
+  let (Context (Interp.Env _ instructions _ _ _ _ _ _ debug) _ _ _ _ _ _ _ _ _ _) = top_level in
   match instr with
   | Interp_ast.V_ctor (Id_aux (Id i) _) _ _ parm ->
      match (find_instruction i instructions) with
@@ -670,14 +672,14 @@ let interp_value_to_instr_external top_level instr =
 
 
 let decode_to_instruction top_level registers value : instruction_or_decode_error = 
-  let mode = make_interpreter_mode true false in
-  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _ _ _ _ _ _) = top_level in
+  let (Context ((Interp.Env _ instructions _ _ _ _ _ _ debug) as top_env) direction _ _ _ _ _ _ _ _ _) = top_level in
+  let mode = make_interpreter_mode true false debug in
   let intern_val = intern_opcode direction value in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
   let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (instr_decoded_error,events) =
-    interp_to_value_helper (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false
+    interp_to_value_helper debug (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false
       (fun _ -> Interp.resume 
           mode 
           (Interp.Thunk_frame 
@@ -687,7 +689,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
     | Ivh_value instr -> 
       let instr_external = interp_value_to_instr_external top_level instr in
       let (instr_decoded_error,events) =
-        interp_to_value_helper (Just value) Ivh_unsupported val_str instr_external internal_direction
+        interp_to_value_helper debug (Just value) Ivh_unsupported val_str instr_external internal_direction
           registers [] false
         (fun _ -> Interp.resume 
             mode
@@ -1028,9 +1030,9 @@ let rec ie_loop mode register_values (IState interp_state context) =
       | _ -> Assert_extra.failwith "interp_to_outcome may have produced a nondet action"
       end ;;
   
-val interp_exhaustive : maybe (list (reg_name * register_value)) -> instruction_state -> list event
-let interp_exhaustive register_values i_state = 
-  let mode = make_mode_exhaustive in
+val interp_exhaustive : bool -> maybe (list (reg_name * register_value)) -> instruction_state -> list event
+let interp_exhaustive debug register_values i_state =
+  let mode = make_mode_exhaustive debug in
   match ie_loop mode register_values i_state with
     | (events,_) -> events
 end
@@ -1086,7 +1088,7 @@ and state_to_outcome_s pp_instruction_state mode state =
   let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in
   (next_outcome, 
    Just ((pp_instruction_state state), 
-         (fun env -> interp_exhaustive (Just env) state))
+         (fun env -> interp_exhaustive mode.internal_mode.Interp.debug (Just env) state))
   )
 
 val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 602efad3..6978aeb9 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -292,7 +292,7 @@ let run
         interact mode env stack
       | "e" | "exh" | "exhaust" ->
         interactf "interpreting exhaustively from current state\n";
-        let events = interp_exhaustive None stack in
+        let events = interp_exhaustive false None stack in
         interactf "%s" (format_events events);
         interact mode env stack
       | "c" | "cont" | "continuation" ->
@@ -433,7 +433,7 @@ let run
               (List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in
           show "nondeterministic evaluation begun" "" "" "";
           let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
-              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
               choose_order (false,mode,!track_dependencies,env'); in
           show "nondeterministic evaluation ended" "" "" "";
           (step next,env',next)
@@ -445,7 +445,7 @@ let run
           else begin
             show "undefined triggered a non_det" "" "" "";
             let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
-              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next))
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies false) next))
               choose_order (false,mode,!track_dependencies,env'); in
             (step i_state,env',i_state) end
         | Escape0(Some e,_) ->
@@ -462,11 +462,11 @@ let run
         | Write_memv1 _ -> assert false)
         (*| _ -> assert false*)
       in
-      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies) next) in
+      loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies false) next) in
   let mode = match mode with
   | None -> if eager_eval then Run else Step
   | Some m -> m in
-  let imode = make_mode eager_eval !track_dependencies in
+  let imode = make_mode eager_eval !track_dependencies false in
   let (IState(instr_state,context)) = istate in
   let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in
   interactf "%s: %s %s\n" (grey name) (blue "evaluate") 
diff --git a/src/lem_interp/type_check.lem b/src/lem_interp/type_check.lem
index 179e53d3..6c6cda1a 100644
--- a/src/lem_interp/type_check.lem
+++ b/src/lem_interp/type_check.lem
@@ -54,7 +54,7 @@ open import Interp_ast
 open import Interp_utilities
 open import Instruction_extractor
 
-type tannot = Interp_utilities.tannot
+type tannot = Interp_ast.tannot
 
 (*Env of t counter, nexp counter, order counter, type env, order env, nexp env, nec env*)
 type envs = | Env of nat * nat * nat * map string (t * nec) * map string order * map string ne * map string nec