Fix bug in translate_no_ind and add test case

The bug was found by @IlmariReissumies
ncough · Apr 21, 2018 · 49d2f76 · 49d2f76
1 parent ffce1e9
commit 49d2f76
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 15 deletions.
diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
@@ -245,23 +245,28 @@ in
   fun update_precondition new_pre = let
     fun update_aux (name,ml_name,tm,th,pre,module) = let
       val th1 = D th
-      val new_pre = (if is_imp (concl (SPEC_ALL new_pre))
-                     then (* case: new_pre is an induction theorem *)
-                       (MATCH_MP IMP_EQ_T (MP (D new_pre) TRUTH)
-                        handle HOL_ERR _ => new_pre)
-                     else new_pre)
+      val (new_pre,th1) =
+        (if is_imp (concl (SPEC_ALL new_pre))
+         then (* case: new_pre is an induction theorem *)
+           (((MATCH_MP IMP_EQ_T (MP (D new_pre) TRUTH)
+             handle HOL_ERR _ => new_pre)
+             |> PURE_REWRITE_RULE [GSYM CONJ_ASSOC]),
+            PURE_REWRITE_RULE [GSYM CONJ_ASSOC] th1)
+        else (new_pre,th1))
       val th2 = PURE_REWRITE_RULE [new_pre,PRECONDITION_T] th1
       in if aconv (concl th1) (concl th2)
-         then (name,ml_name,tm,th,pre,module) else let
-           val th2 = REWRITE_RULE [] th2
-           val th = remove_Eq_from_v_thm th2
-           val thm_name = name ^ "_v_thm"
-           val _ = print ("Updating " ^ thm_name ^ "\n")
-           val _ = save_thm(thm_name,th)
-           val new_pre = if can (find_term is_PRECONDITION) (concl (SPEC_ALL th))
-                         then new_pre else TRUTH
-           val th = th |> UNDISCH_ALL
-           in (name,ml_name,tm,th,new_pre,module) end end
+         then (name,ml_name,tm,th,pre,module) else
+           let
+             val th2 = REWRITE_RULE [] th2
+             val th = remove_Eq_from_v_thm th2
+             val thm_name = name ^ "_v_thm"
+             val _ = print ("Updating " ^ thm_name ^ "\n")
+             val _ = save_thm(thm_name,th)
+             val new_pre = if can (find_term is_PRECONDITION) (concl (SPEC_ALL th))
+                           then new_pre else TRUTH
+             val th = th |> UNDISCH_ALL
+           in (name,ml_name,tm,th,new_pre,module) end
+      end
     val _ = (v_thms := map update_aux (!v_thms))
     in new_pre end
   fun add_eval_thm th = let

diff --git a/translator/ml_translator_testScript.sml b/translator/ml_translator_testScript.sml
@@ -102,4 +102,34 @@ val _ = register_exn_type ``:exn_type``
 
 val _ = (print_asts := true);
 
+(* test no_ind *)
+
+val word64_msb_thm = Q.prove(
+  `!w. word_msb (w:word64) =
+         ((w && 0x8000000000000000w) = 0x8000000000000000w)`,
+  blastLib.BBLAST_TAC);
+
+val res = translate word64_msb_thm;
+
+val res = translate (miscTheory.arith_shift_right_def
+                     |> INST_TYPE [alpha|->``:64``]
+                     |> PURE_REWRITE_RULE [wordsTheory.dimindex_64]
+                     |> CONV_RULE (DEPTH_CONV wordsLib.WORD_GROUND_CONV));
+
+val ind_lemma = Q.prove(
+  `^(first is_forall (hyp res))`,
+  rpt gen_tac
+  \\ rpt (disch_then strip_assume_tac)
+  \\ match_mp_tac (latest_ind ())
+  \\ rpt strip_tac
+  \\ last_x_assum match_mp_tac
+  \\ rpt strip_tac
+  \\ fs [FORALL_PROD]
+  \\ first_x_assum match_mp_tac \\ wordsLib.WORD_EVAL_TAC \\ rw[])
+  |> update_precondition;
+
+val shift_test_def = Define `shift_test (x:word64) y = arith_shift_right x y`
+
+val res = translate shift_test_def;
+
 val _ = export_theory();