isabelle: src/HOL/Codegenerator_Test/Generate_Pretty.thy@fdc301f592c4 (annotated)

31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	1
d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	3
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 29933 diff changeset	4	header {* Pervasive test of code generator using pretty literals *}
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	5
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	6	theory Generate_Pretty
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	7	imports Candidates_Pretty
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	8	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	9
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	10	lemma [code, code del]: "nat_of_char = nat_of_char" ..
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	11	lemma [code, code del]: "char_of_nat = char_of_nat" ..
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37475 diff changeset	12
47108 2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 43317 diff changeset	13	declare Quickcheck_Narrowing.one_code_int_code [code del]
2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 43317 diff changeset	14	declare Quickcheck_Narrowing.int_of_code [code del]
43317 f9283eb3a4bf fixing code generation test bulwahn parents: 42842 diff changeset	15
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	16	subsection {* Check whether generated code compiles *}
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	17
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	18	text {*
37824 365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	19	If any of the checks fails, inspect the code generated
365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	20	by a corresponding @{text export_code} command.
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	21	*}
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	22
40711 81bc73585eec globbing constant expressions use more idiomatic underscore rather than star haftmann parents: 37825 diff changeset	23	export_code _ checking SML OCaml? Haskell? Scala?
25616 28d373f1482a added div/mod examples haftmann parents: 24530 diff changeset	24
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	25	end

author	Christian Sternagel
	Thu, 30 Aug 2012 15:44:03 +0900
changeset 49093	fdc301f592c4
parent 47108	2a1953f0d20d
child 50629	264ece81df93
permissions	-rw-r--r--