# HG changeset patch # User huffman # Date 1258065089 28800 # Node ID 053ac8080c11aebc72e35cfad691e42bf6ce9a21 # Parent d2f3104ca3d20669b2e90161418d3362aebbc766# Parent af07d9cd86cef5a947a90536bab01ddacb4b8d8c merged diff -r d2f3104ca3d2 -r 053ac8080c11 CONTRIBUTORS --- a/CONTRIBUTORS Thu Nov 12 14:31:11 2009 -0800 +++ b/CONTRIBUTORS Thu Nov 12 14:31:29 2009 -0800 @@ -6,7 +6,9 @@ Contributions to this Isabelle version -------------------------------------- - +* November 2009: Lukas Bulwahn, TUM + Predicate Compiler: a compiler for inductive predicates to equational specfications + * November 2009: Sascha Boehme, TUM HOL-Boogie: an interactive prover back-end for Boogie and VCC diff -r d2f3104ca3d2 -r 053ac8080c11 NEWS --- a/NEWS Thu Nov 12 14:31:11 2009 -0800 +++ b/NEWS Thu Nov 12 14:31:29 2009 -0800 @@ -37,6 +37,9 @@ *** HOL *** +* New commands "code_pred" and "values" to invoke the predicate compiler +and to enumerate values of inductive predicates. + * Combined former theories Divides and IntDiv to one theory Divides in the spirit of other number theory theories in HOL; some constants (and to a lesser extent also facts) have been suffixed with _nat und _int @@ -91,6 +94,9 @@ zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default. INCOMPATIBILITY. +* Added theorem List.map_map as [simp]. Removed List.map_compose. +INCOMPATIBILITY. + * New testing tool "Mirabelle" for automated (proof) tools. Applies several tools and tactics like sledgehammer, metis, or quickcheck, to every proof step in a theory. To be used in batch mode via the diff -r d2f3104ca3d2 -r 053ac8080c11 src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/FOL/ex/LocaleTest.thy Thu Nov 12 14:31:29 2009 -0800 @@ -453,8 +453,7 @@ subsection {* Interpretation in theory, then sublocale *} -interpretation (* fol: *) logic "op +" "minus" -(* FIXME declaration of qualified names *) +interpretation fol: logic "op +" "minus" by unfold_locales (rule int_assoc int_minus2)+ locale logic2 = @@ -464,17 +463,15 @@ and notnot: "-- (-- x) = x" begin -(* FIXME interpretation below fails definition lor (infixl "||" 50) where "x || y = --(-- x && -- y)" -*) end sublocale logic < two: logic2 by unfold_locales (rule assoc notnot)+ -thm two.assoc +thm fol.two.assoc subsection {* Declarations and sublocale *} diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Code_Evaluation.thy --- a/src/HOL/Code_Evaluation.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Code_Evaluation.thy Thu Nov 12 14:31:29 2009 -0800 @@ -145,7 +145,7 @@ (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))") code_const "term_of \ String.literal \ term" - (Eval "HOLogic.mk'_message'_string") + (Eval "HOLogic.mk'_literal") code_reserved Eval HOLogic diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Datatype.thy Thu Nov 12 14:31:29 2009 -0800 @@ -562,6 +562,14 @@ Sumr :: "('b => 'c) => 'a + 'b => 'c" "Sumr == sum_case undefined" +lemma [code]: + "Suml f (Inl x) = f x" + by (simp add: Suml_def) + +lemma [code]: + "Sumr f (Inr x) = f x" + by (simp add: Sumr_def) + lemma Suml_inject: "Suml f = Suml g ==> f = g" by (unfold Suml_def) (erule sum_case_inject) diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Decision_Procs/Ferrack.thy --- a/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Decision_Procs/Ferrack.thy Thu Nov 12 14:31:29 2009 -0800 @@ -1928,7 +1928,8 @@ { fix t n assume tnY: "(t,n) \ set ?Y" hence "(t,n) \ set ?SS" by simp hence "\ (t',n') \ set ?S. simp_num_pair (t',n') = (t,n)" - by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) + by (auto simp add: split_def simp del: map_map) + (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) then obtain t' n' where tn'S: "(t',n') \ set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto from simp_num_pair_l[OF tnb np tns] diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Decision_Procs/MIR.thy --- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Decision_Procs/MIR.thy Thu Nov 12 14:31:29 2009 -0800 @@ -1522,7 +1522,7 @@ also fix y have "\ = (\x. (Ifm (y#bs) ?cyes) \ (Ifm (x#bs) ?cno))" using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast also have "\ = (Ifm bs (decr ?cyes) \ Ifm bs (E ?cno))" - by (auto simp add: decr[OF yes_nb]) + by (auto simp add: decr[OF yes_nb] simp del: partition_filter_conv) also have "\ = (Ifm bs (conj (decr ?cyes) (qe ?cno)))" using qe[rule_format, OF no_qf] by auto finally have "Ifm bs (E p) = Ifm bs (CJNB qe p)" @@ -5298,7 +5298,8 @@ { fix t n assume tnY: "(t,n) \ set ?Y" hence "(t,n) \ set ?SS" by simp hence "\ (t',n') \ set ?S. simp_num_pair (t',n') = (t,n)" - by (auto simp add: split_def) (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) + by (auto simp add: split_def simp del: map_map) + (rule_tac x="((aa,ba),(ab,bb))" in bexI, simp_all) then obtain t' n' where tn'S: "(t',n') \ set ?S" and tns: "simp_num_pair (t',n') = (t,n)" by blast from tn'S Snb have tnb: "numbound0 t'" and np: "n' > 0" by auto from simp_num_pair_l[OF tnb np tns] diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Thu Nov 12 14:31:29 2009 -0800 @@ -1233,7 +1233,7 @@ also have "\ = (\x. (Ifm vs (y#bs) ?cyes) \ (Ifm vs (x#bs) ?cno))" using bound0_I[OF yes_nb, where bs="bs" and b'="y"] by blast also have "\ = (Ifm vs bs (decr0 ?cyes) \ Ifm vs bs (E ?cno))" - by (auto simp add: decr0[OF yes_nb]) + by (auto simp add: decr0[OF yes_nb] simp del: partition_filter_conv) also have "\ = (Ifm vs bs (conj (decr0 ?cyes) (qe ?cno)))" using qe[rule_format, OF no_qf] by auto finally have "Ifm vs bs (E p) = Ifm vs bs (CJNB qe p)" diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Imperative_HOL/Heap.thy --- a/src/HOL/Imperative_HOL/Heap.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Imperative_HOL/Heap.thy Thu Nov 12 14:31:29 2009 -0800 @@ -231,7 +231,7 @@ the literature? *} lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" - by (simp add: get_array_def set_array_def) + by (simp add: get_array_def set_array_def o_def) lemma array_get_set_neq [simp]: "r =!!= s \ get_array r (set_array s x h) = get_array r h" by (simp add: noteq_arrs_def get_array_def set_array_def) diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Import/HOL/rich_list.imp --- a/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Import/HOL/rich_list.imp Thu Nov 12 14:31:29 2009 -0800 @@ -130,7 +130,7 @@ "MAP_o" > "HOL4Base.rich_list.MAP_o" "MAP_SNOC" > "HOL4Base.rich_list.MAP_SNOC" "MAP_REVERSE" > "List.rev_map" - "MAP_MAP_o" > "List.map_compose" + "MAP_MAP_o" > "List.map_map" "MAP_FOLDR" > "HOL4Base.rich_list.MAP_FOLDR" "MAP_FOLDL" > "HOL4Base.rich_list.MAP_FOLDL" "MAP_FLAT" > "List.map_concat" diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Integration.thy --- a/src/HOL/Integration.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Integration.thy Thu Nov 12 14:31:29 2009 -0800 @@ -542,7 +542,7 @@ apply (erule subst) apply (subst listsum_subtractf [symmetric]) apply (rule listsum_abs [THEN order_trans]) - apply (subst map_compose [symmetric, unfolded o_def]) + apply (subst map_map [unfolded o_def]) apply (subgoal_tac "e = (\(u, x, v)\D. (e / (b - a)) * (v - u))") apply (erule ssubst) apply (simp add: abs_minus_commute) diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Lambda/StrongNorm.thy --- a/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 14:31:29 2009 -0800 @@ -186,7 +186,7 @@ by (rule typing.App) qed with Cons True show ?thesis - by (simp add: map_compose [symmetric] comp_def) + by (simp add: comp_def) qed next case False diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Lambda/WeakNorm.thy --- a/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Lambda/WeakNorm.thy Thu Nov 12 14:31:29 2009 -0800 @@ -148,7 +148,7 @@ hence "e\0:Ts \ T'\ \ map (\t. lift t 0) (map (\t. t[u/i]) as) : Ts" by (rule lift_types) thus "e\0:Ts \ T'\ \ map (\t. lift (t[u/i]) 0) as : Ts" - by (simp_all add: map_compose [symmetric] o_def) + by (simp_all add: o_def) qed with asred show "e\0:Ts \ T'\ \ Var 0 \\ map (\t. lift t 0) as' : T'" by (rule subject_reduction') @@ -167,7 +167,7 @@ also note rred finally have "(Var 0 \\ map (\t. lift (t[u/i]) 0) as)[u \ a[u/i]/0] \\<^sub>\\<^sup>* r" . with rnf Cons eq show ?thesis - by (simp add: map_compose [symmetric] o_def) iprover + by (simp add: o_def) iprover qed next assume neq: "x \ i" diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Library/Countable.thy Thu Nov 12 14:31:29 2009 -0800 @@ -165,7 +165,7 @@ text {* Lists *} lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs" - by (simp add: comp_def map_compose [symmetric]) + by (simp add: comp_def) primrec list_encode :: "'a\countable list \ nat" diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Library/Enum.thy Thu Nov 12 14:31:29 2009 -0800 @@ -10,7 +10,7 @@ class enum = fixes enum :: "'a list" - assumes UNIV_enum [code]: "UNIV = set enum" + assumes UNIV_enum: "UNIV = set enum" and enum_distinct: "distinct enum" begin @@ -72,7 +72,7 @@ by (induct n) simp_all lemma length_n_lists: "length (n_lists n xs) = length xs ^ n" - by (induct n) (auto simp add: length_concat map_compose [symmetric] o_def listsum_triv) + by (induct n) (auto simp add: length_concat o_def listsum_triv) lemma length_n_lists_elem: "ys \ set (n_lists n xs) \ length ys = n" by (induct n arbitrary: ys) auto @@ -114,10 +114,6 @@ by (simp add: length_n_lists) qed -lemma map_of_zip_map: (*FIXME move to Map.thy*) - "map_of (zip xs (map f xs)) = (\x. if x \ set xs then Some (f x) else None)" - by (induct xs) (simp_all add: expand_fun_eq) - lemma map_of_zip_enum_is_Some: assumes "length ys = length (enum \ 'a\enum list)" shows "\y. map_of (zip (enum \ 'a\enum list) ys) x = Some y" @@ -250,7 +246,7 @@ by (auto simp add: image_def) have "set (map set (sublists xs)) = Pow (set xs)" by (induct xs) - (simp_all add: aux Let_def Pow_insert Un_commute) + (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map) then show ?thesis by simp qed diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Library/Mapping.thy Thu Nov 12 14:31:29 2009 -0800 @@ -128,7 +128,7 @@ lemma bulkload_tabulate: "bulkload xs = tabulate [0.. True" | "sorted (x#y#zs) \ x <= y \ sorted (y#zs)" -primrec insort :: "'a \ 'a list \ 'a list" where -"insort x [] = [x]" | -"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))" - -primrec sort :: "'a list \ 'a list" where -"sort [] = []" | -"sort (x#xs) = insort x (sort xs)" +primrec insort_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where +"insort_key f x [] = [x]" | +"insort_key f x (y#ys) = (if f x \ f y then (x#y#ys) else y#(insort_key f x ys))" + +primrec sort_key :: "('b \ 'a) \ 'b list \ 'b list" where +"sort_key f [] = []" | +"sort_key f (x#xs) = insort_key f x (sort_key f xs)" + +abbreviation "sort \ sort_key (\x. x)" +abbreviation "insort \ insort_key (\x. x)" end @@ -698,8 +701,8 @@ lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys" by (induct xs) auto -lemma map_compose: "map (f o g) xs = map f (map g xs)" -by (induct xs) (auto simp add: o_def) +lemma map_map [simp]: "map f (map g xs) = map (f \ g) xs" +by (induct xs) auto lemma rev_map: "rev (map f xs) = map f (rev xs)" by (induct xs) auto @@ -1183,6 +1186,12 @@ then show ?thesis by (auto simp add: partition_filter1 partition_filter2) qed +lemma partition_filter_conv[simp]: + "partition f xs = (filter f xs,filter (Not o f) xs)" +unfolding partition_filter2[symmetric] +unfolding partition_filter1[symmetric] by simp + +declare partition.simps[simp del] subsubsection {* @{text concat} *} @@ -1722,6 +1731,9 @@ subsubsection {* @{text takeWhile} and @{text dropWhile} *} +lemma length_takeWhile_le: "length (takeWhile P xs) \ length xs" + by (induct xs) auto + lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs" by (induct xs) auto @@ -1736,6 +1748,15 @@ lemma takeWhile_tail: "\ P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs" by (induct xs) auto +lemma takeWhile_nth: "j < length (takeWhile P xs) \ takeWhile P xs ! j = xs ! j" +apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto + +lemma dropWhile_nth: "j < length (dropWhile P xs) \ dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))" +apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto + +lemma length_dropWhile_le: "length (dropWhile P xs) \ length xs" +by (induct xs) auto + lemma dropWhile_append1 [simp]: "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" by (induct xs) auto @@ -1765,6 +1786,66 @@ lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)" by (induct xs) auto +lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \ f) xs)" +by (induct xs) auto + +lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \ f) xs)" +by (induct xs) auto + +lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs" +by (induct xs) auto + +lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs" +by (induct xs) auto + +lemma hd_dropWhile: + "dropWhile P xs \ [] \ \ P (hd (dropWhile P xs))" +using assms by (induct xs) auto + +lemma takeWhile_eq_filter: + assumes "\ x. x \ set (dropWhile P xs) \ \ P x" + shows "takeWhile P xs = filter P xs" +proof - + have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)" + by simp + have B: "filter P (dropWhile P xs) = []" + unfolding filter_empty_conv using assms by blast + have "filter P xs = takeWhile P xs" + unfolding A filter_append B + by (auto simp add: filter_id_conv dest: set_takeWhileD) + thus ?thesis .. +qed + +lemma takeWhile_eq_take_P_nth: + "\ \ i. \ i < n ; i < length xs \ \ P (xs ! i) ; n < length xs \ \ P (xs ! n) \ \ + takeWhile P xs = take n xs" +proof (induct xs arbitrary: n) + case (Cons x xs) + thus ?case + proof (cases n) + case (Suc n') note this[simp] + have "P x" using Cons.prems(1)[of 0] by simp + moreover have "takeWhile P xs = take n' xs" + proof (rule Cons.hyps) + case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp + next case goal2 thus ?case using Cons by auto + qed + ultimately show ?thesis by simp + qed simp +qed simp + +lemma nth_length_takeWhile: + "length (takeWhile P xs) < length xs \ \ P (xs ! length (takeWhile P xs))" +by (induct xs) auto + +lemma length_takeWhile_less_P_nth: + assumes all: "\ i. i < j \ P (xs ! i)" and "j \ length xs" + shows "j \ length (takeWhile P xs)" +proof (rule classical) + assume "\ ?thesis" + hence "length (takeWhile P xs) < length xs" using assms by simp + thus ?thesis using all `\ ?thesis` nth_length_takeWhile[of P xs] by auto +qed text{* The following two lemmmas could be generalized to an arbitrary property. *} @@ -1838,19 +1919,32 @@ "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" by (induct rule:list_induct2, simp_all) +lemma zip_map_map: + "zip (map f xs) (map g ys) = map (\ (x, y). (f x, g y)) (zip xs ys)" +proof (induct xs arbitrary: ys) + case (Cons x xs) note Cons_x_xs = Cons.hyps + show ?case + proof (cases ys) + case (Cons y ys') + show ?thesis unfolding Cons using Cons_x_xs by simp + qed simp +qed simp + +lemma zip_map1: + "zip (map f xs) ys = map (\(x, y). (f x, y)) (zip xs ys)" +using zip_map_map[of f xs "\x. x" ys] by simp + +lemma zip_map2: + "zip xs (map f ys) = map (\(x, y). (x, f y)) (zip xs ys)" +using zip_map_map[of "\x. x" xs f ys] by simp + lemma map_zip_map: - "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)" -apply(induct xs arbitrary:ys) apply simp -apply(case_tac ys) -apply simp_all -done + "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)" +unfolding zip_map1 by auto lemma map_zip_map2: - "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)" -apply(induct xs arbitrary:ys) apply simp -apply(case_tac ys) -apply simp_all -done + "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)" +unfolding zip_map2 by auto text{* Courtesy of Andreas Lochbihler: *} lemma zip_same_conv_map: "zip xs xs = map (\x. (x, x)) xs" @@ -1867,6 +1961,9 @@ "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}" by(simp add: set_conv_nth cong: rev_conj_cong) +lemma zip_same: "((a,b) \ set (zip xs xs)) = (a \ set xs \ a = b)" +by(induct xs) auto + lemma zip_update: "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]" by(rule sym, simp add: update_zip) @@ -1893,6 +1990,16 @@ apply (case_tac ys, simp_all) done +lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \ fst) (zip xs ys)" +proof (induct xs arbitrary: ys) + case (Cons x xs) thus ?case by (cases ys) auto +qed simp + +lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \ snd) (zip xs ys)" +proof (induct xs arbitrary: ys) + case (Cons x xs) thus ?case by (cases ys) auto +qed simp + lemma set_zip_leftD: "(x,y)\ set (zip xs ys) \ x \ set xs" by (induct xs ys rule:list_induct2') auto @@ -1913,6 +2020,35 @@ "length xs = length ys \ zip xs ys = zs \ map fst zs = xs \ map snd zs = ys" by (auto simp add: zip_map_fst_snd) +lemma distinct_zipI1: + "distinct xs \ distinct (zip xs ys)" +proof (induct xs arbitrary: ys) + case (Cons x xs) + show ?case + proof (cases ys) + case (Cons y ys') + have "(x, y) \ set (zip xs ys')" + using Cons.prems by (auto simp: set_zip) + thus ?thesis + unfolding Cons zip_Cons_Cons distinct.simps + using Cons.hyps Cons.prems by simp + qed simp +qed simp + +lemma distinct_zipI2: + "distinct xs \ distinct (zip xs ys)" +proof (induct xs arbitrary: ys) + case (Cons x xs) + show ?case + proof (cases ys) + case (Cons y ys') + have "(x, y) \ set (zip xs ys')" + using Cons.prems by (auto simp: set_zip) + thus ?thesis + unfolding Cons zip_Cons_Cons distinct.simps + using Cons.hyps Cons.prems by simp + qed simp +qed simp subsubsection {* @{text list_all2} *} @@ -2259,6 +2395,12 @@ lemma length_concat: "length (concat xss) = listsum (map length xss)" by (induct xss) simp_all +lemma listsum_map_filter: + fixes f :: "'a \ 'b \ comm_monoid_add" + assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0" + shows "listsum (map f (filter P xs)) = listsum (map f xs)" +using assms by (induct xs) auto + text{* For efficient code generation --- @{const listsum} is not tail recursive but @{const foldl} is. *} lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs" @@ -2640,6 +2782,11 @@ "length(remdups(concat xss)) = card(\xs \ set xss. set xs)" by(simp add: set_concat distinct_card[symmetric]) +lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)" +proof - + have xs: "concat[xs] = xs" by simp + from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp +qed subsubsection {* @{text remove1} *} @@ -3083,6 +3230,12 @@ context linorder begin +lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)" +by (induct xs, auto) + +lemma length_sort[simp]: "length (sort_key f xs) = length xs" +by (induct xs, auto) + lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))" apply(induct xs arbitrary: x) apply simp by simp (blast intro: order_trans) @@ -3092,37 +3245,88 @@ by (induct xs) (auto simp add:sorted_Cons) lemma sorted_nth_mono: - "sorted xs \ i <= j \ j < length xs \ xs!i <= xs!j" + "sorted xs \ i \ j \ j < length xs \ xs!i \ xs!j" by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons) -lemma set_insort: "set(insort x xs) = insert x (set xs)" +lemma sorted_rev_nth_mono: + "sorted (rev xs) \ i \ j \ j < length xs \ xs!j \ xs!i" +using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"] + rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"] +by auto + +lemma sorted_nth_monoI: + "(\ i j. \ i \ j ; j < length xs \ \ xs ! i \ xs ! j) \ sorted xs" +proof (induct xs) + case (Cons x xs) + have "sorted xs" + proof (rule Cons.hyps) + fix i j assume "i \ j" and "j < length xs" + with Cons.prems[of "Suc i" "Suc j"] + show "xs ! i \ xs ! j" by auto + qed + moreover + { + fix y assume "y \ set xs" + then obtain j where "j < length xs" and "xs ! j = y" + unfolding in_set_conv_nth by blast + with Cons.prems[of 0 "Suc j"] + have "x \ y" + by auto + } + ultimately + show ?case + unfolding sorted_Cons by auto +qed simp + +lemma sorted_equals_nth_mono: + "sorted xs = (\j < length xs. \i \ j. xs ! i \ xs ! j)" +by (auto intro: sorted_nth_monoI sorted_nth_mono) + +lemma set_insort: "set(insort_key f x xs) = insert x (set xs)" by (induct xs) auto -lemma set_sort[simp]: "set(sort xs) = set xs" +lemma set_sort[simp]: "set(sort_key f xs) = set xs" by (induct xs) (simp_all add:set_insort) -lemma distinct_insort: "distinct (insort x xs) = (x \ set xs \ distinct xs)" +lemma distinct_insort: "distinct (insort_key f x xs) = (x \ set xs \ distinct xs)" by(induct xs)(auto simp:set_insort) -lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs" +lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs" by(induct xs)(simp_all add:distinct_insort set_sort) +lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)" +by(induct xs)(auto simp:sorted_Cons set_insort) + lemma sorted_insort: "sorted (insort x xs) = sorted xs" -apply (induct xs) - apply(auto simp:sorted_Cons set_insort) -done +using sorted_insort_key[where f="\x. x"] by simp + +theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))" +by(induct xs)(auto simp:sorted_insort_key) theorem sorted_sort[simp]: "sorted (sort xs)" -by (induct xs) (auto simp:sorted_insort) - -lemma insort_is_Cons: "\x\set xs. a \ x \ insort a xs = a # xs" +by(induct xs)(auto simp:sorted_insort) + +lemma insort_is_Cons: "\x\set xs. f a \ f x \ insort_key f a xs = a # xs" by (cases xs) auto lemma sorted_remove1: "sorted xs \ sorted (remove1 a xs)" -by (induct xs, auto simp add: sorted_Cons) +by(induct xs)(auto simp add: sorted_Cons) + +lemma insort_key_remove1: "\ a \ set xs; sorted (map f xs) ; inj_on f (set xs) \ + \ insort_key f a (remove1 a xs) = xs" +proof (induct xs) + case (Cons x xs) + thus ?case + proof (cases "x = a") + case False + hence "f x \ f a" using Cons.prems by auto + hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons) + thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons) + qed (auto simp: sorted_Cons insort_is_Cons) +qed simp lemma insort_remove1: "\ a \ set xs; sorted xs \ \ insort a (remove1 a xs) = xs" -by (induct xs, auto simp add: sorted_Cons insort_is_Cons) +using insort_key_remove1[where f="\x. x"] by simp lemma sorted_remdups[simp]: "sorted l \ sorted (remdups l)" @@ -3178,6 +3382,11 @@ case 3 then show ?case by (cases n) simp_all qed +lemma sorted_dropWhile: "sorted xs \ sorted (dropWhile P xs)" + unfolding dropWhile_eq_drop by (rule sorted_drop) + +lemma sorted_takeWhile: "sorted xs \ sorted (takeWhile P xs)" + apply (subst takeWhile_eq_take) by (rule sorted_take) end @@ -3772,6 +3981,12 @@ | "length_unique (x#xs) = (if x \ set xs then length_unique xs else Suc (length_unique xs))" +primrec + concat_map :: "('a => 'b list) => 'a list => 'b list" +where + "concat_map f [] = []" + | "concat_map f (x#xs) = f x @ concat_map f xs" + text {* Only use @{text mem} for generating executable code. Otherwise use @{prop "x : set xs"} instead --- it is much easier to reason about. @@ -3865,7 +4080,11 @@ lemma length_remdups_length_unique [code_unfold]: "length (remdups xs) = length_unique xs" - by (induct xs) simp_all +by (induct xs) simp_all + +lemma concat_map_code[code_unfold]: + "concat(map f xs) = concat_map f xs" +by (induct xs) simp_all declare INFI_def [code_unfold] declare SUPR_def [code_unfold] @@ -3923,6 +4142,11 @@ "setsum f (set [m.. i = 0 ..< length xs. xs ! i)" +using setsum_set_upt_conv_listsum[of "op ! xs" 0 "length xs"] +by (simp add: map_nth) text {* Code for summation over ints. *} diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Map.thy --- a/src/HOL/Map.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Map.thy Thu Nov 12 14:31:29 2009 -0800 @@ -218,6 +218,10 @@ ultimately show ?case by simp qed +lemma map_of_zip_map: + "map_of (zip xs (map f xs)) = (\x. if x \ set xs then Some (f x) else None)" + by (induct xs) (simp_all add: expand_fun_eq) + lemma finite_range_map_of: "finite (range (map_of xys))" apply (induct xys) apply (simp_all add: image_constant) diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/BV/JVM.thy --- a/src/HOL/MicroJava/BV/JVM.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/BV/JVM.thy Thu Nov 12 14:31:29 2009 -0800 @@ -117,11 +117,7 @@ from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def) also from w have "phi' = map OK (map ok_val phi')" - apply (clarsimp simp add: wt_step_def not_Err_eq) - apply (rule map_id [symmetric]) - apply (erule allE, erule impE, assumption) - apply clarsimp - done + by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI) finally have check_types: "check_types G maxs maxr (map OK (map ok_val phi'))" . diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/BV/LBVJVM.thy --- a/src/HOL/MicroJava/BV/LBVJVM.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy Thu Nov 12 14:31:29 2009 -0800 @@ -166,7 +166,7 @@ by (simp add: check_types_def) also from step have [symmetric]: "map OK (map ok_val phi) = phi" - by (auto intro!: map_id simp add: wt_step_def) + by (auto intro!: nth_equalityI simp add: wt_step_def) finally have "check_types G mxs ?mxr (map OK (map ok_val phi))" . } moreover { diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Nov 12 14:31:29 2009 -0800 @@ -269,12 +269,6 @@ (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)" by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def) - -lemma map_id [rule_format]: - "(\n < length xs. f (g (xs!n)) = xs!n) \ map f (map g xs) = xs" - by (induct xs, auto) - - lemma is_type_pTs: "\ wf_prog wf_mb G; (C,S,fs,mdecls) \ set G; ((mn,pTs),rT,code) \ set mdecls \ \ set pTs \ types G" diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/Comp/CorrComp.thy --- a/src/HOL/MicroJava/Comp/CorrComp.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy Thu Nov 12 14:31:29 2009 -0800 @@ -552,7 +552,7 @@ apply (simp only: wf_java_mdecl_def) apply (subgoal_tac "(\y\set pns. y \ set (map fst lvars))") -apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd) +apply (simp add: init_vars_def locvars_xstate_def locvars_locals_def galldefs unique_def split_def map_of_map_as_map_upd del: map_map) apply (intro strip) apply (simp (no_asm_simp) only: append_Cons [THEN sym]) apply (rule progression_lvar_init_aux) diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/Comp/CorrCompTp.thy --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Thu Nov 12 14:31:29 2009 -0800 @@ -132,7 +132,7 @@ apply (case_tac "vname = This") apply (simp add: inited_LT_def) apply (simp add: inited_LT_def) -apply (simp (no_asm_simp) only: map_compose map_append [THEN sym] map.simps [THEN sym]) +apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] map.simps [symmetric]) apply (subgoal_tac "length (takeWhile (\z. z \ vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)") apply (simp (no_asm_simp) only: List.nth_map ok_val.simps) apply (subgoal_tac "map_of lvars = map_of (map (\ p. (fst p, snd p)) lvars)") @@ -166,7 +166,7 @@ lemma inited_LT_at_index_no_err: " i < length (inited_LT C pTs lvars) \ inited_LT C pTs lvars ! i \ Err" apply (simp only: inited_LT_def) -apply (simp only: map_compose map_append [THEN sym] map.simps [THEN sym] length_map) +apply (simp only: map_map [symmetric] map_append [symmetric] map.simps [symmetric] length_map) apply (simp only: nth_map) apply simp done diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/Comp/LemmasComp.thy --- a/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Thu Nov 12 14:31:29 2009 -0800 @@ -68,7 +68,7 @@ with fst_eq Cons show "unique (map f (a # list)) = unique (a # list)" - by (simp add: unique_def fst_set) + by (simp add: unique_def fst_set image_compose) qed qed @@ -292,7 +292,7 @@ apply (simp add: method_def) apply (frule wf_subcls1) apply (simp add: comp_class_rec) -apply (simp add: map_compose [THEN sym] split_iter split_compose del: map_compose) +apply (simp add: split_iter split_compose map_map[symmetric] del: map_map) apply (rule_tac R="%x y. ((x S) = (Option.map (\(D, rT, b). (D, rT, snd (snd (compMethod G D (S, rT, b))))) (y S)))" in class_rec_relation) @@ -311,7 +311,7 @@ apply (simp add: split_beta compMethod_def) apply (simp add: map_of_map [THEN sym]) apply (simp add: split_beta) -apply (simp add: map_compose [THEN sym] Fun.comp_def split_beta) +apply (simp add: Fun.comp_def split_beta) apply (subgoal_tac "(\x\(vname list \ fdecl list \ stmt \ expr) mdecl. (fst x, Object, snd (compMethod G Object diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 12 14:31:29 2009 -0800 @@ -284,8 +284,7 @@ apply (frule fields_rec, assumption) apply (rule HOL.trans) apply (simp add: o_def) -apply (simp (no_asm_use) - add: split_beta split_def o_def map_compose [THEN sym] del: map_compose) +apply (simp (no_asm_use) add: split_beta split_def o_def) done lemma method_Object [simp]: diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Predicate.thy Thu Nov 12 14:31:29 2009 -0800 @@ -828,28 +828,6 @@ code_abort not_unique -text {* dummy setup for @{text code_pred} and @{text values} keywords *} - -ML {* -local - -structure P = OuterParse; - -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; - -in - -val _ = OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate" - OuterKeyword.thy_goal (P.term_group >> (K (Proof.theorem_i NONE (K I) [[]]))); - -val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" - OuterKeyword.diag ((opt_modes -- P.term) - >> (fn (modes, t) => Toplevel.no_timing o Toplevel.keep - (K ()))); - -end -*} - no_notation inf (infixl "\" 70) and sup (infixl "\" 65) and diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Product_Type.thy Thu Nov 12 14:31:29 2009 -0800 @@ -777,7 +777,7 @@ "apfst f (x, y) = (f x, y)" by (simp add: apfst_def) -lemma upd_snd_conv [simp, code]: +lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)" by (simp add: apsnd_def) @@ -829,6 +829,9 @@ "apsnd f x = apsnd g x \ f (snd x) = g (snd x)" by (cases x) simp +lemma apsnd_apfst_commute: + "apsnd f (apfst g p) = apfst g (apsnd f p)" + by simp text {* Disjoint union of a family of sets -- Sigma. diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Nitpick/HISTORY Thu Nov 12 14:31:29 2009 -0800 @@ -10,7 +10,7 @@ * Optimized Kodkod encoding of datatypes whose constructors don't appear in the formula to falsify * Added support for codatatype view of datatypes - * Fixed soundness bug related to sets of sets + * Fixed soundness bugs related to sets and sets of sets * Fixed monotonicity check * Fixed error in display of uncurried constants * Speeded up scope enumeration diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 12 14:31:29 2009 -0800 @@ -1448,7 +1448,7 @@ fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel | Op2 (Apply, _, R, u1, u2) => if is_Cst Unrep u2 andalso is_set_type (type_of u1) - andalso not (is_opt_rep (rep_of u1)) then + andalso is_FreeName u1 then false_atom else to_apply R u1 u2 diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Nov 12 14:31:29 2009 -0800 @@ -96,6 +96,7 @@ val nickname_of : nut -> string val is_skolem_name : nut -> bool val is_eval_name : nut -> bool + val is_FreeName : nut -> bool val is_Cst : cst -> nut -> bool val fold_nut : (nut -> 'a -> 'a) -> nut -> 'a -> 'a val map_nut : (nut -> nut) -> nut -> nut @@ -367,6 +368,8 @@ fun is_eval_name u = String.isPrefix eval_prefix (nickname_of u) handle NUT ("Nitpick_Nut.nickname_of", _) => false +fun is_FreeName (FreeName _) = true + | is_FreeName _ = false (* cst -> nut -> bool *) fun is_Cst cst (Cst (cst', _, _)) = (cst = cst') | is_Cst _ _ = false @@ -764,9 +767,8 @@ (* A nut is said to be constructive if whenever it evaluates to unknown in our three-valued logic, it would evaluate to a unrepresentable value ("unrep") - according to the HOL semantics. For example, "Suc n" is - constructive if "n" is representable or "Unrep", because unknown implies - unrep. *) + according to the HOL semantics. For example, "Suc n" is constructive if "n" + is representable or "Unrep", because unknown implies unrep. *) (* nut -> bool *) fun is_constructive u = is_Cst Unrep u orelse @@ -830,13 +832,9 @@ else if is_Cst Unrep u2 then if is_constructive u1 then Cst (Unrep, T, R) - else if is_boolean_type T andalso not (is_opt_rep (rep_of u1)) then - (* Selectors are an unfortunate exception to the rule that non-"Opt" - predicates return "False" for unrepresentable domain values. *) - case u1 of - ConstName (s, _, _) => if is_sel s then unknown_boolean T R - else Cst (False, T, Formula Neut) - | _ => Cst (False, T, Formula Neut) + else if is_boolean_type T then + if is_FreeName u1 then Cst (False, T, Formula Neut) + else unknown_boolean T R else case u1 of Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) => Cst (Unrep, T, R) diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Nov 12 14:31:29 2009 -0800 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/Predicate_Compile/predicate_compile.ML Author: Lukas Bulwahn, TU Muenchen -FIXME. +Entry point for the predicate compiler; definition of Toplevel commands code_pred and values *) signature PREDICATE_COMPILE = @@ -10,7 +10,7 @@ val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory end; -structure Predicate_Compile : PREDICATE_COMPILE = +structure Predicate_Compile (*: PREDICATE_COMPILE*) = struct (* options *) @@ -105,12 +105,16 @@ (Graph.strong_conn gr) thy end -fun extract_options ((modes, raw_options), const) = +fun extract_options (((expected_modes, proposed_modes), raw_options), const) = let fun chk s = member (op =) raw_options s in Options { - expected_modes = Option.map (pair const) modes, + expected_modes = Option.map (pair const) expected_modes, + proposed_modes = if not (null proposed_modes) then [(const, map fst proposed_modes)] else [], + proposed_names = + map_filter + (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name)) proposed_modes, show_steps = chk "show_steps", show_intermediate_results = chk "show_intermediate_results", show_proof_trace = chk "show_proof_trace", @@ -125,17 +129,18 @@ } end -fun code_pred_cmd ((modes, raw_options), raw_const) lthy = +fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy = let val thy = ProofContext.theory_of lthy val const = Code.read_const thy raw_const - val options = extract_options ((modes, raw_options), const) + val options = extract_options (((expected_modes, proposed_modes), raw_options), const) in if (is_inductify options) then let val lthy' = LocalTheory.theory (preprocess options const) lthy |> LocalTheory.checkpoint - val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of + val const = + case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of SOME c => c | NONE => const val _ = print_step options "Starting Predicate Compile Core..." @@ -146,7 +151,7 @@ Predicate_Compile_Core.code_pred_cmd options raw_const lthy end -val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup +val setup = Predicate_Compile_Core.setup val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes", "show_mode_inference", "show_compilation", "skip_proof", "inductify", "random", "depth_limited", @@ -157,35 +162,25 @@ (* Parser for mode annotations *) -(*val parse_argmode' = P.nat >> rpair NONE || P.$$$ "(" |-- P.enum1 "," --| P.$$$ ")"*) -datatype raw_argmode = Argmode of string | Argmode_Tuple of string list - -val parse_argmode' = - ((Args.$$$ "i" || Args.$$$ "o") >> Argmode) || - (Args.$$$ "(" |-- P.enum1 "," (Args.$$$ "i" || Args.$$$ "o") --| Args.$$$ ")" >> Argmode_Tuple) - -fun mk_numeral_mode ss = flat (map_index (fn (i, s) => if s = "i" then [i + 1] else []) ss) +fun parse_mode_basic_expr xs = + (Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output || + Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs +and parse_mode_tuple_expr xs = + (parse_mode_basic_expr --| Args.$$$ "*" -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr) + xs +and parse_mode_expr xs = + (parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs -val parse_smode' = P.$$$ "[" |-- P.enum1 "," parse_argmode' --| P.$$$ "]" - >> (fn m => flat (map_index - (fn (i, Argmode s) => if s = "i" then [(i + 1, NONE)] else [] - | (i, Argmode_Tuple ss) => [(i + 1, SOME (mk_numeral_mode ss))]) m)) - -val parse_smode = (P.$$$ "[" |-- P.enum "," P.nat --| P.$$$ "]") - >> map (rpair (NONE : int list option)) - -fun gen_parse_mode smode_parser = - (Scan.optional - ((P.enum "=>" ((Args.$$$ "X" >> K NONE) || (smode_parser >> SOME))) --| Args.$$$ "==>") []) - -- smode_parser - -val parse_mode = gen_parse_mode parse_smode - -val parse_mode' = gen_parse_mode parse_smode' +val mode_and_opt_proposal = parse_mode_expr -- + Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE val opt_modes = - Scan.optional (P.$$$ "(" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- - P.enum1 "," (parse_mode || parse_mode') --| P.$$$ ")" >> SOME) NONE + Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |-- + P.enum1 "," mode_and_opt_proposal --| P.$$$ ")") [] + +val opt_expected_modes = + Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |-- + P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE (* Parser for options *) @@ -198,10 +193,10 @@ val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; -val opt_smode = (P.$$$ "_" >> K NONE) || (parse_smode >> SOME) +val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME) val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |-- - P.enum ", " opt_smode --| P.$$$ "]" >> SOME) NONE + P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE val value_options = let @@ -217,7 +212,8 @@ val _ = OuterSyntax.local_theory_to_proof "code_pred" "prove equations for predicate specified by intro/elim rules" - OuterKeyword.thy_goal (opt_modes -- scan_options -- P.term_group >> code_pred_cmd) + OuterKeyword.thy_goal + (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd) val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Nov 12 14:31:29 2009 -0800 @@ -21,6 +21,7 @@ (fn (i, is) => string_of_int i ^ (case is of NONE => "" | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js) +(* FIXME: remove! *) fun string_of_mode (iss, is) = space_implode " -> " (map (fn NONE => "X" @@ -28,10 +29,118 @@ (iss @ [SOME is])); fun string_of_tmode (Mode (predmode, termmode, param_modes)) = - "predmode: " ^ (string_of_mode predmode) ^ + "predmode: " ^ (string_of_mode predmode) ^ (if null param_modes then "" else "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes)) +(* new datatype for mode *) + +datatype mode' = Bool | Input | Output | Pair of mode' * mode' | Fun of mode' * mode' + +(* equality of instantiatedness with respect to equivalences: + Pair Input Input == Input and Pair Output Output == Output *) +fun eq_mode' (Fun (m1, m2), Fun (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4) + | eq_mode' (Pair (m1, m2), Pair (m3, m4)) = eq_mode' (m1, m3) andalso eq_mode' (m2, m4) + | eq_mode' (Pair (m1, m2), Input) = eq_mode' (m1, Input) andalso eq_mode' (m2, Input) + | eq_mode' (Pair (m1, m2), Output) = eq_mode' (m1, Output) andalso eq_mode' (m2, Output) + | eq_mode' (Input, Pair (m1, m2)) = eq_mode' (Input, m1) andalso eq_mode' (Input, m2) + | eq_mode' (Output, Pair (m1, m2)) = eq_mode' (Output, m1) andalso eq_mode' (Output, m2) + | eq_mode' (Input, Input) = true + | eq_mode' (Output, Output) = true + | eq_mode' (Bool, Bool) = true + | eq_mode' _ = false + +(* name: binder_modes? *) +fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode' + | strip_fun_mode Bool = [] + | strip_fun_mode _ = error "Bad mode for strip_fun_mode" + +fun dest_fun_mode (Fun (mode, mode')) = mode :: dest_fun_mode mode' + | dest_fun_mode mode = [mode] + +fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode' + | dest_tuple_mode _ = [] + +fun string_of_mode' mode' = + let + fun string_of_mode1 Input = "i" + | string_of_mode1 Output = "o" + | string_of_mode1 Bool = "bool" + | string_of_mode1 mode = "(" ^ (string_of_mode3 mode) ^ ")" + and string_of_mode2 (Pair (m1, m2)) = string_of_mode3 m1 ^ " * " ^ string_of_mode2 m2 + | string_of_mode2 mode = string_of_mode1 mode + and string_of_mode3 (Fun (m1, m2)) = string_of_mode2 m1 ^ " => " ^ string_of_mode3 m2 + | string_of_mode3 mode = string_of_mode2 mode + in string_of_mode3 mode' end + +fun ascii_string_of_mode' mode' = + let + fun ascii_string_of_mode' Input = "i" + | ascii_string_of_mode' Output = "o" + | ascii_string_of_mode' Bool = "b" + | ascii_string_of_mode' (Pair (m1, m2)) = + "P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2 + | ascii_string_of_mode' (Fun (m1, m2)) = + "F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B" + and ascii_string_of_mode'_Fun (Fun (m1, m2)) = + ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2) + | ascii_string_of_mode'_Fun Bool = "B" + | ascii_string_of_mode'_Fun m = ascii_string_of_mode' m + and ascii_string_of_mode'_Pair (Pair (m1, m2)) = + ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2 + | ascii_string_of_mode'_Pair m = ascii_string_of_mode' m + in ascii_string_of_mode'_Fun mode' end + +fun translate_mode T (iss, is) = + let + val Ts = binder_types T + val (Ts1, Ts2) = chop (length iss) Ts + fun translate_smode Ts is = + let + fun translate_arg (i, T) = + case AList.lookup (op =) is (i + 1) of + SOME NONE => Input + | SOME (SOME its) => + let + fun translate_tuple (i, T) = if member (op =) its (i + 1) then Input else Output + in + foldr1 Pair (map_index translate_tuple (HOLogic.strip_tupleT T)) + end + | NONE => Output + in map_index translate_arg Ts end + fun mk_mode arg_modes = foldr1 Fun (arg_modes @ [Bool]) + val param_modes = + map (fn (T, NONE) => Input | (T, SOME is) => mk_mode (translate_smode (binder_types T) is)) + (Ts1 ~~ iss) + in + mk_mode (param_modes @ translate_smode Ts2 is) + end; + +fun translate_mode' nparams mode' = + let + fun err () = error "translate_mode': given mode cannot be translated" + val (m1, m2) = chop nparams (strip_fun_mode mode') + val translate_to_tupled_mode = + (map_filter I) o (map_index (fn (i, m) => + if eq_mode' (m, Input) then SOME (i + 1) + else if eq_mode' (m, Output) then NONE + else err ())) + val translate_to_smode = + (map_filter I) o (map_index (fn (i, m) => + if eq_mode' (m, Input) then SOME (i + 1, NONE) + else if eq_mode' (m, Output) then NONE + else SOME (i + 1, SOME (translate_to_tupled_mode (dest_tuple_mode m))))) + fun translate_to_param_mode m = + case rev (dest_fun_mode m) of + Bool :: _ :: _ => SOME (translate_to_smode (strip_fun_mode m)) + | _ => if eq_mode' (m, Input) then NONE else err () + in + (map translate_to_param_mode m1, translate_to_smode m2) + end + +fun string_of_mode thy constname mode = + string_of_mode' (translate_mode (Sign.the_const_type thy constname) mode) + (* general syntactic functions *) (*Like dest_conj, but flattens conjunctions however nested*) @@ -40,8 +149,6 @@ fun conjuncts t = conjuncts_aux t []; -(* syntactic functions *) - fun is_equationlike_term (Const ("==", _) $ _ $ _) = true | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true | is_equationlike_term _ = false @@ -70,8 +177,23 @@ fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT) | is_predT _ = false - +(* guessing number of parameters *) +fun find_indexes pred xs = + let + fun find is n [] = is + | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs; + in rev (find [] 0 xs) end; + +fun guess_nparams T = + let + val argTs = binder_types T + val nparams = fold Integer.max + (map (fn x => x + 1) (find_indexes is_predT argTs)) 0 + in nparams end; + (*** check if a term contains only constructor functions ***) +(* FIXME: constructor terms are supposed to be seen in the way the code generator + sees constructors.*) fun is_constrt thy = let val cnstrs = flat (maps @@ -159,7 +281,9 @@ (* Different options for compiler *) datatype options = Options of { - expected_modes : (string * mode list) option, + expected_modes : (string * mode' list) option, + proposed_modes : (string * mode' list) list, + proposed_names : ((string * mode') * string) list, show_steps : bool, show_proof_trace : bool, show_intermediate_results : bool, @@ -175,6 +299,10 @@ }; fun expected_modes (Options opt) = #expected_modes opt +fun proposed_modes (Options opt) name = AList.lookup (op =) (#proposed_modes opt) name +fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode') + (#proposed_names opt) (name, mode) + fun show_steps (Options opt) = #show_steps opt fun show_intermediate_results (Options opt) = #show_intermediate_results opt fun show_proof_trace (Options opt) = #show_proof_trace opt @@ -190,6 +318,8 @@ val default_options = Options { expected_modes = NONE, + proposed_modes = [], + proposed_names = [], show_steps = false, show_intermediate_results = false, show_proof_trace = false, diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 12 14:31:29 2009 -0800 @@ -9,7 +9,7 @@ val setup : theory -> theory val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state - val values_cmd : string list -> Predicate_Compile_Aux.smode option list option + val values_cmd : string list -> Predicate_Compile_Aux.mode' option list option -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit val register_predicate : (string * thm list * thm * int) -> theory -> theory val register_intros : string * thm list -> theory -> theory @@ -36,7 +36,7 @@ val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref - val code_pred_intros_attrib : attribute + val code_pred_intro_attrib : attribute (* used by Quickcheck_Generator *) (* temporary for testing of the compilation *) datatype compilation_funs = CompilationFuns of { @@ -128,32 +128,25 @@ (* destruction of intro rules *) (* FIXME: look for other place where this functionality was used before *) -fun strip_intro_concl nparams intro = let - val _ $ u = Logic.strip_imp_concl intro - val (pred, all_args) = strip_comb u - val (params, args) = chop nparams all_args -in (pred, (params, args)) end +fun strip_intro_concl nparams intro = + let + val _ $ u = Logic.strip_imp_concl intro + val (pred, all_args) = strip_comb u + val (params, args) = chop nparams all_args + in (pred, (params, args)) end (** data structures **) -(* new datatype for modes: *) -(* -datatype instantiation = Input | Output -type arg_mode = Tuple of instantiation list | Atom of instantiation | HigherOrderMode of mode -type mode = arg_mode list -type tmode = Mode of mode * -*) - fun gen_split_smode (mk_tuple, strip_tuple) smode ts = let fun split_tuple' _ _ [] = ([], []) | split_tuple' is i (t::ts) = - (if i mem is then apfst else apsnd) (cons t) + (if member (op =) is i then apfst else apsnd) (cons t) (split_tuple' is (i+1) ts) fun split_tuple is t = split_tuple' is 1 (strip_tuple t) fun split_smode' _ _ [] = ([], []) | split_smode' smode i (t::ts) = - (if i mem (map fst smode) then + (if member (op =) (map fst smode) i then case (the (AList.lookup (op =) smode i)) of NONE => apfst (cons t) | SOME is => @@ -274,7 +267,7 @@ (AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode) fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode - of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ + of NONE => error ("No function defined for mode " ^ string_of_mode thy name mode ^ " of predicate " ^ name) | SOME data => data; @@ -291,7 +284,7 @@ (AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode) fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of - NONE => error ("No random function defined for mode " ^ string_of_mode mode ^ + NONE => error ("No random function defined for mode " ^ string_of_mode thy name mode ^ " of predicate " ^ name) | SOME data => data @@ -310,7 +303,7 @@ fun the_depth_limited_function_data thy name mode = case lookup_depth_limited_function_data thy name mode of - NONE => error ("No depth-limited function defined for mode " ^ string_of_mode mode + NONE => error ("No depth-limited function defined for mode " ^ string_of_mode thy name mode ^ " of predicate " ^ name) | SOME data => data @@ -325,7 +318,7 @@ (AList.lookup (op =) (snd (#annotated_functions (the_pred_data thy name))) mode) fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name mode - of NONE => error ("No annotated function defined for mode " ^ string_of_mode mode + of NONE => error ("No annotated function defined for mode " ^ string_of_mode thy name mode ^ " of predicate " ^ name) | SOME data => data @@ -337,17 +330,17 @@ (* diagnostic display functions *) -fun print_modes options modes = +fun print_modes options thy modes = if show_modes options then tracing ("Inferred modes:\n" ^ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map - string_of_mode ms)) modes)) + (string_of_mode thy s) ms)) modes)) else () fun print_pred_mode_table string_of_entry thy pred_mode_table = let - fun print_mode pred (mode, entry) = "mode : " ^ (string_of_mode mode) - ^ (string_of_entry pred mode entry) + fun print_mode pred (mode, entry) = "mode : " ^ string_of_mode thy pred mode + ^ string_of_entry pred mode entry fun print_pred (pred, modes) = "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes) val _ = tracing (cat_lines (map print_pred pred_mode_table)) @@ -417,25 +410,29 @@ fun print (pred, modes) u = let val _ = writeln ("predicate: " ^ pred) - val _ = writeln ("modes: " ^ (commas (map string_of_mode modes))) - in u end + val _ = writeln ("modes: " ^ (commas (map (string_of_mode thy pred) modes))) + in u end in fold print (all_modes_of thy) () end (* validity checks *) -fun check_expected_modes (options : Predicate_Compile_Aux.options) modes = - case expected_modes options of - SOME (s, ms) => (case AList.lookup (op =) modes s of - SOME modes => - if not (eq_set (op =) (ms, modes)) then - error ("expected modes were not inferred:\n" - ^ "inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes) - ^ "\n expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms)) - else () - | NONE => ()) - | NONE => () +fun check_expected_modes preds (options : Predicate_Compile_Aux.options) modes = + case expected_modes options of + SOME (s, ms) => (case AList.lookup (op =) modes s of + SOME modes => + let + val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes + in + if not (eq_set eq_mode' (ms, modes')) then + error ("expected modes were not inferred:\n" + ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes') ^ "\n" + ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms)) + else () + end + | NONE => ()) + | NONE => () (* importing introduction rules *) @@ -464,7 +461,7 @@ val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred)) val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i)) (1 upto nparams)) ctxt' - val params = map Free (param_names ~~ paramTs) + val params = map2 (curry Free) param_names paramTs in (((outp_pred, params), []), ctxt') end | import_intros inp_pred nparams (th :: ths) ctxt = let @@ -511,7 +508,7 @@ let val (_, (_, args)) = strip_intro_concl nparams intro val prems = Logic.strip_imp_prems intro - val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args) + val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args val frees = (fold o fold_aterms) (fn t as Free _ => if member (op aconv) params t then I else insert (op aconv) t @@ -567,25 +564,6 @@ Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt) end; -(* special case: predicate with no introduction rule *) -fun noclause thy predname elim = let - val T = (Logic.unvarifyT o Sign.the_const_type thy) predname - val Ts = binder_types T - val names = Name.variant_list [] - (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts))) - val vs = map2 (curry Free) names Ts - val clausehd = HOLogic.mk_Trueprop (list_comb (Const (predname, T), vs)) - val intro_t = Logic.mk_implies (@{prop False}, clausehd) - val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)) - val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P) - val intro = Goal.prove (ProofContext.init thy) names [] intro_t - (fn _ => etac @{thm FalseE} 1) - val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t - (fn _ => etac elim 1) -in - ([intro], elim) -end - fun expand_tuples_elim th = th (* updaters *) @@ -617,7 +595,6 @@ val elim = (Drule.standard o Skip_Proof.make_thm thy) (mk_casesrule (ProofContext.init thy) pred nparams intros) - val (intros, elim) = (*if null intros then noclause thy name elim else*) (intros, elim) in mk_pred_data ((intros, SOME elim, nparams), no_compilation) end @@ -653,23 +630,10 @@ end; *) -(* guessing number of parameters *) -fun find_indexes pred xs = - let - fun find is n [] = is - | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs; - in rev (find [] 0 xs) end; - -fun guess_nparams T = +fun add_intro thm thy = let - val argTs = binder_types T - val nparams = fold Integer.max - (map (fn x => x + 1) (find_indexes is_predT argTs)) 0 - in nparams end; - -fun add_intro thm thy = let - val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) - fun cons_intro gr = + val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) + fun cons_intro gr = case try (Graph.get_node gr) name of SOME pred_data => Graph.map_node name (map_pred_data (apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr @@ -680,13 +644,15 @@ in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end; in PredData.map cons_intro thy end -fun set_elim thm = let +fun set_elim thm = + let val (name, _) = dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm))))) fun set (intros, _, nparams) = (intros, SOME thm, nparams) in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end -fun set_nparams name nparams = let +fun set_nparams name nparams = + let fun set (intros, elim, _ ) = (intros, elim, nparams) in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end @@ -974,7 +940,6 @@ (iss ~~ args1))) end end)) (AList.lookup op = modes name) - in case strip_comb (Envir.eta_contract t) of (Const (name, _), args) => the_default default (mk_modes name args) @@ -1081,7 +1046,7 @@ if show_mode_inference options then let val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^ - p ^ " violates mode " ^ string_of_mode m) + p ^ " violates mode " ^ string_of_mode thy p m) val _ = tracing (string_of_clause thy p (nth rs i)) in () end else () @@ -1170,10 +1135,6 @@ | mk_Eval_of additional_arguments ((x, T), SOME mode) names = let val Ts = binder_types T - (*val argnames = Name.variant_list names - (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); - val args = map Free (argnames ~~ Ts) - val (inargs, outargs) = split_smode mode args*) fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t | mk_split_lambda [x] t = lambda x t | mk_split_lambda xs t = @@ -1200,7 +1161,7 @@ val vnames = Name.variant_list names (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j) (1 upto length Ts)) - val args = map Free (vnames ~~ Ts) + val args = map2 (curry Free) vnames Ts fun split_args (i, arg) (ins, outs) = if member (op =) pis i then (arg::ins, outs) @@ -1289,18 +1250,18 @@ let val names = Term.add_free_names t []; val Ts = binder_types (fastype_of t); - val vs = map Free - (Name.variant_list names (replicate (length Ts) "x") ~~ Ts) + val vs = map2 (curry Free) + (Name.variant_list names (replicate (length Ts) "x")) Ts in fold_rev lambda vs (f (list_comb (t, vs))) end; -fun compile_param compilation_modifiers compfuns thy (NONE, t) = t - | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms)), t) = +fun compile_param compilation_modifiers compfuns thy NONE t = t + | compile_param compilation_modifiers compfuns thy (m as SOME (Mode (mode, _, ms))) t = let val (f, args) = strip_comb (Envir.eta_contract t) val (params, args') = chop (length ms) args - val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) + val params' = map2 (compile_param compilation_modifiers compfuns thy) ms params val f' = case f of Const (name, T) => Const (Comp_Mod.function_name_of compilation_modifiers thy name mode, @@ -1316,7 +1277,7 @@ case strip_comb t of (Const (name, T), params) => let - val params' = map (compile_param compilation_modifiers compfuns thy) (ms ~~ params) + val params' = map2 (compile_param compilation_modifiers compfuns thy) ms params val name' = Comp_Mod.function_name_of compilation_modifiers thy name mode val T' = Comp_Mod.funT_of compilation_modifiers compfuns mode T in @@ -1428,8 +1389,12 @@ val vnames = Name.variant_list (all_vs @ param_vs) (map (fn j => "x" ^ string_of_int i ^ "p" ^ string_of_int j) pis) - in if null pis then [] - else [HOLogic.mk_tuple (map Free (vnames ~~ map (fn j => nth Ts (j - 1)) pis))] end + in + if null pis then + [] + else + [HOLogic.mk_tuple (map2 (curry Free) vnames (map (fn j => nth Ts (j - 1)) pis))] + end val in_ts = maps mk_input_term (snd mode) val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1' val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers @@ -1472,7 +1437,7 @@ map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1 val param_names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1))); - val params = map Free (param_names ~~ Ts1') + val params = map2 (curry Free) param_names Ts1' fun mk_args (i, T) argnames = let val vname = Name.variant (param_names @ argnames) ("x" ^ string_of_int (length Ts1' + i)) @@ -1490,17 +1455,17 @@ val vnames = Name.variant_list (param_names @ argnames) (map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j) (1 upto (length Ts))) - in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ argnames) end + in (HOLogic.mk_tuple (map2 (curry Free) vnames Ts), vnames @ argnames) end end val (args, argnames) = fold_map mk_args (1 upto (length Ts2) ~~ Ts2) [] val (inargs, outargs) = split_smode is args val param_names' = Name.variant_list (param_names @ argnames) (map (fn i => "p" ^ string_of_int i) (1 upto (length iss))) - val param_vs = map Free (param_names' ~~ Ts1) + val param_vs = map2 (curry Free) param_names' Ts1 val (params', names) = fold_map (mk_Eval_of []) ((params ~~ Ts1) ~~ iss) [] val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ args)) val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ args)) - val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params') + val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) param_vs params' val funargs = params @ inargs val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs), if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs)) @@ -1520,24 +1485,20 @@ (introthm, elimthm) end; -fun create_constname_of_mode thy prefix name mode = +fun create_constname_of_mode options thy prefix name T mode = let - fun string_of_mode mode = if null mode then "0" - else space_implode "_" - (map (fn (i, NONE) => string_of_int i | (i, SOME pis) => string_of_int i ^ "p" - ^ space_implode "p" (map string_of_int pis)) mode) - val HOmode = space_implode "_and_" - (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) []) + val system_proposal = prefix ^ (Long_Name.base_name name) + ^ "_" ^ ascii_string_of_mode' (translate_mode T mode) + val name = the_default system_proposal (proposed_names options name (translate_mode T mode)) in - (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^ - (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode)) + Sign.full_bname thy name end; fun split_tupleT is T = let fun split_tuple' _ _ [] = ([], []) | split_tuple' is i (T::Ts) = - (if i mem is then apfst else apsnd) (cons T) + (if member (op =) is i then apfst else apsnd) (cons T) (split_tuple' is (i+1) Ts) in split_tuple' is 1 (HOLogic.strip_tupleT T) @@ -1550,7 +1511,8 @@ fun mk_proj i j t = (if i = j then I else HOLogic.mk_fst) (funpow (i - 1) HOLogic.mk_snd t) - fun mk_arg' i (si, so) = if i mem pis then + fun mk_arg' i (si, so) = + if member (op =) pis i then (mk_proj si ni xin, (si+1, so)) else (mk_proj so (n - ni) xout, (si, so+1)) @@ -1559,12 +1521,12 @@ HOLogic.mk_tuple args end -fun create_definitions preds (name, modes) thy = +fun create_definitions options preds (name, modes) thy = let val compfuns = PredicateCompFuns.compfuns val T = AList.lookup (op =) preds name |> the fun create_definition (mode as (iss, is)) thy = let - val mode_cname = create_constname_of_mode thy "" name mode + val mode_cname = create_constname_of_mode options thy "" name T mode val mode_cbasename = Long_Name.base_name mode_cname val Ts = binder_types T val (Ts1, Ts2) = chop (length iss) Ts @@ -1573,16 +1535,9 @@ val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (HOLogic.mk_tupleT Us2)) val names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts))); - (* old *) - (* - val xs = map Free (names ~~ (Ts1' @ Ts2)) - val (xparams, xargs) = chop (length iss) xs - val (xins, xouts) = split_smode is xargs - *) - (* new *) val param_names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts1'))) - val xparams = map Free (param_names ~~ Ts1') + val xparams = map2 (curry Free) param_names Ts1' fun mk_vars (i, T) names = let val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i)) @@ -1634,13 +1589,13 @@ fold create_definition modes thy end; -fun define_functions comp_modifiers compfuns preds (name, modes) thy = +fun define_functions comp_modifiers compfuns options preds (name, modes) thy = let val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers - val mode_cname = create_constname_of_mode thy function_name_prefix name mode + val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode val funT = Comp_Mod.funT_of comp_modifiers compfuns mode T in thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)] @@ -1672,8 +1627,8 @@ (* MAJOR FIXME: prove_params should be simple - different form of introrule for parameters ? *) -fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1) - | prove_param thy (m as SOME (Mode (mode, is, ms)), t) = +fun prove_param thy NONE t = TRY (rtac @{thm refl} 1) + | prove_param thy (m as SOME (Mode (mode, is, ms))) t = let val (f, args) = strip_comb (Envir.eta_contract t) val (params, _) = chop (length ms) args @@ -1690,7 +1645,7 @@ THEN print_tac "prove_param" THEN f_tac THEN print_tac "after simplification in prove_args" - THEN (EVERY (map (prove_param thy) (ms ~~ params))) + THEN (EVERY (map2 (prove_param thy) ms params)) THEN (REPEAT_DETERM (atac 1)) end @@ -1711,7 +1666,7 @@ (* work with parameter arguments *) THEN (atac 1) THEN (print_tac "parameter goal") - THEN (EVERY (map (prove_param thy) (ms ~~ args1))) + THEN (EVERY (map2 (prove_param thy) ms args1)) THEN (REPEAT_DETERM (atac 1)) end | _ => rtac @{thm bindI} 1 @@ -1804,8 +1759,7 @@ THEN rtac @{thm not_predI} 1 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 THEN (REPEAT_DETERM (atac 1)) - (* FIXME: work with parameter arguments *) - THEN (EVERY (map (prove_param thy) (param_modes ~~ params))) + THEN (EVERY (map2 (prove_param thy) param_modes params)) else rtac @{thm not_predI'} 1) THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 @@ -1888,8 +1842,9 @@ *) (* TODO: remove function *) -fun prove_param2 thy (NONE, t) = all_tac - | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let +fun prove_param2 thy NONE t = all_tac + | prove_param2 thy (m as SOME (Mode (mode, is, ms))) t = + let val (f, args) = strip_comb (Envir.eta_contract t) val (params, _) = chop (length ms) args val f_tac = case f of @@ -1898,11 +1853,11 @@ :: @{thm "Product_Type.split_conv"}::[])) 1 | Free _ => all_tac | _ => error "prove_param2: illegal parameter term" - in + in print_tac "before simplification in prove_args:" THEN f_tac THEN print_tac "after simplification in prove_args" - THEN (EVERY (map (prove_param2 thy) (ms ~~ params))) + THEN (EVERY (map2 (prove_param2 thy) ms params)) end @@ -1916,7 +1871,7 @@ (prop_of (predfun_elim_of thy name mode)))) THEN (etac (predfun_elim_of thy name mode) 1) THEN print_tac "prove_expr2" - THEN (EVERY (map (prove_param2 thy) (ms ~~ args))) + THEN (EVERY (map2 (prove_param2 thy) ms args)) THEN print_tac "finished prove_expr2" | _ => etac @{thm bindE} 1) @@ -1987,7 +1942,7 @@ [predfun_definition_of thy (the name) (iss, is)]) 1 THEN etac @{thm not_predE} 1 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 - THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params))) + THEN (EVERY (map2 (prove_param2 thy) param_modes params)) else etac @{thm not_predE'} 1) THEN rec_tac @@ -2078,7 +2033,7 @@ fun dest_prem thy params t = (case strip_comb t of - (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t + (v as Free _, ts) => if member (op =) params v then Prem (ts, v) else Sidecond t | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of Prem (ts, t) => Negprem (ts, t) | Negprem _ => error ("Double negation not allowed in premise: " ^ @@ -2091,7 +2046,7 @@ else Sidecond t | _ => Sidecond t) -fun prepare_intrs thy prednames intros = +fun prepare_intrs options thy prednames intros = let val intrs = map prop_of intros val nparams = nparams_of thy (hd prednames) @@ -2108,7 +2063,7 @@ val (paramTs, _) = chop nparams (binder_types (snd (hd preds))) val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i) (1 upto length paramTs)) - in map Free (param_names ~~ paramTs) end + in map2 (curry Free) param_names paramTs end | intr :: _ => fst (chop nparams (snd (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))))) val param_vs = maps term_vs params @@ -2151,7 +2106,11 @@ (Rs as _ :: _, Type ("bool", [])) => map SOME (all_smodes_of_typs Rs) | _ => [NONE]) Ts), all_smodes_of_typs Us) end - val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds + val all_modes = map (fn (s, T) => + case proposed_modes options s of + NONE => (s, modes_of_typ T) + | SOME modes' => (s, map (translate_mode' nparams) modes')) + preds in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; (* sanity check of introduction rules *) @@ -2160,14 +2119,15 @@ let val concl = Logic.strip_imp_concl (prop_of intro) val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) - val params = List.take (args, nparams_of thy (fst (dest_Const p))) + val params = fst (chop (nparams_of thy (fst (dest_Const p))) args) fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of (Ts as _ :: _ :: _) => - if (length (HOLogic.strip_tuple arg) = length Ts) then true + if length (HOLogic.strip_tuple arg) = length Ts then + true else - error ("Format of introduction rule is invalid: tuples must be expanded:" - ^ (Syntax.string_of_term_global thy arg) ^ " in " ^ - (Display.string_of_thm_global thy intro)) + error ("Format of introduction rule is invalid: tuples must be expanded:" + ^ (Syntax.string_of_term_global thy arg) ^ " in " ^ + (Display.string_of_thm_global thy intro)) | _ => true val prems = Logic.strip_imp_prems (prop_of intro) fun check_prem (Prem (args, _)) = forall check_arg args @@ -2201,7 +2161,7 @@ fun add_code_equations thy nparams preds result_thmss = let - fun add_code_equation ((predname, T), (pred, result_thms)) = + fun add_code_equation (predname, T) (pred, result_thms) = let val full_mode = (replicate nparams NONE, map (rpair NONE) (1 upto (length (binder_types T) - nparams))) @@ -2211,7 +2171,7 @@ val Ts = binder_types T val arg_names = Name.variant_list [] (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) - val args = map Free (arg_names ~~ Ts) + val args = map2 (curry Free) arg_names Ts val predfun = Const (predfun_name_of thy predname full_mode, Ts ---> PredicateCompFuns.mk_predT @{typ unit}) val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"}) @@ -2228,7 +2188,7 @@ (pred, result_thms) end in - map add_code_equation (preds ~~ result_thmss) + map2 add_code_equation preds result_thmss end (** main function of predicate compiler **) @@ -2237,7 +2197,7 @@ { compile_preds : theory -> string list -> string list -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table, - define_functions : (string * typ) list -> string * mode list -> theory -> theory, + define_functions : options -> (string * typ) list -> string * mode list -> theory -> theory, infer_modes : options -> theory -> (string * mode list) list -> (string * mode list) list -> string list -> (string * (term list * indprem list) list) list -> moded_clause list pred_mode_table, @@ -2259,16 +2219,16 @@ (*val _ = check_intros_elim_match thy prednames*) (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = - prepare_intrs thy prednames (maps (intros_of thy) prednames) + prepare_intrs options thy prednames (maps (intros_of thy) prednames) val _ = print_step options "Infering modes..." val moded_clauses = #infer_modes (dest_steps steps) options thy extra_modes all_modes param_vs clauses val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses - val _ = check_expected_modes options modes - val _ = print_modes options modes + val _ = check_expected_modes preds options modes + val _ = print_modes options thy modes (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." - val thy' = fold (#define_functions (dest_steps steps) preds) modes thy + val thy' = fold (#define_functions (dest_steps steps) options preds) modes thy |> Theory.checkpoint val _ = print_step options "Compiling equations..." val compiled_terms = @@ -2373,7 +2333,7 @@ val random_comp_modifiers = Comp_Mod.Comp_Modifiers {function_name_of = random_function_name_of, set_function_name = set_random_function_name, - function_name_prefix = "random", + function_name_prefix = "random_", funT_of = K random_function_funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = fn names => [Free (Name.variant names "size", @{typ code_numeral})], wrap_compilation = K (K (K (K (K I)))) @@ -2384,12 +2344,13 @@ val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers {function_name_of = annotated_function_name_of, set_function_name = set_annotated_function_name, - function_name_prefix = "annotated", + function_name_prefix = "annotated_", funT_of = funT_of : (compilation_funs -> mode -> typ -> typ), additional_arguments = K [], wrap_compilation = fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation => - mk_tracing ("calling predicate " ^ s ^ " with mode " ^ string_of_mode mode) compilation, + mk_tracing ("calling predicate " ^ s ^ + " with mode " ^ string_of_mode' (translate_mode T mode)) compilation, transform_additional_arguments = K I : (indprem -> term list -> term list) } @@ -2435,19 +2396,16 @@ fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); -val code_pred_intros_attrib = attrib add_intro; +val code_pred_intro_attrib = attrib add_intro; (*FIXME - Naming of auxiliary rules necessary? -- add default code equations P x y z = P_i_i_i x y z *) val setup = PredData.put (Graph.empty) #> - Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro)) + Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro)) "adding alternative introduction rules for code generation of inductive predicates" - (*FIXME name discrepancy in attribs and ML code*) - (*FIXME intros should be better named intro*) (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *) fun generic_code_pred prep_const options raw_const lthy = @@ -2519,7 +2477,7 @@ val user_mode' = map (rpair NONE) user_mode val all_modes_of = if random then all_random_modes_of else all_modes_of fun fits_to is NONE = true - | fits_to is (SOME pm) = (is = pm) + | fits_to is (SOME pm) = (is = (snd (translate_mode' 0 pm))) fun valid ((SOME (Mode (_, is, ms))) :: ms') (pm :: pms) = fits_to is pm andalso valid (ms @ ms') pms | valid (NONE :: ms') pms = valid ms' pms @@ -2593,14 +2551,7 @@ in if k = ~1 orelse length ts < k then elemsT else Const (@{const_name Set.union}, setT --> setT --> setT) $ elemsT $ cont end; - (* -fun random_values ctxt k t = - let - val thy = ProofContext.theory_of ctxt - val _ = - in - end; - *) + fun values_cmd print_modes param_user_modes options k raw_t state = let val ctxt = Toplevel.context_of state; diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 12 14:31:29 2009 -0800 @@ -186,9 +186,11 @@ @{const_name "False"}, @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat}, @{const_name Nat.one_nat_inst.one_nat}, -@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, @{const_name "HOL.zero_class.zero"}, +@{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"}, +@{const_name "HOL.zero_class.zero"}, @{const_name "HOL.one_class.one"}, @{const_name HOL.plus_class.plus}, @{const_name Nat.ord_nat_inst.less_eq_nat}, +@{const_name Nat.ord_nat_inst.less_nat}, @{const_name number_nat_inst.number_of_nat}, @{const_name Int.Bit0}, @{const_name Int.Bit1}, diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 14:31:29 2009 -0800 @@ -6,29 +6,14 @@ signature PREDICATE_COMPILE_FUN = sig -val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory + val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory val rewrite_intro : theory -> thm -> thm list - val setup_oracle : theory -> theory val pred_of_function : theory -> string -> string option end; structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN = struct - -(* Oracle for preprocessing *) - -val (oracle : (string * (cterm -> thm)) option Unsynchronized.ref) = Unsynchronized.ref NONE; - -fun the_oracle () = - case !oracle of - NONE => error "Oracle is not setup" - | SOME (_, oracle) => oracle - -val setup_oracle = Thm.add_oracle (Binding.name "pred_compile_preprocessing", I) #-> - (fn ora => fn thy => let val _ = (oracle := SOME ora) in thy end) - - fun is_funtype (Type ("fun", [_, _])) = true | is_funtype _ = false; @@ -393,9 +378,6 @@ in ([], thy) end end -(* preprocessing intro rules - uses oracle *) - -(* theory -> thm -> thm *) fun rewrite_intro thy intro = let fun lookup_pred (Const (name, T)) = @@ -435,7 +417,7 @@ |> map (fn (concl'::conclprems, _) => Logic.list_implies ((flat prems') @ conclprems, concl'))) in - map (Drule.standard o the_oracle () o cterm_of thy) intro_ts' - end; + map (Drule.standard o (Skip_Proof.make_thm thy)) intro_ts' + end end; diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Tools/res_atp.ML Thu Nov 12 14:31:29 2009 -0800 @@ -352,20 +352,32 @@ filter (not o known) c_clauses end; -fun valid_facts facts = - Facts.fold_static (fn (name, ths) => - if Facts.is_concealed facts name orelse - (run_blacklist_filter andalso is_package_def name) then I - else - let val xname = Facts.extern facts name in - if Name_Space.is_hidden xname then I - else cons (xname, filter_out Res_Axioms.bad_for_atp ths) - end) facts []; - fun all_valid_thms ctxt = let val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt); val local_facts = ProofContext.facts_of ctxt; + val full_space = + Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts); + + fun valid_facts facts = + (facts, []) |-> Facts.fold_static (fn (name, ths0) => + let + fun check_thms a = + (case try (ProofContext.get_thms ctxt) a of + NONE => false + | SOME ths1 => Thm.eq_thms (ths0, ths1)); + + val name1 = Facts.extern facts name; + val name2 = Name_Space.extern full_space name; + val ths = filter_out Res_Axioms.bad_for_atp ths0; + in + if Facts.is_concealed facts name orelse null ths orelse + run_blacklist_filter andalso is_package_def name then I + else + (case find_first check_thms [name1, name2, name] of + NONE => I + | SOME a => cons (a, ths)) + end); in valid_facts global_facts @ valid_facts local_facts end; fun multi_name a th (n, pairs) = diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/Word/WordShift.thy --- a/src/HOL/Word/WordShift.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/Word/WordShift.thy Thu Nov 12 14:31:29 2009 -0800 @@ -1102,7 +1102,7 @@ apply simp apply (rule bin_nth_rsplit) apply simp_all - apply (simp add : word_size rev_map map_compose [symmetric]) + apply (simp add : word_size rev_map) apply (rule trans) defer apply (rule map_ident [THEN fun_cong]) @@ -1113,7 +1113,7 @@ lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))" unfolding word_rcat_def to_bl_def' of_bl_def - by (clarsimp simp add : bin_rcat_bl map_compose) + by (clarsimp simp add : bin_rcat_bl) lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)" diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy Thu Nov 12 14:31:29 2009 -0800 @@ -3,35 +3,21 @@ begin section {* Set operations *} -(* -definition Empty where "Empty == {}" -declare empty_def[symmetric, code_pred_inline] -*) + declare eq_reflection[OF empty_def, code_pred_inline] -(* -definition Union where "Union A B == A Un B" - -lemma [code_pred_intros]: "A x ==> Union A B x" -and [code_pred_intros] : "B x ==> Union A B x" -unfolding Union_def Un_def Collect_def mem_def by auto - -code_pred Union -unfolding Union_def Un_def Collect_def mem_def by auto - -declare Union_def[symmetric, code_pred_inline] -*) declare eq_reflection[OF Un_def, code_pred_inline] +declare eq_reflection[OF UNION_def, code_pred_inline] section {* Alternative list definitions *} subsection {* Alternative rules for set *} -lemma set_ConsI1 [code_pred_intros]: +lemma set_ConsI1 [code_pred_intro]: "set (x # xs) x" unfolding mem_def[symmetric, of _ x] by auto -lemma set_ConsI2 [code_pred_intros]: +lemma set_ConsI2 [code_pred_intro]: "set xs x ==> set (x' # xs) x" unfolding mem_def[symmetric, of _ x] by auto @@ -49,13 +35,12 @@ done qed - subsection {* Alternative rules for list_all2 *} -lemma list_all2_NilI [code_pred_intros]: "list_all2 P [] []" +lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []" by auto -lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" +lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" by auto code_pred list_all2 diff -r d2f3104ca3d2 -r 053ac8080c11 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 14:31:11 2009 -0800 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 12 14:31:29 2009 -0800 @@ -6,31 +6,35 @@ inductive False' :: "bool" -code_pred (mode : []) False' . +code_pred (expected_modes: bool) False' . code_pred [depth_limited] False' . code_pred [random] False' . inductive EmptySet :: "'a \ bool" -code_pred (mode: [], [1]) EmptySet . +code_pred (expected_modes: o => bool, i => bool) EmptySet . definition EmptySet' :: "'a \ bool" where "EmptySet' = {}" -code_pred (mode: [], [1]) [inductify] EmptySet' . +code_pred (expected_modes: o => bool, i => bool) [inductify] EmptySet' . inductive EmptyRel :: "'a \ 'b \ bool" -code_pred (mode: [], [1], [2], [1, 2]) EmptyRel . +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) EmptyRel . inductive EmptyClosure :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" for r :: "'a \ 'a \ bool" code_pred - (mode: [] ==> [], [] ==> [1], [] ==> [2], [] ==> [1, 2], - [1] ==> [], [1] ==> [1], [1] ==> [2], [1] ==> [1, 2], - [2] ==> [], [2] ==> [1], [2] ==> [2], [2] ==> [1, 2], - [1, 2] ==> [], [1, 2] ==> [1], [1, 2] ==> [2], [1, 2] ==> [1, 2]) + (expected_modes: (o => o => bool) => o => o => bool, (o => o => bool) => i => o => bool, + (o => o => bool) => o => i => bool, (o => o => bool) => i => i => bool, + (i => o => bool) => o => o => bool, (i => o => bool) => i => o => bool, + (i => o => bool) => o => i => bool, (i => o => bool) => i => i => bool, + (o => i => bool) => o => o => bool, (o => i => bool) => i => o => bool, + (o => i => bool) => o => i => bool, (o => i => bool) => i => i => bool, + (i => i => bool) => o => o => bool, (i => i => bool) => i => o => bool, + (i => i => bool) => o => i => bool, (i => i => bool) => i => i => bool) EmptyClosure . thm EmptyClosure.equation @@ -39,20 +43,21 @@ where "False \ False''" -code_pred (mode: []) False'' . +code_pred (expected_modes: []) False'' . inductive EmptySet'' :: "'a \ bool" where "False \ EmptySet'' x" -code_pred (mode: [1]) EmptySet'' . -code_pred (mode: [], [1]) [inductify] EmptySet'' . +code_pred (expected_modes: [1]) EmptySet'' . +code_pred (expected_modes: [], [1]) [inductify] EmptySet'' . *) + inductive True' :: "bool" where "True \ True'" -code_pred (mode: []) True' . +code_pred (expected_modes: bool) True' . consts a' :: 'a @@ -60,15 +65,29 @@ where "Fact a' a'" -code_pred (mode: [], [1], [2], [1, 2]) Fact . +code_pred (expected_modes: o => o => bool, i => o => bool, o => i => bool, i => i => bool) Fact . inductive zerozero :: "nat * nat => bool" where "zerozero (0, 0)" -code_pred (mode: [i], [(i, o)], [(o, i)], [o]) zerozero . +code_pred (expected_modes: i => bool, i * o => bool, o * i => bool, o => bool) zerozero . code_pred [random] zerozero . +inductive JamesBond :: "nat => int => code_numeral => bool" +where + "JamesBond 0 0 7" + +code_pred JamesBond . + +values "{(a, b, c). JamesBond a b c}" +values "{(a, c, b). JamesBond a b c}" +values "{(b, a, c). JamesBond a b c}" +values "{(b, c, a). JamesBond a b c}" +values "{(c, a, b). JamesBond a b c}" +values "{(c, b, a). JamesBond a b c}" + + subsection {* Alternative Rules *} datatype char = C | D | E | F | G | H @@ -77,22 +96,22 @@ where "(x = C) \ (x = D) ==> is_C_or_D x" -code_pred (mode: [1]) is_C_or_D . +code_pred (expected_modes: i => bool) is_C_or_D . thm is_C_or_D.equation inductive is_D_or_E where "(x = D) \ (x = E) ==> is_D_or_E x" -lemma [code_pred_intros]: +lemma [code_pred_intro]: "is_D_or_E D" by (auto intro: is_D_or_E.intros) -lemma [code_pred_intros]: +lemma [code_pred_intro]: "is_D_or_E E" by (auto intro: is_D_or_E.intros) -code_pred (mode: [], [1]) is_D_or_E +code_pred (expected_modes: o => bool, i => bool) is_D_or_E proof - case is_D_or_E from this(1) show thesis @@ -115,11 +134,11 @@ where "x = F \ x = G ==> is_F_or_G x" -lemma [code_pred_intros]: +lemma [code_pred_intro]: "is_F_or_G F" by (auto intro: is_F_or_G.intros) -lemma [code_pred_intros]: +lemma [code_pred_intro]: "is_F_or_G G" by (auto intro: is_F_or_G.intros) @@ -130,7 +149,7 @@ text {* Compilation of is_FGH requires elimination rule for is_F_or_G *} -code_pred (mode: [], [1]) is_FGH +code_pred (expected_modes: o => bool, i => bool) is_FGH proof - case is_F_or_G from this(1) show thesis @@ -156,7 +175,7 @@ inductive zerozero' :: "nat * nat => bool" where "equals (x, y) (0, 0) ==> zerozero' (x, y)" -code_pred (mode: [1]) zerozero' . +code_pred (expected_modes: i => bool) zerozero' . lemma zerozero'_eq: "zerozero' x == zerozero x" proof - @@ -176,7 +195,7 @@ text {* if preprocessing fails, zerozero'' will not have all modes. *} -code_pred (mode: [o], [(i, o)], [(o,i)], [i]) [inductify] zerozero'' . +code_pred (expected_modes: i * i => bool, i * o => bool, o * i => bool, o => bool) [inductify] zerozero'' . subsection {* Numerals *} @@ -214,7 +233,7 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -code_pred (mode: [], [1]) even . +code_pred (expected_modes: i => bool, o => bool) even . code_pred [depth_limited] even . code_pred [random] even . @@ -237,7 +256,7 @@ definition odd' where "odd' x == \ even x" -code_pred (mode: [1]) [inductify] odd' . +code_pred (expected_modes: i => bool) [inductify] odd' . code_pred [inductify, depth_limited] odd' . code_pred [inductify, random] odd' . @@ -249,7 +268,7 @@ where "n mod 2 = 0 \ is_even n" -code_pred (mode: [1]) is_even . +code_pred (expected_modes: i => bool) is_even . subsection {* append predicate *} @@ -257,7 +276,8 @@ "append [] xs xs" | "append xs ys zs \ append (x # xs) ys (x # zs)" -code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append . +code_pred (modes: i => i => o => bool as "concat", o => o => i => bool as "slice", o => i => i => bool as prefix, + i => o => i => bool as suffix) append . code_pred [depth_limited] append . code_pred [random] append . code_pred [annotated] append . @@ -270,11 +290,12 @@ values "{(ys, xs). append xs ys [0, Suc 0, 2]}" values "{zs. append [0, Suc 0, 2] [17, 8] zs}" values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" -values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" -values [random] 15 "{(ys, zs). append [1::nat, 2] ys zs}" -value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" -value [code] "Predicate.the (append_3 ([]::int list))" +values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" +values [random] 1 "{(ys, zs). append [1::nat, 2] ys zs}" + +value [code] "Predicate.the (concat [0::int, 1, 2] [3, 4, 5])" +value [code] "Predicate.the (slice ([]::int list))" text {* tricky case with alternative rules *} @@ -287,9 +308,10 @@ lemma append2_Nil: "append2 [] (xs::'b list) xs" by (simp add: append2.intros(1)) -lemmas [code_pred_intros] = append2_Nil append2.intros(2) +lemmas [code_pred_intro] = append2_Nil append2.intros(2) -code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append2 +code_pred (expected_modes: i => i => o => bool, o => o => i => bool, o => i => i => bool, + i => o => i => bool, i => i => i => bool) append2 proof - case append2 from append2(1) show thesis @@ -309,13 +331,13 @@ "tupled_append ([], xs, xs)" | "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" -code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append . +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, + i * o * i => bool, i * i * i => bool) tupled_append . code_pred [random] tupled_append . thm tupled_append.equation -(* -TODO: values with tupled modes -values "{xs. tupled_append ([1,2,3], [4,5], xs)}" -*) + +(*TODO: values with tupled modes*) +(*values "{xs. tupled_append ([1,2,3], [4,5], xs)}"*) inductive tupled_append' where @@ -323,7 +345,8 @@ | "[| ys = fst (xa, y); x # zs = snd (xa, y); tupled_append' (xs, ys, zs) |] ==> tupled_append' (x # xs, xa, y)" -code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) tupled_append' . +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, + i * o * i => bool, i * i * i => bool) tupled_append' . thm tupled_append'.equation inductive tupled_append'' :: "'a list \ 'a list \ 'a list \ bool" @@ -331,7 +354,8 @@ "tupled_append'' ([], xs, xs)" | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, zs) \ tupled_append'' (x # xs, yszs)" -code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append'' . +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, + i * o * i => bool, i * i * i => bool) [inductify] tupled_append'' . thm tupled_append''.equation inductive tupled_append''' :: "'a list \ 'a list \ 'a list \ bool" @@ -339,7 +363,8 @@ "tupled_append''' ([], xs, xs)" | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" -code_pred (mode: [(i,i,o)], [(i,o,i)], [(o,i,i)], [(o,o,i)], [i]) [inductify] tupled_append''' . +code_pred (expected_modes: i * i * o => bool, o * o * i => bool, o * i * i => bool, + i * o * i => bool, i * i * i => bool) [inductify] tupled_append''' . thm tupled_append'''.equation subsection {* map_ofP predicate *} @@ -349,7 +374,7 @@ "map_ofP ((a, b)#xs) a b" | "map_ofP xs a b \ map_ofP (x#xs) a b" -code_pred (mode: [1], [1, 2], [1, 2, 3], [1, 3]) map_ofP . +code_pred (expected_modes: i => o => o => bool, i => i => o => bool, i => o => i => bool, i => i => i => bool) map_ofP . thm map_ofP.equation subsection {* filter predicate *} @@ -361,7 +386,7 @@ | "P x ==> filter1 P xs ys ==> filter1 P (x#xs) (x#ys)" | "\ P x ==> filter1 P xs ys ==> filter1 P (x#xs) ys" -code_pred (mode: [1] ==> [1], [1] ==> [1, 2]) filter1 . +code_pred (expected_modes: (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter1 . code_pred [depth_limited] filter1 . code_pred [random] filter1 . @@ -373,7 +398,7 @@ | "P x ==> filter2 P xs ys ==> filter2 P (x#xs) (x#ys)" | "\ P x ==> filter2 P xs ys ==> filter2 P (x#xs) ys" -code_pred (mode: [1, 2, 3], [1, 2]) filter2 . +code_pred (expected_modes: i => i => i => bool, i => i => o => bool) filter2 . code_pred [depth_limited] filter2 . code_pred [random] filter2 . thm filter2.equation @@ -384,7 +409,7 @@ where "List.filter P xs = ys ==> filter3 P xs ys" -code_pred (mode: [] ==> [1], [] ==> [1, 2], [1] ==> [1], [1] ==> [1, 2]) filter3 . +code_pred (expected_modes: (o => bool) => i => o => bool, (o => bool) => i => i => bool , (i => bool) => i => o => bool, (i => bool) => i => i => bool) filter3 . code_pred [depth_limited] filter3 . thm filter3.depth_limited_equation @@ -392,7 +417,7 @@ where "List.filter P xs = ys ==> filter4 P xs ys" -code_pred (mode: [1, 2], [1, 2, 3]) filter4 . +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) filter4 . code_pred [depth_limited] filter4 . code_pred [random] filter4 . @@ -402,7 +427,7 @@ "rev [] []" | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" -code_pred (mode: [1], [2], [1, 2]) rev . +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) rev . thm rev.equation @@ -412,7 +437,7 @@ "tupled_rev ([], [])" | "tupled_rev (xs, xs') \ tupled_append (xs', [x], ys) \ tupled_rev (x#xs, ys)" -code_pred (mode: [(i, o)], [(o, i)], [i]) tupled_rev . +code_pred (expected_modes: i * o => bool, o * i => bool, i * i => bool) tupled_rev . thm tupled_rev.equation subsection {* partition predicate *} @@ -423,7 +448,8 @@ | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -code_pred (mode: [1] ==> [1], [1] ==> [2, 3], [1] ==> [1, 2], [1] ==> [1, 3], [1] ==> [1, 2, 3]) partition . +code_pred (expected_modes: (i => bool) => i => o => o => bool, (i => bool) => o => i => i => bool, + (i => bool) => i => i => o => bool, (i => bool) => i => o => i => bool, (i => bool) => i => i => i => bool) partition . code_pred [depth_limited] partition . code_pred [random] partition . @@ -438,18 +464,21 @@ | "f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, x # ys, zs)" | "\ f x \ tupled_partition f (xs, ys, zs) \ tupled_partition f (x # xs, ys, x # zs)" -code_pred (mode: [i] ==> [i], [i] ==> [(i, i, o)], [i] ==> [(i, o, i)], [i] ==> [(o, i, i)], [i] ==> [(i, o, o)]) tupled_partition . +code_pred (expected_modes: (i => bool) => i => bool, (i => bool) => (i * i * o) => bool, (i => bool) => (i * o * i) => bool, + (i => bool) => (o * i * i) => bool, (i => bool) => (i * o * o) => bool) tupled_partition . thm tupled_partition.equation -lemma [code_pred_intros]: +lemma [code_pred_intro]: "r a b \ tranclp r a b" "r a b \ tranclp r b c \ tranclp r a c" by auto subsection {* transitive predicate *} -code_pred (mode: [1] ==> [1, 2], [1] ==> [1], [2] ==> [1, 2], [2] ==> [2], [] ==> [1, 2], [] ==> [1], [] ==> [2], [] ==> []) tranclp +code_pred (modes: (i => o => bool) => i => i => bool, (i => o => bool) => i => o => bool as forwards_trancl, + (o => i => bool) => i => i => bool, (o => i => bool) => o => i => bool as backwards_trancl, (o => o => bool) => i => i => bool, (o => o => bool) => i => o => bool, + (o => o => bool) => o => i => bool, (o => o => bool) => o => o => bool) tranclp proof - case tranclp from this converse_tranclpE[OF this(1)] show thesis by metis @@ -476,11 +505,10 @@ text {* values command needs mode annotation of the parameter succ to disambiguate which mode is to be chosen. *} -values [mode: [1]] 20 "{n. tranclp succ 10 n}" -values [mode: [2]] 10 "{n. tranclp succ n 10}" +values [mode: i => o => bool] 20 "{n. tranclp succ 10 n}" +values [mode: o => i => bool] 10 "{n. tranclp succ n 10}" values 20 "{(n, m). tranclp succ n m}" - subsection {* IMP *} types @@ -548,9 +576,8 @@ values 5 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}" -(* FIXME: values 3 "{(a,q). step (par nil nil) a q}" -*) + inductive tupled_step :: "(proc \ nat \ proc) \ bool" where @@ -570,8 +597,8 @@ | "k \ l \ divmod_rel (k - l) l q r \ divmod_rel k l (Suc q) r" code_pred divmod_rel .. - -value [code] "Predicate.the (divmod_rel_1_2 1705 42)" +thm divmod_rel.equation +value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)" subsection {* Minimum *} @@ -657,7 +684,7 @@ | "is_ord (MKT n l r h) = ((\n' \ set_of l. n' < n) \ (\n' \ set_of r. n < n') \ is_ord l \ is_ord r)" -code_pred (mode: [1], [1, 2]) [inductify] set_of . +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] set_of . thm set_of.equation code_pred [inductify] is_ord . @@ -673,19 +700,15 @@ thm rel_comp.equation code_pred [inductify] Image . thm Image.equation -(*TODO: *) - -declare Id_on_def[unfolded UNION_def, code_pred_def] - -code_pred [inductify] Id_on . +code_pred (expected_modes: (o => bool) => o => bool, (o => bool) => i * o => bool, + (o => bool) => o * i => bool, (o => bool) => i => bool) [inductify] Id_on . thm Id_on.equation code_pred [inductify] Domain . thm Domain.equation code_pred [inductify] Range . thm Range.equation code_pred [inductify] Field . -declare Sigma_def[unfolded UNION_def, code_pred_def] -declare refl_on_def[unfolded UNION_def, code_pred_def] +thm Field.equation code_pred [inductify] refl_on . thm refl_on.equation code_pred [inductify] total_on . @@ -708,21 +731,82 @@ (*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*) -code_pred [inductify] concat . -code_pred [inductify] hd . -code_pred [inductify] tl . +code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat . +thm concatP.equation + +values "{ys. concatP [[1, 2], [3, (4::int)]] ys}" +values "{ys. concatP [[1, 2], [3]] [1, 2, (3::nat)]}" + +code_pred [inductify, depth_limited] List.concat . +thm concatP.depth_limited_equation + +values [depth_limit = 3] 3 + "{xs. concatP xs ([0] :: nat list)}" + +values [depth_limit = 5] 3 + "{xs. concatP xs ([1] :: int list)}" + +values [depth_limit = 5] 3 + "{xs. concatP xs ([1] :: nat list)}" + +values [depth_limit = 5] 3 + "{xs. concatP xs [(1::int), 2]}" + +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] hd . +thm hdP.equation +values "{x. hdP [1, 2, (3::int)] x}" +values "{(xs, x). hdP [1, 2, (3::int)] 1}" + +code_pred (expected_modes: i => o => bool, i => i => bool) [inductify] tl . +thm tlP.equation +values "{x. tlP [1, 2, (3::nat)] x}" +values "{x. tlP [1, 2, (3::int)] [3]}" + code_pred [inductify] last . +thm lastP.equation + code_pred [inductify] butlast . +thm butlastP.equation + code_pred [inductify] take . +thm takeP.equation + code_pred [inductify] drop . +thm dropP.equation code_pred [inductify] zip . +thm zipP.equation + (*code_pred [inductify] upt .*) code_pred [inductify] remdups . +thm remdupsP.equation +code_pred [inductify, depth_limited] remdups . +values [depth_limit = 4] 5 "{xs. remdupsP xs [1, (2::int)]}" + code_pred [inductify] remove1 . +thm remove1P.equation +values "{xs. remove1P 1 xs [2, (3::int)]}" + code_pred [inductify] removeAll . +thm removeAllP.equation +code_pred [inductify, depth_limited] removeAll . + +values [depth_limit = 4] 10 "{xs. removeAllP 1 xs [(2::nat)]}" + code_pred [inductify] distinct . +thm distinct.equation + code_pred [inductify] replicate . +thm replicateP.equation +values 5 "{(n, xs). replicateP n (0::int) xs}" + code_pred [inductify] splice . +thm splice.simps +thm spliceP.equation + +values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}" +(* TODO: correct error messages:*) +(* values {(xs, ys, zs). spliceP xs ... } *) + code_pred [inductify] List.rev . code_pred [inductify] map . code_pred [inductify] foldr . @@ -786,7 +870,7 @@ | "w \ S\<^isub>4 \ b # w \ B\<^isub>4" | "\v \ B\<^isub>4; w \ B\<^isub>4\ \ a # v @ w \ B\<^isub>4" -code_pred (mode: [], [1]) S\<^isub>4p . +code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p . subsection {* Lambda *} @@ -838,10 +922,58 @@ | appR [simp, intro!]: "s \\<^sub>\ t ==> u \ s \\<^sub>\ u \ t" | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" -code_pred (mode: [1, 2], [1, 2, 3]) typing . +code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing . thm typing.equation -code_pred (mode: [1], [1, 2]) beta . +code_pred (modes: i => o => bool as reduce') beta . thm beta.equation +values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \\<^sub>\ x}" + +definition "reduce t = Predicate.the (reduce' t)" + +value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))" + +code_pred [random] typing . + +values [random] 1 "{(\, t, T). \ \ t : T}" + +subsection {* A minimal example of yet another semantics *} + +text {* thanks to Elke Salecker *} + +types +vname = nat +vvalue = int +var_assign = "vname \ vvalue" --"variable assignment" + +datatype ir_expr = + IrConst vvalue +| ObjAddr vname +| Add ir_expr ir_expr + +datatype val = + IntVal vvalue + +record configuration = +Env :: var_assign + +inductive eval_var :: +"ir_expr \ configuration \ val \ bool" +where + irconst: "eval_var (IrConst i) conf (IntVal i)" +| objaddr: "\ Env conf n = i \ \ eval_var (ObjAddr n) conf (IntVal i)" +| plus: "\ eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \ \ eval_var (Add l r) conf (IntVal (vl+vr))" + +(* TODO: breaks if code_pred_intro is used? *) +(* +lemmas [code_pred_intro] = irconst objaddr plus +*) +thm eval_var.cases + +code_pred eval_var . (*by (rule eval_var.cases)*) +thm eval_var.equation + +values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\x. 0)|) val}" + end \ No newline at end of file diff -r d2f3104ca3d2 -r 053ac8080c11 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Thu Nov 12 14:31:11 2009 -0800 +++ b/src/Tools/Code/code_ml.ML Thu Nov 12 14:31:29 2009 -0800 @@ -1,4 +1,4 @@ -(* Title: Tools/code/code_ml.ML +(* Title: Tools/code/code_ml.ML_ Author: Florian Haftmann, TU Muenchen Serializer for SML and OCaml. @@ -25,29 +25,34 @@ val target_OCaml = "OCaml"; val target_Eval = "Eval"; -datatype ml_stmt = - MLExc of string * int - | MLVal of string * ((typscheme * iterm) * (thm * bool)) - | MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list * string list - | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list - | MLClass of string * (vname * ((class * string) list * (string * itype) list)) - | MLClassinst of string * ((class * (string * (vname * sort) list)) +datatype ml_binding = + ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list) + | ML_Instance of string * ((class * (string * (vname * sort) list)) * ((class * (string * (string * dict list list))) list * ((string * const) * (thm * bool)) list)); -fun stmt_names_of (MLExc (name, _)) = [name] - | stmt_names_of (MLVal (name, _)) = [name] - | stmt_names_of (MLFuns (fs, _)) = map fst fs - | stmt_names_of (MLDatas ds) = map fst ds - | stmt_names_of (MLClass (name, _)) = [name] - | stmt_names_of (MLClassinst (name, _)) = [name]; +datatype ml_stmt = + ML_Exc of string * int + | ML_Val of ml_binding + | ML_Funs of ml_binding list * string list + | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list + | ML_Class of string * (vname * ((class * string) list * (string * itype) list)); + +fun stmt_name_of_binding (ML_Function (name, _)) = name + | stmt_name_of_binding (ML_Instance (name, _)) = name; + +fun stmt_names_of (ML_Exc (name, _)) = [name] + | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding] + | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings + | stmt_names_of (ML_Datas ds) = map fst ds + | stmt_names_of (ML_Class (name, _)) = [name]; (** SML serailizer **) fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons = let - fun pr_dicts fxy ds = + fun pr_dicts is_pseudo_fun fxy ds = let fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_" | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_"; @@ -58,7 +63,9 @@ | pr_proj (ps as _ :: _) p = brackets [Pretty.enum " o" "(" ")" ps, p]; fun pr_dict fxy (DictConst (inst, dss)) = - brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss) + brackify fxy ((str o deresolve) inst :: + (if is_pseudo_fun inst then [str "()"] + else map (pr_dicts is_pseudo_fun BR) dss)) | pr_dict fxy (DictVar (classrels, v)) = pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v) in case ds @@ -66,11 +73,11 @@ | [d] => pr_dict fxy d | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds end; - fun pr_tyvar_dicts vs = + fun pr_tyvar_dicts is_pseudo_fun vs = vs |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort) - |> map (pr_dicts BR); + |> map (pr_dicts is_pseudo_fun BR); fun pr_tycoexpr fxy (tyco, tys) = let val tyco' = (str o deresolve) tyco @@ -83,144 +90,155 @@ of NONE => pr_tycoexpr fxy (tyco, tys) | SOME (i, pr) => pr pr_typ fxy tys) | pr_typ fxy (ITyVar v) = str ("'" ^ v); - fun pr_term is_closure thm vars fxy (IConst c) = - pr_app is_closure thm vars fxy (c, []) - | pr_term is_closure thm vars fxy (IVar NONE) = + fun pr_term is_pseudo_fun thm vars fxy (IConst c) = + pr_app is_pseudo_fun thm vars fxy (c, []) + | pr_term is_pseudo_fun thm vars fxy (IVar NONE) = str "_" - | pr_term is_closure thm vars fxy (IVar (SOME v)) = + | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = str (lookup_var vars v) - | pr_term is_closure thm vars fxy (t as t1 `$ t2) = + | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t - of SOME c_ts => pr_app is_closure thm vars fxy c_ts + of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts | NONE => brackify fxy - [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) - | pr_term is_closure thm vars fxy (t as _ `|=> _) = + [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2]) + | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; fun pr (pat, ty) = - pr_bind is_closure thm NOBR pat + pr_bind is_pseudo_fun thm NOBR pat #>> (fn p => concat [str "fn", p, str "=>"]); val (ps, vars') = fold_map pr binds vars; - in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end - | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = + in brackets (ps @ [pr_term is_pseudo_fun thm vars' NOBR t']) end + | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) - then pr_case is_closure thm vars fxy cases - else pr_app is_closure thm vars fxy c_ts - | NONE => pr_case is_closure thm vars fxy cases) - and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) = + then pr_case is_pseudo_fun thm vars fxy cases + else pr_app is_pseudo_fun thm vars fxy c_ts + | NONE => pr_case is_pseudo_fun thm vars fxy cases) + and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = if is_cons c then let val k = length tys in if k < 2 then - (str o deresolve) c :: map (pr_term is_closure thm vars BR) ts + (str o deresolve) c :: map (pr_term is_pseudo_fun thm vars BR) ts else if k = length ts then - [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_closure thm vars NOBR) ts)] - else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand k app)] end - else if is_closure c + [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_pseudo_fun thm vars NOBR) ts)] + else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] end + else if is_pseudo_fun c then (str o deresolve) c @@ str "()" else (str o deresolve) c - :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts - and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure) + :: (map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts + and pr_app is_pseudo_fun thm vars = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun) syntax_const thm vars - and pr_bind is_closure = gen_pr_bind (pr_term is_closure) - and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) = + and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun) + and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind is_closure thm NOBR pat - |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t]) + |> pr_bind is_pseudo_fun thm NOBR pat + |>> (fn p => semicolon [str "val", p, str "=", pr_term is_pseudo_fun thm vars NOBR t]) val (ps, vars') = fold_map pr binds vars; in Pretty.chunks [ [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block, - [str ("in"), Pretty.fbrk, pr_term is_closure thm vars' NOBR body] |> Pretty.block, + [str ("in"), Pretty.fbrk, pr_term is_pseudo_fun thm vars' NOBR body] |> Pretty.block, str ("end") ] end - | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) = + | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = let fun pr delim (pat, body) = let - val (p, vars') = pr_bind is_closure thm NOBR pat vars; + val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars; in - concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body] + concat [str delim, p, str "=>", pr_term is_pseudo_fun thm vars' NOBR body] end; in brackets ( str "case" - :: pr_term is_closure thm vars NOBR t + :: pr_term is_pseudo_fun thm vars NOBR t :: pr "of" clause :: map (pr "|") clauses ) end - | pr_case is_closure thm vars fxy ((_, []), _) = + | pr_case is_pseudo_fun thm vars fxy ((_, []), _) = (concat o map str) ["raise", "Fail", "\"empty case\""]; - fun pr_stmt (MLExc (name, n)) = + fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs as eq :: eqs'))) = let - val exc_str = - (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; + val vs_dict = filter_out (null o snd) vs; + val shift = if null eqs' then I else + map (Pretty.block o single o Pretty.block o single); + fun pr_eq definer ((ts, t), (thm, _)) = + let + val consts = fold Code_Thingol.add_constnames (t :: ts) []; + val vars = reserved + |> intro_base_names + (is_none o syntax_const) deresolve consts + |> intro_vars ((fold o Code_Thingol.fold_varnames) + (insert (op =)) ts []); + val prolog = if needs_typ then + concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty] + else Pretty.strs [definer, deresolve name]; + in + concat ( + prolog + :: (if is_pseudo_fun name then [str "()"] + else pr_tyvar_dicts is_pseudo_fun vs_dict + @ map (pr_term is_pseudo_fun thm vars BR) ts) + @ str "=" + @@ pr_term is_pseudo_fun thm vars NOBR t + ) + end in - (concat o map str) ( - (if n = 0 then "val" else "fun") - :: deresolve name - :: replicate n "_" - @ "=" - :: "raise" - :: "Fail" - @@ exc_str + (Pretty.block o Pretty.fbreaks o shift) ( + pr_eq definer eq + :: map (pr_eq "|") eqs' ) end - | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) = - let - val consts = Code_Thingol.add_constnames t []; - val vars = reserved - |> intro_base_names - (is_none o syntax_const) deresolve consts; - in - concat [ - str "val", - (str o deresolve) name, - str ":", - pr_typ NOBR ty, - str "=", - pr_term (K false) thm vars NOBR t - ] - end - | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) = + | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = let - fun pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) = - let - val vs_dict = filter_out (null o snd) vs; - val shift = if null eqs' then I else - map (Pretty.block o single o Pretty.block o single); - fun pr_eq definer ((ts, t), (thm, _)) = - let - val consts = fold Code_Thingol.add_constnames (t :: ts) []; - val vars = reserved - |> intro_base_names - (is_none o syntax_const) deresolve consts - |> intro_vars ((fold o Code_Thingol.fold_varnames) - (insert (op =)) ts []); - in - concat ( - str definer - :: (str o deresolve) name - :: (if member (op =) pseudo_funs name then [str "()"] - else pr_tyvar_dicts vs_dict - @ map (pr_term (member (op =) pseudo_funs) thm vars BR) ts) - @ str "=" - @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t - ) - end - in - (Pretty.block o Pretty.fbreaks o shift) ( - pr_eq definer eq - :: map (pr_eq "|") eqs' - ) - end; + fun pr_superclass (_, (classrel, dss)) = + concat [ + (str o Long_Name.base_name o deresolve) classrel, + str "=", + pr_dicts is_pseudo_fun NOBR [DictConst dss] + ]; + fun pr_classparam ((classparam, c_inst), (thm, _)) = + concat [ + (str o Long_Name.base_name o deresolve) classparam, + str "=", + pr_app (K false) thm reserved NOBR (c_inst, []) + ]; + in + concat ( + str definer + :: (str o deresolve) inst + :: (if is_pseudo_fun inst then [str "()"] + else pr_tyvar_dicts is_pseudo_fun arity) + @ str "=" + :: Pretty.enum "," "{" "}" + (map pr_superclass superarities @ map pr_classparam classparam_insts) + :: str ":" + @@ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) + ) + end; + fun pr_stmt (ML_Exc (name, n)) = + (concat o map str) ( + (if n = 0 then "val" else "fun") + :: deresolve name + :: replicate n "_" + @ "=" + :: "raise" + :: "Fail" + @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";" + ) + | pr_stmt (ML_Val binding) = + semicolon [pr_binding (K false) true "val" binding] + | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = + let + val pr_binding' = pr_binding (member (op =) pseudo_funs) false; fun pr_pseudo_fun name = concat [ str "val", (str o deresolve) name, @@ -228,10 +246,11 @@ (str o deresolve) name, str "();" ]; - val (ps, p) = split_last (pr_funn "fun" funn :: map (pr_funn "and") funns); + val (ps, p) = split_last + (pr_binding' "fun" binding :: map (pr_binding' "and") bindings); val pseudo_ps = map pr_pseudo_fun pseudo_funs; in Pretty.chunks (ps @ Pretty.block ([p, str ";"]) :: pseudo_ps) end - | pr_stmt (MLDatas (datas as (data :: datas'))) = + | pr_stmt (ML_Datas (datas as (data :: datas'))) = let fun pr_co (co, []) = str (deresolve co) @@ -258,7 +277,7 @@ val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas'); in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end - | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = + | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) = let val w = first_upper v ^ "_"; fun pr_superclass_field (class, classrel) = @@ -300,32 +319,6 @@ :: map pr_superclass_proj superclasses @ map pr_classparam_proj classparams ) - end - | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = - let - fun pr_superclass (_, (classrel, dss)) = - concat [ - (str o Long_Name.base_name o deresolve) classrel, - str "=", - pr_dicts NOBR [DictConst dss] - ]; - fun pr_classparam ((classparam, c_inst), (thm, _)) = - concat [ - (str o Long_Name.base_name o deresolve) classparam, - str "=", - pr_app (K false) thm reserved NOBR (c_inst, []) - ]; - in - semicolon ([ - str (if null arity then "val" else "fun"), - (str o deresolve) inst ] @ - pr_tyvar_dicts arity @ [ - str "=", - Pretty.enum "," "{" "}" - (map pr_superclass superarities @ map pr_classparam classparam_insts), - str ":", - pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) - ]) end; in pr_stmt end; @@ -354,14 +347,16 @@ fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons = let - fun pr_dicts fxy ds = + fun pr_dicts is_pseudo_fun fxy ds = let fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1); fun pr_proj ps p = fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p fun pr_dict fxy (DictConst (inst, dss)) = - brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss) + brackify fxy ((str o deresolve) inst :: + (if is_pseudo_fun inst then [str "()"] + else map (pr_dicts is_pseudo_fun BR) dss)) | pr_dict fxy (DictVar (classrels, v)) = pr_proj (map deresolve classrels) ((str o pr_dictvar) v) in case ds @@ -369,11 +364,11 @@ | [d] => pr_dict fxy d | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds end; - fun pr_tyvar_dicts vs = + fun pr_tyvar_dicts is_pseudo_fun vs = vs |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort) - |> map (pr_dicts BR); + |> map (pr_dicts is_pseudo_fun BR); fun pr_tycoexpr fxy (tyco, tys) = let val tyco' = (str o deresolve) tyco @@ -386,103 +381,73 @@ of NONE => pr_tycoexpr fxy (tyco, tys) | SOME (i, pr) => pr pr_typ fxy tys) | pr_typ fxy (ITyVar v) = str ("'" ^ v); - fun pr_term is_closure thm vars fxy (IConst c) = - pr_app is_closure thm vars fxy (c, []) - | pr_term is_closure thm vars fxy (IVar NONE) = + fun pr_term is_pseudo_fun thm vars fxy (IConst c) = + pr_app is_pseudo_fun thm vars fxy (c, []) + | pr_term is_pseudo_fun thm vars fxy (IVar NONE) = str "_" - | pr_term is_closure thm vars fxy (IVar (SOME v)) = + | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = str (lookup_var vars v) - | pr_term is_closure thm vars fxy (t as t1 `$ t2) = + | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t - of SOME c_ts => pr_app is_closure thm vars fxy c_ts + of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts | NONE => - brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2]) - | pr_term is_closure thm vars fxy (t as _ `|=> _) = + brackify fxy [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2]) + | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; - val (ps, vars') = fold_map (pr_bind is_closure thm BR o fst) binds vars; - in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end - | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 + val (ps, vars') = fold_map (pr_bind is_pseudo_fun thm BR o fst) binds vars; + in brackets (str "fun" :: ps @ str "->" @@ pr_term is_pseudo_fun thm vars' NOBR t') end + | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) - then pr_case is_closure thm vars fxy cases - else pr_app is_closure thm vars fxy c_ts - | NONE => pr_case is_closure thm vars fxy cases) - and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) = + then pr_case is_pseudo_fun thm vars fxy cases + else pr_app is_pseudo_fun thm vars fxy c_ts + | NONE => pr_case is_pseudo_fun thm vars fxy cases) + and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = if is_cons c then if length tys = length ts then case ts of [] => [(str o deresolve) c] - | [t] => [(str o deresolve) c, pr_term is_closure thm vars BR t] + | [t] => [(str o deresolve) c, pr_term is_pseudo_fun thm vars BR t] | _ => [(str o deresolve) c, Pretty.enum "," "(" ")" - (map (pr_term is_closure thm vars NOBR) ts)] - else [pr_term is_closure thm vars BR (Code_Thingol.eta_expand (length tys) app)] - else if is_closure c + (map (pr_term is_pseudo_fun thm vars NOBR) ts)] + else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand (length tys) app)] + else if is_pseudo_fun c then (str o deresolve) c @@ str "()" else (str o deresolve) c - :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts) - and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure) + :: ((map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts) + and pr_app is_pseudo_fun = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun) syntax_const - and pr_bind is_closure = gen_pr_bind (pr_term is_closure) - and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) = + and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun) + and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); fun pr ((pat, ty), t) vars = vars - |> pr_bind is_closure thm NOBR pat + |> pr_bind is_pseudo_fun thm NOBR pat |>> (fn p => concat - [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"]) + [str "let", p, str "=", pr_term is_pseudo_fun thm vars NOBR t, str "in"]) val (ps, vars') = fold_map pr binds vars; in brackify_block fxy (Pretty.chunks ps) [] - (pr_term is_closure thm vars' NOBR body) + (pr_term is_pseudo_fun thm vars' NOBR body) end - | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) = + | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = let fun pr delim (pat, body) = let - val (p, vars') = pr_bind is_closure thm NOBR pat vars; - in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end; + val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars; + in concat [str delim, p, str "->", pr_term is_pseudo_fun thm vars' NOBR body] end; in brackets ( str "match" - :: pr_term is_closure thm vars NOBR t + :: pr_term is_pseudo_fun thm vars NOBR t :: pr "with" clause :: map (pr "|") clauses ) end - | pr_case is_closure thm vars fxy ((_, []), _) = + | pr_case is_pseudo_fun thm vars fxy ((_, []), _) = (concat o map str) ["failwith", "\"empty case\""]; - fun pr_stmt (MLExc (name, n)) = - let - val exc_str = - (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; - in - (concat o map str) ( - "let" - :: deresolve name - :: replicate n "_" - @ "=" - :: "failwith" - @@ exc_str - ) - end - | pr_stmt (MLVal (name, (((vs, ty), t), (thm, _)))) = - let - val consts = Code_Thingol.add_constnames t []; - val vars = reserved - |> intro_base_names - (is_none o syntax_const) deresolve consts; - in - concat [ - str "let", - (str o deresolve) name, - str ":", - pr_typ NOBR ty, - str "=", - pr_term (K false) thm vars NOBR t - ] - end - | pr_stmt (MLFuns (funn :: funns, pseudo_funs)) = + fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs))) = let fun pr_eq ((ts, t), (thm, _)) = let @@ -494,9 +459,9 @@ (insert (op =)) ts []); in concat [ (Pretty.block o Pretty.commas) - (map (pr_term (member (op =) pseudo_funs) thm vars NOBR) ts), + (map (pr_term is_pseudo_fun thm vars NOBR) ts), str "->", - pr_term (member (op =) pseudo_funs) thm vars NOBR t + pr_term is_pseudo_fun thm vars NOBR t ] end; fun pr_eqs is_pseudo [((ts, t), (thm, _))] = let @@ -509,9 +474,9 @@ in concat ( (if is_pseudo then [str "()"] - else map (pr_term (member (op =) pseudo_funs) thm vars BR) ts) + else map (pr_term is_pseudo_fun thm vars BR) ts) @ str "=" - @@ pr_term (member (op =) pseudo_funs) thm vars NOBR t + @@ pr_term is_pseudo_fun thm vars NOBR t ) end | pr_eqs _ (eqs as (eq as (([_], _), _)) :: eqs') = @@ -548,13 +513,58 @@ o single o pr_eq) eqs' ) end; - fun pr_funn definer (name, ((vs, ty), eqs)) = - concat ( - str definer - :: (str o deresolve) name - :: pr_tyvar_dicts (filter_out (null o snd) vs) - @| pr_eqs (member (op =) pseudo_funs name) eqs - ); + val prolog = if needs_typ then + concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty] + else Pretty.strs [definer, deresolve name]; + in + concat ( + prolog + :: pr_tyvar_dicts is_pseudo_fun (filter_out (null o snd) vs) + @| pr_eqs (is_pseudo_fun name) eqs + ) + end + | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = + let + fun pr_superclass (_, (classrel, dss)) = + concat [ + (str o deresolve) classrel, + str "=", + pr_dicts is_pseudo_fun NOBR [DictConst dss] + ]; + fun pr_classparam_inst ((classparam, c_inst), (thm, _)) = + concat [ + (str o deresolve) classparam, + str "=", + pr_app (K false) thm reserved NOBR (c_inst, []) + ]; + in + concat ( + str definer + :: (str o deresolve) inst + :: pr_tyvar_dicts is_pseudo_fun arity + @ str "=" + @@ brackets [ + enum_default "()" ";" "{" "}" (map pr_superclass superarities + @ map pr_classparam_inst classparam_insts), + str ":", + pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) + ] + ) + end; + fun pr_stmt (ML_Exc (name, n)) = + (concat o map str) ( + "let" + :: deresolve name + :: replicate n "_" + @ "=" + :: "failwith" + @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";;" + ) + | pr_stmt (ML_Val binding) = + Pretty.block [pr_binding (K false) true "let" binding, str ";;"] + | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = + let + val pr_binding' = pr_binding (member (op =) pseudo_funs) false; fun pr_pseudo_fun name = concat [ str "let", (str o deresolve) name, @@ -563,10 +573,10 @@ str "();;" ]; val (ps, p) = split_last - (pr_funn "let rec" funn :: map (pr_funn "and") funns); + (pr_binding' "let rec" binding :: map (pr_binding' "and") bindings); val pseudo_ps = map pr_pseudo_fun pseudo_funs; in Pretty.chunks (ps @ Pretty.block ([p, str ";;"]) :: pseudo_ps) end - | pr_stmt (MLDatas (datas as (data :: datas'))) = + | pr_stmt (ML_Datas (datas as (data :: datas'))) = let fun pr_co (co, []) = str (deresolve co) @@ -593,7 +603,7 @@ val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas'); in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end - | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) = + | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) = let val w = "_" ^ first_upper v; fun pr_superclass_field (class, classrel) = @@ -623,36 +633,8 @@ ) ] :: map pr_classparam_proj classparams - ) end - | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = - let - fun pr_superclass (_, (classrel, dss)) = - concat [ - (str o deresolve) classrel, - str "=", - pr_dicts NOBR [DictConst dss] - ]; - fun pr_classparam_inst ((classparam, c_inst), (thm, _)) = - concat [ - (str o deresolve) classparam, - str "=", - pr_app (K false) thm reserved NOBR (c_inst, []) - ]; - in - concat ( - str "let" - :: (str o deresolve) inst - :: pr_tyvar_dicts arity - @ str "=" - @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [ - enum_default "()" ";" "{" "}" (map pr_superclass superarities - @ map pr_classparam_inst classparam_insts), - str ":", - pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) - ] - ) - end; - in pr_stmt end; + ) end; + in pr_stmt end; fun pr_ocaml_module name content = Pretty.chunks ( @@ -744,32 +726,41 @@ val base' = if upper then first_upper base else base; val ([base''], nsp') = Name.variants [base'] nsp; in (base'', nsp') end; - fun rearrange_fun name (tysm as (vs, ty), raw_eqs) = + fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) = + let + val eqs = filter (snd o snd) raw_eqs; + val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs + of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty + then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE) + else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) + | _ => (eqs, NONE) + else (eqs, NONE) + in (ML_Function (name, (tysm, eqs')), is_value) end + | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, arity)), _))) = + (ML_Instance (name, stmt), if null arity then SOME (name, false) else NONE) + | ml_binding_of_stmt (name, _) = + error ("Binding block containing illegal statement: " ^ labelled_name name) + fun add_fun (name, stmt) = let - val eqs = filter (snd o snd) raw_eqs; - val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs - of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty - then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], false) - else (eqs, not (member (op =) (Code_Thingol.add_constnames t []) name)) - | _ => (eqs, false) - else (eqs, false) - in ((name, (tysm, eqs')), is_value) end; - fun check_kind [((name, (tysm, [(([], t), thm)])), true)] = MLVal (name, ((tysm, t), thm)) - | check_kind [((name, ((vs, ty), [])), _)] = - MLExc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty) - | check_kind funns = - MLFuns (map fst funns, map_filter - (fn ((name, ((vs, _), [(([], _), _)])), _) => - if null (filter_out (null o snd) vs) then SOME name else NONE - | _ => NONE) funns); - fun add_funs stmts = fold_map - (fn (name, Code_Thingol.Fun (_, stmt)) => - map_nsp_fun_yield (mk_name_stmt false name) - #>> rpair (rearrange_fun name stmt) - | (name, _) => - error ("Function block containing illegal statement: " ^ labelled_name name) - ) stmts - #>> (split_list #> apsnd check_kind); + val (binding, some_value_name) = ml_binding_of_stmt (name, stmt); + val ml_stmt = case binding + of ML_Function (name, ((vs, ty), [])) => + ML_Exc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty) + | _ => case some_value_name + of NONE => ML_Funs ([binding], []) + | SOME (name, true) => ML_Funs ([binding], [name]) + | SOME (name, false) => ML_Val binding + in + map_nsp_fun_yield (mk_name_stmt false name) + #>> (fn name' => ([name'], ml_stmt)) + end; + fun add_funs stmts = + let + val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst); + in + fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts + #>> rpair ml_stmt + end; fun add_datatypes stmts = fold_map (fn (name, Code_Thingol.Datatype (_, stmt)) => @@ -782,7 +773,7 @@ #>> (split_list #> apsnd (map_filter I #> (fn [] => error ("Datatype block without data statement: " ^ (commas o map (labelled_name o fst)) stmts) - | stmts => MLDatas stmts))); + | stmts => ML_Datas stmts))); fun add_class stmts = fold_map (fn (name, Code_Thingol.Class (_, stmt)) => @@ -797,11 +788,10 @@ #>> (split_list #> apsnd (map_filter I #> (fn [] => error ("Class block without class statement: " ^ (commas o map (labelled_name o fst)) stmts) - | [stmt] => MLClass stmt))); - fun add_inst [(name, Code_Thingol.Classinst stmt)] = - map_nsp_fun_yield (mk_name_stmt false name) - #>> (fn base => ([base], MLClassinst (name, stmt))); - fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = + | [stmt] => ML_Class stmt))); + fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) = + add_fun stmt + | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) = add_funs stmts | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) = add_datatypes stmts @@ -813,8 +803,10 @@ add_class stmts | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) = add_class stmts - | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) = - add_inst stmts + | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) = + add_fun stmt + | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) = + add_funs stmts | add_stmts stmts = error ("Illegal mutual dependencies: " ^ (commas o map (labelled_name o fst)) stmts); fun add_stmts' stmts nsp_nodes =