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
903 stars 198 forks source link

ADT Constructors' ordinal value is according to alphabetical order, not declaration order #2499

Open AdiHarif opened 1 month ago

AdiHarif commented 1 month ago

I was trying to define functors that receive ADTs as parameters and couldnt find any documentation about it.

From the tests in this repo i figured that when unpacking an ADT value in the functor implementation, the first value of the returned array is the constructors ordinal number (given that there is at least one parameterized constructor). I assumed that this ordinal value is according to constructors' declaration order, however found out that it is according to alphabetical order.

Is this by design? to be honest i find it somewhat not intuitive...

Example Souffle program:

.functor get_ctor_ordinal(v: T): unsigned stateful

.type T =
      B {}
    | A {}
    | C { x: unsigned }

.decl R(v: T, o: unsigned)

R($B(), @get_ctor_ordinal($B())).
R($A(), @get_ctor_ordinal($A())).
R($C(1), @get_ctor_ordinal($C(1))).

.output R

Functor Implementation:

RamDomain get_ctor_ordinal(SymbolTable* symbolTable, RecordTable* recordTable, RamDomain value) {
    const RamDomain* record = recordTable->unpack(value, 2);
    return record[0];
}

Output:

---------------
R
v       o
===============
$B      1
$A      0
$C(1)   2
===============
quentin commented 1 month ago

Hi, a good explanation of ADT representation is still missing from the docs.

You can refer to https://github.com/souffle-lang/souffle/issues/2055#issuecomment-917902328

And yes, ADT branches are indexed by alphabetical order.

AdiHarif commented 1 month ago

Thanks! Is there a reason for indexing these branching alphabetically?