// totally ordered set of integers
public type Ordered :
   empty,
   ordered(Ordered,Int,Ordered).


// automagically generated
public type Ordered_accu($T) :
   accu
   (
      $T->$T empty,
      (Int,$T) -> $T cons,
   ).

// automagically generated
public define $T accu (Ordered t,$T acc,Ordered_accu($T) d)
   =
if t is
{
   empty then empty(d)(acc),
   ordered(l,i,r) then accu(l,cons(d)(i,accu(r,acc,d)),d)
}.

// automagically generated
public type Ordered_fold($T) :
   fold
   (
      $T empty,
      ($T,Int,$T) -> $T ordered
   ).

// automagically generated
public define $T fold (Ordered s,Ordered_fold($T) d)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)(fold(l,d),i,fold(r,d)) 
}.

// automagically generated
public type Ordered_cata($T) :
   cata
   (
      $T empty,
      (One->$T,Int,One->$T) -> $T ordered
   ).

// automagically generated
public define $T cata (Ordered s,Ordered_cata($T) d,One _)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)
   ((One u)|->cata(l,d,u),i,(One u)|->cata(r,d,u)) 
}.

// automagically generated
public type Ordered_recu($T) :
   recu
   (
      $T empty,
      (Ordered,$T,Int,Ordered,$T) -> $T ordered
   ).

// automagically generated
public define $T recu (Ordered s,Ordered_recu($T) d)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)(l,recu(l,d),i,r,recu(r,d)) 
}.

// automagically generated
public type Ordered_para($T) :
   para
   (
      $T empty,
      (Ordered,One->$T,Int,Ordered,One->$T) -> $T ordered
   ).

// automagically generated
public define $T para (Ordered s,Ordered_para($T) d,One _)
   =
if s is
{
   empty then empty(d),
   ordered(l,i,r) then ordered(d)
   (l,(One u)|->para(l,d,u),i,r,(One u)|->para(r,d,u)) 
}.


public define Word32 cardinal (Ordered s)
   =
fold
(
   s,
   fold
   (
      0,
      (Word32 l,Int _,Word32 r) |-> l + 1 + r
   )
).

   // an alternative cardinal using 'accu' instead of 'fold'
   public define Word32 cardinal (Ordered s)
   =
accu
(
   s,
   0,
   accu
   (
      (Word32 n) |-> n,
      (Int _,Word32 n) |-> n + 1
   )
).

public define Bool member (Ordered s,Int n)
   =
cata
(
   s,
   cata
   (
      false,
      (One->Bool l,Int i,One->Bool r) |->
         if n < i then l(unique)
         else if n > i then r(unique)
         else true  
   ),
   unique
).

public define Bool forall (Ordered s,(Int)->Bool cond)
   =
cata
(
   s,
   cata
   (
      true,
      (One->Bool l,Int i,One->Bool r) |->
            cond(i) & l(unique) & r(unique)  
   ),
   unique
).

public define Ordered insert (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      ordered(empty,n,empty),
      (Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered dr) |->
         if n < i then ordered(dl(unique),i,r)
         else if n > i then ordered(l,i,dr(unique))
         else s  
   ),
   unique
).

public define Ordered Ordered s + Int n
   =
insert(s,n).

public define Int minimum (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      n,
      (Ordered l,One->Int dl,Int i,Ordered r,One->Int _) |->
         if l is empty then i else dl(unique)
   ),
   unique
).
      
public define Ordered remove_minimum (Ordered sl,Int n,Ordered sr)
   =
if sl is empty then
   sr
else
   ordered
   (
      para
      (
         sl,
         para
         (
            empty,
            (Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered _) |->
               if l is empty then r
               else ordered(dl(unique),i,r)
         ),
         unique
      ),
      n,
      sr
   ).
   
// concatenation of sa + sb where max(sa) < min(sb)
public define Ordered concat (Ordered sa,Ordered sb)
   =
if sa is empty then
   sb
else if sb is
   {
      empty then sa
      ordered(lb,nb,rb) then
         ordered(sa,minimum(lb,nb),remove_minimum(lb,nb,rb))
   }.
   
public define Ordered remove (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      empty,
      (Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered dr) |->
         if n < i then ordered(dl(unique),i,r)
         else if n > i then ordered(l,i,dr(unique))
         else concat(l,r)
   ),
   unique
).
      
// returns (sa,b,sb) where max(sa) < n < min(sb) and b = member(s,n)
public define (Ordered,Bool,Ordered) split (Ordered s,Int n)
   =
para
(
   s,
   para
   (
      (empty,false,empty),
      (Ordered l,One->(Ordered,Bool,Ordered) dl,Int i,Ordered r,One->(Ordered,Bool,Ordered) dr) |->
         if n < i then
            (if dl(unique) is (a,b,c) then (a,b,ordered(c,i,r)))
         else if n > i then
            (if dr(unique) is (a,b,c) then (ordered(l,i,a),b,c))
         else (l,true,r)
   ),
   unique
).

public define Ordered filter (Ordered s,Int->Bool cond)
   =
fold
(
   s,
   fold
   (
      empty,
      (Ordered l,Int i,Ordered r) |->
         if cond(i) then ordered(l,i,r) 
         else concat(l,r)
   )
).

public define Ordered union (Ordered sa,Ordered sb)
   =
fold
(
   sa,
   fold
   (
      (Ordered s) |-> s,
      (Ordered->Ordered l,Int i,Ordered->Ordered r) |->
         (Ordered s) |->
         if s is
         {
            empty then empty,
            ordered(sl,si,sr) then
               if split(s,i) is (a,b,c) then ordered(l(a),i,r(c))
         }
   )
)
(sb).

public define Ordered Ordered sa + Ordered sb
   =
union(sa,sb).

public define Ordered intersection (Ordered sa,Ordered sb)
   =
fold
(
   sa,
   fold
   (
      (Ordered s) |-> empty,
      (Ordered->Ordered l,Int i,Ordered->Ordered r) |->
         (Ordered s) |->
         if s is
         {
            empty then empty,
            ordered(sl,si,sr) then
               if split(s,i) is (a,b,c) then
               if b then ordered(l(a),i,r(c))
               else concat(l(a),r(c))
         }
   )
)
(sb).

public define Ordered difference (Ordered sa,Ordered sb)
   =
recu
(
   sa,
   recu
   (
      (Ordered s) |-> empty,
      (Ordered l,Ordered->Ordered dl,Int i,Ordered r,Ordered->Ordered dr) |->
         (Ordered s) |->
         if s is
         {
            empty then ordered(l,i,r),
            ordered(sl,si,sr) then
               if split(s,i) is (a,b,c) then
               if b then concat(dl(a),dr(c))
               else ordered(dl(a),i,dr(c))
         }
   )
)
(sb).

public define Ordered Ordered sa - Ordered sb
   =
difference(sa,sb).

public define Bool subset (Ordered sa,Ordered sb)
   =
fold
(
   sa,
   fold
   (
      (Ordered s) |-> true,
      (Ordered->Bool l,Int i,Ordered->Bool r) |->
         (Ordered s) |->
         if s is
         {
            empty then true,
            ordered(sl,si,sr) then
               if i < si then l(sl) & member(sl,i) & r(s)
               else if i > si then l(s) & member(sr,i) & r(sr)
               else l(sl) & r(sr)
         }
   )
)
(sb).

public define Bool Ordered sa = Ordered sb
   =
subset(sa,sb) & subset(sb,sa).

public define List(Int) to_ordered_list(Ordered t)   
   =
accu
(
   t,
   [],
   accu
   (
      (List(Int) l) |-> l,
      (Int i,List(Int) l) |-> [i . l]
   )
).

// skew max-heap
public type Skew :
   empty,
   skew(Skew,Int,Skew).

// automagically generated   
public type Skew_fuse :
   fuse
   (
   (Skew,Skew,(Skew,Skew)->Skew,(Skew,Skew)->Skew) -> Skew both_not_empty
   ).

// automagically generated
public define Skew fuse(Skew sa,Skew sb,Skew_fuse d)
   =
if sa is {
   empty then sb
   skew(_,_,_) then
      if sb is
      {
         empty then sa
         skew(_,_,_) then both_not_empty(d)
         (sa,sb,(Skew u,Skew v)|->fuse(u,v,d),(Skew u,Skew v)|->fuse(u,v,d))
      }
}.

public define Skew join(Skew s1,Skew s2)   
   =
fuse
(
   s1,
   s2,
   fuse
   (
      (Skew sa,Skew sb,(Skew,Skew)->Skew fa,(Skew,Skew)->Skew fb) |->
         if sa is {empty then alert,skew(la,na,ra) then
         if sb is {empty then alert,skew(lb,nb,rb) then
         if na > nb then skew(la,na,fa(ra,sb)) 
         else skew(fb(sa,lb),nb,rb)}}
   )
).

public define Skew insert(Skew s,Int n)   
   =
join(s,skew(empty,n,empty)).

public define Skew remove(Skew l,Skew r)
   =   
join(l,r).