Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- module Zsyntax.Formula
- search :: Ord a => Sequent a -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label])
- searchLabelled :: Ord a => GoalNSequent a Label -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label])
- toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label
- type SearchRes a = [Res a]
- data Extraction a
- = AllResults (NonEmpty a)
- | NoResults FailureReason
- data FailureReason
- type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l
- type Label = Int
- extractResults :: Int -> SearchRes a -> Extraction a
Documentation
module Zsyntax.Formula
search :: Ord a => Sequent a -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label]) Source #
Searches for a derivation of the specified sequent.
search g == searchLabelled (toLabelledGoal g)
searchLabelled :: Ord a => GoalNSequent a Label -> (SearchRes (DecoratedLSequent a Label), [DecoratedLSequent a Label]) Source #
Searches for a derivation of the specified goal sequent. Returns the search results, as well as all searched sequents.
toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label Source #
Turns a sequent into a labelled sequent that is suitable for proof search, by breaking the linear context formulas into neutral formulas, and labelling all subformulas with unique labels.
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.
type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l Source #
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.