Permalink
Browse files

Add checks for cheats

  • Loading branch information...
xrchz committed Oct 7, 2018
1 parent 761b55f commit 23dbe76c0da185b84b56ae2da085d68d92bbf218
@@ -37,6 +37,7 @@ val compile_correct_applied =
val cake_compiled_thm =
CONJ compile_correct_applied cake_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "cake_compiled_thm";
(* TODO: compose this with a correctness theorem for compiler_x32? *)
@@ -37,6 +37,7 @@ val compile_correct_applied =
val cake_compiled_thm =
CONJ compile_correct_applied cake_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "cake_compiled_thm";
(* TODO: compose this with a correctness theorem for compiler_x64? *)
@@ -224,7 +224,8 @@ val compile_correct = Q.store_thm("compile_correct",
\\ fs[] )
\\ fs[])
\\ match_mp_tac primSemEnvTheory.prim_type_sound_invariants
\\ simp[]);
\\ simp[])
|> check_thm;
val type_config_ok = Q.store_thm ("type_config_ok",
`env_rel prim_tenv infer$init_config ∧
@@ -25,6 +25,7 @@ val compile_correct_applied =
val cat_compiled_thm =
CONJ compile_correct_applied cat_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "cat_compiled_thm";
val _ = export_theory();
@@ -25,6 +25,7 @@ val compile_correct_applied =
val diff_compiled_thm =
CONJ compile_correct_applied diff_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "diff_compiled_thm";
val _ = export_theory();
@@ -26,6 +26,7 @@ val compile_correct_applied =
val echo_compiled_thm =
CONJ compile_correct_applied echo_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "echo_compiled_thm";
val _ = export_theory();
@@ -25,6 +25,7 @@ val compile_correct_applied =
val grep_compiled_thm =
CONJ compile_correct_applied grep_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "grep_compiled_thm";
val _ = export_theory();
@@ -27,6 +27,7 @@ val compile_correct_applied =
val helloErr_compiled_thm =
CONJ compile_correct_applied helloErr_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "hello_compiled_thm";
val _ = export_theory();
@@ -26,6 +26,7 @@ val compile_correct_applied =
val hello_compiled_thm =
CONJ compile_correct_applied hello_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "hello_compiled_thm";
val _ = export_theory();
@@ -26,6 +26,7 @@ val compile_correct_applied =
val cat_compiled_thm =
CONJ compile_correct_applied cat_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "cat_compiled_thm";
val _ = export_theory();
@@ -25,6 +25,7 @@ val compile_correct_applied =
val patch_compiled_thm =
CONJ compile_correct_applied patch_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "patch_compiled_thm";
val _ = export_theory();
@@ -25,6 +25,7 @@ val compile_correct_applied =
val sort_compiled_thm =
CONJ compile_correct_applied sort_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "sort_compiled_thm";
val _ = export_theory();
View
@@ -25,6 +25,9 @@ val asm_exists_tac = first_assum(match_exists_tac o concl)
val has_pair_type = can dest_prod o type_of
(* -- *)
fun check_tag t = Tag.isEmpty t orelse Tag.isDisk t
val check_thm = Lib.assert (check_tag o Thm.tag)
val option_bind_tm = prim_mk_const{Thy="option",Name="OPTION_BIND"};
val option_ignore_bind_tm = prim_mk_const{Thy="option",Name="OPTION_IGNORE_BIND"};
val option_guard_tm = prim_mk_const{Thy="option",Name="OPTION_GUARD"};
@@ -27,6 +27,7 @@ val compile_correct_applied =
val wordcount_compiled_thm =
CONJ compile_correct_applied wordcount_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "wordcount_compiled_thm";
val _ = export_theory();

0 comments on commit 23dbe76

Please sign in to comment.