Remove e_rm_reg_def following HOL (04d2447)

CakeML · Dec 28, 2017 · 4db3cb0 · 4db3cb0
1 parent 37176c6
commit 4db3cb0
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/compiler/bootstrap/translation/x64ProgScript.sml b/compiler/bootstrap/translation/x64ProgScript.sml
@@ -93,7 +93,7 @@ val if_neq = Q.prove(`
 
 val fconv = SIMP_RULE (srw_ss()) [SHIFT_ZERO,case_ifs,case_ifs2,if_neq]
 
-val defaults = [x64_ast_def,x64_encode_def,encode_def,e_rm_reg_def,e_gen_rm_reg_def,e_ModRM_def,e_opsize_def,e_imm32_def,rex_prefix_def,x64_dec_fail_def,e_opc_def,e_rax_imm_def,e_rm_imm_def,asmSemTheory.is_test_def,x64_cmp_def,e_opsize_imm_def,e_imm8_def,e_rm_imm8_def,not_byte_def,e_imm16_def,e_imm64_def,Zsize_width_def,x64_bop_def,zreg2num_totalnum2zerg,e_imm_8_32_def,Zbinop_name2num_x64_sh,x64_sh_notZtest,exh_if_collapse,is_rax_zr_thm]
+val defaults = [x64_ast_def,x64_encode_def,encode_def,e_gen_rm_reg_def,e_ModRM_def,e_opsize_def,e_imm32_def,rex_prefix_def,x64_dec_fail_def,e_opc_def,e_rax_imm_def,e_rm_imm_def,asmSemTheory.is_test_def,x64_cmp_def,e_opsize_imm_def,e_imm8_def,e_rm_imm8_def,not_byte_def,e_imm16_def,e_imm64_def,Zsize_width_def,x64_bop_def,zreg2num_totalnum2zerg,e_imm_8_32_def,Zbinop_name2num_x64_sh,x64_sh_notZtest,exh_if_collapse,is_rax_zr_thm]
 
 val x64_enc_thms =
   x64_enc_def

diff --git a/compiler/encoders/x64/proofs/x64_targetProofScript.sml b/compiler/encoders/x64/proofs/x64_targetProofScript.sml
@@ -431,7 +431,7 @@ val encode_rwts =
       open x64Theory
    in
       [x64_enc_def, x64_ast_def, x64_bop_def, x64_cmp_def, x64_sh_def,
-       x64_encode_def, encode_def, e_rm_reg_def, e_gen_rm_reg_def,
+       x64_encode_def, encode_def, e_gen_rm_reg_def,
        e_ModRM_def, e_opsize_def, rex_prefix_def, e_opc_def, e_rm_imm8_def,
        e_opsize_imm_def, not_byte_def, e_rax_imm_def, e_rm_imm_def,
        e_imm_8_32_def, e_imm_def, e_imm8_def, e_imm16_def, e_imm32_def,

diff --git a/compiler/encoders/x64/x64_eval_encodeScript.sml b/compiler/encoders/x64/x64_eval_encodeScript.sml
@@ -42,7 +42,7 @@ in
     RIGHT_CONV_RULE
       (Conv.DEPTH_CONV rex_prefix_conv THENC SIMP_CONV (srw_ss()) [])
   val enc_rwts =
-    [x64_encode_def, x64_enc_def, encode_def, e_rm_reg_def, e_gen_rm_reg_def,
+    [x64_encode_def, x64_enc_def, encode_def, e_gen_rm_reg_def,
      e_ModRM_def, not_fail, cond_rand, listTheory.LIST_BIND_def]
   fun enc_thm s rwts =
     let
@@ -127,7 +127,7 @@ val sub_overflow_rwt =
 
 local
   val thms =
-    [e_rm_reg_def, e_gen_rm_reg_def, e_ModRM_def, e_opsize_def,
+    [e_gen_rm_reg_def, e_ModRM_def, e_opsize_def,
      mk_let_thm `(rex_prefix (v || 8w),1w: word8)`,
      mk_let_thm `(rex_prefix (7w && v),1w: word8)`]
 in

diff --git a/compiler/encoders/x64/x64_targetLib.sml b/compiler/encoders/x64/x64_targetLib.sml
@@ -33,7 +33,7 @@ in
      (ERR "x64_encode_conv" "")
      (computeLib.compset_conv (wordsLib.words_compset())
       [computeLib.Defs
-         [x64_bop_def, x64_cmp_def, x64_sh_def, e_rm_reg_def, e_gen_rm_reg_def,
+         [x64_bop_def, x64_cmp_def, x64_sh_def, e_gen_rm_reg_def,
           e_ModRM_def, e_opsize_def, rex_prefix_def, e_opc_def, e_rm_imm8_def,
           e_opsize_imm_def, not_byte_def, e_rax_imm_def, e_rm_imm_def,
           e_imm_8_32_def, e_imm_def, e_imm8_def, e_imm16_def, e_imm32_def,