|
|
The problem here is that processing the type qualification introduces extra unifications to the goals
generated for the promise but the code in compiler/assertion.m that examines the promise goal
does cover the situation where extra unifications are present.
(1) The working case
For the declaration:
:- promise all [A, B, C, ABC] (A * B) * C = ABC <=> A * (B * C) = ABC.
the corresponding "promise" predicate generated by the compiler is:
accumbug.'promise__10__accumbug.m'(A, B, C, ABC) :-
\+ (
ABC = int.(V_5 * C),
V_5 = int.(A * B),
\+ (
ABC = int.(A * V_6),
V_6 = int.(B * C)
)
),
\+ (
ABC = int.(A * V_8),
V_8 = int.(B * C),
\+ (
ABC = int.(V_7 * C),
V_7 = int.(A * B)
)
).
(2) The broken case
For the declaration:
:- promise all [A, B, C, ABC] (A * B) * C = ABC : int <=> A * (B * C) = ABC.
the corresponding "promise" predicate generated by the compiler is:
accumbug.'promise__9__accumbug.m'(A, B, C, ABC) :-
\+ (
V_5 = int.(V_6 * C),
V_6 = int.(A * B),
V_5 = ABC, (**)
\+ (
ABC = int.(A * V_7),
V_7 = int.(B * C)
)
),
\+ (
ABC = int.(A * V_10),
V_10 = int.(B * C),
\+ (
V_8 = int.(V_9 * C),
V_9 = int.(A * B),
V_8 = ABC (**)
)
).
The code in assertion.m does not account for the extra unifications at (**) |
|
accumbug.m (302) 2011-03-28 07:56