form_test.php
inputに対しprimitive形までを出力します。
memo
①token消去…文字列に対する演算で、結果も文字列になります。
消去自体はpreg_replaceで計算されますが、その準備としてactivate_abbrが使用されます。例
{all #x #w #T . #P } = all #x\,(#x #w #T xr #P)【\(\forall{\sf xwT}.{\sf P}\)】=【\(\forall{\sf x}({\sf xwT}\Rightarrow{\sf P})\)】
↓
{all ([^ ]+) ([^ ]+) ([^{}]+) . ([^{}]+) } = all $1 ( $1 $2 $3 xr $4 )
②postfix…shunting_yard(操車場アルゴリズム)で得ます。
③prefix…parseにより入れ子配列にしてから、post_preにより得ます。
parseする際、DB tokenでカラム wordがあるもの(現状では\(, \Longrightarrow \Longleftrightarrow\)のみ)は置き換えられます。
④word消去…入れ子配列に対する演算で、結果も入れ子配列になります。
del_word0で一回の消去を試行します。@の処理は別にdel_atで試行します。
①④の計算は、変化が無くなるまで繰り返されます。
form_test.phpでは①④は途中結果も表示するように変更されています。
①の計算では消去すべきtokenを見つけたら、一度にできるだけ消去を試みます。
初期では \(,\) などはtokenとされていて、DBにその名残があります。