Merge remote-tracking branch 'origin/infcomp3' into bool_unit_datatypes

want the latest inferencer before updating the inferencer proofs

bootstrap/proofs/bootstrapProofScript.sml

@@ -167,6 +167,17 @@ val COMPILER_RUN_INV_empty_stack = store_thm("COMPILER_RUN_INV_empty_stack",
   Cases_on`Tmod_state "REPL" replModule_decls`>>
   fs[update_io_def,compilerProofTheory.env_rs_def])
 
+val COMPILER_RUN_INV_handler = store_thm("COMPILER_RUN_INV_handler",
+  ``COMPILER_RUN_INV bs1 grd1 inp1 out1 ==>
+    (bs1.handler = 0)``,
+  rw[COMPILER_RUN_INV_def] >> PairCases_on`grd1` >>
+  Cases_on`Tmod_state "REPL" replModule_decls`>>
+  fs[evaluateReplTheory.update_io_def,compilerProofTheory.env_rs_def]);
+
+val LUPDATE_SAME_lem = prove(
+  ``∀ls n v. (v = EL n ls) ∧ n < LENGTH ls ⇒ LUPDATE v n ls = ls``,
+  metis_tac[miscTheory.LUPDATE_SAME])
+
 val COMPILER_RUN_INV_init = store_thm("COMPILER_RUN_INV_init",
   ``COMPILER_RUN_INV repl_bc_state bootstrap_grd
        (dest_Refv (EL iloc (SND (Tmod_state "REPL" replModule_decls))))
@@ -175,16 +186,15 @@ val COMPILER_RUN_INV_init = store_thm("COMPILER_RUN_INV_init",
     Cases_on`Tmod_state "REPL" replModule_decls` >>
     simp[update_io_def] >>
     strip_assume_tac repl_env_def >> rfs[] >>
-    Cases_on`EL iloc r`>>fs[]>>Cases_on`EL (iloc+1) r`>>fs[]>>
-    ntac 2 (pop_assum (mp_tac o SYM)) >>
-    simp[miscTheory.LUPDATE_SAME] >> rw[] >>
+    simp[LUPDATE_SAME_lem] >>
     strip_assume_tac bootstrap_bc_state_def >>
     MATCH_MP_TAC env_rs_with_bs_irr >>
     qexists_tac`bootstrap_bc_state with code := bootstrap_bc_state.code ++ REVERSE compile_call_repl_step` >>
     simp[initCompEnvTheory.install_code_def] >>
     rfs[]  >>
     MATCH_MP_TAC env_rs_append_code >>
-    rfs[] >> first_assum(match_exists_tac o concl) >> simp[] >>
+    rfs[] >>
+    first_assum(match_exists_tac o concl) >> simp[] >>
     simp[bytecodeTheory.bc_state_component_equality] >>
     simp[compilerTheory.compiler_state_component_equality] >>
     `∃x y z. bootstrap_grd = (x,y,z)` by metis_tac[pair_CASES] >>
@@ -731,10 +741,20 @@ val COMPILER_RUN_INV_ptrs = store_thm("COMPILER_RUN_INV_ptrs",
   ``∀bs grd inp out.
       COMPILER_RUN_INV bs grd inp out ⇒
       EL ^(rhs(concl iind_eq)) bs.globals = SOME (RefPtr iptr) ∧
-      EL ^(rhs(concl oind_eq)) bs.globals = SOME (RefPtr optr)``,
+      ^(rhs(concl iind_eq)) < LENGTH bs.globals ∧
+      EL ^(rhs(concl oind_eq)) bs.globals = SOME (RefPtr optr) ∧
+      ^(rhs(concl oind_eq)) < LENGTH bs.globals``,
   rw[COMPILER_RUN_INV_def,GSYM iind_eq,GSYM oind_eq] >>
   rw[ptrs_def])
 
+(* initial value of input reference *)
+
+val INPUT_TYPE_NONE = store_thm("INPUT_TYPE_NONE",
+  ``INPUT_TYPE NONE
+      (dest_Refv (EL iloc (SND (Tmod_state "REPL" replModule_decls))))``,
+  simp[INPUT_TYPE_def,OPTION_TYPE_def] >>
+  simp[repl_env_def])
+
 (* Changing the references preserves the invariant *)
 
 fun just_exists_suff_tac th (g as (_,w)) =

bootstrap/translation/repl/evaluateReplScript.sml

@@ -38,11 +38,58 @@ val append_3 = save_thm("append_3",
   |> UNDISCH |> SYM |> REWRITE_RULE[last_3_decs]
   |> prove_hyps_by(CONV_TAC(computeLib.CBV_CONV repl_decs_cs)))
 
+val evaluate_dec_tys_NONE = prove(
+  ``∀dec ck mn env s s' tys c tds tvs tn cts cn as.
+    evaluate_dec ck (SOME mn) env s dec (s',Rval (tys,c)) ∧
+    ¬MEM cn (ctors_of_dec dec)
+    ⇒
+    (ALOOKUP tys cn = NONE)``,
+  Induct >> rw[Once evaluate_dec_cases] >>
+  simp[alistTheory.ALOOKUP_def] >>
+  simp[alistTheory.ALOOKUP_FAILS] >>
+  simp[semanticPrimitivesTheory.build_tdefs_def] >>
+  fs[MEM_FLAT,MEM_MAP,pairTheory.EXISTS_PROD,pairTheory.FORALL_PROD,PULL_EXISTS])
+
+val evaluate_decs_tys_NONE = prove(
+  ``∀decs ck mn env s s' tys c tds tvs tn cts cn as.
+    evaluate_decs ck (SOME mn) env s decs (s',tys,Rval c) ∧
+    ¬MEM cn (FLAT (MAP ctors_of_dec decs))
+    ⇒
+    (ALOOKUP tys cn = NONE)``,
+  Induct >> rw[Once evaluate_decs_cases] >>
+  simp[alistTheory.ALOOKUP_APPEND] >>
+  Cases_on`r`>>fs[semanticPrimitivesTheory.combine_dec_result_def] >>
+  first_x_assum(fn th => first_x_assum(mp_tac o MATCH_MP (ONCE_REWRITE_RULE[GSYM AND_IMP_INTRO] th))) >>
+  disch_then(fn th => first_x_assum(mp_tac o MATCH_MP (ONCE_REWRITE_RULE[GSYM AND_IMP_INTRO] th))) >> simp[] >>
+  imp_res_tac evaluate_dec_tys_NONE >> simp[])
+
+val evaluate_Tmod_tys_NONE = store_thm("evaluate_Tmod_tys_NONE",
+  ``evaluate_top F env s (Tmod mn NONE decs) (s',([(m,tys)],e),Rval r) ⇒
+    ¬MEM cn (FLAT (MAP ctors_of_dec decs))
+    ⇒
+    (ALOOKUP tys cn = NONE)``,
+  rw[evaluate_top_cases,miscTheory.FEMPTY_FUPDATE_EQ] >>
+  METIS_TAC[evaluate_decs_tys_NONE]) |> GEN_ALL
+
+val ALOOKUP_NONE_lemma =
+  MATCH_MP evaluate_Tmod_tys_NONE (CONJUNCT1 evaluate_replModule)
+  |> Q.SPEC`"NONE"`
+  |> CONV_RULE(LAND_CONV (computeLib.CBV_CONV repl_decs_cs THENC EVAL))
+  |> C MP TRUTH
+
+val build_conv_lemma =
+  ``build_conv (merge_alist_mod_env ([],Tmod_tys "REPL" replModule_decls)
+      (THE prim_sem_env).sem_envC) (SOME (Short "NONE")) []``
+  |> ((REWRITE_CONV[initSemEnvTheory.prim_sem_env_eq]) THENC EVAL)
+  |> SIMP_RULE std_ss [alistTheory.ALOOKUP_APPEND,alistTheory.ALOOKUP_def,ALOOKUP_NONE_lemma]
+  |> CONV_RULE(RAND_CONV EVAL)
+
 val iloc_repl_env_exist =
   MATCH_MP evalPropsTheory.evaluate_Tmod_last3 (CONJUNCT1 evaluate_replModule)
   |> SIMP_RULE (srw_ss())[]
   |> C MATCH_MP append_3
-  |> REWRITE_RULE[GSYM append_3]
+  |> REWRITE_RULE[GSYM append_3,build_conv_lemma]
+  |> SIMP_RULE std_ss []
 
 val repl_env_def = new_specification("repl_env_def",["iloc","repl_env"],iloc_repl_env_exist)
 

bytecode/bytecodeExtraScript.sml

@@ -18,12 +18,12 @@ val real_inst_length_def = zDefine `
    | Stack (TagEq v33) => if v33 < 268435456 then 28 else 1
    | Stack IsBlock => 25
    | Stack Equal => 5
-   | Stack Add => 3
-   | Stack Sub => 3
+   | Stack Add => 8
+   | Stack Sub => 11
    | Stack Mult => 8
-   | Stack Div => 20
-   | Stack Mod => 23
-   | Stack Less => 24
+   | Stack Div => 11
+   | Stack Mod => 11
+   | Stack Less => 13
    | Label l => 0
    | Jump (Lab l') => 2
    | Jump (Addr v37) => 2
@@ -42,12 +42,12 @@ val real_inst_length_def = zDefine `
    | Update => 6
    | Length => 3
    | LengthByte => 5
-   | Galloc v17 => 1
    | Gupdate v18 => if v18 < 10000 then 19 else 1
    | Gread v19 => if v19 < 10000 then 16 else 1
    | Stop v20 => 9
    | Tick => 1
    | Print => 5
+   | PrintWord8 => 1
    | PrintC v21 => 33
    | _ => 1:num`;
 
@@ -479,7 +479,7 @@ val good_labels_def = Define`
 val code_executes_ok_def = Define `
   code_executes_ok s1 ⇔
       (* termination *)
-      (?s2 b. bc_next^* s1 s2 /\ bc_fetch s2 = SOME (Stop b)) \/
+      (?s2 b. bc_next^* s1 s2 /\ bc_fetch s2 = SOME (Stop b) /\ s2.stack = [] /\ s2.handler = 0) \/
       (* or divergence with no output *)
       !n. ?s2. NRC bc_next n s1 s2 /\ (s2.output = s1.output)`;
 

bytecode/bytecodeLabelsScript.sml

@@ -557,6 +557,14 @@ val code_labels_no_labels = store_thm("code_labels_no_labels",
 
 open bytecodeExtraTheory
 
+val strip_labels_handler = store_thm("strip_labels_handler",
+  ``(strip_labels s).handler = s.handler``,
+  rw[strip_labels_def])
+
+val strip_labels_stack = store_thm("strip_labels_stack",
+  ``(strip_labels s).stack = s.stack``,
+  rw[strip_labels_def])
+
 val code_executes_ok_strip_labels = store_thm("code_executes_ok_strip_labels",
   ``code_executes_ok bs1 /\ length_ok bs1.inst_length ==>
     code_executes_ok (strip_labels bs1)``,
@@ -566,7 +574,7 @@ val code_executes_ok_strip_labels = store_thm("code_executes_ok_strip_labels",
     \\ IMP_RES_TAC bc_next_strip_labels_RTC
     \\ FULL_SIMP_TAC std_ss []
     \\ IMP_RES_TAC RTC_bc_next_preserves
-    \\ METIS_TAC [bc_fetch_strip_labels])
+    \\ METIS_TAC [bc_fetch_strip_labels,strip_labels_handler,strip_labels_stack])
   \\ DISJ2_TAC \\ REPEAT GEN_TAC
   \\ POP_ASSUM MP_TAC
   \\ POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`n`]) \\ STRIP_TAC

compiler/proofs/compilerProofScript.sml

@@ -1226,6 +1226,7 @@ val env_rs_def = Define`
     contains_primitives bs.code ∧
     rs.next_global = LENGTH genv ∧
     bs.stack = [] ∧
+    bs.handler = 0 ∧
     EVERY (sv_every closed) s ∧
     EVERY closed (MAP SND envE) ∧
     EVERY closed (MAP SND (FLAT (MAP SND envM))) ∧
@@ -1315,6 +1316,7 @@ val env_rs_with_bs_irr = store_thm("env_rs_with_bs_irr",
     env_rs env cs grd rs bs
     ∧ bs'.globals = bs.globals
     ∧ bs'.stack = bs.stack
+    ∧ bs'.handler = bs.handler
     ∧ bs'.refs = bs.refs
     ∧ bs'.clock = bs.clock
     ∧ bs'.code = bs.code
@@ -2095,6 +2097,7 @@ val compile_top_thm = store_thm("compile_top_thm",
       simp[to_i2_invariant_def] >> strip_tac >>
       imp_res_tac EVERY2_LENGTH >> rfs[] ) >>
     conj_tac >- simp[Abbr`bs2`] >>
+    conj_tac >- simp[Abbr`bs2`] >>
     ONCE_REWRITE_TAC[CONJ_ASSOC] >>
     conj_tac >- (
       first_x_assum(mp_tac o MATCH_MP evaluate_dec_closed) >>
@@ -2312,6 +2315,7 @@ val compile_top_thm = store_thm("compile_top_thm",
       simp[to_i2_invariant_def] >> strip_tac >>
       imp_res_tac EVERY2_LENGTH >> rfs[] ) >>
     conj_tac >- simp[Abbr`bs2`] >>
+    conj_tac >- simp[Abbr`bs2`] >>
     ONCE_REWRITE_TAC[CONJ_ASSOC] >>
     conj_tac >- (
       simp[EVERY_APPEND] >>
@@ -2538,6 +2542,7 @@ val compile_top_thm = store_thm("compile_top_thm",
       simp[to_i2_invariant_def] >> strip_tac >>
       imp_res_tac EVERY2_LENGTH >> rfs[] ) >>
     conj_tac >- simp[Abbr`bs2`] >>
+    conj_tac >- simp[Abbr`bs2`] >>
     ONCE_REWRITE_TAC[CONJ_ASSOC] >>
     conj_tac >- (
       first_x_assum(mp_tac o MATCH_MP evaluate_decs_closed) >>
@@ -2739,6 +2744,7 @@ val compile_top_thm = store_thm("compile_top_thm",
       simp[to_i2_invariant_def] >> strip_tac >>
       imp_res_tac EVERY2_LENGTH >> rfs[] ) >>
     conj_tac >- simp[Abbr`bs2`] >>
+    conj_tac >- simp[Abbr`bs2`] >>
     ONCE_REWRITE_TAC[CONJ_ASSOC] >>
     conj_tac >- (
       simp[EVERY_APPEND] >>

explorer/pp/Holmakefile

@@ -1,4 +1,4 @@
-INCLUDES = ../.. $(HOLDIR)/examples/l3-machine-code/x64/model $(HOLDIR)/examples/parsing ../../parsing ../../compiler ../../inference ../../semantics ../../initial ../../bytecode ./astPP ../../x86-64 ../../standalone ./astPP
+INCLUDES = ../.. $(HOLDIR)/examples/l3-machine-code/x64/model $(HOLDIR)/examples/parsing ../../parsing ../../compiler ../../inference ../../semantics ../../initial ../../bytecode ./astPP ../../x86-64/compile ../../standalone ./astPP
 
 OPTIONS = QUIT_ON_FAILURE
 
@@ -11,7 +11,7 @@ TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
 all: $(TARGETS) $(HOLHEAP)
 .PHONY: all
 
-BARE_THYS =  $(HOLDIR)/examples/l3-machine-code/x64/model/x64DisassembleLib $(HOLDIR)/examples/parsing/pegexecTheory ../../compiler/free_varsTheory ./astPP/astPP ../../x86-64/x64_code_evalTheory ../../x86-64/x64_heapTheory
+BARE_THYS =  $(HOLDIR)/examples/l3-machine-code/x64/model/x64DisassembleLib $(HOLDIR)/examples/parsing/pegexecTheory ../../compiler/free_varsTheory ./astPP/astPP ../../x86-64/compile/bc_compileTheory
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 

explorer/pp/allPP.sml

@@ -46,7 +46,7 @@ in
 exception compilationError of string;
 type allIntermediates = {
   ils:term list,
-  globMap:term list, 
+  globMap:term list,
   ctors:term list,
   modMap:term list,
   annotations:term list}
@@ -56,13 +56,13 @@ fun allIntermediates prog =
   let
       val t1 = eval ``get_all_asts ^(prog)``
       val ast = rand (rhsThm t1)
-      
+
       val _ =if ast = ``"<parse error>\n"`` then raise compilationError "Parse Error" else ();
 
       val infer = eval ``infer_all_asts ^(t1|>concl|>rhs)``
       val infer_res = rhsThm infer;
       (*Bypass type checks -- dangerous!*)
-      val _ = let val (res,msg) = dest_comb infer_res in 
+      val _ = let val (res,msg) = dest_comb infer_res in
                 if (term_to_string res) = "Failure" then raise compilationError ("Type Inference Error: "^(term_to_string msg)) else () end;
 
       (*i1 translation*)
@@ -105,10 +105,10 @@ fun allIntermediates prog =
 
       (*compileCexp*)
       val cs = rhsThm (eval ``<|out:=[];next_label:=compile_primitives.rnext_label|>``);
-      
+
       val lab_closures = eval ``label_closures (LENGTH []) (^(cs).next_label) ^(p6)``
       val (Ce,nl) = pairSyntax.dest_pair(rhsThm lab_closures)
-      
+
       val _ = (collectAnnotations := ([]:term list))
       (*Cheat and call PP internally so that the stateful annotations are updated*)
       val _ = term_to_string Ce
@@ -117,10 +117,10 @@ fun allIntermediates prog =
       val cs = rhsThm (eval ``compile_code_env (^(cs) with next_label := ^(nl)) ^(Ce)``)
 
       val compile_Cexp = eval ``compile [] TCNonTail 0 ^(cs) ^(Ce)``
-      (*val compile_Cexp = eval ``compile_Cexp [] 0 
+      (*val compile_Cexp = eval ``compile_Cexp [] 0
                            <|out:=[];next_label:=compile_primitives.rnext_label|> ^(p6)``*)
       val p7_1 = rhsThm compile_Cexp
-      
+
       (*compile print err*)
       val compile_print_err = eval ``compile_print_err ^(p7_1)``;
       val p7_2 = rhsThm compile_print_err
@@ -157,13 +157,13 @@ fun allIntermediates prog =
       val rem_labels = with_flag (quiet,true) eval ``remove_labels_all_asts real_inst_length (Success ^(p7))``
 
       (*Bytecode to asm*)
-      val asm = eval ``x64_code 0 ^(rhsThm rem_labels |> rand)``
+      val asm = eval ``bc_compile 0 ^(rhsThm rem_labels |> rand)``
       val p9 = rhsThm asm
 
       val p8 = rhsThm (eval ``(NONE,^(p8))``)
 
       val p7 = rhsThm (eval ``(SOME x,^(p7))``)
-      
+
   in
      {ils=[ast,p1,p2,p3,p4,p5,p6,p7,p8,p9],
       ctors=ctors,globMap=globMap,modMap=modMap,annotations=(!collectAnnotations)}