Otter.Internal.Structures

Documentation

data Stage

Stages of proof search

Constructors

Initial

Initial node

Active

Active node

Inactive

Inactive node

Concl

Conclusion node

FSChecked

Forward subsumption-checked

BSChecked

Backward subsumption-checked

GlIndex

Global index node

Goal

Goal node

data SearchNode :: Stage -> * -> *

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)

Defined in Otter.Internal.Structures

Methods

showsPrec :: Int -> SearchNode s a -> ShowS

show :: SearchNode s a -> String

showList :: [SearchNode s a] -> ShowS

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

Instances

Foldable GlobalIndex

Defined in Otter.Internal.Structures

Methods

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)

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)

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

Methods

subsumes :: n -> n -> Bool

Instances

(Ord a, Ord l) => Subsumable (LSequent a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

subsumes :: LSequent a l -> LSequent a l -> Bool

Subsumable s => Subsumable (tm ::: s)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

subsumes :: (tm ::: s) -> (tm ::: s) -> Bool

(Ord a, Ord l) => Subsumable (GoalNSequent a l)

Defined in Zsyntax.Labelled.Rule.Frontier

Methods

subsumes :: GoalNSequent a l -> GoalNSequent a l -> Bool

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