isabelle: src/HOL/Codegenerator_Test/Generate.thy@cd935b7cb3fb (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	4	section \<open>Pervasive test of code generator\<close>
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
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 50629 diff changeset	7	imports
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 50629 diff changeset	8	Candidates
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 50629 diff changeset	9	"~~/src/HOL/Library/AList_Mapping"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 50629 diff changeset	10	"~~/src/HOL/Library/Finite_Lattice"
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 28686 diff changeset	11	begin
24430 df56b9779a3d made SML/NJ happy haftmann parents: 24423 diff changeset	12
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	13	text \<open>
37824 365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	14	If any of the checks fails, inspect the code generated
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	15	by a corresponding \<open>export_code\<close> command.
0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	16	\<close>
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	17
50629 264ece81df93 code checking for Scala is mandatory, since Scala is now required anyway for Isabelle haftmann parents: 40711 diff changeset	18	export_code _ checking SML OCaml? Haskell? Scala
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	19
23266 50f0a4f12ed3 tuned document; wenzelm parents: 22845 diff changeset	20	end

author	haftmann
	Sun, 02 Jul 2017 20:13:38 +0200
changeset 66251	cd935b7cb3fb
parent 66191	d91108ba9474
child 66453	cc19f7ca2ed6
permissions	-rw-r--r--