search

LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
290 stars 36 forks source link

[typeabbrev] type `dl (dl A)` where `dl` is typeabbrev is no more "looping" #266

Closed FissoreD closed 2 months ago

FissoreD commented 2 months ago 
typeabbrev (dl A) (list A).
pred p i:dl (dl A).

dl (dl A) is no more considered as an invalid (looping) type.

A typeabbrev can be created only if all of the constants in it have already been declared before it. Recursive typeabbrev (like typeabbrev dl dl are still forbidden)

gares commented 2 months ago

Can't we detect statically that the typeabbrev is not silly, as in the LHS does not occur in the RHS (and the RHS is only made of known symbols)? The last part may require some cleanup (planned but not done).