% File 'app.pl'
%----
:- ensure_loaded(typeops).

:- type int.
:- type nat.
:- subtype negint < int.
:- subtype nat < int.
:- subtype posint < nat.
:- subtype zero < nat.
:- type zero --> 0.
:- type posint --> {X | integer(X), X>0 }.
:- type negint --> {X | integer(X), X<0 }.
:- type list(T) --> [] ; [ T | list(T) ].

:- pred append_old(list(T), list(T), list(T)).
%= pred append(list(@T1), list(@T2), list(@T3)) with T1 =< T, T2 =< T, T3 =< T.
append_old([], L, L).
append_old([X|Xs], Y, [X|XYs]) :- append_old(Xs, Y, XYs).

:- pred append(list(T), list(T), list(@T)).
%= pred append(list(@T1), list(@T2), list(@T)) with T1 =< T, T2 =< T.
append(X, Y, Z) :- append_old(X, Y, Z).


%----------------- TEST QUERIES ----------------------------------------

?- append([0], [1], L), append(L, [-1], X).  % ok
?- append(L, [-1], X), append([0], [1], L).  % ok

?- append([-1], [2], L).              % ok
?- append([0,1], L, [-1]).            % ill-typed
?- append([0,1], L, [1,2,3]).         % ill-typed

?- append_old([-1], [2], L).          % ok
?- append_old([0,1], L, [-1]).        % ok !!!
?- append_old([0,1], L, [1,2,3]).     % ok !!!

/*----------------- TYPICAL OUTPUT -------------------------------------

tap:  Type-Error
      ========== 
  The query 
     :- append([0,1],A,[-1]).
    is not type-consistent.
    
    The clause/query with the last atom GENERALIZED to 
    append(A4,A,[-1])
    would be type-consistent using VT=[A4*list(negint),A*list(negint)]

-----
tap:  Type-Error
      ========== 
  The query 
     :- append([0,1],A,[1,2,3]).
    is not type-consistent.
    
    The clause/query with the last atom GENERALIZED to 
    append(A4,A,[1,2,3])
    would be type-consistent using VT=[A4*list(posint),A*list(posint)]  */
/*------------------- PROLOG OUTPUT -------------------------------------
Output of loading this file in PROLOG: four useless atoms

{Warning: user:append([0,1],L,[-1]) - goal failed}
{Warning: user:append([0,1],L,[1,2,3]) - goal failed}
{Warning: user:append_old([0,1],L,[-1]) - goal failed}
{Warning: user:append_old([0,1],L,[1,2,3]) - goal failed}
*/
