|
Notes |
|
|
|
Ian, what exactly are you talking about? The example you attached
doesn't seem to match the description you posted.
Note that just because the compiler can replace goals, doesn't
necessarily mean it will. Also, in order to be able to safely be
able to replace a goal the compiler must be able to prove that it
the goal terminates and does not throw an exception.
If you run your example with --fully-strict --no-inlining and with --enable-termination --analyse-exceptions
you will get the same result as the case with inlining enabled.
(If you look in compiler/goal_form.m you will notice that in the absence
of those two analyses the compiler cannot infer termination/non-exception
throwing across procedure boundaries.)
In any case, the real problem is that the following purity promise is
a lie:
promise_pure (
impure set_m(I)
)
An additional complication in this case, is that trace goals have a
particular semantics w.r.t goal replacement, i.e. they are never replaced
but calls to procedures containing them may be.
|
|
|
|
(0000032)
|
maclarty
|
|
2007-10-18 18:21
|
|
I think you misunderstood what I was saying.
The documentation currently says that with --fully-strict, the compiler is *not* allowed to replace (semi)pure det goals with no outputs, however the compiler replaces the following with 'true' when the --fully-strict option is given.
promise_pure (
impure set_m(I)
)
The attached example illustrates this (don't you get the output 0 2 when you compile fs.m with --fully-strict?).
Yes, I know the promise_pure is a lie, and I'm not actually using this in any real code. It was just something I came across and I didn't expect this behaviour based on what the reference manual says. |
|
|
|
|
The documentation and the implementation seem to differ on what should be
happening with --fully-strict / --no-fully-strict.
(1) The comments (and code) in compiler/simplify.m mean suggest that if --fully-strict
is enabled then det goals with no outputs should not be replaced by true, and
goals that always fail should not be replaced by false.
(2) The documentation gives a different impression: rather than preventing the compiler
from replacing such goals, --fully-strict and --no-fully-strict just alter the requirements
under which the replacement can occur.
For --no-fully-strict the compiler can replace any semi(pure) det goal with no outputs,
regardless of whether it terminates or throws an exception. (And similarly for the always
fails case.)
For --fully-strict it can only perform that replacement if it can prove that the goal does
terminate and does not throw an exception.
The help message for --no-fully-strict says:
"Allow mmc to optimize away infinite loops or calls to error/1"
That suggest to me that --fully-strict is still allowed to optimise away the goals if
doing so won't change the termination or exception throwing properties of the
program, i.e. doing so won't turn a non-terminating program into a terminating one.
(The reference manual says something.)
It doesn't appear that this is what the compiler does though. There is a bug somewhere here,
I'm just not sure what it is. We should decide what --fully-strict/--no-fully-strict actually
mean before trying to work that out though. |
|
|
|
(0000034)
|
maclarty
|
|
2007-10-19 09:17
|
|
Perhaps we should make the semantics of --no-fully-strict simply:
Allow the compiler to improve completeness by replacing infinite loops or calls to error with 'true' or 'false'.
And then change simplify.m so that it doesn't use the --fully-strict option to decide if it can replace terminating (semi)pure det goals with no outputs with 'true' (similarly for failing goals).
The last change I made to the docs tried to get the docs more in line with what the compiler actually does. But I now think we should be fixing the compiler to get it in line with the original docs. The original docs don't say anything about terminating (semi)pure goals that produce no outputs, so simply.m shouldn't be checking the --fully-strict options to decide if it can optimise these away or not (they don't affect completeness anyway). |
|
|
|
|
Actually, looking at it with fresh eyes, the code in simplify.m does the
correct thing, i.e. behaviour (2) in my last note, either --no-fully-strict
is set or the goal must terminate and not throw an exception. (I mistook
the disjunctions for conjunctions last night.) |
|
|
|
|
Incidentally, this means that the warning message at compiler/simplify.m:653
is incorrect because compiling with --fully-strict is not sufficient
to disable the optimisation. |
|
|
|
|
|
Fixed - see log message for r1.219 of compiler/simplify.m. |
|
fs.m (452) 2007-10-12 12:57