Fix breakages caused by d64dda1

Author: mn200

examples/computability/kolmog/kraft_ineqScript.sml

@@ -15,7 +15,7 @@ open realTheory;
 open real_sigmaTheory;
 open transcTheory;
 open boolListsTheory;
-
+local open numposrepTheory in end
 val _ = new_theory "kraft_ineq";
 
 val _ = intLib.deprecate_int()
@@ -948,7 +948,7 @@ Proof
 QED
 
 Definition TN2BL_def:
-  TN2BL n = MAP ((=) 1) $ REVERSE $ num_to_bin_list n
+  TN2BL n = MAP ((=) 1) $ num_to_bin_list n
 End
 
 Definition padL_def:

src/n-bit/bitstringLib.sml

@@ -115,14 +115,14 @@ local
 
    val num_from_bin_list_compute = prove(
      “(num_from_bin_list [] = 0) /\
-      (!l. num_from_bin_list (0::l) = NUMERAL (l2n 2 (0::l))) /\
-      (!l. num_from_bin_list (1::l) = NUMERAL (l2n 2 (1::l)))”,
+      (!l. num_from_bin_list (0::l) = NUMERAL (l2n 2 $ REVERSE (0::l))) /\
+      (!l. num_from_bin_list (1::l) = NUMERAL (l2n 2 $ REVERSE (1::l)))”,
       simp [numposrepTheory.num_from_bin_list_def] >> qm [NUMERAL_DEF])
 
    val cnv =
       Conv.REWR_CONV bitstringTheory.v2n_def
       THENC Conv.RAND_CONV (PURE_REWRITE_CONV [bitstringTheory.bitify_def])
-      THENC PURE_ONCE_REWRITE_CONV [num_from_bin_list_compute]
+      THENC Conv.REWR_CONV (GSYM NUMERAL_DEF)
       THENC Conv.TRY_CONV
               (Conv.RAND_CONV (PURE_REWRITE_CONV [l2n_2_numeric, iDUB_removal])
                THENC Conv.TRY_CONV (Conv.REWR_CONV NORM_0))

src/n-bit/selftest.sml

@@ -663,8 +663,26 @@ val () = qtest_conv "WORD_GROUND_CONV" wordsLib.WORD_GROUND_CONV
 
 val elapsed = Timer.checkRealTimer tt
 
-val _ = print ("\nTotal time: " ^ Lib.time_to_string elapsed ^ "\n");
-
+val _ = print ("\nTotal time: " ^ Lib.time_to_string elapsed ^
+               "\n\nbitstringLib tests\n\n");
+
+(* bitstringLib tests *)
+val _ = List.app convtest [
+      ("v2w_n2w_CONV (v2w [F; F] : bool[2])", bitstringLib.v2w_n2w_CONV,
+       “v2w [F; F] : bool[2]”, “0w : bool[2]”),
+      ("v2w_n2w_CONV (v2w [T; F] : bool[2])", bitstringLib.v2w_n2w_CONV,
+       “v2w [T; F] : bool[2]”, “2w : bool[2]”),
+      ("v2w_n2w_CONV (v2w [T; F; T] : bool[3])", bitstringLib.v2w_n2w_CONV,
+       “v2w [T; F; T] : bool[3]”, “5w : bool[3]”),
+      ("n2w_v2w_CONV (10w : word4)", bitstringLib.n2w_v2w_CONV,
+       “10w : word4”, “v2w [T; F; T; F] : word4”),
+      ("FIX_CONV (fixwidth 3 [F; T])", bitstringLib.FIX_CONV,
+       “fixwidth 3 [F; T]”, “[F;F;T]”),
+      ("FIX_CONV (fixwidth 3 [T; F; F; T])", bitstringLib.FIX_CONV,
+       “fixwidth 3 [T; F; F; T]”, “[F;F;T]”),
+      ("FIX_v2w_CONV (v2w [F;T] : word4)", bitstringLib.FIX_v2w_CONV,
+       “v2w [F; T] : word4”, “v2w [F; F; F; T] : word4”)
+    ]
 
 
 val _ = OS.Process.exit OS.Process.success