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
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51143 diff changeset	4	header {* Pervasive test of code generator *}
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
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51143 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: 51143 diff changeset	10	"~~/src/HOL/Library/Finite_Lattice"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51143 diff changeset	11	"~~/src/HOL/Library/Code_Binary_Nat"
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	12	begin
7d1a16c77f7c tuned haftmann parents: diff changeset	13
37745 6315b6426200 checking generated code for various target languages haftmann parents: 37695 diff changeset	14	text {*
37824 365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	15	If any of the checks fails, inspect the code generated
365e37fe93f3 added Isar syntax for code checking haftmann parents: 37819 diff changeset	16	by a corresponding @{text export_code} command.
37745 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
54228 229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	19	text {* Formal joining of hierarchy of implicit definitions in Scala *}
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	20
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	21	class semiring_numeral_even_odd = semiring_numeral_div + even_odd
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	22
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	23	instance nat :: semiring_numeral_even_odd ..
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	24
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	25	definition semiring_numeral_even_odd :: "'a itself \<Rightarrow> 'a::semiring_numeral_even_odd"
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	26	where
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	27	"semiring_numeral_even_odd TYPE('a) = undefined"
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	28
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	29	definition semiring_numeral_even_odd_nat :: "nat itself \<Rightarrow> nat"
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	30	where
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	31	"semiring_numeral_even_odd_nat = semiring_numeral_even_odd"
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	32
229282d53781 purely algebraic foundation for even/odd haftmann parents: 51161 diff changeset	33	export_code _ checking SML OCaml? Haskell? Scala
25616 28d373f1482a added div/mod examples haftmann parents: 24530 diff changeset	34
24195 7d1a16c77f7c tuned haftmann parents: diff changeset	35	end

author	blanchet
	Sat, 12 Jul 2014 11:31:22 +0200
changeset 57546	2b561e7a0512
parent 54228	229282d53781
child 58678	398e05aa84d4
permissions	-rw-r--r--