isabelle: src/HOL/Codegenerator_Test/Code_Test_Scala.thy@4b1b85f38944 (annotated)

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
61856 4b1b85f38944 add gcd instance for integer and serialisation to target language operations Andreas Lochbihler parents: 59720 diff changeset	7	theory Code_Test_Scala imports "../Library/Code_Test" "../GCD" begin
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	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 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	11	test_code "14 + 7 * -12 = (140 div -2 :: integer)" in Scala
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	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 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	14
61856 4b1b85f38944 add gcd instance for integer and serialisation to target language operations Andreas Lochbihler parents: 59720 diff changeset	15	test_code -- \<open>Tests for the serialisation of @{const gcd} on @{typ integer}\<close>
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 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	25	end

author	Andreas Lochbihler
	Fri, 18 Dec 2015 11:14:28 +0100
changeset 61856	4b1b85f38944
parent 59720	f893472fff31
child 63167	0909deb8059b
permissions	-rw-r--r--