Strange behaviour

[segeljakt]

Hi, thank you for the excellent crate. I am experimenting with using crepe for type-checking a programming language. I ran into some strange behaviour which causes an expression to get assigned multiple types (output relations). The code is here: (https://github.com/segeljakt/datalog-tests/blob/bug/src/main.rs)

These are my rules for type checking:

#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)]
pub(crate) struct Expr(usize);

#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)]
pub(crate) struct Type(usize);

#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)]
pub(crate) enum ExprKind {
    Let(Expr, Expr),
    I32(i32),
    U32(u32),
}

#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)]
pub(crate) enum TypeKind {
    I32,
    U32,
    Bool,
}

use crepe::crepe;

crepe! {
    @input
    #[derive(Debug)]
    struct ExprOf(Expr, ExprKind);

    @output
    #[derive(Debug)]
    struct TypeOf(Expr, TypeKind);

    // typeof(let _ = e0 in e1)
    TypeOf(e0, tk0) <-
        ExprOf(e0, ek0),
        let ExprKind::Let(_, e1) = ek0,
        TypeOf(e1, tk0);

    // typeof(100i32)
    TypeOf(e0, TypeKind::I32) <-
        ExprOf(e0, ek0),
        let ExprKind::I32(_) = ek0;

    // typeof(100u32)
    TypeOf(e0, TypeKind::U32) <-
        ExprOf(e0, ek0),
        let ExprKind::U32(_) = ek0;
}

This is my input and output:

$ cargo run
===============[Test 0]===============
let _ = 50i32 in 150u32

Inputs: {
    ExprOf(Expr(2), Let(Expr(0), Expr(1)))
    ExprOf(Expr(0), I32(50))
    ExprOf(Expr(1), U32(150))
}

Outputs: {
    TypeOf(Expr(1), U32)
    TypeOf(Expr(0), I32)
    TypeOf(Expr(2), I32)
    TypeOf(Expr(2), U32)
}

I expect Expr(2) to have type U32, but it strangely seems to also get assigned the type I32. Am I doing something wrong?

[domenicquirl]

I could replicate this behaviour and was intrigued by a warning of e1 being unused. The following is the output of cargo expand for the typeof(let _ = e0 in e1) rule:

for __crepe_var in __exprof.iter() {
    let e0 = __crepe_var.0;
    let ek0 = __crepe_var.1;

    #[allow(irrefutable_let_patterns)]
    if let ExprKind::Let(_, _, e1) = ek0 {
        for __crepe_var in __typeof_update.iter() {
            let e1 = __crepe_var.0;
            let tk0 = __crepe_var.1;
            let __crepe_goal = TypeOf(e0, tk0);
            if !__typeof.contains(&__crepe_goal) {
                __typeof_new.insert(__crepe_goal);
            }
        }
    }
}

// same rule if you swap `TypeOf` and `let` condition:
for __crepe_var in __exprof.iter() {
    let e0 = __crepe_var.0;
    let ek0 = __crepe_var.1;
    for __crepe_var in __typeof_update.iter() {
        let e1 = __crepe_var.0;
        let tk0 = __crepe_var.1;

        #[allow(irrefutable_let_patterns)]
        if let ExprKind::Let(_, _, e1) = ek0 {
            let __crepe_goal = TypeOf(e0, tk0);
            if !__typeof.contains(&__crepe_goal) {
                __typeof_new.insert(__crepe_goal);
            }
        }
    }
}

It is clearly visible that e1 is overwritten and unused twice in both examples, which I suppose might be the cause for this issue.

[ekzhang]

Thanks for the bug report! This was an oversight in implementing Clause::Let(guard), where the bound datalog variables were not updated. In your case, e1 was assigned, but the compiler didn't register that it was already bound, so it tried to bind it again on the next line TypeOf(e1, tk0).

I was able to replicate it with the following (failing) test:

// This test ensures that variables defined in `let` bindings are registered.

use crepe::crepe;

crepe! {
    @input
    struct Input(i32);

    @output
    #[derive(Debug)]
    struct Output(i32);

    Output(x) <-
        Input(x),
        let y = 2 * x,
        Input(y);
}

fn main() {
    let mut rt = Crepe::new();
    rt.extend(&[Input(2), Input(3), Input(4)]);
    let (res,) = rt.run();
    let res: Vec<_> = res.into_iter().collect();
    assert_eq!(res, vec![Output(2)]);
}

Will try to fix. In the meantime, you can work around this by adding an extra pair of parentheses. For example,

    Output(x) <-
        Input(x),
        let y = 2 * x,
        Input((y));

This produces the correct output but is definitely not ideal.