Основная идея — условие превращается во вспомогательную функцию, которая
проверяет, собственно, условие, и, если оно не выполняется, передаёт управление
следующим предложениям:

    F {
      . . .
      Pat1, ResC1: PatC1 = Res1;
      Pat2 = Res2;
      . . .
    }

    ↓ ↓ ↓

    F {
      . . .
      Pat1 = <F_check [перем] ResC1>;
      e.X = <F_cont e.X>;
    }

    F_check {
      [перем] PatC1 = Res1;
      [перем] e.Other = <F_cont Pat1>;
    }

    F_cont {
      Pat2 = Res2;
      . . .
    }

Здесь `F_check` — функция проверки условия, `F_cont` — функция-«континуация»,
образованная из предложений, следующих за условием. Континуация вводится
тольлко для упрощения и избежания дублирования кода. Как `[перем]` обозначен
набор переменных, присутствовавших в образце.

Интересно становится, если образец перед условием содержит открытые e-переменные.

    F {
      . . .
      PL1 e.A s.B e.C PR1, ResC1: PatC1 = Res1;
      Pat2 = Res2;
      . . .
    }

Здесь как `PL1` и `PR1` обозначены фрагменты образца, которые могут содержать
несбалансированные скобки. Также в этом примере будем полагать, что открытая
e-переменная здесь только одна. Первый шаг преобразований известен: континуация
и вызов функции проверки:

    F {
      . . .
      PL1 e.A e.C PR1 = <F_check [перем] ResC1>;
      e.X = <F_cont e.X>;
    }

    F_cont {
      Pat2 = Res2;
      . . .
    }

(Здесь мы полагаем, что открытая переменная имеет общий вид `e.A e.C`.
Вместо `e.C` здесь может находиться любой жёсткий образец.)

А что же функция проверки? С первым предложением понятно:

    F_check {
      [перем] PatC1 = Res1;
      [перем] e.Other = А тут чего?
    }

В случае фейла нужно как-то осуществить откат — попробовать новое
сопоставление:

    F_check {
      [перем] PatC1 = Res1;
      [перем] e.Other = <F_forward PL1 (e.A) e.C PR1>;
    }

    F_forward {
      PL1 (e.A_fix) t.A_next e.A_rest PR1
        = <F_next PL1 (e.A_fix t.A_next) e.A_rest PR1>;

      PL1 (e.A) PR1 = <F_cont PL1 e.A PR1>;
    }

    F_next {
      PL1’ (e.A_fix) e.A_var e.C PR1’ = <F_check [перем’] ResC1’>;
      PL1  (e.A_fix) e.A_rest    PR1  = <F_cont PL1 e.A_fix e.A_rest PR1>;
    }

Функция `F_forward` осуществляет продвижение открытой e-переменной на один терм
вперёд. Если это не удаётся, то восстанавливается аргумент функции и управление
передаётся на континуацию.

Функция `F_next` осуществляет сопоставление с уже «продвинутой» открытой
переменной. Вместо `e.A`, которая была в исходной программе, здесь фигурируют
две переменные — фиксированная `e.A_fix` и переменная `e.A_var`. Апострофы
в частях `PL1’`, `PR1’`, `ResC1’` символизируют выполненную подстановку
`e.A → e.A_fix e.A_var`.

Рассмотрим случай нескольких открытых e-переменных на конкретном примере.

    F {
      /* E0 */
      (e.A (e.B (e.A e.B) e.C) e.D) (e.E e.E e.F)
        , <G (e.A) (e.B) (e.E)> : Ok
        = Ok;

      Other = Fail;
    }

Результат преобразования может выглядеть примерно так:

    F {
      /* E0 */
      (e.A (e.B (e.A e.B) e.C) e.D) (e.E e.E e.F)
        = <F_check
            (e.A) (e.B) (e.C) (e.D) (e.E) (e.F)
            <G (e.A) (e.B) (e.E)>
          >;

      e.Other = <F_cont e.Other>;
    }

    F_cont {
      Other = Fail;
    }

    F_check {
      (e.A) (e.B) (e.C) (e.D) (e.E) (e.F) Ok
        = Ok;

      (e.A) (e.B) (e.C) (e.D) (e.E) (e.F) e.Other
        = <F_forward_1
            /* E1 */
            ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E) e.E e.F)
          >;
    }

    F_forward_1 {
      /* E2 */
      ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix) t.E_next e.E_rest)
        = <F_next_1
            /* E3 */
            ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix t.E_next) e.E_rest)
          >;

      /* E4 */
      ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix))
        = <F_forward_2
            /* E5 */
            ((e.A) ((e.B) (e.A e.B) e.C) e.D) (e.E_fix)
          >;
    }

    F_next_1 {
      /* E6 */
      ((e.A) ((e.B) (e.A e.B) e.C) e.D)
      ((e.E_fix) e.E_var e.E_fix e.E_var e.F)
        = <F_check
            (e.A) (e.B) (e.C) (e.D) (e.E_fix e.E_var) (e.F)
            <G (e.A) (e.B) (e.E_fix e.E_var)>
          >;

      /* E7 */
      ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix) e.E_rest)
        = <F_forward_2
            /* E8 */
            ((e.A) ((e.B) (e.A e.B) e.C) e.D) (e.E_fix e.E_rest)
          >;
    }

    F_forward_2 {
      /* E9 */
      ((e.A) ((e.B_fix) t.B_next e.B_rest) e.D) (e.E_rest)
        = <F_next_2
            /* E10 */
            ((e.A) ((e.B_fix t.B_next) e.B_rest) e.D) (e.E_rest)
          >;

      /* E11 */
      ((e.A) ((e.B_fix)) e.D) (e.E_rest)
        = <F_forward_3
            /* E12 */
            ((e.A) (e.B_fix) e.D) (e.E_rest)
          >;
    }

    F_next_2 {
      /* E13 */
      ((e.A) ((e.B_fix) e.B_var (e.A e.B_fix e.B_var) e.C) e.D) (e.E e.E e.F)
        = <F_check
            (e.A) (e.B_fix e.B_var) (e.C) (e.D) (e.E) (e.F)
            <G (e.A) (e.B_fix e.B_var) (e.E)
          >;

      /* E14 */
      ((e.A) ((e.B_fix) e.B_rest) e.D) (e.E_rest)
        = <F_forward_3
            /* E15 */
            ((e.A) (e.B_fix e.B_rest) e.D) (e.E_rest)
          >;
    }

    F_forward_3 {
      /* E16 */
      ((e.A_fix) t.A_next e.A_rest) (e.E_rest)
        = <F_next_3
            /* E17 */
            ((e.A_fix t.A_next) e.A_rest) (e.E_rest)
          >;

      /* E18 */
      ((e.A_fix)) (e.E_rest)
        = <F_cont
            /* E19 */
            (e.A_fix) (e.E_rest)
          >;
    }

    F_next_3 {
      /* E20 */
      ((e.A_fix) e.A_var (e.B (e.A_fix e.A_var e.B) e.C) e.D) (e.E e.E e.F)
        = <F_check
            (e.A_fix e.A_var) (e.B) (e.C) (e.D) (e.E) (e.F)
            <G (e.A_fix e.A_var) (e.B) (e.E)
          >;

      /* E21 */
      ((e.A_fix) e.A_rest) (e.E_rest)
        = <F_cont
            /* E22 */
            (e.A_fix e.A_rest) (e.E_rest)
          >;
    }

Функция `F_check` осуществляют проверку условия для каждой из стадий процесса,
`F_forward_1` и `F_next_1` осуществляют удлинение последней сопоставленной
открытой e-переменной (`e.E`), `F_forward_2`, `F_next_2` — предпоследней `e.B`,
`F_forward_3`, `F_next_3` — самой первой `e.A`. Семейство функций `F_forward_N`
осуществляет продвижение на один терм зафиксированной части удлиняемой
переменной, семейство `F_next_N` — ищет сопоставление при данном удлинении
и выполняет проверку. Если сопоставить остаток выражения при данном положении
зафиксированных переменных возможно, то выполняется проверка (`F_check`),
в противном случае — пытаемся удлинить предыдущую переменную.

В процессе преобразований у нас получилось 22 новых выражения (`E0` — старое):

    E0:  (e.A (e.B (e.A e.B) e.C) e.D) (e.E e.E e.F)
    E1:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E) e.E e.F)

    E2:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix) t.E_next e.E_rest)
    E3:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix t.E_next) e.E_rest)
    E4:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix))
    E5:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) (e.E_fix)
    E6:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix) e.E_var e.E_fix e.E_var e.F)
    E7:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) ((e.E_fix) e.E_rest)
    E8:  ((e.A) ((e.B) (e.A e.B) e.C) e.D) (e.E_fix e.E_rest)

    E9:  ((e.A) ((e.B_fix) t.B_next e.B_rest) e.D) (e.E_rest)
    E10: ((e.A) ((e.B_fix t.B_next) e.B_rest) e.D) (e.E_rest)
    E11: ((e.A) ((e.B_fix)) e.D)                   (e.E_rest)
    E12: ((e.A) (e.B_fix) e.D)                     (e.E_rest)
    E13: ((e.A) ((e.B_fix) e.B_var (e.A e.B_fix e.B_var) e.C) e.D) (e.E e.E e.F)
    E14: ((e.A) ((e.B_fix) e.B_rest) e.D)          (e.E_rest)
    E15: ((e.A) (e.B_fix e.B_rest) e.D)            (e.E_rest)

    E16: ((e.A_fix) t.A_next e.A_rest) (e.E_rest)
    E17: ((e.A_fix t.A_next) e.A_rest) (e.E_rest)
    E18: ((e.A_fix))                   (e.E_rest)
    E19: (e.A_fix)                     (e.E_rest)
    E20: ((e.A_fix) e.A_var (e.B (e.A_fix e.A_var e.B) e.C) e.D) (e.E e.E e.F)
    E21: ((e.A_fix) e.A_rest)          (e.E_rest)
    E22: (e.A_fix e.A_rest)            (e.E_rest)

Чтобы понять, каким образом образуются все эти выражения, и, соответственно, как
построить функции `F_forward_N` и `F_next_N`, рассмотрим процесс [сопоставления
с образцом][1] исходного выражения. Операции сопоставления жёстких элементов
(термов, скобок, s-, t- и повторных переменных), во-первых, всегда однозначны,
во-вторых, их относительный порядок сопоставления не важен. Поэтому будем
рассматривать только этапы сопоставления открытых e-переменных. Знаками `[[…]]`
будем окружать ещё не проанализированные фрагменты. Tекущую сопоставляемую
e-переменную будем заключать в фигурные скобки. Открытые e-переменные,
сопоставленные ранее, будем окружать угловыми скобками.

       [[(   e.A   (   e.B   (e.A e.B) e.C  ) e.D  ) (   e.E   e.E e.F  )]]

    S6:  ([[{e.A}  (   e.B   (e.A e.B) e.C  ) e.D]]) ([[ e.E   e.E e.F]])
    S5:  (  {e.A}[[(   e.B   (e.A e.B) e.C  ) e.D]]) ([[ e.E   e.E e.F]])

    S4:  (  <e.A>  ([[{e.B}  (e.A e.B) e.C]]) e.D  ) ([[ e.E   e.E e.F]])
    S3:  (  <e.A>  (  {e.B}[[(e.A e.B) e.C]]) e.D  ) ([[ e.E   e.E e.F]])

    S2:  (  <e.A>  (  <e.B>  (e.A e.B) e.C  ) e.D  ) ([[{e.E}  e.E e.F]])
    S1:  (  <e.A>  (  <e.B>  (e.A e.B) e.C  ) e.D  ) (  {e.E}[[e.E e.F]])

    S0:  (  <e.A>  (  <e.B>  (e.A e.B) e.C  ) e.D  ) (  <e.E>  e.E e.F  )

Фрагменты, ограниченные `[[…]]`, будем называть дырками, переменные, окружённые
фигурными скобками, будем называть активными переменными. На стадиях S2, S4, S6
дырки будем именовать по открытым переменным внутри них. Открытые переменные
дырок (здесь это `e.A`, `e.B` и `e.E`) будем называть представителями дырок.
Если представитель дырок активный, дырку также будем называть активной.

Выражение E1 получается окружением всех открытых (`<…>`) переменных в S0
круглыми скобками.

Выражения E2, E9, E16 получаются из состояний S2, S4, S6 заменой активной дырки
с представителем `e.X` на `(e.X_fix) t.X_next e.X_rest`, остальных дырок
на переменные `e.Y_rest`, где `e.Y` — представитель дырки.

Выражения E3, E10, E17 получаются аналогично E2, E9, E16 с немного другой
заменой активных дырок (на `(e.X_fix t.X_next) e.X_rest`).

Аналогично предыдущим, заменяются E4, E11, E18 и E5, E12, E19.

Выражения E6, E13, E20 получаются путём замены в S1, S3, S5 активных переменных
вида `e.X` на `(e.X_fix) e.X_var`, а также подстановки `e.X → e.X_fix e.X_var`
в дырках, где фигурируют эти переменные. Последняя подстановка распространяется
и на правую часть предложения, где осуществляется вызов функции `F_check`
(правая часть та же, что и в преобразованной «корневой» `F`, но с упомянутой
подстановкой).

Выражения E7, E14, E21 и E8, E15, E22 строятся из S2, S4, S6 по аналогии
с E2—E5, E9—E12, E16—E19.

Попробуем обобщить генерацию выражений. Обозначим шаблоны, по которым
создаются E2—E8, E9—E15, E16—E22 как T1—T7. Шаблон для E1 обозначим как T0.
Стадии S6, S4, S2 будем называть первыми полуэтапами, S5, S3, S1 — вторыми
полуэтапами. Стадию S0 назовём финальным этапом (он совпадает с исходным
выражением за исключением разметки открытых переменных).

Шаблон **T0** образуется из финального этапа путём окружения открытых
переменных в скобки.

В **T1…T4, T6, T7** все неактивные дырки первого полуэтапа с представителями
`e.Y` заменяются на переменную `e.Y_rest`. Активные дырки в каждом из этих
шаблонов заменяются по-своему (далее, `e.X` — представитель дырки):

* **T1**: `(e.X_fix) t.X_next e.X_rest`
* **T2**: `(e.X_fix t.X_next) e.X_rest`
* **T3**: `(e.X_fix)`
* **T4**: `e.X_fix`
* **T6**: `(e.X_fix) e.X_rest`
* **T7**: `e.X_fix e.X_rest`

Шаблон **T5** строится из выражения первого полуэтапа, в котором активное
вхождение открытой e-переменной `e.X` заменяется на `(e.X_fix) e.X_var`, прочие
её вхождения (они будут внутри дырок и в правой части соответствующего
предложения) — на `e.X_fix e.X_var`. Заметим, что в отличие от других шаблонов,
здесь заменяются не дырки, а сами переменные.

С выражениями разобрались. Теперь нужно разобраться с шаблонами функций.
Перепишем преобразованный код (функцию `F` и функции `F_***`), заменяя выражения
на `Ex[Ty]`, где Ex и Ty — краткая ссылка на выражение и номер шаблона.

    F {
      E0 = <F_check [перем] [рез]>;
      e.Other = <F_cont e.Other>;
    }

    F_cont {
      Other = Fail;
    }

    F_check {
      [перем] Ok = Ok;
      [перем] e.Other = <F_forward_1 E1[T0]>;
    }

    F_forward_1 {
      E2[T1] = <F_next_1 E3[T2]>;
      E4[T3] = <F_forward_2 E5[T4]>;
    }

    F_next_1 {
      E6[T5] = <F_check [перем|e.E→e.E_fix e.E_var] [рез|e.E→e.E_fix e.E_var]>;
      E7[T6] = <F_forward_2 E8[T7]>;
    }

    F_forward_2 {
      E9[T1] = <F_next_2 E10[T2]>;
      E11[T3] = <F_forward_3 E12[T4]>;
    }

    F_next_2 {
      E13[T5] = <F_check [перем|e.B→e.B_fix e.B_var] [рез|e.B→e.B_fix e.B_var]>;
      E14[T6] = <F_forward_3 E15[T7]>;
    }

    F_forward_3 {
      E16[T1] = <F_next_3 E17[T2]>;
      E18[T3] = <F_cont E19[T4]>;
    }

    F_next_3 {
      E20[T5] = <F_check [перем|e.A→e.A_fix e.A_var] [рез|e.A→e.A_fix e.A_var]>;
      E21[T6] = <F_cont E22[T7]>;
    }

Здесь `[перем]` и `[рез]` обозначают, соответственно, список переменных образца
(при этом e-переменные заключаются в скобки) и результатное выражение условия.
`[перем|v→e]` и `[рез|v→e]` означают применение указанной подстановки — замены
переменной на соответствующее выражение.

Следовательно, для функций общий шаблон получается таким. Исходная функция вида

    F {
       [предложения без условий]
       Pat, ResC : PatC [остаток предложения];
       [последующие предложения]
    }

будет преобразовываться в семейство функций вида, здесь K — номер очередной
открытой переменной (в обратном порядке: 1 — последняя сопоставленная,
N — первая сопоставленная).

    F {
      [предложения без условий]
      Pat = <F_check vars(Pat) ResC>;
      e.Other = <F_cont e.Other>;
    }

    F_cont {
      [последующие предложения]
    }

    F_check {
      [перем] PatC [остаток предложения];
      [перем] e.Other = <F_forward_1 T0(Pat)>;
    }

    . . .

    F_forward_K {
      T1(Pat, K) = <F_next_K T2(Pat, K)>;
      T3(Pat, K) = <F_forward_K+1 T4(Pat, K)>;
    }

    F_next_K {
      T5(Pat, K)
        = <F_check
            vars(Pat) | e.K → e.K_fix e.K_var
            ResC | e.K → e.K_fix e.K_var
          >;

      T6(Pat, K) = <F_forward_K+1 T7(Pat, K)>;
    }

Здесь `Ty(Pat, K)` — применение шаблона Ty к K-й стадии сопоставления. Функция
`F_forwark_N+1` (где N — число переменных) является синонимом для `F_cont`.
Так что если образец в условии не содержит открытых переменных (N = 0), вызов
`F_forward_1` в `F_check` будет просто вызовом `F_cont`, как и описывалось
в начале документа.

`[остаток предложения]` и `[последующие предложения]` также могут содержать
условия, поэтому к функциям `F_cont` и `F_check` нужно будет рекурсивно
повторить этот алгоритм. Остальные функции не выходят за пределы Базисного
Рефала.

[1]: http://refal.ru/chap2_r5.html
