mazeppa
v0.4.3
SuperCompilación 1 es una técnica de transformación del programa que evalúa simbólicamente un programa dado, con valores de tiempo de ejecución como incógnitas. Al hacerlo, descubre los patrones de ejecución del programa original y los sintetiza en funciones independientes; El resultado de la supercompilación es un programa residual más eficiente. En términos de poder transformador, la supercompilación subsume tanto la deforestación 2 como la evaluación parcial 3 , e incluso exhibe ciertas capacidades de prueba del teorema.
Mazeppa es un supercompilador moderno destinado a ser un objetivo de compilación para los idiomas funcionales de llamada por valor. Tener supercompiladores anteriores comparados y revisados diligentemente, Mazeppa
Primero, prepare el sistema OCAML en su máquina:
$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup
Luego instale Mazeppa como un paquete opam :
$ opam install mazeppa
Escriba mazeppa --help para confirmar la instalación.
Alternativamente, puede clonar el repositorio e instalar Mazeppa manualmente:
$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh
Flambda es un poderoso programa Inliner y especializador para OCAML. Si construye Mazeppa con un compilador OCAML habilitado para el flambda, puede ver un rendimiento mucho mejor. Para configurarlo:
$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)
(Puede usar una versión diferente en lugar de 5.2.0 si lo desea).
Para verificar si Flambda se habilitó con éxito, ejecute:
$ ocamlopt -config | grep flambda
Puedes jugar con Mazeppa sin instalarlo. Tener Ocaml instalado y el repositorio clonado (como se indicó anteriormente), ejecute el siguiente comando desde el directorio raíz:
$ ./scripts/play.sh
(Se requiere GraphViz: sudo apt install graphviz ).
Esto lanzará Mazeppa con --inspect en playground/main.mz y visualizará el gráfico de proceso en target/graph.svg . Este último puede verse en el código VS por la extensión de vista previa SVG.
./scripts/play.sh recompilará automáticamente las fuentes en OCAML, si se cambia algo.
La mejor manera de entender cómo funciona la supercompilación es con el ejemplo. Considere la siguiente función que toma una lista y calcula una suma de sus elementos cuadrados:
[ 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))
};
Este programa está escrito en el estilo funcional idiomático y listado . Cada función hace solo una cosa y lo hace bien. Sin embargo, aquí hay un problema grave: mapSq esencialmente construye una lista que se deconstruye inmediatamente por sum , lo que significa que 1) necesitamos asignar memoria adicional para la lista intermedia, y 2) necesitamos dos pases de cálculo en lugar de uno. La solución a este problema se llama deforestación 2 , que es un caso especial de supercompilación.
Veamos qué hace Mazeppa con este programa:
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
La bandera --inspect le dice a Mazeppa que proporcione un informe detallado sobre el proceso de transformación. El sum-squares/target/ Directorio contendrá los siguientes archivos:
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dot contiene el gráfico de proceso completo para nuestro programa. Puede obtener una imagen del gráfico ejecutando dot -Tsvg target/graph.dot > target/graph.svg .nodes.json contiene el contenido de todos los nodos en el gráfico. Sin este archivo, no podría entender mucho solo con el gráfico.program.json contiene el programa inicial en Mazeppa IR : Nuestro supercompilador funciona con esta representación particular en lugar del programa original.output.mz contiene el programa residual final. output.mz contendrá el siguiente código:
[ examples/sum-squares/target/output.mz ]
main(xs) := f0(xs);
f0(xs) := match xs {
Cons(x, xs') -> +(*(x, x), f0(xs')),
Nil() -> 0i32
};
El supercompilador ha fusionado con éxito sum y mapSq en una sola función, f0 ! A diferencia del programa original, f0 funciona en un solo pase, sin tener que asignar ninguna memoria adicional.
¿Cómo llegó el supercompilador a este punto? Veamos el gráfico de proceso generado:
Para referencia, nodes.json contiene los siguientes datos en 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 " ]
] (No necesitaremos inspeccionar program.json para este pequeño ejemplo, pero no dude en mirarlo: no es demasiado complicado).
El supercompilador comienza con el nodo n0 que contiene main(xs) . Después de dos pasos de desarrollo de la función, alcanzamos el nodo n2 que contiene sum(.g1(xs)) , donde .g1 es la función IR que corresponde a nuestro mapSq . En este punto, no tenemos otra opción que analizar la llamada .g1(xs) conjeturando qué valores xs podría tomar en tiempo de ejecución. Dado que nuestro mapSq solo acepta los constructores Nil y Cons , es suficiente considerar los casos xs=Cons(.v0, .v1) y xs=Nil() solamente.
El nodo n4 es lo que sucede después de sustituir Cons(.v0, .v1) para xs , donde .v0 y .v1 son variables nuevas. Después de tres desarrollos de funciones más, llegamos a n7 . Esta es la primera vez que tenemos que dividir la llamada +(*(.v0, .v0), sum(.g1(.v1))) en .v3=*(.v0, .v0) ( n8 ) y .v4=sum(.g1(.v1)) ( n11 ) y proceda a supercompiling +(.v3, .v4) ( n13 ); La razón para hacerlo es que un nodo anterior ( n2 ) está estructuralmente integrado en n7 , por lo que la supercompilación podría continuar para siempre. Ahora, ¿qué sucede con sum(.g1(.v1)) ( n11 )? ¡Lo hemos visto antes! Recuerde que n2 contiene sum(.g1(xs)) , que es solo un cambio de nombre de sum(.g1(.v1)) ; Así que decidimos doblar n11 en n2 , porque no tiene sentido supercompilear lo mismo dos veces. Las otras ramas de n7 , a saber, n13 y n8 , están descompuestas , lo que significa que simplemente procedemos a transformar sus argumentos.
En cuanto a la otra rama de n2 , sum(Nil()) ( n16 ), es suficiente simplemente desplegar esta llamada a 0i32 ( n18 ).
Después de completar el gráfico de proceso, la residualización lo convierte en un programa final. Durante esta etapa, los patrones de ejecución dinámica se convierten en funciones: el nodo n2 ahora se convierte en la función f0 , en la medida en que algún otro nodo ( n11 ) lo señala. En cualquier programa residual, habrá exactamente tantas funciones como nodos con líneas discontinuas entrantes, más main .
En resumen, la supercompilación consiste en 1) definiciones de funciones de desarrollo, 2) analizar las llamadas que coinciden con un patrón una variable desconocida, 3) descomponiendo el cálculo en partes más pequeñas, 4) plegables cálculos repetidos y 5) las llamadas de descomposición que no pueden desarrollarse, como +(.v3, .v4) ( n13 ) en nuestro ejemplo. Se garantiza que todo el proceso de supercompilación finaliza, porque cuando algún cálculo se está volviendo peligrosamente más grande y más grande, lo dividimos en subproblemas y los resolvemos de forma aislada.
Hay muchos otros ejemplos interesantes de deforestación en los examples/ carpetas, incluidas las estructuras de datos en forma de árbol. De hecho, hemos reimplementado todas las muestras del trabajo anterior en la supercompilación de llamadas por valor de orden superior por Peter A. Jonsson y Johan Nordlander 4 5 ; En todos los casos, Mazeppa ha funcionado de manera similar o mejor.
Ahora considere otro ejemplo, esta vez que implica una evaluación parcial:
[ 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 implementa el famoso algoritmo de exponencia por cuadrado. El programa original es ineficiente: examina recursivamente el parámetro x de powerSq , aunque se conoce perfectamente en el tiempo de compilación. Ejecutar Mazeppa en main(a) producirá el siguiente programa residual:
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
Se ha eliminado toda la función powerSq , logrando así el efecto de la evaluación parcial. (Si consideramos que powerSq es un intérprete para un programa x y los datos de entrada a , entonces es la primera proyección de Futamura: especializar un intérprete para obtener un programa objetivo eficiente). Además, observe cómo el supercompilador ha logrado compartir el argumento *(a, *(a, a)) dos veces, para que no se recompore cada vez. El programa residual de hecho refleja la exponencia por cuadros.
Vayamos más allá de la deforestación y la evaluación parcial. Considere una función matches(p, s) de dos cadenas, que devuelve T() si s contiene p y F() de lo contrario. La implementación ingenua en Mazeppa sería la siguiente, donde p está especializada para "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)
};
(Aquí representamos cadenas como listas de personajes por simplicidad, pero no se preocupe, Mazeppa también proporciona cadenas incorporadas).
El algoritmo es correcto pero ineficiente. Considere lo que sucede cuando "aa" coincide con éxito, pero 'b' no. El algoritmo comenzará a coincidir con "aab" una vez más del segundo personaje de s , aunque ya se puede decir que el segundo personaje de s es 'a' . El autómata finito determinista construido por el algoritmo Knuth-Morris-Pratt (KMP) 6 es una forma alternativa de resolver este problema.
Al ejecutar Mazeppa en la muestra anterior, podemos obtener un algoritmo de coincidencia de cadena eficiente para p="aab" que refleje KMP en acción:
[ 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()
};
¡El algoritmo ingenuo que escribimos se ha transformado automáticamente en una versión eficiente bien conocida! Mientras que el algoritmo ingenuo tiene complejidad o (| p | * | s |) , el especializado es o (| s |) .
La sintetización de KMP es un ejemplo estándar que muestra el poder de la supercompilación con respecto a otras técnicas (por ejemplo, ver 7 y 8 ). Obtener KMP por evaluación parcial no es posible sin cambiar la definición original de matches 9 10 .
Valentin Turchin, el inventor de la supercompilación, describe el concepto de transición del metasíneo de la siguiente manera 11 12 13 :
Considere un sistema de cualquier tipo. Supongamos que hay una manera de hacer una cantidad de copias de ella, posiblemente con variaciones. Suponga que estos sistemas se unen en un nuevo sistema S ' que tiene los sistemas del tipo S como sus subsistemas, e incluye también un mecanismo adicional que controla el comportamiento y la producción de los subsistemas S. Luego llamamos a S ' un metasstema con respecto a S , y la creación de una transición de Metasystem. Como resultado de las transiciones consecutivas de MetaStem, surge una estructura multinivel de control, lo que permite formas complicadas de comportamiento.
Por lo tanto, la supercompilación se puede ver fácilmente como una transición de MetaSstem: hay un programa de objetos en Mazeppa, y existe el supercompilador de Mazeppa que controla y supervisa la ejecución del programa de objetos. Sin embargo, podemos ir más allá y realizar cualquier número de transiciones de MetaSstem dentro del ámbito del programa de objetos en sí, como lo demuestra el siguiente ejemplo.
Usaremos el código de examples/lambda-calculus/ . A continuación se muestra un procedimiento estándar de normalización por evaluación para obtener formas normales beta de términos de cálculo lambda sin tipo:
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 a veces se llaman reflect / reify ).
Esta es esencialmente una máquina de gran paso para una sustitución eficiente de evitación de captura: en lugar de reconstruir términos en cada reducción beta, mantenemos un entorno de valores. eval proyecta un término para el "dominio semántico", mientras que quote hace lo contrario; normalize es simplemente la composición de quote y eval . Para evitar molestarse con una nueva generación de nombres, colocamos índices de Bruijn en los niveles de constructor Var y de Bruijn en NVar ; Este último se convierte en el primero en quoteNeutral .
Ahora calculemos algo con esta máquina:
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))))));
El cuerpo de main calcula la forma normal del término lambda example() que multiplica los números de la iglesia two() y three() .
Al supercompiling main() , obtenemos el número de la iglesia de 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)))))))));
¡El intérprete de cálculo Lambda ha sido completamente aniquilado!
En este ejemplo, acabamos de ver una escalera de metasíneo de dos niveles (en Turchin's Terminology 14 ): en el nivel 0, tenemos el supercompilador MAZeppa que transforma el programa de objetos, mientras que en el nivel 1, tenemos el programa de objetos que normaliza los términos de cálculo lambda. Puede haber un número arbitrario de niveles de interpretación, y Mazeppa se puede usar para colapsarlos a todos. Este comportamiento general de la supercompilación fue explorado por el propio Turchin en 1 (Sección 7), donde pudo supercompilar dos programas interpretables, uno como Fortan y otro en LISP, para obtener un factor de aceleración de 40 en ambos casos.
El Normalizador Lambda también nos muestra cómo encarnar las funciones de orden superior en un idioma de primer orden. En Mazeppa, no podemos tratar las funciones como valores, ¡pero no significa que no podamos simularlas! Al realizar una transición de Metasystem, podemos implementar eficientemente funciones de orden superior en un lenguaje de primer orden. Junto con la desfuncionalización y la conversión de cierre, esta técnica se puede utilizar para la recopilación de idiomas de orden superior en un código eficiente de primer orden.
Ejemplos relacionados: Máquina virtual imperativa, egoísta.
En retrospectiva, el principal problema que impidió la adopción generalizada de la supercompilación es su imprevisibilidad: el lado oscuro de su poder. Para tener una idea de lo que significa, considere cómo podemos resolver cualquier problema de SAT "sobre la marcha":
[ 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)
};
Hay dos cosas mal con este código perfectamente correcto: 1) El supercompilador expandirá la fórmula en el espacio exponencial, y 2) el supercompilador intentará resolver la fórmula expandida en tiempo exponencial. A veces, no queremos evaluar todo en el tiempo de compilación.
Sin embargo, desesperación no: proporcionamos una solución para este problema. Primero consideremos cómo posponer la resolución de la fórmula hasta el tiempo de ejecución. Resulta que lo único que debemos hacer es anotar la formula de la función con @extract de la siguiente manera:
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
Cuando Mazeppa ve solve(formula(a, b, c, d, e, f, g)) , extrae la llamada a formula en una nueva variable .v0 y procede supercompiendo la llamada extraída y solve(.v0) de forma aislada. La última llamada solo reproducirá el solucionador SAT original.
Pero la supercomposición de la llamada a formula aún dará como resultado una explosión exponencial. Examinemos por qué sucede esto. Nuestra fórmula original consiste en llamadas a or y and ; mientras or obviamente no es peligroso, and propaga el parámetro rest a ambas ramas de If (el primer caso match ), este es el lugar exacto donde ocurre la explosión. Así que marquemos and con @extract también:
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
¡Eso es todo! Cuándo and se transformará, Mazeppa extraerá la llamada de su contexto circundante y lo supercompará de forma aislada. Al agregar dos anotaciones en los lugares apropiados, hemos resuelto el problema de la explosión del código y el tiempo de ejecución exponencial de la supercompilación. En general, cada vez que Mazeppa ve ctx[f(t1, ..., tN)] , donde f está marcado @extract y ctx[.] Es un contexto circundante no vacío . En una posición REDEX , enchufará una nueva variable v en ctx y continuará transformando los siguientes nodos por separado: f(t1, ..., tN) y ctx[v] .
Finalmente, tenga en cuenta que @extract es solo un mecanismo de bajo nivel; Un front-end de compilador debe llevar a cabo maquinaria adicional para decirle a Mazeppa qué funciona para extraer. Esto se puede hacer de dos maneras:
formula and como extraíble, dejando todas las otras funciones intactas.Ambos métodos se pueden combinar para lograr un efecto deseado.
Mazeppa emplea una opción de diseño interesante para tener funciones ansiosas y constructores perezosos. El siguiente ejemplo, donde magic(1u32, 1u32) genera números de fibonacci, se adoptó de 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))
}
};
Si los constructores estuvieran ansiosos, magic(1u32, 1u32) nunca terminaría. ¡Sin embargo, Cons no evalúan sus argumentos! Dado que getIt solo consume una parte finita de la lista infinita, el programa termina e imprime 2u32 :
$ mazeppa eval
2u32
Los constructores perezosos permiten la deforestación sin esfuerzo, como se discute a continuación.
Después de instalar Mazeppa a través de opam o ./scripts/install.sh , ¡está disponible como una biblioteca OCAML!
Configure un nuevo proyecto Dune de la siguiente manera:
$ dune init project my_compiler
Agregue mazeppa como una biblioteca de terceros a su bin/dune :
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
Pegue el siguiente código en bin/main.ml (esto es examples/sum-squares/main.mz codificado en 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
;; Ejecute dune exec my_compiler para ver el programa residual deseado:
[([], "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))))]
)))
]
Puede llamar a Mazeppa tantas veces como desee, incluso en paralelo. Tenga en cuenta que exponemos una interfaz limitada al supercompilador; En particular, no hay forma de inspeccionar lo que hace en el proceso (es decir, --inspect ).
Además de la supercompilación, también proporcionamos un evaluador incorporado:
val eval : Raw_program .t -> Raw_term .t Solo se puede llamar a los programas cuyas funciones main no aceptan parámetros. A diferencia de supercompile , produce un término evaluado de tipo Raw_term.t y posiblemente puede divergir.
Vea otras funciones de API y su documentación en lib/mazeppa.mli .
Supongamos que main.mz contiene una versión ligeramente modificada del ejemplo de fibonacci perezoso:
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))
}
};
El siguiente comando lo traduce a C11 con extensiones GNU (es decir, -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 );
} El comando translate requiere tanto --language , que es el idioma de destino para la traducción, y --entry , que es el nombre de un símbolo externo que correspondirá a su función main . El programa de entrada Mazeppa proviene de stdin ( cat main.mz en nuestro ejemplo); El programa GNU11 de salida se escribe en stdout .
Avancemos más y compilemos el programa de salida a un archivo de objeto. Primero, copie c/deps/sds.c , c/deps/sds.h y c/deps/sdsalloc.h a su directorio actual; En segundo lugar, instale boehm gc en su computadora:
$ sudo apt install libgc-dev -y
Luego ejecute el siguiente comando:
$ cat main.mz
| mazeppa translate --language C --entry fib --dump-header-to .
| gcc -c -o program.o -std=gnu11 -xc -
La opción --dump-header-to escribe el contenido de mazeppa.h en una ubicación especificada; Esto es necesario para que el programa de salida compilara. El comando gcc acepta el programa de salida de stdin y produce program.o . O.
Ahora lo que queda es invocar la función fib generada. Crear main.c con el siguiente contenido:
#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 ));
} Este programa de "controlador" simplemente invoca fib con un entero Mazeppa ( MZ_INT ) e imprime el resultado. Puede usar cualquier funcionalidad de mazeppa.h , siempre que no tenga prefijo con mz_priv_ o MZ_PRIV_ .
Para unir todas las piezas:
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out imprime fib(10) = 55 y sale, como se esperaba.
--inspect en un entorno real: úselo solo para fines de depuración.@extract (como se muestra arriba) para controlar si continúa con supercompilación o extrae el redex."otus" es más pequeño que "octopus" pero "octopusx" no lo es. Mazeppa emplea varias opciones de diseño interesantes (clasificadas por importancia):
Código de primer orden. Max Bolingbroke y Simon Peyton Jones 15 informan que para un ejemplo particular, su supercompilador de orden superior para un subconjunto de Haskell gastó el 42% del tiempo de ejecución en la gestión de nombres y el nombre de nombre. Si bien es cierto que los modelos de evaluación simplistas, como la normalización de los términos de Lambda, nos permiten evitar una sobrecarga significativa de la evitación de captura, la supercompilación es más complicada. Por ejemplo, además de hacer un cálculo simbólico, la supercompilación debe analizar los resultados previamente calculados para tomar decisiones informadas sobre una transformación adicional: considere las pruebas de instancia de términos, las pruebas de incrustación homeomórfica, la mayoría de las generalizaciones específicas, etc., la introducción de funciones de orden más alta inevitablemente todos estos análisis, lo que hace que la supercompilación sea más delgada, más reclutamiento de memoria, y endurecer a la razón. En Mazeppa, nos apegamos a la filosofía de mejoras graduales: en lugar de tratar de manejar muchas características elegantes al mismo tiempo, 1) arreglamos el lenguaje central para una manipulación conveniente por una máquina, 2) realice tantas transiciones de metasistema como sea necesario para mejorar el lenguaje central para los humanos.
Constructores perezosos. Es una observación bien conocida de que los idiomas de llamada por valor son difíciles para la deforestación adecuada. Todavía es posible deforestarlos, pero no sin análisis adicional 4 5 . Sin embargo, si los constructores son perezosos (es decir, no evalúan sus argumentos), la deforestación simplemente funciona . Turchin lo hizo funcionar mediante la transformación de orden normal de un lenguaje de llamada por valor, pero el resultado es que el código residual puede terminar con más frecuencia. En Mazeppa, tenemos funciones de llamado por valor y constructores de llamadas por nombre (llamadas por necesidad), que 1) hace posible la deforestación y 2) preserva la semántica original de código.
Gráficos de proceso sin término. En Mazeppa, los gráficos de procesos no contienen ninguna referencia a los términos: la residualización puede funcionar sin ellos. Como resultado, el recolector de basura puede desear los términos que se usaron durante la construcción de un subgrafio. Además de eso, esta política tiene varias otras ventajas importantes: 1) El gráfico todavía está allí para inspección con --inspect , 2) Cuando se dibuja, solo revela información sobre las decisiones que el supercompilador ha tomado, lo que hace que sea mucho más fácil de ver. Varios supercompiladores existentes se abstienen de los gráficos de proceso adecuados (por ejemplo, el Supero 17 de Neil Mitchell y los 15 mencionados anteriormente), pero como resultado, 1) son menos capaces de inspección por un usuario, 2) Los algoritmos se desordenan con los detalles de la generación de código.
Análisis de configuración bidimensional. Por lo general, un supercompilador mantiene una "historia" de un subconjunto de todos los antepasados mientras transforma un nodo; Si este nodo está "lo suficientemente cerca" de uno de sus antepasados, es hora de dividir el término en partes más pequeñas para garantizar la terminación. En Mazeppa, mantenemos dos estructuras de datos separadas: la que contiene un subconjunto de antepasados de nodos y el que contiene un subconjunto de nodos completamente transformados. La primera estructura de datos se utiliza para garantizar la terminación (como de costumbre), mientras que la segunda se utiliza para mejorar el intercambio de funciones en el código residual. Específicamente, si el nodo actual (de tipo especial) es un cambio de nombre de algún nodo transformado previamente, doblamos el nodo actual en este nodo anterior. De esta manera, Mazeppa realiza un análisis vertical y horizontal de las configuraciones, lo que hace que el código residual sea más compacto y la supercompilación más eficiente.
Análisis de productividad de la función. Cuando una función interna de la función de la función coincide con un valor desconocido, ocurren dos cosas potencialmente peligrosas: 1) La supercompilación reproduce la estructura de la función de coincidencia de patrones, 2) la supercompilación empuja todo el contexto circundante a todas las ramas de esta función. Sin un mayor control, esta situación puede conducir a una explosión significativa en el tamaño del código, a veces incluso causando que un supercompilador no termine en una cantidad razonable de tiempo. Para mejorar, Mazeppa duplica el contexto de que esta llamada interna produce un valor de nivel superior definido de al menos un punto de salida, porque si lo hace, las grandes posibilidades de que este valor pueda deconstruir mediante una coincidencia de patrones posterior. De lo contrario, Mazeppa extrae la llamada interna y la transforma de forma aislada (como si estuviera marcada con @extract ). Además, si el contexto realmente se duplica, la siguiente regla se aplica a todas las ramas: si la rama produce un valor de nivel superior definido desde todos los puntos de salida, se transforma en el contexto como de costumbre; De lo contrario, la rama se extrae del contexto y se transforma de forma aislada. En la práctica, este análisis evita una gran cantidad de especializaciones innecesarias, compactando así el tamaño del programa residual y haciendo que la supercompilación sea mucho más manejable.
Historias inteligentes. En lugar de comparar ciegamente un nodo actual con todos sus antepasados, empleamos un control de grano más fino, es decir, 1) los nodos globales (los que analizan una variable desconocida) se comparan solo con los nodos globales, 2) los nodos locales (los que reducen linealmente en un solo paso) se comparan con los nodos locales solo con el último nodo global, pero no incluyen los nodos triviales (los que se rompen los términos más pequeños en los términos más pequeños con los componentes más pequeños con los últimos componentes con los últimos componentes con los últimos componentes en los que se encuentran los últimos componentes con los últimos componentes. Además de un enfoque más económico para la verificación de la terminación, este esquema permite que Mazeppa descubra más oportunidades de optimización; Ver 18 , Secciones 4.6 y 4.7. La terminación de la supercompilación está garantizada por el hecho de que la incrustación homeomórfica todavía se prueba en todas las subsecuencias potencialmente infinitas de los términos globales y locales (no puede existir una secuencia infinita de términos triviales solo).
Firmas de redex. El silbato solo se prueba en términos con firmas RedEx iguales. Una firma REDEX es un par de 1) el símbolo de una función y 2) una lista de categorías de valor de argumento. Una categoría de valor es una especie de metainformación sobre un argumento, que puede ser 1) VConst para valores como 42i32 o "hello world" , 2) VNeutral para valores tales como x o +(x, x) o 3) VCCall(c) para llamadas de constructor como Foo(...) . El silbato todavía se prueba en todas las secuencias de términos potencialmente infinitas, porque cualquier secuencia infinita debe contener al menos una subsecuencia infinita de los términos con la misma firma REDEX. Esta estrategia permite que Mazeppa evite la sobre generalización en ciertos casos, como lo demuestran los siguientes dos ejemplos:
f(A()) está incrustado homeomórficamente en f(g(B(A()))) ; Sin embargo, dado que los operadores REDEX son diferentes ( f y g ), MazeppA continúa la reducción y alcanza el resultado ideal.f(A(Good())) está incrustada en f(f(f(B(A(Good()))))) y el operador REDEX es f en ambos casos, MazeppA no generaliza demasiado porque estos dos términos tienen categorías de valor diferentes en sus firmas REDEX: en el primer caso, f se llama A(...) , mientras que en el segundo caso, se convoca en B(...) . Al igual que en el ejemplo anterior, Mazeppa alcanza el resultado ideal de la supercompilación únicamente por reducción.Incrustación homeomórfica optimizada. A lo largo de las décadas, la incrustación homeomórfica ha ganado reputación por ser un excelente método para la verificación de terminación en línea 19 . Desafortunadamente, principalmente debido al flujo de control no lineal (cuando se aplican tanto el buceo como el acoplamiento), puede ser inexcusablemente costoso de calcular. Lo que es aún peor, se vuelve a ejecutar para todos los nodos parentales calificados cada vez que se agrega un nuevo término a la historia, lo que ralentiza progresivamente la supercompilación a medida que la historia crece: ¡hasta ahora en la mayor parte del tiempo de supercompilación! Para hacer frente a eso, mantenemos dos cachés separados:
Hash en consecuencia. Los cachés de incrustación homeomórficos descritos anteriormente dependen de cuántos términos se comparten . Por lo tanto, empleamos el hash que considera mientras desarrollamos los cuerpos de la función: si algún término t nuevo es estructuralmente igual a algunos términos existentes existentes, este último se reutiliza. Para evitar fugas de memoria, empleamos un efímero global que tiene consejos débiles a los términos. Además de los tiempos de supercompilación mejorados (debido a la memoización), el hash que considera también reduce el consumo de memoria; consulte el #4 (comentario).
Normalización durante el desarrollo. Cuando se desarrolla una llamada de función, sustituimos los parámetros y normalizamos el cuerpo tanto como sea posible (es decir, sin más desarrollo, para garantizar la terminación). Para ver por qué, considere la función factorial f(n) ; Con un despliegue simple, atraparíamos en una situación desagradable donde f(1u32) está incrustada en *(1u32, f(-(1u32, 1u32))) , causando sobre generalización . En realidad, Mazeppa se desarrollaría f(1u32) a *(1u32, f(0u32)) , lo que hace que este último sea un candidato para un mayor desarrollo. Este enfoque se sugirió en 20 , Sección 4.5. Sus otros méritos son: 1) menos trabajo para futuros pasos de conducción, 2) menos cálculo "banal" en gráficos de proceso, 3) cantidad reducida de pruebas costosas de incrustación homeomórfica.
*(1u32, f(-(1u32, 1u32))) ya no se verifica contra f(1u32) debido a los diferentes operadores de RedEx. Sin embargo, otras ventajas de la normalización aún se mantienen.Implementación en OCAML. Mazeppa se implementa utilizando una combinación de estilos de programación funcional e imperativo, que es muy natural en OCAML. Las excepciones se utilizan no solo para situaciones "excepcionales", la mutabilidad dentro de las funciones es común. Aunque no tenemos un supercompilador similar escrito en EG Haskell o Rust para comparación, creemos que es Ocaml lo que nos dio una implementación de trabajo sin tener que pelear con el idioma y nunca terminar el trabajo.
Si bien la mayor parte de lo anterior no es particularmente novedoso, creemos que la combinación de estas características hace que Mazeppa sea una alternativa más práctica que sus predecesores.
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 ).Notas:
_ ) 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 | Significado |
|---|---|
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 | Notas |
|---|---|---|
// ... 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)Notación:
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 ; entonces: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. Programa. 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. Electrón. 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. Volumen 2. No. 4.2. 2010. ↩
