ekzhang / crepe

Datalog compiler embedded in Rust as a procedural macro
Apache License 2.0
453 stars 16 forks source link

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

Closed eqv closed 4 years ago

eqv commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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!

eqv commented 4 years ago

Sweet! Thanks a lot!