author | haftmann |
Thu, 25 May 2017 14:38:41 +0200 | |
changeset 65919 | b6d458915f1b |
parent 65552 | f533820e7248 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
59720 | 1 |
(* Title: HOL/Codegenerator_Test/Code_Test_Scala.thy |
58039 | 2 |
Author: Andreas Lochbihler, ETH Zurich |
3 |
||
4 |
Test case for test_code on Scala |
|
5 |
*) |
|
6 |
||
65552
f533820e7248
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
wenzelm
parents:
63167
diff
changeset
|
7 |
theory Code_Test_Scala imports "../Library/Code_Test" begin |
58039 | 8 |
|
58520
a4d1f8041af0
accomplish potentially case-insenstive file systems for Scala
haftmann
parents:
58348
diff
changeset
|
9 |
declare [[scala_case_insensitive]] |
a4d1f8041af0
accomplish potentially case-insenstive file systems for Scala
haftmann
parents:
58348
diff
changeset
|
10 |
|
58039 | 11 |
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala |
12 |
||
58348
2d47c7d10b62
add target language evaluators for the value command;
Andreas Lochbihler
parents:
58039
diff
changeset
|
13 |
value [Scala] "14 + 7 * -12 :: integer" |
58039 | 14 |
|
63167 | 15 |
test_code \<comment> \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close> |
61856
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
16 |
"gcd 15 10 = (5 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
17 |
"gcd 15 (- 10) = (5 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
18 |
"gcd (- 10) 15 = (5 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
19 |
"gcd (- 10) (- 15) = (5 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
20 |
"gcd 0 (- 10) = (10 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
21 |
"gcd (- 10) 0 = (10 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
22 |
"gcd 0 0 = (0 :: integer)" |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
23 |
in Scala |
4b1b85f38944
add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents:
59720
diff
changeset
|
24 |
|
58039 | 25 |
end |