#ifndef GOOSE_SEMA_UNIFY_H
#define GOOSE_SEMA_UNIFY_H

namespace goose::sema
{
    struct NoUnification {};
    struct AmbiguousUnification {};
    using UniSol = pair< Term, UnificationContext >;

    using UnificationSolution = variant
    <
        NoUnification,
        AmbiguousUnification,
        UniSol
    >;

    UnificationSolution FindBestUnification( const Term& lhs, const Term& rhs, const Context& context );

    using UniGen = Generator< pair< Term, UnificationContext > >;

    // Perform one unification pass, or two if holes need to be substituted.
    UniGen FullUnify( const Term& lhs, const Term& rhs, const Context& context );

    // If substitution is needed, perform substitution on lhs and rhs and then
    // perform a second unification pass.
    UniGen UnifyPass2( const Term& lhs, const Term& rhs, const Term& s, UnificationContext ucPass1 );

    // Perform one unification pass
    UniGen Unify( const Term& lhs, const Term& rhs, const UnificationContext& context );

    UniGen HalfUnify( const Term& lhs, const UnificationContext& context );
}

#endif
