| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Otter.Internal.Search
Synopsis
- data ProverState n = PS {
- _rules :: [SearchProperRule n]
- _actives :: ActiveNodes n
- _inactives :: InactiveNodes n
- _index :: GlobalIndex n
- _isGoal :: n -> Bool
- type Prover s g a = State (ProverState s) a
- type RuleAppRes n = ([ConclNode n], [SearchProperRule n])
- popInactive :: Prover s g (Maybe (ActiveNode s))
- getActives :: Prover s g (ActiveNodes s)
- getRules :: Prover s g [SearchProperRule s]
- isGoalM :: FSCheckedNode s -> Prover s g (Maybe (FSCheckedNode s))
- haveGoal :: [FSCheckedNode s] -> Prover s g (Maybe (FSCheckedNode s))
- filterUnsubsumed :: Subsumable s => [ConclNode s] -> Prover s g [SearchNode FSChecked s]
- isNotFwdSubsumed :: Subsumable s => ConclNode s -> Prover s g (Maybe (SearchNode FSChecked s))
- removeSubsumedBy :: Subsumable s => SearchNode FSChecked s -> Prover s g (SearchNode BSChecked s)
- addRule :: SearchProperRule s -> Prover s g ()
- addInactive :: SearchNode BSChecked s -> Prover s g ()
- percolate :: ActiveNodes s -> [SearchProperRule s] -> RuleAppRes s
- processNewActive :: ActiveNode s -> Prover s g (RuleAppRes s)
- merge :: Maybe (SearchNode s a) -> SearchRes a -> SearchRes a
- loop :: Subsumable s => Prover s g (SearchRes s)
- doSearch :: Subsumable s => [SearchNode Initial s] -> [SearchProperRule s] -> Prover s g (SearchRes s)
- search :: Subsumable s => [s] -> [s -> Rule s s] -> (s -> Bool) -> (SearchRes s, [s])
Documentation
data ProverState n Source #
Constructors
| PS | |
Fields
| |
type Prover s g a = State (ProverState s) a Source #
type RuleAppRes n = ([ConclNode n], [SearchProperRule n]) Source #
Result type of matching a list of rules to an input sequent.
popInactive :: Prover s g (Maybe (ActiveNode s)) Source #
getActives :: Prover s g (ActiveNodes s) Source #
getRules :: Prover s g [SearchProperRule s] Source #
isGoalM :: FSCheckedNode s -> Prover s g (Maybe (FSCheckedNode s)) Source #
haveGoal :: [FSCheckedNode s] -> Prover s g (Maybe (FSCheckedNode s)) Source #
filterUnsubsumed :: Subsumable s => [ConclNode s] -> Prover s g [SearchNode FSChecked s] Source #
isNotFwdSubsumed :: Subsumable s => ConclNode s -> Prover s g (Maybe (SearchNode FSChecked s)) Source #
removeSubsumedBy :: Subsumable s => SearchNode FSChecked s -> Prover s g (SearchNode BSChecked s) Source #
addRule :: SearchProperRule s -> Prover s g () Source #
addInactive :: SearchNode BSChecked s -> Prover s g () Source #
percolate :: ActiveNodes s -> [SearchProperRule s] -> RuleAppRes s Source #
processNewActive :: ActiveNode s -> Prover s g (RuleAppRes s) Source #
doSearch :: Subsumable s => [SearchNode Initial s] -> [SearchProperRule s] -> Prover s g (SearchRes s) Source #