src/HOL/Codegenerator_Test/Code_Test_Scala.thy
author nipkow
Fri, 27 Mar 2020 12:28:05 +0100
changeset 71593 71579bd59cd4
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
added lemma
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 58626
diff changeset
     1
(*  Title:      HOL/Codegenerator_Test/Code_Test_Scala.thy
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     2
    Author:     Andreas Lochbihler, ETH Zurich
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     3
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     4
Test case for test_code on Scala
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     5
*)
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     6
68155
8b50f29a1992 new tool Code_Lazy
Andreas Lochbihler
parents: 67207
diff changeset
     7
theory Code_Test_Scala imports  "HOL-Library.Code_Test" Code_Lazy_Test begin
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     8
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
     9
test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
    10
58348
2d47c7d10b62 add target language evaluators for the value command;
Andreas Lochbihler
parents: 58039
diff changeset
    11
value [Scala] "14 + 7 * -12 :: integer"
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
    12
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 68155
diff changeset
    13
test_code \<comment> \<open>Tests for the serialisation of \<^const>\<open>gcd\<close> on \<^typ>\<open>integer\<close>\<close>
61856
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    14
  "gcd 15 10 = (5 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    15
  "gcd 15 (- 10) = (5 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    16
  "gcd (- 10) 15 = (5 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    17
  "gcd (- 10) (- 15) = (5 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    18
  "gcd 0 (- 10) = (10 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    19
  "gcd (- 10) 0 = (10 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    20
  "gcd 0 0 = (0 :: integer)"
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    21
in Scala
4b1b85f38944 add gcd instance for integer and serialisation to target language operations
Andreas Lochbihler
parents: 59720
diff changeset
    22
68155
8b50f29a1992 new tool Code_Lazy
Andreas Lochbihler
parents: 67207
diff changeset
    23
test_code "stake 10 (cycle ''ab'') = ''ababababab''" in Scala
8b50f29a1992 new tool Code_Lazy
Andreas Lochbihler
parents: 67207
diff changeset
    24
58039
469a375212c1 add testing framework for generated code
Andreas Lochbihler
parents:
diff changeset
    25
end