@@ -16,13 +16,15 @@ use crate::{
1616} ;
1717use common:: indexmap:: IndexSet ;
1818use constraint:: collect_constraints;
19- use hir:: { hir_def:: { HirIngot , Func } , Ingot } ;
19+ use hir:: {
20+ hir_def:: HirIngot ,
21+ Ingot ,
22+ } ;
2023use salsa:: Update ;
2124
2225pub ( crate ) mod constraint;
2326mod proof_forest;
2427
25-
2628#[ salsa:: tracked( return_ref) ]
2729pub fn is_goal_satisfiable < ' db > (
2830 db : & ' db dyn HirAnalysisDb ,
@@ -38,30 +40,6 @@ pub fn is_goal_satisfiable<'db>(
3840 ProofForest :: new ( db, ingot, goal, assumptions) . solve ( )
3941}
4042
41- /// A minimal, user-facing explanation of trait goal satisfiability.
42- #[ derive( Debug , Clone , PartialEq , Eq ) ]
43- pub enum GoalExplanation < ' db > {
44- Success ,
45- ContainsInvalid ,
46- NeedsConfirmation ,
47- Failure { subgoal : Option < super :: trait_def:: TraitInstId < ' db > > } ,
48- }
49-
50- /// Facade: Explain why a goal is (not) satisfiable, reusing existing solver.
51- pub fn explain_goal < ' db > (
52- db : & ' db dyn HirAnalysisDb ,
53- ingot : Ingot < ' db > ,
54- goal : Canonical < TraitInstId < ' db > > ,
55- assumptions : PredicateListId < ' db > ,
56- ) -> GoalExplanation < ' db > {
57- match is_goal_satisfiable ( db, ingot, goal, assumptions) {
58- GoalSatisfiability :: Satisfied ( _) => GoalExplanation :: Success ,
59- GoalSatisfiability :: ContainsInvalid => GoalExplanation :: ContainsInvalid ,
60- GoalSatisfiability :: NeedsConfirmation ( _) => GoalExplanation :: NeedsConfirmation ,
61- GoalSatisfiability :: UnSat ( sub) => GoalExplanation :: Failure { subgoal : sub. map ( |s| s. value ) } ,
62- }
63- }
64-
6543/// Checks if the given type is well-formed, i.e., the arguments of the given
6644/// type applications satisfies the constraints under the given assumptions.
6745#[ salsa:: tracked]
@@ -318,13 +296,3 @@ impl<'db> PredicateListId<'db> {
318296 Self :: new ( db, all_predicates. into_iter ( ) . collect :: < Vec < _ > > ( ) )
319297 }
320298}
321-
322- /// Public helper: collect full assumptions (constraints) applicable to a function definition,
323- /// including parent trait/impl bounds when relevant.
324- pub fn func_assumptions_for_func < ' db > (
325- db : & ' db dyn HirAnalysisDb ,
326- func : Func < ' db > ,
327- ) -> PredicateListId < ' db > {
328- constraint:: collect_func_def_constraints ( db, super :: func_def:: HirFuncDefKind :: Func ( func) , true )
329- . instantiate_identity ( )
330- }
0 commit comments