--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Tue Jan 28 07:17:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Tue Jan 28 13:02:42 2025 +0100
@@ -8,9 +8,11 @@
"HOL-Library.Code_Target_Bit_Shifts"
begin
-unbundle bit_operations_syntax
+context
+ includes bit_operations_syntax
+begin
-definition computations where
+qualified definition computations where
\<open>computations = (
[bit (473514 :: integer) 5, bit (- 805167 :: integer) 7],
[473514 AND 767063, - 805167 AND 767063, 473514 AND - 314527, - 805167 AND - 314527 :: integer],
@@ -27,7 +29,7 @@
[signed_take_bit 12 473514, signed_take_bit 12 (- 805167) :: integer]
)\<close>
-definition results where
+qualified definition results where
\<open>results = (
[True, True],
[208898, 242769, 209184, - 839103 :: integer],
@@ -44,7 +46,7 @@
[- 1622, - 2351 :: integer]
)\<close>
-definition check where
+qualified definition check where
\<open>check \<longleftrightarrow> computations = results\<close>
lemma check
@@ -56,15 +58,15 @@
lemma check
by eval
-test_code check in OCaml
-test_code check in GHC
test_code check in Scala
text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close>
-definition \<open>check_max = ()\<close>
+qualified definition \<open>check_max = ()\<close>
-definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+qualified definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+end
code_printing
code_module Check_Max \<rightharpoonup>
@@ -75,9 +77,9 @@
val _ = ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); raise Fail "Bad max") handle Size => ())
in () end;
\<close>
- | constant check_max \<rightharpoonup>
+ | constant Generate_Target_Bit_Operations.check_max \<rightharpoonup>
(SML) "check'_max Bit'_Shifts.word'_max'_index"
-test_code \<open>snd anchor = ()\<close> in PolyML
+test_code \<open>snd Generate_Target_Bit_Operations.anchor = ()\<close> in PolyML
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_GHC.thy Tue Jan 28 13:02:42 2025 +0100
@@ -0,0 +1,14 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language specific implementations for GHC\<close>
+
+theory Generate_Target_GHC
+ imports
+ "HOL-Codegenerator_Test.Generate_Target_String_Literals"
+ "HOL-Codegenerator_Test.Generate_Target_Bit_Operations"
+begin
+
+test_code Generate_Target_String_Literals.check in GHC
+test_code Generate_Target_Bit_Operations.check in GHC
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_MLton.thy Tue Jan 28 13:02:42 2025 +0100
@@ -0,0 +1,14 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language specific implementations for MLton\<close>
+
+theory Generate_Target_MLton
+ imports
+ "HOL-Codegenerator_Test.Generate_Target_String_Literals"
+ "HOL-Codegenerator_Test.Generate_Target_Bit_Operations"
+begin
+
+test_code Generate_Target_String_Literals.check in MLton
+test_code Generate_Target_Bit_Operations.check in MLton
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_OCaml.thy Tue Jan 28 13:02:42 2025 +0100
@@ -0,0 +1,14 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language specific implementations for OCaml\<close>
+
+theory Generate_Target_OCaml
+ imports
+ "HOL-Codegenerator_Test.Generate_Target_String_Literals"
+ "HOL-Codegenerator_Test.Generate_Target_Bit_Operations"
+begin
+
+test_code Generate_Target_String_Literals.check in OCaml
+test_code Generate_Target_Bit_Operations.check in OCaml
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codegenerator_Test/Generate_Target_SMLNJ.thy Tue Jan 28 13:02:42 2025 +0100
@@ -0,0 +1,14 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+section \<open>Test of target-language specific implementations for SML/NJ\<close>
+
+theory Generate_Target_SMLNJ
+ imports
+ "HOL-Codegenerator_Test.Generate_Target_String_Literals"
+ "HOL-Codegenerator_Test.Generate_Target_Bit_Operations"
+begin
+
+test_code Generate_Target_String_Literals.check in SMLNJ
+test_code Generate_Target_Bit_Operations.check in SMLNJ
+
+end
\ No newline at end of file
--- a/src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy Tue Jan 28 07:17:30 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy Tue Jan 28 13:02:42 2025 +0100
@@ -7,7 +7,10 @@
"HOL-Library.Code_Test"
begin
-definition computations where
+context
+begin
+
+qualified definition computations where
\<open>computations = (
STR ''abc'' + STR 0x20 + STR ''def'',
String.implode ''abc'',
@@ -18,7 +21,7 @@
STR ''abc'' < STR ''def''
)\<close>
-definition results where
+qualified definition results where
\<open>results = (
STR ''abc def'',
STR ''abc'',
@@ -29,7 +32,7 @@
True
)\<close>
-definition check where
+qualified definition check where
\<open>check \<longleftrightarrow> computations = results\<close>
lemma check
@@ -41,8 +44,8 @@
lemma check
by eval
-test_code check in OCaml
-test_code check in GHC
test_code check in Scala
end
+
+end
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy Tue Jan 28 07:17:30 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy Tue Jan 28 13:02:42 2025 +0100
@@ -51,7 +51,7 @@
fun replicate n x = (if n <= 0 then [] else x :: replicate (n - 1) x);
-val max_index = pow (2, (Word.wordSize - 3)) - 1; (*experimentally determined*)
+val max_index = pow (fromInt 2, Int.- (Word.wordSize, 3)) - fromInt 1; (*experimentally determined*)
val word_of_int = Word.fromLargeInt o toLarge;
--- a/src/HOL/ROOT Tue Jan 28 07:17:30 2025 +0100
+++ b/src/HOL/ROOT Tue Jan 28 13:02:42 2025 +0100
@@ -377,17 +377,24 @@
Code_Lazy_Test
Code_Test_PolyML
Code_Test_Scala
- theories [condition = "ISABELLE_GHC,ISABELLE_OCAMLFIND"]
Generate_Target_String_Literals
Generate_Target_Bit_Operations
+ theories [condition = ISABELLE_MLTON]
+ Generate_Target_MLton
+ theories [condition = ISABELLE_SMLNJ]
+ Generate_Target_SMLNJ
+ theories [condition = ISABELLE_OCAMLFIND]
+ Generate_Target_OCaml
+ theories [condition = ISABELLE_GHC]
+ Generate_Target_GHC
+ theories [condition = ISABELLE_MLTON]
+ Code_Test_MLton
+ theories [condition = ISABELLE_SMLNJ]
+ Code_Test_SMLNJ
+ theories [condition = ISABELLE_OCAMLFIND]
+ Code_Test_OCaml
theories [condition = ISABELLE_GHC]
Code_Test_GHC
- theories [condition = ISABELLE_MLTON]
- Code_Test_MLton
- theories [condition = ISABELLE_OCAMLFIND]
- Code_Test_OCaml
- theories [condition = ISABELLE_SMLNJ]
- Code_Test_SMLNJ
session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" +
description "