# HG changeset patch # User Chengsong # Date 1659474682 -3600 # Node ID 3178f0e948ac7f1611198814202b3e2f48ec28dd # Parent 692911c0b9819e71f8cac6f82ab1b47d17de14de more diff -r 692911c0b981 -r 3178f0e948ac ChengsongTanPhdThesis/Chapters/Bitcoded1.tex --- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex Thu Jul 21 20:22:35 2022 +0100 +++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex Tue Aug 02 22:11:22 2022 +0100 @@ -178,11 +178,6 @@ Because of the lossiness, the process of decoding a bitlist requires additionally a regular expression. The function $\decode$ is defined as: -We define the reverse operation of $\code$, which is $\decode$. -As expected, $\decode$ not only requires the bit-codes, -but also a regular expression to guide the decoding and -fill the gaps of characters: - %\begin{definition}[Bitdecoding of Values]\mbox{} \begin{center} @@ -214,27 +209,35 @@ %\end{definition} \noindent -The function $\decode'$ returns a pair consisting of a partially decoded value and some leftover: -$\decode'$ does most of the job while $\decode$ throws -away leftover bit-codes and returns the value only. +The function $\decode'$ returns a pair consisting of +a partially decoded value and some leftover bit list that cannot +be decide yet. +The function $\decode'$ succeeds if the left-over +bit-sequence is empty. $\decode$ is terminating as $\decode'$ is terminating. -We have the property that $\decode$ and $\code$ are +$\decode'$ is terminating +because at least one of $\decode'$'s parameters will go down in terms +of size. +Assuming we have a value $v$ and regular expression $r$ +with $\vdash v:r$, +then we have the property that $\decode$ and $\code$ are reverse operations of one another: \begin{lemma} -\[\vdash v : r \implies \decode \; (\code \; v) \; r = \textit{Some}(v) \] +\[If \vdash v : r \; then \;\decode \; (\code \; v) \; r = \textit{Some}(v) \] \end{lemma} \begin{proof} By proving a more general version of the lemma, on $\decode'$: \[\vdash v : r \implies \decode' \; ((\code \; v) @ ds) \; r = (v, ds) \] -Then setting $ds$ to be $[]$ and unfolding $\decode$ definition -we get the lemma. +Then setting $ds$ to be $[]$ and unfolding $\decode$ definition, +we obtain the property. \end{proof} With the $\code$ and $\decode$ functions in hand, we know how to -switch between bit-codes and value--the two different representations of -lexing information. -The next step is to integrate this information into the working regular expression. +switch between bit-codes and values. +The next step is to integrate this information into regular expression. Attaching bits to the front of regular expressions is the solution Sulzamann and Lu -gave for storing partial values on the fly: +gave for storing partial values in regular expressions. +Annotated regular expressions are therefore defined as the Isabelle +datatype: \begin{center} \begin{tabular}{lcl} @@ -249,16 +252,18 @@ %(in \textit{ALTS}) \noindent -We call these regular expressions carrying bit-codes \emph{Annotated regular expressions}. -$bs$ stands for bit-codes, $a$ for $\mathbf{a}$nnotated regular -expressions and $as$ for a list of annotated regular expressions. -The alternative constructor ($\sum$) has been generalised to -accept a list of annotated regular expressions rather than just 2. +where $bs$ stands for bit-codes, $a$ for $\mathbf{a}$nnotated regular +expressions and $as$ for lists of annotated regular expressions. +The alternative constructor, written, $\sum$, has been generalised to +accept a list of annotated regular expressions rather than just two. +Why is it generalised? This is because when we open up nested +alternatives, there could be more than two elements at the same level +after de-duplication, which can no longer be stored in a binary +constructor. - -The first thing we define related to bit-coded regular expressions -is how we move bits, for instance pasting it at the front of an annotated regular expression. -The operation $\fuse$ is just to attach bit-codes +The first operation we define related to bit-coded regular expressions +is how we move bits to the inside of regular expressions. +Called $\fuse$, this operation is attaches bit-codes to the front of an annotated regular expression: \begin{center} \begin{tabular}{lcl} @@ -277,14 +282,12 @@ \end{center} \noindent -With that we are able to define $\internalise$. +With \emph{fuse} we are able to define the $\internalise$ function +that translates a ``standard'' regular expression into an +annotated regular expression. +This function will be applied before we start +with the derivative phase of the algorithm. -To do lexing using annotated regular expressions, we shall first -transform the usual (un-annotated) regular expressions into annotated -regular expressions. This operation is called \emph{internalisation} and -defined as follows: - -%\begin{definition} \begin{center} \begin{tabular}{lcl} $(\ZERO)^\uparrow$ & $\dn$ & $\ZERO$\\ @@ -303,7 +306,7 @@ \noindent We use an up arrow with postfix notation -to denote the operation, +to denote this operation. for convenience. The $\textit{internalise} \; r$ notation is more cumbersome. The opposite of $\textit{internalise}$ is @@ -312,16 +315,17 @@ regular expressions is transformed to the binary alternatives for plain regular expressions. \begin{center} - \begin{tabular}{lcr} - $\erase \; \ZERO$ & $\dn$ & $\ZERO$\\ - $\erase \; _{bs}\ONE$ & $\dn$ & $\ONE$\\ - $\erase \; _{bs}\mathbf{c}$ & $\dn$ & $\mathbf{c}$\\ - $\erase \; _{bs} a_1 \cdot a_2$ & $\dn$ & $\erase \; r_1\cdot\erase\; r_2$\\ - $\erase \; _{bs} [] $ & $\dn$ & $\ZERO$\\ - $\erase \; _{bs} [a] $ & $\dn$ & $\erase \; a$\\ - $\erase \; _{bs} \sum [a_1, \; a_2]$ & $\dn$ & $\erase \; a_1 +\erase \; a_2$\\ - $\erase \; _{bs} \sum (a :: as)$ & $\dn$ & $\erase \; a + \erase \; _{[]} \sum as$\\ - $\erase \; _{bs} a^*$ & $\dn$ & $(\erase \; a)^*$ + \begin{tabular}{lcl} + $\ZERO_\downarrow$ & $\dn$ & $\ZERO$\\ + $( _{bs}\ONE )_\downarrow$ & $\dn$ & $\ONE$\\ + $( _{bs}\mathbf{c} )_\downarrow$ & $\dn$ & $\mathbf{c}$\\ + $( _{bs} a_1 \cdot a_2 )_\downarrow$ & $\dn$ & + $ (a_1) _\downarrow \cdot (a_2) _\downarrow$\\ + $( _{bs} [])_\downarrow $ & $\dn$ & $\ZERO $\\ + $( _{bs} [a] )_\downarrow$ & $\dn$ & $a_\downarrow$\\ + $_{bs} \sum [a_1, \; a_2]$ & $\dn$ & $ (a_1) _\downarrow + ( a_2 ) _\downarrow $\\ + $(_{bs} \sum (a :: as))_\downarrow$ & $\dn$ & $ a_\downarrow + \; (_{[]} \sum as)_\downarrow$\\ + $( _{bs} a^* )_\downarrow$ & $\dn$ & $(a_\downarrow)^*$ \end{tabular} \end{center} \noindent @@ -331,13 +335,12 @@ testing whether they contain empty string in their lauguage requires a dedicated function $\bnullable$ which simply calls $\erase$ first before testing whether it is $\nullable$. -\begin{center} - \begin{tabular}{lcr} - $\bnullable \; a $ & $\dn$ & $\nullable \; (a_\downarrow)$ - \end{tabular} -\end{center} +\begin{definition} + $\bnullable \; a \dn \nullable \; (a_\downarrow)$ +\end{definition} The function for collecting the -bitcodes of a $\bnullable$ annotated regular expression +bitcodes at the end of the derivative +phase from a (b)nullable regular expression is a generalised version of the $\textit{mkeps}$ function for annotated regular expressions, called $\textit{bmkeps}$: @@ -359,74 +362,105 @@ %\end{definition} \noindent -This function completes the value information by travelling along the +$\bmkeps$ completes the value information by travelling along the path of the regular expression that corresponds to a POSIX value and -collecting all the bitcodes, and using $S$ to indicate the end of star +collecting all the bitcodes, and attaching $S$ to indicate the end of star iterations. -The most central question is how these partial lexing information -represented as bit-codes is augmented and carried around -during a derivative is taken. -This is done by adding bitcodes to the -derivatives, for example when one more star iteratoin is taken (we -call the operation of derivatives on annotated regular expressions $\bder$ -because it is derivatives on regular expressiones with \emph{b}itcodes), +Now we give out the central part of this lexing algorithm, +the $\bder$ function (stands for \emph{b}itcoded-derivative). +For most time we use the infix notation $(\_\backslash\_)$ +to mean $\bder$ for brevity when +there is no danger of confusion with derivatives on plain regular expressions. +For example, we write $( _{[]}r^* ) \backslash c$ instead of $\bder \;c \; _{[]}r^*$, +as the bitcodes at the front of $r^*$ indicates that it is +a bit-coded regular expression, not a plain one. +$\bder$ tells us how regular expressions can be recursively traversed, +where the bitcodes are augmented and carried around +when a derivative is taken. +\begin{center} + \begin{tabular}{@{}lcl@{}} + $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\ + $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\ + $(_{bs}{\bf d})\,\backslash c$ & $\dn$ & + $\textit{if}\;c=d\; \;\textit{then}\; + _{bs}\ONE\;\textit{else}\;\ZERO$\\ + $(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ & + $_{bs}\sum\;(\textit{map} \; (\_\backslash c) \; as )$\\ + $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ & + $\textit{if}\;\textit{bnullable}\,a_1$\\ + & &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\ + & &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\ + & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\ + $(_{bs}a^*)\,\backslash c$ & $\dn$ & + $_{bs}(\textit{fuse}\, [Z] \; r\,\backslash c)\cdot + (_{[]}r^*))$ +\end{tabular} +\end{center} +\noindent +We give the intuition behind some of the more involved cases in +$\bder$. For example, +in the \emph{star} case, +a derivative on $_{bs}a^*$ means +that one more star iteratoin needs to be taken. we need to unfold it into a sequence, and attach an additional bit $Z$ to the front of $r \backslash c$ -to indicate one more star iteration. -\begin{center} - \begin{tabular}{@{}lcl@{}} - $\bder \; c\; (_{bs}a^*) $ & $\dn$ & - $_{bs}(\textit{fuse}\, [Z] \; \bder \; c \; a)\cdot - (_{[]}a^*))$ -\end{tabular} -\end{center} +as a record to indicate one new star iteration is unfolded. \noindent -For most time we use the infix notation $\backslash$ to mean $\bder$ for brevity when -there is no danger of confusion with derivatives on plain regular expressions, -for example, the above can be expressed as \begin{center} \begin{tabular}{@{}lcl@{}} $(_{bs}a^*)\,\backslash c$ & $\dn$ & - $_{bs}(\textit{fuse}\, [Z] \; a\,\backslash c)\cdot + $_{bs}(\underbrace{\textit{fuse}\, [Z] \; a\,\backslash c}_{\text{One more iteration}})\cdot (_{[]}a^*))$ \end{tabular} \end{center} \noindent -Using the picture we used earlier to depict this, the transformation when -taking a derivative w.r.t a star is like below: +This information will be recovered later by the $\decode$ function. +The intuition is that the bit $Z$ will be decoded at the right location, +because we accumulate bits from left to right (a rigorous proof will be given +later). -\begin{tabular}{@{}l@{\hspace{1mm}}l@{\hspace{0mm}}c@{}} -\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}] - \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] +\begin{tikzpicture}[ > = stealth, % arrow head style + shorten > = 1pt, % don't touch arrow head to node + semithick % line style + ] + + \tikzstyle{every state}=[ + draw = black, + thin, + fill = cyan!29, + minimum size = 7mm + ] + \begin{scope}[node distance=1cm and 0cm, every node/.style=state] + \node (k) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] {$bs$ \nodepart{two} $a^*$ }; -%\caption{term 1 \ref{term:1}'s matching configuration} -\end{tikzpicture} -& + \node (l) [below =of k, rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] + { $bs$ + [Z] + \nodepart{two} $(a\backslash c )\cdot a^*$ }; + \end{scope} + \path[->] + (k) edge (l); +\end{tikzpicture} + +Pictorially the process looks like below. +Like before, the red region denotes +previous lexing information (stored as bitcodes in $bs$). + \begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}] - \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] - {$v_{\text{previous iterations}}$ - \nodepart{two} $a^*$}; -%\caption{term 1 \ref{term:1}'s matching configuration} -\end{tikzpicture} -\\ -\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}] - \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] + \begin{scope}[node distance=1cm] + \node (a) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] + {$bs$ + \nodepart{two} $a^*$ }; + \node (b) [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] { $bs$ + [Z] \nodepart{two} $(a\backslash c )\cdot a^*$ }; %\caption{term 1 \ref{term:1}'s matching configuration} + \end{scope} \end{tikzpicture} -& -\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}] - \node [rectangle split, rectangle split horizontal, rectangle split parts=2, rectangle split part fill={red!30,blue!20},] - {$v_{\text{previous iterations}}$ + 1 more iteration - \nodepart{two} $(a\backslash c )\cdot a^*$ }; -%\caption{term 1 \ref{term:1}'s matching configuration} -\end{tikzpicture} -\end{tabular} + \noindent Another place in the $\bder$ function where it differs from normal derivatives (on un-annotated regular expressions) @@ -474,25 +508,6 @@ The rest of the clauses of $\bder$ is rather similar to $\der$, and is put together here as a wholesome definition for $\bder$: -\begin{center} - \begin{tabular}{@{}lcl@{}} - $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\ - $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\ - $(_{bs}{\bf d})\,\backslash c$ & $\dn$ & - $\textit{if}\;c=d\; \;\textit{then}\; - _{bs}\ONE\;\textit{else}\;\ZERO$\\ - $(_{bs}\sum \;\textit{as})\,\backslash c$ & $\dn$ & - $_{bs}\sum\;(\textit{map} \; (\_\backslash c) \; as )$\\ - $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ & - $\textit{if}\;\textit{bnullable}\,a_1$\\ - & &$\textit{then}\;_{bs}\sum\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\ - & &$\phantom{\textit{then},\;_{bs}\sum\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\ - & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\ - $(_{bs}a^*)\,\backslash c$ & $\dn$ & - $_{bs}(\textit{fuse}\, [Z] \; r\,\backslash c)\cdot - (_{[]}r^*))$ -\end{tabular} -\end{center} \noindent Generalising the derivative operation with bitcodes to strings, we have \begin{center} diff -r 692911c0b981 -r 3178f0e948ac thys3/BlexerSimp.thy --- a/thys3/BlexerSimp.thy Thu Jul 21 20:22:35 2022 +0100 +++ b/thys3/BlexerSimp.thy Tue Aug 02 22:11:22 2022 +0100 @@ -303,27 +303,7 @@ apply(subgoal_tac "(cc @ a # dB6 cc' (tset (cc @ [a]))) s\* (cc @ (p6 cc a) # dB6 cc' (tset (cc @ [a])))") sorry -(* -lemma ss6_stronger_aux: - shows "(rs1 @ rs2) s\* (rs1 @ dB6 rs2 (set (map erase rs1)))" - apply(induct rs2 arbitrary: rs1) - apply simp - apply(case_tac "erase a \ erase ` set rs1") - apply(simp) - apply(drule_tac x = "rs1" in meta_spec) - apply(subgoal_tac "(rs1 @ a # rs2) s\* (rs1 @ rs2)") - using srewrites_trans apply blast - using deletes_dB apply presburger - apply(case_tac "set (turnIntoTerms (erase a)) \ erase ` set rs1") - - apply simp - apply(auto) - prefer 2 - apply(drule_tac x="rs1 @ [a]" in meta_spec) - apply(simp) - sorry -*) lemma ss6_stronger: @@ -348,6 +328,7 @@ harmless sorry *) + sorry thm seqFold.simps @@ -359,7 +340,8 @@ done -lemma tint_seqFold_eq: shows"set (tint (seqFold (erase x42) [erase x43])) = +lemma tint_seqFold_eq: shows +"set (tint (seqFold (erase x42) [erase x43])) = set (tint (SEQ (erase x42) (erase x43)))" apply(case_tac "erase x42 = ONE") apply simp @@ -377,18 +359,31 @@ -lemma top_bitcodes_preserved_p6: - shows "\ r = ASEQ bs a1 a2 \ \ p6 as r = AZERO \ (\bs3. top (p6 as r) = bs @ bs3)" - apply(induct r arbitrary: as) - apply simp - apply simp - apply simp - apply(case_tac "a1") - apply simp +lemma p6fa_aux: + shows " fuse bs + (bsimp_AALTs bs\<^sub>0 as) = + + (bsimp_AALTs (bs @ bs\<^sub>0) as)" + by (metis bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_AALTs.simps(3) fuse.simps(1) fuse.simps(4) fuse_append neq_Nil_conv) - sorry +lemma p6pfuse_alts: + shows +" \bs\<^sub>0 as\<^sub>0. + \\a bs. set (tint (erase a)) = set (tint (erase (fuse bs a))); a = AALTs bs\<^sub>0 as\<^sub>0\ + \ \ set (tint (erase a)) \ (\x\set as. set (tint (erase x))) \ + fuse bs + (case a of AZERO \ AZERO | AONE x \ AONE x | ACHAR x xa \ ACHAR x xa + | ASEQ bs r1 r2 \ bsimp_ASEQ bs (prune6 (\x\set as. set (tint (erase x))) r1 [erase r2]) r2 + | AALTs bs rs0 \ bsimp_AALTs bs (filter notZero (map (\r. prune6 (\x\set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \ ASTAR x xa) + = + (case fuse bs a of AZERO \ AZERO | AONE x \ AONE x | ACHAR x xa \ ACHAR x xa + | ASEQ bs r1 r2 \ bsimp_ASEQ bs (prune6 (\x\set as. set (tint (erase x))) r1 [erase r2]) r2 + | AALTs bs rs0 \ bsimp_AALTs bs (filter notZero (map (\r. prune6 (\x\set as. set (tint (erase x))) r []) rs0)) | ASTAR x xa \ ASTAR x xa)" + apply simp + using p6fa_aux by presburger + @@ -406,9 +401,27 @@ apply simp using tint_seqFold_eq apply simp + apply (smt (z3) bsimp_ASEQ.simps(1) bsimp_ASEQ0 bsimp_ASEQ1 bsimp_ASEQ2 fuse.simps(1) fuse.simps(5) fuse_append) + using p6pfuse_alts apply presburger + by simp + +(* +The top-level bitlist stays the same: +\<^sub>b\<^sub>sa ------pruning-----> \<^sub>b\<^sub>s\<^sub>' b \ \bs3. bs' = bs @ bs3 +*) +lemma top_bitcodes_preserved_p6: + shows "top r = bs \ p6 as r = AZERO \ (\bs3. top (p6 as r) = bs @ bs3)" + + + apply(induct r arbitrary: as) + +(*this sorry requires more care *) + sorry + + corollary prune6_preserves_fuse_srewrite: shows "(as @ map (fuse bs) [a] @ as2) s\* (as @ map (fuse bs) [p6 as a] @ as2)" apply(subgoal_tac "map (fuse bs) [a] = [fuse bs a]") @@ -567,7 +580,14 @@ case (ss6 a1 a2 rsa rsb rsc) then show ?case by (smt (verit, best) Nil_is_append_conv bmkepss1 bmkepss2 bnullable_correctness in_set_conv_decomp list.distinct(1) list.set_intros(1) nullable_correctness set_ConsD subsetD) -qed (auto) +next + prefer 10 + case (ss7 as a as1) + then show ?case + +(*this sorry requires more effort*) + sorry +qed(auto) lemma rewrites_bmkeps: assumes "r1 \* r2" "bnullable r1" @@ -606,6 +626,12 @@ shows "(map f [a]) = [f a]" by (simp) +lemma "set (tint (erase a)) \ (\x\set as. set (tint (erase x))) \ + set (tint (erase (bder c a))) \ (\x\set (map (bder c) as). set (tint (erase x)))" + + sorry + + lemma rewrite_preserves_bder: shows "r1 \ r2 \ (bder c r1) \* (bder c r2)" and "rs1 s\ rs2 \ map (bder c) rs1 s\* map (bder c) rs2" @@ -681,6 +707,11 @@ apply(rule_tac rrewrite_srewrite.ss6) using Der_def der_correctness apply auto[1] by blast +next + case (ss7 as a as1) + then show ?case + apply simp + sorry qed lemma rewrites_preserves_bder: @@ -733,18 +764,20 @@ by (metis rrewrites_trans star_seq star_seq2) then have "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 r1 r2)" by simp } - ultimately show "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 r1 r2)" sorry + ultimately show "ASEQ bs1 r1 r2 \* bsimpStrong6 (ASEQ bs1 r1 r2)" + by blast next case (2 bs1 rs) have IH: "\x. x \ set rs \ x \* bsimpStrong6 x" by fact then have "rs s\* (map bsimpStrong6 rs)" by (simp add: trivialbsimp_srewrites) also have "... s\* flts (map bsimpStrong6 rs)" by (simp add: fltsfrewrites) - also have "... s\* distinctWith (flts (map bsimpStrong6 rs)) eq1 {}" by (simp add: ss6_stronger) - finally have "AALTs bs1 rs \* AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" + also have "... s\* dB6 (flts (map bsimpStrong6 rs)) {}" by (simp add: ss6_stronger) + finally have "AALTs bs1 rs \* AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" using contextrewrites0 by auto - also have "... \* bsimp_AALTs bs1 (distinctWith (flts (map bsimpStrong6 rs)) eq1 {})" + also have "... \* bsimp_AALTs bs1 (dB6 (flts (map bsimpStrong6 rs)) {})" by (simp add: bsimp_AALTs_rewrites) - finally show "AALTs bs1 rs \* bsimpStrong6 (AALTs bs1 rs)" sorry + finally show "AALTs bs1 rs \* bsimpStrong6 (AALTs bs1 rs)" + using bsimpStrong6.simps(2) by presburger qed (simp_all)