unifiable.chr

:- module(unifiable, [t/2, t_var/2, capture/2, type(tags/0)]).
:- use_module(prelude).
:- chr_constraint t/2, t_var/2, capture/2.
:- chr_type tags ---> var_atom ; atom_eq ; atom_neq ; struct_mismatch ; struct_match.

% var-vs-atom: succeeds.
t(var_atom, R) <=> unifiable(_, quote(foo)) | R = yes.
t(var_atom, R) <=> R = no.

% atom-vs-atom equal: succeeds.
t(atom_eq, R) <=> unifiable(quote(foo), quote(foo)) | R = yes.
t(atom_eq, R) <=> R = no.

% atom-vs-atom different: fails.
t(atom_neq, R) <=> unifiable(quote(foo), quote(bar)) | R = yes.
t(atom_neq, R) <=> R = no.

% structure mismatch: fails.
t(struct_mismatch, R) <=> unifiable(quote(f(_)), quote(g(_))) | R = yes.
t(struct_mismatch, R) <=> R = no.

% same-shape compound: succeeds.
t(struct_match, R) <=> unifiable(quote(f(_, 2)), quote(f(1, _))) | R = yes.
t(struct_match, R) <=> R = no.

% No-binding probe: after unifiable(X, foo), X must still be unbound.
t_var(X, R) <=>
    unifiable(X, quote(foo)),
    var(X) | R = still_unbound.
t_var(_, R) <=> R = bound.

% Capture the boolean directly.
capture(X, R) <=>
    R is unifiable(X, quote(foo)).