mazeppa
v0.4.3
Supercompilation 1 é uma técnica de transformação do programa que avalia simbolicamente um determinado programa, com valores de tempo de execução como desconhecidos. Ao fazer isso, ele descobre padrões de execução do programa original e os sintetiza em funções independentes; O resultado da supercompilação é um programa residual mais eficiente. Em termos de poder transformacional, a supercompilação subumes o desmatamento 2 e a avaliação parcial 3 , e até exibe certas capacidades do teorema.
O Mazeppa é um supercompiler moderno destinado a ser um alvo de compilação para linguagens funcionais de chamada por valor. Tendo supercompilers anteriores comparados e revisados diligentemente, Mazeppa
Primeiro, prepare o sistema OCAML em sua máquina:
$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup
Em seguida, instale o Mazeppa como um pacote opam :
$ opam install mazeppa
Tipo mazeppa --help para confirmar a instalação.
Como alternativa, você pode clonar o repositório e instalar o Mazeppa manualmente:
$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh
Flambda é um poderoso programa e especializador para o OCAML. Se você construir Mazeppa com um compilador OCAML habilitado para Flambda, poderá ver um desempenho muito melhor. Para configurá -lo:
$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)
(Você pode usar uma versão diferente em vez de 5.2.0 , se desejar.)
Para verificar se Flambda foi ativado com sucesso, execute:
$ ocamlopt -config | grep flambda
Você pode brincar com Mazeppa sem realmente instalá -lo. Tendo o OCAML instalado e o repositório clonado (como acima), execute o seguinte comando no diretório raiz:
$ ./scripts/play.sh
(GraphViz é necessário: sudo apt install graphviz .)
Isso lançará o Mazeppa com --inspect no playground/main.mz e visualizar o gráfico do processo no target/graph.svg . Este último pode ser visualizado no código VS pela extensão de visualização SVG.
./scripts/play.sh recomitará automaticamente as fontes no OCAML, se algo for alterado.
A melhor maneira de entender como a supercompilação funciona é por exemplo. Considere a seguinte função que pega uma lista e calcula uma soma de seus elementos quadrados:
[ 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 é escrito no estilo funcional idiomático e listado . Toda função faz apenas uma coisa e faz bem. No entanto, há um problema sério aqui: mapSq constrói essencialmente uma lista que será desconstruída imediatamente por sum , o que significa que 1) precisamos alocar memória extra para a lista intermediária e 2) precisamos de dois passes de computação em vez de um. A solução para esse problema é chamada de desmatamento 2 , que é um caso especial de supercompilação.
Vamos ver o que Mazeppa faz com este programa:
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
A bandeira --inspect diz a Mazeppa para fornecer um relatório detalhado sobre o processo de transformação. O sum-squares/target/ DIRETORY CONTIRÁ os seguintes arquivos:
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dot contém o gráfico de processo completo para o nosso programa. Você pode obter uma imagem do gráfico executando dot -Tsvg target/graph.dot > target/graph.svg .nodes.json contém o conteúdo de todos os nós no gráfico. Sem esse arquivo, você não seria capaz de entender muito apenas do gráfico.program.json contém o programa inicial em Mazeppa IR : Nosso supercompiler trabalha com essa representação específica em vez do programa original.output.mz contém o programa residual final. output.mz conterá o seguinte 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
};
O supercompiler mesclou com sucesso sum e mapSq em uma única função, f0 ! Ao contrário do programa original, f0 funciona em um único passe, sem precisar alocar nenhuma memória extra.
Como o supercompiler chegou a esse ponto? Vamos ver o gráfico de processo gerado:
Para referência, nodes.json contém os seguintes dados em 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 " ]
] (Não precisaremos inspecionar program.json para este pequeno exemplo, mas fique à vontade para analisá -lo: não é muito complicado.)
O supercompiler começa com o nó n0 contendo main(xs) . Após duas etapas de desdobramento de função, atingimos o nó n2 contendo sum(.g1(xs)) , onde .g1 é a função IR que corresponde ao nosso mapSq . Nesse ponto, não temos outra opção senão analisar a chamada .g1(xs) conjentando o que os valores xs podem levar em tempo de execução. Como nosso mapSq aceita apenas os construtores Nil e Cons , é suficiente considerar os casos xs=Cons(.v0, .v1) e xs=Nil() somente.
O nó n4 é o que acontece depois de substituirmos Cons(.v0, .v1) por xs , onde .v0 e .v1 são variáveis frescas. Após mais três funções, chegamos ao n7 . É a primeira vez que precisamos dividir a chamada +(*(.v0, .v0), sum(.g1(.v1))) em .v3=*(.v0, .v0) ( n8 ) e .v4=sum(.g1(.v1)) +(.v3, .v4) ) ( n11 n13 e prosseguir supercomilor A razão para isso é que um nó anterior ( n2 ) está estruturalmente incorporado no n7 , para que a supercompilação possa continuar para sempre. Agora, o que acontece com sum(.g1(.v1)) ( n11 )? Nós vimos isso antes! Lembre -se de que n2 contém sum(.g1(xs)) , que é apenas uma renomeação da sum(.g1(.v1)) ; Por isso, decidimos dobrar n11 em n2 , porque não faz sentido supercomplicar a mesma coisa duas vezes. Os outros ramos de n7 , a saber, n13 e n8 , são decompostos , o que significa que simplesmente procedemos transformando seus argumentos.
Quanto ao outro ramo de n2 , sum(Nil()) ( n16 ), é suficiente apenas desdobrar essa chamada para 0i32 ( n18 ).
Após a conclusão do gráfico do processo, a residualização o converte em um programa final. Durante esse estágio, os padrões dinâmicos de execução se tornam funções - o nó n2 agora se torna a função f0 , na medida em que algum outro nó ( n11 ) aponta para ele. Em qualquer programa residual, haverá exatamente tantas funções quanto nós com linhas tracejadas de entrada, além de main .
Em resumo, a supercompilação consiste em 1) definições de funções em desdobramento, 2) analisando chamadas que correspondem a um padrão de uma variável desconhecida, 3) quebrando a computação em partes menores, 4) cálculos repetidos dobráveis e 5) em decomposição chamadas que não podem ser desdobradas, como +(.v3, .v4) ( n13 ) no nosso exemplo. Todo o processo de supercompilação é garantido para terminar, porque quando algum computação está se tornando perigosamente cada vez maior, dividimos -o em subproblemas e os resolvemos isoladamente.
Existem muitos outros exemplos interessantes de desmatamento nos examples/ pasta, incluindo estruturas de dados semelhantes a árvores. De fato, reimpletamos todas as amostras do trabalho anterior sobre supercompilação de chamada de ordem superior de Peter A. Jonsson e Johan Nordlander 4 5 ; Em todos os casos, o Mazeppa teve um desempenho semelhante ou melhor.
Agora considere outro exemplo, desta vez envolvendo avaliação 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 o famoso algoritmo de exponenciação por quadrado. O programa original é ineficiente: examina recursivamente o parâmetro x do powerSq , embora seja perfeitamente conhecido em tempo de compilação. A execução do Mazeppa no main(a) produzirá o seguinte programa residual:
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
Toda a função powerSq foi eliminada, alcançando assim o efeito da avaliação parcial. (Se considerarmos powerSq como um intérprete para um programa x e dados de entrada a , é a primeira projeção de Futamura: especializando um intérprete para obter um programa de destino eficiente. Além disso, observe como o supercompiler conseguiu compartilhar o argumento *(a, *(a, a)) duas vezes, o que não é recompado a cada tempo. O programa residual de fato reflete a exponenciação ao quadrilha.
Vamos além do desmatamento e da avaliação parcial. Considere uma função matches(p, s) de duas cordas, que retornam T() se s contém p e F() caso contrário. A implementação ingênua em Mazeppa seria o seguinte, onde p é especializado em "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)
};
(Aqui representamos strings como listas de caracteres para simplificar, mas não se preocupe, o Mazeppa também fornece seqüências embutidas.)
O algoritmo é correto, mas ineficiente. Considere o que acontece quando "aa" é comparado com sucesso, mas 'b' não é. O algoritmo começará a corresponder "aab" mais uma vez do segundo personagem de s , embora já se possa dizer que o segundo personagem de s é 'a' . O autômato finito determinístico criado pelo algoritmo Knuth-Morris-Pratt (KMP) 6 é uma maneira alternativa de resolver esse problema.
Ao executar o Mazeppa na amostra acima, podemos obter um algoritmo de correspondência de string eficiente para p="aab" que reflete o KMP em ação:
[ 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 algoritmo ingênuo que escrevemos foi automaticamente transformado em uma versão eficiente bem conhecida! Enquanto o algoritmo ingênuo tem complexidade o (| p | * | s |) , o especializado é o (| s |) .
A sintetização de KMP é um exemplo padrão que mostra o poder da supercompilação em relação a outras técnicas (por exemplo, ver 7 e 8 ). A obtenção de KMP por avaliação parcial não é possível sem alterar a definição original de matches 9 10 .
Valentin Turchin, o inventor da supercompilação, descreve o conceito de transição do metaSistema da seguinte maneira 11 12 13 :
Considere um sistema de qualquer tipo. Suponha que exista uma maneira de fazer um número de cópias, possivelmente com variações. Suponha que esses sistemas estejam unidos em um novo sistema S ' que possui os sistemas do tipo S como seus subsistemas e inclui também um mecanismo adicional que controla o comportamento e a produção dos S -Subsystems. Em seguida, chamamos de S ' A Metasystem em relação a S , e a criação da transição de metaystem. Como resultado da transição consecutiva do metaSistema, surge uma estrutura multinível de controle, o que permite formas de comportamento complicadas.
Assim, a supercompilação pode ser prontamente vista como uma transição de metaSistema: existe um programa de objetos em Mazeppa, e há o Mazeppa Supercompiler que controla e supervisiona a execução do programa de objetos. No entanto, podemos ir mais longe e executar qualquer número de transições de metaSistema dentro do reino do próprio programa de objetos, como o próximo exemplo demonstra.
Usaremos o código dos examples/lambda-calculus/ . Abaixo está um procedimento padrão de normalização por avaliação para obter as formas normais beta de termos de cálculo lambda não saqueados:
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 às vezes é chamado de reflect / reify .)
Esta é essencialmente uma máquina grande para a substituição eficiente da substituição de captura: em vez de reconstruir os termos em cada redução beta, mantemos um ambiente de valores. eval projeta um termo para o "domínio semântico", enquanto quote faz o oposto; normalize é simplesmente a composição da quote e eval . Para evitar se preocupar com a nova geração de nomes, colocamos os índices de Bruijn nos níveis de construtor e de Bruijn NVar Var Este último é convertido no primeiro em quoteNeutral .
Agora vamos calcular algo com 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))))));
O corpo de main calcula a forma normal do termo lambda example() que multiplica os números da igreja two() e three() .
Por supercomplicar main() , obtemos o número de igreja 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)))))))));
O intérprete de cálculo de Lambda foi completamente aniquilado!
Neste exemplo, acabamos de ver uma escada de metaSistema de dois níveis (na terminologia de Turchin 14 ): no nível 0, temos o supercompiler Mazeppa transformando o programa de objetos, enquanto no nível 1, temos o programa de objetos normalizando os termos do cálculo lambda. Pode haver um número arbitrário de níveis de interpretação, e o Mazeppa pode ser usado para colapsar todos eles. Esse comportamento geral da supercompilação foi explorado pelo próprio Turchin em 1 (seção 7), onde ele conseguiu supercompilar dois programas interpretáveis, um para o Fortran e outro no Lisp, para obter um fator de aceleração de 40 em ambos os casos.
O normalizador da Lambda também nos mostra como encarnar as funções de ordem superior em um idioma de primeira ordem. Em Mazeppa, não podemos tratar as funções como valores, mas isso não significa que não possamos simulá -las! Ao executar uma transição de metaystem, podemos implementar com eficiência funções de ordem superior em uma linguagem de primeira ordem. Juntamente com a desnutalização e a conversão de fechamento, essa técnica pode ser usada para compilação de idiomas de ordem superior em código de primeira ordem eficiente.
Exemplos relacionados: Máquina virtual imperativa, autoconfiança.
Em retrospecto, o principal problema que impedia a adoção generalizada da supercompilação é sua imprevisibilidade - o lado sombrio de seu poder. Para ter uma noção do que isso significa, considere como podemos resolver qualquer problema no SAT "na mosca":
[ 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)
};
Há duas coisas erradas com este código perfeitamente correto: 1) o supercompiler expandirá a fórmula no espaço exponencial e 2) o supercompiler tentará resolver a fórmula expandida em tempo exponencial. Às vezes, simplesmente não queremos avaliar tudo em tempo de compilação.
No entanto, não desespero: fornecemos uma solução para esse problema. Vamos primeiro considerar como adiar a solução da fórmula até o tempo de execução. Acontece que a única coisa que precisamos fazer é anotar a formula da função com @extract da seguinte maneira:
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
Quando o Mazeppa vê solve(formula(a, b, c, d, e, f, g)) , extrai a chamada para a formula para uma nova variável .v0 e prossegue sobrecarregar a chamada extraída e solve(.v0) em isolamento. A última chamada apenas reproduzirá o solucionador de SAT original.
Mas a supercomposição da chamada para a formula ainda resultará em uma explosão exponencial. Vamos examinar por que isso acontece. Nossa fórmula original consiste em chamadas para or e and ; Embora or obviamente não seja perigoso and propaga o parâmetro rest para ambos os ramos de If (o primeiro caso match ) - este é o local exato onde ocorre a explosão. Então, vamos marcar and com @extract também:
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
É isso! Quando and deve ser transformado, Mazeppa extrairá a chamada para fora de seu contexto circundante e a supercomporá isoladamente. Ao adicionar duas anotações em locais apropriados, resolvemos o problema de explosão de código e tempo de execução exponencial de supercompilação. Em geral, sempre que Mazeppa vê ctx[f(t1, ..., tN)] , onde f está marcado @extract e ctx[.] É um contexto circundante não vazio . Em uma posição RedEx , ele conectará uma variável v em ctx e prosseguirá transformando os seguintes nós separadamente: f(t1, ..., tN) e ctx[v] .
Finalmente, observe que @extract é apenas um mecanismo de baixo nível; Um front-end do compilador deve realizar máquinas adicionais para dizer a Mazeppa que funções para extrair. Isso pode ser feito de duas maneiras:
formula and como extraível, deixando todas as outras funções intocadas.Ambos os métodos podem ser combinados para obter um efeito desejado.
A Mazeppa emprega uma escolha interessante de design para ter funções ansiosas e construtores preguiçosos. O exemplo a seguir, onde magic(1u32, 1u32) gera números de Fibonacci, foi adotada por 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))
}
};
Se os construtores estivessem ansiosos, magic(1u32, 1u32) nunca terminaria. No entanto, Cons não avalia seus argumentos! Como getIt consome apenas uma parte finita da lista infinita, o programa termina e imprime 2u32 :
$ mazeppa eval
2u32
Os construtores preguiçosos permitem o desmatamento sem esforço, conforme discutido abaixo.
Depois de instalar o Mazeppa via opam ou ./scripts/install.sh , ele está disponível como uma biblioteca OCAML!
Configure um novo projeto de duna da seguinte maneira:
$ dune init project my_compiler
Adicione mazeppa como uma biblioteca de terceiros na sua bin/dune :
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
Cole o seguinte código em bin/main.ml (são examples/sum-squares/main.mz codificado em 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
;; Run dune exec my_compiler para ver o programa residual desejado:
[([], "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))))]
)))
]
Você pode chamar Mazeppa quantas vezes quiser, inclusive em paralelo. Observe que expomos uma interface limitada ao supercompiler; Em particular, não há como inspecionar o que ele faz no processo (ou seja, --inspect ).
Além da supercompilação, também fornecemos um avaliador interno:
val eval : Raw_program .t -> Raw_term .t Ele só pode ser chamado em programas cujas main funções não aceitam parâmetros. Ao contrário supercompile , ele produz um termo avaliado do tipo Raw_term.t e pode divergir.
Veja outras funções da API e sua documentação em lib/mazeppa.mli .
Suponha que main.mz contenha uma versão ligeiramente modificada do exemplo de Fibonacci preguiçoso:
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))
}
};
O comando a seguir o traduz para C11 com extensões GNU (ou seja, -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 );
} O comando translate requer ambos --language , que é o idioma de destino para tradução e --entry , que é o nome de um símbolo externo que corresponderá à sua função main . O programa Mazeppa de entrada vem do stdin ( cat main.mz em nosso exemplo); O programa GNU11 de saída é gravado para stdout .
Vamos avançar ainda mais e compilar o programa de saída para um arquivo de objeto. Primeiro, cópia c/deps/sds.c , c/deps/sds.h e c/deps/sdsalloc.h no seu diretório atual; Segundo, instale o Boehm GC no seu computador:
$ sudo apt install libgc-dev -y
Em seguida, execute o seguinte comando:
$ cat main.mz
| mazeppa translate --language C --entry fib --dump-header-to .
| gcc -c -o program.o -std=gnu11 -xc -
A opção --dump-header-to escreve o conteúdo do mazeppa.h em um local especificado; Isso é necessário para o programa de saída compilar. O comando gcc aceita o programa de saída do stdin e produz program.o .
Agora, o que resta é realmente invocar a função fib gerada. Crie main.c com o seguinte conteúdo:
#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 ));
} Esse programa "driver" apenas chama fib com um inteiro mazeppa ( MZ_INT ) e imprime o resultado. Você pode usar qualquer funcionalidade do mazeppa.h , desde que ele não seja prefixado com mz_priv_ ou MZ_PRIV_ .
Para reunir todas as peças:
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out imprime fib(10) = 55 e sai, como esperado.
--inspect em um ambiente real: use -o apenas para fins de depuração.@extract (como mostrado acima) para controlar se deve continuar supercompilação ou extrair o RedEx."otus" é menor que "octopus" , mas "octopusx" não é. Mazeppa emprega várias opções de design interessantes (classificadas por importância):
Código de primeira ordem. Max Bolingbroke e Simon Peyton Jones 15 relatam que, para um exemplo em particular, seu supercompilador de ordem superior para um subconjunto de Haskell gastou 42% do tempo de execução no gerenciamento de nomes e renomeação. Embora seja verdade que os modelos de avaliação simplista, como a normalização dos termos do Lambda, nos permitem evitar uma sobrecarga significativa de prevenção de captura, a supercompilação é mais complicada. Por exemplo, além de fazer computação simbólica, a supercompilação precisa analisar os resultados calculados anteriormente para tomar decisões informadas sobre a transformação adicional: considere testes de instância de termo, testes de incorporação homeomórfica, generalizações específicas, etc. Introdução de funções mais lentas, mais complicações com memória mais lenta. Em Mazeppa, mantemos a filosofia de melhorias graduais: em vez de tentar lidar com muitos recursos sofisticados ao mesmo tempo, 1) corrigimos a linguagem principal para manipulação conveniente por uma máquina, 2) executar quantas transições de metaSistema são necessárias para melhorar a linguagem central para o ser humano.
Construtores preguiçosos. É uma observação bem conhecida de que as linguagens de chamada por valor são difíceis para o desmatamento adequado. Ainda é possível desmatar -os, mas não sem análise adicional 4 5 . No entanto, se os construtores são preguiçosos (ou seja, eles não avaliam seus argumentos), o desmatamento funciona apenas . O Turchin fez funcionar pela transformação de ordem normal de uma linguagem de chamada por valor, mas o resultado é que o código residual pode terminar com mais frequência. Em Mazeppa, temos funções de chamada por valor e construtores de call-by-name (chamada por necessidade), que 1) possibilita o desmatamento e 2) preserva a semântica original do código.
Gráficos de processo sem termos. Em Mazeppa, os gráficos de processo não contêm nenhuma referência a termos: a residualização pode funcionar sem eles. Como resultado, o coletor de lixo pode desalocar termos que foram usados durante a construção de um subgraf. Além disso, essa política possui várias outras vantagens importantes: 1) o gráfico ainda está lá para inspeção com --inspect , 2) quando é desenhado, ele apenas revela informações sobre as decisões que o supercompiler tomou, o que facilita muito a observar. Vários supercompiladores existentes abstêm os gráficos de processo adequados (por exemplo, o SuperO 17 de Neil Mitchell e o acima mencionado 15 ), mas, como resultado, 1) são menos capazes de inspeção por um usuário, 2) os algoritmos ficam confusos com detalhes da geração de código.
Análise de configuração bidimensional. Geralmente, um supercompiler mantém uma "história" de um subconjunto de todos os ancestrais enquanto transforma um nó; Se esse nó estiver "próximo o suficiente" para um de seus ancestrais, é hora de dividir o termo em partes menores para garantir a rescisão. Em Mazeppa, mantemos duas estruturas de dados separadas: a que contém um subconjunto dos ancestrais do nó e o que contém um subconjunto de nós totalmente transformados. A antiga estrutura de dados é usada para garantir a rescisão (como sempre), enquanto o último é usado para aprimorar o compartilhamento de funções no código residual. Especificamente, se o nó atual (de tipo especial) for uma renomeação de algum nó anteriormente transformado, dobramos o nó atual nesse nó anterior. Dessa forma, o Mazeppa executa a análise vertical e horizontal de configurações, o que torna o código residual mais compacto e a supercompilação mais eficiente.
Análise de produtividade da função. Quando um padrão de chamada de função interna corresponde a um valor desconhecido, duas coisas potencialmente perigosas acontecem: 1) a supercompilação reproduz a estrutura da função de correspondência de padrões, 2) a supercompilação impulsiona todo o contexto circundante a todos os ramos desta função. Sem controle adicional, essa situação pode levar a uma explosão significativa no tamanho do código, às vezes até fazendo com que um supercompiler não termine em uma quantidade razoável de tempo. Para melhorar, Mazeppa duplica o contexto se essa chamada interna produz um valor definitivo de nível superior a partir de pelo menos um ponto de saída, porque, se o fizer, grandes chances de que esse valor possa ser desconstruído pela correspondência subsequente de padrões. Caso contrário, o Mazeppa extrai a chamada interna e a transforma isoladamente (como se estivesse marcada com @extract ). Além disso, se o contexto for realmente duplicado, a regra a seguir se aplica a todas as filiais: se a filial produzir um valor definitivo de nível superior de todos os pontos de saída, será transformado no contexto como de costume; Caso contrário, o ramo é extraído do contexto e transformado isoladamente. Na prática, essa análise impede uma enorme quantidade de especializações desnecessárias, compactificando o tamanho do programa residual e tornando a supercompilação muito mais tratável.
Histórias inteligentes. Instead of blindly comparing a current node with all its ancestors, we employ a more fine-grained control, that is: 1) global nodes (the ones that analyze an unknown variable) are compared with global nodes only, 2) local nodes (the ones that reduce linearly in a single step) are compared with local nodes only up to the latest global node, but not including it, and 3) trivial nodes (the ones that break down terms into smaller components) are not compared with algo mais. Além de uma abordagem mais econômica para a verificação de rescisão, esse esquema permite que Mazeppa descubra mais oportunidades de otimização; Veja 18 , seções 4.6 e 4.7. A rescisão da supercompilação é garantida pelo fato de que a incorporação homeomórfica ainda é testada em todas as subsequências potencialmente infinitas de termos globais e locais (não há apenas uma sequência infinita de termos triviais).
Assinaturas RedEx. O apito é testado apenas em termos com assinaturas iguais de redel . Uma assinatura RedEx é um par de 1) símbolo de uma função e 2) uma lista de categorias de valor de argumento. Uma categoria de valor é uma espécie deformação sobre um argumento, que pode ser 1) VConst para valores como 42i32 ou "hello world" , 2) VNeutral para valores como x ou +(x, x) ou 3) VCCall(c) para chamadas de construtor como Foo(...) . O apito ainda é testado em todas as seqüências potencialmente infinitas de termos, porque qualquer sequência infinita deve conter pelo menos uma subsequência infinita de termos com a mesma assinatura do RedEx. Essa estratégia permite que Mazeppa evite a excesso de generalização em certos casos, como os dois exemplos a seguir demonstram:
f(A()) é homeomorficamente incorporado a f(g(B(A()))) ; No entanto, como os operadores RedEx são diferentes ( f e g ), o Mazeppa continua a redução e atinge o resultado ideal.f(A(Good())) seja incorporado em f(f(f(B(A(Good()))))) e o operador RedEx é f em ambos os casos, o f não é generalizado demais porque esses dois termos têm categorias de valor diferentes em suas A(...) , no primeiro caso, é chamado de B(...) , enquanto. Assim como no exemplo anterior, Mazeppa atinge o resultado ideal da supercompilação exclusivamente por redução.Incorporação homeomórfica otimizada. Ao longo das décadas, a incorporação homeomórfica ganhou reputação de ser um excelente método para a verificação de rescisão on -line 19 . Infelizmente, principalmente devido ao fluxo de controle não linear (quando o mergulho e o acoplamento se aplicam), pode ser indesticável de calcular. O que é ainda pior, ele é reexecionado para todos os nós pais qualificados sempre que um novo termo é adicionado à história, que diminui progressivamente a supercompilação à medida que a história cresce: ir até comer a maior parte do tempo de supercompilação! Para lidar com isso, mantemos dois caches separados:
Hash consting. Os caches de incorporação homeomórfica descritos acima dependem de quantos termos são compartilhados . Portanto, empregamos a hash consting durante os órgãos de função que se desenrolam: se algum novo termo t for estruturalmente igual a alguns termos existentes, o último será reutilizado. Para evitar vazamentos de memória, empregamos um Ephemeron global, segurando dicas fracas a termos. Além de melhorar os tempos de supercompilação (devido à memórias), a consumo de hash também reduz o consumo de memória - ver #4 (comentário).
Normalização durante o desdobramento. Quando uma chamada de função é desdobrada, substituímos os parâmetros e normalizamos o corpo o máximo possível (ou seja, sem desdobramentos adicionais, para garantir a rescisão). Para ver o porquê, considere a função fatorial f(n) ; Com um simples desdobramento, prenderíamos em uma situação desagradável em que f(1u32) é incorporado a *(1u32, f(-(1u32, 1u32))) , causando excesso de generalização . Na realidade, Mazeppa se desenrolaria f(1u32) para *(1u32, f(0u32)) , tornando o último candidato para se desenrolar. Essa abordagem foi sugerida em 20 , Seção 4.5. Seus outros méritos são: 1) menos trabalho para futuras etapas de direção, 2) menos computação "banal" em gráficos de processo, 3) quantidade reduzida de testes caros de incorporação homeomórfica.
*(1u32, f(-(1u32, 1u32))) não é mais verificado contra f(1u32) por causa de diferentes operadores RedEx. No entanto, outras vantagens da normalização ainda se mantêm.Implementação em OCAML. O Mazeppa é implementado usando uma combinação de estilos de programação funcionais e imperativos, o que é muito natural de fazer no OCAML. Exceções são usadas não apenas para situações "excepcionais", as funções internas de mutabilidade são comuns. Embora não tenhamos um supercompiler semelhante escrito em EG Haskell ou Rust para comparação, acreditamos que é o OCAML que nos deu uma implementação em funcionamento sem ter que brigar com o idioma e nunca terminar o trabalho.
Embora a maioria das opções acima não seja particularmente nova, acreditamos que a combinação desses recursos faz de Mazeppa uma alternativa mais prática do que seus antecessores.
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)Notação:
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 ; então: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. Elétron. Notes Theor. Comput. Sci. 151, 1 (March, 2006), 143–160. https://doi.org/10.1016/j.entcs.2005.11.028 ↩
Klyuchnikov, Ilya, and Dimitur Krustev. "Supercompilation: Ideas and methods." The Monad. Reader Issue 23 (2014): 17. ↩
Klimov, Andrei & Romanenko, Sergei. (2018). Supercompilation: main principles and basic concepts. Keldysh Institute Preprints. 1-36. 10.20948/prepr-2018-111. ↩
Romanenko, Sergei. (2018). Supercompilation: homeomorphic embedding, call-by-name, partial evaluation. Keldysh Institute Preprints. 1-32. 10.20948/prepr-2018-209. ↩
Robert Glück and Morten Heine Sørensen. 1996. A Roadmap to Metacomputation by Supercompilation. In Selected Papers from the International Seminar on Partial Evaluation. Springer-Verlag, Berlin, Heidelberg, 137–160. https://dl.acm.org/doi/10.5555/647372.724040 ↩
Secher, JP (2001). Driving in the Jungle. In: Danvy, O., Filinski, A. (eds) Programs as Data Objects. PADO 2001. Lecture Notes in Computer Science, vol 2053. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44978-7_12 ↩
Hoffmann, B., Plump, D. (1988). Jungle evaluation for efficient term rewriting. In: Grabowski, J., Lescanne, P., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1988. Lecture Notes in Computer Science, vol 343. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50667-5_71 ↩
Hamilton, Geoff. (2007). Distillation: Extracting the essence of programs. Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. 61-70. 10.1145/1244381.1244391. ↩
Hamilton, GW (2010). Extracting the Essence of Distillation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2009. Lecture Notes in Computer Science, vol 5947. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11486-1_13 ↩
Hamilton, Geoff & Mendel-Gleason, Gavin. (2010). A Graph-Based Definition of Distillation. ↩
Hamilton, Geoff & Jones, Neil. (2012). Distillation with labelled transition systems. Conference Record of the Annual ACM Symposium on Principles of Programming Languages. 15-24. 10.1145/2103746.2103753. ↩
Hamilton, Geoff. "The Next 700 Program Transformers." International Symposium on Logic-Based Program Synthesis and Transformation. Cham: Springer International Publishing, 2021. ↩
Klyuchnikov, Ilya, and Sergei Romanenko. "Towards higher-level supercompilation." Second International Workshop on Metacomputation in Russia. Vol. 2. No. 4.2. 2010. ↩
