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