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

58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	1	(* Title: Code_Test_GHC.thy
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
58626 6c473ed0ac70 move Code_Test to HOL/Library; Andreas Lochbihler parents: 58414 diff changeset	7	theory Code_Test_GHC imports "../Library/Code_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
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	13	end

author	Andreas Lochbihler
	Wed, 11 Feb 2015 18:39:56 +0100
changeset 59527	edaabc1ab1ed
parent 58626	6c473ed0ac70
child 59720	f893472fff31
permissions	-rw-r--r--