58 |
58 |
59 test_code check in OCaml |
59 test_code check in OCaml |
60 test_code check in GHC |
60 test_code check in GHC |
61 test_code check in Scala |
61 test_code check in Scala |
62 |
62 |
63 text \<open>Checking the index maximum for \<text>\<open>SML\<close>\<close> |
63 text \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close> |
64 |
64 |
65 ML \<open> |
65 definition \<open>check_max = ()\<close> |
|
66 |
|
67 definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close> |
|
68 |
|
69 code_printing |
|
70 code_module Check_Max \<rightharpoonup> |
|
71 (SML) \<open> |
66 fun check_max max = |
72 fun check_max max = |
67 let |
73 let |
68 val _ = IntInf.~>> (0, max); |
74 val _ = IntInf.~>> (0, max); |
69 val _ = \<^assert> ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); false) handle Size => true) |
75 val _ = ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); raise Fail "Bad max") handle Size => ()) |
70 in () end; |
76 in () end; |
71 \<close> |
77 \<close> |
|
78 | constant check_max \<rightharpoonup> |
|
79 (SML) "check'_max Bit'_Shifts.word'_max'_index" |
72 |
80 |
73 definition \<open>check_max = ()\<close> |
81 test_code \<open>snd anchor = ()\<close> in PolyML |
74 |
|
75 code_printing constant check \<rightharpoonup> |
|
76 (Eval) "check'_max Bit'_Shifts.word'_max'_index" |
|
77 |
|
78 definition \<open>anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\<close> |
|
79 |
|
80 ML \<open> |
|
81 \<^code>\<open>anchor\<close>; |
|
82 \<close> |
|
83 |
82 |
84 end |
83 end |