It either succeeds, fails, or has no value.

A goal that succeeds returns a stream of one or more substitutions.

A goal that fails returns an empty stream.

A goal that has no value never returns.

A goal that succeeds only once, i.e. it produces a singleton stream containing the current substitution. Contrast that with always.

N.B. The current substitution is the substitution that's passed to the goal.

A goal that fails.

A goal that succeeds an unbounded number of times.

Contrast that with succeed, which succeeds only once.

A goal that neither succeeds nor fails.

Try to unify two values. It succeeds if unification is possible, and fails otherwise.

The disjunction of two goals. It succeeds if and only if either of the goals succeed.

The disjunction of zero or more goals. It succeeds if and only if there is at least one goal that succeeds.

The conjunction of two goals. It succeeds if and only if both goals succeed.

The conjunction of zero or more goals. It succeeds if and only if all the goals succeed.

The disjunction of conjunctions.

conde
    [ [ g11, ..., g1N1 ]
    , [ g21, ..., g2N2 ]
    , ...
    , [ gM1, ..., gMNM ]
    ]

is equivalent to

disj
    [ conj [ g11, ..., g1N1 ]
    , conj [ g21, ..., g2N2 ]
    , ...
    , conj [ gM1, ..., gMNM ]
    ]

where M >= 0 and Ni >= 0 for all 1 <= i <= M.

If M = 0 then we have conde [].

If Ni = 0 for some i then the (i-1)th element of the list given to conde is the empty list.

Useful for defining recursive goals.

For e.g. here's a possible definition of always.

always : Goal a
always =
    disj2 succeed (lazy (\_ -> always))

Challenge: Define never using lazy.

Create a lexically-scoped logic variable, with a given name.

callFresh "fruit"
    (\fruit ->
        equals (Const "plum") fruit
    )

N.B. You only have access to the variable within the function you provide.

Create a lexically-scoped logic variable.

fresh
    (\fruit ->
        equals (Const "plum") fruit
    )

N.B. It uses callFresh under the hood but you have no control over the name of the variable. The name is only useful for debugging purposes anyway.

Create two lexicaly-scoped logic variables.

Create three lexically-scoped logic variables.

Create four lexically-scoped logic variables.

Create five lexically-scoped logic variables.

Create six lexically-scoped logic variables.

Create seven lexically-scoped logic variables.

Create eight lexically-scoped logic variables.

ifte stands for if-then-else.

ifte g1 g2 g3 is a goal that applies g1 to the current substitution. If g1 succeeds, it applies g2 to each of the substitutions produced by g1. If g1 fails, it applies g3 to the current substitution. Otherwise, if g1 has no value, the goal, ifte g1 g2 g3, also has no value.

once g is a goal that applies g to the current substitution. If g succeeds, the first substitution produced by g is used to create a singleton stream which becomes the stream produced by once g. The remaining substitutions produced by g are dropped, i.e. we cutoff all other possibilities. If g fails, once g fails. And, if g has no value, once g also has no value.

conda
    [ [ g11, ..., g1N1 ]
    , [ g21, ..., g2N2 ]
    , ...
    , [ gM1, ..., gMNM ]
    ]

is equivalent to

ifte
    g11
    (conj [ g12, ..., g1N1 ])
    (conda
        [ [ g21, ..., g2N2 ]
        , ...
        , [ gM1, ..., gMNM ]
        ]
    )

where M >= 1, N1 >= 1, and Ni >= 0 for all 2 <= i <= M.

For the case when M = 0 or when M >= 1 and N1 = 0, conda fails.

N.B. conda corresponds to Prolog's soft-cut.

condu
    [ [ g11, g12, ..., g1N1 ]
    , [ g21, g22, ..., g2N2 ]
    , ...
    , [ gM1, gM2, ..., gMNM ]
    ]

is equivalent to

conda
    [ [ once g11, g12, ..., g1N1 ]
    , [ once g21, g22, ..., g2N2 ]
    , ...
    , [ once gM1, gM2, ..., gMNM ]
    ]

where M >= 0 and Ni >= 0 for all 1 <= i <= M.

If a condu line is empty, the equivalent conda line is also empty.

N.B. condu corresponds to Mercury's committed choice.

Used by the various run functions to determine the number of substitutions to take from a stream of substitutions.

Unbounded means to take the entire stream of substitutions, which may be finite or infinite.

Apply a goal to the empty substitution and return the list of substitutions produced by that goal.

The length of the list is determined by the argument of type Length.

It's similar to runS, except that for each substitution that would be in the list returned by runS, it reifies each substitution with a fresh variable.

It's similar to run, except that the value used for reification is a list containing two fresh variables.

It's similar to run, except that the value used for reification is a list containing three fresh variables.

It's similar to run, except that the value used for reification is a list containing four fresh variables.

It's similar to run, except that the value used for reification is a list containing five fresh variables.

It's similar to run, except that the value used for reification is a list containing six fresh variables.

It's similar to run, except that the value used for reification is a list containing seven fresh variables.

It's similar to run, except that the value used for reification is a list containing eight fresh variables.

Convert a list of values to a representation that's useful for debugging and testing.