Merge pull request #965 from CakeML/explorer

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.

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]>>