:- ensure_loaded(typeops_meta).

% meta-programming
%
% foldl/4 predicate
%   foldl(op, b, [e1, e2, ..., en], ((...((b op e1) op e2)...) op en))
        
           
 
%+++++++++++++++++++++++++++++ type definitions +++++++++++++++++++++++ 

:- import_type(prolog_types).
 
%+++++++++++++++++++++++++++++ predicates  +++++++++++++++++++++++ 

:- import_pred(prolog_meta, fcall/4).
:- import_pred(prolog_meta, fcall/3).
:- import_pred(prolog_meta, fcall/2).

:- import_pred(prolog_meta, '>='/2).
:- import_pred(prolog_meta, '=<'/2).
:- import_pred(prolog_meta, '>'/2).
:- import_pred(prolog_meta, '='/2).
:- import_pred(prolog_meta, !/0).
:- import_pred(prolog_meta, is/2).
:- import_pred(prolog_meta, integer/1).


:- pred foldl(meta((trmName(@T1, @T, @T1) of mpred)), T1, list(T), @T2)
        with T1 =< T2.
foldl(_F, B, [], B).
foldl(F, Bs, [A|As], Cs) :-
	fcall(F, Bs, A, Bs1),
	foldl(F, Bs1, As, Cs).

:- pred foldl_wrong1(meta((trmName(T, T, T) of mpred)), T, list(T), T).
foldl_wrong1(_F, B, [], B).
foldl_wrong1(F, Bs, [A|As], Cs) :-
	fcall(F, Bs, A, Bs1),
	foldl_wrong1(F, Bs1, As, Cs).

:- pred foldl_wrong2(meta((trmName(@T1, @T, @T1) of mpred)), T1, list(T), T1).
foldl_wrong2(A, B, C, D) :- foldl(A, B, C, D).

:- pred foldl_wrong3(meta((trmName(T1, T, T1) of mpred)), T1, list(@T), @T1).
foldl_wrong3(A, B, C, D) :- foldl(A, B, C, D).

:- pred foldl_wrong4(meta((trmName(@T1, @T, @T1) of mpred)),
		                                      @T1, list(@T), @T1).
foldl_wrong4(A, B, C, D) :- foldl(A, B, C, D).

:- pred foldl_wrong5(meta((trmName(T1, T, T1) of mpred)),
		                                      @T1, list(@T), @T1).
foldl_wrong5(A, B, C, D) :- foldl(A, B, C, D).

%-----------

:- pred append(list(T), list(T), list(@T)).
append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).


% insert number into sorted list
:- pred insert(numexpr,list(numexpr), list(numexpr)).
insert(N,[],[N]).
insert(N, [H|L], O) :- 
	N =< H, 
	O = [N,H|L].
insert(N, [H|L0], [H|L]) :- 
	N > H, 
	insert(N, L0, L).

:- pred converse_insert(list(numexpr), numexpr, list(numexpr)).
converse_insert(A, B, C) :- insert(B, A, C). 

:- pred plus_nat(nat, nat, nat).
plus_nat(X,Y,Z) :- integer(X), integer(Y), X > 0, Y > 0, Z is X + Y.

%-----------

?- foldl(append, [], [[1,2,3], [5,6], [7,8,9]], X).
?- foldl_wrong1(append, [], [[1,2,3], [5,6], [7,8,9]], X).
?- foldl_wrong2(append, [], [[1,2,3], [5,6], [7,8,9]], X).
?- foldl_wrong3(append, [], [[1,2,3], [5,6], [7,8,9]], X).
?- foldl_wrong4(append, [], [[1,2,3], [5,6], [7,8,9]], X).
?- foldl_wrong5(append, [], [[1,2,3], [5,6], [7,8,9]], X).

%----------

?- foldl(insert, [], [3,2,4,8], Ys).                % ill-typed
?- foldl(converse_insert, [], [3,2,4,8], Ys).       % ok

?- foldl_wrong1(insert, [], [3,2,4,8], Ys).          % ill-typed 
?- foldl_wrong1(converse_insert, [], [3,2,4,8], Ys). % ill-typed !!!

%----------

?- foldl(append, [], [[1,2,3], [5,6], [7,8,9]], [-1]).        % ill-typed
?- foldl_wrong2(append, [], [[1,2,3], [5,6], [7,8,9]], [-1]). % ok !!!

%----------

?- foldl(plus_nat, 1, [1, -2, 3], -1).                % ill-typed
?- foldl_wrong2(plus_nat, 1, [1, -2, 3], -1).         % ill-typed
?- foldl_wrong3(plus_nat, 1, [1, -2, 3], -1).         % ill-typed
?- foldl_wrong3(plus_nat, 1, [1, -2, 3], X).          % ok !!!

%----------

?- foldl(append, [1], [[1,2,3], [5,6], [7,-8,9]], X).        % ok
?- foldl_wrong4(append, [1], [[1,2,3], [5,6], [7,-8,9]], X). % ill-typed !!!
?- foldl_wrong5(append, [1], [[1,2,3], [5,6], [7,-8,9]], X). % ok

%----------

?- foldl(append, [1], [[5,6], [7,-8,9]], [1,5,6,7,-8,9]).       % ok
?- foldl_wrong4(append, [1], [[5,6], [7,-8,9]], [1,5,6,7,-8,9]).% ill-typed !!!
?- foldl_wrong5(append, [1], [[5,6], [7,-8,9]], [1,5,6,7,-8,9]).% ill-typed !!!

