1
+ //! Defines traits used to embed the chalk-engine in another crate.
2
+ //!
3
+ //! chalk and rustc both define types which implement the traits in this
4
+ //! module. This allows each user of chalk-engine to define their own
5
+ //! `DomainGoal` type, add arena lifetime parameters, and more. See
6
+ //! [`Context`] trait for a list of types.
7
+
1
8
use crate :: fallible:: Fallible ;
2
9
use crate :: hh:: HhGoal ;
3
10
use crate :: { DelayedLiteral , ExClause , SimplifiedAnswer } ;
@@ -163,8 +170,10 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
163
170
fn empty_constraints ( ccs : & C :: CanonicalConstrainedSubst ) -> bool ;
164
171
165
172
fn canonical ( u_canon : & C :: UCanonicalGoalInEnvironment ) -> & C :: CanonicalGoalInEnvironment ;
166
- fn is_trivial_substitution ( u_canon : & C :: UCanonicalGoalInEnvironment ,
167
- canonical_subst : & C :: CanonicalConstrainedSubst ) -> bool ;
173
+ fn is_trivial_substitution (
174
+ u_canon : & C :: UCanonicalGoalInEnvironment ,
175
+ canonical_subst : & C :: CanonicalConstrainedSubst ,
176
+ ) -> bool ;
168
177
fn num_universes ( _: & C :: UCanonicalGoalInEnvironment ) -> usize ;
169
178
170
179
/// Convert a goal G *from* the canonical universes *into* our
@@ -244,11 +253,7 @@ pub trait InferenceTable<C: Context, I: Context>:
244
253
fn into_hh_goal ( & mut self , goal : I :: Goal ) -> HhGoal < I > ;
245
254
246
255
// Used by: simplify
247
- fn add_clauses (
248
- & mut self ,
249
- env : & I :: Environment ,
250
- clauses : I :: ProgramClauses ,
251
- ) -> I :: Environment ;
256
+ fn add_clauses ( & mut self , env : & I :: Environment , clauses : I :: ProgramClauses ) -> I :: Environment ;
252
257
253
258
/// Upcast this domain goal into a more general goal.
254
259
fn into_goal ( & self , domain_goal : I :: DomainGoal ) -> I :: Goal ;
@@ -300,10 +305,7 @@ pub trait UnificationOps<C: Context, I: Context> {
300
305
value : & C :: CanonicalConstrainedSubst ,
301
306
) -> I :: CanonicalConstrainedSubst ;
302
307
303
- fn lift_delayed_literal (
304
- & self ,
305
- value : DelayedLiteral < I > ,
306
- ) -> DelayedLiteral < C > ;
308
+ fn lift_delayed_literal ( & self , value : DelayedLiteral < I > ) -> DelayedLiteral < C > ;
307
309
308
310
// Used by: logic
309
311
fn invert_goal ( & mut self , value : & I :: GoalInEnvironment ) -> Option < I :: GoalInEnvironment > ;
@@ -324,9 +326,10 @@ pub trait UnificationOps<C: Context, I: Context> {
324
326
325
327
/// "Truncation" (called "abstraction" in the papers referenced below)
326
328
/// refers to the act of modifying a goal or answer that has become
327
- /// too large in order to guarantee termination. The SLG solver
328
- /// doesn't care about the precise truncation function, so long as
329
- /// it's deterministic and so forth.
329
+ /// too large in order to guarantee termination.
330
+ ///
331
+ /// The SLG solver doesn't care about the precise truncation function,
332
+ /// so long as it's deterministic and so forth.
330
333
///
331
334
/// Citations:
332
335
///
0 commit comments