cairo_lang_semantic/expr/inference/
solver.rs

1use std::collections::BTreeMap;
2use std::sync::Arc;
3
4use cairo_lang_debug::DebugWithDb;
5use cairo_lang_defs::ids::LanguageElementId;
6use cairo_lang_proc_macros::SemanticObject;
7use cairo_lang_utils::LookupIntern;
8use itertools::Itertools;
9
10use super::canonic::{CanonicalImpl, CanonicalMapping, CanonicalTrait, MapperError, ResultNoErrEx};
11use super::conform::InferenceConform;
12use super::infers::InferenceEmbeddings;
13use super::{
14    ImplVarTraitItemMappings, InferenceData, InferenceError, InferenceId, InferenceResult,
15    InferenceVar, LocalImplVarId,
16};
17use crate::db::SemanticGroup;
18use crate::items::constant::ImplConstantId;
19use crate::items::imp::{
20    ImplId, ImplImplId, ImplLookupContext, UninferredImpl, find_candidates_at_context,
21    find_closure_generated_candidate,
22};
23use crate::substitution::SemanticRewriter;
24use crate::types::{ImplTypeById, ImplTypeId};
25use crate::{ConcreteTraitId, GenericArgumentId, TypeId, TypeLongId};
26
27/// A generic solution set for an inference constraint system.
28#[derive(Clone, PartialEq, Eq, Debug)]
29pub enum SolutionSet<T> {
30    None,
31    Unique(T),
32    Ambiguous(Ambiguity),
33}
34
35/// Describes the kinds of inference ambiguities.
36#[derive(Clone, Debug, Eq, Hash, PartialEq, SemanticObject)]
37pub enum Ambiguity {
38    MultipleImplsFound {
39        concrete_trait_id: ConcreteTraitId,
40        impls: Vec<ImplId>,
41    },
42    FreeVariable {
43        impl_id: ImplId,
44        #[dont_rewrite]
45        var: InferenceVar,
46    },
47    WillNotInfer(ConcreteTraitId),
48    NegativeImplWithUnresolvedGenericArgs {
49        impl_id: ImplId,
50        ty: TypeId,
51    },
52}
53impl Ambiguity {
54    pub fn format(&self, db: &(dyn SemanticGroup + 'static)) -> String {
55        match self {
56            Ambiguity::MultipleImplsFound { concrete_trait_id, impls } => {
57                let impls_str =
58                    impls.iter().map(|imp| format!("`{}`", imp.format(db.upcast()))).join(", ");
59                format!(
60                    "Trait `{:?}` has multiple implementations, in: {impls_str}",
61                    concrete_trait_id.debug(db)
62                )
63            }
64            Ambiguity::FreeVariable { impl_id, var: _ } => {
65                format!("Candidate impl {:?} has an unused generic parameter.", impl_id.debug(db),)
66            }
67            Ambiguity::WillNotInfer(concrete_trait_id) => {
68                format!(
69                    "Cannot infer trait {:?}. First generic argument must be known.",
70                    concrete_trait_id.debug(db)
71                )
72            }
73            Ambiguity::NegativeImplWithUnresolvedGenericArgs { impl_id, ty } => format!(
74                "Cannot infer negative impl in `{}` as it contains the unresolved type `{}`",
75                impl_id.format(db),
76                ty.format(db)
77            ),
78        }
79    }
80}
81
82/// Query implementation of [SemanticGroup::canonic_trait_solutions].
83/// Assumes the lookup context is already enriched by [enrich_lookup_context].
84pub fn canonic_trait_solutions(
85    db: &dyn SemanticGroup,
86    canonical_trait: CanonicalTrait,
87    lookup_context: ImplLookupContext,
88    impl_type_bounds: BTreeMap<ImplTypeById, TypeId>,
89) -> Result<SolutionSet<CanonicalImpl>, InferenceError> {
90    let mut concrete_trait_id = canonical_trait.id;
91    let impl_type_bounds = Arc::new(impl_type_bounds);
92    // If the trait is not fully concrete, we might be able to use the trait's items to find a
93    // more concrete trait.
94    if !concrete_trait_id.is_fully_concrete(db) {
95        let mut solver =
96            Solver::new(db, canonical_trait, lookup_context.clone(), impl_type_bounds.clone());
97        match solver.solution_set(db) {
98            SolutionSet::None => {}
99            SolutionSet::Unique(imp) => {
100                concrete_trait_id =
101                    imp.0.concrete_trait(db).expect("A solved impl must have a concrete trait");
102            }
103            SolutionSet::Ambiguous(ambiguity) => {
104                return Ok(SolutionSet::Ambiguous(ambiguity));
105            }
106        }
107    }
108    // Solve the trait without the trait items, so we'd be able to find conflicting impls.
109    let mut solver = Solver::new(
110        db,
111        CanonicalTrait { id: concrete_trait_id, mappings: ImplVarTraitItemMappings::default() },
112        lookup_context,
113        impl_type_bounds,
114    );
115
116    Ok(solver.solution_set(db))
117}
118
119/// Cycle handling for [canonic_trait_solutions].
120pub fn canonic_trait_solutions_cycle(
121    _db: &dyn SemanticGroup,
122    _cycle: &salsa::Cycle,
123    _canonical_trait: &CanonicalTrait,
124    _lookup_context: &ImplLookupContext,
125    _impl_type_bounds: &BTreeMap<ImplTypeById, TypeId>,
126) -> Result<SolutionSet<CanonicalImpl>, InferenceError> {
127    Err(InferenceError::Cycle(InferenceVar::Impl(LocalImplVarId(0))))
128}
129
130/// Adds the defining module of the trait and the generic arguments to the lookup context.
131pub fn enrich_lookup_context(
132    db: &dyn SemanticGroup,
133    concrete_trait_id: ConcreteTraitId,
134    lookup_context: &mut ImplLookupContext,
135) {
136    lookup_context.insert_module(concrete_trait_id.trait_id(db).module_file_id(db.upcast()).0);
137    let generic_args = concrete_trait_id.generic_args(db);
138    // Add the defining module of the generic args to the lookup.
139    for generic_arg in &generic_args {
140        if let GenericArgumentId::Type(ty) = generic_arg {
141            enrich_lookup_context_with_ty(db, *ty, lookup_context);
142        }
143    }
144}
145
146/// Adds the defining module of the type to the lookup context.
147pub fn enrich_lookup_context_with_ty(
148    db: &dyn SemanticGroup,
149    ty: TypeId,
150    lookup_context: &mut ImplLookupContext,
151) {
152    match ty.lookup_intern(db) {
153        TypeLongId::ImplType(impl_type_id) => {
154            lookup_context.insert_impl(impl_type_id.impl_id());
155        }
156        long_ty => {
157            if let Some(module_id) = long_ty.module_id(db) {
158                lookup_context.insert_module(module_id);
159            }
160        }
161    }
162}
163
164/// A canonical trait solver.
165#[derive(Debug)]
166pub struct Solver {
167    pub canonical_trait: CanonicalTrait,
168    pub lookup_context: ImplLookupContext,
169    candidate_solvers: Vec<CandidateSolver>,
170}
171impl Solver {
172    fn new(
173        db: &dyn SemanticGroup,
174        canonical_trait: CanonicalTrait,
175        lookup_context: ImplLookupContext,
176        impl_type_bounds: Arc<BTreeMap<ImplTypeById, TypeId>>,
177    ) -> Self {
178        let filter = canonical_trait.id.filter(db);
179        let mut candidates =
180            find_candidates_at_context(db, &lookup_context, &filter).unwrap_or_default();
181        find_closure_generated_candidate(db, canonical_trait.id)
182            .map(|candidate| candidates.insert(candidate));
183        let candidate_solvers = candidates
184            .into_iter()
185            .filter_map(|candidate| {
186                CandidateSolver::new(
187                    db,
188                    &canonical_trait,
189                    candidate,
190                    &lookup_context,
191                    impl_type_bounds.clone(),
192                )
193                .ok()
194            })
195            .collect();
196
197        Self { canonical_trait, lookup_context, candidate_solvers }
198    }
199
200    pub fn solution_set(&mut self, db: &dyn SemanticGroup) -> SolutionSet<CanonicalImpl> {
201        let mut unique_solution: Option<CanonicalImpl> = None;
202        for candidate_solver in &mut self.candidate_solvers {
203            let Ok(candidate_solution_set) = candidate_solver.solution_set(db) else {
204                continue;
205            };
206
207            let candidate_solution = match candidate_solution_set {
208                SolutionSet::None => continue,
209                SolutionSet::Unique(candidate_solution) => candidate_solution,
210                SolutionSet::Ambiguous(ambiguity) => return SolutionSet::Ambiguous(ambiguity),
211            };
212            if let Some(unique_solution) = unique_solution {
213                // There might be multiple unique solutions from different candidates that are
214                // solved to the same impl id (e.g. finding it near the trait, and
215                // through an impl alias). This is valid.
216                if unique_solution.0 != candidate_solution.0 {
217                    return SolutionSet::Ambiguous(Ambiguity::MultipleImplsFound {
218                        concrete_trait_id: self.canonical_trait.id,
219                        impls: vec![unique_solution.0, candidate_solution.0],
220                    });
221                }
222            }
223            unique_solution = Some(candidate_solution);
224        }
225        unique_solution.map(SolutionSet::Unique).unwrap_or(SolutionSet::None)
226    }
227}
228
229/// A solver for a candidate to a canonical trait.
230#[derive(Debug)]
231pub struct CandidateSolver {
232    pub candidate: UninferredImpl,
233    inference_data: InferenceData,
234    canonical_embedding: CanonicalMapping,
235    candidate_impl: ImplId,
236    pub lookup_context: ImplLookupContext,
237}
238impl CandidateSolver {
239    fn new(
240        db: &dyn SemanticGroup,
241        canonical_trait: &CanonicalTrait,
242        candidate: UninferredImpl,
243        lookup_context: &ImplLookupContext,
244        impl_type_bounds: Arc<BTreeMap<ImplTypeById, TypeId>>,
245    ) -> InferenceResult<CandidateSolver> {
246        let mut inference_data: InferenceData = InferenceData::new(InferenceId::Canonical);
247        let mut inference = inference_data.inference(db);
248        inference.data.impl_type_bounds = impl_type_bounds.clone();
249        let (canonical_trait, canonical_embedding) = canonical_trait.embed(&mut inference);
250
251        // If the closure params are not var free, we cannot infer the negative impl.
252        // We use the canonical trait concretize the closure params.
253        if let UninferredImpl::GeneratedImpl(imp) = candidate {
254            inference.conform_traits(imp.lookup_intern(db).concrete_trait, canonical_trait.id)?;
255        }
256
257        // Add the defining module of the candidate to the lookup.
258        let mut lookup_context = lookup_context.clone();
259        lookup_context.insert_lookup_scope(db, &candidate);
260        // Instantiate the candidate in the inference table.
261        let candidate_impl =
262            inference.infer_impl(candidate, canonical_trait.id, &lookup_context, None)?;
263        for (trait_type, ty) in canonical_trait.mappings.types.iter() {
264            let mapped_ty =
265                inference.reduce_impl_ty(ImplTypeId::new(candidate_impl, *trait_type, db))?;
266
267            // Conform the candidate's type to the trait's type.
268            inference.conform_ty(mapped_ty, *ty)?;
269        }
270        for (trait_const, const_id) in canonical_trait.mappings.constants.iter() {
271            let mapped_const_id = inference.reduce_impl_constant(ImplConstantId::new(
272                candidate_impl,
273                *trait_const,
274                db,
275            ))?;
276            // Conform the candidate's constant to the trait's constant.
277            inference.conform_const(mapped_const_id, *const_id)?;
278        }
279
280        for (trait_impl, impl_id) in canonical_trait.mappings.impls.iter() {
281            let mapped_impl_id =
282                inference.reduce_impl_impl(ImplImplId::new(candidate_impl, *trait_impl, db))?;
283            // Conform the candidate's impl to the trait's impl.
284            inference.conform_impl(mapped_impl_id, *impl_id)?;
285        }
286
287        Ok(CandidateSolver {
288            candidate,
289            inference_data,
290            canonical_embedding,
291            candidate_impl,
292            lookup_context,
293        })
294    }
295    fn solution_set(
296        &mut self,
297        db: &dyn SemanticGroup,
298    ) -> InferenceResult<SolutionSet<CanonicalImpl>> {
299        let mut inference = self.inference_data.inference(db);
300        let solution_set = inference.solution_set()?;
301        Ok(match solution_set {
302            SolutionSet::None => SolutionSet::None,
303            SolutionSet::Ambiguous(ambiguity) => SolutionSet::Ambiguous(ambiguity),
304            SolutionSet::Unique(_) => {
305                let candidate_impl = inference.rewrite(self.candidate_impl).no_err();
306                match CanonicalImpl::canonicalize(db, candidate_impl, &self.canonical_embedding) {
307                    Ok(canonical_impl) => {
308                        inference.validate_neg_impls(&self.lookup_context, canonical_impl)?
309                    }
310                    Err(MapperError(var)) => {
311                        return Ok(SolutionSet::Ambiguous(Ambiguity::FreeVariable {
312                            impl_id: candidate_impl,
313                            var,
314                        }));
315                    }
316                }
317            }
318        })
319    }
320}
cairo_lang_semantic/expr/inference/solver.rs

cairo_lang_semantic/expr/inference/
solver.rs
