# HG changeset patch
# User Chengsong
# Date 1650355681 -3600
# Node ID 61eff2abb0b640bfa3282362066ff00afa369ad7
# Parent 48ce16d61e03f35c8bdfcd18673ddeb49cb68547
problem with erase
diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/ClosedForms.thy Tue Apr 19 09:08:01 2022 +0100
@@ -25,62 +25,62 @@
inductive
- hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto> _" [99, 99] 99)
+ hrewrite:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto> _" [99, 99] 99)
where
- "RSEQ RZERO r2 \<leadsto> RZERO"
-| "RSEQ r1 RZERO \<leadsto> RZERO"
-| "RSEQ RONE r \<leadsto> r"
-| "r1 \<leadsto> r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r2 r3"
-| "r3 \<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 \<leadsto> RSEQ r1 r4"
-| "r \<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto> (RALTS (rs1 @ [r'] @ rs2))"
+ "RSEQ RZERO r2 h\<leadsto> RZERO"
+| "RSEQ r1 RZERO h\<leadsto> RZERO"
+| "RSEQ RONE r h\<leadsto> r"
+| "r1 h\<leadsto> r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r2 r3"
+| "r3 h\<leadsto> r4 \<Longrightarrow> RSEQ r1 r3 h\<leadsto> RSEQ r1 r4"
+| "r h\<leadsto> r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto> (RALTS (rs1 @ [r'] @ rs2))"
(*context rule for eliminating 0, alts--corresponds to the recursive call flts r::rs = r::(flts rs)*)
-| "RALTS (rsa @ [RZERO] @ rsb) \<leadsto> RALTS (rsa @ rsb)"
-| "RALTS (rsa @ [RALTS rs1] @ rsb) \<leadsto> RALTS (rsa @ rs1 @ rsb)"
-| "RALTS [] \<leadsto> RZERO"
-| "RALTS [r] \<leadsto> r"
-| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) \<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
+| "RALTS (rsa @ [RZERO] @ rsb) h\<leadsto> RALTS (rsa @ rsb)"
+| "RALTS (rsa @ [RALTS rs1] @ rsb) h\<leadsto> RALTS (rsa @ rs1 @ rsb)"
+| "RALTS [] h\<leadsto> RZERO"
+| "RALTS [r] h\<leadsto> r"
+| "a1 = a2 \<Longrightarrow> RALTS (rsa@[a1]@rsb@[a2]@rsc) h\<leadsto> RALTS (rsa @ [a1] @ rsb @ rsc)"
inductive
- hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ \<leadsto>* _" [100, 100] 100)
+ hrewrites:: "rrexp \<Rightarrow> rrexp \<Rightarrow> bool" ("_ h\<leadsto>* _" [100, 100] 100)
where
- rs1[intro, simp]:"r \<leadsto>* r"
-| rs2[intro]: "\<lbrakk>r1 \<leadsto>* r2; r2 \<leadsto> r3\<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
-
-
-lemma hr_in_rstar : "r1 \<leadsto> r2 \<Longrightarrow> r1 \<leadsto>* r2"
+ rs1[intro, simp]:"r h\<leadsto>* r"
+| rs2[intro]: "\<lbrakk>r1 h\<leadsto>* r2; r2 h\<leadsto> r3\<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
+
+
+lemma hr_in_rstar : "r1 h\<leadsto> r2 \<Longrightarrow> r1 h\<leadsto>* r2"
using hrewrites.intros(1) hrewrites.intros(2) by blast
lemma hreal_trans[trans]:
- assumes a1: "r1 \<leadsto>* r2" and a2: "r2 \<leadsto>* r3"
- shows "r1 \<leadsto>* r3"
+ assumes a1: "r1 h\<leadsto>* r2" and a2: "r2 h\<leadsto>* r3"
+ shows "r1 h\<leadsto>* r3"
using a2 a1
apply(induct r2 r3 arbitrary: r1 rule: hrewrites.induct)
apply(auto)
done
-lemma hmany_steps_later: "\<lbrakk>r1 \<leadsto> r2; r2 \<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 \<leadsto>* r3"
+lemma hmany_steps_later: "\<lbrakk>r1 h\<leadsto> r2; r2 h\<leadsto>* r3 \<rbrakk> \<Longrightarrow> r1 h\<leadsto>* r3"
by (meson hr_in_rstar hreal_trans)
lemma hrewrites_seq_context:
- shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r3"
+ shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r3"
apply(induct r1 r2 rule: hrewrites.induct)
apply simp
using hrewrite.intros(4) by blast
lemma hrewrites_seq_context2:
- shows "r1 \<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 \<leadsto>* RSEQ r0 r2"
+ shows "r1 h\<leadsto>* r2 \<Longrightarrow> RSEQ r0 r1 h\<leadsto>* RSEQ r0 r2"
apply(induct r1 r2 rule: hrewrites.induct)
apply simp
using hrewrite.intros(5) by blast
lemma hrewrites_seq_context0:
- shows "r1 \<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RZERO"
- apply(subgoal_tac "RSEQ r1 r3 \<leadsto>* RSEQ RZERO r3")
+ shows "r1 h\<leadsto>* RZERO \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RZERO"
+ apply(subgoal_tac "RSEQ r1 r3 h\<leadsto>* RSEQ RZERO r3")
using hrewrite.intros(1) apply blast
by (simp add: hrewrites_seq_context)
lemma hrewrites_seq_contexts:
- shows "\<lbrakk>r1 \<leadsto>* r2; r3 \<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 \<leadsto>* RSEQ r2 r4"
+ shows "\<lbrakk>r1 h\<leadsto>* r2; r3 h\<leadsto>* r4\<rbrakk> \<Longrightarrow> RSEQ r1 r3 h\<leadsto>* RSEQ r2 r4"
by (meson hreal_trans hrewrites_seq_context hrewrites_seq_context2)
@@ -1215,7 +1215,7 @@
-(*a more refined notion of \<leadsto>* is needed,
+(*a more refined notion of h\<leadsto>* is needed,
this lemma fails when rs1 contains some RALTS rs where elements
of rs appear in later parts of rs1, which will be picked up by rs2
and deduplicated*)
@@ -1546,11 +1546,11 @@
lemma grewrite_ralts:
- shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
+ shows "rs \<leadsto>g rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
by (smt (verit) grewrite_cases_middle hr_in_rstar hrewrite.intros(11) hrewrite.intros(7) hrewrite.intros(8))
lemma grewrites_ralts:
- shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* RALTS rs'"
+ shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* RALTS rs'"
apply(induct rule: grewrites.induct)
apply simp
using grewrite_ralts hreal_trans by blast
@@ -1558,8 +1558,8 @@
lemma distinct_grewrites_subgoal1:
shows "
- \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 \<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 \<leadsto>* rsimp_ALTs rs3"
- apply(subgoal_tac "RALTS rs1 \<leadsto>* RALTS rs3")
+ \<lbrakk>rs1 \<leadsto>g* [a]; RALTS rs1 h\<leadsto>* a; [a] \<leadsto>g rs3\<rbrakk> \<Longrightarrow> RALTS rs1 h\<leadsto>* rsimp_ALTs rs3"
+ apply(subgoal_tac "RALTS rs1 h\<leadsto>* RALTS rs3")
apply (metis hrewrite.intros(10) hrewrite.intros(9) rs2 rsimp_ALTs.cases rsimp_ALTs.simps(1) rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
apply(subgoal_tac "rs1 \<leadsto>g* rs3")
using grewrites_ralts apply blast
@@ -1571,7 +1571,7 @@
lemma grewrites_ralts_rsimpalts:
- shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs \<leadsto>* rsimp_ALTs rs' "
+ shows "rs \<leadsto>g* rs' \<Longrightarrow> RALTS rs h\<leadsto>* rsimp_ALTs rs' "
apply(induct rs rs' rule: grewrites.induct)
apply(case_tac rs)
using hrewrite.intros(9) apply force
@@ -1592,7 +1592,7 @@
by (metis (no_types, opaque_lifting) grewrite_ralts hr_in_rstar hreal_trans hrewrite.intros(10) neq_Nil_conv rsimp_ALTs.simps(2) rsimp_ALTs.simps(3))
lemma hrewrites_alts:
- shows " r \<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) \<leadsto>* (RALTS (rs1 @ [r'] @ rs2))"
+ shows " r h\<leadsto>* r' \<Longrightarrow> (RALTS (rs1 @ [r] @ rs2)) h\<leadsto>* (RALTS (rs1 @ [r'] @ rs2))"
apply(induct r r' rule: hrewrites.induct)
apply simp
using hrewrite.intros(6) by blast
@@ -1601,17 +1601,17 @@
srewritescf:: "rrexp list \<Rightarrow> rrexp list \<Rightarrow> bool" (" _ scf\<leadsto>* _" [100, 100] 100)
where
ss1: "[] scf\<leadsto>* []"
-| ss2: "\<lbrakk>r \<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
+| ss2: "\<lbrakk>r h\<leadsto>* r'; rs scf\<leadsto>* rs'\<rbrakk> \<Longrightarrow> (r#rs) scf\<leadsto>* (r'#rs')"
lemma hrewrites_alts_cons:
- shows " RALTS rs \<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) \<leadsto>* RALTS (r # rs')"
+ shows " RALTS rs h\<leadsto>* RALTS rs' \<Longrightarrow> RALTS (r # rs) h\<leadsto>* RALTS (r # rs')"
oops
-lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) \<leadsto>* (RALTS (rs@rs2))"
+lemma srewritescf_alt: "rs1 scf\<leadsto>* rs2 \<Longrightarrow> (RALTS (rs@rs1)) h\<leadsto>* (RALTS (rs@rs2))"
apply(induct rs1 rs2 arbitrary: rs rule: srewritescf.induct)
apply(rule rs1)
@@ -1626,7 +1626,7 @@
corollary srewritescf_alt1:
assumes "rs1 scf\<leadsto>* rs2"
- shows "RALTS rs1 \<leadsto>* RALTS rs2"
+ shows "RALTS rs1 h\<leadsto>* RALTS rs2"
using assms
by (metis append_Nil srewritescf_alt)
@@ -1634,7 +1634,7 @@
lemma trivialrsimp_srewrites:
- "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x \<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
+ "\<lbrakk>\<And>x. x \<in> set rs \<Longrightarrow> x h\<leadsto>* f x \<rbrakk> \<Longrightarrow> rs scf\<leadsto>* (map f rs)"
apply(induction rs)
apply simp
@@ -1643,15 +1643,15 @@
lemma hrewrites_list:
shows
-" (\<And>xa. xa \<in> set x \<Longrightarrow> xa \<leadsto>* rsimp xa) \<Longrightarrow> RALTS x \<leadsto>* RALTS (map rsimp x)"
+" (\<And>xa. xa \<in> set x \<Longrightarrow> xa h\<leadsto>* rsimp xa) \<Longrightarrow> RALTS x h\<leadsto>* RALTS (map rsimp x)"
apply(induct x)
apply(simp)+
by (simp add: srewritescf_alt1 ss2 trivialrsimp_srewrites)
-(* apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")*)
+(* apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")*)
lemma hrewrite_simpeq:
- shows "r1 \<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ shows "r1 h\<leadsto> r2 \<Longrightarrow> rsimp r1 = rsimp r2"
apply(induct rule: hrewrite.induct)
apply simp+
apply (simp add: basic_rsimp_SEQ_property3)
@@ -1668,7 +1668,7 @@
using grewrite.intros(4) grewrite_equal_rsimp by presburger
lemma hrewrites_simpeq:
- shows "r1 \<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
+ shows "r1 h\<leadsto>* r2 \<Longrightarrow> rsimp r1 = rsimp r2"
apply(induct rule: hrewrites.induct)
apply simp
apply(subgoal_tac "rsimp r2 = rsimp r3")
@@ -1678,13 +1678,13 @@
lemma simp_hrewrites:
- shows "r1 \<leadsto>* rsimp r1"
+ shows "r1 h\<leadsto>* rsimp r1"
apply(induct r1)
apply simp+
apply(case_tac "rsimp r11 = RONE")
apply simp
apply(subst basic_rsimp_SEQ_property1)
- apply(subgoal_tac "RSEQ r11 r12 \<leadsto>* RSEQ RONE r12")
+ apply(subgoal_tac "RSEQ r11 r12 h\<leadsto>* RSEQ RONE r12")
using hreal_trans hrewrite.intros(3) apply blast
using hrewrites_seq_context apply presburger
apply(case_tac "rsimp r11 = RZERO")
@@ -1698,8 +1698,8 @@
apply simp+
using hrewrites_seq_contexts apply presburger
apply simp
- apply(subgoal_tac "RALTS x \<leadsto>* RALTS (map rsimp x)")
- apply(subgoal_tac "RALTS (map rsimp x) \<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
+ apply(subgoal_tac "RALTS x h\<leadsto>* RALTS (map rsimp x)")
+ apply(subgoal_tac "RALTS (map rsimp x) h\<leadsto>* rsimp_ALTs (rdistinct (rflts (map rsimp x)) {}) ")
using hreal_trans apply blast
apply (meson flts_gstar greal_trans grewrites_ralts_rsimpalts gstar_rdistinct)
@@ -1707,9 +1707,9 @@
by simp
lemma interleave_aux1:
- shows " RALT (RSEQ RZERO r1) r \<leadsto>* r"
- apply(subgoal_tac "RSEQ RZERO r1 \<leadsto>* RZERO")
- apply(subgoal_tac "RALT (RSEQ RZERO r1) r \<leadsto>* RALT RZERO r")
+ shows " RALT (RSEQ RZERO r1) r h\<leadsto>* r"
+ apply(subgoal_tac "RSEQ RZERO r1 h\<leadsto>* RZERO")
+ apply(subgoal_tac "RALT (RSEQ RZERO r1) r h\<leadsto>* RALT RZERO r")
apply (meson grewrite.intros(1) grewrite_ralts hreal_trans hrewrite.intros(10) hrewrites.simps)
using rs1 srewritescf_alt1 ss1 ss2 apply presburger
by (simp add: hr_in_rstar hrewrite.intros(1))
@@ -1717,7 +1717,7 @@
lemma rnullable_hrewrite:
- shows "r1 \<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
+ shows "r1 h\<leadsto> r2 \<Longrightarrow> rnullable r1 = rnullable r2"
apply(induct rule: hrewrite.induct)
apply simp+
apply blast
@@ -1726,7 +1726,7 @@
lemma interleave1:
- shows "r \<leadsto> r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
+ shows "r h\<leadsto> r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
apply(induct r r' rule: hrewrite.induct)
apply (simp add: hr_in_rstar hrewrite.intros(1))
apply (metis (no_types, lifting) basic_rsimp_SEQ_property3 list.simps(8) list.simps(9) rder.simps(1) rder.simps(5) rdistinct.simps(1) rflts.simps(1) rflts.simps(2) rsimp.simps(1) rsimp.simps(2) rsimp.simps(3) rsimp_ALTs.simps(1) simp_hrewrites)
@@ -1758,7 +1758,7 @@
using hrewrite.intros(11) by auto
lemma interleave_star1:
- shows "r \<leadsto>* r' \<Longrightarrow> rder c r \<leadsto>* rder c r'"
+ shows "r h\<leadsto>* r' \<Longrightarrow> rder c r h\<leadsto>* rder c r'"
apply(induct rule : hrewrites.induct)
apply simp
by (meson hreal_trans interleave1)
@@ -1775,7 +1775,7 @@
using inside_simp_seq_nullable apply blast
apply simp
apply (smt (verit, del_insts) basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 der_simp_nullability rder.simps(1) rder.simps(5) rnullable.simps(2) rsimp.simps(1) rsimp_SEQ.simps(1) rsimp_idem)
- apply(subgoal_tac "rder x (RALTS xa) \<leadsto>* rder x (rsimp (RALTS xa))")
+ apply(subgoal_tac "rder x (RALTS xa) h\<leadsto>* rder x (rsimp (RALTS xa))")
using hrewrites_simpeq apply presburger
using interleave_star1 simp_hrewrites apply presburger
by simp
diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/ClosedFormsBounds.thy
--- a/thys2/ClosedFormsBounds.thy Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/ClosedFormsBounds.thy Tue Apr 19 09:08:01 2022 +0100
@@ -752,6 +752,7 @@
lemma rders_simp_bounded:
+ fixes "r"
shows "\<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
apply(induct r)
apply(rule_tac x = "Suc 0 " in exI)
@@ -767,9 +768,11 @@
apply (metis alts_closed_form_bounded size_list_estimation')
using star_closed_form_bounded by blast
+corollary rders_simp_finiteness:
+ shows "\<forall>r. \<exists>N. \<forall>s. rsize (rders_simp r s) \<le> N"
+ using rders_simp_bounded by auto
-unused_thms
end
diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/SizeBound3.thy
--- a/thys2/SizeBound3.thy Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/SizeBound3.thy Tue Apr 19 09:08:01 2022 +0100
@@ -1,6 +1,6 @@
theory SizeBound3
- imports "Lexer"
+ imports "ClosedFormsBounds"
begin
section \<open>Bit-Encodings\<close>
@@ -1160,17 +1160,1025 @@
using blexer_correctness main_blexer_simp by simp
+fun
+ rerase :: "arexp \<Rightarrow> rrexp"
+where
+ "rerase AZERO = RZERO"
+| "rerase (AONE _) = RONE"
+| "rerase (ACHAR _ c) = RCHAR c"
+| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
+| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
+| "rerase (ASTAR _ r) = RSTAR (rerase r)"
-export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers
+
+
+lemma asize_rsize:
+ shows "rsize (rerase r) = asize r"
+ apply(induct r)
+ apply simp+
+
+ apply (metis (mono_tags, lifting) comp_apply map_eq_conv)
+ by simp
+
+lemma rb_nullability:
+ shows " rnullable (rerase a) = bnullable a"
+ apply(induct a)
+ apply simp+
+ done
+
+lemma fuse_anything_doesnt_matter:
+ shows "rerase a = rerase (fuse bs a)"
+ by (smt (verit) fuse.elims rerase.simps(2) rerase.simps(3) rerase.simps(4) rerase.simps(5) rerase.simps(6))
+
+
+lemma rerase_preimage:
+ shows "rerase r = RZERO \<Longrightarrow> r = AZERO"
+ apply(case_tac r)
+ apply simp+
+ done
+
+lemma rerase_preimage2:
+ shows "rerase r = RONE \<Longrightarrow> \<exists>bs. r = AONE bs"
+ apply(case_tac r)
+ apply simp+
+ done
+
+lemma rerase_preimage3:
+ shows "rerase r= RCHAR c \<Longrightarrow> \<exists>bs. r = ACHAR bs c"
+ apply(case_tac r)
+ apply simp+
+ done
+
+lemma rerase_preimage4:
+ shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2"
+ apply(case_tac r)
+ apply(simp)+
+ done
+
+lemma rerase_preimage5:
+ shows "rerase r = RALTS rs \<Longrightarrow> \<exists>bs as. r = AALTs bs as \<and> map rerase as = rs"
+ apply(case_tac r)
+ apply(simp)+
+ done
+
+lemma rerase_preimage6:
+ shows "rerase r = RSTAR r0 \<Longrightarrow> \<exists>bs a0. r = ASTAR bs a0 \<and> rerase a0 = r0 "
+ apply(case_tac r)
+ apply(simp)+
+ done
+
+lemma map_rder_bder:
+ shows "\<lbrakk> \<And>xa a. \<lbrakk>xa \<in> set x; rerase a = xa\<rbrakk> \<Longrightarrow> rerase (bder c a) = rder c xa;
+ map rerase as = x\<rbrakk> \<Longrightarrow>
+ map rerase (map (bder c) as) = map (rder c) x"
+ apply(induct x arbitrary: as)
+ apply simp+
+ by force
-unused_thms
+lemma der_rerase:
+ shows "rerase a = r \<Longrightarrow> rerase (bder c a) = rder c r"
+ apply(induct r arbitrary: a)
+ apply simp
+ using rerase_preimage apply fastforce
+ using rerase_preimage2 apply force
+ apply (metis bder.simps(3) rder.simps(3) rerase.simps(1) rerase.simps(2) rerase_preimage3)
+ apply(insert rerase_preimage4)[1]
+ apply(subgoal_tac " \<exists>bs a1 a2. a = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2")
+ prefer 2
+ apply presburger
+ apply(erule exE)+
+ apply(erule conjE)+
+ apply(subgoal_tac " rerase (bder c a1) = rder c r1")
+ prefer 2
+ apply blast
+ apply(subgoal_tac " rerase (bder c a2) = rder c r2")
+ prefer 2
+ apply blast
+ apply(case_tac "rnullable r1")
+ apply(subgoal_tac "bnullable a1")
+ apply simp
+ using fuse_anything_doesnt_matter apply presburger
+ using rb_nullability apply blast
+ apply (metis bder.simps(5) rb_nullability rder.simps(5) rerase.simps(5))
+ apply simp
+ apply(insert rerase_preimage5)[1]
+ apply(subgoal_tac "\<exists>bs as. a = AALTs bs as \<and> map rerase as = x")
+ prefer 2
+
+ apply blast
+ apply(erule exE)+
+ apply(erule conjE)+
+ apply(subgoal_tac "map rerase (map (bder c) as) = map (rder c) x")
+ using bder.simps(4) rerase.simps(4) apply presburger
+ using map_rder_bder apply blast
+ using fuse_anything_doesnt_matter rerase_preimage6 by force
+
+lemma der_rerase2:
+ shows "rerase (bder c a) = rder c (rerase a)"
+ using der_rerase by force
+
+lemma ders_rerase:
+ shows "rerase (bders a s) = rders (rerase a) s"
+ apply(induct s rule: rev_induct)
+ apply simp
+ by (simp add: bders_append der_rerase rders_append)
+
+lemma rerase_bsimp_ASEQ:
+ shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)"
+ by (smt (verit, ccfv_SIG) SizeBound3.bsimp_ASEQ0 SizeBound3.bsimp_ASEQ2 basic_rsimp_SEQ_property1 basic_rsimp_SEQ_property2 basic_rsimp_SEQ_property3 bsimp_ASEQ.simps(1) bsimp_ASEQ1 fuse_anything_doesnt_matter rerase.simps(1) rerase.simps(2) rerase.simps(5) rerase_preimage rerase_preimage2 rsimp_SEQ.simps(1))
+
+lemma rerase_bsimp_AALTs:
+ shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)"
+ apply(induct rs arbitrary: bs)
+ apply simp+
+ by (smt (verit, ccfv_threshold) Cons_eq_map_conv bsimp_AALTs.elims fuse_anything_doesnt_matter list.discI list.inject list.simps(9) rerase.simps(4) rsimp_ALTs.elims)
+
+
+fun anonalt :: "arexp \<Rightarrow> bool"
+ where
+ "anonalt (AALTs bs2 rs) = False"
+| "anonalt r = True"
+
+
+fun agood :: "arexp \<Rightarrow> bool" where
+ "agood AZERO = False"
+| "agood (AONE cs) = True"
+| "agood (ACHAR cs c) = True"
+| "agood (AALTs cs []) = False"
+| "agood (AALTs cs [r]) = False"
+| "agood (AALTs cs (r1#r2#rs)) = (distinct (map erase (r1 # r2 # rs)) \<and>(\<forall>r' \<in> set (r1#r2#rs). agood r' \<and> anonalt r'))"
+| "agood (ASEQ _ AZERO _) = False"
+| "agood (ASEQ _ (AONE _) _) = False"
+| "agood (ASEQ _ _ AZERO) = False"
+| "agood (ASEQ cs r1 r2) = (agood r1 \<and> agood r2)"
+| "agood (ASTAR cs r) = True"
+
+
+fun anonnested :: "arexp \<Rightarrow> bool"
+ where
+ "anonnested (AALTs bs2 []) = True"
+| "anonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
+| "anonnested (AALTs bs2 (r # rs2)) = anonnested (AALTs bs2 rs2)"
+| "anonnested r = True"
-inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99)
- where
- "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) "
+lemma k0:
+ shows "flts (r # rs1) = flts [r] @ flts rs1"
+ apply(induct r arbitrary: rs1)
+ apply(auto)
+ done
+
+lemma k00:
+ shows "flts (rs1 @ rs2) = flts rs1 @ flts rs2"
+ apply(induct rs1 arbitrary: rs2)
+ apply(auto)
+ by (metis append.assoc k0)
+
+
+lemma bbbbs:
+ assumes "agood r" "r = AALTs bs1 rs"
+ shows "bsimp_AALTs bs (flts [r]) = AALTs bs (map (fuse bs1) rs)"
+ using assms
+ by (smt (verit, ccfv_SIG) Cons_eq_map_conv agood.simps(4) agood.simps(5) append.right_neutral bsimp_AALTs.elims flts.simps(1) flts.simps(3) list.map_disc_iff)
+
+lemma bbbbs1:
+ shows "anonalt r \<or> (\<exists>bs rs. r = AALTs bs rs)"
+ by (meson anonalt.elims(3))
+
+
+
+lemma good_fuse:
+ shows "agood (fuse bs r) = agood r"
+ apply(induct r arbitrary: bs)
+ apply(auto)
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac x2a)
+ apply(simp_all)
+ apply(case_tac list)
+ apply(simp_all)
+ apply(case_tac x2a)
+ apply(simp_all)
+ apply(case_tac list)
+ apply(simp_all)
+ done
+
+lemma good0:
+ assumes "rs \<noteq> Nil" "\<forall>r \<in> set rs. anonalt r" "distinct (map erase rs)"
+ shows "agood (bsimp_AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. agood r)"
+ using assms
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply simp+
+ apply (simp add: good_fuse)
+ apply(subgoal_tac "bsimp_AALTs bs1 (v # vb # vc) = AALTs bs1 (v # vb # vc)")
+ prefer 2
+
+
+ using bsimp_AALTs.simps(3) apply presburger
+ apply(simp only:)
+ apply(subgoal_tac "agood (AALTs bs1 (v # vb # vc)) = ((\<forall>r \<in> (set (v # vb # vc)). agood r \<and> anonalt r) \<and> distinct (map erase (v # vb # vc)))")
+ prefer 2
+ using agood.simps(6) apply blast
+ apply(simp only:)
+ apply(subgoal_tac "((\<forall>r\<in>set (v # vb # vc). agood r \<and> anonalt r) \<and> distinct (map erase (v # vb # vc))) = ((\<forall>r\<in>set (v # vb # vc). agood r) \<and> distinct (map erase (v # vb # vc)))")
+ prefer 2
+ apply blast
+ apply(simp only:)
+ apply(subgoal_tac "((\<forall>r \<in> set (v # vb # vc). agood r) \<and> distinct (map erase (v # vb # vc))) = (\<forall> r \<in> set (v # vb # vc). agood r) ")
+ prefer 2
+ apply(subgoal_tac "distinct (map erase (v # vb # vc)) = True")
+ prefer 2
+ apply blast
+ prefer 2
+ apply force
+ apply simp
+ done
+
+
+lemma nn11a:
+ assumes "anonalt r"
+ shows "anonalt (fuse bs r)"
+ using assms
+ apply(induct r)
+ apply(auto)
+ done
+
+lemma flts0:
+ assumes "r \<noteq> AZERO" "anonalt r"
+ shows "flts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ done
+
+lemma flts1:
+ assumes "agood r"
+ shows "flts [r] \<noteq> []"
+ using assms
+ apply(induct r)
+ apply(simp_all)
+ apply(case_tac x2a)
+ apply(simp)
+ apply(simp)
+ done
+
+lemma flts2:
+ assumes "agood r"
+ shows "\<forall>r' \<in> set (flts [r]). agood r' \<and> anonalt r'"
+ using assms
+ apply(induct r)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 2
+ apply(simp)
+ apply(auto)[1]
+ apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) good_fuse)
+ apply (metis bsimp_AALTs.elims agood.simps(4) agood.simps(5) agood.simps(6) nn11a)
+ apply fastforce
+ apply(simp)
+ done
+
+
+lemma flts3:
+ assumes "\<forall>r \<in> set rs. agood r \<or> r = AZERO"
+ shows "\<forall>r \<in> set (flts rs). agood r"
+ using assms
+ apply(induct rs arbitrary: rule: flts.induct)
+ apply(simp_all)
+ by (metis SizeBound3.flts2 UnE append.right_neutral flts.simps(1) flts.simps(3) list.set_map)
+
+
+lemma flts3b:
+ assumes "\<exists>r\<in>set rs. agood r"
+ shows "flts rs \<noteq> []"
+ using assms
+ apply(induct rs arbitrary: rule: flts.induct)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ apply(auto)
+ done
+
+lemma k0a:
+ shows "flts [AALTs bs rs] = map (fuse bs) rs"
+ apply(simp)
+ done
+
+
+lemma k0b:
+ assumes "anonalt r" "r \<noteq> AZERO"
+ shows "flts [r] = [r]"
+ using assms
+ apply(case_tac r)
+ apply(simp_all)
+ done
+
+lemma flts4_nogood:
+ shows "bsimp_AALTs bs0 rs = AZERO \<Longrightarrow> \<forall>r \<in> set rs. \<not> agood r"
+ by (metis SizeBound3.flts3b arexp.distinct(7) bsimp_AALTs.elims flts.simps(1) flts.simps(2) fuse_anything_doesnt_matter rerase.simps(1) rerase_preimage)
+
+lemma flts4_append:
+ shows "bsimp_AALTs bs0 (rs @ flts rsa) = AZERO \<Longrightarrow> bsimp_AALTs bs0 rs = AZERO"
+ by (metis append_is_Nil_conv arexp.simps(13) bsimp_AALTs.elims bsimp_AALTs.simps(1) butlast_append butlast_snoc)
+
+lemma flts4:
+ assumes "bsimp_AALTs bs (flts rs) = AZERO"
+ shows "\<forall>r \<in> set rs. \<not> agood r"
+ using assms
+ apply(induct rs arbitrary: bs rule: flts.induct)
+ apply(auto)
+ defer
+ apply (metis (no_types, lifting) Nil_is_append_conv append_self_conv2 bsimp_AALTs.elims butlast.simps(2) butlast_append flts3b anonalt.simps(1) anonalt.simps(2))
+ apply (metis agood.simps(1) agood.simps(2) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject)
+ apply (metis agood.simps(1) agood.simps(3) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.distinct(1) list.inject)
+ apply (metis agood.simps(1) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject)
+ apply (metis arexp.distinct(7) bsimp_AALTs.elims list.distinct(1) list.inject)
+ apply (metis agood.simps(1) agood.simps(33) arexp.distinct(7) bsimp_AALTs.elims good_fuse list.discI list.inject)
+ by (metis SizeBound3.bbbbs SizeBound3.k0a arexp.simps(13) flts4_append)
+
+
+lemma flts_nil:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ agood (bsimp y) \<or> bsimp y = AZERO"
+ and "\<forall>r\<in>set rs. \<not> agood (bsimp r)"
+ shows "flts (map bsimp rs) = []"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ by force
+
+lemma flts_nil2:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow>
+ agood (bsimp y) \<or> bsimp y = AZERO"
+ and "bsimp_AALTs bs (flts (map bsimp rs)) = AZERO"
+ shows "flts (map bsimp rs) = []"
+ using assms
+ apply(induct rs arbitrary: bs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(simp)
+ apply(subst (asm) k0)
+ apply(auto)
+ apply (metis flts.simps(1) flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+ by (metis flts.simps(2) flts4 k0 less_add_Suc1 list.set_intros(1))
+
+
+
+lemma good_SEQ:
+ assumes "r1 \<noteq> AZERO" "r2 \<noteq> AZERO" "\<forall>bs. r1 \<noteq> AONE bs"
+ shows "agood (ASEQ bs r1 r2) = (agood r1 \<and> agood r2)"
+ using assms
+ apply(case_tac r1)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ apply(case_tac r2)
+ apply(simp_all)
+ done
+
+lemma asize0:
+ shows "0 < asize r"
+ apply(induct r)
+ apply(auto)
+ done
+
+lemma nn1qq:
+ assumes "anonnested (AALTs bs rs)"
+ shows "\<nexists>bs1 rs1. AALTs bs1 rs1 \<in> set rs"
+ using assms
+ apply(induct rs rule: flts.induct)
+ apply(auto)
+ done
+
+lemma nn1c:
+ assumes "\<forall>r \<in> set rs. anonnested r"
+ shows "\<forall>r \<in> set (flts rs). anonalt r"
+ using assms
+ apply(induct rs rule: flts.induct)
+ apply(auto)
+ apply(rule nn11a)
+ by (metis nn1qq anonalt.elims(3))
+
+lemma n0:
+ shows "anonnested (AALTs bs rs) \<longleftrightarrow> (\<forall>r \<in> set rs. anonalt r)"
+ apply(induct rs arbitrary: bs)
+ apply(auto)
+ apply (metis SizeBound3.nn1qq anonalt.elims(3) list.set_intros(1))
+ apply (metis SizeBound3.bbbbs1 SizeBound3.nn1qq list.set_intros(2))
+ by (metis anonalt.elims(2) anonnested.simps(3) anonnested.simps(4) anonnested.simps(5) anonnested.simps(6) anonnested.simps(7))
+
+
+
+lemma nn1bb:
+ assumes "\<forall>r \<in> set rs. anonalt r"
+ shows "anonnested (bsimp_AALTs bs rs)"
+ using assms
+ apply(induct bs rs rule: bsimp_AALTs.induct)
+ apply(auto)
+ apply (metis nn11a anonalt.simps(1) anonnested.elims(3))
+ using n0 by auto
+
+lemma nn10:
+ assumes "anonnested (AALTs cs rs)"
+ shows "anonnested (AALTs (bs @ cs) rs)"
+ using assms
+ apply(induct rs arbitrary: cs bs)
+ apply(simp_all)
+ apply(case_tac a)
+ apply(simp_all)
+ done
+
+lemma nn1a:
+ assumes "anonnested r"
+ shows "anonnested (fuse bs r)"
+ using assms
+ apply(induct bs r arbitrary: rule: fuse.induct)
+ apply(simp_all add: nn10)
+ done
+
+lemma dB_keeps_property:
+ shows "(\<forall>r \<in> set rs. P r) \<longrightarrow> (\<forall>r \<in> set (distinctBy rs erase rset). P r)"
+ apply(induct rs arbitrary: rset)
+ apply simp+
+ done
+
+lemma dB_filters_out:
+ shows "erase a \<in> rset \<Longrightarrow> a \<notin> set (distinctBy rs erase (rset))"
+ apply(induct rs arbitrary: rset)
+ apply simp
+ apply(case_tac "a = aa")
+ apply simp+
+ done
+
+lemma dB_will_be_distinct:
+ shows "distinct (distinctBy rs erase (insert (erase a) rset)) \<Longrightarrow> distinct (a # (distinctBy rs erase (insert (erase a) rset)))"
+ using dB_filters_out by force
+
+
+
+lemma dB_does_the_job2:
+ shows "distinct (distinctBy rs erase rset)"
+ apply(induct rs arbitrary: rset)
+ apply simp
+ apply(case_tac "erase a \<in> rset")
+ apply simp
+ apply(drule_tac x = "insert (erase a) rset" in meta_spec)
+ apply(subgoal_tac "distinctBy (a # rs) erase rset = a # distinctBy rs erase (insert (erase a ) rset)")
+ apply(simp only:)
+ using dB_will_be_distinct apply presburger
+ by auto
+
+lemma dB_does_more_job:
+ shows "distinct (map erase (distinctBy rs erase rset))"
+ apply(induct rs arbitrary:rset)
+ apply simp
+ apply(case_tac "erase a \<in> rset")
+ apply simp+
+ using dB_filters_out by force
+
+lemma dB_mono2:
+ shows "rset \<subseteq> rset' \<Longrightarrow> distinctBy rs erase rset = [] \<Longrightarrow> distinctBy rs erase rset' = []"
+ apply(induct rs arbitrary: rset rset')
+ apply simp+
+ by (meson in_mono list.discI)
+
+
+lemma nn1b:
+ shows "anonnested (bsimp r)"
+ apply(induct r)
+ apply(simp_all)
+ apply(case_tac "bsimp r1 = AZERO")
+ apply(simp)
+ apply(case_tac "bsimp r2 = AZERO")
+ apply(simp)
+ apply(case_tac "\<exists>bs. bsimp r1 = AONE bs")
+ apply(auto)[1]
+ apply (simp add: nn1a)
+ apply(subst bsimp_ASEQ1)
+ apply(auto)
+ apply(rule nn1bb)
+ apply(auto)
+ apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r")
+ prefer 2
+ apply (metis (mono_tags, lifting) SizeBound3.nn1c image_iff list.set_map)
+ apply(subgoal_tac "\<forall>r \<in> set (distinctBy (flts (map bsimp x2a)) erase {}). anonalt r")
+ prefer 2
+ using dB_keeps_property apply presburger
+ by blast
+
+
+lemma induct_smaller_elem_list:
+ shows "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))"
+ apply(induct list)
+ apply simp+
+ by fastforce
+
+lemma no0s_fltsbsimp:
+ shows "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO"
+ oops
+
+lemma flts_all0s:
+ shows "\<forall>r \<in> set rs. r = AZERO \<Longrightarrow> flts rs = []"
+ apply(induct rs)
+ apply simp+
+ done
+
+
+
+
+
+lemma good1:
+ shows "agood (bsimp a) \<or> bsimp a = AZERO"
+ apply(induct a taking: asize rule: measure_induct)
+ apply(case_tac x)
+ apply(simp)
+ apply(simp)
+ apply(simp)
+ prefer 3
+ apply(simp)
+ prefer 2
+ (* AALTs case *)
+ apply(simp only:)
+ apply(case_tac "x52")
+ apply(simp)
+ (* AALTs list at least one - case *)
+ apply(simp only: )
+ apply(frule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ (* either first element is agood, or AZERO *)
+ apply(erule disjE)
+ prefer 2
+ apply(simp)
+ (* in the AZERO case, the size is smaller *)
+ apply(drule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(subst (asm) bsimp.simps)
+ apply(subst (asm) bsimp.simps)
+ apply(assumption)
+ (* in the agood case *)
+ apply(frule_tac x="AALTs x51 list" in spec)
+ apply(drule mp)
+ apply(simp add: asize0)
+ apply(erule disjE)
+ apply(rule disjI1)
+ apply(simp add: good0)
+ apply(subst good0)
+ using SizeBound3.flts3b distinctBy.elims apply force
+ apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)))) anonalt")
+ prefer 2
+ apply (metis Cons_eq_map_conv SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
+ using dB_keeps_property apply presburger
+ using dB_does_more_job apply presburger
+ apply(subgoal_tac " Ball (set ( (flts (bsimp a # map bsimp list)) )) agood")
+ using dB_keeps_property apply presburger
+ apply(subgoal_tac "\<forall>r \<in> (set (bsimp a # map bsimp list)). (agood r) \<or> (r = AZERO)")
+ using SizeBound3.flts3 apply blast
+
+ apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (asize a + sum_list (map asize list))")
+
+ apply simp
+
+ apply(subgoal_tac "\<forall>r \<in> set list. asize r < Suc (sum_list (map asize list))")
+
+ apply fastforce
+ using induct_smaller_elem_list apply blast
+
+
+
+
+ apply simp
+ apply(subgoal_tac "agood (bsimp a)")
+ prefer 2
+ apply blast
+ apply(subgoal_tac "\<forall>r \<in> (set (map bsimp list)). r = AZERO \<or> agood r")
+ prefer 2
+ apply (metis add_Suc_right image_iff induct_smaller_elem_list list.set_map trans_less_add2)
+ apply(subgoal_tac "\<not>(\<exists> r\<in>set (map bsimp list). agood r)")
+ prefer 2
+ apply (metis SizeBound3.flts3 SizeBound3.flts3b distinctBy.elims empty_iff flts4_nogood list.set_intros(1))
+ apply(subgoal_tac "\<forall>r \<in> set (map bsimp list). r = AZERO")
+ prefer 2
+ apply blast
+ apply(subgoal_tac "flts (map bsimp list) = []")
+ prefer 2
+ using flts_all0s apply presburger
+ apply (smt (verit, del_insts) SizeBound3.flts2 SizeBound3.good0 SizeBound3.k0 dB_does_more_job dB_keeps_property distinctBy.simps(1) flts.simps(1))
+ apply(subgoal_tac "agood (bsimp x42) \<or> bsimp x42 = AZERO")
+ apply(subgoal_tac "agood (bsimp x43) \<or> bsimp x43 = AZERO")
+ apply(case_tac "bsimp x42 = AZERO")
+ apply simp
+ apply(case_tac "bsimp x43 = AZERO")
+ apply simp
+ apply(case_tac "\<exists>bs'. bsimp x42 = AONE bs'")
+ apply(erule exE)
+ apply simp
+ using good_fuse apply presburger
+ apply simp
+ apply(subgoal_tac "bsimp_ASEQ x41 (bsimp x42) (bsimp x43) = ASEQ x41 (bsimp x42) (bsimp x43)")
+ prefer 2
+ using bsimp_ASEQ1 apply presburger
+ using SizeBound3.good_SEQ apply presburger
+ using asize.simps(5) less_add_Suc2 apply presburger
+ by simp
+
+
+
+
+
+
+lemma good1a:
+ assumes "L (erase a) \<noteq> {}"
+ shows "agood (bsimp a)"
+ using good1 assms
+ using L_bsimp_erase by force
+
+
+
+lemma flts_append:
+ "flts (xs1 @ xs2) = flts xs1 @ flts xs2"
+ apply(induct xs1 arbitrary: xs2 rule: rev_induct)
+ apply(auto)
+ apply(case_tac xs)
+ apply(auto)
+ apply(case_tac x)
+ apply(auto)
+ apply(case_tac x)
+ apply(auto)
+ done
+
+lemma g1:
+ assumes "agood (bsimp_AALTs bs rs)"
+ shows "bsimp_AALTs bs rs = AALTs bs rs \<or> (\<exists>r. rs = [r] \<and> bsimp_AALTs bs [r] = fuse bs r)"
+using assms
+ apply(induct rs arbitrary: bs)
+ apply(simp)
+ apply(case_tac rs)
+ apply(simp only:)
+ apply(simp)
+ apply(case_tac list)
+ apply(simp)
+ by simp
+
+lemma flts_0:
+ assumes "anonnested (AALTs bs rs)"
+ shows "\<forall>r \<in> set (flts rs). r \<noteq> AZERO"
+ using assms
+ apply(induct rs arbitrary: bs rule: flts.induct)
+ apply(simp)
+ apply(simp)
+ defer
+ apply(simp)
+ apply(simp)
+ apply(simp)
+apply(simp)
+ apply(rule ballI)
+ apply(simp)
+ done
+
+lemma flts_0a:
+ assumes "anonnested (AALTs bs rs)"
+ shows "AZERO \<notin> set (flts rs)"
+ using assms
+ using flts_0 by blast
+
+lemma qqq1:
+ shows "AZERO \<notin> set (flts (map bsimp rs))"
+ by (metis ex_map_conv flts3 agood.simps(1) good1)
+
+
+fun nonazero :: "arexp \<Rightarrow> bool"
+ where
+ "nonazero AZERO = False"
+| "nonazero r = True"
+
+lemma flts_concat:
+ shows "flts rs = concat (map (\<lambda>r. flts [r]) rs)"
+ apply(induct rs)
+ apply(auto)
+ apply(subst k0)
+ apply(simp)
+ done
+
+lemma flts_single1:
+ assumes "anonalt r" "nonazero r"
+ shows "flts [r] = [r]"
+ using assms
+ apply(induct r)
+ apply(auto)
+ done
+
+lemma flts_qq:
+ assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> agood y \<longrightarrow> bsimp y = y"
+ "\<forall>r'\<in>set rs. agood r' \<and> anonalt r'"
+ shows "flts (map bsimp rs) = rs"
+ using assms
+ apply(induct rs)
+ apply(simp)
+ apply(simp)
+ apply(subst k0)
+ apply(subgoal_tac "flts [bsimp a] = [a]")
+ prefer 2
+ apply(drule_tac x="a" in spec)
+ apply(drule mp)
+ apply(simp)
+ apply(auto)[1]
+ using agood.simps(1) k0b apply blast
+ apply(auto)[1]
+ done
+
+lemma test:
+ assumes "agood r"
+ shows "bsimp r = r"
+ using assms
+ apply(induct r taking: "asize" rule: measure_induct)
+ apply(erule agood.elims)
+ apply(simp_all)
+ apply(subst k0)
+ apply(subst (2) k0)
+ apply(subst flts_qq)
+ apply(auto)[1]
+ apply(auto)[1]
+ oops
+
+
+
+lemma bsimp_idem:
+ shows "bsimp (bsimp r) = bsimp r"
+ using test good1
+ oops
+
+
+lemma erase_preimage1:
+ assumes "anonalt r"
+ shows "erase r = ONE \<Longrightarrow> \<exists>bs. r = AONE bs"
+ apply(case_tac r)
+ apply simp+
+ using anonalt.simps(1) assms apply presburger
+ by fastforce
+
+lemma erase_preimage_char:
+ assumes "anonalt r"
+ shows "erase r = CH c \<Longrightarrow> \<exists>bs. r = ACHAR bs c"
+ apply(case_tac r)
+ apply simp+
+ using assms apply fastforce
+ by simp
+
+lemma erase_preimage_seq:
+ assumes "anonalt r"
+ shows "erase r = SEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> erase a1 = r1 \<and> erase a2 = r2"
+ apply(case_tac r)
+ apply simp+
+ using assms apply fastforce
+ by simp
+
+lemma rerase_preimage_seq:
+ assumes "anonalt r"
+ shows "rerase r = RSEQ r1 r2 \<Longrightarrow> \<exists>bs a1 a2. r = ASEQ bs a1 a2 \<and> rerase a1 = r1 \<and> rerase a2 = r2 "
+ using rerase_preimage4 by presburger
+
+lemma seq_recursive_equality:
+ shows "\<lbrakk>r1 = a1; r2 = a2\<rbrakk> \<Longrightarrow> SEQ r1 r2 = SEQ a1 a2"
+ by meson
+
+lemma almost_identical_image:
+ assumes "agood r" "\<forall>r \<in> rset. agood r"
+ shows "erase r \<in> erase ` rset \<Longrightarrow> \<exists>r' \<in> rset. erase r' = erase r"
+ by auto
+
+lemma goodalts_never_change:
+ assumes "r = AALTs bs rs" "agood r"
+ shows "\<exists>r1 r2. erase r = ALT r1 r2"
+ by (metis agood.simps(4) agood.simps(5) assms(1) assms(2) bmkepss.cases erase.simps(6))
+
+
+fun shape_preserving :: "arexp \<Rightarrow> bool" where
+ "shape_preserving AZERO = True"
+| "shape_preserving (AONE bs) = True"
+| "shape_preserving (ACHAR bs c) = True"
+| "shape_preserving (AALTs bs []) = False"
+| "shape_preserving (AALTs bs [a]) = False"
+| "shape_preserving (AALTs bs (a1 # a2 # rs)) = (\<forall>r \<in> set (a1 # a2 # rs). shape_preserving r)"
+| "shape_preserving (ASEQ bs r1 r2) = (shape_preserving r1 \<and> shape_preserving r2)"
+| "shape_preserving (ASTAR bs r) = shape_preserving r"
+
+
+lemma good_shape_preserving:
+ assumes "\<nexists>bs r0. r = ASTAR bs r0"
+ shows "agood r \<Longrightarrow> shape_preserving r"
+ using assms
+
+ apply(induct r)
+ prefer 6
+
+ apply blast
+ apply simp
+
+ oops
+
+
+
+
+
+lemma shadow_arexp_rerase_erase:
+ shows "\<lbrakk>agood r; agood r'; erase r = erase r'\<rbrakk> \<Longrightarrow> rerase r = rerase r'"
+ apply(induct r )
+ apply simp
+ apply(induct r')
+ apply simp+
+ apply (metis goodalts_never_change rexp.distinct(15))
+ apply simp+
+ apply (metis anonalt.elims(3) erase_preimage_char goodalts_never_change rerase.simps(3) rexp.distinct(21))
+ apply(induct r')
+ apply simp
+ apply simp
+ apply simp
+ apply(subgoal_tac "agood r1")
+ prefer 2
+ apply (metis SizeBound3.good_SEQ agood.simps(10) agood.simps(11) agood.simps(2) agood.simps(3) agood.simps(33) agood.simps(7) bsimp.cases)
+ apply(subgoal_tac "agood r2")
+ apply(subgoal_tac "agood r'1")
+ apply(subgoal_tac "agood r'2")
+ apply(subgoal_tac "rerase r'1 = rerase r1")
+ apply(subgoal_tac "rerase r'2 = rerase r2")
+
+ using rerase.simps(5) apply presburger
+ sledgehammer
+
+
+lemma rerase_erase_good:
+ assumes "agood r" "\<forall>r \<in> rset. agood r"
+ shows "erase r \<in> erase ` rset \<Longrightarrow> rerase r \<in> rerase ` rset"
+ using assms
+ apply(case_tac r)
+ apply simp+
+ oops
+
+lemma rerase_erase_both:
+ assumes "\<forall>r \<in> rset. agood r" "agood r"
+ shows "(rerase r \<in> (rerase ` rset)) \<longleftrightarrow> (erase r \<in> (erase ` rset))"
+ using assms
+ apply(induct r )
+ apply force
+ apply simp
+ apply(case_tac "RONE \<in> rerase ` rset")
+ apply(subgoal_tac "\<exists>bs. (AONE bs) \<in> rset")
+ apply (metis erase.simps(2) rev_image_eqI)
+ apply (metis image_iff rerase_preimage2)
+ apply(subgoal_tac "\<nexists>bs. (AONE bs) \<in> rset")
+ apply(subgoal_tac "ONE \<notin> erase ` rset")
+
+ apply blast
+ sledgehammer
+ apply (metis erase_preimage1 image_iff)
+ apply (metis rerase.simps(2) rev_image_eqI)
+ apply (smt (verit, best) erase.simps(3) erase_preimage_char image_iff rerase.simps(3) rerase_preimage3)
+(* apply simp
+ apply(subgoal_tac "(RSEQ (rerase r1) (rerase r2) \<in> rerase ` rset) \<Longrightarrow> (SEQ (erase r1) (erase r2) \<in> erase ` rset)")
+ prefer 2
+ apply(subgoal_tac "\<exists>bs a1 a2. (ASEQ bs a1 a2) \<in> rset \<and> rerase a1 = rerase r1 \<and> rerase a2 = rerase r2")
+ prefer 2
+ apply (metis (full_types) image_iff rerase_preimage4)
+ apply(erule exE)+
+ apply(subgoal_tac "erase (ASEQ bs a1 a2) \<in> (erase ` rset) ")
+ apply(subgoal_tac "SEQ (erase a1) (erase a2) \<in> (erase ` rset)")
+ apply(subgoal_tac "SEQ (erase a1) (erase a2) = SEQ (erase r1) (erase r2)")
+ apply metis
+ apply(erule conjE)+*)
+ apply(drule_tac x = "rset" in meta_spec)+
+
+
+
+
+ oops
+
+
+lemma rerase_pushin1_general:
+ assumes "\<forall>r \<in> set rs. agood r"
+ shows "map rerase (distinctBy rs erase (erase ` rset)) = rdistinct (map rerase rs) (rerase ` rset)"
+ apply(induct rs arbitrary: rset)
+ apply simp+
+ apply(case_tac "erase a \<in> erase ` rset")
+ apply simp
+
+
+
+ oops
+
+lemma rerase_erase:
+ assumes "\<forall>r \<in> set as. agood r \<and> anonalt r"
+ shows "rdistinct (map rerase as) (rerase ` rset) = map rerase (distinctBy as erase (erase ` rset))"
+ using assms
+ apply(induct as)
+ apply simp+
+
+ sorry
+
+
+lemma rerase_pushin1:
+ assumes "\<forall>r \<in> set rs. anonalt r \<and> agood r"
+ shows "map rerase (distinctBy rs erase {}) = rdistinct (map rerase rs) {}"
+ apply(insert rerase_erase)
+ by (metis assms image_empty)
+
+
+
+
+
+
+
+lemma nonalt_flts : shows
+ "\<forall>r \<in> set (flts (map bsimp rs)). r \<noteq> AZERO"
+ using SizeBound3.qqq1 by force
+
+
+
+
+lemma rerase_list_ders:
+ shows "\<And>x1 x2a.
+ (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> rerase (bsimp x2aa) = rsimp (rerase x2aa)) \<Longrightarrow>
+ (map rerase (distinctBy (flts (map bsimp x2a)) erase {})) = (rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {})"
+ apply(subgoal_tac "\<forall>r \<in> set (flts (map bsimp x2a)). anonalt r ")
+ prefer 2
+ apply (metis SizeBound3.nn1b SizeBound3.nn1c ex_map_conv)
+ sledgehammer
+
+ sorry
+
+
+lemma simp_rerase:
+ shows "rerase (bsimp a) = rsimp (rerase a)"
+ apply(induct a)
+ apply simp+
+ using rerase_bsimp_ASEQ apply presburger
+ apply simp
+ apply(subst rerase_bsimp_AALTs)
+ apply(subgoal_tac "map rerase (distinctBy (flts (map bsimp x2a)) erase {}) = rdistinct (rflts (map (rsimp \<circ> rerase) x2a)) {}")
+ apply simp
+ using rerase_list_ders apply blast
+ by simp
+
+lemma rders_simp_size:
+ shows " rders_simp (rerase r) s = rerase (bders_simp r s)"
+ apply(induct s rule: rev_induct)
+ apply simp
+ apply(subst rders_simp_append)
+ apply(subst bders_simp_append)
+ apply(subgoal_tac "rders_simp (rerase r ) xs = rerase (bders_simp r xs)")
+ apply(simp only:)
+ apply simp
+ apply (simp add: der_rerase2 simp_rerase)
+ by simp
+
+
+
+
+corollary aders_simp_finiteness:
+ assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
+ shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
+ using assms
+ apply(subgoal_tac "\<forall>s. asize (bders_simp r s) = rsize (rerase (bders_simp r s))")
+ apply(erule exE)
+ apply(rule_tac x = "N" in exI)
+ using rders_simp_size apply auto[1]
+ using asize_rsize by auto
+
+theorem annotated_size_bound:
+ shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
+ apply(insert aders_simp_finiteness)
+ by (simp add: rders_simp_bounded)
+
end
diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/SizeBoundStrong.thy
--- a/thys2/SizeBoundStrong.thy Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/SizeBoundStrong.thy Tue Apr 19 09:08:01 2022 +0100
@@ -502,6 +502,31 @@
decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append)
qed
+corollary main_decode1_horribly_wrong:
+ assumes "\<Turnstile> v : ders s r"
+ shows "Some(v) = decode (retrieve (bders (intern r) s) v) r"
+ using assms
+proof (induct s arbitrary: v rule: rev_induct)
+ case Nil
+ have "\<Turnstile> v : ders [] r" by fact
+ then have "\<Turnstile> v: r" by simp
+ then have "Some v = decode (retrieve (intern r) v) r"
+ using decode_code retrieve_code by force
+ then show "Some (v) = decode (retrieve (bders (intern r) []) v) r"
+ by simp
+next
+ case (snoc c s v)
+ have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow>
+ Some ( v) = decode (retrieve (bders (intern r) s) v ) r" by fact
+ have asm: "\<Turnstile> v: ders (s @ [c]) r" by fact
+ then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r"
+ using Prf_injval ders_snoc by force
+ then have injv: "Some (injval (ders s r) c v) =
+decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r"
+ by (simp add: IH asm2)
+ oops
+
+
definition blex where
"blex a s \<equiv> if bnullable (bders a s) then Some (bmkeps (bders a s)) else None"
@@ -592,17 +617,17 @@
| \<open>collect erasedR2 (r # rs) = collect erasedR2 rs\<close>
-fun pruneRexp where
+fun pruneRexp :: "arexp \<Rightarrow> rexp list \<Rightarrow> arexp"
+ where
"pruneRexp (ASEQ bs r1 r2) allowableTerms =
(let termsTruncated = (collect (erase r2) allowableTerms) in
(let pruned = pruneRexp r1 termsTruncated in
- (bsimp_ASEQ1 bs pruned r2)))"
+ (bsimp_ASEQ bs pruned r2)))"
| \<open>pruneRexp (AALTs bs rs) allowableTerms =
(let rsp = (filter (\<lambda>r. r \<noteq> AZERO) (map (\<lambda>r. pruneRexp r allowableTerms) rs) ) in bsimp_AALTs bs rsp )
\<close>
| \<open>pruneRexp r allowableTerms = (if (erase r) \<in> (set allowableTerms) then r else AZERO)\<close>
-
fun oneSimp :: \<open>rexp \<Rightarrow> rexp\<close> where
\<open> oneSimp (SEQ ONE r) = r \<close>
| \<open> oneSimp (SEQ r1 r2) = SEQ (oneSimp r1) r2 \<close>
@@ -617,14 +642,16 @@
where
\<open>addToAcc r acc = filter (\<lambda>r1. oneSimp r1 \<notin> set acc) (breakIntoTerms (erase r)) \<close>
+
+(*newSubRexps: terms that are new--have not existed in acc before*)
fun dBStrong :: "arexp list \<Rightarrow> rexp list \<Rightarrow> arexp list"
where
-"dBStrong [] acc = []"
+ "dBStrong [] acc = []"
| "dBStrong (r # rs) acc = (if (erase r) \<in> (set acc) then dBStrong rs acc
else let newSubRexps = (addToAcc r acc) in
(case (pruneRexp r newSubRexps) of
- AZERO \<Rightarrow> dBStrong rs (newSubRexps @ acc) |
- r1 \<Rightarrow> r1 # (dBStrong rs (newSubRexps @ acc))
+ AZERO \<Rightarrow> dBStrong rs (map oneSimp newSubRexps @ acc) |
+ r1 \<Rightarrow> r1 # (dBStrong rs (map oneSimp newSubRexps @ acc))
)
)
"
diff -r 48ce16d61e03 -r 61eff2abb0b6 thys2/blexer2.sc
--- a/thys2/blexer2.sc Sat Apr 16 09:52:57 2022 +0100
+++ b/thys2/blexer2.sc Tue Apr 19 09:08:01 2022 +0100
@@ -10,6 +10,7 @@
//
// amm lexer.sc all
+import scala.util.Try
// regular expressions including records
abstract class Rexp
@@ -28,6 +29,7 @@
// values
abstract class Val
+case object Failure extends Val
case object Empty extends Val
case class Chr(c: Char) extends Val
case class Sequ(v1: Val, v2: Val) extends Val
@@ -58,6 +60,166 @@
case class ANOT(bs: Bits, r: ARexp) extends ARexp
case class AANYCHAR(bs: Bits) extends ARexp
+trait Generator[+T] {
+ self => // an alias for "this"
+ def generate(): T
+
+ def gen(n: Int) : List[T] =
+ if (n == 0) Nil else self.generate() :: gen(n - 1)
+
+ def map[S](f: T => S): Generator[S] = new Generator[S] {
+ def generate = f(self.generate())
+ }
+ def flatMap[S](f: T => Generator[S]): Generator[S] = new Generator[S] {
+ def generate = f(self.generate()).generate()
+ }
+
+
+}
+
+ // tests a property according to a given random generator
+ def test[T](r: Generator[T], amount: Int = 100)(pred: T => Boolean) {
+ for (_ <- 0 until amount) {
+ val value = r.generate()
+ assert(pred(value), s"Test failed for: $value")
+ }
+ println(s"Test passed $amount times")
+ }
+ def test2[T, S](r: Generator[T], s: Generator[S], amount: Int = 100)(pred: (T, S) => Boolean) {
+ for (_ <- 0 until amount) {
+ val valueR = r.generate()
+ val valueS = s.generate()
+ assert(pred(valueR, valueS), s"Test failed for: $valueR, $valueS")
+ }
+ println(s"Test passed $amount times")
+ }
+
+// random integers
+val integers = new Generator[Int] {
+ val rand = new java.util.Random
+ def generate() = rand.nextInt()
+}
+
+// random booleans
+val booleans = integers.map(_ > 0)
+
+// random integers in the range lo and high
+def range(lo: Int, hi: Int): Generator[Int] =
+ for (x <- integers) yield (lo + x.abs % (hi - lo)).abs
+
+// random characters
+def chars_range(lo: Char, hi: Char) = range(lo, hi).map(_.toChar)
+val chars = chars_range('a', 'z')
+
+
+def oneOf[T](xs: T*): Generator[T] =
+ for (idx <- range(0, xs.length)) yield xs(idx)
+
+def single[T](x: T) = new Generator[T] {
+ def generate() = x
+}
+
+def pairs[T, U](t: Generator[T], u: Generator[U]): Generator[(T, U)] =
+ for (x <- t; y <- u) yield (x, y)
+
+// lists
+def emptyLists = single(Nil)
+
+def nonEmptyLists : Generator[List[Int]] =
+ for (head <- integers; tail <- lists) yield head :: tail
+
+def lists: Generator[List[Int]] = for {
+ kind <- booleans
+ list <- if (kind) emptyLists else nonEmptyLists
+} yield list
+
+def char_list(len: Int): Generator[List[Char]] = {
+ if(len <= 0) single(Nil)
+ else{
+ for {
+ c <- chars
+ tail <- char_list(len - 1)
+ } yield c :: tail
+ }
+}
+
+def strings(len: Int): Generator[String] = for(cs <- char_list(len)) yield cs.toString
+
+
+// (simple) binary trees
+trait Tree[T]
+case class Inner[T](left: Tree[T], right: Tree[T]) extends Tree[T]
+case class Leaf[T](x: T) extends Tree[T]
+
+def leafs[T](t: Generator[T]): Generator[Leaf[T]] =
+ for (x <- t) yield Leaf(x)
+
+def inners[T](t: Generator[T]): Generator[Inner[T]] =
+ for (l <- trees(t); r <- trees(t)) yield Inner(l, r)
+
+def trees[T](t: Generator[T]): Generator[Tree[T]] =
+ for (kind <- range(0, 2);
+ tree <- if (kind == 0) leafs(t) else inners(t)) yield tree
+
+// regular expressions
+
+// generates random leaf-regexes; prefers CHAR-regexes
+def leaf_rexp() : Generator[Rexp] =
+ for (kind <- range(0, 5);
+ c <- chars_range('a', 'd')) yield
+ kind match {
+ case 0 => ZERO
+ case 1 => ONE
+ case _ => CHAR(c)
+ }
+
+// generates random inner regexes with maximum depth d
+def inner_rexp(d: Int) : Generator[Rexp] =
+ for (kind <- range(0, 3);
+ l <- rexp(d);
+ r <- rexp(d))
+ yield kind match {
+ case 0 => ALTS(l, r)
+ case 1 => SEQ(l, r)
+ case 2 => STAR(r)
+ }
+
+// generates random regexes with maximum depth d;
+// prefers inner regexes in 2/3 of the cases
+def rexp(d: Int = 100): Generator[Rexp] =
+ for (kind <- range(0, 3);
+ r <- if (d <= 0 || kind == 0) leaf_rexp() else inner_rexp(d - 1)) yield r
+
+
+// some test functions for rexps
+def height(r: Rexp) : Int = r match {
+ case ZERO => 1
+ case ONE => 1
+ case CHAR(_) => 1
+ case ALTS(r1, r2) => 1 + List(height(r1), height(r2)).max
+ case SEQ(r1, r2) => 1 + List(height(r1), height(r2)).max
+ case STAR(r) => 1 + height(r)
+}
+
+// def size(r: Rexp) : Int = r match {
+// case ZERO => 1
+// case ONE => 1
+// case CHAR(_) => 1
+// case ALTS(r1, r2) => 1 + size(r1) + size(r2)
+// case SEQ(r1, r2) => 1 + size(r1) + size(r2)
+// case STAR(r) => 1 + size(r)
+// }
+
+// randomly subtracts 1 or 2 from the STAR case
+def size_faulty(r: Rexp) : Int = r match {
+ case ZERO => 1
+ case ONE => 1
+ case CHAR(_) => 1
+ case ALTS(r1, r2) => 1 + size_faulty(r1) + size_faulty(r2)
+ case SEQ(r1, r2) => 1 + size_faulty(r1) + size_faulty(r2)
+ case STAR(r) => 1 + size_faulty(r) - range(0, 2).generate
+}
+
// some convenience for typing in regular expressions
@@ -184,104 +346,12 @@
}
// some "rectification" functions for simplification
-def F_ID(v: Val): Val = v
-def F_RIGHT(f: Val => Val) = (v:Val) => Right(f(v))
-def F_LEFT(f: Val => Val) = (v:Val) => Left(f(v))
-def F_ALT(f1: Val => Val, f2: Val => Val) = (v:Val) => v match {
- case Right(v) => Right(f2(v))
- case Left(v) => Left(f1(v))
-}
-def F_SEQ(f1: Val => Val, f2: Val => Val) = (v:Val) => v match {
- case Sequ(v1, v2) => Sequ(f1(v1), f2(v2))
-}
-def F_SEQ_Empty1(f1: Val => Val, f2: Val => Val) =
- (v:Val) => Sequ(f1(Empty), f2(v))
-def F_SEQ_Empty2(f1: Val => Val, f2: Val => Val) =
- (v:Val) => Sequ(f1(v), f2(Empty))
-def F_ERROR(v: Val): Val = throw new Exception("error")
-// simplification
-def simp(r: Rexp): (Rexp, Val => Val) = r match {
- case ALTS(r1, r2) => {
- val (r1s, f1s) = simp(r1)
- val (r2s, f2s) = simp(r2)
- (r1s, r2s) match {
- case (ZERO, _) => (r2s, F_RIGHT(f2s))
- case (_, ZERO) => (r1s, F_LEFT(f1s))
- case _ => if (r1s == r2s) (r1s, F_LEFT(f1s))
- else (ALTS (r1s, r2s), F_ALT(f1s, f2s))
- }
- }
- case SEQ(r1, r2) => {
- val (r1s, f1s) = simp(r1)
- val (r2s, f2s) = simp(r2)
- (r1s, r2s) match {
- case (ZERO, _) => (ZERO, F_ERROR)
- case (_, ZERO) => (ZERO, F_ERROR)
- case (ONE, _) => (r2s, F_SEQ_Empty1(f1s, f2s))
- case (_, ONE) => (r1s, F_SEQ_Empty2(f1s, f2s))
- case _ => (SEQ(r1s,r2s), F_SEQ(f1s, f2s))
- }
- }
- case r => (r, F_ID)
-}
-// lexing functions including simplification
-def lex_simp(r: Rexp, s: List[Char]) : Val = s match {
- case Nil => if (nullable(r)) mkeps(r) else
- { throw new Exception(s"lexing error $r not nullable") }
- case c::cs => {
- val (r_simp, f_simp) = simp(der(c, r))
- inj(r, c, f_simp(lex_simp(r_simp, cs)))
- }
-}
-
-def lexing_simp(r: Rexp, s: String) =
- env(lex_simp(r, s.toList))
// The Lexing Rules for the WHILE Language
-def PLUS(r: Rexp) = r ~ r.%
-
-def Range(s : List[Char]) : Rexp = s match {
- case Nil => ZERO
- case c::Nil => CHAR(c)
- case c::s => ALTS(CHAR(c), Range(s))
-}
-def RANGE(s: String) = Range(s.toList)
-
-val SYM = RANGE("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz_")
-val DIGIT = RANGE("0123456789")
-val ID = SYM ~ (SYM | DIGIT).%
-val NUM = PLUS(DIGIT)
-val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write"
-val SEMI: Rexp = ";"
-val OP: Rexp = ":=" | "=" | "-" | "+" | "*" | "!=" | "<" | ">"
-val WHITESPACE = PLUS(" " | "\n" | "\t" | "\r")
-val RPAREN: Rexp = "{"
-val LPAREN: Rexp = "}"
-val STRING: Rexp = "\"" ~ SYM.% ~ "\""
-
-
-//ab \ a --> 1b
-//
-val WHILE_REGS = (("k" $ KEYWORD) |
- ("i" $ ID) |
- ("o" $ OP) |
- ("n" $ NUM) |
- ("s" $ SEMI) |
- ("str" $ STRING) |
- ("p" $ (LPAREN | RPAREN)) |
- ("w" $ WHITESPACE)).%
-
-val NREGS = NTIMES(5, OPTIONAL(SYM))
-val NREGS1 = ("test" $ NREGS)
-// Two Simple While Tests
-//========================
-val NOTREG = "hehe" ~ NOT((ANYCHAR.%) ~ "haha" ~ (ANYCHAR.%))
-
-
// bnullable function: tests whether the aregular
// expression can recognise the empty string
def bnullable (r: ARexp) : Boolean = r match {
@@ -371,252 +441,186 @@
}
case r => r
}
- }
- def strongBsimp(r: ARexp): ARexp =
- {
- r match {
- case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(r2)) match {
- case (AZERO, _) => AZERO
- case (_, AZERO) => AZERO
- case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
- case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
- }
- case AALTS(bs1, rs) => {
- val rs_simp = rs.map(strongBsimp(_))
- val flat_res = flats(rs_simp)
- val dist_res = distinctBy4(flat_res)//distinctBy(flat_res, erase)
- dist_res match {
- case Nil => AZERO
- case s :: Nil => fuse(bs1, s)
- case rs => AALTS(bs1, rs)
- }
-
- }
- case r => r
+}
+def strongBsimp(r: ARexp): ARexp =
+{
+ r match {
+ case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(r2)) match {
+ case (AZERO, _) => AZERO
+ case (_, AZERO) => AZERO
+ case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
+ case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
}
+ case AALTS(bs1, rs) => {
+ val rs_simp = rs.map(strongBsimp(_))
+ val flat_res = flats(rs_simp)
+ val dist_res = distinctBy4(flat_res)//distinctBy(flat_res, erase)
+ dist_res match {
+ case Nil => AZERO
+ case s :: Nil => fuse(bs1, s)
+ case rs => AALTS(bs1, rs)
+ }
+
+ }
+ case r => r
}
-
- def bders (s: List[Char], r: ARexp) : ARexp = s match {
- case Nil => r
- case c::s => bders(s, bder(c, r))
- }
-
- def flats(rs: List[ARexp]): List[ARexp] = rs match {
- case Nil => Nil
- case AZERO :: rs1 => flats(rs1)
- case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
- case r1 :: rs2 => r1 :: flats(rs2)
- }
-
- def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
- case Nil => Nil
- case (x::xs) => {
- val res = f(x)
- if (acc.contains(res)) distinctBy(xs, f, acc)
- else x::distinctBy(xs, f, res::acc)
- }
- }
-
- def projectFirstChild(rs: List[ARexp]) : List[ARexp] = rs match {
- case (ASEQ(bs, r1, r2p)::rs1) => r1::projectFirstChild(rs1)
- case Nil => Nil
- }
+}
-
- def distinctBy2(xs: List[ARexp], acc: List[Rexp] = Nil): List[ARexp] = xs match {
- case Nil => Nil
- case (x::xs) => {
- val res = erase(x)
- if(acc.contains(res))
- distinctBy2(xs, acc)
- else
- x match {
- case ASEQ(bs0, AALTS(bs1, rs), r2) =>
- val newTerms = distinctBy2(rs.map(r1 => ASEQ(Nil, r1, r2)), acc)
- val rsPrime = projectFirstChild(newTerms)
- newTerms match {
- case Nil => distinctBy2(xs, acc)
- case t::Nil => ASEQ(bs0, fuse(bs1, rsPrime.head), r2)::distinctBy2(xs, erase(t)::acc)
- case ts => ASEQ(bs0, AALTS(bs1, rsPrime), r2)::distinctBy2(xs, newTerms.map(erase(_)):::acc)
- }
- case x => x::distinctBy2(xs, res::acc)
- }
- }
- }
-
- def deepFlts(r: ARexp): List[ARexp] = r match{
+def bders (s: List[Char], r: ARexp) : ARexp = s match {
+ case Nil => r
+ case c::s => bders(s, bder(c, r))
+}
- case ASEQ(bs, r1, r2) => deepFlts(r1).map(r1p => ASEQ(bs, r1p, r2))
- case ASTAR(bs, r0) => List(r)
- case ACHAR(_, _) => List(r)
- case AALTS(bs, rs) => rs.flatMap(deepFlts(_))//throw new Error("doubly nested alts in bsimp r")
- }
-
-
- def distinctBy3(xs: List[ARexp], acc: List[Rexp] = Nil): List[ARexp] = xs match {
+def flats(rs: List[ARexp]): List[ARexp] = rs match {
case Nil => Nil
- case (x::xs) => {
- val res = erase(x)
- if(acc.contains(res))
- distinctBy3(xs, acc)
- else
- x match {
- case ASEQ(bs0, AALTS(bs1, rs), r2) =>
- val newTerms = distinctBy3(rs.flatMap(deepFlts(_)).map(r1 => ASEQ(Nil, r1, r2)), acc)//deepFlts(rs.flatMap(r1 => ASEQ(Nil, r1, r2)), acc)
- val rsPrime = projectFirstChild(newTerms)
- newTerms match {
- case Nil => distinctBy3(xs, acc)
- case t::Nil => ASEQ(bs0, fuse(bs1, rsPrime.head), r2)::distinctBy3(xs, erase(t)::acc)
- case ts => ASEQ(bs0, AALTS(bs1, rsPrime), r2)::distinctBy3(xs, newTerms.map(erase(_)):::acc)
- }
- case x => x::distinctBy3(xs, res::acc)
- }
- }
+ case AZERO :: rs1 => flats(rs1)
+ case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
+ case r1 :: rs2 => r1 :: flats(rs2)
}
- def pruneRexp(r: ARexp, allowableTerms: List[Rexp]) : ARexp = {
- r match {
- case ASEQ(bs, r1, r2) =>
- val termsTruncated = allowableTerms.collect(rt => rt match {
- case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2))
- })
- val pruned : ARexp = pruneRexp(r1, termsTruncated)
- pruned match {
- case AZERO => AZERO
- case AONE(bs1) => fuse(bs ++ bs1, r2)
- case pruned1 => ASEQ(bs, pruned1, r2)
- }
-
- case AALTS(bs, rs) =>
- //allowableTerms.foreach(a => println(shortRexpOutput(a)))
- val rsp = rs.map(r =>
- pruneRexp(r, allowableTerms)
- )
- .filter(r => r != AZERO)
- rsp match {
- case Nil => AZERO
- case r1::Nil => fuse(bs, r1)
- case rs1 => AALTS(bs, rs1)
- }
- case r =>
- if(allowableTerms.contains(erase(r))) r else AZERO //assert(r != AZERO)
- }
+def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
+ case Nil => Nil
+ case (x::xs) => {
+ val res = f(x)
+ if (acc.contains(res)) distinctBy(xs, f, acc)
+ else x::distinctBy(xs, f, res::acc)
}
-
- def oneSimp(r: Rexp) : Rexp = r match {
- case SEQ(ONE, r) => r
- case SEQ(r1, r2) => SEQ(oneSimp(r1), r2)
- case r => r//assert r != 0
-
- }
+}
- def distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+def pruneRexp(r: ARexp, allowableTerms: List[Rexp]) : ARexp = {
+ r match {
+ case ASEQ(bs, r1, r2) =>
+ val termsTruncated = allowableTerms.collect(rt => rt match {
+ case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2))
+ })
+ val pruned : ARexp = pruneRexp(r1, termsTruncated)
+ pruned match {
+ case AZERO => AZERO
+ case AONE(bs1) => fuse(bs ++ bs1, r2)
+ case pruned1 => ASEQ(bs, pruned1, r2)
+ }
+
+ case AALTS(bs, rs) =>
+ //allowableTerms.foreach(a => println(shortRexpOutput(a)))
+ val rsp = rs.map(r =>
+ pruneRexp(r, allowableTerms)
+ )
+ .filter(r => r != AZERO)
+ rsp match {
+ case Nil => AZERO
+ case r1::Nil => fuse(bs, r1)
+ case rs1 => AALTS(bs, rs1)
+ }
+ case r =>
+ if(allowableTerms.contains(erase(r))) r else AZERO //assert(r != AZERO)
+ }
+}
+
+def oneSimp(r: Rexp) : Rexp = r match {
+ case SEQ(ONE, r) => r
+ case SEQ(r1, r2) => SEQ(oneSimp(r1), r2)
+ case r => r//assert r != 0
- case Nil => Nil
- case x :: xs =>
- //assert(acc.distinct == acc)
- val erased = erase(x)
- if(acc.contains(erased))
- distinctBy4(xs, acc)
- else{
- val addToAcc = breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
- //val xp = pruneRexp(x, addToAcc)
- pruneRexp(x, addToAcc) match {
- case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
- case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
- }
-
- }
- }
+}
- def breakIntoTerms(r: Rexp) : List[Rexp] = r match {
- case SEQ(r1, r2) => breakIntoTerms(r1).map(r11 => SEQ(r11, r2))
- // breakIntoTerms(r1).map(r11 => r11 match {
- // case ONE => r2
- // case r => SEQ(r11, r2)
- // }
- //)
- case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
- case _ => r::Nil
- }
-
- def prettyRexp(r: Rexp) : String = r match {
- case STAR(r0) => s"${prettyRexp(r0)}*"
- case SEQ(CHAR(c), r2) => c.toString ++ prettyRexp(r2)
- case SEQ(r1, r2) => s"${prettyRexp(r1)}~${prettyRexp(r2)}"
- case CHAR(c) => c.toString
- case ANYCHAR => "."
- // case NOT(r0) => s
- }
-
- def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
- case (ONE, bs) => (Empty, bs)
- case (CHAR(f), bs) => (Chr(f), bs)
- case (ALTS(r1, r2), Z::bs1) => {
- val (v, bs2) = decode_aux(r1, bs1)
- (Left(v), bs2)
+def distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+ case Nil => Nil
+ case x :: xs =>
+ //assert(acc.distinct == acc)
+ val erased = erase(x)
+ if(acc.contains(erased))
+ distinctBy4(xs, acc)
+ else{
+ val addToAcc = breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
+ //val xp = pruneRexp(x, addToAcc)
+ pruneRexp(x, addToAcc) match {
+ case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
+ case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
+ }
+
}
- case (ALTS(r1, r2), S::bs1) => {
- val (v, bs2) = decode_aux(r2, bs1)
- (Right(v), bs2)
- }
- case (SEQ(r1, r2), bs) => {
- val (v1, bs1) = decode_aux(r1, bs)
- val (v2, bs2) = decode_aux(r2, bs1)
- (Sequ(v1, v2), bs2)
- }
- case (STAR(r1), S::bs) => {
- val (v, bs1) = decode_aux(r1, bs)
- //println(v)
- val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
- (Stars(v::vs), bs2)
- }
- case (STAR(_), Z::bs) => (Stars(Nil), bs)
- case (RECD(x, r1), bs) => {
- val (v, bs1) = decode_aux(r1, bs)
- (Rec(x, v), bs1)
- }
- case (NOT(r), bs) => (Nots(prettyRexp(r)), bs)
- }
+}
+
- def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
- case (v, Nil) => v
- case _ => throw new Exception("Not decodable")
- }
+def breakIntoTerms(r: Rexp) : List[Rexp] = r match {
+ case SEQ(r1, r2) => breakIntoTerms(r1).map(r11 => SEQ(r11, r2))
+ case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
+ case _ => r::Nil
+}
-def blexSimp(r: Rexp, s: String) : List[Bit] = {
- blex_simp(internalise(r), s.toList)
+def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
+ case (ONE, bs) => (Empty, bs)
+ case (CHAR(f), bs) => (Chr(f), bs)
+ case (ALTS(r1, r2), Z::bs1) => {
+ val (v, bs2) = decode_aux(r1, bs1)
+ (Left(v), bs2)
+ }
+ case (ALTS(r1, r2), S::bs1) => {
+ val (v, bs2) = decode_aux(r2, bs1)
+ (Right(v), bs2)
+ }
+ case (SEQ(r1, r2), bs) => {
+ val (v1, bs1) = decode_aux(r1, bs)
+ val (v2, bs2) = decode_aux(r2, bs1)
+ (Sequ(v1, v2), bs2)
+ }
+ case (STAR(r1), S::bs) => {
+ val (v, bs1) = decode_aux(r1, bs)
+ //println(v)
+ val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
+ (Stars(v::vs), bs2)
+ }
+ case (STAR(_), Z::bs) => (Stars(Nil), bs)
+ case (RECD(x, r1), bs) => {
+ val (v, bs1) = decode_aux(r1, bs)
+ (Rec(x, v), bs1)
+ }
+ case (NOT(r), bs) => (Nots(r.toString), bs)
}
+def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
+ case (v, Nil) => v
+ case _ => throw new Exception("Not decodable")
+}
+
+
+
def blexing_simp(r: Rexp, s: String) : Val = {
val bit_code = blex_simp(internalise(r), s.toList)
decode(r, bit_code)
- }
+}
+def simpBlexer(r: Rexp, s: String) : Val = {
+ Try(blexing_simp(r, s)).getOrElse(Failure)
+}
- def strong_blexing_simp(r: Rexp, s: String) : Val = {
- decode(r, strong_blex_simp(internalise(r), s.toList))
- }
+def strong_blexing_simp(r: Rexp, s: String) : Val = {
+ decode(r, strong_blex_simp(internalise(r), s.toList))
+}
+
+def strongBlexer(r: Rexp, s: String) : Val = {
+ Try(strong_blexing_simp(r, s)).getOrElse(Failure)
+}
- def strong_blex_simp(r: ARexp, s: List[Char]) :Bits = s match {
- case Nil => {
- if (bnullable(r)) {
- //println(asize(r))
- val bits = mkepsBC(r)
- bits
- }
- else
- throw new Exception("Not matched")
+def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
+ case Nil => {
+ if (bnullable(r)) {
+ //println(asize(r))
+ val bits = mkepsBC(r)
+ bits
}
- case c::cs => {
- val der_res = bder(c,r)
- val simp_res = strongBsimp(der_res)
- strong_blex_simp(simp_res, cs)
- }
+ else
+ throw new Exception("Not matched")
}
+ case c::cs => {
+ val der_res = bder(c,r)
+ val simp_res = strongBsimp(der_res)
+ strong_blex_simp(simp_res, cs)
+ }
+}
@@ -629,12 +633,12 @@
def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
- def bders_simpS(s: List[Char], r: ARexp) : ARexp = s match {
+ def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
case Nil => r
- case c::s => bders_simpS(s, strongBsimp(bder(c, r)))
+ case c::s => bdersStrong(s, strongBsimp(bder(c, r)))
}
- def bdersSimpS(s: String, r: Rexp) : ARexp = bders_simpS(s.toList, internalise(r))
+ def bdersStrongRexp(s: String, r: Rexp) : ARexp = bdersStrong(s.toList, internalise(r))
def erase(r:ARexp): Rexp = r match{
case AZERO => ZERO
@@ -650,59 +654,63 @@
}
-def allCharSeq(r: Rexp) : Boolean = r match {
- case CHAR(c) => true
- case SEQ(r1, r2) => allCharSeq(r1) && allCharSeq(r2)
- case _ => false
-}
+ def allCharSeq(r: Rexp) : Boolean = r match {
+ case CHAR(c) => true
+ case SEQ(r1, r2) => allCharSeq(r1) && allCharSeq(r2)
+ case _ => false
+ }
+
+ def flattenSeq(r: Rexp) : String = r match {
+ case CHAR(c) => c.toString
+ case SEQ(r1, r2) => flattenSeq(r1) ++ flattenSeq(r2)
+ case _ => throw new Error("flatten unflattenable rexp")
+ }
-def flattenSeq(r: Rexp) : String = r match {
- case CHAR(c) => c.toString
- case SEQ(r1, r2) => flattenSeq(r1) ++ flattenSeq(r2)
- case _ => throw new Error("flatten unflattenable rexp")
-}
+ def shortRexpOutput(r: Rexp) : String = r match {
+ case CHAR(c) => c.toString
+ case ONE => "1"
+ case ZERO => "0"
+ case SEQ(r1, r2) if(allCharSeq(r)) => flattenSeq(r)//"[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
+ case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
+ case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
+ case STAR(STAR(r)) => "(..)*"// ++ shortRexpOutput(r) ++ "]*"
+ case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
+ //case RTOP => "RTOP"
+ }
+
-def shortRexpOutput(r: Rexp) : String = r match {
- case CHAR(c) => c.toString
- case ONE => "1"
- case ZERO => "0"
- case SEQ(r1, r2) if(allCharSeq(r)) => flattenSeq(r)//"[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
- case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
- case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
- case STAR(STAR(r)) => "(..)*"// ++ shortRexpOutput(r) ++ "]*"
- case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
- //case RTOP => "RTOP"
+ def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
+ case Nil => {
+ if (bnullable(r)) {
+ //println(asize(r))
+ val bits = mkepsBC(r)
+ bits
+ }
+ else
+ throw new Exception("Not matched")
+ }
+ case c::cs => {
+ val der_res = bder(c,r)
+ val simp_res = bsimp(der_res)
+ blex_simp(simp_res, cs)
+ }
}
-def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
- case Nil => {
- if (bnullable(r)) {
- //println(asize(r))
- val bits = mkepsBC(r)
- bits
- }
- else
- throw new Exception("Not matched")
+
+
+ def size(r: Rexp) : Int = r match {
+ case ZERO => 1
+ case ONE => 1
+ case CHAR(_) => 1
+ case ANYCHAR => 1
+ case NOT(r0) => 1 + size(r0)
+ case SEQ(r1, r2) => 1 + size(r1) + size(r2)
+ case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
+ case STAR(r) => 1 + size(r)
}
- case c::cs => {
- val der_res = bder(c,r)
- val simp_res = bsimp(der_res)
- blex_simp(simp_res, cs)
- }
- }
- def size(r: Rexp) : Int = r match {
- case ZERO => 1
- case ONE => 1
- case CHAR(_) => 1
- case ANYCHAR => 1
- case NOT(r0) => 1 + size(r0)
- case SEQ(r1, r2) => 1 + size(r1) + size(r2)
- case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
- case STAR(r) => 1 + size(r)
- }
- def asize(a: ARexp) = size(erase(a))
+ def asize(a: ARexp) = size(erase(a))
//pder related
type Mon = (Char, Rexp)
@@ -808,6 +816,9 @@
(((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).%
// @main
+
+
+
def small() = {
@@ -834,56 +845,89 @@
// //println(refSize)
// println(pderSTAR.size)
- val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%)
- val B : Rexp = ((ONE).%)
- val C : Rexp = ("d") ~ ((ONE).%)
- val PRUNE_REG : Rexp = (C | B | A)
- val APRUNE_REG = internalise(PRUNE_REG)
- // // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG))
- // // println("program executes and gives: as disired!")
- // // println(shortRexpOutput(erase(program_solution)))
+ // val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%)
+ // val B : Rexp = ((ONE).%)
+ // val C : Rexp = ("d") ~ ((ONE).%)
+ // val PRUNE_REG : Rexp = (C | B | A)
+ // val APRUNE_REG = internalise(PRUNE_REG)
+ // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG))
+ // println("program executes and gives: as disired!")
+ // println(shortRexpOutput(erase(program_solution)))
// val simpedPruneReg = strongBsimp(APRUNE_REG)
// println(shortRexpOutput(erase(simpedPruneReg)))
- // for(i <- List(1,2 ) ){// 100, 400, 800, 840, 841, 900
- // val prog0 = "a" * i
- // //println(s"test: $prog0")
- // println(s"testing with $i a's" )
- // //val bd = bdersSimp(prog0, STARREG)//DB
- // val sbd = bdersSimpS(prog0, STARREG)//strongDB
- // starPrint(erase(sbd))
- // val subTerms = breakIntoTerms(erase(sbd))
- // //val subTermsLarge = breakIntoTerms(erase(bd))
+
+
+ for(i <- List(1,2,3,4,10, 100, 400, 841, 900 ) ){// 100, 400, 800, 840, 841, 900
+ val prog0 = "a" * i
+ //println(s"test: $prog0")
+ println(s"testing with $i a's" )
+ //val bd = bdersSimp(prog0, STARREG)//DB
+ val sbd = bdersStrongRexp(prog0, STARREG)//strongDB
+ starPrint(erase(sbd))
+ val subTerms = breakIntoTerms(erase(sbd))
+ //val subTermsLarge = breakIntoTerms(erase(bd))
- // println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}")
+ println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}")
- // println("the number of distinct subterms for bsimp with strongDB")
- // println(subTerms.distinct.size)
- // //println(subTermsLarge.distinct.size)
- // println("which coincides with the number of PDER terms")
+ println("the number of distinct subterms for bsimp with strongDB")
+ println(subTerms.distinct.size)
+ //println(subTermsLarge.distinct.size)
+ if(pderSTAR.size > subTerms.length)
+ println(s"which is less than or equal to the number of PDER terms: ${pderSTAR.size}")
- // // println(shortRexpOutput(erase(sbd)))
- // // println(shortRexpOutput(erase(bd)))
+ // println(shortRexpOutput(erase(sbd)))
+ // println(shortRexpOutput(erase(bd)))
- // println("pdersize, original, strongSimp")
- // println(refSize, size(STARREG), asize(sbd))
+ println("pdersize, original, strongSimp")
+ println(refSize, size(STARREG), asize(sbd))
- // val vres = strong_blexing_simp( STARREG, prog0)
- // println(vres)
- // }
-// println(vs.length)
-// println(vs)
+ //val vres = strong_blexing_simp( STARREG, prog0)
+ //println(vres)
+ }
+ // println(vs.length)
+ // println(vs)
// val prog1 = """read n; write n"""
// println(s"test: $prog1")
// println(lexing_simp(WHILE_REGS, prog1))
- val display = ("a"| "ab").%
- val adisplay = internalise(display)
- bders_simp( "aaaaa".toList, adisplay)
+ // val display = ("a"| "ab").%
+ // val adisplay = internalise(display)
+ // bders_simp( "aaaaa".toList, adisplay)
}
-small()
+def generator_test() {
+ // println("XXX generates 10 random integers in the range 0..2")
+ // println(range(0, 3).gen(10).mkString("\n"))
+
+ // println("XXX gnerates random lists and trees")
+ // println(lists.generate())
+ // println(trees(chars).generate())
+
+ // println("XXX generates 10 random characters")
+ // println(chars.gen(10).mkString("\n"))
+
+ // println("XXX generates 10 random leaf-regexes")
+ // println(leaf_rexp().gen(10).mkString("\n"))
+
+ // println("XXX generates 1000 regexes of maximal 10 height")
+ // println(rexp(10).gen(1000).mkString("\n"))
+
+ // println("XXX generates 1000 regexes and tests an always true-test")
+ // test(rexp(10), 1000) { _ => true }
+ // println("XXX generates regexes and tests a valid predicate")
+ // test(rexp(10), 1000) { r => height(r) <= size(r) }
+ // println("XXX faulty test")
+ // test(rexp(10), 100) { r => height(r) <= size_faulty(r) }
+ println("testing strongbsimp against bsimp")
+ test2(rexp(10), strings(2), 100) { (r : Rexp, s: String) =>
+ (simpBlexer(r, s) == strongBlexer(r, s))
+ }
+
+}
+// small()
+generator_test()