mazeppa
v0.4.3
SuperCompilation 1은 런타임 값을 미지의 런 타임 값으로 주어진 프로그램을 상징적으로 평가하는 프로그램 변환 기술입니다. 그렇게함으로써 원래 프로그램의 실행 패턴을 발견하고 독립형 함수로 합성합니다. 슈퍼 컴파일의 결과는보다 효율적인 잔류 프로그램입니다. 변형력의 관점에서, 슈퍼 컴파일은 삼림 벌채 2 와 부분 평가 3을 모두 사용하고, 심지어 정리 증명의 특정 기능을 나타냅니다.
Mazeppa 는 콜 별 기능 언어의 편집 목표가되기위한 현대적인 슈퍼 컴퓨터입니다. 사전 슈퍼 컴퓨터가 부지런히 비교되고 수정 된 Mazeppa
먼저 컴퓨터에서 OCAML 시스템을 준비하십시오.
$ bash -c "sh <(curl -fsSL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh)"
$ opam init --auto-setup
그런 다음 Mazeppa를 opam 패키지로 설치하십시오.
$ opam install mazeppa
설치를 확인하려면 mazeppa --help 입력하십시오.
또는 저장소를 복제하고 mazeppa를 수동으로 설치할 수 있습니다.
$ git clone https://github.com/mazeppa-dev/mazeppa.git
$ cd mazeppa
$ ./scripts/install.sh
Flambda는 OCAML의 강력한 프로그램 인 라이너 및 스페셜 라이저입니다. Flambda 지원 OCAML 컴파일러로 Mazeppa를 구축하면 성능이 훨씬 향상 될 수 있습니다. 설정하려면 :
$ opam switch create 5.2.0+flambda ocaml-variants.5.2.0+options ocaml-option-flambda
$ eval $(opam env --switch=5.2.0+flambda)
(원하는 경우 5.2.0 대신 다른 버전을 사용할 수 있습니다.)
Flambda가 성공적으로 활성화되었는지 확인하려면 실행하십시오.
$ ocamlopt -config | grep flambda
실제로 설치하지 않고 Mazeppa와 함께 플레이 할 수 있습니다. OCAML을 설치하고 저장소가 클로닝 된 상태에서 (위와 같이) 루트 디렉토리에서 다음 명령을 실행합니다.
$ ./scripts/play.sh
(GraphViz가 필요합니다 : sudo apt install graphviz ).)
이것은 playground/main.mz 에서 --inspect 사용하여 Mazeppa를 시작하고 target/graph.svg 에서 프로세스 그래프를 시각화합니다. 후자는 SVG 미리보기 확장에 의해 대 코드에서 볼 수 있습니다.
./scripts/play.sh 무엇이든 변경되면 OCAML의 소스를 자동으로 재 컴파일합니다.
슈퍼 컴파일의 작동 방식을 이해하는 가장 좋은 방법은 예입니다. 목록을 취하고 제곱 요소의 합을 계산하는 다음 기능을 고려하십시오.
[ examples/sum-squares/main.mz ]
main(xs) := sum(mapSq(xs));
sum(xs) := match xs {
Nil() -> 0i32,
Cons(x, xs) -> +(x, sum(xs))
};
mapSq(xs) := match xs {
Nil() -> Nil(),
Cons(x, xs) -> Cons(*(x, x), mapSq(xs))
};
이 프로그램은 관용적이고 목록이 많은 기능 스타일로 작성되었습니다. 모든 기능은 한 가지만 수행하며 잘 수행합니다. 그러나 여기에는 심각한 문제가 있습니다. mapSq 본질적으로 sum 에 의해 즉시 해체 될 목록을 구성합니다. 즉, 우리는 1) 중간 목록에 추가 메모리를 할당해야하며 2) 하나 대신 두 가지 계산 패스가 필요합니다. 이 문제에 대한 해결책을 삼림 벌채 2 라고하며, 이는 특별한 슈퍼 컴파일의 경우입니다.
이 프로그램에서 Mazeppa가하는 일을 보자.
$ mkdir sum-squares
$ cd sum-squares
# Copy-paste the program above.
$ nano main.mz
$ mazeppa run --inspect
--inspect 플래그는 Mazeppa에게 변환 과정에 대한 자세한 보고서를 제공하도록 지시합니다. sum-squares/target/ 디렉토리에는 다음 파일이 포함됩니다.
target
├── graph.dot
├── nodes.json
├── output.mz
└── program.json
graph.dot 에는 프로그램의 완전한 프로세스 그래프가 포함되어 있습니다. dot -Tsvg target/graph.dot > target/graph.svg 실행하여 그래프 사진을 얻을 수 있습니다.nodes.json 에는 그래프에 모든 노드의 내용이 포함되어 있습니다. 이 파일이 없으면 그래프만으로는 이해할 수 없습니다.program.json 에는 Mazeppa IR 의 초기 프로그램이 포함되어 있습니다. SuperCompiler는 원래 프로그램 대신이 특정 표현과 함께 작동합니다.output.mz 에는 최종 잔류 프로그램이 포함되어 있습니다. output.mz 다음 코드를 포함합니다.
[ examples/sum-squares/target/output.mz ]
main(xs) := f0(xs);
f0(xs) := match xs {
Cons(x, xs') -> +(*(x, x), f0(xs')),
Nil() -> 0i32
};
SuperCompiler는 sum 과 mapSq 단일 함수 f0 으로 성공적으로 병합했습니다! 원래 프로그램과 달리 f0 추가 메모리를 할당하지 않고 단일 패스로 작동합니다.
SuperCompiler는 어떻게이 시점에 도달 했습니까? 생성 된 프로세스 그래프를 보자.
참고로 nodes.json JSON에 다음 데이터를 포함합니다.
[
[ " n0 " , " main(xs) " ],
[ " n1 " , " sum(mapSq(xs)) " ],
[ " n2 " , " sum(.g1(xs)) " ],
[ " n3 " , " xs " ],
[ " n4 " , " sum(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n5 " , " .g0(Cons(*(.v0, .v0), mapSq(.v1))) " ],
[ " n6 " , " +(*(.v0, .v0), sum(mapSq(.v1))) " ],
[ " n7 " , " +(*(.v0, .v0), sum(.g1(.v1))) " ],
[ " n8 " , " *(.v0, .v0) " ],
[ " n9 " , " .v0 " ],
[ " n10 " , " .v0 " ],
[ " n11 " , " sum(.g1(.v1)) " ],
[ " n12 " , " .v1 " ],
[ " n13 " , " +(.v3, .v4) " ],
[ " n14 " , " .v3 " ],
[ " n15 " , " .v4 " ],
[ " n16 " , " sum(Nil()) " ],
[ " n17 " , " .g0(Nil()) " ],
[ " n18 " , " 0i32 " ]
] (우리는이 작은 예를 위해 program.json 검사 할 필요는 없지만 자유롭게 살펴보십시오. 너무 복잡하지 않습니다.)
SuperCompiler는 main(xs) 포함하는 노드 n0 으로 시작합니다. 두 단계의 기능이 전개 된 후, 우리는 sum(.g1(xs)) 포함하는 노드 n2 에 도달합니다. 여기서 .g1 우리의 mapSq 에 해당하는 ir 함수입니다. 이 시점에서, 우리는 xs 런타임에 취할 수있는 값을 추측하여 전화 .g1(xs) 을 분석하는 것 외에 다른 선택은 없습니다. mapSq 는 생성자를 Nil 및 Cons 만 받아들이므로 xs=Cons(.v0, .v1) 및 xs=Nil() 만 고려하는 것으로 충분합니다.
노드 n4 는 xs 로 Cons(.v0, .v1) 대체 한 후에 발생합니다. 여기서 .v0 및 .v1 은 새로운 변수입니다. 3 번의 기능이 더 전개되면 n7 에 도착합니다. Call +(*(.v0, .v0), sum(.g1(.v1))) .v3=*(.v0, .v0) ( n8 ) 및 .v4=sum(.g1(.v1)) ( n11 )으로 분할 해야하는 것은 이번 +(.v3, .v4) n13 입니다. 그렇게하는 이유는 이전 노드 ( n2 )가 n7 에 구조적으로 내장되어 있으므로 슈퍼 컴파일이 영원히 계속 될 수 있기 때문입니다. 이제 sum(.g1(.v1)) ( n11 )에서 어떻게됩니까? 우리는 그것을 일찍 보았습니다! n2 sum(.g1(xs)) 함유하고 있으며, 이는 단지 sum(.g1(.v1)) 의 이름을 바꾸는 것입니다. 그래서 우리는 n11 n2 로 접기 로 결정했습니다. 왜냐하면 같은 것을 두 번 슈퍼 컴파일하는 것은 의미가 없기 때문입니다. n7 의 다른 가지, 즉 n13 및 n8 은 분해되어 단순히 논증을 변화시킨다는 것을 의미합니다.
n2 의 다른 지점, sum(Nil()) ( n16 )의 경우이 호출을 0i32 ( n18 )로 전개하는 것으로 충분합니다.
프로세스 그래프가 완료된 후 잔류화는 최종 프로그램으로 변환합니다. 이 단계에서 동적 실행 패턴이 함수가됩니다. Node n2 이제 다른 노드 ( n11 )가 가리키는 것처럼 기능 f0 이됩니다. 모든 잔류 프로그램에서는 수신 선이있는 노드와 main 있는 노드만큼이나 많은 기능이 있습니다.
요약하면, SuperCompilation은 1) 전개 함수 정의, 2) 패턴 매치를 알 수없는 변수로 분석하는 것을 분석하고, 3) 작은 부분으로 계산을 분해, 4) 반복 계산 및 5) +(.v3, .v4) ( n13 )와 같이 전개 할 수없는 호출을 분해합니다. 전체 수퍼 컴파일 프로세스는 종료 될 수 있습니다. 일부 계산이 위험하고 점점 커질 때 하위 문제로 분류하여 분리하여 해결하기 때문입니다.
트리와 같은 데이터 구조를 포함하여 examples/ 폴더에는 삼림 벌채의 다른 흥미로운 예가 많이 있습니다. 실제로, 우리는 Peter A. Jonsson과 Johan Nordlander 4 5 의 고차 콜 별 수퍼 컴파일에 대한 이전 연구에서 모든 샘플을 다시 구현했습니다. 모든 경우에, Mazeppa는 비슷하거나 더 나은 성과를 거두었습니다.
이제 또 다른 예를 고려하십시오. 이번에는 부분 평가와 관련이 있습니다.
[ examples/power-sq/main.mz ]
main(a) := powerSq(a, 7u8);
powerSq(a, x) := match =(x, 0u8) {
T() -> 1i32,
F() -> match =(%(x, 2u8), 0u8) {
T() -> square(powerSq(a, /(x, 2u8))),
F() -> *(a, powerSq(a, -(x, 1u8)))
}
};
square(a) := *(a, a);
powerSq 유명한 지수 별 제곱 알고리즘을 구현합니다. 원래 프로그램은 비효율적입니다. 컴파일 타임에 완벽하게 알려져 있지만 powerSq 의 x 매개 변수를 재귀 적으로 검사합니다. main(a) 에서 Mazeppa를 실행하면 다음 잔류 프로그램이 제공됩니다.
[ examples/power-sq/target/output.mz ]
main(a) := let v0 := *(a, *(a, a)); *(a, *(v0, v0));
전체 powerSq 함수가 제거되어 부분 평가의 효과를 달성했습니다. ( powerSq 프로그램 x 및 입력 데이터 a 의 통역사로 간주하는 경우, 그것은 최초의 Futamura 프로젝션입니다. 효율적인 대상 프로그램을 얻기 위해 통역사를 전문화 합니다. *(a, *(a, a)) 잔류 프로그램은 실제로 제곱에 의한 지수를 반영합니다.
삼림 벌채와 부분 평가를 넘어서합시다. 두 문자열의 함수 matches(p, s) 고려하십시오. s 에 p 및 F() 가 포함 된 경우 T() 반환합니다. Mazeppa의 순진한 구현은 다음과 같습니다. 여기서 p "aab" 에 특화되어 있습니다.
[ examples/kmp-test/main.mz ]
main(s) := matches(Cons('a', Cons('a', Cons('b', Nil()))), s);
matches(p, s) := go(p, s, p, s);
go(pp, ss, op, os) := match pp {
Nil() -> T(),
Cons(p, pp) -> goFirst(p, pp, ss, op, os)
};
goFirst(p, pp, ss, op, os) := match ss {
Nil() -> F(),
Cons(s, ss) -> match =(p, s) {
T() -> go(pp, ss, op, os),
F() -> failover(op, os)
}
};
failover(op, os) := match os {
Nil() -> F(),
Cons(_s, ss) -> matches(op, ss)
};
(여기서 우리는 단순성을위한 문자 목록으로 문자열을 나타내지 만 걱정하지 마십시오. Mazeppa는 내장 문자열도 제공합니다.)
알고리즘은 정확하지만 비효율적입니다. "aa" 성공적으로 일치 할 때 어떻게되는지 고려하지만 'b' 그렇지 않습니다. 알고리즘은 s 의 두 번째 문자와 다시 한 번 "aab" 와 일치하기 시작하지만 이미 s 의 두 번째 문자는 'a' 라고 말할 수 있습니다. Knuth-Morris-Pratt 알고리즘 (KMP) 6 에 의해 구축 된 결정 론적 유한 자동화는이 문제를 해결하는 대안적인 방법입니다.
위의 샘플에서 mazeppa를 실행하면 실제로 KMP를 반영하는 p="aab" 에 대한 효율적인 문자열 일치 알고리즘을 얻을 수 있습니다.
[ examples/kmp-test/target/output.mz ]
main(s) := f0(s);
f0(s) := match s {
Cons(s', ss) -> match =(97u8, s') {
F() -> f1(ss),
T() -> f2(ss)
},
Nil() -> F()
};
f1(ss) := f0(ss);
f2(ss) := match ss {
Cons(s, ss') -> match =(97u8, s) {
F() -> f1(ss'),
T() -> f4(ss')
},
Nil() -> F()
};
f3(ss) := f2(ss);
f4(ss) := match ss {
Cons(s, ss') -> match =(98u8, s) {
F() -> match =(97u8, s) {
F() -> f1(ss'),
T() -> f4(ss')
},
T() -> T()
},
Nil() -> F()
};
우리가 쓴 순진한 알고리즘은 자동으로 잘 알려진 효율적인 버전으로 변환되었습니다! 순진한 알고리즘은 복잡성 O (| p | * | s |) 를 가지지 만 특수 알고리즘은 O (| s |) 입니다.
KMP 합성은 다른 기술과 관련하여 슈퍼 컴파일의 힘을 보여주는 표준 예입니다 (예 : 7 및 8 참조). matches 의 원래 정의를 변경하지 않으면 부분 평가에 의해 KMP를 얻는 것이 불가능합니다. 9 10 .
슈퍼 컴파일의 발명가 인 Valentin Turchin은 다음과 같은 방식으로 Metasystem 전이 의 개념을 설명합니다. 11 12 13 :
모든 종류의 시스템 을 고려하십시오. 변형이있는 몇 가지 사본을 만들 수있는 방법이 있다고 가정 해 봅시다. 이러한 시스템이 S 유형 의 시스템을 하위 시스템으로 사용하는 새로운 시스템으로 통합되었으며 S- 서브 시티스의 동작 및 생산을 제어하는 추가 메커니즘도 포함한다고 가정 해 봅시다. 그런 다음 우리는 S ' 와 S ' 와 관련하여 METASYSTEM을 부릅니다. 연속 메타 시스텀의 결과로, 다단계 제어 구조가 발생하여 복잡한 형태의 행동을 허용합니다.
따라서, 슈퍼 컴파일은 Metasystem 전환으로 쉽게 볼 수 있습니다. Mazeppa에는 객체 프로그램이 있으며 객체 프로그램의 실행을 제어하고 감독하는 Mazeppa SuperCompiler가 있습니다. 그러나 다음 예에서 알 수 있듯이 객체 프로그램 자체의 영역 내에서 더 많은 수의 메타지 전환을 수행 할 수 있습니다.
우리는 examples/lambda-calculus/ 의 코드를 사용할 것입니다. 아래는 표준 정규화 별 평가 절차입니다.
normalize(lvl, env, t) := quote(lvl, eval(env, t));
normalizeAt(lvl, env, t) := normalize(+(lvl, 1u64), Cons(vvar(lvl), env), t);
vvar(lvl) := Neutral(NVar(lvl));
eval(env, t) := match t {
Var(idx) -> indexEnv(env, idx),
Lam(body) -> Closure(env, body),
Appl(m, n) ->
let mVal := eval(env, m);
let nVal := eval(env, n);
match mVal {
Closure(env, body) -> eval(Cons(nVal, env), body),
Neutral(nt) -> Neutral(NAppl(nt, nVal))
}
};
quote(lvl, v) := match v {
Closure(env, body) -> Lam(normalizeAt(lvl, env, body)),
Neutral(nt) -> quoteNeutral(lvl, nt)
};
quoteNeutral(lvl, nt) := match nt {
NVar(var) -> Var(-(-(lvl, var), 1u64)),
NAppl(nt, nVal) -> Appl(quoteNeutral(lvl, nt), quote(lvl, nVal))
};
indexEnv(env, idx) := match env {
Nil() -> Panic(++("the variable is unbound: ", string(idx))),
Cons(value, xs) -> match =(idx, 0u64) {
T() -> value,
F() -> indexEnv(xs, -(idx, 1u64))
}
};
( eval / quote 때때로 reflect / reify 라고 불립니다.)
이것은 본질적으로 효율적인 캡처 피하 대체를위한 큰 단계 기계입니다. 각 베타 감소에 대한 용어를 재구성하는 대신 값 환경을 유지합니다. eval 는 "의미 론적 영역"에 대한 용어를 투사하는 반면 quote 그 반대입니다. normalize 단순히 quote 과 eval 의 구성입니다. 신선한 이름 생성을 방지하기 위해, 우리는 de bruijn 지수를 Var 생성자와 de bruijn 레벨 에 NVar 에 넣습니다. 후자는 quoteNeutral 에서 전자로 전환된다.
이제이 컴퓨터로 무언가를 계산하겠습니다.
main() := normalize(0u64, Nil(), example());
example() := Appl(Appl(mul(), two()), three());
two() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))));
three() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64),
Var(0u64))))));
mul() := Lam(Lam(Lam(Lam(Appl(
Appl(Var(3u64), Appl(Var(2u64), Var(1u64))),
Var(0u64))))));
main 본문은 교회 숫자 two() 및 three() 에 곱하는 Lambda 용어 example() 의 정상적인 형태를 계산합니다.
SuperCompiling main() 을 통해 6의 교회 숫자를 얻습니다.
[ examples/lambda-calculus/target/output.mz ]
main() := Lam(Lam(Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64), Appl(Var(1u64)
, Appl(Var(1u64), Appl(Var(1u64), Var(0u64)))))))));
Lambda Calculus 통역사는 완전히 전멸되었습니다!
이 예에서 우리는 방금 2 단계 메시 스템 계단 (Turchin 's terminology 14 에서)을 보았습니다. 레벨 0에는 Mazeppa SuperCompiler가 객체 프로그램을 변환하는 반면 레벨 1에는 Lambda 미적분학 용어를 정규화하는 객체 프로그램이 있습니다. 임의의 수의 해석 수준이있을 수 있으며 Mazeppa를 사용하여 모든 것을 무너 뜨릴 수 있습니다. 슈퍼 컴파일의 이러한 일반적인 행동은 Turchin 자신에 의해 1 (섹션 7)에 의해 탐구되었으며, 두 경우 모두 Fortran과 유사하고 LISP로 2 개의 해석 가능한 프로그램을 슈퍼 컴파일 할 수 있었으며 두 경우 모두 속도 업 계수를 얻을 수있었습니다.
Lambda Normalizer는 또한 고차 기능을 1 차 언어로 성화시키는 방법을 보여줍니다. Mazeppa에서는 기능을 값으로 취급 할 수는 없지만 시뮬레이션 할 수 없다는 의미는 아닙니다! Metasystem 전환을 수행함으로써 우리는 1 차 언어로 고차의 기능을 효율적으로 구현할 수 있습니다. 방어 화 및 클로저 변환과 함께이 기술은 고차 언어를 효율적인 1 차 코드로 편집하는 데 사용할 수 있습니다.
관련 사례 : 명령형 가상 머신, 자기 간 프리터.
돌이켜 보면, 슈퍼 컴파일의 광범위한 채택을 막는 주요 문제는 그 힘의 어두운면 인 예측 불가능 성입니다. 그것이 무엇을 의미하는지 이해하려면 "즉시"문제를 해결할 수있는 방법을 고려하십시오.
[ examples/sat-solver/main.mz ]
main(a, b, c, d, e, f, g) := solve(formula(a, b, c, d, e, f, g));
formula(a, b, c, d, e, f, g) :=
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Var(e), or(Not(g), F()))),
and(or(Var(e), or(Not(g), or(Var(f), F()))),
and(or(Not(g), or(Var(c), or(Var(d), F()))),
and(or(Var(a), or(Not(b), or(Not(c), F()))),
and(or(Not(f), or(Not(e), or(Var(g), F()))),
and(or(Var(a), or(Var(a), or(Var(c), F()))),
and(or(Not(g), or(Not(d), or(Not(b), F()))),
T()))))))));
or(x, rest) := match x {
Var(x) -> If(x, T(), rest),
Not(x) -> If(x, rest, T())
};
and(clause, rest) := match clause {
If(x, m, n) -> If(x, and(m, rest), and(n, rest)),
T() -> rest,
F() -> F()
};
solve(formula) := match formula {
If(x, m, n) -> analyze(x, m, n),
T() -> T(),
F() -> F()
};
analyze(x, m, n) := match x {
T() -> solve(m),
F() -> solve(n)
};
이 완벽하게 올바른 코드에는 두 가지가 있습니다. 1) SuperCompiler는 지수 공간에서 공식을 확장하고 2) SuperCompiler는 지수 시간에 확장 된 공식을 해결하려고합니다. 때로는 컴파일 타임에 모든 것을 평가하고 싶지 않습니다.
그러나 절망은 아닙니다 : 우리는이 문제에 대한 해결책을 제공합니다. 먼저 런타임까지 공식을 해결하는 방법을 고려해 봅시다. 우리가해야 할 유일한 것은 다음과 같이 @extract 로 함수 formula 주석을 달라는 것입니다.
@extract
formula(a, b, c, d, e, f, g) :=
// Everything is the same.
Mazeppa가 solve(formula(a, b, c, d, e, f, g)) 보면 formula 을 신선한 변수 .v0 으로 추출하고 추출 된 통화 및 solve(.v0) 분리하는 것을 슈퍼 컴퓨팅합니다. 후자의 호출은 원래 SAT 솔버를 재현합니다.
그러나 formula 에 대한 호출을 슈퍼 컴퓨팅하면 여전히 지수 적 블로우가 발생할 수 있습니다. 이런 일이 발생하는 이유를 살펴 보겠습니다. 우리의 원래 공식은 or 로 구성됩니다 and 위험하지 or 위험하지 and rest 매개 변수를 If (첫 번째 match 케이스)의 두 분기로 전파합니다. 이곳은 블로우 업이 발생하는 정확한 장소입니다. 따라서 @extract 표시 and 같이 표시하겠습니다.
@extract
and(clause, rest) := match clause {
// Everything is the same.
};
그게 다야! 변형 and 때, Mazeppa는 주변 컨텍스트에서 호출을 추출하여 분리하여 슈퍼 컴파일합니다. 적절한 장소에 두 개의 주석을 추가함으로써 코드 블로우 업 문제와 수퍼 컴파일의 지수 실행 시간을 모두 해결했습니다. 일반적으로 Mazeppa가 ctx[f(t1, ..., tN)] 볼 때마다 f @extract 로 표시되고 ctx[.] 주변 컨텍스트가 아닌 컨텍스트입니다 . Redex 위치 에서는 새로운 변수 v ctx 에 연결하고 다음 노드를 개별적으로 변환합니다. f(t1, ..., tN) 및 ctx[v] .
마지막으로 @extract 는 저수준 메커니즘 일뿐입니다. 컴파일러 프론트 엔드는 추가 기계를 수행하여 추출 할 기능을하는 Mazeppa에게 알려야합니다. 이것은 두 가지 방법으로 수행 할 수 있습니다.
formula and 추출 가능성을 모두 표시하여 다른 모든 함수를 그대로 유지합니다.두 방법 모두 결합하여 원하는 효과를 달성 할 수 있습니다.
Mazeppa는 열렬한 기능과 게으른 생성자를 갖기 위해 흥미로운 디자인 선택을 사용합니다. magic(1u32, 1u32) 이 Fibonacci 번호를 생성하는 다음 예는 Haskell에서 채택되었습니다.
[ examples/lazy-fibonacci/main.mz ]
main() := getIt(magic(1u32, 1u32), 3u64);
magic(m, n) := match =(m, 0u32) {
T() -> Nil(),
F() -> Cons(m, magic(n, +(m, n)))
};
getIt(xs, n) := match xs {
Nil() -> Panic("undefined"),
Cons(x, xs) -> match =(n, 1u64) {
T() -> x,
F() -> getIt(xs, -(n, 1u64))
}
};
생성자가 열망한다면 magic(1u32, 1u32) 결코 종료되지 않을 것입니다. 그러나 Cons 그 주장을 평가하지 않습니다! getIt 무한 목록의 유한 한 부분 만 소비하기 때문에 프로그램은 종료되고 2u32 인쇄합니다.
$ mazeppa eval
2u32
게으른 생성자는 아래에서 논의 된 바와 같이 쉽게 변하는 삼림 벌채를 가능하게합니다.
opam 또는 ./scripts/install.sh 통해 Mazeppa를 설치 한 후 OCAML 라이브러리로 제공됩니다!
다음과 같이 새로운 모래 언덕 프로젝트를 설정하십시오.
$ dune init project my_compiler
bin/dune 에 mazeppa 타사 라이브러리로 추가하십시오.
(executable
(public_name my_compiler)
(name main)
(libraries my_compiler mazeppa))
다음 코드를 bin/main.ml 에 붙여 넣습니다 (이것은 OCAML에서 인코딩 된 examples/sum-squares/main.mz 입니다) :
open Mazeppa
let input : Raw_program.t =
let sym = Symbol. of_string in
let open Raw_term in
let open Checked_oint in
[ [], sym " main " , [ sym " xs " ], call ( " sum " , [ call ( " mapSq " , [ var " xs " ]) ])
; ( []
, sym " sum "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), int ( I32 ( I32. of_int_exn 0 ))
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call ( " + " , [ var " x " ; call ( " sum " , [ var " xs " ]) ]) )
] ) )
; ( []
, sym " mapSq "
, [ sym " xs " ]
, Match
( var " xs "
, [ (sym " Nil " , [] ), call ( " Nil " , [] )
; ( (sym " Cons " , [ sym " x " ; sym " xs " ])
, call
( " Cons "
, [ call ( " * " , [ var " x " ; var " x " ]); call ( " mapSq " , [ var " xs " ]) ] ) )
] ) )
]
;;
let () =
try
let output = Mazeppa. supercompile input in
Printf. printf " %s n " ( Raw_program. show output)
with
| Mazeppa. Panic msg ->
Printf. eprintf " Something went wrong: %s n " msg;
exit 1
;; dune exec my_compiler 실행하여 원하는 잔여 프로그램을보십시오.
[([], "main", ["xs"], (Raw_term.Call ("f0", [(Raw_term.Var "xs")])));
([], "f0", ["xs"],
(Raw_term.Match ((Raw_term.Var "xs"),
[(("Cons", ["x"; "xs'"]),
(Raw_term.Call ("+",
[(Raw_term.Call ("*", [(Raw_term.Var "x"); (Raw_term.Var "x")]));
(Raw_term.Call ("f0", [(Raw_term.Var "xs'")]))]
)));
(("Nil", []), (Raw_term.Const (Const.Int (Checked_oint.I32 0))))]
)))
]
병렬을 포함하여 원하는만큼 Mazeppa를 호출 할 수 있습니다. 제한된 인터페이스를 SuperCompiler에 노출시킵니다. 특히, 프로세스에서 수행하는 일을 검사 할 방법이 없습니다 (즉, --inspect ).
수퍼 컴파일 외에도 내장 평가자도 제공합니다.
val eval : Raw_program .t -> Raw_term .t main 기능이 매개 변수를 허용하지 않는 프로그램에서만 호출 될 수 있습니다. supercompile 과 달리 Raw_term.t 유형의 평가 된 용어를 생성하며 분기 될 수 있습니다.
lib/mazeppa.mli 의 다른 API 기능 및 해당 문서를 참조하십시오.
main.mz 에 약간 수정 된 게으른 피보나치의 예제가 포함되어 있다고 가정합니다.
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))
}
};
다음 명령은 GNU 확장 (예 : -std=gnu11 )으로 C11로 변환합니다.
$ cat main.mz | mazeppa translate --language C --entry fib
#include "mazeppa.h"
MZ_ENUM_USER_TAGS ( op_Cons , op_Nil );
static mz_Value op_main ( mz_ArgsPtr args );
static mz_Value op_magic ( mz_ArgsPtr args );
static mz_Value op_getIt ( mz_ArgsPtr args );
static mz_Value thunk_0 ( mz_EnvPtr env ) {
mz_Value var_m = ( env )[ 0 ];
mz_Value var_n = ( env )[ 1 ];
return ({
struct mz_value args [ 2 ];
( args )[ 0 ] = var_n ;
( args )[ 1 ] = MZ_OP2 ( var_m , add , var_n );
op_magic ( args );
});
}
static mz_Value op_main ( mz_ArgsPtr args ) {
mz_Value var_n = ( args )[ 0 ];
return ({
struct mz_value args [ 2 ];
( args )[ 0 ] = ({
struct mz_value args [ 2 ];
( args )[ 0 ] = MZ_INT ( U , 32 , UINT32_C ( 1 ));
( args )[ 1 ] = MZ_INT ( U , 32 , UINT32_C ( 1 ));
op_magic ( args );
});
( args )[ 1 ] = var_n ;
op_getIt ( args );
});
}
static mz_Value op_magic ( mz_ArgsPtr args ) {
mz_Value var_m = ( args )[ 0 ];
mz_Value var_n = ( args )[ 1 ];
return ({
struct mz_value tmp = MZ_OP2 ( var_m , equal , MZ_INT ( U , 32 , UINT32_C ( 0 )));
switch (( tmp ). tag ) {
case op_T : {
tmp = MZ_EMPTY_DATA ( op_Nil );
break ;
}
case op_F : {
tmp = MZ_DATA ( op_Cons , 2 , MZ_SIMPLE_THUNK ( var_m ), MZ_THUNK ( thunk_0 , 2 , var_m , var_n ));
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
}
static mz_Value op_getIt ( mz_ArgsPtr args ) {
mz_Value var_xs = ( args )[ 0 ];
mz_Value var_n = ( args )[ 1 ];
return ({
struct mz_value tmp = var_xs ;
switch (( tmp ). tag ) {
case op_Nil : {
tmp = mz_panic ( MZ_STRING ( "undefined" ));
break ;
}
case op_Cons : {
mz_Value var_x = (( tmp ). payload )[ 0 ];
mz_Value var_xs$ = (( tmp ). payload )[ 1 ];
tmp = ({
struct mz_value tmp = MZ_OP2 ( var_n , equal , MZ_INT ( U , 64 , UINT64_C ( 1 )));
switch (( tmp ). tag ) {
case op_T : {
tmp = mz_force ( var_x );
break ;
}
case op_F : {
tmp = ({
struct mz_value args [ 2 ];
( args )[ 0 ] = mz_force ( var_xs$ );
( args )[ 1 ] = MZ_OP2 ( var_n , sub , MZ_INT ( U , 64 , UINT64_C ( 1 )));
op_getIt ( args );
});
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
break ;
}
default : MZ_UNEXPECTED_TAG (( tmp ). tag );
}
tmp ;
});
}
extern mz_Value fib ( mz_Value var_n ) {
return MZ_CALL_MAIN ( var_n );
} translate 명령에는 번역의 대상 언어 인 --language 와 main 함수에 해당하는 외부 기호의 이름 인 --entry 가 모두 필요합니다. 입력 mazeppa 프로그램은 stdin ( cat main.mz 예제)에서 나옵니다. 출력 GNU11 프로그램은 stdout 에 기록됩니다.
더 나아가서 출력 프로그램을 객체 파일로 컴파일하겠습니다. 먼저 c/deps/sds.c , c/deps/sds.h 및 c/deps/sdsalloc.h 현재 디렉토리로 복사하십시오. 둘째, 컴퓨터에 Boehm GC를 설치하십시오.
$ sudo apt install libgc-dev -y
그런 다음 다음 명령을 실행합니다.
$ cat main.mz
| mazeppa translate --language C --entry fib --dump-header-to .
| gcc -c -o program.o -std=gnu11 -xc -
--dump-header-to 옵션은 mazeppa.h 의 내용을 지정된 위치에 씁니다. 출력 프로그램이 컴파일하는 데 필요합니다. gcc 명령은 stdin 에서 출력 프로그램을 수락하고 program.o 생성합니다.
이제 남은 것은 생성 된 fib 함수를 실제로 호출하는 것입니다. 다음 내용으로 main.c 만듭니다.
#include "mazeppa.h"
mz_Value fib ( mz_Value n );
int main ( void ) {
// Always initialize Boehm GC before invoking Mazeppa code.
GC_INIT ();
mz_Value v = fib ( MZ_INT ( U , 64 , 10 ));
printf ( "fib(10) = %" PRIu32 "n" , MZ_GET ( U32 , v ));
} 이 "드라이버"프로그램은 Mazeppa Integer ( MZ_INT )로 fib 호출하고 결과를 인쇄합니다. mz_priv_ 또는 MZ_PRIV_ 로 접두사가없는 경우 mazeppa.h 의 모든 기능을 사용할 수 있습니다.
모든 조각을 모으기 위해 :
$ gcc main.c program.o sds.c -lgc -std=gnu11
./a.out fib(10) = 55 인쇄하고 예상대로 종료합니다.
--inspect 실제 환경에서 변하는 : 디버깅 목적으로 만 사용하십시오.@extract (위 그림과 같이)를 사용하여 슈퍼 컴파일을 계속할 것인지 또는 레덱스를 추출할지 제어하십시오."otus" 는 "octopus" 보다 작지만 "octopusx" 그렇지 않습니다. Mazeppa는 몇 가지 흥미로운 디자인 선택을 사용합니다 (중요도별로 순위) :
1 차 코드. Max Bolingbroke와 Simon Peyton Jones 15는 한 가지 특별한 예에 대해 Haskell의 하위 집합에 대한 고차 슈퍼 컴퓨터가 이름을 관리하고 이름을 바꾸는 데 실행 시간의 42%를 소비했다고보고했습니다. Lambda 용어의 정규화와 같은 단순한 평가 모델이 캡처 회피의 상당한 오버 헤드를 피할 수 있도록 허용하는 것은 사실이지만, 슈퍼 컴파일은 더 복잡합니다. 예를 들어, 상징적 계산을 수행하는 것 외에도, SuperCompilation은 이전에 계산 된 결과를 분석하여 추가 변환에 대한 정보에 근거한 결정을 내려야합니다. 용어 인스턴스 테스트, 동종 모피 임베딩 테스트, 대부분의 구체적인 일반화 등을 고려하는 등의 고차 기능을 도입하면 불가피하게 이러한 모든 분석을 복잡하게 만들어 슈퍼 컴퓨팅 속도를 높이고 더 많은 메모리가 필요합니다. Mazeppa에서 우리는 점진적인 개선의 철학을 고수합니다. 동시에 많은 멋진 기능을 처리하려고 시도하는 대신 1) 기계에 의한 편리한 조작을 위해 핵심 언어를 수정, 2) 핵심 언어를 인간에게 더 나은 핵심 언어로 만들기 위해 필요한만큼 많은 메타지 전환을 수행합니다.
게으른 생성자. 콜 별 언어가 적절한 삼림 벌채에 어렵다는 것은 잘 알려진 관찰입니다. 비틀기는 여전히 가능하지만 추가 분석이 없을 수는 없습니다. 4 5 . 그러나 생성자가 게으른 경우 (즉, 그들의 주장을 평가하지 않으면) 삼림 벌채는 단지 작동합니다 . Turchin은 콜 별 언어의 정상 주문 변환으로 작동했지만 결과는 잔여 코드가 더 자주 종료 될 수 있습니다. Mazeppa에는 Call-value 함수와 콜 별 (Call-by-need) 생성자가 있으며, 이는 1) 삼림 벌채를 가능하게하고 2) 코드의 원래 의미를 보존합니다.
용어없는 프로세스 그래프. Mazeppa에서 프로세스 그래프에는 용어에 대한 참조가 포함되어 있지 않습니다. 잔류화는 그들없이 작동 할 수 있습니다. 결과적으로 쓰레기 수집기는 하위 그래프를 구성하는 동안 사용 된 용어를 처리 할 수 있습니다. 또한,이 정책에는 다음과 같은 몇 가지 중요한 이점이 있습니다. 1) 그래프는 여전히 --inspect 검사 하기 위해 존재합니다. 기존의 몇몇 슈퍼 컴퓨터는 적절한 프로세스 그래프 (예 : Neil Mitchell 's Supero 17 및 앞서 언급 한 15 )를 삼가지만 결과적으로 1) 사용자의 검사가 덜 가능합니다. 2) 알고리즘은 코드 생성 세부 사항으로 혼란스러워집니다.
2 차원 구성 분석. 일반적으로 SuperCompiler는 노드를 변환하면서 모든 조상의 하위 집합의 "역사"를 유지합니다. 이 노드가 조상 중 한 명과 "충분히"라면 종료를 보장하기 위해이 용어를 작은 부분으로 나누어야합니다. Mazeppa에서는 대신 두 개의 별도의 데이터 구조를 보관합니다. 노드 조상의 하위 집합을 포함하는 것과 완전히 변환 된 노드의 서브 세트를 포함하는 것입니다. 이전 데이터 구조는 종료를 보장하는 데 사용되는 반면 (평소와 같이) 후자는 잔류 코드에서 함수 공유를 향상시키는 데 사용됩니다. 구체적으로, 전류 노드 (특별한 종류)가 이전에 변환 된 일부 노드의 이름을 바꾸는 경우 현재 노드를 이전 노드로 접습니다. 이런 식으로 Mazeppa는 구성의 수직 및 수평 분석을 수행하여 잔류 코드를보다 작고 슈퍼 컴파일을보다 효율적으로 만듭니다.
기능 생산성 분석. 내부 함수가 패턴 일치를 알 수없는 값으로 호출 할 때, 잠재적으로 위험한 두 가지 일이 발생합니다. 1) Super Compilation은 패턴 매칭 함수의 구조를 재현합니다. 더 이상의 통제력이 없으면,이 상황은 코드 크기의 상당한 폭발로 이어질 수 있으며, 때로는 슈퍼 컴퓨터가 합리적인 시간 안에 종료되지 않도록합니다. 개선하기 위해 Mazeppa는 컨텍스트를 복제합니다.이 내부 호출은 적어도 하나의 종료 지점에서 명확한 최상위 값을 생성합니다. 왜냐하면,이 값은 후속 패턴 매칭으로 인해이 값을 해체 할 수 있기 때문입니다. 그렇지 않으면, Mazeppa는 내부 호출을 추출하여 @extract 로 표시된 것처럼 분리하여 변환합니다. 또한 컨텍스트가 실제로 복제 된 경우 다음 규칙은 모든 분기에 적용됩니다. 분기가 모든 종료 지점에서 명확한 최상위 값을 생성하면 평소와 같이 컨텍스트에서 변환됩니다. 그렇지 않으면, 분기는 컨텍스트에서 추출되어 분리되어 변형됩니다. 실제로,이 분석은 엄청난 양의 불필요한 전문화를 방지하여 잔류 프로그램 크기를 압축하고 초과 컴파일이 훨씬 더 큰 영향을 미칩니다.
똑똑한 역사. 전류 노드를 모든 조상과 맹목적으로 비교하는 대신, 우리는보다 세밀한 제어를 사용합니다. 1) 글로벌 노드 (알 수없는 변수를 분석하는 것)는 글로벌 노드 만 비교됩니다. 2) 로컬 노드 (단일 단계에서 선형 적으로 감소하는 노드)는 최신 노드 와만 비교되는 것과 비교됩니다. 또 다른. 종료 점검에 대한보다 경제적 인 접근 외에도이 체계는 Mazeppa가 더 많은 최적화 기회를 발견 할 수 있도록합니다. 18 , 섹션 4.6 및 4.7을 참조하십시오. 슈퍼 컴파일의 종료는 동종 모피 임베딩이 여전히 전 세계 및 로컬 용어의 모든 무한한 후속에서 테스트된다는 사실에 의해 보장됩니다 (사소한 용어의 무한한 순서 만 존재할 수는 없습니다).
레덱 서명. 호루라기는 동일한 레덱 시그니처가 있는 용어로만 테스트됩니다. Redex 서명은 1) 함수의 기호와 2) 인수 값 범주 목록입니다. 값 범주 +(x, x) 인수에 대한 일종의 메타 VConst 형식이며, 1) 42i32 또는 "hello world" Foo(...) 같은 x 에 대해 VNeutral 일 수 있습니다 VCCall(c) 휘파람은 여전히 잠재적으로 무한한 모든 용어 시퀀스에서 테스트됩니다. 무한 시퀀스는 동일한 레덱 시그니처와 적어도 하나의 무한 하속 시퀀스를 포함해야하기 때문입니다. 이 전략은 다음 두 가지 예에서 알 수 있듯이 Mazeppa는 특정한 경우 과도한 일반화를 피할 수 있습니다.
f(A()) f(g(B(A()))) 에 항상 내장되어 있습니다. 그러나 Redex 운영자는 다르기 때문에 ( f 및 g ) Mazeppa는 계속 감소하고 이상적인 결과에 도달합니다.f(A(Good())) 가 f(f(f(B(A(Good()))))) 에 포함되어 있지만 레덱 연산자는 두 경우 모두 Mazeppa가 레덱스 서명에서 f 값 범주를 가지고 있기 때문에 과도하게 일반화되지 않습니다. 첫 번째 경우 A(...) 에서 호출되는 반면, f B(...) . 이전 예와 마찬가지로 Mazeppa는 감소에 의해서만 슈퍼 컴파일의 이상적인 결과에 도달합니다.최적화 된 동종 이성 임베딩. 수십 년 동안, 동종 형성 임베딩은 온라인 종료 확인을위한 훌륭한 방법으로 명성을 얻었습니다 . 불행히도, 주로 비선형 제어 흐름 (다이빙 및 커플 링이 모두 적용될 때)으로 인해 계산 비용이 많이 들지 않을 수 있습니다. 더 나쁜 것은 새로운 용어가 역사에 추가 될 때마다 모든 자격을 갖춘 부모 노드에 대해 다시 실행됩니다. 이는 역사가 성장함에 따라 점차적으로 슈퍼 컴파일을 느리게합니다. 대부분의 수퍼 컴파일 시간을 먹는 한! 이에 대처하기 위해 두 개의 별도 캐시를 유지합니다.
해시 컨소싱. 위에서 설명한 동종 모피 임베딩 캐시는 공유되는 용어의 수에 따라 다릅니다. 따라서 우리는 기능 본문을 전개하는 동안 해시 컨소싱을 사용합니다. 일부 새로운 용어 T가 기존 용어 와 구조적으로 동일하면 후자는 재사용됩니다. 메모리 누출을 피하기 위해 우리는 약한 포인터를 보유한 글로벌 Ephemeron을 사용합니다. Hash Consing은 메모리 소비를 줄인 슈퍼 컴파일 시간 (메모 화로 인해)이 개선 된 것 외에도 #4 (댓글)를 참조하십시오.
전개 동안 정규화. 함수 호출이 전개되면 매개 변수를 대체하고 신체를 가능한 한 많이 정상화합니다 (즉, 추가 전개없이 종료를 보장합니다). 이유를 확인하려면 Factorial 함수 f(n) 고려하십시오. 간단한 전개를 통해 우리는 f(1u32) *(1u32, f(-(1u32, 1u32))) 에 포함되어 과도한 일반화를 유발하는 불쾌한 상황에서 덫을 놓을 것입니다. 실제로, Mazeppa는 f(1u32) 로 *(1u32, f(0u32)) 로 전개되어 후자는 추가 전개의 후보가됩니다. 이 접근법은 20 장 , 4.5 절에 제안되었습니다. 다른 장점은 다음과 같습니다. 1) 미래의 운전 단계에 대한 작업 감소, 2) 프로세스 그래프의 "평범한"계산, 3) 값 비싼 동종 임베드 테스트의 양이 줄어 듭니다.
*(1u32, f(-(1u32, 1u32))) 다른 Redex 연산자로 인해 더 이상 f(1u32) 에 대해 확인되지 않습니다. 그러나 정규화의 다른 장점은 여전히 유지됩니다.OCAML에서 구현. Mazeppa는 OCAML에서 수행하기에 매우 자연스러운 기능 및 명령 프로그래밍 스타일의 조합을 사용하여 구현됩니다. 예외는 "예외적 인"상황에만 사용되며 내부 기능 내부의 돌연변이가 일반적입니다. 우리는 예를 들어 Haskell이나 Rust에 비교하여 쓰여진 비슷한 슈퍼 컴퓨터를 가지고 있지는 않지만, 언어와 싸움을하지 않고 작업을 끝내지 않고 작업 구현을 제공 한 것은 OCAML이라고 생각합니다.
위의 대부분은 특별히 새로운 것이 아니지만, 우리는 이러한 기능의 조합으로 인해 Mazeppa가 이전 모델보다 더 실용적인 대안이라고 생각합니다.
A symbol <SYMBOL> is a sequence of letters ( a , ... , z and A , ... , Z ) and digits ( 0 , ... , 9 ), followed by an optional question mark ( ? ), followed by an optional sequence of ' characters. The underscore character ( _ ) may be the first character of a symbol, which may informally indicate that the value or function being defined is not used; otherwise, the first character must be a letter. The following sequences of characters are also permitted as symbols: ~ , # , + , - , * , / , % , | , & , ^ , << , >> , = , != , > , >= , < , <= , ++ . The following are reserved words that may not be used as symbols: match , let .
There are four classes of unsigned integer constants :
0b ( 0B ) followed by a non-empty sequence of binary digits 0 and 1 .0o ( 0O ) followed by a non-empty sequence of octal digits 0 , ... , 7 .0 , ... , 9 .0x ( 0X ) followed by a non-empty sequence of decimal digits 0 , ... , 9 and letters a , ... , f ( A , ... , F ).Notes:
_ ) except for the first position in the sequence of digits.- ) placed right before the sequence of digits and underscore characters.<INT> produced by appending an integer type <INT-TY> ( u8 , u16 , u32 , u64 , u128 , i8 , i16 , i32 , i64 , i128 ) right after the original integer constant. For example, the constants 123i8 , 123u16 , and 123i32 all belong to the set <INT> . A string constant <STRING> is a sequence, between double quotes ( " ), of zero or more printable characters (we refer to printable characters as those numbered 33-126 in the ASCII character set), spaces, or string escape sequences :
| Escape sequence | 의미 |
|---|---|
f | Form feed (ASCII 12) |
n | Line feed (ASCII 10) |
r | Carriage return (ASCII 13) |
t | Horizontal tab (ASCII 9) |
v | Vertical tab (ASCII 11) |
xhh | ASCII code in hexadecimal |
" | " |
\ | |
where h is either 0 , ... , 9 or a , ... , f or A , ... , F .
A character constant <CHAR> is either a sole character enclosed in single quotes ( ' ) or a character escape sequence enclosed in single quotes. The character escape sequence is the same as for strings, except that " is replaced by ' .
There are no other constants in Mazeppa.
A comment <COMMENT> is any sequence of characters after // , which is terminated by a newline character. (We only allow single-line comments for simplicity.)
The entry point <program> is defined by the following rules:
<def-attr-list> <SYMBOL> ( <SYMBOL> , ... , <SYMBOL> ) := <term> ; <program><COMMENT> <program> where <def-attr-list> is a whitespace-separated sequence of function attributes (the same attribute can occur multiple times). Right now, the only allowed function attribute is @extract .
<term> is defined as follows:
<SYMBOL> (a variable)<const> (a constant)<SYMBOL> ( <term> , ... , <term> ) (a function call)match <term> { <match-case> , ... , <match-case> } (pattern matching)let <SYMBOL> := <term> ; <term> (a let-binding)let <pattern> := <term> ; <term> (a pattern let-binding)<COMMENT> <term> (a comment)The rest of the auxiliary rules are:
<const> :
<INT> or <STRING> or <CHAR> . <match-case> :
<pattern> -> <term> <pattern> :
<SYMBOL> ( <SYMBOL> , ... , <SYMBOL> ) . In Mazeppa, primitive operations employ the same syntax as that of ordinary function calls. To distinguish between the two, we define <op1> and <op2> to be the following sets of symbols:
<op1> is one of ~ , # , length , string , <INT-TY> .<op2> is one of + , - , * , / , % , | , & , ^ , << , >> , = , != , > , >= , < , <= , ++ , get . Furthermore, <op2> has the following subclasses:
<arith-op2> is one of + , - , * , / , % , | , & , ^ , << , >> .<cmp-op2> is one of = , != , > , >= , < , <= .<op1> or <op2> . 2) A function must define a symbol starting with a lowercase letter. 3) No duplicate symbols can occur among function parameters. 4) Every free variable inside a function body must be bound by a corresponding parameter in the function definition.match { ... } must not be empty. 2) No duplicate constructors can occur among case patterns in match { ... } . 3) No duplicate symbols can occur among pattern parameters C(x1, ..., xN) . 4) No let-binding can bind <op1> or <op2> . 5) Panic must be called with only one argument; T and F with zero arguments.If a program, function, or term conforms to these restrictions, we call it well-formed .
| 원형 | Desugared form | 메모 |
|---|---|---|
// ... rest | rest | rest is in <program> or <term> |
let p := t; u | match t { p -> u } | p is in <pattern> |
c | ASCII(c) | c is in <CHAR> |
where ASCII(c) is an appropriate u8 integer constant, according to the ASCII table; for example, ASCII( 'a' ) is 97u8 .
Suppose that t is a well-formed term closed under environment env (defined below) and program is a well-formed program. Then the evaluation of t is governed by the following big-step environment machine:
eval(env, x) = eval({ }, env(x))eval(env, const) = const , where const is in <const> .eval(env, f(t1, ..., tN)) =t1Val ^= eval(env, t1)tNVal ^= eval(env, tN)eval({ x1 -> t1Val, ..., xN -> tNVal }, body) , where f(x1, ..., xN) := body; is in program .eval(env, C(t1, ..., tN)) = C(t1[env], ..., tN[env]) , where C starts with an uppercase letter.eval(env, op(t)) =tVal ^= eval(env, t)evalOp1(op, tVal) , where op is in <op1> .eval(env, op(t1, t2)) =t1Val ^= eval(env, t1)t2Val ^= eval(env, t2)evalOp2(t1Val, op, t2Val) , where op is in <op2> .eval(env, match t { p1 -> t1, ..., pN -> tN }) =Ci(s1, ..., sN) ^= eval(env, t)eval(env', tI) , whereCi(x1, ..., xN) -> tI is among the rules in match t { ... } , andenv' is env[x1 -> s1, ..., xN -> sN] .eval(env, let x := t; u) =tVal ^= eval(env, t)eval(env[x -> tVal], u)표기법:
env is a total environment over t , whose general form is { x1 -> t1, ..., xN -> tN } . Each tI term must be closed and well-formed; this property is preserved by eval .env(x) is tI , where x -> tI is in env .env[x1 -> t1, ..., xN -> tN] is the environment env extended with new bindings x1 -> t1 , ... , xN -> tN . If some xI is already bound in env , it is rebound.t[env] denotes a simultaneous substitution of all free variables in t by their bound values in env .tVal ^= eval(env, t) evaluates t under env ; 그 다음에:Panic(t') , the result of the whole evaluation rule is Panic(t') .tVal is available for the next clauses. (Note that eval is a partial function, so evaluation of t can "get stuck" without a superimposed type system.)
In what follows, 1) signed integers are represented in two's complement notation, 2) panic denotes Panic(s) , where s is some (possibly varying) implementation-defined string constant.
evalOp1 takes care of the unary operators for primitive types ( x is in <INT> , s is in <STRING> ):
evalOp1(~, x) is the bitwise negation of x of the same type.evalOp1(string, x) is the string representation of x (in decimal).evalOp1(ty, x) , where ty is in <INT-TY> , is x converted to an integer of type ty .x is not in the range of ty , the result is panic .evalOp1(#, x) , where x is a u8 integer, is a string containing only the ASCII character of x .x is not printable, the result takes the form "xhh" .evalOp1(length, s) is a u64 integer denoting the length of s .evalOp1(string, s) is s . Likewise, evalOp2 takes care of the binary operators for primitive types:
evalOp2(x, op, y) , where x and y have the same integer type and op is in <arith-op2> , performs a corresponding arithmetic operation on x and y , yielding a value of the same type as that of x and y .evalOp2(x, op, y) , where x and y have the same integer type and op is in <cmp-op2> , performs a corresponding comparison operation on x and y , yielding either T() or F() .evalOp2(s1, op, s2) , where s1 and s2 are strings and op is in <cmp-op2> , performs a corresponding lexicographical comparison on s1 and s2 , yielding either T() or F() .evalOp2(s1, ++, s2) is the concatenation of s1 and s2 .evalOp2(s, get, idx) , where idx is a u64 integer, is the idx -th character (of type u8 ) of s .idx is out of bounds, the result is panic . The definition of eval is now complete.
version field in dune-project and bin/main.ml .dune build to generate mazeppa.opam .CHANGELOG.md .Not yet, we need to battle-test Mazeppa on some actual programming language. Our long-term goal is to find suitable heuristics to profitably supercompile any source file under 10'000 LoC (in Mazeppa).
For debugging and other purposes, we provide a built-in definitional interpreter that can execute Mazeppa programs. You can launch it by typing mazeppa eval (make sure that your main function does not accept parameters). For the purpose of real execution, we recommend translating Mazeppa to C and then compiling C to machine code, as shown above.
Since Mazeppa is a purely functional language, the only way to implement I/O is as in Haskell 23 : having a pure program that performs computation and a dirty runtime that performs side effects issued by the program. There are no plans to introduce direct I/O into Mazeppa: it will only make everything more complicated.
No, we do not think that a type system is necessary at this point. It is the responsibility of a front-end compiler to ensure that programs do not "go wrong".
The more we make supercompilation predictable, the less it is capable of theorem proving. For those interested in program analysis rather than optimization, we suggest looking into distillation 24 .
For the English audience, the following paper presents a decent introduction into supercompilation:
However, the following papers in Russian describe a supercompilation model that is closer the majority of existing supercompilers, including Mazeppa:
Mazeppa itself is inspired by this excellent paper (in English):
Finally, the international META workshops are great collections of articles about supercompilation and adjacent fields:
Several approaches can lead to superlinear speedup of non-esoteric programs by supercompilation:
None of the above is planned to be implemented in Mazeppa, because 1) we think that writing asymptotically good programs is the responsibility of the programmer, not the optimizer, and 2) predictability of supercompilation is of greater importance to us. However, for those who are interested in this topic, the references may be helpful.
Just fork the repository, work in your own branch, and submit a pull request. Prefer rebasing when introducing changes to keep the commit history as clean as possible.
Valentin F. Turchin. 1986. The concept of a supercompiler. ACM Trans. 프로그램. Lang. Syst. 8, 3 (July 1986), 292–325. https://doi.org/10.1145/5956.5957 ↩ ↩ 2
Philip Wadler. 1988. Deforestation: transforming programs to eliminate trees. Theor. 컴퓨터. 공상 과학. 73, 2 (June 22, 1990), 231–248. https://doi.org/10.1016/0304-3975(90)90147-A ↩ ↩ 2
Futamura, Y. (1983). Partial computation of programs. In: Goto, E., Furukawa, K., Nakajima, R., Nakata, I., Yonezawa, A. (eds) RIMS Symposia on Software Science and Engineering. Lecture Notes in Computer Science, vol 147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11980-9_13 ↩
Peter A. Jonsson and Johan Nordlander. 2009. Positive supercompilation for a higher order call-by-value language. SIGPLAN Not. 44, 1 (January 2009), 277–288. https://doi.org/10.1145/1594834.1480916 ↩ ↩ 2
Jonsson, Peter & Nordlander, Johan. (2010). Strengthening supercompilation for call-by-value languages. ↩ ↩ 2
DE Knuth, JH Morris, and VR Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6:page 323 (1977). ↩
Glück, R., Klimov, AV (1993). Occam's razor in metacomputation: the notion of a perfect process tree. In: Cousot, P., Falaschi, M., Filé, G., Rauzy, A. (eds) Static Analysis. WSA 1993. Lecture Notes in Computer Science, vol 724. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57264-3_34 ↩
Sørensen MH, Glück R, Jones ND. A positive supercompiler. Journal of Functional Programming. 1996;6(6):811-838. doi:10.1017/S0956796800002008 ↩
Consel, Charles, and Olivier Danvy. "Partial evaluation of pattern matching in strings." Information Processing Letters 30.2 (1989): 79-86. ↩
Jones, Neil & Gomard, Carsten & Sestoft, Peter. (1993). Partial Evaluation and Automatic Program Generation. ↩
Turchin, VF (1996). Metacomputation: Metasystem transitions plus supercompilation. In: Danvy, O., Glück, R., Thiemann, P. (eds) Partial Evaluation. Lecture Notes in Computer Science, vol 1110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61580-6_24 ↩
Turchin, Valentin F. "Program transformation with metasystem transitions." Journal of Functional Programming 3.3 (1993): 283-313. ↩
Turchin, Valentin F.. “A dialogue on Metasystem transition.” World Futures 45 (1995): 5-57. ↩
Turchin, V., and A. Nemytykh. Metavariables: Their implementation and use in Program Transformation. CCNY Technical Report CSc TR-95-012, 1995. ↩
Maximilian Bolingbroke and Simon Peyton Jones. 2010. Supercompilation by evaluation. In Proceedings of the third ACM Haskell symposium on Haskell (Haskell '10). Association for Computing Machinery, New York, NY, USA, 135–146. https://doi.org/10.1145/1863523.1863540 ↩ ↩ 2
Friedman, Daniel P. and David S. Wise. “CONS Should Not Evaluate its Arguments.” International Colloquium on Automata, Languages and Programming (1976). ↩
Mitchell, Neil. “Rethinking supercompilation.” ACM SIGPLAN International Conference on Functional Programming (2010). ↩
Sørensen, MHB (1998). Convergence of program transformers in the metric space of trees. In: Jeuring, J. (eds) Mathematics of Program Construction. MPC 1998. Lecture Notes in Computer Science, vol 1422. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054297 ↩
Leuschel, Michael. "Homeomorphic embedding for online termination of symbolic methods." The essence of computation: complexity, analysis, transformation (2002): 379-403. ↩
Jonsson, Peter & Nordlander, Johan. (2011). Taming code explosion in supercompilation. PERM'11 - Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. 33-42. 10.1145/1929501.1929507. ↩ ↩ 2
Tejiščák, Matúš. Erasure in dependently typed programming. Diss. University of St Andrews, 2020. ↩
Glück, Robert, Andrei Klimov, and Antonina Nepeivoda. "Nonlinear Configurations for Superlinear Speedup by Supercompilation." Fifth International Valentin Turchin Workshop on Metacomputation. 2016. ↩
Peyton Jones, Simon. (2002). Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. ↩
GW Hamilton. 2006. Poitín: Distilling Theorems From Conjectures. 전자. Notes Theor. 컴퓨터. 공상 과학. 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. ↩
