isabelle: src/HOL/ex/Codegenerator.thy@46be40d304d7 (annotated)

19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	1	(* ID: $Id$
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	2	Author: Florian Haftmann, TU Muenchen
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	3	*)
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	4
21877 e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	5	header {* Tests and examples for code generator *}
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	6
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	7	theory Codegenerator
21877 e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	8	imports
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	9	Main
21892 af35b480916e import path made absolute haftmann parents: 21877 diff changeset	10	"~~/src/HOL/ex/Records"
21877 e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	11	AssocList
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	12	Binomial
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	13	Commutative_Ring
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	14	GCD
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	15	List_Prefix
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	16	Nat_Infinity
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	17	NatPair
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	18	Nested_Environment
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	19	Permutation
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	20	Primes
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	21	Product_ord
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	22	SetsAndFunctions
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	23	State_Monad
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	24	While_Combinator
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	25	Word
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	26	(a lot of stuff to test)
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	27	begin
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	28
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	29	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 21319 diff changeset	30	n :: nat where
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	31	"n = 42"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	32
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	33	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 21319 diff changeset	34	k :: "int" where
20351 c7658e811ffb added more examples haftmann parents: 20187 diff changeset	35	"k = -42"
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	36
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	37	datatype mut1 = Tip \| Top mut2
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	38	and mut2 = Tip \| Top mut1
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	39
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	40	consts
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	41	mut1 :: "mut1 \<Rightarrow> mut1"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	42	mut2 :: "mut2 \<Rightarrow> mut2"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	43
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	44	primrec
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	45	"mut1 mut1.Tip = mut1.Tip"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	46	"mut1 (mut1.Top x) = mut1.Top (mut2 x)"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	47	"mut2 mut2.Tip = mut2.Tip"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	48	"mut2 (mut2.Top x) = mut2.Top (mut1 x)"
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	49
20702 8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	50	definition
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	51	"mystring = ''my home is my castle''"
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	52
21877 e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	53	text {* nested lets and such *}
20968 5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	54
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	55	definition
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	56	"abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	57
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	58	definition
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	59	"nested_let x = (let (y, z) = x in let w = y z in w * w)"
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	60
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	61	definition
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	62	"case_let x = (let (y, z) = x in case y of () => z)"
5294baa98468 added examples for nested let haftmann parents: 20952 diff changeset	63
21155 95142d816793 added particular test for partially applied case constants haftmann parents: 21125 diff changeset	64	definition
95142d816793 added particular test for partially applied case constants haftmann parents: 21125 diff changeset	65	"base_case f = f list_case"
95142d816793 added particular test for partially applied case constants haftmann parents: 21125 diff changeset	66
20702 8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	67	definition
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	68	"apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	69
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	70	definition
21877 e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	71	"keywords fun datatype x instance funa classa =
e871f57b1adb now testing executable content of nearly all HOL haftmann parents: 21545 diff changeset	72	Suc fun + datatype * x mod instance - funa - classa"
20702 8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	73
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	74	hide (open) const keywords
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	75
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	76	definition
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	77	"shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
8b79d853eabb added examples for variable name handling haftmann parents: 20597 diff changeset	78
21898 46be40d304d7 deactivated test for the moment haftmann parents: 21892 diff changeset	79	(code_gen "" (Haskell -) (SML #)*)
19281 b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	80
b411f25fff25 added example for operational classes and code generator haftmann parents: diff changeset	81	end

author	haftmann
	Fri, 22 Dec 2006 15:35:17 +0100
changeset 21898	46be40d304d7
parent 21892	af35b480916e
child 21911	e29bcab0c81c
permissions	-rw-r--r--