Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- data Stage
- data SearchNode :: Stage -> * -> *
- type ActiveNode n = SearchNode Active n
- type FSCheckedNode n = SearchNode FSChecked n
- type BSCheckedNode n = SearchNode BSChecked n
- type InactiveNode n = SearchNode Inactive n
- data ActiveNodes n
- data InactiveNodes n
- type ConclNode n = SearchNode Concl n
- data GlobalIndex n
- type SearchRule n = Rule (ActiveNode n) (ConclNode n)
- type SearchProperRule n = ProperRule (ActiveNode n) (ConclNode n)
- class Subsumable n where
- initIsFSCheckd :: SearchNode Initial n -> FSCheckedNode n
- initIsBSCheckd :: SearchNode Initial n -> BSCheckedNode n
- initialize :: n -> SearchNode Initial n
- removeSubsumedByOp :: Subsumable n => FSCheckedNode n -> InactiveNodes n -> (InactiveNodes n, BSCheckedNode n)
- fwdSubsumes :: Subsumable n => GlobalIndex n -> SearchNode Concl n -> Maybe (FSCheckedNode n)
- activate :: ActiveNodes n -> InactiveNode n -> (ActiveNodes n, ActiveNode n)
- popInactiveOp :: InactiveNodes n -> Maybe (InactiveNodes n, InactiveNode n)
- addToInactives :: InactiveNodes n -> GlobalIndex n -> BSCheckedNode n -> (InactiveNodes n, GlobalIndex n)
- foldActives :: (forall f. Foldable f => f (ActiveNode n) -> b) -> ActiveNodes n -> b
- mkGoal :: n -> SearchNode Goal n
- emptyActives :: ActiveNodes n
- emptyInactives :: InactiveNodes n
- emptyGI :: GlobalIndex n
- toProperRule :: (n -> Rule n n) -> SearchProperRule n
- extractNode :: SearchNode s seq -> seq
Documentation
Stages of proof search
data SearchNode :: Stage -> * -> * Source #
Type of search nodes in the search space, given by a node together with a proof search stage.
Instances
Show a => Show (SearchNode s a) Source # | |
Defined in Otter.Internal.Structures showsPrec :: Int -> SearchNode s a -> ShowS # show :: SearchNode s a -> String # showList :: [SearchNode s a] -> ShowS # |
type ActiveNode n = SearchNode Active n Source #
type FSCheckedNode n = SearchNode FSChecked n Source #
type BSCheckedNode n = SearchNode BSChecked n Source #
type InactiveNode n = SearchNode Inactive n Source #
data ActiveNodes n Source #
data InactiveNodes n Source #
type ConclNode n = SearchNode Concl n Source #
data GlobalIndex n Source #
Instances
Foldable GlobalIndex Source # | |
Defined in Otter.Internal.Structures fold :: Monoid m => GlobalIndex m -> m # foldMap :: Monoid m => (a -> m) -> GlobalIndex a -> m # foldr :: (a -> b -> b) -> b -> GlobalIndex a -> b # foldr' :: (a -> b -> b) -> b -> GlobalIndex a -> b # foldl :: (b -> a -> b) -> b -> GlobalIndex a -> b # foldl' :: (b -> a -> b) -> b -> GlobalIndex a -> b # foldr1 :: (a -> a -> a) -> GlobalIndex a -> a # foldl1 :: (a -> a -> a) -> GlobalIndex a -> a # toList :: GlobalIndex a -> [a] # null :: GlobalIndex a -> Bool # length :: GlobalIndex a -> Int # elem :: Eq a => a -> GlobalIndex a -> Bool # maximum :: Ord a => GlobalIndex a -> a # minimum :: Ord a => GlobalIndex a -> a # sum :: Num a => GlobalIndex a -> a # product :: Num a => GlobalIndex a -> a # |
type SearchRule n = Rule (ActiveNode n) (ConclNode n) Source #
Type of elements that represent the result of applying an inference rule.
Such application may either fail, succeed with a value (when the rule has been fully applied), or succeed with a function (when the rule is only partially applied and has still some premises to match).
type SearchProperRule n = ProperRule (ActiveNode n) (ConclNode n) Source #
Type of inference rules. Axioms are not considered rules in this case, so a rule takes at least one premise. Hence the corresponding type is a function from a premise sequent to a rule application result.
class Subsumable n where Source #
Instances
(Ord a, Ord l) => Subsumable (LSequent a l) Source # | |
Subsumable s => Subsumable (tm ::: s) Source # | |
(Ord a, Ord l) => Subsumable (GoalNSequent a l) Source # | |
Defined in Zsyntax.Labelled.Rule.Frontier subsumes :: GoalNSequent a l -> GoalNSequent a l -> Bool Source # |
initIsFSCheckd :: SearchNode Initial n -> FSCheckedNode n Source #
initIsBSCheckd :: SearchNode Initial n -> BSCheckedNode n Source #
initialize :: n -> SearchNode Initial n Source #
removeSubsumedByOp :: Subsumable n => FSCheckedNode n -> InactiveNodes n -> (InactiveNodes n, BSCheckedNode n) Source #
fwdSubsumes :: Subsumable n => GlobalIndex n -> SearchNode Concl n -> Maybe (FSCheckedNode n) Source #
activate :: ActiveNodes n -> InactiveNode n -> (ActiveNodes n, ActiveNode n) Source #
popInactiveOp :: InactiveNodes n -> Maybe (InactiveNodes n, InactiveNode n) Source #
addToInactives :: InactiveNodes n -> GlobalIndex n -> BSCheckedNode n -> (InactiveNodes n, GlobalIndex n) Source #
foldActives :: (forall f. Foldable f => f (ActiveNode n) -> b) -> ActiveNodes n -> b Source #
mkGoal :: n -> SearchNode Goal n Source #
emptyActives :: ActiveNodes n Source #
emptyGI :: GlobalIndex n Source #
toProperRule :: (n -> Rule n n) -> SearchProperRule n Source #
extractNode :: SearchNode s seq -> seq Source #