ソルバー
Chalk の再帰的ソルバーのドキュメントも読むことを検討してください。 この実装と非常によく似ており、このアプローチの制限についても説明されています。
大まかな流れ
ソルバーのエントリーポイントは InferCtxtEvalExt::evaluate_root_goal です。この関数はルートの EvalCtxt をセットアップし、その後 EvalCtxt::evaluate_goal を呼び出して、実際にトレイトソルバーに入ります。
EvalCtxt::evaluate_goal は 正準化、キャッシュ、オーバーフロー、ソルバーサイクルを処理します。それが完了すると、別個のローカルな InferCtxt を持つネストされた EvalCtxt を作成し、EvalCtxt::compute_goal を呼び出します。これは「実際のソルバーの挙動」を担当します。PredicateKind でマッチし、それぞれについて別の関数に委譲します。
Vec<T>: Clone のようなトレイトゴールの場合、EvalCtxt::compute_trait_goal は、このゴールを証明できる可能性のあるすべての方法を EvalCtxt::assemble_and_evaluate_candidates によって収集する必要があります。各候補は、推論制約が他の候補に漏れないよう、別々の「プローブ」で処理されます。その後、組み立てられた候補を EvalCtxt::merge_candidates によってマージしようとします。
重要な概念と設計パターン
EvalCtxt::add_goal
ネストされたゴールを証明するために、EvalCtxt::compute_goal を直接呼び出すのではなく、代わりに EvalCtxt::all_goal でそのゴールを EvalCtxt に追加します。その後、EvalCtxt::try_evaluate_added_goals または EvalCtxt::evaluate_added_goals_and_make_canonical_response のいずれかですべてのネストされたゴールをまとめて証明します。これにより、後続のゴールからの推論制約を扱えるようになります。
たとえば、ネストされたゴールとして ?x: Debug と (): ConstrainToU8<?x> の両方がある場合、?x: Debug を証明することは最初は曖昧ですが、(): ConstrainToU8<?x> を証明した後は ?x が u8 に制約され、u8: Debug の証明に成功します。
TyKind でのマッチング
ソルバーでは型を遅延正規化するため、あらゆる型と定数が潜在的に未正規化であると常に仮定する必要があります。これは、TyKind でのマッチングが簡単に誤りになり得ることを意味します。
正規化は 2 つの異なる方法で扱います。関連型を正規化するときに Trait ゴールを証明する場合、self 型と構造的に一致するかどうかに応じて、候補を別々に組み立てます。self 型に一致する候補は EvalCtxt::assemble_candidates_via_self_ty で処理され、これは EvalCtxt::assemble_candidates_after_normalizing_self_ty を介して再帰し、self 型を 1 レベル正規化します。それ以外のすべての場合で TyKind にマッチする必要があるときは、まず EvalCtxt::try_normalize_ty を使用して、その型を可能な限り正規化します。
高階ランクのゴール
ゴールが高階ランクである場合、たとえば for<'a> F: FnOnce(&'a ()) では、EvalCtxt::compute_goal は即座に 'a をプレースホルダーでインスタンス化し、その後 F: FnOnce(&'!a ()) をネストされたゴールとして再帰的に証明します。
選択への対処
一部のゴールは複数の方法で証明できます。このような場合、それぞれの選択肢を別々の「プローブ」で試し、その後 EvalCtxt::try_merge_responses を使用して結果のレスポンスをマージしようとします。レスポンスのマージに失敗した場合は、代わりに EvalCtxt::flounder を使用して曖昧性を返します。一部のゴールについては、EvalCtxt::try_merge_responses が失敗した場合に、いくつかの選択肢を他より不完全に優先しようとします。
さらに学ぶ
ソルバーはかなり自己完結しているはずです。上記の情報が、コード自体を見るときの良い基礎になることを願っています。その際に行き詰まった場合や、不明確だったり、より良いコメントが必要だったり、ここで言及すべき癖や設計判断がある場合は、Zulip で連絡してください。