Twee

The main prover loop.

Configuration and prover state.

data Config f

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

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

The default prover configuration.

configIsComplete :: Config f -> Bool

Does this configuration run the prover in a complete mode?

initialState :: Config f -> State f

The initial state.

Messages.

data Message f

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

Function f => Pretty (Message f)

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

Emit a message.

clearMessages :: State f -> State f

Forget about all emitted messages.

messages :: State f -> [Message f]

Get all emitted messages.

The CP queue.

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

Compute all critical pairs from a rule.

data Passive

Constructors

Passive

Fields

• passive_score :: !Int32
• passive_rule1 :: !Id
• passive_rule2 :: !Id
• passive_how :: !How

Instances

Eq Passive

Defined in Twee

Methods

(==) :: Passive -> Passive -> Bool

(/=) :: Passive -> Passive -> Bool

Ord Passive

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

Constructors

Batch

Fields

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

data BatchKind

Constructors

Rule1

Rule2

Instances

Eq BatchKind

Defined in Twee

Methods

(==) :: BatchKind -> BatchKind -> Bool

(/=) :: BatchKind -> BatchKind -> Bool

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

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

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

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

Renormalise a queued Passive.

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

Check if we should renormalise the queue.

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

Renormalise the entire queue.

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

Enqueue a set of critical pairs.

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

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

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

Eq (Active f)

Defined in Twee

Methods

(==) :: Active f -> Active f -> Bool

(/=) :: Active f -> Active f -> Bool

Function f => Pretty (Active f)

Defined in Twee

Methods

pPrintPrec :: PrettyLevel -> Rational -> Active f -> Doc

pPrint :: Active f -> Doc

pPrintList :: PrettyLevel -> [Active f] -> Doc

Has (Active f) Id

Defined in Twee

Methods

the :: Active f -> Id

Has (Active f) Depth

Defined in Twee

Methods

the :: Active f -> Depth

f ~ g => Has (Active f) (Positions2 g)

Defined in Twee

Methods

the :: Active f -> Positions2 g

f ~ g => Has (Active f) (Rule g)

Defined in Twee

Methods

the :: Active f -> Rule g

active_cp :: Active f -> CriticalPair f

activeRules :: Active f -> [Rule f]

data Info

Constructors

Info

Fields

• 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

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

(Labelled f, Show f) => Show (Goal f)

Defined in Twee

Methods

showsPrec :: Int -> Goal f -> ShowS

show :: Goal f -> String

showList :: [Goal f] -> ShowS

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

Constructors

Output

Fields

• 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