「コンパイラ」 講義資料 - 東北大学電気通信研究所 大堀研究室

講義の目的
.
.
..
.
東北大学 電気・情報系「コンパイラ」 講義資料
.
.
講義の概要
大堀 淳
東北大学 電気通信研究所
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
1 / 230
講義の概要
講義の目的
序論 (特に,講義を聴講せずに本スライドを参考にされる方へ) I
本講義を聴講する者や本スライドを参考にする者の大部分は,実際にコ
ンパイラを書く必用も機会もないと思われる.しかしにも拘らず,
「コン
パイラ」は,主に以下の2つの理由から,それらの人々を含む計算機科
学を学ぶすべての人にとって重要な,計算機科学のカリキュラムの中心
をなす科目の一つである.
...
...
1
計算の記述とその計算機での実現は,情報処理の基礎である.
2
コンパイル技術の確立の研究の過程には,計算機科学の典型的なア
イデアや考え方が豊富に含まれている.
これらを技術が構築される過程を追体験しそれらアイデアと原理を理解
することは,将来の斬新な情報処理システム構築にとって本質的で重要
な示唆を与えると考える.
本講義では,
「コンパイラ」の科目のこれら役割を念頭におき,コンパイ
ラの基本概念および基本原理,さらにそれらの基礎となったアイデアの
理解を主な目的とした講義設計を試みる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
2 / 230
講義の概要
講義の目的
序論 (特に,講義を聴講せずに本スライドを参考にされる方へ) II
これら基本概念や原理,さらにそれらが基礎とする本質的な洞察やアイ
デアは,種々のコンパイラの教科書では必ずしもきちんと扱われていな
いことが多いようにおもわれる.
一例としてコンパイラの主要技術である「LR 構文解析」を取り上げてみ
よう.この技術は,Knuth による画期的でしかも(多くの優れたアイデア
がそうであるように)単純な以下の2つのアイデアを基礎としている.
...
最右導出の(最後の)一ステップは,オートマトンを使い再構築で
きる.従って,オートマトンを繰り返し使うことにより,
(ある範囲
の)文脈自由文法を解析できる.
...
過去のオートマトンの状態遷移をスタックに記録することにより,
オートマトンによる繰り返しスキャンのオーバヘッドを抑止できる.
1
2
このアイデアと原理の理解は,
(一般に複雑で難解と受け取られている)
LR 構文解析アルゴリズムの理解を見通しのよいものにするばかりでな
く,計算機科学における問題解決の典型を追体験する上でも貴重である.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
3 / 230
講義の概要
講義の目的
序論 (特に,講義を聴講せずに本スライドを参考にされる方へ) III
しかし残念ながら,
(コンパイル技術の詳細の解説を目的とした)既存の
コンパイラの教科書では,例えばこの基本的な原理その基礎となるアイ
デアなどが極めて分かりにくい構成になっているように思われる.
そこで,本講義では,コンパイラの細な実装技術の紹介に重きを置くの
ではなく,これら基本原理や基礎となるアイデアを理解することに目標
とし,以下の内容を扱う予定である.
プログラミング言語と計算機の基本構造,コンパイラの役割
語彙の定義と解析原理
構文構造の定義と LR 構文解析の原理
型(文脈依存のプログラム構造)の定義と解析
種々の言語機能の翻訳
意味の定義と変換
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
4 / 230
講義の概要
講義の目的
序論 (特に,講義を聴講せずに本スライドを参考にされる方へ) IV
これら原理を理解した上で,さらにコンパイラやプログラミング言語処
理系に関してより深い理解を得たいと思う者のために,我々が実際に開
発を行っている実用を目指した次世代関数型言語 SML#のコンパイラ
http://www.pllab.riec.tohoku.ac.jp/smlsharp/ja/
を例に具体的なコンパイルの内部構造の紹介や,SML#コンパイラから抽
出した各コンパイルステップのスケルトンの提供などをも行っていく予
定である.
本講義や本資料に関する質問やコメントを歓迎します.直接著者まで電子
メール等でお送り頂ければ幸です.なお,本資料は随時改訂いたします.
東北大学電気通信研究所 大堀 淳
本資料は授業に合わせて作成途上です.ミスや誤植等お知らせください.
更新日:2015 年 10 月 1 日
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
5 / 230
講義の概要
講義の目的
内容
.
. .1 講義の概要
.
. .2 言語処理系の原理と構造
.
. .3 高水準言語の役割
.
. .4 字句解析
.
. .5 構文解析
.
. .6 型の解析と型推論
.
. .7 コンパイラバックエンド
.
. .8 現実のコンパイラ
.
. .9 要点の復習
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
6 / 230
講義の概要
講義に関する情報
講義に関する情報
日時:木曜 2次限(10:30 – 12:00) (電気系 1 号館 1A)
講師:大堀 淳,電気通信研究所 教授,ソフトウエア構成研究分野
専門:
プログラミング言語(基礎理論,処理系,新しい言語の実現)
データベース(言語とデータベースの統合,データモデル理論)
メールアドレス:ohori at riec dot tohoku dot ac dot jp
URL(大堀研究室)
:http://www.pllab.riec.tohoku.ac.jp/
URL(大堀)
:http://www.riec.tohoku.ac.jp/˜ohori/
次世代高信頼プログラミング言語 SML#のコンパイラ開発中.
http://www.pllab.riec.tohoku.ac.jp/smlsharp/ja/
評価:(主に)期末テスト + 宿題
講義資料(本スライド等)のページ
(研究室の URL)/education/lectures/compiler.html
「大堀研究室」=⇒ 「教育」=⇒ 「講義関連資料(lecture notes)」
=⇒ 「コンパイラ」 とたどる
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
7 / 230
講義の概要
講義予定
講義予定
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
日時
10 月 1 日
10 月 8 日
10 月 15 日
10 月 22 日
10 月 29 日
11 月 5 日
11 月 12 日
11 月 19 日
11 月 26 日
12 月 3 日
12 月 10 日
12 月 17 日
12 月 24 日
1月7日
1 月 14 日
1 月 21 日
内容(予定)
コンパイラの役割と構造,
字句解析(1)
:正規言語を用いた語彙の表現
高水準言語 ML の紹介,プログラミング演習
字句解析(2)
:有限状態機械による字句解析
構文解析(1)
:文脈自由文法を用いた言語の表現
構文解析(2)
:LR 構文解析の原理(1)
構文解析(3)
:LR 構文解析の原理(2)
構文解析(4)
:LR 構文解析プログラミング
静的解析(1)
:型の解析と型推論
静的解析(2)
:型の解析と型推論
種々の言語機能の実現
意味解析(1)
:操作的意味論と関数の表現
意味解析(2)
:スタックマシントコード生成
最先端言語の実現
講義のまとめと試験
予備
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
8 / 230
言語処理系の原理と構造
計算機の行う計算の表現
講義内容
.
. .2 言語処理系の原理と構造
計算機の行う計算の表現
計算の概念の厳密な定義
補足:シンボルを用いた情報の表現
コンピュータの万能性
高機能計算機と高水準プログラミング言語
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
9 / 230
言語処理系の原理と構造
計算機の行う計算の表現
計算機の行う計算の表現
プログラミング言語の形式的定義:
「計算機」が行う「計算」を表現する言語
「計算機」行う「計算」の一般的な定義:
記号を用いた情報の表現,解釈,変換一般
この「定義」に対する疑問:
情報の表現,解釈,変換とは何か.
情報を処理する計算機など厳密に定義できるのか.
もしできたとして,どのような計算機を定義すればよいのか.
計算機によって種々の能力や限界の違いがあるのではないか.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
10 / 230
言語処理系の原理と構造
計算の概念の厳密な定義
計算の概念の厳密な定義
Turing による「計算」の構造の分析:
有限のシンボル集合を用いる
種々の情報や処理手順をシンボル列で表現する
シンボル列を格納する記憶装置を使用し,
シンボルの読込み,
別のシンボルへの変換,
シンボルの書出
からなる処理を繰り返し,必用な情報を作り出す.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
11 / 230
言語処理系の原理と構造
補足:シンボルを用いた情報の表現
補足:シンボルを用いた情報の表現 I
総ての情報は記号の有限集合(アルファベット,Σ)を用いて表現可能
原則
どのようなアルファベットでもよい.
表現方法は一通りではない(無限に存在).
表現の約束を知っている者は,誰でも機械的に情報を取り出せる.
同様の原理:
Gödel 数:
「あらゆる命題は数で表現しうる」
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
12 / 230
言語処理系の原理と構造
コンピュータの万能性
汎用の計算機としてのデジタルコンピュータ
Turing による汎用の計算機 チューリング機械 M:
一ますづつ読み書きできる一次元の記憶テープ
制御機構
M = (Q, Σ, Γ, δ, q1 , F)
有限の状態集合
入力文字集合
記憶テープに書くシンボルの有限の集合
機械の動作を記述した表(関数:(p, s) 7→ (p′ , s′ , 右 or 左))
現在の状態 p と現在のヘッド位置のテープのシンボル s に対して,次
の状態 q′ を記述,テープに書き出すべきシンボル s′ ,書き出した後
のテープの移動方向(右,左).
q1 機械の初期状態の指定.
F 機械が計算を終了し停止する条件を表す最終状態集合.
Q
Σ
Γ
δ
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
13 / 230
言語処理系の原理と構造
コンピュータの万能性
デジタルコンピュータの能力
疑問:
このような単純な機械で十分だろうか?
高度な問題を解くためには,より高機能で複雑な機械を発明しなけ
ればならないのではないか?
Turing や Church の一連の研究による回答:
チューリング機械は,およそ計算可能ないかなる計算も実行するこ
とができる.
チューリング機械は,適当な動作表を用意すれば,離散的な状態を
もつ任意の機械を模倣できる.
これが,今日の情報処理の基本原理.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
14 / 230
言語処理系の原理と構造
コンピュータの万能性
デジタルコンピュータはすべて等価である
洞察:
デジタルコンピュータは,それ自身離散的な状態をもつ機械
すると基本原理から直ちに以下のことが帰結する.
任意のデジタルコンピュータは Turing 機械で模倣できる.
(ごく簡単な Turing 機械の機能を含む)任意のデジタルコンピュー
タは,他のデジタルコンピュータを模倣できる.
デジタルコンピュータの問題解決能力はすべて等価.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
15 / 230
言語処理系の原理と構造
コンピュータの万能性
プログラムによる他の計算機の模倣
M 上に M′ を模倣するプログラムを構築
M の記憶領域上に,M′ の制御部の記述と状態を情報として格納
入力データに対して,M′ の制御部の記述に従って,状態を変更
計算機 M による計算機 M′ の模倣を
M ≤ M′
と書く.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
16 / 230
言語処理系の原理と構造
コンピュータの万能性
高性能機械の実現戦略
洞察
模倣の対象は凡そ実現可能な総てのデジタルコンピュータ
これから導かれる高性能計算機の設計の枠組み
.. 望ましい機能をもつ仮想的なデジタルコンピュータ M を設計
1
.
実現不可能な機能を含まな無い限り,機能に制約はない.
.. すでに実現されている,あるいは明らかに実現可能な,デジタルコ
2
ンピュータ M0 を用意する.
.. M0 からはじめて,M に至る模倣の系列
3
.
.
M0 ≤ M1 ≤ · · · ≤ M
を実現.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
17 / 230
言語処理系の原理と構造
コンピュータの万能性
補足:実現可能な機能
ある機能が実現可能か不可能かの確認方法:
すでに実現されてている計算機上で,その機能を実現するプログラ
ムを構築.
その機能を実現する計算機は存在し得ないことを証明.
これには以下の2つの戦略がある.
直接証明する.
この機能を実現する機械がもしあれば,それを使って,すでに計算不
可能と証明されている機能が実現できてしまうことを示す.
何れの場合も証明は簡単ではない.
直感的に言えば,無限の情報を持つものの性質を計算するような機能は,
実現不可能である場合が多い.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
18 / 230
言語処理系の原理と構造
コンピュータの万能性
補足:模倣プログラム構築は機械の構築そのもの
上記の補足から以下のことが分かる.
模倣プログラムを実現する系統的な方法は存在しない.
高度な機能を模倣するプログラムの設計と実現は,高度なデジタル
コンピュータの設計と実現そのもの.
模倣プログラムの品質も,その作成者(プログラマ)によってそれ
ぞれに異なる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
19 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
コンピュータとプログラミング言語
デジタルコンピュータの構造はその記述言語で表現される.
チューリング機械
プログラム:
0 1 1 R 0
0 - 1 R 1
1 1 1 R 1
機械の構造
一次元のテープと読み取りヘッ
ドを持ち,テープの一ますの読
み書きとテープの左右への移動
のみを行う
レジスタマシン
プログラム:
mov eax, [esp+4]
add eax, [esp+8]
ret
大堀 淳 (東北大学 電気通信研究所)
機械の構造
ランダムアクセス可能なメモ
リー,高速レジスタ,種々の算
術演算ユニットなどを備えた
CPU 構造に対応.
コンパイラ講義資料
20 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
プログラミング言はすべて等価
前節の結果:
Turing 機械はレジスタ機械を模倣することができ,またレジス
タ機械は Turing 機械を模倣できる.
つまり,一方の言語で他方を実行するプログラムを実現できる.
前節の結果のプログラミング言語から見た言い換え:
プログラミング言語はすべて等価である.
プログラミング言語は,その言語で適当なプログラムを組みさえす
れば,他の任意のプログラミング言語を実現できる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
21 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
プログラミング言語開発の枠組み
...
問題解決に適した書きやすいプログラミング言語 L を設計する.
計算不可能な機能さえ含まな無い限り,特にその機能に制約はない.
...
...
2
実現されている(実現可能な)プログラミング言語 L0 を用意する.
3
L0 からはじめて,L に至る実現の系列
1
L0 ≤ L1 ≤ · · · ≤ L
を実現する.
この原理に従い,既存の言語を使って別の言語を実現するプロ
グラムが,プログラミング言語処理系.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
22 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
言語 L による L′ の実現 L ≤ L′ はどのように行うか? I
.
方式1:インタープリタ
.
.
.
..
′
.L を用いて L が動く機械を模倣するプログラム I を実現する
..
言語 L′ を実行する機械を実現するプログラム I を L′ のインタープ
リタと呼ぶ.
I は L′ が動くデジタル計算機そのものであるから,これによって任
意の L′ のプログラムが直ちに実行できる
L′ を解釈する機械は抽象的な概念.L′ の意味と考えてもよい.
この方式は,実現しようとする言語に対応する機械の定義に従ってプロ
グラムを書くだけでよく,比較的簡単に実現できる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
23 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
言語 L による L′ の実現 L ≤ L′ はどのように行うか? II
インタープリタによる言語の実現
L2を解釈する機械M2
L1を解釈する機械M1
L1で書いたL2解
釈プログラム
L1を解釈する機械M1
言語L1
大堀 淳 (東北大学 電気通信研究所)
≦
コンパイラ講義資料
言語L2
24 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
言語 L による L′ の実現 L ≤ L′ はどのように行うか? III
方式 2:コンパイラ
..
′
.L のプログラムを L のプログラムに変換するプログラム C を実現する
..
.
.
.
.
言語 L′ をべつな言語 L に変換するプログラム C を L′ のコンパイラ
と呼ぶ.
L が動くデジタル計算機があれば,任意の L′ のプログラムを実行で
きる
コンパイラ C はどの言語で実現されていてもよい.
一般に言語の翻訳は,言語の意味の解釈(interpreter)より複雑な作業で
あり,実現は難しいが,言語のより効率よい実現が可能.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
25 / 230
言語処理系の原理と構造
高機能計算機と高水準プログラミング言語
言語 L による L′ の実現 L ≤ L′ はどのように行うか? IV
コンパイラによる言語の実現
L2言語処理系
L1解釈機械M1
言語L1
L3解釈機械M3
L3で書かれたL2
⇒L1コンパイラ
L1解釈機械M1
言語L1
大堀 淳 (東北大学 電気通信研究所)
≦
言語L2
コンパイラ講義資料
26 / 230
高水準言語の役割
講義内容
.
. .3 高水準言語の役割
SML#の紹介
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
27 / 230
高水準言語の役割
高水準言語の役割
プログラミング言語定義再考
表装的定義:計算の記述
より本質的定義:複雑な情報処理システムの記述システム
その望ましい性質:
厳密な定義があること.
高水準かつ高機能であること.
信頼性が高く安全であること.
本講義では,これらの観点から現時点で最も優れた言語である ML を紹
介し,そのような言語を現実のデジタルコンピュータで実現するコンパ
イラの構築原理を学ぶ.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
28 / 230
高水準言語の役割
SML#の紹介
講義で使用するプログラミング言語
本講義では,プログラミングに SML#を使用する.
.. 教育用計算機室にインストール済み.
1
.
以下のコマンドを入力し,パスを設定する.
% PATH=$PATH:/opt/local/bin
...
2
各自のPCにインストールして使用する(推奨)
インストール方法:SML#ホームページの「SML#の情報を網羅した
公式ドキュメント」の中の「II 5 SML#プログラミング環境の準備」
の「II 5.3. SML#のインストール」を参照.
推奨プログラミング環境:
Linux(Ubuntu, Vine),MacBook.
Linux は VMWare Player を使えば Windows から快適に使用できる.
emacs エディタ
SML#をソースからインストール
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
29 / 230
高水準言語の役割
SML#の紹介
ML の紹介
以下の資料を使用する.
教科書「プログラミング言語 Standard ML 入門」
大堀研究室で構築中の次世代 ML 言語:SML#ホームページ
SML# プログラミングテキスト「ソフトウェア技術者のための高信
頼関数型言語活用技術(基礎編)」
これらは,本講義のページからリンクが張ってある.さらに,
「SML #プ
ロジェクトのページ」の「Stadnard ML 言語の情報」を参照.
本講義では,ポイントと思われる以下の点を説明する.
再帰的関数と高階の関数
リストの扱い
データ型の定義と利用
モジュールの利用
資料「Standard ML プログラミングのエッセンス (2011 年 10 月 11 日)
Standard ML(SML#) 言語活用のヒント」のリンク先.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
30 / 230
字句解析
言語の階層的な定義と解析
講義内容
.
. .4 字句解析
言語の階層的な定義と解析
記号列の定義と解析
語彙の定義と解析
ML-lex:字句解析の具体例
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
31 / 230
字句解析
言語の階層的な定義と解析
言語の階層的な構造
言語は通常以下の 3 層構造で理解することが多い.
1
2
3
構造
記号列
語彙列
文章
構成要素造
アルファベット
定数,名前,区切り記号等
主語,述語,修飾句,文等の文法概念
言語を理解するためには,これらそれぞれの層に対して,その構造の
.. 構造の定義
1
.
...
2
その構造の解析方式
を理解する必用がある.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
32 / 230
字句解析
記号列の定義と解析
記号列の定義
.
文字列の定義
Σ∗ = {a1 a2 . . . a n|0 ≤ n, ai ∈ Σ}
.
..
以下の記法を用いる.
.
.
.
..
有限集合 Σ 上の文字列集合 Σ∗ は以下のような集合である.
Σ の要素 a, b, c, ....
Σ∗ の要素 x, w, ....
空文字列 ϵ .
空集合 ∅.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
33 / 230
字句解析
記号列の定義と解析
文字列の操作
文字列 x = a1 a2 . . . a n と y = b1 b2 . . . b m の連結を xy を以下のように定義
する.
xy = a1 a2 . . . a n b1 b2 . . . b m
文字列の集合に対して以下の演算を定義する.以下の演算を定義する.
AB = {xy | x ∈ A, y ∈ B}
{
{ϵ}
(n = 0)
An =
A A n−1
(n ≥ 1)
∪
A∗ =
{ A n | n ≥ 0}
∪
A+ =
{ A n | n ≥ 1}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
34 / 230
字句解析
記号列の定義と解析
文字列の解析
文字列は構造を持たないため解析は自明な処理.
現実のプログラミング言語での文字列の解析(読み込み)処理
文字列は 1 文字以上の「空白文字」で区切られている.
空白文字は「空白」,
「タブ」,
「改行」等を含み,これらは Σ の集合
の要素ではない.
(これらは,文字列の中に含めることができない.
)
文字解析では,処理の最初に,連続した空白文字の読みとばす.
空白が現れるまでの文字を文字列と認識.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
35 / 230
字句解析
記号列の定義と解析
文字列解析(空白文字の読みとばし)
fun isSpace c = case c of
#" " => true
| #"\n" => true
| #"\t" => true
| _ => false
fun skipSpaces inStream =
case TextIO.lookahead inStream of
SOME c =>
if isSpace c then
(TextIO.input1 inStream; skipSpaces inStream)
else ()
| _ => ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
36 / 230
字句解析
記号列の定義と解析
文字列解析(文字列の読み込み)
fun readString inStream =
let
fun readRest s =
case TextIO.lookahead inStream of
SOME c => if isSpace c then s
else (TextIO.input1 inStream;
readRest (s ˆ String.str c))
| _ => s
in
(skipSpaces inStream;
readRest "")
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
37 / 230
字句解析
記号列の定義と解析
文字列解析(処理本体)
fun readAndPrintLoop inStream =
if TextIO.endOfStream inStream then
()
else
let
val string = readString inStream
in
(
print strring;
print "\n";
readAndPrintLoop inStream
)
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
38 / 230
字句解析
記号列の定義と解析
文字列解析(トップレベル)
fun processFile processor file =
let
val inStream = TextIO.openIn file
in
(
processor inStream;
TextIO.closeIn inStream
)
end
fun analyzeFile file = processFile readAndPrintLoop file
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
39 / 230
字句解析
記号列の定義と解析
演習
以上を参考に,以下の各処理を行うプログラムを作成せよ.
.. ファイルのコピーする.
1
.
...
...
...
...
...
2
1 文字以上連続する空白を1つの空白に置き換える.
3
英文大文字をすべて小文字に変換する.
4
ファイルの文字数を求める.
5
ファイルの中の文字列の数を求める.
6
ファイルの中の文字列をリストにして返す.
1から3は,入力ファイル名と出力ファイル名を受け取り,入力ファイ
ルをオープンし,処理を行い,出力ファイルに書き出すものとする.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
40 / 230
字句解析
語彙の定義と解析
字句解析処理
プログラミング言語の定義と解析の実質的な最初の作業は字句(語彙)
の定義である.
.
字句(語彙)
..
ひとまとまりとして認識されるシンボルの最小単位.
.
各種定数
構文の区切り文字
.
..
.
これらは,
「正規言語(表現)」を用いて定義され,有限オートマトンを
使って解析される.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
.
名前
41 / 230
字句解析
語彙の定義と解析
正規言語の定義
.
正規言語
.
...
...
...
.
. ..
..
2
{ϵ} は正規言語である.
3
a ∈ Σ なる a に対して,{a} は正規言語である.
4
R が正規言語なら R∗ は正規言語である.
5
R1 と R2 が正規言語なら, R1 ∪ R2 と R1 R2 は正規言語である.
.
.
正規言語の閉包性
.
.
..
以下の規則で生成される言語属.
.. 空集合 ∅ は正規言語である.
1
.
..
.
..
大堀 淳 (東北大学 電気通信研究所)
¬R, R n, R+ , R \ S, R ∩ S
コンパイラ講義資料
.
.
R, S が正規言語なら,以下の各集合も正規言語である.
42 / 230
字句解析
語彙の定義と解析
(拡張)正規表現
正規表現 r
ϕ
ϵ
a
r*
rs
r|s
意味する集合 [[r]]
∅
{ϵ}
{a}
[[r]]∗
[[r]][[s]]
[[r]] ∪ [[s]]
直感的意味
空集合
空文字
文字 a
r の 0 回以上の繰り返し
r に続けて s
r かまたは s
.
[a1 a2 · · · a n]
[a1 -a n]
[ˆa1 -a n]
r+
r?
(r)
{name}
Σ
{a1 , a2 , . . . , a n}
{a|a1 ≤ a ≤ a n}
Σ \ {a1 , . . . , a n}
[[r]]+
[[r]] ∪ {ϵ}
[[r]]
[[r]]
空白意外の任意の 1 文字
a1 から a n のどれか一文字
a1 から a2 までの間のどれか 1 文字
a1 から a2 以外の 1 文字
r の 1 回以上の繰り返し
0 回または 1 回の r
大堀 淳 (東北大学 電気通信研究所)
(式を区別するための区切り)
(定義 name = r の参照)
コンパイラ講義資料
43 / 230
字句解析
語彙の定義と解析
正規表現による語彙の定義
通常,プログラミング言語の語彙は正規表現によって定義される.
例:
num=[0-9]+;
frac="."{num};
exp=[eE](˜?){num};
real=(˜?)(({num}{frac}?{exp})|({num}{frac}{exp}?));
real は浮動小数点定数の集合を表す正規表現.
(これは実際に SML#で使
用されている定義.
)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
44 / 230
字句解析
語彙の定義と解析
有限状態オートマトンによる正規言語の解析
.
.
定理
.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
.
..
与えられた任意の正規表現に対して,その正規言語を認識する決定性有
.限状態オートマトン(DFA)を構築できる.
..
.
.
定理
..
任意の正規言語に対して,その言語を認識する決定性有限状態オートマ
トン(
DFA)が存在する.
.
..
.
さらに,
.
45 / 230
字句解析
語彙の定義と解析
有限状態機械
有限状態機械 D:書き換え可能なメモリーを持たない逐次機械.以下の
構造を持つ.
D = (Q, Σ, δ, q0 , F)
Q : 状態の有限集合
Σ : 入力文字集合
δ : 状態遷移関数 Q × Σ → Q
q0 : 初期状態
F : 最終状態集合
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
46 / 230
字句解析
語彙の定義と解析
機械 D が認識する言語 L(D)
有限状態機械 D は,言語 L( D) の認識機と見なすことができる.
δ̂:δ の Q × Σ∗ への拡張:
δ̂(q, ϵ) = q
δ̂(q, ax) = δ̂(δ(q, a), x)
D = (Q, Σ, δ, q0 , F) が認識する言語:
L(D) = {x | δ̂(q0 , x) ∈ F}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
47 / 230
字句解析
語彙の定義と解析
正規言語を認識する DFA 作成手順
与えられた正規表現 r から,
L(D r ) = [[r]]
である有限状態機械 D r を以下の手順で構築する.
...
...
1
DFA より一般的な非決定性有限状態機械(NFA)を定義する.
2
与えられた正規表現 r に対して
L(N r ) = [[r]]
となる NFA N r の構築手順を与える.
...
3
NFA N を,
L(N) = L(D N )
を満たす DFA D N へ変換する手順を与える.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
48 / 230
字句解析
語彙の定義と解析
非決定性有限状態機械(NFA)
有限状態機械 N:
N = (Q, Σ, δ, q0 , F)
Q : 状態の有限集合
Σ : 入力文字集合
δ : 状態遷移関数 Q × (Σ ∪ {ϵ}) → 2Q
q0 : 初期状態
F : 最終状態集合
NFA は DFA に比べて以下の柔軟性がある.
同じ入力シンボルに対して複数の状態への遷移がある.
入力を消費せずに別の状態の遷移できる.
(ϵ 遷移)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
49 / 230
字句解析
語彙の定義と解析
NFA が認識する言語
ϵ 到達関係の定義
ϵ
p −→ p
q ∈ δ(p, ϵ)
ϵ
p −→ q
ϵ -Closure(P) の定義:
ϵ
p −→ q
ϵ
q −→ r
ϵ
p −→ r
ϵ
Cl(P) = {q | p ∈ P, p −→ q}
δ の 2Q × Σ∗ への拡張
δ̂(P, ϵ) = Cl(P)∪
δ̂(P, a) = Cl(
δ(p, a))
p∈Cl(P)
δ̂(P, aw) = δ̂(δ̂(P, a), w)
NFA N が認識する言語 L(N)
L(N) = {x | δ̂({q0 }, x) ∩ F , ∅}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
50 / 230
字句解析
語彙の定義と解析
N r の構築
正規言語の再帰的な定義
r ::= ϕ | ϵ | a | r∗ | (r|r) | rr
に従い, L(N r ) = [[r]] なる NFA N r でかつ以下の性質をもつものを r の構
造に関して再帰的に構築する.
他の状態から初期状態への遷移はない.
唯一の最終状態を持ち,かつ.最終状態からの遷移はない.
例えば r∗ は,L(N r ) = [[r]] なる NFA N r を使い,以下のように構築できる.
ε
ε
Nr
ε
ε
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
51 / 230
字句解析
語彙の定義と解析
NFA と DFA の等価性
任意の DFA D はそれ自身 NFA の特殊な場合である.
.
定理
.
..
任意の NFA N = (Q N , Σ, δ N , q N , F N ) に対して
.なる DFA D N = (Q D , Σ, δ D , q D , F D ) が存在する.
..
.
.
L(N) = L(D N )
証明(の概要)
:
Q D = 2QN ( N の状態の集合の集合)
q D = Cl({q N })
F D = {q|q ∈ Q D , q ∩ F D , ∅} ( F D の要素を含むものすべて)
δ D は,δ N の拡張 δˆN : 2QN × Σ∗ → 2QN を 2QN × Σ へ制限して得られ
る関数とする.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
52 / 230
字句解析
語彙の定義と解析
D N の構築
以上の結果,すなわち,
.. Cl(P) の計算
1
.
...
...
2
δ の δ̂ への拡張
3
δ̂ を用いた 2Q を状態とする機械の構築
は,任意の NFA N を,それと等価な DFA D N に変換する手続きを与えて
いる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
53 / 230
字句解析
語彙の定義と解析
課題
...
1
(Subset Construction)以下の洞察を参考に,NFA N から DFA D N
へ変換する効率よい手続きを記述せよ.
D N の状態集合 Q D は,
{P | P ⊆ Q N , かつある w があって P = δˆN ({q0 }, w)}
のみで十分.
そこで, pD = Cl({pN }) から始めて,δˆN によって一文字で到達可能な
集合を列挙していけば,Q D と δ D が得られる.
つまり,以下の計算を行えばよい.
..1.
..2.
Q D ←− {pD } とする.
Q D が増えなくなるまで以下を繰り返す
Q D ←− Q D ∪ {δˆN (P, a) | P ∈ Q D , a ∈ Σ}
...
2
正規表現 a(b|c) ∗ d を受理する NFA を定義し,それを DFA に変換
せよ.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
54 / 230
字句解析
ML-lex:字句解析の具体例
講義内容
.
. .4 字句解析
言語の階層的な定義と解析
記号列の定義と解析
語彙の定義と解析
ML-lex:字句解析の具体例
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
55 / 230
字句解析
ML-lex:字句解析の具体例
字句解析処理の作成手順
以上の理論を基礎とし,字句の定義からその字句のための字句解析解プ
ログラムを自動的に作成するツール lex が実用化されている.
以下の手順で使用する.
.. lex の約束に従い語彙の定義を正規言語で記述したファイル
1
.
(mylex.lex) を用意
..2 lex ツールで mylex.lex を処理し,正規言語で定義した語彙を解析す
るプログラムソースファイル (mylex.lex.xx) を生成.
.. mylex.lex.xx を字句解析を必用とするプログラムから呼び出す.
3
.
.
Standard ML 系の言語では,ML-Lex として実装されている.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
56 / 230
字句解析
ML-lex:字句解析の具体例
ML-Lex の使い方
....
..
語彙記述ファイル mylex.lex の作成
ML-Lex を用いて mylex.lex から字句解析関数を自動生成する.
% smlsharp
# use "lexgen.sml";
# LexGen.lexGen "coreML.lex";
これによって,coreML.lex.sml が生成される.
.3. coreML.lex.sml の中に生成される makeLexer 関数に文字読み込み
関数を与える
val lexer = CoreML.makeLexer characterReader
lexer が求める句解析関数.
.4. lexer を使って,語彙を読み込み処理を行う.
...
val nextToken = lexer ()
...
case nextToken of ..
1
2
.
.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
57 / 230
字句解析
ML-lex:字句解析の具体例
語彙記述ファイル mylex.lex
以下の形式のファイル
種々のユーザ定義
%%
ML-lex のための補助定義
%%
正規表現の定義
注
ML-lex のための補助定義は主に
name = regularExpression ;
の形の正規言語の定義.{name} の形で参照できる.
正規言語の定義は,可能な正規表現と,それに対する動作表す ML
の式の組みをリストする.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
58 / 230
字句解析
ML-lex:字句解析の具体例
語彙記述ファイルの例 I
type lexresult = Tokens.token
val eof = fn () => Tokens.EOF
fun atoi s = valOf (Int.fromString s)
%%
%structure
alpha
digit
ws
eol
sym
symbol
num
CoreML
= [A-Za-z];
= [0-9];
= [\ \t];
= "\r\n" | "\n" | "\r";
= [!%&$+/:<=>?@˜|#*] | \- | \ˆ;
= {sym}|\\;
= [0-9]+;
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
59 / 230
字句解析
ML-lex:字句解析の具体例
語彙記述ファイルの例 II
frac
exp
real
quote
underscore
idchars
id
=
=
=
=
=
=
=
"."{num};
[eE](˜?){num};
(˜?)(({num}{frac}?{exp})|({num}{frac}{exp}?));
"’";
"\_";
{alpha}|{digit}|{quote}|{underscore};
({alpha}|{quote}){idchars}*;
%%
{ws}
=> (lex());
{eol}
=> (lex ());
"andalso" => (Tokens.ANDALSO);
"and" => (Tokens.AND);
"as" => (Tokens.AS);
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
60 / 230
字句解析
ML-lex:字句解析の具体例
語彙記述ファイルの例 III
...
"_" => (Tokens.UNDERBAR);
"{" => (Tokens.LBRACE);
"|" => (Tokens.BAR);
"}"
=> (Tokens.RBRACE);
{id}
=> (Tokens.ID (yytext));
{num}
=> (Tokens.INT (atoi yytext));
˜{num}
=> (Tokens.INT (atoi yytext));
{symbol}+
=> (Tokens.ID (yytext));
{real}
=> (Tokens.REAL (yytext));
\"{idchars}*\" => (Tokens.STRING
(String.substring
(yytext, 1, String.size yytext - 2)));
.
=> (Tokens.SPECIAL(yytext));
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
61 / 230
字句解析
ML-lex:字句解析の具体例
ML-lex の使用例 I
structure Tokens = struct
datatype token =
EOF
| AND
| ANDALSO
...
| RBRACE
| RBRACKET
| INT of int
| REAL of string
| SPECIAL of string
| STRING of string
| UNDERBAR
....
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
62 / 230
字句解析
ML-lex:字句解析の具体例
ML-lex の使用例 II
fun token2string token =
case token of
EOF => "EOF "
| AND => "AND"
| ANDALSO => "ANDALSO"
....
| RBRACE => "RBRACE"
| RBRACKET => "RBRACKET"
| INT i => "INT " ˆ (Int.toString i)
| REAL string => "REAL " ˆ string
| SPECIAL string => "SPECIAL " ˆ string
| STRING string => "STRING " ˆ string
| UNDERBAR => "UNDERBAR"
....
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
63 / 230
字句解析
ML-lex:字句解析の具体例
ML-lex の使用例 III
fun interactiveReadN inStream n =
let
fun readRest 0 s = s
| readRest n s =
(case TextIO.lookahead inStream of
SOME #"\n" => (TextIO.input1 inStream; s ˆ "\n")
| SOME c => (TextIO.input1 inStream;
readRest (n - 1) (s ˆ String.str c))
| _ => s)
in
readRest n ""
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
64 / 230
字句解析
ML-lex:字句解析の具体例
ML-lex の使用例 IV
fun loop lexer =
let
val nextToken = lexer()
val _ = print (Tokens.token2string nextToken ˆ "\n")
in
if nextToken = Tokens.EOF then ()
else loop lexer
end
fun main () =
let
val lexer = CoreML.makeLexer
(interactiveReadN TextIO.stdIn)
in loop lexer
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
65 / 230
字句解析
ML-lex:字句解析の具体例
(補足)ML-lex の規則の詳細指定
ML-Lex の補助定義
%s identifier list ;
オートマトンの状態指定.
正規言語の規則の一般形
<start state list> regular expression => ( code );
この機能により,種々の詳細な動作指定が可能.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
66 / 230
構文解析
(生成)文法による構文構造の定義
講義内容
.
. .5 構文解析
(生成)文法による構文構造の定義
文脈自由文法による文法構造の定義
文脈自由言語の構文解析
LR 構文解析の原理
LR パーザ─の構築
YACC システム
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
67 / 230
構文解析
LR 構文解析の原理
LR 構文解析の原理
本節の内容
.. 生成文法の考え方
1
.. 文脈自由言語の構文解析戦略
2
.. LR 構文解析のアイデアと原理
3
.. LR 構文解析の基本定理の証明
4
.. 構文解析アルゴリズム
5
を含む詳細な解説を
.
.
.
.
.
LR 構文解析の原理,大堀 淳,コンピュータ ソフトウェア,Vol.
31 (2014) No. 1 p. 1 30-1 42
に出版したので,この解説論文を参照.
J-Stage のコンピュータソフトウエアレポジトリからダウンロードできる.
論文の URL は,以下の通り
https://www.jstage.jst.go.jp/article/jssst/
31/1/31 1 30/ article/-char/ja/
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
68 / 230
構文解析
YACC システム
パーザ─生成システム:YACC
以上の理論に基づき,LALR パーザ生成ツールが実用化されている.
本講義では,以下を材料に,このツールの使用方法を学ぶ.
.1. 言語:Standard ML Core Language
Standard ML の解説スライドの最後に文法規則を記載.
.. YACC システム:ML yacc 以下の資料に簡単な日本語の解説がある.
2
.
.
http://www.pllab.riec.tohoku.ac.jp/education/lectures
/compiler/code/mlyaccKaisetsu.pdf
...
3
ML yacc を使用して構築したパーザ.
http://www.pllab.riec.tohoku.ac.jp/education/lectures
/compiler/code/coreMLParse.tgz
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
69 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 I
以下に,Standard ML の核言語の文法と,それに対応する ML-Yacc にお
ける定義の例を示す.
(補足)
文法の定義は「Syntax」のように青色で,対応する ML-Yacc のソー
スは,
「Syntax」のようにタイプライタフォントで示す.
双方とも簡略化してある.主な点は以下の通り.
トップレベルの削除
型の指定の削除
datatype,type 宣言の削除
その他型が出てくる構文の削除
Standard ML の核言語の文法は,The Definition of Standard ML に
準拠.
ML-Yacc のソース例は,SML #コンパイラチームで実際に使用した
ものの対応部分を抜き出したもの.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
70 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 II
補助規則:
xSeq
::=
|
|
大堀 淳 (東北大学 電気通信研究所)
x
(x1 ,· · · ,x n)
one element
empty sequence
finite sequence( n ≥ 2)
コンパイラ講義資料
71 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 III
原子式
atexp
exprow
appexp
infix
::=
|
|
|
|
|
|
|
|
::=
::=
|
::=
|
scon
⟨op⟩ longvid
{⟨exprow⟩ }
()
(exp1 ,· · · ,exp n)
[exp1 ,· · · ,exp n]
(exp1 ;· · · ;exp n)
let dec in exp1 ;· · · ;exp n end
(exp)
lab = exp ⟨, exprow⟩
atexp
appexp atexp
appexp
infix vid infix
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
(left associative)
72 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 IV
constant :
|
|
|
|
id
INT ()
WORD ()
STRING ()
REAL ()
CHAR ()
: ID ()
| EQ ()
| ASTERISK ()
expid : id ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
73 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 V
atexp :
|
|
|
|
|
|
|
|
|
|
|
|
|
|
constant ()
expid ()
OP expid ()
LBRACE exprow RBRACE ()
LBRACE RBRACE ()
HASH id ()
HASH INT ()
LPAREN RPAREN ()
LPAREN expseq_comma RPAREN ()
LBRACKET RBRACKET ()
LBRACKET exp RBRACKET ()
LBRACKET expseq_comma RBRACKET ()
LPAREN exp SEMICOLON expseq_semicolon RPAREN ()
LET decseq_semicolon IN expseq_semicolon END ()
LPAREN exp RPAREN ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
74 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 VI
expseq_comma : exp COMMA exp ()
| expseq_comma COMMA exp ()
expseq_semicolon : exp ()
| expseq_semicolon SEMICOLON exp ()
appexp :
|
|
|
atexp ()
appexp atexp ()
appexp HASH LBRACE exprow RBRACE ()
appexp HASH LPAREN expseq_comma RPAREN ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
75 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 VII
式の文法
exp
::=
|
|
|
|
|
|
|
|
大堀 淳 (東北大学 電気通信研究所)
infix
exp andalso exp
exp orelse exp
exp handle match
raise exp
if exp then exp else exp
while exp do exp
case exp of match
fn match
コンパイラ講義資料
76 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 VIII
exp :
|
|
|
|
|
|
|
|
|
appexp ()
exp ANDALSO exp ()
exp ORELSE exp ()
exp HANDLE match ()
RAISE exp ()
IF exp THEN exp ELSE exp ()
WHILE exp DO exp ()
CASE exp OF match ()
FN match ()
CAST LPAREN exp RPAREN ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
77 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 IX
式の文法 (つづき)
match
mrule
::=
::=
mrule ⟨| match⟩
pat => exp
match : pat DARROW exp ()
| pat DARROW exp BAR match ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
78 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 X
パターン
atpat
::=
patrow
|
|
|
|
|
|
::=
|
|
::=
|
|
|
pat
大堀 淳 (東北大学 電気通信研究所)
scon
⟨op⟩ longvid
{⟨patrow⟩ }
()
(pat1 ,· · · ,pat n)
[pat1 ,· · · ,pat n]
(pat)
...
lab = pat ⟨, patrow⟩
vid ⟨as pat⟩ ⟨,patrow⟩
atpat
⟨op⟩ longvid atpat
pat vid pat
⟨op⟩ pat as pat
コンパイラ講義資料
79 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 XI
patid : ID ()
atpat : UNDERBAR ()
| patid ()
| OP patid ()
| constant ()
| LBRACE RBRACE ()
| LBRACE fields RBRACE ()
| LPAREN RPAREN ()
| LPAREN patseq_comma RPAREN ()
| LBRACKET RBRACKET ()
| LBRACKET pat RBRACKET ()
| LBRACKET patseq_comma RBRACKET ()
| LPAREN pat RPAREN ()
apppat : atpat ()
| apppat atpat ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
80 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 XII
pat : apppat ()
| pat AS pat ()
| LPAREN pat BAR pat RPAREN ()
fields : label EQ pat ()
| label optaspat ()
| PERIODS ()
| label EQ pat COMMA fields ()
| label optaspat COMMA fields ()
optaspat : ()
| AS pat ()
patseq_comma : pat COMMA pat ()
| patseq_comma COMMA pat ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
81 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 XIII
宣言
dec
valbind
funbind
::=
|
|
|
|
|
|
|
::=
|
::=
val valbind
fun funbind
local dec in dec end
opne longstrid1 · · · longstrid n
dec ; dec
infix ⟨d⟩ vid1 · · · vid n
infixr ⟨d⟩ vid1 · · · vid n
nonfix vid1 · · · vid n
pat = exp ⟨and valbind⟩
rec valbind
⟨op⟩ vid atpat11 · · · atpat1n = exp1
| ⟨op⟩ vid atpat21 · · · atpat2n = exp2
| ···
| ⟨op⟩ vid atpat m1 · · · atpat mn = exp m
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
( m, n ≥ 1)
82 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 XIV
decseq_semicolon :
|
|
|
dec :
|
|
|
|
|
|
|
|
()
SEMICOLON decseq_semicolon ()
dec decseq_semicolon ()
LOCAL decseq_semicolon IN decseq_semicolo
decseq_semicolon ()
VAL valbind ()
VAL REC valbind ()
FUN fvalbind ()
EXCEPTION exbinds ()
OPEN idseq ()
INFIX INT idseq ()
INFIXR INT idseq ()
INFIX idseq ()
INFIXR idseq ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
83 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 XV
| NONFIX idseq ()
idseq : id ()
| id idseq ()
exbinds : exbind ()
| exbind AND exbinds ()
exbind :
|
|
|
|
condec ()
id EQ id ()
id EQ OP id ()
OP id EQ id ()
OP id EQ OP id ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
84 / 230
構文解析
YACC システム
SML の核言語の文法と ML-Yacc の入力 XVI
valbind : pat EQ exp ()
| pat EQ exp AND valbind
()
fvalbind : frules ()
| frules AND fvalbind ()
frules : frule ()
| frule BAR frules ()
frule : apppat EQ exp ()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
85 / 230
型の解析と型推論
文法の定義の限界
講義内容
.
. .6 型の解析と型推論
文法の定義の限界
型システム
型推論アルゴリズム
型推論アルゴリズム(1)の実装
PTS の分析
多相型の推論
多相型の型推論アルゴリズム
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
86 / 230
型の解析と型推論
文法の定義の限界
文脈自由文法の限界
ほとんどの場合,言語を正確に定義するには,文脈に依存した規則が
必用.
例:
変数の参照.
通常,言語には変数や代名詞が存在するが,それらは,参照の前に
定義されていることが要求される.
# val x = foo + 1;
stdIn:1.8-1.11 Error: unbound variable : foo
関数の使い方.
関数や動詞などは通常その作用の対象が限定される.
# "cat" + 1;
stdIn:2.1-2.9 Error:
operator and operand don’t agree
これらは,文脈自由文法では定義困難.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
87 / 230
型の解析と型推論
文法の定義の限界
言語の定義の階層の再吟味
文脈に依存しない言語の構造の定義
構造
構成要素
定義の枠組み
記号列
語彙列
文章
アルファベット
定数,名前,区切り記号等
主語,述語,修飾句,文等の文法概念
記号列集合
正規言語
文脈自由文法
+
文脈依存の言語構造の定義
構造
構成要素
定義の枠組み
参照関係
参照関係,型の関係
型システム
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
88 / 230
型の解析と型推論
型システム
型の概念 I
...
データの種類
# 1;
val it = 1 : int
# "cat";
val it = "cat" : string
...
データ構造
# (1,2);
val it = (1, 2) : int * int
# {Region = "Bordeaux", Year=1988};
val it = {Region = "Bordeaux", Year = 1988}
: {Region:string , Year:int}
# [1,2];
val it = [1,2] : int list
1
2
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
89 / 230
型の解析と型推論
型システム
型の概念 II
...
関数の振る舞い
# fun f x = x + 1;
val f = fn : int -> int
# fun f (x,y) = x ˆ y;
val f = fn : string * string -> string
...
関数の汎用性
# fun id x = x;
val id = fn : [’a .’a -> ’a]
# fun length nil = 0
| length (h::t) = 1 + length t;
val length = fn : [’a .’a list -> int]
3
4
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
90 / 230
型の解析と型推論
型システム
簡単な言語とその型の定義
型システムの問題を理解するため,単純化した以下の言語と型を考える.
.. 言語の定義.
1
.
exp
id
n
s
exp exp
(exp,exp)
fn id => exp
::=
|
|
|
|
|
...
2
(変数)
(整数定数)
(文字列定数)
(関数適用)
(組み)
(関数式
型の集合の定義.
大堀 淳 (東北大学 電気通信研究所)
τ
::=
|
|
|
|
t
int
string
τ -> τ
τ*τ
コンパイラ講義資料
(型変数)
(整数型)
(文字列型)
(関数)
(組型)
91 / 230
型の解析と型推論
型システム
式の型の定義
式の型の定義の考え方.
.. 式は変数による参照を含む.
1
.
...
2
式の変数の使われ方は変数の定義(宣言)される文脈に依存.
この変数の定義される文脈を,変数の型環境でモデル化する.
Γ ::= {x1 : τ1 , . . . , x n : τ n}
例えば,
val x = 1;
val y = ”cat”;
[X]
なら,[ X ] の部分の型環境は,{x: int, y : string} である.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
92 / 230
型の解析と型推論
型システム
式の型判定
式 exp が型環境 Γ で型 τ を持つとう関係を
Γ ⊢ exp : τ
と書き,これを「型判定」と呼ぶ.
型判定が成立するか否かの条件を,式の構文に応じて以下のような形の
規則で定義する.
原子式の場合
(規則名) Γ ⊢ ex p : τ (条件)
一つの式から生成される複合式の場合.
Γ1 ⊢ ex p1 : τ1
(規則名)
(条件)
Γ2 ⊢ ex p2 : τ2
2つの式から生成される複合式の場合.
Γ1 ⊢ ex p1 : τ1
Γ2 ⊢ ex p2 : τ3
(規則名)
(条件)
Γ3 ⊢ ex p3 : τ3
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
93 / 230
型の解析と型推論
型システム
型システムの定義
(var) Γ ⊢ x : τ
(x : τ ∈ Γ)
(int) Γ ⊢ n : int
(str) Γ ⊢ s : st ring
(app)
Γ ⊢ ex p1 : τ1 → τ2
Γ ⊢ ex p2 : τ1
Γ ⊢ ex p1 ex p2 : τ2
(pair)
Γ ⊢ ex p1 : τ1
Γ ⊢ ex p2 : τ2
Γ ⊢ (ex p1 , ex p2 ) : τ1 ∗ τ2
(abs)
Γ ∪ {x : τ1 } ⊢ ex p1 : τ2
Γ ⊢ fn x => ex p1 : τ1 → τ2
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
94 / 230
型の解析と型推論
型推論アルゴリズム
型推論問題
...
...
1
2
式 exp が与えられた時,Γ ⊢ ex p : τ となる (Γ, τ) を求めよ.
式 exp と Γ が与えられた時,S(Γ) ⊢ ex p : τ となる (S, τ) を求めよ.
ただし S は型変数への代入.
型変数の集合を Tvar とし,型の集合を Ty pe とする.型変数への代
入 S は,Tvar から Ty pe への関数でかつ,{t | S(t) , t} が有限であ
るもの.
..1.
..2.
S(τ):τ の中の型変数に S を適用して得られる型
S(Γ):Γ の中の型変数に S を適用して得られる型環境
両方可能であるが,2の方がより現実的でかつ多相型に拡張可能.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
95 / 230
型の解析と型推論
型推論アルゴリズム
型の単一化
型推論問題は,型の単一化を使って解く.
.
.
型等式集合の単一化(unification)
.
E を型の組みの集合とする.総ての (τ1 , τ2 ) ∈ E について,S(τ1 ) = S(τ2 )
となる型変数への代入
S を E の単一化という.
.
..
.
この後者の問題を解くアルゴリズムを与える.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
.
..
.
型等式の単一化(unification)
..
型 τ1 と τ2 が与えられた時,S(τ1 ) = S(τ2 ) となる型変数への代入 S を τ1
と
. τ2 の単一化という.
..
.
より一般化した問題.
.
96 / 230
型の解析と型推論
型推論アルゴリズム
単一化アルゴリズム
二つの型の組み(型の等式)の集合の組み (E, S) の変形関係 =⇒ を使い,
単一化アルゴリズム U を

∗


 S
((E, ∅) =⇒ (∅, S) のとき )
U(E) = 

 failure
( 上記以外 )
と定義する.
補足
E はこれから単一化をしようとする型の等式集合
S は, t = τ の形の「すでに解けている」型の等式集合
S は {(t 1 , τ1 ), . . . , (t n, τ n)} の形をしており,それ自身単一化と見な
せる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
97 / 230
型の解析と型推論
型推論アルゴリズム
単一化アルゴリズムの変形規則
(u-i)
(u-ii)
(E ∪ {(τ, τ)}, S) =⇒ (E, S)
(E ∪ {(t, τ)}, S) =⇒ ([τ/t](E), {(t, τ)} ∪ [τ/t](S))
(ただし t < FTV(τ) のとき)
(u-iii) (E ∪ {(τ1 → τ2 , τ1 → τ2 )}, S) =⇒ (E ∪ {(τ1 , τ1 ), (τ2 , τ2 )}, S)
(u-iv) (E ∪
注
1
1
{(τ
1
×
1
2
τ ,
1
2
τ1
2
×
2
2
τ )},
2
S) =⇒ (E ∪
1 2
1 2
1 1
2 2
{(τ , τ ), (τ , τ )},
1 2
1 2
S)
[τ1 /t 1 , . . . , τ n/t n] は型変数 t 1 , . . . , t n にそれぞれ τ1 , . . . , τ n を代入す
る型代入.
FTV(τ) は τ の中の型変数の集合.
(u-ii) の中の条件 t < FTV(τ) は, t = τ が解をもつ条件であり,occur
check と呼ばれる.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
98 / 230
型の解析と型推論
型推論アルゴリズム
型推論アルゴリズム(1)
PTS(n) = (∅, int)
PTS(s) = (∅, string)
PTS(x) = ({x : t}, t) ( t fresh)
PTS(fn x => ex p) = let (Γ1 , τ1 ) = PTS(ex p)
in if x ∈ dom(Γ1 ) then (Γ1 | x , Γ1 (x) → τ1 )
else (Γ1 , t → τ1 ) ( t fresh)
PTS(exp1 exp2 ) = let (Γ1 , τ1 ) = PTS(ex p1 )
(Γ2 , τ2 ) = PTS(ex p2 )
S = U(mat ches({Γ1 , Γ2 }) ∪ {(τ1 , τ2 → t}) ( t fresh)
in (S(Γ1 ) ∪ S(Γ2 ), S(t))
PTS((exp1 , ex p2 )) = let (Γi , τi ) = PTS(ex pi ) (i ∈ {1, 2})
S = U(mat ches({Γ1 , Γ2 }))
in (S(Γ1 ∪ Γ2 ), S(τ1 ) × S(τ2 ))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
99 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
モジュール構成
モジュール
exp.grm
Absyn
Parser
Types
TypeContext
Unify
Printer
Typeinf
Main
大堀 淳 (東北大学 電気通信研究所)
機能
ソース言語の ml-yacc の入力
ソース言語の構文木
パーザ
型 (τ) 等の定義
型環境 (Γ) や型代入 (S) の定義
単一化アルゴリズム
t au,Γ, ex p のプリンタ
PTS アルゴリズム
トップレベル関数
コンパイラ講義資料
100 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
exp.grm
start : exp (exp)
exp : appexp (appexp)
| IF exp THEN exp ELSE exp (Absyn.EXPIF(exp1, exp2, exp3))
| FN ID DARROW exp (Absyn.EXPFN(ID, exp))
constant : INT (Absyn.INT(INT))
| STRING (Absyn.STRING(STRING))
atexp : constant (constant)
| ID (Absyn.EXPID(ID))
| LPAREN exp COMMA exp RPAREN
(Absyn.EXPPAIR(exp1, exp2))
| LPAREN exp RPAREN (exp)
appexp : atexp (atexp)
| appexp atexp (Absyn.EXPAPP(appexp, atexp))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
101 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Absyn.ppg I
structure Absyn =
struct
(*%
* @prefix format
*)
datatype exp
= (*%
* @prefix format
* @format(value) value
*)
INT of int
| (*%
* @prefix format
* @format(value) "\"" value "\""
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
102 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Absyn.ppg II
*)
STRING of string
| (*%
* @prefix format
* @format(id) id
*)
EXPID of string
| (*%
* @prefix format
* @format(exp1 * exp2)
* !N0{ "(" exp1 "," exp2 ")" }
*)
EXPPAIR of exp * exp
| (*%
* @prefix format
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
103 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Absyn.ppg III
* @format(exp1 * exp2) L10{ exp1 + exp2 }
*)
EXPAPP of exp * exp
| (*%
* @prefix format
* @format(cond * ifTrue * ifFalse)
*
!N0{ "if" 2[ +d {cond} ]
*
+1 "then" 2[ +d {ifTrue} ]
*
+1 "else" 2[ +d {ifFalse} ] }
*)
EXPIF of exp * exp * exp
| (*%
* @prefix format
* @format(id * exp) !N0{ "fn" + id + "=>" + exp }
*)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
104 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Absyn.ppg IV
EXPFN of string * exp
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
105 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Types.ppg I
structure Types =
struct
local
val nextTyId = ref 0
fun newTyId () = (!nextTyId before nextTyId := !nextTyId +
in
fun initSeed () = nextTyId := 0
fun newTyIdName () =
let
fun tyIdName tid =
let
fun numeral n =
if n < 26
then [ord #"a" + n]
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
106 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Types.ppg II
else
let val (msb, rest) = (n mod 26, (n div 26
in (ord #"a" + msb) :: (numeral rest)
end
in
(implode(map chr (rev (numeral tid))))
end
in
tyIdName (newTyId())
end
end
(*%
* @prefix format
*)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
107 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Types.ppg III
datatype ty =
(*%
* @prefix format
* @format "int"
*)
INTty
| (*%
* @prefix format
* @format "string"
*)
STRINGty
| (*%
* @prefix format
* @format(tyid) "’" tyid
*)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
108 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Types.ppg IV
TYVARty of string
| (*%
* @prefix format
* @format(domain * range)
* R1{ domain +d "->" + range }
*)
FUNty of ty * ty
| (*%
* @prefix format
* @format(field)
N2{ field }
* @format:field(fst * snd)
N3{fst} + "*" + N3{snd}
*)
PAIRty of ty * ty
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
109 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Types.ppg V
fun newTy () = TYVARty (newTyIdName())
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
110 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
TypeContext.ppg I
structure TypeContext = struct
local
structure T = Types
in
(*% *)
type ’a record =
(*%
* @format(field fields)
*
!N0{ "{" 2[1 fields(field)(+","+1)] 1 "}" }
* @format:field(label * ty) {label} d ":" d {ty}
*)
(string * ’a) list
fun formatGenericSmapTy parm smap =
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
111 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
TypeContext.ppg II
let
val L = StringMap.listItemsi smap
in
format_record parm L
end
type ty = Types.ty
(*%
* @prefix format
* @formatter(formatTy) Types.formatty
* @formatter(genericSmapTy) formatGenericSmapTy
*)
type typeContext =
(*%
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
112 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
TypeContext.ppg III
* @prefix format
* @format(ty:formatTy smap:genericSmapTy) smap(ty)
*)
ty StringMap.map
val emptyTypeContext = StringMap.empty
val emptySubst = StringMap.empty
fun substTy subst ty =
case ty of
T.INTty => ty
| T.STRINGty => ty
| T.TYVARty string =>
(case StringMap.find(subst,string) of
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
113 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
TypeContext.ppg IV
SOME newTy => newTy
| NONE => ty)
| T.FUNty (domTy, ranTy) => T.FUNty(substTy subst domTy, s
| T.PAIRty (fstTy, sndTy) => T.PAIRty(substTy subst fstTy,
fun composeSubst subst1 subst2 =
StringMap.unionWith
(fn (ty1, ty2) => ty1)
(StringMap.map (substTy subst1) subst2,
subst1)
fun substContext subst context =
StringMap.map (substTy subst) context
fun allMatches (context1, context2) =
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
114 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
TypeContext.ppg V
StringMap.listItems
(StringMap.intersectWith
(fn (ty1,ty2) => (ty1, ty2))
(context1, context2))
end
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
115 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml I
structure Unify = struct
local
structure T = Types
structure TC = TypeContext
in
exception Unify
fun FTV ty =
let
fun FTV’ ty set =
case ty of
T.INTty => set
| T.STRINGty => set
| T.TYVARty string => StringSet.add (set,string)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
116 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml II
| T.FUNty (domTy, ranTy) =>
FTV’ ranTy (FTV’ domTy set)
| T.PAIRty (fstTy, sndTy) =>
FTV’ sndTy (FTV’ fstTy set)
in
FTV’ ty StringSet.empty
end
fun occurs (T.TYVARty string, ty) =
StringSet.member(FTV ty, string)
| occurs _ = false
fun unify tyEquations =
let
fun unify’ (nil, subst) = subst
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
117 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml III
| unify’ ((ty1,ty2)::rest, subst) =
(case (ty1,ty2) of
(T.TYVARty string1, T.TYVARty string2) =>
if string1 = string2 then unify’ (rest, subst)
else
let
val substOne =
StringMap.singleton(string1, ty2)
val subst = TC.composeSubst substOne subst
in
unify’
(
map (fn (ty1,ty2) =>
(TC.substTy subst ty1,
TC.substTy subst ty2)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
118 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml IV
)
rest,
subst
)
end
| (T.TYVARty string, _) =>
if occurs (ty1, ty2) then raise Unify
else
let
val substOne =
StringMap.singleton(string, ty2)
val subst = TC.composeSubst substOne subst
in
unify’
(
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
119 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml V
|
|
|
|
|
|
map (fn (ty1,ty2) =>
(TC.substTy subst ty1,
TC.substTy subst ty2)
)
rest,
subst
)
end
(_, T.TYVARty string) =>
unify’ ((ty2, ty1)::rest, subst)
(T.INTty, T.INTty) => unify’ (rest, subst)
(T.INTty, _) => raise Unify
(_, T.INTty) => raise Unify
(T.STRINGty, T.STRINGty) => unify’ (rest, subst)
(T.STRINGty, _) => raise Unify
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
120 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml VI
| (_, T.STRINGty) => raise Unify
| (T.FUNty(domTy1, ranTy1),
T.FUNty(domTy2, ranTy2)) =>
unify’ ((domTy1,domTy2)
::(ranTy1,ranTy2)::rest,
subst)
| (T.FUNty _, _) => raise Unify
| (_, T.FUNty _) => raise Unify
| (T.PAIRty(fstTy1, sndTy1), T.
PAIRty(fstTy2, sndTy2)) =>
unify’ ((fstTy1, fstTy2)
::(sndTy1, sndTy2)::rest,
subst)
)
in
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
121 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Unify.sml VII
unify’ (tyEquations, StringMap.empty)
end
end
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
122 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Typeinf.sml I
structure Typeinf = struct
local
structure A = Absyn
structure T = Types
structure TC = TypeContext
structure U = Unify
in
exception NotImplemented
fun initPTS () = T.initSeed()
fun PTS absyn =
case absyn of
A.INT (int) => (StringMap.empty, T.INTty)
| A.STRING (string) => (StringMap.empty, T.STRINGty)
| A.EXPID (string) =>
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
123 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Typeinf.sml II
let
val newty = T.newTy()
in
(StringMap.singleton(string, newty), newty)
end
| A.EXPPAIR (exp1, exp2) =>
let
val (typeContext1, ty1) = PTS exp1
val (typeContext2, ty2) = PTS exp2
val tyEquations =
allMatches (typeContext1, typeContext2))
val subst = U.unify tyEquations
val newTypeContext =
substContext
subst
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
124 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Typeinf.sml III
(StringMap.unionWith #1
(typeContext1, typeContext2))
in
(newTypeContext,
T.PAIRty(TC.substTy subst ty1,
TC.substTy subst ty2))
end
| A.EXPAPP (exp1, exp2) =>
let
val (typeContext1, ty1) = PTS exp1
val (typeContext2, ty2) = PTS exp2
val tyEquations =
allMatches (typeContext1, typeContext2))
val newty = T.newTy()
val subst = U.unify ((T.FUNty(ty2, newty), ty1)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
125 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Typeinf.sml IV
:: tyEquations)
val newTypeContext =
substContext
subst
(StringMap.unionWith
#1
(typeContext1, typeContext2))
in
(newTypeContext, TC.substTy subst newty)
end
| A.EXPFN (string, exp) =>
let
val (typeContext, ty) = PTS exp
in
case StringMap.find(typeContext, string) of
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
126 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Typeinf.sml V
SOME domty =>
(#1
(StringMap.remove(typeContext, string)),
T.FUNty(domty, ty))
| NONE => (typeContext, T.FUNty(T.newTy(), ty))
end
| A.EXPIF (exp1, exp2, exp3) => raise NotImplemented
end
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
127 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Printer.sml I
structure Printer = struct
local
structure A = Absyn
structure T = Types
structure TC = TypeContext
in
fun prettyPrint expressions =
let
val ppgenParameter =
{spaceString = " ",
newlineString = "\n",
columns = 80}
in
SMLFormat.prettyPrint
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
128 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Printer.sml II
ppgenParameter
expressions
end
fun printExp exp = print (prettyPrint (A.formatexp exp))
fun printTy ty = print (prettyPrint (T.formatty ty))
fun printTypeContext typeContext = print (prettyPrint (TC.fo
end
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
129 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Main.sml I
structure Main = struct
local
structure P = Printer
structure T = Types
structure U = Unify
in
fun mainLoop lexer =
let
val (exp,lexer) = Parser.parse lexer
val lexer = Parser.readChar lexer
val _ = (print "Parse result:\n";
P.printExp exp;
print "\n")
val _ = Typeinf.initPTS()
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
130 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Main.sml II
in
let
val (typeContext, ty) = Typeinf.PTS exp
val _ = (print "Inferred typing:\n";
P.printTypeContext typeContext;
print " |- ";
P.printExp exp;
print " : ";
P.printTy ty;
print "\n")
in
if Parser.isEOF lexer then ()
else mainLoop lexer
end
handle U.Unify => (print "Type error\n";
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
131 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
Main.sml III
if Parser.isEOF lexer then ()
else mainLoop lexer)
end
fun top () =
let
val lexer = Parser.makeLexer()
in
mainLoop lexer
end
end
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
132 / 230
型の解析と型推論
型推論アルゴリズム(1)の実装
課題
...
1
...
...
...
2
3
4
整数に対する以下の算術式の構文を追加せよ.
exp ::= ...
|
exp + exp
|
exp - exp
|
exp * exp
|
exp / exp
2つの要素の組みを任意個の要素の組みに拡張せよ.
組みからの要素取りだし演算#1 等を追加せよ.
型推論アルゴリズムに以下のような印字をする処理を加えよ.
{y:’a} |- y : ’a
{x:’b} |- x : ’b
{y:’c} |- y : ’c
{x:’b , y:’c} |- (x,y) : ’b * ’c
{x:’b , y:’c} |- (y,(x,y)) : ’c * ’b * ’c
{y:’c} |- fn x => (y,(x,y)) : ’b -> (’c * ’b * ’c)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
133 / 230
型の解析と型推論
PTS の分析
PTS の性質
PTS の性質
PTS(e) = (Γ, τ)
の時,Γ ⊢ e : τ が成立.さらに,
任意の型変数の代入 S に対して,S(Γ) ⊢ e : S(τ) が成立
そこで,
PTS(e) の結果は,e の持ちうる型判定のもっとも典型的なもの,
とみることができる.
「多相型」はこの考え方を洗練したもの.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
134 / 230
型の解析と型推論
PTS の分析
PTS の結果の分析 (1):閉じた式の場合 I
例,
PTS(fn x => x) = (∅, t− > t)
実際,以下が成立
∅ ⊢ fn x => x : t -> t
さらに,
∅ ⊢ fn x => x : int -> int
∅ ⊢ fn x => x : string -> string
∅ ⊢ fn x => x : (int int) -> (int -> int)
..
.
すなわち,任意の型 τ に対して.以下の型判定が成立.
∅ ⊢ fn x => x : τ -> τ
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
135 / 230
型の解析と型推論
PTS の分析
PTS の結果の分析 (1):閉じた式の場合 II
そこで,
PTS(fn x => x) = (∅, t → t)
の結果は
fn x => x は,型 t → t の中の t を任意の型で置き換えて得ら
れるすべての型をもつ
という,fn x => x の汎用性を表現していると解釈できる.このような
汎用性を,多相性と呼ぶことにし,論理学の全称命題の記号を使い,
∅ ⊢ fn x => x : ∀(t).t → t
と書く.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
136 / 230
型の解析と型推論
PTS の分析
PTS の結果の分析 (2):自由変数を含む場合 I
次に fn x => (x, y) の例を考えてみよう.
PTS(fn x => (x, y)) = ({y : t}, s → s ∗ t)
したがって,
{y : t} ⊢ fn x => (x, y) : s → s ∗ t
である.この場合, t はこの式の外の変数 y に依存するので,
{y : t} ⊢ fn x => (x, y) : ∀(s, t).s → s ∗ t
とは考えることができない.この式は, s に関してのみ多相性がある
{y : t} ⊢ fn x => (x, y) : ∀(s).s → s ∗ t
と解釈するのが妥当である.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
137 / 230
型の解析と型推論
多相型の推論
多相型型推論規則 I
通常の型の集合に加え,多相型の集合を新たに考え,
σ ::= τ | ∀(t 1 , . . . , t n).τ
変数の型環境は多相型も許すことにする.
Γ ::= {x1 : σ1 , . . . , x n : σ n}
この下で,多相型をもつ変数を使う規則を以下のように定める.
(var)
Γ(x) = ∀(t 1 , . . . , t n).τ0 かつ τ = [τ1 /t 1 , . . . , τ n/t n]τ0
Γ⊢x:τ
この規則は,変数 x の束縛変数は,任意の型に置き換えて使用してよい
ことを意味している.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
138 / 230
型の解析と型推論
多相型の推論
多相型型推論規則 II
他の規則は以前と同様.
(int) Γ ⊢ n : int
(str) Γ ⊢ s : st ring
(app)
Γ ⊢ ex p1 : τ1 → τ2
Γ ⊢ ex p2 : τ1
Γ ⊢ ex p1 ex p2 : τ2
(pair)
Γ ⊢ ex p1 : τ1
Γ ⊢ ex p2 : τ2
Γ ⊢ (ex p1 , ex p2 ) : τ1 ∗ τ2
(abs)
Γ ∪ {x : τ1 } ⊢ ex p1 : τ2
Γ ⊢ fn x => ex p1 : τ1 → τ2
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
139 / 230
型の解析と型推論
多相型の推論
宣言の型推論規則
多相型をもつ変数は宣言で作られる.宣言とその型規則.
dec
(dec)
::=
val id = exp
Γ ⊢ ex p : τ
{t 1 , . . . , t n} = FTV(τ)
Γ ⊢ val x = ex p : Γ ∪ {x : ∀(t 1 , . . . , t n).τ}
トップレベル宣言とその型規則
top
::=
ϵ | top dec
(top-1) ⊢ ϵ : ∅
(top-2)
⊢ t op : Γ1
Γ1 ⊢ dec : Γ2
⊢ t op dec : Γ2
(注) ⊢ t op : Γ なら, t op に自由変数は含まず, FTV(Γ) = ∅ である.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
140 / 230
型の解析と型推論
多相型の型推論アルゴリズム
型推論アルゴリズムの改良
これまでの宣言から得られる型環境を入力とし推論を進める必用がある.
そこで,
式 exp と Γ が与えられた時,S(Γ) ⊢ ex p : τ となる (S, τ) を求
めよ.
の問題を解く型推論アルゴリズムを構築する.
W(Γ, exp) = (S, τ)
ここで,
Γ:現在の型環境
トップレベルですでに定義された変数の型(型変数を含まない)
関数の仮引数の(仮に仮定した)型;最初は型変数
S:関数の仮引数の型への代入
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
141 / 230
型の解析と型推論
多相型の型推論アルゴリズム
簡易版 Milner の型推論アリゴリズム W :式の型
W(Γ, n) = (∅, int)
W(Γ, s) = (∅, string)
W(Γ, x) = if x ∈ dom(Γ) then (∅, freshInst(Γ(x)) else error
W(Γ, fn x => ex p) = let (S1 , τ1 ) = W(Γ{x : t}, ex p1 ) in (S1 , S1 (t) → τ1 )
W(Γ, exp1 ex p2 ) = let (S1 , τ1 ) = W(Γ, ex p1 );
(S2 , τ2 ) = W(S1 (Γ), ex p2 );
S3 = U({(S2 (τ1 ), τ2 → t)})
in (S3 ◦ S2 ◦ S1 , S3 (t))
W(Γ, (exp1 , ex p2 )) = let (S1 , τ1 ) = W(Γ, ex p1 ); (S2 , τ2 ) = W(S1 (Γ), exp2 )
in (S2 ◦ S1 , S2 (τ1 ) × τ2 )
freshInst(∀(t 1 , . . . , t n).τ) = [t 1′ /t 1 , . . . , t ′n/t n]τ
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
( t ′ , . . . , t ′n fresh)
1
142 / 230
型の解析と型推論
多相型の型推論アルゴリズム
簡易版 Milner の型推論アリゴリズム W :宣言の型
宣言の型推論の基本的構造:
W t op(Γ, val x = ex p) =
let
(S, τ) = W(Γ, exp)
{t 1 , . . . , t n} = FTV(τ)
in
Γ ∪ {x : ∀(t 1 , . . . , t n).τ}
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
143 / 230
型の解析と型推論
多相型の型推論アルゴリズム
課題
「簡易版」ではない完全な ML の型推論アルゴリズムでは,トップレベル
の宣言の代りに,以下の「多相型 let 式」をもつ.
exp
::=
|
···
let id = exp in exp end
この式は以下の型付け規則に従う.
(let)
Γ ⊢ ex p1 : τ1
{t 1 , . . . , t n} = FTV(τ1 ) \ FTV(Γ)
Γ ∪ {x : ∀(t 1 , . . . , t n).τ1 } ⊢ ex p2 : τ2
Γ ⊢ let x = ex p1 in ex p2 end : τ2
「宣言」はこの多相型 let 構文の特殊な場合であり,導入する必用はない.
多相型 let 構文が扱えるように W を拡張し,実装せよ.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
144 / 230
コンパイラバックエンド
講義内容
.
. .7 コンパイラバックエンド
インタープリタとコンパイラ
操作的意味の定義
インタープリタの実装
再帰関数の実現
パターンマッチングの実現
コンパイルの枠組み
計算機のモデル:SECD 機械
SECD 機械語コードへのコンパイル
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
145 / 230
コンパイラバックエンド
インタープリタとコンパイラ
インタープリタとコンパイラ
フロントエンド:
1
2
3
コンパイル処理
字句解析
構文解析
型の解析
出力
トークン列
構文木
型付きラムダ計算
...
インタープリタ
型付きラムダ計算を解釈実行するプログラムを作成.
...
コンパイラ
フロントエンドに続き,以下のステップを実行
コンパイル処理 出力
4 疑似コード生成 疑似コード
5 コード生成
機械語コード
1
2
得られた機械語コードをハードウエアで実行.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
146 / 230
コンパイラバックエンド
インタープリタとコンパイラ
インタープリタのとコンパイラの性質
インタープリタ
実現が簡単
言語の意味の定義としての役割を果たす.
コンパイラ
対象とする機械により複雑な処理が必用
高速な実行
複雑な言語の場合,以下の手順をとることが多い.
その言語の操作的意味を書き下す.
操作的意味を実現するインタープリタを実装し動作を確認
コンパイラを実装
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
147 / 230
コンパイラバックエンド
操作的意味の定義
型付きラムダ計算の操作的意味の定義
以下の型付きラムダ式を考える.
e ::= x | c | fn x => e | e e | (e,e)
|
add(e,e) | sub(e,e) | mul(e,e) | div(e,e) | eq(e,e)
静的型判定
Γ⊢e:τ
に対応する動的な意味を,以下の関係として定義する.
E⊢e⇓v
ここで,
E:実行時環境
e:評価対象式
v:実行結果の値
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
148 / 230
コンパイラバックエンド
操作的意味の定義
式の操作的意味の定義
実行時の値の定義
v ::= c | (v, v) | Cls(E, x, e)
ここで,Cls(E, x, e) は環境が E であるときに定義された関数 fn x => e
を表す値.関数閉包(function closure)と呼ばれる.
環境 E は,関数本体 e に含まれる変数の値を保持する.
例えば,
val x = 2;
fn y => y + x;
の時.関数式 fn y => y + x の値は Cls({x 7→ 2}, y, y + x) なる関数閉
包でである.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
149 / 230
コンパイラバックエンド
操作的意味の定義
操作的意味の定義
(const) E ⊢ c ⇓ c
(var) E ⊢ x ⇓ E(x)
(fn) E ⊢ fn x => e ⇓ Cls(E, x, e)
(app)
E ⊢ e1 ⇓ Cls(E0 , x0 , e0 )
E ⊢ e2 ⇓ v0
E ⊢ e1 e2 ⇓ v
(pair)
E ⊢ e1 ⇓ v1
E ⊢ e2 ⇓ v2
E ⊢ (e1 , e2 ) ⇓ (v1 , v2 )
(add)
E ⊢ e1 ⇓ n1
E ⊢ e2 ⇓ n2
E ⊢ add(e1 ,e2 ) ⇓ n1 + n2
(eq)
E ⊢ e1 ⇓ n1
E ⊢ e2 ⇓ n2
E ⊢ eq(e1 ,e2 ) ⇓ b
大堀 淳 (東北大学 電気通信研究所)
{
b=
コンパイラ講義資料
E0 {x 7→ v0 } ⊢ e0 ⇓ v
t rue n1 = n2
f alse n1 , n2
150 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 I
以上の操作的意味をそのままプログラムすると,インタープリタが実現
できる.
v ::= c | (v, v) | Cls(E, x, e)
datatype value
= INT of int
| BOOL of bool
| STRING of string
| PAIR of value * value
| CLOSURE of env * string * Absyn.exp
withtype env = value StringMap.map
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
151 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 II
E⊢e⇓v
structure A = Absyn
structure V = Values
fun eval exp env =
case exp of
(const) E ⊢ c ⇓ c
A.INT int => V.INT int
| A.STRING string => V.STRING string
| A.BOOL bool => V.BOOL bool
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
152 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 III
(var) E ⊢ x ⇓ E(x)
| A.EXPID string =>
(case StringMap.find(env, string) of
SOME v => v
| _ => raise RuntimeError
)
(fn) E ⊢ fn x => e ⇓ Cls(E, x, e)
| A.EXPFN (string, exp) => V.CLOSURE(env, string, exp)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
153 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 IV
(app)
E ⊢ e1 ⇓ Cls(E0 , x0 , e0 )
E ⊢ e2 ⇓ v0
E ⊢ e1 e2 ⇓ v
E0 {x 7→ v0 } ⊢ e0 ⇓ v
| A.EXPAPP (exp1, exp2) =>
let
val v1 = eval exp1 env
val v2 = eval exp2 env
in
case v1 of
V.CLOSURE(env1, id1, exp1) =>
eval exp1 (StringMap.insert(env1, id1, v2))
| _ => raise RuntimeError
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
154 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 V
(pair)
E ⊢ e1 ⇓ v1
E ⊢ e2 ⇓ v2
E ⊢ (e1 , e2 ) ⇓ (v1 , v2 )
| A.EXPPAIR (exp1, exp2) =>
let
val v1 = eval exp1 env
val v2 = eval exp2 env
in
V.PAIR(v1,v2)
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
155 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 VI
(add)
E ⊢ e1 ⇓ n1
E ⊢ e2 ⇓ n2
E ⊢ add(e1 ,e2 ) ⇓ n1 + n2
| A.EXPADD (exp1, exp2) =>
let
val v1 = eval exp1 env
val v2 = eval exp2 env
in
case (v1,v2) of
(V.INT i1, V.INT i2) => V.INT (i1 + i2)
| _ => raise RuntimeError
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
156 / 230
コンパイラバックエンド
インタープリタの実装
インタプリタの実現 VII
(eq)
E ⊢ e1 ⇓ n1
E ⊢ e2 ⇓ n2
E ⊢ eq(e1 ,e2 ) ⇓ b
{
b=
t rue n1 = n2
f alse n1 , n2
| A.EXPEQ (exp1, exp2) =>
let
val v1 = eval exp1 env
val v2 = eval exp2 env
in
case (v1,v2) of
(V.INT i1, V.INT i2) => if i1 = i2 then
V.BOOL true
else V.BOOL false
| _ => raise RuntimeError
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
157 / 230
コンパイラバックエンド
インタープリタの実装
宣言の評価
(val)
E⊢e⇓v
E ⊢ val x = e ⇓ E{x 7→ v}
fun mainLoop env lexer =
let
val (top,lexer) = Parser.parse lexer
val lexer = Parser.readChar lexer
val v = E.eval exp env
val newEnv = StringMap.insert(env, id,
in
if Parser.isEOF lexer then ()
else mainLoop newEnv lexer
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
v)
158 / 230
コンパイラバックエンド
再帰関数の実現
再帰関数の実現(1)
:文法の追加
...
1
再帰的関数定義の追加
fun f x = e
val f = fn x => eとの違いは, f を e の中で使用してもよい点.
..2 式の拡張
再帰的関数定義を系統的に実現するために,以下の式を導入.
.
e ::= · · · | fix f (x) => e
fix f (x) => e は,直感的には,自分自身を f として受け取り,
fn x => eとなる関数.
...
3
以下の変換を行う.
変換前
fun f x = e
大堀 淳 (東北大学 電気通信研究所)
変換後
val f = fix f (x) => e
コンパイラ講義資料
159 / 230
コンパイラバックエンド
再帰関数の実現
fun 構文の展開
fun mainLoop gamma env lexer =
let
val (top,lexer) = Parser.parse lexer
val lexer = Parser.readChar lexer
val (id, exp) =
case top of
A.EXP exp => ("it", exp)
| A.DEC (A.FUN(fid, id, exp)) =>
(fid, A.EXPREC(fid,id,exp))
| A.DEC (A.VAL bind) => bind
...
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
160 / 230
コンパイラバックエンド
再帰関数の実現
再帰関数の実現(2)
:型規則と型推論
(fix)
Γ{ f : τ1 → τ2 , x : τ1 } ⊢ ex p : τ2
Γ ⊢ fix f (x) => ex p : τ1 → τ2
| A.EXPREC (f, x, exp) =>
let
val argty = T.newTy()
val funty = T.newTy()
val newGamma =
StringMap.insert
(StringMap.insert(gamma, f, funty), x, argty)
val (S1, ty) = W newGamma exp
val S2 = U.unify [(TC.substTy S1 funty,
T.FUNty(TC.substTy S1 argty, ty))]
in
(S2 & S1,TC.substTy (S2 & S1) funty)
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
161 / 230
コンパイラバックエンド
再帰関数の実現
再帰関数の実現(3)
:操作的意味論と評価関数 I
値の定義の拡張
v ::= · · · | Rec(E, f, x, e)
fix 式の評価規則の追加
(fn) E ⊢ fix f (x) => e ⇓ Rec(E, f, x, e)
fix 式の評価関数
| A.EXPREC (string1, string2, exp) =>
V.RECCLOSURE(env, string1, string2,
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
exp)
162 / 230
コンパイラバックエンド
再帰関数の実現
再帰関数の実現(3)
:操作的意味論と評価関数 II
関数適用の規則の追加
(app)
E ⊢ e1 ⇓ Rec(E0 , f0 , x0 , e0 )
E ⊢ e2 ⇓ v0
E0 { f 7→ Rec(E0 , f0 , x0 , e0 ), x 7→ v0 } ⊢ e0 ⇓ v
E ⊢ e1 e2 ⇓ v
| A.EXPAPP (exp1, exp2) =>
let val v1 = eval exp1 env
val v2 = eval exp2 env
in case v1 of
V.CLOSURE(env, id1, exp1) => ...
| V.RECCLOSURE(env1, fid, id1, exp1) =>
eval exp1 (StringMap.insert
(StringMap.insert(env1,fid, v1),id1,v2))
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
163 / 230
コンパイラバックエンド
再帰関数の実現
課題
インタープリタを以下の言語に拡張せよ.
大堀 淳 (東北大学 電気通信研究所)
exp
::=
dec
|
::=
|
···
let decl in exp
val id = exp
fun id id = exp end
コンパイラ講義資料
164 / 230
コンパイラバックエンド
パターンマッチングの実現
パッターンマッチング(1)
:文法の追加
...
パターン構文の導入
...
関数式の変更と case 式の追加
1
2
p ::= x | c | ( p, p)
e
::=
|
...
3
· · · | fn p => e
case e of p1 => e1 | · · · | pn => e n
宣言の変更
dec
::=
|
大堀 淳 (東北大学 電気通信研究所)
val p = exp
fun p id = exp end
コンパイラ講義資料
165 / 230
コンパイラバックエンド
コンパイルの枠組み
疑似コードの生成
型付きラムダ計算の処理系より実際のデジタル計算機により近い近い
「抽象的な機械」を考え,その機械が理解する言語に変換する.
抽象機械
操作的意味論
擬似コード生成系
擬似コード
ラムダ計算
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
166 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械
典型的かつ歴史的に重要な抽象機械
P.J. Landin, ”The Mechanical Evaluation of Expressions”, The
Computer Journal, 6:308–320, 1964
特徴
演算はすべてスタックを用いて行う
変数の値を格納する環境を装備
関数呼び出しをプリミティブとしてサポート
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
167 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の構造
SECD 機械の状態: (S, E, C, D)
S:スタック(演算のための記憶装置)
E:環境(値の束縛を保持)
C:命令列
D:ダンプ(関数呼び出しのためのスタック)
S
::=
nil | V ::S
V
::=
c | Cls(E, x, C) | Rec(E, f, x, C) | (V, V)
E
::=
{x1 : V1 , . . . , x n : V n}
C
::=
nil | I::C
I
::=
Push(c) | Acc(x) | MakeCls(x, C) | MakeRec( f, x, C) |
App | Add | Sub | Mul | Div | Eq | Return | Pair | IF(C, C)
D
::=
nil | (E, C):: D
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
168 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の実装 I
datatype value
= INT of int
| BOOL of bool
| STRING of string
| PAIR of value * value
| CLOSURE of env * string * S.code
| RECCLOSURE of env * string * string * S.code
withtype env = value StringMap.map
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
169 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の実装 II
datatype inst
= PUSHINT of int
| PUSHSTRING of string
| PUSHBOOL of bool
| ACC of string
| APPLY
| PAIR
| ADD | SUB | MUL | DIV | EQ
| MAKECLS of string * code
| MAKEREC of string * string * code
| IF of code * code
| RETURN
withtype code = inst list
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
170 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 I
命令列 C の先頭の命令を読み,S, E. D の内容を変更する.
(S, E, C, D) −→ (S′ , E′ , C′ , D′ )
structure I = Instructions
structure V = Values
exception RuntimeError
fun exec (S, E, C, D) = exec (S’, E’, C’, D’)
| ...
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
171 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 II
演算命令:
(i1 ::i2 ::S, E, Add::C, D) −→ ((i2 + i1 )::S, E, C, D)
(i1 ::i2 ::S, E, Sub::C, D) −→ ((i2 − i1 )::S, E, C, D)
(i1 ::i2 ::S, E, Mul::C, D) −→ ((i2 ∗ i1 )::S, E, C, D)
(i1 ::i2 ::S, E, Div::C, D) −→ ((i2 /i1 )::S, E, C, D)
(i1 ::i2 ::S, E, Eq::C, D) −→ (t rue::S, E, C, D) (if i2 = i1 )
(i1 ::i2 ::S, E, Eq::C, D) −→ ( f alse::S, E, C, D) (if i2 , i1 )
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
172 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 III
| exec (V.INT i1:: V.INT i2::S, E, I.ADD :: C, D) =
exec (V.INT(i2 + i1)::S, E, C, D)
| exec (V.INT i1:: V.INT i2::S, E, I.SUB :: C, D) =
exec (V.INT(i2 - i1)::S, E, C, D)
| exec (V.INT i1:: V.INT i2::S, E, I.MUL :: C, D) =
exec (V.INT(i2 * i1)::S, E, C, D)
| exec (V.INT i1:: V.INT i2::S, E, I.DIV :: C, D) =
exec (V.INT(i2 div i1)::S, E, C, D)
| exec (V.INT i1:: V.INT i2::S, E, I.EQ :: C, D) =
exec (V.BOOL(i2 = i1)::S, E, C, D)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
173 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 IV
スタック操作:
(S, E, Push( c)::C, D) −→ (c::S, E, C, D)
(v1 ::v2 ::S, E, Pair::C, D) −→ ((v2 , v1 )::S, E, C, D)
| exec
exec
| exec
exec
| exec
exec
| exec
exec
(S, E, I.PUSHINT int :: C, D) =
(V.INT int::S, E, C, D)
(S, E, I.PUSHSTRING string :: C, D) =
(V.STRING string::S, E, C, D)
(S, E, I.PUSHBOOL bool :: C, D) =
(V.BOOL bool::S, E, C, D)
(v1::v2::S, E, I.PAIR :: C, D) =
(V.PAIR(v2, v1)::S, E, C, D)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
174 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 V
分岐:
(t rue::S, E, IF(C1 ,C2 )::C, D) −→ (S, E, C1 @C, D)
( f alse::S, E, IF(C1 ,C2 )::C, D) −→ (S, E, C2 @C, D)
| exec
exec
| exec
exec
(V.BOOL true::S, E, I.IF(C1,C2) :: C, D) =
(S, E, C1 @ C, D)
(V.BOOL false::S, E, I.IF(C1,C2) :: C, D) =
(S, E, C2 @ C, D)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
175 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 VI
変数参照
(S, E{x : v}, Acc( x)::C, D) −→ (v::S, E, C, D)
| exec (S, E, I.ACC string :: C, D) =
(case StringMap.find(E, string) of
SOME v => exec (v::S, E, C, D)
| _ => raise RuntimeError
)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
176 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 VII
クロージャ生成
(S, E, MakeCls(x,C0 )::C, D) −→ (Cls(E, x, C0 )::S, E, C, D)
(S, E, MakeRec(f, x,C0 )::C, D) −→ (Rec(E, f, x, C0 )::S, E, C, D)
| exec
exec
| exec
exec
(S, E, I.MAKECLS(x,C0) :: C, D) =
(V.CLOSURE(E, x, C0)::S, E, C, D)
(S, E, I.MAKEREC(f, x, C0) :: C, D) =
(V.RECCLOSURE(E, f, x, C0)::S, E, C, D)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
177 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 VIII
関数呼び出し
(v1 ::Cls(E0 , x, C0 )::S, E, App::C, D) −→ (S, E0 {x : v0 }, C0 , (E, C):: D)
(v1 :: Rec(E0 , f, x, C0 )::S, E, App::C, D) −→
(S, E0 { f : Rec(E0 , f, x, C0 ), x : v0 }, C0 , (E, C):: D)
| exec (v::V.CLOSURE(E0, x, C0)::S, E, I.APPLY :: C, D) =
exec (S, StringMap.insert(E0,x,v), C0, (C,E)::D)
| exec (v1::(v2 as V.RECCLOSURE(E0, f, x, C0))::S, E,
I.APPLY :: C, D) =
exec (S, StringMap.insert(StringMap.insert(E0,f,v2),x,v1),
C0, (C,E)::D)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
178 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作の定義と実装 IX
関数からの復帰
(S, E, Return::C, (E0 , C0 ):: D) −→ (S, E0 , C0 , D)
| exec (v::S, _, I.RETURN :: C, (C0, E0)::D) =
exec (v::S, E0, C0, D)
プログラム終了
(v::S, E, Return::C, nil) −→ v
| exec (v::S, _, I.RETURN :: C, nil) = v
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
179 / 230
コンパイラバックエンド
計算機のモデル:SECD 機械
SECD 機械の動作例
講義にて紹介.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
180 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル I
戦略:
各部分項を SECD のコード列にコンパイル
各部分項の結果をスタックに(逆順に)プッシュ
スタック上の部分項の結果を用いて演算
[[e]] = C
structure Comp = struct
local
structure A = Absyn
structure I = Instructions
in
fun comp absyn =
case absyn of
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
181 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル II
定数:
[[c]] = [Const(c)]
A.INT (int) => [I.PUSHINT int]
| A.STRING (string) => [I.PUSHSTRING string]
| A.BOOL (bool) => [I.PUSHBOOL bool]
| A.EXPID (string) => [I.ACC string]
変数
[[x]] = [Acc(x)]
| A.EXPID (string) => [I.ACC string]
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
182 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル III
分岐
[[if e0 then e1 else e2 ]] = [[e0 ]]@[IF([[e1 ]],[[e2 ]])]
| A.EXPIF (exp1, exp2, exp3) =>
let
val C1 = comp exp1
val C2 = comp exp2
val C3 = comp exp3
in
C1 @ [I.IF(C2, C3)]
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
183 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル IV
算術演算
[[add(e1 ,e2 )]] = [[e1 ]]@[[e2 ]]@[Add]
| A.EXPADD (exp1, exp2) =>
let
val C1 = comp exp1
val C2 = comp exp2
in
C1 @ C2 @ [I.ADD]
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
184 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル V
関数式
[[fn x => e]] = [MakeCls(x,[[e]]@[Return])]
| A.EXPFN (string, exp) =>
let
val C = comp exp
in
[I.MAKECLS(string, C @ [I.RETURN])]
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
185 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル VI
再帰的関数式
[[fix f(x) => e]] = [MakeRec( f , x, [[e]]@[Return])]
| A.EXPREC (string1, string2, exp) =>
let
val C = comp exp
in
[I.MAKEREC(string1, string2, C @ [I.RETURN])]
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
186 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル VII
関数適用
[[e1 e2 ]] = [[e1 ]]@[[e2 ]]@[App]
| A.EXPAPP (exp1, exp2) =>
let
val C1 = comp exp1
val C2 = comp exp2
in
C1 @ C2 @ [I.APPLY]
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
187 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
SECD 機械語コードへのコンパイル VIII
組み
[[(e1 , e2 )]] = [[e1 ]]@[[e2 ]]@[Pair]
| A.EXPPAIR (exp1, exp2) =>
let
val C1 = comp exp1
val C2 = comp exp2
in
C1 @ C2 @ [I.PAIR]
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
188 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
コンパイルの正しさ(補足)
ラムダ式の操作的意味論の値を SECD 機械の値に以下のように翻訳する.
c= c
cls(E, x, e) = Cls(E, x, [[e]]@[Return])
rec(E, f, x, e) = Rec(E, f, x, [[e]]@[Return])
(v1 , v2 ) = (v1 , v2 )
E = {x : E(x) | x ∈ dom(E)}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
.
.
.
以下の関係が示せる.
.
Theorem
..
∗
もし
E ⊢ e ⇓ v なら (S, E, [[e]]@C, D) −→ (v::S, E, C, D) である.
.
..
∗
従って, E ⊢ e ⇓ v なら (S, E, [[e]], nil) −→ v である.
189 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
コンパイラメインループ
fun mainLoop gamma env lexer =
let
val (top,lexer) = Parser.parse lexer
...
in
let
...
val code = (C.comp exp)@[I.RETURN]
val v = E.exec (nil, env, code, nil)
val newEnv = StringMap.insert(env, id,
in
if Parser.isEOF lexer then ()
else mainLoop newGamma newEnv lexer
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
v)
190 / 230
コンパイラバックエンド
SECD 機械語コードへのコンパイル
課題
...
必用なら文献(大堀 他,コンピュータサイエンス入門 アルゴリズム
とプログラミング言語,岩波書店等)を参考に,コンパイルの正し
さを示す前の定理を証明せよ.
.2. 実際のコードでは,IF 等の分岐命令は適当なコード列に分岐する.
そこで,コンパイラに以下の改良を加えよ.
1
.
..1.
SECD 機械にラベル付きコードと分岐命令の追加
I
::=
· · · | Jump(l) | Iftrue(l)
C
::=
nil | I :: C | l : C
jump(l) は, l とラベル付けられたコードブロックに分岐する.
Iftrue(l) は,スタックトップにある値が true なら l のラベルを持つ
コードブロックに分岐する. l : C は l というラベルをもつコードブ
ロックである.
..2. if 構文に対する翻訳アルゴリズムを改良し,上記のコードを生成する
ようにせよ.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
191 / 230
現実のコンパイラ
講義内容
.
. .8 現実のコンパイラ
種々の高度な機能のコンパイル
コンパイラの構成の例:SML#
コンパイル段階の例
種々の高度な機能のコンパイル例
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
192 / 230
現実のコンパイラ
種々の高度な機能のコンパイル
種々の高度な機能のコンパイル
SML #なんどの現実の高機能言語のコンパイルには,以下のような種々
の高度な処理が要求される.
派生構文の展開
モジュールのコンパイル
データ型のコンパイル
パターンマッチングのコンパイル
最適化処理
関数定義の最適化
Uncurry 変換
型主導の最適化
インライン展開
関数融合
コードレベルの最適化
結果表示コードの生成
.
.
.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
193 / 230
現実のコンパイラ
コンパイラの構成の例:SML#
SML#コンパイラの中間言語
...
...
...
...
...
...
...
...
...
...
...
...
1
抽象構文木
2
型なしのパターン言語
3
型変数のスコープを明示した型なしのパターン言語
4
型付きパターン言語
5
フラットな型付きパターン言語
6
多相型レコード計算
7
型付きラムダ計算
8
型付きビットマップパッシング計算
9
型付き A-Normal 式
10
SML#シンボリックコード
11
SML#命令列
12
SML#バイトコード言語
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
194 / 230
現実のコンパイラ
コンパイラの構成の例:SML#
SML#コンパイラの処理ステップ
...
...
...
...
...
...
...
...
1
構文解析
2
派生構文の展開
3
関数定義の最適化
4
5
ユーザ定義型変数の解釈
型推論
6
Uncurry 変換
7
プリントコード生成
8
モジュールコンパイル
大堀 淳 (東北大学 電気通信研究所)
...
パターンマッチングコンパ
イル
...
...
...
...
...
...
...
10
多相型レコードコンパイル
11
ビットマップ/Closure 変換
12
A-Normal 変換
13
A-Normal 最適化
14
抽象コードへの変換
15
抽象コード最適化
16
アセンブル
9
コンパイラ講義資料
195 / 230
現実のコンパイラ
コンパイラの構成の例:SML#
SML#のコンパイルステップの表示
以上の各ステップの様子は,SML#コンパイラに以下のようなスイッチを
与えることで見ることができる.
smlsharp --xswitchTrace=yes
--xprintSource=yes
\
--xprintPL=yes
\
--xprintTP=yes
\
--xprintRC=yes
\
--xprintTL=yes
\
--xprintTFP=yes
\
--xprintAN=yes
\
--xprintBUC=yes
\
--xprintUC=yes
\
--xprintIS=yes
\
--xprintLS=yes
\
--xskipPrinter=yes
大堀 淳 (東北大学 電気通信研究所)
\
コンパイラ講義資料
196 / 230
現実のコンパイラ
コンパイル段階の例
構文解析
入力文字列 =⇒ 抽象構文木
fun fib 0 = 1
| fib 1 = 1
| fib n = fib (n - 1) + fib (n - 2);
Source expr:
fun fib 0 = 1
| fib 1 = 1
| fib n = fib (n - 1) + fib (n - 2)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
197 / 230
現実のコンパイラ
コンパイル段階の例
派生構文の展開
抽象構文木 =⇒ 型なしのパターン言語
Elaborated:
fun fib 0 = 1
| fib 1 = 1
| fib n = +((fib (-(n, 1))), (fib (-(n, 2))))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
198 / 230
現実のコンパイラ
コンパイル段階の例
型推論
型無しのパターン言語(2) =⇒ 型付きパターン言語
Statically evaluated:
fun fib:int -> int 0 = 1
| fib 1 =1
| fib n:int = +((fib (-(n, 1), (fib(-(n, 2))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
199 / 230
現実のコンパイラ
コンパイル段階の例
パターンマッチングコンパイル I
フラットな型付きパターン言語 =⇒ 多相型レコード計算
val rec fib : int -> int =
(fn $12 : int =>(switch $12 : int
of 0 => 1
| 1 => 1
| _ => ))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
200 / 230
現実のコンパイラ
コンパイル段階の例
ビットマップ/Closure 変換
型付きラムダ計算 =⇒ 型付きビットマップパッシング計算
BUC transformed:
local
val rec 80 : int -> int =
fun {tyvars =(), bitmapFree =0wx0, tagArgs=(),
sizevals=(), args=(75:int),resultTy=int}
=> switch 75
of 0 => 1
| 1 => 1
| _ => addInt(RecCall(80, (subInt(75,1)) ),
RecCall(80, (subInt(75,2)) ))
val 81:BOXEDty = (bitmap=0wx0;totalsize=0wx0;sizes=()())
in
val 74:int -> int = Closure( 80, 81 )
end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
201 / 230
現実のコンパイラ
コンパイル段階の例
A-Normal 変換 I
型付きビットマップパッシング計算 =⇒ A-Normal 式
let rec 80
{tyvars =
code =
switch
of 0
| 1
| _
=
(), ...
arg(75)
=> 1
=> 1
=> let 82: ATOM = 1 in
let 83 : ATOM = subInt(arg(75),82) in
let 84 : ATOM = 0wx1 in
let 85 : ATOM = RecCall (80,83) in
let 86 : ATOM = 2 in
let 87 : ATOM = subInt(arg(75),86) in
let 88 : ATOM = RecCall ((80,87) in
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
202 / 230
現実のコンパイラ
コンパイル段階の例
A-Normal 変換 II
addInt(85,88)
}
in let 89
let 81
let 74
let 90
Return
:
:
:
:
ATOM = 0wx0 in
BOXED = (bitmap=89;size=89;( );( )) in
BOXED = Closure(80,81) in
ATOM = SetGlobalValue((0x6,0x15d) = 74) in
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
203 / 230
現実のコンパイラ
コンパイル段階の例
A-Normal 式最適化 I
A-Normal 式 =⇒ A-Normal 式
Anormal optimized:
let rec 80 =
{tyvars = (), ...
code =
switch arg(75)
of 0 => 1
| 1 => 1
| _ => let 82
let 83
let 84
let 85
let 86
let 87
大堀 淳 (東北大学 電気通信研究所)
:
:
:
:
:
:
ATOM
ATOM
ATOM
ATOM
ATOM
ATOM
=
=
=
=
=
=
1 in
subInt(arg(75),1) in
0wx1 in
RecCall (80,83) in
2 in
subInt(arg(75),2) in
コンパイラ講義資料
204 / 230
現実のコンパイラ
コンパイル段階の例
A-Normal 式最適化 II
let 88 : ATOM = RecCall (80,87) in
addInt(85,88)
}
in let 89
let 81
let 74
let 90
Return
:
:
:
:
ATOM = 0wx0 in
BOXED = (bitmap=89;size=89;( );( )) in
BOXED = Closure(80,81) in
ATOM = SetGlobalValue((0x6,0x15d) = 74) in
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
205 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード列 I
A-Normal 式 =⇒ 疑似コード列
Linearized:
{
V93
{
args = [],
bitmapvals = {args = [], frees = []},
pointers = [V74, V81],
atoms = [V90, V89],
doubles = [],
records = []
}
V89 = LoadWord 0x0
V81 = MakeBlock 0x0 V89 V89 [] []
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
206 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード列 II
V74 = MakeClosure L80 V81
SetGlobal( 0x6 , 0x15d , V74 )
Exit
}
{
V80
{
args = [V75],
bitmapvals = {args = [], frees = []},
pointers = [],
atoms =
[V75,V95,V88,V87,V86,V85,V84,V83,V82,V97,V99],
doubles = [],
records = []
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
207 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード列 III
}
SwitchInt V75 0x2 [{0 => L96},{1 => L98}] L94
L96:
V97 = LoadInt 1
Return V97 S
L98:
V99 = LoadInt 1
Return V99 S
L94:
V82
V83
V84
V85
V86
V87
=
=
=
=
=
=
LoadInt 1
SubInt_Const_2( V75 , 1 )
LoadWord 0x1
SelfRecursiveCallStatic_M 0x1 L80 [V83] [V84]
LoadInt 2
SubInt_Const_2( V75 , 2 )
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
208 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード列 IV
V88 = SelfRecursiveCallStatic_M 0x1 L80 [V87] [V84]
V95 = CallPrim 0x2 addInt [V85,V88] [S,S] S
Return V95 S
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
209 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード最適化 I
疑似コード列 =⇒ 疑似コード列
SymbolicInstructions Optimized:
{
V93
{ args = [],
bitmapvals = {args = [], frees = []},
pointers = [V74, V81],
atoms = [V90, V89],
doubles = [],
records = []}
V81 = LoadEmptyBlock
V74 = MakeClosure L80 V81
SetGlobal( 0x6 , 0x15d , V74 )
Exit
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
210 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード最適化 II
}
{ V80
{ args = [V75],
bitmapvals = {args = [], frees = []},
pointers = [],
atoms =
[V75,V95,V88,V87,V86,V85,V84,V83,V82,V97,V99],
doubles = [],
records = []}
SwitchInt V75 0x2 [{0 => L96},{1 => L98}] L94
L96:
V97 = LoadInt 1
Return V97 S
L98:
V99 = LoadInt 1
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
211 / 230
現実のコンパイラ
コンパイル段階の例
疑似コード最適化 III
Return V99 S
L94:
V83 = SubInt_Const_2( V75 , 1 )
V85 = SelfRecursiveCallStatic_S L80 V83 S
V87 = SubInt_Const_2( V75 , 2 )
V88 = SelfRecursiveCallStatic_S L80 V87 S
V95 = CallPrim 0x2 addInt [V85,V88] [S,S] S
Return V95 S
}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
212 / 230
現実のコンパイラ
コンパイル段階の例
アセンブル I
疑似コード列 =⇒ SML #抽象機械命令列
Assembled:
FunEntry{frameSize = 0xa,
startOffset = 0x9,
arity = 0x0,
argsdest = [],
bitmapvalsFreesCount = 0x0,
bitmapvalsFrees = [],
bitmapvalsArgsCount = 0x0,
bitmapvalsArgs = [],
pointers = 0x3, atoms = 0x3,
recordGroupsCount = 0x0,
recordGroups = []}
LoadEmptyBlock{destination = 0x7}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
213 / 230
現実のコンパイラ
コンパイル段階の例
アセンブル II
MakeClosure{entryPoint = 0x14, ENVOffset = 0x7, destination
SetGlobal_S{globalArrayIndex = 0x6, offset = 0x15d, variable
Exit
FunEntry{frameSize = 0x10,
startOffset = 0x1e,
arity = 0x1,
argsdest = [0x6],
bitmapvalsFreesCount = 0x0,
bitmapvalsFrees = [],
bitmapvalsArgsCount = 0x0,
bitmapvalsArgs = [],
pointers = 0x1,
atoms = 0xb,
recordGroupsCount = 0x0,
recordGroups = []}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
214 / 230
現実のコンパイラ
コンパイル段階の例
アセンブル III
SwitchInt{targetOffset = 0x6, casesCount = 0x2, cases = [0,
LoadInt{value = 1, destination = 0xf}
Return_S{variableOffset = 0xf}
LoadInt{value = 1, destination = 0x10}
Return_S{variableOffset = 0x10}
SubInt_Const_2{argIndex1 = 0x6, argValue2 = 1, destination =
SelfRecursiveCallStatic_S{entryPoint = 0x14, argOffset = 0xd
SubInt_Const_2{argIndex1 = 0x6, argValue2 = 2, destination =
SelfRecursiveCallStatic_S{entryPoint = 0x14, argOffset = 0x9
AddInt{argIndex1 = 0xb, argIndex2 = 0x8, destination = 0x7}
Return_S{variableOffset = 0x7}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
215 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
相互再帰関数の最適化
Elaborated:
fun f 0 = 0 | n = g (+((h (-(n, 1))), n))
and g x = x
and h 0 = 1 | n = +(n, (f (-(n, 1))))
VAL REC optimize:
nonrecfun g x = x
fun h 0 = 1 | n = +(n, (f (-(n, 1))))
and f 0 = 0 | n = g (+((h (-(n, 1))), n))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
216 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
Uncurry 変換 I
Elaborated:
fun sum n =
let fun sum’ 0 r = r
| sum’ n r = sum’ (-(n, 1)) (+(r, 1))
in sum’ n 0 end
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
217 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
Uncurry 変換 II
Uncurying Optimized:
val sum =
(fn $22:int =>
(case $22 of
n =>
let
val rec sum’ =
(fn {$24:int, $23:int} =>
(case {$24, $23}
of {0,r} => r
| {n,r} => sum’ {(-(n, 1), +(r, 1))}
in
sum’ {n,0}
end)
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
218 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
モジュールコンパイル I
struct
fun fib 0
| fib 1
| fib n
end;
Sample.fib
= 1
= 1
= fib (n - 1) + fib (n - 2)
3;
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
219 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
モジュールコンパイル II
Module Compiled:
val rec Sample.fib =
(fn {$0} =>
(case {$0}
of {0} => 1
| {1} => 1
| {n} =>+(fib {(-(n, 1)}, fib{(-(n, 2)}
)
SetGlobalValue((0x6,346) = Sample.fib
val it : int = GetGlobalValue(0x6,346) {3}
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
220 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
型主導レコードコンパイル I
fun makeGreeting {name= {first = "David", ...},...} =
"Hi, Dave"
| makeGreeting {name = {last,...}, ...} =
"Dear Mr./Ms." ˆ last;
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
221 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
型主導レコードコンパイル II
Recor Compiled to:
val makeGreeting =
[’a#{name:’b},’b#{first:string, last:string}.
fn {$175, $174, $173, $167} =>
bind $170 = $167[$175]
in bind $171 = $170[$174]
in switch $171
of "David" => "Hi, Dave"
| _ =>
bind last = $170[$173]
in "Dear Mr./Ms." ˆ last
end
end
end
]
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
222 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
ユーザ定義データ型のコンパイル I
val L = [1,2];
fun length nil = 0
| length h :: t = 1 + length t
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
223 / 230
現実のコンパイラ
種々の高度な機能のコンパイル例
ユーザ定義データ型のコンパイル II
Record Compiled:
val L : int list = {1, 1, {1, 2, {0}}}
[’a.
val rec length : ’a list -> int =
fn $0 : ’a list =>
switch $0[0]
of 0 => 0
| 1 =>
bind t = $0[2]
in (addInt(1,length t))
end
| _ => (raise {2, "MATCHCOMPILERBUG"})
]
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
224 / 230
要点の復習
講義内容
.
. .9 要点の復習
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
225 / 230
要点の復習
要点の復習 I
...
1
計算機とプログラミング言語
情報のコード化
汎用の情報処理システム
インタープリタとコンパイラ
...
2
字句解析
正規言語
非決定性有限状態機械
決定性有限状態機械
...
3
構文解析
文脈自由文法
LR 構文解析のアイデア
最右導出
特性文字列
LR(O)オートマトンが認識する言語
構文解析表
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
226 / 230
要点の復習
要点の復習 II
...
4
型の解析と型推論
型の導出システム
型推論アルゴリズム
単一化アルゴリズム
...
5
ラムダ式の操作的意味論
値の集合
クロージャによる関数の表現
環境を用いた再帰的な評価
...
6
疑似コード生成
SECD 機械
コンパイル
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
227 / 230
要点の復習
期末試験のための演習問題 I
注意
実際の試験では,必用に応じて型付け規則や評価規則を含む種々の
定義を与えるので,種々の規則の詳細を暗記する必用は必ずしもな
い.それら規則の考え方を理解すること.
詳しくは講義で解説する.
...
1
正規表現と字句解析
(1) 正規表現 r と s を解析するオートマトン N r と N s が与えられていると
する.これらを用いて,以下の正規表現を解析する非決定性オートマ
トン N を構築せよ.
..1.
..2.
r|s
r∗
(2) 以下の正規表現を受理する非決定性オートマトンを与えよ.
(a ∗ bd∗)|(a ∗ ce∗))
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
228 / 230
要点の復習
期末試験のための演習問題 II
...
2
構文解析
文脈自由文法
G = (N, Σ, P, S)
に対する特性オートマトン NC が受理する言語 L(NG ) はどのような
言語か?
以下の文法を考える.
S ::= E$
E ::= E + E
| E - E
| 1
..1.
..2.
この文法の(非決定性)特性オートマトンを構築せよ.
文字列 “1 + 1 * 1 に対する最右導出をすべて与えよ.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
229 / 230
要点の復習
期末試験のための演習問題 III
...
3
型推論
..1.
..2.
...
4
...
5
式 fn x => e に対する型付け規則を与えよ.
fn f => fn x =>f (f x) に対する型の導出を構築せよ.
操作的意味論
..1.
..2.
e1 e2 に対する評価規則を与えよ.
(fn x => (x x)) (fn x => x) の評価結果を示せ.
疑似コードへのコンパイル
..1.
..2.
e1 e2 に対するコンパイル規則を与えよ.
(fn x => (x x)) (fn x => x) を疑似コードへコンパイルした結果
を示せ.
大堀 淳 (東北大学 電気通信研究所)
コンパイラ講義資料
230 / 230