| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Twee
Description
The main prover loop.
- data Config f = Config {}
- 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_messages_rev :: ![Message f]
- defaultConfig :: Config f
- configIsComplete :: Config f -> Bool
- initialState :: State f
- data Message f
- = NewActive !(Active f)
- | NewEquation !(Equation f)
- | DeleteActive !(Active f)
- | SimplifyQueue
- | Interreduce
- 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 => Config f -> State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
- simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)
- 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_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_rule :: !(Rule f)
- rule_proof :: !(Proof f)
- rule_positions :: !(Positions f)
- newtype RuleId = RuleId Id
- addActive :: Function f => Config f -> State f -> (Id -> RuleId -> RuleId -> Active 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
- data Goal f = Goal {}
- addGoal :: Function f => Config f -> State f -> Goal f -> State f
- normaliseGoals :: Function f => State f -> State f
- recomputeGoals :: 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 -> Resulting f
- normalForms :: Function f => State f -> Term f -> Set (Resulting f)
- simplifyTerm :: Function f => State f -> Term f -> Term f
Configuration and prover state.
The prover configuration.
Constructors
| Config | |
Fields
| |
The prover state.
Constructors
| State | |
Fields
| |
defaultConfig :: Config f Source #
The default prover configuration.
configIsComplete :: Config f -> Bool Source #
Does this configuration run the prover in a complete mode?
initialState :: State f Source #
The initial state.
Messages.
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. |
| Interreduce | The rules were reduced wrt each other. |
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 => Config 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.
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.
Constructors
| Active | |
Fields
| |
active_cp :: Active f -> CriticalPair f Source #
data ActiveRule f Source #
Constructors
| ActiveRule | |
Fields
| |
Instances
| Eq (ActiveRule f) Source # | |
| PrettyTerm f => Symbolic (ActiveRule f) 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) (Lemma g) Source # | |
| (~) * f g => Has (ActiveRule f) (Proof g) Source # | |
| (~) * f g => Has (ActiveRule f) (Rule g) Source # | |
| type ConstantOf (ActiveRule f) Source # | |
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 #