Ad hoc расширения прогонки

Проблема
=======
Турчин когда-то описал прогонку функций ([Турчин, 1972](http://pat.keldysh.ru/~roman/doc/Turchin/1972-Turchin--E%27kvivalentnye_preobrazovaniya_rekursivnyx_funkcij__opisannyx_na_yazyke_Refal--ru.pdf), [Турчин, 1974](http://pat.keldysh.ru/~roman/doc/Turchin/1974-Turchin--E%27kvivalentnye_preobrazovaniya_programm_na_Refale--CNIPIASS--ru.pdf)), однако, описанный алгоритм прогонки работает только для ограниченного Рефала — базисного Рефала, в образцах которого запрещены t-переменные и открытые и повторные e-переменные (т.н. L-выражения).

Алгоритм естественно расширяется на неповторные t-переменные, поэтому далее мы будем под L-выражениями подразумевать образцы, в которых запрещены открытые e-переменные и повторные t- и e-переменные.

Прогонка для функций Рефала-5 общего вида в общем случае не разрешима. Нужен переход как минимум в формализм Рефала-4 или Рефала Плюс (последний основан на Рефале-4 и включает возможности Рефала-5 как синтаксический сахар над Рефалом-4), но и там всё не так просто. Формально в Рефале Плюс (и в Рефале-6) можно встроить тело функции на место её вызова, но теории достижения содержательной цели прогонки не сформулировано ([Романенко, 1987а](https://pat.keldysh.ru/~roman/doc/1987-Romanenko--Refal-4_-_rasshirenie_Refala-2.pdf), [Романенко, 1987б](https://pat.keldysh.ru/~roman/doc/1987-Romanenko--Progonka_dlya_programm_na_Refale-4.pdf)).

Напомним, что есть содержательная цель прогонки. Выполнение программы на Рефале в общем случае есть цепь операций синтеза (построения результатных выражений) и последующего анализа (сопоставления с образцом). В случае базисного Рефала результатные выражения строятся только для аргументов функции, для Рефала-5 операции синтеза также включают и левые части условий (см. также #248). В общем, имеем цепочку:
```
S A S A S A S A …
```
Содержательная цель прогонки — заменить участок `A′ S′ A″ S″` участком `A* S*`, где `A*` включает в себя в некотором смысле композицию анализа `A′` и `A″`, а `S*` — композицию `S′` и `S″`. Т.е. устранить необходимость в построении выражения `S′`, которое затем снова начнёт разбираться.

Так вот. Теории, позволяющей в рамках Рефала-4/Рефала Плюс полностью прогнать функцию пока не разработано. Исследования Сергея Романенко прервались на препринте [Романенко, 1987б](https://pat.keldysh.ru/~roman/doc/1987-Romanenko--Progonka_dlya_programm_na_Refale-4.pdf), где в конце так и написано:

> В заключение следует сказать, что предлагаемый набор преобразований представляет собой _исчисление,_ в то время как для выполнения преобразований с помощью компьютера необходимы _алгоритмы._ Таким образом, вопрос о том, когда и какие преобразования применять, нуждается в дополнительном рассмотрении.

Так что для полноценной прогонки нужно (а) переходить в более широкий формализм, (б) для нового формализма разрабатывать алгоритм на основе имеющегося исчисления.

Решение
======
Но если теория говорит нам, что решения в общем виде не существует (либо оно не известно), то всегда можно поискать ограниченные, но часто появляющиеся на практике частные случаи и решать задачу уже для них.

Переходить в формализм Рефала-4 на уровне промежуточного представления пока не предлагается, предлагается так и оставаться в рамках базисного Рефала с условиями, которое сейчас используется между рассахаривателем и генератором RASL’а.

На самом деле уже заложены возможности для обработки частных случаев. Так например, алгоритм обобщённого сопоставления не требует L-выражения справа, вместо этого пытается решить уравнение до тех пор, пока методы решения с L-выражениями работают. Если эти методы становятся неприменимы, возвращается признак `Undefined`, говорящий о том, что решения нет (см. #156).

Кроме того, алгоритм уже имеет некоторые простые расширения, выводящие его за рамки L-выражений. Например, обнаруживается, что уравнение `A e.X : B e.1 X e.2` решений не имеет. Если повторная переменная в правой части получила два s-значения (символы или s-переменные), то разрешается пара `SVAL′ : SVAL″` (а она всегда разрешается) независимо от типа повторной переменной. Исходный алгоритм Турчина разрешает быть повторными только s-переменным.

Турчинский алгоритм прогоняет все предложения исходной функции за раз. Реализованный алгоритм прогоняет за раз по одному предложению. Если какое-то предложение прогнать нельзя, строится вызов «остаточной» функции `Func*N`, полученной из исходной вычёркиванием первых N предложений. Это тоже ad hoc расширение, позволяющее оптимизировать функции, у которых только часть предложений относятся к ограниченному Рефалу.

Предлагаемые расширения
===================
Ревизия алгоритма обобщённого сопоставления
--------------------------------------------------------
**В первую очередь** нужно провести ревизию алгоритма обобщённого сопоставления. На данный момент он может вернуть `Undefined` там, где на самом деле можно доказать отсутствие решения. Примеры мне сейчас искать лень, позже добавлю в комментариях.

Открытые переменные в правой части уравнения
----------------------------------------------------------
Пусть у нас есть такие две функции:
```Refal
F {
Pf = Rf1 Rf2;
}

G {
Pg = Rg;
…
}
```
Тогда, если `Pf` является L-выражением, а `Pg` содержит ровно одну открытую переменную, то к `Pf` можно применить подстановку `e.X → Pg` и таким образом прогнать `G` на одно предложение (получив вызов `G*1`).

В примере аргументом функции `G` является переменная `e.X`, но случай можно обобщить и для более сложных аргументов. В общем случае, если в наборе сужений для уравнения `arg : Pg` есть только одна открытая переменная, то подстановку набора сужений в L-выражение применять безопасно.

Если в решении открытых переменных несколько, то подстановка сужений безопасна только тогда, когда их порядок не меняется. Например, здесь она безопасна:
```Refal
F {
(e.X) e.Y (e.Z) = ;
}

$DRIVE G;

G {
e.A 1 e.B (e.C 2 e.D) = e.A e.D;
}
```
Но если в вызове заменить `e.X` на `e.Z`, семантика нарушится.

Кроме того, безопасно решать уравнение вида `T1 … Tn : e.1 P e.2`, где `T1` … `Tn` — термы (символы, s-, t-переменные, скобочные термы). Можно статически перебрать все возможные удлинения переменной `e.1` и получить _упорядоченный_ набор решений. Случай на практике распространён, особенно в виде условий
```Refal
Pat, A B C D : e.B s.X e.E = Res;
```
где переменная `s.X` входит в образец. На прогонку условий есть отдельная задача #248.

Не-L-образцы в вызывающей функции
---------------------------------------------
Тема затронута в #231, там же есть примеры.

Если мы имеем не-L-образец в вызывающей функции, то можем применять сужения только к t- и e-переменным, которые (а) входят в образец один раз и (б) означиваются до цикла удлинения открытой переменной. Реализация этого расширения требует понятия неразменных переменных, предложенных в #231.

Повторные t- или e-переменные в правой части уравнения
---------------------------------------------------------------------
Будем говорить, что выражение _L-подобно,_ если стирание имён переменных обращает его в жёсткое выражение. Повторные переменные следует по-разному рассматривать в L-подобных образцах и не-L-подобных.

Текущая реализация алгоритма сначала рассматривает правую часть как жёсткое выражение, т.е. имена переменных в правой части не учитывает. Если правая часть оказалась не-L-подобной, то возвращается `Undefined` (либо «решений нет», если это удалось выявить). В противном случае в построенном наборе присваиваний находятся присваивания кратным переменным вида `E1 ← var` и `E2 ← var`, одно из присваиваний сохраняется в результате, второе стирается и решается уравнение вида `E1 : E2`.

Это уравнение, в отличие от исходного, симметрично и потенциально содержит слева и справа переменные одного сорта. В текущей реализации оно решается либо для случая, когда и `E1`, и `E2` являются s-значениями (s-переменные или символы), или дословно совпадают. Способ решения уравнения `S1 : S2` описан ещё Турчиным, он приводит либо к успеху, либо к сужению `s.X → S2`, либо к неуспеху. Второй случай, очевидно, тождество.

Поэтому первое направление ad hoc-расширений — это развитие методов решения уравнений вида `E1 : E2`.

Второе направление расширений — решение уравнений с не-L-подобной правой частью. Например, уравнений вида `E : e.X e.Y (e.Y)`. Здесь нет открытых переменных, т.к. второе вхождение закрытое, а первое — повторное. Можно ли объединить методы решения уравнений с открытыми переменными с расширенными методами решения уравнений `E1 : E2` предыдущего абзаца, чтобы решать уравнения этого вида — тут нужно разбираться.

Прогонка функций в предложениях с условиями
--------------------------------------------------------
Текущая версия эти предложения просто игнорирует. (Это неправильно, поскольку должна на самом деле остужать функции drive и inline с холодными аргументами, поскольку они могут блокировать другие функции, которые можно специализировать.)

Более продвинутое решение — нужно прогонять вызовы в первом результатном выражении (в первом условии или правой части без условий), а в остальных — только встраивать.

Но наиболее общее решение — учитывать разновидности переменных. Переменные из первого образца можно сужать, последующие — неразменные. Подробности в уже упомянутой задаче #231.

Прогонка функций с условиями
-------------------------------------
Если предложение прогоняемой функции имеет вид `Pat = Res`, то всё понятно. Сопоставляем аргумент с `Pat`, получаем набор присваиваний и сужений. Присваивания применяем к `Res`, сужения к вызывающей функции, вызов заменяем на модифицированный `Res`. Понятно, что тут тоже вагон нюансов, которые рассматрваются, например, здесь или в #230 и в #231.

Но вот если прогоняемое предложение имеет вид `Pat, Res1 : Pat1 = Res;`, становится уже сложнее. Допустим, мы решили уравнение `arg : Pat`. Что дальше? Подставить `Res1 : Pat1 = Res` на место вызова нельзя. Добавлять условие к предложению вызывающей функции? Наверное, можно в каких-то случаях, но слишком не очевидно влияние на семантику. Можно, наверное, подставить условие, если оно пассивно, но тоже надо думать.

Поэтому возможное решение — если прогоняемая функция содержит условия, то её можно при помощи `Desugaring-UnCondition` привести к набору функций без условий, каждую из которых рассматривать как прогоняемую (или встраиваемую в зависимости от типа исходной функции). Но тоже нужно проанализировать это решение на предмет деградации производительности.

Возврат условий из функции обобщённого сопоставления
--------------------------------------------------------------------
Функция обобщённого сопоставления в норме или возвращает набор пар наборов сужений и присваиваний (в том числе пустой, если решений нет), или признак невозможности сопоставления `Undefined`.

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

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

Но тут нужно понять, не будет ли оверхед на условия выше, чем отказ от подобного фокуса. Возможно, понять экспериментально.

Неразрешённые уравнения могут быть двух видов: вида `E : L`, где `E` — фрагмент аргумента, а `L` — фрагмент образца прогоняемой функции, и `E1 : E2`, где обе части — фрагменты аргумента, присвоенные повторной переменной. Для этих двух видов уравнений, очевидно, потребуются разные способы построить условие.

Замечу, что используется термин _неразрешённые_ уравнения, а не _неразрешимые._ Некоторые из уравнений могут быть разрешимы методами теории уравнений в словах, но они сложны и поэтому не будут реализовываться в компиляторе. Поэтому такая терминология.