souffle icon indicating copy to clipboard operation
souffle copied to clipboard

Alias type for List and ADT types

Open b-scholz opened this issue 2 years ago • 3 comments

The current version of Souffle prohibits alias types for lists and ADTs. For example,

.type myList = [l:myList, n:number]
.type myEqList = myList

and

.type myADT = b {l:myList, n:number}
.type myEqADT = myADT

will fail.

It is a simple change in the type system. We need a special case. In method TypeDeclarationChecker::checkUnionType the case,

 } else if (!isA<ast::UnionType>(subtype) && !isA<ast::SubsetType>(subtype)) {
            report.addError(tfm::format("Union type %s contains the non-primitive type %s",
                                    type.getQualifiedName(), sub),
                    type.getSrcLoc());
        }

can be extended to

 } else if (!isA<ast::UnionType>(subtype) && !isA<ast::SubsetType>(subtype) && types.getTypes() > 1) {
            report.addError(tfm::format("Union type %s contains the non-primitive type %s",
                                    type.getQualifiedName(), sub),
                    type.getSrcLoc());
        }

for this purpose. Also, I would like to remark that it might be better to introduce an equivalence type class rather than using the union-type class.

However, the I/O system needs fixing as well. I.e., the root type must be passed on (i.e. the actual List / ADT) so that the I/O system can handle the complex type.

b-scholz avatar Sep 08 '21 10:09 b-scholz

I found a bug that may be related to the discussion here.

.type TPositive = number
.decl N(a1:number)
.decl Positive(x:TPositive)
.decl Divisible(x:number, y:number)
N(-2).
N(i+1) :- N(i), i < 5.
Positive(as(x, TPositive)) :- N(x), x > 0.
Divisible(x, y) :- N(x), Positive(y), x % y = 0.
.output Positive
.output Divisible

In the above, the last clause defining Divisible causes errors. When you remove the line (and corresponding .output), you will not get an error.

hide-kawabata avatar Sep 13 '21 03:09 hide-kawabata

Also, the following example is not working:

.type L=[a:L,  b:number]
.type A=L

.decl R(x:A)
R(nil).
R([nil,1]).

.output R

b-scholz avatar Sep 13 '21 10:09 b-scholz

We have similar issues with ADTs:

.type L= next {a:L,  b:number} | end {}
.type A=L

.decl R(x:A)
R($end()).
R($next($end(),1)).

.output R

b-scholz avatar Sep 13 '21 10:09 b-scholz