isabelle: src/HOL/Codegenerator_Test/Generate.thy@000049335247 (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 {*
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	13	If any of the @{text ML} ... check fails, inspect the code generated
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	14	by the previous @{text export_code} command.
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
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	17	export_code "*" in SML module_name Code_Test file -
37819 000049335247 check without explicit path haftmann parents: 37745 diff changeset	18	ML {* Code_ML.check_SML @{theory} *}
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	19
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	20	export_code "*" in OCaml module_name Code_Test file -
37819 000049335247 check without explicit path haftmann parents: 37745 diff changeset	21	ML {* Code_ML.check_OCaml @{theory} *}
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	22
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	23	export_code "*" in Haskell module_name Code_Test file -
37819 000049335247 check without explicit path haftmann parents: 37745 diff changeset	24	ML {* Code_Haskell.check @{theory} *}
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	25
6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	26	export_code "*" in Scala module_name Code_Test file -
37819 000049335247 check without explicit path haftmann parents: 37745 diff changeset	27	ML {* Code_Scala.check @{theory} *}
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	28
23266 50f0a4f12ed3 tuned document; wenzelm parents: 22845 diff changeset	29	end

author	haftmann
	Wed, 14 Jul 2010 14:20:47 +0200
changeset 37819	000049335247
parent 37745	6315b6426200
child 37824	365e37fe93f3
permissions	-rw-r--r--