Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support const evaluation #736

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Conversation

HKalbasi
Copy link
Member

@HKalbasi HKalbasi commented Dec 2, 2021

Fix #548

This PR at current state is just for early feedback, and contains several todos.

My approach is this: Caller of chalk sees code that contains unevaluated const generic parameter. That can be arbitrary expression (which may contains block expressions, let, loop, ...) , but caller (after possible normalizing and partial evaluation, which currently there isn't any) changes them to a simple named function. For example it will change N < 128 to #le128(N) (or #F324(N)). The only thing that chalk knows about that functions is that it will return same output for the same input. And caller of chalk should provide a const_eval function that chalk can call it when all arguments of a function are concrete constants. In this way the complexity of arbitary rust syntax and const evaluation with miri would be abstracted away in chalk. So, this example from it's time to get hyped:

impl<const N: usize> Copy for Foo<N> where Assert::<{N < 128}>: IsTrue {}

Would become this in chalk:

test! {
        const_eval {
            |name, args| {
                match name.as_str() {
                    "le128" => (args[0] < 128) as u32,
                    _ => panic!("Unknown function"),
                }
            }
        }

        program {
            struct S<const N> {}

            trait Trait {}

            struct Assert<const E> {}
            trait IsTrue {}
            impl IsTrue for Assert<1> {}

            impl<const N> Trait for S<N> where Assert<#le128(N)>: IsTrue {}
        }

        goal {
            S<3>: Trait
        } yields {
            "Unique; substitution[], lifetime constraints []"
        }

        goal {
            S<240>: Trait
        } yields {
            "No possible solution"
        }
    }

This currently passes in my branch. If this is the correct way, we can continue this PR, otherwise we can close this and/or talk about what the correct approach is.

@jackh726
Copy link
Member

jackh726 commented Dec 7, 2021

Hi @HKalbasi. Thanks for the PR!

Adding const evaluation was attempted previously in #596. At that point, we hadn't put much thought into how to handle const eval (and still haven't). I'll try to take an initial pass at this soon, but you should take at that PR if you haven't seen it.

@HKalbasi
Copy link
Member Author

HKalbasi commented Dec 7, 2021

I had seen that PR, and if I understand correctly, unevaluated constants in that PR were an unknown value, but here they are projection of other constant variables. Not sure if this one is correct, but I wrote it with that PR in mind.

@bors
Copy link
Collaborator

bors commented Dec 9, 2021

☔ The latest upstream changes (presumably #735) made this pull request unmergeable. Please resolve the merge conflicts.

@bors
Copy link
Collaborator

bors commented Feb 13, 2022

☔ The latest upstream changes (presumably #744) made this pull request unmergeable. Please resolve the merge conflicts.

@nikomatsakis
Copy link
Contributor

Hi @HKalbasi ! Thanks for this. I'm going to take a look later today or this week.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Support const evaluation
4 participants