Semantic equality to syntactic equality #401

basil-cow · 2020-04-16T21:01:05Z

No description provided.

nikomatsakis

some old comments, perhaps no longer relevant

chalk-ir/src/lib.rs

nikomatsakis · 2020-04-29T15:02:45Z

chalk-solve/src/clauses/builder.rs

+            .intern(interner)
+        };
+
+        self.clauses.push(syn_eq_lower(interner, &clause));


One thing I was considering in doing this was making ClauseBuilder generic over two Interner values, one of which represented "Semantically equal" predicates and one of which represented "syntactically equal". This helps ensure we are not failing to do the conversion. I'm not sure how much value it really adds, though.

Yeah, I thought about making syn_eq_lower to return a SynLowered<Fold::Result>

Not sure I follow -- what is SynLowered, just a newtype?

nikomatsakis · 2020-04-29T15:04:03Z

chalk-solve/src/clauses/program_clauses.rs

@@ -735,6 +735,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {

            // add new type parameter U
            builder.push_bound_ty(|builder, ty| {
+                let alias = AliasTy::Projection(projection.clone());


just a random refactoring?

basil-cow · 2020-05-04T23:35:03Z

Woah you can push to my branch

bjorn3 · 2020-05-05T09:44:28Z

@Areredify There is a checkbox "Allow edits and access to secrets by maintainers" both when opening a PR and when you opened it at the bottom of the sidebar. It is checked by default.

nikomatsakis · 2020-05-05T09:42:58Z

chalk-solve/src/clauses/syntactic_eq.rs

+        clause: &ProgramClause<I>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<ProgramClause<I>> {
+        let interner = self.interner;


I think we should either

save the old values of new_params/new_goals, and restore before we return

or assert that they are empty (if that is known to be true)

I don't see why they would be known to be empty, though, so I think we should save the values of the vector. The alternative would be to rewrite the code to not touch pre-existing things and just save the lengths.

Probably we need to save binders_len too

We know them to be empty because only domain goals and program clauses contain types (and EqGoal, but it is unique), and when folding domain goals we are guaranteed to not encounter another goal or clause. If we restrict input types of syn_lower to only be ProgramClause and Goal, then the lowering should be correct.

ok, then add assertions -- I guess it's true that we only have to worry about domain goal, and it cannot contain clauses. Right. I was thinking about how goals can contain clauses in general (and vice versa, of course).

nikomatsakis · 2020-05-05T09:43:26Z

chalk-solve/src/clauses/syntactic_eq.rs

+        let ((binders, implication), in_binders) = match clause.data(interner) {
+            ProgramClauseData::ForAll(for_all) => (for_all.clone().into(), true),
+            // introduce a dummy binder and shift implication through it
+            ProgramClauseData::Implies(implication) => (


I keep meaning to factor away ProgramClauseData::Implies, and just always have a binder.

nikomatsakis · 2020-05-05T09:44:04Z

chalk-solve/src/clauses/syntactic_eq.rs

+        };
+        let mut binders: Vec<_> = binders.as_slice(interner).clone().into();
+
+        let outer_binder = outer_binder.shifted_in();


Comment:

// Adjust the outer binder to account for the binder in the program clause

nikomatsakis · 2020-05-05T09:45:31Z

chalk-solve/src/clauses/syntactic_eq.rs

+
+        let outer_binder = outer_binder.shifted_in();
+
+        self.binders_len = binders.len();


Comment here, referencing the function comment:

// First lower the "consequence" -- in our example that is // // ``` // Implemented(<X as Iterator>::Item: Debug) // ``` // // then save out the `new_params` and `new_goals` vectors to store any new variables created as a result. In this case, that would be the `Y` parameter and `AliasEq(<X as Iterator>::Item, Y)` goals. // // Note that these new parameters will have indices that come after the existing parameters, so any references to existing parameters like `X` in the "conditions" are still valid even if we insert new parameters.

nikomatsakis · 2020-05-05T09:45:51Z

chalk-solve/src/clauses/syntactic_eq.rs

+        self.binders_len = binders.len();
+        let consequence = implication.consequence.fold_with(self, outer_binder)?;
+        // Immediately move `new_params` out of of the folder struct so it's safe
+        // to call `.fold_with` again


(then I think you can remove this comment, it's explained more usefully above)

nikomatsakis · 2020-05-05T09:56:39Z

chalk-solve/src/clauses/syntactic_eq.rs

+
+        let outer_binder = outer_binder.shifted_in();
+
+        self.binders_len = binders.len();


Comment:

Set binders_len to binders.len since new parameters will be added into the existing forall<...> binder on the program clause.

nikomatsakis · 2020-05-05T09:57:29Z

chalk-solve/src/clauses/syntactic_eq.rs

+
+struct SynEqFolder<'i, I: Interner> {
+    interner: &'i I,
+    new_params: Vec<ParameterKind<()>>,


comments on these fields -- what do they store?

My suggestions:

Store the kinds of any new parameters that are introduced during folding. These parameters will either be added to an enclosing exists binder (when lowering a goal) or an enclosing forall binder (when lowering a program clause).

nikomatsakis · 2020-05-05T09:57:48Z

chalk-solve/src/clauses/syntactic_eq.rs

+struct SynEqFolder<'i, I: Interner> {
+    interner: &'i I,
+    new_params: Vec<ParameterKind<()>>,
+    new_goals: Vec<Goal<I>>,


For each new parameter X, introduces an AliasEq goal that defines it, like AliasEq(<T as Iterator>::Item, X)

nikomatsakis · 2020-05-05T09:58:11Z

chalk-solve/src/clauses/syntactic_eq.rs

+    interner: &'i I,
+    new_params: Vec<ParameterKind<()>>,
+    new_goals: Vec<Goal<I>>,
+    binders_len: usize,


Stores the number of variables in the binder that we are adding parameters into thus far. Incremented for each new variable we add.

nikomatsakis · 2020-05-05T09:58:42Z

chalk-solve/src/clauses/syntactic_eq.rs

+    TyData,
+};
+
+pub fn syn_eq_lower<I: Interner, T: Fold<I>>(interner: &I, clause: &T) -> <T as Fold<I>>::Result {


Needs a comment. Also, I wonder if it's worth adding some other trait since you only really want to fold program clauses and goals here..? Nah, probably not, but we should add a comment about it.

I think making it into syn_lower_clause and syn_lower_goal should be enough

Yeah, two separate functions would be fine

jackh726 · 2020-10-15T01:35:51Z

Closing in favor of #589

basil-cow force-pushed the sem_eq branch 2 times, most recently from 8d371a2 to 011cbd3 Compare April 17, 2020 13:32

basil-cow force-pushed the sem_eq branch 2 times, most recently from eea51d7 to ccce5d0 Compare May 3, 2020 19:20

nikomatsakis reviewed May 4, 2020

View reviewed changes

nikomatsakis reviewed May 5, 2020

View reviewed changes

basil-cow and others added 2 commits May 21, 2020 15:54

alias eq mvp

3dfee39

expand coinductive reasoning

a4e70aa

basil-cow force-pushed the sem_eq branch from c2549a2 to a4e70aa Compare May 21, 2020 13:52

nikomatsakis mentioned this pull request May 23, 2020

Generate auto trait clauses for opaque type goals #468

Merged

nathanwhit mentioned this pull request Aug 2, 2020

[WIP] Convert from semantic to syntactic equality #589

Open

jackh726 closed this Oct 15, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Semantic equality to syntactic equality #401

Semantic equality to syntactic equality #401

basil-cow commented Apr 16, 2020

nikomatsakis left a comment

nikomatsakis Apr 29, 2020

basil-cow May 4, 2020

nikomatsakis May 5, 2020

nikomatsakis Apr 29, 2020

basil-cow commented May 4, 2020

bjorn3 commented May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

basil-cow May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

nikomatsakis May 5, 2020

basil-cow May 5, 2020

nikomatsakis May 5, 2020

jackh726 commented Oct 15, 2020


		let outer_binder = outer_binder.shifted_in();

		self.binders_len = binders.len();

Semantic equality to syntactic equality #401

Semantic equality to syntactic equality #401

Conversation

basil-cow commented Apr 16, 2020

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

basil-cow commented May 4, 2020

bjorn3 commented May 5, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jackh726 commented Oct 15, 2020