From 3307c1e62d544ac16661bf867be473ca48503c52 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 21 Jul 2023 16:33:55 +0200 Subject: [PATCH 01/16] Define a function that returns each intermediate form of a compilation The end of the file also counts proves a theorem showing that there are 36 outputs. this can be understood as there being 36 compilation passes in the compiler at present. As new passes are added (and some removed), this theorem will need to be revised. --- compiler/backend/backend_passesScript.sml | 330 ++++++++++++++++++++++ 1 file changed, 330 insertions(+) create mode 100644 compiler/backend/backend_passesScript.sml diff --git a/compiler/backend/backend_passesScript.sml b/compiler/backend/backend_passesScript.sml new file mode 100644 index 0000000000..fbcca662da --- /dev/null +++ b/compiler/backend/backend_passesScript.sml @@ -0,0 +1,330 @@ +(* + Reformulates compile definition to expose each internal compiler phase +*) + +open preamble backendTheory + +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 + +Triviality 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 + +Triviality 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 bvl_to_clos",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 + +Triviality 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 + +(* +bvl_inlineTheory.optimise_def +*) + +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 + +Triviality 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 + +Triviality 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 + +Triviality 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 + +Triviality 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 + +Triviality 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 + +Triviality 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 + +val _ = export_theory(); From ce0678a033756fe3eb1c3a669c386157c2101f5c Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 21 Jul 2023 16:50:34 +0200 Subject: [PATCH 02/16] Tidy up --- compiler/backend/README.md | 4 ++++ compiler/backend/backend_passesScript.sml | 9 +++------ 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/compiler/backend/README.md b/compiler/backend/README.md index 0e399691c5..2b3a62ee95 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 diff --git a/compiler/backend/backend_passesScript.sml b/compiler/backend/backend_passesScript.sml index fbcca662da..0693eeadc6 100644 --- a/compiler/backend/backend_passesScript.sml +++ b/compiler/backend/backend_passesScript.sml @@ -1,5 +1,6 @@ (* - Reformulates compile definition to expose each internal compiler phase + Reformulates compile definition to expose the result of each internal + compiler pass *) open preamble backendTheory @@ -91,7 +92,7 @@ Definition to_bvl_all_def: 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 bvl_to_clos",Bvl prog' func_names)] 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 @@ -107,10 +108,6 @@ Proof \\ rpt (pairarg_tac \\ gvs []) QED -(* -bvl_inlineTheory.optimise_def -*) - Definition to_bvi_all_def: to_bvi_all (c:'a config) p = let (ps,c,p,names) = to_bvl_all c p in From 0cf77adab059c2c45fd939e55da86e42ee07abdf Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 2 Aug 2023 07:01:58 +0200 Subject: [PATCH 03/16] Make compilationLib output BVL and DataLang pretty print --- compiler/backend/README.md | 6 + compiler/backend/backend_passesScript.sml | 18 +- compiler/backend/displayLangScript.sml | 37 +- compiler/backend/presLangLib.sig | 13 + compiler/backend/presLangLib.sml | 55 +++ compiler/backend/presLangScript.sml | 456 ++++++++++++------ compiler/backend/str_treeScript.sml | 161 +++++++ compiler/compilationLib.sml | 22 +- .../compilation/x64/helloCompileScript.sml | 9 + 9 files changed, 615 insertions(+), 162 deletions(-) create mode 100644 compiler/backend/presLangLib.sig create mode 100644 compiler/backend/presLangLib.sml create mode 100644 compiler/backend/str_treeScript.sml diff --git a/compiler/backend/README.md b/compiler/backend/README.md index 2b3a62ee95..49c10caac6 100644 --- a/compiler/backend/README.md +++ b/compiler/backend/README.md @@ -238,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. @@ -307,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/backend_passesScript.sml b/compiler/backend/backend_passesScript.sml index 0693eeadc6..b947ce70da 100644 --- a/compiler/backend/backend_passesScript.sml +++ b/compiler/backend/backend_passesScript.sml @@ -37,7 +37,7 @@ Definition to_flat_all_def: ((ps: (mlstring # 'a any_prog) list),c,p) End -Triviality to_flat_thm: +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, @@ -55,7 +55,7 @@ Definition to_clos_all_def: ((ps: (mlstring # 'a any_prog) list),c,p) End -Triviality to_clos_thm: +Theorem to_clos_thm: SND (to_clos_all c p) = to_clos c p Proof assume_tac to_flat_thm @@ -99,7 +99,7 @@ Definition to_bvl_all_def: ((ps: (mlstring # 'a any_prog) list),c,p,func_names) End -Triviality to_bvl_thm: +Theorem to_bvl_thm: SND (to_bvl_all c p ) = to_bvl c p Proof assume_tac to_clos_thm @@ -138,7 +138,7 @@ Definition to_bvi_all_def: ((ps: (mlstring # 'a any_prog) list),c,p,names) End -Triviality to_bvi_thm: +Theorem to_bvi_thm: SND (to_bvi_all c p ) = to_bvi c p Proof assume_tac to_bvl_thm @@ -169,7 +169,7 @@ Definition to_data_all_def: ((ps: (mlstring # 'a any_prog) list),c,p,names) End -Triviality to_data_thm: +Theorem to_data_thm: SND (to_data_all (c:'a config) p) = to_data c p Proof assume_tac to_bvi_thm @@ -228,7 +228,7 @@ Definition to_word_all_def: ((ps: (mlstring # 'a any_prog) list),c,p,names) End -Triviality to_word_thm: +Theorem to_word_thm: SND (to_word_all (c:'a config) p) = to_word c p Proof assume_tac to_data_thm @@ -249,7 +249,7 @@ Definition to_stack_all_def: ((ps: (mlstring # 'a any_prog) list),bm,c,p,names) End -Triviality to_stack_thm: +Theorem to_stack_thm: SND (to_stack_all (c:'a config) p) = to_stack c p Proof assume_tac to_word_thm @@ -279,7 +279,7 @@ Definition to_lab_all_def: ((ps: (mlstring # 'a any_prog) list),bm,c,p:'a prog,names) End -Triviality to_lab_thm: +Theorem to_lab_thm: SND (to_lab_all (c:'a config) p) = to_lab c p Proof assume_tac to_stack_thm @@ -296,7 +296,7 @@ Definition to_target_all_def: ((ps: (mlstring # 'a any_prog) list), attach_bitmaps names c bm p) End -Triviality to_target_thm: +Theorem to_target_thm: SND (to_target_all c p) = to_target c p Proof assume_tac to_lab_thm 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..87ab88b6a0 --- /dev/null +++ b/compiler/backend/presLangLib.sig @@ -0,0 +1,13 @@ +signature presLangLib = +sig + + include Abbrev + + val data_to_strs : term (* names *) -> term (* prog *) -> string list + val bvl_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..e9afcf8e60 --- /dev/null +++ b/compiler/backend/presLangLib.sml @@ -0,0 +1,55 @@ +(* + 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 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 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..be70036ae4 100644 --- a/compiler/backend/presLangScript.sml +++ b/compiler/backend/presLangScript.sml @@ -6,14 +6,14 @@ open preamble astTheory mlintTheory mloptionTheory open flatLangTheory closLangTheory displayLangTheory source_to_flatTheory dataLangTheory wordLangTheory labLangTheory - stackLangTheory; + stackLangTheory bvlTheory; val _ = new_theory"presLang"; (* basics *) val empty_item_def = Define` - empty_item name = Item NONE name []`; + empty_item name = String name`; val num_to_display_def = Define` num_to_display (n : num) = String (toString n)`; @@ -38,6 +38,10 @@ val num_to_hex_def = Define ` (if n < 16 then [] else num_to_hex (n DIV 16)) ++ num_to_hex_digit (n MOD 16)`; +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 check that is true. *) @@ -80,12 +84,12 @@ val lit_to_display_def = Define` Item NONE (strlit "Word64") [display_word_to_hex_string w])`; val list_to_display_def = Define` - (list_to_display f xs = displayLang$List (MAP f xs))` + (list_to_display f xs = displayLang$Tuple (MAP f xs))` val option_to_display_def = Define` (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'])` (* semantic ops and values *) @@ -161,7 +165,7 @@ val shift_to_display_def = Define` (shift_to_display Ror = empty_item (strlit "Ror"))`; - (* flatLang *) +(* flatLang *) val MEM_pat_size = prove( ``!pats a. MEM a (pats:flatLang$pat list) ==> pat_size a < pat1_size pats``, @@ -266,127 +270,146 @@ val MEM_pats_size = prove( Induct \\ fs [flatLangTheory.exp_size_def] \\ rw [] \\ fs [flatLangTheory.exp_size_def] \\ res_tac \\ fs []); -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` + ) +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 = 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]` + | 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`; +Definition flat_to_display_decs_def: + flat_to_display_decs = list_to_display flat_to_display_dec +End -(* 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 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 _ => String(strlit "Constant") | 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 _ => String(strlit "Build") + | 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") + | Equal => String (strlit "Equal") | EqualConst c => Item NONE (strlit "EqualConst") [] (* TODO: fix *) | 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,128 +417,220 @@ 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 + +Definition commas_def: + commas [] = strlit "" ∧ + commas [x] = x ∧ + commas (x::xs) = x ^ strlit "," ^ commas xs +End (* The clos_to_display function uses the same approach to de bruijn indices as the pat_to_display function *) -val clos_to_display_def = tDefine "clos_to_display" ` +Definition clos_to_display_def: (clos_to_display h (Var t n) = - Item (SOME t) (strlit "Var") [display_num_as_varn (h-n-1)]) /\ + 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; + 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); + Item (SOME t) (strlit "let") + [Tuple (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]) /\ + 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]) /\ + Item (SOME t) (strlit "tick") [clos_to_display h x]) /\ (clos_to_display h (Handle t x y) = - Item (SOME t) (strlit "Handle") + 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)]) /\ + Item (SOME t) (strlit "call") ([num_to_display ticks; num_to_display dest] ++ + 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") + Item (SOME t) (strlit "app") + ([option_to_display num_to_display opt_n; + clos_to_display h x] ++ MAP (clos_to_display h) xs)) /\ + (clos_to_display 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 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); + Tuple (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)]) /\ + Item (SOME t) (strlit "op") (clos_op_to_display LN op :: + 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) /\ + Tuple [display_num_as_varn (h+i); String (strlit "<-"); 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 [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 + :: clos_to_display_letrecs 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 + +(* 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 (* 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 = Tuple (MAP num_to_display + (MAP FST (sptree$toSortedAList ns))) +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 -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") +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 + +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")`; + | 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 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`; + num_to_display n2; data_prog_to_display names prog]) ps`; (* asm *) @@ -755,7 +870,7 @@ val word_exp_to_display_def = tDefine "word_exp_to_display" ` 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 n; displayLang$Tuple (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") @@ -797,13 +912,13 @@ val word_prog_to_display_def = tDefine "word_prog_to_display" ` (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 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; + 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 NONE = empty_item (strlit "none")) /\ (word_prog_to_display_handler (SOME (n1, prog, n2, n3)) = - Item NONE (strlit "SOME") [Tuple [num_to_display n1; + 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 @@ -893,4 +1008,59 @@ val tap_stack_def = Define ` val tap_lab_def = Define ` tap_lab conf v = add_tap conf (strlit "lab") lab_secs_to_display v`; +(* ------------------------- *) + +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 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 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")) + +(* + +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/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/compilationLib.sml b/compiler/compilationLib.sml index fe9d12d7fc..beaae867d6 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 @@ -123,6 +141,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`` @@ -168,6 +187,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/examples/compilation/x64/helloCompileScript.sml b/examples/compilation/x64/helloCompileScript.sml index 2537199656..1b5c53ca33 100644 --- a/examples/compilation/x64/helloCompileScript.sml +++ b/examples/compilation/x64/helloCompileScript.sml @@ -5,7 +5,16 @@ open preamble helloProgTheory compilationLib val _ = new_theory "helloCompile" +val _ = (compilationLib.output_ILs := SOME "hello"); + val hello_compiled = save_thm("hello_compiled", compile_x64 "hello" hello_prog_def); +(* +val backend_config_def = x64_backend_config_def; +val cbv_to_bytes = cbv_to_bytes_x64; +val name = "hello_compiled"; +val prog_def = hello_prog_def; +*) + val _ = export_theory (); From db9158d1bc95f468a24889cde253beaecba81788 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 3 Aug 2023 12:58:53 +0200 Subject: [PATCH 04/16] Progress on new --explore definitions --- compiler/backend/backendScript.sml | 22 +- compiler/backend/backend_passesScript.sml | 37 +- compiler/backend/presLangScript.sml | 770 +++++++++++++--------- 3 files changed, 518 insertions(+), 311 deletions(-) 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 index b947ce70da..070a8e621e 100644 --- a/compiler/backend/backend_passesScript.sml +++ b/compiler/backend/backend_passesScript.sml @@ -3,7 +3,7 @@ compiler pass *) -open preamble backendTheory +open preamble backendTheory presLangTheory val _ = new_theory"backend_passes"; @@ -324,4 +324,39 @@ Proof \\ 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 LN (funs,decs) + | 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/presLangScript.sml b/compiler/backend/presLangScript.sml index be70036ae4..d58ca8aaad 100644 --- a/compiler/backend/presLangScript.sml +++ b/compiler/backend/presLangScript.sml @@ -325,15 +325,18 @@ Termination End Definition flat_to_display_dec_def: - flat_to_display_dec d = + 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 -Definition flat_to_display_decs_def: - flat_to_display_decs = list_to_display flat_to_display_dec +(* source to displayLang *) + +Definition source_to_display_dec_def: + source_to_display_dec (d:ast$dec) = + empty_item (strlit "source dec") End (* clos to displayLang *) @@ -363,6 +366,30 @@ Definition attach_name_def: | 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") [display_word_to_hex_string 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") [display_word_to_hex_string 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 @@ -371,9 +398,9 @@ Definition clos_op_to_display_def: | GlobalsPtr => String (strlit "GlobalsPtr") | SetGlobalsPtr => String (strlit "SetGlobalsPtr") | Cons num => item_with_num (strlit "Cons") num - | Constant _ => String(strlit "Constant") + | Constant c => Item NONE (strlit "Constant") [const_to_display c] | ConsExtend num => item_with_num (strlit "ConsExtend") num - | Build _ => String(strlit "Build") + | Build bs => Item NONE (strlit "Build") (MAP const_part_to_display bs) | El => String (strlit "El") | LengthBlock => String (strlit "LengthBlock") | Length => String (strlit "Length") @@ -399,7 +426,7 @@ Definition clos_op_to_display_def: | Label num => Item NONE (strlit "Label") [String (attach_name ns (SOME num))] | FFI s => Item NONE (strlit "FFI") [string_imp s] | Equal => String (strlit "Equal") - | EqualConst c => Item NONE (strlit "EqualConst") [] (* TODO: fix *) + | EqualConst c => Item NONE (strlit "EqualConst") [const_part_to_display c] | Const i => Item NONE (strlit "Const") [int_to_display i] | Add => String (strlit "Add") | Sub => String (strlit "Sub") @@ -445,67 +472,82 @@ Definition commas_def: commas (x::xs) = x ^ strlit "," ^ commas xs End -(* The clos_to_display function uses the same approach to de bruijn +(* The clos_to_display ns function uses the same approach to de bruijn indices as the pat_to_display function *) Definition clos_to_display_def: - (clos_to_display h (Var t n) = + (clos_to_display ns 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") - [Tuple (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) = + (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 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] ++ - MAP (clos_to_display h) xs)) /\ - (clos_to_display h (App t opt_n x xs) = + [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 h x] ++ MAP (clos_to_display h) xs)) /\ - (clos_to_display h (Fn name_hint n1 n2 vn x) = + 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 name_hint n1 n2 es e) = + 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; - Tuple (clos_to_display_letrecs h (LENGTH es-1) (LENGTH es) es); - clos_to_display h e]) /\ - (clos_to_display h (Op t op xs) = + 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 h) xs)) /\ - (clos_to_display_lets h i [] = []) /\ - (clos_to_display_lets h i (x::xs) = - Tuple [display_num_as_varn (h+i); String (strlit "<-"); 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) = + 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) + 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)` + | 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: @@ -557,6 +599,58 @@ Definition bvl_fun_to_display_def: 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 *) Definition num_set_to_display_def: @@ -626,28 +720,24 @@ Definition data_fun_to_display_def: data_prog_to_display names body] End -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 names prog]) ps`; - (* 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_num (strlit "Imm") (w2n 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; @@ -659,20 +749,23 @@ 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_with_nums (strlit "Addr") [reg; w2n 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» @@ -681,9 +774,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] @@ -700,18 +794,20 @@ 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] | 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) @@ -720,11 +816,12 @@ val asm_asm_to_display_def = Define ` num_to_display (w2n w)] | Call w => item_with_num «Call» (w2n w) | JumpReg r => item_with_num «JumpReg>» r - | Loc r w => item_with_nums «Loc» [r; w2n w]` + | Loc r w => item_with_nums «Loc» [r; w2n 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» @@ -743,107 +840,165 @@ 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 n => item_with_num «Temp» (w2n n) +End -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_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 + +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) = + Item NONE «get» [num_to_display n; store_name_to_display sn] ∧ + stack_prog_to_display ns (Set sn n) = + Item NONE «set» [store_name_to_display sn; + num_to_display n] ∧ + stack_prog_to_display ns (OpCurrHeap b n1 n2) = + Item NONE «op_curr_heap» + [asm_binop_to_display b; num_to_display n1; 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 «return» + [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_with_num «direct» 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» + | NONE => empty_item «no_handle» + | SOME (p,l1,l2) => + Item NONE «handle» + [num_to_display 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» [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_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» [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`; + 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) = item_with_nums «stack_store» [n; m] ∧ + stack_prog_to_display ns (StackStoreAny n m) = item_with_nums «stack_store_any» [n; m] ∧ + stack_prog_to_display ns (StackLoad n m) = item_with_nums «stack_load» [n; m] ∧ + stack_prog_to_display ns (StackLoadAny n m) = item_with_nums «stack_load_any» [n; m] ∧ + 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) = item_with_nums «bitmap_load» [n; m] ∧ + 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 + +Triviality MEM_word_exps_size_ARB = + wordLangTheory.MEM_IMP_exp_size |> Q.GEN `l` |> Q.SPEC `ARB`; -val word_exp_to_display_def = tDefine "word_exp_to_display" ` +Definition word_exp_to_display_def: (word_exp_to_display (wordLang$Const v) = item_with_num (strlit "Const") (w2n v)) /\ (word_exp_to_display (Var n) @@ -860,153 +1015,96 @@ 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 [] - ); +End -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") +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; 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") + (word_prog_to_display ns (Inst i) = + Item NONE (strlit "inst") [asm_inst_to_display i]) /\ + (word_prog_to_display ns (Assign n exp) = + Item NONE (strlit "assign") + [num_to_display n; word_exp_to_display exp]) /\ + (word_prog_to_display ns (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") + (word_prog_to_display ns (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_prog_to_display ns (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» + (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) = Item NONE «op_curr_heap» [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") + (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") + [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] (* 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)) = + (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 "none")) /\ + (word_prog_to_display_ret ns (SOME (n1, ms, prog, n2, n3)) = + Item NONE (strlit "some") [Tuple [num_to_display n1; num_set_to_display ms; + word_prog_to_display ns prog; num_to_display n2; num_to_display n3]]) /\ + (word_prog_to_display_handler ns NONE = empty_item (strlit "none")) /\ + (word_prog_to_display_handler ns (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`; + word_prog_to_display ns prog; num_to_display 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 (* ------------------------- *) @@ -1015,6 +1113,30 @@ Definition map_to_append_def: 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 names (decs,funs) = + Append (map_to_append (v2strs (strlit "\n\n") o + display_to_str_tree o + clos_dec_to_display names) funs) + (map_to_append (v2strs (strlit "\n\n") o + display_to_str_tree o + clos_fun_to_display names) decs) +End + Definition bvl_to_strs_def: bvl_to_strs names xs = map_to_append (v2strs (strlit "\n\n") o @@ -1032,6 +1154,23 @@ val bvl_test = |> 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 @@ -1049,6 +1188,37 @@ val data_test = |> 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))” @@ -1063,4 +1233,14 @@ val _ = data_to_strs data_prog_tm names_tm |> print_strs *) +(* + +TODO: + - do source pp + - get names in closLang + clos_to_bvlTheory.get_src_names_def + clos_to_bvlTheory.add_src_names_def + +*) + val _ = export_theory(); From 419b208da80a2efe842668feddbb204efd12942b Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 3 Aug 2023 13:12:20 +0200 Subject: [PATCH 05/16] Update compiler for new --explore output --- compiler/compilerScript.sml | 63 +++++++++++++------------------------ 1 file changed, 21 insertions(+), 42 deletions(-) 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(); From d38be62c62cea505716eebbd6d6d0d5181530f7f Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 3 Aug 2023 23:37:41 +0200 Subject: [PATCH 06/16] More progress on new explore --- compiler/backend/backend_passesScript.sml | 2 +- compiler/backend/presLangLib.sig | 5 +- compiler/backend/presLangLib.sml | 19 + compiler/backend/presLangScript.sml | 413 +++++++++++++----- compiler/compilationLib.sml | 3 + .../compilation/x64/helloCompileScript.sml | 9 +- 6 files changed, 337 insertions(+), 114 deletions(-) diff --git a/compiler/backend/backend_passesScript.sml b/compiler/backend/backend_passesScript.sml index 070a8e621e..3f05f01fe7 100644 --- a/compiler/backend/backend_passesScript.sml +++ b/compiler/backend/backend_passesScript.sml @@ -328,7 +328,7 @@ 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 LN (funs,decs) + | 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 diff --git a/compiler/backend/presLangLib.sig b/compiler/backend/presLangLib.sig index 87ab88b6a0..0c8f5a5146 100644 --- a/compiler/backend/presLangLib.sig +++ b/compiler/backend/presLangLib.sig @@ -3,8 +3,11 @@ sig include Abbrev - val data_to_strs : term (* names *) -> term (* prog *) -> string list + 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 diff --git a/compiler/backend/presLangLib.sml b/compiler/backend/presLangLib.sml index e9afcf8e60..911471c494 100644 --- a/compiler/backend/presLangLib.sml +++ b/compiler/backend/presLangLib.sml @@ -32,12 +32,31 @@ fun dest_app_list tm = let 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] diff --git a/compiler/backend/presLangScript.sml b/compiler/backend/presLangScript.sml index d58ca8aaad..440c579ecc 100644 --- a/compiler/backend/presLangScript.sml +++ b/compiler/backend/presLangScript.sml @@ -6,37 +6,45 @@ open preamble astTheory mlintTheory mloptionTheory open flatLangTheory closLangTheory displayLangTheory source_to_flatTheory dataLangTheory wordLangTheory labLangTheory - stackLangTheory bvlTheory; + stackLangTheory bvlTheory clos_to_bvlTheory; val _ = new_theory"presLang"; (* basics *) -val empty_item_def = Define` - empty_item name = String 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) @@ -63,11 +71,16 @@ 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 word_to_display_def: + word_to_display w = + empty_item (implode ("0x" ++ num_to_hex (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)]) /\ @@ -78,53 +91,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$Tuple (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'])` + | 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")) @@ -133,18 +154,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")) @@ -153,31 +176,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"))`; + (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 *) -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 []); +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] @@ -187,11 +389,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 @@ -200,8 +404,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 @@ -253,22 +456,28 @@ 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 Definition add_name_hint_def: add_name_hint prefix name_hint = @@ -332,13 +541,6 @@ Definition flat_to_display_dec_def: | Dexn n1 n2 => item_with_nums (strlit "dexn") [n1; n2] End -(* source to displayLang *) - -Definition source_to_display_dec_def: - source_to_display_dec (d:ast$dec) = - empty_item (strlit "source dec") -End - (* clos to displayLang *) Definition num_to_varn_def: @@ -374,7 +576,7 @@ Definition const_part_to_display_def: 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") [display_word_to_hex_string w] + Item NONE (strlit "W64") [word_to_display w] End Definition const_to_display_def: @@ -385,7 +587,7 @@ Definition const_to_display_def: const_to_display (ConstStr s) = Item NONE (strlit "ConstStr") [String (concat [strlit "\""; s; strlit "\""])] ∧ const_to_display (ConstWord64 w) = - Item NONE (strlit "ConstWord64") [display_word_to_hex_string w] + Item NONE (strlit "ConstWord64") [word_to_display w] Termination WF_REL_TAC ‘measure const_size’ End @@ -734,7 +936,7 @@ End 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 Definition asm_arith_to_display_def: @@ -754,7 +956,8 @@ End 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 Definition asm_memop_to_display_def: @@ -800,7 +1003,8 @@ End 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] @@ -810,13 +1014,13 @@ End 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 *) @@ -840,7 +1044,7 @@ Definition store_name_to_display_def: | 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: @@ -1000,7 +1204,7 @@ Triviality MEM_word_exps_size_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) @@ -1023,6 +1227,12 @@ Termination \\ rw [] 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") @@ -1056,7 +1266,11 @@ Definition word_prog_to_display_def: (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] (* TODO: include ws *)) /\ + [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")) /\ @@ -1128,13 +1342,14 @@ Definition flat_to_strs_def: End Definition clos_to_strs_def: - clos_to_strs names (decs,funs) = - Append (map_to_append (v2strs (strlit "\n\n") o - display_to_str_tree o - clos_dec_to_display names) funs) - (map_to_append (v2strs (strlit "\n\n") o - display_to_str_tree o - clos_fun_to_display names) decs) + 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: @@ -1233,14 +1448,4 @@ val _ = data_to_strs data_prog_tm names_tm |> print_strs *) -(* - -TODO: - - do source pp - - get names in closLang - clos_to_bvlTheory.get_src_names_def - clos_to_bvlTheory.add_src_names_def - -*) - val _ = export_theory(); diff --git a/compiler/compilationLib.sml b/compiler/compilationLib.sml index beaae867d6..c310268c04 100644 --- a/compiler/compilationLib.sml +++ b/compiler/compilationLib.sml @@ -93,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`` @@ -120,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`` @@ -176,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`` diff --git a/examples/compilation/x64/helloCompileScript.sml b/examples/compilation/x64/helloCompileScript.sml index 1b5c53ca33..0fc2c19184 100644 --- a/examples/compilation/x64/helloCompileScript.sml +++ b/examples/compilation/x64/helloCompileScript.sml @@ -5,16 +5,9 @@ open preamble helloProgTheory compilationLib val _ = new_theory "helloCompile" -val _ = (compilationLib.output_ILs := SOME "hello"); +val _ = (output_ILs := SOME "hello"); val hello_compiled = save_thm("hello_compiled", compile_x64 "hello" hello_prog_def); -(* -val backend_config_def = x64_backend_config_def; -val cbv_to_bytes = cbv_to_bytes_x64; -val name = "hello_compiled"; -val prog_def = hello_prog_def; -*) - val _ = export_theory (); From e4bc0085f12d1e0f77e48be9817a76367bf3c0c6 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 13 Jul 2023 23:09:55 +0200 Subject: [PATCH 07/16] More permissive no_closures and minor tidy up --- translator/ml_translatorScript.sml | 157 ++++++++++++++--------------- 1 file changed, 77 insertions(+), 80 deletions(-) diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index 0b49015a10..91594f61a6 100644 --- a/translator/ml_translatorScript.sml +++ b/translator/ml_translatorScript.sml @@ -36,25 +36,28 @@ Definition empty_state_def: eval_state := NONE|> End -val Eval_def = Define ` +Definition Eval_def: Eval env exp P = !refs. ?res refs'. eval_rel (empty_state with refs := refs) env exp (empty_state with refs := refs ++ refs') res /\ - P (res:v)`; + P (res:v) +End -val AppReturns_def = Define ` (* think of this as a Hoare triple {P} cl {Q} *) +Definition AppReturns_def: (* think of this as a Hoare triple {P} cl {Q} *) AppReturns P cl Q = !v. P v ==> !refs. ?env exp refs' u. do_opapp [cl;v] = SOME (env,exp) /\ eval_rel (empty_state with refs := refs) env exp (empty_state with refs := refs++refs') u /\ - Q u`; + Q u +End -val Arrow_def = Define ` +Definition Arrow_def: Arrow a b = - \f v. !x. AppReturns (a x) v (b (f x))`; + \f v. !x. AppReturns (a x) v (b (f x)) +End Overload "-->" = ``Arrow`` @@ -376,18 +379,21 @@ QED (* Equality *) -val no_closures_def = tDefine "no_closures" ` - (no_closures (Litv l) = T) /\ - (no_closures (Conv name vs) = EVERY no_closures vs) /\ - (no_closures (FP_WordTree _) = T) /\ - (no_closures (FP_BoolTree _) = T) /\ - (no_closures _ = F)` - (WF_REL_TAC `measure v_size` \\ REPEAT STRIP_TAC +Definition no_closures_def: + (no_closures (Conv _ vs) = EVERY no_closures vs) /\ + (no_closures (Vectorv vs) = EVERY no_closures vs) /\ + (no_closures (Closure _ _ _) = F) /\ + (no_closures (Recclosure _ _ _) = F) /\ + (no_closures (Env _ _) = F) /\ + (no_closures _ = T) +Termination + WF_REL_TAC `measure v_size` \\ REPEAT STRIP_TAC \\ Induct_on `vs` \\ FULL_SIMP_TAC (srw_ss()) [MEM] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [MEM,v_size_def] - \\ DECIDE_TAC) + \\ DECIDE_TAC +End -val types_match_def = tDefine "types_match" ` +Definition types_match_def: (types_match (Litv l1) (Litv l2) = lit_same_type l1 l2) /\ (types_match (Loc l1) (Loc l2) = T) /\ (types_match (Conv cn1 vs1) (Conv cn2 vs2) = @@ -399,15 +405,18 @@ val types_match_def = tDefine "types_match" ` (types_match v1 v2 /\ types_match_list vs1 vs2)) /\ (* We could change this case to T, or change the semantics to have a type error * when equality reaches unequal-length lists *) - (types_match_list _ _ = F)` - (WF_REL_TAC `measure (\x. case x of INL (v1,v2) => v_size v1 | - INR (vs1,vs2) => v1_size vs1)`); + (types_match_list _ _ = F) +Termination + WF_REL_TAC `measure (\x. case x of INL (v1,v2) => v_size v1 | + INR (vs1,vs2) => v1_size vs1)` +End -val EqualityType_def = Define ` +Definition EqualityType_def: EqualityType (abs:'a->v->bool) <=> (!x1 v1. abs x1 v1 ==> no_closures v1) /\ (!x1 v1 x2 v2. abs x1 v1 /\ abs x2 v2 ==> ((v1 = v2) = (x1 = x2))) /\ - (!x1 v1 x2 v2. abs x1 v1 /\ abs x2 v2 ==> types_match v1 v2)`; + (!x1 v1 x2 v2. abs x1 v1 /\ abs x2 v2 ==> types_match v1 v2) +End Triviality LSL_n2w_eq: a < 2 ** (dimindex (:'a) - n) /\ b < 2 ** (dimindex (:'a) - n) /\ @@ -2078,9 +2087,10 @@ QED (* vectors *) -val VECTOR_TYPE_def = Define ` +Definition VECTOR_TYPE_def: VECTOR_TYPE a (Vector l) v <=> - ?l'. v = Vectorv l' /\ LENGTH l = LENGTH l' /\ LIST_REL a l l'`; + ?l'. v = Vectorv l' /\ LENGTH l = LENGTH l' /\ LIST_REL a l l' +End Definition VECTOR_v_def: VECTOR_v v_a (Vector l) = Vectorv (MAP v_a l) @@ -2190,9 +2200,9 @@ QED (* This is useful to force the type inferencer to give the type unit to an unused argument. *) -val force_unit_type_def = Define ` - force_unit_type (u:unit) x = x` - |> curry save_thm "force_unit_type_def[simp,compute]"; +Definition force_unit_type_def[simp,compute]: + force_unit_type (u:unit) x = x +End Theorem Eval_force_unit_type: Eval env x1 (UNIT_TYPE u) ==> @@ -2214,8 +2224,9 @@ Proof \\ fs [can_pmatch_all_def,pmatch_def] QED -val force_gc_to_run_def = Define ` - force_gc_to_run (i1:int) (i2:int) = ()`; +Definition force_gc_to_run_def: + force_gc_to_run (i1:int) (i2:int) = () +End Theorem Eval_force_gc_to_run: Eval env x1 (INT i1) ==> @@ -2225,8 +2236,9 @@ Proof tac2 \\ fs [do_app_def,INT_def,UNIT_TYPE_def] QED -val force_out_of_memory_error_def = Define ` - force_out_of_memory_error (x:'a) = x`; +Definition force_out_of_memory_error_def: + force_out_of_memory_error (x:'a) = x +End val two_pow_64 = EVAL ``2i**64`` |> concl |> rand @@ -2346,13 +2358,16 @@ Proof SIMP_TAC (srw_ss()) [Eval_Val_BOOL_T,TRUE_def] QED -val MEMBER_def = Define ` +Definition MEMBER_def: (MEMBER (x:'a) [] <=> F) /\ - (MEMBER x (y::ys) <=> (x = y) \/ MEMBER x ys)`; + (MEMBER x (y::ys) <=> (x = y) \/ MEMBER x ys) +End -val MEM_EQ_MEMBER = Q.prove( - `!ys x. MEM x ys = MEMBER x ys`, - Induct \\ FULL_SIMP_TAC (srw_ss()) [MEMBER_def]); +Triviality MEM_EQ_MEMBER: + !ys x. MEM x ys = MEMBER x ys +Proof + Induct \\ FULL_SIMP_TAC (srw_ss()) [MEMBER_def] +QED Theorem MEMBER_INTRO: (MEM = MEMBER) /\ (MEM x = MEMBER x) /\ (MEM x ys = MEMBER x ys) @@ -2380,15 +2395,17 @@ QED (* removing shadowed elements from an alist *) -val ASHADOW_def = tDefine "ASHADOW" ` +Definition ASHADOW_def: (ASHADOW [] = []) /\ (ASHADOW (x::xs) = if EXISTS (\y. FST x = FST y) xs then x :: ASHADOW (FILTER (\y. FST x <> FST y) xs) - else x :: ASHADOW xs)` - (WF_REL_TAC `measure LENGTH` \\ fs [LENGTH] \\ REPEAT STRIP_TAC + else x :: ASHADOW xs) +Termination + WF_REL_TAC `measure LENGTH` \\ fs [LENGTH] \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC LESS_EQ_LESS_TRANS - \\ Q.EXISTS_TAC `LENGTH xs` \\ fs [rich_listTheory.LENGTH_FILTER_LEQ]) + \\ Q.EXISTS_TAC `LENGTH xs` \\ fs [rich_listTheory.LENGTH_FILTER_LEQ] +End val ASHADOW_PREFIX = Q.prove( `!xs ys. @@ -2456,49 +2473,24 @@ val ALL_DISTINCT_MAP_FST_ASHADOW = Q.prove( (* size lemmas *) -val v1_size = Q.prove( - `!vs v. (MEM v vs ==> v_size v < v1_size vs)`, - Induct \\ SRW_TAC [] [semanticPrimitivesTheory.v_size_def] - \\ RES_TAC \\ DECIDE_TAC); - -(* TODO: what are the correct size lemmas? One of them should be replacin lists with namespaces - -val v3_size = Q.prove( - `!env x v. (MEM (x,v) env ==> v_size v < v5_size env)`, - Induct \\ SRW_TAC [] [semanticPrimitivesTheory.v_size_def] - \\ SRW_TAC [] [semanticPrimitivesTheory.v_size_def] - \\ RES_TAC \\ DECIDE_TAC); - -val v2_size = Q.prove( - `!xs a. MEM a xs ==> v3_size a < v1_size xs`, +Triviality v1_size: + !vs v. (MEM v vs ==> v_size v < v1_size vs) +Proof Induct \\ SRW_TAC [] [semanticPrimitivesTheory.v_size_def] - \\ SRW_TAC [] [semanticPrimitivesTheory.v_size_def] - \\ RES_TAC \\ DECIDE_TAC); - -Theorem v_size_lemmas: - (MEM (x,y) envE ==> v_size y <= v3_size envE) /\ - (MEM (x,y) xs /\ MEM (t,xs) p1 ==> v_size y <= v2_size p1) /\ - (MEM v vs ==> v_size v < v7_size vs) -Proof - FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC - \\ IMP_RES_TAC v4_size - \\ IMP_RES_TAC v2_size - \\ IMP_RES_TAC v6_size - \\ FULL_SIMP_TAC std_ss [semanticPrimitivesTheory.v_size_def] - \\ DECIDE_TAC + \\ RES_TAC \\ DECIDE_TAC QED -*) (* introducing a module (Tmod) *) -val type_names_def = Define ` +Definition type_names_def: (type_names [] names = names) /\ (type_names (Dtype _ tds :: xs) names = type_names xs (MAP (FST o SND) tds ++ names)) /\ - (type_names (x :: xs) names = type_names xs names)`; + (type_names (x :: xs) names = type_names xs names) +End -val type_names_eq = Q.prove( - `!ds names . +Triviality type_names_eq: + !ds names . type_names ds names = (FLAT (REVERSE (MAP (\d. case d of @@ -2509,9 +2501,11 @@ val type_names_eq = Q.prove( | Dtabbrev _ tvs tn t => [] | Dlocal _ _ => [] | Denv _ => [] - | Dexn _ v10 v11 => []) ds))) ++ names`, + | Dexn _ v10 v11 => []) ds))) ++ names +Proof Induct \\ fs [type_names_def] \\ Cases_on `h` - \\ fs [type_names_def] \\ fs [FORALL_PROD,listTheory.MAP_EQ_f]); + \\ fs [type_names_def] \\ fs [FORALL_PROD,listTheory.MAP_EQ_f] +QED val lookup_APPEND = Q.prove( `!xs ys n. ~(MEM n (MAP FST ys)) ==> @@ -2828,19 +2822,21 @@ QED (* pattern match translation *) -val Mat_cases_def = Define ` +Definition Mat_cases_def: Mat_cases (INL (vars,x:exp)) = [(Pcon NONE (MAP Pvar vars),x)] /\ Mat_cases (INR ps) = MAP (\ (name,vars,x:exp,t:stamp). - (Pcon (SOME name) (MAP Pvar vars),x)) ps`; + (Pcon (SOME name) (MAP Pvar vars),x)) ps +End -val good_cons_env_def = Define ` +Definition good_cons_env_def: good_cons_env ps env <=> EVERY (\ (name,vars,x,t). ALL_DISTINCT (pats_bindings (MAP Pvar vars) []) /\ lookup_cons name env = SOME (LENGTH vars, t)) ps /\ let (name,vars,x,t1) = HD ps in - EVERY (\ (name,vars,x,t2). same_type t1 t2) ps` + EVERY (\ (name,vars,x,t2). same_type t1 t2) ps +End Theorem evaluate_match_MAP = Q.prove(` !l1 xs. @@ -2875,9 +2871,10 @@ Proof Induct \\ Cases_on `vals` \\ fs [] \\ fs [pmatch_def] QED -val write_list_def = Define ` +Definition write_list_def: write_list [] (env:v sem_env) = env /\ - write_list ((n,v)::xs) env = write_list xs (write n v env)`; + write_list ((n,v)::xs) env = write_list xs (write n v env) +End Theorem write_list_thm: !xs env. From 37bd31b41d81d7cf1f41122469b0df8d68d5f3e5 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Mon, 17 Jul 2023 15:00:56 +0800 Subject: [PATCH 08/16] emit better (?) names in bvl_to_bvi --- compiler/backend/bvl_to_bviScript.sml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/compiler/backend/bvl_to_bviScript.sml b/compiler/backend/bvl_to_bviScript.sml index 80f6e4639d..9552db9ef4 100644 --- a/compiler/backend/bvl_to_bviScript.sml +++ b/compiler/backend/bvl_to_bviScript.sml @@ -410,11 +410,13 @@ Definition get_names_def: if n = ConcatByte_location then mlstring$strlit "ConcatByte" else if n < num_stubs then mlstring$strlit "bvi_unknown" else let k = n - num_stubs in - if k MOD nss = 0 then - dtcase lookup (k DIV nss) old_names of - | NONE => mlstring$strlit "bvi_unmapped" - | SOME name => name - else mlstring$strlit "bvi_aux")) final_nums) + let kd = k DIV nss in + let km = k MOD nss in + let n = (dtcase lookup kd old_names of + | NONE => mlstring$strlit "bvi_unmapped" + | SOME name => name) in + let aux = (if km = 0 then mlstring$strlit "" else mlstring$strlit "bvi_aux") in + n ^ aux)) final_nums) End Definition compile_def: From 2f067b5c0f25081f1030fcb7d1b221714d029ad2 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Tue, 18 Jul 2023 10:35:43 +0800 Subject: [PATCH 09/16] add _ --- compiler/backend/bvl_to_bviScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/backend/bvl_to_bviScript.sml b/compiler/backend/bvl_to_bviScript.sml index 9552db9ef4..3cbeedfc77 100644 --- a/compiler/backend/bvl_to_bviScript.sml +++ b/compiler/backend/bvl_to_bviScript.sml @@ -415,7 +415,7 @@ Definition get_names_def: let n = (dtcase lookup kd old_names of | NONE => mlstring$strlit "bvi_unmapped" | SOME name => name) in - let aux = (if km = 0 then mlstring$strlit "" else mlstring$strlit "bvi_aux") in + let aux = (if km = 0 then mlstring$strlit "" else mlstring$strlit "_bvi_aux") in n ^ aux)) final_nums) End From b520d63364cd4e44583b5aa3ac90c5d9d8576bd5 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Sat, 22 Jul 2023 19:38:31 +0800 Subject: [PATCH 10/16] improve some bottleneck steps in lpr example --- basis/TextIOProgScript.sml | 12 +++--- basis/TextIOProofScript.sml | 3 +- .../lpr_checker/array/lpr_arrayProgScript.sml | 43 ++++++++++++++++--- 3 files changed, 43 insertions(+), 15 deletions(-) diff --git a/basis/TextIOProgScript.sml b/basis/TextIOProgScript.sml index 85ffb2d203..5f218a8673 100644 --- a/basis/TextIOProgScript.sml +++ b/basis/TextIOProgScript.sml @@ -516,12 +516,12 @@ val _ = (append_prog o process_topdecs)` val _ = (append_prog o process_topdecs)` fun b_input1_aux is = case is of InstreamBuffered fd rref wref surplus => - if (!wref) = (!rref) then None - else - let val readat = (!rref) in - rref := (!rref) + 1; - Char.some (Char.fromByte (Word8Array.sub surplus readat)) - end`; + let val readat = (!rref) in + if (!wref) = readat then None + else + (rref := readat + 1; + Char.some (Char.fromByte (Word8Array.sub surplus readat))) + end`; val _ = ml_prog_update open_local_in_block; diff --git a/basis/TextIOProofScript.sml b/basis/TextIOProofScript.sml index d5d44d72ef..29ba1deaa1 100644 --- a/basis/TextIOProofScript.sml +++ b/basis/TextIOProofScript.sml @@ -2466,9 +2466,8 @@ Proof \\ rw[] >-(xsimpl \\ fs[std_preludeTheory.OPTION_TYPE_def])) >-(simp[INSTREAM_BUFFERED_BL_FD_RW_def, REF_NUM_def] \\ xpull + \\ gvs[] \\ xlet_auto >- xsimpl - \\ rveq \\ xlet_auto >- xsimpl - \\ rveq \\ xlet_auto >- xsimpl \\ xlet_auto >- xsimpl \\ xlet_auto >- (xsimpl \\ fs[instream_buffered_inv_def]) \\ xlet_auto >- xsimpl \\ fs [CharProgTheory.fromByte_def] diff --git a/examples/lpr_checker/array/lpr_arrayProgScript.sml b/examples/lpr_checker/array/lpr_arrayProgScript.sml index 7e40460085..d808e6bc3f 100644 --- a/examples/lpr_checker/array/lpr_arrayProgScript.sml +++ b/examples/lpr_checker/array/lpr_arrayProgScript.sml @@ -2227,20 +2227,34 @@ open mlintTheory; (* TODO: Mostly copied from mlintTheory *) val result = translate fromChar_unsafe_def; -val fromChars_range_unsafe_tail_def = Define` - fromChars_range_unsafe_tail l 0 str mul acc = acc ∧ - fromChars_range_unsafe_tail l (SUC n) str mul acc = - fromChars_range_unsafe_tail l n str (mul * 10) (acc + fromChar_unsafe (strsub str (l + n)) * mul)`; +Definition fromChars_range_unsafe_tail_def: + fromChars_range_unsafe_tail b n str mul acc = + if n ≤ b then acc + else + let m = sub_nocheck n 1 in + fromChars_range_unsafe_tail b m str (mul * 10) + (acc + fromChar_unsafe (strsub str m) * mul) +Termination + WF_REL_TAC`measure (λ(b,n,_). n)`>> + rw[sub_nocheck_def] +End Theorem fromChars_range_unsafe_tail_eq: ∀n l s mul acc. - fromChars_range_unsafe_tail l n s mul acc = (fromChars_range_unsafe l n s) * mul + acc + fromChars_range_unsafe_tail l (n+l) s mul acc = + (fromChars_range_unsafe l n s) * mul + acc Proof - Induct>>rw[fromChars_range_unsafe_tail_def,fromChars_range_unsafe_def] + Induct + >- + rw[Once fromChars_range_unsafe_tail_def,fromChars_range_unsafe_def]>> + rw[]>> + simp[Once fromChars_range_unsafe_tail_def,ADD1,fromChars_range_unsafe_def,sub_nocheck_def]>> + fs[ADD1] QED Theorem fromChars_range_unsafe_alt: - fromChars_range_unsafe l n s = fromChars_range_unsafe_tail l n s 1 0 + fromChars_range_unsafe l n s = + fromChars_range_unsafe_tail l (n+l) s 1 0 Proof rw[fromChars_range_unsafe_tail_eq] QED @@ -2272,6 +2286,21 @@ val result = translate lpr_parsingTheory.fromString_unsafe_def; val fromstring_unsafe_side_def = definition"fromstring_unsafe_side_def"; val fromchars_unsafe_side_def = theorem"fromchars_unsafe_side_def"; val fromchars_range_unsafe_tail_side_def = theorem"fromchars_range_unsafe_tail_side_def"; + +Theorem fromchars_range_unsafe_tail_side_def: + ∀a1 a0 a2 a3 a4. + fromchars_range_unsafe_tail_side a0 a1 a2 a3 a4 ⇔ + ¬(a1 ≤ a0) ⇒ + (T ∧ a1 < 1 + strlen a2 ∧ 0 < strlen a2) ∧ + fromchars_range_unsafe_tail_side a0 (a1 − 1) a2 (a3 * 10) + (a4 + fromChar_unsafe (strsub a2 (a1 − 1)) * a3) +Proof + Induct>> + rw[Once fromchars_range_unsafe_tail_side_def]>> + simp[sub_nocheck_def]>>eq_tac>>rw[ADD1]>> + gvs[] +QED + val fromchars_range_unsafe_side_def = fetch "-" "fromchars_range_unsafe_side_def"; Theorem fromchars_unsafe_side_thm: From ca07d6427957afd7b0999b882cf1bd3ab76b9b42 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Mon, 31 Jul 2023 10:25:20 +1000 Subject: [PATCH 11/16] Fix errors caused by HOL deleting various quotient_*Theory --- candle/overloading/syntax/holSyntaxExtraScript.sml | 2 +- compiler/backend/proofs/backendProofScript.sml | 4 ++-- compiler/backend/proofs/bvi_tailrecProofScript.sml | 4 ++-- compiler/backend/proofs/clos_annotateProofScript.sml | 4 ++-- compiler/backend/proofs/flat_patternProofScript.sml | 3 --- compiler/backend/proofs/source_evalProofScript.sml | 11 +++++------ compiler/inference/proofs/inferPropsScript.sml | 4 ++-- 7 files changed, 14 insertions(+), 18 deletions(-) diff --git a/candle/overloading/syntax/holSyntaxExtraScript.sml b/candle/overloading/syntax/holSyntaxExtraScript.sml index b1d5d38d69..e5d9876e3c 100644 --- a/candle/overloading/syntax/holSyntaxExtraScript.sml +++ b/candle/overloading/syntax/holSyntaxExtraScript.sml @@ -6865,7 +6865,7 @@ Proof `!l ty1 ty2. equal_upto l ty1 ty2 ==> l = [] ==> ty1 = ty2` suffices_by metis_tac[] \\ ho_match_mp_tac equal_upto_ind \\ fs[] - \\ CONV_TAC(DEPTH_CONV ETA_CONV) \\ fs[quotient_listTheory.LIST_REL_EQ] + \\ CONV_TAC(DEPTH_CONV ETA_CONV) \\ fs[] QED diff --git a/compiler/backend/proofs/backendProofScript.sml b/compiler/backend/proofs/backendProofScript.sml index a492791fd7..417ff48a4b 100644 --- a/compiler/backend/proofs/backendProofScript.sml +++ b/compiler/backend/proofs/backendProofScript.sml @@ -485,8 +485,8 @@ Proof simp [keep_progs_def, FUN_EQ_THM] QED -Triviality compile_inc_progs_defs = LIST_CONJ - [compile_inc_progs_def, keep_progs_T, quotient_pairTheory.PAIR_MAP_I] +Triviality compile_inc_progs_defs = + LIST_CONJ [compile_inc_progs_def, keep_progs_T] Theorem cake_orac_eqs: state_co (\c (env_id, decs). inc_compile env_id c diff --git a/compiler/backend/proofs/bvi_tailrecProofScript.sml b/compiler/backend/proofs/bvi_tailrecProofScript.sml index 3dc98cf9e4..2fb9e78900 100644 --- a/compiler/backend/proofs/bvi_tailrecProofScript.sml +++ b/compiler/backend/proofs/bvi_tailrecProofScript.sml @@ -1070,7 +1070,7 @@ Proof \\ fs[state_rel_def] ) \\ imp_res_tac state_rel_const \\ fs[case_eq_thms] - \\ rveq \\ fs[OPTREL_def,quotient_pairTheory.PAIR_REL_THM] + \\ rveq \\ fs[OPTREL_def,PAIR_REL_THM] \\ fs[state_rel_def] QED @@ -1087,7 +1087,7 @@ Proof \\ first_x_assum(qspec_then`vs`strip_assume_tac) \\ fs[case_eq_thms,OPTREL_def] \\ rw[] \\ rfs[] \\ fs[PULL_EXISTS] - \\ rveq \\ fs[quotient_pairTheory.PAIR_REL] + \\ rveq \\ fs[PAIR_REL] \\ TRY(pairarg_tac \\ fs[]) \\ imp_res_tac state_rel_const \\ fs[bvlSemTheory.do_app_def,case_eq_thms,bvl_to_bvi_id] diff --git a/compiler/backend/proofs/clos_annotateProofScript.sml b/compiler/backend/proofs/clos_annotateProofScript.sml index 001d2ac72f..1634556f91 100644 --- a/compiler/backend/proofs/clos_annotateProofScript.sml +++ b/compiler/backend/proofs/clos_annotateProofScript.sml @@ -386,7 +386,7 @@ Proof \\ imp_res_tac v_to_list \\ fs[] \\ rw[] \\ TRY (strip_tac \\ rw[]) \\ fs[EVERY2_MAP,v_rel_Number] - \\ fsrw_tac[ETA_ss][EQ_SYM_EQ,quotient_listTheory.LIST_REL_EQ] + \\ fsrw_tac[ETA_ss][EQ_SYM_EQ] \\ fs[LIST_EQ_REWRITE,EL_MAP,LIST_REL_EL_EQN] \\ rfs[EL_MAP] \\ METIS_TAC[EL_MAP,o_DEF] QED @@ -401,7 +401,7 @@ Proof \\ imp_res_tac v_to_list \\ fs[] \\ rw[] \\ TRY (strip_tac \\ rw[]) \\ fs[EVERY2_MAP,v_rel_Number] - \\ fsrw_tac[ETA_ss][EQ_SYM_EQ,quotient_listTheory.LIST_REL_EQ] + \\ fsrw_tac[ETA_ss][EQ_SYM_EQ] \\ fs[LIST_EQ_REWRITE,EL_MAP,LIST_REL_EL_EQN] \\ rfs[EL_MAP] \\ METIS_TAC[EL_MAP,o_DEF] QED diff --git a/compiler/backend/proofs/flat_patternProofScript.sml b/compiler/backend/proofs/flat_patternProofScript.sml index 65e69f85e9..28e7ff284b 100644 --- a/compiler/backend/proofs/flat_patternProofScript.sml +++ b/compiler/backend/proofs/flat_patternProofScript.sml @@ -685,9 +685,6 @@ Theorem v_rel_l_cases = TypeBase.nchotomy_of ``: v`` val env_rel_def = ``env_rel N env1 env2`` |> SIMP_CONV bool_ss [v_rel_cases] -val add_q = augment_srw_ss [simpLib.named_rewrites "pair_rel_thm" - [quotient_pairTheory.PAIR_REL_THM]]; - Definition install_conf_rel_def: install_conf_rel pat_cfg ic1 ic2 <=> (ic2.compile_oracle = diff --git a/compiler/backend/proofs/source_evalProofScript.sml b/compiler/backend/proofs/source_evalProofScript.sml index 73a0a5ceb3..d56fba7045 100644 --- a/compiler/backend/proofs/source_evalProofScript.sml +++ b/compiler/backend/proofs/source_evalProofScript.sml @@ -126,7 +126,7 @@ Proof Induct \\ simp [FORALL_PROD, EXISTS_PROD] \\ rw [] - \\ fs [namespaceTheory.nsBindList_def, quotient_pairTheory.PAIR_REL_THM] + \\ fs [namespaceTheory.nsBindList_def] \\ irule env_rel_add_nsBind \\ simp [] QED @@ -428,8 +428,7 @@ Theorem pmatch: Proof disch_tac \\ ho_match_mp_tac pmatch_ind - \\ rw [pmatch_def, match_result_rel_def, - quotient_pairTheory.PAIR_REL_THM] + \\ rw [pmatch_def, match_result_rel_def] \\ rveq \\ fs [] \\ imp_res_tac v_to_env_id_SOME \\ fs [pmatch_def] @@ -1010,7 +1009,7 @@ Proof \\ simp [build_rec_env_merge, nsAppend_to_nsBindList] \\ irule env_rel_add_nsBindList \\ simp [LIST_REL_MAP1, SIMP_RULE (bool_ss ++ ETA_ss) [] LIST_REL_MAP2] - \\ simp [ELIM_UNCURRY, quotient_pairTheory.PAIR_REL_THM, EVERY2_refl] + \\ simp [ELIM_UNCURRY, EVERY2_refl] ) >~ [‘getOpClass op = Icing’] >- ( @@ -1141,7 +1140,7 @@ Proof \\ simp [build_rec_env_merge, nsAppend_to_nsBindList] \\ irule env_rel_add_nsBindList \\ simp [LIST_REL_MAP1, SIMP_RULE (bool_ss ++ ETA_ss) [] LIST_REL_MAP2] - \\ simp [quotient_pairTheory.PAIR_REL_THM, ELIM_UNCURRY] + \\ simp [ELIM_UNCURRY] \\ simp [GSYM pairarg_to_pair_map, ELIM_UNCURRY, EVERY2_refl] QED @@ -1198,7 +1197,7 @@ Proof \\ irule env_rel_add_nsBindList \\ simp [] \\ simp [LIST_REL_MAP1, SIMP_RULE (bool_ss ++ ETA_ss) [] LIST_REL_MAP2] - \\ simp [quotient_pairTheory.PAIR_REL_THM, ELIM_UNCURRY] + \\ simp [ELIM_UNCURRY] \\ simp [EVERY2_refl] QED diff --git a/compiler/inference/proofs/inferPropsScript.sml b/compiler/inference/proofs/inferPropsScript.sml index 4dcb02a1cf..9743b5bc32 100644 --- a/compiler/inference/proofs/inferPropsScript.sml +++ b/compiler/inference/proofs/inferPropsScript.sml @@ -4081,7 +4081,7 @@ Proof match_mp_tac nsAll_alist_to_ns \\ simp[EVERY_MAP,every_zip_snd] \\ imp_res_tac generalise_inf_set_tids - \\ fs[GSYM LIST_REL_MAP_inv_image, quotient_listTheory.LIST_REL_EQ] + \\ fs[GSYM LIST_REL_MAP_inv_image] \\ simp[GSYM (Q.ISPEC`inf_set_tids`(CONV_RULE SWAP_FORALL_CONV EVERY_MAP))] \\ pop_assum(assume_tac o SYM) \\ simp[] @@ -4120,7 +4120,7 @@ Proof \\ simp[MAP2_MAP, UNCURRY, EVERY_MAP] \\ simp[every_zip_snd] \\ imp_res_tac generalise_inf_set_tids - \\ fs[GSYM LIST_REL_MAP_inv_image, quotient_listTheory.LIST_REL_EQ] + \\ fs[GSYM LIST_REL_MAP_inv_image] \\ simp[GSYM (Q.ISPEC`inf_set_tids`(CONV_RULE SWAP_FORALL_CONV EVERY_MAP))] \\ pop_assum(assume_tac o SYM) \\ simp[] From 29e25c94bcd7c93354293f7f2f084717b62eb204 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 3 Aug 2023 23:39:49 +0200 Subject: [PATCH 12/16] Fix backendProof for explorer reorg --- compiler/backend/proofs/backendProofScript.sml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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 []) From 05f3824af99a8801277b84b82d17ad26ba928932 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sun, 6 Aug 2023 10:25:11 +0200 Subject: [PATCH 13/16] Update bootstrap translation for new --explore --- .../translation/compiler32ProgScript.sml | 66 ++++++++------ .../translation/compiler64ProgScript.sml | 71 +++++++++------ .../translation/explorerProgScript.sml | 89 +++++++++++-------- .../translation/to_target32ProgScript.sml | 12 +++ .../translation/to_target64ProgScript.sml | 12 +++ .../translation/to_word32ProgScript.sml | 35 +++++--- .../translation/to_word64ProgScript.sml | 36 +++++--- 7 files changed, 208 insertions(+), 113 deletions(-) diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml index a4572fd76e..7b101ed9ed 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)); diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml index fb6ced0e2a..203217e396 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)); 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; From 118cbe66d0af38057592f9540fac6f5834e4c5d3 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sun, 6 Aug 2023 14:37:15 +0200 Subject: [PATCH 14/16] Fix some breakage --- compiler/bootstrap/translation/compiler32ProgScript.sml | 1 - compiler/bootstrap/translation/compiler64ProgScript.sml | 1 - compiler/proofs/compilerProofScript.sml | 5 +++-- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml index 7b101ed9ed..12687f3ef1 100644 --- a/compiler/bootstrap/translation/compiler32ProgScript.sml +++ b/compiler/bootstrap/translation/compiler32ProgScript.sml @@ -249,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 203217e396..521255201a 100644 --- a/compiler/bootstrap/translation/compiler64ProgScript.sml +++ b/compiler/bootstrap/translation/compiler64ProgScript.sml @@ -268,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/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: From de787171f1c2ef362fff6762e464a6496de600ed Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 7 Aug 2023 23:21:17 +0200 Subject: [PATCH 15/16] Fix for tap_config_enc' evaluation --- .../bootstrap/compilation/x64/64/x64_config_encScript.sml | 8 ++++++++ 1 file changed, 8 insertions(+) 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 = From 409796dab83156a6e6c32f0f15c3f141d94150df Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 8 Aug 2023 15:40:24 +0200 Subject: [PATCH 16/16] Make explorer output neater --- compiler/backend/presLangScript.sml | 123 +++++++++++++++++----------- 1 file changed, 77 insertions(+), 46 deletions(-) diff --git a/compiler/backend/presLangScript.sml b/compiler/backend/presLangScript.sml index 440c579ecc..98e37b3253 100644 --- a/compiler/backend/presLangScript.sml +++ b/compiler/backend/presLangScript.sml @@ -71,9 +71,12 @@ Proof \\ (PURE_CASE_TAC \\ simp[ASCIInumbersTheory.n2s_def]) QED +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 (implode ("0x" ++ num_to_hex (w2n w))) + word_to_display w = empty_item (num_to_hex_mlstring (w2n w)) End Definition item_with_word_def: @@ -856,8 +859,10 @@ End (* dataLang *) Definition num_set_to_display_def: - num_set_to_display ns = Tuple (MAP num_to_display - (MAP FST (sptree$toSortedAList ns))) + num_set_to_display ns = + String $ concat [strlit "{"; + commas (MAP toString (MAP FST (sptree$toSortedAList ns))); + strlit "}"] End Definition data_seqs_def: @@ -1064,42 +1069,43 @@ QED 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) = - Item NONE «get» [num_to_display n; store_name_to_display sn] ∧ - stack_prog_to_display ns (Set sn n) = - Item NONE «set» [store_name_to_display sn; - num_to_display n] ∧ - stack_prog_to_display ns (OpCurrHeap b n1 n2) = - Item NONE «op_curr_heap» - [asm_binop_to_display b; num_to_display n1; num_to_display n2] ∧ + 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 «return» + 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 + | INL l => Item NONE «direct» [String (attach_name ns (SOME l))] | INR r => item_with_num «reg» r); (case eh of - | NONE => empty_item «no_handle» + | NONE => empty_item «no_handler» | SOME (p,l1,l2) => - Item NONE «handle» - [num_to_display l1; num_to_display l2; stack_prog_to_display ns p])] ∧ + 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» - [asm_cmp_to_display c; num_to_display n; - asm_reg_imm_to_display to; stack_prog_to_display ns x; + [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» - [asm_cmp_to_display c; num_to_display n; - asm_reg_imm_to_display to; stack_prog_to_display ns x] ∧ + [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 ∧ @@ -1123,13 +1129,25 @@ Definition stack_prog_to_display_def: 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) = item_with_nums «stack_store» [n; m] ∧ - stack_prog_to_display ns (StackStoreAny n m) = item_with_nums «stack_store_any» [n; m] ∧ - stack_prog_to_display ns (StackLoad n m) = item_with_nums «stack_load» [n; m] ∧ - stack_prog_to_display ns (StackLoadAny n m) = item_with_nums «stack_load_any» [n; m] ∧ + 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) = item_with_nums «bitmap_load» [n; m] ∧ + 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’ @@ -1210,7 +1228,7 @@ Definition word_exp_to_display_def: (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)) /\ @@ -1237,18 +1255,22 @@ 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; num_to_display n2]) mvs)]) /\ + [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) = - Item NONE (strlit "assign") - [num_to_display n; word_exp_to_display exp]) /\ - (word_prog_to_display ns (Get n sn) = Item NONE (strlit "get") - [num_to_display n; store_name_to_display sn]) /\ - (word_prog_to_display ns (Set sn exp) = Item NONE (strlit "set") - [store_name_to_display sn; word_exp_to_display exp]) /\ - (word_prog_to_display ns (Store exp n) = Item NONE (strlit "store") - [word_exp_to_display exp; num_to_display n]) /\ + 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") @@ -1256,13 +1278,18 @@ Definition word_prog_to_display_def: 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) = Item NONE «op_curr_heap» - [asm_binop_to_display b; num_to_display n1; num_to_display n2]) /\ + (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") - [word_prog_to_display ns p1; word_prog_to_display ns p2]) /\ + (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") @@ -1286,14 +1313,18 @@ Definition word_prog_to_display_def: (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 "none")) /\ + (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 "some") [Tuple [num_to_display n1; num_set_to_display ms; - word_prog_to_display ns prog; num_to_display n2; num_to_display n3]]) /\ - (word_prog_to_display_handler ns NONE = empty_item (strlit "none")) /\ + 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 "some") [Tuple [num_to_display n1; - word_prog_to_display ns prog; num_to_display n2; num_to_display 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