isabelle: src/HOL/Codegenerator_Test/Code_Test_PolyML.thy@1fad64843239 (annotated)

59720 f893472fff31 proper headers; wenzelm parents: 58626 diff changeset	1	(* Title: HOL/Codegenerator_Test/Code_Test_PolyML.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
81642 e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	5	theory Code_Test_PolyML
e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	6	imports
e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	7	"HOL-Library.Code_Test"
e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	8	Code_Lazy_Test
e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	9	begin
e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	10
e77e8ef5bf9b explicit tests for target-language bit operations haftmann parents: 68155 diff changeset	11	text \<open>Test cases for \<^text>\<open>test_code\<close>\<close>
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	12
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	13	test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	14
58348 2d47c7d10b62 add target language evaluators for the value command; Andreas Lochbihler parents: 58039 diff changeset	15	value [PolyML] "14 + 7 * -12 :: integer"
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	16
68155 8b50f29a1992 new tool Code_Lazy Andreas Lochbihler parents: 66453 diff changeset	17	test_code "stake 10 (cycle ''ab'') = ''ababababab''" in PolyML
8b50f29a1992 new tool Code_Lazy Andreas Lochbihler parents: 66453 diff changeset	18
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	19	end

author	wenzelm
	Sat, 15 Feb 2025 14:17:38 +0100
changeset 82180	1fad64843239
parent 81815	0b31f0909060
permissions	-rw-r--r--