souffle-lang/souffle

ADTs with negation

gilbert opened this issue · 2 comments

Hi, relatively new to Datalog here. I'm trying to write a rule that "collapses" a specific branch when the rule encounters it.

However, when I try to use negation to match the rest of the cases, I get Error: Ungrounded ADT branch. Is there a way to do this without pattern matching every other case manually, or am I taking the wrong approach? Thank you!

.type MyType
  = A { id: symbol }
  | B { id: symbol }
  | C { id: symbol }
  | D { id: symbol }


.decl foo(n: number, mytype: MyType)
// Definition omitted; working properly

.decl bar(n: number, mytype: MyType)

bar(n, mtype) :-
  foo(n, $A(id)),
  foo(n+1, mtype).

bar(n, mtype) :-
  foo(n, mtype),
  mtype != $A(_).  // Error occurs here

Duplicate of #2315
Hi, the question is discussed in the issue above.

My search was not as thorough as I thought it was. Thanks!