型シノニム (Dtype) を消去し、参照箇所で本体の型に展開する

[cedretaber]

closes #26 (#14 の 6 番目「Dtype を実装する」)

概要

型シノニム(Definition natlist := list nat のような型を返す Definition)は miniml 上で Dtype 宣言として抽出されますが、Java バックエンドはスタブ(裸の type トークンを出力)のままでした。参照側も Java に存在しないシノニム名をそのまま印字するため、シノニムを含むコードは javac を通りませんでした。

Java には型エイリアス機能が無く、ラッパークラスで名前を残すとランタイム表現が変わってしまうため、本 PR は 宣言を消去し、参照箇所でシノニムを本体の型に展開する 方針を採ります。失われるのはシグネチャ上の名前のみで、ランタイム表現は不変です(型変数の Object 消去で既により多くの情報が落ちているため、追加の損失は小さい)。

変更点

• エイリアス表と展開関数 (plugins/extraction/java.ml)
  • pp_decl が Dtype を見た時点で表(Constant → 正規化済み本体)に登録し、宣言は何も出力しない
  • expand_aliases が Tglob(alias, args) を type_subst_list による引数代入付きで再帰展開。Mlutil.type_expand は Unset Extraction TypeExpand で恒等関数になるため流用せず、フラグ非依存の自前実装にしています(Java では展開が正しさの要件のため)
• 展開の適用箇所(関門): ml_type が AST から printer に入る全箇所
  • 宣言レベル: Dterm / Dfix の型、Dind のコンストラクタフィールド型
  • 式レベル: MLcons / MLcase の型注釈(デフォルトの Extraction TypeExpand では上流で展開済みですが、Unset 時はここが唯一の防壁になります)
  • 関門通過後はエイリアスが存在しないため、既存の型ユーティリティ(消去・キャスト判定・arrows_upto)は無変更です
• エッジケース
  • Axiom t : Type(本体が Taxiom)→ Object 扱いで登録(項レベル公理の扱いと整合)
  • Prop 由来(Tdummy)→ そのまま(Object に印字される)
• 型のカスタム抽出(Extract Constant t => "...")のサポート
  • カスタム型には展開すべき ml_type の本体が無く、Java ではエイリアス宣言も書けないため、文字列そのものを展開結果と見なし、宣言は出力せず全型位置でカスタム文字列を印字します(pp_type_global)
  • Java には宣言が存在しない以上、Inlined / 非 Inlined の区別は型については意味を持たないため同じ扱いです
  • 文字列が Java の型として妥当かはユーザー責任(OCaml/Haskell バックエンドと同じ契約。項のカスタム抽出は従来からこの扱いで印字されています)

テスト

• type_alias(14 ケース目): 単相シノニム / 関数型シノニム(展開後は arrow が見えるため冗長な receiver cast が出ない)/ パラメータ付き / シノニムのシノニム / inductive のフィールド型 / MLcons・MLcase 型注釈中の型引数 / 公理型、の 7 形をカバー。Driver で代表値をランタイム検証
• type_alias_noexpand(15 ケース目): Unset Extraction TypeExpand 下でも出力が正しいことを golden で固定(式レベル関門の回帰保護)
• type_custom(16 ケース目): Extract Constant big => "java.math.BigInteger" と項のカスタム抽出を組み合わせ、シノニム → カスタム型の連鎖も含めて golden + javac + ランタイム検証(BigInteger の実演算)
• 既存 13 ケースの golden はバイト単位で不変です

抽出例(修正前 → 修正後):

// 修正前: 裸の type トークン + 未宣言型名 + 偽キャスト
type
static Function<nat, natlist> singleton = n -> ((natlist) (Object) ((list) new Cons(n, ...)));

// 修正後
static Function<nat, list> singleton = n -> new Cons(n, ((list) new Nil()));

カスタム型の抽出例:

static java.math.BigInteger zero_big = java.math.BigInteger.ZERO;
static Function<java.math.BigInteger, java.math.BigInteger> inc2 = b ->
  inc_big.apply(inc_big.apply(b));

実装中に見つけた既存の問題(本 PR のスコープ外)

エイリアスとは無関係の既存バグを 3 件確認しました。テストはこれらを意図的に回避する形にしてあります(回避理由は .v のコメントに記載):

1. 部分適用コンストラクタの eta 展開などで λ 式が Object 型フィールドの引数位置に直接出ると、functional interface へのキャストが無く javac が通らない(例: Cons S Nil)
2. 単一コンストラクタ・単一フィールドの inductive は Singleton 分類で項レベル消去されるのに、Java バックエンドはラッパークラスを実出力するため実行時 ClassCastException になる
3. トップレベル定数名に含まれる '(例: inc2')が Java 識別子にそのまま出力される(ローカル変数は pr_id が $ に置換するが、トップレベル名は Common.pp_global 経由で素通し)

必要でしたら別 issue として起票します。

🤖 Generated with Claude Code