search

LPCIC / elpi

Embeddable Lambda Prolog Interpreter
GNU Lesser General Public License v2.1
283 stars 35 forks source link

eta vs oc (take 2) #223

Closed gares closed 7 months ago

gares commented 7 months ago 
type test-unif o -> o.
test-unif T :- print "Original goal is" T, fail.
test-unif T :- T, !, print "--> Unif success" T "\n".
% test-unif T :- print "--> FAIL in this unification:" T "\n".

main :-
  test-unif ((x\y\X x y) = (x\y\X y x)), !,
  test-unif (Q = (x\y\Q x y)), !,
  test-unif (Z = (x\y\Z y x)), !.

This is incomplete

       with RestrictionFailure ->
        (* avoid fail occur-check on: x\A x = A *)
        match eta_contract_flex depth adepth ~argsdepth:bdepth e a with
        | None -> false
        | Some a -> unif argsdepth matching depth adepth a bdepth b e end

and the code in bind is also incomplete w.r.t. the same problem:

X = x\y\ X y x

is not just an eta, one can restrict X to a\b\Y and then you get a\b\Y = x\y\(a\b\ Y) y x that has a solution. The current code first detect the OC and then tries to amend, both in the optimized UVar case and in the general AppUVar one.

gares commented 7 months ago

CC @FissoreD