# HG changeset patch
# User haftmann
# Date 1738065762 -3600
# Node ID 513f8fa74c82b7fe6446db8c9106ab49dd508bca
# Parent  7d608575b20531b2e5e59a1e1b1de88b609b00c5
more explicit tests for non-PolyML SML platforms

diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- 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
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Codegenerator_Test/Generate_Target_GHC.thy
--- /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
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Codegenerator_Test/Generate_Target_MLton.thy
--- /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
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Codegenerator_Test/Generate_Target_OCaml.thy
--- /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
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Codegenerator_Test/Generate_Target_SMLNJ.thy
--- /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
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Codegenerator_Test/Generate_Target_String_Literals.thy
--- 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
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/Library/Code_Target_Bit_Shifts.thy
--- 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;
 
diff -r 7d608575b205 -r 513f8fa74c82 src/HOL/ROOT
--- 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 "