:- op(950,fy, $).
$(X) :-
	  copy_term(X,Y),numbervars(Y,0,_),portray_clause(call:Y),nl,
	  X,
	  copy_term(X,Z),numbervars(Z,0,_),portray_clause(exit:Z),nl.

... --> [] | [_], ... .

(A | B) --> A ; B.


seq(Es,Es) -->
	[].
seq([E|Es0],Es) -->
	[E],
	seq(Es0,Es).

spec(Es0,Es) -->
	seq(_,_),
	[E],
	seq(Es0,Es1),
	rspec(E,Es1,Es).

rspec(E,Es0,Es) -->
	[E],
	seq(Es0,Es1),
	(	{Es1=Es}
	|	rspec(E,Es1,Es)
	).

alleq(_).
alleq(Xs1) :-
	phrase(spec(Xs2,[]),Xs1),
	alleq(Xs2).


t_arg(f(X,Y),X,Y).
g_arg(g(X,Y),X,Y).

n_n_skel(S, S, _).
n_n_skel(s(S0), S, T) :-
	t_arg(T, X, Y),
	n_n_skel(S0, S1, X),
	n_n_skel(S1, S, Y).


test(n,[nondet]) :-
	n_n_skel(s(0),_,_).

nat(0).
nat(s(N)) :-
	nat(N).


call_nth(Goal, C) :-
	State = count(0),
	Goal,
	arg(1, State, C1),
	C2 is C1+1,
	nb_setarg(1, State, C2),
	C = C2.


gen(Specific, SVars, General) :-
   $nat(S0),
   n_n_skel(S0,S1, Specific),  termalleq(Specific),
   term_variables(Specific, SVars),
   n_n_skel(S1, _, General),  termalleq(General).


wrong(General, Specific) :-
   gen(Specific, SVars, General),
   (   subsumes_term(General, Specific)
   ->  \+ (  General = Specific,
	     term_variables(SVars, SVars2),
	     SVars == SVars2
	   )
   ;   \+ \+ (     unify_with_occurs_check(General, Specific),
		term_variables(SVars, SVars2),
		SVars == SVars2
	   )
   ).




test(alle, [(occurs_check=Flag):Fall:(CGoal>Goal) == nix]) :-
%	S0 = s(s(s(s(s(s(s(0))))))),
	call_nth((
		  nat(S0),
		  n_n_skel(S0,S1, Specific),  termalleq(Specific),
		  term_variables(Specific, SVars),
		  n_n_skel(S1, _, General),  termalleq(General)), Nth),
	( Nth mod 100000 =:= 0 -> $(Nth^true) ; true),
	Goal = subsumes(General, Specific),
	copy_term(Goal,CGoal),
	Goal,
	(  Fall=1, \+ term_variables(SVars,SVars) % untouched
	;	Fall=2, General \== Specific
	).

termalleq(Term) :-
	term_variables(Term, Vars),
	alleq(Vars).



:- end_tests(subsumes2).