Специализация без шаблона

[Mazdaywik]

UPD 24.10.2020: название заявки обновлено, т.к. именно это требуется в комментариях.

Мотивация

Сейчас компилятор требует, чтобы в образцах предложений специализируемой функции статические параметры соответствовали переменным того же типа. Однако, это довольно жёсткое ограничение: для некоторых содержательных функций приходится писать довольно громоздкий и корявый код.

Например, в своём недавнем письме в рассылку [email protected] я разбирал пример с интерпретатором диалекта Форта, где пришлось написать так:

$SPEC Loop e.stack (e.CODE) (e.DICT);

Loop {
  e.Stack (e.Code_) (e.Dict)
    , e.Code_
    : {
        /* empty */ = e.Stack;

        DUP e.Code
          = e.Stack : e.Stack^ t.Top
          = <Loop e.Stack t.Top t.Top (e.Code) (e.Dict)>;

        DROP e.Code
          = e.Stack : e.Stack^ t.Top
          = <Loop e.Stack (e.Code) (e.Dict)>;
        …
      }
}

Чтобы функцию можно было специализировать по e.CODE потребовалось написать одно предложение с блоком. Более естественный вариант выглядел бы так:

$SPEC Loop e.stack (e.CODE) (e.DICT);

Loop {
  e.Stack (/* empty */) (e.Dict) = e.Stack;

  e.Stack (DUP e.Code) (e.Dict)
    = e.Stack : e.Stack^ t.Top
    = <Loop e.Stack t.Top t.Top (e.Code) (e.Dict)>;

  e.Stack (DROP e.Code) (e.Dict)
    = e.Stack : e.Stack^ t.Top
    = <Loop e.Stack (e.Code) (e.Dict)>;

  …
}

Но нельзя, e.CODE здесь уточняется не в e-переменную, а в выражение.

Почему так сделано? Потому что функция, помеченная $SPEC, по сути является шаблоном, по которому строятся экземпляры, адаптированные к каждому конкретному вызову. И строятся они буквально шаблонной заменой значений статических параметров на их актуальные значения. А для шаблонной замены параметрам неизбежно должны соответствовать переменные того же типа в предложениях — на место этих переменных подставляется фактический аргумент.

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

Почему так не было сделано? Подход с возможностями прогонки требует наличия функции обобщённого сопоставления с образцом, которая может решить эту систему уравнений. Но на момент начала работ по обоим оптимизациям (прогонка #122, специализация #126) этой функциональности не было, был её ограниченный вариант, допускающий лишь успешные сопоставления. Прогонку делал Кирилл Ситников @InfiniteDisorder, специализацию — Дарья Сухомлинова @StrixSeloputo. Поскольку функция решения уравнений есть содержательная часть работы Кирилла, было решено ограничить Дарью базовым вариантом специализации.

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

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

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

• Базовый вариант — отказываться от специализации этого вызова.
• Тонкий вариант — специализация только предшествующих предложений. Для предложений, начиная с первого Undefined, генерируется как при прогонке остаточная функция Func*N, которая вызывается в неуспешном предложении. Побочный эффект: оптимизация будет увеличивать число шагов.
• Другой, ещё более тонкий вариант — динамически обобщать аргумент. Поговорим о нём подробнее.

Что значит: сопоставление не удалось разрешить? Это значит, что при решении системы получилось уравнение вида E : Le, где E — фрагмент аргумента, а Le — фрагмент образца и с этим уравнением алгоритм решения справиться не может. (Частный случай E1 : E2, возникающий при наличии двух присваиваний E1 ← var и E2 ← var можно трактовать как уравнение 〈E1, E2〉 : 〈var, var〉, не будем его подробно рассматривать.)

Уравнение вида var : Le решить в каком-то смысле можно при любом Le (при соответствии типа переменной, конечно) — его решением можно назвать сужение var → Le (но есть тонкости с переменными). Решение для системы (var1) … (varN) : (Le1) … (LeN) вида var1 → Le1, …, varN → LeN можно подставить в L-образец, если порядок переменных var1 … varN тот же, что и в системе уравнений. В том смысле, что при подстановке не должен меняться порядок следования открытых e-переменных (см. #249).

Если решатель нашёл неразрешённое уравнение E : Le (или несколько таких уравнений), то в исходном аргументе можно заменить E на новую переменную и заново выполнить прогонку. Т.е., в каком-то смысле мы часть аргумента делаем динамической.

Базовый вариант должен быть реализован в первую очередь. Любая пометка оптимизации ($DRIVE, $INLINE, $SPEC) это всего лишь совет компилятору оптимизировать функцию. Если оптимизация возможна, то она выполняется. Если нет, остаётся как есть. Такое решение в духе Си++, где ключевые слова inline и register тоже являются исключительно советами. Если программист сам написал предложение, где статические параметры в совокупности отображаются в не-L-кортеж образцов, значит он готов к тому, что функция иногда специализироваться не сможет.

Программа максимум: специализация без шаблона

Здесь предлагается специализируемые функции просто помечать ключевым словом $SPEC, например в форме $SPEC Map { … }.

Если реализована программа-минимум, то описание

$SPEC Func;

должно считаться эквивалентным

$SPEC Func e.ALL-STATIC-ARG;

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

Map [t.Func] {
  t.Next e.Rest = <Apply t.Func t.Next> <Map [t.Func] e.Rest>;
  /* empty */ = /* empty */;
}

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

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

Например, в функции

$SPEC Replace (e.FROM) (e.TO) e.text;

Replace {
  (e.From) (e.To) e.Text-B e.From e.Text-E
    = e.Text-B e.To <Replace (e.From) (e.To) e.Text-E>;

  (e.From) (e.To) e.Text = e.Text;
}

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

$SPEC Replace {
  (e.From) (e.To) e.Text-B e.From e.Text-E
    = e.Text-B e.To <Replace (e.From) (e.To) e.Text-E>;,

  (e.From) (e.To) e.Text = e.Text;
}

Test { (e.X) (e.Y) (e.Z) = <Replace ('Foo') ('Bar') e.X e.Y e.Z> }

возникнет нетривиальное уравнение e.X e.Y e.Z : e.Text-B 'Foo' e.Text-E, которое решить невозможно и придётся динамически обобщить e.X e.Y e.Z до одной переменной, скажем, e.0.

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

[Mazdaywik]

На курсовую работу предлагается реализовать программу-минимум, причём в базовом варианте. Заметим, это не препятствует реализации синтаксиса $SPEC F { … } как синтаксического сахара. Такая функция будет специализироваться, только если все её образцы являются L-выражениями.

[Mazdaywik]

Задача не была выбрана в качестве курсовой.

[Mazdaywik]

Задача не была выбрана в качестве ВКР.

[Mazdaywik]

Другой подход к специализации без шаблона

Если шаблон не задан, то его можно выводить — вычислять входной формат как ГСО образцов, и параметры, сужающиеся в переменные того же типа или (в дальнейшем) L-выражения, объявлять статическими. Дальнейшая специализация идёт обычным образом по шаблону. Так, в частности описано в #252.

Но интереснее другое: можно формировать шаблон индивидуально для каждого вызова — вычислять ГСО от образцов вызываемой функции и фактического аргумента вызова. В этом случае можно оптимизировать вызовы, которые иначе бы не оптимизировались. Например, вызов <Replace ('AAA') <F …>> для примера выше с явно заданным шаблоном (e.FROM) (e.TO) e.text не оптимизируется, однако для вызова выведется шаблон (e.S1) e.d2, с которым оптимизировать функцию можно будет.

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

Недостаток по сравнению с динамическим обобщением — снижается потенциальная глубина оптимизации, ведь иногда возможны решения и для не-L-образцов.

[Mazdaywik]

Специализировать все функции?

А почему бы и нет?

• Изначально специализация мыслилась не как «принудительная базисная конфигурация», а как «генерация специализированных функций по шаблону». Сама функция была шаблоном (в духе шаблонов C++), только значениями шаблонных параметров были не типы, а значения.

  Без шаблонов можно было бы и обойтись:

  Map [t.Func] {
    t.Next e.Rest = <Apply t.Func t.Next> <Map [t.Func] e.Rest>;
    /* empty */ = /* empty */;
  }
  

• Другая причина существования объявлений $SPEC: аналогия. Аналогия с C++, где есть оптимизируемые функции, помечаемые ключевым словом inline. Хотя, конечно, современные компиляторы C++ умеют и сами распознавать встраиваемые функции (т.е. встраивать функции без inline), и могут игнорировать это ключевое слово. Так что слово inline в некотором смысле ничего не даёт.

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

• Какие функции специализировать? Изначальная постановка задачи была тупая: создать функцию по шаблону. Если в шаблоне снова есть вызов специализируемой функции — либо найти уже имеющийся по сигнатуре, либо сгенерировать новый.

  Такой подход может привести к зацикливанию. Но при решении задачи Останавливать специализацию по отношению Хигмана-Крускала #253 специализация станет безопасной, зацикливаться никогда не будет. А значит, оптимизировать можно любую функцию.

  Как специализировать функции без шаблонов, написано выше — и в тексте заявки, и в предыдущем комментарии.

• Изначально предполагалось специализировать только рекурсивные функции (так, в частности, предлагается делать и в Автоматическая разметка оптимизируемых функций #252), поскольку эффект от оптимизации нерекурсивной функции будет менее заметен. Но позже выяснилось, что некоторые нерекурсивные функции тоже полезно специализировать (Специализация замыканий #160) — замыкания, соответствующие не только непосредственно вложенным функциям, но и присваиваниям и блокам. Они не всегда могут прогнаться (например, могут содержать не-L-выражения, активные аргументы), но специализация позволит распространить информацию далее. Примеры в Специализация замыканий #160.

• Другим аргументом против оптимизации всех функций является быстродействие. Если пытаться оптимизировать каждый вызов, то компиляция будет выполняться чертовски долго.

  Контраргумент: никто не предлагает включать этот режим по умолчанию. Для этого режима можно добавить опцию «продвинутой» специализации. А по умолчанию специализатор будет оптимизировать только явно размеченные функции, как и раньше.

  Впрочем, интересно посмотреть, какую долю вызовов в тексте программы занимают явно размеченные специализируемые функции Map, MapAccum и Reduce.

[Mazdaywik]

Соображение про динамическое обобщение

Допустим, алгоритм обобщённого сопоставления обнаружил, что сопоставление не определено и нужно обобщить некий участок левой части. Какое уравнение не решилось, знает сам алгоритм. Как он должен сообщить об этом наружу?

Предлагается между лексемами выражения (т.е. между символами, переменными, по обе стороны от каждой скобки) вставлять координаты — последовательные номера. Выражение 'A' (e.X &F (t.Y)) e.Z будет выглядеть тогда вот так:

0 (Symbol Char 'A') 1
(Brackets 2 (TkVariable 'eX') 3 (Symbol Name 'F') 4 (Brackets 5 (TkVariable 'tY') 6) 7) 8
(TkVariable 'eZ') 9

Теперь, когда сопоставление невозможно, алгоритм будет возвращать не просто Undefined, а Undefined s.Left s.Right — координаты той части, которую нужно обобщить.

Обобщение, приводящее к решению уравнения, может быть неоднозначным. Поэтому остаётся открытым вопрос: какое обобщение выбрать?

При наличии повторных t-. e-переменных мы получаем уравнение вида E1 : E2. И для успешного решения может быть достаточно обобщить или E1, или E2. Какое из них нужно обобщить?

Динамическое обобщение потребуется не только для настоящей задачи, оно также будет крайне полезно для дефорестации (#165).

[Mazdaywik]

• На данный момент при специализации проверяется дерево новой функции на абсурдность. Абсурдность здесь понимается как наличие замыканий в образцах. Оно может возникнуть, если статический параметр является повторной переменной или внутри проекций динамических параметров, или в образцах условий. Если получилась такая «абсурдная» функция, то вызов просто не специализируется. В случае динамического обобщения естественным решением будет обобщение замыкания до s-переменной.
• При специализации разумно обобщать смежные e-переменные до новых e-переменных. И сейчас, и при реализации прогонки. Сейчас — нет нужды передавать e-переменные отдельно, ведь потом они и так будут располагаться везде по соседству. Потом — усложнится прогонка, будут создаваться лишние предложения.
  Важная оговорка: сливать можно только неповторные переменные!

Оба этих соображения актуальны и для дефорестации (#165).

[Mazdaywik]

Соображения про динамическое обобщение

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

Постановка задачи на расширенную специализацию функций

Исходные данные

У нас есть специализируемая функция S и некоторый её вызов <S ARG>:

F {
  … <S ARG> …
}

S {
  Pat1 TailN;
  …
  PatN TailN;
}

Здесь Pati — образцовое выражение в начале i-го предложения, Taili — «остаток» предложения, содержащий условия и правую часть.

Для простоты будем считать, что ARG пассивный (иначе заменяем в нём вызовы функций на новые e-переменные) и множество переменных из тела S не пересекается со множеством переменных из ARG (иначе переименуем переменные в S).

Функции F и S — это функции в рассахаренном синтаксическом дереве, т.е. не содержат блоков и присваиваний, и соответственно, в аргументе ARG будут находиться не вложенные функции, а замыкания.

Идеальный случай специализации

Мы хотим построить специализированный экземпляр S′ для данного вызова, учитывающий всю статически известную информацию о вызове.

В актуальной реализации вся статически известная информация о вызове — это только выражение ARG. Конечно, оно может обогатиться в результате всяких прогонок и специализаций функции F, включая планируемую прогонку условий, но даже при обогащении оно останется выражением. Рассматривать условия как рестрикции на переменные из ARG мы не будем.

А что же тогда будет статически не известным? Значения переменных из ARG!

Таким образом, вызов будет иметь вид <S′ wrap(vars(ARG))>. vars(•) — функция, возвращающая множество переменных из ARG, перечисленных в порядке их первого появления в ARG. Упорядочивание гарантирует, что новые переменные, соответствующие вызовам, сохранят свой порядок, и что если какие-то переменные сужаются в открытые переменные в S/S′, то их порядок тоже сохранится. wrap(•) — функция, которая строит из переменных форматное выражение — s- и t-переменные перечисляет как есть, e-переменные заворачивает в скобки кроме одной.

Рассмотрим уравнение

ARG : Pati

где Pati — i-й образец функции S (i = 1…N). Его решениями будет набор пар (Ci1, Ai1), …, (Cij, Aij), …, (CiKi, AiKi), где Ki — число решений этого уравнения. Компоненты Cij будут представлять собой сужения — подстановки для vars(ARG), компоненты Aij — присваивания — подстановки для vars(Pati).

Тогда вид функции S′ можно будет описать следующим образом:

S′ {
  …
  wrap(vars(ARG)) / Cij  Taili / Aij;
  …
}

Идеал достижим не всегда

К сожалению, идеал достижим не всегда. Не для любого уравнения вида ARG : Pat существует решение в виде конечного набора пар сужение+присваивание. И что же делать?

• Самый простой вариант — отказываться от специализации таких вызовов.
• Более интересный вариант — динамическое обобщение.

Задача динамического обобщения

Если в функции S существуют такие образцы Pati, что уравнение ARG : Pati неразрешимо, то мы обобщаем ARG.

Под обобщением выражения ARG мы будем подразумевать поиск выражения ARG′ и подстановки Sg, таких, что ARG ≡ ARG′ / Sg.

Задачей динамического обобщения мы будем подразумевать поиск такого обобщения ARG′+Sg, что для всех образцов Pati функции S уравнение ARG′ : Pati разрешимо — его решение представимо в виде конечного набора пар сужение+присваивание.

При использовании динамического обобщения вызов функции S будет специализироваться по следующей схеме:

F {
  … <S′ wrap(vars(ARG′)) / Sg> …
}

S′ {
  …
  wrap(vars(ARG′)) / Cij  Taili / Aij;
  …
}

Замыкания и абсурдные функции

Объекты замыканий в образцах синтаксически и семантически недопустимы.

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

Замыкания в образцах могли возникнуть из-за того, что подстановки для статических переменных содержали замыкание и сами статические переменные находились или в динамических участках образца, или в образцах условий.

В рамках расширенной специализации никаких динамических фрагментов образца нет, образец экземпляра фактически представляет собой набор сужений, приведённый к формату. Алгоритм обобщённого сопоставления гарантирует, что сужения никогда не будут содержать объектов замыканий, т.к. он используется и при прогонке. Таким образом, нужно контролировать переменные из Pati, которые входят в образцы условий в Taili.

Список таких «беззамыкательных» переменных для каждого предложения можно подготовить заранее (хотя это преждевременная оптимизация). Далее, можно либо отдельно проверять присваивания таким переменным, или подсказать алгоритму обобщённого сопоставления, что в этих переменных замыкания запрещены. Подсказать можно, сделав их повторными в правой части уравнения. Назовём список «беззамыкательных» переменных dangvar. Тогда уравнение

ARG (e.NEW) : Pati (wrap(dangvar))

разрешимо, если переменным из dangvar не присваиваются значения с замыканиями. И если уравнение неразрешимо, то оно попросит обобщить эти замыкания. Но для этого алгоритм обобщённого сопоставления нужно существенно расширять на случай образцов общего вида в правой части (#249).

Поэтому на первом этапе проще проверять присваивания.

Выводы

Таким образом, любой вызов функции S можно будет специализировать, возможно с обобщением.

Сигнатурой экземпляра S′ будет ARG или ARG′ с нормированными именами переменных.

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

• отсутствуют символы и объекты замыканий,
• нет повторных переменных,
• нет смежных e-переменных,
• число скобок на единицу меньше числа e-переменных.

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

Соображение по выбору обобщения

Нам нужно найти обобщение ARG′ такое, что уравнение ARG′ : Pati разрешимо для любого образца функции S. Как его найти?

Предлагается последовательно сопоставлять ARG с каждым из образцов до тех пор, пока не найдётся уравнение, требующего обобщения в левой части. Обобщение нашли, заменили ARG на ARG′, повторяем процедуру. Повторяем процедуру до тех пор, пока не найдётся обобщение, удовлетворяющее все образцы.

Предложенный алгоритм может давать неоптимальный результат, т.к. обобщение неоднозначное. Навскидку привести пример мне здесь сложно, но это аналогично тому, как если бы мы искали обобщение образцов, обобщая их попарно. Обобщили первый со вторым, третий с обобщением первых двух и т.д. Результат может не быть даже ЛСО.

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

Динамическое обобщение в расширенном сопоставлении с образцом

Функция обобщённого сопоставления решает уравнение вида E : P, где E — некоторое выражение, а P — некоторый образец. Решение представляется в виде конечного набора пар сужения+присваивания (в том числе и пустого, когда у уравнения решений нет).

Уравнение E : P может быть неразрешимо, т.е. не иметь представления в виде конечного набора пар подстановок.

Задачей динамического обобщения при сопоставлении с образцом является поиск обобщения E′+Sg для E такого, что E′ : P разрешимо.

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

В процессе решения уравнения формируется система уравнений вида

E1 : P1
…
Ek : Pk

где Ei и Pi соответствуют каким-то участкам в E и P соответственно. При решении переменные из Ei могут сужаться (например, e.X заменится на t.1 e.2), но при этом всегда можно помнить, «откуда родом» этот участок. Я не буду здесь подробно останавливаться на этом механизме, это чисто техническая проблема. Важно то, что левым частям системы соответствуют какие-то участки в исходном выражении E.

При планируемой расширенной поддержке повторных переменных (#249) также потребуется уравнения вида

E1 = E2

где E1 и E2 — фрагменты E, E1 и E2 могут быть выражениями произвольного вида. Для таких фрагментов также можно отслеживать их координаты обеих частей уравнения.

Далее уравнения первого типа (выражение с образцом) мы будем записывать через двоеточие, второго типа (выражение с выражением, повторные переменные) через знак равенства.

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

• Уравнения запрещённого вида — это уравнения, которые или решатель сейчас решать не умеет, или уравнения, дающие абсурдный результат. Примеры:

  • var : … {{ &F … }} … — формально должно построиться сужение вида var → … {{ … }} …, но сужения с замыканиями запрещены. Сужения применяются к образцу, а в образце недопустимы объекты замыканий.
  • E : e.B P e.E — открытые переменные мы решать пока не умеем. Рецепт из  препринта Романенко относится к Рефалу-4, в Рефале-5(λ) его можно применять очень ограниченно. Т.е. некоторые открытые переменные разрешить можно, а некоторые — нет.

• Уравнения, зацикливающие решатель могут возникнуть только при полноценной прогонке повторных переменных (т.к. уравнения вида E : P на каждом шаге уменьшают P). На данный момент они относятся к первому типу, т.к. решатель распознаёт только крайне узкий набор уравнений вида E1 = E2, которые априори разрешимы. Более продвинутый решатель может зацикливаться, например, на

  • A e.X = e.X A.

  Его решением будет бесконечный набор сужений e.X → ε, e.X → A, e.X → A A…, поскольку в текущей реализации переменная сужаться должна ровно один раз.

  (На самом деле, решение этого уравнения можно представить и в конечном виде. Первое решение: e.X → ε. Второе решение с тривиальным сужением e.X → e.1 и парой условий-сужений , e.1 : A e.2, e.1 → e.2 A. Но второе решение непредставимо в рамках принятого формализма, а также общий метод получения решений такого вида мне не очевиден.)

С запрещёнными уравнениями всё просто. Видим «неправильное» уравнение, прерываем процесс решения с возвратом признака обобщения. Но вот что делать с зацикливающими уравнениями? По внешнему виду они не всегда различимы.

Возможный подход к решению зацикливающих уравнений заключается в обнаружении зацикливания при помощи отношения Хигмана-Крускала. При решении системы уравнений мы храним историю решения. Если следующая система опасно похожа на одну из предыдущих, то процесс решения прерываем, а участки выражения, соответствующие левым частям уравнений, обобщаем.

[Mazdaywik]

В пред-предыдущем комментарии основная идея описана. Переформулирую её в псевдокоде. Сначала несколько цитат из предыдущего комментария.

Исходные данные

У нас есть специализируемая функция S и некоторый её вызов <S ARG>:

F {
  … <S ARG> …
}

S {
  Pat1 TailN;
  …
  PatN TailN;
}

Здесь Pati — образцовое выражение в начале i-го предложения, Taili — «остаток» предложения, содержащий условия и правую часть.

Для простоты будем считать, что ARG пассивный (иначе заменяем в нём вызовы функций на новые e-переменные) и множество переменных из тела S не пересекается со множеством переменных из ARG (иначе переименуем переменные в S).

Функции F и S — это функции в рассахаренном синтаксическом дереве, т.е. не содержат блоков и присваиваний, и соответственно, в аргументе ARG будут находиться не вложенные функции, а замыкания.

Идеальный случай специализации

Мы хотим построить специализированный экземпляр S′ для данного вызова, учитывающий всю статически известную информацию о вызове.

В актуальной реализации вся статически известная информация о вызове — это только выражение ARG. Конечно, оно может обогатиться в результате всяких прогонок и специализаций функции F, включая планируемую прогонку условий, но даже при обогащении оно останется выражением. Рассматривать условия как рестрикции на переменные из ARG мы не будем.

А что же тогда будет статически не известным? Значения переменных из ARG!

Таким образом, вызов будет иметь вид <S′ wrap(vars(ARG))>. vars(•) — функция, возвращающая множество переменных из ARG, перечисленных в порядке их первого появления в ARG. Упорядочивание гарантирует, что новые переменные, соответствующие вызовам, сохранят свой порядок, и что если какие-то переменные сужаются в открытые переменные в S/S′, то их порядок тоже сохранится. wrap(•) — функция, которая строит из переменных форматное выражение — s- и t-переменные перечисляет как есть, e-переменные заворачивает в скобки кроме одной.

Рассмотрим уравнение

ARG : Pati

где Pati — i-й образец функции S (i = 1…N). Его решениями будет набор пар (Ci1, Ai1), …, (Cij, Aij), …, (CiKi, AiKi), где Ki — число решений этого уравнения. Компоненты Cij будут представлять собой сужения — подстановки для vars(ARG), компоненты Aij — присваивания — подстановки для vars(Pati).

Тогда вид функции S′ можно будет описать следующим образом:

S′ {
  …
  wrap(vars(ARG)) / Cij  Taili / Aij;
  …
}

Идеал достижим не всегда

К сожалению, идеал достижим не всегда. Не для любого уравнения вида ARG : Pat существует решение в виде конечного набора пар сужение+присваивание. И что же делать?

• Самый простой вариант — отказываться от специализации таких вызовов.
• Более интересный вариант — динамическое обобщение.

Задача динамического обобщения

Если в функции S существуют такие образцы Pati, что уравнение ARG : Pati неразрешимо, то мы обобщаем ARG.

Под обобщением выражения ARG мы будем подразумевать поиск выражения ARG′ и подстановки Sg, таких, что ARG ≡ ARG′ / Sg.

Задачей динамического обобщения мы будем подразумевать поиск такого обобщения ARG′+Sg, что для всех образцов Pati функции S уравнение ARG′ : Pati разрешимо — его решение представимо в виде конечного набора пар сужение+присваивание.

При использовании динамического обобщения вызов функции S будет специализироваться по следующей схеме:

F {
  … <S′ wrap(vars(ARG′)) / Sg> …
}

S′ {
  …
  wrap(vars(ARG′)) / Cij  Taili / Aij;
  …
}

Алгоритм в псевдокоде

Входные данные: вызов <S ARG>, функция S { …Pati Taili;… }, текущая история History.
Выходные данные: новый вызов <S@n ARG′>, экземпляр S@n { … }, история экземпляра History′. Последние два значения могут отсутствовать.

def SpecCall(<S ARG>, S { Pat1 Tail1; …; PatN TailN; }, History): ‹<S′ ARG′>, (S′ { … },History′)›
    ‹ARG*, Sg› := ExtractCalls(ARG);
    i := 1
    sols := []
    // ищем динамическое обобщение для аргумента и образцов
    while i <= N:
        ‹sol′, Sg′, expr′› := SOLVE_SPEC(ARG*, Pi)
        if Sg′ ≠ ∅:
            Sg := { (E / Sg ← v) | (E ← v) ∈ Sg′ }
            ARG* := expr′
            sols := ∅
            i := 1
        else:
            sols += [sol′]
            i += 1

    loop:
        // тривиальная сигнатура
        if ARG* == e.X:
            return ‹<S ARG>, ∅›

        // проверяем, известна ли сигнатура
        sig = PrepareSignature(S, ARG*)
        if S@j := FindSignature(sig):
            return ‹<S@j, wrap(vars(ARG*)) / Sg>, ∅›

        // проверяем на зацикливание
        if sig′ := StopRelation(sig, History):
            gen_sig := GlobalGen(sig, sig′)
            Sg′ := GenericMatch(ARG*, gen_sig)
            ARG* := gen_sig
            Sg := { (E / Sg ← v) | (E ← v) ∈ Sg′ }
        else:
            sentences := []
            for i := 1 to N:
                for (C, A) ∈ sols[i]:
                    sentences += [wrap(vars(ARG*)) / C  Taili / A;]
            instance := S@NEW {
              sentences
            }
            History′ := History ++ sig
            return ‹<S@NEW wrap(vars(ARG*)) / Sg>, (instance, History′)›

Как-то так. Если есть вопросы, пишите в комментариях.

Изменения структур данных

Потребуется изменить следующие структуры данных:

-   t.Signature ::= ((e.InstanceName) t.StaticVarVals*)
-   t.StaticVarVals ::= (e.Expression)
+   t.Signature ::= ((e.InstanceName) e.Expression)
   e.InstanceName ::= e.Name
   e.Histories ::= ((e.InstanceName) e.History)*
-   e.History ::= ((e.FuncName) t.StaticVarVals*)*
+   e.History ::= ((e.FuncName) e.Expression)*

Переписать потребуется только функции TrivialHistory и SpecCall. Причём TrivialHistory допустимо переписать так, чтобы она возвращала пустую историю. Либо (что более предпочтительно) шаблон специализации.

TrivialHistory {
  e.Name (e.Pattern)
    = (<AddSuffix e.Name ('@' 0)>)
      e.Pattern
    : e.HistoryRecord
    = ((e.Name) (e.HistoryRecord));
}

[VladisP]

Некоторые важные замечания

1. Из пред-предыдущего комментария нужно также учитывать параграф про замыкания и абсурдные функции. В частности, ARG (e.NEW) : Pati (wrap(dangvar))
2. После положительной проверки на зацикливание нужно заново искать динамическое обобщение для аргумента и образцов (вызывать SOLVE_SPEC)
3. При поиске динамического обобщения для аргумента и образцов более правильно работать с подстановками будет так: Sg := Sg ∪ { (E / Sg ← v) | (E ← v) ∊ Sg′ }
4. При положительной проверке на зацикливание перед вызовом GenericMatch нужно присвоить индексы переменным из gen_sig

[Mazdaywik]

Специализация без шаблона была необходимым условием для #314.