# HG changeset patch
# User haftmann
# Date 1737016017 -3600
# Node ID d4eaefc626ec1a0cd3e67a36c4bd11f5fd917ec5
# Parent  8df58b532ecb5fc75b2f84784ca38706a31dfb50
explicit check for (experimentally determined) border value

diff -r 8df58b532ecb -r d4eaefc626ec src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 09:26:56 2025 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy	Thu Jan 16 09:26:57 2025 +0100
@@ -60,4 +60,25 @@
 test_code check in GHC
 test_code check in Scala
 
+text \<open>Checking the index maximum for \<text>\<open>SML\<close>\<close>
+
+ML \<open>
+fun check_max max =
+  let
+    val _ = IntInf.~>> (0, max);
+    val _ = \<^assert> ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); false) handle Size => true)
+  in () end;
+\<close>
+
+definition \<open>check_max = ()\<close>
+
+code_printing constant check \<rightharpoonup>
+  (Eval) "check'_max Bit'_Shifts.word'_max'_index"
+
+definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close>
+
+ML \<open>
+\<^code>\<open>anchor\<close>;
+\<close>
+
 end
diff -r 8df58b532ecb -r d4eaefc626ec src/HOL/Library/Code_Target_Bit_Shifts.thy
--- a/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 09:26:56 2025 +0100
+++ b/src/HOL/Library/Code_Target_Bit_Shifts.thy	Thu Jan 16 09:26:57 2025 +0100
@@ -41,6 +41,7 @@
   type int = IntInf.int
   val push : int -> int -> int
   val drop : int -> int -> int
+  val word_max_index : Word.word (*only for validation*)
 end = struct
 
 type int = IntInf.int;