adapter API

adapter パッケージには公開項目がない。これは契約テスト用のパッケージであり、そのホワイトボックステストは下流風の小さな AST を定義し、それに対して @syntax.BindingSyntax を実装し、Term[T] ではない AST 上で汎用代入と汎用書き換えがドキュメントどおりに振る舞うことを検査する。

package "Luna-Flow/type_theory/adapter"

// Values

// Errors

// Types and methods

// Type aliases

// Traits

独自の AST を適合させるために実装するインターフェースは @syntax.BindingSyntax であり、それによって得られるアルゴリズムは @syntax.generic_free_variables、@substitution.GenericSubstitution、@rewrite.generic_top_down_once である。契約は adapter の設計で説明されており、adapter チュートリアルではアダプタを段階的に構築する。

テストが検査する内容

テストファイル src/adapter/poly_adapter_wbtest.mbt は、4 種類のノードを持つ非公開の AST を用いる：整数リテラル（Opaque として射影）、変数、n 項の和ノード（Apply として射影）、スコープノード（Bind として射影）である。検査するのは次の点である

• GenericSubstitution::apply_once は同時かつ 1 パスで代入する：$\{x \mapsto y,\ y \mapsto 2\}$ を $x + y$ に適用すると $y + 2$ になる；
• 代入はその定義域外の変数をそのまま残す（部分評価）；
• generic_top_down_once は引数の内部にある簡約基を見つけ、トレイトのコンストラクタを通じて親を再構築し、パス [ApplyArgument(0)] を報告する。