-- | The main prover loop.
{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances #-}
module Twee where

import Twee.Base
import Twee.Rule hiding (normalForms)
import qualified Twee.Rule as Rule
import Twee.Equation
import qualified Twee.Proof as Proof
import Twee.Proof(Axiom(..), Proof(..), Derivation, ProvedGoal(..), provedGoal, certify, derivation)
import Twee.CP hiding (Config)
import qualified Twee.CP as CP
import Twee.Join hiding (Config, defaultConfig)
import qualified Twee.Join as Join
import qualified Twee.Rule.Index as RuleIndex
import Twee.Rule.Index(RuleIndex(..))
import qualified Twee.Index as Index
import Twee.Index(Index)
import Twee.Constraints
import Twee.Utils
import Twee.Task
import qualified Data.BatchedQueue as Queue
import Data.BatchedQueue(Queue)
import qualified Data.IntMap.Strict as IntMap
import Data.IntMap(IntMap)
import Data.Maybe
import Data.List
import Data.Function
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.Int
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import qualified Control.Monad.Trans.State.Strict as StateM
import qualified Data.IntSet as IntSet
import Data.IntSet(IntSet)
import Twee.Profile
import Data.Ord
import Data.PackedSequence(PackedSequence)
import qualified Data.PackedSequence as PackedSequence

----------------------------------------------------------------------
-- * Configuration and prover state.
----------------------------------------------------------------------

-- | The prover configuration.
data Config f =
  Config {
    forall f. Config f -> Maybe (Term f -> Bool)
cfg_accept_term            :: Maybe (Term f -> Bool),
    forall f. Config f -> Int64
cfg_max_critical_pairs     :: Int64,
    forall f. Config f -> Int
cfg_max_cp_depth           :: Int,
    forall f. Config f -> Bool
cfg_simplify               :: Bool,
    forall f. Config f -> Int
cfg_renormalise_percent    :: Int,
    forall f. Config f -> Int
cfg_cp_sample_size         :: Int,
    forall f. Config f -> Int
cfg_renormalise_threshold  :: Int,
    forall f. Config f -> Bool
cfg_set_join_goals         :: Bool,
    forall f. Config f -> Bool
cfg_always_simplify        :: Bool,
    forall f. Config f -> Bool
cfg_complete_subsets       :: Bool,
    forall f. Config f -> Config
cfg_critical_pairs         :: CP.Config,
    forall f. Config f -> Config
cfg_join                   :: Join.Config,
    forall f. Config f -> Config f
cfg_proof_presentation     :: Proof.Config f }

-- | The prover state.
data State f =
  State {
    forall f. State f -> RuleIndex f (Rule f)
st_rules          :: !(RuleIndex f (Rule f)),
    forall f. State f -> IntMap (Active f)
st_active_set     :: !(IntMap (Active f)),
    forall f. State f -> Index f (Equation f)
st_joinable       :: !(Index f (Equation f)),
    forall f. State f -> [Goal f]
st_goals          :: ![Goal f],
    forall f. State f -> Queue Batch
st_queue          :: !(Queue Batch),
    forall f. State f -> Id
st_next_active    :: {-# UNPACK #-} !Id,
    forall f. State f -> Int64
st_considered     :: {-# UNPACK #-} !Int64,
    forall f. State f -> Id
st_simplified_at  :: {-# UNPACK #-} !Id,
    forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_cp_sample      :: !(Sample (Maybe (Overlap (Active f) f))),
    forall f. State f -> IntSet
st_not_complete   :: !IntSet,
    forall f. State f -> Index f (Rule f)
st_complete       :: !(Index f (Rule f)),
    forall f. State f -> [Message f]
st_messages_rev   :: ![Message f] }

-- | The default prover configuration.
defaultConfig :: Config f
defaultConfig :: forall f. Config f
defaultConfig =
  Config {
    cfg_accept_term :: Maybe (Term f -> Bool)
cfg_accept_term = forall a. Maybe a
Nothing,
    cfg_max_critical_pairs :: Int64
cfg_max_critical_pairs = forall a. Bounded a => a
maxBound,
    cfg_max_cp_depth :: Int
cfg_max_cp_depth = forall a. Bounded a => a
maxBound,
    cfg_simplify :: Bool
cfg_simplify = Bool
True,
    cfg_renormalise_percent :: Int
cfg_renormalise_percent = Int
5,
    cfg_renormalise_threshold :: Int
cfg_renormalise_threshold = Int
20,
    cfg_cp_sample_size :: Int
cfg_cp_sample_size = Int
100,
    cfg_set_join_goals :: Bool
cfg_set_join_goals = Bool
True,
    cfg_always_simplify :: Bool
cfg_always_simplify = Bool
False,
    cfg_complete_subsets :: Bool
cfg_complete_subsets = Bool
False,
    cfg_critical_pairs :: Config
cfg_critical_pairs = Config
CP.defaultConfig,
    cfg_join :: Config
cfg_join = Config
Join.defaultConfig,
    cfg_proof_presentation :: Config f
cfg_proof_presentation = forall f. Config f
Proof.defaultConfig }

-- | Does this configuration run the prover in a complete mode?
configIsComplete :: Config f -> Bool
configIsComplete :: forall f. Config f -> Bool
configIsComplete Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} =
  forall a. Maybe a -> Bool
isNothing (Maybe (Term f -> Bool)
cfg_accept_term) Bool -> Bool -> Bool
&&
  Int64
cfg_max_critical_pairs forall a. Eq a => a -> a -> Bool
== forall a. Bounded a => a
maxBound Bool -> Bool -> Bool
&&
  Int
cfg_max_cp_depth forall a. Eq a => a -> a -> Bool
== forall a. Bounded a => a
maxBound

-- | The initial state.
initialState :: Config f -> State f
initialState :: forall f. Config f -> State f
initialState Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} =
  State {
    st_rules :: RuleIndex f (Rule f)
st_rules = forall f a. RuleIndex f a
RuleIndex.empty,
    st_active_set :: IntMap (Active f)
st_active_set = forall a. IntMap a
IntMap.empty,
    st_joinable :: Index f (Equation f)
st_joinable = forall f a. Index f a
Index.empty,
    st_goals :: [Goal f]
st_goals = [],
    st_queue :: Queue Batch
st_queue = forall a. Queue a
Queue.empty,
    st_next_active :: Id
st_next_active = Id
1,
    st_considered :: Int64
st_considered = Int64
0,
    st_simplified_at :: Id
st_simplified_at = Id
1,
    st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = forall a. Int -> Sample a
emptySample Int
cfg_cp_sample_size,
    st_not_complete :: IntSet
st_not_complete = IntSet
IntSet.empty,
    st_complete :: Index f (Rule f)
st_complete = forall f a. Index f a
Index.empty,
    st_messages_rev :: [Message f]
st_messages_rev = [] }

----------------------------------------------------------------------
-- * Messages.
----------------------------------------------------------------------

-- | A message which is produced by the prover when something interesting happens.
data Message f =
    -- | A new rule.
    NewActive !(Active f)
    -- | A new joinable equation.
  | NewEquation !(Equation f)
    -- | A rule was deleted.
  | DeleteActive !(Active f)
    -- | The CP queue was simplified.
  | SimplifyQueue
    -- | All except these axioms are complete (with a suitable-chosen subset of the rules).
  | NotComplete !IntSet
    -- | The rules were reduced wrt each other.
  | Interreduce
    -- | Status update: how many queued critical pairs there are.
  | Status !Int

instance Function f => Pretty (Message f) where
  pPrint :: Message f -> Doc
pPrint (NewActive Active f
rule) = forall a. Pretty a => a -> Doc
pPrint Active f
rule
  pPrint (NewEquation Equation f
eqn) =
    String -> Doc
text String
"  (hard)" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Equation f
eqn
  pPrint (DeleteActive Active f
rule) =
    String -> Doc
text String
"  (delete rule " Doc -> Doc -> Doc
<#> forall a. Pretty a => a -> Doc
pPrint (forall f. Active f -> Id
active_id Active f
rule) Doc -> Doc -> Doc
<#> String -> Doc
text String
")"
  pPrint Message f
SimplifyQueue =
    String -> Doc
text String
"  (simplifying queued critical pairs...)"
  pPrint (NotComplete IntSet
ax) =
    case IntSet -> [Int]
IntSet.toList IntSet
ax of
      [Int
n] ->
        String -> Doc
text String
"  (axiom" Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint Int
n Doc -> Doc -> Doc
<+> Doc
"is not completed yet)"
      [Int]
xs ->
        String -> Doc
text String
"  (axioms" Doc -> Doc -> Doc
<+> String -> Doc
text (forall a. Show a => a -> String
show [Int]
xs) Doc -> Doc -> Doc
<+> Doc
"are not completed yet)"
  pPrint Message f
Interreduce =
    String -> Doc
text String
"  (simplifying rules with respect to one another...)"
  pPrint (Status Int
n) =
    String -> Doc
text String
"  (" Doc -> Doc -> Doc
<#> forall a. Pretty a => a -> Doc
pPrint Int
n Doc -> Doc -> Doc
<+> String -> Doc
text String
"queued critical pairs)"

-- | Emit a message.
message :: PrettyTerm f => Message f -> State f -> State f
message :: forall f. PrettyTerm f => Message f -> State f -> State f
message !Message f
msg state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  State f
state { st_messages_rev :: [Message f]
st_messages_rev = Message f
msgforall a. a -> [a] -> [a]
:[Message f]
st_messages_rev }

-- | Forget about all emitted messages.
clearMessages :: State f -> State f
clearMessages :: forall f. State f -> State f
clearMessages state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  State f
state { st_messages_rev :: [Message f]
st_messages_rev = [] }

-- | Get all emitted messages.
messages :: State f -> [Message f]
messages :: forall f. State f -> [Message f]
messages State f
state = forall a. [a] -> [a]
reverse (forall f. State f -> [Message f]
st_messages_rev State f
state)

----------------------------------------------------------------------
-- * The CP queue.
----------------------------------------------------------------------

-- | Compute all critical pairs from a rule.
{-# INLINEABLE makePassives #-}
makePassives :: Function f => Config f -> State f -> Active f -> [Passive]
makePassives :: forall f.
Function f =>
Config f -> State f -> Active f -> [Passive]
makePassives config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Active f
rule =
-- XXX factor out depth calculation
  forall symbol a b. symbol -> (a -> b) -> a -> a
stampWith String
"make critical pair" forall (t :: * -> *) a. Foldable t => t a -> Int
length
  [ forall f. Function f => Config f -> Overlap (Active f) f -> Passive
makePassive Config f
config Overlap (Active f) f
overlap
  | Active f -> Bool
ok Active f
rule,
    Overlap (Active f) f
overlap <- forall a b f.
(Function f, Has a (Rule f), Has b (Rule f),
 Has b (Positions2 f)) =>
Index f a -> [b] -> b -> [Overlap b f]
overlaps (forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) (forall a. (a -> Bool) -> [a] -> [a]
filter Active f -> Bool
ok [Active f]
rules) Active f
rule ]
  where
    rules :: [Active f]
rules = forall a. IntMap a -> [a]
IntMap.elems IntMap (Active f)
st_active_set
    ok :: Active f -> Bool
ok Active f
rule = forall a b. Has a b => a -> b
the Active f
rule forall a. Ord a => a -> a -> Bool
< Int -> Depth
Depth Int
cfg_max_cp_depth

data Passive =
  Passive {
    Passive -> Int32
passive_score :: {-# UNPACK #-} !Int32,
    Passive -> Id
passive_rule1 :: {-# UNPACK #-} !Id,
    Passive -> Id
passive_rule2 :: {-# UNPACK #-} !Id,
    Passive -> How
passive_how   :: !How }
  deriving Passive -> Passive -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Passive -> Passive -> Bool
$c/= :: Passive -> Passive -> Bool
== :: Passive -> Passive -> Bool
$c== :: Passive -> Passive -> Bool
Eq

instance Ord Passive where
  compare :: Passive -> Passive -> Ordering
compare = forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Passive -> (Int32, Int, Int, How)
f
    where
      f :: Passive -> (Int32, Int, Int, How)
f Passive{Int32
Id
How
passive_how :: How
passive_rule2 :: Id
passive_rule1 :: Id
passive_score :: Int32
passive_how :: Passive -> How
passive_rule2 :: Passive -> Id
passive_rule1 :: Passive -> Id
passive_score :: Passive -> Int32
..} =
        (Int32
passive_score,
         Int -> Int -> Int
intMax (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
passive_rule1) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
passive_rule2),
         Int -> Int -> Int
intMin (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
passive_rule1) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
passive_rule2),
         How
passive_how)

data Batch =
  Batch {
    Batch -> BatchKind
batch_kind      :: !BatchKind,
    Batch -> Id
batch_rule      :: {-# UNPACK #-} !Id,
    Batch -> Passive
batch_best      :: {-# UNPACK #-} !Passive,
    Batch -> PackedSequence (Int32, Id, How)
batch_rest      :: {-# UNPACK #-} !(PackedSequence (Int32, Id, How)) }

data BatchKind = Rule1 | Rule2 deriving BatchKind -> BatchKind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BatchKind -> BatchKind -> Bool
$c/= :: BatchKind -> BatchKind -> Bool
== :: BatchKind -> BatchKind -> Bool
$c== :: BatchKind -> BatchKind -> Bool
Eq

instance Queue.Batch Batch where
  type Label Batch = Id
  type Entry Batch = Passive

  makeBatch :: Label Batch -> [Entry Batch] -> [Batch]
makeBatch Label Batch
rule [Entry Batch]
ps =
    BatchKind -> [Passive] -> [Batch]
make1 BatchKind
Rule1 [Passive]
ps1 forall a. [a] -> [a] -> [a]
++ BatchKind -> [Passive] -> [Batch]
make1 BatchKind
Rule2 [Passive]
ps2
    where
      ([Passive]
ps1, [Passive]
ps2) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Passive -> Bool
isRule1 [Entry Batch]
ps
      isRule1 :: Passive -> Bool
isRule1 Passive{Int32
Id
How
passive_how :: How
passive_rule2 :: Id
passive_rule1 :: Id
passive_score :: Int32
passive_how :: Passive -> How
passive_rule2 :: Passive -> Id
passive_rule1 :: Passive -> Id
passive_score :: Passive -> Int32
..} = Label Batch
rule forall a. Eq a => a -> a -> Bool
== Id
passive_rule1

      make1 :: BatchKind -> [Passive] -> [Batch]
make1 BatchKind
_ [] = []
      make1 BatchKind
kind (Passive
p:[Passive]
ps) =
        [Batch {
           batch_kind :: BatchKind
batch_kind = BatchKind
kind,
           batch_rule :: Id
batch_rule = Label Batch
rule,
           batch_best :: Passive
batch_best = Passive
p,
           batch_rest :: PackedSequence (Int32, Id, How)
batch_rest = 
             forall a. Serialize a => [a] -> PackedSequence a
PackedSequence.fromList forall a b. (a -> b) -> a -> b
$
               [ (Int32
passive_score, if BatchKind
kind forall a. Eq a => a -> a -> Bool
== BatchKind
Rule1 then Id
passive_rule2 else Id
passive_rule1, How
passive_how)
               | Passive{Int32
Id
How
passive_how :: How
passive_rule1 :: Id
passive_rule2 :: Id
passive_score :: Int32
passive_how :: Passive -> How
passive_rule2 :: Passive -> Id
passive_rule1 :: Passive -> Id
passive_score :: Passive -> Int32
..} <- [Passive]
ps ] }]

  unconsBatch :: Batch -> (Entry Batch, Maybe Batch)
unconsBatch batch :: Batch
batch@Batch{PackedSequence (Int32, Id, How)
Id
BatchKind
Passive
batch_rest :: PackedSequence (Int32, Id, How)
batch_best :: Passive
batch_rule :: Id
batch_kind :: BatchKind
batch_rest :: Batch -> PackedSequence (Int32, Id, How)
batch_best :: Batch -> Passive
batch_rule :: Batch -> Id
batch_kind :: Batch -> BatchKind
..} =
    (Passive
batch_best,
     do ((Int32, Id, How)
p, PackedSequence (Int32, Id, How)
ps) <- forall a.
Serialize a =>
PackedSequence a -> Maybe (a, PackedSequence a)
PackedSequence.uncons PackedSequence (Int32, Id, How)
batch_rest
        forall (m :: * -> *) a. Monad m => a -> m a
return Batch
batch{batch_best :: Passive
batch_best = BatchKind -> (Int32, Id, How) -> Passive
unpack BatchKind
batch_kind (Int32, Id, How)
p, batch_rest :: PackedSequence (Int32, Id, How)
batch_rest = PackedSequence (Int32, Id, How)
ps})
    where
      unpack :: BatchKind -> (Int32, Id, How) -> Passive
unpack BatchKind
Rule1 (Int32
score, Id
rule2, How
how) =
        Int32 -> Id -> Id -> How -> Passive
Passive Int32
score Id
batch_rule Id
rule2 How
how
      unpack BatchKind
Rule2 (Int32
score, Id
rule1, How
how) =
        Int32 -> Id -> Id -> How -> Passive
Passive Int32
score Id
rule1 Id
batch_rule How
how

  batchLabel :: Batch -> Label Batch
batchLabel Batch{PackedSequence (Int32, Id, How)
Id
BatchKind
Passive
batch_rest :: PackedSequence (Int32, Id, How)
batch_best :: Passive
batch_rule :: Id
batch_kind :: BatchKind
batch_rest :: Batch -> PackedSequence (Int32, Id, How)
batch_best :: Batch -> Passive
batch_rule :: Batch -> Id
batch_kind :: Batch -> BatchKind
..} = Id
batch_rule
  batchSize :: Batch -> Int
batchSize Batch{PackedSequence (Int32, Id, How)
Id
BatchKind
Passive
batch_rest :: PackedSequence (Int32, Id, How)
batch_best :: Passive
batch_rule :: Id
batch_kind :: BatchKind
batch_rest :: Batch -> PackedSequence (Int32, Id, How)
batch_best :: Batch -> Passive
batch_rule :: Batch -> Id
batch_kind :: Batch -> BatchKind
..} = Int
1 forall a. Num a => a -> a -> a
+ forall a. PackedSequence a -> Int
PackedSequence.size PackedSequence (Int32, Id, How)
batch_rest

{-# INLINEABLE makePassive #-}
makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive
makePassive :: forall f. Function f => Config f -> Overlap (Active f) f -> Passive
makePassive Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} overlap :: Overlap (Active f) f
overlap@Overlap{Term f
Equation f
How
Active f
overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_top :: forall a f. Overlap a f -> Term f
overlap_how :: forall a f. Overlap a f -> How
overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule1 :: forall a f. Overlap a f -> a
overlap_eqn :: Equation f
overlap_top :: Term f
overlap_how :: How
overlap_rule2 :: Active f
overlap_rule1 :: Active f
..} =
  Passive {
    passive_score :: Int32
passive_score = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall f a. Function f => Config -> Depth -> Overlap a f -> Int
score Config
cfg_critical_pairs Depth
depth Overlap (Active f) f
overlap),
    passive_rule1 :: Id
passive_rule1 = forall f. Active f -> Id
active_id Active f
overlap_rule1,
    passive_rule2 :: Id
passive_rule2 = forall f. Active f -> Id
active_id Active f
overlap_rule2,
    passive_how :: How
passive_how   = How
overlap_how }
  where
    depth :: Depth
depth = forall a. Enum a => a -> a
succ (forall a b. Has a b => a -> b
the Active f
overlap_rule1 forall a. Ord a => a -> a -> a
`max` forall a b. Has a b => a -> b
the Active f
overlap_rule2)

-- | Turn a Passive back into an overlap.
-- Doesn't try to simplify it.
{-# INLINEABLE findPassive #-}
findPassive :: forall f. Function f => State f -> Passive -> Maybe (Overlap (Active f) f)
findPassive :: forall f.
Function f =>
State f -> Passive -> Maybe (Overlap (Active f) f)
findPassive State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Passive{Int32
Id
How
passive_how :: How
passive_rule2 :: Id
passive_rule1 :: Id
passive_score :: Int32
passive_how :: Passive -> How
passive_rule2 :: Passive -> Id
passive_rule1 :: Passive -> Id
passive_score :: Passive -> Int32
..} = do
  Active f
rule1 <- forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
passive_rule1) IntMap (Active f)
st_active_set
  Active f
rule2 <- forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
passive_rule2) IntMap (Active f)
st_active_set
  forall a f.
How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt How
passive_how Active f
rule1 Active f
rule2
    (forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding (forall a b. Has a b => a -> b
the Active f
rule2 :: Rule f) (forall a b. Has a b => a -> b
the Active f
rule1)) (forall a b. Has a b => a -> b
the Active f
rule2)

-- | Renormalise a queued Passive.
{-# INLINEABLE simplifyPassive #-}
simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe (Passive)
simplifyPassive :: forall f.
Function f =>
Config f -> State f -> Passive -> Maybe Passive
simplifyPassive Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Passive
passive = do
  Overlap (Active f) f
overlap <- forall f.
Function f =>
State f -> Passive -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive
passive
  Overlap (Active f) f
overlap <- forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap
  let r1 :: Active f
r1 = forall a f. Overlap a f -> a
overlap_rule1 Overlap (Active f) f
overlap
      r2 :: Active f
r2 = forall a f. Overlap a f -> a
overlap_rule2 Overlap (Active f) f
overlap
  forall (m :: * -> *) a. Monad m => a -> m a
return Passive
passive {
    passive_score :: Int32
passive_score = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$
      forall a b. (Integral a, Num b) => a -> b
fromIntegral (Passive -> Int32
passive_score Passive
passive) Int -> Int -> Int
`intMin`
      -- XXX factor out depth calculation
      forall f a. Function f => Config -> Depth -> Overlap a f -> Int
score Config
cfg_critical_pairs (forall a. Enum a => a -> a
succ (forall a b. Has a b => a -> b
the Active f
r1 forall a. Ord a => a -> a -> a
`max` forall a b. Has a b => a -> b
the Active f
r2)) Overlap (Active f) f
overlap }

-- | Check if we should renormalise the queue.
{-# INLINEABLE shouldSimplifyQueue #-}
shouldSimplifyQueue :: Function f => Config f -> State f -> Bool
shouldSimplifyQueue :: forall f. Function f => Config f -> State f -> Bool
shouldSimplifyQueue Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter forall a. Maybe a -> Bool
isNothing (forall a. Sample a -> [a]
sampleValue Sample (Maybe (Overlap (Active f) f))
st_cp_sample)) forall a. Num a => a -> a -> a
* Int
100 forall a. Ord a => a -> a -> Bool
>= Int
cfg_renormalise_threshold forall a. Num a => a -> a -> a
* Int
cfg_cp_sample_size

-- | Renormalise the entire queue.
{-# INLINEABLE simplifyQueue #-}
simplifyQueue :: Function f => Config f -> State f -> State f
simplifyQueue :: forall f. Function f => Config f -> State f -> State f
simplifyQueue Config f
config State f
state =
  forall f. Function f => Config f -> State f -> State f
resetSample Config f
config State f
state { st_queue :: Queue Batch
st_queue = Queue Batch -> Queue Batch
simp (forall f. State f -> Queue Batch
st_queue State f
state) }
  where
    simp :: Queue Batch -> Queue Batch
simp =
      forall a.
Batch a =>
(Entry a -> Maybe (Entry a)) -> Queue a -> Queue a
Queue.mapMaybe (forall f.
Function f =>
Config f -> State f -> Passive -> Maybe Passive
simplifyPassive Config f
config State f
state)

-- | Enqueue a set of critical pairs.
{-# INLINEABLE enqueue #-}
enqueue :: Function f => State f -> Id -> [Passive] -> State f
enqueue :: forall f. Function f => State f -> Id -> [Passive] -> State f
enqueue State f
state Id
rule [Passive]
passives =
  State f
state { st_queue :: Queue Batch
st_queue = forall a. Batch a => Label a -> [Entry a] -> Queue a -> Queue a
Queue.insert Id
rule [Passive]
passives (forall f. State f -> Queue Batch
st_queue State f
state) }

-- | Dequeue a critical pair.
--
-- Also takes care of:
--
--   * removing any orphans from the head of the queue
--   * ignoring CPs that are too big
{-# INLINEABLE dequeue #-}
dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
dequeue :: forall f.
Function f =>
Config f
-> State f
-> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
dequeue Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  case Int64
-> Queue Batch
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Batch)
deq Int64
0 Queue Batch
st_queue of
    -- Explicitly make the queue empty, in case it e.g. contained a
    -- lot of orphans
    Maybe
  ((Info, CriticalPair f, Active f, Active f), Int64, Queue Batch)
Nothing -> (forall a. Maybe a
Nothing, State f
state { st_queue :: Queue Batch
st_queue = forall a. Queue a
Queue.empty })
    Just ((Info, CriticalPair f, Active f, Active f)
overlap, Int64
n, Queue Batch
queue) ->
      (forall a. a -> Maybe a
Just (Info, CriticalPair f, Active f, Active f)
overlap,
       State f
state { st_queue :: Queue Batch
st_queue = Queue Batch
queue, st_considered :: Int64
st_considered = Int64
st_considered forall a. Num a => a -> a -> a
+ Int64
n })
  where
    deq :: Int64
-> Queue Batch
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Batch)
deq !Int64
n Queue Batch
queue = do
      let ok :: Id -> Bool
ok Id
id = forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
id forall a. Int -> IntMap a -> Bool
`IntMap.member` IntMap (Active f)
st_active_set
      (Passive
passive, Queue Batch
queue) <- forall a.
Batch a =>
(Label a -> Bool) -> Queue a -> Maybe (Entry a, Queue a)
Queue.removeMinFilter Id -> Bool
ok Queue Batch
queue
      case forall f.
Function f =>
State f -> Passive -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive
passive of
        Just (overlap :: Overlap (Active f) f
overlap@Overlap{overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_eqn = Term f
t :=: Term f
u, overlap_rule1 :: forall a f. Overlap a f -> a
overlap_rule1 = Active f
rule1, overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule2 = Active f
rule2})
          | forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe (Term f -> Bool)
cfg_accept_term forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f
t),
            forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe (Term f -> Bool)
cfg_accept_term forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f
u),
            CriticalPair f
cp <- forall f a.
(Function f, Has a (Rule f)) =>
Overlap a f -> CriticalPair f
makeCriticalPair Overlap (Active f) f
overlap ->
              forall (m :: * -> *) a. Monad m => a -> m a
return ((Info -> Info -> Info
combineInfo (forall f. Active f -> Info
active_info Active f
rule1) (forall f. Active f -> Info
active_info Active f
rule2), CriticalPair f
cp, Active f
rule1, Active f
rule2), Int64
nforall a. Num a => a -> a -> a
+Int64
1, Queue Batch
queue)
        Maybe (Overlap (Active f) f)
_ -> Int64
-> Queue Batch
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Batch)
deq (Int64
nforall a. Num a => a -> a -> a
+Int64
1) Queue Batch
queue

    combineInfo :: Info -> Info -> Info
combineInfo Info
i1 Info
i2 =
      Info {
        -- XXX factor out depth calculation
        info_depth :: Depth
info_depth = forall a. Enum a => a -> a
succ (forall a. Ord a => a -> a -> a
max (Info -> Depth
info_depth Info
i1) (Info -> Depth
info_depth Info
i2)),
        info_max :: IntSet
info_max = IntSet -> IntSet -> IntSet
IntSet.union (Info -> IntSet
info_max Info
i1) (Info -> IntSet
info_max Info
i2) }

----------------------------------------------------------------------
-- * Active rewrite rules.
----------------------------------------------------------------------

data Active f =
  Active {
    forall f. Active f -> Id
active_id    :: {-# UNPACK #-} !Id,
    forall f. Active f -> Info
active_info  :: {-# UNPACK #-} !Info,
    forall f. Active f -> Rule f
active_rule  :: {-# UNPACK #-} !(Rule f),
    forall f. Active f -> Maybe (Term f)
active_top   :: !(Maybe (Term f)),
    forall f. Active f -> Proof f
active_proof :: {-# UNPACK #-} !(Proof f),
    -- A model in which the rule is false (used when reorienting)
    forall f. Active f -> Model f
active_model :: !(Model f),
    forall f. Active f -> Positions2 f
active_positions :: !(Positions2 f) }

active_cp :: Active f -> CriticalPair f
active_cp :: forall f. Active f -> CriticalPair f
active_cp Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
  CriticalPair {
    cp_eqn :: Equation f
cp_eqn = forall f. Rule f -> Equation f
unorient Rule f
active_rule,
    cp_top :: Maybe (Term f)
cp_top = Maybe (Term f)
active_top,
    cp_proof :: Derivation f
cp_proof = forall f. Proof f -> Derivation f
derivation Proof f
active_proof }

activeRules :: Active f -> [Rule f]
activeRules :: forall f. Active f -> [Rule f]
activeRules Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
  case Positions2 f
active_positions of
    ForwardsPos Positions f
_ -> [Rule f
active_rule]
    BothPos Positions f
_ Positions f
_ -> [Rule f
active_rule, forall f. Rule f -> Rule f
backwards Rule f
active_rule]

data Info =
  Info {
    Info -> Depth
info_depth :: {-# UNPACK #-} !Depth,
    Info -> IntSet
info_max   :: !IntSet }

instance Eq (Active f) where
  == :: Active f -> Active f -> Bool
(==) = forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall f. Active f -> Id
active_id

instance Function f => Pretty (Active f) where
  pPrint :: Active f -> Doc
pPrint Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
    forall a. Pretty a => a -> Doc
pPrint Id
active_id Doc -> Doc -> Doc
<#> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pPrint (forall a. Symbolic a => a -> a
canonicalise Rule f
active_rule)

instance Has (Active f) Id where the :: Active f -> Id
the = forall f. Active f -> Id
active_id
instance Has (Active f) Depth where the :: Active f -> Depth
the = Info -> Depth
info_depth forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Active f -> Info
active_info
instance f ~ g => Has (Active f) (Rule g) where the :: Active f -> Rule g
the = forall f. Active f -> Rule f
active_rule
instance f ~ g => Has (Active f) (Positions2 g) where the :: Active f -> Positions2 g
the = forall f. Active f -> Positions2 f
active_positions

-- Add a new active.
{-# INLINEABLE addActive #-}
addActive :: Function f => Config f -> State f -> (Id -> Active f) -> State f
addActive :: forall f.
Function f =>
Config f -> State f -> (Id -> Active f) -> State f
addActive Config f
config state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Id -> Active f
active0 =
  let
    active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} = Id -> Active f
active0 Id
st_next_active
    state' :: State f
state' =
      forall f. PrettyTerm f => Message f -> State f -> State f
message (forall f. Active f -> Message f
NewActive Active f
active) forall a b. (a -> b) -> a -> b
$
      forall f. Function f => State f -> Active f -> State f
addActiveOnly State f
state{st_next_active :: Id
st_next_active = Id
st_next_activeforall a. Num a => a -> a -> a
+Id
1} Active f
active
  in if forall a f.
(Has a (Rule f), Function f) =>
(Index f (Equation f), Index f (Rule f))
-> RuleIndex f a -> Equation f -> Bool
subsumed (Index f (Equation f)
st_joinable, Index f (Rule f)
st_complete) RuleIndex f (Rule f)
st_rules (forall f. Rule f -> Equation f
unorient Rule f
active_rule) then
    State f
state
  else
    forall f. Function f => Config f -> State f -> State f
normaliseGoals Config f
config forall a b. (a -> b) -> a -> b
$
    State f -> Active f -> State f
enqueueRule State f
state' Active f
active
  where
    enqueueRule :: State f -> Active f -> State f
enqueueRule State f
state Active f
rule =
      forall f. Function f => Int -> [Passive] -> State f -> State f
sample (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Passive]
passives) [Passive]
passives forall a b. (a -> b) -> a -> b
$
      forall f. Function f => State f -> Id -> [Passive] -> State f
enqueue State f
state (forall a b. Has a b => a -> b
the Active f
rule) [Passive]
passives
      where
        passives :: [Passive]
passives = forall f.
Function f =>
Config f -> State f -> Active f -> [Passive]
makePassives Config f
config State f
state Active f
rule

-- Update the list of sampled critical pairs.
{-# INLINEABLE sample #-}
sample :: Function f => Int -> [Passive] -> State f -> State f
sample :: forall f. Function f => Int -> [Passive] -> State f -> State f
sample Int
m [Passive]
passives state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  State f
state{st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = forall a. (Int, [a]) -> Sample a -> Sample a
addSample (Int
m, forall a b. (a -> b) -> [a] -> [b]
map Passive -> Maybe (Overlap (Active f) f)
find [Passive]
passives) Sample (Maybe (Overlap (Active f) f))
st_cp_sample}
  where
    find :: Passive -> Maybe (Overlap (Active f) f)
find Passive
passive = do
      Overlap (Active f) f
overlap <- forall f.
Function f =>
State f -> Passive -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive
passive
      forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap

-- Reset the list of sampled critical pairs.
{-# INLINEABLE resetSample #-}
resetSample :: Function f => Config f -> State f -> State f
resetSample :: forall f. Function f => Config f -> State f -> State f
resetSample Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {a} {f}.
(Entry a ~ Passive, Ordered f, Minimal f, PrettyTerm f,
 EqualsBonus f, Labelled f, Batch a) =>
State f -> a -> State f
sample1 State f
state' (forall a. Queue a -> [a]
Queue.toBatches Queue Batch
st_queue)
  where
    state' :: State f
state' =
      State f
state {
        st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = forall a. Int -> Sample a
emptySample Int
cfg_cp_sample_size }

    sample1 :: State f -> a -> State f
sample1 State f
state a
batch = forall f. Function f => Int -> [Passive] -> State f -> State f
sample (forall a. Batch a => a -> Int
Queue.batchSize a
batch) (forall a. Batch a => a -> [Entry a]
Queue.unbatch a
batch) State f
state

-- Simplify the sampled critical pairs.
-- (A sampled critical pair is replaced with Nothing if it can be
-- simplified.)
{-# INLINEABLE simplifySample #-}
simplifySample :: Function f => State f -> State f
simplifySample :: forall f. Function f => State f -> State f
simplifySample state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  State f
state{st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = forall a b. (a -> b) -> Sample a -> Sample b
mapSample (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Overlap (Active f) f -> Maybe (Overlap (Active f) f)
simp) Sample (Maybe (Overlap (Active f) f))
st_cp_sample}
  where
    simp :: Overlap (Active f) f -> Maybe (Overlap (Active f) f)
simp Overlap (Active f) f
overlap = do
      Overlap (Active f) f
overlap' <- forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a f. Overlap a f -> Equation f
overlap_eqn Overlap (Active f) f
overlap forall a. Eq a => a -> a -> Bool
== forall a f. Overlap a f -> Equation f
overlap_eqn Overlap (Active f) f
overlap')
      forall (m :: * -> *) a. Monad m => a -> m a
return Overlap (Active f) f
overlap

-- Add an active without generating critical pairs. Used in interreduction.
{-# INLINEABLE addActiveOnly #-}
addActiveOnly :: Function f => State f -> Active f -> State f
addActiveOnly :: forall f. Function f => State f -> Active f -> State f
addActiveOnly state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
  State f
state {
    st_rules :: RuleIndex f (Rule f)
st_rules = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {f}. RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
insertRule RuleIndex f (Rule f)
st_rules (forall f. Active f -> [Rule f]
activeRules Active f
active),
    st_active_set :: IntMap (Active f)
st_active_set = forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
active_id) Active f
active IntMap (Active f)
st_active_set }
  where
    insertRule :: RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
insertRule RuleIndex f (Rule f)
rules Rule f
rule =
      forall f a.
(Symbolic a, ConstantOf a ~ f, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
RuleIndex.insert (forall f. Rule f -> Term f
lhs Rule f
rule) Rule f
rule RuleIndex f (Rule f)
rules

-- Delete an active. Used in interreduction, not suitable for general use.
{-# INLINE deleteActive #-}
deleteActive :: Function f => State f -> Active f -> State f
deleteActive :: forall f. Function f => State f -> Active f -> State f
deleteActive state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
  State f
state {
    st_rules :: RuleIndex f (Rule f)
st_rules = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall {f}. RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
deleteRule RuleIndex f (Rule f)
st_rules (forall f. Active f -> [Rule f]
activeRules Active f
active),
    st_active_set :: IntMap (Active f)
st_active_set = forall a. Int -> IntMap a -> IntMap a
IntMap.delete (forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
active_id) IntMap (Active f)
st_active_set }
  where
    deleteRule :: RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
deleteRule RuleIndex f (Rule f)
rules Rule f
rule =
      forall f a.
(Symbolic a, ConstantOf a ~ f, Eq a, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
RuleIndex.delete (forall f. Rule f -> Term f
lhs Rule f
rule) Rule f
rule RuleIndex f (Rule f)
rules

-- Try to join a critical pair.
{-# INLINEABLE consider #-}
consider :: Function f => Config f -> State f -> Info -> CriticalPair f -> State f
consider :: forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
info CriticalPair f
cp =
  forall f.
Function f =>
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing (forall f. State f -> RuleIndex f (Rule f)
st_rules State f
state) Config f
config State f
state Info
info CriticalPair f
cp

-- Try to join a critical pair, but using a different set of critical
-- pairs for normalisation.
{-# INLINEABLE considerUsing #-}
considerUsing ::
  Function f =>
  RuleIndex f (Rule f) -> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing :: forall f.
Function f =>
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing RuleIndex f (Rule f)
rules config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Info
info CriticalPair f
cp0 =
  forall symbol a. symbol -> a -> a
stamp String
"consider critical pair" forall a b. (a -> b) -> a -> b
$
  -- Important to canonicalise the rule so that we don't get
  -- bigger and bigger variable indices over time
  let cp :: CriticalPair f
cp = forall a. Symbolic a => a -> a
canonicalise CriticalPair f
cp0 in
  case forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> CriticalPair f
-> Either
     (CriticalPair f, Model f)
     (Maybe (CriticalPair f), [CriticalPair f])
joinCriticalPair Config
cfg_join (Index f (Equation f)
st_joinable, Index f (Rule f)
st_complete) RuleIndex f (Rule f)
rules forall a. Maybe a
Nothing CriticalPair f
cp of
    Right (Maybe (CriticalPair f)
mcp, [CriticalPair f]
cps) ->
      let
        state' :: State f
state' = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> forall f.
Function f =>
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing RuleIndex f (Rule f)
rules Config f
config State f
state Info
info CriticalPair f
cp) State f
state [CriticalPair f]
cps
      in case Maybe (CriticalPair f)
mcp of
        Just CriticalPair f
cp -> forall f. Function f => State f -> Equation f -> State f
addJoinable State f
state' (forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp)
        Maybe (CriticalPair f)
Nothing -> State f
state'

    Left (CriticalPair f
cp, Model f
model) ->
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> forall f.
Function f =>
Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addCP Config f
config Model f
model State f
state Info
info CriticalPair f
cp) State f
state (forall f. Function f => CriticalPair f -> [CriticalPair f]
split CriticalPair f
cp)

{-# INLINEABLE addCP #-}
addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addCP :: forall f.
Function f =>
Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addCP Config f
config Model f
model state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Info
info CriticalPair{Maybe (Term f)
Equation f
Derivation f
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
  let
    pf :: Proof f
pf = forall f. Function f => Derivation f -> Proof f
certify Derivation f
cp_proof
    rule :: Rule f
rule = forall f. Function f => Equation f -> Proof f -> Rule f
orient Equation f
cp_eqn Proof f
pf
  in
  forall f.
Function f =>
Config f -> State f -> (Id -> Active f) -> State f
addActive Config f
config State f
state forall a b. (a -> b) -> a -> b
$ \Id
n ->
  Active {
    active_id :: Id
active_id = Id
n,
    active_info :: Info
active_info = Info
info,
    active_rule :: Rule f
active_rule = Rule f
rule,
    active_model :: Model f
active_model = Model f
model,
    active_top :: Maybe (Term f)
active_top = Maybe (Term f)
cp_top,
    active_proof :: Proof f
active_proof = Proof f
pf,
    active_positions :: Positions2 f
active_positions = forall f. Rule f -> Positions2 f
positionsRule Rule f
rule }

-- Add a new equation.
{-# INLINEABLE addAxiom #-}
addAxiom :: Function f => Config f -> State f -> Axiom f -> State f
addAxiom :: forall f. Function f => Config f -> State f -> Axiom f -> State f
addAxiom Config f
config State f
state Axiom f
axiom =
  forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state
    Info { info_depth :: Depth
info_depth = Depth
0, info_max :: IntSet
info_max = [Int] -> IntSet
IntSet.fromList [forall f. Axiom f -> Int
axiom_number Axiom f
axiom | forall f. Config f -> Bool
cfg_complete_subsets Config f
config] }
    CriticalPair {
      cp_eqn :: Equation f
cp_eqn = forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom,
      cp_top :: Maybe (Term f)
cp_top = forall a. Maybe a
Nothing,
      cp_proof :: Derivation f
cp_proof = forall f. Axiom f -> Derivation f
Proof.axiom Axiom f
axiom }

-- Record an equation as being joinable.
{-# INLINEABLE addJoinable #-}
addJoinable :: Function f => State f -> Equation f -> State f
addJoinable :: forall f. Function f => State f -> Equation f -> State f
addJoinable State f
state eqn :: Equation f
eqn@(Term f
t :=: Term f
u) =
  forall f. PrettyTerm f => Message f -> State f -> State f
message (forall f. Equation f -> Message f
NewEquation Equation f
eqn) forall a b. (a -> b) -> a -> b
$
  State f
state {
    st_joinable :: Index f (Equation f)
st_joinable =
      forall a f.
(Symbolic a, ConstantOf a ~ f) =>
Term f -> a -> Index f a -> Index f a
Index.insert Term f
t (Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u) forall a b. (a -> b) -> a -> b
$
      forall a f.
(Symbolic a, ConstantOf a ~ f) =>
Term f -> a -> Index f a -> Index f a
Index.insert Term f
u (Term f
u forall f. Term f -> Term f -> Equation f
:=: Term f
t) (forall f. State f -> Index f (Equation f)
st_joinable State f
state) }

-- Find a confluent subset of the rules.
{-# INLINEABLE checkCompleteness #-}
checkCompleteness :: Function f => Config f -> State f -> State f
checkCompleteness :: forall f. Function f => Config f -> State f -> State f
checkCompleteness Config f
_ state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} | Id
st_simplified_at forall a. Eq a => a -> a -> Bool
== Id
st_next_active = State f
state
checkCompleteness Config f
_config State f
state =
  State f
state { st_not_complete :: IntSet
st_not_complete = IntSet
excluded,
          st_complete :: Index f (Rule f)
st_complete = forall a f.
(Symbolic a, ConstantOf a ~ f) =>
(a -> Term f) -> [a] -> Index f a
Index.fromListWith forall f. Rule f -> Term f
lhs [Rule f]
rules }
  where
    maxSet :: IntSet -> Int
maxSet IntSet
s = if IntSet -> Bool
IntSet.null IntSet
s then forall a. Bounded a => a
minBound else IntSet -> Int
IntSet.findMax IntSet
s
    maxN :: Int
maxN = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [IntSet -> Int
maxSet (Info -> IntSet
info_max (forall f. Active f -> Info
active_info Active f
r)) | Active f
r <- forall a. IntMap a -> [a]
IntMap.elems (forall f. State f -> IntMap (Active f)
st_active_set State f
state)]
    excluded :: IntSet
excluded = IntSet -> IntSet
go IntSet
IntSet.empty
    go :: IntSet -> IntSet
go IntSet
excl
      | Int
m forall a. Ord a => a -> a -> Bool
> Int
maxN = IntSet
excl
      | Bool
otherwise = IntSet -> IntSet
go (Int -> IntSet -> IntSet
IntSet.insert Int
m IntSet
excl)
      where
        m :: Int
m = IntSet -> Int
bound IntSet
excl

    bound :: IntSet -> Int
bound IntSet
excl = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (IntSet -> Passive -> Int
passiveMax IntSet
excl) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Batch a => Queue a -> [Entry a]
Queue.toList forall a b. (a -> b) -> a -> b
$ forall f. State f -> Queue Batch
st_queue State f
state

    passiveMax :: IntSet -> Passive -> Int
passiveMax IntSet
excl Passive
p = forall a. a -> Maybe a -> a
fromMaybe forall a. Bounded a => a
maxBound forall a b. (a -> b) -> a -> b
$ do
      Overlap{overlap_rule1 :: forall a f. Overlap a f -> a
overlap_rule1 = Active f
r1, overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule2 = Active f
r2} <- forall f.
Function f =>
State f -> Passive -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive
p
      let s :: IntSet
s = Info -> IntSet
info_max (forall f. Active f -> Info
active_info Active f
r1) IntSet -> IntSet -> IntSet
`IntSet.union` Info -> IntSet
info_max (forall f. Active f -> Info
active_info Active f
r2)
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard (IntSet
s IntSet -> IntSet -> Bool
`IntSet.disjoint` IntSet
excl)
      (Int
n, IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.maxView IntSet
s
      forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
    rules :: [Rule f]
rules = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall f. Active f -> [Rule f]
activeRules (forall a. (a -> Bool) -> [a] -> [a]
filter Active f -> Bool
ok (forall a. IntMap a -> [a]
IntMap.elems (forall f. State f -> IntMap (Active f)
st_active_set State f
state)))
    ok :: Active f -> Bool
ok Active f
r = Info -> IntSet
info_max (forall f. Active f -> Info
active_info Active f
r) IntSet -> IntSet -> Bool
`IntSet.disjoint` IntSet
excluded

-- Assume that all rules form a confluent rewrite system.
{-# INLINEABLE assumeComplete #-}
assumeComplete :: Function f => State f -> State f
assumeComplete :: forall f. Function f => State f -> State f
assumeComplete State f
state =
  State f
state { st_not_complete :: IntSet
st_not_complete = IntSet
IntSet.empty,
          st_complete :: Index f (Rule f)
st_complete = forall a f.
(Symbolic a, ConstantOf a ~ f) =>
(a -> Term f) -> [a] -> Index f a
Index.fromListWith forall f. Rule f -> Term f
lhs (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall f. Active f -> [Rule f]
activeRules (forall a. IntMap a -> [a]
IntMap.elems (forall f. State f -> IntMap (Active f)
st_active_set State f
state))) }

-- For goal terms we store the set of all their normal forms.
-- Name and number are for information only.
data Goal f =
  Goal {
    forall f. Goal f -> String
goal_name         :: String,
    forall f. Goal f -> Int
goal_number       :: Int,
    forall f. Goal f -> Equation f
goal_eqn          :: Equation f,
    forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f),
    forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_rhs :: Map (Term f) (Derivation f),
    forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs          :: Map (Term f) (Term f, Reduction f),
    forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_rhs          :: Map (Term f) (Term f, Reduction f) }
  deriving Int -> Goal f -> ShowS
forall f. (Labelled f, Show f) => Int -> Goal f -> ShowS
forall f. (Labelled f, Show f) => [Goal f] -> ShowS
forall f. (Labelled f, Show f) => Goal f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Goal f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [Goal f] -> ShowS
show :: Goal f -> String
$cshow :: forall f. (Labelled f, Show f) => Goal f -> String
showsPrec :: Int -> Goal f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> Goal f -> ShowS
Show

-- Add a new goal.
{-# INLINEABLE addGoal #-}
addGoal :: Function f => Config f -> State f -> Goal f -> State f
addGoal :: forall f. Function f => Config f -> State f -> Goal f -> State f
addGoal Config f
config state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Goal f
goal =
  forall f. Function f => Config f -> State f -> State f
normaliseGoals Config f
config State f
state { st_goals :: [Goal f]
st_goals = Goal f
goalforall a. a -> [a] -> [a]
:[Goal f]
st_goals }

-- Normalise all goals.
{-# INLINEABLE normaliseGoals #-}
normaliseGoals :: Function f => Config f -> State f -> State f
normaliseGoals :: forall f. Function f => Config f -> State f -> State f
normaliseGoals Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
  State f
state {
    st_goals :: [Goal f]
st_goals =
      forall a b. (a -> b) -> [a] -> [b]
map (forall {f}.
(Map (Term f) (Term f, Reduction f)
 -> Map (Term f) (Term f, Reduction f))
-> Goal f -> Goal f
goalMap (Strategy f
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
nf (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite forall f. Function f => Rule f -> Subst f -> Bool
reduces (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)))) [Goal f]
st_goals }
  where
    goalMap :: (Map (Term f) (Term f, Reduction f)
 -> Map (Term f) (Term f, Reduction f))
-> Goal f -> Goal f
goalMap Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
f goal :: Goal f
goal@Goal{Int
String
Map (Term f) (Term f, Reduction f)
Map (Term f) (Derivation f)
Equation f
goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} =
      Goal f
goal { goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_lhs = Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
f Map (Term f) (Term f, Reduction f)
goal_lhs, goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_rhs = Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
f Map (Term f) (Term f, Reduction f)
goal_rhs }
    nf :: Strategy f
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
nf Strategy f
reduce Map (Term f) (Term f, Reduction f)
goals
      | Bool
cfg_set_join_goals =
        let pair :: (Term f, Reduction f) -> (Term f, Reduction f)
pair (Term f
t, Reduction f
red) = (forall a b. (a, b) -> a
fst (Map (Term f) (Term f, Reduction f)
goals forall k a. Ord k => Map k a -> k -> a
Map.! Term f
t), Reduction f
red) in
        forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> (Term f, Reduction f)
pair forall a b. (a -> b) -> a -> b
$ forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
Rule.normalForms Strategy f
reduce (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a b. (a, b) -> b
snd Map (Term f) (Term f, Reduction f)
goals)
      | Bool
otherwise =
        forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$
          [ (forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
q, (Term f
u, Reduction f
r forall f. Reduction f -> Reduction f -> Reduction f
`trans` Reduction f
q))
          | (Term f
t, (Term f
u, Reduction f
r)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Term f, Reduction f)
goals,
            let q :: Reduction f
q = forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
Rule.normaliseWith (forall a b. a -> b -> a
const Bool
True) Strategy f
reduce Term f
t ]

-- Recompute all normal forms of all goals. Starts from the original goal term.
-- Different from normalising all goals, because there may be an intermediate
-- term on one of the reduction paths which we can now rewrite in a different
-- way.
{-# INLINEABLE recomputeGoals #-}
recomputeGoals :: Function f => Config f -> State f -> State f
recomputeGoals :: forall f. Function f => Config f -> State f -> State f
recomputeGoals Config f
config State f
state =
  -- Make this strict so that newTask can time it correctly
  forall {a}. [a] -> ()
forceList (forall a b. (a -> b) -> [a] -> [b]
map forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs (forall f. State f -> [Goal f]
st_goals State f
state')) seq :: forall a b. a -> b -> b
`seq`
  forall {a}. [a] -> ()
forceList (forall a b. (a -> b) -> [a] -> [b]
map forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_rhs (forall f. State f -> [Goal f]
st_goals State f
state')) seq :: forall a b. a -> b -> b
`seq`
  State f
state'
  where
    state' :: State f
state' =
      forall f. Function f => Config f -> State f -> State f
normaliseGoals Config f
config (State f
state { st_goals :: [Goal f]
st_goals = forall a b. (a -> b) -> [a] -> [b]
map forall f. Goal f -> Goal f
resetGoal (forall f. State f -> [Goal f]
st_goals State f
state) })

    forceList :: [a] -> ()
forceList [] = ()
    forceList (a
x:[a]
xs) = a
x seq :: forall a b. a -> b -> b
`seq` [a] -> ()
forceList [a]
xs

resetGoal :: Goal f -> Goal f
resetGoal :: forall f. Goal f -> Goal f
resetGoal goal :: Goal f
goal@Goal{Int
String
Map (Term f) (Term f, Reduction f)
Map (Term f) (Derivation f)
Equation f
goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} =
  Goal f
goal { goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_lhs = forall {a} {a} {a}. Map a a -> Map a (a, [a])
expansions Map (Term f) (Derivation f)
goal_expanded_lhs,
         goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_rhs = forall {a} {a} {a}. Map a a -> Map a (a, [a])
expansions Map (Term f) (Derivation f)
goal_expanded_rhs }
  where
    expansions :: Map a a -> Map a (a, [a])
expansions Map a a
m =
      forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\a
t a
_ -> (a
t, [])) Map a a
m

-- Rewrite goal terms backwards using rewrite rules.
{-# INLINEABLE rewriteGoalsBackwards #-}
rewriteGoalsBackwards :: Function f => State f -> State f
rewriteGoalsBackwards :: forall f. Function f => State f -> State f
rewriteGoalsBackwards State f
state =
  State f
state { st_goals :: [Goal f]
st_goals = forall a b. (a -> b) -> [a] -> [b]
map Goal f -> Goal f
backwardsGoal (forall f. State f -> [Goal f]
st_goals State f
state) }
  where
    backwardsGoal :: Goal f -> Goal f
backwardsGoal goal :: Goal f
goal@Goal{Int
String
Map (Term f) (Term f, Reduction f)
Map (Term f) (Derivation f)
Equation f
goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} =
      forall f. Goal f -> Goal f
resetGoal Goal f
goal {
        goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_expanded_lhs = Map (Term f) (Derivation f) -> Map (Term f) (Derivation f)
backwardsMap Map (Term f) (Derivation f)
goal_expanded_lhs,
        goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_rhs = Map (Term f) (Derivation f) -> Map (Term f) (Derivation f)
backwardsMap Map (Term f) (Derivation f)
goal_expanded_rhs }
    backwardsMap :: Map (Term f) (Derivation f) -> Map (Term f) (Derivation f)
backwardsMap Map (Term f) (Derivation f)
m =
      forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$
        forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Derivation f)
m forall a. [a] -> [a] -> [a]
++
        [ (forall f. Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
r, Derivation f
p forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` Derivation f
q)
        | (Term f
t, Derivation f
p) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Derivation f)
m,
          Rule f
r <- Term f -> Reduction f
backwardsTerm Term f
t,
          let q :: Derivation f
q = forall f. Function f => Term f -> Rule f -> Derivation f
ruleProof Term f
t Rule f
r ]
    backwardsTerm :: Term f -> Reduction f
backwardsTerm Term f
t = do
      Rule f
rule <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. Has a b => a -> b
the (forall f a. Index f a -> [a]
Index.elems (forall f a. RuleIndex f a -> Index f a
RuleIndex.index_all (forall f. State f -> RuleIndex f (Rule f)
st_rules State f
state)))
      forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall a. Ord a => [a] -> [a]
usort (forall a. Symbolic a => a -> [Var]
vars (forall f. Rule f -> Term f
lhs Rule f
rule)) forall a. Eq a => a -> a -> Bool
== forall a. Ord a => [a] -> [a]
usort (forall a. Symbolic a => a -> [Var]
vars (forall f. Rule f -> Term f
rhs Rule f
rule)))
      [Rule f
r] <- forall f. Strategy f -> Strategy f
anywhere (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule (\Rule f
_ Subst f
_ -> Bool
True) (forall f. Rule f -> Rule f
backwards Rule f
rule)) Term f
t
      forall (m :: * -> *) a. Monad m => a -> m a
return Rule f
r

-- Create a goal.
{-# INLINE goal #-}
goal :: Int -> String -> Equation f -> Goal f
goal :: forall f. Int -> String -> Equation f -> Goal f
goal Int
n String
name (Term f
t :=: Term f
u) =
  Goal {
    goal_name :: String
goal_name = String
name,
    goal_number :: Int
goal_number = Int
n,
    goal_eqn :: Equation f
goal_eqn = Term f
t forall f. Term f -> Term f -> Equation f
:=: Term f
u,
    goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_expanded_lhs = forall k a. k -> a -> Map k a
Map.singleton Term f
t (forall f. Term f -> Derivation f
Proof.Refl Term f
t),
    goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_rhs = forall k a. k -> a -> Map k a
Map.singleton Term f
u (forall f. Term f -> Derivation f
Proof.Refl Term f
u),
    goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_lhs = forall k a. k -> a -> Map k a
Map.singleton Term f
t (Term f
t, []),
    goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_rhs = forall k a. k -> a -> Map k a
Map.singleton Term f
u (Term f
u, []) }

----------------------------------------------------------------------
-- Interreduction.
----------------------------------------------------------------------

-- Simplify all rules.
{-# INLINEABLE interreduce #-}
interreduce :: Function f => Config f -> State f -> State f
interreduce :: forall f. Function f => Config f -> State f -> State f
interreduce Config f
_ state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} | Id
st_simplified_at forall a. Eq a => a -> a -> Bool
== Id
st_next_active = State f
state
interreduce config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state =
  let
    state' :: State f
state' =
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall f. Function f => Config f -> State f -> Active f -> State f
interreduce1 Config f
config)
        -- Clear out st_joinable, since we don't know which
        -- equations have made use of each active.
        State f
state { st_joinable :: Index f (Equation f)
st_joinable = forall f a. Index f a
Index.empty, st_complete :: Index f (Rule f)
st_complete = forall f a. Index f a
Index.empty }
        (forall a. IntMap a -> [a]
IntMap.elems (forall f. State f -> IntMap (Active f)
st_active_set State f
state))
    in State f
state' { st_joinable :: Index f (Equation f)
st_joinable = forall f. State f -> Index f (Equation f)
st_joinable State f
state, st_complete :: Index f (Rule f)
st_complete = forall f. State f -> Index f (Rule f)
st_complete State f
state, st_simplified_at :: Id
st_simplified_at = forall f. State f -> Id
st_next_active State f
state' }

{-# INLINEABLE interreduce1 #-}
interreduce1 :: Function f => Config f -> State f -> Active f -> State f
interreduce1 :: forall f. Function f => Config f -> State f -> Active f -> State f
interreduce1 config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
  -- Exclude the active from the rewrite rules when testing
  -- joinability, otherwise it will be trivially joinable.
  case
    forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> CriticalPair f
-> Either
     (CriticalPair f, Model f)
     (Maybe (CriticalPair f), [CriticalPair f])
joinCriticalPair Config
cfg_join
      (forall f a. Index f a
Index.empty, forall f a. Index f a
Index.empty) -- (st_joinable state)
      (forall f. State f -> RuleIndex f (Rule f)
st_rules (forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active))
      (forall a. a -> Maybe a
Just Model f
active_model) (forall f. Active f -> CriticalPair f
active_cp Active f
active)
  of
    Right (Maybe (CriticalPair f)
_, [CriticalPair f]
cps) ->
      forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
active_info CriticalPair f
cp)) [CriticalPair f]
cps forall a b. (a -> b) -> a -> b
$
      forall f. PrettyTerm f => Message f -> State f -> State f
message (forall f. Active f -> Message f
DeleteActive Active f
active) forall a b. (a -> b) -> a -> b
$
      forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
    Left (CriticalPair f
cp, Model f
model)
      | forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` forall f. CriticalPair f -> Equation f
cp_eqn (forall f. Active f -> CriticalPair f
active_cp Active f
active) ->
        forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
active_info CriticalPair f
cp)) (forall f. Function f => CriticalPair f -> [CriticalPair f]
split CriticalPair f
cp) forall a b. (a -> b) -> a -> b
$
        forall f. PrettyTerm f => Message f -> State f -> State f
message (forall f. Active f -> Message f
DeleteActive Active f
active) forall a b. (a -> b) -> a -> b
$
        forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
      | Model f
model forall a. Eq a => a -> a -> Bool
/= Model f
active_model ->
        forall a b c. (a -> b -> c) -> b -> a -> c
flip forall f. Function f => State f -> Active f -> State f
addActiveOnly Active f
active { active_model :: Model f
active_model = Model f
model } forall a b. (a -> b) -> a -> b
$
        forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
      | Bool
otherwise ->
        State f
state

----------------------------------------------------------------------
-- The main loop.
----------------------------------------------------------------------

data Output m f =
  Output {
    forall (m :: * -> *) f. Output m f -> Message f -> m ()
output_message :: Message f -> m () }

{-# INLINE complete #-}
complete :: (Function f, MonadIO m) => Output m f -> Config f -> State f -> m (State f)
complete :: forall f (m :: * -> *).
(Function f, MonadIO m) =>
Output m f -> Config f -> State f -> m (State f)
complete Output{Message f -> m ()
output_message :: Message f -> m ()
output_message :: forall (m :: * -> *) f. Output m f -> Message f -> m ()
..} config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state =
  forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
StateM.execStateT State f
state forall a b. (a -> b) -> a -> b
$ do
    [Task (StateT (State f) m) ()]
tasks <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
      [forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
10 (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
cfg_renormalise_percent forall a. Fractional a => a -> a -> a
/ Double
100) forall a b. (a -> b) -> a -> b
$ do
         State f
state <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall f. Function f => Config f -> State f -> Bool
shouldSimplifyQueue Config f
config State f
state) forall a b. (a -> b) -> a -> b
$ do
           forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message forall f. Message f
SimplifyQueue
           forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put forall a b. (a -> b) -> a -> b
$! forall f. Function f => Config f -> State f -> State f
simplifyQueue Config f
config State f
state,
       forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.02 forall a b. (a -> b) -> a -> b
$ do
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_complete_subsets forall a b. (a -> b) -> a -> b
$ do
           State f
state <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
           let !state' :: State f
state' = forall f. Function f => Config f -> State f -> State f
checkCompleteness Config f
config State f
state
           forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message (forall f. IntSet -> Message f
NotComplete (forall f. State f -> IntSet
st_not_complete State f
state'))
           forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put forall a b. (a -> b) -> a -> b
$! State f
state',
       forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.05 forall a b. (a -> b) -> a -> b
$ do
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_simplify forall a b. (a -> b) -> a -> b
$ do
           forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message forall f. Message f
Interreduce
           State f
state <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
           forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put forall a b. (a -> b) -> a -> b
$! forall f. Function f => State f -> State f
simplifySample forall a b. (a -> b) -> a -> b
$! forall f. Function f => Config f -> State f -> State f
interreduce Config f
config State f
state,
       forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.02 forall a b. (a -> b) -> a -> b
$ do
          State f
state <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
          forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put forall a b. (a -> b) -> a -> b
$! forall f. Function f => Config f -> State f -> State f
recomputeGoals Config f
config State f
state,
       forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
60 Double
0.01 forall a b. (a -> b) -> a -> b
$ do
          State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
          let !n :: Int
n = forall a. Batch a => Queue a -> Int
Queue.size Queue Batch
st_queue
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message (forall f. Int -> Message f
Status Int
n)]

    let
      loop :: StateT (State f) m ()
loop = do
        Bool
progress <- forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
StateM.state (forall f. Function f => Config f -> State f -> (Bool, State f)
complete1 Config f
config)
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_always_simplify forall a b. (a -> b) -> a -> b
$ do
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message forall f. Message f
Interreduce
          State f
state <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
          forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put forall a b. (a -> b) -> a -> b
$! forall f. Function f => State f -> State f
simplifySample forall a b. (a -> b) -> a -> b
$! forall f. Function f => Config f -> State f -> State f
interreduce Config f
config State f
state
        State f
state <- forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Message f -> m ()
output_message (forall f. State f -> [Message f]
messages State f
state)
        forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (forall f. State f -> State f
clearMessages State f
state)
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall (m :: * -> *) a. MonadIO m => Task m a -> m (Maybe a)
checkTask [Task (StateT (State f) m) ()]
tasks
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
progress StateT (State f) m ()
loop

    StateT (State f) m ()
loop

{-# INLINEABLE complete1 #-}
complete1 :: Function f => Config f -> State f -> (Bool, State f)
complete1 :: forall f. Function f => Config f -> State f -> (Bool, State f)
complete1 config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state
  | forall f. State f -> Int64
st_considered State f
state forall a. Ord a => a -> a -> Bool
>= Int64
cfg_max_critical_pairs =
    (Bool
False, State f
state)
  | forall f. Function f => State f -> Bool
solved State f
state = (Bool
False, State f
state)
  | Bool
otherwise =
    case forall f.
Function f =>
Config f
-> State f
-> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
dequeue Config f
config State f
state of
      (Maybe (Info, CriticalPair f, Active f, Active f)
Nothing, State f
state) -> (Bool
False, State f
state)
      (Just (Info
info, CriticalPair f
overlap, Active f
_, Active f
_), State f
state) ->
        (Bool
True, forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
info CriticalPair f
overlap)

{-# INLINEABLE solved #-}
solved :: Function f => State f -> Bool
solved :: forall f. Function f => State f -> Bool
solved = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Function f => State f -> [ProvedGoal f]
solutions

-- Return whatever goals we have proved and their proofs.
{-# INLINEABLE solutions #-}
solutions :: Function f => State f -> [ProvedGoal f]
solutions :: forall f. Function f => State f -> [ProvedGoal f]
solutions State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} = do
  Goal{goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs = Map (Term f) (Term f, Reduction f)
ts, goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_rhs = Map (Term f) (Term f, Reduction f)
us, Int
String
Map (Term f) (Derivation f)
Equation f
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} <- [Goal f]
st_goals
  let sols :: [Term f]
sols = forall k a. Map k a -> [k]
Map.keys (forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Map (Term f) (Term f, Reduction f)
ts Map (Term f) (Term f, Reduction f)
us)
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term f]
sols))
  let Term f
sol:[Term f]
_ = [Term f]
sols
  let t :: (Term f, Reduction f)
t = Map (Term f) (Term f, Reduction f)
ts forall k a. Ord k => Map k a -> k -> a
Map.! Term f
sol
      u :: (Term f, Reduction f)
u = Map (Term f) (Term f, Reduction f)
us forall k a. Ord k => Map k a -> k -> a
Map.! Term f
sol
      -- Strict so that we check the proof before returning a solution
      !p :: Proof f
p =
        forall f. Function f => Derivation f -> Proof f
Proof.certify forall a b. (a -> b) -> a -> b
$
          forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Map (Term f) (Derivation f)
-> (Term f, Reduction f) -> Derivation f
expandedProof Map (Term f) (Derivation f)
goal_expanded_lhs (Term f, Reduction f)
t forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
          forall f. Derivation f -> Derivation f
Proof.symm (forall {f}.
(Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f) =>
Map (Term f) (Derivation f)
-> (Term f, Reduction f) -> Derivation f
expandedProof Map (Term f) (Derivation f)
goal_expanded_rhs (Term f, Reduction f)
u)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall f. Int -> String -> Proof f -> ProvedGoal f
provedGoal Int
goal_number String
goal_name Proof f
p)
  where
    expandedProof :: Map (Term f) (Derivation f)
-> (Term f, Reduction f) -> Derivation f
expandedProof Map (Term f) (Derivation f)
m (Term f
t, Reduction f
red) =
      Map (Term f) (Derivation f)
m forall k a. Ord k => Map k a -> k -> a
Map.! Term f
t forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` forall f. Function f => Term f -> Reduction f -> Derivation f
reductionProof Term f
t Reduction f
red

-- Return all current rewrite rules.
{-# INLINEABLE rules #-}
rules :: Function f => State f -> [Rule f]
rules :: forall f. Function f => State f -> [Rule f]
rules = forall a b. (a -> b) -> [a] -> [b]
map forall f. Active f -> Rule f
active_rule forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IntMap a -> [a]
IntMap.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. State f -> IntMap (Active f)
st_active_set

----------------------------------------------------------------------
-- For code which uses twee as a library.
----------------------------------------------------------------------

{-# INLINEABLE completePure #-}
completePure :: Function f => Config f -> State f -> State f
completePure :: forall f. Function f => Config f -> State f -> State f
completePure Config f
cfg State f
state
  | Bool
progress = forall f. Function f => Config f -> State f -> State f
completePure Config f
cfg (forall f. State f -> State f
clearMessages State f
state')
  | Bool
otherwise = State f
state'
  where
    (Bool
progress, State f
state') = forall f. Function f => Config f -> State f -> (Bool, State f)
complete1 Config f
cfg State f
state

{-# INLINEABLE normaliseTerm #-}
normaliseTerm :: Function f => State f -> Term f -> Reduction f
normaliseTerm :: forall f. Function f => State f -> Term f -> Reduction f
normaliseTerm State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Term f
t =
  forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (forall a b. a -> b -> a
const Bool
True) (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite forall f. Function f => Rule f -> Subst f -> Bool
reduces (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)) Term f
t

{-# INLINEABLE normalForms #-}
normalForms :: Function f => State f -> Term f -> Map (Term f) (Reduction f)
normalForms :: forall f.
Function f =>
State f -> Term f -> Map (Term f) (Reduction f)
normalForms State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Term f
t =
  forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$
  forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
Rule.normalForms (forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite forall f. Function f => Rule f -> Subst f -> Bool
reduces (forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)) (forall k a. k -> a -> Map k a
Map.singleton Term f
t [])

{-# INLINEABLE simplifyTerm #-}
simplifyTerm :: Function f => State f -> Term f -> Term f
simplifyTerm :: forall f. Function f => State f -> Term f -> Term f
simplifyTerm State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Queue Batch
Sample (Maybe (Overlap (Active f) f))
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Batch
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Batch
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Term f
t =
  forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify (forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Term f
t