Setting a variable can apparently skip code

[swasey]

In some circumstances, Elpi skips code it should interpret.

In the following, std.fatal-error "Skipped" inside should_panic should run, but does not. (The continuation doesn't matter. I picked a fatal error to speed up minimization.)

EDIT: Simplified the example.

    pred should_panic o:bool.
    should_panic D :- D = ff, std.fatal-error "Skipped".

    main :- (should_panic tt; true).

I noticed this under coq-elpi and elpi 1.18.2. It seems to persist in 1.19.5 and in elpi master (commit a349485a).

To run:

    cd ELPI
    dune b
    dune exec -- elpi -test FILE.elpi

[gares]

Hum, I think there is a misconception in the meaning of "output".

should_panic D is unified with should_panic tt, this sets D to tt. Then D = ff, or better tt = ff is run, that fails, hence fatal-error is never reached.

Output means that a clause like p tt is used on a goal like p X, that is the goal can be assigned by the unification step. If you set the argument as input, then the clause p tt would not be used for p X since "it expects to read data from the first argument, but the goal provides none". I'm under the impression you expect output to mean "don't look at the goal until the whole clause has run".

Does this make sense?

[swasey]

It makes some sense, and is in line with the push back I expected.

If the only side-effects were to unification variables, I'd be happier with the present situation. :)

EDIT: That said, if this is well-known and expected behavior for (lambda) prolog, I'd be happy to close the issue.

[gares]

I'm a bit lost ;-)

I don't get exactly what you expect. Take these two rules:

p X :- X = t, stuff.
p X' :- X = t, stuff, X' = X.

The latter is a transformation of the former that ignores X' value until the very end. In the pure world of logic, they are equivalent. Operationally they are not, esp if stuff performs side effects.

Maybe if you give me a larger example and you explain me the actual issue I can suggest some trick to avoid it bites again. For example I extensively use std.do! to kill backtracking, especially in code adding stuff to the Coq environment. In this the kind of effect that bites you?

[swasey]

I had guessed wrong about the operational model. I guessed that your transformed p X' :- X = t, stuff, X' = X. was roughly how your untransformed p X :- X = t, stuff. worked.

I don't think there's a bug here. (And I cannot argue that the operational model I had in mind even works.)

[gares]

In your defense, Prolog modes are a named a misleadingly, since output means input_or_output, in the sense that no data is required, but if some data is present then it can be used.

[swasey]

Janno made a very similar point offline. :)

Thanks for the time. Closing this issue.