講義の目的 . . .. . 東北大学 電気・情報系「コンパイラ」 講義資料 . . 講義の概要 大堀 淳 東北大学 電気通信研究所 大堀 淳 (東北大学 電気通信研究所) コンパイラ講義資料 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
© Copyright 2024 ExpyDoc