Mutual exclusion: retroactive check between local clauses and catchall

[gares]

We should track when a predicate has a catch-all rule and when it loads a rule that is mut_excl via a pi-quatified variable.

Currently, if there is a catch all rule followed by the other kind, we detect the problem, but not vice versa.

The simplest fix would be to track the pi-quantified one and error when a catch-all is accumulated (since the other case is already ok).

[FissoreD]

An example breaking the code is the following:

func f int ->.
func f1.
f1 :-
  pi x\ (f x :- print "CIAO") =>
    (f x, fail).
f X :- halt "Mh".
main :- f1.

The call to f x in f1 produces a choice point, which is not expected.

A catch-all rule is a rule where all the indexed input arguments are unification variables.

[gares]

I think we should put in the "pred_info" metadata twp two booleans (maybe with a loc):

• has catch all
• has hyp clause on pi

and no matter in which order we update that info, we end up having both bools set to true, and in that case we error.

[FissoreD]

Yep already done

[FissoreD]

I'm testing and preparing a PR :)

[FissoreD]

Problem in the current set-up:

func f int ->.
func f1.
f1 :- pi x\ (f x :- print "CIAO") => (f x, fail).
f (X as V) :- halt "Mh".
main :- f1.

That is: the term (X as V) is not considered as a catchall since it is not flex term...

[FissoreD]

Also uvar