[m-dev.] Re: for review: add parsing/storing of assertions

[Fergus Henderson]

On 19-Jul-1999, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> Conceptually, you can add (an instance of) the assertion to the clause
[in which it is used]
> as an extra conjunct.  The extra conjunct is ignored at runtime since we
> "know" its valid and should therefore just succeed.  However, at debug
> time it should be checked.  I think its probably a good idea for the
> compiler to keep track of these dummy calls so ultimately the
> declarative debugger will be able to check the assertions.

Yes, I agree; for debugging purposes, it would be helpful if
for each time that the compiler makes use of an assertion,
it somehow recorded that in the hlds__goal.

One way of doing this would be to insert a call to a dummy predicate
associated with the assertion.  Each mode of this predicate would have
determinism `det' and would leave the insts of its arguments unchanged.
(It would have to be polymorphically moded, with the compiler
inferring which modes were used, like we currently do for unifications
and for predicates with no mode declarations.)
The body of the predicate would be empty, in general, although
if the appropriate compiler option was enabled, then in *some* cases the body
could contain code to check the assertion and call error/1 if it fails.
But this could only be done if the assertion body was well-moded in that mode.

But there's a bit of a catch-22 here: these dummy calls should be inserted
only if debugging is enabled, since they might otherwise inhibit optimization.
But `:- assertion' declarations would only be used if optimization is enabled,
because (by the definition of the semantics of `:- assertion' declarations)
a non-optimizing compiler is free to ignore all such declarations.
So they would only show up if you were debugging optimized code.
If you are debugging optimized code, this is presumably because the code
only fails when it is optimized, so having the debugger annotations interfere
with the optimization is quite undesirable.

Another approach would be to add an extra field to the goal_info.
The drawback of this approach is that it would be a little more difficult
to ensure that all of the various optimization phases of the compiler
correctly preserve such annotations.  But the advantage is that we could be
sure that the annotations did not inhibit further optimization. 
The catch-22 described above means that this is probably a better approach.

> I suspect
> the current method of assertions being temporarily treated as predicates
> then the predicate info being thrown away is a mistake.

As I understand it, the predicate info is not thrown away.
We call module_info_remove_pred_id, which removes the pred_id
from the list of valid predicate ids that later passes (e.g. mode analysis,
determinism analysis, code generation) will process, but the information
about the assertion predicate remains in the predicate table.

> We should
> generate a predicate for each assertion (possibly even allow named
> assertions with some suitable syntax) and (in some grades) even
> generate code for these predicates (all arguments will be mode in and
> the predicates should be semidet - the determinism will require some
> fudging where they are used).

Yes, the determinism for the dummy calls should always be `det', not `semidet'.
But all arguments having mode `in' is not sufficient, I think.
For many uses of assertions, the arguments of the dummy calls will not
all have mode `in' -- some will have mode `free -> free', or `ui', etc.

But as discussed above I think it's probably better to use a different
kind of annotation to indicate uses, rather than inserting dummy calls.

> >There's another issue that should be raised:  should there be only one
> >flavor of assertion?  I think there are really two different kinds:
> >assertions that specify (part of) the semantics of a predicate or
> >function, and assertions about their implementation.  The former are
> >the sorts of things one would like to have checked, preferably
> >statically, but if not then dynamically.  If the check fails, the
> >code is probably buggy.  The latter sort of assertion are really just
> >hints to the compiler; if they can be statically checked, so much the
> >better, but if not, we should be prepared to trust the programmer.
> 
> If there is such a distinction (which I have some doubts about), I would
> have thought the implementation-related assertions are the ones the
> compiler would have more chance of checking.  If you look at determinism
> declarations, for example, you can see them a form of assertion.  At the
> high level (semantics) saying a pred is det is an assertion of the
> existence and uniqueness of answers for all possible (well typed)
> inputs (you can write this down in first order logic).  At the low level
> it says something more strict, related to what Prolog people would
> describe as choice points (or lack of).  The compiler is able to check
> the low level information which allows the high level information to be
> inferred.

The low level information about lack of choice points does imply the high
level information about uniqueness of answers, but the low level information
about lack of failure does not quite imply existence of answers -- for that
you need in addition a guarantee of termination.  

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------