[m-rev.] Re: for review: parsing_utils improvements

[Ian MacLarty]

On Tue, Sep 29, 2009 at 4:06 PM, Julien Fischer
<juliensf at csse.unimelb.edu.au> wrote:
>
> On Tue, 29 Sep 2009, Ian MacLarty wrote:
>
>> On Tue, Sep 29, 2009 at 12:50 PM, Ian MacLarty
>> <maclarty at csse.unimelb.edu.au> wrote:
>>>
>>> Index: library/parsing_utils.m
>>> ===================================================================
>>
>> ...
>>>
>>> +
>>> +parse(InputString, SkipWS, Parser, Result) :-
>>> +    % This is pure, because it will always return the same results for
>>> +    % the same inputs (the mutable in Src cannot be accessed outside
>>> +    % of the promise_pure scope below).
>>> +    promise_pure(
>>> +        new_src_and_ps(InputString, SkipWS, Src, PS0),
>>> +        ( Parser(Src, Val, PS0, _) ->
>>> +            Result = ok(Val)
>>> +        ;
>>> +            MutVar = Src ^ error_info,
>>> +            semipure get_mutvar(MutVar, error_info(Offset, MaybeMsg)),
>>> +            offset_to_line_number_and_position(src_to_line_numbers(Src),
>>> +                Offset, Line, Col),
>>> +            Result0 = error(MaybeMsg, Line, Col),
>>> +            % We make parse/4 cc_multi because declaratively
>>> +            % parse(Str, SkipWS, Parser, error(MaybeMsg, Line, Col)) is
>>> true
>>> +            % for all MaybeMsg, Line and Col iff
>>> +            %   new_src_and_ps(Str, SkipWS, Src, PS0),
>>> +            %   Parser(Src, _, PS0, _)
>>> +            % is false, but operationally MaybeMsg, Line and Col are
>>> +            % restricted to one value each.
>>> +            cc_multi_equal(Result0, Result)
>>
>> Peter Wang and have been discussing whether this should be cc_multi
>> and we both think it should actually be det.  The reason is that the
>> determinism is an operational property of the procedure and not a
>> declarative property.  From the reference manual:
>>
>> For each mode of a predicate or function,
>> we categorise that mode according to how many times it can succeed,
>> and whether or not it can fail before producing its first solution.
>>
>> So, I propose to make the parse/4 predicate det.  Are the any objections?
>>
>> By the same reasoning I think that exception.try should also be det
>> and not cc_multi.  Would there be any objections to changing that? (in
>> a separate diff of course)
>
> Yes, because that's not the model of exception handling that is used in
> Mercury.
>
> See the following post from Fergus to mercury-users,
> <http://www.mercury.csse.unimelb.edu.au/mailing-lists/mercury-users/mercury-users.9807/0010.html>,
> from back when the exception module in its current (more or less) form
> was introduced.
>

My understanding of why try is cc_multi is because the declarative
semantics of try don't say what exception you'll get if you get an
exception.  Indeed the declarative semantics don't even say when
you'll get an exception.  So the interpretation of try always includes
an infinite number of atoms with exceptions in the result argument
position.  So in that sense you can view it as multi and the cc_multi
is because we only pick one of those atoms.

But how is that different from what is happening in parse/4? (Or do
you think parse/3 should be cc_multi?)  We could give the declarative
semantics of parse/3 as:

parse(Input, Parser, Result) <=>
    new_src_and_ps(Str, Src, PS0),
    ( Parser(Src, Val, PS0, _), Result = ok(Val)
    ; not Parser(Src, _, PS0, _), Result = error(_, _, _)
    )

So declaratively, if Parser(Src, _, PS0, _) is false, Result will be
error/3, but the arguments to error/3 are unspecified.  This looks a
lot like the declarative semantics of try.  So surely parse/3 should
be cc_multi too?

But then this use of cc_multi doesn't seem to fit the notion of
determinism described in the reference manual, which only talks about
how many times a *procedure* should *succeed* (an operational
property).  parse/3 can succeed exactly once, as can try, so surely
their determinisms should be det?

Here's another interesting example:

:- pred p(list(T)::free >> list(free)) is det.
p([_]).

This compiles.  It succeeds only once, but declaratively it has many
solutions (the interpretation includes many ground atoms).  If try is
cc_multi then why isn't p multi?

Ian.

--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------