isabelle: src/HOL/Codegenerator_Test/Candidates.thy@89347c0cc6a3 (annotated)

31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	1
d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	2	(* Author: Florian Haftmann, TU Muenchen *)
21917 12b8fde1f9c0 added haftmann parents: diff changeset	3
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62425 diff changeset	4	section \<open>A huge collection of equations to generate code from\<close>
21917 12b8fde1f9c0 added haftmann parents: diff changeset	5
37695 71e84a203c19 introduced distinct session HOL-Codegenerator_Test haftmann parents: 37407 diff changeset	6	theory Candidates
21917 12b8fde1f9c0 added haftmann parents: diff changeset	7	imports
82516 88f101c3cfe2 official theory for using bit shift operations for ordinary arithmetic if feasible haftmann parents: 81706 diff changeset	8	Basic_Setup
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	9	"HOL-Library.Library"
69252 fc359b60121c dedicated examples for sorting haftmann parents: 68484 diff changeset	10	"HOL-Library.Sorting_Algorithms"
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	11	"HOL-Library.Subseq_Order"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	12	"HOL-Library.RBT"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	13	"HOL-Data_Structures.Tree_Map"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	14	"HOL-Data_Structures.Tree_Set"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	15	"HOL-Computational_Algebra.Computational_Algebra"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	16	"HOL-Computational_Algebra.Polynomial_Factorial"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	17	"HOL-Number_Theory.Eratosthenes"
72029 83456d9f0ed5 clarified examples; wenzelm parents: 72025 diff changeset	18	"HOL-Examples.Records"
75955 5305c65dcbb2 Gauss numbers haftmann parents: 75647 diff changeset	19	"HOL-Examples.Gauss_Numbers"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	20	begin
12b8fde1f9c0 added haftmann parents: diff changeset	21
82516 88f101c3cfe2 official theory for using bit shift operations for ordinary arithmetic if feasible haftmann parents: 81706 diff changeset	22	setup \<open>Codegenerator_Test.drop_partial_term_of\<close>
61129 774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	23
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	24	text \<open>Simple example for the predicate compiler.\<close>
59484 a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	25
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	26	inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	27	where
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	28	empty: "sublist [] xs"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	29	\| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	30	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	31
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	32	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	33
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62425 diff changeset	34	text \<open>Explicit check in \<open>OCaml\<close> for correct precedence of let expressions in list expressions\<close>
61129 774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	35
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	36	definition funny_list :: "bool list"
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	37	where
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	38	"funny_list = [let b = True in b, False]"
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	39
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	40	definition funny_list' :: "bool list"
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	41	where
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	42	"funny_list' = funny_list"
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	43
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	44	lemma [code]:
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	45	"funny_list' = [True, False]"
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	46	by (simp add: funny_list_def funny_list'_def)
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	47
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	48	definition check_list :: unit
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	49	where
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	50	"check_list = (if funny_list = funny_list' then () else undefined)"
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	51
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62425 diff changeset	52	text \<open>Explicit check in \<open>Scala\<close> for correct bracketing of abstractions\<close>
61130 8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	53
8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	54	definition funny_funs :: "(bool \<Rightarrow> bool) list \<Rightarrow> (bool \<Rightarrow> bool) list"
8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	55	where
8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	56	"funny_funs fs = (\<lambda>x. x \<or> True) # (\<lambda>x. x \<or> False) # fs"
8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	57
75647 34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	58	text \<open>Explicit checks for strings etc.\<close>
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	59
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	60	definition \<open>hello = ''Hello, world!''\<close>
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	61
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	62	definition \<open>hello2 = String.explode (String.implode hello)\<close>
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	63
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	64	definition \<open>which_hello \<longleftrightarrow> hello \<le> hello2\<close>
34cd1d210b92 officical abstract characters for code generation haftmann parents: 72515 diff changeset	65
21917 12b8fde1f9c0 added haftmann parents: diff changeset	66	end

author	haftmann
	Thu, 19 Jun 2025 17:15:40 +0200
changeset 82734	89347c0cc6a3
parent 82516	88f101c3cfe2
permissions	-rw-r--r--