isabelle: src/HOL/Codegenerator_Test/Candidates.thy@67360d50ebb3 (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
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27103 diff changeset	8	Complex_Main
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"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 66251 diff changeset	18	"HOL-ex.Records"
21917 12b8fde1f9c0 added haftmann parents: diff changeset	19	begin
12b8fde1f9c0 added haftmann parents: diff changeset	20
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 69252 diff changeset	21	text \<open>Drop technical stuff from \<^theory>\<open>HOL.Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
61129 774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	22
59484 a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	23	setup \<open>
59842 9fda99b3d5ee tuned; wenzelm parents: 59733 diff changeset	24	fn thy =>
59484 a130ae7a9398 slightly more standard code setup for String.literal, with explicit special case in predicate compiler haftmann parents: 58889 diff changeset	25	let
59842 9fda99b3d5ee tuned; wenzelm parents: 59733 diff changeset	26	val tycos = Sign.logical_types thy;
9fda99b3d5ee tuned; wenzelm parents: 59733 diff changeset	27	val consts = map_filter (try (curry (Axclass.param_of_inst thy)
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 69252 diff changeset	28	\<^const_name>\<open>Quickcheck_Narrowing.partial_term_of\<close>)) tycos;
66251 cd935b7cb3fb proper concept of code declaration wrt. atomicity and Isar declarations haftmann parents: 66014 diff changeset	29	in fold Code.declare_unimplemented_global consts thy end
61129 774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	30	\<close>
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	31
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	32	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	33
51161 6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	34	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	35	where
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	36	empty: "sublist [] xs"
6ed12ae3b3e1 attempt to re-establish conventions which theories are loaded into the grand unified library theory; haftmann parents: 51160 diff changeset	37	\| 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	38	\| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
33500 22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	39
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	40	code_pred sublist .
22e5725be1f3 added predicate example haftmann parents: 33356 diff changeset	41
61129 774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	42	text \<open>Avoid popular infix.\<close>
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	code_reserved SML upto
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	45
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62425 diff changeset	46	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	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 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	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	"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	51
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	52	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	53	where
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	54	"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	55
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	56	lemma [code]:
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	57	"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	58	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	59
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	60	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	61	where
774752af4a1f parenthesing let-expressions in OCaml similar to case expressions avoids precendence problems due to ambiguous scope; haftmann parents: 59842 diff changeset	62	"check_list = (if funny_list = funny_list' then () else undefined)"
31378 d1cbf6393964 tuned code generator test theories haftmann parents: 30446 diff changeset	63
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62425 diff changeset	64	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	65
8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	66	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	67	where
8e736ce4c6f4 unconditional parenthesing of (chained) abstractions in Scala, with explicit regression setup haftmann parents: 61129 diff changeset	68	"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	69
21917 12b8fde1f9c0 added haftmann parents: diff changeset	70	end

author	paulson
	Thu, 12 Sep 2019 14:51:50 +0100
changeset 70689	67360d50ebb3
parent 69597	ff784d5a5bfb
child 72025	b4ed07cbe954
permissions	-rw-r--r--