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

[Lee Naish]

Some general comments:

Assertions are a very general concept and a very flexible syntax has
been chosen for them.  For now, they are just used for the accumulator
introduction optimisation, but its likely that in the future they will
be used for various other things (determinism detection, the declarative
debugging oracle, promise_one_solution,...).  From my experieice with
assertions with assertions for declarative debugging, sometimes
specialised assertions/representations are worthwhile.  Its worth thinking
about this broader/longer term view of assertions a bit more and, eg
acknowledging in the documentation that this is the first version of
assertion support and its geared towards accumulators (ie associativity).

Peter Ross <petdr at cs.mu.OZ.AU> writes:

>+	% check_assertion
>+	%
>+	% An assertion is valid, iff the assertion begins with the
>+	% universally quantified variables and each variable is
>+	% explicitly quantified before its use.  At a later date these
>+	% restrictions should be relaxed, once we work out how to

Best avoid the "valid" terminology - all assertions should be (logically)
valid.  I suggest "well formed".  check_assertion ->
check_assertion_well_formed.

Fergus' comments re the quantifier are correct I think.  However, I
don't think it matters too much in general if the syntactic form of
assertions is restricted.  For the different uses of assertions its
typically easiest to look for syntactic matches rather that applying a
FOL theorem prover to the assertions to see if what you are looking for
is a consequence of the assertions.  Of course it should be well
documented what syntactic forms are allowed/recognised for different
optimisations etc.

>+	% A table that records all the assertions in the system.
>+	% 
>+:- type assert_id.
>+:- type assertion_table.
>+
>+:- pred assertion_table_init(assertion_table::out) is det.
>+
>+	%
>+	% After typechecking is finished the pred_info describing the
>+	% assertion should be removed from further processing and the
>+	% pred_id which describes the assertion stored in the
>+	% assertion_table.
>+	%
>+:- pred remove_assertion_from_further_processing(pred_id::in,
>+		module_info::in, module_info::out) is det.
>+
>+:- pred assertion_table_lookup(assertion_table::in, assert_id::in,
>+		pred_id::out) is det.

I agree with previous comments re naming of
remove_assertion_from_further_processing.

Also, one would think the interface above should include
assertion_table_add_assertion.

I suspect its worth making this interface a bit more abstract also.  In
particular, this interface makes the assumption that assertions are
represented by pred_ids.  A separate assertion type might be better - in
the future you might want to store assertions corrresponding to
determinism declarations, various promise constructs etc in the
assertion table and a pred_id might not be a convenient way to do this.

I also wonder if there should be a somewhat higher level interface to
the assertion table corresponding to what information you are actually
looking for (eg associativity), rather than a simple lookup.  The idea
is that ultimately you might be *inferring* things from your collection
of assertions.  You want this inference to be done within some well
defined interface instead of in some ad hoc way, possibly in several
different places in the compiler which use assertions in different ways.

	lee
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------