[m-users.] Determinism issue with parser

[Sean Charles (emacstheviking)]

Zoltan, your replies have always helped and continue to do so.

If by "one" you mean one determinism declaration, they why do you
"change one and recompile"?

The answer; simple frustration at being fully cognisant of my own ignorance, that’s why.

I —understand— the reasons why it is telling me I am wrong but then chaos seems to erupt inside my head. It’s —my— decision as to the determinism of the code I write, IIUIC that’s the point of declaring it, then the compiler tells me otherwise when it knows better (often).

As for using solutions/1, it crossed my mind but for me that’s a biiig code smell and I refused to do it.

Part of my confusion is understanding what it means to have more than one solution if the inputs are the same?!?! How can that be? For example, in this predicate where I check for a body form:

:- pred parse_body_term(snode::out, astcon::in, astcon::out) is multi.

parse_body_term(Term, !A) :-
    (
        parse_atom(Term, !A)
    ;
        parse_list(Term, !A)
    ;
        parse_map(Term, !A)
    ;
        parse_feltcall(Term, !A)
    ;
        parse_fncall(Term, !A)
    ;
        parse_sexp(Term, !A)
    ).

I thought that this was semidet because either one of those disjuncts succeed or they all fail, I don’t understand why it says multi, multi is ‘can’t fail, >1 solutions’ but if I consume tokens in the parse_map() disjunct branch, how can it then come back for more? I just don’t get it, that’s something that really confuses me at the moment. Hence my question ‘what does it mean to have more than one solution?’. 

det: for example ‘*’, given x*y, the result is deterministic.
semidet: for example, given x/y, if y is nonzero the result is deterministic, if y is zero presumably it fails. pedagogical usage here that’s all.

for me the confusion starts with `multi`, to have more than one solution surely it has to be called more than once with different inputs or is stepping through a set of facts?

I think if I had managed to get mdb to work it might help to single step the code but I tried for a few hours and emacs version was wrong, lots of problems etc so I went back to ’thinking’ about it and trace[] all over the place.

Not a good place to be at the moment but things worthwhile are never easy to attain.

Thanks.


> On 4 Jul 2021, at 16:56, Zoltan Somogyi <zoltan.somogyi at runbox.com> wrote:
> 
> 
> 2021-07-05 01:21 GMT+10:00 "Volker Wysk" <post at volker-wysk.de>:
>> I've built a big parser for my project, too. It should always produce one
>> solution; it can't fail. But the compiler can't infer that it is
>> deterministic, for many parts of it. (That would be undecidable.) 
>> 
>> So I've resigned to this state of affairs. I just collect all the (exactly
>> one) solutions with solutions/2 and produce an error message in case there
>> should be more than one, which would be a bug in my parser.
> 
> That works, but I would consider it fragile. The reason is that convincing
> someone (the next maintainer of the parser, perhaps) that there will be
> exactly one overall solution requires a single correctness argument over
> the entire code, and humans are not very reliable as reasoning machines;
> the longer the argument, the higher the probability of error.
> 
> I would instead add disambiguation code to the places in the parser
> than can introduce (as far as the compiler is concerned) the possibility
> of nondeterminism. You can you can see why there is no such possibility;
> I would try  to make the compiler that too. In most cases, this is not too hard,
> at least in my experience.
> 
> This approach replaces a single bug, global correctness argument with lots of
> small, local correctness arguments, which can be understood, documented,
> and if need be fixed, much more easily. Modularity in correctness arguments,
> if you will.
> 
> Zoltan.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/users/attachments/20210704/043b2328/attachment.html>