mazeppa
v0.4.3
SuperCompilation 1 هي تقنية تحويل البرنامج التي تقيّم رمزًا برنامجًا معينًا ، مع قيم وقت التشغيل غير معروفة. عند القيام بذلك ، يكتشف أنماط تنفيذ البرنامج الأصلي وتجميعها في وظائف مستقلة ؛ نتيجة supercompilation هو برنامج متبقي أكثر كفاءة. فيما يتعلق بالقوة التحويلية ، فإن SuperCompilation يستمع إلى كل من إزالة الغابات 2 والتقييم الجزئي 3 ، وحتى يعرض قدرات معينة من النظريات التي تثبت.
Mazeppa هو SuperCompiler الحديث الذي يهدف إلى أن يكون هدفًا تجميعًا للغات الوظيفية للاتصال بالقيمة. وجود supercompilers سابقة المقارنة والمراجعة بجد ، 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 هو برنامج قوي ومتخصص في OCAML. إذا قمت ببناء Mazeppa مع مترجم OCAML الذي يدعم Flambda ، فقد ترى أداء أفضل بكثير. لإعداده:
$ 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 Code بواسطة امتداد SVG Preview.
./scripts/play.sh ستعيد ترجمة المصادر تلقائيًا في OCAML ، إذا تم تغيير أي شيء.
على سبيل المثال أفضل طريقة لفهم كيفية عمل SuperCompilation. ضع في اعتبارك الوظيفة التالية التي تأخذ قائمة وتحسب مجموع عناصرها المربعة:
[ 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 ، وهي حالة خاصة من supercompilation.
دعونا نرى ما يفعله 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 : يعمل SuperCompiler الخاص بنا مع هذا التمثيل المحدد بدلاً من البرنامج الأصلي.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
};
قام SuperCompiler بدمج sum و mapSq بنجاح في وظيفة واحدة ، f0 ! على عكس البرنامج الأصلي ، يعمل f0 في تمريرة واحدة ، دون الحاجة إلى تخصيص أي ذاكرة إضافية.
كيف وصلت SuperCompiler إلى هذه النقطة؟ دعونا نرى الرسم البياني للعملية المولدة:
للرجوع إليها ، يحتوي 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 لهذا المثال الصغير ، ولكن لا تتردد في النظر إليه: إنه ليس معقدًا للغاية.)
يبدأ SuperCompiler مع العقدة n0 التي تحتوي على main(xs) . بعد خطوتين من الوظيفة ، نصل إلى العقدة n2 التي تحتوي على sum(.g1(xs)) ، حيث .g1 هي وظيفة الأشعة تحت الحمراء التي تتوافق مع 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))) n8 n11 .v4=sum(.g1(.v1)) إلى .v3=*(.v0, .v0) +(.v3, .v4) *( n13 والسبب في القيام بذلك هو أن العقدة السابقة ( n2 ) مضمنة هيكلياً في n7 ، لذلك قد يستمر SuperCompilation إلى الأبد. الآن ، ماذا يحدث مع 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 .
باختصار ، يتكون SuperCompilation من 1) تعريفات الوظائف التي تتكشف ، 2) تحليل المكالمات التي تطابق النمط متغيرًا غير معروف ، 3) تقسيم الحساب إلى أجزاء أصغر ، 4) حسابات متكررة قابلة للطي ، و 5) مكالمات متحللة لا يمكن الكشف عنها ، مثل +(.v3, .v4) ( n13 ) في مثالنا. يتم ضمان الانتهاء من عملية SuperCompilation بأكملها ، لأنه عندما تصبح بعض الحسابات أكبر وأكبر بشكل خطير ، نقوم بتقسيمها إلى مشكلات فرعية وحلها بمعزل عن ذلك.
هناك الكثير من الأمثلة الأخرى المثيرة للاهتمام من إزالة الغابات في examples/ المجلد ، بما في ذلك هياكل البيانات الشبيهة بالأشجار. في الواقع ، قمنا بإعادة تنفيذ جميع العينات من العمل السابق على SuperCompilation من الدرجة العليا للاتصال من قبل بيتر أ. جونسون وجوهان نوردلاندر 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: متخصص في المترجم المترجم للحصول على برنامج مستهدف فعال.) لاحظ أيضًا كيف تمكن SuperCompiler من مشاركة الوسيطة *(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)
};
(هنا نمثل سلاسل كقوائم من الأحرف للبساطة ، ولكن لا تقلق ، يوفر Mazeppa سلاسل مدمجة أيضًا.)
الخوارزمية صحيحة ولكنها غير فعالة. فكر في ما يحدث عندما يتم مطابقة "aa" بنجاح ، ولكن 'b' ليس كذلك. ستبدأ الخوارزمية في مطابقة "aab" مرة أخرى من الشخصية الثانية لـ s ، على الرغم من أنه يمكن القول بالفعل أن الشخصية الثانية لـ s 'a' . يعد Automaton المحدود المحدد الذي تم بناؤه بواسطة خوارزمية Knuth-Morris-Pratt (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 .
يصف Valentin Turchin ، مخترع SuperCompilation ، مفهوم انتقال نظام MetaSystem بالطريقة التالية 11 12 13 :
النظر في نظام من أي نوع. لنفترض أن هناك طريقة لجعل بعض النسخ منه ، ربما مع الاختلافات. لنفترض أن هذه الأنظمة متحدة في نظام جديد يحتوي على أنظمة من نوع S كنظمه الفرعية ، وتتضمن أيضًا آلية إضافية تتحكم في سلوك وإنتاج Subsystems . ثم نسمي S ' A MetAsystem فيما يتعلق بـ S ، وإنشاء S' A MetAsystem Transition. نتيجة للتحولات المتتالية لتصنيع MetAsystem ، ينشأ بنية تحكم متعددة المستويات ، مما يسمح بأشكال معقدة من السلوك.
وبالتالي ، يمكن اعتبار SuperCompilation بسهولة بمثابة انتقال MetaSystem: يوجد برنامج كائن في Mazeppa ، وهناك Mazeppa Supercompiler الذي يتحكم ويشرف على تنفيذ برنامج الكائن. ومع ذلك ، يمكننا الذهاب إلى أبعد من ذلك وإجراء أي عدد من انتقالات نظام metAsystem داخل عالم برنامج الكائن نفسه ، كما يوضح المثال التالي.
سنستخدم الكود من examples/lambda-calculus/ . فيما يلي إجراء تطبيع قياسي حسب التقدير للحصول على أشكال بيتا الطبيعية لمصطلحات حساب حساب التفاضل والتكامل اللامسق غير المعقدة:
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 Bustructor و 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 الشكل الطبيعي لمثال Lambda 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 تمامًا!
في هذا المثال ، شاهدنا للتو درجًا من مستويين من مستويين (في مصطلحات Turchin 14 ): في المستوى 0 ، لدينا Mazeppa Supercompiler يحول برنامج الكائن ، بينما في المستوى 1 ، لدينا برمجة الكائن التي تطبيع مصطلحات حساب Lambda. يمكن أن يكون هناك عدد تعسفي لمستويات التفسير ، ويمكن استخدام Mazeppa لانهيارها جميعًا. تم استكشاف هذا السلوك العام للتشكيل الفائق من قبل Turchin نفسه في 1 (القسم 7) ، حيث تمكن من SuperCompile برنامجين قابلين للتفسير ، واحد يشبه فورتران وواحد في Lisp ، للحصول على عامل تسريع من 40 في كلتا الحالتين.
يوضح لنا معهد Lambda أيضًا كيفية تجسد الوظائف ذات الترتيب العالي في لغة من الدرجة الأولى. في Mazeppa ، لا يمكننا التعامل مع الوظائف كقيم ، لكن هذا لا يعني أننا لا نستطيع محاكاةها! من خلال إجراء انتقال 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) سيقوم SuperCompiler بتوسيع الصيغة في الفضاء الأسي ، و 2) سيحاول SuperCompiler حل الصيغة الموسعة في الوقت الأسي. في بعض الأحيان ، لا نريد تقييم كل شيء في وقت الترجمة.
ومع ذلك ، اليأس لا: نحن نقدم حل لهذه المشكلة. دعونا أولاً نفكر في كيفية تأجيل حل الصيغة حتى وقت التشغيل. اتضح أن الشيء الوحيد الذي يتعين علينا القيام به هو التعليق على 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 SAT الأصلي.
لكن Supercompling ، سيظل النداء إلى formula يؤدي إلى تفجير أسي. دعونا ندرس لماذا يحدث هذا. تتكون صيغةنا الأصلية من مكالمات إلى or and ؛ بينما من الواضح or غير خطير ، and معلمة rest لكلا فرعين If (حالة match الأولى) - هذا هو المكان بالضبط الذي يحدث فيه الانفجار. لذلك دعونا نضع علامة and @extract أيضًا:
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
هذا هو! متى and تحويلها ، ستستخلص Mazeppa من السياق المحيط به و supercompile في عزلة. من خلال إضافة اثنين من التعليقات التوضيحية في الأماكن المناسبة ، قمنا بحل كل من مشكلة تفجير التعليمات البرمجية ووقت التشغيل الأسي للتشغيل الفائق. بشكل عام ، عندما يرى Mazeppa ctx[f(t1, ..., tN)] ، حيث يتم وضع @extract f و ctx[.] هو سياق محيط غير فارغ مع . في موضع REDEX ، سيقوم بتوصيل متغير جديد v إلى ctx ويتابع تحويل العقد التالية بشكل منفصل: f(t1, ..., tN) و ctx[v] .
أخيرًا ، لاحظ أن @extract ليست سوى آلية منخفضة المستوى ؛ يجب أن يقوم الواجهة الأمامية للمترجم آلية إضافية لإخبار Mazeppa والتي تعمل على الاستخراج. يمكن القيام بذلك بطريقتين:
formula and قابلة للاستخراج ، مما يترك جميع الوظائف الأخرى دون أن تمس.يمكن الجمع بين كلتا الطريقتين لتحقيق التأثير المطلوب.
توظف Mazeppa اختيار تصميم مثير للاهتمام للحصول على وظائف حريصة ومشاركات كسول. المثال التالي ، حيث تم اعتماد magic(1u32, 1u32) أرقام فيبوناتشي ، من هاسكل:
[ 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 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 عدة مرات كما تريد ، بما في ذلك بالتوازي. لاحظ أننا نعرض واجهة محدودة إلى SuperCompiler ؛ على وجه الخصوص ، لا توجد طريقة لتفقد ما تفعله في هذه العملية ( --inspect ،
إلى جانب SuperCompilation ، نقدم أيضًا مُقيِّمًا مدمجًا:
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 . يأتي برنامج المدخلات Mazeppa من 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 .
الآن ما تبقى هو في الواقع استدعاء وظيفة 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 مع عدد صحيح Mazeppa ( 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 (كما هو موضح أعلاه) للتحكم في ما إذا كان يجب متابعة SuperCompilation أو استخراج Redex."otus" أصغر من "octopus" ولكن "octopusx" ليس كذلك. توظف Mazeppa العديد من خيارات التصميم المثيرة للاهتمام (المرتبة حسب الأهمية):
رمز الترتيب الأول. ذكر Max Bolingbroke و Simon Peyton Jones 15 أنه بالنسبة لمثال معين ، أمضى SuperCompiler العالي من الدرجة الأولى لمجموعة فرعية من Haskell 42 ٪ من وقت التنفيذ على إدارة الأسماء وإعادة تسميتها. على الرغم من أنه من الصحيح أن نماذج التقييم البسيطة ، مثل تطبيع مصطلحات Lambda ، تسمح لنا بتجنب النفقات العامة الكبيرة لتجنب التقاط ، إلا أن supercompilation أكثر تعقيدًا. على سبيل المثال ، إلى جانب إجراء حساب رمزي ، يحتاج SuperCompilation إلى تحليل النتائج المحسوبة مسبقًا لاتخاذ قرارات مستنيرة بشأن مزيد من التحول: النظر في اختبارات مثيل المصطلح ، واختبارات التضمين المثلية ، والتعميمات الأكثر تحديدًا ، وما إلى ذلك. في Mazeppa ، نلتزم بفلسفة التحسينات التدريجية: بدلاً من محاولة التعامل مع العديد من الميزات الفاخرة في نفس الوقت ، نحن 1) إصلاح اللغة الأساسية للتلاعب المريح بواسطة آلة ، 2) أداء أكبر عدد ممكن من انتقالات نظام MetaSyster لجعل اللغة الأساسية أفضل للإنسان.
بنيات كسول. إنها ملاحظة معروفة أن لغات النداء على حدة صعبة لإزالة الغابات. لا يزال من الممكن إزالة الغابات ، ولكن ليس بدون تحليل إضافي 4 5 . ومع ذلك ، إذا كان المنشئون كسولًا (أي أنهم لا يقيمون حججهم) ، فإن إزالة الغابات تعمل فقط . جعلت Turchin أنها تعمل من خلال التحول الطبيعي للغة كل شيء على حدة ، ولكن النتيجة هي أن الكود المتبقي قد ينتهي في كثير من الأحيان. في Mazeppa ، لدينا وظائف بالاتصال على حدة ومكالمات من خلال اسم النداء (Call-By-Beed) ، والتي 1) تجعل إزالة الغابات ممكنة و 2) يحافظ على الدلالات الأصلية للرمز.
الرسوم البيانية لعملية خالية من المصطلحات. في Mazeppa ، لا تحتوي الرسوم البيانية للعمليات على أي إشارات إلى المصطلحات: يمكن أن تعمل الإبقاء بدونها. نتيجة لذلك ، يمكن لمجمع القمامة تخصيص المصطلحات التي تم استخدامها أثناء بناء خريطة فرعية. بالإضافة إلى ذلك ، فإن هذه السياسة لها العديد من المزايا المهمة الأخرى: 1) لا يزال الرسم البياني موجودًا للتفتيش مع --inspect ، 2) عندما يتم رسمها ، فإنها تكشف فقط عن معلومات حول القرارات التي اتخذتها SuperCompiler ، مما يجعل من الأسهل بكثير النظر إليه. يمتنع العديد من المتسابقين السوبر كومبليون عن الرسوم البيانية العملية (على سبيل المثال ، نيل ميتشل سوبرو 17 و 15 أعلاه) ، ولكن نتيجة لذلك ، 1) فهي أقل قدرة على التفتيش من قبل مستخدم ، 2) تصبح الخوارزميات تشوش مع تفاصيل توليد الرمز.
تحليل التكوين ثنائي الأبعاد. عادةً ما يحتفظ SuperCompiler بـ "تاريخ" لمجموعة فرعية من جميع الأجداد أثناء تحويل العقدة ؛ إذا كانت هذه العقدة "قريبة بما يكفي" لأحد أسلافها ، فقد حان الوقت لكسر المصطلح إلى أجزاء أصغر لضمان الإنهاء. في Mazeppa ، نحتفظ بهيكلين منفصلين للبيانات بدلاً من ذلك: المجموعة التي تحتوي على مجموعة فرعية من أسلاف Node والآخر الذي يحتوي على مجموعة فرعية من العقد المحولة بالكامل. يتم استخدام بنية البيانات السابقة لضمان الإنهاء (كالعادة) ، بينما يتم استخدام الأخير لتعزيز مشاركة الوظائف في الكود المتبقي. على وجه التحديد ، إذا كانت العقدة الحالية (من النوع الخاص) هي إعادة تسمية بعض العقدة المحولة مسبقًا ، فنحن نطوي العقدة الحالية في هذه العقدة السابقة. وبهذه الطريقة ، يقوم Mazeppa بإجراء التحليل الرأسي والأفقي للتكوينات ، مما يجعل التعليمات البرمجية المتبقية أكثر إحكاما و SuperCompilation أكثر كفاءة.
تحليل الإنتاجية وظيفة. عندما يطابق نمط استدعاء الوظيفة الداخلية قيمة غير معروفة ، يحدث شيئان محتملان خطيران: 1) يستنسخ SuperCompilation بنية وظيفة مطابقة الأنماط ، 2) SuperCompilation يدفع السياق المحيط بأكمله إلى جميع فروع هذه الوظيفة. بدون مزيد من التحكم ، يمكن أن يؤدي هذا الموقف إلى انفجار كبير في حجم الرمز ، وأحيانًا تسبب في عدم الإنهاء في فترة زمنية معقولة. للتخفيف من ذلك ، تكرر Mazeppa السياق IFF تنتج هذه المكالمة الداخلية قيمة محددة من المستوى الأعلى من نقطة خروج واحدة على الأقل ، لأنه إذا حدث ذلك ، يمكن تفكيك هذه القيمة من خلال مطابقة النمط اللاحقة. خلاف ذلك ، يستخلص Mazeppa المكالمة الداخلية ويحولها بمعزل عن غيرها (تمامًا كما لو كانت مميزة بـ @extract ). علاوة على ذلك ، إذا تم تكرار السياق فعليًا ، تنطبق القاعدة التالية على جميع الفروع: إذا كان الفرع قد أنتج قيمة محددة من المستوى الأعلى من جميع نقاط الخروج ، فسيتم تحويلها في السياق كالمعتاد ؛ خلاف ذلك ، يتم استخراج الفرع من السياق ويتحول في عزلة. في الممارسة العملية ، يمنع هذا التحليل قدرًا هائلاً من التخصصات غير الضرورية ، وبالتالي تكثيف حجم البرنامج المتبقي وجعل SuperCompilation أكثر قابلية للعلاج.
تاريخ ذكي. بدلاً من مقارنة العقدة الحالية بشكل أعمى مع جميع أسلافها ، نستخدم تحكمًا أكثر حبيبية ، أي: 1) تتم مقارنة العقد العالمية (العقد التي تحلل متغيرًا غير معروف) أي شيء آخر. إلى جانب نهج أكثر اقتصادية لفحص الإنهاء ، يتيح هذا المخطط Mazeppa اكتشاف المزيد من فرص التحسين ؛ انظر 18 ، الأقسام 4.6 و 4.7. يتم ضمان إنهاء الانتهاء من SuperCompilation من خلال حقيقة أن التضمين المثلي لا يزال يتم اختباره على جميع الأطراف اللانهائية المحتملة للمصطلحات العالمية والمحلية (لا يمكن أن يوجد تسلسل لا حصر له من المصطلحات التافهة فقط).
توقيعات REDEX. يتم اختبار صافرة فقط بشروط مع توقيعات REDEX متساوية. توقيع Redex هو زوج من 1) رمز الوظيفة و 2) قائمة بفئات قيمة الوسيطة. فئة القيمة هي نوع من المعلومات المتعددة حول الوسيطة ، والتي يمكن أن تكون إما 1) VConst لقيم مثل 42i32 أو "hello world" ، 2) VNeutral لقيم مثل x أو +(x, x) ، أو 3) VCCall(c) لمكالمات المُنشأة مثل Foo(...) . لا يزال يتم اختبار صافرة على جميع تسلسلات المصطلحات غير المحتملة ، لأن أي تسلسل لا حصر له يجب أن يحتوي على بعد لا حصر له على الأقل من المصطلحات مع نفس توقيع Redex. تتيح هذه الاستراتيجية Mazeppa تجنب الإفراط في التقويم في بعض الحالات ، كما يوضح المثالان التاليان:
f(A()) في f(g(B(A()))) ؛ ومع ذلك ، نظرًا لأن مشغلي Redex مختلفون ( f و g ) ، فإن Mazeppa تواصل الحد من النتيجة المثالية.f(A(Good())) مضمّن في f(f(f(B(A(Good()))))) ومشغل REDEX هو f في كلتا الحالتين ، فإن Mazeppa لا يفرط في المعرة لأن هذين المصطلحين لهما فئات قيمة مختلفة في توقيعات Redex الخاصة بهما: في الحالة الأولى ، يتم استدعاء f على A(...) ، في حين أن المصطلح الثاني ، يدعو إلى B(...) . كما هو الحال في المثال السابق ، تصل Mazeppa إلى النتيجة المثالية للتشكيل الفائق فقط عن طريق التخفيض.محسّن التضمين المثلي. على مر العقود ، اكتسب التضمين المثلي سمعة لكونه وسيلة ممتازة للتحقق من الإنهاء عبر الإنترنت 19 . لسوء الحظ ، ويرجع ذلك أساسًا إلى تدفق التحكم غير الخطي (عند تطبيق كل من الغوص والاقتران) ، يمكن أن يكون مكلفًا بشكل لا يغتفر. ما هو أسوأ من ذلك ، يتم إعادة تنفيذه لجميع العقد الوالدين المؤهلين كلما تتم إضافة مصطلح جديد إلى التاريخ ، الذي يبطئ تدريجياً بشكل تدريجي مع نمو التاريخ: الذهاب إلى ما هو تناول معظم وقت SuperCompilation! للتعامل مع ذلك ، نحافظ على ذاكرة التخزين المؤقتة منفصلة:
هاش. تعتمد ذاكرة التخزين المؤقت التضمين المثلية الموصوفة أعلاه على عدد المصطلحات التي يتم مشاركتها . لذلك ، نستخدم إهانة التجزئة أثناء تتكشف أجسام الوظائف: إذا كانت بعض المصطلح الجديد 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. برنامج. 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. الإلكترون. 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. ↩
