# 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 \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] )\ -definition results where +qualified definition results where \results = ( [True, True], [208898, 242769, 209184, - 839103 :: integer], @@ -44,7 +46,7 @@ [- 1622, - 2351 :: integer] )\ -definition check where +qualified definition check where \check \ computations = results\ 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 \Checking the index maximum for \\PolyML\\ -definition \check_max = ()\ +qualified definition \check_max = ()\ -definition \anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\ +qualified definition \anchor = (Code_Target_Bit_Shifts.drop_bit, check_max)\ + +end code_printing code_module Check_Max \ @@ -75,9 +77,9 @@ val _ = ((IntInf.~>> (0, Word.+ (max, Word.fromInt 1)); raise Fail "Bad max") handle Size => ()) in () end; \ - | constant check_max \ + | constant Generate_Target_Bit_Operations.check_max \ (SML) "check'_max Bit'_Shifts.word'_max'_index" -test_code \snd anchor = ()\ in PolyML +test_code \snd Generate_Target_Bit_Operations.anchor = ()\ 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 \Test of target-language specific implementations for GHC\ + +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 \Test of target-language specific implementations for MLton\ + +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 \Test of target-language specific implementations for OCaml\ + +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 \Test of target-language specific implementations for SML/NJ\ + +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 \computations = ( STR ''abc'' + STR 0x20 + STR ''def'', String.implode ''abc'', @@ -18,7 +21,7 @@ STR ''abc'' < STR ''def'' )\ -definition results where +qualified definition results where \results = ( STR ''abc def'', STR ''abc'', @@ -29,7 +32,7 @@ True )\ -definition check where +qualified definition check where \check \ computations = results\ 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 "