isabelle: src/HOL/Codegenerator_Test/Generate.thy@6584098d5378 (annotated)

19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	1
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	3
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	4	header {* Pervasive test of code generator *}
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	5
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 34306 diff changeset	6	theory Generate
71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 34306 diff changeset	7	imports Candidates
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	8	begin
24430 df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	9
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	10	subsection {* Check whether generated code compiles *}
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	11
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	12	text {*
37824 365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	13	If any of the checks fails, inspect the code generated
365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	14	by a corresponding @{text export_code} command.
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	15	*}
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	16
40711 81bc73585eec globbing constant expressions use more idiomatic underscore rather than star haftmann parents: 37825 diff changeset	17	export_code _ checking SML OCaml? Haskell? Scala?
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	18
23266 50f0a4f12ed3 tuned document; wenzelm parents: 22845 diff changeset	19	end

author	wenzelm
	Fri, 30 Mar 2012 17:22:17 +0200
changeset 47230	6584098d5378
parent 40711	81bc73585eec
child 50629	264ece81df93
permissions	-rw-r--r--