mazeppa
v0.4.3
Supercompilation 1 -это метод преобразования программы, который символически оценивает данную программу с значениями времени выполнения как неизвестные. При этом он обнаруживает шаблоны выполнения исходной программы и синтезирует их в автономные функции; Результатом суперкомпиляции является более эффективная остаточная программа. С точки зрения трансформационной власти, суперкомпиляция подчиняется как вырубку , так и частичной оценке 3 , и даже демонстрирует определенные возможности доказывания теоремы.
Mazeppa -это современный суперкомпилер, предназначенный для того, чтобы стать целью компиляции для функциональных языков по вызову. Стабильно сравнивая и пересмотренные суперкомпильщики.
Во -первых, приготовьте систему OCAML на своей машине:
$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup
Затем установите Mazeppa в качестве пакета opam :
$ opam install mazeppa
Тип mazeppa --help для подтверждения установки.
В качестве альтернативы, вы можете клонировать репозиторий и установить Mazeppa вручную:
$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh
Flambda - мощная программа Inliner и Specializer для OCAML. Если вы создаете Mazeppa с компилятором с поддержкой Flambda OCAML, вы можете увидеть гораздо лучшую производительность. Чтобы настроить:
$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)
(Вы можете использовать другую версию вместо 5.2.0 , если хотите.)
Чтобы проверить, была ли Flambda успешно включена, запустите:
$ ocamlopt -config | grep flambda
Вы можете поиграть с Mazeppa, не устанавливая ее. Установленная OCAML и клонирован репозитория (как указано выше), запустите следующую команду из корневого каталога:
$ ./scripts/play.sh
(Graphviz требуется: sudo apt install graphviz .)
Это запустит Mazeppa с --inspect на playground/main.mz и визуализирует график процесса в target/graph.svg . Последнее может быть просмотрено в коде VS с помощью расширения предварительного просмотра SVG.
./scripts/play.sh автоматически перекомпиляет источники в OCAML, если что -то изменится.
Лучший способ понять, как работает суперкомпиляция, - это пример. Рассмотрим следующую функцию, которая принимает список и вычисляет сумму его квадратных элементов:
[ examples/sum-squares/main.mz ]
main(xs) := sum(mapSq(xs));
sum(xs) := match xs {
Nil() -> 0i32,
Cons(x, xs) -> +(x, sum(xs))
};
mapSq(xs) := match xs {
Nil() -> Nil(),
Cons(x, xs) -> Cons(*(x, x), mapSq(xs))
};
Эта программа написана в идиоматическом, листинном функциональном стиле. Каждая функция делает только одну вещь, и делает это хорошо. Тем не менее, здесь существует серьезная проблема: mapSq по существу строит список, который будет немедленно деконструирован по sum , что означает, что мы 1) нам нужно выделить дополнительную память для промежуточного списка, и 2) нам нужно два прохода вычислений вместо одного. Решение этой проблемы называется вырубкой леса 2 , которое является особым случаем суперкомпиляции.
Посмотрим, что Mazeppa делает с этой программой:
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
Флаг --inspect говорит Mazeppa дать подробный отчет о процессе преобразования. sum-squares/target/ каталог будет содержать следующие файлы:
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dot содержит полный график процесса для нашей программы. Вы можете получить изображение графика, используя dot -Tsvg target/graph.dot > target/graph.svg .nodes.json содержит содержание всех узлов на графике. Без этого файла вы не сможете многое понять только с графика.program.json содержит первоначальную программу в Mazeppa IR : наш суперкомпилер работает с этим конкретным представлением вместо оригинальной программы.output.mz содержит окончательную остаточную программу. output.mz будет содержать следующий код:
[ examples/sum-squares/target/output.mz ]
main(xs) := f0(xs);
f0(xs) := match xs {
Cons(x, xs') -> +(*(x, x), f0(xs')),
Nil() -> 0i32
};
Суперкомпилер успешно объединил sum и mapSq в одну функцию, f0 ! В отличие от оригинальной программы, f0 работает за один проход, без необходимости распределять дополнительную память.
Как суперкомпилер дошел до этой точки? Давайте посмотрим на сгенерированный график процесса:
Для справки, nodes.json содержит следующие данные в JSON:
[
[ " n0 " , " main(xs) " ],
[ " n1 " , " sum(mapSq(xs)) " ],
[ " n2 " , " sum(.g1(xs)) " ],
[ " n3 " , " xs " ],
[ " n4 " , " sum(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n5 " , " .g0(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n6 " , " +(*(.v0, .v0), sum(mapSq(.v1))) " ],
[ " n7 " , " +(*(.v0, .v0), sum(.g1(.v1))) " ],
[ " n8 " , " *(.v0, .v0) " ],
[ " n9 " , " .v0 " ],
[ " n10 " , " .v0 " ],
[ " n11 " , " sum(.g1(.v1)) " ],
[ " n12 " , " .v1 " ],
[ " n13 " , " +(.v3, .v4) " ],
[ " n14 " , " .v3 " ],
[ " n15 " , " .v4 " ],
[ " n16 " , " sum(Nil()) " ],
[ " n17 " , " .g0(Nil()) " ],
[ " n18 " , " 0i32 " ]
] (Нам не нужно будет осматривать program.json на этот крошечный пример, но не стесняйтесь смотреть на нее: это не слишком сложно.)
Суперкомпилер начинается с узла n0 , содержащего main(xs) . После двух этапов разворачивания функции мы достигаем узла n2 , содержащего sum(.g1(xs)) , где .g1 - это IR -функция, которая соответствует нашему mapSq . На этом этапе у нас нет другого выбора, чем анализировать вызов .g1(xs) предполагая, какие значения xs могут занять во время выполнения. Поскольку наш mapSq принимает только конструкторы Nil и Cons , достаточно рассмотреть случаи xs=Cons(.v0, .v1) и xs=Nil() .
Узел n4 - это то, что происходит после того, как мы заменим Cons(.v0, .v1) для xs , где .v0 и .v1 являются свежими переменными. После еще трех функций разворачивается, мы прибываем на n7 . Это первый раз, когда мы должны разделить вызов +(*(.v0, .v0), sum(.g1(.v1))) на .v3=*(.v0, .v0) ( n8 ) и .v4=sum(.g1(.v1)) ( n11 ) и продолжить суперкомпилинг +(.v3, .v4) ( n13 ); Причина для этого заключается в том, что предыдущий узел ( n2 ) структурно встроен в n7 , поэтому суперкомпиляция в противном случае может продолжаться навсегда. Теперь, что происходит с sum(.g1(.v1)) ( n11 )? Мы видели это раньше! Напомним, что n2 содержит sum(.g1(xs)) , что является лишь переименованием sum(.g1(.v1)) ; Таким образом, мы решаем сложить n11 в n2 , потому что это не имеет смысла дважды одно и то же. Другие ветви n7 , а именно n13 и n8 , разлагаются , что означает, что мы просто продолжаем трансформировать их аргументы.
Что касается другой ветви n2 , sum(Nil()) ( n16 ), достаточно, чтобы просто развернуть этот призыв на 0i32 ( n18 ).
После того, как график процесса завершен, остаточная обработка преобразует его в окончательную программу. На этом этапе динамические шаблоны выполнения становятся функциями - узел n2 теперь становится функцией f0 , поскольку какой -то другой узел ( n11 ) указывает на него. В любой остаточной программе будет столько функций, сколько и узлов с входящими пунктирными линиями, плюс main .
Таким образом, суперкомпиляция состоит из 1) разворачивающихся определений функций, 2) анализ вызовов, которые матч с шаблоном неизвестной переменной, 3) разбивая вычисления на более мелкие части, 4) складывание повторных вычислений и 5) разлагающихся вызовов, которые не могут быть развернуты, такие как +(.v3, .v4) ( n13 ) в нашем примере. Весь процесс суперкомпиляции гарантированно завершится, потому что, когда некоторые вычисления становятся опасно больше и больше, мы разбиваем его на подпроекты и решаем их в изоляции.
В examples/ папке есть множество других интересных примеров обезлесения, включая структуры данных, подобные деревьям. Фактически, мы переопределили все образцы из предыдущей работы по суперкомпиляции вызовов высшего порядка, проведенного Питером А. Джонссоном и Йоханом Нордландером 4 5 ; Во всех случаях Mazeppa работала так же или лучше.
Теперь рассмотрим другой пример, на этот раз, включающий частичную оценку:
[ examples/power-sq/main.mz ]
main(a) := powerSq(a, 7u8);
powerSq(a, x) := match =(x, 0u8) {
T() -> 1i32,
F() -> match =(%(x, 2u8), 0u8) {
T() -> square(powerSq(a, /(x, 2u8))),
F() -> *(a, powerSq(a, -(x, 1u8)))
}
};
square(a) := *(a, a);
powerSq реализует знаменитый алгоритм экспоненты за подготовкой. Первоначальная программа неэффективна: рекурсивно рассматривает параметр x powerSq , хотя она прекрасно известна во время компиляции. Запуск Mazeppa на main(a) даст следующую остаточную программу:
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
Вся функция powerSq была устранена, что достигнет влияния частичной оценки. (Если мы рассматриваем powerSq как интерпретатор для программы x и входных данных a , то это первый проекция Futamura: специализируя интерпретатор для получения эффективной целевой программы.) Кроме того, обратите внимание, как суперкомпильер удалось поделиться аргументом *(a, *(a, a)) дважды, чтобы он не отменял каждый раз. Остаточная программа действительно отражает экспонентацию путем квадрата.
Давайте выходим за рамки обезлесения и частичной оценки. Рассмотрим matches(p, s) двух строк, что возвращает T() если s содержит p и F() в противном случае. Наивная реализация в Mazeppa будет следующей, где p специализируется на "aab" :
[ examples/kmp-test/main.mz ]
main(s) := matches(Cons('a', Cons('a', Cons('b', Nil()))), s);
matches(p, s) := go(p, s, p, s);
go(pp, ss, op, os) := match pp {
Nil() -> T(),
Cons(p, pp) -> goFirst(p, pp, ss, op, os)
};
goFirst(p, pp, ss, op, os) := match ss {
Nil() -> F(),
Cons(s, ss) -> match =(p, s) {
T() -> go(pp, ss, op, os),
F() -> failover(op, os)
}
};
failover(op, os) := match os {
Nil() -> F(),
Cons(_s, ss) -> matches(op, ss)
};
(Здесь мы представляем строки как списки символов для простоты, но не волнуйтесь, Mzeppa также предоставляет встроенные строки.)
Алгоритм правильный, но неэффективный. Подумайте, что происходит, когда "aa" успешно соответствует, но 'b' - нет. Алгоритм начнет совпадать с "aab" еще раз со второго персонажа s , хотя уже можно сказать, что вторым персонажем s является 'a' . Детерминированный конечный автомат, созданный алгоритмом Кнут-Морриса-Пратта (KMP) 6, является альтернативным способом решения этой проблемы.
Запустив Mazeppa на приведенной выше образец, мы можем получить эффективный алгоритм соответствия строк для p="aab" , который отражает KMP в действии:
[ examples/kmp-test/target/output.mz ]
main(s) := f0(s);
f0(s) := match s {
Cons(s', ss) -> match =(97u8, s') {
F() -> f1(ss),
T() -> f2(ss)
},
Nil() -> F()
};
f1(ss) := f0(ss);
f2(ss) := match ss {
Cons(s, ss') -> match =(97u8, s) {
F() -> f1(ss'),
T() -> f4(ss')
},
Nil() -> F()
};
f3(ss) := f2(ss);
f4(ss) := match ss {
Cons(s, ss') -> match =(98u8, s) {
F() -> match =(97u8, s) {
F() -> f1(ss'),
T() -> f4(ss')
},
T() -> T()
},
Nil() -> F()
};
Наивный алгоритм, который мы написали, был автоматически превращен в известную эффективную версию! В то время как наивный алгоритм имеет сложность O (| P | * | S |) , специализированный - O (| S |) .
Синтезирование KMP является стандартным примером, который демонстрирует силу суперкомпиляции по отношению к другим методам (например, см. 7 и 8 ). Получение KMP по частичной оценке невозможно без изменения исходного определения matches 9 10 .
Валентин Турчин, изобретатель суперкомпиляции, описывает концепцию перехода метасистемы следующим образом 11 12 13 :
Рассмотрим систему любого рода. Предположим, что есть способ сделать из этого некоторое количество копий, возможно, с вариациями. Предположим, что эти системы объединены в новую систему S ' , которая имеет системы S типа S в качестве подсистемы, и включает в себя также дополнительный механизм, который контролирует поведение и производство S -Subsystems. Затем мы называем S ' MetasyStem по отношению к S и созданию S' Metasystem переход. В результате последовательных переходов метасистемы возникает многоуровневая структура контроля, которая позволяет сложные формы поведения.
Таким образом, суперкомпиляция можно легко рассматривать как переход на метасистему: в Mazepppa существует объектная программа, и есть суперкомпилер Marepppa, который управляет и контролирует выполнение объектной программы. Тем не менее, мы можем пойти дальше и выполнить любое количество переходов Metasystem в области самой объектной программы, как показывает следующий пример.
Мы будем использовать код из examples/lambda-calculus/ . Ниже приведена стандартная процедура нормализации по оценке для получения бета-нормальных форм нетипированных терминов исчисления Lambda:
normalize(lvl, env, t) := quote(lvl, eval(env, t));
normalizeAt(lvl, env, t) := normalize(+(lvl, 1u64), Cons(vvar(lvl), env), t);
vvar(lvl) := Neutral(NVar(lvl));
eval(env, t) := match t {
Var(idx) -> indexEnv(env, idx),
Lam(body) -> Closure(env, body),
Appl(m, n) ->
let mVal := eval(env, m);
let nVal := eval(env, n);
match mVal {
Closure(env, body) -> eval(Cons(nVal, env), body),
Neutral(nt) -> Neutral(NAppl(nt, nVal))
}
};
quote(lvl, v) := match v {
Closure(env, body) -> Lam(normalizeAt(lvl, env, body)),
Neutral(nt) -> quoteNeutral(lvl, nt)
};
quoteNeutral(lvl, nt) := match nt {
NVar(var) -> Var(-(-(lvl, var), 1u64)),
NAppl(nt, nVal) -> Appl(quoteNeutral(lvl, nt), quote(lvl, nVal))
};
indexEnv(env, idx) := match env {
Nil() -> Panic(++("the variable is unbound: ", string(idx))),
Cons(value, xs) -> match =(idx, 0u64) {
T() -> value,
F() -> indexEnv(xs, -(idx, 1u64))
}
};
( eval / quote иногда называют reflect / reify .)
По сути, это машина для эффективной замены, предотвращающего захват, является большим шагом: вместо реконструкции терминов при каждом бета-сокращении мы поддерживаем среду значений. eval проецирует термин «семантическому домену», в то время как quote делает наоборот; normalize - это просто состав quote и eval . Чтобы не беспокоиться о генерации свежих имен, мы поместили индексы De Bruijn в уровнях Var Constructor и De Bruijn в NVar ; Последний преобразуется в первое в quoteNeutral .
Теперь давайте вычислим что -нибудь с помощью этой машины:
main() := normalize(0u64, Nil(), example());
example() := Appl(Appl(mul(), two()), three());
two() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))));
three() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64),
Var(0u64))))));
mul() := Lam(Lam(Lam(Lam(Appl(
Appl(Var(3u64), Appl(Var(2u64), Var(1u64))),
Var(0u64))))));
Тело main вычисляет нормальную форму примера лямбда example() , который умножает цифры церкви two() и three() .
Supercompiling main() , мы получаем Церковное число 6:
[ examples/lambda-calculus/target/output.mz ]
main() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64)
, Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))))))));
Интерпретатор Lambda Calculus был полностью уничтожен!
В этом примере мы только что видели двухуровневую лестницу Metasystem (в терминологии Turchin 14 ): на уровне 0 у нас есть суперкомпилер Mazepppa, преобразующий объектную программу, в то время как на уровне 1 у нас есть объектная программа, нормализующая термины Lambda Calculus. Там может быть произвольное количество уровней интерпретации, и может быть использовано лазепп, чтобы свернуть их все. Это общее поведение суперкомпиляции было изучено самим Турчином в 1 (раздел 7), где он смог суперкомпиля две интерпретируемые программы, одну из них, похожая на Фортран и одна в LISP, чтобы получить коэффициент ускорения в 40 в обоих случаях.
Нормализатор Lambda также показывает нам, как воплотить функции более высокого порядка на язык первого порядка. В Marepppa мы не можем рассматривать функции как значения, но это не означает, что мы не можем их моделировать! Выполнив переход Metasystem, мы можем эффективно реализовать функции высшего порядка на языке первого порядка. Наряду с дефункционализацией и конверсией закрытия, этот метод может быть использован для компиляции языков более высокого порядка в эффективный код первого порядка.
Связанные примеры: императивная виртуальная машина, самообвинение.
Оглядываясь назад, основной проблемой, которая предотвратила широкое распространение суперкомпиляции, является ее непредсказуемость - темная сторона ее силы. Чтобы понять, что это значит, подумайте, как мы можем решить любую проблему SAT "на лету":
[ examples/sat-solver/main.mz ]
main(a, b, c, d, e, f, g) := solve(formula(a, b, c, d, e, f, g));
formula(a, b, c, d, e, f, g) :=
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Var(e), or(Not(g), F()))),
and(or(Var(e), or(Not(g), or(Var(f), F()))),
and(or(Not(g), or(Var(c), or(Var(d), F()))),
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Not(e), or(Var(g), F()))),
and(or(Var(a), or(Var(a), or(Var(c), F()))),
and(or(Not(g), or(Not(d), or(Not(b), F()))),
T()))))))));
or(x, rest) := match x {
Var(x) -> If(x, T(), rest),
Not(x) -> If(x, rest, T())
};
and(clause, rest) := match clause {
If(x, m, n) -> If(x, and(m, rest), and(n, rest)),
T() -> rest,
F() -> F()
};
solve(formula) := match formula {
If(x, m, n) -> analyze(x, m, n),
T() -> T(),
F() -> F()
};
analyze(x, m, n) := match x {
T() -> solve(m),
F() -> solve(n)
};
В этом совершенно правильном коде есть две вещи: 1) Суперкомпилер расширит формулу в экспоненциальном пространстве, и 2) суперкомпилер попытается решить расширенную формулу в экспоненциальное время. Иногда мы просто не хотим оценивать все во время компиляции.
Однако отчасти не: мы предоставляем решение для этой проблемы. Давайте сначала рассмотрим, как отложить решение формулы до времени выполнения. Оказывается, единственное, что нам нужно сделать, это аннотировать formula функции @extract следующим образом:
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
Когда Mazeppa видит solve(formula(a, b, c, d, e, f, g)) , она извлекает призыв к formula в свежую переменную .v0 и вызывает суперкомпирацию извлеченного вызова и solve(.v0) в изоляции. Последний вызов просто воспроизводит оригинальный решатель SAT.
Но суперкомпингирование вызова к formula все равно приведет к экспоненциальному взрыву. Давайте рассмотрим, почему это происходит. Наша первоначальная формула состоит из звонков or и and ; в то время как or очевидно, не опасно, and распространяет параметр rest в обеих ветвях If (первый случай match ) - это точное место, где происходит взрыв. Итак, давайте отметим and также с @extract :
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
Вот и все! Когда and должно быть трансформировано, Mazeppa извлекает вызов из окружающего контекста и в изоляции. Добавив две аннотации в соответствующих местах, мы решили как проблему взрыва кода, так и экспоненциальное время выполнения суперкомпиляции. В целом, всякий раз, когда Mazeppa видит ctx[f(t1, ..., tN)] , где f помечена @extract и ctx[.] -это непустые окружающий контекст с . В положении Redex он подключит свежую переменную v к ctx и продолжит преобразование следующих узлов отдельно: f(t1, ..., tN) и ctx[v] .
Наконец, обратите внимание, что @extract -это всего лишь механизм низкого уровня; Передний компилятор должен выполнять дополнительную машину, чтобы сообщить Mzeppa, которая функционирует для извлечения. Это можно сделать двумя способами:
formula , and как извлекаемый, оставляя все другие функции нетронутыми.Оба метода могут быть объединены для достижения желаемого эффекта.
Mazeppa использует интересный выбор дизайна, чтобы иметь нетерпеливые функции и ленивые конструкторы. Следующий пример, где magic(1u32, 1u32) генерирует числа Фибоначчи, была принята из Haskell:
[ examples/lazy-fibonacci/main.mz ]
main() := getIt(magic(1u32, 1u32), 3u64);
magic(m, n) := match =(m, 0u32) {
T() -> Nil(),
F() -> Cons(m, magic(n, +(m, n)))
};
getIt(xs, n) := match xs {
Nil() -> Panic("undefined"),
Cons(x, xs) -> match =(n, 1u64) {
T() -> x,
F() -> getIt(xs, -(n, 1u64))
}
};
Если бы конструкторы были нетерпеливы, magic(1u32, 1u32) никогда не прекратилась бы. Тем не менее, Cons не оценивают свои аргументы! Поскольку getIt потребляет только конечную часть бесконечного списка, программа завершает и печатает 2u32 :
$ mazeppa eval
2u32
Ленивые конструкторы обеспечивают легкое обезлесение, как обсуждалось ниже.
После установки Mazeppa через opam или ./scripts/install.sh он доступен в виде библиотеки OCAML!
Настройте новый проект Dune следующим образом:
$ dune init project my_compiler
Добавьте mazeppa в качестве сторонней библиотеки в свою bin/dune :
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
Вставьте следующий код в bin/main.ml (это examples/sum-squares/main.mz кодируемые в OCAML):
open Mazeppa
let input : Raw_program.t =
let sym = Symbol. of_string in
let open Raw_term in
let open Checked_oint in
[ [], sym " main " , [ sym " xs " ], call ( " sum " , [ call ( " mapSq " , [ var " xs " ]) ])
; ( []
, sym " sum "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), int ( I32 ( I32. of_int_exn 0 ))
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call ( " + " , [ var " x " ; call ( " sum " , [ var " xs " ]) ]) )
] ) )
; ( []
, sym " mapSq "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), call ( " Nil " , [] )
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call
( " Cons "
, [ call ( " * " , [ var " x " ; var " x " ]); call ( " mapSq " , [ var " xs " ]) ] ) )
] ) )
]
;;
let () =
try
let output = Mazeppa. supercompile input in
Printf. printf " %s n " ( Raw_program. show output)
with
| Mazeppa. Panic msg ->
Printf. eprintf " Something went wrong: %s n " msg;
exit 1
;; Запустите dune exec my_compiler чтобы увидеть желаемую остаточную программу:
[([], "main", ["xs"], (Raw_term.Call ("f0", [(Raw_term.Var "xs")])));
([], "f0", ["xs"],
(Raw_term.Match ((Raw_term.Var "xs"),
[(("Cons", ["x"; "xs'"]),
(Raw_term.Call ("+",
[(Raw_term.Call ("*", [(Raw_term.Var "x"); (Raw_term.Var "x")]));
(Raw_term.Call ("f0", [(Raw_term.Var "xs'")]))]
)));
(("Nil", []), (Raw_term.Const (Const.Int (Checked_oint.I32 0))))]
)))
]
Вы можете назвать Mazeppa столько раз, сколько захотите, в том числе параллельно. Обратите внимание, что мы выставляем ограниченный интерфейс с суперкомпилером; В частности, нет никакого способа осмотреть то, что он делает в процессе (т.е. --inspect ).
Помимо суперкомпиляции, мы также предоставляем встроенный оценщик:
val eval : Raw_program .t -> Raw_term .t Его можно вызвать только в программы, main функции, не принимают параметры. В отличие от supercompile , он производит оцененный термин типа Raw_term.t и может расходиться.
См. Другие функции API и их документацию в lib/mazeppa.mli .
Предположим, что main.mz содержит слегка модифицированную версию ленивого примера Fibonacci:
main(n) := getIt(magic(1u32, 1u32), n);
magic(m, n) := match =(m, 0u32) {
T() -> Nil(),
F() -> Cons(m, magic(n, +(m, n)))
};
getIt(xs, n) := match xs {
Nil() -> Panic("undefined"),
Cons(x, xs) -> match =(n, 1u64) {
T() -> x,
F() -> getIt(xs, -(n, 1u64))
}
};
Следующая команда переводит его в C11 с расширениями GNU (т.е. -std=gnu11 ):
$ cat main.mz | mazeppa translate --language C --entry fib
#include "mazeppa.h"
MZ_ENUM_USER_TAGS ( op_Cons , op_Nil );
static mz_Value op_main ( mz_ArgsPtr args );
static mz_Value op_magic ( mz_ArgsPtr args );
static mz_Value op_getIt ( mz_ArgsPtr args );
static mz_Value thunk_0 ( mz_EnvPtr env ) {
mz_Value var_m = ( env )[ 0 ];
mz_Value var_n = ( env )[ 1 ];
return ({
struct mz_value args [ 2 ];
( args )[ 0 ] = var_n ;
( args )[ 1 ] = MZ_OP2 ( var_m , add , var_n );
op_magic ( args );
});
}
static mz_Value op_main ( mz_ArgsPtr args ) {
mz_Value var_n = ( args )[ 0 ];
return ({
struct mz_value args [ 2 ];
( args )[ 0 ] = ({
struct mz_value args [ 2 ];
( args )[ 0 ] = MZ_INT ( U , 32 , UINT32_C ( 1 ));
( args )[ 1 ] = MZ_INT ( U , 32 , UINT32_C ( 1 ));
op_magic ( args );
});
( args )[ 1 ] = var_n ;
op_getIt ( args );
});
}
static mz_Value op_magic ( mz_ArgsPtr args ) {
mz_Value var_m = ( args )[ 0 ];
mz_Value var_n = ( args )[ 1 ];
return ({
struct mz_value tmp = MZ_OP2 ( var_m , equal , MZ_INT ( U , 32 , UINT32_C ( 0 )));
switch (( tmp ). tag ) {
case op_T : {
tmp = MZ_EMPTY_DATA ( op_Nil );
break ;
}
case op_F : {
tmp = MZ_DATA ( op_Cons , 2 , MZ_SIMPLE_THUNK ( var_m ), MZ_THUNK ( thunk_0 , 2 , var_m , var_n ));
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
}
static mz_Value op_getIt ( mz_ArgsPtr args ) {
mz_Value var_xs = ( args )[ 0 ];
mz_Value var_n = ( args )[ 1 ];
return ({
struct mz_value tmp = var_xs ;
switch (( tmp ). tag ) {
case op_Nil : {
tmp = mz_panic ( MZ_STRING ( "undefined" ));
break ;
}
case op_Cons : {
mz_Value var_x = (( tmp ). payload )[ 0 ];
mz_Value var_xs$ = (( tmp ). payload )[ 1 ];
tmp = ({
struct mz_value tmp = MZ_OP2 ( var_n , equal , MZ_INT ( U , 64 , UINT64_C ( 1 )));
switch (( tmp ). tag ) {
case op_T : {
tmp = mz_force ( var_x );
break ;
}
case op_F : {
tmp = ({
struct mz_value args [ 2 ];
( args )[ 0 ] = mz_force ( var_xs$ );
( args )[ 1 ] = MZ_OP2 ( var_n , sub , MZ_INT ( U , 64 , UINT64_C ( 1 )));
op_getIt ( args );
});
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
}
extern mz_Value fib ( mz_Value var_n ) {
return MZ_CALL_MAIN ( var_n );
} Команда translate требует оба --language , который является целевым языком для перевода, и --entry , который является именем внешнего символа, который будет соответствовать вашей main функции. Программа входной лазины поступает от stdin ( cat main.mz в нашем примере); Выходная программа GNU11 записана в stdout .
Давайте продвигаем дальше и составим программу вывода в файл объекта. Во -первых, скопируйте c/deps/sds.c , c/deps/sds.h и c/deps/sdsalloc.h в ваш текущий каталог; Во -вторых, установите Boehm GC на свой компьютер:
$ sudo apt install libgc-dev -y
Затем выполните следующую команду:
$ cat main.mz
| mazeppa translate --language C --entry fib --dump-header-to .
| gcc -c -o program.o -std=gnu11 -xc -
Опция --dump-header-to Переписывает содержание mazeppa.h в указанное место; Это необходимо для компиляции вывода. Команда gcc принимает программу вывода из stdin и производит program.o . O.
Теперь осталось, чтобы фактически вызвать сгенерированную функцию fib . Создайте main.c со следующим контентом:
#include "mazeppa.h"
mz_Value fib ( mz_Value n );
int main ( void ) {
// Always initialize Boehm GC before invoking Mazeppa code.
GC_INIT ();
mz_Value v = fib ( MZ_INT ( U , 64 , 10 ));
printf ( "fib(10) = %" PRIu32 "n" , MZ_GET ( U32 , v ));
} Эта «драйверная» программа просто вызывает fib с целочисленным целым ( MZ_INT ) и печатает результат. Вы можете использовать любую функциональность от mazeppa.h , при условии, что он не префикс mz_priv_ или MZ_PRIV_ .
Чтобы собрать все кусочки вместе:
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out Печать fib(10) = 55 и выходы, как и ожидалось.
--inspect в реальной среде: используйте его только для отладки.@extract (как показано выше), чтобы контролировать, продолжать ли суперкомпиляция или извлечь Redex."otus" меньше, чем "octopus" , но "octopusx" не является. Mazeppa использует несколько интересных вариантов дизайна (оценивается по важности):
Код первого порядка. Макс Болингброк и Саймон Пейтон Джонс 15 сообщают, что для одного конкретного примера их суперкомпилера высшего порядка для подмножества Хаскелла потратила 42% времени исполнения на управление именами и переименованием. Хотя это правда, что упрощенные модели оценки, такие как нормализация терминов Lambda, позволяют нам избежать значительных накладных расходов избегания захвата, суперкомпиляция является более сложной. Например, помимо символических вычислений, суперкомпиляция должна анализировать ранее вычисленные результаты для принятия обоснованных решений о дальнейшей трансформации: рассмотрим тесты термина, гомеоморфные тесты встраивания, большинство специфических обобщений и т. Д. Вводя функции более высокого порядка неизбежно усложняют все эти анализы, что делает суперкомпиляцию, более медленную, более сложную память и усердно усложняет разум. В Mazeppa мы придерживаемся философии постепенных улучшений: вместо того, чтобы пытаться справиться с многими причудливыми функциями одновременно, мы 1) исправляем основной язык для удобного манипуляции машиной, 2) выполнять столько переходов метасистем, сколько необходимо, чтобы сделать основной язык лучше для человека.
Ленивые конструкторы. Это хорошо известное наблюдение, что языки по вызову за ценами трудно для правильного обезлесения. По -прежнему возможно, чтобы вырубить их, но не без дополнительного анализа 4 5 . Однако, если конструкторы ленивы (то есть они не оценивают свои аргументы), вырубка лесов просто работает . Turchin заставил его работать путем преобразования нормального порядка языка вызовов, но результат заключается в том, что остаточный код может заканчиваться чаще. В Mazepppa у нас есть функции по вызову и конструкторы по вызову (вызовов), которые делают возможным обезлесение и 2) сохраняет исходную семантику кода.
Бесплатные графики процесса. В Marepppa графики процессов не содержат никаких ссылок на термины: остаточная может работать без них. В результате коллекционер мусора может сдавать термины, которые использовались во время строительства подграфа. Кроме того, от того, что эта политика имеет несколько других важных преимуществ: 1) График все еще существует для проверки с --inspect -2) Когда он нарисован, он раскрывает только информацию о решениях, принятых суперкомпилером, что значительно облегчает его. Несколько существующих суперкомпилеров воздерживаются от надлежащих графиков процесса (например, Supero 17 Нила Митчелла и вышеупомянутого 15 ), но в результате они менее способны для проверки пользователем, 2) алгоритмы становятся загроможденными деталями генерации кода.
Двумерный анализ конфигурации. Обычно суперкомпилер сохраняет «историю» подмножества всех предков, трансформируя узел; Если этот узел «достаточно близок» к одному из его предков, пришло время разбить термин на более мелкие части, чтобы гарантировать прекращение. В вместо этого мы храним две отдельные структуры данных: одна, содержащая подмножество предков узла и такую, содержащую подмножество полностью преобразованных узлов. Первая структура данных используется для гарантирования прекращения (как обычно), в то время как последняя используется для улучшения совместного использования функций в остаточном коде. В частности, если текущий узел (особого рода) является переименованием некоторых ранее преобразованных узлов, мы складываем текущий узел в этот предыдущий узел. Таким образом, Mazeppa выполняет как вертикальный , так и горизонтальный анализ конфигураций, что делает остаточный код более компактным и суперкомпиляцией более эффективной.
Функция анализа производительности. Когда внутренняя функция вызывает шаблоны, значения неизвестного, происходят две потенциально опасные вещи: 1) суперкомпиляция воспроизводит структуру функции соответствия шаблона, 2) суперкомпиляция подталкивает весь окружающий контекст ко всем ветвям этой функции. Без дальнейшего контроля эта ситуация может привести к значительному взрыву в размере кода, иногда даже приводит к тому, что суперкомпилера не прекращается в разумное время. Чтобы улучшить, Mazepppa дублирует контекст IFF, что этот внутренний вызов дает определенное значение верхнего уровня, по крайней мере, из одной точки выхода, потому что, если он это сделает, большие шансы на то, что это значение может быть деконструировано с помощью последующего сопоставления шаблонов. В противном случае, Mzepppa извлекает внутренний вызов и преобразует его изоляцией (как если бы он был помечен @extract ). Кроме того, если контекст фактически дублируется, следующее правило относится ко всем ветвям: если ветвь дает определенное значение верхнего уровня из всех точек выхода, оно преобразуется в контексте, как обычно; В противном случае ветвь извлекается из контекста и преобразуется в изоляции. На практике этот анализ предотвращает огромное количество ненужных специализаций, тем самым составляя размер остаточной программы и делает суперкомпиляцию гораздо более проведенной.
Умные истории. Вместо того, чтобы слепо сравнивать текущий узел со всеми его предками, мы используем более мелкозернистый контроль, то есть: 1) Глобальные узлы (те, которые анализируют неизвестную переменную), сравниваются только с глобальными узлами, 2) Локальные узлы (те, которые уменьшаются линейно на одном этапе), сравниваются с локальными узлами до последних глобальных узлов, но не в том, что он не в том, что они не могут быть в виде малыша). что-нибудь еще. Помимо более экономического подхода к проверке прекращения, эта схема позволяет Mazeppa открывать больше возможностей для оптимизации; См. 18 , разделы 4.6 и 4.7. Прекращение суперкомпиляции гарантируется тем фактом, что гомеоморфное внедрение все еще тестируется на всех потенциально бесконечных последующих последствиях глобальных и местных терминов (не может существовать бесконечная последовательность только тривиальных терминов).
Redex подписчики. Свист проверяется только на терминах с равными подписями Redex . Подпись Redex - это пара 1) символ функции и 2) список категорий значений аргумента. Категория значений - это своего рода метаинформация о аргументе, которая может быть 1) VConst для таких значений, как 42i32 или "hello world" , 2) VNeutral для таких значений, как x или +(x, x) , или 3) VCCall(c) для конструкторов, таких как Foo(...) . Свист все еще проверяется на всех потенциально бесконечных последовательностях терминов, потому что любая бесконечная последовательность должна содержать, по крайней мере, одну бесконечную последующую последовательность терминов с той же подписью Redex. Эта стратегия позволяет Мазепе избегать чрезмерной генерализации в некоторых случаях, как показывают следующие два примера:
f(A()) гомеоморфически встроен в f(g(B(A()))) ; Однако, поскольку операторы Redex различны ( f и g ), Mazeppa продолжает сокращение и достигает идеального результата.f(A(Good())) встроен в f(f(f(B(A(Good()))))) а оператор Redex в обоих случаях, Mazeppa не чрезмерно генеризует, потому что f два термина имеют разные категории ценных значений в своих подписях Redex: в первом случае f вызывает на A(...) , хотя в втором случае, это позаботится B(...) . Как и в предыдущем примере, Mazeppa достигает идеального результата суперкомпиляции исключительно путем сокращения.Оптимизированное гомеоморфное внедрение. За десятилетия гомеоморфное встраивание приобрело репутацию отличного метода для проверки 19 онлайн. К сожалению, в основном из-за нелинейного потока управления (когда применяются как дайвинг, так и связь), для вычисления может быть непростительно дорого. Что еще хуже, он пересматривается для всех квалифицированных родительских узлов всякий раз, когда в историю добавляется новый термин, который постепенно замедляет суперкомпиляцию по мере роста истории: заходит до еды большей части времени суперкомпиляции! Чтобы справиться с этим, мы поддерживаем два отдельных кеша:
Хэш пособия. Гомеоморфные кэши, описанные выше, зависят от того, сколько терминов разделяется . Поэтому мы используем хэш, рассматриваемый во время разворачивания функций: если какой -то новый термин T структурно равен некоторым существующим терминам , последний используется повторно. Чтобы избежать утечек памяти, мы используем глобальный эфемер, удерживающий слабые указатели на термины. Помимо улучшенного времени суперкомпиляции (из -за памяти), хэш, рассчитывающий, также уменьшает потребление памяти - см. № 4 (комментарий).
Нормализация во время развертывания. Когда вызов функции разворачивается, мы заменяем параметры и как можно больше нормализуем тело (т.е., без дальнейших разворотов, гарантировать прекращение). Чтобы понять почему, рассмотрим факторную функцию f(n) ; При простом развертывании мы поймали бы в неприятной ситуации, когда f(1u32) внедряется в *(1u32, f(-(1u32, 1u32))) , вызывая чрезмерную генерализацию . В действительности, Mazeppa разворачивалась бы f(1u32) до *(1u32, f(0u32)) , что сделает последнего кандидатом для дальнейшего развертывания. Этот подход был предложен в 20 , раздел 4.5. Другие его достоинства: 1) меньше работы для будущих этапов вождения, 2) меньше «банальных» вычислений на графиках процессов, 3) уменьшенное количество дорогих тестов гомеоморфного встраивания.
*(1u32, f(-(1u32, 1u32))) больше не проверяется на f(1u32) из-за различных операторов Redex. Однако другие преимущества нормализации все еще сохраняются.Реализация в OCAML. Mazeppa реализуется с использованием комбинации функциональных и императивных стилей программирования, что очень естественно для OCAML. Исключения используются не только для «исключительных» ситуаций, так как изменение внутри функций является общей. Хотя у нас нет подобного суперкомпилера, написанного в EG Haskell или Rust для сравнения, мы считаем, что именно OCAML дал нам рабочую реализацию без необходимости ссориться с языком и никогда не заканчивать работу.
Хотя большинство из вышеперечисленных не особенно новое, мы считаем, что комбинация этих особенностей делает Mazeppa более практичной альтернативой, чем ее предшественники.
A symbol <SYMBOL> is a sequence of letters ( a , ... , z and A , ... , Z ) and digits ( 0 , ... , 9 ), followed by an optional question mark ( ? ), followed by an optional sequence of ' characters. The underscore character ( _ ) may be the first character of a symbol, which may informally indicate that the value or function being defined is not used; otherwise, the first character must be a letter. The following sequences of characters are also permitted as symbols: ~ , # , + , - , * , / , % , | , & , ^ , << , >> , = , != , > , >= , < , <= , ++ . The following are reserved words that may not be used as symbols: match , let .
There are four classes of unsigned integer constants :
0b ( 0B ) followed by a non-empty sequence of binary digits 0 and 1 .0o ( 0O ) followed by a non-empty sequence of octal digits 0 , ... , 7 .0 , ... , 9 .0x ( 0X ) followed by a non-empty sequence of decimal digits 0 , ... , 9 and letters a , ... , f ( A , ... , F ).Примечания:
_ ) except for the first position in the sequence of digits.- ) placed right before the sequence of digits and underscore characters.<INT> produced by appending an integer type <INT-TY> ( u8 , u16 , u32 , u64 , u128 , i8 , i16 , i32 , i64 , i128 ) right after the original integer constant. For example, the constants 123i8 , 123u16 , and 123i32 all belong to the set <INT> . A string constant <STRING> is a sequence, between double quotes ( " ), of zero or more printable characters (we refer to printable characters as those numbered 33-126 in the ASCII character set), spaces, or string escape sequences :
| Escape sequence | Значение |
|---|---|
f | Form feed (ASCII 12) |
n | Line feed (ASCII 10) |
r | Carriage return (ASCII 13) |
t | Horizontal tab (ASCII 9) |
v | Vertical tab (ASCII 11) |
xhh | ASCII code in hexadecimal |
" | " |
\ | |
where h is either 0 , ... , 9 or a , ... , f or A , ... , F .
A character constant <CHAR> is either a sole character enclosed in single quotes ( ' ) or a character escape sequence enclosed in single quotes. The character escape sequence is the same as for strings, except that " is replaced by ' .
There are no other constants in Mazeppa.
A comment <COMMENT> is any sequence of characters after // , which is terminated by a newline character. (We only allow single-line comments for simplicity.)
The entry point <program> is defined by the following rules:
<def-attr-list> <SYMBOL> ( <SYMBOL> , ... , <SYMBOL> ) := <term> ; <program><COMMENT> <program> where <def-attr-list> is a whitespace-separated sequence of function attributes (the same attribute can occur multiple times). Right now, the only allowed function attribute is @extract .
<term> is defined as follows:
<SYMBOL> (a variable)<const> (a constant)<SYMBOL> ( <term> , ... , <term> ) (a function call)match <term> { <match-case> , ... , <match-case> } (pattern matching)let <SYMBOL> := <term> ; <term> (a let-binding)let <pattern> := <term> ; <term> (a pattern let-binding)<COMMENT> <term> (a comment)The rest of the auxiliary rules are:
<const> :
<INT> or <STRING> or <CHAR> . <match-case> :
<pattern> -> <term> <pattern> :
<SYMBOL> ( <SYMBOL> , ... , <SYMBOL> ) . In Mazeppa, primitive operations employ the same syntax as that of ordinary function calls. To distinguish between the two, we define <op1> and <op2> to be the following sets of symbols:
<op1> is one of ~ , # , length , string , <INT-TY> .<op2> is one of + , - , * , / , % , | , & , ^ , << , >> , = , != , > , >= , < , <= , ++ , get . Furthermore, <op2> has the following subclasses:
<arith-op2> is one of + , - , * , / , % , | , & , ^ , << , >> .<cmp-op2> is one of = , != , > , >= , < , <= .<op1> or <op2> . 2) A function must define a symbol starting with a lowercase letter. 3) No duplicate symbols can occur among function parameters. 4) Every free variable inside a function body must be bound by a corresponding parameter in the function definition.match { ... } must not be empty. 2) No duplicate constructors can occur among case patterns in match { ... } . 3) No duplicate symbols can occur among pattern parameters C(x1, ..., xN) . 4) No let-binding can bind <op1> or <op2> . 5) Panic must be called with only one argument; T and F with zero arguments.If a program, function, or term conforms to these restrictions, we call it well-formed .
| Original form | Desugared form | Примечания |
|---|---|---|
// ... rest | rest | rest is in <program> or <term> |
let p := t; u | match t { p -> u } | p is in <pattern> |
c | ASCII(c) | c is in <CHAR> |
where ASCII(c) is an appropriate u8 integer constant, according to the ASCII table; for example, ASCII( 'a' ) is 97u8 .
Suppose that t is a well-formed term closed under environment env (defined below) and program is a well-formed program. Then the evaluation of t is governed by the following big-step environment machine:
eval(env, x) = eval({ }, env(x))eval(env, const) = const , where const is in <const> .eval(env, f(t1, ..., tN)) =t1Val ^= eval(env, t1)tNVal ^= eval(env, tN)eval({ x1 -> t1Val, ..., xN -> tNVal }, body) , where f(x1, ..., xN) := body; is in program .eval(env, C(t1, ..., tN)) = C(t1[env], ..., tN[env]) , where C starts with an uppercase letter.eval(env, op(t)) =tVal ^= eval(env, t)evalOp1(op, tVal) , where op is in <op1> .eval(env, op(t1, t2)) =t1Val ^= eval(env, t1)t2Val ^= eval(env, t2)evalOp2(t1Val, op, t2Val) , where op is in <op2> .eval(env, match t { p1 -> t1, ..., pN -> tN }) =Ci(s1, ..., sN) ^= eval(env, t)eval(env', tI) , whereCi(x1, ..., xN) -> tI is among the rules in match t { ... } , andenv' is env[x1 -> s1, ..., xN -> sN] .eval(env, let x := t; u) =tVal ^= eval(env, t)eval(env[x -> tVal], u)Notation:
env is a total environment over t , whose general form is { x1 -> t1, ..., xN -> tN } . Each tI term must be closed and well-formed; this property is preserved by eval .env(x) is tI , where x -> tI is in env .env[x1 -> t1, ..., xN -> tN] is the environment env extended with new bindings x1 -> t1 , ... , xN -> tN . If some xI is already bound in env , it is rebound.t[env] denotes a simultaneous substitution of all free variables in t by their bound values in env .tVal ^= eval(env, t) evaluates t under env ; затем:Panic(t') , the result of the whole evaluation rule is Panic(t') .tVal is available for the next clauses. (Note that eval is a partial function, so evaluation of t can "get stuck" without a superimposed type system.)
In what follows, 1) signed integers are represented in two's complement notation, 2) panic denotes Panic(s) , where s is some (possibly varying) implementation-defined string constant.
evalOp1 takes care of the unary operators for primitive types ( x is in <INT> , s is in <STRING> ):
evalOp1(~, x) is the bitwise negation of x of the same type.evalOp1(string, x) is the string representation of x (in decimal).evalOp1(ty, x) , where ty is in <INT-TY> , is x converted to an integer of type ty .x is not in the range of ty , the result is panic .evalOp1(#, x) , where x is a u8 integer, is a string containing only the ASCII character of x .x is not printable, the result takes the form "xhh" .evalOp1(length, s) is a u64 integer denoting the length of s .evalOp1(string, s) is s . Likewise, evalOp2 takes care of the binary operators for primitive types:
evalOp2(x, op, y) , where x and y have the same integer type and op is in <arith-op2> , performs a corresponding arithmetic operation on x and y , yielding a value of the same type as that of x and y .evalOp2(x, op, y) , where x and y have the same integer type and op is in <cmp-op2> , performs a corresponding comparison operation on x and y , yielding either T() or F() .evalOp2(s1, op, s2) , where s1 and s2 are strings and op is in <cmp-op2> , performs a corresponding lexicographical comparison on s1 and s2 , yielding either T() or F() .evalOp2(s1, ++, s2) is the concatenation of s1 and s2 .evalOp2(s, get, idx) , where idx is a u64 integer, is the idx -th character (of type u8 ) of s .idx is out of bounds, the result is panic . The definition of eval is now complete.
version field in dune-project and bin/main.ml .dune build to generate mazeppa.opam .CHANGELOG.md .Not yet, we need to battle-test Mazeppa on some actual programming language. Our long-term goal is to find suitable heuristics to profitably supercompile any source file under 10'000 LoC (in Mazeppa).
For debugging and other purposes, we provide a built-in definitional interpreter that can execute Mazeppa programs. You can launch it by typing mazeppa eval (make sure that your main function does not accept parameters). For the purpose of real execution, we recommend translating Mazeppa to C and then compiling C to machine code, as shown above.
Since Mazeppa is a purely functional language, the only way to implement I/O is as in Haskell 23 : having a pure program that performs computation and a dirty runtime that performs side effects issued by the program. There are no plans to introduce direct I/O into Mazeppa: it will only make everything more complicated.
No, we do not think that a type system is necessary at this point. It is the responsibility of a front-end compiler to ensure that programs do not "go wrong".
The more we make supercompilation predictable, the less it is capable of theorem proving. For those interested in program analysis rather than optimization, we suggest looking into distillation 24 .
For the English audience, the following paper presents a decent introduction into supercompilation:
However, the following papers in Russian describe a supercompilation model that is closer the majority of existing supercompilers, including Mazeppa:
Mazeppa itself is inspired by this excellent paper (in English):
Finally, the international META workshops are great collections of articles about supercompilation and adjacent fields:
Several approaches can lead to superlinear speedup of non-esoteric programs by supercompilation:
None of the above is planned to be implemented in Mazeppa, because 1) we think that writing asymptotically good programs is the responsibility of the programmer, not the optimizer, and 2) predictability of supercompilation is of greater importance to us. However, for those who are interested in this topic, the references may be helpful.
Just fork the repository, work in your own branch, and submit a pull request. Prefer rebasing when introducing changes to keep the commit history as clean as possible.
Valentin F. Turchin. 1986. The concept of a supercompiler. ACM Trans. Program. Lang. Система 8, 3 (July 1986), 292–325. https://doi.org/10.1145/5956.5957 ↩ ↩ 2
Philip Wadler. 1988. Deforestation: transforming programs to eliminate trees. Theor. Comput. Наука 73, 2 (June 22, 1990), 231–248. https://doi.org/10.1016/0304-3975(90)90147-A ↩ ↩ 2
Futamura, Y. (1983). Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds) RIMS Symposia on Software Science and Engineering. Lecture Notes in Computer Science, vol 147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11980-9_13 ↩
Peter A. Jonsson and Johan Nordlander. 2009. Positive supercompilation for a higher order call-by-value language. SIGPLAN Not. 44, 1 (January 2009), 277–288. https://doi.org/10.1145/1594834.1480916 ↩ ↩ 2
Jonsson, Peter & Nordlander, Johan. (2010). Strengthening supercompilation for call-by-value languages. ↩ ↩ 2
DE Knuth, JH Morris, and VR Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6:page 323 (1977). ↩
Glück, R., Klimov, AV (1993). Occam's razor in metacomputation: the notion of a perfect process tree. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_34 ↩
Sørensen MH, Glück R, Jones ND. A positive supercompiler. Journal of Functional Programming. 1996;6(6):811-838. doi:10.1017/S0956796800002008 ↩
Consel, Charles, and Olivier Danvy. "Partial evaluation of pattern matching in strings." Information Processing Letters 30.2 (1989): 79-86. ↩
Jones, Neil & Gomard, Carsten & Sestoft, Peter. (1993). Partial Evaluation and Automatic Program Generation. ↩
Turchin, VF (1996). Metacomputation: Metasystem transitions plus supercompilation. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_24 ↩
Turchin, Valentin F. "Program transformation with metasystem transitions." Journal of Functional Programming 3.3 (1993): 283-313. ↩
Turchin, Valentin F.. “A dialogue on Metasystem transition.” World Futures 45 (1995): 5-57. ↩
Turchin, V., and A. Nemytykh. Metavariables: Their implementation and use in Program Transformation. CCNY Technical Report CSc TR-95-012, 1995. ↩
Maximilian Bolingbroke and Simon Peyton Jones. 2010. Supercompilation by evaluation. In Proceedings of the third ACM Haskell symposium on Haskell (Haskell '10). Association for Computing Machinery, New York, NY, USA, 135–146. https://doi.org/10.1145/1863523.1863540 ↩ ↩ 2
Friedman, Daniel P. and David S. Wise. “CONS Should Not Evaluate its Arguments.” International Colloquium on Automata, Languages and Programming (1976). ↩
Mitchell, Neil. “Rethinking supercompilation.” ACM SIGPLAN International Conference on Functional Programming (2010). ↩
Sørensen, MHB (1998). Convergence of program transformers in the metric space of trees. In: Jeuring, J. (eds) Mathematics of Program Construction. MPC 1998. Lecture Notes in Computer Science, vol 1422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054297 ↩
Leuschel, Michael. "Homeomorphic embedding for online termination of symbolic methods." The essence of computation: complexity, analysis, transformation (2002): 379-403. ↩
Jonsson, Peter & Nordlander, Johan. (2011). Taming code explosion in supercompilation. PERM'11 - Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. 33-42. 10.1145/1929501.1929507. ↩ ↩ 2
Tejiščák, Matúš. Erasure in dependently typed programming. Diss. University of St Andrews, 2020. ↩
Glück, Robert, Andrei Klimov, and Antonina Nepeivoda. "Nonlinear Configurations for Superlinear Speedup by Supercompilation." Fifth International Valentin Turchin Workshop on Metacomputation. 2016. ↩
Peyton Jones, Simon. (2002). Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. ↩
GW Hamilton. 2006. Poitín: Distilling Theorems From Conjectures. Electron. Notes Theor. Comput. Наука 151, 1 (March, 2006), 143–160. https://doi.org/10.1016/j.entcs.2005.11.028 ↩
Klyuchnikov, Ilya, and Dimitur Krustev. "Supercompilation: Ideas and methods." The Monad. Reader Issue 23 (2014): 17. ↩
Klimov, Andrei & Romanenko, Sergei. (2018). Supercompilation: main principles and basic concepts. Keldysh Institute Preprints. 1-36. 10.20948/prepr-2018-111. ↩
Romanenko, Sergei. (2018). Supercompilation: homeomorphic embedding, call-by-name, partial evaluation. Keldysh Institute Preprints. 1-32. 10.20948/prepr-2018-209. ↩
Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. https://dl.acm.org/doi/10.5555/647372.724040 ↩
Secher, JP (2001). Driving in the Jungle. In: Danvy, O., Filinski, A. (eds) Programs as Data Objects. PADO 2001. Lecture Notes in Computer Science, vol 2053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44978-7_12 ↩
Hoffmann, B., Plump, D. (1988). Jungle evaluation for efficient term rewriting. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_71 ↩
Hamilton, Geoff. (2007). Distillation: Extracting the essence of programs. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. 61-70. 10.1145/1244381.1244391. ↩
Hamilton, GW (2010). Extracting the Essence of Distillation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_13 ↩
Hamilton, Geoff & Mendel-Gleason, Gavin. (2010). A Graph-Based Definition of Distillation. ↩
Hamilton, Geoff & Jones, Neil. (2012). Distillation with labelled transition systems. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 15-24. 10.1145/2103746.2103753. ↩
Hamilton, Geoff. "The Next 700 Program Transformers." International Symposium on Logic-Based Program Synthesis and Transformation. Cham: Springer International Publishing, 2021. ↩
Klyuchnikov, Ilya, and Sergei Romanenko. "Towards higher-level supercompilation." Second International Workshop on Metacomputation in Russia. Тол. 2. No. 4.2. 2010. ↩
