signature SPACE structure Space : SPACE
The Space structure provides access to first class computation spaces. First class computation spaces can be used to program inference engines for problem solving.
For example, simple depth-first one solution search can be done as follows.
fun searchOne s = case ask s of FAILED => NONE | SUCCEEDED => SOME (Space.merge s) | ALTERNATIVES(n) => let val c = Space.clone s in Space.commit(s, SINGLE 1); case searchOne s of NONE => (Space.commit(c, RANGE(2, n)); searchOne c) | SOME s => SOME s end
Given the money script, a solution can be searched by invoking
val solution = searchOne (Space.space money)
More sophisticated search engines are provided by the structure Search.
import signature SPACE from "x-alice:/lib/constraints/SPACE-sig" import structure Space from "x-alice:/lib/constraints/Space"
signature SPACE = sig eqtype 'a space datatype state = MERGED | FAILED | SUCCEEDED | ALTERNATIVES of int datatype verbose_state = VERBOSE_SUSPENDED of verbose_state | VERBOSE_MERGED | VERBOSE_FAILED | VERBOSE_SUCCEEDED_STUCK | VERBOSE_SUCCEEDED_ENTAILED | VERBOSE_ALTERNATIVES of int datatype choice = SINGLE of int | RANGE of int * int val space : (unit -> 'a) -> 'a space val ask : 'a space -> state val askVerbose : 'a space -> verbose_state val clone : 'a space -> 'a space val commit : 'a space * choice -> unit val inject : 'a space * ('a -> unit) -> unit val merge : 'a space -> 'a val kill : 'a space -> unit val waitStable : 'a space -> unit end
The type of computation spaces.
This datatype is used to communicate the state of a computation space.
This datatype is used to communicate the verbose state of a computation space.
This datatype is used to select alternatives of the selected choice of a space.
returns a newly created space, in which a thread containing an application of the unary function p to the root variable of the space is created.
waits until s becomes stable or merged and then returns the state of s.
If s is merged, MERGED is returned.
If s is stable and failed, FAILED is returned.
If s is stable and succeeded and there are no threads in s synchronizing on choices, SUCCEEDED is returned.
If s is stable and succeeded and there is at least one thread in s which synchronizes on a choice, ALTERNATIVES i is returned, where i gives the number of alternatives on the selected choice.
Synchronizes on stability of s.
Raises a runtime error if the current space is not admissible for s.
returns the state of s in verbose form. Reduces immediately, even if s is not yet stable.
If s becomes merged, VERBOSE_MERGED is returned.
If s becomes suspended (that is, blocked but not stable), VERBOSE_SUSPENDED t is returned. t is a future that is bound to the verbose state of s when s becomes stable again.
If s is stable and failed, VERBOSE_FAILED is returned.
If s is stable and succeeded and there are no threads in s synchronizing on choices, either VERBOSE_SUCCEEDED_STUCK, or VERBOSE_SUCCEEDED_ENTAILED is returned. The former happens when s still contains threads.
If s is stable and succeeded and there is at least one thread in s which synchronizes on a choice, VERBOSE_ALTERNATIVES i is returned, where i gives the number of alternatives on the selected choice.
Does not synchronize on stability of s.
Raises a runtime error if the current space is not admissible for s.
blocks until s becomes stable and returns a new space which is a copy of s.
Synchronizes on stability of s.
Raises a runtime error if s is already merged, or if the current space is not admissible for s.
blocks until s becomes stable and then commits to alternatives of the selected choice of s.
if c is RANGE(l, h), then all but the l,l+1,...,h alternatives of the selected choice of s are discarded. If a single alternative remains, the topmost choice is replaced by this alternative. If no alternative remains, the space is failed.
SINGLE i is an abbreviation for RANGE(i, i).
Synchronizes on stability of s.
Raises a runtime error, if s has been merged already, if there exists no selected choice in s, or if the current space is not admissible for s.
creates a thread in s which contains an application of p to the root variable of s.
Does not synchronize on stability of s.
Raises a runtime error if s is already merged, or if the current space is not admissible for s.
merges s with the current space and returns the root variable of s.
Does not synchronizes on stability of s.
Raises a runtime error if s is already merged, or if the current space is not admissible for s.
kills s by injecting a failure into a space.
Synchronizes on stability of s and returns unit.