diff --git a/compiler/backend/README.md b/compiler/backend/README.md
index 0e399691c5..49c10caac6 100644
--- a/compiler/backend/README.md
+++ b/compiler/backend/README.md
@@ -25,6 +25,10 @@ to the front-end, i.e. parsing and type inference.
 [backend_commonScript.sml](backend_commonScript.sml):
 Definitions that are common for many parts of the compiler backend.
 
+[backend_passesScript.sml](backend_passesScript.sml):
+Reformulates compile definition to expose the result of each internal
+compiler pass
+
 [bviScript.sml](bviScript.sml):
 The BVI intermediate language. This language is very similar to BVL.
 One of the more notable differences is that exception handling is
@@ -234,6 +238,9 @@ This directory contains the mips-specific part of the compiler backend.
 [pattern_matching](pattern_matching):
 The CakeML pattern matching expressions compiler
 
+[presLangLib.sml](presLangLib.sml):
+Library that helps pretty print code
+
 [presLangScript.sml](presLangScript.sml):
 Functions for converting various intermediate languages
 into displayLang representations.
@@ -303,6 +310,9 @@ This compiler phase maps stackLang programs, which has structure
 such as If, While, Return etc, to labLang programs that are a soup
 of goto-like jumps.
 
+[str_treeScript.sml](str_treeScript.sml):
+A Lisp inspired tree of mlstrings and a pretty printing function
+
 [wordLangScript.sml](wordLangScript.sml):
 The wordLang intermediate language consists of structured programs
 that overate over machine words, a list-like stack and a flat memory.
diff --git a/compiler/backend/backendScript.sml b/compiler/backend/backendScript.sml
index cc65343af2..0963be388d 100644
--- a/compiler/backend/backendScript.sml
+++ b/compiler/backend/backendScript.sml
@@ -44,16 +44,14 @@ val attach_bitmaps_def = Define `
                   |>) /\
   attach_bitmaps names c bm NONE = NONE`
 
-val compile_tap_def = Define`
-  compile_tap c p =
+Definition compile_def:
+  compile c p =
     let p = source_to_source$compile p in
     let _ = empty_ffi (strlit "finished: source_to_source") in
     let (c',p) = source_to_flat$compile c.source_conf p in
-    let td = tap_flat c.tap_conf p [] in
     let _ = empty_ffi (strlit "finished: source_to_flat") in
     let c = c with source_conf := c' in
     let p = flat_to_clos$compile_prog p in
-    let td = tap_clos c.tap_conf p td in
     let _ = empty_ffi (strlit "finished: flat_to_clos") in
     let (c',p,names) = clos_to_bvl$compile c.clos_conf p in
     let c = c with clos_conf := c' in
@@ -63,32 +61,26 @@ val compile_tap_def = Define`
     let c = c with bvl_conf updated_by (λc. c with <| inlines := l; next_name1 := n1; next_name2 := n2 |>) in
     let _ = empty_ffi (strlit "finished: bvl_to_bvi") in
     let p = bvi_to_data$compile_prog p in
-    let td = tap_data_lang c.tap_conf (p,names) td in
     let _ = empty_ffi (strlit "finished: bvi_to_data") in
     let (col,p) = data_to_word$compile c.data_conf c.word_to_word_conf c.lab_conf.asm_conf p in
     let c = c with word_to_word_conf updated_by (λc. c with col_oracle := col) in
     let names = sptree$union (sptree$fromAList $ (data_to_word$stub_names () ++
       word_to_stack$stub_names () ++ stack_alloc$stub_names () ++
       stack_remove$stub_names ())) names in
-    let td = tap_word c.tap_conf (p,names) td in
     let _ = empty_ffi (strlit "finished: data_to_word") in
     let (bm,c',fs,p) = word_to_stack$compile c.lab_conf.asm_conf p in
-    let td = tap_stack c.tap_conf (p,names) td in
     let c = c with word_conf := c' in
     let _ = empty_ffi (strlit "finished: word_to_stack") in
     let p = stack_to_lab$compile
       c.stack_conf c.data_conf (2 * max_heap_limit (:'a) c.data_conf - 1)
       (c.lab_conf.asm_conf.reg_count - (LENGTH c.lab_conf.asm_conf.avoid_regs +3))
       (c.lab_conf.asm_conf.addr_offset) p in
-    let td = tap_lab c.tap_conf (p,names) td in
     let _ = empty_ffi (strlit "finished: stack_to_lab") in
     let res = attach_bitmaps names c bm
       (lab_to_target$compile c.lab_conf (p:'a prog)) in
     let _ = empty_ffi (strlit "finished: lab_to_target") in
-      (res, td)`;
-
-val compile_def = Define`
-  compile c p = FST (compile_tap c p)`;
+      res
+End
 
 val to_flat_def = Define`
   to_flat c p =
@@ -175,7 +167,7 @@ val to_target_def = Define`
 Theorem compile_eq_to_target:
    compile = to_target
 Proof
-  srw_tac[][FUN_EQ_THM,compile_def,compile_tap_def,
+  srw_tac[][FUN_EQ_THM,compile_def,
      to_target_def,
      to_lab_def,
      to_stack_def,
@@ -280,7 +272,7 @@ val from_source_def = Define`
 Theorem compile_eq_from_source:
    compile = from_source
 Proof
-  srw_tac[][FUN_EQ_THM,compile_def,compile_tap_def,
+  srw_tac[][FUN_EQ_THM,compile_def,
      from_source_def,
      from_lab_def,
      from_stack_def,
@@ -430,7 +422,7 @@ Proof
      to_bvl_def,
      to_clos_def,
      to_flat_def,to_livesets_def] >>
-  fs[compile_def,compile_tap_def]>>
+  fs[compile_def]>>
   pairarg_tac>>
   fs[data_to_wordTheory.compile_def,word_to_wordTheory.compile_def]>>
   fs[from_livesets_def,from_word_def,from_stack_def,from_lab_def]>>
diff --git a/compiler/backend/backend_passesScript.sml b/compiler/backend/backend_passesScript.sml
new file mode 100644
index 0000000000..3f05f01fe7
--- /dev/null
+++ b/compiler/backend/backend_passesScript.sml
@@ -0,0 +1,362 @@
+(*
+  Reformulates compile definition to expose the result of each internal
+  compiler pass
+*)
+
+open preamble backendTheory presLangTheory
+
+val _ = new_theory"backend_passes";
+
+val _ = set_grammar_ancestry ["backend"];
+
+Datatype:
+  any_prog = Source (ast$dec list)
+           | Flat (flatLang$dec list)
+           | Clos (closLang$exp list) ((num # num # closLang$exp) list)
+           | Bvl ((num # num # bvl$exp) list) (mlstring sptree$num_map)
+           | Bvi ((num # num # bvi$exp) list) (mlstring sptree$num_map)
+           | Data ((num # num # dataLang$prog) list) (mlstring sptree$num_map)
+           | Word ((num # num # α wordLang$prog) list) (mlstring sptree$num_map)
+           | Stack ((num # α stackLang$prog) list) (mlstring sptree$num_map)
+           | Lab (α sec list) (mlstring sptree$num_map)
+End
+
+Definition to_flat_all_def:
+  to_flat_all (c:'a config) p =
+    let ps = [] in
+    let ps = ps ++ [(strlit "original source code",Source p)] in
+    let p = source_let$compile_decs p in
+    let ps = ps ++ [(strlit "after source_let",Source p)] in
+    let (c',p) = source_to_flat$compile_prog c.source_conf p in
+    let ps = ps ++ [(strlit "after source_to_flat",Flat p)] in
+    let p = flat_elim$remove_flat_prog p in
+    let ps = ps ++ [(strlit "after remove_flat",Flat p)] in
+    let p = MAP (flat_pattern$compile_dec c'.pattern_cfg) p in
+    let ps = ps ++ [(strlit "after flat_pattern",Flat p)] in
+    let c = c with source_conf := c' in
+      ((ps: (mlstring # 'a any_prog) list),c,p)
+End
+
+Theorem to_flat_thm:
+  SND (to_flat_all c p) = to_flat c p
+Proof
+  fs [to_flat_all_def,to_flat_def,source_to_sourceTheory.compile_def,
+      source_to_flatTheory.compile_prog_def,
+      source_to_flatTheory.compile_def,
+      source_to_flatTheory.compile_flat_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Definition to_clos_all_def:
+  to_clos_all (c:'a config) p =
+    let (ps,c,p) = to_flat_all c p in
+    let p = flat_to_clos$compile_prog p in
+    let ps = ps ++ [(strlit "after flat_to_clos",Clos p [])] in
+      ((ps: (mlstring # 'a any_prog) list),c,p)
+End
+
+Theorem to_clos_thm:
+  SND (to_clos_all c p) = to_clos c p
+Proof
+  assume_tac to_flat_thm
+  \\ fs [to_clos_all_def,to_clos_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Definition to_bvl_all_def:
+  to_bvl_all (c:'a config) p =
+    let (ps,c,es0) = to_clos_all c p in
+    let c0 = c.clos_conf in
+    let es = clos_mti$compile c0.do_mti c0.max_app es0 in
+    let ps = ps ++ [(strlit "after clos_mti",Clos es [])] in
+    let loc = c0.next_loc + MAX 1 (LENGTH es) in
+    let loc = if loc MOD 2 = 0 then loc else loc + 1 in
+    let (n,es) = clos_number$renumber_code_locs_list loc es in
+    let ps = ps ++ [(strlit "after clos_number",Clos es [])] in
+    let (kc,es) = clos_known$compile c0.known_conf es in
+    let ps = ps ++ [(strlit "after clos_known",Clos es [])] in
+    let (es,g,aux) = clos_call$compile c0.do_call es in
+    let ps = ps ++ [(strlit "after clos_call",Clos es aux)] in
+    let prog = chain_exps c0.next_loc es ++ aux in
+    let prog = clos_annotate$compile prog in
+    let ps = ps ++ [(strlit "after clos_annotate",Clos [] prog)] in
+    let c1 = c0 with
+         <|start := c0.next_loc; next_loc := n; known_conf := kc;
+           call_state := (g,aux)|> in
+    let init_stubs = toAList (init_code c1.max_app) in
+    let init_globs =
+            [(num_stubs c1.max_app − 1,0,
+              init_globals c1.max_app (num_stubs c1.max_app + c1.start))] in
+    let comp_progs = clos_to_bvl$compile_prog c1.max_app prog in
+    let prog' = init_stubs ++ init_globs ++ comp_progs in
+    let func_names =
+            make_name_alist (MAP FST prog') prog (num_stubs c1.max_app)
+              c0.next_loc (LENGTH es0) in
+    let ps = ps ++ [(strlit "after clos_to_bvl",Bvl prog' func_names)] in
+    let c2 = c1 with start := num_stubs c1.max_app − 1 in
+    let p = code_sort prog' in
+    let c = c with clos_conf := c2 in
+      ((ps: (mlstring # 'a any_prog) list),c,p,func_names)
+End
+
+Theorem to_bvl_thm:
+  SND (to_bvl_all c p ) = to_bvl c p
+Proof
+  assume_tac to_clos_thm
+  \\ fs [to_bvl_all_def,to_bvl_def,clos_to_bvlTheory.compile_def,
+         clos_to_bvlTheory.compile_common_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Definition to_bvi_all_def:
+  to_bvi_all (c:'a config) p =
+    let (ps,c,p,names) = to_bvl_all c p in
+    let start = c.clos_conf.start in
+    let c0 = c.bvl_conf in
+    let limit = c0.inline_size_limit in
+    let split_seq = c0.split_main_at_seq in
+    let cut_size = c0.exp_cut in
+    let (inlines,prog1) = bvl_inline$tick_compile_prog limit LN p in
+    let prog = MAP (λ(name,arity,exp). (name,arity, HD (remove_ticks [exp]))) prog1 in
+    let ps = ps ++ [(strlit "after bvl_inline and remove_ticks",Bvl prog names)] in
+    let prog = MAP (λ(name,arity,exp). (name,arity, let_op_sing exp)) prog in
+    let ps = ps ++ [(strlit "after let_op_sing",Bvl prog names)] in
+    let prog = MAP (λ(name,arity,exp). (name,arity,
+                       bvl_handle$compile_any split_seq cut_size arity exp)) prog in
+    let ps = ps ++ [(strlit "after bvl_handle",Bvl prog names)] in
+    let (loc,code,n1) = bvl_to_bvi$compile_prog start 0 prog in
+    let (n2,code') = bvi_tailrec$compile_prog (bvl_num_stubs + 2) code in
+    let (s,p,l,n1,n2,names) = (loc,code',inlines,n1,n2,get_names (MAP FST code') names) in
+    let names = sptree$union (sptree$fromAList $ (data_to_word$stub_names () ++
+      word_to_stack$stub_names () ++ stack_alloc$stub_names () ++
+      stack_remove$stub_names ())) names in
+    let ps = ps ++ [(strlit "after bvl_to_bvi",Bvi code names)] in
+    let ps = ps ++ [(strlit "after bvi_tailrec",Bvi code' names)] in
+    let c = c with clos_conf updated_by (λc. c with start := s) in
+    let c = c with bvl_conf updated_by
+      (λc. c with <| inlines := l; next_name1 := n1; next_name2 := n2 |>) in
+     ((ps: (mlstring # 'a any_prog) list),c,p,names)
+End
+
+Theorem to_bvi_thm:
+  SND (to_bvi_all c p ) = to_bvi c p
+Proof
+  assume_tac to_bvl_thm
+  \\ fs [to_bvi_all_def,to_bvi_def,bvl_to_bviTheory.compile_def,
+         bvl_inlineTheory.compile_inc_def,bvl_inlineTheory.compile_prog_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [MAP_MAP_o,o_DEF]
+  \\ rpt $ pop_assum mp_tac
+  \\ qpat_abbrev_tac ‘f1 = MAP _ prog1’
+  \\ qpat_abbrev_tac ‘f2 = MAP _ prog1’
+  \\ qsuff_tac ‘f1 = f2’ >- (rw [] \\ gvs [])
+  \\ unabbrev_all_tac
+  \\ fs [FUN_EQ_THM,FORALL_PROD,MAP_EQ_f]
+  \\ gvs [bvl_inlineTheory.optimise_def]
+QED
+
+Definition to_data_all_def:
+  to_data_all (c:'a config) p =
+    let (ps,c,p,names) = to_bvi_all c p in
+    let p = MAP (λ(a,n,e). (a,n,FST (compile n (COUNT_LIST n) T [] [e]))) p in
+    let ps = ps ++ [(strlit "after bvi_to_data",Data p names)] in
+    let p = MAP (λ(a,n,e). (a,n,FST (data_live$compile e LN))) p in
+    let ps = ps ++ [(strlit "after data_live",Data p names)] in
+    let p = MAP (λ(a,n,e). (a,n,data_simp$simp e Skip)) p in
+    let ps = ps ++ [(strlit "after data_simp",Data p names)] in
+    let p = MAP (λ(a,n,e). (a,n,data_space$compile e)) p in
+    let ps = ps ++ [(strlit "after data_space",Data p names)] in
+      ((ps: (mlstring # 'a any_prog) list),c,p,names)
+End
+
+Theorem to_data_thm:
+  SND (to_data_all (c:'a config) p) = to_data c p
+Proof
+  assume_tac to_bvi_thm
+  \\ fs [to_data_all_def,to_data_def,bvi_to_dataTheory.compile_prog_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [MAP_MAP_o,o_DEF,LAMBDA_PROD]
+  \\ gvs [MAP_EQ_f,FORALL_PROD,bvi_to_dataTheory.compile_part_def,
+          bvi_to_dataTheory.compile_exp_def,bvi_to_dataTheory.optimise_def]
+QED
+
+Definition to_word_all_def:
+  to_word_all (c:'a config) p =
+    let (ps,c,p,names) = to_data_all c p in
+    let data_conf = c.data_conf in
+    let word_conf = c.word_to_word_conf in
+    let asm_conf = c.lab_conf.asm_conf in
+    let data_conf =
+            data_conf with
+            <|has_fp_ops := (1 < asm_conf.fp_reg_count);
+              has_fp_tern :=
+                (asm_conf.ISA = ARMv7 ∧ 2 < asm_conf.fp_reg_count)|> in
+    let p = stubs (:α) data_conf ++ MAP (compile_part data_conf) p in
+    let ps = ps ++ [(strlit "after data_to_word",Word p names)] in
+    let (two_reg_arith,reg_count) =
+            (asm_conf.two_reg_arith,
+             asm_conf.reg_count − (5 + LENGTH asm_conf.avoid_regs)) in
+    let (n_oracles,col) = next_n_oracle (LENGTH p) word_conf.col_oracle in
+    let p = ZIP (p,n_oracles) in
+    let alg = word_conf.reg_alg in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,word_simp$compile_exp prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_simp",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,
+                     inst_select asm_conf (max_var prog + 1) prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_inst",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,full_ssa_cc_trans arg_count prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_ssa",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,word_common_subexp_elim prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after word_cse",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,FST (remove_dead prog LN)),col_opt)) p in
+    let ps = ps ++ [(strlit "after remove_dead in word_alloc",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,
+                   if two_reg_arith then three_to_two_reg prog else prog),col_opt)) p in
+    let ps = ps ++ [(strlit "after three_to_two_reg from word_inst",Word (MAP FST p) names)] in
+    let p = MAP (λ((name_num,arg_count,prog),col_opt).
+                  ((name_num,arg_count,
+                   remove_must_terminate
+                     (word_alloc name_num asm_conf alg reg_count prog col_opt)))) p in
+    let ps = ps ++ [(strlit "after word_alloc (and remove_must_terminate)",Word p names)] in
+    let c = c with word_to_word_conf updated_by (λc. c with col_oracle := col) in
+      ((ps: (mlstring # 'a any_prog) list),c,p,names)
+End
+
+Theorem to_word_thm:
+  SND (to_word_all (c:'a config) p) = to_word c p
+Proof
+  assume_tac to_data_thm
+  \\ fs [to_word_all_def,to_word_def,data_to_wordTheory.compile_def,
+         word_to_wordTheory.compile_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [MAP_MAP_o,o_DEF,LAMBDA_PROD]
+  \\ gvs [MAP_EQ_f,FORALL_PROD,word_to_wordTheory.full_compile_single_def,
+          word_to_wordTheory.compile_single_def]
+QED
+
+Definition to_stack_all_def:
+  to_stack_all (c:'a config) p =
+    let (ps,c,p,names) = to_word_all c p in
+    let (bm,c',fs,p) = word_to_stack$compile c.lab_conf.asm_conf p in
+    let ps = ps ++ [(strlit "after word_to_stack",Stack p names)] in
+    let c = c with word_conf := c' in
+      ((ps: (mlstring # 'a any_prog) list),bm,c,p,names)
+End
+
+Theorem to_stack_thm:
+  SND (to_stack_all (c:'a config) p) = to_stack c p
+Proof
+  assume_tac to_word_thm
+  \\ fs [to_stack_all_def,to_stack_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Definition to_lab_all_def:
+  to_lab_all (c:'a config) p =
+    let (ps,bm,c,p,names) = to_stack_all c p in
+    let stack_conf = c.stack_conf in
+    let data_conf = c.data_conf in
+    let max_heap = 2 * max_heap_limit (:'a) c.data_conf - 1 in
+    let sp = c.lab_conf.asm_conf.reg_count - (LENGTH c.lab_conf.asm_conf.avoid_regs + 3) in
+    let offset = c.lab_conf.asm_conf.addr_offset in
+    let prog = stack_rawcall$compile p in
+    let ps = ps ++ [(strlit "after stack_rawcall",Stack prog names)] in
+    let prog = stack_alloc$compile data_conf prog in
+    let ps = ps ++ [(strlit "after stack_alloc",Stack prog names)] in
+    let prog = stack_remove$compile stack_conf.jump offset (is_gen_gc data_conf.gc_kind)
+                 max_heap sp InitGlobals_location prog in
+    let ps = ps ++ [(strlit "after stack_remove",Stack prog names)] in
+    let prog = stack_names$compile stack_conf.reg_names prog in
+    let ps = ps ++ [(strlit "after stack_names",Stack prog names)] in
+    let p = MAP prog_to_section prog in
+    let ps = ps ++ [(strlit "after stack_to_lab",Lab p names)] in
+      ((ps: (mlstring # 'a any_prog) list),bm,c,p:'a prog,names)
+End
+
+Theorem to_lab_thm:
+  SND (to_lab_all (c:'a config) p) = to_lab c p
+Proof
+  assume_tac to_stack_thm
+  \\ fs [to_lab_all_def,to_lab_def,stack_to_labTheory.compile_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Definition to_target_all_def:
+  to_target_all (c:'a config) p =
+    let (ps,bm,c,p,names) = to_lab_all c p in
+    let p = filter_skip p in
+    let ps = ps ++ [(strlit "after filter_skip",Lab p names)] in
+    let p = compile_lab c.lab_conf p in
+      ((ps: (mlstring # 'a any_prog) list), attach_bitmaps names c bm p)
+End
+
+Theorem to_target_thm:
+  SND (to_target_all c p) = to_target c p
+Proof
+  assume_tac to_lab_thm
+  \\ fs [to_target_all_def,to_target_def,lab_to_targetTheory.compile_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Theorem compile_eq_to_target_all:
+  compile c p = SND (to_target_all c p)
+Proof
+  rewrite_tac [compile_eq_to_target,GSYM to_target_thm]
+QED
+
+Theorem number_of_passes:
+  LENGTH (FST (to_target_all c p)) = 36
+Proof
+  fs [to_target_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_lab_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_stack_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_word_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_data_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_bvi_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_bvl_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_clos_all_def] \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [to_flat_all_def] \\ rpt (pairarg_tac \\ gvs [])
+QED
+
+Definition any_prog_pp_def:
+  any_prog_pp p = case p of
+    | Source p => source_to_strs p
+    | Flat p => flat_to_strs p
+    | Clos decs funs => clos_to_strs (decs,funs)
+    | Bvl p names => bvl_to_strs names p
+    | Bvi p names => bvi_to_strs names p
+    | Data p names => data_to_strs names p
+    | Word p names => word_to_strs names p
+    | Stack p names => stack_to_strs names p
+    | Lab p names => lab_to_strs names p
+End
+
+Definition any_prog_pp_with_title_def:
+  any_prog_pp_with_title (title,p) acc =
+    Append (List [strlit "# "; title; strlit "\n\n"]) $
+    Append (any_prog_pp p) acc
+End
+
+Definition compile_tap_def:
+  compile_tap (c:'a config) p =
+    if c.tap_conf.explore_flag then
+      let (ps,out) = to_target_all c p in
+        (out, FOLDR any_prog_pp_with_title Nil ps)
+    else (compile c p, Nil)
+End
+
+Theorem compile_alt:
+  compile c p = FST (compile_tap c p)
+Proof
+  rw [compile_tap_def]
+  \\ mp_tac compile_eq_to_target_all
+  \\ pairarg_tac \\ gvs []
+QED
+
+val _ = export_theory();
diff --git a/compiler/backend/displayLangScript.sml b/compiler/backend/displayLangScript.sml
index 8dde542203..d1cad2a915 100644
--- a/compiler/backend/displayLangScript.sml
+++ b/compiler/backend/displayLangScript.sml
@@ -5,20 +5,22 @@
   supports Tuples, Items (e.g. datatype constructors), and Lists.
 *)
 open preamble jsonLangTheory mlintTheory backend_commonTheory;
+open str_treeTheory;
 
 val _ = new_theory"displayLang";
 
-val _ = Datatype`
+Datatype:
   sExp =
     | Item (tra option) mlstring (sExp list)
     | String mlstring
     | Tuple (sExp list)
-    | List (sExp list)`;
+    | List (sExp list)
+End
 
 val sExp_size_def = fetch "-" "sExp_size_def";
 
 (* display_to_json *)
-val trace_to_json_def = Define`
+Definition trace_to_json_def:
   (trace_to_json (backend_common$Cons tra num) =
     Object [(strlit "name", String (strlit "Cons"));
       (strlit "num", String (toString num));
@@ -36,16 +38,17 @@ val trace_to_json_def = Define`
   /\
   (* TODO: cancel entire trace when None, or verify that None will always be at
   * the top level of a trace. *)
-  (trace_to_json None = Null)`;
+  (trace_to_json None = Null)
+End
 
 Theorem MEM_sExp_size:
-   !es a. MEM a es ==> sExp_size a < sExp1_size es
+  !es a. MEM a es ==> sExp_size a < sExp1_size es
 Proof
   Induct \\ fs [] \\ rw [sExp_size_def] \\ fs [] \\ res_tac \\ fs []
 QED
 
 (* Converts a display expression to JSON *)
-val display_to_json_def = tDefine"display_to_json" `
+Definition display_to_json_def:
   (display_to_json (Item tra name es) =
     let es' = MAP display_to_json es in
     let props = [(strlit "name", String name); (strlit "args", Array es')] in
@@ -59,8 +62,24 @@ val display_to_json_def = tDefine"display_to_json" `
     let es' = MAP display_to_json es in
       Object [(strlit "isTuple", Bool T); (strlit "elements", Array es')])
   /\
-   (display_to_json (List es) = Array (MAP display_to_json es))`
-  (WF_REL_TAC `measure sExp_size` \\ rw []
-   \\ imp_res_tac MEM_sExp_size \\ fs []);
+   (display_to_json (List es) = Array (MAP display_to_json es))
+Termination
+  WF_REL_TAC `measure sExp_size` \\ rw []
+  \\ imp_res_tac MEM_sExp_size \\ fs []
+End
+
+Definition display_to_str_tree_def:
+  (display_to_str_tree (Item tra name es) =
+     mk_list (Str name :: MAP display_to_str_tree es)) ∧
+  (display_to_str_tree (String s : sExp) = Str s) /\
+  (display_to_str_tree (Tuple es) =
+     if NULL es then Str (strlit "()")
+     else mk_list (MAP display_to_str_tree es)) ∧
+  (display_to_str_tree (List es) =
+     if NULL es then Str (strlit "()")
+     else mk_list (MAP GrabLine (MAP display_to_str_tree es)))
+Termination
+  WF_REL_TAC `measure sExp_size` \\ rw []
+End
 
 val _ = export_theory();
diff --git a/compiler/backend/presLangLib.sig b/compiler/backend/presLangLib.sig
new file mode 100644
index 0000000000..0c8f5a5146
--- /dev/null
+++ b/compiler/backend/presLangLib.sig
@@ -0,0 +1,16 @@
+signature presLangLib =
+sig
+
+   include Abbrev
+
+   val flat_to_strs : term (* prog *) -> string list
+   val clos_to_strs : term (* prog *) -> string list
+   val bvl_to_strs : term (* names *) -> term (* prog *) -> string list
+   val bvi_to_strs : term (* names *) -> term (* prog *) -> string list
+   val data_to_strs : term (* names *) -> term (* prog *) -> string list
+
+   val print_strs : string list -> unit
+
+   val write_strs_to_file : string -> string list -> unit
+
+end
diff --git a/compiler/backend/presLangLib.sml b/compiler/backend/presLangLib.sml
new file mode 100644
index 0000000000..911471c494
--- /dev/null
+++ b/compiler/backend/presLangLib.sml
@@ -0,0 +1,74 @@
+(*
+  Library that helps pretty print code
+*)
+structure presLangLib :> presLangLib =
+struct
+
+open HolKernel boolLib bossLib;
+
+local
+  val s1 = HolKernel.syntax_fns1 "misc"
+  val s2 = HolKernel.syntax_fns2 "misc"
+  val m1 = HolKernel.syntax_fns1 "mlstring"
+in
+  val (Append_tm,mk_Append,dest_Append,is_Append) = s2 "Append";
+  val (List_tm,mk_List,dest_List,is_List) = s1 "List";
+  val (strlit_tm,mk_strlit,dest_strlit,is_strlit) = m1 "strlit";
+end
+
+(* expects tm to be a concrete app_list *)
+fun dest_app_list tm = let
+  fun aux tm acc =
+    if is_Append tm then
+      let val (x,y) = dest_Append tm
+      in aux x (aux y acc) end
+    else if is_List tm then
+      let val x = dest_List tm
+      in fst (listSyntax.dest_list x) @ acc end
+    else acc
+  in aux tm [] end;
+
+(* turns mlstring app_list into string list *)
+fun mlstring_app_list_to_string_list tm =
+  map (stringSyntax.fromHOLstring o dest_strlit) (dest_app_list tm);
+
+fun flat_to_strs flat_prog_tm =
+  presLangTheory.flat_to_strs_def
+      |> SPECL [flat_prog_tm]
+      |> concl |> dest_eq |> fst |> EVAL |> concl |> rand
+      |> mlstring_app_list_to_string_list;
+
+fun clos_to_strs clos_prog_tm =
+  presLangTheory.clos_to_strs_def
+      |> SPECL [clos_prog_tm]
+      |> Q.SPEC ‘[]’
+      |> concl |> dest_eq |> fst |> EVAL |> concl |> rand
+      |> mlstring_app_list_to_string_list;
+
+fun bvl_to_strs names_tm bvl_prog_tm =
+  presLangTheory.bvl_to_strs_def
+      |> SPECL [names_tm,bvl_prog_tm]
+      |> concl |> dest_eq |> fst |> EVAL |> concl |> rand
+      |> mlstring_app_list_to_string_list;
+
+fun bvi_to_strs names_tm bvi_prog_tm =
+  presLangTheory.bvi_to_strs_def
+      |> SPECL [names_tm,bvi_prog_tm]
+      |> concl |> dest_eq |> fst |> EVAL |> concl |> rand
+      |> mlstring_app_list_to_string_list;
+
+fun data_to_strs names_tm data_prog_tm =
+  presLangTheory.data_to_strs_def
+      |> SPECL [names_tm,data_prog_tm]
+      |> concl |> dest_eq |> fst |> EVAL |> concl |> rand
+      |> mlstring_app_list_to_string_list;
+
+fun print_strs strs = app print strs;
+
+fun write_strs_to_file filename strs = let
+  val f = TextIO.openOut filename
+  val _ = app (curry TextIO.output f) strs
+  val _ = TextIO.closeOut f
+  in () end;
+
+end
diff --git a/compiler/backend/presLangScript.sml b/compiler/backend/presLangScript.sml
index f14ec23244..98e37b3253 100644
--- a/compiler/backend/presLangScript.sml
+++ b/compiler/backend/presLangScript.sml
@@ -6,37 +6,49 @@ open preamble astTheory mlintTheory mloptionTheory
 open flatLangTheory closLangTheory
      displayLangTheory source_to_flatTheory
      dataLangTheory wordLangTheory labLangTheory
-     stackLangTheory;
+     stackLangTheory bvlTheory clos_to_bvlTheory;
 
 val _ = new_theory"presLang";
 
 (* basics *)
 
-val empty_item_def = Define`
-  empty_item name = Item NONE name []`;
+Definition empty_item_def:
+  empty_item name = String name
+End
 
-val num_to_display_def = Define`
-  num_to_display (n : num) = String (toString n)`;
+Definition num_to_display_def:
+  num_to_display (n : num) = String (toString n)
+End
 
-val int_to_display_def = Define`
-  int_to_display (i : int) = String (toString i)`;
+Definition int_to_display_def:
+  int_to_display (i : int) = String (toString i)
+End
 
-val string_imp_def = Define`
-  string_imp s = String (implode s)`;
+Definition string_imp_def:
+  string_imp s = String (implode s)
+End
 
-val item_with_num_def = Define`
-  item_with_num name n = Item NONE name [num_to_display n]`;
+Definition item_with_num_def:
+  item_with_num name n = Item NONE name [num_to_display n]
+End
 
-val item_with_nums_def = Define`
-  item_with_nums name ns = Item NONE name (MAP num_to_display ns)`;
+Definition item_with_nums_def:
+  item_with_nums name ns = Item NONE name (MAP num_to_display ns)
+End
 
-val bool_to_display_def = Define`
-  bool_to_display b = empty_item (if b then strlit "True" else strlit "False")`;
+Definition bool_to_display_def:
+  bool_to_display b = empty_item (if b then strlit "True" else strlit "False")
+End
 
-val num_to_hex_def = Define `
+Definition num_to_hex_def:
   num_to_hex n =
     (if n < 16 then [] else num_to_hex (n DIV 16)) ++
-    num_to_hex_digit (n MOD 16)`;
+    num_to_hex_digit (n MOD 16)
+End
+
+Definition separate_lines_def:
+  separate_lines name xs = List (String name :: xs)
+End
 
 (* num_to_hex "implements" words$word_to_hex_string in a
    simple way that the translator can handle. these lemmas
@@ -59,11 +71,19 @@ Proof
   \\ (PURE_CASE_TAC \\ simp[ASCIInumbersTheory.n2s_def])
 QED
 
-val display_word_to_hex_string_def = Define `
-  display_word_to_hex_string w =
-    empty_item (implode ("0x" ++ num_to_hex (w2n w)))`;
+Definition num_to_hex_mlstring_def:
+  num_to_hex_mlstring n = implode ("0x" ++ num_to_hex n)
+End
+
+Definition word_to_display_def:
+  word_to_display w = empty_item (num_to_hex_mlstring (w2n w))
+End
 
-val lit_to_display_def = Define`
+Definition item_with_word_def:
+  item_with_word name w = Item NONE name [word_to_display w]
+End
+
+Definition lit_to_display_def:
   (lit_to_display (IntLit i) =
     Item NONE (strlit "IntLit") [empty_item (toString i)])
   /\
@@ -74,53 +94,61 @@ val lit_to_display_def = Define`
     Item NONE (strlit "StrLit") [string_imp s])
   /\
   (lit_to_display (Word8 w) =
-    Item NONE (strlit "Word8") [display_word_to_hex_string w])
+    Item NONE (strlit "Word8") [word_to_display w])
   /\
   (lit_to_display (Word64 w) =
-    Item NONE (strlit "Word64") [display_word_to_hex_string w])`;
+    Item NONE (strlit "Word64") [word_to_display w])
+End
 
-val list_to_display_def = Define`
-  (list_to_display f xs = displayLang$List (MAP f xs))`
+Definition list_to_display_def:
+  (list_to_display f xs = displayLang$Tuple (MAP f xs))
+End
 
-val option_to_display_def = Define`
+Definition option_to_display_def:
   (option_to_display f opt = case opt of
-          | NONE => empty_item (strlit "NONE")
-          | SOME opt' => Item NONE (strlit "SOME") [f opt'])`
+          | NONE => empty_item (strlit "none")
+          | SOME opt' => Item NONE (strlit "some") [f opt'])
+End
 
-(* semantic ops and values *)
+(* source *)
 
-val fp_cmp_to_display_def = Define `
+Definition fp_cmp_to_display_def:
   fp_cmp_to_display cmp = case cmp of
     | FP_Less => empty_item (strlit "FP_Less")
     | FP_LessEqual => empty_item (strlit "FP_LessEqual")
     | FP_Greater => empty_item (strlit "FP_Greater")
     | FP_GreaterEqual => empty_item (strlit "FP_GreaterEqual")
-    | FP_Equal => empty_item (strlit "FP_Equal")`
+    | FP_Equal => empty_item (strlit "FP_Equal")
+End
 
-val fp_uop_to_display_def = Define `
+Definition fp_uop_to_display_def:
   fp_uop_to_display op = case op of
     | FP_Abs => empty_item (strlit "FP_Abs")
     | FP_Neg => empty_item (strlit "FP_Neg")
-    | FP_Sqrt => empty_item (strlit "FP_Sqrt")`
+    | FP_Sqrt => empty_item (strlit "FP_Sqrt")
+End
 
-val fp_bop_to_display_def = Define `
+Definition fp_bop_to_display_def:
   fp_bop_to_display op = case op of
     | fpValTree$FP_Add => empty_item (strlit "FP_Add")
     | FP_Sub => empty_item (strlit "FP_Sub")
     | FP_Mul => empty_item (strlit "FP_Mul")
-    | FP_Div => empty_item (strlit "FP_Div")`
+    | FP_Div => empty_item (strlit "FP_Div")
+End
 
-val fp_top_to_display_def = Define `
+Definition fp_top_to_display_def:
   fp_top_to_display op =
     case op of
-      |FP_Fma => empty_item (strlit "FP_Fma")`
+      |FP_Fma => empty_item (strlit "FP_Fma")
+End
 
-val word_size_to_display_def = Define`
+Definition word_size_to_display_def:
   (word_size_to_display W8 = empty_item (strlit "W8"))
   /\
-  (word_size_to_display W64 = empty_item (strlit "W64"))`;
+  (word_size_to_display W64 = empty_item (strlit "W64"))
+End
 
-val opn_to_display_def = Define`
+Definition opn_to_display_def:
   (opn_to_display Plus = empty_item (strlit "Plus"))
   /\
   (opn_to_display Minus = empty_item (strlit "Minus"))
@@ -129,18 +157,20 @@ val opn_to_display_def = Define`
   /\
   (opn_to_display Divide = empty_item (strlit "Divide"))
   /\
-  (opn_to_display Modulo = empty_item (strlit "Modulo"))`;
+  (opn_to_display Modulo = empty_item (strlit "Modulo"))
+End
 
-val opb_to_display_def = Define`
+Definition opb_to_display_def:
   (opb_to_display Lt = empty_item (strlit "Lt"))
   /\
   (opb_to_display Gt = empty_item (strlit "Gt"))
   /\
   (opb_to_display Leq = empty_item (strlit "Leq"))
   /\
-  (opb_to_display Geq = empty_item (strlit "Geq"))`;
+  (opb_to_display Geq = empty_item (strlit "Geq"))
+End
 
-val opw_to_display_def = Define`
+Definition opw_to_display_def:
   (opw_to_display Andw = empty_item (strlit "Andw"))
   /\
   (opw_to_display Orw = empty_item (strlit "Orw"))
@@ -149,31 +179,210 @@ val opw_to_display_def = Define`
   /\
   (opw_to_display Add = empty_item (strlit "Add"))
   /\
-  (opw_to_display Sub = empty_item (strlit "Sub"))`;
+  (opw_to_display Sub = empty_item (strlit "Sub"))
+End
 
-val shift_to_display_def = Define`
+Definition shift_to_display_def:
   (shift_to_display Lsl = empty_item (strlit "Lsl"))
   /\
   (shift_to_display Lsr = empty_item (strlit "Lsr"))
   /\
   (shift_to_display Asr = empty_item (strlit "Asr"))
   /\
-  (shift_to_display Ror = empty_item (strlit "Ror"))`;
-
-
- (* flatLang *)
-
-val MEM_pat_size = prove(
-  ``!pats a. MEM a (pats:flatLang$pat list) ==> pat_size a < pat1_size pats``,
-  Induct \\ rw [] \\ rw [flatLangTheory.pat_size_def] \\ res_tac \\ fs []);
+  (shift_to_display Ror = empty_item (strlit "Ror"))
+End
+
+Definition op_to_display_def:
+  op_to_display (p:ast$op) =
+  case p of
+  | Opn op => opn_to_display op
+  | Opb op => opb_to_display op
+  | Opw ws op =>
+      Item NONE (strlit "Opw") [ word_size_to_display ws; opw_to_display op ]
+  | Shift ws sh num => Item NONE (strlit "Shift")
+                            [word_size_to_display ws;
+                             shift_to_display sh;
+                             num_to_display num]
+  | Equality => empty_item (strlit "Equality")
+  | FP_cmp cmp => fp_cmp_to_display cmp
+  | FP_uop op => fp_uop_to_display op
+  | FP_bop op => fp_bop_to_display op
+  | FP_top op => fp_top_to_display op
+  | FpFromWord => empty_item (strlit "FpFromWord")
+  | FpToWord => empty_item (strlit "FpToWord")
+  | Real_cmp cmp => empty_item (strlit "Real_cmp")
+  | Real_uop op => empty_item (strlit "Real_uop")
+  | Real_bop op => empty_item (strlit "Real_bop")
+  | RealFromFP => empty_item (strlit "RealFromFP")
+  | Opapp => empty_item (strlit "Opapp")
+  | Opassign => empty_item (strlit "Opassign")
+  | Opref => empty_item (strlit "Opref")
+  | Opderef => empty_item (strlit "Opderef")
+  | Aw8alloc => empty_item (strlit "Aw8alloc")
+  | Aw8sub => empty_item (strlit "Aw8sub")
+  | Aw8length => empty_item (strlit "Aw8length")
+  | Aw8update => empty_item (strlit "Aw8update")
+  | WordFromInt ws =>
+      Item NONE (strlit "WordFromInt") [word_size_to_display ws]
+  | WordToInt ws =>
+      Item NONE (strlit "WordToInt") [word_size_to_display ws]
+  | CopyStrStr => empty_item (strlit "CopyStrStr")
+  | CopyStrAw8 => empty_item (strlit "CopyStrAw8")
+  | CopyAw8Str => empty_item (strlit "CopyAw8Str")
+  | CopyAw8Aw8 => empty_item (strlit "CopyAw8Aw8")
+  | Ord => empty_item (strlit "Ord")
+  | Chr => empty_item (strlit "Chr")
+  | Chopb op => Item NONE (strlit "Chopb") [opb_to_display op]
+  | Implode => empty_item (strlit "Implode")
+  | Explode => empty_item (strlit "Explode")
+  | Strsub => empty_item (strlit "Strsub")
+  | Strlen => empty_item (strlit "Strlen")
+  | Strcat => empty_item (strlit "Strcat")
+  | VfromList => empty_item (strlit "VfromList")
+  | Vsub => empty_item (strlit "Vsub")
+  | Vlength => empty_item (strlit "Vlength")
+  | Aalloc => empty_item (strlit "Aalloc")
+  | AallocEmpty => empty_item (strlit "AallocEmpty")
+  | AallocFixed => empty_item (strlit "AallocFixed")
+  | Asub => empty_item (strlit "Asub")
+  | Alength => empty_item (strlit "Alength")
+  | Aupdate => empty_item (strlit "Aupdate")
+  | Asub_unsafe => empty_item (strlit "Asub_unsafe")
+  | Aupdate_unsafe => empty_item (strlit "Aupdate_unsafe")
+  | Aw8sub_unsafe => empty_item (strlit "Aw8sub_unsafe")
+  | Aw8update_unsafe => empty_item (strlit "Aw8update_unsafe")
+  | ListAppend => empty_item (strlit "ListAppend")
+  | ConfigGC => empty_item (strlit "ConfigGC")
+  | FFI v35 => empty_item (strlit "FFI v35")
+  | Eval => empty_item (strlit "Eval")
+  | Env_id => empty_item (strlit "Eval")
+End
+
+Definition lop_to_display_def:
+  lop_to_display (c:ast$lop) =
+  case c of
+  | And => empty_item «And»
+  | Or  => empty_item «Or»
+End
+
+Definition id_to_display_def:
+  id_to_display (Short n) =
+    Item NONE «Short» [String (implode n)] ∧
+  id_to_display (Long n i) =
+    Item NONE «Long» [String (implode n); id_to_display i]
+End
+
+Definition ast_t_to_display_def:
+  ast_t_to_display c =
+  case c of
+  | Atvar n => Item NONE «Atvar» [String (implode n)]
+  | Atfun t1 t2 => Item NONE «Atfun» [ast_t_to_display t1; ast_t_to_display t2]
+  | Attup ts => Item NONE «Attup» [Tuple (MAP ast_t_to_display ts)]
+  | Atapp ts id => Item NONE «Attup» [Tuple (MAP ast_t_to_display ts);
+                                      id_to_display id]
+Termination
+  WF_REL_TAC ‘measure ast_t_size’
+End
+
+Definition pat_to_display_def:
+  pat_to_display (c:ast$pat) =
+  case c of
+  | Pany => Item NONE «Pany» []
+  | Pvar v => Item NONE «Pvar» [String (implode v)]
+  | Plit l => Item NONE «Plit» [lit_to_display l]
+  | Pcon opt_id pats =>
+      Item NONE «Pcon» [option_to_display id_to_display opt_id;
+                        Tuple (MAP pat_to_display pats)]
+  | Pas t v => Item NONE «Pas» [pat_to_display t; String (implode v)]
+  | Pref t => Item NONE «Pref» [pat_to_display t]
+  | Ptannot x y => Item NONE «Ptannot» [pat_to_display x; ast_t_to_display y]
+Termination
+  WF_REL_TAC ‘measure pat_size’
+End
+
+Definition exp_to_display_def:
+  exp_to_display (c:ast$exp) =
+  case c of
+  | Lit l => Item NONE «Lit» [lit_to_display l]
+  | Raise e => Item NONE «Raise» [exp_to_display e]
+  | Con opt_id es => Item NONE «Con» [option_to_display id_to_display opt_id;
+                                      Tuple (MAP exp_to_display es)]
+  | Var id => Item NONE «Var» [id_to_display id]
+  | Fun n e => Item NONE «Fun» [String (implode n); exp_to_display e]
+  | App op es => Item NONE «App» (op_to_display op ::
+                                  MAP exp_to_display es)
+  | Log lop e1 e2 => Item NONE «Log» [lop_to_display lop;
+                                      exp_to_display e1;
+                                      exp_to_display e2]
+  | If e1 e2 e3 => Item NONE «If» [exp_to_display e1;
+                                   exp_to_display e2;
+                                   exp_to_display e3]
+  | Let n_opt e1 e2 => Item NONE «Let»
+      [option_to_display (λn. String (implode n)) n_opt;
+       exp_to_display e1;
+       exp_to_display e2]
+  | Mat e pats => Item NONE «Mat»
+      [exp_to_display e;
+       Tuple (MAP (λ(p,e). Tuple [pat_to_display p; exp_to_display e]) pats)]
+  | Handle e pats => Item NONE «Handle»
+      [exp_to_display e;
+       Tuple (MAP (λ(p,e). Tuple [pat_to_display p; exp_to_display e]) pats)]
+  | Letrec fns e => Item NONE «Letrec»
+      [Tuple (MAP (λ(m,n,e). Tuple [String (implode m);
+                                    String (implode n);
+                                    exp_to_display e]) fns);
+       exp_to_display e]
+  | Tannot e _ => Item NONE «Tannot» [exp_to_display e]
+  | Lannot e _ => Item NONE «Lannot» [exp_to_display e]
+  | FpOptimise _ e => Item NONE «FpOptimise» [exp_to_display e]
+Termination
+  WF_REL_TAC ‘measure exp_size’
+End
+
+Definition source_to_display_dec_def:
+  source_to_display_dec (d:ast$dec) =
+  case d of
+  | Dlet _ pat e => Item NONE «Dlet» [pat_to_display pat; exp_to_display e]
+  | Dletrec _ fns => Item NONE «Dletrec»
+                          (MAP (λ(m,n,e). Tuple [String (implode m);
+                                                 String (implode n);
+                                                 exp_to_display e]) fns)
+  | Dtype _ ts => Item NONE «Dtype» (MAP (λ(ns,n,z).
+                    Tuple [Tuple (MAP (λn. String (implode n)) ns);
+                           String (implode n);
+                           Tuple (MAP (λ(n,tys). Tuple [String (implode n);
+                              Tuple (MAP ast_t_to_display tys)]) z)]) ts)
+  | Dtabbrev _ ns n ty =>
+      Item NONE «Dtabbrev» [Tuple (MAP (λn. String (implode n)) ns);
+                            String (implode n);
+                            ast_t_to_display ty]
+  | Dexn _ n tys => Item NONE «Dexn» [String (implode n);
+                                      Tuple (MAP ast_t_to_display tys)]
+  | Dmod n ds => Item NONE «Dmod» [String (implode n);
+                                   Tuple (MAP source_to_display_dec ds)]
+  | Dlocal xs ys => Item NONE «Dlocal» [Tuple (MAP source_to_display_dec xs);
+                                        Tuple (MAP source_to_display_dec ys)]
+  | Denv n => Item NONE «Denv» [String (implode n)]
+Termination
+  WF_REL_TAC ‘measure dec_size’
+End
+
+(* flatLang *)
+
+Triviality MEM_pat_size:
+  !pats a. MEM a (pats:flatLang$pat list) ==> pat_size a < pat1_size pats
+Proof
+  Induct \\ rw [] \\ rw [flatLangTheory.pat_size_def] \\ res_tac \\ fs []
+QED
 
-val opt_con_to_display_def = Define `
+Definition opt_con_to_display_def:
   opt_con_to_display ocon = case ocon of
     | NONE => empty_item (strlit "ConIdNone")
     | SOME (c, NONE) => item_with_num (strlit "ConIdUntyped") c
-    | SOME (c, SOME t) => item_with_nums (strlit "ConIdTyped") [c; t]`
+    | SOME (c, SOME t) => item_with_nums (strlit "ConIdTyped") [c; t]
+End
 
-val flat_pat_to_display_def = tDefine "flat_pat_to_display" `
+Definition flat_pat_to_display_def:
   flat_pat_to_display p =
     case p of
        | flatLang$Pvar varN => Item NONE (strlit "Pvar") [string_imp varN]
@@ -183,11 +392,13 @@ val flat_pat_to_display_def = tDefine "flat_pat_to_display" `
             (MAP flat_pat_to_display pats)
        | Pas pat varN => Item NONE (strlit "Pas") [flat_pat_to_display pat;
                                                    string_imp varN]
-       | Pref pat => Item NONE (strlit "Pref") [flat_pat_to_display pat] `
-  (WF_REL_TAC `measure pat_size` \\ rw []
-   \\ imp_res_tac MEM_pat_size \\ fs [])
+       | Pref pat => Item NONE (strlit "Pref") [flat_pat_to_display pat]
+Termination
+  WF_REL_TAC `measure pat_size` \\ rw []
+  \\ imp_res_tac MEM_pat_size \\ fs []
+End
 
-val flat_op_to_display_def = Define `
+Definition flat_op_to_display_def:
   flat_op_to_display op = case op of
     | Opn op => opn_to_display op
     | Opb op => opb_to_display op
@@ -196,8 +407,7 @@ val flat_op_to_display_def = Define `
     | Shift ws sh num => Item NONE (strlit "Shift") [
       word_size_to_display ws;
       shift_to_display sh;
-      num_to_display num
-    ]
+      num_to_display num]
     | Equality => empty_item (strlit "Equality")
     | FP_cmp cmp => fp_cmp_to_display cmp
     | FP_uop op => fp_uop_to_display op
@@ -249,144 +459,189 @@ val flat_op_to_display_def = Define `
     | LenEq n1 => item_with_nums (strlit "LenEq") [n1]
     | El n => item_with_num (strlit "El") n
     | Id => empty_item (strlit "Id")
-    `
+End
 
-val MEM_funs_size = prove(
-  ``!fs v1 v2 e. MEM (v1,v2,e) fs ==> flatLang$exp_size e < exp1_size fs``,
+Triviality MEM_funs_size:
+  !fs v1 v2 e. MEM (v1,v2,e) fs ==> flatLang$exp_size e < exp1_size fs
+Proof
   Induct \\ fs [flatLangTheory.exp_size_def] \\ rw []
-  \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []);
+  \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []
+QED
 
-val MEM_exps_size = prove(
-  ``!exps e. MEM e exps ==> flatLang$exp_size e < exp6_size exps``,
+Triviality MEM_exps_size:
+  !exps e. MEM e exps ==> flatLang$exp_size e < exp6_size exps
+Proof
   Induct \\ fs [flatLangTheory.exp_size_def] \\ rw []
-  \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []);
+  \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []
+QED
 
-val MEM_pats_size = prove(
-  ``!pats p e. MEM (p, e) pats ==> flatLang$exp_size e < exp3_size pats``,
+Triviality MEM_pats_size:
+  !pats p e. MEM (p, e) pats ==> flatLang$exp_size e < exp3_size pats
+Proof
   Induct \\ fs [flatLangTheory.exp_size_def] \\ rw []
-  \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []);
+  \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []
+QED
 
-val flat_to_display_def = tDefine"flat_to_display" `
+Definition add_name_hint_def:
+  add_name_hint prefix name_hint =
+    concat [prefix; strlit "<"; name_hint; strlit ">"]
+End
+
+Definition flat_to_display_def:
   (flat_to_display (flatLang$Raise tra exp) =
-    Item (SOME tra) (strlit "Raise") [flat_to_display exp])
+    Item (SOME tra) (strlit "raise") [flat_to_display exp])
   /\
   (flat_to_display (Handle tra exp pes) =
-    Item (SOME tra) (strlit "Handle") (flat_to_display exp
+    Item (SOME tra) (strlit "handle") (flat_to_display exp
         :: MAP (\(pat,exp). displayLang$Tuple [flat_pat_to_display pat; flat_to_display exp]) pes))
   /\
-  (flat_to_display (Lit tra lit) = Item (SOME tra) (strlit "Lit") [])
+  (flat_to_display (Lit tra lit) = Item (SOME tra) (strlit "lit") [])
   /\
   (flat_to_display (flatLang$Con tra id_opt exps) =
-    Item (SOME tra) (strlit "Con") (opt_con_to_display id_opt
+    Item (SOME tra) (strlit "con") (opt_con_to_display id_opt
         :: MAP flat_to_display exps))
   /\
   (flat_to_display (Var_local tra varN) =
-    Item (SOME tra) (strlit "Var_local") [string_imp varN])
+    Item (SOME tra) (strlit "var_local") [string_imp varN])
   /\
-  (flat_to_display (Fun _ varN exp) =
-    Item (SOME None) (strlit "Fun") [string_imp varN; flat_to_display exp])
+  (flat_to_display (Fun name_hint varN exp) =
+    Item (SOME None) (add_name_hint (strlit "fun") (implode name_hint))
+      [string_imp varN; flat_to_display exp])
   /\
   (flat_to_display (App tra op exps) =
-    Item (SOME tra) (strlit "App") (flat_op_to_display op :: MAP flat_to_display exps))
+    Item (SOME tra) (strlit "app") (flat_op_to_display op :: MAP flat_to_display exps))
   /\
   (flat_to_display (If tra exp1 exp2 exp3) =
-    Item (SOME tra) (strlit "If") [flat_to_display exp1; flat_to_display exp2;
+    Item (SOME tra) (strlit "if") [flat_to_display exp1; flat_to_display exp2;
         flat_to_display exp3])
   /\
   (flat_to_display (Mat tra exp pes) =
-    Item (SOME tra) (strlit "Mat") (flat_to_display exp
+    Item (SOME tra) (strlit "mat") (flat_to_display exp
         :: MAP (\(pat,exp). displayLang$Tuple [flat_pat_to_display pat; flat_to_display exp]) pes))
   /\
   (flat_to_display (Let tra varN_opt exp1 exp2) =
-    Item (SOME tra) (strlit "Let") [option_to_display string_imp varN_opt;
+    Item (SOME tra) (strlit "let") [option_to_display string_imp varN_opt;
         flat_to_display exp1; flat_to_display exp2])
   /\
-  (flat_to_display (Letrec _ funs exp) =
-    Item (SOME None) (strlit "Letrec")
-        [List (MAP (\(v1,v2,e). Tuple [string_imp v1; string_imp v2;
+  (flat_to_display (Letrec name_hint funs exp) =
+    Item (SOME None) (add_name_hint (strlit "letrec") (implode name_hint))
+        [Tuple (MAP (\(v1,v2,e). Tuple [string_imp v1; string_imp v2;
               flat_to_display e]) funs); flat_to_display exp]
-  )`
-  (WF_REL_TAC `inv_image $< (flatLang$exp_size)`
-   \\ rw [flatLangTheory.exp_size_def]
-   \\ imp_res_tac MEM_funs_size \\ fs []
-   \\ imp_res_tac MEM_exps_size \\ fs []
-   \\ imp_res_tac MEM_pats_size \\ fs []
-);
-
-val flat_to_display_dec_def = Define`
-  flat_to_display_dec d =
+  )
+Termination
+  WF_REL_TAC `inv_image $< (flatLang$exp_size)`
+  \\ rw [flatLangTheory.exp_size_def]
+  \\ imp_res_tac MEM_funs_size \\ fs []
+  \\ imp_res_tac MEM_exps_size \\ fs []
+  \\ imp_res_tac MEM_pats_size \\ fs []
+End
+
+Definition flat_to_display_dec_def:
+  flat_to_display_dec (d:flatLang$dec) =
     case d of
-       | Dlet exp => Item NONE (strlit "Dlet") [flat_to_display exp]
-       | Dtype mods con_arities => item_with_num (strlit "Dtype") mods
-       | Dexn n1 n2 => item_with_nums (strlit "Dexn") [n1; n2]`
+       | Dlet exp => Item NONE (strlit "dlet") [flat_to_display exp]
+       | Dtype mods con_arities => item_with_num (strlit "dtype") mods
+       | Dexn n1 n2 => item_with_nums (strlit "dexn") [n1; n2]
+End
 
-val flat_to_display_decs_def = Define`
-  flat_to_display_decs = list_to_display flat_to_display_dec`;
-
-(* pat to displayLang *)
+(* clos to displayLang *)
 
-val num_to_varn_def = tDefine "num_to_varn" `
+Definition num_to_varn_def:
   num_to_varn n = if n < 26 then [CHR (97 + n)]
-                  else (num_to_varn ((n DIV 26)-1)) ++ ([CHR (97 + (n MOD 26))])`
-  (WF_REL_TAC `measure I` \\ rw [] \\ fs [DIV_LT_X]);
+                  else (num_to_varn ((n DIV 26)-1)) ++ ([CHR (97 + (n MOD 26))])
+Termination
+  WF_REL_TAC `measure I` \\ rw [] \\ fs [DIV_LT_X]
+End
 
-val display_num_as_varn_def = Define `
-  display_num_as_varn n = string_imp (num_to_varn n)`;
+Definition display_num_as_varn_def:
+  display_num_as_varn n = string_imp (num_to_varn n)
+End
 
-(* clos to displayLang *)
-
-val num_to_varn_list_def = Define `
+Definition num_to_varn_list_def:
   num_to_varn_list h n =
     if n = 0 then [] else
-      num_to_varn (h + n) :: num_to_varn_list h (n-1)`
-
-val clos_op_to_display_def = Define `
-  clos_op_to_display op = case op of
+      num_to_varn (h + n) :: num_to_varn_list h (n-1)
+End
+
+Definition attach_name_def:
+  attach_name ns NONE = strlit "none" ∧
+  attach_name ns (SOME d) =
+    case lookup d ns of
+    | NONE => toString d
+    | SOME name => concat [name; strlit "@"; toString d]
+End
+
+Definition const_part_to_display_def:
+  const_part_to_display (Int i : const_part) =
+    Item NONE (strlit "Int") [int_to_display i] ∧
+  const_part_to_display (Con t vs) =
+    Item NONE (strlit "Con") [num_to_display t; Tuple (MAP num_to_display vs)] ∧
+  const_part_to_display (Str s) =
+    Item NONE (strlit "Str") [String (concat [strlit "\""; s; strlit "\""])] ∧
+  const_part_to_display (W64 w) =
+    Item NONE (strlit "W64") [word_to_display w]
+End
+
+Definition const_to_display_def:
+  const_to_display (ConstInt i : const) =
+    Item NONE (strlit "ConstInt") [int_to_display i] ∧
+  const_to_display (ConstCons t vs) =
+    Item NONE (strlit "ConstCons") [num_to_display t; Tuple (MAP const_to_display vs)] ∧
+  const_to_display (ConstStr s) =
+    Item NONE (strlit "ConstStr") [String (concat [strlit "\""; s; strlit "\""])] ∧
+  const_to_display (ConstWord64 w) =
+    Item NONE (strlit "ConstWord64") [word_to_display w]
+Termination
+  WF_REL_TAC ‘measure const_size’
+End
+
+Definition clos_op_to_display_def:
+  clos_op_to_display ns op = case op of
     | Global num => item_with_num (strlit "Global") num
     | SetGlobal num => item_with_num (strlit "SetGlobal") num
-    | AllocGlobal => empty_item (strlit "AllocGlobal")
-    | GlobalsPtr => empty_item (strlit "GlobalsPtr")
-    | SetGlobalsPtr => empty_item (strlit "SetGlobalsPtr")
+    | AllocGlobal => String (strlit "AllocGlobal")
+    | GlobalsPtr => String (strlit "GlobalsPtr")
+    | SetGlobalsPtr => String (strlit "SetGlobalsPtr")
     | Cons num => item_with_num (strlit "Cons") num
-    | Constant _ => empty_item(strlit "Constant")
+    | Constant c => Item NONE (strlit "Constant") [const_to_display c]
     | ConsExtend num => item_with_num (strlit "ConsExtend") num
-    | Build _ => empty_item(strlit "Build")
-    | El => empty_item (strlit "El")
-    | LengthBlock => empty_item (strlit "LengthBlock")
-    | Length => empty_item (strlit "Length")
-    | LengthByte => empty_item (strlit "LengthByte")
+    | Build bs => Item NONE (strlit "Build") (MAP const_part_to_display bs)
+    | El => String (strlit "El")
+    | LengthBlock => String (strlit "LengthBlock")
+    | Length => String (strlit "Length")
+    | LengthByte => String (strlit "LengthByte")
     | RefByte b => Item NONE (strlit "RefByte") [bool_to_display b]
-    | RefArray => empty_item (strlit "RefArray")
-    | DerefByte => empty_item (strlit "DerefByte")
-    | UpdateByte => empty_item (strlit "UpdateByte")
-    | ConcatByteVec => empty_item (strlit "ConcatByteVec")
+    | RefArray => String (strlit "RefArray")
+    | DerefByte => String (strlit "DerefByte")
+    | UpdateByte => String (strlit "UpdateByte")
+    | ConcatByteVec => String (strlit "ConcatByteVec")
     | CopyByte b => Item NONE (strlit "CopyByte") [bool_to_display b]
-    | ListAppend => empty_item (strlit "ListAppend")
+    | ListAppend => String (strlit "ListAppend")
     | FromList num => item_with_num (strlit "FromList") num
-    | FromListByte => empty_item (strlit "FromListByte")
-    | ToListByte => empty_item (strlit "ToListByte")
-    | LengthByteVec => empty_item (strlit "LengthByteVec")
-    | DerefByteVec => empty_item (strlit "DerefByteVec")
+    | FromListByte => String (strlit "FromListByte")
+    | ToListByte => String (strlit "ToListByte")
+    | LengthByteVec => String (strlit "LengthByteVec")
+    | DerefByteVec => String (strlit "DerefByteVec")
     | TagLenEq n1 n2 => item_with_nums (strlit "TagLenEq") [n1; n2]
     | ElemAt num => item_with_num (strlit "ElemAt") num
     | LenEq num => item_with_num (strlit "LenEq") num
     | TagEq num => item_with_num (strlit "TagEq") num
-    | Ref => empty_item (strlit "Ref")
-    | Update => empty_item (strlit "Update")
-    | Label num => item_with_num (strlit "Label") num
+    | Ref => String (strlit "Ref")
+    | Update => String (strlit "Update")
+    | Label num => Item NONE (strlit "Label") [String (attach_name ns (SOME num))]
     | FFI s => Item NONE (strlit "FFI") [string_imp s]
-    | Equal => empty_item (strlit "Equal")
-    | EqualConst c => Item NONE (strlit "EqualConst") [] (* TODO: fix *)
+    | Equal => String (strlit "Equal")
+    | EqualConst c => Item NONE (strlit "EqualConst") [const_part_to_display c]
     | Const i => Item NONE (strlit "Const") [int_to_display i]
-    | Add => empty_item (strlit "Add")
-    | Sub => empty_item (strlit "Sub")
-    | Mult => empty_item (strlit "Mult")
-    | Div => empty_item (strlit "Div")
-    | Mod => empty_item (strlit "Mod")
-    | Less => empty_item (strlit "Less")
-    | LessEq => empty_item (strlit "LessEq")
-    | Greater => empty_item (strlit "Greater")
-    | GreaterEq => empty_item (strlit "GreaterEq")
+    | Add => String (strlit "Add")
+    | Sub => String (strlit "Sub")
+    | Mult => String (strlit "Mult")
+    | Div => String (strlit "Div")
+    | Mod => String (strlit "Mod")
+    | Less => String (strlit "Less")
+    | LessEq => String (strlit "LessEq")
+    | Greater => String (strlit "Greater")
+    | GreaterEq => String (strlit "GreaterEq")
     | WordOp ws op =>
         Item NONE (strlit "WordOp") [ word_size_to_display ws; opw_to_display op ]
     | WordShift ws sh num => Item NONE (strlit "WordShift") [
@@ -394,145 +649,302 @@ val clos_op_to_display_def = Define `
       shift_to_display sh;
       num_to_display num
     ]
-    | WordFromInt => empty_item (strlit "WordFromInt")
-    | WordToInt => empty_item (strlit "WordToInt")
+    | WordFromInt => String (strlit "WordFromInt")
+    | WordToInt => String (strlit "WordToInt")
     | WordFromWord b => Item NONE (strlit "WordFromWord") [bool_to_display b]
     | FP_cmp cmp => fp_cmp_to_display cmp
     | FP_uop op => fp_uop_to_display op
     | FP_bop op => fp_bop_to_display op
     | FP_top op => fp_top_to_display op
-    | BoundsCheckBlock => empty_item (strlit "BoundsCheckBlock")
-    | BoundsCheckArray => empty_item (strlit "BoundsCheckArray")
+    | BoundsCheckBlock => String (strlit "BoundsCheckBlock")
+    | BoundsCheckArray => String (strlit "BoundsCheckArray")
     | BoundsCheckByte b => Item NONE (strlit "BoundsCheckByte") [bool_to_display b]
     | LessConstSmall num => item_with_num (strlit "LessConstSmall") num
-    | closLang$ConfigGC => empty_item (strlit "ConfigGC")
-    | Install => empty_item (strlit "Install")
-`
+    | closLang$ConfigGC => String (strlit "ConfigGC")
+    | Install => String (strlit "Install")
+End
 
-val MEM_clos_exps_size = prove(
-  ``!exps e. MEM e exps ==> closLang$exp_size e < exp3_size exps``,
+Triviality MEM_clos_exps_size:
+  !exps e. MEM e exps ==> closLang$exp_size e < exp3_size exps
+Proof
   Induct \\ fs [closLangTheory.exp_size_def] \\ rw []
-  \\ fs [closLangTheory.exp_size_def] \\ res_tac \\ fs []);
+  \\ fs [closLangTheory.exp_size_def] \\ res_tac \\ fs []
+QED
 
-(* The clos_to_display function uses the same approach to de bruijn
+Definition commas_def:
+  commas [] = strlit "" ∧
+  commas [x] = x ∧
+  commas (x::xs) = x ^ strlit "," ^ commas xs
+End
+
+(* The clos_to_display ns function uses the same approach to de bruijn
    indices as the pat_to_display function *)
-val clos_to_display_def = tDefine "clos_to_display" `
-  (clos_to_display h (Var t n) =
-    Item (SOME t) (strlit "Var") [display_num_as_varn (h-n-1)]) /\
-  (clos_to_display h (If t x1 x2 x3) =
-    Item (SOME t) (strlit "If") [clos_to_display h x1; clos_to_display h x2;
-        clos_to_display h x3]) /\
-  (clos_to_display h (closLang$Let t xs x) =
-    Item (SOME t) (strlit "Let'")
-        [List (clos_to_display_lets h (LENGTH xs - 1) xs);
-            clos_to_display (h + LENGTH xs) x]) /\
-  (clos_to_display h (Raise t x) =
-    Item (SOME t) (strlit "Raise") [clos_to_display h x]) /\
-  (clos_to_display h (Tick t x) =
-    Item (SOME t) (strlit "Tick") [clos_to_display h x]) /\
-  (clos_to_display h (Handle t x y) =
-    Item (SOME t) (strlit "Handle")
-        [clos_to_display h x; display_num_as_varn h;
-            clos_to_display (h+1) y]) /\
-  (clos_to_display h (Call t ticks dest xs) =
-    Item (SOME t) (strlit "Call") [num_to_display ticks; num_to_display dest;
-       List (MAP (clos_to_display h) xs)]) /\
-  (clos_to_display h (App t opt_n x xs) =
-    Item (SOME t) (strlit "App'")
-        [option_to_display num_to_display opt_n;
-         clos_to_display h x; List (MAP (clos_to_display h) xs)]) /\
-  (clos_to_display h (Fn _ n1 n2 vn x) =
-    Item (SOME None) (strlit "Fn")
+Definition clos_to_display_def:
+  (clos_to_display ns h (Var t n) =
+    Item (SOME t) (strlit "var") [display_num_as_varn (h-n-1)]) /\
+  (clos_to_display ns h (If t x1 x2 x3) =
+    Item (SOME t) (strlit "if") [clos_to_display ns h x1; clos_to_display ns h x2;
+        clos_to_display ns h x3]) /\
+  (clos_to_display ns h (closLang$Let t xs x) =
+    separate_lines (strlit "let")
+        [Tuple (clos_to_display_lets ns h (LENGTH xs - 1) xs);
+            clos_to_display ns (h + LENGTH xs) x]) /\
+  (clos_to_display ns h (Raise t x) =
+    Item (SOME t) (strlit "raise") [clos_to_display ns h x]) /\
+  (clos_to_display ns h (Tick t x) =
+    Item (SOME t) (strlit "tick") [clos_to_display ns h x]) /\
+  (clos_to_display ns h (Handle t x y) =
+    Item (SOME t) (strlit "handle")
+        [clos_to_display ns h x; display_num_as_varn h;
+            clos_to_display ns (h+1) y]) /\
+  (clos_to_display ns h (Call t ticks dest xs) =
+    Item (SOME t) (strlit "call")
+      ([num_to_display ticks; String (attach_name ns (SOME dest))] ++
+       MAP (clos_to_display ns h) xs)) /\
+  (clos_to_display ns h (App t opt_n x xs) =
+    Item (SOME t) (strlit "app")
+        ([option_to_display num_to_display opt_n;
+          clos_to_display ns h x] ++ MAP (clos_to_display ns h) xs)) /\
+  (clos_to_display ns h (Fn name_hint n1 n2 vn x) =
+    Item (SOME None) (add_name_hint (strlit "fn") name_hint)
         [option_to_display num_to_display n1;
          option_to_display (list_to_display num_to_display) n2;
          list_to_display string_imp (num_to_varn_list h vn);
-         clos_to_display h x]) /\
-  (clos_to_display h (closLang$Letrec _ n1 n2 es e) =
-    Item (SOME None) (strlit "Letrec'")
+         clos_to_display ns h x]) /\
+  (clos_to_display ns h (closLang$Letrec name_hint n1 n2 es e) =
+    Item (SOME None) (add_name_hint (strlit "letrec") (commas name_hint))
         [option_to_display num_to_display n1;
          option_to_display (list_to_display num_to_display) n2;
-         List (clos_to_display_letrecs h (LENGTH es-1) (LENGTH es) es);
-         clos_to_display h e]) /\
-  (clos_to_display h (Op t op xs) =
-    Item (SOME t) (strlit "Op") [clos_op_to_display op;
-        List (MAP (clos_to_display h) xs)]) /\
-  (clos_to_display_lets h i [] = []) /\
-  (clos_to_display_lets h i (x::xs) =
-    Tuple [display_num_as_varn (h+i); clos_to_display h x] :: clos_to_display_lets h (i-1) xs) /\
-  (clos_to_display_letrecs h i len [] = []) /\
-  (clos_to_display_letrecs h i len ((vn,e)::es) =
+         Tuple (clos_to_display_letrecs ns h (LENGTH es-1) (LENGTH es) es);
+         clos_to_display ns h e]) /\
+  (clos_to_display ns h (Op t op xs) =
+    Item (SOME t) (strlit "op") (clos_op_to_display LN op ::
+        MAP (clos_to_display ns h) xs)) /\
+  (clos_to_display_lets ns h i [] = []) /\
+  (clos_to_display_lets ns h i (x::xs) =
+    Tuple [display_num_as_varn (h+i); String (strlit "<-"); clos_to_display ns h x]
+      :: clos_to_display_lets ns h (i-1) xs) /\
+  (clos_to_display_letrecs ns h i len [] = []) /\
+  (clos_to_display_letrecs ns h i len ((vn,e)::es) =
     Tuple [display_num_as_varn (h+i);
         list_to_display string_imp (num_to_varn_list (h+len-1) vn);
-        clos_to_display (h+len+vn) e]
-    :: clos_to_display_letrecs h (i-1) len es)`
- (WF_REL_TAC `measure (\x. case x of
-    | INL (_,e) => exp_size e
-    | INR (INL (_,_,es)) => exp3_size es
-    | INR (INR (_,_,_,es)) => exp1_size es)`
+        clos_to_display ns (h+len+vn) e]
+    :: clos_to_display_letrecs ns h (i-1) len es)
+Termination
+  WF_REL_TAC `measure (\x. case x of
+    | INL (_,_,e) => exp_size e
+    | INR (INL (_,_,_,es)) => exp3_size es
+    | INR (INR (_,_,_,_,es)) => exp1_size es)`
   \\ rw [closLangTheory.exp_size_def]
   \\ imp_res_tac MEM_clos_exps_size \\ fs []
- );
+End
+
+Definition clos_fun_to_display_def:
+  clos_fun_to_display names (n,argc,body) =
+    Tuple [String «func»;
+           String (attach_name names (SOME n));
+           Tuple (REVERSE $ GENLIST display_num_as_varn argc);
+           clos_to_display names argc body]
+End
+
+Definition clos_dec_to_display_def:
+  clos_dec_to_display names dec =
+    Tuple [String «dec»;
+           clos_to_display names 0 dec]
+End
+
+(* bvl to displayLang *)
+
+Triviality MEM_bvl_exps_size:
+  !exps e. MEM e exps ==> bvl$exp_size e < exp1_size exps
+Proof
+  Induct \\ fs [bvlTheory.exp_size_def] \\ rw []
+  \\ fs [bvlTheory.exp_size_def] \\ res_tac \\ fs []
+QED
+
+Definition bvl_to_display_def:
+  (bvl_to_display ns h (Var n) =
+    Item NONE (strlit "var") [display_num_as_varn (h-n-1)]) /\
+  (bvl_to_display ns h (If x1 x2 x3) =
+    Item NONE (strlit "if") [bvl_to_display ns h x1; bvl_to_display ns h x2;
+        bvl_to_display ns h x3]) /\
+  (bvl_to_display ns h (bvl$Let xs x) =
+    separate_lines (strlit "let")
+        (bvl_to_display_lets ns h (LENGTH xs - 1) xs ++
+            [bvl_to_display ns (h + LENGTH xs) x])) /\
+  (bvl_to_display ns h (Raise x) =
+    Item NONE (strlit "raise") [bvl_to_display ns h x]) /\
+  (bvl_to_display ns h (Tick x) =
+    Item NONE (strlit "tick") [bvl_to_display ns h x]) /\
+  (bvl_to_display ns h (Handle x y) =
+    Item NONE (strlit "handle")
+        [bvl_to_display ns h x; display_num_as_varn h;
+            bvl_to_display ns (h+1) y]) /\
+  (bvl_to_display ns h (Call ticks dest xs) =
+    Item NONE (strlit "call")
+         (String (attach_name ns dest) ::
+          MAP (bvl_to_display ns h) xs)) /\
+  (bvl_to_display ns h (Op op xs) =
+    Item NONE (strlit "op") (clos_op_to_display ns op ::
+                             MAP (bvl_to_display ns h) xs)) /\
+  (bvl_to_display_lets ns h i [] = []) /\
+  (bvl_to_display_lets ns h i (x::xs) =
+    Tuple [display_num_as_varn (h+i); String (strlit "<-"); bvl_to_display ns h x]
+    :: bvl_to_display_lets ns h (i-1) xs)
+Termination
+  WF_REL_TAC ‘measure $ λx. case x of INL (ns,h,x) => exp_size x
+                                    | INR (ns,h,i,xs) => exp1_size xs’
+End
+
+Definition bvl_fun_to_display_def:
+  bvl_fun_to_display names (n,argc,body) =
+    Tuple [String «func»;
+           String (attach_name names (SOME n));
+           Tuple (REVERSE $ GENLIST display_num_as_varn argc);
+           bvl_to_display names argc body]
+End
+
+(* bvi to displayLang *)
+
+Triviality MEM_bvi_exps_size:
+  !exps e. MEM e exps ==> bvi$exp_size e < exp2_size exps
+Proof
+  Induct \\ fs [bviTheory.exp_size_def] \\ rw []
+  \\ fs [bviTheory.exp_size_def] \\ res_tac \\ fs []
+QED
+
+Definition bvi_to_display_def:
+  (bvi_to_display ns h (Var n) =
+    Item NONE (strlit "var") [display_num_as_varn (h-n-1)]) /\
+  (bvi_to_display ns h (If x1 x2 x3) =
+    Item NONE (strlit "if") [bvi_to_display ns h x1; bvi_to_display ns h x2;
+        bvi_to_display ns h x3]) /\
+  (bvi_to_display ns h (bvi$Let xs x) =
+    separate_lines (strlit "let")
+        (bvi_to_display_lets ns h (LENGTH xs - 1) xs ++
+            [bvi_to_display ns (h + LENGTH xs) x])) /\
+  (bvi_to_display ns h (Raise x) =
+    Item NONE (strlit "raise") [bvi_to_display ns h x]) /\
+  (bvi_to_display ns h (Tick x) =
+    Item NONE (strlit "tick") [bvi_to_display ns h x]) /\
+  (bvi_to_display ns h (Call ticks dest xs handler) =
+    Item NONE (strlit "call")
+         (String (attach_name ns dest) ::
+          MAP (bvi_to_display ns h) xs ++
+          (case handler of
+           | NONE => []
+           | SOME e => [Item NONE (strlit "handler") [display_num_as_varn h;
+                                                      empty_item (strlit "->");
+                                                      bvi_to_display ns (h+1) e]]))) /\
+  (bvi_to_display ns h (Op op xs) =
+    Item NONE (strlit "op") (clos_op_to_display ns op ::
+                             MAP (bvi_to_display ns h) xs)) /\
+  (bvi_to_display_lets ns h i [] = []) /\
+  (bvi_to_display_lets ns h i (x::xs) =
+    Tuple [display_num_as_varn (h+i); String (strlit "<-"); bvi_to_display ns h x]
+    :: bvi_to_display_lets ns h (i-1) xs)
+Termination
+  WF_REL_TAC ‘measure $ λx. case x of INL (ns,h,x) => exp_size x
+                                    | INR (ns,h,i,xs) => exp2_size xs’
+End
+
+Definition bvi_fun_to_display_def:
+  bvi_fun_to_display names (n,argc,body) =
+    Tuple [String «func»;
+           String (attach_name names (SOME n));
+           Tuple (REVERSE $ GENLIST display_num_as_varn argc);
+           bvi_to_display names argc body]
+End
 
 (* dataLang *)
 
-val num_set_to_display_def = Define
-  `num_set_to_display ns = List (MAP num_to_display
-    (MAP FST (sptree$toAList ns)))`;
+Definition num_set_to_display_def:
+  num_set_to_display ns =
+    String $ concat [strlit "{";
+                     commas (MAP toString (MAP FST (sptree$toSortedAList ns)));
+                     strlit "}"]
+End
+
+Definition data_seqs_def:
+  data_seqs z =
+    case z of
+    | dataLang$Seq x y => Append (data_seqs x) (data_seqs y)
+    | _ => List [z]
+End
+
+Triviality MEM_append_data_seqs:
+  ∀x. MEM a (append (data_seqs x)) ⇒ prog_size a ≤ prog_size x
+Proof
+  Induct \\ simp [Once data_seqs_def,dataLangTheory.prog_size_def]
+  \\ rw [] \\ res_tac \\ gvs []
+QED
 
-val data_prog_to_display_def  = Define `
-  data_prog_to_display prog = case prog of
-    | dataLang$Skip => empty_item (strlit "Skip")
-    | dataLang$Move x y => Item NONE (strlit "Move")
-        [num_to_display x; num_to_display y]
-    | Call rets target args NONE => Item NONE (strlit "Call")
+Definition data_prog_to_display_def:
+  data_prog_to_display ns prog = case prog of
+    | dataLang$Skip => empty_item (strlit "skip")
+    | dataLang$Move x y => Tuple
+        [num_to_display x; String (strlit ":="); num_to_display y]
+    | Call rets target args NONE => Item NONE (strlit "call")
         [option_to_display (\(x, y). Tuple
                 [num_to_display x; num_set_to_display y]) rets;
-            option_to_display num_to_display target;
+            String (attach_name ns target);
             list_to_display num_to_display args;
-            empty_item (strlit "NONE")]
-     | Call rets target args (SOME (v, handler)) => Item NONE (strlit "Call")
+            empty_item (strlit "none")]
+     | Call rets target args (SOME (v, handler)) => Item NONE (strlit "call")
         [option_to_display (\(x, y). Tuple
                 [num_to_display x; num_set_to_display y]) rets;
-            option_to_display num_to_display target;
+            String (attach_name ns target);
+            list_to_display num_to_display args;
+            Item NONE (strlit "some") [Tuple [num_to_display v;
+                data_prog_to_display ns handler]]]
+    | Assign n op args n_set => Tuple
+        [num_to_display n;
+         String (strlit ":=");
+         clos_op_to_display ns op;
             list_to_display num_to_display args;
-            Item NONE (strlit "SOME") [Tuple [num_to_display v;
-                data_prog_to_display handler]]]
-    | Assign n op ns n_set => Item NONE (strlit "Assign")
-        [num_to_display n; clos_op_to_display op;
-            list_to_display num_to_display ns;
             option_to_display num_set_to_display n_set]
-    | Seq x y => Item NONE (strlit "Seq")
-        [data_prog_to_display x; data_prog_to_display y]
-    | If n x y => Item NONE (strlit "If")
-        [num_to_display n; data_prog_to_display x; data_prog_to_display y]
-    | MakeSpace n ns => Item NONE (strlit "MakeSpace")
+    | Seq x y =>
+        (let xs = append (Append (data_seqs x) (data_seqs y)) in
+           separate_lines (strlit "seq") (MAP (data_prog_to_display ns) xs))
+    | If n x y => Item NONE (strlit "if")
+        [num_to_display n; data_prog_to_display ns x; data_prog_to_display ns y]
+    | MakeSpace n ns => Item NONE (strlit "make_space")
         [num_to_display n; num_set_to_display ns]
-    | Raise n => Item NONE (strlit "Raise") [num_to_display n]
-    | Return n => Item NONE (strlit "Return") [num_to_display n]
-    | Tick => empty_item (strlit "Tick")`;
-
-val data_progs_to_display_def = Define`
-  data_progs_to_display (ps, names) = list_to_display
-    (\(n1, n2, prog). displayLang$Tuple [num_to_display n1;
-        String (getOpt (sptree$lookup n1 names) (strlit "_unmatched"));
-        num_to_display n2; data_prog_to_display prog]) ps`;
+    | Raise n => Item NONE (strlit "raise") [num_to_display n]
+    | Return n => Item NONE (strlit "return") [num_to_display n]
+    | Tick => empty_item (strlit "tick")
+Termination
+  WF_REL_TAC ‘measure $ prog_size o SND’
+  \\ fs [append_thm] \\ rw []
+  \\ imp_res_tac MEM_append_data_seqs \\ fs []
+End
+
+Definition data_fun_to_display_def:
+  data_fun_to_display names (n,argc,body) =
+    Tuple [String «func»;
+           String (attach_name names (SOME n));
+           Tuple (GENLIST num_to_display argc);
+           data_prog_to_display names body]
+End
 
 (* asm *)
 
-val asm_binop_to_display_def = Define `
+Definition asm_binop_to_display_def:
   asm_binop_to_display op = case op of
     | asm$Add => empty_item (strlit "Add")
     | Sub => empty_item (strlit "Sub")
     | And => empty_item (strlit "And")
     | Or => empty_item (strlit "Or")
-    | Xor => empty_item (strlit "Xor")`;
+    | Xor => empty_item (strlit "Xor")
+End
 
-val asm_reg_imm_to_display_def = Define `
+Definition asm_reg_imm_to_display_def:
   asm_reg_imm_to_display reg_imm = case reg_imm of
     | asm$Reg reg => item_with_num (strlit "Reg") reg
-    | Imm imm => item_with_num (strlit "Imm") (w2n imm)`;
+    | Imm imm => item_with_word (strlit "Imm") imm
+End
 
-val asm_arith_to_display_def = Define `
+Definition asm_arith_to_display_def:
   asm_arith_to_display op = case op of
     | asm$Binop bop n1 n2 reg_imm => Item NONE (strlit "Binop")
         [asm_binop_to_display bop; num_to_display n1; num_to_display n2;
@@ -544,20 +956,24 @@ val asm_arith_to_display_def = Define `
     | LongDiv n1 n2 n3 n4 n5 => item_with_nums (strlit "LongDiv") [n1; n2; n3; n4; n5]
     | AddCarry n1 n2 n3 n4 => item_with_nums (strlit "AddCarry") [n1; n2; n3; n4]
     | AddOverflow n1 n2 n3 n4 => item_with_nums (strlit "AddOverflow") [n1; n2; n3; n4]
-    | SubOverflow n1 n2 n3 n4 => item_with_nums (strlit "SubOverflow") [n1; n2; n3; n4]`;
+    | SubOverflow n1 n2 n3 n4 => item_with_nums (strlit "SubOverflow") [n1; n2; n3; n4]
+End
 
-val asm_addr_to_display_def = Define `
+Definition asm_addr_to_display_def:
   asm_addr_to_display addr = case addr of
-    | Addr reg w => item_with_nums (strlit "Addr") [reg; w2n w]`;
+    | Addr reg w => Item NONE (strlit "Addr")
+                         [num_to_display reg; word_to_display w]
+End
 
-val asm_memop_to_display_def = Define `
+Definition asm_memop_to_display_def:
   asm_memop_to_display op = case op of
     | Load => empty_item (strlit "Load")
     | Load8 => empty_item (strlit "Load8")
     | Store => empty_item (strlit "Store")
-    | Store8 => empty_item (strlit "Store8")`;
+    | Store8 => empty_item (strlit "Store8")
+End
 
-val asm_cmp_to_display_def = Define`
+Definition asm_cmp_to_display_def:
   asm_cmp_to_display op = case op of
     | Equal => empty_item «Equal»
     | Lower => empty_item «Lower»
@@ -566,9 +982,10 @@ val asm_cmp_to_display_def = Define`
     | NotEqual => empty_item «NotEqual»
     | NotLower => empty_item «NotLower»
     | NotLess => empty_item «NotLess»
-    | NotTest => empty_item «NotTest»`
+    | NotTest => empty_item «NotTest»
+End
 
-val asm_fp_to_display_def = Define `
+Definition asm_fp_to_display_def:
   asm_fp_to_display op = case op of
     | FPLess n1 n2 n3 => item_with_nums (strlit "FPLess") [n1; n2; n3]
     | FPLessEqual n1 n2 n3 => item_with_nums (strlit "FPLessEqual") [n1; n2; n3]
@@ -585,31 +1002,35 @@ val asm_fp_to_display_def = Define `
     | FPMovToReg n1 n2 n3 => item_with_nums (strlit "FPMovToReg") [n1; n2; n3]
     | FPMovFromReg n1 n2 n3 => item_with_nums (strlit "FPMovFromReg") [n1; n2; n3]
     | FPToInt n1 n2 => item_with_nums (strlit "FPToInt") [n1; n2]
-    | FPFromInt n1 n2 => item_with_nums (strlit "FPFromInt") [n1; n2]`;
+    | FPFromInt n1 n2 => item_with_nums (strlit "FPFromInt") [n1; n2]
+End
 
-val asm_inst_to_display_def = Define `
+Definition asm_inst_to_display_def:
   asm_inst_to_display inst = case inst of
     | asm$Skip => empty_item (strlit "Skip")
-    | Const reg w => item_with_nums (strlit "Const") [reg; w2n w]
+    | Const reg w => Item NONE (strlit "Const") [num_to_display reg;
+                                                 word_to_display w]
     | Arith a => Item NONE (strlit "Arith") [asm_arith_to_display a]
     | Mem mop r addr => Item NONE (strlit "Mem") [asm_memop_to_display mop;
         num_to_display r; asm_addr_to_display addr]
-    | FP fp => Item NONE (strlit "FP") [asm_fp_to_display fp]`;
+    | FP fp => Item NONE (strlit "FP") [asm_fp_to_display fp]
+End
 
-val asm_asm_to_display_def = Define `
+Definition asm_asm_to_display_def:
   asm_asm_to_display inst = case inst of
     | Inst i => asm_inst_to_display i
-    | Jump w => item_with_num «Jump» (w2n w)
+    | Jump w => item_with_word «Jump» w
     | JumpCmp c r to w => Item NONE «JumpCmp»
       [asm_cmp_to_display c; num_to_display r; asm_reg_imm_to_display to;
-       num_to_display (w2n w)]
-    | Call w => item_with_num «Call» (w2n w)
+       word_to_display w]
+    | Call w => item_with_word «Call» w
     | JumpReg r => item_with_num «JumpReg>» r
-    | Loc r w => item_with_nums «Loc» [r; w2n w]`
+    | Loc r w => Item NONE «Loc» [num_to_display r; word_to_display w]
+End
 
 (* stackLang *)
 
-val store_name_to_display_def = Define `
+Definition store_name_to_display_def:
   store_name_to_display st = case st of
     | NextFree => empty_item «NextFree»
     | EndOfHeap => empty_item «EndOfHeap»
@@ -628,115 +1049,186 @@ val store_name_to_display_def = Define `
     | CodeBufferEnd => empty_item «CodeBufferEnd»
     | BitmapBuffer => empty_item «BitmapBuffer»
     | BitmapBufferEnd => empty_item «BitmapBufferEnd»
-    | Temp n => item_with_num «Temp» (w2n n)`;
+    | Temp w => item_with_word «Temp» w
+End
+
+Definition stack_seqs_def:
+  stack_seqs z =
+    case z of
+    | stackLang$Seq x y => Append (stack_seqs x) (stack_seqs y)
+    | _ => List [z]
+End
+
+Triviality MEM_append_stack_seqs:
+  ∀x. MEM a (append (stack_seqs x)) ⇒ prog_size ARB a ≤ prog_size ARB x
+Proof
+  Induct \\ simp [Once stack_seqs_def,stackLangTheory.prog_size_def]
+  \\ rw [] \\ res_tac \\ gvs []
+QED
 
-val stack_prog_to_display_def = Define`
-  stack_prog_to_display prog = case prog of
-    | stackLang$Skip => empty_item «Skip»
-    | Inst i => asm_inst_to_display i
-    | Get n sn => Item NONE «Get» [num_to_display n;
-        store_name_to_display sn]
-    | Set sn n => Item NONE «Set» [store_name_to_display sn;
-        num_to_display n]
-    | OpCurrHeap b n1 n2 => Item NONE «OpCurrHeap»
-        [asm_binop_to_display b; num_to_display n1; num_to_display n2]
-    | Call rh tgt eh => Item NONE «Call»
-        [(case rh of
-            | NONE => empty_item «Tail»
-            | SOME (p,lr,l1,l2) => Item NONE «Return»
-              [num_to_display lr; num_to_display l1; num_to_display l2;
-               stack_prog_to_display p]);
+Definition stack_prog_to_display_def:
+  stack_prog_to_display ns stackLang$Skip = empty_item «skip» ∧
+  stack_prog_to_display ns (Inst i) = asm_inst_to_display i ∧
+  stack_prog_to_display ns (Get n sn) = Tuple
+    [num_to_display n; String (strlit "<-"); store_name_to_display sn] ∧
+  stack_prog_to_display ns (Set sn n) = Tuple
+    [store_name_to_display sn; String (strlit "<-"); num_to_display n] ∧
+  stack_prog_to_display ns (OpCurrHeap b n1 n2) = Tuple
+    [num_to_display n1; String (strlit ":="); String (strlit "CurrHeap");
+     asm_binop_to_display b; num_to_display n2] ∧
+  stack_prog_to_display ns (Call rh tgt eh) =
+    Item NONE «call»
+         [(case rh of
+           | NONE => empty_item «tail»
+           | SOME (p,lr,l1,l2) =>
+               Item NONE «returning»
+                    [num_to_display lr;
+                     String (attach_name ns (SOME l1));
+                     num_to_display l2;
+                     stack_prog_to_display ns p]);
          (case tgt of
-            | INL l => item_with_num «Direct» l
-            | INR r => item_with_num «Reg» r);
+          | INL l => Item NONE «direct» [String (attach_name ns (SOME l))]
+          | INR r => item_with_num «reg» r);
          (case eh of
-            | NONE => empty_item «NoHandle»
-            | SOME (p,l1,l2) => Item NONE «Handle»
-              [num_to_display l1; num_to_display l2; stack_prog_to_display p])]
-    | Seq x y => Item NONE «Seq»
-        [stack_prog_to_display x; stack_prog_to_display y]
-    | If c n to x y => Item NONE «If»
-        [asm_cmp_to_display c; num_to_display n;
-         asm_reg_imm_to_display to; stack_prog_to_display x;
-         stack_prog_to_display y]
-    | While c n to x => Item NONE «While»
-        [asm_cmp_to_display c; num_to_display n;
-         asm_reg_imm_to_display to; stack_prog_to_display x]
-    | JumpLower n1 n2 n3 => item_with_nums «JumpLower» [n1; n2; n3]
-    | Alloc n => item_with_num «Alloc» n
-    | StoreConsts n1 n2 _ => item_with_nums «StoreConsts» [n1; n2]
-    | Raise n => item_with_num «Raise» n
-    | Return n1 n2 => item_with_nums «Return» [n1; n2]
-    | FFI nm cp cl ap al ra => Item NONE «FFI»
-        (string_imp nm :: MAP num_to_display [cp; cl; ap; al; ra])
-    | Tick => empty_item «Tick»
-    | LocValue n1 n2 n3 => item_with_nums «LocValue» [n1; n2; n3]
-    | Install n1 n2 n3 n4 n5 => item_with_nums «Install»
-        [n1; n2; n3; n4; n5]
-    | CodeBufferWrite n1 n2 => item_with_nums «CodeBufferWrite»
-        [n1; n2]
-    | DataBufferWrite n1 n2 => item_with_nums «DataBufferWrite»
-        [n1; n2]
-    | RawCall n => item_with_num «RawCall» n
-    | StackAlloc n => item_with_num «StackAlloc» n
-    | StackFree n => item_with_num «StackFree» n
-    | StackStore n m => item_with_nums «StackStore» [n; m]
-    | StackStoreAny n m => item_with_nums «StackStoreAny» [n; m]
-    | StackLoad n m => item_with_nums «StackLoad» [n; m]
-    | StackLoadAny n m => item_with_nums «StackLoadAny» [n; m]
-    | StackGetSize n => item_with_num «RawCall» n
-    | StackSetSize n => item_with_num «RawCall» n
-    | BitmapLoad n m => item_with_nums «BitmapLoad» [n; m]
-    | Halt n => item_with_num «Halt» n`;
-
-val stack_progs_to_display_def = Define`
-  stack_progs_to_display (ps,names) = list_to_display
-    (\(n1, prog). displayLang$Tuple [num_to_display n1;
-        String (getOpt (sptree$lookup n1 names) «NOT FOUND»);
-        stack_prog_to_display prog]) ps`;
+          | NONE => empty_item «no_handler»
+          | SOME (p,l1,l2) =>
+              Item NONE «handler»
+                   [String (attach_name ns (SOME l1));
+                    num_to_display l2;
+                    stack_prog_to_display ns p])] ∧
+   stack_prog_to_display ns (Seq x y) =
+        (let xs = append (Append (stack_seqs x) (stack_seqs y)) in
+           separate_lines (strlit "seq") (MAP (stack_prog_to_display ns) xs)) ∧
+   stack_prog_to_display ns (If c n to x y) = Item NONE «if»
+        [Tuple [asm_cmp_to_display c; num_to_display n; asm_reg_imm_to_display to];
+         stack_prog_to_display ns x;
+         stack_prog_to_display ns y] ∧
+   stack_prog_to_display ns (While c n to x) = Item NONE «while»
+        [Tuple [asm_cmp_to_display c; num_to_display n; asm_reg_imm_to_display to];
+         stack_prog_to_display ns x] ∧
+   stack_prog_to_display ns (JumpLower n1 n2 n3) =
+     item_with_nums «jump_lower» [n1; n2; n3] ∧
+   stack_prog_to_display ns (Alloc n) = item_with_num «alloc» n ∧
+   stack_prog_to_display ns (StoreConsts n1 n2 _) = item_with_nums «store_consts» [n1; n2] ∧
+   stack_prog_to_display ns (Raise n) = item_with_num «raise» n ∧
+   stack_prog_to_display ns (Return n1 n2) = item_with_nums «return» [n1; n2] ∧
+   stack_prog_to_display ns (FFI nm cp cl ap al ra) = Item NONE «ffi»
+        (string_imp nm :: MAP num_to_display [cp; cl; ap; al; ra]) ∧
+   stack_prog_to_display ns (Tick) = empty_item «tick» ∧
+   stack_prog_to_display ns (LocValue n1 n2 n3) =
+     Item NONE «loc_value» [num_to_display n1;
+                            String (attach_name ns (SOME n2));
+                            num_to_display n3] ∧
+   stack_prog_to_display ns (Install n1 n2 n3 n4 n5) =
+     item_with_nums «install» [n1; n2; n3; n4; n5] ∧
+   stack_prog_to_display ns (CodeBufferWrite n1 n2) =
+     item_with_nums «code_buffer_write» [n1; n2] ∧
+   stack_prog_to_display ns (DataBufferWrite n1 n2) =
+     item_with_nums «data_buffer_write» [n1; n2] ∧
+   stack_prog_to_display ns (RawCall n) =
+     Item NONE «raw_call» [String (attach_name ns (SOME n))] ∧
+   stack_prog_to_display ns (StackAlloc n) = item_with_num «stack_alloc» n ∧
+   stack_prog_to_display ns (StackFree n) = item_with_num «stack_free» n ∧
+   stack_prog_to_display ns (StackStore n m) =
+     Tuple [String («stack[» ^ num_to_hex_mlstring n ^ «] := » ^ toString m)] ∧
+   stack_prog_to_display ns (StackStoreAny n m) =
+     Tuple [String («stack[var » ^ toString n ^ «] := » ^ toString m)] ∧
+   stack_prog_to_display ns (StackLoad n m) =
+     Tuple [String (concat [toString n;
+                            strlit " := stack[";
+                            num_to_hex_mlstring m; strlit"]"])] ∧
+   stack_prog_to_display ns (StackLoadAny n m) =
+     Tuple [String (concat [toString n;
+                            strlit " := stack[var ";
+                            toString m; strlit"]"])] ∧
+   stack_prog_to_display ns (StackGetSize n) = item_with_num «stack_get_size» n ∧
+   stack_prog_to_display ns (StackSetSize n) = item_with_num «stack_set_size» n ∧
+   stack_prog_to_display ns (BitmapLoad n m) =
+     Tuple [String (concat [toString n;
+                            strlit " := bitmap[";
+                            num_to_hex_mlstring m;
+                            strlit"]"])] ∧
+   stack_prog_to_display ns (Halt n) = item_with_num «halt» n
+Termination
+  WF_REL_TAC ‘measure $ prog_size ARB o SND’
+  \\ gvs [append_thm] \\ rw []
+  \\ imp_res_tac MEM_append_stack_seqs \\ fs []
+End
+
+Definition stack_fun_to_display_def:
+  stack_fun_to_display names (n,body) =
+    Tuple [String «func»;
+           String (attach_name names (SOME n));
+           stack_prog_to_display names body]
+End
 
 (* labLang *)
 
-val lab_asm_to_display_def = Define`
-  lab_asm_to_display la = case la of
-    | labLang$Jump (Lab s n) => item_with_nums «Jump» [s; n]
-    | JumpCmp c r ri (Lab s n) => Item NONE «JumpCmp»
-      [asm_cmp_to_display c; num_to_display r;
-       asm_reg_imm_to_display ri; num_to_display s; num_to_display n]
-    | Call (Lab s n) => item_with_nums «Call» [s; n]
-    | LocValue r (Lab s n) => item_with_nums «LocValue» [r; s; n]
-    | CallFFI name => Item NONE «CallFFI» [string_imp name]
-    | Install => empty_item «Install»
-    | Halt => empty_item «Halt»`
-
-val lab_line_to_display_def = Define`
-  lab_line_to_display line = case line of
-    | Label se nu le => item_with_nums «Label» [se; nu; le]
+Definition lab_asm_to_display_def:
+  lab_asm_to_display ns la = case la of
+    | labLang$Jump (Lab s n) =>
+        Item NONE «jump»
+          [String (attach_name ns (SOME s)); num_to_display n]
+    | JumpCmp c r ri (Lab s n) =>
+        Item NONE «jump_cmp»
+          [Tuple [asm_cmp_to_display c; num_to_display r;
+                  asm_reg_imm_to_display ri];
+           String (attach_name ns (SOME s)); num_to_display n]
+    | Call (Lab s n) =>
+        Item NONE «call»
+          [String (attach_name ns (SOME s)); num_to_display n]
+    | LocValue r (Lab s n) =>
+        Item NONE «loc_value»
+          [num_to_display r; String (attach_name ns (SOME s)); num_to_display n]
+    | CallFFI name => Item NONE «call_FFI» [string_imp name]
+    | Install => empty_item «install»
+    | Halt => empty_item «halt»
+End
+
+Definition lab_line_to_display_def:
+  lab_line_to_display ns line = case line of
+    | Label s n le =>
+        Item NONE «label» [String (attach_name ns (SOME s)); num_to_display n]
     | Asm aoc enc len => (case aoc of
-      | Asmi i => Item NONE «Asm» [asm_asm_to_display i]
-      | Cbw r1 r2 => item_with_nums «Cbw» [r1; r2])
-    | LabAsm la pos enc len => lab_asm_to_display la`
+      | Asmi i => Item NONE «asm» [asm_asm_to_display i]
+      | Cbw r1 r2 => item_with_nums «cbw» [r1; r2])
+    | LabAsm la pos enc len => lab_asm_to_display ns la
+End
 
-val lab_secs_to_display_def = Define`
-  lab_secs_to_display (ss,names) = list_to_display (\sec.
-    case sec of Section n lines => displayLang$Tuple [num_to_display n;
-        String (getOpt (sptree$lookup n names) «NOT FOUND»);
-        list_to_display lab_line_to_display lines]) ss`
+Definition lab_fun_to_display_def:
+  lab_fun_to_display names (Section n lines) =
+    List (String (attach_name names (SOME n))
+           :: MAP (lab_line_to_display names) lines)
+End
 
 (* wordLang *)
 
-val MEM_word_exps_size_ARB =
-    wordLangTheory.MEM_IMP_exp_size |> Q.GEN `l` |> Q.SPEC `ARB`;
+Definition word_seqs_def:
+  word_seqs z =
+    case z of
+    | wordLang$Seq x y => Append (word_seqs x) (word_seqs y)
+    | _ => List [z]
+End
+
+Triviality MEM_append_word_seqs:
+  ∀x. MEM a (append (word_seqs x)) ⇒ prog_size ARB a ≤ prog_size ARB x
+Proof
+  Induct \\ simp [Once word_seqs_def,wordLangTheory.prog_size_def]
+  \\ rw [] \\ res_tac \\ gvs []
+QED
 
-val word_exp_to_display_def = tDefine "word_exp_to_display" `
+Triviality MEM_word_exps_size_ARB =
+  wordLangTheory.MEM_IMP_exp_size |> Q.GEN `l` |> Q.SPEC `ARB`;
+
+Definition word_exp_to_display_def:
   (word_exp_to_display (wordLang$Const v)
-    = item_with_num (strlit "Const") (w2n v)) /\
+    = item_with_word (strlit "Const") v) /\
   (word_exp_to_display (Var n)
     = item_with_num (strlit "Var") n) /\
   (word_exp_to_display (Lookup st)
     = Item NONE (strlit "Lookup") [store_name_to_display st]) /\
   (word_exp_to_display (Load exp2)
-    = Item NONE (strlit "Load") [word_exp_to_display exp2]) /\
+    = Item NONE (strlit "MemLoad") [word_exp_to_display exp2]) /\
   (word_exp_to_display (Op bop exs)
     = Item NONE (strlit "Op") (asm_binop_to_display bop
         :: MAP word_exp_to_display exs)) /\
@@ -745,152 +1237,246 @@ val word_exp_to_display_def = tDefine "word_exp_to_display" `
       shift_to_display sh;
       word_exp_to_display exp;
       num_to_display num
-    ])`
- (WF_REL_TAC `measure (wordLang$exp_size ARB)`
+    ])
+Termination
+  WF_REL_TAC `measure (wordLang$exp_size ARB)`
   \\ rw []
   \\ imp_res_tac MEM_word_exps_size_ARB
   \\ rw []
- );
-
-val word_prog_to_display_def = tDefine "word_prog_to_display" `
-  (word_prog_to_display Skip = empty_item (strlit "Skip")) /\
-  (word_prog_to_display (Move n mvs) = Item NONE (strlit "Move")
-    [num_to_display n; displayLang$List (MAP (\(n1, n2). Tuple
-        [num_to_display n1; num_to_display n2]) mvs)]) /\
-  (word_prog_to_display (Inst i) = empty_item (strlit "Inst")) /\
-  (word_prog_to_display (Assign n exp) = Item NONE (strlit "Assign")
-    [num_to_display n; word_exp_to_display exp]) /\
-  (word_prog_to_display (Get n sn) = Item NONE (strlit "Get")
-    [num_to_display n; store_name_to_display sn]) /\
-  (word_prog_to_display (Set sn exp) = Item NONE (strlit "Set")
-    [store_name_to_display sn; word_exp_to_display exp]) /\
-  (word_prog_to_display (Store exp n) = Item NONE (strlit "Store")
-    [word_exp_to_display exp; num_to_display n]) /\
-  (word_prog_to_display (MustTerminate prog) = Item NONE (strlit "MustTerminate")
-    [word_prog_to_display prog]) /\
-  (word_prog_to_display (Call a b c d) = Item NONE (strlit "Call")
-    [word_prog_to_display_ret a; option_to_display num_to_display b;
-        list_to_display num_to_display c;
-        word_prog_to_display_handler d]) /\
-  (word_prog_to_display (OpCurrHeap b n1 n2) = Item NONE «OpCurrHeap»
-    [asm_binop_to_display b; num_to_display n1; num_to_display n2]) /\
-  (word_prog_to_display (Seq prog1 prog2) = Item NONE (strlit "Seq")
-    [word_prog_to_display prog1; word_prog_to_display prog2]) /\
-  (word_prog_to_display (If cmp n reg p1 p2) = Item NONE (strlit "If")
-    [word_prog_to_display p1; word_prog_to_display p2]) /\
-  (word_prog_to_display (Alloc n ns) = Item NONE (strlit "Alloc")
-    [num_to_display n; num_set_to_display ns]) /\
-  (word_prog_to_display (StoreConsts a b c d ws) = Item NONE (strlit "StoreConsts")
-    [num_to_display a; num_to_display b; num_to_display c; num_to_display d] (* TODO: include ws *)) /\
-  (word_prog_to_display (Raise n) = item_with_num (strlit "Raise") n) /\
-  (word_prog_to_display (Return n1 n2) = item_with_nums (strlit "Return") [n1; n2]) /\
-  (word_prog_to_display Tick = empty_item (strlit "Tick")) /\
-  (word_prog_to_display (LocValue n1 n2) =
-    item_with_nums (strlit "LocValue") [n1; n2]) /\
-  (word_prog_to_display (Install n1 n2 n3 n4 ns) =
-    Item NONE (strlit "Install") (MAP num_to_display [n1; n2; n3; n4]
-        ++ [num_set_to_display ns])) /\
-  (word_prog_to_display (CodeBufferWrite n1 n2) =
-    item_with_nums (strlit "CodeBufferWrite") [n1; n2]) /\
-  (word_prog_to_display (DataBufferWrite n1 n2) =
-    item_with_nums (strlit "DataBufferWrite") [n1; n2]) /\
-  (word_prog_to_display (FFI nm n1 n2 n3 n4 ns) =
-    Item NONE (strlit "FFI") (string_imp nm :: MAP num_to_display [n1; n2; n3; n4]
-        ++ [num_set_to_display ns])) /\
-  (word_prog_to_display_ret NONE = empty_item (strlit "NONE")) /\
-  (word_prog_to_display_ret (SOME (n1, ns, prog, n2, n3)) =
-    Item NONE (strlit "SOME") [Tuple [num_to_display n1; num_set_to_display ns;
-        word_prog_to_display prog; num_to_display n2; num_to_display n3]]) /\
-  (word_prog_to_display_handler NONE = empty_item (strlit "NONE")) /\
-  (word_prog_to_display_handler (SOME (n1, prog, n2, n3)) =
-    Item NONE (strlit "SOME") [Tuple [num_to_display n1;
-        word_prog_to_display prog; num_to_display n2; num_to_display n3]])
-`
-  (WF_REL_TAC `measure (\x. case x of
-        | INL p => wordLang$prog_size ARB p
-        | INR (INL v) => wordLang$prog1_size ARB v
-        | INR (INR v) => wordLang$prog3_size ARB v)`
-    \\ rw []
-  )
-;
-
-val word_progs_to_display_def = Define`
-  word_progs_to_display (ps,names) = list_to_display
-    (\(n1, n2, prog). displayLang$Tuple [num_to_display n1;
-        String (getOpt (sptree$lookup n1 names) (strlit "NOT FOUND"));
-        num_to_display n2; word_prog_to_display prog]) ps`;
-
-(* Function to construct general functions from a language to JSON. Call with
-* the name of the language and what function to use to convert it to
-* displayLang to obtain a wrapper function which exports JSON. *)
-val lang_to_json_def = Define`
-  lang_to_json langN func =
-    \ p . Object [
-      (strlit "lang", String langN);
-      (strlit "prog", display_to_json (func p))]`;
-
-(* tap configuration. which bits of compilation should we save?
-   top-level code for assembling the tapped data. *)
-
-val () = Datatype `
-  tap_config = Tap_Config
-    (* save filename prefix *) mlstring
-    (* bits which should be saved. the boolean indicates
-       the presence of a '*' suffix, and matches all suffixes *)
-    ((mlstring # bool) list)`;
-
-val mk_tap_star = Define `
-  mk_tap_star str = if isSuffix (strlit "*") str
-    then (substring str 0 (strlen str - 1), T)
-    else (str, F)`;
-
-val mk_tap_config = Define `
-  mk_tap_config fname taps = Tap_Config (case fname of
-    | NONE => (strlit "default.tap") | SOME s => s) (MAP mk_tap_star taps)`;
-
-val default_tap_config = Define `
-  default_tap_config = mk_tap_config NONE []`;
-
-val should_tap_def = Define `
-  should_tap (conf : tap_config) nm = case conf of
-    | Tap_Config _ taps => EXISTS (\(s, star). if star then
-        isPrefix s nm else s = nm) taps`;
-
-val tap_name_def = Define `
-  tap_name (conf : tap_config) nm = case conf of
-    | Tap_Config fname _ => concat [fname; strlit "."; nm]`;
-
-val () = Datatype `
-  tap_data = Tap_Data mlstring (unit -> jsonLang$obj)`;
-
-val add_tap_def = Define `
-  add_tap conf nm (to_display : 'a -> displayLang$sExp) (v : 'a) tds
-    = if should_tap conf nm
-    then Tap_Data (tap_name conf nm)
-            (\_. lang_to_json nm to_display v) :: tds
-    else tds`;
-
-val tap_data_mlstrings_def = Define `
-  tap_data_mlstrings td = case td of
-    | Tap_Data nm json_f => (nm, json_to_mlstring (json_f ()))`;
-
-val tap_flat_def = Define `
-  tap_flat conf v = add_tap conf (strlit "flat") flat_to_display_decs v`;
-
-val tap_clos_def = Define`
-  tap_clos conf v = add_tap conf (strlit "clos")
-    (list_to_display (clos_to_display 0)) v`;
-
-val tap_data_lang_def = Define `
-  tap_data_lang conf v = add_tap conf (strlit "data") data_progs_to_display v`;
-
-val tap_word_def = Define `
-  tap_word conf v = add_tap conf (strlit "word") word_progs_to_display v`;
-
-val tap_stack_def = Define `
-  tap_stack conf v = add_tap conf (strlit "stack") stack_progs_to_display v`;
-
-val tap_lab_def = Define `
-  tap_lab conf v = add_tap conf (strlit "lab") lab_secs_to_display v`;
+End
+
+Definition ws_to_display_def:
+  ws_to_display [] = [] ∧
+  ws_to_display ((b,x)::xs) =
+    Tuple [bool_to_display b; word_to_display x] :: ws_to_display xs
+End
+
+Definition word_prog_to_display_def:
+  (word_prog_to_display ns Skip = empty_item (strlit "skip")) /\
+  (word_prog_to_display ns (Move n mvs) = Item NONE (strlit "move")
+    [num_to_display n; displayLang$Tuple (MAP (\(n1, n2). Tuple
+        [num_to_display n1;
+         String (strlit ":=");
+         num_to_display n2]) mvs)]) /\
+  (word_prog_to_display ns (Inst i) =
+    Item NONE (strlit "inst") [asm_inst_to_display i]) /\
+  (word_prog_to_display ns (Assign n exp) =
+     Tuple [num_to_display n;
+            String (strlit ":=");
+            word_exp_to_display exp]) /\
+  (word_prog_to_display ns (Get n sn) = Tuple
+    [num_to_display n; String (strlit "<-"); store_name_to_display sn]) /\
+  (word_prog_to_display ns (Set sn exp) = Tuple
+    [store_name_to_display sn; String (strlit "<-"); word_exp_to_display exp]) /\
+  (word_prog_to_display ns (Store exp n) = Tuple
+    [String (strlit "mem"); word_exp_to_display exp;
+     String (strlit ":="); num_to_display n]) /\
+  (word_prog_to_display ns (MustTerminate prog) = Item NONE (strlit "must_terminate")
+    [word_prog_to_display ns prog]) /\
+  (word_prog_to_display ns (Call a b c d) = Item NONE (strlit "call")
+    [word_prog_to_display_ret ns a;
+     option_to_display (λn. String (attach_name ns (SOME n))) b;
+     list_to_display num_to_display c;
+     word_prog_to_display_handler ns d]) /\
+  (word_prog_to_display ns (OpCurrHeap b n1 n2) = Tuple
+    [num_to_display n1; String (strlit ":="); String (strlit "CurrHeap");
+     asm_binop_to_display b; num_to_display n2]) /\
+  (word_prog_to_display ns (Seq prog1 prog2) =
+    (let xs = append (Append (word_seqs prog1) (word_seqs prog2)) in
+       separate_lines (strlit "seq") (MAP (word_prog_to_display ns) xs))) /\
+  (word_prog_to_display ns (If cmp n reg p1 p2) =
+    Item NONE (strlit "if")
+      [Tuple [asm_cmp_to_display cmp;
+              num_to_display n;
+              asm_reg_imm_to_display reg];
+       word_prog_to_display ns p1; word_prog_to_display ns p2]) /\
+  (word_prog_to_display ns (Alloc n ms) = Item NONE (strlit "alloc")
+    [num_to_display n; num_set_to_display ms]) /\
+  (word_prog_to_display ns (StoreConsts a b c d ws) = Item NONE (strlit "store_consts")
+    [num_to_display a;
+     num_to_display b;
+     num_to_display c;
+     num_to_display d;
+     Tuple (ws_to_display ws)]) /\
+  (word_prog_to_display ns (Raise n) = item_with_num (strlit "raise") n) /\
+  (word_prog_to_display ns (Return n1 n2) = item_with_nums (strlit "return") [n1; n2]) /\
+  (word_prog_to_display ns Tick = empty_item (strlit "tick")) /\
+  (word_prog_to_display ns (LocValue n1 n2) =
+    Item NONE (strlit "loc_value") [String (attach_name ns (SOME n1)); num_to_display n2]) /\
+  (word_prog_to_display ns (Install n1 n2 n3 n4 ms) =
+    Item NONE (strlit "install") (MAP num_to_display [n1; n2; n3; n4]
+        ++ [num_set_to_display ms])) /\
+  (word_prog_to_display ns (CodeBufferWrite n1 n2) =
+    item_with_nums (strlit "code_buffer_write") [n1; n2]) /\
+  (word_prog_to_display ns (DataBufferWrite n1 n2) =
+    item_with_nums (strlit "data_buffer_write") [n1; n2]) /\
+  (word_prog_to_display ns (FFI nm n1 n2 n3 n4 ms) =
+    Item NONE (strlit "ffi") (string_imp nm :: MAP num_to_display [n1; n2; n3; n4]
+        ++ [num_set_to_display ms])) /\
+  (word_prog_to_display_ret ns NONE = empty_item (strlit "tail")) /\
+  (word_prog_to_display_ret ns (SOME (n1, ms, prog, n2, n3)) =
+    Item NONE (strlit "returning") [Tuple [num_to_display n1; num_set_to_display ms;
+        word_prog_to_display ns prog;
+        String (attach_name ns (SOME n2));
+        num_to_display n3]]) /\
+  (word_prog_to_display_handler ns NONE = empty_item (strlit "no_handler")) /\
+  (word_prog_to_display_handler ns (SOME (n1, prog, n2, n3)) =
+    Item NONE (strlit "handler") [Tuple [num_to_display n1;
+        word_prog_to_display ns prog;
+        String (attach_name ns (SOME n2));
+        num_to_display n3]])
+Termination
+  WF_REL_TAC `measure (\x. case x of
+        | INL (_,p) => wordLang$prog_size ARB p
+        | INR (INL (_,v)) => wordLang$prog1_size ARB v
+        | INR (INR (_,v)) => wordLang$prog3_size ARB v)`
+  \\ rw [] \\ imp_res_tac MEM_append_word_seqs \\ rw []
+End
+
+Definition word_fun_to_display_def:
+  word_fun_to_display names (n,argc,body) =
+    Tuple [String «func»;
+           String (attach_name names (SOME n));
+           Tuple (GENLIST num_to_display argc);
+           word_prog_to_display names body]
+End
+
+(* tap configuration *)
+
+Datatype:
+  tap_config = <| explore_flag : bool |>
+End
+
+Definition default_tap_config_def:
+  default_tap_config = <| explore_flag := F |>
+End
+
+(* ------------------------- *)
+
+Definition map_to_append_def:
+  map_to_append f [] = Nil ∧
+  map_to_append f (x::xs) = Append (List (f x)) (map_to_append f xs)
+End
+
+Definition source_to_strs_def:
+  source_to_strs decs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   source_to_display_dec) decs
+End
+
+Definition flat_to_strs_def:
+  flat_to_strs (decs:flatLang$dec list) =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   flat_to_display_dec) decs
+End
+
+Definition clos_to_strs_def:
+  clos_to_strs (decs,funs) =
+    let names = clos_to_bvl$get_src_names (decs ++ MAP (SND o SND) funs) LN in
+      Append (map_to_append (v2strs (strlit "\n\n") o
+                             display_to_str_tree o
+                             clos_dec_to_display names) decs)
+             (map_to_append (v2strs (strlit "\n\n") o
+                             display_to_str_tree o
+                             clos_fun_to_display names) funs)
+End
+
+Definition bvl_to_strs_def:
+  bvl_to_strs names xs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   bvl_fun_to_display names) xs
+End
+
+val bvl_test =
+  “concat $ append $ bvl_to_strs
+     (insert 50 (strlit "foo") (insert 60 (strlit "bar") LN))
+     [(50,2,Let [Var 0; Var 1]
+              $ Op Add [Var 0; Var 1; Var 2; Var 3]);
+      (60,2,Let [Var 0; Var 1]
+              $ Call 0 (SOME 50) [Var 2; Var 0])]”
+  |> EVAL |> concl |> rand |> rand |> stringSyntax.fromHOLstring
+  |> (fn t => (print "\n\n"; print t; print "\n"))
+
+Definition bvi_to_strs_def:
+  bvi_to_strs names xs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   bvi_fun_to_display names) xs
+End
+
+val bvi_test =
+  “concat $ append $ bvi_to_strs
+     (insert 50 (strlit "foo") (insert 60 (strlit "bar") LN))
+     [(50,2,Let [Var 0]
+              $ Op Add [Var 0; Var 1; Var 2; Var 3]);
+      (60,2,Let [Var 0; Var 1]
+              $ Call 0 (SOME 50) [Var 2; Var 0] (SOME (Var 0)))]”
+  |> EVAL |> concl |> rand |> rand |> stringSyntax.fromHOLstring
+  |> (fn t => (print "\n\n"; print t; print "\n"))
+
+Definition data_to_strs_def:
+  data_to_strs names xs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   data_fun_to_display names) xs
+End
+
+val data_test =
+  “concat $ append $ data_to_strs
+     (insert 50 (strlit "foo") (insert 60 (strlit "bar") LN))
+     [(50,2,Seq (Move 5 1) $
+            Seq (Assign 3 Add [0;1] NONE) $
+            Seq (Assign 6 Sub [5;3] NONE) $ Return 6);
+      (60,2,Skip)]”
+  |> EVAL |> concl |> rand |> rand |> stringSyntax.fromHOLstring
+  |> (fn t => (print "\n\n"; print t; print "\n"))
+
+Definition word_to_strs_def:
+  word_to_strs names xs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   word_fun_to_display names) xs
+End
+
+Definition stack_to_strs_def:
+  stack_to_strs names xs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   stack_fun_to_display names) xs
+End
+
+Definition lab_to_strs_def:
+  lab_to_strs names xs =
+    map_to_append (v2strs (strlit "\n\n") o
+                   display_to_str_tree o
+                   lab_fun_to_display names) xs
+End
+
+val lab_test =
+  “concat $ append $ lab_to_strs
+     (insert 50 (strlit "foo") (insert 60 (strlit "bar") LN))
+     [Section 50 [Label 50 1 0;
+                  Asm (Asmi (Inst (Const 5 (70w:word32)))) [] 0;
+                  Label 50 2 0];
+      Section 60 [Label 50 5 0]]”
+  |> EVAL |> concl |> rand |> rand |> stringSyntax.fromHOLstring
+  |> (fn t => (print "\n\n"; print t; print "\n"))
+
+(*
+
+val names_tm = “(insert 50 (strlit "foo") (insert 60 (strlit "bar") LN))”
+
+val data_prog_tm =
+    “[(50,2,Seq (Move 5 1) $
+            Seq (Assign 3 Add [0;1] NONE) $
+            Seq (Assign 6 Sub [5;3] NONE) $ Return 6);
+      (60n,2n,Skip)]”
+
+val _ = data_to_strs data_prog_tm names_tm |> print_strs
+
+*)
 
 val _ = export_theory();
diff --git a/compiler/backend/proofs/backendProofScript.sml b/compiler/backend/proofs/backendProofScript.sml
index 417ff48a4b..53a85050b8 100644
--- a/compiler/backend/proofs/backendProofScript.sml
+++ b/compiler/backend/proofs/backendProofScript.sml
@@ -56,6 +56,8 @@ QED
 
 (* -- *)
 
+val compile_tap_def = backend_passesTheory.compile_tap_def;
+
 Theorem backend_upper_w2w[simp]:
   backend$upper_w2w = data_to_word_gcProof$upper_w2w
 Proof
@@ -419,7 +421,7 @@ Proof
   \\ TRY (gen_tac \\ pop_assum kall_tac)
   \\ rpt gen_tac
   \\ fs [compile_inc_progs_def, backendTheory.compile_def,
-            backendTheory.compile_tap_def, clos_to_bvlTheory.compile_def,
+            compile_tap_def, clos_to_bvlTheory.compile_def,
             clos_to_bvlTheory.compile_common_def,
             clos_to_bvlTheory.clos_to_bvl_compile_inc_def, lab_to_targetTheory.compile_def,
             bvl_to_bviTheory.bvl_to_bvi_compile_inc_all_def ]
@@ -1699,7 +1701,7 @@ Proof
   \\ conj_tac >- (
     fs []
     \\ drule_then drule to_lab_labels_ok
-    \\ fs [backendTheory.compile_def, backendTheory.compile_tap_def]
+    \\ fs [backendTheory.compile_def, compile_tap_def]
     \\ rpt (pairarg_tac \\ fs [])
     \\ drule_then strip_assume_tac attach_bitmaps_SOME
     \\ simp [to_stack_def, to_word_def, to_data_def, to_bvi_def, to_bvl_def,
@@ -1874,7 +1876,7 @@ Proof
     )
     \\ rw []
     \\ TRY (qpat_x_assum `_ < SUC _` mp_tac \\ EVAL_TAC \\ simp [])
-    \\ fs [backendTheory.compile_def, backendTheory.compile_tap_def,
+    \\ fs [backendTheory.compile_def, compile_tap_def,
           to_bvi_def, to_bvl_def, to_clos_def, to_flat_def,
           bvl_to_bviTheory.compile_def]
     \\ rpt (pairarg_tac \\ fs [])
@@ -1920,7 +1922,7 @@ Proof
     )
     \\ simp [FST_state_co, pred_setTheory.IN_PREIMAGE, cake_orac_0,
             config_tuple2_def]
-    \\ fs [backendTheory.compile_def, backendTheory.compile_tap_def,
+    \\ fs [backendTheory.compile_def, compile_tap_def,
           to_bvi_def, to_bvl_def, to_clos_def, to_flat_def,
           bvl_to_bviTheory.compile_def]
     \\ rpt (pairarg_tac \\ fs [])
diff --git a/compiler/backend/str_treeScript.sml b/compiler/backend/str_treeScript.sml
new file mode 100644
index 0000000000..a5e387accb
--- /dev/null
+++ b/compiler/backend/str_treeScript.sml
@@ -0,0 +1,161 @@
+(*
+  A Lisp inspired tree of mlstrings and a pretty printing function
+*)
+open HolKernel Parse boolLib bossLib;
+open arithmeticTheory listTheory pairTheory mlstringTheory;
+
+val _ = new_theory "str_tree";
+
+(* datatype and helper functions *)
+
+Datatype:
+  str_tree = Str mlstring | Pair str_tree str_tree | GrabLine str_tree
+End
+
+Definition isPair_def[simp]:
+  isPair (Pair _ _) = T ∧
+  isPair _ = F
+End
+
+Definition mk_list_def:
+  mk_list [] = Str (strlit "") ∧
+  mk_list (x::xs) = Pair x (mk_list xs)
+End
+
+(* pretty printing *)
+
+Definition dest_list_def:
+  dest_list (Pair x y) = (let (l,e) = dest_list y in (x::l,e)) ∧
+  dest_list other = ([],other)
+End
+
+Triviality dest_list_size:
+  ∀v e l.
+    (l,e) = dest_list v ⇒
+    str_tree_size e ≤ str_tree_size v ∧
+    (isPair v ⇒ str_tree_size e < str_tree_size v) ∧
+    ∀x. MEM x l ⇒ str_tree_size x < str_tree_size v
+Proof
+  Induct_on ‘v’ \\ fs [dest_list_def]
+  \\ pairarg_tac \\ fs [] \\ rw [] \\ res_tac \\ fs [fetch "-" "str_tree_size_def"]
+QED
+
+Datatype:
+  pretty = Parenthesis pretty
+         | String mlstring
+         | Append pretty bool pretty
+         | Size num pretty
+End
+
+Definition newlines_def:
+  newlines [] = String (strlit "") ∧
+  newlines [x] = x ∧
+  newlines (x::xs) = Append x T (newlines xs)
+End
+
+Definition v2pretty_def:
+  v2pretty v =
+    case v of
+    | Str s => String s
+    | GrabLine w => Size 100000 (v2pretty w)
+    | _ =>
+      let (l,e) = dest_list v in
+        Parenthesis
+          (if e = Str (strlit "") then
+            newlines (MAP v2pretty l)
+           else
+             Append (newlines (MAP v2pretty l)) T
+               (Append (String (strlit " . ")) T (v2pretty e)))
+Termination
+  WF_REL_TAC ‘measure str_tree_size’ \\ rw []
+  \\ imp_res_tac dest_list_size \\ fs [fetch "-" "str_tree_size_def"]
+End
+
+Definition get_size_def:
+  get_size (Size n x) = n ∧
+  get_size (Append x _ y) = get_size x + get_size y + 1 ∧
+  get_size (Parenthesis x) = get_size x + 2 ∧
+  get_size _ = 0
+End
+
+Definition get_next_size_def:
+  get_next_size (Size n x) = n ∧
+  get_next_size (Append x _ y) = get_next_size x ∧
+  get_next_size (Parenthesis x) = get_next_size x + 2 ∧
+  get_next_size _ = 0
+End
+
+Definition annotate_def:
+  annotate (String s) = Size (strlen s) (String s) ∧
+  annotate (Parenthesis b) =
+    (let b = annotate b in
+       Size (get_size b + 2) (Parenthesis b)) ∧
+  annotate (Append b1 n b2) =
+    (let b1 = annotate b1 in
+     let b2 = annotate b2 in
+       (* Size (get_size b1 + get_size b2 + 1) *) (Append b1 n b2)) ∧
+  annotate (Size n b) = Size n (annotate b)
+End
+
+Definition remove_all_def:
+  remove_all (Parenthesis v) = Parenthesis (remove_all v) ∧
+  remove_all (String v1) = String v1 ∧
+  remove_all (Append v2 _ v3) = Append (remove_all v2) F (remove_all v3) ∧
+  remove_all (Size v4 v5) = remove_all v5
+End
+
+Definition smart_remove_def:
+  smart_remove i k (Size n b) =
+    (if k + n < 70 then remove_all b else smart_remove i k b) ∧
+  smart_remove i k (Parenthesis v) = Parenthesis (smart_remove (i+1) (k+1) v) ∧
+  smart_remove i k (String v1) = String v1 ∧
+  smart_remove i k (Append v2 b v3) =
+    let n2 = get_size v2 in
+    let n3 = get_next_size v3 in
+      if k + n2 + n3 < 50 then
+        Append (smart_remove i k v2) F (smart_remove i (k+n2) v3)
+      else
+        Append (smart_remove i k v2) T (smart_remove i i v3)
+End
+
+Definition flatten_def:
+  flatten indent (Size n p) s = flatten indent p s ∧
+  flatten indent (Parenthesis p) s =
+    strlit "(" :: flatten (concat [indent; strlit "   "]) p (strlit ")" :: s) ∧
+  flatten indent (String t) s = t :: s ∧
+  flatten indent (Append p1 b p2) s =
+    flatten indent p1 ((if b then indent else strlit " ") :: flatten indent p2 s)
+End
+
+Definition v2strs_def:
+  v2strs end v = flatten (strlit "\n") (smart_remove 0 0 (annotate (v2pretty v))) [end]
+End
+
+Triviality test1:
+  concat (v2strs (strlit "")
+                 (Pair (Str (strlit "hello"))
+                       (Pair (Str (strlit "there")) (Str (strlit ""))))) =
+  strlit "(hello there)"
+Proof
+  EVAL_TAC
+QED
+
+Triviality test2:
+  concat (v2strs (strlit "")
+                 (mk_list (Str (strlit "test") ::
+                  MAP GrabLine [Str (strlit "hi"); Str (strlit "there")]))) =
+  strlit "(test\n   hi\n   there)"
+Proof
+  EVAL_TAC
+QED
+
+(*
+Definition vs2str_def:
+  vs2str [] coms = "\n" ∧
+  vs2str (x::xs) coms =
+    ((case coms of [] => [] | (c::cs) => if is_comment c then c else []) ++
+    ("\n" ++ (v2str x ++ ("\n" ++ vs2str xs (case coms of [] => [] | c::cs => cs)))))
+End
+*)
+
+val _ = export_theory();
diff --git a/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml b/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml
index a630675701..9c4bef5bde 100644
--- a/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml
+++ b/compiler/bootstrap/compilation/x64/64/x64_config_encScript.sml
@@ -5,6 +5,13 @@ open preamble backend_enc_decTheory x64BootstrapTheory;
 
 val _ = new_theory "x64_config_enc";
 
+Theorem tap_config_enc'_comp[compute]:
+  tap_config_enc' c = Tree 0 [bool_enc' (c.explore_flag)]
+Proof
+  Cases_on ‘c’
+  \\ fs [backend_enc_decTheory.tap_config_enc'_def]
+QED
+
 val confs = LIST_CONJ
   [to_dataBootstrapTheory.flat_conf_def,
    to_dataBootstrapTheory.bvl_conf_def,
@@ -25,6 +32,7 @@ Theorem encode_backend_config_cake_config =
 
 val _ = let
   val filename = "config_enc_str.txt"
+(* config_enc_str_def |> concl |> rand |> repeat (snd o stringSyntax.dest_string) *)
   val str = config_enc_str_def |> concl |> rand |> stringSyntax.fromHOLstring
   val n = size str
   fun nice_size_str n =
diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml
index a4572fd76e..12687f3ef1 100644
--- a/compiler/bootstrap/translation/compiler32ProgScript.sml
+++ b/compiler/bootstrap/translation/compiler32ProgScript.sml
@@ -39,26 +39,7 @@ Proof
   rw[FUN_EQ_THM] \\ EVAL_TAC
 QED
 
-(*
-
-val def = spec32 backendTheory.compile_explorer_def
-
-val res = translate def
-
-val backend_compile_explorer_side = Q.prove(`
-  ∀x y. backend_compile_explorer_side x y = T`,
-  simp[definition"backend_compile_explorer_side_def",PULL_FORALL] \\
-  rpt gen_tac \\ ntac 3 strip_tac \\
-  qmatch_goalsub_abbrev_tac`compile c.do_mti c.max_app [z]` \\
-  `∃a. compile c.do_mti c.max_app [z] = [a]` by
-    (Cases_on`c.do_mti`>>fs[clos_mtiTheory.compile_def]>>
-    metis_tac[clos_mtiTheory.intro_multi_sing])>>
-  specl_args_of_then ``renumber_code_locs_list``
-    (clos_numberTheory.renumber_code_locs_length|>CONJUNCT1) assume_tac>>
-  rfs[LENGTH_EQ_NUM_compute] \\
-  strip_tac \\ fs[]) |> update_precondition;
-
-*)
+val r = translate presLangTheory.default_tap_config_def;
 
 val def = spec32
   (backendTheory.attach_bitmaps_def
@@ -67,16 +48,50 @@ val def = spec32
 
 val res = translate def
 
-val def = spec32 backendTheory.compile_tap_def
+val def = spec32 backendTheory.compile_def
   |> REWRITE_RULE[max_heap_limit_32_thm]
 
 val res = translate def
 
-val def = spec32 backendTheory.compile_def
+val _ = register_type “:32 any_prog”
 
-val res = translate def
+val r = backend_passesTheory.to_flat_all_def |> spec32 |> translate;
+val r = backend_passesTheory.to_clos_all_def |> spec32 |> translate;
+val r = backend_passesTheory.to_bvl_all_def |> spec32 |> translate;
+val r = backend_passesTheory.to_bvi_all_def |> spec32 |> translate;
+
+Triviality backend_passes_to_bvi_all_side:
+  backend_passes_to_bvi_all_side c p
+Proof
+  fs [fetch "-" "backend_passes_to_bvi_all_side_def"]
+  \\ rewrite_tac [GSYM LENGTH_NIL,bvl_inlineTheory.LENGTH_remove_ticks]
+  \\ fs []
+QED
+
+val _ = update_precondition backend_passes_to_bvi_all_side
+
+val r = backend_passesTheory.to_data_all_def |> spec32 |> translate;
+
+val r = backend_passesTheory.to_word_all_def |> spec32
+          |> REWRITE_RULE [data_to_wordTheory.stubs_def,APPEND] |> translate;
+
+val r = backend_passesTheory.to_stack_all_def |> spec32
+          |> REWRITE_RULE[max_heap_limit_32_thm] |> translate;
+
+val r = backend_passesTheory.to_lab_all_def |> spec32
+          |> REWRITE_RULE[max_heap_limit_32_thm] |> translate;
+
+val r = backend_passesTheory.to_target_all_def |> spec32 |> translate;
+
+val r = presLangTheory.word_to_strs_def |> spec32 |> translate
+val r = presLangTheory.stack_to_strs_def |> spec32 |> translate
+val r = presLangTheory.lab_to_strs_def |> spec32 |> translate
+
+val r = backend_passesTheory.any_prog_pp_def |> spec32 |> translate;
+val r = backend_passesTheory.any_prog_pp_with_title_def |> spec32 |> translate;
+val r = backend_passesTheory.compile_tap_def |> spec32 |> translate;
 
-val _ = res |> hyp |> null orelse
+val _ = r |> hyp |> null orelse
         failwith "Unproved side condition in the translation of backendTheory.compile_def.";
 
 (* exportTheory *)
@@ -157,7 +172,8 @@ val _ = translate (compilerTheory.parse_sexp_input_def
 val def = spec32 (compilerTheory.compile_def);
 val res = translate def;
 
-val res = translate basisProgTheory.basis_def
+val _ = print "About to translate basis (this takes some time) ";
+val res = translate basisProgTheory.basis_def;
 
 val res = translate (primTypesTheory.prim_tenv_def
                      |> CONV_RULE (RAND_CONV EVAL));
@@ -233,7 +249,6 @@ val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 (* Rest of the translation *)
 val res = translate (extend_conf_def |> spec32 |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]);
 val res = translate parse_target_32_def;
-val res = translate Appends_def;
 val res = translate add_tap_output_def;
 
 val res = format_compiler_result_def
diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml
index fb6ced0e2a..521255201a 100644
--- a/compiler/bootstrap/translation/compiler64ProgScript.sml
+++ b/compiler/bootstrap/translation/compiler64ProgScript.sml
@@ -40,26 +40,7 @@ Proof
   rw[FUN_EQ_THM] \\ EVAL_TAC
 QED
 
-(*
-
-val def = spec64 backendTheory.compile_explorer_def
-
-val res = translate def
-
-val backend_compile_explorer_side = Q.prove(`
-  ∀x y. backend_compile_explorer_side x y = T`,
-  simp[definition"backend_compile_explorer_side_def",PULL_FORALL] \\
-  rpt gen_tac \\ ntac 3 strip_tac \\
-  qmatch_goalsub_abbrev_tac`compile c.do_mti c.max_app [z]` \\
-  `∃a. compile c.do_mti c.max_app [z] = [a]` by
-    (Cases_on`c.do_mti`>>fs[clos_mtiTheory.compile_def]>>
-    metis_tac[clos_mtiTheory.intro_multi_sing])>>
-  specl_args_of_then ``renumber_code_locs_list``
-    (clos_numberTheory.renumber_code_locs_length|>CONJUNCT1) assume_tac>>
-  rfs[LENGTH_EQ_NUM_compute] \\
-  strip_tac \\ fs[]) |> update_precondition;
-
-*)
+val r = translate presLangTheory.default_tap_config_def;
 
 val def = spec64
           (backendTheory.attach_bitmaps_def
@@ -68,17 +49,51 @@ val def = spec64
 
 val res = translate def
 
-val def = spec64 backendTheory.compile_tap_def
-            |> REWRITE_RULE[max_heap_limit_64_thm]
+val def = spec64 backendTheory.compile_def
+  |> REWRITE_RULE[max_heap_limit_64_thm]
 
 val res = translate def
 
-val def = spec64 backendTheory.compile_def
+val _ = register_type “:64 any_prog”
 
-val res = translate def
+val r = backend_passesTheory.to_flat_all_def |> spec64 |> translate;
+val r = backend_passesTheory.to_clos_all_def |> spec64 |> translate;
+val r = backend_passesTheory.to_bvl_all_def |> spec64 |> translate;
+val r = backend_passesTheory.to_bvi_all_def |> spec64 |> translate;
+
+Triviality backend_passes_to_bvi_all_side:
+  backend_passes_to_bvi_all_side c p
+Proof
+  fs [fetch "-" "backend_passes_to_bvi_all_side_def"]
+  \\ rewrite_tac [GSYM LENGTH_NIL,bvl_inlineTheory.LENGTH_remove_ticks]
+  \\ fs []
+QED
+
+val _ = update_precondition backend_passes_to_bvi_all_side
+
+val r = backend_passesTheory.to_data_all_def |> spec64 |> translate;
+
+val r = backend_passesTheory.to_word_all_def |> spec64
+          |> REWRITE_RULE [data_to_wordTheory.stubs_def,APPEND] |> translate;
+
+val r = backend_passesTheory.to_stack_all_def |> spec64
+          |> REWRITE_RULE[max_heap_limit_64_thm] |> translate;
+
+val r = backend_passesTheory.to_lab_all_def |> spec64
+          |> REWRITE_RULE[max_heap_limit_64_thm] |> translate;
+
+val r = backend_passesTheory.to_target_all_def |> spec64 |> translate;
+
+val r = presLangTheory.word_to_strs_def |> spec64 |> translate
+val r = presLangTheory.stack_to_strs_def |> spec64 |> translate
+val r = presLangTheory.lab_to_strs_def |> spec64 |> translate
+
+val r = backend_passesTheory.any_prog_pp_def |> spec64 |> translate;
+val r = backend_passesTheory.any_prog_pp_with_title_def |> spec64 |> translate;
+val r = backend_passesTheory.compile_tap_def |> spec64 |> translate;
 
-val _ = res |> hyp |> null orelse
-                           failwith "Unproved side condition in the translation of backendTheory.compile_def.";
+val _ = r |> hyp |> null orelse
+        failwith "Unproved side condition in the translation of backendTheory.compile_def.";
 
 (* exportTheory *)
 (* TODO: exportTheory functions that don't depend on the word size
@@ -158,8 +173,8 @@ val _ = translate (compilerTheory.parse_sexp_input_def
 val def = spec64 (compilerTheory.compile_def);
 val res = translate def;
 
-val _ = print "About to translate basis (this takes some time)";
-val res = translate basisProgTheory.basis_def
+val _ = print "About to translate basis (this takes some time) ";
+val res = translate basisProgTheory.basis_def;
 
 val res = translate (primTypesTheory.prim_tenv_def
                        |> CONV_RULE (RAND_CONV EVAL));
@@ -253,7 +268,6 @@ val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 (* Rest of the translation *)
 val res = translate (extend_conf_def |> spec64 |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]);
 val res = translate parse_target_64_def;
-val res = translate Appends_def;
 val res = translate add_tap_output_def;
 
 val res = format_compiler_result_def
diff --git a/compiler/bootstrap/translation/explorerProgScript.sml b/compiler/bootstrap/translation/explorerProgScript.sml
index 7178de8dc1..809a12f422 100644
--- a/compiler/bootstrap/translation/explorerProgScript.sml
+++ b/compiler/bootstrap/translation/explorerProgScript.sml
@@ -56,28 +56,24 @@ QED
 
 val _ = json_to_mlstring_ind |> update_precondition;
 
-val res = translate presLangTheory.num_to_hex_def;
+(* str_tree and displayLang *)
+
+val r = translate str_treeTheory.v2strs_def;
+val r = translate displayLangTheory.display_to_str_tree_def;
 
-val res = translate
-  (presLangTheory.display_word_to_hex_string_def |> INST_TYPE [``:'a``|->``:8``]);
-val res = translate
-  (presLangTheory.display_word_to_hex_string_def |> INST_TYPE [``:'a``|->``:64``]);
+(* presLang *)
 
-val res = translate displayLangTheory.trace_to_json_def;
-val res = translate displayLangTheory.display_to_json_def;
+val res = translate presLangTheory.num_to_hex_def;
+val res = translate (presLangTheory.word_to_display_def |> INST_TYPE [``:'a``|->``:8``]);
+val res = translate (presLangTheory.word_to_display_def |> INST_TYPE [``:'a``|->``:64``]);
 
-(* fixme: flat op datatype has been translated with use_string_type, which
-   for compatibility here needs that switch on, and looks like it results
-   in an unnecessary explode/implode pair *)
 val _ = ml_translatorLib.use_string_type true;
-val res = translate (presLangTheory.flat_op_to_display_def);
+val res = translate presLangTheory.source_to_strs_def;
 val _ = ml_translatorLib.use_string_type false;
 
-val _ = translate presLangTheory.lang_to_json_def
-
-(* again *)
 val _ = ml_translatorLib.use_string_type true;
-val r = translate presLangTheory.lit_to_display_def
+val res = translate presLangTheory.flat_to_strs_def;
+val res = translate presLangTheory.clos_op_to_display_def;
 val _ = ml_translatorLib.use_string_type false;
 
 val r = translate presLangTheory.num_to_varn_def
@@ -88,38 +84,55 @@ val num_to_varn_side = Q.prove(`
   `n MOD 26 < 26` by simp[] \\ decide_tac)
   |> update_precondition;
 
-Theorem string_imp_lam:
-  string_imp = \s. String (implode s)
-Proof
-  fs [FUN_EQ_THM,presLangTheory.string_imp_def]
-QED
+val r = presLangTheory.display_num_as_varn_def
+          |> REWRITE_RULE [presLangTheory.string_imp_def]
+          |> translate;
 
-val string_imp = SIMP_RULE bool_ss [string_imp_lam];
+val r = translate presLangTheory.data_prog_to_display_def;
+val r = translate presLangTheory.data_fun_to_display_def;
+val r = translate presLangTheory.data_to_strs_def;
 
-val r = translate (presLangTheory.display_num_as_varn_def |> string_imp);
-val _ = ml_translatorLib.use_string_type true;
-val res = translate (presLangTheory.flat_to_display_def)
-val _ = ml_translatorLib.use_string_type false;
+val r = translate presLangTheory.bvl_to_display_def;
+val r = translate presLangTheory.bvl_fun_to_display_def;
+val r = translate presLangTheory.bvl_to_strs_def;
 
-val res = translate presLangTheory.tap_flat_def;
+val r = translate presLangTheory.bvi_to_display_def;
+val r = translate presLangTheory.bvi_fun_to_display_def;
+val r = translate presLangTheory.bvi_to_strs_def;
 
-val _ = ml_translatorLib.use_string_type true;
-val r = translate (presLangTheory.clos_op_to_display_def |> string_imp);
-val _ = ml_translatorLib.use_string_type false;
+val r = translate clos_to_bvlTheory.init_code_def;
 
-val r = translate (presLangTheory.clos_to_display_def |> string_imp);
+Triviality bvl_jump_jumplist_side:
+  ∀x y. bvl_jump_jumplist_side x y
+Proof
+  ho_match_mp_tac bvl_jumpTheory.JumpList_ind
+  \\ rw [] \\ simp [Once to_bvlProgTheory.bvl_jump_jumplist_side_def]
+  \\ Cases_on ‘xs’ \\ fs []
+QED
+
+Triviality init_code_side:
+  init_code_side x
+Proof
+  fs [fetch "-" "init_code_side_def",
+      to_bvlProgTheory.clos_to_bvl_generate_generic_app_side_def,
+      to_bvlProgTheory.bvl_jump_jump_side_def,bvl_jump_jumplist_side]
+QED
 
-val res = translate presLangTheory.tap_clos_def;
+Triviality string_imp_thm:
+  string_imp = λs. String (implode s)
+Proof
+  fs [FUN_EQ_THM,presLangTheory.string_imp_def]
+QED
 
-val res = translate presLangTheory.tap_data_lang_def;
+val _ = ml_translatorLib.use_string_type true;
+val r = presLangTheory.clos_to_display_def
+          |> REWRITE_RULE [string_imp_thm]
+          |> translate
 
-(* we can't translate the tap_word bits yet, because that's 32/64 specific.
-   that's done in the to_word* scripts. *)
+val r = translate presLangTheory.clos_dec_to_display_def;
+val r = translate presLangTheory.clos_to_strs_def;
 
-(* more parts of the external interface *)
-val res = translate presLangTheory.default_tap_config_def;
-val res = translate presLangTheory.mk_tap_config_def;
-val res = translate presLangTheory.tap_data_mlstrings_def;
+val _ = update_precondition init_code_side;
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
diff --git a/compiler/bootstrap/translation/to_target32ProgScript.sml b/compiler/bootstrap/translation/to_target32ProgScript.sml
index 54ac23b6fa..1610266b38 100644
--- a/compiler/bootstrap/translation/to_target32ProgScript.sml
+++ b/compiler/bootstrap/translation/to_target32ProgScript.sml
@@ -348,6 +348,18 @@ val res = translate compile_lab_thm;
 
 val res = translate (spec32 compile_def)
 
+(* explorer specific functions *)
+
+val res = presLangTheory.asm_cmp_to_display_def |> spec32 |> translate;
+val res = presLangTheory.asm_asm_to_display_def |> spec32 |> translate;
+val res = presLangTheory.lab_asm_to_display_def |> spec32
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.lab_line_to_display_def |> spec32 |> translate;
+val res = presLangTheory.lab_fun_to_display_def |> spec32 |> translate;
+val res = presLangTheory.stack_prog_to_display_def |> spec32
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.stack_fun_to_display_def |> spec32 |> translate;
+
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
diff --git a/compiler/bootstrap/translation/to_target64ProgScript.sml b/compiler/bootstrap/translation/to_target64ProgScript.sml
index 1fc6aa3352..db0072280f 100644
--- a/compiler/bootstrap/translation/to_target64ProgScript.sml
+++ b/compiler/bootstrap/translation/to_target64ProgScript.sml
@@ -348,6 +348,18 @@ val res = translate compile_lab_thm;
 
 val res = translate (spec64 compile_def);
 
+(* explorer specific functions *)
+
+val res = presLangTheory.asm_cmp_to_display_def |> spec64 |> translate;
+val res = presLangTheory.asm_asm_to_display_def |> spec64 |> translate;
+val res = presLangTheory.lab_asm_to_display_def |> spec64
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.lab_line_to_display_def |> spec64 |> translate;
+val res = presLangTheory.lab_fun_to_display_def |> spec64 |> translate;
+val res = presLangTheory.stack_prog_to_display_def |> spec64
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.stack_fun_to_display_def |> spec64 |> translate;
+
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
diff --git a/compiler/bootstrap/translation/to_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml
index 155c12814e..cab42ff540 100644
--- a/compiler/bootstrap/translation/to_word32ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word32ProgScript.sml
@@ -631,17 +631,30 @@ val _ = translate stack_removeTheory.stub_names_def
 val res = translate (data_to_wordTheory.compile_def
                      |> SIMP_RULE std_ss [data_to_wordTheory.stubs_def] |> conv32_RHS);
 
-(* translate some 32/64 specific parts of the tap/explorer
-   that can't be translated in explorerProgScript *)
-val res = translate (presLangTheory.tap_word_def |> conv32);
-val res = translate (presLangTheory.store_name_to_display_def |> conv32);
-val res = translate (presLangTheory.stack_prog_to_display_def |> conv32);
-val res = translate (presLangTheory.stack_progs_to_display_def |> conv32);
-val res = translate (presLangTheory.tap_stack_def |> conv32);
-val res = translate (presLangTheory.lab_asm_to_display_def |> conv32);
-val res = translate (presLangTheory.lab_line_to_display_def |> conv32);
-val res = translate (presLangTheory.lab_secs_to_display_def |> conv32);
-val res = translate (presLangTheory.tap_lab_def |> conv32);
+(* explorer specific functions *)
+
+val _ = ml_translatorLib.use_string_type false;
+val r = presLangTheory.num_to_hex_def |> translate;
+val r = presLangTheory.word_to_display_def |> conv32 |> translate;
+val r = presLangTheory.item_with_word_def |> conv32 |> translate;
+val r = presLangTheory.asm_binop_to_display_def |> translate;
+val r = presLangTheory.asm_reg_imm_to_display_def |> conv32 |> translate;
+val r = presLangTheory.asm_arith_to_display_def |> conv32 |> translate;
+val r = presLangTheory.word_to_display_def |> INST_TYPE [“:'a”|->“:5”] |> translate
+val r = presLangTheory.item_with_word_def |> INST_TYPE [“:'a”|->“:5”] |> translate
+val r = presLangTheory.store_name_to_display_def |> conv32 |> translate
+val r = presLangTheory.word_exp_to_display_def |> conv32 |> translate
+val r = presLangTheory.asm_inst_to_display_def |> conv32 |> translate;
+val r = presLangTheory.ws_to_display_def |> conv32 |> translate
+val r = presLangTheory.word_seqs_def |> conv32 |> translate
+
+val _ = ml_translatorLib.use_string_type true;
+val r = presLangTheory.word_prog_to_display_def
+          |> conv32
+          |> REWRITE_RULE [presLangTheory.string_imp_def]
+          |> translate
+
+val r = presLangTheory.word_fun_to_display_def |> conv32 |> translate
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml
index c9c7d9e121..7aa3095fa1 100644
--- a/compiler/bootstrap/translation/to_word64ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word64ProgScript.sml
@@ -623,17 +623,31 @@ val _ = translate stack_removeTheory.stub_names_def
 val res = translate (data_to_wordTheory.compile_def
                      |> SIMP_RULE std_ss [data_to_wordTheory.stubs_def] |> conv64_RHS);
 
-(* translate some 32/64 specific parts of the tap/explorer
-   that can't be translated in explorerProgScript *)
-val res = translate (presLangTheory.tap_word_def |> conv64);
-val res = translate (presLangTheory.store_name_to_display_def |> conv64);
-val res = translate (presLangTheory.stack_prog_to_display_def |> conv64);
-val res = translate (presLangTheory.stack_progs_to_display_def |> conv64);
-val res = translate (presLangTheory.tap_stack_def |> conv64);
-val res = translate (presLangTheory.lab_asm_to_display_def |> conv64);
-val res = translate (presLangTheory.lab_line_to_display_def |> conv64);
-val res = translate (presLangTheory.lab_secs_to_display_def |> conv64);
-val res = translate (presLangTheory.tap_lab_def |> conv64);
+
+(* explorer specific functions *)
+
+val _ = ml_translatorLib.use_string_type false;
+val r = presLangTheory.num_to_hex_def |> translate;
+val r = presLangTheory.word_to_display_def |> conv64 |> translate;
+val r = presLangTheory.item_with_word_def |> conv64 |> translate;
+val r = presLangTheory.asm_binop_to_display_def |> translate;
+val r = presLangTheory.asm_reg_imm_to_display_def |> conv64 |> translate;
+val r = presLangTheory.asm_arith_to_display_def |> conv64 |> translate;
+val r = presLangTheory.word_to_display_def |> INST_TYPE [“:'a”|->“:5”] |> translate
+val r = presLangTheory.item_with_word_def |> INST_TYPE [“:'a”|->“:5”] |> translate
+val r = presLangTheory.store_name_to_display_def |> conv64 |> translate
+val r = presLangTheory.word_exp_to_display_def |> conv64 |> translate
+val r = presLangTheory.asm_inst_to_display_def |> conv64 |> translate;
+val r = presLangTheory.ws_to_display_def |> conv64 |> translate
+val r = presLangTheory.word_seqs_def |> conv64 |> translate
+
+val _ = ml_translatorLib.use_string_type true;
+val r = presLangTheory.word_prog_to_display_def
+          |> conv64
+          |> REWRITE_RULE [presLangTheory.string_imp_def]
+          |> translate
+
+val r = presLangTheory.word_fun_to_display_def |> conv64 |> translate
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
diff --git a/compiler/compilationLib.sml b/compiler/compilationLib.sml
index fe9d12d7fc..c310268c04 100644
--- a/compiler/compilationLib.sml
+++ b/compiler/compilationLib.sml
@@ -11,7 +11,7 @@ open preamble backendTheory
      riscv_compileLib export_riscvTheory
      ag32_compileLib export_ag32Theory
      x64_compileLib export_x64Theory
-    mlstringSyntax
+    mlstringSyntax presLangLib
 
 val _ = Globals.max_print_depth := 20;
 
@@ -47,8 +47,26 @@ in
          uninteresting_consts then false else true;
 end
 
+val output_ILs = ref (NONE : string option);
+
+fun output_IL prog transform filename_suffix title =
+  case !output_ILs of
+    NONE => ()
+  | SOME filename =>
+    let
+        val fname = filename ^ "_" ^ filename_suffix
+        val _ = print "Writing file "
+        val _ = print fname
+        val _ = print " ... "
+        val strs = ("# " ^ title ^ "\n\n") :: transform prog
+        val _ = write_strs_to_file fname strs
+        val _ = print "done.\n"
+    in () end
+
 (*
 
+val _ = (output_ILs := SOME "hello")
+
   lab_prog_def
   |> concl |> rand |> find_terms is_const |> filter interesting
 
@@ -75,6 +93,7 @@ fun compile_to_data cs conf_def prog_def data_prog_name =
         FORK_CONV(REWR_CONV(SYM flat_conf_def),
                   REWR_CONV(SYM flat_prog_def))));
     val () = computeLib.extend_compset [computeLib.Defs [flat_prog_def]] cs;
+    val _ = output_IL p flat_to_strs "flat.txt" "FlatLang"
 
     val flat_conf_source_conf =
       ``flat_conf.source_conf``
@@ -102,6 +121,7 @@ fun compile_to_data cs conf_def prog_def data_prog_name =
       to_clos_thm0 |> CONV_RULE(RAND_CONV(
         RAND_CONV(REWR_CONV(SYM clos_prog_def))));
     val () = computeLib.extend_compset [computeLib.Defs [clos_prog_def]] cs;
+    val _ = output_IL p clos_to_strs "clos.txt" "ClosLang"
 
     val to_bvl_thm0 =
       ``to_bvl ^conf_tm ^prog_tm``
@@ -123,6 +143,7 @@ fun compile_to_data cs conf_def prog_def data_prog_name =
                             REWR_CONV(SYM bvl_names_def)))));
     val () = computeLib.extend_compset [computeLib.Defs
                                          [bvl_prog_def,bvl_names_def]] cs;
+    val _ = output_IL p (bvl_to_strs names) "bvl.txt" "BVL"
 
     val bvl_conf_clos_conf_start =
       ``bvl_conf.clos_conf.start``
@@ -157,6 +178,7 @@ fun compile_to_data cs conf_def prog_def data_prog_name =
                             REWR_CONV(SYM bvi_names_def)))));
     val () = computeLib.extend_compset
       [computeLib.Defs [bvi_prog_def,bvi_names_def]] cs;
+    val _ = output_IL p (bvi_to_strs names) "bvi.txt" "BVI"
 
     val to_data_thm0 =
       ``to_data ^conf_tm ^prog_tm``
@@ -168,6 +190,7 @@ fun compile_to_data cs conf_def prog_def data_prog_name =
       |> timez "to_data" (CONV_RULE(RAND_CONV(RAND_CONV eval)))
     val (_,rest) = to_data_thm0 |> rconc |> dest_pair
     val (p,names) = rest |> dest_pair
+    val _ = output_IL p (data_to_strs names) "data.txt" "DataLang"
 
     val data_prog_def = mk_abbrev data_prog_name p
     val to_data_thm =
diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml
index afaa031f29..5e0b35efc6 100644
--- a/compiler/compilerScript.sml
+++ b/compiler/compilerScript.sml
@@ -8,7 +8,7 @@ open preamble
      lexer_funTheory lexer_implTheory
      cmlParseTheory
      inferTheory
-     backendTheory
+     backendTheory backend_passesTheory
      mlintTheory mlstringTheory basisProgTheory
      fromSexpTheory simpleSexpParseTheory
 
@@ -83,10 +83,10 @@ OPTIONS:
                 type inference. There are no gurantees of safety if
                 the type inferencer is skipped.
 
-  --explore     outputs several intermediate forms of the compiled
-                program in JSON format
+  --explore     outputs intermediate forms of the compiled program
 
   --pancake     takes a pancake program as input
+
 ADDITIONAL OPTIONS:
 
 Optimisations can be configured using the following advanced options.
@@ -241,7 +241,7 @@ Definition parse_cml_input_def:
     | Success _ x _ => INR x
 End
 
-val compile_def = Define`
+Definition compile_def:
   compile c prelude input =
     let _ = empty_ffi (strlit "finished: start up") in
     case
@@ -249,7 +249,7 @@ val compile_def = Define`
       then parse_sexp_input input
       else parse_cml_input input
     of
-    | INL msg => (Failure (ParseError msg), [])
+    | INL msg => (Failure (ParseError msg), Nil)
     | INR prog =>
        let _ = empty_ffi (strlit "finished: lexing and parsing") in
        let full_prog = if c.exclude_prelude then prog else prelude ++ prog in
@@ -260,19 +260,20 @@ val compile_def = Define`
        of
        | Failure (locs, msg) =>
            (Failure (TypeError (concat [msg; implode " at ";
-               locs_to_string (implode input) locs])), [])
+               locs_to_string (implode input) locs])), Nil)
        | Success ic =>
           let _ = empty_ffi (strlit "finished: type inference") in
           if c.only_print_types then
             (Failure (TypeError (concat ([strlit "\n"] ++
                                          inf_env_to_types_string ic ++
-                                         [strlit "\n"]))), [])
+                                         [strlit "\n"]))), Nil)
           else if c.only_print_sexp then
-            (Failure (TypeError (implode(print_sexp (listsexp (MAP decsexp full_prog))))),[])
+            (Failure (TypeError (implode(print_sexp (listsexp (MAP decsexp full_prog))))),Nil)
           else
-          case backend$compile_tap c.backend_config full_prog of
+          case backend_passes$compile_tap c.backend_config full_prog of
           | (NONE, td) => (Failure AssembleError, td)
-          | (SOME (bytes,data,c), td) => (Success (bytes,data,c), td)`;
+          | (SOME (bytes,data,c), td) => (Success (bytes,data,c), td)
+End
 
 Definition compile_pancake_def:
   compile_pancake c input =
@@ -526,12 +527,7 @@ val parse_stack_conf_def = Define`
 (* tap *)
 val parse_tap_conf_def = Define`
   parse_tap_conf ls stack =
-  let tap_all = find_str (strlit"--explore") ls in
-  let tap_all_star = (case tap_all of NONE => []
-    | SOME _ => [strlit"*"]) in
-  let taps = find_strs (strlit"--tap=") ls in
-  let fname = find_str (strlit"--tapfname=") ls in
-  INL (mk_tap_config fname (tap_all_star ++ taps))`
+    INL (<| explore_flag := MEMBER (strlit"--explore") ls |>)`
 
 (* lab *)
 val parse_lab_conf_def = Define`
@@ -626,25 +622,16 @@ val format_compiler_result_def = Define`
     (Success ((bytes:word8 list),(data:'a word list),(c:'a backend$config))) =
     (bytes_export (the [] c.lab_conf.ffi_names) bytes data, implode "")`;
 
-val Appends_def = Define`
-  Appends [] = List [] /\
-  Appends (x :: xs) = Append x (Appends xs)`;
-
 (* FIXME TODO: this is an awful workaround to avoid implementing a file writer
    right now. *)
 val add_tap_output_def = Define`
-  add_tap_output td out = if NULL td then out
-    else Appends (List [strlit "compiler output with tap data\n\n"]
-      :: FLAT (MAP (\td. let (nm, data) = tap_data_mlstrings td in
-          [List [strlit "-- "; nm; strlit " --\n\n"]; data;
-            List [strlit "\n\n"]])
-        td)
-      ++ [List [strlit "-- compiled data --\n\n"]; out])`;
+  add_tap_output td out =
+    if td = Nil then out else td :mlstring app_list`;
 
 (* The top-level compiler with everything instantiated except it doesn't do exporting *)
 
 (* The top-level compiler with almost everything instantiated except the top-level configuration *)
-val compile_64_def = Define`
+Definition compile_64_def:
   compile_64 cl input =
   let confexp = parse_target_64 cl in
   let topconf = parse_top_config cl in
@@ -671,7 +658,8 @@ val compile_64_def = Define`
     | INR err =>
     (List[], error_to_str (ConfigError (get_err_str ext_conf))))
   | _ =>
-    (List[], error_to_str (ConfigError (concat [get_err_str confexp;get_err_str topconf])))`
+    (List[], error_to_str (ConfigError (concat [get_err_str confexp;get_err_str topconf])))
+End
 
 Definition compile_pancake_64_def:
   compile_pancake_64 cl input =
@@ -711,7 +699,7 @@ Definition full_compile_64_def:
       add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err
 End
 
-val compile_32_def = Define`
+Definition compile_32_def:
   compile_32 cl input =
   let confexp = parse_target_32 cl in
   let topconf = parse_top_config cl in
@@ -738,7 +726,8 @@ val compile_32_def = Define`
     | INR err =>
     (List[], error_to_str (ConfigError (get_err_str ext_conf))))
   | _ =>
-    (List[], error_to_str (ConfigError (concat [get_err_str confexp;get_err_str topconf])))`
+    (List[], error_to_str (ConfigError (concat [get_err_str confexp;get_err_str topconf])))
+End
 
 Definition compile_pancake_32_def:
   compile_pancake_32 cl input =
@@ -777,15 +766,5 @@ Definition full_compile_32_def:
     in
       add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err
 End
-(*
-val full_compile_32_def = Define `
-  full_compile_32 cl inp fs =
-    if has_help_flag cl then
-      add_stdout fs help_string
-    else if has_version_flag cl then
-      add_stdout fs current_build_info_str
-    else
-      let (out, err) = compile_32 cl inp in
-      add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err`
-*)
+
 val _ = export_theory();
diff --git a/compiler/proofs/compilerProofScript.sml b/compiler/proofs/compilerProofScript.sml
index c291a56711..338e2fa178 100644
--- a/compiler/proofs/compilerProofScript.sml
+++ b/compiler/proofs/compilerProofScript.sml
@@ -88,10 +88,11 @@ Proof
 QED
 
 Theorem compile_tap_compile:
-   ∀conf p res td. backend$compile_tap conf p = (res,td) ⇒
+  ∀conf p res td.
+    backend_passes$compile_tap conf p = (res,td) ⇒
     backend$compile conf p = res
 Proof
-  simp[backendTheory.compile_def]
+  metis_tac [backend_passesTheory.compile_alt,FST]
 QED
 
 Definition read_limits_def:
diff --git a/examples/compilation/x64/helloCompileScript.sml b/examples/compilation/x64/helloCompileScript.sml
index 2537199656..0fc2c19184 100644
--- a/examples/compilation/x64/helloCompileScript.sml
+++ b/examples/compilation/x64/helloCompileScript.sml
@@ -5,6 +5,8 @@ open preamble helloProgTheory compilationLib
 
 val _ = new_theory "helloCompile"
 
+val _ = (output_ILs := SOME "hello");
+
 val hello_compiled = save_thm("hello_compiled",
   compile_x64 "hello" hello_prog_def);