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

Structs, Enums and Non-Copy values as Ground Terms. #1

Closed
eqv opened this issue Sep 11, 2020 · 8 comments
Closed

Structs, Enums and Non-Copy values as Ground Terms. #1

eqv opened this issue Sep 11, 2020 · 8 comments

Comments

@eqv
Copy link

eqv commented Sep 11, 2020

It seems that the ground terms are limited to types implementing Copy, could this be loosened to contain values that are only Clone?.
In a similar vein, it seems that no pattern matching can be used in the body of a clause. For program analysis, it would be super useful to do stuff like this:

#[derive(Copy,Clone,Eq,PartialEq,Hash)]
enum Opt{
    Foo(u32),
    Bar(u32),
}

crepe! {
    @input
    struct Input(Opt);

    @output
    struct Output(u32);

    Output(i) <- Input(Opt::Foo(i));
}
@ekzhang
Copy link
Owner

ekzhang commented Sep 12, 2020

Hey @eqv! Thanks for the suggestions. I think it should be possible to allow Clone types, though doing so might lead to extra memory copies. I will work on this and try to make it reasonably efficient.

For destructuring, that's a great idea! There's a minor syntactical problem because I can't distinguish binding a Datalog variable with destructuring, versus making a function call or actually constructing a constraint using Datalog variables. For example, Opt::Foo(i) looks just like primes::nth_prime(i). And what about Output(i) <- Input(Opt::Foo(i)), Input(Opt::Bar(i))? The first one should destructure, and the second one should construct & look at an index.

Instead, what about adding a third type of syntax (let bindings) to rule clauses? So:

Output(i) <-
    Input(foo),
    if let Opt::Foo(i) = foo;


// or

Output(i) <-
    Input(foo),
    if let Opt::Foo(i) = foo,
    Input(Opt::Bar(i))

Would love to hear your thoughts on this design choice. I think this might solve both the destructuring problem, as well as the problem of just allowing temporary bindings in rules :)

@eqv
Copy link
Author

eqv commented Sep 12, 2020

That's pretty amazing. I actually tried both options just to see if they work! So I think they are pretty intuitive. In the case Input(Opt::Bar(i)) we should be able to conclude that its a pattern match since Input(_) is a relation right? I'm not sure if the if in the let clause is needed, but then again, It also doesn't hurt. I like it a lot!

@ekzhang
Copy link
Owner

ekzhang commented Sep 13, 2020

Just as an update, I haven't been able to get the code working for non-Copy structs. It seems like the issue is more difficult than I thought. I do have an experimental version, but it would require you to write ugly code like this to appease the borrow checker:

crepe! {
    @input
    struct Edge(String, String);

    @output
    struct Reachable(String, String);

    // Transitive closure
    Reachable(n.clone(), m.clone()) <- Edge(n, m);
    Reachable(n.clone(), m.clone()) <- Edge(n, k), Reachable(k, m);
}

Perhaps you can try to serialize your data into Copy terms, such as by giving everything an ID before giving it to Crepe? I think that this would be better for efficiency also - Formulog takes an approach where they put complex datatypes (e.g. strings, lists) into a hash-indexed cache and compare them by ID, for efficiency reasons.

Something that might help would be to allow lifetime parameters in relations. I'll make a new issue for this.


Working on the pattern matching next!

@eqv
Copy link
Author

eqv commented Sep 13, 2020

Would the solution above still work for copy types without explicitly calling clone? In that case it would seem like a pretty good option? The thing is, I was pretty much trying to avoid copying complex data structures by adding a Rc, which is not copy ^^.

@ekzhang
Copy link
Owner

ekzhang commented Sep 13, 2020

Why would an Rc be helpful for this? See #2 - couldn't you use a normal reference with lifetime specifier just as easily (it only needs to live as long as the Crepe struct)?

@eqv
Copy link
Author

eqv commented Sep 13, 2020

Yeah that would work as well, and be more efficient, but it's easier just to slap an Rc on it, clone everything all the time and call it a day, so I tried that first.

@ekzhang
Copy link
Owner

ekzhang commented Sep 14, 2020

You should be able to destructure with let bindings now if you update to v0.1.2. See https://github.com/ekzhang/crepe/blob/master/tests/test_destructure.rs for an example. Thanks!

@ekzhang ekzhang closed this as completed Sep 14, 2020
@eqv
Copy link
Author

eqv commented Sep 14, 2020

Sweet! Thanks a lot!

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

No branches or pull requests

2 participants