isabelle: src/HOL/Codegenerator_Test/Code_Test_GHC.thy@2d47c7d10b62 (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
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	7	theory Code_Test_GHC imports Code_Test begin
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	definition id_integer :: "integer \<Rightarrow> integer" where "id_integer = id"
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	10
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	11	test_code "id_integer (14 + 7 * -12) = 140 div -2" in GHC
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 [GHC] "14 + 7 * -12 :: integer"
58039 469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	14
469a375212c1 add testing framework for generated code Andreas Lochbihler parents: diff changeset	15	end

author	Andreas Lochbihler
	Tue, 16 Sep 2014 16:04:08 +0200
changeset 58348	2d47c7d10b62
parent 58039	469a375212c1
child 58414	f945e7af0d27
permissions	-rw-r--r--