[m-dev.] Typecheck assertions

[Fergus Henderson]

On 02-Jul-1999, Peter Ross <petdr at cs.mu.OZ.AU> wrote:
> 
> If you have an assertion of the form
> 
> :- assertion 
>         (
>                 (some [AB] (app(A, B, AB), app(AB, C, ABC)))
>         <=>
>                 (some [BC] (app(B, C, BC), app(A, BC, ABC)))
>         ).
> 
> Is the following the best way to typecheck these assertions?
> 
> Create a new pred in the form:
> 
> assertion_a :-
>         some [A,B,C,ABC] (
>                 (some [AB] (app(A, B, AB), app(AB, C, ABC)))
>         <=>
>                 (some [BC] (app(B, C, BC), app(A, BC, ABC)))
>         ).
> and then typecheck that.

Shouldn't that be `all [A,B,C,ABC]' rather than `some [A,B,C,ABC]'?

That general approach would certainly work.
It seems like a fairly good approach.

> How hard will it be to generate meaningful error messages this way?

Quite easy.  Basically you'd just need to change hlds_out__write_pred_id.

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