--- a/NEWS Thu Apr 01 10:26:45 2010 +0200
+++ b/NEWS Thu Apr 01 10:27:06 2010 +0200
@@ -96,6 +96,10 @@
without introducing dependencies on parameters or assumptions, which
is not possible in Isabelle/Pure.
+* Proof terms: Type substitutions on proof constants now use canonical
+order of type variables. INCOMPATIBILITY: Tools working with proof
+terms may need to be adapted.
+
*** HOL ***
--- a/src/HOL/Code_Numeral.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Code_Numeral.thy Thu Apr 01 10:27:06 2010 +0200
@@ -280,6 +280,16 @@
hide (open) const of_nat nat_of int_of
+subsubsection {* Lazy Evaluation of an indexed function *}
+
+function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Predicate.pred"
+where
+ "iterate_upto f n m = Predicate.Seq (%u. if n > m then Predicate.Empty else Predicate.Insert (f n) (iterate_upto f (n + 1) m))"
+by pat_completeness auto
+
+termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
+
+hide (open) const iterate_upto
subsection {* Code generator setup *}
--- a/src/HOL/DSequence.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/DSequence.thy Thu Apr 01 10:27:06 2010 +0200
@@ -27,12 +27,6 @@
None => None
| Some s => Option.map (apsnd (%r i pol. Some r)) (Lazy_Sequence.yield s))"
-definition yieldn :: "code_numeral => 'a dseq => code_numeral => bool => 'a list * 'a dseq"
-where
- "yieldn n dseq i pol = (case eval dseq i pol of
- None => ([], %i pol. None)
- | Some s => let (xs, s') = Lazy_Sequence.yieldn n s in (xs, %i pol. Some s))"
-
fun map_seq :: "('a => 'b dseq) => 'a Lazy_Sequence.lazy_sequence => 'b dseq"
where
"map_seq f xq i pol = (case Lazy_Sequence.yield xq of
@@ -91,8 +85,11 @@
type 'a dseq = int -> bool -> 'a Lazy_Sequence.lazy_sequence option
-val yieldn = @{code yieldn}
val yield = @{code yield}
+fun yieldn n s d pol = case s d pol of
+ NONE => ([], fn d => fn pol => NONE)
+ | SOME s => let val (xs, s') = Lazy_Sequence.yieldn n s in (xs, fn d => fn pol => SOME s') end
+
val map = @{code map}
end;
--- a/src/HOL/Finite_Set.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Finite_Set.thy Thu Apr 01 10:27:06 2010 +0200
@@ -616,125 +616,56 @@
subsubsection{*From @{const fold_graph} to @{term fold}*}
-lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
- by (auto simp add: less_Suc_eq)
-
-lemma insert_image_inj_on_eq:
- "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A;
- inj_on h {i. i < Suc m}|]
- ==> A = h ` {i. i < m}"
-apply (auto simp add: image_less_Suc inj_on_def)
-apply (blast intro: less_trans)
-done
-
-lemma insert_inj_onE:
- assumes aA: "insert a A = h`{i::nat. i<n}" and anot: "a \<notin> A"
- and inj_on: "inj_on h {i::nat. i<n}"
- shows "\<exists>hm m. inj_on hm {i::nat. i<m} & A = hm ` {i. i<m} & m < n"
-proof (cases n)
- case 0 thus ?thesis using aA by auto
-next
- case (Suc m)
- have nSuc: "n = Suc m" by fact
- have mlessn: "m<n" by (simp add: nSuc)
- from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
- let ?hm = "Fun.swap k m h"
- have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn
- by (simp add: inj_on)
- show ?thesis
- proof (intro exI conjI)
- show "inj_on ?hm {i. i < m}" using inj_hm
- by (auto simp add: nSuc less_Suc_eq intro: subset_inj_on)
- show "m<n" by (rule mlessn)
- show "A = ?hm ` {i. i < m}"
- proof (rule insert_image_inj_on_eq)
- show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
- show "?hm m \<notin> A" by (simp add: swap_def hkeq anot)
- show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
- using aA hkeq nSuc klessn
- by (auto simp add: swap_def image_less_Suc fun_upd_image
- less_Suc_eq inj_on_image_set_diff [OF inj_on])
- qed
- qed
-qed
-
context fun_left_comm
begin
-lemma fold_graph_determ_aux:
- "A = h`{i::nat. i<n} \<Longrightarrow> inj_on h {i. i<n}
- \<Longrightarrow> fold_graph f z A x \<Longrightarrow> fold_graph f z A x'
- \<Longrightarrow> x' = x"
-proof (induct n arbitrary: A x x' h rule: less_induct)
- case (less n)
- have IH: "\<And>m h A x x'. m < n \<Longrightarrow> A = h ` {i. i<m}
- \<Longrightarrow> inj_on h {i. i<m} \<Longrightarrow> fold_graph f z A x
- \<Longrightarrow> fold_graph f z A x' \<Longrightarrow> x' = x" by fact
- have Afoldx: "fold_graph f z A x" and Afoldx': "fold_graph f z A x'"
- and A: "A = h`{i. i<n}" and injh: "inj_on h {i. i<n}" by fact+
- show ?case
- proof (rule fold_graph.cases [OF Afoldx])
- assume "A = {}" and "x = z"
- with Afoldx' show "x' = x" by auto
+lemma fold_graph_insertE_aux:
+ "fold_graph f z A y \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_graph f z (A - {a}) y'"
+proof (induct set: fold_graph)
+ case (insertI x A y) show ?case
+ proof (cases "x = a")
+ assume "x = a" with insertI show ?case by auto
next
- fix B b u
- assume AbB: "A = insert b B" and x: "x = f b u"
- and notinB: "b \<notin> B" and Bu: "fold_graph f z B u"
- show "x'=x"
- proof (rule fold_graph.cases [OF Afoldx'])
- assume "A = {}" and "x' = z"
- with AbB show "x' = x" by blast
- next
- fix C c v
- assume AcC: "A = insert c C" and x': "x' = f c v"
- and notinC: "c \<notin> C" and Cv: "fold_graph f z C v"
- from A AbB have Beq: "insert b B = h`{i. i<n}" by simp
- from insert_inj_onE [OF Beq notinB injh]
- obtain hB mB where inj_onB: "inj_on hB {i. i < mB}"
- and Beq: "B = hB ` {i. i < mB}" and lessB: "mB < n" by auto
- from A AcC have Ceq: "insert c C = h`{i. i<n}" by simp
- from insert_inj_onE [OF Ceq notinC injh]
- obtain hC mC where inj_onC: "inj_on hC {i. i < mC}"
- and Ceq: "C = hC ` {i. i < mC}" and lessC: "mC < n" by auto
- show "x'=x"
- proof cases
- assume "b=c"
- then moreover have "B = C" using AbB AcC notinB notinC by auto
- ultimately show ?thesis using Bu Cv x x' IH [OF lessC Ceq inj_onC]
- by auto
- next
- assume diff: "b \<noteq> c"
- let ?D = "B - {c}"
- have B: "B = insert c ?D" and C: "C = insert b ?D"
- using AbB AcC notinB notinC diff by(blast elim!:equalityE)+
- have "finite A" by(rule fold_graph_imp_finite [OF Afoldx])
- with AbB have "finite ?D" by simp
- then obtain d where Dfoldd: "fold_graph f z ?D d"
- using finite_imp_fold_graph by iprover
- moreover have cinB: "c \<in> B" using B by auto
- ultimately have "fold_graph f z B (f c d)" by(rule Diff1_fold_graph)
- hence "f c d = u" by (rule IH [OF lessB Beq inj_onB Bu])
- moreover have "f b d = v"
- proof (rule IH[OF lessC Ceq inj_onC Cv])
- show "fold_graph f z C (f b d)" using C notinB Dfoldd by fastsimp
- qed
- ultimately show ?thesis
- using fun_left_comm [of c b] x x' by (auto simp add: o_def)
- qed
- qed
+ assume "x \<noteq> a"
+ then obtain y' where y: "y = f a y'" and y': "fold_graph f z (A - {a}) y'"
+ using insertI by auto
+ have 1: "f x y = f a (f x y')"
+ unfolding y by (rule fun_left_comm)
+ have 2: "fold_graph f z (insert x A - {a}) (f x y')"
+ using y' and `x \<noteq> a` and `x \<notin> A`
+ by (simp add: insert_Diff_if fold_graph.insertI)
+ from 1 2 show ?case by fast
qed
-qed
+qed simp
+
+lemma fold_graph_insertE:
+ assumes "fold_graph f z (insert x A) v" and "x \<notin> A"
+ obtains y where "v = f x y" and "fold_graph f z A y"
+using assms by (auto dest: fold_graph_insertE_aux [OF _ insertI1])
lemma fold_graph_determ:
"fold_graph f z A x \<Longrightarrow> fold_graph f z A y \<Longrightarrow> y = x"
-apply (frule fold_graph_imp_finite [THEN finite_imp_nat_seg_image_inj_on])
-apply (blast intro: fold_graph_determ_aux [rule_format])
-done
+proof (induct arbitrary: y set: fold_graph)
+ case (insertI x A y v)
+ from `fold_graph f z (insert x A) v` and `x \<notin> A`
+ obtain y' where "v = f x y'" and "fold_graph f z A y'"
+ by (rule fold_graph_insertE)
+ from `fold_graph f z A y'` have "y' = y" by (rule insertI)
+ with `v = f x y'` show "v = f x y" by simp
+qed fast
lemma fold_equality:
"fold_graph f z A y \<Longrightarrow> fold f z A = y"
by (unfold fold_def) (blast intro: fold_graph_determ)
+lemma fold_graph_fold: "finite A \<Longrightarrow> fold_graph f z A (fold f z A)"
+unfolding fold_def
+apply (rule theI')
+apply (rule ex_ex1I)
+apply (erule finite_imp_fold_graph)
+apply (erule (1) fold_graph_determ)
+done
+
text{* The base case for @{text fold}: *}
lemma (in -) fold_empty [simp]: "fold f z {} = z"
@@ -742,21 +673,11 @@
text{* The various recursion equations for @{const fold}: *}
-lemma fold_insert_aux: "x \<notin> A
- \<Longrightarrow> fold_graph f z (insert x A) v \<longleftrightarrow>
- (\<exists>y. fold_graph f z A y \<and> v = f x y)"
-apply auto
-apply (rule_tac A1 = A and f1 = f in finite_imp_fold_graph [THEN exE])
- apply (fastsimp dest: fold_graph_imp_finite)
-apply (blast intro: fold_graph_determ)
-done
-
lemma fold_insert [simp]:
"finite A ==> x \<notin> A ==> fold f z (insert x A) = f x (fold f z A)"
-apply (simp add: fold_def fold_insert_aux)
-apply (rule the_equality)
- apply (auto intro: finite_imp_fold_graph
- cong add: conj_cong simp add: fold_def[symmetric] fold_equality)
+apply (rule fold_equality)
+apply (erule fold_graph.insertI)
+apply (erule fold_graph_fold)
done
lemma fold_fun_comm:
@@ -1185,7 +1106,7 @@
interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
from assms show ?thesis
proof (induct rule: fold_graph.induct)
- case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
+ case emptyI show ?case by (subst mult_commute [of z b], fast)
next
case (insertI x A y)
have "fold_graph times z (insert x (insert b A)) (x * (z * y))"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Apr 01 10:27:06 2010 +0200
@@ -270,15 +270,23 @@
using assms by (auto simp add: assert_def return_bind raise_bind)
subsubsection {* A monadic combinator for simple recursive functions *}
-
-function (default "\<lambda>(f,g,x,h). (Inr Exn, undefined)")
+
+text {* Using a locale to fix arguments f and g of MREC *}
+
+locale mrec =
+fixes
+ f :: "'a => ('b + 'a) Heap"
+ and g :: "'a => 'a => 'b => 'b Heap"
+begin
+
+function (default "\<lambda>(x,h). (Inr Exn, undefined)")
mrec
where
- "mrec f g x h =
+ "mrec x h =
(case Heap_Monad.execute (f x) h of
(Inl (Inl r), h') \<Rightarrow> (Inl r, h')
| (Inl (Inr s), h') \<Rightarrow>
- (case mrec f g s h' of
+ (case mrec s h' of
(Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
| (Inr e, h'') \<Rightarrow> (Inr e, h''))
| (Inr e, h') \<Rightarrow> (Inr e, h')
@@ -292,17 +300,17 @@
apply (erule mrec_rel.cases)
by simp
-lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
+lemma mrec_default: "\<not> mrec_dom (x, h) \<Longrightarrow> mrec x h = (Inr Exn, undefined)"
unfolding mrec_def
- by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
+ by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(x, h)", simplified])
-lemma f_di_reverse:
- assumes "\<not> mrec_dom (f, g, x, h)"
+lemma mrec_di_reverse:
+ assumes "\<not> mrec_dom (x, h)"
shows "
(case Heap_Monad.execute (f x) h of
- (Inl (Inl r), h') \<Rightarrow> mrecalse
- | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (f, g, s, h')
- | (Inr e, h') \<Rightarrow> mrecalse
+ (Inl (Inl r), h') \<Rightarrow> False
+ | (Inl (Inr s), h') \<Rightarrow> \<not> mrec_dom (s, h')
+ | (Inr e, h') \<Rightarrow> False
)"
using assms
by (auto split:prod.splits sum.splits)
@@ -310,40 +318,103 @@
lemma mrec_rule:
- "mrec f g x h =
+ "mrec x h =
(case Heap_Monad.execute (f x) h of
(Inl (Inl r), h') \<Rightarrow> (Inl r, h')
| (Inl (Inr s), h') \<Rightarrow>
- (case mrec f g s h' of
+ (case mrec s h' of
(Inl z, h'') \<Rightarrow> Heap_Monad.execute (g x s z) h''
| (Inr e, h'') \<Rightarrow> (Inr e, h''))
| (Inr e, h') \<Rightarrow> (Inr e, h')
)"
-apply (cases "mrec_dom (f,g,x,h)", simp)
-apply (frule f_default)
-apply (frule f_di_reverse, simp)
-by (auto split: sum.split prod.split simp: f_default)
+apply (cases "mrec_dom (x,h)", simp)
+apply (frule mrec_default)
+apply (frule mrec_di_reverse, simp)
+by (auto split: sum.split prod.split simp: mrec_default)
definition
- "MREC f g x = Heap (mrec f g x)"
+ "MREC x = Heap (mrec x)"
lemma MREC_rule:
- "MREC f g x =
+ "MREC x =
(do y \<leftarrow> f x;
(case y of
Inl r \<Rightarrow> return r
| Inr s \<Rightarrow>
- do z \<leftarrow> MREC f g s ;
+ do z \<leftarrow> MREC s ;
g x s z
done) done)"
unfolding MREC_def
unfolding bindM_def return_def
apply simp
apply (rule ext)
- apply (unfold mrec_rule[of f g x])
+ apply (unfold mrec_rule[of x])
by (auto split:prod.splits sum.splits)
+
+lemma MREC_pinduct:
+ assumes "Heap_Monad.execute (MREC x) h = (Inl r, h')"
+ assumes non_rec_case: "\<And> x h h' r. Heap_Monad.execute (f x) h = (Inl (Inl r), h') \<Longrightarrow> P x h h' r"
+ assumes rec_case: "\<And> x h h1 h2 h' s z r. Heap_Monad.execute (f x) h = (Inl (Inr s), h1) \<Longrightarrow> Heap_Monad.execute (MREC s) h1 = (Inl z, h2) \<Longrightarrow> P s h1 h2 z
+ \<Longrightarrow> Heap_Monad.execute (g x s z) h2 = (Inl r, h') \<Longrightarrow> P x h h' r"
+ shows "P x h h' r"
+proof -
+ from assms(1) have mrec: "mrec x h = (Inl r, h')"
+ unfolding MREC_def execute.simps .
+ from mrec have dom: "mrec_dom (x, h)"
+ apply -
+ apply (rule ccontr)
+ apply (drule mrec_default) by auto
+ from mrec have h'_r: "h' = (snd (mrec x h))" "r = (Sum_Type.Projl (fst (mrec x h)))"
+ by auto
+ from mrec have "P x h (snd (mrec x h)) (Sum_Type.Projl (fst (mrec x h)))"
+ proof (induct arbitrary: r h' rule: mrec.pinduct[OF dom])
+ case (1 x h)
+ obtain rr h' where "mrec x h = (rr, h')" by fastsimp
+ obtain fret h1 where exec_f: "Heap_Monad.execute (f x) h = (fret, h1)" by fastsimp
+ show ?case
+ proof (cases fret)
+ case (Inl a)
+ note Inl' = this
+ show ?thesis
+ proof (cases a)
+ case (Inl aa)
+ from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
+ by auto
+ next
+ case (Inr b)
+ note Inr' = this
+ obtain ret_mrec h2 where mrec_rec: "mrec b h1 = (ret_mrec, h2)" by fastsimp
+ from this Inl 1(1) exec_f mrec show ?thesis
+ proof (cases "ret_mrec")
+ case (Inl aaa)
+ from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
+ show ?thesis
+ apply auto
+ apply (rule rec_case)
+ unfolding MREC_def by auto
+ next
+ case (Inr b)
+ from this Inl 1(1) exec_f mrec Inr' mrec_rec 1(3) show ?thesis by auto
+ qed
+ qed
+ next
+ case (Inr b)
+ from this 1(1) mrec exec_f 1(3) show ?thesis by simp
+ qed
+ qed
+ from this h'_r show ?thesis by simp
+qed
+
+end
+
+text {* Providing global versions of the constant and the theorems *}
+
+abbreviation "MREC == mrec.MREC"
+lemmas MREC_rule = mrec.MREC_rule
+lemmas MREC_pinduct = mrec.MREC_pinduct
+
hide (open) const heap execute
--- a/src/HOL/Imperative_HOL/Relational.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Imperative_HOL/Relational.thy Thu Apr 01 10:27:06 2010 +0200
@@ -469,7 +469,7 @@
(* thm crel_mapI is missing *)
-subsection {* Introduction rules for reference commands *}
+subsubsection {* Introduction rules for reference commands *}
lemma crel_lookupI:
shows "crel (!ref) h h (get_ref ref h)"
@@ -483,7 +483,7 @@
shows "crel (Ref.change f ref) h (set_ref ref (f (get_ref ref h)) h) (f (get_ref ref h))"
unfolding change_def Let_def by (auto intro!: crelI crel_returnI crel_lookupI crel_updateI)
-subsection {* Introduction rules for the assert command *}
+subsubsection {* Introduction rules for the assert command *}
lemma crel_assertI:
assumes "P x"
@@ -492,7 +492,26 @@
unfolding assert_def
by (auto intro!: crel_ifI crel_returnI crel_raiseI)
-section {* Defintion of the noError predicate *}
+subsection {* Induction rule for the MREC combinator *}
+
+lemma MREC_induct:
+ assumes "crel (MREC f g x) h h' r"
+ assumes "\<And> x h h' r. crel (f x) h h' (Inl r) \<Longrightarrow> P x h h' r"
+ assumes "\<And> x h h1 h2 h' s z r. crel (f x) h h1 (Inr s) \<Longrightarrow> crel (MREC f g s) h1 h2 z \<Longrightarrow> P s h1 h2 z
+ \<Longrightarrow> crel (g x s z) h2 h' r \<Longrightarrow> P x h h' r"
+ shows "P x h h' r"
+proof (rule MREC_pinduct[OF assms(1)[unfolded crel_def, symmetric]])
+ fix x h h1 h2 h' s z r
+ assume "Heap_Monad.execute (f x) h = (Inl (Inr s), h1)"
+ "Heap_Monad.execute (MREC f g s) h1 = (Inl z, h2)"
+ "P s h1 h2 z"
+ "Heap_Monad.execute (g x s z) h2 = (Inl r, h')"
+ from assms(3)[unfolded crel_def, OF this(1)[symmetric] this(2)[symmetric] this(3) this(4)[symmetric]]
+ show "P x h h' r" .
+next
+qed (auto simp add: assms(2)[unfolded crel_def])
+
+section {* Definition of the noError predicate *}
text {* We add a simple definitional setting for crel intro rules
where we only would like to show that the computation does not result in a exception for heap h,
--- a/src/HOL/IsaMakefile Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Apr 01 10:27:06 2010 +0200
@@ -297,10 +297,12 @@
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
Tools/Predicate_Compile/predicate_compile_aux.ML \
+ Tools/Predicate_Compile/predicate_compile_compilations.ML \
Tools/Predicate_Compile/predicate_compile_core.ML \
Tools/Predicate_Compile/predicate_compile_data.ML \
Tools/Predicate_Compile/predicate_compile_fun.ML \
Tools/Predicate_Compile/predicate_compile.ML \
+ Tools/Predicate_Compile/predicate_compile_specialisation.ML \
Tools/Predicate_Compile/predicate_compile_pred.ML \
Tools/quickcheck_generators.ML \
Tools/Qelim/cooper_data.ML \
--- a/src/HOL/Lattices.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Lattices.thy Thu Apr 01 10:27:06 2010 +0200
@@ -90,10 +90,10 @@
by (rule order_trans) auto
lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
- by (blast intro: inf_greatest)
+ by (rule inf_greatest) (* FIXME: duplicate lemma *)
lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
- by (blast intro: order_trans le_infI1 le_infI2)
+ by (blast intro: order_trans inf_le1 inf_le2)
lemma le_inf_iff [simp]:
"x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
@@ -103,6 +103,9 @@
"x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
+lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
+ by (fast intro: inf_greatest le_infI1 le_infI2)
+
lemma mono_inf:
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_inf"
shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
@@ -123,11 +126,11 @@
lemma le_supI:
"a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
- by (blast intro: sup_least)
+ by (rule sup_least) (* FIXME: duplicate lemma *)
lemma le_supE:
"a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
- by (blast intro: le_supI1 le_supI2 order_trans)
+ by (blast intro: order_trans sup_ge1 sup_ge2)
lemma le_sup_iff [simp]:
"x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
@@ -137,6 +140,9 @@
"x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
+lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
+ by (fast intro: sup_least le_supI1 le_supI2)
+
lemma mono_sup:
fixes f :: "'a \<Rightarrow> 'b\<Colon>semilattice_sup"
shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
@@ -345,6 +351,12 @@
by (rule distrib_lattice.intro, rule dual_lattice)
(unfold_locales, fact inf_sup_distrib1)
+lemmas sup_inf_distrib =
+ sup_inf_distrib1 sup_inf_distrib2
+
+lemmas inf_sup_distrib =
+ inf_sup_distrib1 inf_sup_distrib2
+
lemmas distrib =
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
@@ -393,39 +405,13 @@
"x \<squnion> \<bottom> = x"
by (rule sup_absorb1) simp
-lemma inf_eq_top_eq1:
- assumes "A \<sqinter> B = \<top>"
- shows "A = \<top>"
-proof (cases "B = \<top>")
- case True with assms show ?thesis by simp
-next
- case False with top_greatest have "B \<sqsubset> \<top>" by (auto intro: neq_le_trans)
- then have "A \<sqinter> B \<sqsubset> \<top>" by (rule less_infI2)
- with assms show ?thesis by simp
-qed
-
-lemma inf_eq_top_eq2:
- assumes "A \<sqinter> B = \<top>"
- shows "B = \<top>"
- by (rule inf_eq_top_eq1, unfold inf_commute [of B]) (fact assms)
+lemma inf_eq_top_iff [simp]:
+ "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+ by (simp add: eq_iff)
-lemma sup_eq_bot_eq1:
- assumes "A \<squnion> B = \<bottom>"
- shows "A = \<bottom>"
-proof -
- interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
- by (rule dual_bounded_lattice)
- from dual.inf_eq_top_eq1 assms show ?thesis .
-qed
-
-lemma sup_eq_bot_eq2:
- assumes "A \<squnion> B = \<bottom>"
- shows "B = \<bottom>"
-proof -
- interpret dual: bounded_lattice "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
- by (rule dual_bounded_lattice)
- from dual.inf_eq_top_eq2 assms show ?thesis .
-qed
+lemma sup_eq_bot_iff [simp]:
+ "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+ by (simp add: eq_iff)
end
@@ -472,10 +458,7 @@
"- x = - y \<longleftrightarrow> x = y"
proof
assume "- x = - y"
- then have "- x \<sqinter> y = \<bottom>"
- and "- x \<squnion> y = \<top>"
- by (simp_all add: compl_inf_bot compl_sup_top)
- then have "- (- x) = y" by (rule compl_unique)
+ then have "- (- x) = - (- y)" by (rule arg_cong)
then show "x = y" by simp
next
assume "x = y"
@@ -499,18 +482,14 @@
lemma compl_inf [simp]:
"- (x \<sqinter> y) = - x \<squnion> - y"
proof (rule compl_unique)
- have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)"
- by (rule inf_sup_distrib1)
- also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
- by (simp only: inf_commute inf_assoc inf_left_commute)
- finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
+ have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
+ by (simp only: inf_sup_distrib inf_aci)
+ then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
by (simp add: inf_compl_bot)
next
- have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))"
- by (rule sup_inf_distrib2)
- also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
- by (simp only: sup_commute sup_assoc sup_left_commute)
- finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
+ have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
+ by (simp only: sup_inf_distrib sup_aci)
+ then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
by (simp add: sup_compl_top)
qed
@@ -522,6 +501,21 @@
then show ?thesis by simp
qed
+lemma compl_mono:
+ "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
+proof -
+ assume "x \<sqsubseteq> y"
+ then have "x \<squnion> y = y" by (simp only: le_iff_sup)
+ then have "- (x \<squnion> y) = - y" by simp
+ then have "- x \<sqinter> - y = - y" by simp
+ then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
+ then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
+qed
+
+lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
+ "- x \<le> - y \<longleftrightarrow> y \<le> x"
+by (auto dest: compl_mono)
+
end
@@ -550,7 +544,7 @@
have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
qed
-
+
subsection {* @{const min}/@{const max} on linear orders as
special case of @{const inf}/@{const sup} *}
--- a/src/HOL/Lazy_Sequence.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Lazy_Sequence.thy Thu Apr 01 10:27:06 2010 +0200
@@ -20,15 +20,6 @@
"yield Empty = None"
| "yield (Insert x xq) = Some (x, xq)"
-fun yieldn :: "code_numeral => 'a lazy_sequence => 'a list * 'a lazy_sequence"
-where
- "yieldn i S = (if i = 0 then ([], S) else
- case yield S of
- None => ([], S)
- | Some (x, S') => let
- (xs, S'') = yieldn (i - 1) S'
- in (x # xs, S''))"
-
lemma [simp]: "yield xq = Some (x, xq') ==> size xq' < size xq"
by (cases xq) auto
@@ -119,6 +110,13 @@
where
"if_seq b = (if b then single () else empty)"
+function iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a Lazy_Sequence.lazy_sequence"
+where
+ "iterate_upto f n m = Lazy_Sequence.Lazy_Sequence (%u. if n > m then None else Some (f n, iterate_upto f (n + 1) m))"
+by pat_completeness auto
+
+termination by (relation "measure (%(f, n, m). Code_Numeral.nat_of (m + 1 - n))") auto
+
definition not_seq :: "unit lazy_sequence => unit lazy_sequence"
where
"not_seq xq = (case yield xq of None => single () | Some ((), xq) => empty)"
@@ -131,6 +129,7 @@
datatype 'a lazy_sequence = Lazy_Sequence of unit -> ('a * 'a lazy_sequence) option
val yield : 'a lazy_sequence -> ('a * 'a lazy_sequence) option
val yieldn : int -> 'a lazy_sequence -> ('a list * 'a lazy_sequence)
+ val map : ('a -> 'b) -> 'a lazy_sequence -> 'b lazy_sequence
end;
structure Lazy_Sequence : LAZY_SEQUENCE =
@@ -140,7 +139,16 @@
val yield = @{code yield}
-val yieldn = @{code yieldn}
+fun anamorph f k x = (if k = 0 then ([], x)
+ else case f x
+ of NONE => ([], x)
+ | SOME (v, y) => let
+ val (vs, z) = anamorph f (k - 1) y
+ in (v :: vs, z) end);
+
+fun yieldn S = anamorph yield S;
+
+val map = @{code map}
end;
*}
@@ -151,8 +159,61 @@
code_const Lazy_Sequence (Eval "Lazy'_Sequence.Lazy'_Sequence")
+section {* With Hit Bound Value *}
+text {* assuming in negative context *}
+
+types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
+
+definition hit_bound :: "'a hit_bound_lazy_sequence"
+where
+ [code]: "hit_bound = Lazy_Sequence (%u. Some (None, empty))"
+
+
+definition hb_single :: "'a => 'a hit_bound_lazy_sequence"
+where
+ [code]: "hb_single x = Lazy_Sequence (%u. Some (Some x, empty))"
+
+primrec hb_flat :: "'a hit_bound_lazy_sequence hit_bound_lazy_sequence => 'a hit_bound_lazy_sequence"
+where
+ "hb_flat Empty = Empty"
+| "hb_flat (Insert xq xqq) = append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq)"
+
+lemma [code]:
+ "hb_flat xqq = Lazy_Sequence (%u. case yield xqq of
+ None => None
+ | Some (xq, xqq') => yield (append (case xq of None => hit_bound | Some xq => xq) (hb_flat xqq')))"
+apply (cases "xqq")
+apply (auto simp add: Seq_yield)
+unfolding Lazy_Sequence_def
+by auto
+
+primrec hb_map :: "('a => 'b) => 'a hit_bound_lazy_sequence => 'b hit_bound_lazy_sequence"
+where
+ "hb_map f Empty = Empty"
+| "hb_map f (Insert x xq) = Insert (Option.map f x) (hb_map f xq)"
+
+lemma [code]:
+ "hb_map f xq = Lazy_Sequence (%u. Option.map (%(x, xq'). (Option.map f x, hb_map f xq')) (yield xq))"
+apply (cases xq)
+apply (auto simp add: Seq_yield)
+unfolding Lazy_Sequence_def
+apply auto
+done
+
+definition hb_bind :: "'a hit_bound_lazy_sequence => ('a => 'b hit_bound_lazy_sequence) => 'b hit_bound_lazy_sequence"
+where
+ [code]: "hb_bind xq f = hb_flat (hb_map f xq)"
+
+definition hb_if_seq :: "bool => unit hit_bound_lazy_sequence"
+where
+ "hb_if_seq b = (if b then hb_single () else empty)"
+
+definition hb_not_seq :: "unit hit_bound_lazy_sequence => unit lazy_sequence"
+where
+ "hb_not_seq xq = (case yield xq of None => single () | Some (x, xq) => empty)"
+
hide (open) type lazy_sequence
-hide (open) const Empty Insert Lazy_Sequence yield yieldn empty single append flat map bind if_seq not_seq
-hide fact yield.simps yieldn.simps empty_def single_def append.simps flat.simps map.simps bind_def if_seq_def not_seq_def
+hide (open) const Empty Insert Lazy_Sequence yield empty single append flat map bind if_seq iterate_upto not_seq
+hide fact yield.simps empty_def single_def append.simps flat.simps map.simps bind_def iterate_upto.simps if_seq_def not_seq_def
end
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Thu Apr 01 10:27:06 2010 +0200
@@ -1,5 +1,5 @@
theory Predicate_Compile_Alternative_Defs
-imports "../Predicate_Compile"
+imports Main
begin
section {* Common constants *}
@@ -46,15 +46,95 @@
setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
-subsection {* Inductive definitions for arithmetic on natural numbers *}
+section {* Arithmetic operations *}
+
+subsection {* Arithmetic on naturals and integers *}
+
+definition plus_eq_nat :: "nat => nat => nat => bool"
+where
+ "plus_eq_nat x y z = (x + y = z)"
-inductive plusP
+definition minus_eq_nat :: "nat => nat => nat => bool"
+where
+ "minus_eq_nat x y z = (x - y = z)"
+
+definition plus_eq_int :: "int => int => int => bool"
+where
+ "plus_eq_int x y z = (x + y = z)"
+
+definition minus_eq_int :: "int => int => int => bool"
+where
+ "minus_eq_int x y z = (x - y = z)"
+
+definition subtract
where
- "plusP x 0 x"
-| "plusP x y z ==> plusP x (Suc y) (Suc z)"
+ [code_inline]: "subtract x y = y - x"
-setup {* Predicate_Compile_Fun.add_function_predicate_translation
- (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
+setup {*
+let
+ val Fun = Predicate_Compile_Aux.Fun
+ val Input = Predicate_Compile_Aux.Input
+ val Output = Predicate_Compile_Aux.Output
+ val Bool = Predicate_Compile_Aux.Bool
+ val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
+ val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
+ val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
+ val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
+ val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio
+ val minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio
+ fun subtract_nat compfuns (_ : typ) =
+ let
+ val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
+ in
+ absdummy (@{typ nat}, absdummy (@{typ nat},
+ Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
+ (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
+ Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
+ Predicate_Compile_Aux.mk_single compfuns
+ (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
+ end
+ fun enumerate_addups_nat compfuns (_ : typ) =
+ absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
+ (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
+ (@{term "Code_Numeral.nat_of"} $ Bound 0) $
+ (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
+ @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
+ fun enumerate_nats compfuns (_ : typ) =
+ let
+ val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
+ val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
+ in
+ absdummy(@{typ nat}, absdummy (@{typ nat},
+ Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
+ (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
+ (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
+ @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
+ (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
+ end
+in
+ Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_nat}
+ [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
+ (ooi, (enumerate_addups_nat, false))]
+ #> Predicate_Compile_Fun.add_function_predicate_translation
+ (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
+ #> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_nat}
+ [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
+ #> Predicate_Compile_Fun.add_function_predicate_translation
+ (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
+ #> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_eq_int}
+ [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
+ (oii, (@{const_name subtract}, false))]
+ #> Predicate_Compile_Fun.add_function_predicate_translation
+ (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
+ #> Predicate_Compile_Core.force_modes_and_functions @{const_name minus_eq_int}
+ [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
+ (ioi, (@{const_name minus}, false))]
+ #> Predicate_Compile_Fun.add_function_predicate_translation
+ (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
+end
+*}
+
+subsection {* Inductive definitions for ordering on naturals *}
inductive less_nat
where
@@ -88,12 +168,18 @@
section {* Alternative list definitions *}
-text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
-
-lemma [code_pred_def]:
- "length [] = 0"
- "length (x # xs) = Suc (length xs)"
-by auto
+subsection {* Alternative rules for length *}
+
+definition size_list :: "'a list => nat"
+where "size_list = size"
+
+lemma size_list_simps:
+ "size_list [] = 0"
+ "size_list (x # xs) = Suc (size_list xs)"
+by (auto simp add: size_list_def)
+
+declare size_list_simps[code_pred_def]
+declare size_list_def[symmetric, code_pred_inline]
subsection {* Alternative rules for set *}
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy Thu Apr 01 10:27:06 2010 +0200
@@ -7,8 +7,11 @@
uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
begin
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term
+ Predicate_Compile_Aux.New_Pos_Random_DSeq false true 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs",
+ Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true true 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs",
+ Predicate_Compile_Quickcheck.quickcheck_compile_term Predicate_Compile_Aux.New_Pos_Random_DSeq true false 4) *}
end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/New_DSequence.thy Thu Apr 01 10:27:06 2010 +0200
@@ -0,0 +1,103 @@
+
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* Depth-Limited Sequences with failure element *}
+
+theory New_DSequence
+imports Random_Sequence
+begin
+
+section {* Positive Depth-Limited Sequence *}
+
+types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
+
+definition pos_empty :: "'a pos_dseq"
+where
+ "pos_empty = (%i. Lazy_Sequence.empty)"
+
+definition pos_single :: "'a => 'a pos_dseq"
+where
+ "pos_single x = (%i. Lazy_Sequence.single x)"
+
+definition pos_bind :: "'a pos_dseq => ('a => 'b pos_dseq) => 'b pos_dseq"
+where
+ "pos_bind x f = (%i.
+ if i = 0 then
+ Lazy_Sequence.empty
+ else
+ Lazy_Sequence.bind (x (i - 1)) (%a. f a i))"
+
+definition pos_union :: "'a pos_dseq => 'a pos_dseq => 'a pos_dseq"
+where
+ "pos_union xq yq = (%i. Lazy_Sequence.append (xq i) (yq i))"
+
+definition pos_if_seq :: "bool => unit pos_dseq"
+where
+ "pos_if_seq b = (if b then pos_single () else pos_empty)"
+
+definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_dseq"
+where
+ "pos_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto f n m)"
+
+definition pos_map :: "('a => 'b) => 'a pos_dseq => 'b pos_dseq"
+where
+ "pos_map f xq = (%i. Lazy_Sequence.map f (xq i))"
+
+section {* Negative Depth-Limited Sequence *}
+
+types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
+
+definition neg_empty :: "'a neg_dseq"
+where
+ "neg_empty = (%i. Lazy_Sequence.empty)"
+
+definition neg_single :: "'a => 'a neg_dseq"
+where
+ "neg_single x = (%i. Lazy_Sequence.hb_single x)"
+
+definition neg_bind :: "'a neg_dseq => ('a => 'b neg_dseq) => 'b neg_dseq"
+where
+ "neg_bind x f = (%i.
+ if i = 0 then
+ Lazy_Sequence.hit_bound
+ else
+ hb_bind (x (i - 1)) (%a. f a i))"
+
+definition neg_union :: "'a neg_dseq => 'a neg_dseq => 'a neg_dseq"
+where
+ "neg_union x y = (%i. Lazy_Sequence.append (x i) (y i))"
+
+definition neg_if_seq :: "bool => unit neg_dseq"
+where
+ "neg_if_seq b = (if b then neg_single () else neg_empty)"
+
+definition neg_iterate_upto
+where
+ "neg_iterate_upto f n m = (%i. Lazy_Sequence.iterate_upto (%i. Some (f i)) n m)"
+
+definition neg_map :: "('a => 'b) => 'a neg_dseq => 'b neg_dseq"
+where
+ "neg_map f xq = (%i. Lazy_Sequence.hb_map f (xq i))"
+
+section {* Negation *}
+
+definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
+where
+ "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
+
+definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
+where
+ "neg_not_seq x = (%i. case Lazy_Sequence.yield (x i) of
+ None => Lazy_Sequence.hb_single ()
+ | Some ((), xq) => Lazy_Sequence.empty)"
+
+hide (open) type pos_dseq neg_dseq
+
+hide (open) const
+ pos_empty pos_single pos_bind pos_union pos_if_seq pos_iterate_upto pos_not_seq pos_map
+ neg_empty neg_single neg_bind neg_union neg_if_seq neg_iterate_upto neg_not_seq neg_map
+hide (open) fact
+ pos_empty_def pos_single_def pos_bind_def pos_union_def pos_if_seq_def pos_iterate_upto_def pos_not_seq_def pos_map_def
+ neg_empty_def neg_single_def neg_bind_def neg_union_def neg_if_seq_def neg_iterate_upto_def neg_not_seq_def neg_map_def
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/New_Random_Sequence.thy Thu Apr 01 10:27:06 2010 +0200
@@ -0,0 +1,106 @@
+
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+theory New_Random_Sequence
+imports Quickcheck New_DSequence
+begin
+
+types 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
+types 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
+
+definition pos_empty :: "'a pos_random_dseq"
+where
+ "pos_empty = (%nrandom size seed. New_DSequence.pos_empty)"
+
+definition pos_single :: "'a => 'a pos_random_dseq"
+where
+ "pos_single x = (%nrandom size seed. New_DSequence.pos_single x)"
+
+definition pos_bind :: "'a pos_random_dseq => ('a \<Rightarrow> 'b pos_random_dseq) \<Rightarrow> 'b pos_random_dseq"
+where
+ "pos_bind R f = (\<lambda>nrandom size seed. New_DSequence.pos_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
+definition pos_union :: "'a pos_random_dseq => 'a pos_random_dseq => 'a pos_random_dseq"
+where
+ "pos_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.pos_union (R1 nrandom size seed) (R2 nrandom size seed))"
+
+definition pos_if_random_dseq :: "bool => unit pos_random_dseq"
+where
+ "pos_if_random_dseq b = (if b then pos_single () else pos_empty)"
+
+definition pos_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a pos_random_dseq"
+where
+ "pos_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.pos_iterate_upto f n m)"
+
+definition pos_not_random_dseq :: "unit neg_random_dseq => unit pos_random_dseq"
+where
+ "pos_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.pos_not_seq (R nrandom size seed))"
+
+fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence"
+where
+ "iter random nrandom seed =
+ (if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom - 1) seed')))"
+
+definition Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a pos_random_dseq"
+where
+ "Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
+
+definition pos_map :: "('a => 'b) => 'a pos_random_dseq => 'b pos_random_dseq"
+where
+ "pos_map f P = pos_bind P (pos_single o f)"
+
+
+definition neg_empty :: "'a neg_random_dseq"
+where
+ "neg_empty = (%nrandom size seed. New_DSequence.neg_empty)"
+
+definition neg_single :: "'a => 'a neg_random_dseq"
+where
+ "neg_single x = (%nrandom size seed. New_DSequence.neg_single x)"
+
+definition neg_bind :: "'a neg_random_dseq => ('a \<Rightarrow> 'b neg_random_dseq) \<Rightarrow> 'b neg_random_dseq"
+where
+ "neg_bind R f = (\<lambda>nrandom size seed. New_DSequence.neg_bind (R nrandom size seed) (%a. f a nrandom size seed))"
+
+definition neg_union :: "'a neg_random_dseq => 'a neg_random_dseq => 'a neg_random_dseq"
+where
+ "neg_union R1 R2 = (\<lambda>nrandom size seed. New_DSequence.neg_union (R1 nrandom size seed) (R2 nrandom size seed))"
+
+definition neg_if_random_dseq :: "bool => unit neg_random_dseq"
+where
+ "neg_if_random_dseq b = (if b then neg_single () else neg_empty)"
+
+definition neg_iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a neg_random_dseq"
+where
+ "neg_iterate_upto f n m = (\<lambda>nrandom size seed. New_DSequence.neg_iterate_upto f n m)"
+
+definition neg_not_random_dseq :: "unit pos_random_dseq => unit neg_random_dseq"
+where
+ "neg_not_random_dseq R = (\<lambda>nrandom size seed. New_DSequence.neg_not_seq (R nrandom size seed))"
+(*
+fun iter :: "(code_numeral * code_numeral => ('a * (unit => term)) * code_numeral * code_numeral) => code_numeral => code_numeral * code_numeral => 'a Lazy_Sequence.lazy_sequence"
+where
+ "iter random nrandom seed =
+ (if nrandom = 0 then Lazy_Sequence.empty else Lazy_Sequence.Lazy_Sequence (%u. let ((x, _), seed') = random seed in Some (x, iter random (nrandom - 1) seed')))"
+
+definition Random :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed)) \<Rightarrow> 'a pos_random_dseq"
+where
+ "Random g = (%nrandom size seed depth. iter (g size) nrandom seed)"
+*)
+definition neg_map :: "('a => 'b) => 'a neg_random_dseq => 'b neg_random_dseq"
+where
+ "neg_map f P = neg_bind P (neg_single o f)"
+(*
+hide const DSequence.empty DSequence.single DSequence.eval
+ DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
+ DSequence.map
+*)
+
+hide (open) const
+ pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
+ neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
+hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
+(* FIXME: hide facts *)
+(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
+
+end
\ No newline at end of file
--- a/src/HOL/Predicate.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Predicate.thy Thu Apr 01 10:27:06 2010 +0200
@@ -516,7 +516,7 @@
lemma is_empty_sup:
"is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
- by (auto simp add: is_empty_def intro: sup_eq_bot_eq1 sup_eq_bot_eq2)
+ by (auto simp add: is_empty_def)
definition singleton :: "(unit => 'a) \<Rightarrow> 'a pred \<Rightarrow> 'a" where
"singleton dfault A = (if \<exists>!x. eval A x then THE x. eval A x else dfault ())"
--- a/src/HOL/Predicate_Compile.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Predicate_Compile.thy Thu Apr 01 10:27:06 2010 +0200
@@ -5,13 +5,15 @@
header {* A compiler for predicates defined by introduction rules *}
theory Predicate_Compile
-imports Random_Sequence Quickcheck
+imports New_Random_Sequence
uses
"Tools/Predicate_Compile/predicate_compile_aux.ML"
+ "Tools/Predicate_Compile/predicate_compile_compilations.ML"
"Tools/Predicate_Compile/predicate_compile_core.ML"
"Tools/Predicate_Compile/predicate_compile_data.ML"
"Tools/Predicate_Compile/predicate_compile_fun.ML"
"Tools/Predicate_Compile/predicate_compile_pred.ML"
+ "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
"Tools/Predicate_Compile/predicate_compile.ML"
begin
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Thu Apr 01 10:27:06 2010 +0200
@@ -16,7 +16,6 @@
value "False'"
-
inductive True' :: "bool"
where
"True ==> True'"
@@ -788,7 +787,7 @@
definition
"case_f xs ys = (case (xs @ ys) of [] => [] | (x # xs) => xs)"
-code_pred [inductify] case_f .
+code_pred [inductify, skip_proof] case_f .
thm case_fP.equation
thm case_fP.intros
@@ -841,7 +840,6 @@
values "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"
(*values [depth_limited 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*)
-declare list.size(3,4)[code_pred_def]
lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
(*
code_pred [inductify] lexn .
@@ -888,7 +886,7 @@
by auto
qed
-code_pred [random_dseq inductify] lexn
+code_pred [random_dseq] lexn
proof -
fix r n xs ys
assume 1: "lexn r n (xs, ys)"
@@ -903,26 +901,21 @@
apply fastsimp done
qed
+values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
-values [random_dseq 1, 2, 5] 10 "{(n, xs, ys::int list). lexn (%(x, y). x <= y) n (xs, ys)}"
-thm lenlex_conv
-thm lex_conv
-declare list.size(3,4)[code_pred_def]
-(*code_pred [inductify, show_steps, show_intermediate_results] length .*)
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name Orderings.top_class.top}] *}
-code_pred [inductify] lex .
+code_pred [inductify, skip_proof] lex .
thm lex.equation
thm lex_def
declare lenlex_conv[code_pred_def]
-code_pred [inductify] lenlex .
+code_pred [inductify, skip_proof] lenlex .
thm lenlex.equation
code_pred [random_dseq inductify] lenlex .
thm lenlex.random_dseq_equation
values [random_dseq 4, 2, 4] 100 "{(xs, ys::int list). lenlex (%(x, y). x <= y) (xs, ys)}"
+
thm lists.intros
-
code_pred [inductify] lists .
thm lists.equation
@@ -965,8 +958,8 @@
thm is_ord_aux.equation
thm is_ord.equation
+subsection {* Definitions about Relations *}
-subsection {* Definitions about Relations *}
term "converse"
code_pred (modes:
(i * i => bool) => i * i => bool,
@@ -1030,14 +1023,14 @@
subsection {* Inverting list functions *}
-(*code_pred [inductify] length .
-code_pred [random inductify] length .
+code_pred [inductify] size_list .
+code_pred [new_random_dseq inductify] size_list .
thm size_listP.equation
-thm size_listP.random_equation
-*)
-(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*)
+thm size_listP.new_random_dseq_equation
-code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify] List.concat .
+values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
+
+code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
thm concatP.equation
values "{ys. concatP [[1, 2], [3, (4::int)]] ys}"
@@ -1068,31 +1061,31 @@
values "{x. tlP [1, 2, (3::nat)] x}"
values "{x. tlP [1, 2, (3::int)] [3]}"
-code_pred [inductify] last .
+code_pred [inductify, skip_proof] last .
thm lastP.equation
-code_pred [inductify] butlast .
+code_pred [inductify, skip_proof] butlast .
thm butlastP.equation
-code_pred [inductify] take .
+code_pred [inductify, skip_proof] take .
thm takeP.equation
-code_pred [inductify] drop .
+code_pred [inductify, skip_proof] drop .
thm dropP.equation
-code_pred [inductify] zip .
+code_pred [inductify, skip_proof] zip .
thm zipP.equation
-code_pred [inductify] upt .
-code_pred [inductify] remdups .
+code_pred [inductify, skip_proof] upt .
+code_pred [inductify, skip_proof] remdups .
thm remdupsP.equation
code_pred [dseq inductify] remdups .
values [dseq 4] 5 "{xs. remdupsP xs [1, (2::int)]}"
-code_pred [inductify] remove1 .
+code_pred [inductify, skip_proof] remove1 .
thm remove1P.equation
values "{xs. remove1P 1 xs [2, (3::int)]}"
-code_pred [inductify] removeAll .
+code_pred [inductify, skip_proof] removeAll .
thm removeAllP.equation
code_pred [dseq inductify] removeAll .
@@ -1100,17 +1093,17 @@
code_pred [inductify] distinct .
thm distinct.equation
-code_pred [inductify] replicate .
+code_pred [inductify, skip_proof] replicate .
thm replicateP.equation
values 5 "{(n, xs). replicateP n (0::int) xs}"
-code_pred [inductify] splice .
+code_pred [inductify, skip_proof] splice .
thm splice.simps
thm spliceP.equation
values "{xs. spliceP xs [1, 2, 3] [1, 1, 1, 2, 1, (3::nat)]}"
-code_pred [inductify] List.rev .
+code_pred [inductify, skip_proof] List.rev .
code_pred [inductify] map .
code_pred [inductify] foldr .
code_pred [inductify] foldl .
@@ -1159,7 +1152,7 @@
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
-code_pred [inductify] S\<^isub>3p .
+code_pred [inductify, skip_proof] S\<^isub>3p .
thm S\<^isub>3p.equation
values 10 "{x. S\<^isub>3p x}"
@@ -1175,6 +1168,8 @@
code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
+hide const a b
+
subsection {* Lambda *}
datatype type =
@@ -1275,4 +1270,129 @@
values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
+section {* Function predicate replacement *}
+
+text {*
+If the mode analysis uses the functional mode, we
+replace predicates that resulted from functions again by their functions.
+*}
+
+inductive test_append
+where
+ "List.append xs ys = zs ==> test_append xs ys zs"
+
+code_pred [inductify, skip_proof] test_append .
+thm test_append.equation
+
+text {* If append is not turned into a predicate, then the mode
+ o => o => i => bool could not be inferred. *}
+
+values 4 "{(xs::int list, ys). test_append xs ys [1, 2, 3, 4]}"
+
+text {* If appendP is not reverted back to a function, then mode i => i => o => bool
+ fails after deleting the predicate equation. *}
+
+declare appendP.equation[code del]
+
+values "{xs::int list. test_append [1,2] [3,4] xs}"
+values "{xs::int list. test_append (replicate 1000 1) (replicate 1000 2) xs}"
+values "{xs::int list. test_append (replicate 2000 1) (replicate 2000 2) xs}"
+
+subsection {* Function with tuples *}
+
+fun append'
+where
+ "append' ([], ys) = ys"
+| "append' (x # xs, ys) = x # append' (xs, ys)"
+
+inductive test_append'
+where
+ "append' (xs, ys) = zs ==> test_append' xs ys zs"
+
+code_pred [inductify, skip_proof] test_append' .
+
+thm test_append'.equation
+
+values "{(xs::int list, ys). test_append' xs ys [1, 2, 3, 4]}"
+
+declare append'P.equation[code del]
+
+values "{zs :: int list. test_append' [1,2,3] [4,5] zs}"
+
+section {* Arithmetic examples *}
+
+subsection {* Examples on nat *}
+
+inductive plus_nat_test :: "nat => nat => nat => bool"
+where
+ "x + y = z ==> plus_nat_test x y z"
+
+code_pred [inductify, skip_proof] plus_nat_test .
+code_pred [new_random_dseq inductify] plus_nat_test .
+
+thm plus_nat_test.equation
+thm plus_nat_test.new_random_dseq_equation
+
+values [expected "{9::nat}"] "{z. plus_nat_test 4 5 z}"
+values [expected "{9::nat}"] "{z. plus_nat_test 7 2 z}"
+values [expected "{4::nat}"] "{y. plus_nat_test 5 y 9}"
+values [expected "{}"] "{y. plus_nat_test 9 y 8}"
+values [expected "{6::nat}"] "{y. plus_nat_test 1 y 7}"
+values [expected "{2::nat}"] "{x. plus_nat_test x 7 9}"
+values [expected "{}"] "{x. plus_nat_test x 9 7}"
+values [expected "{(0::nat,0::nat)}"] "{(x, y). plus_nat_test x y 0}"
+values [expected "{(0, Suc 0), (Suc 0, 0)}"] "{(x, y). plus_nat_test x y 1}"
+values [expected "{(0, 5), (4, Suc 0), (3, 2), (2, 3), (Suc 0, 4), (5, 0)}"]
+ "{(x, y). plus_nat_test x y 5}"
+
+inductive minus_nat_test :: "nat => nat => nat => bool"
+where
+ "x - y = z ==> minus_nat_test x y z"
+
+code_pred [inductify, skip_proof] minus_nat_test .
+code_pred [new_random_dseq inductify] minus_nat_test .
+
+thm minus_nat_test.equation
+thm minus_nat_test.new_random_dseq_equation
+
+values [expected "{0::nat}"] "{z. minus_nat_test 4 5 z}"
+values [expected "{5::nat}"] "{z. minus_nat_test 7 2 z}"
+values [expected "{16::nat}"] "{x. minus_nat_test x 7 9}"
+values [expected "{16::nat}"] "{x. minus_nat_test x 9 7}"
+values [expected "{0, Suc 0, 2, 3}"] "{x. minus_nat_test x 3 0}"
+values [expected "{0::nat}"] "{x. minus_nat_test x 0 0}"
+
+subsection {* Examples on int *}
+
+inductive plus_int_test :: "int => int => int => bool"
+where
+ "a + b = c ==> plus_int_test a b c"
+
+code_pred [inductify, skip_proof] plus_int_test .
+code_pred [new_random_dseq inductify] plus_int_test .
+
+thm plus_int_test.equation
+thm plus_int_test.new_random_dseq_equation
+
+values [expected "{1::int}"] "{a. plus_int_test a 6 7}"
+values [expected "{1::int}"] "{b. plus_int_test 6 b 7}"
+values [expected "{11::int}"] "{c. plus_int_test 5 6 c}"
+
+inductive minus_int_test :: "int => int => int => bool"
+where
+ "a - b = c ==> minus_int_test a b c"
+
+code_pred [inductify, skip_proof] minus_int_test .
+code_pred [new_random_dseq inductify] minus_int_test .
+
+thm minus_int_test.equation
+thm minus_int_test.new_random_dseq_equation
+
+values [expected "{4::int}"] "{c. minus_int_test 9 5 c}"
+values [expected "{9::int}"] "{a. minus_int_test a 4 5}"
+values [expected "{- 1::int}"] "{b. minus_int_test 4 b 5}"
+
+
+
+
end
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Thu Apr 01 10:27:06 2010 +0200
@@ -108,7 +108,7 @@
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
-code_pred [inductify] S\<^isub>3 .
+code_pred [inductify, skip_proof] S\<^isub>3 .
thm S\<^isub>3.equation
(*
values 10 "{x. S\<^isub>3 x}"
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Apr 01 10:27:06 2010 +0200
@@ -1,1 +1,1 @@
-use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples"];
+use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Thu Apr 01 10:27:06 2010 +0200
@@ -0,0 +1,241 @@
+theory Specialisation_Examples
+imports Main Predicate_Compile_Alternative_Defs
+begin
+
+section {* Specialisation Examples *}
+
+fun nth_el'
+where
+ "nth_el' [] i = None"
+| "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
+
+definition
+ "greater_than_index xs = (\<forall>i x. nth_el' xs i = Some x --> x > i)"
+
+code_pred (expected_modes: i => bool) [inductify] greater_than_index .
+ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_nth_el'P} *}
+
+thm greater_than_index.equation
+
+values [expected "{()}"] "{x. greater_than_index [1,2,4,6]}"
+values [expected "{}"] "{x. greater_than_index [0,2,3,2]}"
+
+subsection {* Common subterms *}
+
+text {* If a predicate is called with common subterms as arguments,
+ this predicate should be specialised.
+*}
+
+definition max_nat :: "nat => nat => nat"
+ where "max_nat a b = (if a <= b then b else a)"
+
+lemma [code_pred_inline]:
+ "max = max_nat"
+by (simp add: expand_fun_eq max_def max_nat_def)
+
+definition
+ "max_of_my_Suc x = max x (Suc x)"
+
+text {* In this example, max is specialised, hence the mode o => i => bool is possible *}
+
+code_pred (modes: o => i => bool) [inductify] max_of_my_Suc .
+
+thm max_of_my_SucP.equation
+
+ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name specialised_max_natP} *}
+
+values "{x. max_of_my_SucP x 6}"
+
+subsection {* Sorts *}
+
+code_pred [inductify] sorted .
+thm sorted.equation
+
+section {* Specialisation in POPLmark theory *}
+
+notation
+ Some ("\<lfloor>_\<rfloor>")
+
+notation
+ None ("\<bottom>")
+
+notation
+ length ("\<parallel>_\<parallel>")
+
+notation
+ Cons ("_ \<Colon>/ _" [66, 65] 65)
+
+primrec
+ nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
+where
+ "[]\<langle>i\<rangle> = \<bottom>"
+| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> \<lfloor>x\<rfloor> | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
+
+primrec assoc :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" ("_\<langle>_\<rangle>\<^isub>?" [90, 0] 91)
+where
+ "[]\<langle>a\<rangle>\<^isub>? = \<bottom>"
+| "(x # xs)\<langle>a\<rangle>\<^isub>? = (if fst x = a then \<lfloor>snd x\<rfloor> else xs\<langle>a\<rangle>\<^isub>?)"
+
+primrec unique :: "('a \<times> 'b) list \<Rightarrow> bool"
+where
+ "unique [] = True"
+| "unique (x # xs) = (xs\<langle>fst x\<rangle>\<^isub>? = \<bottom> \<and> unique xs)"
+
+datatype type =
+ TVar nat
+ | Top
+ | Fun type type (infixr "\<rightarrow>" 200)
+ | TyAll type type ("(3\<forall><:_./ _)" [0, 10] 10)
+
+datatype binding = VarB type | TVarB type
+types env = "binding list"
+
+primrec is_TVarB :: "binding \<Rightarrow> bool"
+where
+ "is_TVarB (VarB T) = False"
+| "is_TVarB (TVarB T) = True"
+
+primrec type_ofB :: "binding \<Rightarrow> type"
+where
+ "type_ofB (VarB T) = T"
+| "type_ofB (TVarB T) = T"
+
+primrec mapB :: "(type \<Rightarrow> type) \<Rightarrow> binding \<Rightarrow> binding"
+where
+ "mapB f (VarB T) = VarB (f T)"
+| "mapB f (TVarB T) = TVarB (f T)"
+
+datatype trm =
+ Var nat
+ | Abs type trm ("(3\<lambda>:_./ _)" [0, 10] 10)
+ | TAbs type trm ("(3\<lambda><:_./ _)" [0, 10] 10)
+ | App trm trm (infixl "\<bullet>" 200)
+ | TApp trm type (infixl "\<bullet>\<^isub>\<tau>" 200)
+
+primrec liftT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<up>\<^isub>\<tau>")
+where
+ "\<up>\<^isub>\<tau> n k (TVar i) = (if i < k then TVar i else TVar (i + n))"
+| "\<up>\<^isub>\<tau> n k Top = Top"
+| "\<up>\<^isub>\<tau> n k (T \<rightarrow> U) = \<up>\<^isub>\<tau> n k T \<rightarrow> \<up>\<^isub>\<tau> n k U"
+| "\<up>\<^isub>\<tau> n k (\<forall><:T. U) = (\<forall><:\<up>\<^isub>\<tau> n k T. \<up>\<^isub>\<tau> n (k + 1) U)"
+
+primrec lift :: "nat \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("\<up>")
+where
+ "\<up> n k (Var i) = (if i < k then Var i else Var (i + n))"
+| "\<up> n k (\<lambda>:T. t) = (\<lambda>:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
+| "\<up> n k (\<lambda><:T. t) = (\<lambda><:\<up>\<^isub>\<tau> n k T. \<up> n (k + 1) t)"
+| "\<up> n k (s \<bullet> t) = \<up> n k s \<bullet> \<up> n k t"
+| "\<up> n k (t \<bullet>\<^isub>\<tau> T) = \<up> n k t \<bullet>\<^isub>\<tau> \<up>\<^isub>\<tau> n k T"
+
+primrec substTT :: "type \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>\<tau>" [300, 0, 0] 300)
+where
+ "(TVar i)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> =
+ (if k < i then TVar (i - 1) else if i = k then \<up>\<^isub>\<tau> k 0 S else TVar i)"
+| "Top[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = Top"
+| "(T \<rightarrow> U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> \<rightarrow> U[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>"
+| "(\<forall><:T. U)[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau> = (\<forall><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. U[k+1 \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>)"
+
+primrec decT :: "nat \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> type" ("\<down>\<^isub>\<tau>")
+where
+ "\<down>\<^isub>\<tau> 0 k T = T"
+| "\<down>\<^isub>\<tau> (Suc n) k T = \<down>\<^isub>\<tau> n k (T[k \<mapsto>\<^isub>\<tau> Top]\<^isub>\<tau>)"
+
+primrec subst :: "trm \<Rightarrow> nat \<Rightarrow> trm \<Rightarrow> trm" ("_[_ \<mapsto> _]" [300, 0, 0] 300)
+where
+ "(Var i)[k \<mapsto> s] = (if k < i then Var (i - 1) else if i = k then \<up> k 0 s else Var i)"
+| "(t \<bullet> u)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet> u[k \<mapsto> s]"
+| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto> s] = t[k \<mapsto> s] \<bullet>\<^isub>\<tau> \<down>\<^isub>\<tau> 1 k T"
+| "(\<lambda>:T. t)[k \<mapsto> s] = (\<lambda>:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
+| "(\<lambda><:T. t)[k \<mapsto> s] = (\<lambda><:\<down>\<^isub>\<tau> 1 k T. t[k+1 \<mapsto> s])"
+
+primrec substT :: "trm \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> trm" ("_[_ \<mapsto>\<^isub>\<tau> _]" [300, 0, 0] 300)
+where
+ "(Var i)[k \<mapsto>\<^isub>\<tau> S] = (if k < i then Var (i - 1) else Var i)"
+| "(t \<bullet> u)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet> u[k \<mapsto>\<^isub>\<tau> S]"
+| "(t \<bullet>\<^isub>\<tau> T)[k \<mapsto>\<^isub>\<tau> S] = t[k \<mapsto>\<^isub>\<tau> S] \<bullet>\<^isub>\<tau> T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>"
+| "(\<lambda>:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda>:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
+| "(\<lambda><:T. t)[k \<mapsto>\<^isub>\<tau> S] = (\<lambda><:T[k \<mapsto>\<^isub>\<tau> S]\<^isub>\<tau>. t[k+1 \<mapsto>\<^isub>\<tau> S])"
+
+primrec liftE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<up>\<^isub>e")
+where
+ "\<up>\<^isub>e n k [] = []"
+| "\<up>\<^isub>e n k (B \<Colon> \<Gamma>) = mapB (\<up>\<^isub>\<tau> n (k + \<parallel>\<Gamma>\<parallel>)) B \<Colon> \<up>\<^isub>e n k \<Gamma>"
+
+primrec substE :: "env \<Rightarrow> nat \<Rightarrow> type \<Rightarrow> env" ("_[_ \<mapsto>\<^isub>\<tau> _]\<^isub>e" [300, 0, 0] 300)
+where
+ "[][k \<mapsto>\<^isub>\<tau> T]\<^isub>e = []"
+| "(B \<Colon> \<Gamma>)[k \<mapsto>\<^isub>\<tau> T]\<^isub>e = mapB (\<lambda>U. U[k + \<parallel>\<Gamma>\<parallel> \<mapsto>\<^isub>\<tau> T]\<^isub>\<tau>) B \<Colon> \<Gamma>[k \<mapsto>\<^isub>\<tau> T]\<^isub>e"
+
+primrec decE :: "nat \<Rightarrow> nat \<Rightarrow> env \<Rightarrow> env" ("\<down>\<^isub>e")
+where
+ "\<down>\<^isub>e 0 k \<Gamma> = \<Gamma>"
+| "\<down>\<^isub>e (Suc n) k \<Gamma> = \<down>\<^isub>e n k (\<Gamma>[k \<mapsto>\<^isub>\<tau> Top]\<^isub>e)"
+
+inductive
+ well_formed :: "env \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile>\<^bsub>wf\<^esub> _" [50, 50] 50)
+where
+ wf_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB T\<rfloor> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
+| wf_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
+| wf_arrow: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
+| wf_all: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<Longrightarrow> TVarB T \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> U \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
+
+inductive
+ well_formedE :: "env \<Rightarrow> bool" ("_ \<turnstile>\<^bsub>wf\<^esub>" [50] 50)
+ and well_formedB :: "env \<Rightarrow> binding \<Rightarrow> bool" ("_ \<turnstile>\<^bsub>wfB\<^esub> _" [50, 50] 50)
+where
+ "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<equiv> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> type_ofB B"
+| wf_Nil: "[] \<turnstile>\<^bsub>wf\<^esub>"
+| wf_Cons: "\<Gamma> \<turnstile>\<^bsub>wfB\<^esub> B \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
+
+inductive_cases well_formed_cases:
+ "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i"
+ "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> Top"
+ "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> T \<rightarrow> U"
+ "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> (\<forall><:T. U)"
+
+inductive_cases well_formedE_cases:
+ "B \<Colon> \<Gamma> \<turnstile>\<^bsub>wf\<^esub>"
+
+inductive
+ subtyping :: "env \<Rightarrow> type \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ <: _" [50, 50, 50] 50)
+where
+ SA_Top: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> S \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
+| SA_refl_TVar: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>wf\<^esub> TVar i \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: TVar i"
+| SA_trans_TVar: "\<Gamma>\<langle>i\<rangle> = \<lfloor>TVarB U\<rfloor> \<Longrightarrow>
+ \<Gamma> \<turnstile> \<up>\<^isub>\<tau> (Suc i) 0 U <: T \<Longrightarrow> \<Gamma> \<turnstile> TVar i <: T"
+| SA_arrow: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> S\<^isub>1 \<rightarrow> S\<^isub>2 <: T\<^isub>1 \<rightarrow> T\<^isub>2"
+| SA_all: "\<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<Longrightarrow> TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> S\<^isub>2 <: T\<^isub>2 \<Longrightarrow>
+ \<Gamma> \<turnstile> (\<forall><:S\<^isub>1. S\<^isub>2) <: (\<forall><:T\<^isub>1. T\<^isub>2)"
+
+inductive
+ typing :: "env \<Rightarrow> trm \<Rightarrow> type \<Rightarrow> bool" ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+where
+ T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
+| T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2"
+| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>1\<^isub>2"
+| T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)"
+| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<Longrightarrow>
+ \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
+| T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
+
+code_pred [inductify, skip_proof] typing .
+
+thm typing.equation
+
+values 6 "{(E, t, T). typing E t T}"
+
+subsection {* Higher-order predicate *}
+
+code_pred [inductify] mapB .
+
+subsection {* Multiple instances *}
+
+inductive subtype_refl' where
+ "\<Gamma> \<turnstile> t : T ==> \<not> (\<Gamma> \<turnstile> T <: T) ==> subtype_refl' t T"
+
+code_pred (modes: i => i => bool, o => i => bool, i => o => bool, o => o => bool) [inductify] subtype_refl' .
+
+thm subtype_refl'.equation
+
+
+end
\ No newline at end of file
--- a/src/HOL/Quickcheck.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Quickcheck.thy Thu Apr 01 10:27:06 2010 +0200
@@ -187,6 +187,10 @@
where
"if_randompred b = (if b then single () else empty)"
+definition iterate_upto :: "(code_numeral => 'a) => code_numeral => code_numeral => 'a randompred"
+where
+ "iterate_upto f n m = Pair (Code_Numeral.iterate_upto f n m)"
+
definition not_randompred :: "unit randompred \<Rightarrow> unit randompred"
where
"not_randompred P = (\<lambda>s. let
@@ -199,9 +203,9 @@
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a randompred \<Rightarrow> 'b randompred)"
where "map f P = bind P (single o f)"
-hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def not_randompred_def Random_def map_def
+hide (open) fact iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
hide (open) type randompred
hide (open) const random collapse beyond random_fun_aux random_fun_lift
- iter' iter empty single bind union if_randompred not_randompred Random map
+ iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
end
--- a/src/HOL/Random.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Random.thy Thu Apr 01 10:27:06 2010 +0200
@@ -1,3 +1,4 @@
+
(* Author: Florian Haftmann, TU Muenchen *)
header {* A HOL random engine *}
@@ -154,6 +155,14 @@
in
+fun next_seed () =
+ let
+ val (seed1, seed') = @{code split_seed} (! seed)
+ val _ = seed := seed'
+ in
+ seed1
+ end
+
fun run f =
let
val (x, seed') = f (! seed);
--- a/src/HOL/Set.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Set.thy Thu Apr 01 10:27:06 2010 +0200
@@ -507,7 +507,6 @@
apply (rule Collect_mem_eq)
done
-(* Due to Brian Huffman *)
lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
by(auto intro:set_ext)
@@ -1002,25 +1001,25 @@
text {* \medskip Finite Union -- the least upper bound of two sets. *}
lemma Un_upper1: "A \<subseteq> A \<union> B"
- by blast
+ by (fact sup_ge1)
lemma Un_upper2: "B \<subseteq> A \<union> B"
- by blast
+ by (fact sup_ge2)
lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
- by blast
+ by (fact sup_least)
text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
lemma Int_lower1: "A \<inter> B \<subseteq> A"
- by blast
+ by (fact inf_le1)
lemma Int_lower2: "A \<inter> B \<subseteq> B"
- by blast
+ by (fact inf_le2)
lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
- by blast
+ by (fact inf_greatest)
text {* \medskip Set difference. *}
@@ -1166,34 +1165,34 @@
text {* \medskip @{text Int} *}
lemma Int_absorb [simp]: "A \<inter> A = A"
- by blast
+ by (fact inf_idem)
lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
- by blast
+ by (fact inf_left_idem)
lemma Int_commute: "A \<inter> B = B \<inter> A"
- by blast
+ by (fact inf_commute)
lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
- by blast
+ by (fact inf_left_commute)
lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
- by blast
+ by (fact inf_assoc)
lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
-- {* Intersection is an AC-operator *}
lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
- by blast
+ by (fact inf_absorb2)
lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
- by blast
+ by (fact inf_absorb1)
lemma Int_empty_left [simp]: "{} \<inter> B = {}"
- by blast
+ by (fact inf_bot_left)
lemma Int_empty_right [simp]: "A \<inter> {} = {}"
- by blast
+ by (fact inf_bot_right)
lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
by blast
@@ -1202,22 +1201,22 @@
by blast
lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
- by blast
+ by (fact inf_top_left)
lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
- by blast
+ by (fact inf_top_right)
lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
- by blast
+ by (fact inf_sup_distrib1)
lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
- by blast
+ by (fact inf_sup_distrib2)
lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
- by blast
+ by (fact inf_eq_top_iff)
lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
- by blast
+ by (fact le_inf_iff)
lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
by blast
@@ -1226,40 +1225,40 @@
text {* \medskip @{text Un}. *}
lemma Un_absorb [simp]: "A \<union> A = A"
- by blast
+ by (fact sup_idem)
lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
- by blast
+ by (fact sup_left_idem)
lemma Un_commute: "A \<union> B = B \<union> A"
- by blast
+ by (fact sup_commute)
lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
- by blast
+ by (fact sup_left_commute)
lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
- by blast
+ by (fact sup_assoc)
lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
-- {* Union is an AC-operator *}
lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
- by blast
+ by (fact sup_absorb2)
lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
- by blast
+ by (fact sup_absorb1)
lemma Un_empty_left [simp]: "{} \<union> B = B"
- by blast
+ by (fact sup_bot_left)
lemma Un_empty_right [simp]: "A \<union> {} = A"
- by blast
+ by (fact sup_bot_right)
lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
- by blast
+ by (fact sup_top_left)
lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
- by blast
+ by (fact sup_top_right)
lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
by blast
@@ -1292,23 +1291,23 @@
by auto
lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
- by blast
+ by (fact sup_inf_distrib1)
lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
- by blast
+ by (fact sup_inf_distrib2)
lemma Un_Int_crazy:
"(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
by blast
lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
- by blast
+ by (fact le_iff_sup)
lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
- by blast
+ by (fact sup_eq_bot_iff)
lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
- by blast
+ by (fact le_sup_iff)
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
by blast
@@ -1320,25 +1319,25 @@
text {* \medskip Set complement *}
lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
- by blast
+ by (fact inf_compl_bot)
lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
- by blast
+ by (fact compl_inf_bot)
lemma Compl_partition: "A \<union> -A = UNIV"
- by blast
+ by (fact sup_compl_top)
lemma Compl_partition2: "-A \<union> A = UNIV"
- by blast
+ by (fact compl_sup_top)
lemma double_complement [simp]: "- (-A) = (A::'a set)"
- by blast
+ by (fact double_compl)
lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
- by blast
+ by (fact compl_sup)
lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
- by blast
+ by (fact compl_inf)
lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
by blast
@@ -1348,16 +1347,16 @@
by blast
lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
- by blast
+ by (fact compl_top_eq)
lemma Compl_empty_eq [simp]: "-{} = UNIV"
- by blast
+ by (fact compl_bot_eq)
lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
- by blast
+ by (fact compl_le_compl_iff)
lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
- by blast
+ by (fact compl_eq_compl_iff)
text {* \medskip Bounded quantifiers.
@@ -1531,16 +1530,16 @@
by blast
lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
- by blast
+ by (fact sup_mono)
lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
- by blast
+ by (fact inf_mono)
lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
by blast
lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
- by blast
+ by (fact compl_mono)
text {* \medskip Monotonicity of implications. *}
--- a/src/HOL/SupInf.thy Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/SupInf.thy Thu Apr 01 10:27:06 2010 +0200
@@ -106,10 +106,10 @@
proof (cases "Sup X \<le> a")
case True
thus ?thesis
- apply (simp add: max_def)
+ apply (simp add: max_def)
apply (rule Sup_eq_maximum)
- apply (metis insertCI)
- apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)
+ apply (rule insertI1)
+ apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans)
done
next
case False
@@ -177,7 +177,7 @@
fixes S :: "real set"
assumes fS: "finite S" and Se: "S \<noteq> {}"
shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans)
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans)
lemma Sup_finite_gt_iff:
fixes S :: "real set"
@@ -331,8 +331,8 @@
have "Inf (insert a X) \<le> Inf X"
apply (rule Inf_greatest)
apply (metis empty_psubset_nonempty psubset_eq x)
- apply (rule Inf_lower_EX)
- apply (blast intro: elim:)
+ apply (rule Inf_lower_EX)
+ apply (erule insertI2)
apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
done
moreover
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Apr 01 10:27:06 2010 +0200
@@ -7,15 +7,19 @@
signature PREDICATE_COMPILE =
sig
val setup : theory -> theory
- val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
+ val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory
val present_graph : bool Unsynchronized.ref
+ val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
end;
-structure Predicate_Compile (*: PREDICATE_COMPILE*) =
+structure Predicate_Compile : PREDICATE_COMPILE =
struct
val present_graph = Unsynchronized.ref false
+val intro_hook = Unsynchronized.ref NONE : (theory -> thm -> unit) option Unsynchronized.ref
+
+
open Predicate_Compile_Aux;
(* Some last processing *)
@@ -93,7 +97,7 @@
val _ = print_step options
("Compiling functions (" ^ commas (map (Syntax.string_of_term_global thy) funnames) ^
") to predicates...")
- val (fun_pred_specs, thy') =
+ val (fun_pred_specs, thy1) =
(if function_flattening options andalso (not (null funnames)) then
if fail_safe_function_flattening options then
case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
@@ -102,21 +106,26 @@
else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy
else ([], thy))
(*||> Theory.checkpoint*)
- val _ = print_specs options thy' fun_pred_specs
+ val _ = print_specs options thy1 fun_pred_specs
val specs = (get_specs prednames) @ fun_pred_specs
- val (intross3, thy''') = process_specification options specs thy'
- val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
+ val (intross3, thy2) = process_specification options specs thy1
+ val _ = print_intross options thy2 "Introduction rules with new constants: " intross3
val intross4 = map_specs (maps remove_pointless_clauses) intross3
- val _ = print_intross options thy''' "After removing pointless clauses: " intross4
- val intross5 =
- map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
- val intross6 = map_specs (map (expand_tuples thy''')) intross5
- val intross7 = map_specs (map (eta_contract_ho_arguments thy''')) intross6
- val _ = print_intross options thy''' "introduction rules before registering: " intross7
+ val _ = print_intross options thy2 "After removing pointless clauses: " intross4
+ val intross5 = map_specs (map (remove_equalities thy2)) intross4
+ val _ = print_intross options thy2 "After removing equality premises:" intross5
+ val intross6 =
+ map (fn (s, ths) => (overload_const thy2 s, map (AxClass.overload thy2) ths)) intross5
+ val intross7 = map_specs (map (expand_tuples thy2)) intross6
+ val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
+ val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
+ val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
+ val (intross9, thy3) = Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
+ val _ = print_intross options thy3 "introduction rules before registering: " intross9
val _ = print_step options "Registering introduction rules..."
- val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''
+ val thy4 = fold Predicate_Compile_Core.register_intros intross9 thy3
in
- thy''''
+ thy4
end;
fun preprocess options t thy =
@@ -170,7 +179,6 @@
if (is_inductify options) then
let
val lthy' = Local_Theory.theory (preprocess options t) lthy
- |> Local_Theory.checkpoint
val const =
case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
SOME c => c
@@ -229,6 +237,8 @@
val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
+val stats = Scan.optional (Args.$$$ "stats" >> K true) false
+
val value_options =
let
val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
@@ -239,7 +249,8 @@
compilation_names))
(Pred, [])
in
- Scan.optional (P.$$$ "[" |-- expected_values -- scan_compilation --| P.$$$ "]") (NONE, (Pred, []))
+ Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
+ ((NONE, false), (Pred, []))
end
(* code_pred command and values command *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Apr 01 10:27:06 2010 +0200
@@ -4,9 +4,140 @@
Auxilary functions for predicate compiler.
*)
-(* FIXME proper signature! *)
+signature PREDICATE_COMPILE_AUX =
+sig
+ (* general functions *)
+ val apfst3 : ('a -> 'd) -> 'a * 'b * 'c -> 'd * 'b * 'c
+ val apsnd3 : ('b -> 'd) -> 'a * 'b * 'c -> 'a * 'd * 'c
+ val aptrd3 : ('c -> 'd) -> 'a * 'b * 'c -> 'a * 'b * 'd
+ val find_indices : ('a -> bool) -> 'a list -> int list
+ val assert : bool -> unit
+ (* mode *)
+ datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
+ val eq_mode : mode * mode -> bool
+ val list_fun_mode : mode list -> mode
+ val strip_fun_mode : mode -> mode list
+ val dest_fun_mode : mode -> mode list
+ val dest_tuple_mode : mode -> mode list
+ val all_modes_of_typ : typ -> mode list
+ val all_smodes_of_typ : typ -> mode list
+ val fold_map_aterms_prodT : ('a -> 'a -> 'a) -> (typ -> 'b -> 'a * 'b) -> typ -> 'b -> 'a * 'b
+ val map_filter_prod : (term -> term option) -> term -> term option
+ val replace_ho_args : mode -> term list -> term list -> term list
+ val ho_arg_modes_of : mode -> mode list
+ val ho_argsT_of : mode -> typ list -> typ list
+ val ho_args_of : mode -> term list -> term list
+ val split_map_mode : (mode -> term -> term option * term option)
+ -> mode -> term list -> term list * term list
+ val split_map_modeT : (mode -> typ -> typ option * typ option)
+ -> mode -> typ list -> typ list * typ list
+ val split_mode : mode -> term list -> term list * term list
+ val split_modeT' : mode -> typ list -> typ list * typ list
+ val string_of_mode : mode -> string
+ val ascii_string_of_mode : mode -> string
+ (* premises *)
+ datatype indprem = Prem of term | Negprem of term | Sidecond of term
+ | Generator of (string * typ)
+ (* general syntactic functions *)
+ val conjuncts : term -> term list
+ val is_equationlike : thm -> bool
+ val is_pred_equation : thm -> bool
+ val is_intro : string -> thm -> bool
+ val is_predT : typ -> bool
+ val is_constrt : theory -> term -> bool
+ val is_constr : Proof.context -> string -> bool
+ val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context
+ val strip_all : term -> (string * typ) list * term
+ (* introduction rule combinators *)
+ val map_atoms : (term -> term) -> term -> term
+ val fold_atoms : (term -> 'a -> 'a) -> term -> 'a -> 'a
+ val fold_map_atoms : (term -> 'a -> term * 'a) -> term -> 'a -> term * 'a
+ val maps_premises : (term -> term list) -> term -> term
+ val map_concl : (term -> term) -> term -> term
+ val map_term : theory -> (term -> term) -> thm -> thm
+ (* split theorems of case expressions *)
+ val prepare_split_thm : Proof.context -> thm -> thm
+ val find_split_thm : theory -> term -> thm option
+ (* datastructures and setup for generic compilation *)
+ datatype compilation_funs = CompilationFuns of {
+ mk_predT : typ -> typ,
+ dest_predT : typ -> typ,
+ mk_bot : typ -> term,
+ mk_single : term -> term,
+ mk_bind : term * term -> term,
+ mk_sup : term * term -> term,
+ mk_if : term -> term,
+ mk_iterate_upto : typ -> term * term * term -> term,
+ mk_not : term -> term,
+ mk_map : typ -> typ -> term -> term -> term
+ };
+ val mk_predT : compilation_funs -> typ -> typ
+ val dest_predT : compilation_funs -> typ -> typ
+ val mk_bot : compilation_funs -> typ -> term
+ val mk_single : compilation_funs -> term -> term
+ val mk_bind : compilation_funs -> term * term -> term
+ val mk_sup : compilation_funs -> term * term -> term
+ val mk_if : compilation_funs -> term -> term
+ val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
+ val mk_not : compilation_funs -> term -> term
+ val mk_map : compilation_funs -> typ -> typ -> term -> term -> term
+ val funT_of : compilation_funs -> mode -> typ -> typ
+ (* Different compilations *)
+ datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
+ | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
+ val negative_compilation_of : compilation -> compilation
+ val compilation_for_polarity : bool -> compilation -> compilation
+ val string_of_compilation : compilation -> string
+ val compilation_names : (string * compilation) list
+ val non_random_compilations : compilation list
+ val random_compilations : compilation list
+ (* Different options for compiler *)
+ datatype options = Options of {
+ expected_modes : (string * mode list) option,
+ proposed_modes : (string * mode list) option,
+ proposed_names : ((string * mode) * string) list,
+ show_steps : bool,
+ show_proof_trace : bool,
+ show_intermediate_results : bool,
+ show_mode_inference : bool,
+ show_modes : bool,
+ show_compilation : bool,
+ show_caught_failures : bool,
+ skip_proof : bool,
+ no_topmost_reordering : bool,
+ function_flattening : bool,
+ fail_safe_function_flattening : bool,
+ no_higher_order_predicate : string list,
+ inductify : bool,
+ compilation : compilation
+ };
+ val expected_modes : options -> (string * mode list) option
+ val proposed_modes : options -> (string * mode list) option
+ val proposed_names : options -> string -> mode -> string option
+ val show_steps : options -> bool
+ val show_proof_trace : options -> bool
+ val show_intermediate_results : options -> bool
+ val show_mode_inference : options -> bool
+ val show_modes : options -> bool
+ val show_compilation : options -> bool
+ val show_caught_failures : options -> bool
+ val skip_proof : options -> bool
+ val no_topmost_reordering : options -> bool
+ val function_flattening : options -> bool
+ val fail_safe_function_flattening : options -> bool
+ val no_higher_order_predicate : options -> string list
+ val is_inductify : options -> bool
+ val compilation : options -> compilation
+ val default_options : options
+ val bool_options : string list
+ val print_step : options -> string -> unit
+ (* simple transformations *)
+ val expand_tuples : theory -> thm -> thm
+ val eta_contract_ho_arguments : theory -> thm -> thm
+ val remove_equalities : theory -> thm -> thm
+end;
-structure Predicate_Compile_Aux =
+structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX =
struct
(* general functions *)
@@ -46,18 +177,21 @@
| eq_mode (Bool, Bool) = true
| eq_mode _ = false
+fun list_fun_mode [] = Bool
+ | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
+
(* name: binder_modes? *)
fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
| strip_fun_mode Bool = []
| strip_fun_mode _ = raise Fail "Bad mode for strip_fun_mode"
+(* name: 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 all_modes_of_typ' (T as Type ("fun", _)) =
let
val (S, U) = strip_type T
@@ -95,7 +229,7 @@
if U = HOLogic.boolT then
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2) (map all_smodes S) [Bool]
else
- raise Fail "all_smodes_of_typ: invalid type for predicate"
+ raise Fail "invalid type for predicate"
end
fun ho_arg_modes_of mode =
@@ -110,7 +244,7 @@
fun ho_args_of mode ts =
let
fun ho_arg (Fun _) (SOME t) = [t]
- | ho_arg (Fun _) NONE = error "ho_arg_of"
+ | ho_arg (Fun _) NONE = raise Fail "mode and term do not match"
| ho_arg (Pair (m1, m2)) (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
ho_arg m1 (SOME t1) @ ho_arg m2 (SOME t2)
| ho_arg (Pair (m1, m2)) NONE = ho_arg m1 NONE @ ho_arg m2 NONE
@@ -295,12 +429,13 @@
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
(Symtab.dest (Datatype.get_all thy)));
fun check t = (case strip_comb t of
- (Free _, []) => true
+ (Var _, []) => true
+ | (Free _, []) => true
| (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
(SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
| _ => false)
| _ => false)
- in check end;
+ in check end;
fun is_funtype (Type ("fun", [_, _])) = true
| is_funtype _ = false;
@@ -327,6 +462,8 @@
val is_constr = Code.is_constr o ProofContext.theory_of;
+fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
+
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
let
val (xTs, t') = strip_ex t
@@ -346,8 +483,6 @@
(* introduction rule combinators *)
-(* combinators to apply a function to all literals of an introduction rules *)
-
fun map_atoms f intro =
let
val (literals, head) = Logic.strip_horn intro
@@ -400,55 +535,13 @@
(* split theorems of case expressions *)
-(*
-fun has_split_rule_cname @{const_name "nat_case"} = true
- | has_split_rule_cname @{const_name "list_case"} = true
- | has_split_rule_cname _ = false
-
-fun has_split_rule_term thy (Const (@{const_name "nat_case"}, _)) = true
- | has_split_rule_term thy (Const (@{const_name "list_case"}, _)) = true
- | has_split_rule_term thy _ = false
-
-fun has_split_rule_term' thy (Const (@{const_name "If"}, _)) = true
- | has_split_rule_term' thy (Const (@{const_name "Let"}, _)) = true
- | has_split_rule_term' thy c = has_split_rule_term thy c
-
-*)
fun prepare_split_thm ctxt split_thm =
(split_thm RS @{thm iffD2})
|> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
-fun find_split_thm thy (Const (name, typ)) =
- let
- fun split_name str =
- case first_field "." str
- of (SOME (field, rest)) => field :: split_name rest
- | NONE => [str]
- val splitted_name = split_name name
- in
- if length splitted_name > 0 andalso
- String.isSuffix "_case" (List.last splitted_name)
- then
- (List.take (splitted_name, length splitted_name - 1)) @ ["split"]
- |> space_implode "."
- |> PureThy.get_thm thy
- |> SOME
- handle ERROR msg => NONE
- else NONE
- end
- | find_split_thm _ _ = NONE
-
-
-(* TODO: split rules for let and if are different *)
-fun find_split_thm' thy (Const (@{const_name "If"}, _)) = SOME @{thm split_if}
- | find_split_thm' thy (Const (@{const_name "Let"}, _)) = SOME @{thm refl} (* TODO *)
- | find_split_thm' thy c = find_split_thm thy c
-
-fun has_split_thm thy t = is_some (find_split_thm thy t)
-
-fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
-
+fun find_split_thm thy (Const (name, T)) = Option.map #split (Datatype_Data.info_of_case thy name)
+ | find_split_thm thy _ = NONE
(* lifting term operations to theorems *)
@@ -462,17 +555,19 @@
| _ => error "equals_conv"
*)
-(* Different options for compiler *)
+(* Different compilations *)
datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
- | Pos_Random_DSeq | Neg_Random_DSeq
-
+ | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
fun negative_compilation_of Pos_Random_DSeq = Neg_Random_DSeq
| negative_compilation_of Neg_Random_DSeq = Pos_Random_DSeq
+ | negative_compilation_of New_Pos_Random_DSeq = New_Neg_Random_DSeq
+ | negative_compilation_of New_Neg_Random_DSeq = New_Pos_Random_DSeq
| negative_compilation_of c = c
fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
+ | compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
| compilation_for_polarity _ c = c
fun string_of_compilation c =
@@ -485,9 +580,60 @@
| Annotated => "annotated"
| Pos_Random_DSeq => "pos_random dseq"
| Neg_Random_DSeq => "neg_random_dseq"
-
-(*datatype compilation_options =
- Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*)
+ | New_Pos_Random_DSeq => "new_pos_random dseq"
+ | New_Neg_Random_DSeq => "new_neg_random_dseq"
+
+val compilation_names = [("pred", Pred),
+ ("random", Random),
+ ("depth_limited", Depth_Limited),
+ ("depth_limited_random", Depth_Limited_Random),
+ (*("annotated", Annotated),*)
+ ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq),
+ ("new_random_dseq", New_Pos_Random_DSeq)]
+
+val non_random_compilations = [Pred, Depth_Limited, DSeq, Annotated]
+
+
+val random_compilations = [Random, Depth_Limited_Random,
+ Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
+
+(* datastructures and setup for generic compilation *)
+
+datatype compilation_funs = CompilationFuns of {
+ mk_predT : typ -> typ,
+ dest_predT : typ -> typ,
+ mk_bot : typ -> term,
+ mk_single : term -> term,
+ mk_bind : term * term -> term,
+ mk_sup : term * term -> term,
+ mk_if : term -> term,
+ mk_iterate_upto : typ -> term * term * term -> term,
+ mk_not : term -> term,
+ mk_map : typ -> typ -> term -> term -> term
+};
+
+fun mk_predT (CompilationFuns funs) = #mk_predT funs
+fun dest_predT (CompilationFuns funs) = #dest_predT funs
+fun mk_bot (CompilationFuns funs) = #mk_bot funs
+fun mk_single (CompilationFuns funs) = #mk_single funs
+fun mk_bind (CompilationFuns funs) = #mk_bind funs
+fun mk_sup (CompilationFuns funs) = #mk_sup funs
+fun mk_if (CompilationFuns funs) = #mk_if funs
+fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
+fun mk_not (CompilationFuns funs) = #mk_not funs
+fun mk_map (CompilationFuns funs) = #mk_map funs
+
+(** function types and names of different compilations **)
+
+fun funT_of compfuns mode T =
+ let
+ val Ts = binder_types T
+ val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
+ in
+ inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
+ end;
+
+(* Different options for compiler *)
datatype options = Options of {
expected_modes : (string * mode list) option,
@@ -557,17 +703,12 @@
"show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
"no_topmost_reordering"]
-val compilation_names = [("pred", Pred),
- ("random", Random),
- ("depth_limited", Depth_Limited),
- ("depth_limited_random", Depth_Limited_Random),
- (*("annotated", Annotated),*)
- ("dseq", DSeq), ("random_dseq", Pos_Random_DSeq)]
-
fun print_step options s =
if show_steps options then tracing s else ()
-(* tuple processing *)
+(* simple transformations *)
+
+(** tuple processing **)
fun expand_tuples thy intro =
let
@@ -622,8 +763,7 @@
intro'''''
end
-(* eta contract higher-order arguments *)
-
+(** eta contract higher-order arguments **)
fun eta_contract_ho_arguments thy intro =
let
@@ -632,5 +772,42 @@
map_term thy (map_concl f o map_atoms f) intro
end
+(** remove equalities **)
+
+fun remove_equalities thy intro =
+ let
+ fun remove_eqs intro_t =
+ let
+ val (prems, concl) = Logic.strip_horn intro_t
+ fun remove_eq (prems, concl) =
+ let
+ fun removable_eq prem =
+ case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
+ SOME (lhs, rhs) => (case lhs of
+ Var _ => true
+ | _ => (case rhs of Var _ => true | _ => false))
+ | NONE => false
+ in
+ case find_first removable_eq prems of
+ NONE => (prems, concl)
+ | SOME eq =>
+ let
+ val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+ val prems' = remove (op =) eq prems
+ val subst = (case lhs of
+ (v as Var _) =>
+ (fn t => if t = v then rhs else t)
+ | _ => (case rhs of
+ (v as Var _) => (fn t => if t = v then lhs else t)))
+ in
+ remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
+ end
+ end
+ in
+ Logic.list_implies (remove_eq (prems, concl))
+ end
+ in
+ map_term thy remove_eqs intro
+ end
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Thu Apr 01 10:27:06 2010 +0200
@@ -0,0 +1,319 @@
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+Structures for different compilations of the predicate compiler
+*)
+
+structure PredicateCompFuns =
+struct
+
+fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
+
+fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
+ | dest_predT T = raise TYPE ("dest_predT", [T], []);
+
+fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
+
+fun mk_single t =
+ let val T = fastype_of t
+ in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
+
+fun mk_bind (x, f) =
+ let val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name sup};
+
+fun mk_if cond = Const (@{const_name Predicate.if_pred},
+ HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) =
+ list_comb (Const (@{const_name Code_Numeral.iterate_upto},
+ [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T),
+ [f, from, to])
+
+fun mk_not t =
+ let
+ val T = mk_predT HOLogic.unitT
+ in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
+
+fun mk_Enum f =
+ let val T as Type ("fun", [T', _]) = fastype_of f
+ in
+ Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f
+ end;
+
+fun mk_Eval (f, x) =
+ let
+ val T = fastype_of x
+ in
+ Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
+ end;
+
+fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
+ (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
+ mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+
+end;
+
+structure RandomPredCompFuns =
+struct
+
+fun mk_randompredT T =
+ @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
+
+fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
+ [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
+ | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
+
+fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in
+ Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
+ end;
+
+fun mk_bind (x, f) =
+ let
+ val T as (Type ("fun", [_, U])) = fastype_of f
+ in
+ Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
+ end
+
+val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
+
+fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
+ HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) =
+ list_comb (Const (@{const_name Quickcheck.iterate_upto},
+ [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T),
+ [f, from, to])
+
+fun mk_not t =
+ let
+ val T = mk_randompredT HOLogic.unitT
+ in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
+ (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+
+end;
+
+structure DSequence_CompFuns =
+struct
+
+fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
+
+fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
+ Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
+ | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
+
+fun mk_single t =
+ let val T = fastype_of t
+ in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
+
+fun mk_if cond = Const (@{const_name DSequence.if_seq},
+ HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+
+fun mk_not t = let val T = mk_dseqT HOLogic.unitT
+ in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
+ (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
+end;
+
+structure New_Pos_Random_Sequence_CompFuns =
+struct
+
+fun mk_pos_random_dseqT T =
+ @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+
+fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+ Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
+ Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
+ | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let
+ val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
+
+fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
+ HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) =
+ list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto},
+ [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
+ ---> mk_pos_random_dseqT T),
+ [f, from, to])
+
+fun mk_not t =
+ let
+ val pT = mk_pos_random_dseqT HOLogic.unitT
+ val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
+ [Type (@{type_name Option.option}, [@{typ unit}])])
+
+ in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
+ (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
+end;
+
+structure New_Neg_Random_Sequence_CompFuns =
+struct
+
+fun mk_neg_random_dseqT T =
+ @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} -->
+ Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
+
+fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+ Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
+ Type (@{type_name Lazy_Sequence.lazy_sequence},
+ [Type (@{type_name Option.option}, [T])])])])])])) = T
+ | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let
+ val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
+
+fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
+ HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) =
+ list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto},
+ [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}]
+ ---> mk_neg_random_dseqT T),
+ [f, from, to])
+
+fun mk_not t =
+ let
+ val nT = mk_neg_random_dseqT HOLogic.unitT
+ val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
+ in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
+ (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
+end;
+
+structure Random_Sequence_CompFuns =
+struct
+
+fun mk_random_dseqT T =
+ @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
+
+fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
+ Type ("fun", [@{typ Random.seed},
+ Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
+ | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+
+fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
+
+fun mk_single t =
+ let
+ val T = fastype_of t
+ in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
+
+fun mk_bind (x, f) =
+ let
+ val T as Type ("fun", [_, U]) = fastype_of f
+ in
+ Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
+ end;
+
+val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
+
+fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
+ HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
+
+fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+
+fun mk_not t =
+ let
+ val T = mk_random_dseqT HOLogic.unitT
+ in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
+
+fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
+ (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
+
+val compfuns = Predicate_Compile_Aux.CompilationFuns
+ {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
+ mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
+end;
+
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Apr 01 10:27:06 2010 +0200
@@ -6,60 +6,59 @@
signature PREDICATE_COMPILE_CORE =
sig
+ type mode = Predicate_Compile_Aux.mode
+ type options = Predicate_Compile_Aux.options
+ type compilation = Predicate_Compile_Aux.compilation
+ type compilation_funs = Predicate_Compile_Aux.compilation_funs
+
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.mode option list option
- -> (string option * (Predicate_Compile_Aux.compilation * int list))
- -> int -> string -> Toplevel.state -> unit
+ val code_pred : options -> string -> Proof.context -> Proof.state
+ val code_pred_cmd : options -> string -> Proof.context -> Proof.state
+ val values_cmd : string list -> mode option list option
+ -> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
val register_predicate : (string * thm list * thm) -> theory -> theory
val register_intros : string * thm list -> theory -> theory
val is_registered : theory -> string -> bool
- val function_name_of : Predicate_Compile_Aux.compilation -> theory
- -> string -> bool * Predicate_Compile_Aux.mode -> string
- val predfun_intro_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
- val predfun_elim_of: Proof.context -> string -> Predicate_Compile_Aux.mode -> thm
+ val function_name_of : compilation -> theory -> string -> mode -> string
+ val predfun_intro_of: Proof.context -> string -> mode -> thm
+ val predfun_elim_of: Proof.context -> string -> mode -> thm
val all_preds_of : theory -> string list
- val modes_of: Predicate_Compile_Aux.compilation
- -> theory -> string -> Predicate_Compile_Aux.mode list
- val all_modes_of : Predicate_Compile_Aux.compilation
- -> theory -> (string * Predicate_Compile_Aux.mode list) list
- val all_random_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
+ val modes_of: compilation -> theory -> string -> mode list
+ val all_modes_of : compilation -> theory -> (string * mode list) list
+ val all_random_modes_of : theory -> (string * mode list) list
val intros_of : theory -> string -> thm list
val add_intro : thm -> theory -> theory
val set_elim : thm -> theory -> theory
+ val register_alternative_function : string -> mode -> string -> theory -> theory
+ val alternative_compilation_of : theory -> string -> mode ->
+ (compilation_funs -> typ -> term) option
+ val functional_compilation : string -> mode -> compilation_funs -> typ -> term
+ val force_modes_and_functions : string -> (mode * (string * bool)) list -> theory -> theory
+ val force_modes_and_compilations : string ->
+ (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
val preprocess_intro : theory -> thm -> thm
val print_stored_rules : theory -> unit
- val print_all_modes : Predicate_Compile_Aux.compilation -> theory -> unit
+ val print_all_modes : compilation -> theory -> unit
val mk_casesrule : Proof.context -> term -> thm list -> term
-
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 dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
option Unsynchronized.ref
+ val new_random_dseq_eval_ref :
+ (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
+ option Unsynchronized.ref
+ val new_random_dseq_stats_eval_ref :
+ (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
+ option Unsynchronized.ref
val code_pred_intro_attrib : attribute
-
(* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
-
- datatype compilation_funs = CompilationFuns of {
- mk_predT : typ -> typ,
- dest_predT : typ -> typ,
- mk_bot : typ -> term,
- mk_single : term -> term,
- mk_bind : term * term -> term,
- mk_sup : term * term -> term,
- mk_if : term -> term,
- mk_not : term -> term,
- mk_map : typ -> typ -> term -> term -> term
- };
-
- val pred_compfuns : compilation_funs
- val randompred_compfuns : compilation_funs
- val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
- val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
+ val add_equations : options -> string list -> theory -> theory
+ val add_depth_limited_random_equations : options -> string list -> theory -> theory
+ val add_random_dseq_equations : options -> string list -> theory -> theory
+ val add_new_random_dseq_equations : options -> string list -> theory -> theory
val mk_tracing : string -> term -> term
end;
@@ -254,11 +253,11 @@
^ "functions defined for predicate " ^ quote name)
| SOME fun_names => fun_names
-fun function_name_of compilation thy name (pol, mode) =
+fun function_name_of compilation thy name mode =
case AList.lookup eq_mode
- (function_names_of (compilation_for_polarity pol compilation) thy name) mode of
+ (function_names_of compilation thy name) mode of
NONE => error ("No " ^ string_of_compilation compilation
- ^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
+ ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
| SOME function_name => function_name
fun modes_of compilation thy name = map fst (function_names_of compilation thy name)
@@ -711,226 +710,315 @@
PredData.map (Graph.map_node name (map_pred_data set))
end
-(* datastructures and setup for generic compilation *)
+(* registration of alternative function names *)
+
+structure Alt_Compilations_Data = Theory_Data
+(
+ type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ val merge = Symtab.merge ((K true)
+ : ((mode * (compilation_funs -> typ -> term)) list *
+ (mode * (compilation_funs -> typ -> term)) list -> bool));
+);
+
+fun alternative_compilation_of thy pred_name mode =
+ AList.lookup eq_mode (Symtab.lookup_list (Alt_Compilations_Data.get thy) pred_name) mode
-datatype compilation_funs = CompilationFuns of {
- mk_predT : typ -> typ,
- dest_predT : typ -> typ,
- mk_bot : typ -> term,
- mk_single : term -> term,
- mk_bind : term * term -> term,
- mk_sup : term * term -> term,
- mk_if : term -> term,
- mk_not : term -> term,
- mk_map : typ -> typ -> term -> term -> term
-};
+fun force_modes_and_compilations pred_name compilations =
+ let
+ (* thm refl is a dummy thm *)
+ val modes = map fst compilations
+ val (needs_random, non_random_modes) = pairself (map fst)
+ (List.partition (fn (m, (fun_name, random)) => random) compilations)
+ val non_random_dummys = map (rpair "dummy") non_random_modes
+ val all_dummys = map (rpair "dummy") modes
+ val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
+ @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
+ val alt_compilations = map (apsnd fst) compilations
+ in
+ PredData.map (Graph.new_node
+ (pred_name, mk_pred_data (([], SOME @{thm refl}), (dummy_function_names, ([], needs_random)))))
+ #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
+ end
-fun mk_predT (CompilationFuns funs) = #mk_predT funs
-fun dest_predT (CompilationFuns funs) = #dest_predT funs
-fun mk_bot (CompilationFuns funs) = #mk_bot funs
-fun mk_single (CompilationFuns funs) = #mk_single funs
-fun mk_bind (CompilationFuns funs) = #mk_bind funs
-fun mk_sup (CompilationFuns funs) = #mk_sup funs
-fun mk_if (CompilationFuns funs) = #mk_if funs
-fun mk_not (CompilationFuns funs) = #mk_not funs
-fun mk_map (CompilationFuns funs) = #mk_map funs
+fun functional_compilation fun_name mode compfuns T =
+ let
+ val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
+ mode (binder_types T)
+ val bs = map (pair "x") inpTs
+ val bounds = map Bound (rev (0 upto (length bs) - 1))
+ val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
+ in list_abs (bs, mk_single compfuns (list_comb (f, bounds))) end
-structure PredicateCompFuns =
+fun register_alternative_function pred_name mode fun_name =
+ Alt_Compilations_Data.map (Symtab.insert_list (eq_pair eq_mode (K false))
+ (pred_name, (mode, functional_compilation fun_name mode)))
+
+fun force_modes_and_functions pred_name fun_names =
+ force_modes_and_compilations pred_name
+ (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
+ fun_names)
+
+(* compilation modifiers *)
+
+structure Comp_Mod =
struct
-fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
-
-fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
- | dest_predT T = raise TYPE ("dest_predT", [T], []);
-
-fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
-
-fun mk_single t =
- let val T = fastype_of t
- in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
-
-fun mk_bind (x, f) =
- let val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name sup};
-
-fun mk_if cond = Const (@{const_name Predicate.if_pred},
- HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
+datatype comp_modifiers = Comp_Modifiers of
+{
+ compilation : compilation,
+ function_name_prefix : string,
+ compfuns : compilation_funs,
+ mk_random : typ -> term list -> term,
+ modify_funT : typ -> typ,
+ additional_arguments : string list -> term list,
+ wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
+ transform_additional_arguments : indprem -> term list -> term list
+}
-fun mk_not t =
- let
- val T = mk_predT HOLogic.unitT
- in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
+fun dest_comp_modifiers (Comp_Modifiers c) = c
-fun mk_Enum f =
- let val T as Type ("fun", [T', _]) = fastype_of f
- in
- Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f
- end;
+val compilation = #compilation o dest_comp_modifiers
+val function_name_prefix = #function_name_prefix o dest_comp_modifiers
+val compfuns = #compfuns o dest_comp_modifiers
-fun mk_Eval (f, x) =
- let
- val T = fastype_of x
- in
- Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
- end;
+val mk_random = #mk_random o dest_comp_modifiers
+val funT_of' = funT_of o compfuns
+val modify_funT = #modify_funT o dest_comp_modifiers
+fun funT_of comp mode = modify_funT comp o funT_of' comp mode
-fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
-
-fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
- (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
-
-val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
- mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
- mk_map = mk_map};
+val additional_arguments = #additional_arguments o dest_comp_modifiers
+val wrap_compilation = #wrap_compilation o dest_comp_modifiers
+val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
end;
-structure RandomPredCompFuns =
-struct
-
-fun mk_randompredT T =
- @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
-
-fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
- [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
- | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
-
-fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
-
-fun mk_single t =
- let
- val T = fastype_of t
- in
- Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
- end;
-
-fun mk_bind (x, f) =
- let
- val T as (Type ("fun", [_, U])) = fastype_of f
- in
- Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
- end
-
-val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
-
-fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
- HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
+val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Depth_Limited,
+ function_name_prefix = "depth_limited_",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ additional_arguments = fn names =>
+ let
+ val depth_name = Name.variant names "depth"
+ in [Free (depth_name, @{typ code_numeral})] end,
+ modify_funT = (fn T => let val (Ts, U) = strip_type T
+ val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
+ wrap_compilation =
+ fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+ let
+ val [depth] = additional_arguments
+ val (_, Ts) = split_modeT' mode (binder_types T)
+ val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+ val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+ in
+ if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+ $ mk_bot compfuns (dest_predT compfuns T')
+ $ compilation
+ end,
+ transform_additional_arguments =
+ fn prem => fn additional_arguments =>
+ let
+ val [depth] = additional_arguments
+ val depth' =
+ Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+ $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
+ in [depth'] end
+ }
-fun mk_not t =
- let
- val T = mk_randompredT HOLogic.unitT
- in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
- (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map};
-
-end;
-
-structure DSequence_CompFuns =
-struct
+val random_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Random,
+ function_name_prefix = "random_",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
+ list_comb (Const(@{const_name Quickcheck.iter},
+ [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] --->
+ PredicateCompFuns.mk_predT T), additional_arguments)),
+ modify_funT = (fn T =>
+ let
+ val (Ts, U) = strip_type T
+ val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
+ in (Ts @ Ts') ---> U end),
+ additional_arguments = (fn names =>
+ let
+ val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
+ in
+ [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
+ Free (seed, @{typ "code_numeral * code_numeral"})]
+ end),
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
-
-fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
- Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
- | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
-
-fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
-
-fun mk_single t =
- let val T = fastype_of t
- in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
- let val T as Type ("fun", [_, U]) = fastype_of f
- in
- Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
+val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Depth_Limited_Random,
+ function_name_prefix = "depth_limited_random_",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
+ list_comb (Const(@{const_name Quickcheck.iter},
+ [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] --->
+ PredicateCompFuns.mk_predT T), tl additional_arguments)),
+ modify_funT = (fn T =>
+ let
+ val (Ts, U) = strip_type T
+ val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+ @{typ "code_numeral * code_numeral"}]
+ in (Ts @ Ts') ---> U end),
+ additional_arguments = (fn names =>
+ let
+ val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
+ in
+ [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
+ Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
+ end),
+ wrap_compilation =
+ fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+ let
+ val depth = hd (additional_arguments)
+ val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
+ mode (binder_types T)
+ val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
+ val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
+ in
+ if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
+ $ mk_bot compfuns (dest_predT compfuns T')
+ $ compilation
+ end,
+ transform_additional_arguments =
+ fn prem => fn additional_arguments =>
+ let
+ val [depth, nrandom, size, seed] = additional_arguments
+ val depth' =
+ Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
+ $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
+ in [depth', nrandom, size, seed] end
+}
-fun mk_if cond = Const (@{const_name DSequence.if_seq},
- HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
-
-fun mk_not t = let val T = mk_dseqT HOLogic.unitT
- in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
-
-fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
- (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
-
-val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map}
-
-end;
-
-structure Random_Sequence_CompFuns =
-struct
+val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Pred,
+ function_name_prefix = "",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun mk_random_dseqT T =
- @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
- HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
-
-fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
- Type ("fun", [@{typ Random.seed},
- Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
- | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Annotated,
+ function_name_prefix = "annotated_",
+ compfuns = PredicateCompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
+ 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,
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
+val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = DSeq,
+ function_name_prefix = "dseq_",
+ compfuns = DSequence_CompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun mk_single t =
- let
- val T = fastype_of t
- in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
-
-fun mk_bind (x, f) =
+val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Pos_Random_DSeq,
+ function_name_prefix = "random_dseq_",
+ compfuns = Random_Sequence_CompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
let
- val T as Type ("fun", [_, U]) = fastype_of f
+ val random = Const ("Quickcheck.random_class.random",
+ @{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
in
- Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
- end;
-
-val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
+ Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+ Random_Sequence_CompFuns.mk_random_dseqT T) $ random
+ end),
-fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
- HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
+ modify_funT = I,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun mk_not t =
- let
- val T = mk_random_dseqT HOLogic.unitT
- in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
+val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = Neg_Random_DSeq,
+ function_name_prefix = "random_dseq_neg_",
+ compfuns = Random_Sequence_CompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
- (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
-val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
- mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
- mk_not = mk_not, mk_map = mk_map}
-
-end;
-
-(* for external use with interactive mode *)
-val pred_compfuns = PredicateCompFuns.compfuns
-val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
+val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = New_Pos_Random_DSeq,
+ function_name_prefix = "new_random_dseq_",
+ compfuns = New_Pos_Random_Sequence_CompFuns.compfuns,
+ mk_random = (fn T => fn additional_arguments =>
+ let
+ val random = Const ("Quickcheck.random_class.random",
+ @{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
+ in
+ Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
+ HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
+ New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
+ end),
+ modify_funT = I,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-(* function types and names of different compilations *)
+val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
+ {
+ compilation = New_Neg_Random_DSeq,
+ function_name_prefix = "new_random_dseq_neg_",
+ compfuns = New_Neg_Random_Sequence_CompFuns.compfuns,
+ mk_random = (fn _ => error "no random generation"),
+ modify_funT = I,
+ additional_arguments = K [],
+ wrap_compilation = K (K (K (K (K I))))
+ : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
+ transform_additional_arguments = K I : (indprem -> term list -> term list)
+ }
-fun funT_of compfuns mode T =
- let
- val Ts = binder_types T
- val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
- in
- inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
- end;
+fun negative_comp_modifiers_of comp_modifiers =
+ (case Comp_Mod.compilation comp_modifiers of
+ Pos_Random_DSeq => neg_random_dseq_comp_modifiers
+ | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
+ | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
+ | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
+ | c => comp_modifiers)
(** mode analysis **)
@@ -1194,50 +1282,60 @@
EQUAL => ord2 (x, x')
| ord => ord
-fun deriv_ord2' thy modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun deriv_ord2' thy pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
let
+ (* prefer modes without requirement for generating random values *)
fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (length mvars1, length mvars2)
+ (* prefer non-random modes *)
fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
if random_mode_in_deriv modes t1 deriv1 then 1 else 0)
+ (* prefer modes with more input and less output *)
fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
int_ord (number_of_output_positions (head_mode_of deriv1),
number_of_output_positions (head_mode_of deriv2))
+ (* prefer recursive calls *)
+ fun is_rec_premise t =
+ case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
+ fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ int_ord (if is_rec_premise t1 then 0 else 1,
+ if is_rec_premise t2 then 0 else 1)
+ val ord = lex_ord mvars_ord (lex_ord random_mode_ord (lex_ord output_mode_ord recursive_ord))
in
- lex_ord mvars_ord (lex_ord random_mode_ord output_mode_ord)
- ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
+ ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2))
end
-fun deriv_ord2 thy modes t = deriv_ord2' thy modes t t
+fun deriv_ord2 thy pred modes t = deriv_ord2' thy pred modes t t
fun deriv_ord ((deriv1, mvars1), (deriv2, mvars2)) =
int_ord (length mvars1, length mvars2)
-fun premise_ord thy modes ((prem1, a1), (prem2, a2)) =
- rev_option_ord (deriv_ord2' thy modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2)
+fun premise_ord thy pred modes ((prem1, a1), (prem2, a2)) =
+ rev_option_ord (deriv_ord2' thy pred modes (term_of_prem prem1) (term_of_prem prem2)) (a1, a2)
fun print_mode_list modes =
tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
-fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pol (modes, (pos_modes, neg_modes)) vs ps =
+fun select_mode_prem (mode_analysis_options : mode_analysis_options) (thy : theory) pred
+ pol (modes, (pos_modes, neg_modes)) vs ps =
let
fun choose_mode_of_prem (Prem t) = partial_hd
- (sort (deriv_ord2 thy modes t) (all_derivations_of thy pos_modes vs t))
+ (sort (deriv_ord2 thy pred modes t) (all_derivations_of thy pos_modes vs t))
| choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
| choose_mode_of_prem (Negprem t) = partial_hd
- (sort (deriv_ord2 thy modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
+ (sort (deriv_ord2 thy pred modes t) (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
(all_derivations_of thy neg_modes vs t)))
| choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem thy p)
in
if #reorder_premises mode_analysis_options then
- partial_hd (sort (premise_ord thy modes) (ps ~~ map choose_mode_of_prem ps))
+ partial_hd (sort (premise_ord thy pred modes) (ps ~~ map choose_mode_of_prem ps))
else
SOME (hd ps, choose_mode_of_prem (hd ps))
end
-fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy param_vs (modes :
+fun check_mode_clause' (mode_analysis_options : mode_analysis_options) thy pred param_vs (modes :
(string * ((bool * mode) * bool) list) list) ((pol, mode) : bool * mode) (ts, ps) =
let
val vTs = distinct (op =) (fold Term.add_frees (map term_of_prem ps) (fold Term.add_frees ts []))
@@ -1262,7 +1360,7 @@
fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
| check_mode_prems acc_ps rnd vs ps =
(case
- (select_mode_prem mode_analysis_options thy pol (modes', (pos_modes', neg_modes')) vs ps) of
+ (select_mode_prem mode_analysis_options thy pred pol (modes', (pos_modes', neg_modes')) vs ps) of
SOME (p, SOME (deriv, [])) => check_mode_prems ((p, deriv) :: acc_ps) rnd
(known_vs_after p vs) (filter_out (equal p) ps)
| SOME (p, SOME (deriv, missing_vars)) =>
@@ -1309,7 +1407,7 @@
fun check_mode m =
let
val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ =>
- map (check_mode_clause' mode_analysis_options thy param_vs modes m) rs)
+ map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
in
Output.cond_timeit false "aux part of check_mode for one mode" (fn _ =>
case find_indices is_none res of
@@ -1332,7 +1430,7 @@
(p, map (fn (m, rnd) =>
(m, map
((fn (ts, ps, rnd) => (ts, ps)) o the o
- check_mode_clause' mode_analysis_options thy param_vs modes m) rs)) ms)
+ check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
end;
fun fixp f (x : (string * ((bool * mode) * bool) list) list) =
@@ -1390,8 +1488,8 @@
else
map (fn (s, ms) => (s, map (fn m => ((true, m), false)) ms)) all_modes
fun iteration modes = map
- (check_modes_pred' mode_analysis_options options thy param_vs clauses (modes @ extra_modes))
- modes
+ (check_modes_pred' mode_analysis_options options thy param_vs clauses
+ (modes @ extra_modes)) modes
val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
if collect_errors then
@@ -1482,40 +1580,8 @@
(t, names)
end;
-structure Comp_Mod =
-struct
-
-datatype comp_modifiers = Comp_Modifiers of
-{
- compilation : compilation,
- function_name_prefix : string,
- compfuns : compilation_funs,
- mk_random : typ -> term list -> term,
- modify_funT : typ -> typ,
- additional_arguments : string list -> term list,
- wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
- transform_additional_arguments : indprem -> term list -> term list
-}
-
-fun dest_comp_modifiers (Comp_Modifiers c) = c
-
-val compilation = #compilation o dest_comp_modifiers
-val function_name_prefix = #function_name_prefix o dest_comp_modifiers
-val compfuns = #compfuns o dest_comp_modifiers
-
-val mk_random = #mk_random o dest_comp_modifiers
-val funT_of' = funT_of o compfuns
-val modify_funT = #modify_funT o dest_comp_modifiers
-fun funT_of comp mode = modify_funT comp o funT_of' comp mode
-
-val additional_arguments = #additional_arguments o dest_comp_modifiers
-val wrap_compilation = #wrap_compilation o dest_comp_modifiers
-val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
-
-end;
-
(* TODO: uses param_vs -- change necessary for compilation with new modes *)
-fun compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss arg =
+fun compile_arg compilation_modifiers additional_arguments ctxt param_vs iss arg =
let
fun map_params (t as Free (f, T)) =
if member (op =) param_vs f then
@@ -1530,18 +1596,19 @@
| map_params t = t
in map_aterms map_params arg end
-fun compile_match compilation_modifiers compfuns additional_arguments
+fun compile_match compilation_modifiers additional_arguments
param_vs iss ctxt eqs eqs' out_ts success_t =
let
+ val compfuns = Comp_Mod.compfuns compilation_modifiers
val eqs'' = maps mk_eq eqs @ eqs'
val eqs'' =
- map (compile_arg compilation_modifiers compfuns additional_arguments ctxt param_vs iss) eqs''
+ map (compile_arg compilation_modifiers additional_arguments ctxt param_vs iss) eqs''
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
val name = Name.variant names "x";
val name' = Name.variant (name :: names) "y";
val T = HOLogic.mk_tupleT (map fastype_of out_ts);
val U = fastype_of success_t;
- val U' = dest_predT compfuns U;
+ val U' = dest_predT compfuns U;
val v = Free (name, T);
val v' = Free (name', T);
in
@@ -1564,16 +1631,20 @@
| (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
| (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
-fun compile_expr compilation_modifiers compfuns ctxt pol (t, deriv) additional_arguments =
+fun compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments =
let
+ val compfuns = Comp_Mod.compfuns compilation_modifiers
fun expr_of (t, deriv) =
(case (t, deriv) of
(t, Term Input) => SOME t
| (t, Term Output) => NONE
| (Const (name, T), Context mode) =>
- SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
- (ProofContext.theory_of ctxt) name (pol, mode),
- Comp_Mod.funT_of compilation_modifiers mode T))
+ (case alternative_compilation_of (ProofContext.theory_of ctxt) name mode of
+ SOME alt_comp => SOME (alt_comp compfuns T)
+ | NONE =>
+ SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+ (ProofContext.theory_of ctxt) name mode,
+ Comp_Mod.funT_of compilation_modifiers mode T)))
| (Free (s, T), Context m) =>
SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
| (t, Context m) =>
@@ -1596,11 +1667,12 @@
list_comb (the (expr_of (t, deriv)), additional_arguments)
end
-fun compile_clause compilation_modifiers compfuns ctxt all_vs param_vs additional_arguments
- (pol, mode) inp (ts, moded_ps) =
+fun compile_clause compilation_modifiers ctxt all_vs param_vs additional_arguments
+ mode inp (ts, moded_ps) =
let
+ val compfuns = Comp_Mod.compfuns compilation_modifiers
val iss = ho_arg_modes_of mode
- val compile_match = compile_match compilation_modifiers compfuns
+ val compile_match = compile_match compilation_modifiers
additional_arguments param_vs iss ctxt
val (in_ts, out_ts) = split_mode mode ts;
val (in_ts', (all_vs', eqs)) =
@@ -1629,8 +1701,7 @@
Prem t =>
let
val u =
- compile_expr compilation_modifiers compfuns ctxt
- pol (t, deriv) additional_arguments'
+ compile_expr compilation_modifiers ctxt (t, deriv) additional_arguments'
val (_, out_ts''') = split_mode mode (snd (strip_comb t))
val rest = compile_prems out_ts''' vs' names'' ps
in
@@ -1638,9 +1709,10 @@
end
| Negprem t =>
let
+ val neg_compilation_modifiers =
+ negative_comp_modifiers_of compilation_modifiers
val u = mk_not compfuns
- (compile_expr compilation_modifiers compfuns ctxt
- (not pol) (t, deriv) additional_arguments')
+ (compile_expr neg_compilation_modifiers ctxt (t, deriv) additional_arguments')
val (_, out_ts''') = split_mode mode (snd (strip_comb t))
val rest = compile_prems out_ts''' vs' names'' ps
in
@@ -1648,7 +1720,7 @@
end
| Sidecond t =>
let
- val t = compile_arg compilation_modifiers compfuns additional_arguments
+ val t = compile_arg compilation_modifiers additional_arguments
ctxt param_vs iss t
val rest = compile_prems [] vs' names'' ps;
in
@@ -1673,6 +1745,8 @@
fun compile_pred compilation_modifiers thy all_vs param_vs s T (pol, mode) moded_cls =
let
val ctxt = ProofContext.init thy
+ val compilation_modifiers = if pol then compilation_modifiers else
+ negative_comp_modifiers_of compilation_modifiers
val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
(all_vs @ param_vs)
val compfuns = Comp_Mod.compfuns compilation_modifiers
@@ -1686,7 +1760,7 @@
val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
(fn T => fn (param_vs, names) =>
- if is_param_type T then
+ if is_param_type T then
(Free (hd param_vs, T), (tl param_vs, names))
else
let
@@ -1696,8 +1770,8 @@
val in_ts' = map_filter (map_filter_prod
(fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
val cl_ts =
- map (compile_clause compilation_modifiers compfuns
- ctxt all_vs param_vs additional_arguments (pol, mode) (HOLogic.mk_tuple in_ts')) moded_cls;
+ map (compile_clause compilation_modifiers
+ ctxt all_vs param_vs additional_arguments mode (HOLogic.mk_tuple in_ts')) moded_cls;
val compilation = Comp_Mod.wrap_compilation compilation_modifiers compfuns
s T mode additional_arguments
(if null cl_ts then
@@ -1705,7 +1779,7 @@
else foldr1 (mk_sup compfuns) cl_ts)
val fun_const =
Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
- (ProofContext.theory_of ctxt) s (pol, mode), funT)
+ (ProofContext.theory_of ctxt) s mode, funT)
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
@@ -2491,7 +2565,7 @@
val arg_names = Name.variant_list []
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val args = map2 (curry Free) arg_names Ts
- val predfun = Const (function_name_of Pred thy predname (true, full_mode),
+ val predfun = Const (function_name_of Pred thy predname full_mode,
Ts ---> PredicateCompFuns.mk_predT @{typ unit})
val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
val eq_term = HOLogic.mk_Trueprop
@@ -2614,125 +2688,6 @@
scc thy' |> Theory.checkpoint
in thy'' end
-val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Depth_Limited,
- function_name_prefix = "depth_limited_",
- compfuns = PredicateCompFuns.compfuns,
- mk_random = (fn _ => error "no random generation"),
- additional_arguments = fn names =>
- let
- val depth_name = Name.variant names "depth"
- in [Free (depth_name, @{typ code_numeral})] end,
- modify_funT = (fn T => let val (Ts, U) = strip_type T
- val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
- wrap_compilation =
- fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
- let
- val [depth] = additional_arguments
- val (_, Ts) = split_modeT' mode (binder_types T)
- val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
- val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
- in
- if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
- $ mk_bot compfuns (dest_predT compfuns T')
- $ compilation
- end,
- transform_additional_arguments =
- fn prem => fn additional_arguments =>
- let
- val [depth] = additional_arguments
- val depth' =
- Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
- $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
- in [depth'] end
- }
-
-val random_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Random,
- function_name_prefix = "random_",
- compfuns = PredicateCompFuns.compfuns,
- mk_random = (fn T => fn additional_arguments =>
- list_comb (Const(@{const_name Quickcheck.iter},
- [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] --->
- PredicateCompFuns.mk_predT T), additional_arguments)),
- modify_funT = (fn T =>
- let
- val (Ts, U) = strip_type T
- val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
- in (Ts @ Ts') ---> U end),
- additional_arguments = (fn names =>
- let
- val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
- in
- [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
- Free (seed, @{typ "code_numeral * code_numeral"})]
- end),
- wrap_compilation = K (K (K (K (K I))))
- : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
-val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Depth_Limited_Random,
- function_name_prefix = "depth_limited_random_",
- compfuns = PredicateCompFuns.compfuns,
- mk_random = (fn T => fn additional_arguments =>
- list_comb (Const(@{const_name Quickcheck.iter},
- [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] --->
- PredicateCompFuns.mk_predT T), tl additional_arguments)),
- modify_funT = (fn T =>
- let
- val (Ts, U) = strip_type T
- val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
- @{typ "code_numeral * code_numeral"}]
- in (Ts @ Ts') ---> U end),
- additional_arguments = (fn names =>
- let
- val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
- in
- [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
- Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
- end),
- wrap_compilation =
- fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
- let
- val depth = hd (additional_arguments)
- val (_, Ts) = split_modeT' mode (binder_types T)
- val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
- val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
- in
- if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
- $ mk_bot compfuns (dest_predT compfuns T')
- $ compilation
- end,
- transform_additional_arguments =
- fn prem => fn additional_arguments =>
- let
- val [depth, nrandom, size, seed] = additional_arguments
- val depth' =
- Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
- $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
- in [depth', nrandom, size, seed] end
-}
-
-(* different instantiantions of the predicate compiler *)
-
-val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Pred,
- function_name_prefix = "",
- compfuns = PredicateCompFuns.compfuns,
- mk_random = (fn _ => error "no random generation"),
- modify_funT = I,
- additional_arguments = K [],
- wrap_compilation = K (K (K (K (K I))))
- : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
val add_equations = gen_add_equations
(Steps {
define_functions =
@@ -2745,70 +2700,6 @@
use_random = false,
qname = "equation"})
-val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Annotated,
- function_name_prefix = "annotated_",
- compfuns = PredicateCompFuns.compfuns,
- mk_random = (fn _ => error "no random generation"),
- modify_funT = I,
- 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,
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
-val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = DSeq,
- function_name_prefix = "dseq_",
- compfuns = DSequence_CompFuns.compfuns,
- mk_random = (fn _ => error "no random generation"),
- modify_funT = I,
- additional_arguments = K [],
- wrap_compilation = K (K (K (K (K I))))
- : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
-val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Pos_Random_DSeq,
- function_name_prefix = "random_dseq_",
- compfuns = Random_Sequence_CompFuns.compfuns,
- mk_random = (fn T => fn additional_arguments =>
- let
- val random = Const ("Quickcheck.random_class.random",
- @{typ code_numeral} --> @{typ Random.seed} -->
- HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
- in
- Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
- HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
- Random_Sequence_CompFuns.mk_random_dseqT T) $ random
- end),
-
- modify_funT = I,
- additional_arguments = K [],
- wrap_compilation = K (K (K (K (K I))))
- : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
-val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Neg_Random_DSeq,
- function_name_prefix = "random_dseq_neg_",
- compfuns = Random_Sequence_CompFuns.compfuns,
- mk_random = (fn _ => error "no random generation"),
- modify_funT = I,
- additional_arguments = K [],
- wrap_compilation = K (K (K (K (K I))))
- : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
val add_depth_limited_equations = gen_add_equations
(Steps {
define_functions =
@@ -2887,6 +2778,23 @@
use_random = true,
qname = "random_dseq_equation"})
+val add_new_random_dseq_equations = gen_add_equations
+ (Steps {
+ define_functions =
+ fn options => fn preds => fn (s, modes) =>
+ let
+ val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+ val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+ in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.compfuns
+ options preds (s, pos_modes)
+ #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.compfuns
+ options preds (s, neg_modes)
+ end,
+ prove = prove_by_skip,
+ add_code_equations = K (K I),
+ comp_modifiers = new_pos_random_dseq_comp_modifiers,
+ use_random = true,
+ qname = "new_random_dseq_equation"})
(** user interface **)
@@ -2912,7 +2820,6 @@
val const = prep_const thy raw_const
val lthy' = Local_Theory.theory (PredData.map
(extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
- |> Local_Theory.checkpoint
val thy' = ProofContext.theory_of lthy'
val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
fun mk_cases const =
@@ -2943,6 +2850,7 @@
| Depth_Limited => add_depth_limited_equations
| Random => add_random_equations
| Depth_Limited_Random => add_depth_limited_random_equations
+ | New_Pos_Random_DSeq => add_new_random_dseq_equations
| compilation => error ("Compilation not supported")
) options [const]))
end
@@ -2961,6 +2869,11 @@
val dseq_eval_ref = Unsynchronized.ref (NONE : (unit -> term DSequence.dseq) option);
val random_dseq_eval_ref =
Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
+val new_random_dseq_eval_ref =
+ Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
+val new_random_dseq_stats_eval_ref =
+ Unsynchronized.ref (NONE :
+ (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
@@ -2975,7 +2888,10 @@
val body = subst_bounds (output_frees, body)
val T_compr = HOLogic.mk_ptupleT fp Ts
val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
- val (pred as Const (name, T), all_args) = strip_comb body
+ val (pred as Const (name, T), all_args) =
+ case strip_comb body of
+ (Const (name, T), all_args) => (Const (name, T), all_args)
+ | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term_global thy head)
in
if defined_functions compilation thy name then
let
@@ -3030,6 +2946,7 @@
[@{term "(1, 1) :: code_numeral * code_numeral"}]
| DSeq => []
| Pos_Random_DSeq => []
+ | New_Pos_Random_DSeq => []
val comp_modifiers =
case compilation of
Pred => predicate_comp_modifiers
@@ -3039,8 +2956,9 @@
(*| Annotated => annotated_comp_modifiers*)
| DSeq => dseq_comp_modifiers
| Pos_Random_DSeq => pos_random_dseq_comp_modifiers
- val t_pred = compile_expr comp_modifiers compfuns (ProofContext.init thy)
- true (body, deriv) additional_arguments;
+ | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
+ val t_pred = compile_expr comp_modifiers (ProofContext.init thy)
+ (body, deriv) additional_arguments;
val T_pred = dest_predT compfuns (fastype_of t_pred)
val arrange = split_lambda (HOLogic.mk_tuple outargs) output_tuple
in
@@ -3050,18 +2968,31 @@
error "Evaluation with values is not possible because compilation with code_pred was not invoked"
end
-fun eval thy param_user_modes (options as (compilation, arguments)) k t_compr =
+fun eval thy stats param_user_modes (options as (compilation, arguments)) k t_compr =
let
+ fun count xs x =
+ let
+ fun count' i [] = i
+ | count' i (x' :: xs) = if x = x' then count' (i + 1) xs else count' i xs
+ in count' 0 xs end
+ fun accumulate xs = map (fn x => (x, count xs x)) (sort int_ord (distinct (op =) xs))
val compfuns =
case compilation of
Random => PredicateCompFuns.compfuns
| DSeq => DSequence_CompFuns.compfuns
| Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
+ | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
| _ => PredicateCompFuns.compfuns
val t = analyze_compr thy compfuns param_user_modes options t_compr;
val T = dest_predT compfuns (fastype_of t);
- val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
- val ts =
+ val t' =
+ if stats andalso compilation = New_Pos_Random_DSeq then
+ mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
+ (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
+ @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
+ else
+ mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
+ val (ts, statistics) =
case compilation of
(* Random =>
fst (Predicate.yieldn k
@@ -3072,27 +3003,48 @@
let
val [nrandom, size, depth] = arguments
in
- fst (DSequence.yieldn k
+ rpair NONE (fst (DSequence.yieldn k
(Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
(fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
thy t' [] nrandom size
|> Random_Engine.run)
- depth true)
+ depth true))
end
| DSeq =>
- fst (DSequence.yieldn k
+ rpair NONE (fst (DSequence.yieldn k
(Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
- DSequence.map thy t' []) (the_single arguments) true)
+ DSequence.map thy t' []) (the_single arguments) true))
+ | New_Pos_Random_DSeq =>
+ let
+ val [nrandom, size, depth] = arguments
+ val seed = Random_Engine.next_seed ()
+ in
+ if stats then
+ apsnd (SOME o accumulate) (split_list
+ (fst (Lazy_Sequence.yieldn k
+ (Code_Eval.eval NONE
+ ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
+ (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
+ |> Lazy_Sequence.map (apfst proc))
+ thy t' [] nrandom size seed depth))))
+ else rpair NONE
+ (fst (Lazy_Sequence.yieldn k
+ (Code_Eval.eval NONE
+ ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
+ (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
+ |> Lazy_Sequence.map proc)
+ thy t' [] nrandom size seed depth)))
+ end
| _ =>
- fst (Predicate.yieldn k
+ rpair NONE (fst (Predicate.yieldn k
(Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
- Predicate.map thy t' []))
- in (T, ts) end;
+ Predicate.map thy t' [])))
+ in ((T, ts), statistics) end;
-fun values ctxt param_user_modes (raw_expected, comp_options) k t_compr =
+fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
let
val thy = ProofContext.theory_of ctxt
- val (T, ts) = eval thy param_user_modes comp_options k t_compr
+ val ((T, ts), statistics) = eval thy stats param_user_modes comp_options k t_compr
val setT = HOLogic.mk_setT T
val elems = HOLogic.mk_set T ts
val cont = Free ("...", setT)
@@ -3107,20 +3059,36 @@
"expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
"computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
in
- if k = ~1 orelse length ts < k then elems
- else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont
+ (if k = ~1 orelse length ts < k then elems
+ else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont, statistics)
end;
fun values_cmd print_modes param_user_modes options k raw_t state =
let
val ctxt = Toplevel.context_of state
val t = Syntax.read_term ctxt raw_t
- val t' = values ctxt param_user_modes options k t
+ val (t', stats) = values ctxt param_user_modes options k t
val ty' = Term.type_of t'
val ctxt' = Variable.auto_fixes t' ctxt
+ val pretty_stat =
+ case stats of
+ NONE => []
+ | SOME xs =>
+ let
+ val total = fold (curry (op +)) (map snd xs) 0
+ fun pretty_entry (s, n) =
+ [Pretty.str "size", Pretty.brk 1,
+ Pretty.str (string_of_int s), Pretty.str ":", Pretty.brk 1,
+ Pretty.str (string_of_int n), Pretty.fbrk]
+ in
+ [Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
+ Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
+ @ maps pretty_entry xs
+ end
val p = PrintMode.with_modes print_modes (fn () =>
- Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+ Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
+ @ pretty_stat)) ();
in Pretty.writeln p end;
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Apr 01 10:27:06 2010 +0200
@@ -28,15 +28,15 @@
)
fun lookup thy net t =
- case Item_Net.retrieve net t of
- [] => NONE
- | [(f, p)] =>
- let
- val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)
- in
- SOME (Envir.subst_term subst p)
- end
- | _ => NONE
+ let
+ val poss_preds = map_filter (fn (f, p) =>
+ SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
+ handle Pattern.MATCH => NONE) (Item_Net.retrieve net t)
+ in
+ case poss_preds of
+ [p] => SOME p
+ | _ => NONE
+ end
fun pred_of_function thy name =
case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
@@ -202,11 +202,12 @@
HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
end)
| _ =>
- if has_split_thm thy (fst (strip_comb t)) then
+ case find_split_thm thy (fst (strip_comb t)) of
+ SOME raw_split_thm =>
let
val (f, args) = strip_comb t
- val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
- val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+ val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
+ val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
val (_, split_args) = strip_comb split_t
@@ -231,7 +232,7 @@
in
maps flatten_of_assm assms
end
- else
+ | NONE =>
let
val (f, args) = strip_comb t
val args = map (Pattern.eta_long []) args
@@ -326,8 +327,14 @@
val thy'' = Fun_Pred.map
(fold Item_Net.update (map (apfst Logic.varify_global)
(distinct (op =) funs ~~ (#preds ind_result)))) thy'
+ fun functional_mode_of T =
+ list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
+ val thy''' = fold
+ (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
+ predname (functional_mode_of T) name)
+ (prednames ~~ distinct (op =) funs) thy''
in
- (specs, thy'')
+ (specs, thy''')
end
fun rewrite_intro thy intro =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Thu Apr 01 10:27:06 2010 +0200
@@ -113,7 +113,7 @@
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
else
- (case (fst (strip_comb atom)) of
+ case (fst (strip_comb atom)) of
(Const (@{const_name If}, _)) => let
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
val atom' = MetaSimplifier.rewrite_term thy
@@ -122,14 +122,16 @@
in
flatten constname atom' (defs, thy)
end
- | _ =>
- if (has_split_thm thy (fst (strip_comb atom))) then
+ | _ =>
+ case find_split_thm thy (fst (strip_comb atom)) of
+ NONE => (atom, (defs, thy))
+ | SOME raw_split_thm =>
let
val (f, args) = strip_comb atom
- val split_thm = prepare_split_thm (ProofContext.init thy) (the (find_split_thm' thy f))
+ val split_thm = prepare_split_thm (ProofContext.init thy) raw_split_thm
(* TODO: contextify things - this line is to unvarify the split_thm *)
(*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (ProofContext.init thy)*)
- val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
+ val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val Tcons = datatype_names_of_case_name thy (fst (dest_Const f))
val ths = maps (instantiated_case_rewrites thy) Tcons
@@ -182,8 +184,7 @@
in
(lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
end
- else
- (atom, (defs, thy)))
+
fun flatten_intros constname intros thy =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Apr 01 10:27:06 2010 +0200
@@ -9,8 +9,14 @@
(*val quickcheck : Proof.context -> term -> int -> term list option*)
val test_ref :
((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
+ val new_test_ref :
+ ((unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option) Unsynchronized.ref;
+ val eval_random_ref :
+ ((unit -> int -> int -> int -> int * int -> term list Predicate.pred) option) Unsynchronized.ref;
+
val tracing : bool Unsynchronized.ref;
- val quickcheck_compile_term : bool -> bool -> int ->
+ val quiet : bool Unsynchronized.ref;
+ val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val nrandom : int Unsynchronized.ref;
@@ -27,13 +33,20 @@
val test_ref =
Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option);
+val new_test_ref =
+ Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) option)
+
+val eval_random_ref =
+ Unsynchronized.ref (NONE : (unit -> int -> int -> int -> int * int -> term list Predicate.pred) option);
+
+
val tracing = Unsynchronized.ref false;
val quiet = Unsynchronized.ref true;
val target = "Quickcheck"
-val nrandom = Unsynchronized.ref 2;
+val nrandom = Unsynchronized.ref 3;
val debug = Unsynchronized.ref false;
@@ -129,11 +142,17 @@
(set_function_flattening (!function_flattening)
(if !debug then debug_options else options))
-fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
-val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
-val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
-val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
-val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
+val mk_predT = Predicate_Compile_Aux.mk_predT PredicateCompFuns.compfuns
+val mk_return' = Predicate_Compile_Aux.mk_single PredicateCompFuns.compfuns
+val mk_bind' = Predicate_Compile_Aux.mk_bind PredicateCompFuns.compfuns
+
+val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
+val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
+val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
+
+val mk_new_randompredT = Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.compfuns
+val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
+val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
| mk_split_lambda [x] t = lambda x t
@@ -160,7 +179,7 @@
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-fun compile_term options ctxt t =
+fun compile_term compilation options ctxt t =
let
val ctxt' = ProofContext.theory (Context.copy_thy) ctxt
val thy = (ProofContext.theory_of ctxt')
@@ -181,33 +200,90 @@
val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
val (thy3, preproc_time) = cpu_time "predicate preprocessing"
(fn () => Predicate_Compile.preprocess options const thy2)
- (* FIXME: this is just for testing the predicate compiler proof procedure! *)
- val thy3' = Predicate_Compile_Core.add_equations options [full_constname] thy3
val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
- (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3')
- val _ = Predicate_Compile_Core.print_all_modes Pos_Random_DSeq thy4
- val modes = Predicate_Compile_Core.modes_of Pos_Random_DSeq thy4 full_constname
+ (fn () =>
+ case compilation of
+ Pos_Random_DSeq =>
+ Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3
+ | New_Pos_Random_DSeq =>
+ Predicate_Compile_Core.add_new_random_dseq_equations options [full_constname] thy3
+ (*| Depth_Limited_Random =>
+ Predicate_Compile_Core.add_depth_limited_random_equations options [full_constname] thy3*))
+ val _ = Predicate_Compile_Core.print_all_modes compilation thy4
+ val modes = Predicate_Compile_Core.modes_of compilation thy4 full_constname
val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool
val prog =
if member eq_mode modes output_mode then
let
- val name = Predicate_Compile_Core.function_name_of Pos_Random_DSeq thy4
- full_constname (true, output_mode)
- val T = (mk_randompredT (HOLogic.mk_tupleT (map snd vs')))
+ val name = Predicate_Compile_Core.function_name_of compilation thy4
+ full_constname output_mode
+ val T =
+ case compilation of
+ Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
+ | New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
+ | Depth_Limited_Random =>
+ [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+ @{typ "code_numeral * code_numeral"}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
in
Const (name, T)
end
else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
- val qc_term = mk_bind (prog,
- mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
- val compilation =
- Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
- (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
- thy4 qc_term []
+
+ val qc_term =
+ case compilation of
+ Pos_Random_DSeq => mk_bind (prog,
+ mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+ | New_Pos_Random_DSeq => mk_new_bind (prog,
+ mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+ | Depth_Limited_Random => fold_rev (curry absdummy)
+ [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
+ @{typ "code_numeral * code_numeral"}]
+ (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
+ mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
+ val prog =
+ case compilation of
+ Pos_Random_DSeq =>
+ let
+ val compiled_term =
+ Code_Eval.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref)
+ (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (DSequence.map o map) proc)
+ thy4 qc_term []
+ in
+ (fn size => fn nrandom => fn depth =>
+ Option.map fst (DSequence.yield
+ (compiled_term nrandom size |> Random_Engine.run) depth true))
+ end
+ | New_Pos_Random_DSeq =>
+ let
+ val compiled_term =
+ Code_Eval.eval (SOME target)
+ ("Predicate_Compile_Quickcheck.new_test_ref", new_test_ref)
+ (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
+ g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
+ thy4 qc_term []
+ in
+ fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
+ (
+ let
+ val seed = Random_Engine.next_seed ()
+ in compiled_term nrandom size seed depth end))
+ end
+ | Depth_Limited_Random =>
+ let
+ val compiled_term = Code_Eval.eval (SOME target)
+ ("Predicate_Compile_Quickcheck.eval_random_ref", eval_random_ref)
+ (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+ g depth nrandom size seed |> (Predicate.map o map) proc)
+ thy4 qc_term []
+ in
+ fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield
+ (compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
+ end
in
- (fn size => fn nrandom => fn depth =>
- Option.map fst (DSequence.yield (compilation nrandom size |> Random_Engine.run) depth true))
+ prog
end
fun try_upto quiet f i =
@@ -229,21 +305,21 @@
(* quickcheck interface functions *)
-fun compile_term' options depth ctxt report t =
+fun compile_term' compilation options depth ctxt report t =
let
- val c = compile_term options ctxt t
+ val c = compile_term compilation options ctxt t
val dummy_report = ([], false)
in
fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
end
-fun quickcheck_compile_term function_flattening fail_safe_function_flattening depth =
+fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
let
val options =
set_fail_safe_function_flattening fail_safe_function_flattening
(set_function_flattening function_flattening (get_options ()))
in
- compile_term' options depth
+ compile_term' compilation options depth
end
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Apr 01 10:27:06 2010 +0200
@@ -0,0 +1,215 @@
+(* Title: HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
+ Author: Lukas Bulwahn, TU Muenchen
+
+Deriving specialised predicates and their intro rules
+*)
+
+signature PREDICATE_COMPILE_SPECIALISATION =
+sig
+ val find_specialisations : string list -> (string * thm list) list -> theory -> (string * thm list) list * theory
+end;
+
+structure Predicate_Compile_Specialisation : PREDICATE_COMPILE_SPECIALISATION =
+struct
+
+open Predicate_Compile_Aux;
+
+(* table of specialisations *)
+structure Specialisations = Theory_Data
+(
+ type T = (term * term) Item_Net.T;
+ val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
+ (single o fst);
+ val extend = I;
+ val merge = Item_Net.merge;
+)
+
+fun specialisation_of thy atom =
+ Item_Net.retrieve (Specialisations.get thy) atom
+
+fun print_specialisations thy =
+ tracing (cat_lines (map (fn (t, spec_t) =>
+ Syntax.string_of_term_global thy t ^ " ~~~> " ^ Syntax.string_of_term_global thy spec_t)
+ (Item_Net.content (Specialisations.get thy))))
+
+fun import (pred, intros) args ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt
+ val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
+ val Ts = binder_types (fastype_of pred')
+ val argTs = map fastype_of args
+ val Tsubst = Type.raw_matches (argTs, Ts) Vartab.empty
+ val args' = map (Envir.subst_term_types Tsubst) args
+ in
+ (((pred', intros'), args'), ctxt')
+ end
+
+(* patterns only constructed of variables and pairs/tuples are trivial constructor terms*)
+fun is_nontrivial_constrt thy t =
+ let
+ val cnstrs = flat (maps
+ (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
+ (Symtab.dest (Datatype.get_all thy)));
+ fun check t = (case strip_comb t of
+ (Var _, []) => (true, true)
+ | (Free _, []) => (true, true)
+ | (Const (@{const_name Pair}, _), ts) =>
+ pairself (forall I) (split_list (map check ts))
+ | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+ (SOME (i, Tname), Type (Tname', _)) => (false,
+ length ts = i andalso Tname = Tname' andalso forall (snd o check) ts)
+ | _ => (false, false))
+ | _ => (false, false))
+ in check t = (false, true) end;
+
+fun specialise_intros black_list (pred, intros) pats thy =
+ let
+ val ctxt = ProofContext.init thy
+ val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
+ val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
+ val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
+ val intros_t = map prop_of intros
+ val result_pats = map Var (fold_rev Term.add_vars pats [])
+ fun mk_fresh_name names =
+ let
+ val name =
+ Name.variant names ("specialised_" ^ Long_Name.base_name (fst (dest_Const pred)))
+ val bname = Sign.full_bname thy name
+ in
+ if Sign.declared_const thy bname then
+ mk_fresh_name (name :: names)
+ else
+ bname
+ end
+ val constname = mk_fresh_name []
+ val constT = map fastype_of result_pats ---> @{typ bool}
+ val specialised_const = Const (constname, constT)
+ val specialisation =
+ [(HOLogic.mk_Trueprop (list_comb (pred, pats)),
+ HOLogic.mk_Trueprop (list_comb (specialised_const, result_pats)))]
+ fun specialise_intro intro =
+ (let
+ val (prems, concl) = Logic.strip_horn (prop_of intro)
+ val env = Pattern.unify thy
+ (HOLogic.mk_Trueprop (list_comb (pred, pats)), concl) (Envir.empty 0)
+ val prems = map (Envir.norm_term env) prems
+ val args = map (Envir.norm_term env) result_pats
+ val concl = HOLogic.mk_Trueprop (list_comb (specialised_const, args))
+ val intro = Logic.list_implies (prems, concl)
+ in
+ SOME intro
+ end handle Pattern.Unif => NONE)
+ val specialised_intros_t = map_filter I (map specialise_intro intros)
+ val thy' = Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
+ val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
+ val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
+ val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
+ [list_comb (pred, pats), list_comb (specialised_const, result_pats)]
+ val thy'' = Specialisations.map (Item_Net.update (t, specialised_t)) thy'
+ val ([spec], thy''') = find_specialisations black_list [(constname, exported_intros)] thy''
+ val thy'''' = Predicate_Compile_Core.register_intros spec thy'''
+ in
+ thy''''
+ end
+
+and find_specialisations black_list specs thy =
+ let
+ val add_vars = fold_aterms (fn Var v => cons v | _ => I);
+ fun fresh_free T free_names =
+ let
+ val free_name = Name.variant free_names "x"
+ in
+ (Free (free_name, T), free_name :: free_names)
+ end
+ fun replace_term_and_restrict thy T t Tts free_names =
+ let
+ val (free, free_names') = fresh_free T free_names
+ val Tts' = map (apsnd (Pattern.rewrite_term thy [(t, free)] [])) Tts
+ val (ts', free_names'') = restrict_pattern' thy Tts' free_names'
+ in
+ (free :: ts', free_names'')
+ end
+ and restrict_pattern' thy [] free_names = ([], free_names)
+ | restrict_pattern' thy ((T, Free (x, _)) :: Tts) free_names =
+ let
+ val (ts', free_names') = restrict_pattern' thy Tts free_names
+ in
+ (Free (x, T) :: ts', free_names')
+ end
+ | restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
+ replace_term_and_restrict thy T t Tts free_names
+ | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
+ case Datatype_Data.get_constrs thy Tcon of
+ NONE => replace_term_and_restrict thy T t Tts free_names
+ | SOME constrs => (case strip_comb t of
+ (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
+ SOME constr_T =>
+ let
+ val (Ts', T') = strip_type constr_T
+ val Tsubst = Type.raw_match (T', T) Vartab.empty
+ val Ts = map (Envir.subst_type Tsubst) Ts'
+ val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names
+ val (ats', ts') = chop (length ats) bts'
+ in
+ (list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names')
+ end
+ | NONE => replace_term_and_restrict thy T t Tts free_names))
+ fun restrict_pattern thy Ts args =
+ let
+ val args = map Logic.unvarify_global args
+ val Ts = map Logic.unvarifyT_global Ts
+ val free_names = fold Term.add_free_names args []
+ val (pat, _) = restrict_pattern' thy (Ts ~~ args) free_names
+ in map Logic.varify_global pat end
+ fun detect' atom thy =
+ case strip_comb atom of
+ (pred as Const (pred_name, _), args) =>
+ let
+ val Ts = binder_types (Sign.the_const_type thy pred_name)
+ val vnames = map fst (fold Term.add_var_names args [])
+ val pats = restrict_pattern thy Ts args
+ in
+ if (exists (is_nontrivial_constrt thy) pats)
+ orelse (has_duplicates (op =) (fold add_vars pats [])) then
+ let
+ val thy' =
+ case specialisation_of thy atom of
+ [] =>
+ if member (op =) ((map fst specs) @ black_list) pred_name then
+ thy
+ else
+ (case try (Predicate_Compile_Core.intros_of thy) pred_name of
+ NONE => thy
+ | SOME [] => thy
+ | SOME intros =>
+ specialise_intros ((map fst specs) @ (pred_name :: black_list))
+ (pred, intros) pats thy)
+ | (t, specialised_t) :: _ => thy
+ val atom' =
+ case specialisation_of thy' atom of
+ [] => atom
+ | (t, specialised_t) :: _ =>
+ let
+ val subst = Pattern.match thy' (t, atom) (Vartab.empty, Vartab.empty)
+ in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom
+ (*FIXME: this exception could be caught earlier in specialisation_of *)
+ in
+ (atom', thy')
+ end
+ else (atom, thy)
+ end
+ | _ => (atom, thy)
+ fun specialise' (constname, intros) thy =
+ let
+ (* FIXME: only necessary because of sloppy Logic.unvarify in restrict_pattern *)
+ val intros = Drule.zero_var_indexes_list intros
+ val (intros_t', thy') = (fold_map o fold_map_atoms) detect' (map prop_of intros) thy
+ in
+ ((constname, map (Skip_Proof.make_thm thy') intros_t'), thy')
+ end
+ in
+ fold_map specialise' specs thy
+ end
+
+end;
\ No newline at end of file
--- a/src/HOL/Tools/inductive_realizer.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Apr 01 10:27:06 2010 +0200
@@ -1,7 +1,7 @@
(* Title: HOL/Tools/inductive_realizer.ML
Author: Stefan Berghofer, TU Muenchen
-Porgram extraction from proofs involving inductive predicates:
+Program extraction from proofs involving inductive predicates:
Realizers for induction and elimination rules.
*)
@@ -64,7 +64,6 @@
fun dt_of_intrs thy vs nparms intrs =
let
val iTs = OldTerm.term_tvars (prop_of (hd intrs));
- val Tvs = map TVar iTs;
val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (prop_of (hd intrs))));
val params = map dest_Var (take nparms ts);
--- a/src/HOL/Tools/rewrite_hol_proof.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Thu Apr 01 10:27:06 2010 +0200
@@ -33,8 +33,8 @@
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% prf1))",
"(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% \
- \ (combination % TYPE('U) % TYPE('T) % f % g % x % y %% prf1 %% prf2)) == \
- \ (cong % TYPE('U) % TYPE('T) % f % g % x % y %% \
+ \ (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) == \
+ \ (cong % TYPE('T) % TYPE('U) % f % g % x % y %% \
\ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% prf1) %% \
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf2))",
@@ -52,20 +52,20 @@
\ (sym % TYPE('T) % x % y %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prf))",
"(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% \
- \ (abstract_rule % TYPE('U) % TYPE('T) % f % g %% prf)) == \
- \ (ext % TYPE('U) % TYPE('T) % f % g %% \
+ \ (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) == \
+ \ (ext % TYPE('T) % TYPE('U) % f % g %% \
\ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% (prf % x)))",
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% \
\ (eq_reflection % TYPE('T) % x % y %% prf)) == prf",
"(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
- \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \
- \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \
+ \ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
+ \ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
\ (iffD1 % A = C % B = D %% \
- \ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \
- \ (cong % TYPE('T=>bool) % TYPE('T) % \
+ \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ (cong % TYPE('T) % TYPE('T=>bool) % \
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
\ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
@@ -74,12 +74,12 @@
"(meta_eq_to_obj_eq % TYPE('T1) % x1 % x2 %% (equal_elim % x3 % x4 %% \
\ (axm.symmetric % TYPE('T2) % x5 % x6 %% \
- \ (combination % TYPE(prop) % TYPE('T) % x7 % x8 % C % D %% \
- \ (combination % TYPE('T3) % TYPE('T) % op == % op == % A % B %% \
+ \ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \
+ \ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
\ (iffD2 % A = C % B = D %% \
- \ (cong % TYPE(bool) % TYPE('T::type) % op = A % op = B % C % D %% \
- \ (cong % TYPE('T=>bool) % TYPE('T) % \
+ \ (cong % TYPE('T::type) % TYPE(bool) % op = A % op = B % C % D %% \
+ \ (cong % TYPE('T) % TYPE('T=>bool) % \
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \
\ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool)) %% \
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prf1)) %% \
@@ -91,14 +91,14 @@
(* All *)
"(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
+ \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
\ (allI % TYPE('a) % Q %% \
\ (Lam x. \
\ iffD1 % P x % Q x %% (prf % x) %% \
\ (spec % TYPE('a) % P % x %% prf')))",
"(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
+ \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
\ (allI % TYPE('a) % P %% \
\ (Lam x. \
\ iffD2 % P x % Q x %% (prf % x) %% \
@@ -107,14 +107,14 @@
(* Ex *)
"(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
+ \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
\ (exE % TYPE('a) % P % EX x. Q x %% prf' %% \
\ (Lam x H : P x. \
\ exI % TYPE('a) % Q % x %% \
\ (iffD1 % P x % Q x %% (prf % x) %% H)))",
"(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% \
- \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE(bool) % TYPE('a) % x2 % x3 %% prf)) %% prf') == \
+ \ (HOL.refl % TYPE('T3) % x1) %% (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prf)) %% prf') == \
\ (exE % TYPE('a) % Q % EX x. P x %% prf' %% \
\ (Lam x H : Q x. \
\ exI % TYPE('a) % P % x %% \
@@ -139,7 +139,7 @@
"(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
\ (HOL.refl % TYPE(bool=>bool) % op & A)) == \
\ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% \
- \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
+ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool)) %% \
\ (HOL.refl % TYPE(bool) % A)))",
@@ -163,7 +163,7 @@
"(cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
\ (HOL.refl % TYPE(bool=>bool) % op | A)) == \
\ (cong % TYPE(bool) % TYPE(bool) % op | A % op | A % B % C %% \
- \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
+ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op | :: bool=>bool=>bool) % (op | :: bool=>bool=>bool) % A % A %% \
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op | :: bool=>bool=>bool)) %% \
\ (HOL.refl % TYPE(bool) % A)))",
@@ -185,7 +185,7 @@
"(cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
\ (HOL.refl % TYPE(bool=>bool) % op --> A)) == \
\ (cong % TYPE(bool) % TYPE(bool) % op --> A % op --> A % B % C %% \
- \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
+ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op --> :: bool=>bool=>bool) % (op --> :: bool=>bool=>bool) % A % A %% \
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op --> :: bool=>bool=>bool)) %% \
\ (HOL.refl % TYPE(bool) % A)))",
@@ -205,29 +205,29 @@
(* = *)
"(iffD1 % B % D %% \
- \ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
+ \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD1 % C % D %% prf2 %% \
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
"(iffD2 % B % D %% \
- \ (iffD1 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
+ \ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD1 % A % B %% prf1 %% \
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
"(iffD1 % A % C %% \
- \ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
+ \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4)== \
\ (iffD2 % C % D %% prf2 %% \
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
"(iffD2 % A % C %% \
- \ (iffD2 % A = C % B = D %% (cong % TYPE('T1) % TYPE(bool) % x1 % x2 % C % D %% \
- \ (cong % TYPE('T2) % TYPE(bool) % op = % op = % A % B %% \
+ \ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% \
+ \ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% \
\ (HOL.refl % TYPE('T3) % op =) %% prf1) %% prf2) %% prf3) %% prf4) == \
\ (iffD2 % A % B %% prf1 %% \
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
@@ -235,7 +235,7 @@
"(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
\ (HOL.refl % TYPE(bool=>bool) % op = A)) == \
\ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% \
- \ (cong % TYPE(bool=>bool) % TYPE(bool) % \
+ \ (cong % TYPE(bool) % TYPE(bool=>bool) % \
\ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool)) %% \
\ (HOL.refl % TYPE(bool) % A)))",
--- a/src/Pure/General/linear_set.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/General/linear_set.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,27 +7,36 @@
package isabelle
+import scala.collection.SetLike
+import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
-object Linear_Set
+
+object Linear_Set extends SetFactory[Linear_Set]
{
private case class Rep[A](
- val first: Option[A], val last: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
+ val start: Option[A], val end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
private def empty_rep[A] = Rep[A](None, None, Map(), Map())
- private def make[A](first: Option[A], last: Option[A], nexts: Map[A, A], prevs: Map[A, A])
- : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(first, last, nexts, prevs) }
+ private def make[A](start: Option[A], end: Option[A], nexts: Map[A, A], prevs: Map[A, A])
+ : Linear_Set[A] = new Linear_Set[A] { override val rep = Rep(start, end, nexts, prevs) }
- def empty[A]: Linear_Set[A] = new Linear_Set
- def apply[A](elems: A*): Linear_Set[A] = empty[A] ++ elems
+ implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
+ override def empty[A] = new Linear_Set[A]
class Duplicate(s: String) extends Exception(s)
class Undefined(s: String) extends Exception(s)
}
-class Linear_Set[A] extends scala.collection.immutable.Set[A]
+class Linear_Set[A]
+ extends scala.collection.immutable.Set[A]
+ with GenericSetTemplate[A, Linear_Set]
+ with SetLike[A, Linear_Set[A]]
{
+ override def companion: GenericCompanion[Linear_Set] = Linear_Set
+
+
/* representation */
protected val rep = Linear_Set.empty_rep[A]
@@ -43,10 +52,10 @@
else
hook match {
case None =>
- rep.first match {
+ rep.start match {
case None => Linear_Set.make(Some(elem), Some(elem), Map(), Map())
case Some(elem1) =>
- Linear_Set.make(Some(elem), rep.last,
+ Linear_Set.make(Some(elem), rep.end,
rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem))
}
case Some(elem1) =>
@@ -54,10 +63,10 @@
else
rep.nexts.get(elem1) match {
case None =>
- Linear_Set.make(rep.first, Some(elem),
+ Linear_Set.make(rep.start, Some(elem),
rep.nexts + (elem1 -> elem), rep.prevs + (elem -> elem1))
case Some(elem2) =>
- Linear_Set.make(rep.first, rep.last,
+ Linear_Set.make(rep.start, rep.end,
rep.nexts + (elem1 -> elem) + (elem -> elem2),
rep.prevs + (elem2 -> elem) + (elem -> elem1))
}
@@ -66,13 +75,13 @@
def delete_after(hook: Option[A]): Linear_Set[A] =
hook match {
case None =>
- rep.first match {
+ rep.start match {
case None => throw new Linear_Set.Undefined("")
case Some(elem1) =>
rep.nexts.get(elem1) match {
case None => empty
case Some(elem2) =>
- Linear_Set.make(Some(elem2), rep.last, rep.nexts - elem1, rep.prevs - elem2)
+ Linear_Set.make(Some(elem2), rep.end, rep.nexts - elem1, rep.prevs - elem2)
}
}
case Some(elem1) =>
@@ -83,9 +92,9 @@
case Some(elem2) =>
rep.nexts.get(elem2) match {
case None =>
- Linear_Set.make(rep.first, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
+ Linear_Set.make(rep.start, Some(elem1), rep.nexts - elem1, rep.prevs - elem2)
case Some(elem3) =>
- Linear_Set.make(rep.first, rep.last,
+ Linear_Set.make(rep.start, rep.end,
rep.nexts - elem2 + (elem1 -> elem3),
rep.prevs - elem2 + (elem3 -> elem1))
}
@@ -100,8 +109,8 @@
if (isEmpty) this
else {
val next =
- if (from == rep.last) None
- else if (from == None) rep.first
+ if (from == rep.end) None
+ else if (from == None) rep.start
else from.map(rep.nexts(_))
if (next == to) this
else delete_after(from).delete_between(from, to)
@@ -113,15 +122,13 @@
override def stringPrefix = "Linear_Set"
- def empty[B]: Linear_Set[B] = Linear_Set.empty
-
- override def isEmpty: Boolean = !rep.first.isDefined
- def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
+ override def isEmpty: Boolean = !rep.start.isDefined
+ override def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
def contains(elem: A): Boolean =
- !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+ !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
- private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+ private def iterator_from(start: Option[A]): Iterator[A] = new Iterator[A] {
private var next_elem = start
def hasNext = next_elem.isDefined
def next =
@@ -133,18 +140,13 @@
}
}
- def elements: Iterator[A] = elements_from(rep.first)
+ override def iterator: Iterator[A] = iterator_from(rep.start)
- def elements(elem: A): Iterator[A] =
- if (contains(elem)) elements_from(Some(elem))
+ def iterator(elem: A): Iterator[A] =
+ if (contains(elem)) iterator_from(Some(elem))
else throw new Linear_Set.Undefined(elem.toString)
- def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
-
- override def + (elem1: A, elem2: A, elems: A*): Linear_Set[A] =
- this + elem1 + elem2 ++ elems
- override def ++ (elems: Iterable[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
- override def ++ (elems: Iterator[A]): Linear_Set[A] = (this /: elems) ((s, elem) => s + elem)
+ def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem)
def - (elem: A): Linear_Set[A] =
if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString)
--- a/src/Pure/General/scan.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/General/scan.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,6 +7,7 @@
package isabelle
+import scala.collection.generic.Addable
import scala.collection.immutable.PagedSeq
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
import scala.util.parsing.combinator.RegexParsers
@@ -27,7 +28,7 @@
def apply(elems: String*): Lexicon = empty ++ elems
}
- class Lexicon extends scala.collection.Set[String] with RegexParsers
+ class Lexicon extends Addable[String, Lexicon] with RegexParsers
{
/* representation */
@@ -65,14 +66,14 @@
}
- /* Set methods */
+ /* pseudo Set methods */
- override def stringPrefix = "Lexicon"
+ def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
- override def isEmpty: Boolean = { main_tree.branches.isEmpty }
+ override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
- def size: Int = content(main_tree, Nil).length
- def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
+ def empty: Lexicon = Lexicon.empty
+ def isEmpty: Boolean = main_tree.branches.isEmpty
def contains(elem: String): Boolean =
lookup(elem) match {
@@ -80,6 +81,11 @@
case _ => false
}
+
+ /* Addable methods */
+
+ def repr = this
+
def + (elem: String): Lexicon =
if (contains(elem)) this
else {
@@ -102,11 +108,6 @@
new Lexicon { override val main_tree = extend(old.main_tree, 0) }
}
- def + (elem1: String, elem2: String, elems: String*): Lexicon =
- this + elem1 + elem2 ++ elems
- def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
- def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
-
/** RegexParsers methods **/
--- a/src/Pure/General/symbol.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/General/symbol.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,7 +7,7 @@
package isabelle
import scala.io.Source
-import scala.collection.{jcl, mutable}
+import scala.collection.mutable
import scala.util.matching.Regex
@@ -54,9 +54,9 @@
}
- /* elements */
+ /* iterator */
- def elements(text: CharSequence) = new Iterator[CharSequence]
+ def iterator(text: CharSequence) = new Iterator[CharSequence]
{
private val matcher = new Matcher(text)
private var i = 0
@@ -124,12 +124,7 @@
}
(min, max)
}
- private val table =
- {
- val table = new jcl.HashMap[String, String] // reasonably efficient?
- for ((x, y) <- list) table + (x -> y)
- table
- }
+ private val table = Map[String, String]() ++ list
def recode(text: String): String =
{
val len = text.length
--- a/src/Pure/General/xml.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/General/xml.scala Thu Apr 01 10:27:06 2010 +0200
@@ -34,34 +34,34 @@
/* string representation */
private def append_text(text: String, s: StringBuilder) {
- if (text == null) s ++ text
+ if (text == null) s ++= text
else {
- for (c <- text.elements) c match {
- case '<' => s ++ "<"
- case '>' => s ++ ">"
- case '&' => s ++ "&"
- case '"' => s ++ """
- case '\'' => s ++ "'"
- case _ => s + c
+ for (c <- text.iterator) c match {
+ case '<' => s ++= "<"
+ case '>' => s ++= ">"
+ case '&' => s ++= "&"
+ case '"' => s ++= """
+ case '\'' => s ++= "'"
+ case _ => s += c
}
}
}
private def append_elem(name: String, atts: Attributes, s: StringBuilder) {
- s ++ name
+ s ++= name
for ((a, x) <- atts) {
- s ++ " "; s ++ a; s ++ "=\""; append_text(x, s); s ++ "\""
+ s ++= " "; s ++= a; s ++= "=\""; append_text(x, s); s ++= "\""
}
}
private def append_tree(tree: Tree, s: StringBuilder) {
tree match {
case Elem(name, atts, Nil) =>
- s ++ "<"; append_elem(name, atts, s); s ++ "/>"
+ s ++= "<"; append_elem(name, atts, s); s ++= "/>"
case Elem(name, atts, ts) =>
- s ++ "<"; append_elem(name, atts, s); s ++ ">"
+ s ++= "<"; append_elem(name, atts, s); s ++= ">"
for (t <- ts) append_tree(t, s)
- s ++ "</"; s ++ name; s ++ ">"
+ s ++= "</"; s ++= name; s ++= ">"
case Text(text) => append_text(text, s)
}
}
--- a/src/Pure/Isar/local_theory.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML Thu Apr 01 10:27:06 2010 +0200
@@ -20,7 +20,6 @@
val target_of: local_theory -> Proof.context
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
- val checkpoint: local_theory -> local_theory
val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
@@ -149,7 +148,8 @@
thy
|> Sign.map_naming (K (naming_of lthy))
|> f
- ||> Sign.restore_naming thy);
+ ||> Sign.restore_naming thy
+ ||> Theory.checkpoint);
fun theory f = #2 o theory_result (f #> pair ());
--- a/src/Pure/Proof/extraction.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Apr 01 10:27:06 2010 +0200
@@ -541,7 +541,7 @@
let
val prf = join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
- val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
+ val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye;
val T = etype_of thy' vs' [] prop;
val defs' = if T = nullT then defs
else fst (extr d defs vs ts Ts hs prf0)
@@ -562,7 +562,7 @@
val corr_prf' = List.foldr forall_intr_prf
(proof_combt
(PThm (serial (),
- ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
+ ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop))
(map (get_var_type corr_prop) (vfs_of prop))
in
@@ -580,7 +580,7 @@
| corr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
let
val (vs', tye) = find_inst prop Ts ts vs;
- val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
+ val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (defs, prf0)
@@ -631,7 +631,7 @@
let
val prf = join_proof body;
val (vs', tye) = find_inst prop Ts ts vs;
- val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
+ val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
case Symtab.lookup realizers s of
NONE => (case find vs' (find' s defs) of
@@ -665,15 +665,15 @@
val corr_prf' =
chtype [] equal_elim_axm %> lhs %> rhs %%
(chtype [propT] symmetric_axm %> rhs %> lhs %%
- (chtype [propT, T] combination_axm %> f %> f %> c %> t' %%
+ (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
(chtype [T --> propT] reflexive_axm %> f) %%
PAxm (cname ^ "_def", eqn,
- SOME (map TVar (OldTerm.term_tvars eqn))))) %% corr_prf;
+ SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf;
val corr_prop = Reconstruct.prop_of corr_prf';
val corr_prf'' = List.foldr forall_intr_prf
(proof_combt
(PThm (serial (),
- ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
+ ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop))
(map (get_var_type corr_prop) (vfs_of prop));
in
@@ -691,7 +691,7 @@
| extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
let
val (vs', tye) = find_inst prop Ts ts vs;
- val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
+ val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
case find vs' (Symtab.lookup_list realizers s) of
SOME (t, _) => (defs, subst_TVars tye' t)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Apr 01 10:27:06 2010 +0200
@@ -179,7 +179,7 @@
(PAxm ("Pure.reflexive", _, _) % _)) =
let val (U, V) = (case T of
Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
- in SOME (prf %% (ax combination_axm [V, U] %> eq % ?? eq % ?? t % ?? t %%
+ in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
(ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
end
@@ -229,7 +229,7 @@
if member (op =) defs s then
let
val vs = vars_of prop;
- val tvars = OldTerm.term_tvars prop;
+ val tvars = Term.add_tvars prop [] |> rev;
val (_, rhs) = Logic.dest_equals prop;
val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
--- a/src/Pure/Proof/proofchecker.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Proof/proofchecker.ML Thu Apr 01 10:27:06 2010 +0200
@@ -35,7 +35,7 @@
fun thm_of_atom thm Ts =
let
- val tvars = OldTerm.term_tvars (Thm.full_prop_of thm);
+ val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
val (fmap, thm') = Thm.varifyT_global' [] thm;
val ctye = map (pairself (Thm.ctyp_of thy))
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
--- a/src/Pure/Proof/reconstruct.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML Thu Apr 01 10:27:06 2010 +0200
@@ -136,8 +136,8 @@
fun mk_cnstrts_atom env vTs prop opTs prf =
let
- val tvars = OldTerm.term_tvars prop;
- val tfrees = OldTerm.term_tfrees prop;
+ val tvars = Term.add_tvars prop [] |> rev;
+ val tfrees = Term.add_tfrees prop [] |> rev;
val (Ts, env') =
(case opTs of
NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
@@ -304,7 +304,7 @@
end;
fun prop_of_atom prop Ts = subst_atomic_types
- (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts)
+ (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
(forall_intr_vfs prop);
val head_norm = Envir.head_norm (Envir.empty 0);
@@ -370,9 +370,9 @@
end
| SOME (maxidx', prf) => (maxidx' + maxidx + 1,
incr_indexes (maxidx + 1) prf, prfs));
- val tfrees = OldTerm.term_tfrees prop;
+ val tfrees = Term.add_tfrees prop [] |> rev;
val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
- (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
+ (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
val varify = map_type_tfree (fn p as (a, S) =>
if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
in
--- a/src/Pure/ProofGeneral/preferences.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Thu Apr 01 10:27:06 2010 +0200
@@ -146,7 +146,7 @@
"Show leading question mark of variable name"];
val tracing_preferences =
- [bool_pref trace_simp_ref
+ [bool_pref trace_simp_default
"trace-simplifier"
"Trace simplification rules.",
nat_pref trace_simp_depth_limit
--- a/src/Pure/System/isabelle_syntax.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/System/isabelle_syntax.scala Thu Apr 01 10:27:06 2010 +0200
@@ -40,7 +40,7 @@
result: StringBuilder)
{
result.append("(")
- val elems = body.elements
+ val elems = body.iterator
if (elems.hasNext) append_elem(elems.next, result)
while (elems.hasNext) {
result.append(", ")
--- a/src/Pure/System/isabelle_system.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Apr 01 10:27:06 2010 +0200
@@ -24,7 +24,7 @@
private val environment: Map[String, String] =
{
- import scala.collection.jcl.Conversions._
+ import scala.collection.JavaConversions._
val env0 = Map(java.lang.System.getenv.toList: _*)
@@ -288,7 +288,7 @@
for (file <- files if file.isFile) logics += file.getName
}
}
- logics.toList.sort(_ < _)
+ logics.toList.sortWith(_ < _)
}
@@ -297,7 +297,7 @@
private def read_symbols(path: String): List[String] =
{
val file = platform_file(path)
- if (file.isFile) Source.fromFile(file).getLines.toList
+ if (file.isFile) Source.fromFile(file).getLines().toList
else Nil
}
val symbols = new Symbol.Interpretation(
--- a/src/Pure/System/standard_system.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/System/standard_system.scala Thu Apr 01 10:27:06 2010 +0200
@@ -12,7 +12,7 @@
BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
File, FileFilter, IOException}
-import scala.io.Source
+import scala.io.{Source, Codec}
import scala.util.matching.Regex
import scala.collection.mutable
@@ -20,6 +20,7 @@
object Standard_System
{
val charset = "UTF-8"
+ def codec(): Codec = Codec(charset)
/* permissive UTF-8 decoding */
@@ -135,7 +136,7 @@
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
- val output = Source.fromInputStream(proc.getInputStream, charset).mkString // FIXME
+ val output = Source.fromInputStream(proc.getInputStream)(codec()).mkString // FIXME
val rc =
try { proc.waitFor }
finally {
--- a/src/Pure/Thy/command.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Thy/command.scala Thu Apr 01 10:27:06 2010 +0200
@@ -35,11 +35,11 @@
{
/* classification */
- def is_command: Boolean = !span.isEmpty && span.first.is_command
+ def is_command: Boolean = !span.isEmpty && span.head.is_command
def is_ignored: Boolean = span.forall(_.is_ignored)
def is_malformed: Boolean = !is_command && !is_ignored
- def name: String = if (is_command) span.first.content else ""
+ def name: String = if (is_command) span.head.content else ""
override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
--- a/src/Pure/Thy/completion.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Thy/completion.scala Thu Apr 01 10:27:06 2010 +0200
@@ -94,7 +94,7 @@
case Some(word) =>
words_lex.completions(word).map(words_map(_)) match {
case Nil => None
- case cs => Some(word, cs.sort(_ < _))
+ case cs => Some(word, cs.sortWith(_ < _))
}
case None => None
}
--- a/src/Pure/Thy/document.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Thy/document.scala Thu Apr 01 10:27:06 2010 +0200
@@ -14,7 +14,7 @@
def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
{
var offset = 0
- for (cmd <- commands.elements) yield {
+ for (cmd <- commands.iterator) yield {
val start = offset
offset += cmd.length
(cmd, start)
@@ -92,17 +92,17 @@
def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
{
// FIXME relative search!
- commands.elements.find(is_unparsed) match {
+ commands.iterator.find(is_unparsed) match {
case Some(first_unparsed) =>
val prefix = commands.prev(first_unparsed)
- val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
+ val body = commands.iterator(first_unparsed).takeWhile(is_unparsed).toList
val suffix = commands.next(body.last)
val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
val (before_edit, spans1) =
- if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
+ if (!spans0.isEmpty && Some(spans0.head) == prefix.map(_.span))
(prefix, spans0.tail)
else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
@@ -128,8 +128,8 @@
val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
- val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
- val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
+ val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+ val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
val doc_edits =
removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
--- a/src/Pure/Thy/html.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Thy/html.scala Thu Apr 01 10:27:06 2010 +0200
@@ -41,29 +41,29 @@
val t = new StringBuilder
def flush() {
if (!t.isEmpty) {
- ts + XML.Text(t.toString)
+ ts += XML.Text(t.toString)
t.clear
}
}
def add(elem: XML.Tree) {
flush()
- ts + elem
+ ts += elem
}
- val syms = Symbol.elements(txt).map(_.toString)
+ val syms = Symbol.iterator(txt).map(_.toString)
while (syms.hasNext) {
val s1 = syms.next
def s2() = if (syms.hasNext) syms.next else ""
s1 match {
case "\n" => add(XML.elem(BR))
- case "\\<^bsub>" => t ++ s1 // FIXME
- case "\\<^esub>" => t ++ s1 // FIXME
- case "\\<^bsup>" => t ++ s1 // FIXME
- case "\\<^esup>" => t ++ s1 // FIXME
+ case "\\<^bsub>" => t ++= s1 // FIXME
+ case "\\<^esub>" => t ++= s1 // FIXME
+ case "\\<^bsup>" => t ++= s1 // FIXME
+ case "\\<^esup>" => t ++= s1 // FIXME
case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
- case _ => t ++ s1
+ case _ => t ++= s1
}
}
flush()
--- a/src/Pure/Thy/markup_node.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Thy/markup_node.scala Thu Apr 01 10:27:06 2010 +0200
@@ -24,7 +24,7 @@
def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
private def add(branch: Markup_Tree) = // FIXME avoid sort
- set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
+ set_branches((branch :: branches).sortWith((a, b) => a.node.start < b.node.start))
private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
@@ -70,7 +70,7 @@
markup <- markups
} yield markup
if (next_x < node.stop)
- filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+ filled_gaps ::: List(new Markup_Node(next_x, node.stop, node.info))
else filled_gaps
}
}
--- a/src/Pure/Thy/state.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/Thy/state.scala Thu Apr 01 10:27:06 2010 +0200
@@ -84,7 +84,7 @@
val (begin, end) = Position.get_offsets(atts)
if (begin.isEmpty || end.isEmpty) state
else if (kind == Markup.ML_TYPING) {
- val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
+ val info = body.head.asInstanceOf[XML.Text].content // FIXME proper match!?
state.add_markup(
command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
}
--- a/src/Pure/build-jars Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/build-jars Thu Apr 01 10:27:06 2010 +0200
@@ -88,7 +88,7 @@
echo "###"
rm -rf classes && mkdir classes
- "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 "${SOURCES[@]}" || \
+ "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target:jvm-1.5 "${SOURCES[@]}" || \
fail "Failed to compile sources"
mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR"
(
--- a/src/Pure/meta_simplifier.ML Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Pure/meta_simplifier.ML Thu Apr 01 10:27:06 2010 +0200
@@ -15,7 +15,7 @@
val debug_simp_value: Config.value Config.T
val trace_simp: bool Config.T
val trace_simp_value: Config.value Config.T
- val trace_simp_ref: bool Unsynchronized.ref
+ val trace_simp_default: bool Unsynchronized.ref
val trace_simp_depth_limit: int Unsynchronized.ref
type rrule
val eq_rrule: rrule * rrule -> bool
@@ -277,9 +277,10 @@
val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
val debug_simp = Config.bool debug_simp_value;
-val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
+val trace_simp_default = Unsynchronized.ref false;
+val trace_simp_value =
+ Config.declare false "trace_simp" (fn _ => Config.Bool (!trace_simp_default));
val trace_simp = Config.bool trace_simp_value;
-val trace_simp_ref = Unsynchronized.ref false;
local
@@ -301,31 +302,25 @@
fun print_term_global ss warn a thy t =
print_term ss warn (K a) t (ProofContext.init thy);
-fun if_enabled (Simpset ({context, ...}, _)) b flag f =
+fun if_enabled (Simpset ({context, ...}, _)) flag f =
(case context of
- SOME ctxt => if b orelse Config.get ctxt flag then f ctxt else ()
+ SOME ctxt => if Config.get ctxt flag then f ctxt else ()
| NONE => ())
-fun debug warn a ss =
- if_enabled ss false debug_simp (fn _ => prnt ss warn (a ()));
-fun trace warn a ss =
- if_enabled ss (!trace_simp_ref) trace_simp (fn _ => prnt ss warn (a ()));
+fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
-fun debug_term warn a ss t =
- if_enabled ss false debug_simp (print_term ss warn a t);
-fun trace_term warn a ss t =
- if_enabled ss (!trace_simp_ref) trace_simp (print_term ss warn a t);
+fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
fun trace_cterm warn a ss ct =
- if_enabled ss (!trace_simp_ref) trace_simp
- (print_term ss warn a (Thm.term_of ct));
+ if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
fun trace_thm a ss th =
- if_enabled ss (!trace_simp_ref) trace_simp
- (print_term ss false a (Thm.full_prop_of th));
+ if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
fun trace_named_thm a ss (th, name) =
- if_enabled ss (!trace_simp_ref) trace_simp (print_term ss false
+ if_enabled ss trace_simp (print_term ss false
(fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
(Thm.full_prop_of th));
--- a/src/Tools/jEdit/README_BUILD Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Thu Apr 01 10:27:06 2010 +0200
@@ -5,10 +5,10 @@
* Proper Java JRE/JDK from Sun, e.g. 1.6.0_18
http://java.sun.com/javase/downloads/index.jsp
-* Netbeans 6.7.1
+* Netbeans 6.8
http://www.netbeans.org/downloads/index.html
-* Scala for Netbeans: version 6.7v1 for NB 6.7
+* Scala for Netbeans: version 6.8v1.1
http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
http://blogtrader.net/dcaoyuan/category/NetBeans
http://wiki.netbeans.org/Scala
@@ -19,6 +19,7 @@
Netbeans Project "jEdit": install official sources as ./contrib/jEdit/.
* jEdit plugins:
+ Netbeans Library "Console" = $HOME/.jedit/jars/Console.jar
Netbeans Library "SideKick" = $HOME/.jedit/jars/SideKick.jar
Netbeans Library "ErrorList" = $HOME/.jedit/jars/ErrorList.jar
Netbeans Library "Hyperlinks" = $HOME/.jedit/jars/Hyperlinks.jar
--- a/src/Tools/jEdit/nbproject/build-impl.xml Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/nbproject/build-impl.xml Thu Apr 01 10:27:06 2010 +0200
@@ -24,7 +24,7 @@
<target depends="test,jar,javadoc" description="Build and test whole project." name="default"/>
<!--
======================
- INITIALIZATION SECTION
+ INITIALIZATION SECTION
======================
-->
<target name="-pre-init">
@@ -40,9 +40,9 @@
<isset property="env.SCALA_HOME"/>
</condition>
<fail unless="scala.home">
-You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
-property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
-Scala installation directory.
+ You must set SCALA_HOME or environment property and append "-J-Dscala.home=scalahomepath"
+ property to the end of "netbeans_default_options" in NetBeansInstallationPath/etc/netbeans.conf to point to
+ Scala installation directory.
</fail>
<property name="scala.compiler" value="${scala.home}/lib/scala-compiler.jar"/>
<property name="scala.library" value="${scala.home}/lib/scala-library.jar"/>
@@ -53,14 +53,13 @@
<pathelement location="${scala.library}"/>
</classpath>
</taskdef>
- <chmod dir="${scala.home}/bin" includes="**/*" perm="u+rx"/>
</target>
<target depends="-pre-init,-init-private" name="-init-user">
<property file="${user.properties.file}"/>
<!-- The two properties below are usually overridden -->
<!-- by the active platform. Just a fallback. -->
- <property name="default.javac.source" value="1.4"/>
- <property name="default.javac.target" value="1.4"/>
+ <property name="default.javac.source" value="1.5"/>
+ <property name="default.javac.target" value="1.5"/>
</target>
<target depends="-pre-init,-init-private,-init-user" name="-init-project">
<property file="nbproject/configs/${config}.properties"/>
@@ -126,6 +125,7 @@
<property name="javadoc.encoding.used" value="${source.encoding}"/>
<property name="includes" value="**"/>
<property name="excludes" value=""/>
+ <property name="extdirs" value=" "/>
<property name="do.depend" value="false"/>
<condition property="do.depend.true">
<istrue value="${do.depend}"/>
@@ -191,7 +191,13 @@
<sequential>
<depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
<classpath>
- <path path="@{classpath}"/>
+ <path>
+ <pathelement path="@{classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ <pathelement location="${build.classes.dir}"/>
+ </path>
</classpath>
</depend>
</sequential>
@@ -217,33 +223,25 @@
<attribute default="${src.dir}" name="srcdir"/>
<attribute default="${build.classes.dir}" name="destdir"/>
<attribute default="${javac.classpath}" name="classpath"/>
+ <attribute default="${extdirs}" name="extdirs"/>
<attribute default="${includes}" name="includes"/>
<attribute default="${excludes}" name="excludes"/>
- <attribute default="${javac.compilerargs}" name="addparams"/>
+ <attribute default="${scalac.compilerargs}" name="addparams"/>
<attribute default="" name="sourcepath"/>
<element name="customize" optional="true"/>
<sequential>
- <fsc addparams="@{addparams}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}">
+ <scalac addparams="-make:transitive -dependencyfile ${basedir}/${build.dir}/.scala_dependencies @{addparams}" deprecation="${scalac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" extdirs="@{extdirs}" force="yes" fork="true" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}" unchecked="${scalac.unchecked}">
<classpath>
- <path path="@{classpath}"/>
- <fileset dir="${scala.lib}">
- <include name="**/*.jar"/>
- </fileset>
+ <path>
+ <pathelement path="@{classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
+ <pathelement location="${build.classes.dir}"/>
+ </path>
</classpath>
<customize/>
- </fsc>
- </sequential>
- </macrodef>
- <macrodef name="depend" uri="http://www.netbeans.org/ns/scala-project/1">
- <attribute default="${src.dir}" name="srcdir"/>
- <attribute default="${build.classes.dir}" name="destdir"/>
- <attribute default="${javac.classpath}" name="classpath"/>
- <sequential>
- <depend cache="${build.dir}/depcache" destdir="@{destdir}" excludes="${excludes}" includes="${includes}" srcdir="@{srcdir}">
- <classpath>
- <path path="@{classpath}"/>
- </classpath>
- </depend>
+ </scalac>
</sequential>
</macrodef>
<macrodef name="force-recompile" uri="http://www.netbeans.org/ns/scala-project/1">
@@ -551,14 +549,14 @@
-->
<target depends="init" name="-javadoc-build">
<mkdir dir="${dist.javadoc.dir}"/>
- <javadoc additionalparam="${javadoc.additionalparam}" author="${javadoc.author}" charset="UTF-8" destdir="${dist.javadoc.dir}" docencoding="UTF-8" encoding="${javadoc.encoding.used}" failonerror="true" noindex="${javadoc.noindex}" nonavbar="${javadoc.nonavbar}" notree="${javadoc.notree}" private="${javadoc.private}" source="${javac.source}" splitindex="${javadoc.splitindex}" use="${javadoc.use}" useexternalfile="true" version="${javadoc.version}" windowtitle="${javadoc.windowtitle}">
+ <scaladoc addparams="${javadoc.additionalparam}" deprecation="yes" destdir="${dist.javadoc.dir}" doctitle="${javadoc.windowtitle}" encoding="${javadoc.encoding.used}" srcdir="${src.dir}" unchecked="yes" windowtitle="${javadoc.windowtitle}">
<classpath>
<path path="${javac.classpath}"/>
+ <fileset dir="${scala.lib}">
+ <include name="**/*.jar"/>
+ </fileset>
</classpath>
- <fileset dir="${src.dir}" excludes="${excludes}" includes="${includes}">
- <filename name="**/*.java"/>
- </fileset>
- </javadoc>
+ </scaladoc>
</target>
<target depends="init,-javadoc-build" if="netbeans.home" name="-javadoc-browse" unless="no.javadoc.preview">
<nbbrowse file="${dist.javadoc.dir}/index.html"/>
@@ -580,7 +578,7 @@
<scalaProject1:depend classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
</target>
<target depends="init,compile,-pre-pre-compile-test,-pre-compile-test,-compile-test-depend" if="have.tests" name="-do-compile-test">
- <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" srcdir=""/>
+ <scalaProject1:scalac classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" srcdir=""/>
<copy todir="${build.test.classes.dir}"/>
</target>
<target name="-post-compile-test">
@@ -595,7 +593,7 @@
<target depends="init,compile,-pre-pre-compile-test,-pre-compile-test-single" if="have.tests" name="-do-compile-test-single">
<fail unless="javac.includes">Must select some files in the IDE or set javac.includes</fail>
<scalaProject1:force-recompile destdir="${build.test.classes.dir}"/>
- <scalaProject1:scalac classpath="${javac.test.classpath}" debug="true" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
+ <scalaProject1:scalac classpath="${javac.test.classpath}" destdir="${build.test.classes.dir}" excludes="" includes="${javac.includes}" sourcepath="" srcdir=""/>
<copy todir="${build.test.classes.dir}"/>
</target>
<target name="-post-compile-test-single">
--- a/src/Tools/jEdit/nbproject/genfiles.properties Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/nbproject/genfiles.properties Thu Apr 01 10:27:06 2010 +0200
@@ -4,5 +4,5 @@
# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
nbproject/build-impl.xml.data.CRC32=8f41dcce
-nbproject/build-impl.xml.script.CRC32=69f2059c
-nbproject/build-impl.xml.stylesheet.CRC32=bc42a706@1.3.0
+nbproject/build-impl.xml.script.CRC32=1c29c971
+nbproject/build-impl.xml.stylesheet.CRC32=8c3c03dd@1.3.4
--- a/src/Tools/jEdit/nbproject/project.properties Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/nbproject/project.properties Thu Apr 01 10:27:06 2010 +0200
@@ -75,3 +75,7 @@
${build.test.classes.dir}
source.encoding=UTF-8
src.dir=${file.reference.isabelle-jedit-src}
+scalac.compilerargs=
+scalac.deprecation=no
+scalac.unchecked=no
+
--- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu Apr 01 10:27:06 2010 +0200
@@ -8,6 +8,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor, Actor._
import scala.collection.mutable
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Apr 01 10:27:06 2010 +0200
@@ -8,6 +8,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor._
import java.awt.event.{MouseAdapter, MouseEvent}
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import java.io.StringReader
import java.awt.{BorderLayout, Dimension}
import java.awt.event.MouseEvent
--- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,14 +7,16 @@
package isabelle.jedit
+import isabelle._
+
import org.gjt.sp.jedit.io.Encoding
import org.gjt.sp.jedit.buffer.JEditBuffer
-import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
+import java.nio.charset.{Charset, CodingErrorAction}
import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
CharArrayReader, ByteArrayOutputStream}
-import scala.io.{Source, BufferedSource}
+import scala.io.{Codec, Source, BufferedSource}
object Isabelle_Encoding
@@ -28,24 +30,23 @@
class Isabelle_Encoding extends Encoding
{
private val charset = Charset.forName(Standard_System.charset)
- private val BUFSIZE = 32768
+ val BUFSIZE = 32768
- private def text_reader(in: InputStream, decoder: CharsetDecoder): Reader =
+ private def text_reader(in: InputStream, codec: Codec): Reader =
{
- def source(): Source =
- BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
+ val source = new BufferedSource(in)(codec)
new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
}
override def getTextReader(in: InputStream): Reader =
- text_reader(in, charset.newDecoder())
+ text_reader(in, Standard_System.codec())
override def getPermissiveTextReader(in: InputStream): Reader =
{
- val decoder = charset.newDecoder()
- decoder.onMalformedInput(CodingErrorAction.REPLACE)
- decoder.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, decoder)
+ val codec = Standard_System.codec()
+ codec.onMalformedInput(CodingErrorAction.REPLACE)
+ codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, codec)
}
override def getTextWriter(out: OutputStream): Writer =
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import java.io.File
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Apr 01 10:27:06 2010 +0200
@@ -8,6 +8,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.collection.Set
import scala.collection.immutable.TreeSet
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor._
import javax.swing.JPanel
--- a/src/Tools/jEdit/src/jedit/plugin.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu Apr 01 10:27:06 2010 +0200
@@ -9,6 +9,8 @@
package isabelle.jedit
+import isabelle._
+
import java.io.{FileInputStream, IOException}
import java.awt.Font
import javax.swing.JTextArea
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import scala.actors.Actor._
import java.awt.{Dimension, Graphics, BorderLayout}
--- a/src/Tools/jEdit/src/jedit/scala_console.scala Thu Apr 01 10:26:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala Thu Apr 01 10:27:06 2010 +0200
@@ -7,6 +7,8 @@
package isabelle.jedit
+import isabelle._
+
import console.{Console, ConsolePane, Shell, Output}
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
@@ -63,7 +65,7 @@
def write(cbuf: Array[Char], off: Int, len: Int)
{
- if (len > 0) write(new String(cbuf.subArray(off, off + len)))
+ if (len > 0) write(new String(cbuf.slice(off, off + len)))
}
override def write(str: String)