#include "axiom"


define FreeProductCategory(M1:Monoid, M2:Monoid):Category == with {

        coerce:M1 -> %;
        coerce:M2 -> %;
        
        length:% -> Integer;

}
FreeProductMonoid(M1: Monoid,M2: Monoid): Join(FreeProductCategory(M1,M2),Monoid)  == add {
        +++ FreeProductMonoid(M1,M2) ist the free product of the monoids M1 and M2
        +++ where the neutral elements are identified
        +++ Representation by two lists of factors:
        +++ factors1 = [a1,a2,a3,...,am] and factors2 = [b1,b2,b3,...,bm]
        +++ corresponds to the element a1*b1*a2*b2*a3*b3*...*am*bm
        +++ a1 and bm are possibly the neutral element
        +++ the neutral element is represented by address@hidden address@hidden
        
        Rep == Record(factors1:List M1, factors2:List M2);
        
        1:% == {
                import from Rep,M1,M2;
                per [ address@hidden,address@hidden;
        }

        one?(x:%):Boolean == {
                import from M1,M2,Rep;
                one? first ((rep x) factors1) and one? first ((rep x) factors2);
        }
        
        coerce(x:M1):% == { 
                import from List M1,List M2,Rep;
                per [[x],address@hidden;
        }

        coerce(y:M2):% == {
                import from List M1,List M2,Rep;
                per address@hidden,[y]];
        }

        _=(x:%,y:%):Boolean == rep x = rep y;

        coerce(w:%):OutputForm ==  {
                import from Integer;
                one? w => outputForm(address@hidden); 
                import from List OutputForm,List List OutputForm;
                import from OutputForm;
                import from Symbol;

                infix("*"::Symbol::OutputForm, reduce(concat,[  (if one? a then [b::OutputForm] else if one? b then [a::OutputForm] else [a::OutputForm, b::OutputForm]) for a:M1 in (rep w) factors1 for b:M2 in (rep w) factors2 ]));
        }

        reduceword!:Rep -> Rep;

        reduceword!(x:Rep):Rep == {
                x1:List M1 := x factors1;
                x2:List M2 := x factors2;
                import from NonNegativeInteger,List M1, List M2;
                -- length one is in reduced form already
                if(#x1 = 1) then x;
                while (#x2 > 1) repeat {
                        while(#x2 > 1 and (one? second x1 or one? first x2)) repeat {
                                setfirst!(x1, first x1 * second x1);
                                setrest!(x1,rest rest x1);
                                setfirst!(x2, first x2  * second x2);
                                setrest!(x2,rest rest x2);
                                -- if there is change, we need to go back
                                if(one? first x1 or one? first x2) then {
                                        reduceword!(x);
                                }
                        }
                        --next letter
                        x1:= rest x1;
                        x2:= rest x2;
                }
                x;
        }

        _*(x:%,y:%):% == {
                w1:List M1 := concat((rep x) factors1, (rep y) factors1);
                w2:List M2 := concat((rep x) factors2, (rep y) factors2);
                res:Rep:=[w1,w2];
                reduceword! res;
                per res;
        }

        length(w:%):Integer == {
                import from Rep, List M1, List M2, NonNegativeInteger;
                n:Integer := (# ((rep w) factors1))::Integer + (# ((rep w) factors2))::Integer;
                if(one? first ((rep w) factors1)) then n:=n-1;
                if(one? last ((rep w) factors2)) then n:=n-1;
                n;
        }        
}