isabelle: src/HOL/Codegenerator_Test/Code_Test_GHC.thy@f7954a960890 (annotated)

59720 f893472fff31 proper headers; wenzelm parents: 58626 diff changeset	1	(* Title: HOL/Codegenerator_Test/Code_Test_GHC.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 GHC
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: 66453 diff changeset	7	theory Code_Test_GHC imports "HOL-Library.Code_Test" Code_Lazy_Test begin
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	8
58414 f945e7af0d27 drop workaround addressed by d0d3c30806b4 Andreas Lochbihler parents: 58348 diff changeset	9	test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
58039 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 [GHC] "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 GHC
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: 66453 diff changeset	23	test_code "stake 10 (cycle ''ab'') = ''ababababab''" in GHC
8b50f29a1992 new tool Code_Lazy Andreas Lochbihler parents: 66453 diff changeset	24
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	25	end

author	wenzelm
	Wed, 16 Dec 2020 15:39:21 +0100
changeset 72932	f7954a960890
parent 69597	ff784d5a5bfb
child 81642	e77e8ef5bf9b
permissions	-rw-r--r--