(unify*) ( x! x-env! y! y-env! trail tmp-env -- success? )

Vocabulary

logic.private

Inputs

x!	an object
x-env!	an object
y!	an object
y-env!	an object
trail	an object
tmp-env	an object

Outputs

success?

an object

Definition

USING: accessors combinators kernel sequences ;

IN: logic.private

:: (unify*)
    ( x! x-env! y! y-env! trail tmp-env -- success? )
    f :> ret-value! f :> ret?! f :> ret2?! [
        {
            {
                [ x logic-var? ]
                [
                    x x-env env-get :> xp xp [
                        xp first2 x-env! x! x x-env dereference
                        x-env! x! t
                    ] [
                        y y-env dereference y-env! y! x y =
                        x-env y-env eq? and ~quotation~ unless
                        t ret?! t ret-value! f
                    ] if
                ]
            }
            {
                [ y logic-var? ]
                [ x y x! y! x-env y-env x-env! y-env! t ]
            }
            [ f ]
        } cond
    ] loop ret? [
        t ret-value! x y [ logic-goal? ] both? [
            x pred>> y pred>> =
            [ x args>> x! y args>> y! ]
            [ f ret-value! t ret2?! ] if
        ] when ret2? [
            {
                {
                    [ x y ~quotation~ both? ]
                    [
                        x y ~quotation~ same?
                        ~quotation~ ~quotation~ if ret-value!
                    ]
                }
                {
                    [ x y ~quotation~ both? ]
                    [
                        x y ~quotation~ same?
                        x y ~quotation~ same? and
                        ~quotation~ ~quotation~ if ret-value!
                    ]
                }
                [ x y = ret-value! ]
            } cond
        ] unless
    ] unless ret-value ;