types

Space = [ S ];
S = Box | BoxSplit;
Box :: info: BoxInfo
       width: Width;
BoxSplit :: one: Space
            two: Space;

BoxInfo = token;
Width = real

values

boxA = mk_Box( mk_token("A"), 70.5 );
boxB = mk_Box( mk_token("B"), 50 );
boxC = mk_Box( mk_token("C"), 35.25 );

bs3 = mk_BoxSplit( boxC, nil );
bs2 = mk_BoxSplit( boxB, bs3 );
bs1 = mk_BoxSplit( boxA, bs2 );

s = bs1 

functions

cata[@X]: @X * (Box -> @X) * (@X * @X -> @X)  -> (Space -> @X)
cata( c, b, s )(space) ==
        if space = nil 
        then c
        elseif is_Box(space) 
        then b(space)
        else s(cata[@X](c, b, s)(space.one),cata[@X](c, b, s)(space.two));

ana[@X]: (@X -> ([Box] | @X * @X )) -> (@X -> Space)
ana(g)(x) == let res = g(x)
             in if res = nil
                then nil
                elseif is_Box(res) 
                then res
                else let mk_(res1,res2) = res
                     in mk_BoxSplit(ana[@X](g)(res1), ana[@X](g)(res2));

para[@X]: @X * (Box -> @X) * (@X * Space * @X * Space -> @X) -> (Space -> @X)
para( c, b, s )(space) == 
        if space = nil 
        then c
        else if is_Box(space)
             then b(space)
             else s(para[@X](c, b, s)(space.one), space.one,
                    para[@X](c, b, s)(space.two), space.two);

        
whichBoxes : Space -> set of BoxInfo
whichBoxes (s) == 
        cata[set of BoxInfo](
                {}, 
                lambda x : Box & {x.info}, 
                lambda x: set of BoxInfo, y: set of BoxInfo & x union y) (s);

freeSpace : Space -> Width
freeSpace( s) == freespace_aux( s, 100);

freespace_aux : Space * Width -> Width
freespace_aux( s, r) == if s = nil then r
                        elseif is_Box(s) then 0
                        else max( freespace_aux(s.one, (r*sqrt(2))/2
),
                                  freespace_aux(s.two, (r*sqrt(2))/2
));

max : Width * Width -> Width
max (x, y) == if x > y then x else y;


insertBox : Box * Space -> Space
insertBox( b, s) == insertbox_aux( b, 100, s)
pre b.width <= freeSpace( s );


removeBox : Box * Space -> Space
removeBox (b, s) == cata[Space](
        nil,
        lambda x : Box & if x.info = b.info then nil else x,
        lambda x : Space, y : Space & mk_BoxSplit(x,y)) (s); 

defragment : Space -> Space 
defragment (s) == cata[Space](
        nil, 
        lambda x: Box & x,
        lambda x : Space, y : Space & 
                if x = nil and y = nil
                then nil
                else  mk_BoxSplit(x,y)) (s)