Прогонка условий

В компиляторе реализована возможность прогонки (#122), позволяющая во время компиляции спекулятивно вычислять некоторые вызовы функций, экономя тем самым шаги времени выполнения.

Её основу составляет алгоритм обобщённого сопоставления, который решает уравнения вида _E_ : _Le,_ где _E_ — произвольное выражение Рефала (пока поддерживаются только пассивные выражения, #230), _Le_ — L-выражение, т.е. образцовое выражение без повторных t-переменных и открытых и повторных e-переменных. На самом деле можно расширить алгоритм обобщённого сопоставления на некоторые случаи, когда _Le_ не является L-выражением. В частности, текущая реализация допускает ограниченные случаи повторных t- и e-переменных, а также может выявлять отсутствие решений для некоторых уравнений, где _Le_ может даже иметь открытые переменные. Но эти т.н. ad hoc-расширения не являются темой данной задачи.

Для вызова прогоняемой функции `` решаются уравнения вида `arg : Pi`, где `Pi` — образец i-го предложения функции `F`. Результаты решения этих уравнений — наборы подстановок — объединяются и применяются к предложению с этим вызовом. Таким образом, в сопоставлении с образцом вызывающего предложения сразу учитывается последующее сопоставление с образцом прогнанной функции.

Рассмотрим предложение вида
```Refal
P, R1 : P1 = R;
```
Что означает условие `R1 : P1`? Оно означает, что если можно сопоставить значение выражения `R1` с образцом `P1`, то вызов функции заменяется на `R`, иначе управление передаётся на следующее предложение.

«…Eсли можно сопоставить…» ≡ «…если существует решение уравнения `E : P1`, где `E` — значение выражения `R`…». Следовательно, если выражение `R1` пассивное, а `P` и `P1` — L-выражения (при этом в P1 все переменные новые), то можно условие `R1 : P1` просто решить как уравнение и применить подстановки (сужения и присваивания) к `P` и `R`.

В частности, если уравнение-условие не имеет решения, то предложение можно просто удалить.

Важные оговорки:
* `R1` — пассивное,
* `P` — L-выражение,
* `P1` — L-выражение,
* все переменные в `P1` новые.

На самом деле по каждому из пунктов можно предложить свои ad hoc расширения.

**Почему `R1` должно быть пассивным?** Пусть выражение `R1` содержит вызов функции с побочным эффектом, а уравнение `R1 : P1` не имеет решения. Тогда при выполнении предложения сначала выполнится побочный эффект функции, после чего управление передастся на следующее предложение. Но при прогонке условия предложение удалится, а значит, побочного эффекта не будет.

Следовательно, если `R1` активное, то уравнение должно разрешаться. При решении будет получен набор присваиваний переменным из `P1`, который будет применён к `R`. Некоторые из переменных получат активные значения, а значит, вызовы из `R1` и `R` перемешаются. Некоторые вызовы при этом могут выполниться неоднократно, некоторые вообще удалятся (если переменная не входит в `R`). Следовательно, необходима дополнительная проверка на переупорядочивание вызовов.

Если сопоставление не однозначно (с сужениями), то могут найтись такие значения аргумента, что они (а) сопоставимы с `P`, (б) не сопоставимы с образцами `P′`, полученными в результате подстановок сужений. А значит, в неоптимизированной программе вызовы из `R1` тоже могут потеряться. Решение уравнения должно быть однозначным.

**Почему `P` должно быть L-выражением?** Потому что применение сужений к не-L-выражению может привести либо к нарушению семантики (если `P` содержит открытые переменные) или к снижению быстродействия (если `P` содержит повторные t- или e-переменные). В #231 предлагается решение — разметка неразменных переменных, на основе их положения в образце. Иначе говоря, к образцу сужения должны применяться безопасно.

**Почему `P1` должен быть L-выражением?** Чтобы можно было решить уравнение. Опять же, если решалка уравнений в некоторых частных случаях даёт удовлетворительный результат для не-L-выражения, то почему бы и нет? В общем, `P1` должен быть таким, чтобы для него можно было решать уравнение.

**Почему переменные в `P1` должны быть новыми?** Переменные, которые входят в `P` уже находятся в области видимости и могут входить в `R1`. Следовательно, если `P` и `P1` содержат одну и ту же переменную, переменная может оказаться в уравнении и слева, и справа, чего алгоритм обобщённого сопоставления явно не ожидает. Решение: для каждой повторной переменной `v.X`, `v.Y`… в `P1` вводим переменную с новым индексом `v.X′`, `v.Y′`… и решаем уравнение вида
```
R1 (v.X) (v.Y)… : P1′ (v.X′) (v.Y′)…
```
где в `P1′` исходные переменные заменены на новые (со штрихом). Такое уравнение будет допустимым для решателя, хоть возможно и неразрешимым.

**Вывод.** Всё как обычно. Для турчинского случая ограниченного Рефала (т.е. L-выражений) всё работает прозрачно, но можно найти и кучу ad hoc вариантов.

Выше рассмотрен случай предложения с единственным условием. Он естественным образом обобщается на случай с пассивным первым условием с L-выражением в образце. Можно описать детали прогонки второго условия прежде первого, но это уже частности.

Модуль `Desugaring-UnCondition.ref` позволяет преобразовывать функции с условиями в эквивалентные функции без них. Можно убедиться (см. [алгоритм преобразования](https://github.com/bmstu-iu9/refal-5-lambda/blob/c47b82f2c188a6dbb70937f005701ed74390c219/doc/5-to-basis/Подход%20к%20преобразованию%20условий.md)), что если исходная функция содержит предложение рассмотренного вида, а к сгенерированным вспомогательным функциям приписать метку `$DRIVE`, то имеющийся алгоритм оптимизирует примерно так, как здесь описано.

Но преобразование в базисный Рефал снижает быстродействие и преобразовывать _всю_ программу ради возможности оптимизации _каких-то_ условий нерационально. Возможно, имеет смысл поэкспериментировать с преобразованием в базисный Рефал функций, где все условия пассивны (после выполнения #230 можно разрешить и активные), а все образцы (включая образцы в условиях) — L-выражения (как с повторными переменными, так и без).