ADT definitions accessible from compiled souffle?

[aeflores]

Is there a way to access the ADT definitions from a compiled instance of a souffle program.
I see that a representation of these definitions is included in the directiveMap here https://github.com/souffle-lang/souffle/blob/master/src/synthesiser/Synthesiser.cpp#L353 for printing and reading files, but I don't see a way to access this programmatically.
Am I missing something?

It also looks like the directive maps of all relations include all the ADT definitions? That seems like a lot of unnecessary duplication.

Should there be an ADTTable similar to the recordTable?

[quentin]

I am currently experimenting some kind of programmatic type descriptors in this branch: https://github.com/quentin/souffle/tree/libsouffle

The types of relations and values are made available through a TypeDesc object. A TypeRegistry allow to retrieve the type descriptor from a specified type name, or to retrieve the vector of all known types.

https://github.com/quentin/souffle/blob/1057b07f246698e064df1ef09fe0949377695d85/src/include/souffle/SouffleInterface.h#L420-L426

https://github.com/quentin/souffle/blob/1057b07f246698e064df1ef09fe0949377695d85/src/include/souffle/SouffleInterface.h#L835-L838

https://github.com/quentin/souffle/blob/324dc25b4391eaf0b7700b4c4e25999f5a67fcf6/src/include/souffle/SouffleTypes.h

[aeflores]

Nice! I also noticed that right now it does not seem possible to create tuples programmatically that contain ADTs. The definitions of << operators https://github.com/quentin/souffle/blob/1057b07f246698e064df1ef09fe0949377695d85/src/include/souffle/SouffleInterface.h#L586 do not really support ADT types, they check for types being s, u, f or i, so there is no way to populate a typle with ADT fields as far as I can tell.

[quentin]

UPDATE: #2594 adds ADT packing helpers

---

You can construct ADT values using the records interface. ADT values are stored like regular records, but with some degree of nesting.

ADT values, like Record values, are numeric index references to the record-table. Those references are stored in relation tuples as a RamDomain column:

souffle/src/include/souffle/io/ReadStream.h

Lines 112 to 119 in e4184ab

	case 'r': {
	recordValues[i] = readRecord(source, recordType, pos, &consumed);
	break;
	}
	case '+': {
	recordValues[i] = readADT(source, recordType, pos, &consumed);
	break;
	}

Take a look at readADT:

souffle/src/include/souffle/io/ReadStream.h

Lines 133 to 140 in e4184ab

	RamDomain readADT(const std::string& source, const std::string& adtName, std::size_t pos = 0,
	std::size_t* charactersRead = nullptr) {
	const std::size_t initial_position = pos;
	// Branch will are encoded as one of the:
	// [branchIdx, [branchValues...]]
	// [branchIdx, branchValue]
	// branchIdx

Enum ADT

The simplest class of ADTs are the enumeration: ADT where every branches are empty:

.type Animal = Dog {} | Bird {} | Cat {}

An Animal value is a simple RamDomain value representing the selected branch index. Branches are indexed from 0 in alphabetic order:

souffle/src/ast/analysis/typesystem/TypeSystem.h

Lines 282 to 283 in 1522179

	* Implementation invariant: branches are in stored in
	* lexicographical order.

In this example $Dog() is equivalent to value 2, $Bird() is 0, $Cat() is 1.

This encoding is visible here in readADT:

souffle/src/include/souffle/io/ReadStream.h

Lines 175 to 177 in e4184ab

	if (adtInfo["enum"].bool_value()) {
	return branchIdx;
	}

Non-Enum ADT

The other class of ADTs are the non-enumeration: ADTs where at least one branch is not empty:

.type BinaryTree = 
    EmptyLeaf {} 
  | Node { left: BinaryTree, right: BinaryTree}
  | ValueLeaf { n : number } 

For non-enumerations, an ADT value is a RamDomain reference into the record table. The referenced record has exactly two fields that encode the ADT value, that I will call F1 and F2 in [F1, F2]. The first field F1 stores the selected branch index as described previously. The usage of the second field F2 depends on the form of selected branch.

If the selected branch has a single field, then F2 is set with the immediate value of that field. For instance $ValueLeaf(23) is encoded by record [F1, F2] = [2, 23]:

If the selected branch is empty, or has more than one field, a record is created in the record-table to store those fields value. And F2 is set with the reference to that record. For instance, $Node($ValueLeaf(23), $EmptyLeaf()) is encoded by record [1, F2] where F2 is reference obtained by packing the 2-fields record value [$ValueLeaf(23), $EmptyLeaf()].

The empty branch case is not different from the multiple-fields branch case. F2 set with the reference to the empty record. For instance $EmptyLeaf() is encoded by record [0,F2] where F2 is the reference to the zero-length empty record value. F2 is the value returned by packing the zero-length record: recordTable.pack(std::vector<RamDomain>(), 0).

This encoding is visible here in readADT:

souffle/src/include/souffle/io/ReadStream.h

Lines 236 to 245 in e4184ab

	RamDomain branchValue = [&]() -> RamDomain {
	if (branchArgs.size() != 1) {
	return recordTable.pack(branchArgs.data(), branchArgs.size());
	} else {
	return branchArgs[0];
	}
	}();
	RamDomain rec[2] = {branchIdx, branchValue};
	return recordTable.pack(rec, 2);

[aeflores]

@quentin I still think you need this #2183, or you won't be able to populate at tuple once you have the encoded value.

[quentin]

@aeflores Good point, actually I have been "cheating" by taking an iterator on the tuple with it = tuple::begin() and then storing arbitrary RamDomain values into it *it = adt_ref;. This bypass the type checking unlike <<.

[b-scholz]

Do you need this information in the Datalog program or outside of the Datalog program?

Indeed, the whole type description is dumped for the I/O system in JSON format.