Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- type SearchRes a = [Res a]
- data Res a
- data Extraction a
- = AllResults (NonEmpty a)
- | NoResults FailureReason
- data FailureReason
- extractResults :: Int -> SearchRes a -> Extraction a
- delay :: SearchRes a -> SearchRes a
- cons :: a -> SearchRes a -> SearchRes a
Documentation
type SearchRes a = [Res a] Source #
Type representing the result of proof search. Every element in the list
corresponds to the result of analysing node in the search space by the search
algorithm. The result is Res
in the positive case the node is a goal node,
or Delay
in the negative case.
The search agorithm produces an element of `SearchRes
a` lazily, inserting
Delay
constructors to ensure that the computation is productive even in the
case no goal node is found in the search space. This allows to perform proof
search in an on-demand fashion, possibly giving up after a certain number of
Delay
s.
data Extraction a Source #
Type of the result of extractResults
, which extracts all positive search
results from a search result stream.
An element of `Extraction a` is either a non-empty list of positive results,
or an element of SpaceExhausted
giving a reason why no result was found.
data FailureReason Source #
Type of reasons why no result can be extracted from a search result stream.
Either the search space has been exhaustively searched and no result was found (the query is not a theorem), or the search was terminated preemptively according to an upper bound imposed on the maximum depth of the search space.
extractResults :: Int -> SearchRes a -> Extraction a Source #
Extract all the positive results from a search result stream, stopping if no result is found after the given number of delays.