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 (ActiveRule f))
• st_active_ids :: !(IntMap (Active f))
• st_rule_ids :: !(IntMap (ActiveRule f))
• st_joinable :: !(Index f (Equation f))
• st_goals :: ![Goal f]
• st_queue :: !(Queue Params)
• st_next_active :: !Id
• st_next_rule :: !RuleId
• st_considered :: !Int64
• st_simplified_at :: !Id
• st_cp_sample :: ![Maybe (Overlap f)]
• st_cp_next_sample :: ![(Integer, Int)]
• st_num_cps :: !Integer
• 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.

data Params

Instances

Params Params

Defined in Twee

Associated Types

type Score Params

type Id Params

type PackedScore Params

type PackedId Params

Methods

packScore :: proxy Params -> Score Params -> PackedScore Params

unpackScore :: proxy Params -> PackedScore Params -> Score Params

packId :: proxy Params -> Id Params -> PackedId Params

unpackId :: proxy Params -> PackedId Params -> Id Params

type Score Params

Defined in Twee

type Score Params = Int

type Id Params

Defined in Twee

type Id Params = RuleId

type PackedScore Params

Defined in Twee

type PackedScore Params = Int32

type PackedId Params

Defined in Twee

type PackedId Params = Int32

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

Compute all critical pairs from a rule.

findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)

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

simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)

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 -> RuleId -> [Passive Params] -> State f

Enqueue a set of critical pairs.

dequeue :: Function f => Config f -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule 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_depth :: !Depth
• active_rule :: !(Rule f)
• active_top :: !(Maybe (Term f))
• active_proof :: !(Proof f)
• active_max :: !Max
• active_model :: !(Model f)
• active_rules :: ![ActiveRule 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

active_cp :: Active f -> CriticalPair f

data ActiveRule f

Constructors

ActiveRule

Fields

• rule_active :: !Id
• rule_rid :: !RuleId
• rule_depth :: !Depth
• rule_max :: !Max
• rule_rule :: !(Rule f)
• rule_positions :: !(Positions f)

Instances

Eq (ActiveRule f)

Defined in Twee

Methods

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

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

PrettyTerm f => Symbolic (ActiveRule f)

Defined in Twee

Associated Types

type ConstantOf (ActiveRule f)

Methods

termsDL :: ActiveRule f -> DList (TermListOf (ActiveRule f))

subst_ :: (Var -> BuilderOf (ActiveRule f)) -> ActiveRule f -> ActiveRule f

Has (ActiveRule f) Max

Defined in Twee

Methods

the :: ActiveRule f -> Max

Has (ActiveRule f) Depth

Defined in Twee

Methods

the :: ActiveRule f -> Depth

Has (ActiveRule f) RuleId

Defined in Twee

Methods

the :: ActiveRule f -> RuleId

Has (ActiveRule f) Id

Defined in Twee

Methods

the :: ActiveRule f -> Id

f ~ g => Has (ActiveRule f) (Positions g)

Defined in Twee

Methods

the :: ActiveRule f -> Positions g

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

Defined in Twee

Methods

the :: ActiveRule f -> Rule g

type ConstantOf (ActiveRule f)

Defined in Twee

type ConstantOf (ActiveRule f) = f

newtype RuleId

Constructors

RuleId Id

Instances

Enum RuleId

Defined in Twee

Methods

succ :: RuleId -> RuleId

pred :: RuleId -> RuleId

toEnum :: Int -> RuleId

fromEnum :: RuleId -> Int

enumFrom :: RuleId -> [RuleId]

enumFromThen :: RuleId -> RuleId -> [RuleId]

enumFromTo :: RuleId -> RuleId -> [RuleId]

enumFromThenTo :: RuleId -> RuleId -> RuleId -> [RuleId]

Eq RuleId

Defined in Twee

Methods

(==) :: RuleId -> RuleId -> Bool

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

Integral RuleId

Defined in Twee

Methods

quot :: RuleId -> RuleId -> RuleId

rem :: RuleId -> RuleId -> RuleId

div :: RuleId -> RuleId -> RuleId

mod :: RuleId -> RuleId -> RuleId

quotRem :: RuleId -> RuleId -> (RuleId, RuleId)

divMod :: RuleId -> RuleId -> (RuleId, RuleId)

toInteger :: RuleId -> Integer

Num RuleId

Defined in Twee

Methods

(+) :: RuleId -> RuleId -> RuleId

(-) :: RuleId -> RuleId -> RuleId

(*) :: RuleId -> RuleId -> RuleId

negate :: RuleId -> RuleId

abs :: RuleId -> RuleId

signum :: RuleId -> RuleId

fromInteger :: Integer -> RuleId

Ord RuleId

Defined in Twee

Methods

compare :: RuleId -> RuleId -> Ordering

(<) :: RuleId -> RuleId -> Bool

(<=) :: RuleId -> RuleId -> Bool

(>) :: RuleId -> RuleId -> Bool

(>=) :: RuleId -> RuleId -> Bool

max :: RuleId -> RuleId -> RuleId

min :: RuleId -> RuleId -> RuleId

Real RuleId

Defined in Twee

Methods

toRational :: RuleId -> Rational

Show RuleId

Defined in Twee

Methods

showsPrec :: Int -> RuleId -> ShowS

show :: RuleId -> String

showList :: [RuleId] -> ShowS

Has (ActiveRule f) RuleId

Defined in Twee

Methods

the :: ActiveRule f -> RuleId

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

sample :: Function f => Config f -> Int -> [Passive Params] -> 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 -> CriticalPair f -> State f

considerUsing :: Function f => RuleIndex f (ActiveRule f) -> Config f -> State f -> CriticalPair f -> State f

addCP :: Function f => Config f -> Model f -> State f -> 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

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