Updated microKanren Kernel

Kernel.elm

-- modified version of https://package.elm-lang.org/packages/dvberkel/microkanren/latest/
-- fixing a bug, and adding reification, some practical features, and an example logic problem

module MicroKanren.Kernel exposing
    ( Goal, State, Stream(..), Term(..), Var
    , callFresh, conjoin, disjoin
    , emptyState, unit
    , walk
    , Substitutions, fish, l, pull, unify, v
    )

{-| μKanren provides an implementation of the

> minimalist language in the [miniKanren](http://minikanren.org/) family of
> relational (logic) programming languages.


## Types

@docs Goal, State, Stream, Term, Var, Substitution


## Goal Constuctors

@docs callFresh, conjoin, disjoin, identical


## Constructors

@docs emptyState, unit


## Accessors

@docs walk

-}

import Dict


{-| Utility for debugging
-}
tap : (a -> b) -> a -> a
tap f a =
    always a (f a)


{-| General purpose fixpoint combinator
-}
fix : (a -> a) -> (a -> a)
fix f p =
    let
        next =
            f p
    in
    if next == p then
        p

    else
        fix f next


{-| Variable indices are identified by integers.
-}
type alias Var =
    Int


{-| A state is a pair of a substitution and a non-negative integer representing a fresh-variable counter.
-}
type alias State a =
    { substitution : Substitutions a
    , fresh : Var
    }


{-| The empty state is a common starting point for many μKanren programs.

While in principle the user of the system may begin with any state, in practice
the user almost always begins with empty-state . empty-state is a user-level
alias for a state virtually devoid of information: the substitution is empty,
and the first variable will be indexed at 0.

-}
emptyState : State a
emptyState =
    { substitution = Dict.empty
    , fresh = 0
    }


{-| A sequences of states is a _stream_.

A goal's success may result in a sequence of (enlarged) states, which we term a
stream. The result of a μKanren program is a stream of satisfying states. The
stream may be finite or infinite, as there may be finite or infinitely many
satisfying states

-}
type Stream a
    = Empty
    | Immature (() -> Stream a)
    | Mature (State a) (Stream a)


{-| a μKanren program proceeds through the application of a _goal_ to a state.

Goals are often understood by analogy to predicates. Whereas the application of
a predicate to an element of its domain can be either true or false, a goal
pursued in a given state can either succeed or fail . When it succeeds it
returns a non-empty stream, otherwise it fails and returns an empty stream.

-}
type alias Goal a =
    State a -> Stream a


{-| Terms of the language consist of variables, objects deemed identical under
eqv? , and pairs of the foregoing.
-}
type Term a
    = Var Var
    | Val a
    | Cons (Term a) (Term a)
    | Nil


type Reified a
    = RVar Var
    | RVal a
    | RList (List (Reified a))


{-| make a value term
-}
v : a -> Term a
v =
    Val


{-| make a list term
-}
l : List (Term a) -> Term a
l =
    List.foldr Cons Nil


{-| A _substitution_ binds variables to terms.
-}
type alias Substitutions a =
    Dict.Dict Var (Term a)


{-| The _walk_ operator searches for a variable's value in the
substitution.
-}
walk : Term a -> Substitutions a -> Term a
walk term substitution =
    case term of
        Var variable ->
            case Dict.get variable substitution of
                Just value ->
                    walk value substitution

                Nothing ->
                    term

        _ ->
            term


{-| the ext-s operator extends the substitution with a new binding.

When extending the substitution, the first argument is always a variable, and
the second is an arbitrary term. In Friedman et. al, ext-s performs a check for
circularities in the substitution; here there is no such prohibition.

-}
extend : Var -> Term a -> Substitutions a -> Substitutions a
extend variable term substitution =
    Dict.insert variable term substitution


{-| ≡ takes two terms as arguments and returns a goal that succeeds
if those two terms unify in the received state.
-}
unify : Term a -> Term a -> Goal a
unify left right =
    \state ->
        case unifyHelper left right state.substitution of
            Just substitution ->
                unit
                    { state
                        | substitution = substitution
                    }

            Nothing ->
                mzero


{-| _unit_ lifts the state into a stream whose only element is that state.
-}
unit : Goal a
unit state =
    Mature state Empty


{-| If those two terms fail to unify in that state, the empty stream, _mzero_ is
returned.
-}
mzero : Stream a
mzero =
    Empty


{-| To unify two terms in a substitution, both are walked in that substitution.
If the two terms walk to the same variable, the original substitution is
returned unchanged. When one of the two terms walks to a variable, the
substitution is extended,
**binding the variable to which that term walks with the value to which the other term walks.**

If both terms walk to pairs, the cars and
then cdrs are unified recursively, succeeding if unification succeeds in the one
and then the other. Finally, non-variable, non-pair terms unify if they are
identical under eqv? , and unification fails otherwise.

-}
unifyHelper : Term a -> Term a -> Substitutions a -> Maybe (Substitutions a)
unifyHelper left right substitution =
    let
        leftWalk : Term a
        leftWalk =
            walk left substitution

        rightWalk : Term a
        rightWalk =
            walk right substitution
    in
    case ( leftWalk, rightWalk ) of
        ( Var leftVariable, Var rightVariable ) ->
            if leftVariable == rightVariable then
                Just substitution

            else
                Just (extend leftVariable rightWalk substitution)

        ( Val leftValue, Val rightValue ) ->
            if leftValue == rightValue then
                Just substitution

            else
                Nothing

        ( Var leftVariable, _ ) ->
            Just (extend leftVariable rightWalk substitution)

        ( _, Var rightVariable ) ->
            Just (extend rightVariable leftWalk substitution)

        ( Cons leftFirst leftRest, Cons rightFirst rightRest ) ->
            unifyHelper leftFirst rightFirst substitution
                |> Maybe.andThen (unifyHelper leftRest rightRest)

        ( Nil, Nil ) ->
            Just substitution

        _ ->
            Nothing


{-| The call/fresh goal constructor takes a unary function f whose body is a
goal, and itself returns a goal.

This returned goal, when provided a state s/c , binds the formal parameter of f
to a new logic variable (built with the variable constructor operator var ), and
passes a state, with the substitution it originally received and a newly
incremented fresh-variable counter, c , to the goal that is the body of f.

-}
callFresh : (Term a -> Goal a) -> Goal a
callFresh f =
    \state -> f (Var state.fresh) { state | fresh = state.fresh + 1 }


callFresh2 : (Term a -> Term a -> Goal a) -> Goal a
callFresh2 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            { state | fresh = state.fresh + 2 }


callFresh3 : (Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh3 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            { state | fresh = state.fresh + 3 }


callFresh4 : (Term a -> Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh4 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            (Var (state.fresh + 3))
            { state | fresh = state.fresh + 4 }


callFresh5 : (Term a -> Term a -> Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh5 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            (Var (state.fresh + 3))
            (Var (state.fresh + 4))
            { state | fresh = state.fresh + 5 }


callFresh6 : (Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh6 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            (Var (state.fresh + 3))
            (Var (state.fresh + 4))
            (Var (state.fresh + 5))
            { state | fresh = state.fresh + 6 }


callFresh7 : (Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh7 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            (Var (state.fresh + 3))
            (Var (state.fresh + 4))
            (Var (state.fresh + 5))
            (Var (state.fresh + 6))
            { state | fresh = state.fresh + 7 }


callFresh8 : (Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh8 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            (Var (state.fresh + 3))
            (Var (state.fresh + 4))
            (Var (state.fresh + 5))
            (Var (state.fresh + 6))
            (Var (state.fresh + 7))
            { state | fresh = state.fresh + 8 }


callFresh9 : (Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Term a -> Goal a) -> Goal a
callFresh9 f =
    \state ->
        f
            (Var state.fresh)
            (Var (state.fresh + 1))
            (Var (state.fresh + 2))
            (Var (state.fresh + 3))
            (Var (state.fresh + 4))
            (Var (state.fresh + 5))
            (Var (state.fresh + 6))
            (Var (state.fresh + 7))
            (Var (state.fresh + 8))
            { state | fresh = state.fresh + 9 }


{-| The disj goal constructor takes two goals as arguments and returns a goal
that succeeds if either of the two subgoals succeed.
-}
disjoin : Goal a -> Goal a -> Goal a
disjoin left right =
    \state ->
        mplus (left state) (right state)


disj : List (Goal a) -> Goal a
disj goals =
    case goals of
        [] ->
            \_ -> mzero

        goal :: rest ->
            disjoin goal (zzz (\() -> disj rest))


conj : List (Goal a) -> Goal a
conj goals =
    case goals of
        [] ->
            unit

        goal :: rest ->
            conjoin goal (zzz (\() -> conj rest))


{-| The conj goal constructor similarly takes two goals as arguments and returns
a goal that succeeds if both goals succeed for that state.
-}
conjoin : Goal a -> Goal a -> Goal a
conjoin left right =
    \state ->
        bind (left state) right


{-| The mplus operator is responsible for merging streams. In a goal constructed
from disj , the resulting stream contains the states that result from success of
either of the two goals.
-}
mplus : Stream a -> Stream a -> Stream a
mplus left right =
    case left of
        Empty ->
            right

        Immature lazyStream ->
            Immature (\_ -> mplus right (lazyStream ()))

        Mature state followingStream ->
            Mature state (mplus right followingStream)


{-| bind receives this resulting stream and the goal g.

In bind that goal ( g ) is invoked on each element of the stream. If the stream
of results of g is empty or becomes exhausted mzero, the empty stream, is
returned. If instead the stream contains a state and potentially more, then g is
invoked on the first state. The stream which is the result of that invocation is
merged to a stream containing the invocation of the rest of the $ passed in the
second goal g.

-}
bind : Stream a -> Goal a -> Stream a
bind stream goal =
    case stream of
        Empty ->
            mzero

        Immature lazyStream ->
            Immature (\_ -> bind (lazyStream ()) goal)

        Mature state followingStream ->
            let
                goalStream =
                    goal state
            in
            mplus goalStream (bind followingStream goal)


caro : Term a -> Term a -> Goal a
caro pair car =
    callFresh (\d -> unify (Cons car d) pair)


cdro : Term a -> Term a -> Goal a
cdro pair cdr =
    callFresh (\a -> unify (Cons a cdr) pair)


zzz : (() -> Goal a) -> Goal a
zzz thunk =
    \state -> Immature (\() -> thunk () state)


membero : Term a -> Term a -> Goal a
membero xs x =
    disjoin
        (caro xs x)
        (callFresh
            (\d ->
                conjoin
                    (cdro xs d)
                    (membero d x)
            )
        )


pull : Stream a -> Stream a
pull stream =
    case stream of
        Immature lazyStream ->
            pull (lazyStream ())

        _ ->
            stream


reifyAll : List (State a) -> List (Reified a)
reifyAll =
    List.map reify


reify : State a -> Reified a
reify =
    reifyTerm (Var 0)


reifyTerm : Term a -> State a -> Reified a
reifyTerm term state =
    case walk term state.substitution of
        Cons a d ->
            case reifyTerm d state of
                RList list ->
                    RList (reifyTerm a state :: list)

                other ->
                    RList [ reifyTerm a state, other ]

        Nil ->
            RList []

        Var vv ->
            RVar vv

        Val vv ->
            RVal vv


take : number -> Stream a -> List (State a)
take n stream =
    if n == 0 then
        []

    else
        case stream of
            Empty ->
                []

            Mature state tailStream ->
                state :: take (n - 1) tailStream

            Immature lazyStream ->
                take n (lazyStream ())


debugStates : List (State a) -> List (State a)
debugStates =
    tap
        (List.indexedMap
            (\i state ->
                let
                    _ =
                        Debug.log (String.fromInt i) ""
                in
                Dict.toList state.substitution
                    |> List.reverse
                    |> List.map (Debug.log "   ")
            )
        )


streamMap : (State a -> Stream a -> b) -> Stream a -> Maybe b
streamMap f stream =
    case stream of
        Mature state stream_ ->
            Just (f state stream_)

        _ ->
            Nothing


pullAll : Stream a -> List (State a)
pullAll stream =
    { stream = stream, states = [] }
        |> fix
            (\r ->
                pull r.stream
                    |> streamMap
                        (\nextState nextStream ->
                            { stream = nextStream, states = nextState :: r.states }
                        )
                    |> Maybe.withDefault r
            )
        |> .states


fish : Int -> List (Reified String)
fish n =
    let
        puzzle : Term String -> Goal String
        puzzle solution =
            callFresh5
                (\h1 h2 h3 h4 h5 ->
                    conj
                        [ unify solution (l [ v "Street", h1, h2, h3, h4, h5 ])
                        , britLivesInRedHouse solution
                        , swedeKeepsDog solution
                        , daneDrinksTea solution
                        , greenHouseOwnerDrinksCoffee solution
                        , poloPlayerRearsBirds solution
                        , yellowHouseOwnerPlaysHockey solution
                        , billiardPlayerDrinksBeer solution
                        , germanPlaysSoccer solution

                        --(center-house-owner-drinks-milk solution)
                        , centerHouseOwnerDrinksMilk solution

                        --  (norvegian-in-first-house solution)
                        , norwegianInFirstHouse solution

                        --
                        --  ;; To-the-left-of clues
                        --  (green-house-left-of-white-house solution)
                        , greenHouseLeftOfWhiteHouse solution

                        --
                        --  ;; Next-to clues
                        --  (baseball-player-lives-next-to-cat-owner solution)
                        , baseballPlayerLivesNextToCatOwner solution

                        --  (hockey-player-lives-next-to-horse-owner solution)
                        , hockeyPlayerLivesNextToHorseOwner solution

                        --  (norvegian-lives-next-to-blue-house solution))
                        , norwegianLivesNextToBlueHouse solution
                        ]
                )

        britLivesInRedHouse solution =
            callFresh3
                (\pet beverage sport ->
                    membero solution (l [ v "House", v "Brit", v "Red", pet, beverage, sport ])
                )

        swedeKeepsDog solution =
            callFresh3
                (\color beverage sport ->
                    membero solution (l [ v "House", v "Swede", color, v "Dog", beverage, sport ])
                )

        daneDrinksTea solution =
            callFresh3
                (\color pet sport ->
                    membero solution (l [ v "House", v "Dane", color, pet, v "Tea", sport ])
                )

        greenHouseOwnerDrinksCoffee solution =
            callFresh3
                (\nationality pet sport ->
                    membero solution (l [ v "House", nationality, v "Green", pet, v "Coffee", sport ])
                )

        poloPlayerRearsBirds solution =
            callFresh3
                (\nationality color beverage ->
                    membero solution (l [ v "House", nationality, color, v "Birds", beverage, v "Polo" ])
                )

        yellowHouseOwnerPlaysHockey solution =
            callFresh3
                (\nationality pet beverage ->
                    membero solution (l [ v "House", nationality, v "Yellow", pet, beverage, v "Hockey" ])
                )

        billiardPlayerDrinksBeer solution =
            callFresh3
                (\nationality color pet ->
                    membero solution (l [ v "House", nationality, color, pet, v "Beer", v "Billiards" ])
                )

        germanPlaysSoccer solution =
            callFresh3
                (\color pet beverage ->
                    membero solution (l [ v "House", v "German", color, pet, beverage, v "Soccer" ])
                )

        centerHouseOwnerDrinksMilk solution =
            callFresh9
                (\h1 h2 h3 h4 h5 nationality color pet sport ->
                    let
                        street =
                            l [ v "Street", h1, h2, h3, h4, h5 ]

                        house =
                            l [ v "House", nationality, color, pet, v "Milk", sport ]
                    in
                    conj
                        [ unify street solution
                        , unify house h3
                        ]
                )

        norwegianInFirstHouse solution =
            callFresh9
                (\h1 h2 h3 h4 h5 color pet beverage sport ->
                    let
                        street =
                            l [ v "Street", h1, h2, h3, h4, h5 ]

                        house =
                            l [ v "House", v "Norwegian", color, pet, beverage, sport ]
                    in
                    conj
                        [ unify street solution
                        , unify house h1
                        ]
                )

        nextToInOrder a b solution =
            callFresh5
                (\h1 h2 h3 h4 h5 ->
                    conj
                        [ unify solution (l [ v "Street", h1, h2, h3, h4, h5 ])
                        , disj
                            [ conj [ unify h1 a, unify h2 b ]
                            , conj [ unify h2 a, unify h3 b ]
                            , conj [ unify h3 a, unify h4 b ]
                            , conj [ unify h4 a, unify h5 b ]
                            ]
                        ]
                )

        greenHouseLeftOfWhiteHouse solution =
            callFresh8
                (\nationality1 pet1 beverage1 sport1 nationality2 pet2 beverage2 sport2 ->
                    let
                        greenHouse =
                            l [ v "House", nationality1, v "Green", pet1, beverage1, sport1 ]

                        whiteHouse =
                            l [ v "House", nationality2, v "White", pet2, beverage2, sport2 ]
                    in
                    conj
                        [ nextToInOrder greenHouse whiteHouse solution
                        ]
                )

        nextTo a b solution =
            disjoin
                (nextToInOrder a b solution)
                (nextToInOrder b a solution)

        -- baseball-player-lives-next-to-cat-owner
        baseballPlayerLivesNextToCatOwner solution =
            callFresh8
                (\nationality1 color1 pet1 beverage1 nationality2 color2 beverage2 sport2 ->
                    let
                        baseballHouse =
                            l [ v "House", nationality1, color1, pet1, beverage1, v "Baseball" ]

                        catHouse =
                            l [ v "House", nationality2, color2, v "Cat", beverage2, sport2 ]
                    in
                    nextTo baseballHouse catHouse solution
                )

        -- hockey-player-lives-next-to-horse-owner
        hockeyPlayerLivesNextToHorseOwner solution =
            callFresh8
                (\nationality1 color1 pet1 beverage1 nationality2 color2 beverage2 sport2 ->
                    let
                        hockeyPlayerHouse =
                            l [ v "House", nationality1, color1, pet1, beverage1, v "Hockey" ]

                        horseOwnerHouse =
                            l [ v "House", nationality2, color2, v "Horse", beverage2, sport2 ]
                    in
                    nextTo hockeyPlayerHouse horseOwnerHouse solution
                )

        -- norwegian-lives-next-to-blue-house
        norwegianLivesNextToBlueHouse solution =
            callFresh8
                (\color1 pet1 beverage1 sport1 nationality2 pet2 beverage2 sport2 ->
                    let
                        norwegialHouse =
                            l [ v "House", v "Norwegian", color1, pet1, beverage1, sport1 ]

                        blueHouse =
                            l [ v "House", nationality2, v "Blue", pet2, beverage2, sport2 ]
                    in
                    nextTo norwegialHouse blueHouse solution
                )
    in
    callFresh puzzle emptyState |> take n |> reifyAll