search

souffle-lang / souffle

Soufflé is a variant of Datalog for tool designers crafting analyses in Horn clauses. Soufflé synthesizes a native parallel C++ program from a logic specification.
http://souffle-lang.github.io/
Universal Permissive License v1.0
907 stars 199 forks source link

Inconsistent printing of binary operations #1971

Open langston-barrett opened 3 years ago

langston-barrett commented 3 years ago

Consider the following program:

.decl num(x: number)
.decl test(x: number, y: number)

num(0).
num(1).

test(x, y) :-
  num(x),
  num(y),
  x band y = 1.

.output test

When I use --show=transformed-datalog, I see:

test(x,y) :- 
   num(x),
   num(y),
   (x&y) = 1. // Why is this '&' and not 'band'?

When I use --show=transformed-ram, I see:

  BEGIN_DEBUG "test(x,y) :- \n   num(x),\n   num(y),\n   (x&y) = 1.\nin file /home/langston/code/mate/drop/test.dl [7:1-10:16]"
   QUERY
    IF (NOT (num = ∅))
     FOR t0 IN num
      FOR t1 IN num
       IF ((t0.0bandt1.0) = number(1))  // Why is there no space around the operator here? And now we're back to 'band'?
        PROJECT (t0.0, t1.0) INTO test

A similar thing happens with bshl/bshr.

$ souffle --version
Souffle: 2.0.2-1248-g17bef0b5(32bit Domains)
b-scholz commented 3 years ago

The main purpose for AST/RAM outputs was mainly debugging, but it would be nice if they correspond with the input.

Could you fix this? The printing of these operators happen here: https://github.com/souffle-lang/souffle/blob/cd687c9fcf303bd13f32db1d2652694e50fb1d62/src/ast/IntrinsicFunctor.cpp#L21

b-scholz commented 3 years ago

For RAM it is here: https://github.com/souffle-lang/souffle/blob/cd687c9fcf303bd13f32db1d2652694e50fb1d62/src/ram/IntrinsicOperator.h#L59

b-scholz commented 3 years ago

The translation is happening in the files FunctorsOps.cpp and FunctorOps.h.

SanaaHamel commented 3 years ago

The reason is because we inherited this awful mess where some infix operators have are symbolic and others are identifiers. It's awful. Internally they're mapped onto their 'canonical' name (if you've done Haskell and the like this should be familiar):

This convention is used to automatically deduce how to pretty print operations.

RAM, on the other hand, didn't need to support this (stupid and) ugly identifier infix operator stuff, so it just uses symbolic ops instead. It's inconsistent w/ AST, but it's less code to impl, and shorter and to read (IMO). Nvm, actually read the RAM. It's nuts. Honestly it should either match AST or use canonical naming.

If I had it my way we'd've ditched these ugly identifier infix operators, but hey, we inherited what was already there.