:- ensure_loaded(typeops).
% :- typical_intern(assert(alltrace)).

% predicate declarations with a parametric type argument 
% (a partial ordered set, poset(T)) 

%+++++++++++++++++++++ type imports and definitions +++++++++++++++++++ 

:- import(prolog_io).

%----------------------------
% A partially ordered set is internally represented by a structure
:- type poset(T) -->
        poset( list(T),            % domain
               list(order1(T))).   % order relationships

:- type order1(T) --> T =< T.


%+++++++++++++++++++++++++++++ declarations +++++++++++++++++++++++ 


:- pred po_leq(poset(T),T,T).
% po_leq(PO, X, Y) is true, if X =< Y in  PO

:- pred po_lub(poset(T),S1,S2,S3) -> S1 =< T, S2 =< T, S3 =<T.
% po_lub(PO, X,Y) = Z         least upper bound
po_lub(PO, X,Y,Z) :- po_leq(PO, X,Z), po_leq(PO, Y,Z), 
                     \+ ( po_leq(PO, X,ZZ), po_leq(PO, Y,ZZ), 
                          \+ po_leq(PO, Z,ZZ) 
    			).

:- pred po_mub(poset(T),S1,S2,S3) -> S1 =< T, S2 =< T, S3 =<T.
% po_mub(PO, X,Y) = Z      minimal upper bound
po_mub(PO, X,Y,Z) :- po_leq(PO, X,Z), po_leq(PO, Y,Z), 
              \+ ( po_leq(PO, X,ZZ),  po_leq(PO, Y,ZZ),
                   \+ Z=ZZ, po_leq(PO, ZZ,Z) 
		 ).

:- pred lubt_list(poset(@T),list(T),T).
% lubt_list(Lat, L,Z) :- Z is lub of set/list L
lubt_list(_,[],_) :- write('!? lub of empty set ??'), abort.
lubt_list(_Lat, [X],X).
lubt_list(Lat, [X,Y|L],Z) :-
        po_lub(Lat, X,Y,Z0),
        lubt_list(Lat, [Z0|L],Z).
