솔버

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를 통해 이 목표를 증명할 수 있는 모든 방법을 수집해야 합니다. 추론 제약이 다른 후보로 새어 나가지 않도록 각 후보는 별도의 “프로브(probe)“에서 처리됩니다. 그런 다음 EvalCtxt::merge_candidates를 통해 수집된 후보들을 병합하려고 시도합니다.

중요한 개념과 설계 패턴

EvalCtxt::add_goal

중첩된 목표를 증명할 때는 EvalCtxt::compute_goal을 직접 호출하지 않고, 대신 EvalCtxt::add_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에 대한 매칭이 쉽게 잘못될 수 있음을 의미합니다.

정규화는 두 가지 방식으로 처리합니다. Trait 목표를 증명하거나 연관 타입을 정규화할 때는, 후보가 self 타입과 구조적으로 일치하는지에 따라 후보를 별도로 수집합니다. self 타입에 대해 매칭하는 후보는 EvalCtxt::assemble_candidates_via_self_ty에서 처리되며, 이 함수는 self 타입을 한 단계 정규화하는 EvalCtxt::assemble_candidates_after_normalizing_self_ty를 통해 재귀합니다. TyKind에 대해 매칭해야 하는 그 밖의 모든 경우에는 먼저 EvalCtxt::try_normalize_ty를 사용하여 타입을 최대한 정규화합니다.

고차 목표

목표가 for<'a> F: FnOnce(&'a ())처럼 고차(higher-ranked)인 경우, EvalCtxt::compute_goal은 'a를 플레이스홀더로 즉시 인스턴스화한 다음 F: FnOnce(&'!a ())를 중첩된 목표로 재귀적으로 증명합니다.

선택 처리

어떤 목표는 여러 방법으로 증명될 수 있습니다. 이러한 경우 각 선택지를 별도의 “프로브“에서 시도한 다음, EvalCtxt::try_merge_responses를 사용하여 결과 응답들을 병합하려고 시도합니다. 응답 병합에 실패하면 대신 EvalCtxt::flounder를 사용하여 모호성을 반환합니다. 일부 목표에서는 EvalCtxt::try_merge_responses가 실패할 경우, 불완전하게나마 일부 선택지를 다른 선택지보다 우선하려고 시도합니다.

더 알아보기

솔버는 비교적 독립적으로 구성되어 있을 것입니다. 위의 정보가 코드 자체를 살펴볼 때 좋은 토대가 되기를 바랍니다. 그 과정에서 막히거나, 불분명해서 더 나은 주석이 필요하거나 여기에서 언급되어야 할 특이점이나 설계 결정이 있다면 Zulip에서 연락해 주십시오.