Minor fixes to bootstrap translation

jonsterling · Mar 29, 2018 · a45bac1 · a45bac1
1 parent 6c7ef75
commit a45bac1
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 2 deletions.
diff --git a/compiler/bootstrap/translation/explorerProgScript.sml b/compiler/bootstrap/translation/explorerProgScript.sml
@@ -24,6 +24,7 @@ fun def_of_const tm = let
 
 val _ = (find_def_for_const := def_of_const);
 
+val res = translate jsonLangTheory.escape_def;
 val res = translate jsonLangTheory.concat_with_def;
 
 val mem_to_string_lemma = prove(

diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml
@@ -526,8 +526,6 @@ val res = translate (wordLangTheory.word_sh_def
   |> REWRITE_RULE [miscTheory.word_ror_eq_any_word64_ror]
   |> RW[shift_left_rwt,shift_right_rwt,arith_shift_right_rwt] |> conv64)
 
-val _ = translate (wordLangTheory.num_exp_def |> conv64);
-
 val _ = translate (asmTheory.word_cmp_def |> REWRITE_RULE[WORD_LO,WORD_LT] |> spec64 |> REWRITE_RULE[word_msb_rw]);
 
 (* TODO: remove when pmatch is fixed *)