mazeppa
v0.4.3
Supercompilation 1 ist eine Programmtransformationstechnik, die symbolisch ein bestimmtes Programm mit Laufzeitwerten als Unbekannte bewertet. Dabei entdeckt es Ausführungsmuster des ursprünglichen Programms und synthetisiert sie in eigenständige Funktionen. Das Ergebnis der Superkompilation ist ein effizienteres Restprogramm. In Bezug auf die Transformationskraft setzt die Superkompilation sowohl die Entwaldung 2 als auch die partielle Bewertung 3 ab und zeigt sogar bestimmte Funktionen des Satzes.
Mazeppa ist ein moderner Superkompilierer, der ein Kompilierungsziel für Call-by-Wert-funktionale Sprachen sein soll. Mazeppa mit früheren Superkompilern fleißig verglichen und überarbeitet,
Bereiten Sie zunächst das OCAML -System auf Ihrer Maschine vor:
$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup
Installieren Sie dann Mazeppa als opam -Paket:
$ opam install mazeppa
Geben Sie mazeppa --help ein, um die Installation zu bestätigen.
Alternativ können Sie das Repository klonen und Mazeppa manuell installieren:
$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh
Flambda ist ein leistungsstarkes Programminline und Specializer für OCAML. Wenn Sie Mazeppa mit einem Flambda-fähigen OCAML-Compiler bauen, sehen Sie möglicherweise eine viel bessere Leistung. Um es einzurichten:
$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)
(Sie können eine andere Version anstelle von 5.2.0 verwenden, wenn Sie dies wünschen.)
Um zu überprüfen, ob Flambda erfolgreich aktiviert wurde, laufen Sie:
$ ocamlopt -config | grep flambda
Sie können mit Mazeppa spielen, ohne es tatsächlich zu installieren. Führen Sie den folgenden Befehl aus dem Stammverzeichnis aus, wenn OCAML installiert und das Repository kloniert wird (wie oben):
$ ./scripts/play.sh
(GraphViz ist erforderlich: sudo apt install graphviz .)
Dadurch wird Mazeppa mit --inspect playground/main.mz starten und das Prozessdiagramm in target/graph.svg visualisieren. Letzteres kann von der SVG -Vorschau -Erweiterung in VS Code angezeigt werden.
./scripts/play.sh wird die Quellen in OCAML automatisch neu kompilieren, wenn etwas geändert wird.
Der beste Weg zu verstehen, wie die Superkompilation funktioniert, ist mit Beispiel. Betrachten Sie die folgende Funktion, die eine Liste übernimmt und eine Summe ihrer quadratischen Elemente berechnet:
[ 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))
};
Dieses Programm ist im idiomatischen, listenden funktionalen Stil geschrieben. Jede Funktion macht nur eine Sache und macht es gut. Hier gibt es jedoch ein ernstes Problem: mapSq erstellt im Wesentlichen eine Liste, die sofort durch sum dekonstruiert wird, was bedeutet, dass wir 1) zusätzlichen Speicher für die Zwischenliste zuweisen müssen, und 2) wir benötigen zwei Berechnungsausweise anstelle von einem. Die Lösung für dieses Problem wird als Entwaldung 2 bezeichnet, was ein Sonderfall der Superkompilation ist.
Lassen Sie uns sehen, was Mazeppa mit diesem Programm macht:
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
Die --inspect Flagge fordert Mazeppa an, einen detaillierten Bericht über den Transformationsprozess zu erstellen. Die sum-squares/target/ Verzeichnis enthält die folgenden Dateien:
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dot enthält das vollständige Prozessdiagramm für unser Programm. Sie können ein Bild des Diagramms erhalten, indem Sie dot -Tsvg target/graph.dot > target/graph.svg ausführen.nodes.json enthält den Inhalt aller Knoten in der Grafik. Ohne diese Datei könnten Sie allein nicht viel aus der Grafik verstehen.program.json enthält das erste Programm in Mazeppa IR : Unser Supercompiler arbeitet mit dieser speziellen Darstellung anstelle des ursprünglichen Programms.output.mz enthält das endgültige Restprogramm. output.mz enthält den folgenden Code:
[ examples/sum-squares/target/output.mz ]
main(xs) := f0(xs);
f0(xs) := match xs {
Cons(x, xs') -> +(*(x, x), f0(xs')),
Nil() -> 0i32
};
Der Supercompiler hat sum und mapSq erfolgreich zu einer einzigen Funktion, f0 , zusammengeführt! Im Gegensatz zum ursprünglichen Programm arbeitet f0 in einem einzigen Pass, ohne zusätzlichen Speicher zuweisen zu müssen.
Wie kam der Superkompiler an diesen Punkt? Lassen Sie uns das generierte Prozessdiagramm sehen:
Als Referenz enthält nodes.json die folgenden Daten in 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 " ]
] (Wir müssen program.json nicht inspizieren. Json für dieses winzige Beispiel, aber sehen Sie es mir gerne an: Es ist nicht zu kompliziert.)
Der Supercompiler beginnt mit dem Knoten n0 main(xs) enthält. Nach zwei Funktionen der Funktionsentwicklung erreichen wir den Knoten n2 , sum(.g1(xs)) enthält, wobei .g1 die IR -Funktion ist, die unserem mapSq entspricht. Zu diesem Zeitpunkt haben wir keine andere Wahl, als den Aufruf .g1(xs) zu analysieren , indem wir vermuteten, welche Werte xs zur Laufzeit dauern könnten. Da unser mapSq nur die Konstrukteure Nil und Cons akzeptiert, reicht es aus, nur die Fälle xs=Cons(.v0, .v1) und xs=Nil() zu berücksichtigen.
Knoten n4 ist das, was nach dem Ersetzen von Cons(.v0, .v1) für xs geschieht, wobei .v0 und .v1 frische Variablen sind. Nach drei weiteren Funktionen kommen wir zu n7 . Dies ist das erste Mal, dass wir den Anruf +(*(.v0, .v0), sum(.g1(.v1))) in .v3=*(.v0, .v0) ( n8 ) und .v4=sum(.g1(.v1)) ( n11 ) aufzeigen müssen und fassen Sie die SupercomPiling +(.v3, .v4) (N13) ( n13 ) (N13); Der Grund dafür ist, dass ein früherer Knoten ( n2 ) strukturell in n7 eingebettet ist, sodass die Superkompilation sonst für immer fortgesetzt wird. Was passiert nun mit sum(.g1(.v1)) ( n11 )? Wir haben es früher gesehen! Erinnern Sie sich daran, dass n2 sum(.g1(xs)) enthält, was nur eine Umbenennung von sum(.g1(.v1)) ist; Deshalb entscheiden wir uns, n11 in n2 zu falten , weil es keinen Sinn macht, das Gleiche zweimal zu übertreffen. Die anderen Zweige von n7 , nämlich n13 und n8 , werden zersetzt , was bedeutet, dass wir einfach ihre Argumente verändern.
Was den anderen Zweig von n2 , sum(Nil()) ( n16 ), reicht aus, um diesen Aufruf nur auf 0i32 ( n18 ) zu entfalten.
Nach Abschluss des Prozessdiagramms konvertiert Residualization es in ein endgültiges Programm. In dieser Phase werden dynamische Ausführungsmuster zu Funktionen - der Knoten n2 wird nun zur Funktion f0 , insofern ein anderer Knoten ( n11 ) darauf hinweist. In jedem Restprogramm gibt es genau so viele Funktionen, wie es Knoten mit eingehenden gestrichelten Linien sowie main gibt.
Zusammenfassend besteht die Superkompilation aus 1) Entfaltungsfunktionsdefinitionen, 2) Analyse von Aufrufen, die eine unbekannte Variable, 3) Berechnung in kleinere Teile, 4) Falten wiederholte Berechnungen und 5) Zersetzung von Anrufen, die nicht entfaltet werden können, wie +(.v3, .v4) ( n13 ) in unserem Beispiel in unserem Beispiel. Der gesamte Superkompilierungsprozess wird garantiert enden, denn wenn einige Berechnungen gefährlich größer und größer werden, zerlegen wir ihn in Unterprobleme und lösen sie isoliert.
Es gibt viele andere interessante Beispiele für die Entwaldung in den examples/ Ordnern, einschließlich baumarischer Datenstrukturen. Tatsächlich haben wir alle Stichproben aus den vorherigen Arbeiten zur Call-by-Wert-Superkompilation höherer Ordnung von Peter A. Jonsson und Johan Nordlander 4 5 neu implementiert. In allen Fällen hat Mazeppa ähnlich oder besser durchgeführt.
Betrachten Sie nun ein anderes Beispiel: Diesmal beinhaltet eine teilweise Bewertung:
[ 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 implementiert den berühmten Algorithmus zur Exponentiation durch Quellen. Das ursprüngliche Programm ist ineffizient: Es untersucht rekursiv den x Parameter von powerSq , obwohl es zur Kompilierungszeit perfekt bekannt ist. Das Laufen von Mazeppa auf main(a) liefert das folgende Restprogramm:
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
Die gesamte powerSq -Funktion wurde eliminiert, wodurch die Wirkung der teilweisen Bewertung erreicht wurde. (Wenn wir powerSq als Interpreter für ein Programm x und Eingabedaten a betrachten, dann ist es die erste Futamura -Projektion: Spezialisierung eines Interpreters, um ein effizientes Zielprogramm zu erhalten.) Außerdem beachten Sie, wie der Supercompiler das Argument *(a, *(a, a)) zweimal geschafft hat, so dass es nicht jeweils neu eingestellt ist. Das Restprogramm spiegelt tatsächlich die Exponentiation durch Quadrate wider.
Lassen Sie uns über die Entwaldung und eine teilweise Bewertung hinausgehen. Betrachten Sie eine Funktion matches(p, s) von zwei Zeichenfolgen, die T() zurückgeben, wenn s p und F() enthält, sonst. Die naive Implementierung in Mazeppa wäre Folgendes, wobei p auf "aab" spezialisiert ist:
[ 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)
};
(Hier repräsentieren wir Strings als Charakterlisten für die Einfachheit, aber keine Sorge, Mazeppa bietet auch integrierte Saiten.)
Der Algorithmus ist korrekt, aber ineffizient. Überlegen Sie, was passiert, wenn "aa" erfolgreich abgestimmt ist, aber 'b' nicht. Der Algorithmus beginnt erneut mit "aab" aus dem zweiten Charakter von s , obwohl bereits gesagt werden kann, dass der zweite Charakter von s 'a' ist. Der deterministische endliche Automaton, der vom Knuth-Morris-Pratt-Algorithmus (KMP) 6 erstellt wurde, ist eine alternative Möglichkeit, dieses Problem zu lösen.
Durch das Ausführen von Mazeppa auf der obigen Probe können wir einen effizienten String -Matching -Algorithmus für p="aab" erhalten, der KMP in Aktion widerspiegelt:
[ 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()
};
Der von uns geschriebene naive Algorithmus wurde automatisch in eine bekannte effiziente Version verwandelt! Während der naive Algorithmus Komplexität O (| P | * | S |) hat, ist der Spezialisierte o (| S |) .
Das Synthese von KMP ist ein Standardbeispiel, das die Kraft der Superkompilation in Bezug auf andere Techniken zeigt (z. B. siehe 7 und 8 ). Das Erhalten von KMP durch partielle Bewertung ist nicht möglich, ohne die ursprüngliche Definition von matches 9 10 zu ändern.
Valentin Turchin, der Erfinder der Superkompilation, beschreibt das Konzept des Metasystem -Übergangs auf folgende Weise 11 12 13 :
Betrachten Sie ein System jeglicher Art. Nehmen wir an, dass es eine Möglichkeit gibt, eine Reihe von Kopien daraus zu machen, möglicherweise mit Variationen. Nehmen wir an, dass diese Systeme in ein neues System -S -System vereint sind, das über die Systeme des S -Typs als Subsystem verfügt, und auch einen zusätzlichen Mechanismus umfasst, der das Verhalten und die Produktion der S -Subsystems steuert. Dann nennen wir S ' ein Metasastem in Bezug auf S und die Erschaffung von S' A Metasastem -Übergang. Infolge des aufeinanderfolgenden Metasystem -Übergangs entsteht eine mehrstufige Kontrollstruktur, die komplizierte Verhaltensformen ermöglicht.
Somit kann die Superkompilation leicht als Metasystem -Übergang angesehen werden: In Mazeppa gibt es ein Objektprogramm, und es gibt den Mazeppa Supercompiler, der die Ausführung des Objektprogramms kontrolliert und überwacht. Wir können jedoch weiter gehen und eine beliebige Anzahl von Metasystem -Übergängen im Bereich des Objektprogramms selbst durchführen, wie das nächste Beispiel zeigt.
Wir werden den Code aus examples/lambda-calculus/ verwenden. Im Folgenden finden Sie ein Verfahren zur Normalisierung von Normalisierung durch Evaluierung zum Erhalten von Beta-Normalformen von nicht typed Lambda Calculus-Begriffen:
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 werden manchmal als reflect / reify bezeichnet.)
Dies ist im Wesentlichen eine große Maschine für eine effiziente Erfassungssubstitution: Anstatt Begriffe zu jeder Beta-Reduktion zu rekonstruieren, behalten wir eine Werteumgebung bei. eval projiziert einen Begriff in die "semantische Domäne", während quote das Gegenteil tut. normalize ist einfach die Zusammensetzung von quote und eval . Um nicht mit der Erzeugung der frischen Namen zu stören, haben wir die Bruijn -Indizes in den Var -Konstruktor und in die Bruijn -Ebene in NVar gesteckt. Letzteres wird in quoteNeutral in die erstere umgewandelt.
Lassen Sie uns nun etwas mit dieser Maschine berechnen:
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))))));
Die main berechnet die normale Form des Lambda -Begriffs example() , der die Kirchenzahlen two() und three() multipliziert.
Durch die Superkompilierung main() erhalten wir die Kirchenzumme von 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)))))))));
Der Lambda Calculus Interpreter wurde vollständig vernichtet!
In diesem Beispiel haben wir gerade eine zweistöckige Metas-Treppe (in Turchins Terminologie 14 ) gesehen: Auf Stufe 0 haben wir das Mazeppa Supercompiler das Objektprogramm, während wir auf Stufe 1 das Objektprogramm normalisieren, die Lambda Calculus-Begriffe normalisieren. Es kann eine willkürliche Anzahl von Interpretationsniveaus geben, und Mazeppa kann verwendet werden, um sie alle zusammenzubrechen. Dieses allgemeine Verhalten der Superkompilation wurde von Turchin selbst in 1 (Abschnitt 7) untersucht, wo er in beiden Fällen zwei interpretierbare Programme, eine fortranartig und eine in LISP, überkompilieren konnte, um einen Beschleunigungsfaktor von 40 zu erhalten.
Der Lambda-Normalizer zeigt uns auch, wie wir Funktionen höherer Ordnung in eine Sprache erster Ordnung inkarnieren können. In Mazeppa können wir Funktionen nicht als Werte behandeln, aber es bedeutet nicht, dass wir sie nicht simulieren können! Durch die Durchführung eines Metasastem-Übergangs können wir Funktionen höherer Ordnung in einer Sprache erster Ordnung effizient implementieren. Zusammen mit der Defunktionalisierung und der Verschlussumwandlung kann diese Technik zur Zusammenstellung von Sprachen höherer Ordnung in einen effizienten Code erster Ordnung erster Ordnung verwendet werden.
Verwandte Beispiele: Imperative virtuelle Maschine, Selbstinterpreter.
Rückblickend ist das Hauptproblem, das die weit verbreitete Einführung der Superkompilation verhinderte, die Unvorhersehbarkeit - die dunkle Seite seiner Macht. Um ein Gefühl dafür zu bekommen, was es bedeutet, überlegen Sie, wie wir jedes SAT -Problem "im laufenden Flug" lösen können:
[ 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)
};
Mit diesem vollkommen korrekten Code sind zwei Dinge falsch: 1) Der Supercompiler erweitert die Formel im Exponentialraum und 2) der Supercompiler versucht, die erweiterte Formel in Exponentialzeit zu lösen. Manchmal möchten wir einfach nicht alles zur Kompilierung bewerten.
Verzweifelt jedoch nicht: Wir bieten eine Lösung für dieses Problem. Lassen Sie uns zunächst überlegen, wie Sie die Lösung der Formel auf die Laufzeit verschieben. Es stellt sich heraus, dass das einzige, was wir tun müssen, die formula mit @extract wie folgt kommentieren muss:
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
Wenn Mazeppa solve(formula(a, b, c, d, e, f, g)) sieht, extrahiert sie den Aufruf zur formula in eine frische Variable .v0 und fährt fort, den extrahierten Aufruf und solve(.v0) isoliert zu übertreffen. Der letztere Anruf reproduziert nur den ursprünglichen SAT -Solver.
Aber die Aufnahme des Aufrufs zur formula führt weiterhin zu einem exponentiellen Blowup. Lassen Sie uns untersuchen, warum dies passiert. Unsere ursprüngliche Formel besteht aus Anrufen zu or and ; Während or offensichtlich nicht gefährlich ist and den rest an beide Zweige von If (der erste match -Fall) ausbreitet - ist dies der genaue Ort, an dem der Blowup auftritt. Lassen Sie uns also auch and @extract markieren:
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
Das ist es! Wann and zu transformieren, wird Mazeppa den Ruf aus seinem umgebenden Kontext herausholen und isoliert überkompilieren. Durch das Hinzufügen von zwei Annotationen an geeigneten Stellen haben wir sowohl das Problem des Codeblass als auch an der exponentiellen Laufzeit der Superkompilation gelöst. Im Allgemeinen, wenn Mazeppa ctx[f(t1, ..., tN)] sieht, ist f markiert @extract und ctx[.] Ein nicht leerer Umgebungskontext mit . In einer Redex -Position steckt es eine frische Variable v in ctx und transformiert die folgenden Knoten separat: f(t1, ..., tN) und ctx[v] .
Beachten Sie schließlich, dass @extract nur ein Mechanismus mit niedrigem Niveau ist. Ein Compiler-Front-End muss zusätzliche Maschinen ausführen, um Mazeppa zu mitteilen, die extrahieren können. Dies kann auf zwei Arten erfolgen:
formula als and als extrahierbar markieren, wodurch alle anderen Funktionen unberührt werden.Beide Methoden können kombiniert werden, um einen gewünschten Effekt zu erzielen.
Mazeppa verwendet eine interessante Designwahl, um eifrige Funktionen und faule Konstruktoren zu haben. Das folgende Beispiel, in dem magic(1u32, 1u32) Fibonacci -Zahlen erzeugt, wurde von Haskell übernommen:
[ 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))
}
};
Wenn Konstruktoren eifrig wären, würde magic(1u32, 1u32) niemals enden. Cons bewertet seine Argumente jedoch nicht! Da getIt nur einen endlichen Teil der unendlichen Liste konsumiert, endet und druckt das Programm 2u32 :
$ mazeppa eval
2u32
Lazy Constructors ermöglichen mühelose Abholzung, wie unten erläutert.
Nach der Installation von Mazeppa über opam oder ./scripts/install.sh ist es als OCAML -Bibliothek erhältlich!
Richten Sie wie folgt ein neues Dune -Projekt ein:
$ dune init project my_compiler
Fügen Sie mazeppa als Bibliothek von Drittanbietern in Ihren bin/dune :
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
Fügen Sie den folgenden Code in bin/main.ml ein (dies sind examples/sum-squares/main.mz die in OCAML codiert sind):
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
;; Führen Sie dune exec my_compiler aus, um das gewünschte Restprogramm anzuzeigen:
[([], "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))))]
)))
]
Sie können Mazeppa so oft anrufen, wie Sie möchten, auch parallel. Beachten Sie, dass wir dem Supercompiler eine begrenzte Schnittstelle zur Verfügung stellen. Insbesondere gibt es keine Möglichkeit, zu prüfen, was es im Prozess tut (dh --inspect ).
Neben der Superkompilation bieten wir auch einen integrierten Bewerter an:
val eval : Raw_program .t -> Raw_term .t Es kann nur zu Programmen aufgerufen werden, deren main keine Parameter akzeptieren. Im Gegensatz zu supercompile erzeugt es einen ausgewerteten Begriff von Typ Raw_term.t und kann möglicherweise abweichen.
Siehe andere API -Funktionen und ihre Dokumentation in lib/mazeppa.mli .
Angenommen, main.mz enthält eine leicht modifizierte Version des faulen Fibonacci -Beispiels:
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))
}
};
Der folgende Befehl übersetzt es in C11 mit GNU -Erweiterungen (dh, -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 );
} Für den Befehl translate werden sowohl --language , die Zielsprache für die Übersetzung, als auch --entry , was der Name eines externen Symbols ist, das Ihrer main entspricht. Das Input Mazeppa -Programm stammt aus stdin ( cat main.mz in unserem Beispiel); Das Ausgangsgnu11 -Programm ist in stdout geschrieben.
Lassen Sie uns weiter voranschreiten und das Ausgabeprogramm in eine Objektdatei kompilieren. Erstens kopieren Sie c/deps/sds.c , c/deps/sds.h und c/deps/sdsalloc.h in Ihr aktuelles Verzeichnis; Zweitens installieren Sie Boehm GC auf Ihrem Computer:
$ sudo apt install libgc-dev -y
Führen Sie dann den folgenden Befehl aus:
$ cat main.mz
| mazeppa translate --language C --entry fib --dump-header-to .
| gcc -c -o program.o -std=gnu11 -xc -
Die --dump-header-to Option schreibt den Inhalt von mazeppa.h an einen bestimmten Ort; Dies ist erforderlich, damit das Ausgabeprogramm kompiliert wird. Der gcc -Befehl akzeptiert das Ausgabeprogramm von stdin und produziert program.o .
Nun bleibt nun, um die generierte fib -Funktion tatsächlich aufzurufen. Erstellen Sie main.c mit dem folgenden Inhalt:
#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 ));
} Dieses "Treiber" -Programm ruft fib nur mit einer Mazeppa Integer ( MZ_INT ) auf und druckt das Ergebnis. Sie können jede Funktionalität von mazeppa.h verwenden, vorausgesetzt, sie sind nicht mit mz_priv_ oder MZ_PRIV_ vorangestellt.
Alle Teile zusammenbringen:
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out druckt fib(10) = 55 und beendet sich erwartungsgemäß.
--inspect : Verwenden Sie es nur für Debugging -Zwecke.@extract (wie oben gezeigt), um zu steuern, ob die Superkompilation fortgesetzt oder die Redex extrahiert werden soll."otus" kleiner als "octopus" , aber "octopusx" nicht. Mazeppa verwendet mehrere interessante Designoptionen (eingestuft nach Wichtigkeit):
Code erster Ordnung. Max Bolingbroke und Simon Peyton Jones 15 berichten, dass für ein bestimmtes Beispiel der Supercompiler höherer Bestellung für eine Teilmenge von Haskell 42% der Ausführungszeit für die Verwaltung von Namen und Umbenennen ausgegeben hat. Während es wahr ist, dass vereinfachte Bewertungsmodelle wie die Normalisierung von Lambda -Begriffen es uns ermöglichen, einen signifikanten Aufwand bei der Vermeidung von Erfassungen zu vermeiden, ist die Superkompilation komplizierter. Neben der symbolischen Berechnung muss die Superkompilation zuvor berechnete Ergebnisse analysieren, um fundierte Entscheidungen über die weitere Transformation zu treffen: Betrachten Sie Terminstanztests, homomorphe Einbettentests, die meisten spezifischen Verallgemeinerungen usw. Die Einführung von Funktionen höherer Ordnung, die all diese Analysen unzureichend beeinträchtigen, machen die Erzeugung, die Superkonkurrenten zu erregen, und harte, die zu härteren, die harteren Verbraucher zu machen. In Mazeppa halten wir uns an die Philosophie allmählicher Verbesserungen: Anstatt zu versuchen, mit vielen ausgefallenen Merkmalen gleichzeitig umzugehen, führen wir die Kernsprache für bequeme Manipulation durch eine Maschine 2) so viele Metasastem -Übergänge durch, um die Kernsprache für den Menschen zu verbessern.
Faule Konstruktoren. Es ist eine bekannte Beobachtung, dass Call-by-Wert-Sprachen schwierig für die ordnungsgemäße Entwaldung sind. Es ist immer noch möglich, sie zu entfassen, aber nicht ohne zusätzliche Analyse 4 5 . Wenn Konstruktoren jedoch faul sind (dh sie bewerten ihre Argumente nicht), funktioniert die Entwaldung nur . Turchin ließ es durch die Transformation einer Call-by-Wert-Sprache normaler Ordnung funktionieren, aber das Ergebnis ist, dass der Restcode häufiger endet. In Mazeppa haben wir Call-by-Wert-Funktionen und Call-by-Namen-Konstruktoren (Call-by-by-Need), die 1) die Entwaldung ermöglichen und 2) die ursprüngliche Semantik des Codes bewahrt.
Termfreie Prozessgraphen. In Mazeppa enthalten Prozessdiagramme keine Verweise auf Begriffe: Die Residualisierung kann ohne sie funktionieren. Infolgedessen kann der Müllsammler Begriffe beenden, die beim Bau eines Untergraphen verwendet wurden. Darüber hinaus hat diese Richtlinie einige andere wichtige Vorteile: 1) Die Grafik ist immer noch zur Inspektion mit --inspect , 2) Wenn sie gezogen wird, enthüllt sie nur Informationen über die Entscheidungen, die der Supercompiler aufgenommen hat, was es viel einfacher macht, es zu betrachten. Mehrere vorhandene Superkompiler untertäuschen auf ordnungsgemäße Prozessdiagramme (z. B. Neil Mitchells Supero 17 und die oben genannten 15 ). Infolgedessen sind sie jedoch weniger in der Lage, von einem Benutzer zu inspizieren.
Zweidimensionale Konfigurationsanalyse. Normalerweise behält ein Superkompiler eine "Geschichte" einer Untergruppe aller Vorfahren, während er einen Knoten verwandelt. Wenn dieser Knoten einem seiner Vorfahren "nahe genug" ist, ist es Zeit, den Begriff in kleinere Teile zu unterteilen, um die Kündigung zu garantieren. In Mazeppa führen wir stattdessen zwei separate Datenstrukturen: diejenige, die eine Untergruppe der Vorfahren des Knotens enthält, und die eine, die eine Teilmenge vollständig transformierter Knoten enthält. Die erstere Datenstruktur wird verwendet, um die Beendigung (wie gewohnt) zu garantieren, während letztere zur Verbesserung der Austausch von Funktionen im Restcode verwendet wird. Wenn der aktuelle Knoten (von besonderer Art) ein Umbenennen einiger zuvor transformierter Knoten ist, falten wir den aktuellen Knoten in diesen vorherigen Knoten. Auf diese Weise führt Mazeppa sowohl die vertikale als auch die horizontale Analyse von Konfigurationen durch, wodurch der Restcode kompakter und Superkompilation effizienter wird.
Funktionsproduktivitätsanalyse. Wenn eine innere Funktion Musteranpassungen einen unbekannten Wert aufruft, passieren zwei potenziell gefährliche Dinge: 1) Die Superkompilation reproduziert die Struktur der Musteranpassungsfunktion, 2) Die Superkompilation bringt den gesamten umgebenden Kontext auf alle Zweige dieser Funktion. Ohne weitere Kontrolle kann diese Situation zu einer erheblichen Explosion der Codegröße führen, was manchmal sogar dazu führt, dass ein Superkompiler nicht in angemessener Zeit endet. Um zu verbessern, dupliziert Mazeppa den Kontext, den dieser innere Aufruf aus mindestens einem Ausstiegspunkt erzeugt, denn wenn dies der Fall ist, kann große Chancen, dass dieser Wert durch nachfolgende Musteranpassung dekonstruiert werden kann. Andernfalls extrahiert Mazeppa den inneren Anruf und transformiert ihn isoliert (als ob er mit @extract markiert wäre). Wenn der Kontext tatsächlich dupliziert ist, gilt die folgende Regel für alle Zweige: Wenn der Zweig einen bestimmten Wert auf oberster Ebene aus allen Exit-Punkten erzeugt, wird er wie gewohnt im Kontext transformiert. Andernfalls wird der Zweig aus dem Kontext extrahiert und isoliert transformiert. In der Praxis verhindert diese Analyse eine große Menge unnötiger Spezialisierungen, wodurch die Größe der Restprogramme kompaktiert und die Superkompilation viel nachvollziehbarer wird.
Smart Histories. Anstatt einen aktuellen Knoten blind mit all seinen Vorfahren zu vergleichen, verwenden wir eine feinkörnigere Kontrolle, dh 1) Globale Knoten (diejenigen, die eine unbekannte Variable analysieren) nur mit globalen Knoten verglichen werden, 2) lokale Knoten (diejenigen, die linear in einem einzigen Schritt reduzieren) werden mit lokalen Knoten nur mit den neuesten globalen Noden, die im Vergleich zu den TRIVE-Tätigkeiten, die im Vergleich zu den Tätern, und 3). anders. Dieses System ermöglicht es von Mazeppa neben einem wirtschaftlicheren Ansatz bei der Begleitprüfung mehr Optimierungsmöglichkeiten. Siehe 18 , Abschnitte 4.6 und 4.7. Die Beendigung der Superkompilation wird durch die Tatsache garantiert, dass die homeromorphe Einbettung immer noch an allen potenziell unendlichen Subsequenzen globaler und lokaler Begriffe getestet wird (es kann nicht nur eine unendliche Folge trivialer Begriffe existieren).
STEX -Signaturen reduzieren. Die Pfeife wird nur zu Begriffen mit gleichen Redex -Signaturen getestet. Eine Redex -Signatur ist ein Paar von 1) das Symbol einer Funktion und 2) eine Liste von Argumentwertkategorien . Eine Wertungskategorie ist eine Art MetainFormation über ein Argument, das entweder 1) VConst für Werte wie 42i32 oder "hello world" , 2) VNeutral für Werte wie x oder +(x, x) oder 3) VCCall(c) für Konstruktoraufrufe wie Foo(...) sein kann. Die Pfeife wird immer noch auf allen potenziell unendlichen Sequenzen von Begriffen getestet, da jede unendliche Sequenz mindestens eine unendliche Untersequenz von Begriffen mit derselben Redex -Signatur enthalten muss. Diese Strategie ermöglicht Mazeppa, in bestimmten Fällen eine Über-Generalisierung zu vermeiden, wie die folgenden zwei Beispiele zeigen:
f(A()) in f in f(g(B(A()))) eingebettet; Da die Redex -Operatoren jedoch unterschiedlich sind ( f und g ), setzt Mazeppa die Reduzierung fort und erreicht das ideale Ergebnis.f(A(Good())) in f(f(f(B(A(Good()))))) und f Redex-Operator in beiden Fällen ist Mazeppa nicht übergeneralisiert, weil diese beiden Begriffe f Wertkategorien in ihren B(...) A(...) Signaturen haben: In der ersten Fall. Genau wie im vorherigen Beispiel erreicht Mazeppa das ideale Ergebnis der Superkompilation ausschließlich durch Reduktion.Optimierte homomorphe Einbettung. Im Laufe der Jahrzehnte hat die homeromorphe Einbettung Ruf als hervorragende Methode für die Online -Kündigung überprüft 19 . Leider kann der nichtlineare Kontrollfluss (wenn sowohl das Tauchen als auch die Kopplung gelten) aufgrund des nicht linearen Kontrollflusss unentschuldbar teuer zu berechnen. Was noch schlimmer ist, es wird für alle qualifizierenden übergeordneten Knoten erneut ausgeführt, wenn ein neuer Begriff zur Geschichte hinzugefügt wird, was die Superkompilation mit zunehmendem Historie zunehmend verlangsamt: so weit das Essen des größten Teils der Superkompilationszeit! Um damit fertig zu werden, behalten wir zwei getrennte Caches bei:
Hash. Die oben beschriebenen homomorphen Einbettungsdarsteller hängen davon ab, wie viele Begriffe geteilt werden. Wir verwenden daher den Hash -Umsatz bei der Entfaltung von Funktionskörpern: Wenn ein neuer Begriff t strukturell einiger vorhandener Begriff s entspricht, wird letzteres wiederverwendet. Um Speicherlecks zu vermeiden, verwenden wir ein globales Ephemeron, das schwache Zeiger bis hin zu Begriffen hält. Neben einer verbesserten Superkontrolle (aufgrund der Memoisierung) verringert auch Hash -Rückgänge den Speicherverbrauch - siehe #4 (Kommentar).
Normalisierung während der Entfaltung. Wenn sich ein Funktionsaufruf entfaltet, ersetzen wir die Parameter und normalisieren den Körper so weit wie möglich (dh ohne weitere Entfaltungen, um die Kündigung zu gewährleisten). Betrachten Sie die faktorielle Funktion f(n) ; Bei einer einfachen Entfaltung würden wir in einer unangenehmen Situation fangen, in der f(1u32) in *(1u32, f(-(1u32, 1u32))) eingebettet ist, was zu einer über Generalalisierung führt. In Wirklichkeit würde Mazeppa f(1u32) bis *(1u32, f(0u32)) entfalten, was letztere zu einem Kandidaten für die weitere Entfaltung macht. Dieser Ansatz wurde in 20 , Abschnitt 4.5 vorgeschlagen. Die anderen Verdienste sind: 1) weniger Arbeit für zukünftige Fahrschritte, 2) weniger "banale" Berechnung in Prozessgraphen, 3) reduzierte Menge teurer homomorpher Einbettungstests.
*(1u32, f(-(1u32, 1u32))) aufgrund verschiedener Redex-Operatoren nicht mehr gegen f(1u32) überprüft. Andere Vorteile der Normalisierung halten jedoch immer noch.Implementierung in OCAML. Mazeppa wird unter Verwendung einer Kombination aus funktionalen und imperativen Programmierstilen implementiert, die in OCAML sehr natürlich ist. Ausnahmen werden nicht nur für "außergewöhnliche" Situationen verwendet, sondern die Veränderlichkeit innerhalb der Funktionen ist häufig. Obwohl wir keinen ähnlichen Supercompiler haben, der in EG Haskell oder Rost zum Vergleich geschrieben wurde, glauben wir, dass es sich um OCAML handelt, das uns eine funktionierende Implementierung gegeben hat, ohne sich mit der Sprache streiten zu müssen und nie die Arbeit zu beenden.
Während die meisten der oben genannten nicht besonders neu sind, glauben wir, dass die Kombination dieser Merkmale Mazeppa zu einer praktischeren Alternative macht als ihre Vorgänger.
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 ).Notes:
_ ) 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 | Bedeutung |
|---|---|
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 | Notizen |
|---|---|---|
// ... 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 ; Dann: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. Programm. Lang. Syst. 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. Sci. 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. Elektron. Notes Theor. Comput. Sci. 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. Vol. 2. No. 4.2. 2010. ↩
