Otter.SearchRes

Documentation

type SearchRes a = [Res a]

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 Delays.

data Res a

Constructors

Res a

Delay

Instances

Functor Res

Defined in Otter.SearchRes

Methods

fmap :: (a -> b) -> Res a -> Res b

(<$) :: a -> Res b -> Res a

data Extraction a

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.

Constructors

AllResults (NonEmpty a)

NoResults FailureReason

data FailureReason

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.

Constructors

NotATheorem

SpaceTooBig

extractResults :: Int -> SearchRes a -> Extraction a

Extract all the positive results from a search result stream, stopping if no result is found after the given number of delays.

delay :: SearchRes a -> SearchRes a

Delays a search result stream.

delay x == Delay : x

cons :: a -> SearchRes a -> SearchRes a

Appends a result to a search result stream.

cons x y = Res x : y