Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 (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
- 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]
- data Params
- makePassives :: Function f => Config f -> State f -> ActiveRule f -> [Passive Params]
- findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
- simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)
- shouldSimplifyQueue :: Function f => Config f -> State f -> Bool
- simplifyQueue :: Function f => Config f -> State f -> State f
- enqueue :: Function f => State f -> RuleId -> [Passive Params] -> State f
- dequeue :: Function f => Config f -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f), State f)
- data Active f = Active {
- 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]
- active_cp :: Active f -> CriticalPair f
- data ActiveRule f = ActiveRule {
- rule_active :: !Id
- rule_rid :: !RuleId
- rule_depth :: !Depth
- rule_max :: !Max
- rule_rule :: !(Rule f)
- rule_positions :: !(Positions f)
- newtype RuleId = RuleId Id
- 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
- 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.
The prover configuration.
The prover state.
State | |
|
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.
A message which is produced by the prover when something interesting happens.
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. |
clearMessages :: State f -> State f Source #
Forget about all emitted messages.
The CP queue.
makePassives :: Function f => Config f -> State f -> ActiveRule f -> [Passive Params] Source #
Compute all critical pairs from a rule.
findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f) Source #
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) Source #
Renormalise a queued Passive.
shouldSimplifyQueue :: Function f => Config f -> State f -> Bool Source #
Check if we should renormalise the queue.
enqueue :: Function f => State f -> RuleId -> [Passive Params] -> State f Source #
Enqueue a set of critical pairs.
dequeue :: Function f => Config f -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule 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.
Active | |
|
active_cp :: Active f -> CriticalPair f Source #
data ActiveRule f Source #
ActiveRule | |
|
Instances
Eq (ActiveRule f) Source # | |
Defined in Twee (==) :: ActiveRule f -> ActiveRule f -> Bool # (/=) :: ActiveRule f -> ActiveRule f -> Bool # | |
PrettyTerm f => Symbolic (ActiveRule f) Source # | |
Defined in Twee type ConstantOf (ActiveRule f) Source # termsDL :: ActiveRule f -> DList (TermListOf (ActiveRule f)) Source # subst_ :: (Var -> BuilderOf (ActiveRule f)) -> ActiveRule f -> ActiveRule f Source # | |
Has (ActiveRule f) Max Source # | |
Has (ActiveRule f) Depth Source # | |
Has (ActiveRule f) RuleId Source # | |
Has (ActiveRule f) Id Source # | |
f ~ g => Has (ActiveRule f) (Positions g) Source # | |
f ~ g => Has (ActiveRule f) (Rule g) Source # | |
type ConstantOf (ActiveRule f) Source # | |
Defined in Twee |
addActive :: Function f => Config f -> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f Source #
considerUsing :: Function f => RuleIndex f (ActiveRule f) -> Config f -> State f -> CriticalPair f -> State f Source #
Goal | |
|