Lattice support

[julienhenry]

This PR implements support for lattice elements in Soufflé, in a similar way as the Flix language (see https://flix.dev/ and in particular this paper )

Given a type named myType declared with .type myType = ..., one can now attach a lattice description for this type in the form :

.lattice myType<> {
    Lub -> @mylub(_,_)
    Glb -> @myglb(_,_)
    Bottom -> $myBottom()
    Top -> $myTop()
}

Now, one can declare a relation with lattice arguments :

.decl Relation R(x:number, y:number, z:myType<>)

Semantically, a tuple R(x,y,z) where z is a lattice element implies all tuples R(x,y,z') where z' <= z is the lattice.

Additionally, such relation R will ensure at each time that there is a single fact of the form R(x, y, ...), and ... will be the least upper bound (using the Lub specification of the lattice) of all the otherwise produced tuples of the form R(x, y, ...).

Clauses using atoms containing lattice attributes will behave accordingly to the semantics of lattice:
Example:

.type Sign =
    Bottom{}
  | Negative{}
  | Positive{}
  | Top{}
  | Zero{}

.lattice Sign<> {
    Bottom -> $Bottom(),
    Lub -> @sign_lub(_,_),
    Glb -> @sign_glb(_,_)
}

Top($Top()).
Pos($Positive()).

A(x) :- Pos(x), Top(x).

will produce the fact A($Positive()) because the fact Top($Top()) implies Top($Positive()) ($Positive() < $Top() in the lattice). Technically, x will be evaluated as the the GLB of the x in Pos(x) and the x in Top(x).

Note that it is still possible to use the type myType as is without the lattice description :

.decl Relation R(x:number, y:number, z:myType)

and the relation R will behave as a regular relation, without automatic lub/glb.

See test interface/lub for a few examples using lattice

For the time being, there is a restriction on the Lub and Glb definitions : they can only be user-defined functors with the right signature. This can be extended in future PRs.

[quentin]

First quick read.

[codecov]

Codecov Report

Merging #2438 (7571422) into master (2914f7b) will increase coverage by 0.24%.
Report is 19 commits behind head on master.
The diff coverage is 77.32%.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #2438      +/-   ##
==========================================
+ Coverage   77.75%   78.00%   +0.24%     
==========================================
  Files         474      483       +9     
  Lines       31164    31999     +835     
==========================================
+ Hits        24232    24961     +729     
- Misses       6932     7038     +106     

Files	Coverage Δ
src/FunctorOps.cpp	60.81% <ø> (ø)
src/RelationTag.h	53.03% <ø> (+0.79%)	⬆️
src/ast/Attribute.h	100.00% <100.00%> (ø)
src/ast/Component.h	100.00% <ø> (ø)
src/ast/IterationCounter.cpp	100.00% <100.00%> (ø)
src/ast/Lattice.h	100.00% <100.00%> (ø)
src/ast/Program.h	100.00% <ø> (ø)
src/ast/QualifiedName.h	94.11% <ø> (ø)
src/ast/Relation.h	100.00% <100.00%> (ø)
src/ast/Term.h	75.00% <100.00%> (-15.00%)	⬇️
... and 76 more

... and 9 files with indirect coverage changes

[quentin]

Great feature and impressive work.
Would be very nice to have it documented on Souffle's website.