Safe Haskell	Safe-Inferred
Language	Haskell2010

Twee

Contents

Configuration and prover state.
Messages.
The CP queue.
Active rewrite rules.

Description

The main prover loop.

Synopsis

data Config f = Config {
- cfg_accept_term :: Maybe (Term f -> Bool)
- cfg_max_critical_pairs :: Int64
- cfg_max_cp_depth :: Int
- cfg_simplify :: Bool
- cfg_renormalise_percent :: Int
- cfg_cp_sample_size :: Int
- cfg_renormalise_threshold :: Int
- cfg_set_join_goals :: Bool
- cfg_always_simplify :: Bool
- cfg_complete_subsets :: Bool
- cfg_critical_pairs :: Config
- cfg_join :: Config
- cfg_proof_presentation :: Config f
}
data State f = State {
- st_rules :: !(RuleIndex f (Rule f))
- st_active_set :: !(IntMap (Active f))
- st_joinable :: !(Index f (Equation f))
- st_goals :: ![Goal f]
- st_queue :: !(Queue Batch)
- st_next_active :: !Id
- st_considered :: !Int64
- st_simplified_at :: !Id
- st_cp_sample :: !(Sample (Maybe (Overlap (Active f) f)))
- st_not_complete :: !IntSet
- st_complete :: !(Index f (Rule f))
- st_messages_rev :: ![Message f]
}
defaultConfig :: Config f
configIsComplete :: Config f -> Bool
initialState :: Config f -> State f
data Message f
- = NewActive !(Active f)
- | NewEquation !(Equation f)
- | DeleteActive !(Active f)
- | SimplifyQueue
- | NotComplete !IntSet
- | Interreduce
- | Status !Int
message :: PrettyTerm f => Message f -> State f -> State f
clearMessages :: State f -> State f
messages :: State f -> [Message f]
makePassives :: Function f => Config f -> State f -> Active f -> [Passive]
data Passive = Passive {
- passive_score :: !Int32
- passive_rule1 :: !Id
- passive_rule2 :: !Id
- passive_how :: !How
}
data Batch = Batch {
- batch_kind :: !BatchKind
- batch_rule :: !Id
- batch_best :: !Passive
- batch_rest :: !(PackedSequence (Int32, Id, How))
}
data BatchKind
- = Rule1
- | Rule2
makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive
findPassive :: forall f. Function f => State f -> Passive -> Maybe (Overlap (Active f) f)
simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe Passive
shouldSimplifyQueue :: Function f => Config f -> State f -> Bool
simplifyQueue :: Function f => Config f -> State f -> State f
enqueue :: Function f => State f -> Id -> [Passive] -> State f
dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
data Active f = Active {
- active_id :: !Id
- active_info :: !Info
- active_rule :: !(Rule f)
- active_top :: !(Maybe (Term f))
- active_proof :: !(Proof f)
- active_model :: !(Model f)
- active_positions :: !(Positions2 f)
}
active_cp :: Active f -> CriticalPair f
activeRules :: Active f -> [Rule f]
data Info = Info {
- info_depth :: !Depth
- info_max :: !IntSet
}
addActive :: Function f => Config f -> State f -> (Id -> Active f) -> State f
sample :: Function f => Int -> [Passive] -> State f -> State f
resetSample :: Function f => Config f -> State f -> State f
simplifySample :: Function f => State f -> State f
addActiveOnly :: Function f => State f -> Active f -> State f
deleteActive :: Function f => State f -> Active f -> State f
consider :: Function f => Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing :: Function f => RuleIndex f (Rule f) -> Config f -> State f -> Info -> CriticalPair f -> State f
addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addAxiom :: Function f => Config f -> State f -> Axiom f -> State f
addJoinable :: Function f => State f -> Equation f -> State f
checkCompleteness :: Function f => Config f -> State f -> State f
assumeComplete :: Function f => State f -> State f
data Goal f = Goal {
- goal_name :: String
- goal_number :: Int
- goal_eqn :: Equation f
- goal_expanded_lhs :: Map (Term f) (Derivation f)
- goal_expanded_rhs :: Map (Term f) (Derivation f)
- goal_lhs :: Map (Term f) (Term f, Reduction f)
- goal_rhs :: Map (Term f) (Term f, Reduction f)
}
addGoal :: Function f => Config f -> State f -> Goal f -> State f
normaliseGoals :: Function f => Config f -> State f -> State f
recomputeGoals :: Function f => Config f -> State f -> State f
resetGoal :: Goal f -> Goal f
rewriteGoalsBackwards :: Function f => State f -> State f
goal :: Int -> String -> Equation f -> Goal f
interreduce :: Function f => Config f -> State f -> State f
interreduce1 :: Function f => Config f -> State f -> Active f -> State f
data Output m f = Output {
- output_message :: Message f -> m ()
}
complete :: (Function f, MonadIO m) => Output m f -> Config f -> State f -> m (State f)
complete1 :: Function f => Config f -> State f -> (Bool, State f)
solved :: Function f => State f -> Bool
solutions :: Function f => State f -> [ProvedGoal f]
rules :: Function f => State f -> [Rule f]
completePure :: Function f => Config f -> State f -> State f
normaliseTerm :: Function f => State f -> Term f -> Reduction f
normalForms :: Function f => State f -> Term f -> Map (Term f) (Reduction f)
simplifyTerm :: Function f => State f -> Term f -> Term f

Configuration and prover state.

data Config f Source #

The prover configuration.

Constructors

Config
Fields cfg_accept_term :: Maybe (Term f -> Bool) cfg_max_critical_pairs :: Int64 cfg_max_cp_depth :: Int cfg_simplify :: Bool cfg_renormalise_percent :: Int cfg_cp_sample_size :: Int cfg_renormalise_threshold :: Int cfg_set_join_goals :: Bool cfg_always_simplify :: Bool cfg_complete_subsets :: Bool cfg_critical_pairs :: Config cfg_join :: Config cfg_proof_presentation :: Config f

data State f Source #

The prover state.

Constructors

State

Fields

st_rules :: !(RuleIndex f (Rule f))
st_active_set :: !(IntMap (Active f))
st_joinable :: !(Index f (Equation f))
st_goals :: ![Goal f]
st_queue :: !(Queue Batch)
st_next_active :: !Id
st_considered :: !Int64
st_simplified_at :: !Id
st_cp_sample :: !(Sample (Maybe (Overlap (Active f) f)))
st_not_complete :: !IntSet
st_complete :: !(Index f (Rule f))
st_messages_rev :: ![Message f]

defaultConfig :: Config f Source #

The default prover configuration.

configIsComplete :: Config f -> Bool Source #

Does this configuration run the prover in a complete mode?

initialState :: Config f -> State f Source #

The initial state.

Messages.

data Message f Source #

A message which is produced by the prover when something interesting happens.

Constructors

NewActive !(Active f)	A new rule.
NewEquation !(Equation f)	A new joinable equation.
DeleteActive !(Active f)	A rule was deleted.
SimplifyQueue	The CP queue was simplified.
NotComplete !IntSet	All except these axioms are complete (with a suitable-chosen subset of the rules).
Interreduce	The rules were reduced wrt each other.
Status !Int	Status update: how many queued critical pairs there are.

Instances

Instances details

Function f => Pretty (Message f) Source #
Instance details Defined in Twee Methods pPrintPrec :: PrettyLevel -> Rational -> Message f -> Doc # pPrint :: Message f -> Doc # pPrintList :: PrettyLevel -> [Message f] -> Doc #

message :: PrettyTerm f => Message f -> State f -> State f Source #

Emit a message.

clearMessages :: State f -> State f Source #

Forget about all emitted messages.

messages :: State f -> [Message f] Source #

Get all emitted messages.

The CP queue.

makePassives :: Function f => Config f -> State f -> Active f -> [Passive] Source #

Compute all critical pairs from a rule.

data Passive Source #

Constructors

Passive
Fields passive_score :: !Int32 passive_rule1 :: !Id passive_rule2 :: !Id passive_how :: !How

Instances

Instances details

Eq Passive Source #
Instance details Defined in Twee Methods (==) :: Passive -> Passive -> Bool # (/=) :: Passive -> Passive -> Bool #
Ord Passive Source #
Instance details Defined in Twee Methods compare :: Passive -> Passive -> Ordering # (<) :: Passive -> Passive -> Bool # (<=) :: Passive -> Passive -> Bool # (>) :: Passive -> Passive -> Bool # (>=) :: Passive -> Passive -> Bool # max :: Passive -> Passive -> Passive # min :: Passive -> Passive -> Passive #

data Batch Source #

Constructors

Batch
Fields batch_kind :: !BatchKind batch_rule :: !Id batch_best :: !Passive batch_rest :: !(PackedSequence (Int32, Id, How))

data BatchKind Source #

Constructors

Rule1
Rule2

Instances

Instances details

Eq BatchKind Source #
Instance details Defined in Twee Methods (==) :: BatchKind -> BatchKind -> Bool # (/=) :: BatchKind -> BatchKind -> Bool #

makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Source #

findPassive :: forall f. Function f => State f -> Passive -> Maybe (Overlap (Active f) f) Source #

Turn a Passive back into an overlap. Doesn't try to simplify it.

simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe Passive Source #

Renormalise a queued Passive.

shouldSimplifyQueue :: Function f => Config f -> State f -> Bool Source #

Check if we should renormalise the queue.

simplifyQueue :: Function f => Config f -> State f -> State f Source #

Renormalise the entire queue.

enqueue :: Function f => State f -> Id -> [Passive] -> State f Source #

Enqueue a set of critical pairs.

dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f) Source #

Dequeue a critical pair.

Also takes care of:

removing any orphans from the head of the queue
ignoring CPs that are too big

Active rewrite rules.

data Active f Source #

Constructors

Active
Fields active_id :: !Id active_info :: !Info active_rule :: !(Rule f) active_top :: !(Maybe (Term f)) active_proof :: !(Proof f) active_model :: !(Model f) active_positions :: !(Positions2 f)

Instances

Instances details

Eq (Active f) Source #
Instance details Defined in Twee Methods (==) :: Active f -> Active f -> Bool # (/=) :: Active f -> Active f -> Bool #
Function f => Pretty (Active f) Source #
Instance details Defined in Twee Methods pPrintPrec :: PrettyLevel -> Rational -> Active f -> Doc # pPrint :: Active f -> Doc # pPrintList :: PrettyLevel -> [Active f] -> Doc #
Has (Active f) Id Source #
Instance details Defined in Twee Methods the :: Active f -> Id Source #
Has (Active f) Depth Source #
Instance details Defined in Twee Methods the :: Active f -> Depth Source #
f ~ g => Has (Active f) (Positions2 g) Source #
Instance details Defined in Twee Methods the :: Active f -> Positions2 g Source #
f ~ g => Has (Active f) (Rule g) Source #
Instance details Defined in Twee Methods the :: Active f -> Rule g Source #

active_cp :: Active f -> CriticalPair f Source #

activeRules :: Active f -> [Rule f] Source #

data Info Source #

Constructors

Info
Fields info_depth :: !Depth info_max :: !IntSet

addActive :: Function f => Config f -> State f -> (Id -> Active f) -> State f Source #

sample :: Function f => Int -> [Passive] -> State f -> State f Source #

resetSample :: Function f => Config f -> State f -> State f Source #

simplifySample :: Function f => State f -> State f Source #

addActiveOnly :: Function f => State f -> Active f -> State f Source #

deleteActive :: Function f => State f -> Active f -> State f Source #

consider :: Function f => Config f -> State f -> Info -> CriticalPair f -> State f Source #

considerUsing :: Function f => RuleIndex f (Rule f) -> Config f -> State f -> Info -> CriticalPair f -> State f Source #

addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f Source #

addAxiom :: Function f => Config f -> State f -> Axiom f -> State f Source #

addJoinable :: Function f => State f -> Equation f -> State f Source #

checkCompleteness :: Function f => Config f -> State f -> State f Source #

assumeComplete :: Function f => State f -> State f Source #

data Goal f Source #

Constructors

Goal
Fields goal_name :: String goal_number :: Int goal_eqn :: Equation f goal_expanded_lhs :: Map (Term f) (Derivation f) goal_expanded_rhs :: Map (Term f) (Derivation f) goal_lhs :: Map (Term f) (Term f, Reduction f) goal_rhs :: Map (Term f) (Term f, Reduction f)

Instances

Instances details

(Labelled f, Show f) => Show (Goal f) Source #
Instance details Defined in Twee Methods showsPrec :: Int -> Goal f -> ShowS # show :: Goal f -> String # showList :: [Goal f] -> ShowS #