mazeppa
v0.4.3
SuperCompilation 1 เป็นเทคนิคการแปลงโปรแกรมที่ประเมินสัญลักษณ์โปรแกรมที่กำหนดด้วยค่ารันไทม์เป็นสิ่งที่ไม่รู้จัก ในการทำเช่นนั้นมันจะค้นพบรูปแบบการดำเนินการของโปรแกรมดั้งเดิมและสังเคราะห์พวกเขาเป็นฟังก์ชั่นแบบสแตนด์อโลน ผลลัพธ์ของการคอมไพล์ซูเปอร์คอมไพล์เป็นโปรแกรมที่เหลืออยู่ที่มีประสิทธิภาพมากขึ้น ในแง่ของพลังการเปลี่ยนแปลงการรวบรวมซูเปอร์คอมไพล์ทั้งการทำลายป่า 2 และการประเมินผลบางส่วน 3 และแม้กระทั่งแสดงความสามารถบางอย่างของทฤษฎีบทที่พิสูจน์ได้
Mazeppa เป็นซูเปอร์คอมไพเลอร์ที่ทันสมัยซึ่งมีจุดประสงค์เพื่อเป็นเป้าหมายการรวบรวมสำหรับภาษาการทำงานแบบโทรโดยค่า มีการเปรียบเทียบและแก้ไข 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 โดยส่วนขยายตัวอย่าง SVG
./scripts/play.sh จะคอมไพล์แหล่งที่มาใน OCAML โดยอัตโนมัติหากมีการเปลี่ยนแปลงอะไร
วิธีที่ดีที่สุดในการทำความเข้าใจว่าการคอมไพล์ซุปเปอร์การทำงานเป็นตัวอย่างอย่างไร พิจารณาฟังก์ชั่นต่อไปนี้ที่ใช้รายการและคำนวณผลรวมขององค์ประกอบกำลังสอง:
[ examples/sum-squares/main.mz ]
main(xs) := sum(mapSq(xs));
sum(xs) := match xs {
Nil() -> 0i32,
Cons(x, xs) -> +(x, sum(xs))
};
mapSq(xs) := match xs {
Nil() -> Nil(),
Cons(x, xs) -> Cons(*(x, x), mapSq(xs))
};
โปรแกรมนี้เขียนขึ้นในรูปแบบการใช้งาน ที่มีการใช้งานจริง ทุกฟังก์ชั่นทำเพียงสิ่งเดียวและทำได้ดี อย่างไรก็ตามมีปัญหาร้ายแรงที่นี่: mapSq สร้างรายการที่จะถูกแยกออกจากกันทันทีโดย sum หมายความว่าเรา 1) เราจำเป็นต้องจัดสรรหน่วยความจำพิเศษสำหรับรายการกลางและ 2) เราต้องการการคำนวณสองครั้งแทนหนึ่ง การแก้ปัญหานี้เรียกว่า การทำลายป่า 2 ซึ่งเป็นกรณีพิเศษของการคอมไพล์ซุปเปอร์
ให้เราดูว่า Mazeppa ทำอะไรกับโปรแกรมนี้:
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
ธง --inspect บอก Mazeppa ให้รายงานโดยละเอียดเกี่ยวกับกระบวนการแปลง sum-squares/target/ Directory จะมีไฟล์ต่อไปนี้:
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dot มี กราฟกระบวนการ ที่สมบูรณ์สำหรับโปรแกรมของเรา คุณสามารถรับรูปภาพของกราฟได้โดยเรียกใช้ dot -Tsvg target/graph.dot > target/graph.svgnodes.json มี เนื้อหา ของโหนดทั้งหมดในกราฟ หากไม่มีไฟล์นี้คุณจะไม่สามารถเข้าใจได้มากนักจากกราฟเพียงอย่างเดียวprogram.json มีโปรแกรมเริ่มต้นใน Mazeppa IR : ซูเปอร์คอมไพเลอร์ของเราทำงานร่วมกับการเป็นตัวแทนนี้โดยเฉพาะแทนที่จะเป็นโปรแกรมดั้งเดิมoutput.mz มีโปรแกรมที่เหลือสุดท้าย output.mz จะมีรหัสต่อไปนี้:
[ examples/sum-squares/target/output.mz ]
main(xs) := f0(xs);
f0(xs) := match xs {
Cons(x, xs') -> +(*(x, x), f0(xs')),
Nil() -> 0i32
};
Supercompiler ได้รวม sum และ mapSq เข้ากับฟังก์ชั่นเดียวได้สำเร็จ f0 ! ซึ่งแตกต่างจากโปรแกรมดั้งเดิม f0 ทำงานในการผ่านครั้งเดียวโดยไม่ต้องจัดสรรหน่วยความจำพิเศษใด ๆ
ซูเปอร์คอมไพเลอร์มาถึงจุดนี้ได้อย่างไร? ให้เราดูกราฟกระบวนการที่สร้างขึ้น:
สำหรับการอ้างอิง nodes.json มีข้อมูลต่อไปนี้ใน JSON:
[
[ " n0 " , " main(xs) " ],
[ " n1 " , " sum(mapSq(xs)) " ],
[ " n2 " , " sum(.g1(xs)) " ],
[ " n3 " , " xs " ],
[ " n4 " , " sum(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n5 " , " .g0(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n6 " , " +(*(.v0, .v0), sum(mapSq(.v1))) " ],
[ " n7 " , " +(*(.v0, .v0), sum(.g1(.v1))) " ],
[ " n8 " , " *(.v0, .v0) " ],
[ " n9 " , " .v0 " ],
[ " n10 " , " .v0 " ],
[ " n11 " , " sum(.g1(.v1)) " ],
[ " n12 " , " .v1 " ],
[ " n13 " , " +(.v3, .v4) " ],
[ " n14 " , " .v3 " ],
[ " n15 " , " .v4 " ],
[ " n16 " , " sum(Nil()) " ],
[ " n17 " , " .g0(Nil()) " ],
[ " n18 " , " 0i32 " ]
] (เราไม่จำเป็นต้องตรวจสอบ program.json สำหรับตัวอย่างเล็ก ๆ นี้ แต่อย่าลังเลที่จะดู: มันไม่ซับซ้อนเกินไป)
Supercompiler เริ่มต้นด้วยโหนด n0 ที่มี main(xs) หลังจากสองขั้นตอนของฟังก์ชั่นที่คลี่ออกเราไปถึงโหนด n2 ที่มี sum(.g1(xs)) โดยที่ .g1 เป็นฟังก์ชัน IR ที่สอดคล้องกับ mapSq ของเรา ณ จุดนี้เราไม่มีทางเลือกอื่นนอกจาก วิเคราะห์ การโทร .g1(xs) โดยการคาดเดาสิ่งที่ค่า xs อาจใช้เวลาทำงาน เนื่องจาก mapSq ของเรายอมรับเฉพาะตัวสร้าง Nil และ Cons จึงเพียงพอที่จะพิจารณากรณี xs=Cons(.v0, .v1) และ xs=Nil() เท่านั้น
Node n4 คือสิ่งที่เกิดขึ้นหลังจากที่เราแทนที่ Cons(.v0, .v1) สำหรับ xs โดยที่ .v0 และ .v1 เป็นตัวแปรสด หลังจากฟังก์ชั่นอีกสามฟังก์ชั่นเรามาถึง n7 นี่เป็นครั้งแรกที่เราต้อง แยก การโทร +(*(.v0, .v0), sum(.g1(.v1))) เป็น .v3=*(.v0, .v0) ( n8 ) และ .v4=sum(.g1(.v1)) +(.v3, .v4) ( n11 n13 เหตุผลในการทำเช่นนั้นคือโหนดก่อนหน้า ( n2 ) ถูกฝังอยู่ในโครงสร้างใน n7 ดังนั้นการรวบรวมซูเปอร์คอมไพล์อาจดำเนินต่อไปตลอดกาล ตอนนี้จะเกิดอะไรขึ้นกับ sum(.g1(.v1)) ( n11 )? เราเคยเห็นมาก่อนหน้านี้! จำได้ว่า n2 มี sum(.g1(xs)) ซึ่งเป็นเพียงการเปลี่ยนชื่อของผล sum(.g1(.v1)) ; ดังนั้นเราจึงตัดสินใจที่จะ พับ n11 ลงใน n2 เพราะมันไม่สมเหตุสมผลเลยที่จะคอมไพล์ในสิ่งเดียวกันสองครั้ง สาขาอื่น ๆ ของ n7 คือ n13 และ n8 ถูก ย่อยสลาย ซึ่งหมายความว่าเราเพียงแค่เปลี่ยนข้อโต้แย้งของพวกเขา
สำหรับสาขาอื่นของ n2 , sum(Nil()) ( n16 ) มันก็เพียงพอที่จะเปิดเผยการโทรนี้ไปที่ 0i32 ( n18 )
หลังจากกราฟกระบวนการเสร็จสมบูรณ์แล้วการตกส่วนที่เหลือจะแปลงเป็นโปรแกรมสุดท้าย ในช่วงนี้รูปแบบการดำเนินการแบบไดนามิกกลายเป็นฟังก์ชั่น - Node n2 ตอนนี้กลายเป็นฟังก์ชัน f0 ซึ่งเป็นโหนดอื่น ๆ ( n11 ) ชี้ไปที่มัน ในโปรแกรมที่เหลือใด ๆ จะมีฟังก์ชั่นมากพอ ๆ กับที่มีโหนดที่มีเส้นประที่เข้ามาพร้อมกับ main
โดยสรุป Supercompilation ประกอบด้วย 1) คำจำกัดความของฟังก์ชั่นการตีแผ่, 2) การวิเคราะห์การโทรที่รูปแบบการจับคู่ตัวแปรที่ไม่รู้จัก, 3) แบ่งการคำนวณลงในชิ้นส่วนที่เล็กกว่า, 4) การคำนวณซ้ำ ๆ และ 5) การสลายการโทรที่ไม่สามารถคลี่ออกได้เช่น +(.v3, .v4) ( n13 ) กระบวนการคอมไพล์ซุปเปอร์ทั้งหมดรับประกันว่าจะสิ้นสุดลงเพราะเมื่อการคำนวณบางอย่างมีขนาดใหญ่ขึ้นและใหญ่ขึ้นเราจึงแบ่งมันออกเป็นปัญหาย่อยและแก้ปัญหาได้
มีตัวอย่างที่น่าสนใจอื่น ๆ อีกมากมายของการตัดไม้ทำลายป่าใน examples/ โฟลเดอร์รวมถึงโครงสร้างข้อมูลเหมือนต้นไม้ ในความเป็นจริงเราได้นำเสนอตัวอย่างทั้งหมดจากงานก่อนหน้านี้ในการรวบรวมค่าใช้จ่ายในการโทรตามค่าที่สูงขึ้นโดย Peter A. Jonsson และ Johan Nordlander 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 ซ้ำซ้ำ ๆ แม้ว่าจะเป็นที่รู้จักอย่างสมบูรณ์แบบในเวลาคอมไพล์ Running Mazeppa บน main(a) จะให้โปรแกรมที่เหลือต่อไปนี้:
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
ฟังก์ชั่น powerSq ทั้งหมดถูกกำจัดออกไปดังนั้นจึงบรรลุผลของการประเมินบางส่วน (ถ้าเราพิจารณาว่า powerSq เป็นล่ามสำหรับโปรแกรม x และข้อมูลอินพุต a นั่นคือการฉาย Futamura ครั้งแรก: เชี่ยวชาญด้านล่ามเพื่อรับโปรแกรมเป้าหมายที่มีประสิทธิภาพ) นอกจากนี้สังเกตว่าซูเปอร์คอมไพเลอร์ได้ แบ่งปัน การโต้แย้ง *(a, *(a, a)) สองครั้ง โปรแกรมที่เหลือสะท้อนให้เห็นถึงการชดเชยโดยการยกกำลัง
ให้เราไปไกลกว่าการทำลายป่าและการประเมินบางส่วน พิจารณาฟังก์ชั่น matches(p, s) ของสองสตริงซึ่งส่งคืน T() ถ้า s มี p และ F() มิฉะนั้น การใช้งานที่ไร้เดียงสาใน Mazeppa จะเป็นสิ่งต่อไปนี้โดยที่ p มีความเชี่ยวชาญใน "aab" :
[ examples/kmp-test/main.mz ]
main(s) := matches(Cons('a', Cons('a', Cons('b', Nil()))), s);
matches(p, s) := go(p, s, p, s);
go(pp, ss, op, os) := match pp {
Nil() -> T(),
Cons(p, pp) -> goFirst(p, pp, ss, op, os)
};
goFirst(p, pp, ss, op, os) := match ss {
Nil() -> F(),
Cons(s, ss) -> match =(p, s) {
T() -> go(pp, ss, op, os),
F() -> failover(op, os)
}
};
failover(op, os) := match os {
Nil() -> F(),
Cons(_s, ss) -> matches(op, ss)
};
(ที่นี่เราเป็นตัวแทนของสตริงเป็นรายการของตัวละครเพื่อความเรียบง่าย แต่ไม่ต้องกังวล Mazeppa ให้สายในตัวเช่นกัน)
อัลกอริทึมถูกต้อง แต่ไม่มีประสิทธิภาพ พิจารณาว่าจะเกิดอะไรขึ้นเมื่อ "aa" เข้ากันได้สำเร็จ แต่ 'b' ไม่ได้ อัลกอริทึมจะเริ่มจับคู่ "aab" อีกครั้งจากตัวละครที่สองของ s แม้ว่ามันจะสามารถพูดได้แล้วว่าตัวละครตัวที่สองของ s คือ 'a' Automaton จำกัด ที่กำหนดขึ้นโดย 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 ' ซึ่งมีระบบประเภท S เป็นระบบย่อยและรวมถึงกลไกเพิ่มเติมที่ควบคุมพฤติกรรมและการผลิตของระบบ S -Subsystems จากนั้นเราเรียก s ' metasystem ด้วยความเคารพต่อ s และการสร้าง S' การเปลี่ยนแปลงระบบ metasystem อันเป็นผลมาจากการเปลี่ยนระบบ 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 เพื่อหลีกเลี่ยงการรบกวนด้วยการสร้างชื่อใหม่เราได้ใส่ ดัชนี เดอ Bruijn ในตัวสร้าง Var และ ระดับ de Bruijn ใน NVar ; หลังถูกแปลงเป็นอดีตใน quoteNeutral
ตอนนี้ให้เราคำนวณบางอย่างด้วยเครื่องนี้:
main() := normalize(0u64, Nil(), example());
example() := Appl(Appl(mul(), two()), three());
two() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))));
three() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64),
Var(0u64))))));
mul() := Lam(Lam(Lam(Lam(Appl(
Appl(Var(3u64), Appl(Var(2u64), Var(1u64))),
Var(0u64))))));
ร่างกายของ main คำนวณรูปแบบปกติของ example() ที่ทวีคูณตัวเลขคริสตจักร two() และ three()
โดย Supercompiling main() เราได้รับตัวเลขโบสถ์ 6:
[ examples/lambda-calculus/target/output.mz ]
main() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64)
, Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))))))));
ล่ามแลมบ์ดาแคลคูลัสได้รับการทำลายล้างอย่างสมบูรณ์!
ในตัวอย่างนี้เราเพิ่งเห็น บันได metasystem สองระดับ (ในคำศัพท์ของ Turchin 14 ): ในระดับ 0 เรามี Mazeppa Supercompiler ที่เปลี่ยนโปรแกรมวัตถุในขณะที่ระดับ 1 เรามีโปรแกรมวัตถุปกติ อาจมีจำนวนการตีความตามอำเภอใจและสามารถใช้ mazeppa เพื่อยุบพวกเขาทั้งหมด พฤติกรรมทั่วไปของการคอมไพล์ซุปเปอร์การคอมไพล์นี้ถูกสำรวจโดย Turchin ใน 1 (ส่วนที่ 7) ซึ่งเขาสามารถคอมไพล์สองโปรแกรมที่ตีความได้หนึ่งโปรแกรมหนึ่งตัวที่มีลักษณะคล้าย Fortran และหนึ่งใน Lisp เพื่อให้ได้ปัจจัยการเร่งความเร็ว 40 ในทั้งสองกรณี
Lambda Normalizer ยังแสดงให้เราเห็นถึงวิธีการจุติฟังก์ชั่นการสั่งซื้อที่สูงขึ้นเป็นภาษาลำดับที่หนึ่ง ใน Mazeppa เราไม่สามารถปฏิบัติต่อฟังก์ชั่นเป็นค่าได้ แต่ไม่ได้หมายความว่าเราไม่สามารถจำลองได้! ด้วยการดำเนินการเปลี่ยนระบบ metasystem เราสามารถใช้ฟังก์ชั่นลำดับที่สูงขึ้นได้อย่างมีประสิทธิภาพในภาษาลำดับที่หนึ่ง นอกเหนือจากการ defunctionalization และการแปลงปิดแล้วเทคนิคนี้สามารถใช้สำหรับการรวบรวมภาษาลำดับที่สูงขึ้นเป็นรหัสลำดับแรกที่มีประสิทธิภาพ
ตัวอย่างที่เกี่ยวข้อง: เครื่องเสมือนที่จำเป็น, ตัวขับเคลื่อนด้วยตนเอง
เมื่อมองย้อนกลับไปปัญหาสำคัญที่ป้องกันการยอมรับอย่างกว้างขวางของการคอมไพล์ซุปเปอร์คือการคาดเดาไม่ได้ - ด้านมืดของพลัง เพื่อให้เข้าใจถึงความหมายของมันให้พิจารณาว่าเราจะแก้ปัญหา SAT ได้อย่างไร "ทันที"::
[ examples/sat-solver/main.mz ]
main(a, b, c, d, e, f, g) := solve(formula(a, b, c, d, e, f, g));
formula(a, b, c, d, e, f, g) :=
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Var(e), or(Not(g), F()))),
and(or(Var(e), or(Not(g), or(Var(f), F()))),
and(or(Not(g), or(Var(c), or(Var(d), F()))),
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Not(e), or(Var(g), F()))),
and(or(Var(a), or(Var(a), or(Var(c), F()))),
and(or(Not(g), or(Not(d), or(Not(b), F()))),
T()))))))));
or(x, rest) := match x {
Var(x) -> If(x, T(), rest),
Not(x) -> If(x, rest, T())
};
and(clause, rest) := match clause {
If(x, m, n) -> If(x, and(m, rest), and(n, rest)),
T() -> rest,
F() -> F()
};
solve(formula) := match formula {
If(x, m, n) -> analyze(x, m, n),
T() -> T(),
F() -> F()
};
analyze(x, m, n) := match x {
T() -> solve(m),
F() -> solve(n)
};
มีสองสิ่งผิดปกติกับรหัสที่ถูกต้องอย่างสมบูรณ์แบบนี้: 1) ซูเปอร์คอมไพเลอร์จะขยายสูตรในพื้นที่เอ็กซ์โปเนนเชียลและ 2) ซุปเปอร์คอมไพเลอร์จะพยายามแก้สูตรที่ขยายตัวในเวลาเอ็กซ์โปเนนเชียล บางครั้งเราก็ไม่ต้องการประเมินทุกอย่างในเวลาคอมไพล์
อย่างไรก็ตามไม่สิ้นหวัง: เราให้วิธีแก้ปัญหานี้ ก่อนอื่นให้เราพิจารณาวิธีเลื่อนการแก้สูตรจนกว่าจะถึงเวลาทำงาน ปรากฎว่าสิ่งเดียวที่เราต้องทำคือการใส่คำอธิบาย formula ฟังก์ชันด้วย @extract ดังนี้:
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
เมื่อ Mazeppa เห็น solve(formula(a, b, c, d, e, f, g)) มันจะสกัดการโทรไปยัง formula เป็นตัวแปรสด .v0 และดำเนินการ supercompiling การโทรที่สกัดและ solve(.v0) ในการแยก การโทรหลังจะทำซ้ำ Sat Solver ดั้งเดิม
แต่การคอมไพล์การโทรไปยัง formula จะยังคงส่งผลให้เกิดการระเบิดแบบทวีคูณ ให้เราตรวจสอบว่าทำไมสิ่งนี้จึงเกิดขึ้น สูตรดั้งเดิมของเราประกอบด้วยการโทร or และ and ; ในขณะที่ or ไม่เป็นอันตรายอย่างเห็นได้ชัด and เผยแพร่พารามิเตอร์ rest ให้กับ ทั้งสอง สาขาของ If (กรณี match แรก) - นี่คือสถานที่ที่แน่นอนที่เกิดการระเบิด ดังนั้นให้เราทำเครื่องหมาย and @extract ด้วย:
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
นั่นคืออะไร! เมื่อใด and จะถูกเปลี่ยนมา Mazeppa จะแยกการโทรออกจากบริบทโดยรอบและซุปเปอร์คอมไพล์มันแยก ด้วยการเพิ่มคำอธิบายประกอบสองรายการในสถานที่ที่เหมาะสมเราได้แก้ไขปัญหาการระเบิดของรหัสและเวลาทำงานแบบเอ็กซ์โปเนนเชียลของซูเปอร์คอมไพล์ โดยทั่วไปเมื่อใดก็ตามที่ Mazeppa เห็น ctx[f(t1, ..., tN)] โดยที่ f ถูกทำเครื่องหมาย @extract และ ctx[.] เป็นบริบทโดยรอบที่ไม่ว่างเปล่า . ใน ตำแหน่ง redex มันจะเสียบตัวแปรสด v เข้ากับ ctx และดำเนินการเปลี่ยนโหนดต่อไปนี้แยกกัน: f(t1, ..., tN) และ ctx[v]
ในที่สุดโปรดทราบว่า @extract เป็นเพียงกลไกระดับต่ำ ส่วนหน้าคอมไพเลอร์จะต้องดำเนินการเครื่องจักรเพิ่มเติมเพื่อบอก Mazeppa ว่าทำหน้าที่แยก สามารถทำได้สองวิธี:
formula และ and สกัดได้ทำให้ฟังก์ชั่นอื่น ๆ ทั้งหมดไม่มีการแตะต้องทั้งสองวิธีสามารถรวมกันเพื่อให้ได้เอฟเฟกต์ที่ต้องการ
Mazeppa มีตัวเลือกการออกแบบที่น่าสนใจเพื่อให้มีฟังก์ชั่นกระตือรือร้นและตัวสร้างขี้เกียจ ตัวอย่างต่อไปนี้โดยที่ magic(1u32, 1u32) สร้างหมายเลข Fibonacci ถูกนำมาใช้จาก Haskell:
[ examples/lazy-fibonacci/main.mz ]
main() := getIt(magic(1u32, 1u32), 3u64);
magic(m, n) := match =(m, 0u32) {
T() -> Nil(),
F() -> Cons(m, magic(n, +(m, n)))
};
getIt(xs, n) := match xs {
Nil() -> Panic("undefined"),
Cons(x, xs) -> match =(n, 1u64) {
T() -> x,
F() -> getIt(xs, -(n, 1u64))
}
};
หากผู้สร้างมีความกระตือรือร้น magic(1u32, 1u32) จะไม่สิ้นสุด อย่างไรก็ตาม Cons ไม่ได้ประเมินข้อโต้แย้ง! เนื่องจาก getIt ใช้เฉพาะส่วนที่ จำกัด ของรายการที่ไม่มีที่สิ้นสุดโปรแกรมจะสิ้นสุดและพิมพ์ 2u32 :
$ mazeppa eval
2u32
ตัวสร้างขี้เกียจเปิดใช้งานการทำลายป่าอย่างง่ายดายตามที่กล่าวไว้ด้านล่าง
หลังจากติดตั้ง mazeppa ผ่าน opam หรือ ./scripts/install.sh แล้วจะมีให้เป็นไลบรารี OCAML!
ตั้งค่าโครงการ Dune ใหม่ดังนี้:
$ dune init project my_compiler
เพิ่ม mazeppa เป็นห้องสมุดบุคคลที่สามลงใน bin/dune ของคุณ:
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
วางรหัสต่อไปนี้ลงใน bin/main.ml (นี่คือ examples/sum-squares/main.mz ที่เข้ารหัสใน OCAML):
open Mazeppa
let input : Raw_program.t =
let sym = Symbol. of_string in
let open Raw_term in
let open Checked_oint in
[ [], sym " main " , [ sym " xs " ], call ( " sum " , [ call ( " mapSq " , [ var " xs " ]) ])
; ( []
, sym " sum "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), int ( I32 ( I32. of_int_exn 0 ))
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call ( " + " , [ var " x " ; call ( " sum " , [ var " xs " ]) ]) )
] ) )
; ( []
, sym " mapSq "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), call ( " Nil " , [] )
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call
( " Cons "
, [ call ( " * " , [ var " x " ; var " x " ]); call ( " mapSq " , [ var " xs " ]) ] ) )
] ) )
]
;;
let () =
try
let output = Mazeppa. supercompile input in
Printf. printf " %s n " ( Raw_program. show output)
with
| Mazeppa. Panic msg ->
Printf. eprintf " Something went wrong: %s n " msg;
exit 1
;; เรียกใช้ dune exec my_compiler เพื่อดูโปรแกรมที่เหลือที่ต้องการ:
[([], "main", ["xs"], (Raw_term.Call ("f0", [(Raw_term.Var "xs")])));
([], "f0", ["xs"],
(Raw_term.Match ((Raw_term.Var "xs"),
[(("Cons", ["x"; "xs'"]),
(Raw_term.Call ("+",
[(Raw_term.Call ("*", [(Raw_term.Var "x"); (Raw_term.Var "x")]));
(Raw_term.Call ("f0", [(Raw_term.Var "xs'")]))]
)));
(("Nil", []), (Raw_term.Const (Const.Int (Checked_oint.I32 0))))]
)))
]
คุณสามารถโทรหา Mazeppa ได้หลายครั้งเท่าที่คุณต้องการรวมถึงในแบบคู่ขนาน โปรดทราบว่าเราเปิดเผยอินเทอร์เฟซที่ จำกัด ให้กับซูเปอร์คอมไพเลอร์ โดยเฉพาะอย่างยิ่งไม่มีทางที่จะตรวจสอบสิ่งที่มันทำในกระบวนการ (เช่น --inspect )
นอกจากการรวบรวมซูเปอร์แล้วเรายังมีผู้ประเมินในตัว:
val eval : Raw_program .t -> Raw_term .t สามารถเรียกใช้ในโปรแกรมที่มีฟังก์ชั่น main ไม่ยอมรับพารามิเตอร์ ซึ่งแตกต่างจาก supercompile มันสร้างเงื่อนไขที่ประเมินของ Type Raw_term.t และอาจแตกต่างกันไป
ดูฟังก์ชั่น API อื่น ๆ และเอกสารประกอบใน lib/mazeppa.mli
สมมติว่า main.mz มีตัวอย่าง Lazy 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 Writes เนื้อหาของ 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 Integer ( MZ_INT ) และพิมพ์ผลลัพธ์ คุณสามารถใช้ฟังก์ชั่นใด ๆ จาก mazeppa.h หากไม่ได้นำหน้าด้วย mz_priv_ หรือ MZ_PRIV_
เพื่อรวบรวมทุกชิ้นเข้าด้วยกัน:
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out พิมพ์ fib(10) = 55 และออกตามที่คาดไว้
--inspect ในสภาพแวดล้อมจริง: ใช้เพื่อการดีบักเท่านั้น@extract (ดังที่แสดงด้านบน) เพื่อควบคุมว่าจะดำเนินการต่อการรวบรวมซุปเปอร์หรือสกัด REDEX"otus" มีขนาดเล็กกว่า "octopus" แต่ "octopusx" ไม่ใช่ Mazeppa มีตัวเลือกการออกแบบที่น่าสนใจหลายประการ (จัดอันดับตามความสำคัญ):
รหัสสั่งซื้อครั้งแรก Max Bolingbroke และ Simon Peyton Jones 15 รายงานว่าสำหรับตัวอย่างหนึ่งโดยเฉพาะซูเปอร์คอมไพเลอร์ที่มีลำดับสูงกว่าสำหรับชุดย่อยของ Haskell ใช้เวลา 42% ของเวลาดำเนินการในการจัดการชื่อและการเปลี่ยนชื่อ ในขณะที่มันเป็นความจริงที่โมเดลการประเมินแบบง่าย ๆ เช่นการทำให้เป็นมาตรฐานของเงื่อนไขแลมบ์ดาอนุญาตให้เราหลีกเลี่ยงค่าใช้จ่ายที่สำคัญของการหลีกเลี่ยงการจับภาพการรวบรวมซุปเปอร์คอมไพล์มีความซับซ้อนมากขึ้น ตัวอย่างเช่นนอกเหนือจากการคำนวณเชิงสัญลักษณ์แล้ว Supercompilation จำเป็นต้องวิเคราะห์ผลลัพธ์ที่คำนวณไว้ก่อนหน้านี้เพื่อทำการตัดสินใจเกี่ยวกับการเปลี่ยนแปลงเพิ่มเติม: พิจารณาการทดสอบอินสแตนซ์คำว่าการทดสอบการฝัง homeomorphic, การสรุปทั่วไปที่เฉพาะเจาะจงมากที่สุด ฯลฯ ใน Mazeppa เรายึดติดกับปรัชญาของการปรับปรุงอย่างค่อยเป็นค่อยไป: แทนที่จะพยายามจัดการกับคุณสมบัติแฟนซีมากมายในเวลาเดียวกันเรา 1) แก้ไขภาษา หลัก เพื่อการจัดการที่สะดวกโดยเครื่อง 2) ทำการเปลี่ยนระบบ metasystem มากเท่าที่จำเป็นเพื่อให้ภาษาหลักดีขึ้นสำหรับมนุษย์
ตัวสร้างขี้เกียจ มันเป็นข้อสังเกตที่รู้จักกันดีว่าภาษาโทรโดยค่าเป็นเรื่องยากสำหรับการตัดไม้ทำลายป่าที่เหมาะสม มันยังคงเป็นไปได้ที่จะตัดไม้ทำลายพวกเขา แต่ไม่ได้ไม่มีการวิเคราะห์เพิ่มเติม 4 5 อย่างไรก็ตามหากผู้สร้างขี้เกียจ (เช่นพวกเขาไม่ได้ประเมินข้อโต้แย้งของพวกเขา) การตัดไม้ทำลายป่า ก็ใช้ได้ Turchin ทำให้มันทำงานได้โดยการแปลงลำดับปกติของภาษาโทรตามค่า แต่ผลลัพธ์ก็คือรหัสที่เหลืออาจยุติบ่อยขึ้น ใน Mazeppa เรามีฟังก์ชั่นการโทรแบบโทรและค่าโทรโดยผู้สร้าง (โทรตามต้องการ) ซึ่ง 1) ทำให้การตัดไม้ทำลายป่าเป็นไปได้และ 2) รักษาความหมายดั้งเดิมของรหัส
กราฟกระบวนการปลอดคำศัพท์ ใน Mazeppa กราฟกระบวนการไม่มีการอ้างอิงใด ๆ กับข้อกำหนด: การตกส่วนที่เหลือสามารถทำงานได้หากไม่มีพวกเขา เป็นผลให้นักสะสมขยะสามารถจัดการเงื่อนไขที่ใช้ในระหว่างการก่อสร้างกราฟย่อย นอกจากนี้ว่านโยบายนี้มีข้อได้เปรียบที่สำคัญอื่น ๆ อีกมากมาย: 1) กราฟยังคงมีอยู่สำหรับการตรวจสอบด้วย --inspect 2) เมื่อมีการวาดมันจะเปิดเผยข้อมูลเกี่ยวกับ การตัดสินใจ ที่ซูเปอร์คอมไพเลอร์ใช้ซึ่งทำให้ดูง่ายขึ้นมาก ซุปเปอร์คอมไพเลอร์ที่มีอยู่หลายแห่งละเว้นจากกราฟกระบวนการที่เหมาะสม (เช่น Supero 17 ของ Neil Mitchell และ 15 ดังกล่าวข้างต้น) แต่ด้วยเหตุนี้ 1) พวกเขามีความสามารถในการตรวจสอบน้อยกว่าโดยผู้ใช้ 2) อัลกอริทึมที่เต็มไปด้วยรายละเอียดการสร้างรหัส
การวิเคราะห์การกำหนดค่าสองมิติ โดยปกติแล้วซูเปอร์คอมไพเลอร์จะรักษา "ประวัติ" ของชุดย่อยของบรรพบุรุษทั้งหมดในขณะที่เปลี่ยนโหนด; หากโหนดนี้ "ใกล้พอ" กับหนึ่งในบรรพบุรุษของมันก็ถึงเวลาที่จะแบ่งคำออกเป็นส่วนเล็ก ๆ เพื่อรับประกันการเลิกจ้าง ใน Mazeppa เราเก็บโครงสร้างข้อมูลสองแบบแยกกันแทน: อันที่มีชุดย่อยของบรรพบุรุษของโหนดและอันที่มีชุดย่อยของโหนดที่ถูกแปลงอย่างสมบูรณ์ โครงสร้างข้อมูลเดิมใช้เพื่อรับประกันการเลิกจ้าง (ตามปกติ) ในขณะที่หลังถูกใช้เพื่อปรับปรุง การแบ่งปันฟังก์ชั่น ในรหัสที่เหลือ โดยเฉพาะหากโหนดปัจจุบัน (ชนิดพิเศษ) เป็นการเปลี่ยนชื่อของโหนดที่ถูกแปลงก่อนหน้านี้เราจะพับโหนดปัจจุบันลงในโหนดก่อนหน้านี้ ด้วยวิธีนี้ Mazeppa ดำเนินการวิเคราะห์ทั้ง แนวตั้ง และ แนวนอน ของการกำหนดค่าซึ่งทำให้รหัสที่เหลือมีขนาดกะทัดรัดมากขึ้นและมีประสิทธิภาพมากขึ้น
การวิเคราะห์ฟังก์ชั่นการผลิต เมื่อรูปแบบการเรียกใช้ฟังก์ชันภายในจับคู่ค่าที่ไม่รู้จักสิ่งที่อาจเป็นอันตรายได้สองสิ่งที่อาจเกิดขึ้น: 1) การรวบรวมซูเปอร์การรวบรวมซ้ำโครงสร้างของฟังก์ชั่นการจับคู่รูปแบบ 2) supercompilation จะผลักบริบทโดยรอบทั้งหมดไปยังสาขาทั้งหมดของฟังก์ชั่นนี้ หากไม่มีการควบคุมเพิ่มเติมสถานการณ์นี้อาจนำไปสู่การระเบิดอย่างมีนัยสำคัญในขนาดโค้ดบางครั้งก็ทำให้ซูเปอร์คอมไพเลอร์ไม่สิ้นสุดในระยะเวลาที่เหมาะสม เพื่อปรับปรุง Mazeppa ทำซ้ำบริบท IFF การโทรภายในนี้จะสร้าง ค่าระดับสูงสุดที่แน่นอน จากจุดออก อย่างน้อยหนึ่ง จุดเพราะถ้าเป็นโอกาสที่ดีที่ค่านี้สามารถ deconstructed โดยการจับคู่รูปแบบที่ตามมา มิฉะนั้น Mazeppa จะสกัดการโทรภายในและแปลงมันแยกกัน (ราวกับว่ามันถูกทำเครื่องหมายด้วย @extract ) นอกจากนี้หากบริบทมีการทำซ้ำจริงกฎต่อไปนี้จะใช้กับสาขาทั้งหมด: หากสาขาสร้างค่าระดับสูงสุดที่แน่นอนจากจุดออก ทั้งหมด มันจะถูกแปลงในบริบทตามปกติ มิฉะนั้นสาขาจะถูกสกัดจากบริบทและเปลี่ยนไปแยก ในทางปฏิบัติการวิเคราะห์นี้จะช่วยป้องกันความเชี่ยวชาญที่ไม่จำเป็นจำนวนมากซึ่งจะทำให้ขนาดโปรแกรมที่เหลืออยู่ระหว่างกัน
ประวัติศาสตร์อัจฉริยะ แทนที่จะเปรียบเทียบโหนดปัจจุบันกับบรรพบุรุษทั้งหมดเราใช้การควบคุมที่ละเอียดยิ่งขึ้นนั่นคือ: 1) โหนดทั่วโลก (โหนดที่วิเคราะห์ตัวแปรที่ไม่รู้จัก) เปรียบเทียบกับโหนดทั่วโลกเท่านั้น 2) โหนดท้องถิ่น สิ่งอื่นใด นอกเหนือจากแนวทางทางเศรษฐกิจที่มากขึ้นในการตรวจสอบการเลิกจ้างแล้วโครงการนี้ยังช่วยให้ Mazeppa ค้นพบโอกาสในการเพิ่มประสิทธิภาพมากขึ้น ดู 18 ส่วน 4.6 และ 4.7 การยกเลิกการรวบรวม supercompilation ได้รับการรับประกันโดยข้อเท็จจริงที่ว่าการฝัง homeomorphic ยังคงถูกทดสอบในการเรียงลำดับที่ไม่มีที่สิ้นสุดทั้งหมดของข้อกำหนดทั่วโลกและท้องถิ่น (ไม่มีลำดับที่ไม่มีที่สิ้นสุดของคำศัพท์เล็กน้อยเท่านั้น)
ลายเซ็น redex นกหวีดถูกทดสอบในคำศัพท์ที่มี ลายเซ็น redex เท่ากัน ลายเซ็น Redex เป็นคู่ของ 1) สัญลักษณ์ของฟังก์ชั่นและ 2) รายการ หมวดหมู่ค่า อาร์กิวเมนต์ หมวดหมู่ค่าคือการเรียงลำดับของ metainformation เกี่ยวกับอาร์กิวเมนต์ซึ่งสามารถเป็น 1) VConst สำหรับค่าเช่น 42i32 หรือ "hello world" , 2) VNeutral สำหรับค่าเช่น x หรือ +(x, x) หรือ 3) VCCall(c) สำหรับ constructor เช่น Foo(...) นกหวีดยังคงทดสอบในลำดับที่ไม่มีที่สิ้นสุดทั้งหมดของคำศัพท์เนื่องจากลำดับที่ไม่มีที่สิ้นสุดใด ๆ จะต้องมีอย่างน้อยหนึ่งลำดับที่ไม่สิ้นสุดของคำที่มีลายเซ็น redex เดียวกัน กลยุทธ์นี้ช่วยให้ Mazeppa หลีกเลี่ยงการขยายใหญ่เกินไปในบางกรณีดังกล่าวสองตัวอย่างต่อไปนี้แสดงให้เห็นว่า:
f(A()) จะถูกฝังอยู่ใน homeomorphically เป็น f(g(B(A()))) ; อย่างไรก็ตามเนื่องจากผู้ให้บริการ REDEX นั้นแตกต่างกัน ( f และ g ) Mazeppa ยังคงลดลงและไปถึงผลลัพธ์ในอุดมคติf(A(Good())) จะถูกฝังลงใน f(f(f(B(A(Good()))))) B(...) A(...) ดำเนินการ redex เป็น f ในทั้งสอง f mazeppa ไม่ได้ขยายใหญ่เกินไปเพราะคำศัพท์สองข้อนี้มีค่าที่แตกต่างกัน เช่นเดียวกับในตัวอย่างก่อนหน้า Mazeppa มาถึงผลลัพธ์ในอุดมคติของการคอมไพล์ซุปเปอร์การลดลงเพียงอย่างเดียวโดยการลดการฝัง homeomorphic ที่ดีที่สุด ในช่วงหลายทศวรรษที่ผ่านมาการฝัง homeomorphic ได้รับชื่อเสียงในการเป็นวิธีที่ยอดเยี่ยมสำหรับการตรวจสอบการเลิกจ้างออนไลน์ 19 น่าเสียดายที่ส่วนใหญ่เกิดจากการไหลของการควบคุมที่ไม่ใช่เชิงเส้น (เมื่อใช้ทั้งการดำน้ำและการมีเพศสัมพันธ์) อาจมีราคาแพงในการคำนวณ สิ่งที่เลวร้ายยิ่งกว่านั้นจะถูกนำไปใช้ใหม่สำหรับโหนดหลักที่มีคุณสมบัติทั้งหมดเมื่อใดก็ตามที่มีการเพิ่มคำศัพท์ใหม่ในประวัติศาสตร์ซึ่งจะทำให้ซุปเปอร์คอมไพล์ลดลงอย่างต่อเนื่องเมื่อประวัติศาสตร์เติบโตขึ้น เพื่อรับมือกับสิ่งนั้นเรารักษาแคชสองตัวแยกกัน:
แฮช consing แคชฝัง homeomorphic ที่อธิบายไว้ข้างต้นขึ้นอยู่กับจำนวนคำที่ ใช้ร่วมกัน ดังนั้นเราจึงใช้แฮชการยืนยันในขณะที่การตีพิมพ์ฟังก์ชั่น: หากคำศัพท์ใหม่ t ใหม่มีโครงสร้างเท่ากับ คำ ที่มีอยู่บางคำที่มีอยู่หลังจะถูกนำกลับมาใช้ใหม่ เพื่อหลีกเลี่ยงการรั่วไหลของหน่วยความจำเราใช้อีเฟมเมอรอนทั่วโลกที่ถือพอยน์เตอร์ที่อ่อนแอ นอกเหนือจากเวลาที่ได้รับการปรับปรุงให้ดีขึ้น (เนื่องจากการบันทึกความทรงจำ) แฮช consing ยังช่วยลดการใช้หน่วยความจำ - ดู #4 (ความคิดเห็น)
การทำให้เป็นมาตรฐานในระหว่างการตีแผ่ เมื่อการเรียกใช้ฟังก์ชั่นคลี่ออกเราจะแทนที่พารามิเตอร์และทำให้ร่างกายเป็นปกติให้มากที่สุด (เช่นโดยไม่ต้องเปิดเผยเพิ่มเติมเพื่อรับประกันการเลิกจ้าง) เพื่อดูว่าทำไมให้พิจารณาฟังก์ชั่นแฟคทอเรียล f(n) ; ด้วยการตีแผ่อย่างง่ายเราจะดักจับในสถานการณ์ที่ไม่พึงประสงค์โดยที่ f(1u32) ถูกฝังลงใน *(1u32, f(-(1u32, 1u32))) ทำให้เกิด การขยายใหญ่เกินไป ในความเป็นจริง Mazeppa จะเปิด f(1u32) ถึง *(1u32, f(0u32)) ทำให้ผู้สมัครเป็นผู้สมัครสำหรับการตีแผ่ต่อไป วิธีการนี้ได้รับการแนะนำใน 20 มาตรา 4.5 ข้อดีอื่น ๆ ของมันคือ: 1) ทำงานน้อยลงสำหรับขั้นตอนการขับขี่ในอนาคต 2) การคำนวณ "ซ้ำ ๆ " น้อยลงในกราฟกระบวนการ 3) ลดจำนวนการทดสอบการฝัง homeomorphic ที่มีราคาแพง
*(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 ).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 | ความหมาย |
|---|---|
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 | Notes |
|---|---|---|
// ... rest | rest | rest is in <program> or <term> |
let p := t; u | match t { p -> u } | p is in <pattern> |
c | ASCII(c) | c is in <CHAR> |
where ASCII(c) is an appropriate u8 integer constant, according to the ASCII table; for example, ASCII( 'a' ) is 97u8 .
Suppose that t is a well-formed term closed under environment env (defined below) and program is a well-formed program. Then the evaluation of t is governed by the following big-step environment machine:
eval(env, x) = eval({ }, env(x))eval(env, const) = const , where const is in <const> .eval(env, f(t1, ..., tN)) =t1Val ^= eval(env, t1)tNVal ^= eval(env, tN)eval({ x1 -> t1Val, ..., xN -> tNVal }, body) , where f(x1, ..., xN) := body; is in program .eval(env, C(t1, ..., tN)) = C(t1[env], ..., tN[env]) , where C starts with an uppercase letter.eval(env, op(t)) =tVal ^= eval(env, t)evalOp1(op, tVal) , where op is in <op1> .eval(env, op(t1, t2)) =t1Val ^= eval(env, t1)t2Val ^= eval(env, t2)evalOp2(t1Val, op, t2Val) , where op is in <op2> .eval(env, match t { p1 -> t1, ..., pN -> tN }) =Ci(s1, ..., sN) ^= eval(env, t)eval(env', tI) , whereCi(x1, ..., xN) -> tI is among the rules in match t { ... } , andenv' is env[x1 -> s1, ..., xN -> sN] .eval(env, let x := t; u) =tVal ^= eval(env, t)eval(env[x -> tVal], u)Notation:
env is a total environment over t , whose general form is { x1 -> t1, ..., xN -> tN } . Each tI term must be closed and well-formed; this property is preserved by eval .env(x) is tI , where x -> tI is in env .env[x1 -> t1, ..., xN -> tN] is the environment env extended with new bindings x1 -> t1 , ... , xN -> tN . If some xI is already bound in env , it is rebound.t[env] denotes a simultaneous substitution of all free variables in t by their bound values in env .tVal ^= eval(env, t) evaluates t under env ; แล้ว:Panic(t') , the result of the whole evaluation rule is Panic(t') .tVal is available for the next clauses. (Note that eval is a partial function, so evaluation of t can "get stuck" without a superimposed type system.)
In what follows, 1) signed integers are represented in two's complement notation, 2) panic denotes Panic(s) , where s is some (possibly varying) implementation-defined string constant.
evalOp1 takes care of the unary operators for primitive types ( x is in <INT> , s is in <STRING> ):
evalOp1(~, x) is the bitwise negation of x of the same type.evalOp1(string, x) is the string representation of x (in decimal).evalOp1(ty, x) , where ty is in <INT-TY> , is x converted to an integer of type ty .x is not in the range of ty , the result is panic .evalOp1(#, x) , where x is a u8 integer, is a string containing only the ASCII character of x .x is not printable, the result takes the form "xhh" .evalOp1(length, s) is a u64 integer denoting the length of s .evalOp1(string, s) is s . Likewise, evalOp2 takes care of the binary operators for primitive types:
evalOp2(x, op, y) , where x and y have the same integer type and op is in <arith-op2> , performs a corresponding arithmetic operation on x and y , yielding a value of the same type as that of x and y .evalOp2(x, op, y) , where x and y have the same integer type and op is in <cmp-op2> , performs a corresponding comparison operation on x and y , yielding either T() or F() .evalOp2(s1, op, s2) , where s1 and s2 are strings and op is in <cmp-op2> , performs a corresponding lexicographical comparison on s1 and s2 , yielding either T() or F() .evalOp2(s1, ++, s2) is the concatenation of s1 and s2 .evalOp2(s, get, idx) , where idx is a u64 integer, is the idx -th character (of type u8 ) of s .idx is out of bounds, the result is panic . The definition of eval is now complete.
version field in dune-project and bin/main.ml .dune build to generate mazeppa.opam .CHANGELOG.md .Not yet, we need to battle-test Mazeppa on some actual programming language. Our long-term goal is to find suitable heuristics to profitably supercompile any source file under 10'000 LoC (in Mazeppa).
For debugging and other purposes, we provide a built-in definitional interpreter that can execute Mazeppa programs. You can launch it by typing mazeppa eval (make sure that your main function does not accept parameters). For the purpose of real execution, we recommend translating Mazeppa to C and then compiling C to machine code, as shown above.
Since Mazeppa is a purely functional language, the only way to implement I/O is as in Haskell 23 : having a pure program that performs computation and a dirty runtime that performs side effects issued by the program. There are no plans to introduce direct I/O into Mazeppa: it will only make everything more complicated.
No, we do not think that a type system is necessary at this point. It is the responsibility of a front-end compiler to ensure that programs do not "go wrong".
The more we make supercompilation predictable, the less it is capable of theorem proving. For those interested in program analysis rather than optimization, we suggest looking into distillation 24 .
For the English audience, the following paper presents a decent introduction into supercompilation:
However, the following papers in Russian describe a supercompilation model that is closer the majority of existing supercompilers, including Mazeppa:
Mazeppa itself is inspired by this excellent paper (in English):
Finally, the international META workshops are great collections of articles about supercompilation and adjacent fields:
Several approaches can lead to superlinear speedup of non-esoteric programs by supercompilation:
None of the above is planned to be implemented in Mazeppa, because 1) we think that writing asymptotically good programs is the responsibility of the programmer, not the optimizer, and 2) predictability of supercompilation is of greater importance to us. However, for those who are interested in this topic, the references may be helpful.
Just fork the repository, work in your own branch, and submit a pull request. Prefer rebasing when introducing changes to keep the commit history as clean as possible.
Valentin F. Turchin. 1986. The concept of a supercompiler. ACM Trans. Program. Lang. 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. วิทยาศาสตร์ 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. วิทยาศาสตร์ 151, 1 (March, 2006), 143–160. https://doi.org/10.1016/j.entcs.2005.11.028 ↩
Klyuchnikov, Ilya, and Dimitur Krustev. "Supercompilation: Ideas and methods." The Monad. Reader Issue 23 (2014): 17. ↩
Klimov, Andrei & Romanenko, Sergei. (2018) Supercompilation: main principles and basic concepts. Keldysh Institute Preprints. 1-36. 10.20948/prepr-2018-111.
Romanenko, Sergei. (2018) Supercompilation: homeomorphic embedding, call-by-name, partial evaluation. Keldysh Institute Preprints. 1-32. 10.20948/prepr-2018-209.
Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. https://dl.acm.org/doi/10.5555/647372.724040 ↩
Secher, JP (2001). Driving in the Jungle. In: Danvy, O., Filinski, A. (eds) Programs as Data Objects. PADO 2001. Lecture Notes in Computer Science, vol 2053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44978-7_12 ↩
Hoffmann, B., Plump, D. (1988). Jungle evaluation for efficient term rewriting. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_71 ↩
Hamilton, Geoff. (2007) Distillation: Extracting the essence of programs. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. 61-70. 10.1145/1244381.1244391.
Hamilton, GW (2010). Extracting the Essence of Distillation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_13 ↩
Hamilton, Geoff & Mendel-Gleason, Gavin. (2010) A Graph-Based Definition of Distillation.
Hamilton, Geoff & Jones, Neil. (2012). Distillation with labelled transition systems. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 15-24. 10.1145/2103746.2103753.
Hamilton, Geoff. "The Next 700 Program Transformers." International Symposium on Logic-Based Program Synthesis and Transformation. Cham: Springer International Publishing, 2021. ↩
Klyuchnikov, Ilya, and Sergei Romanenko. "Towards higher-level supercompilation." Second International Workshop on Metacomputation in Russia. ฉบับ 2. No. 4.2. 2010. ↩
