2024-11-21 23:33 AEDT
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000193mercuryBugpublic2011-03-28 07:562012-07-06 11:19
Reportercolanderman 
Assigned To 
PrioritynormalSeveritytweakReproducibilityalways
StatusconfirmedResolutionopen 
Product Version 
Target VersionFixed in Version 
Summary0000193: --introduce-accumulators doesn't recognize "promise all" containing type annotation
DescriptionSee attached program. Accumulator introduction works with the commented-out "promise all", but not when a do-nothing type annotation is added as in the uncommented "promise all".
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0000325

juliensf (administrator)

2011-04-07 08:10

 It also doesn't work if you module qualify the "*" operators on the lhs of the promise,
instead of type qualifying them.

~0000332

juliensf (administrator)

2011-05-14 02:38

 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 (**)
+Notes

-Issue History
Date Modified Username Field Change
2011-03-28 07:56 colanderman New Issue
2011-03-28 07:56 colanderman File Added: accumbug.m
2011-04-07 08:10 juliensf Note Added: 0000325
2011-05-14 02:38 juliensf Note Added: 0000332
2011-05-14 02:38 juliensf Status new => confirmed
+Issue History