[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

[Ralph Becket]

Mark Brown, Thursday, 15 December 2005:
> 
> The reference manual is meant to be self-explanatory so I will omit
> any preliminary remarks at this stage, except to note that one section
> (marked with an XXX) is not complete, and that some of the cross-referencing
> is not ideal and will be improved later.
> 
> Enjoy!

This is good.

> @@ -2910,18 +2912,16 @@
>  
>  Because of this possibility, predicates or functions which are defined
>  using different code for different modes are by default assumed to be
> -impure; the programmer must either (1) carefully ensure that the
> -logical meaning of the clauses is the same for all modes,
> -in which case a @samp{pragma promise_pure} declaration can be used
> -or (2) declare the predicate or function as impure.
> +impure; the programmer must therefore place a purity annotation on the
> +declaration.
>  @xref{Impurity}.
>  
>  In the example with @samp{append} above, the two ways of implementing
> -append do have the same declarative semantics, so we can safely use
> -the first approach:
> +append do have the same declarative semantics, so we can safely promise
> +it to be pure:
>  
>  @example
> -	:- pragma promise_pure(append/3).
> +	:- promise_pure pred append(list(T), list(T), list(T)).
>  @end example

Just as a matter of style, it would be bad to have `promise_pure' on 
an exported predicate; in that case I'd use the pragma instead.

>  In the example with @samp{var/1} above, the two clauses have different
> @@ -8480,14 +8492,21 @@
>  
>  @table @dfn
>  @item pure
> -For pure procedures, the set of solutions depends only on the
> -values of the input arguments.
> -They do not interact with the ``real'' world (i.e., do any
> -input/output) without taking an io.state (@pxref{Types}) as input and
> -returning one as output, and do not change the value of any data
> -structure that will not be undone on backtracking (unless the data
> -structure would be unreachable on backtracking).  Note that equality
> -axioms are important when considering the value of data structures.
> +For pure predicates and functions, there must exist a declarative semantics
> +(that is, a set of ground solutions) which, given the bindings of
> +arguments when called, fully determines all possible bindings at exit.
> +All pure functions must be referentially transparent in the sense that
> +any two expressions which are syntactically equal must be semantically
> +equal.

What about user defined equality?

> +There are four purity annotations that can be used to assert purity
> +levels in code.
> +The first two of these, @samp{impure} and @samp{semipure},
> +are used to declare that a predicate, function or goal has a certain purity.
> +These two annotations are checked by the compiler
> +according to the rules in @ref{Purity inference},
> +and it is an error if they do not match the purity level it infers.
> +The remaining two, @samp{promise_pure} and @samp{promise_semipure},
> +are used to assert that a predicate, function or goal is known to have
> +a certain purity even though it can't be inferred.
> +The compiler does not insist that these annotations match the inferred purity;
> +it instead checks that the promised purity exceeds the inferred purity ---
> +these annotations indicate points in the program where the programmer
> +assumes responsibility for the safety of the code.
> +(As with all such promises, you should use these with the utmost caution:
> +if you lie to the compiler it will have its revenge!)
> +
> +Note that since Mercury code is pure by default,
> +there is no need for a @samp{pure} annotation.
> +Likewise, since asserting that code is impure imposes no burden of proof
> +on the programmer, there is no need for a @samp{promise_impure} annotation.

I think you should mention impure_true here (which should be a builtin,
and we should make semidet_true and semidet_false builtins, too).

> +Purity annotations are compulsory in some, but not all, places.
> +The compiler will report an error if any purity annotation
> +is not consistent with the inferred purity level,
> +or if a purity annotation is not present where one is required.
> +The places where a purity annotation is required are as follows:
> + at itemize @bullet
> + at item
> +In @samp{pred} and @samp{func} declarations for which the definition
> +is inferred to be something other than pure.
> + at item
> +In front of a goal which introduces impurity or semipurity.

Do you mean "atomic goal" here?

> +The only exception to this is that purity annotations are not compulsory
> +on goals that are within an @code{infer_purity} scope (@pxref{Goals}).
> +Inside such a scope, unannotated goals which introduce impurity (semipurity)
> +are treated as if they had an @code{impure} (@code{semipure}) annotation,
> +and all other goals are left unchanged.
> +(Note, however, that there is a current limitation that the purity level
> +of higher-order calls cannot be inferred,
> +so omitting the annotation from a higher-order call is likely to lead
> +to a type error.
> +XXX there may also be a similar limitation whereby argument unifications
> +are not handled properly without an explicit annotation.)

Yes, I was bitten by this one today.

Otherwise that's excellent.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------