15.4.884  src/lib/src/disjoint-sets-with-constant-time-union.pkg

# disjoint-sets-with-constant-time-union.pkg
#
# See comments in:      src/lib/src/disjoint-sets-with-constant-time-union.api
# Compare to:         src / lib/src/disjoint-sets-with-constant-time-union-simple-version.pkg
#
# Union-find datastructure with path compression and ranked union.
#
# Author:
#    Fritz Henglein
#    DIKU, University of Copenhagen
#    henglein@diku.dk

# Compiled by:
#     src/lib/std/standard.lib



###                "If you can dream it, you can do it."
###
###                              -- Walt Disney


###                "Don't dream it -- be it."
###
###                              -- Rocky Horror Picture Show



package   disjoint_sets_with_constant_time_union
: (weak)  Disjoint_Sets_With_Constant_Time_Union                                        # Disjoint_Sets_With_Constant_Time_Union        is from   src/lib/src/disjoint-sets-with-constant-time-union.api
{
    Disjoint_Set_C(X)
      = ECR  (X, Int)
      | PTR  Disjoint_Set(X)
    withtype Disjoint_Set(X) = Ref( Disjoint_Set_C(X) );

    #
    fun chase (p as REF (ECR _))
            =>
            p;

        chase (p as REF (PTR p'))
            =>
            {   p'' = chase p';
          
                p := PTR p'';

                p'';
            };
    end;
    #
    fun make_singleton_disjoint_set x =  REF (ECR (x, 0));
    #
    fun get p
        =
        case *(chase p)
            #     
            ECR (x, _) =>  x;
            _          =>  raise exception MATCH;
        esac;

      
    fun equal (p, p')
        =
        chase p == chase p';

    #
    fun set (p, x)
        =
        case (chase p)
            #     
             (p' as REF (ECR(_, r))) =>   p' := ECR (x, r);
             _                       =>   raise exception MATCH;
        esac;

    #
    fun link (p, q)
        =
        {   p' = chase p;
            q' = chase q;
          
            if (p' == q')                       FALSE;
            else                p' := PTR q;    TRUE;
            fi;
        };
    #
    fun unify f (p, q)
        =
        case (chase p, chase q)
            #     
            (p' as REF (ECR (pc, pr)), q' as REF (ECR (qc, qr)))
                =>
                {   new_c = f (pc, qc);

                    if (p' == q')
                        #
                        p' := ECR (new_c, pr);

                        FALSE;
                    else
                        if   (pr == qr)   q' := ECR (new_c, qr+1);   p' := PTR q';
                        elif (pr <  qr)   q' := ECR (new_c, qr  );   p' := PTR q';
                        else/*pr >  qr*/  p' := ECR (new_c, pr  );   q' := PTR p';
                        fi;

                        TRUE;
                    fi;
               };
            _ => raise exception MATCH;

        esac;

    #
    fun union (p, q)
        =
        {
            p' = chase p;
            q' = chase q;
          
            if (p' == q')
                #
                FALSE;
            else
                case (*p', *q')
                    #
                     (ECR (pc, pr), ECR (qc, qr))
                       =>
                        {  if   (pr == qr)      q' := ECR (qc, qr+1);   p' := PTR q';
                           elif (pr <  qr)                              p' := PTR q';
                           else                                         q' := PTR p';
                           fi;

                           TRUE;
                       };

                    _ => raise exception MATCH;
                esac;
            fi;
        };

};