[spilling] weird spilling behaviour?

[FissoreD]

is it wanted that: main :- q {p 1} X => q 1 3. is translated into: main :- (p 1 A1 , q A1 A0) => q 1 3. instead of main :- p 1 A1 , (q A1 A0 => q 1 3).

FULL EXAMPLE:

pred p i:int, o:int.
p 1 4.

pred q i:int, o:int.

main :- q {p 1} X => q 1 3. % shouldn't the goal fail?

[gares]

spilling in negative position is broken, it is not even clear what one wants. take

q A {p A 1} X.

should it be

q A Y X :- p A 1 Y.

?

In your example p has a constant input, so any position (but the current one) would do. But if its input was an argument of q then your grafting would be wrong.

[FissoreD]

Mh, I see this is not clear. However, it took me some time yesterday to see why my code behaved strangely :) Maybe we should prevent spilling when used in negative position?

Moreover, when use spilling in positive position, but inside an anonymous lambda-abstraction, the error message is quite difficult to understand, at first sight...

pred p o:int.
p 5.
main :- std.forall [1] (x\ print {p}).

Shouldn't we force a sigma inside the anonymous function for the result of p, or again forbid the use of spilling in anonymous predicates.

In fact, I think spilling is very good, but I complain that, when miss-used, one can spend a lot of time to understand the bug in the code if he is not familiar with spilling

[gares]

hum, in that specific case it should make a sigma. Does it not? It may a bug because we don't know (yet) the types. It surely does a sigma under a pi x\.

I fully agree it is currently a hack.

[FissoreD]

hum, in that specific case it should make a sigma. Does it not?

I post the code generated by the compiler

• main :- std.forall [1] (x\ print {p}). becomes $\to$ main :- std.forall [1] (x\ (p (A0 x) , print (A0 x)). and after the first iteration it produces Fatal error: Unification problem outside the pattern fragment. since it tries to unify p 5 with p (A0 1). the correct compiled version shouldn't be main :- std.forall [1] (x\ sigma A0\ (p A0 , print A0)). ?
• In the case of: main :- pi x\ print {p} the generated code is main :- pi c0 \ p (A0 c0) , print (A0 c0).

It seems that no sigma is produced but rather a pi in the prelude of the rule

[gares]

I wrote sigma, but I meant "put the bound name in scope". In the first case x\ print {p} there is no reason why the output of p should see x (x is not a name, it will be a value, but spilling does not know that)