isabelle: src/HOL/Codegenerator_Test/Generate_Binary

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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	4	section \<open>Pervasive test of code generator\<close>
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	5
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51143 diff changeset	6	theory Generate_Binary_Nat
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51143 diff changeset	7	imports
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51143 diff changeset	8	Candidates
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	9	"HOL-Library.AList_Mapping"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	10	"HOL-Library.Finite_Lattice"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	11	"HOL-Library.Code_Binary_Nat"
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	12	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	13
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	14	text \<open>
37824 365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	15	If any of the checks fails, inspect the code generated
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	16	by a corresponding \<open>export_code\<close> command.
0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	17	\<close>
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	18
58678 398e05aa84d4 purely algebraic characterization of even and odd haftmann parents: 54228 diff changeset	19	export_code _ checking SML OCaml? Haskell? Scala
25616 28d373f1482a added div/mod examples haftmann parents: 24530 diff changeset	20
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	21	end

author	immler
	Sun, 03 Nov 2019 21:46:46 -0500
changeset 71034	e0755162093f
parent 66453	cc19f7ca2ed6
permissions	-rw-r--r--