v0.1.z でのパッケージシステムの処理に関する設計

前提と用語

• 文書ファイルを除くSATySFiコードの書かれたファイルをソースファイルと呼ぶ．
• 各ソースファイルは単一のモジュールの束縛 module … ［:> sig … end］ = struct … end からなっており，これによって束縛されているモジュールをファイルモジュールと呼ぶ．
• パッケージ中のソースファイルのうち1つだけがパッケージ外部からも見えるモジュールを定義している特別なものとし，このファイルモジュールをメインモジュールと呼ぶ．
• 簡単のため，各パッケージは1つのバージョンが固定されていると仮定する．
  • これはいわゆるlockファイルから得る．lockファイルの書き出しはSatyrographosが行なうと責務の分離としてよいかもしれない．
• モジュール名とそのシグネチャを紐づけた $\{X_1 ↦ ξ_1, …, X_n ↦ ξ_n\}$ を大域型環境と呼ぶ．

依存関係の示し方

同一パッケージ内の別ファイルへの依存：

use 〈ファイルモジュール名〉

別パッケージへの依存：

use package 〈メインモジュール名〉

文書ファイルから相対ファイルへの依存：

use 〈ファイルモジュール名〉 of 〈拡張子を除く相対パス〉

具体例

文書ファイル sample.saty は以下のような形で記述されている：

use package StdJa
use Introduction of `introduction`

StdJa.Report.document (|
  title  = {サンプル},
  author = {gfn},
|) '<
  +p{これはサンプル文書です．}
  #Introduction.text;
>

use package StdJa は StdJa をメインモジュールとする std_ja パッケージを読み込む．バージョンはいわゆるlockファイル sample.satysfi-lock に書き出されているとする．このlockファイルはSATySFi自身が生成してもよいし，Satyrographosなどの外部ツールが生成してもよい．いずれとしても，エンドユーザは制約だけを書き，何らかの方法で制約を解消したlockファイルをつくる．

use Introduction of `introduction` は，この文書ファイルから見て ./introduction.satyh に置いてあるファイルを読み込む．テキストモードの場合は拡張子が変わる．

単一の文書ファイルを入力とする場合

処理の全体像

簡単のため，以下の説明では文書は .saty 形式，出力はPDFとする．Markdown入力やテキスト出力モードでも大きくは変わらない．

全体処理

1. lockファイルから，バージョンの固定された各パッケージ $P_1, \ldots, P_m$ に関する情報を読み込む．
2. 文書ファイルから use … of … で依存しているファイル群を辿り，これらを1つのパッケージ $P_{\mathrm{doc}}$ をなすファイル群とみなす．
3. 1で得られたパッケージ群を，依存関係をもとにトポロジカルソートし， $P_{I_1}, \ldots, P_{I_m}$ という列にする．
4. 3で得られた順で各パッケージ $P_{I_i}$ に対し以下の「パッケージごとの処理」を行ない，メインモジュール $X_{I_i}$ のシグネチャ $ξ_{I_i}$ とコンパイル結果の束縛列 $d_{I_i}$ を得る．
5. $P_{\mathrm{doc}}$ についても同様に行なう．コンパイル結果は束縛列 $d$ だけではなく文書本体に対応する式 $e$ も得られる．
6. $d_{I_1} \cdots d_{I_n} d$ を評価した後，式 $e$ を評価し，得られた文書をPDFに出力する．

パッケージごとの処理

1. コンフィグファイルをもとにソースファイル群を列挙し，メインモジュール $X$ も同定しておく．
2. メインモジュールを含む各ソースファイルをパースする．
3. use … の依存関係に基づいてトポロジカルソートして $F_1, \ldots, F_n$ とする．
4. 3で得られた順番で各 $F_i$ を型検査する．このとき，use package … と use … に基づいて一部のモジュールのみを型環境に入れてASTを走査する．
   • 依存する各パッケージのメインモジュールは既に検査を終えておりシグネチャが得られている．
5. メインモジュール $X$ のシグネチャ $ξ$ およびコンパイル結果の束縛列 $d$ が得られたら， $(X, ξ, d)$ を戻り値として返す．
   • 典型的には最後の $F_n$ がメインモジュールを束縛しているソースファイルである．
   • なお， $X$ に対するユーザによるシグネチャ註釈 $S$ があるなら， $ξ$ が $S$ の部分型であるかをここで検査する． $S$ は他パッケージには依存してよいが，パッケージ内の別ファイルで定義された型などに依存していてはならない．

実装の水準の記述

Main

1. 文書ファイルを Parser によりパースし，そのファイルASTを $F_{\mathrm{doc}}$ とする．
2. lockファイルを LockConfig によりデコードし，$L$ とする．
3. $F_{\mathrm{doc}}$ を OpenFileDependencyResolver に渡し，ソートされたファイルAST列 $F_1, …, F_n$ を得る．
4. $L$ を ClosedLockDependencyResolver に渡し，依存関係に関してトポロジカルソートされたパッケージ列 $P_{I_1}, \ldots, P_{I_m}$ を得る．
5. 各 $P_{I_i}$ に対して4で得られた順番に PackageChecker を呼び出してコンパイル結果 $d_{I_i}$ およびシグネチャ $ξ_{I_i}$ を得る．順次 $X_{I_i} ↦ ξ_{I_i}$ を大域型環境に追加して畳み込む．
6. PackageChecker と同様の方法で $F_1, …, F_n$ をそれぞれ順に ModuleTypechecker で型検査し，大域型環境を拡張しながら $d$ を得る．
7. $F_{\mathrm{doc}}$ を Typechecker で型検査し，コンパイル結果 $e$ を得る．
8. 束縛列 $d_{I_1} \cdots d_{I_n} d$ を評価し，その後 $e$ を評価し，得られたドキュメント値 $v$ をPDFに書き出す．

OpenFileDependencyResolver

上記「全体処理」の2をやる．すなわち，文書ファイルASTを受け取り，関連するファイルを列挙してそれらの間の use … of … の依存関係に基づいてトポロジカルソートを行ない，ファイルAST列を返す．

2022年10月23日現在の dev-0-1-0 にある実装の FileDependencyResolver とおおよそ同じ．

ClosedLockDependencyResolver

バージョンの固定されたパッケージの集合を受け取り，それぞれを PackageReader で読み出して，それらの間の依存関係をもとにトポロジカルソートして返す．

PackageReader

上記「パッケージごとの処理」の1と2をやる．すなわち，コンフィグファイルを読んで各ソースファイルを Parser によりパースしてファイルAST集合にし，メインモジュールがどれであるかなどの情報とともに返す．この形式がパッケージ情報 $P$ である．

PackageChecker

1. 大域型環境 $G_0$ とパッケージ情報 $P$ を受け取る．
2. $P$ のソースファイル集合に対し，ClosedFileDependencyResolver を用いて，ソートされたファイルAST列 $F_1, \ldots, F_n$ を得る．
3. 2で得られた順番に，各 $F_i$ を ModuleTypechecker で型検査する．型環境の初期値は $G_{i - 1}$ と use … の指定からつくる．各ファイルのシグネチャとして $ξ_i$ が得られたら，それを大域型環境に加えて $G_i := G_{i - 1} ∪ \{X_i ↦ ξ_i\}$ とする．
4. メインモジュールのコンパイル結果である $d$ とシグネチャ $ξ$ を返す．
   • シグネチャ註釈 $S$ がある場合は， $G_0$ （ $G_n$ などではないことに注意）を用いて内部表現のシグネチャ $ξ'$ にelaborateし， $ξ <: ξ'$ かどうかを検査する．

ClosedFileDependencyResolver

上記「パッケージごとの処理」の3をやる．すなわち，ソースファイルのパスの集合 $\{F_1, \ldots, F_n\}$ を受け取り，それらの間にある use … の依存関係に基づいてトポロジカルソートし，ファイルAST列を返す．