-- | The main prover loop.
{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies #-}
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 Twee.PassiveQueue as Queue
import Twee.PassiveQueue(Queue, Passive(..))
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

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

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

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

-- | The default prover configuration.
defaultConfig :: Config f
defaultConfig :: Config f
defaultConfig =
  Config :: forall f.
Maybe (Term f -> Bool)
-> Int64
-> Int
-> Bool
-> Int
-> Int
-> Int
-> Bool
-> Bool
-> Bool
-> Config
-> Config
-> Config f
-> Config f
Config {
    cfg_accept_term :: Maybe (Term f -> Bool)
cfg_accept_term = Maybe (Term f -> Bool)
forall a. Maybe a
Nothing,
    cfg_max_critical_pairs :: Int64
cfg_max_critical_pairs = Int64
forall a. Bounded a => a
maxBound,
    cfg_max_cp_depth :: Int
cfg_max_cp_depth = Int
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 = Config f
forall f. Config f
Proof.defaultConfig }

-- | Does this configuration run the prover in a complete mode?
configIsComplete :: Config f -> Bool
configIsComplete :: 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)
..} =
  Maybe (Term f -> Bool) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (Term f -> Bool)
cfg_accept_term) Bool -> Bool -> Bool
&&
  Int64
cfg_max_critical_pairs Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
forall a. Bounded a => a
maxBound Bool -> Bool -> Bool
&&
  Int
cfg_max_cp_depth Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
maxBound

-- | The initial state.
initialState :: Config f -> State f
initialState :: 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 :: forall f.
RuleIndex f (Rule f)
-> IntMap (Active f)
-> Index f (Equation f)
-> [Goal f]
-> Queue Params
-> Id
-> Int64
-> Id
-> Sample (Maybe (Overlap (Active f) f))
-> IntSet
-> Index f (Rule f)
-> [Message f]
-> State f
State {
    st_rules :: RuleIndex f (Rule f)
st_rules = RuleIndex f (Rule f)
forall f a. RuleIndex f a
RuleIndex.empty,
    st_active_set :: IntMap (Active f)
st_active_set = IntMap (Active f)
forall a. IntMap a
IntMap.empty,
    st_joinable :: Index f (Equation f)
st_joinable = Index f (Equation f)
forall f a. Index f a
Index.empty,
    st_goals :: [Goal f]
st_goals = [],
    st_queue :: Queue Params
st_queue = Queue Params
forall params. Queue params
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 = Int -> Sample (Maybe (Overlap (Active f) f))
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 = Index f (Rule f)
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) = Active f -> Doc
forall a. Pretty a => a -> Doc
pPrint Active f
rule
  pPrint (NewEquation Equation f
eqn) =
    String -> Doc
text String
"  (hard)" Doc -> Doc -> Doc
<+> Equation f -> 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
<#> Id -> Doc
forall a. Pretty a => a -> Doc
pPrint (Active f -> Id
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
<+> Int -> 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 ([Int] -> String
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
<#> Int -> 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 :: Message f -> State f -> State f
message !Message f
msg state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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
msgMessage f -> [Message f] -> [Message f]
forall a. a -> [a] -> [a]
:[Message f]
st_messages_rev }

-- | Forget about all emitted messages.
clearMessages :: State f -> State f
clearMessages :: State f -> State f
clearMessages state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 :: State f -> [Message f]
messages State f
state = [Message f] -> [Message f]
forall a. [a] -> [a]
reverse (State f -> [Message f]
forall f. State f -> [Message f]
st_messages_rev State f
state)

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

data Params
instance Queue.Params Params where
  type Score Params = Int
  type Id Params = Id
  type PackedId Params = Int32
  type PackedScore Params = Int32
  packScore :: proxy Params -> Score Params -> PackedScore Params
packScore proxy Params
_ = Score Params -> PackedScore Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  unpackScore :: proxy Params -> PackedScore Params -> Score Params
unpackScore proxy Params
_ = PackedScore Params -> Score Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  packId :: proxy Params -> Id Params -> PackedId Params
packId proxy Params
_ = Id Params -> PackedId Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
  unpackId :: proxy Params -> PackedId Params -> Id Params
unpackId proxy Params
_ = PackedId Params -> Id Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- | Compute all critical pairs from a rule.
{-# INLINEABLE makePassives #-}
makePassives :: Function f => Config f -> State f -> Active f -> [Passive Params]
makePassives :: Config f -> State f -> Active f -> [Passive Params]
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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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
  String
-> ([Passive Params] -> Int)
-> [Passive Params]
-> [Passive Params]
forall symbol a b. symbol -> (a -> b) -> a -> a
stampWith String
"make critical pair" [Passive Params] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
  [ Config f -> Overlap (Active f) f -> Passive Params
forall f.
Function f =>
Config f -> Overlap (Active f) f -> Passive Params
makePassive Config f
config Overlap (Active f) f
overlap
  | Active f -> Bool
ok Active f
rule,
    Overlap (Active f) f
overlap <- Index f (Rule f)
-> [Active f] -> Active f -> [Overlap (Active f) f]
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 (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) ((Active f -> Bool) -> [Active f] -> [Active f]
forall a. (a -> Bool) -> [a] -> [a]
filter Active f -> Bool
ok [Active f]
rules) Active f
rule ]
  where
    rules :: [Active f]
rules = IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems IntMap (Active f)
st_active_set
    ok :: Active f -> Bool
ok Active f
rule = Active f -> Depth
forall a b. Has a b => a -> b
the Active f
rule Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Depth
Depth Int
cfg_max_cp_depth

{-# INLINEABLE makePassive #-}
makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Params
makePassive :: Config f -> Overlap (Active f) f -> Passive Params
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 :: forall params.
Score params -> Id params -> Id params -> Int -> Passive params
Passive {
    passive_score :: Score Params
passive_score = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Config -> Depth -> Overlap (Active f) f -> Int
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 Params
passive_rule1 = Active f -> Id
forall f. Active f -> Id
active_id Active f
overlap_rule1,
    passive_rule2 :: Id Params
passive_rule2 = Active f -> Id
forall f. Active f -> Id
active_id Active f
overlap_rule2,
    passive_pos :: Int
passive_pos   = How -> Int
packHow How
overlap_how }
  where
    depth :: Depth
depth = Depth -> Depth
forall a. Enum a => a -> a
succ (Active f -> Depth
forall a b. Has a b => a -> b
the Active f
overlap_rule1 Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
`max` Active f -> Depth
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 Params -> Maybe (Overlap (Active f) f)
findPassive :: State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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{Int
Score Params
Id Params
passive_pos :: Int
passive_rule2 :: Id Params
passive_rule1 :: Id Params
passive_score :: Score Params
passive_pos :: forall params. Passive params -> Int
passive_rule2 :: forall params. Passive params -> Id params
passive_rule1 :: forall params. Passive params -> Id params
passive_score :: forall params. Passive params -> Score params
..} = do
  Active f
rule1 <- Int -> IntMap (Active f) -> Maybe (Active f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Id -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id Params
Id
passive_rule1) IntMap (Active f)
st_active_set
  Active f
rule2 <- Int -> IntMap (Active f) -> Maybe (Active f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Id -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id Params
Id
passive_rule2) IntMap (Active f)
st_active_set
  How
-> Active f
-> Active f
-> Rule f
-> Rule f
-> Maybe (Overlap (Active f) f)
forall a f.
How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt (Int -> How
unpackHow Int
passive_pos) Active f
rule1 Active f
rule2
    (Rule f -> Rule f -> Rule f
forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding (Active f -> Rule f
forall a b. Has a b => a -> b
the Active f
rule2 :: Rule f) (Active f -> Rule f
forall a b. Has a b => a -> b
the Active f
rule1)) (Active f -> Rule f
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 Params -> Maybe (Passive Params)
simplifyPassive :: Config f -> State f -> Passive Params -> Maybe (Passive Params)
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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 Params
passive = do
  Overlap (Active f) f
overlap <- State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
passive
  Overlap (Active f) f
overlap <- Index f (Rule f)
-> Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (RuleIndex f (Rule f) -> Index f (Rule f)
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 = Overlap (Active f) f -> Active f
forall a f. Overlap a f -> a
overlap_rule1 Overlap (Active f) f
overlap
      r2 :: Active f
r2 = Overlap (Active f) f -> Active f
forall a f. Overlap a f -> a
overlap_rule2 Overlap (Active f) f
overlap
  Passive Params -> Maybe (Passive Params)
forall (m :: * -> *) a. Monad m => a -> m a
return Passive Params
passive {
    passive_score :: Score Params
passive_score = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
      Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Passive Params -> Score Params
forall params. Passive params -> Score params
passive_score Passive Params
passive) Int -> Int -> Int
`intMin`
      -- XXX factor out depth calculation
      Config -> Depth -> Overlap (Active f) f -> Int
forall f a. Function f => Config -> Depth -> Overlap a f -> Int
score Config
cfg_critical_pairs (Depth -> Depth
forall a. Enum a => a -> a
succ (Active f -> Depth
forall a b. Has a b => a -> b
the Active f
r1 Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
`max` Active f -> Depth
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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)
..} =
  [Maybe (Overlap (Active f) f)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Maybe (Overlap (Active f) f) -> Bool)
-> [Maybe (Overlap (Active f) f)] -> [Maybe (Overlap (Active f) f)]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe (Overlap (Active f) f) -> Bool
forall a. Maybe a -> Bool
isNothing (Sample (Maybe (Overlap (Active f) f))
-> [Maybe (Overlap (Active f) f)]
forall a. Sample a -> [a]
sampleValue Sample (Maybe (Overlap (Active f) f))
st_cp_sample)) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
100 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
cfg_renormalise_threshold Int -> Int -> Int
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 :: Config f -> State f -> State f
simplifyQueue Config f
config State f
state =
  Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
resetSample Config f
config State f
state { st_queue :: Queue Params
st_queue = Queue Params -> Queue Params
simp (State f -> Queue Params
forall f. State f -> Queue Params
st_queue State f
state) }
  where
    simp :: Queue Params -> Queue Params
simp =
      (Passive Params -> Maybe (Passive Params))
-> Queue Params -> Queue Params
forall params.
Params params =>
(Passive params -> Maybe (Passive params))
-> Queue params -> Queue params
Queue.mapMaybe (Config f -> State f -> Passive Params -> Maybe (Passive Params)
forall f.
Function f =>
Config f -> State f -> Passive Params -> Maybe (Passive Params)
simplifyPassive Config f
config State f
state)

-- | Enqueue a set of critical pairs.
{-# INLINEABLE enqueue #-}
enqueue :: Function f => State f -> Id -> [Passive Params] -> State f
enqueue :: State f -> Id -> [Passive Params] -> State f
enqueue State f
state Id
rule [Passive Params]
passives =
  State f
state { st_queue :: Queue Params
st_queue = Id Params -> [Passive Params] -> Queue Params -> Queue Params
forall params.
Params params =>
Id params -> [Passive params] -> Queue params -> Queue params
Queue.insert Id Params
Id
rule [Passive Params]
passives (State f -> Queue Params
forall f. State f -> Queue Params
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 Params
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
deq Int64
0 Queue Params
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 Params)
Nothing -> (Maybe (Info, CriticalPair f, Active f, Active f)
forall a. Maybe a
Nothing, State f
state { st_queue :: Queue Params
st_queue = Queue Params
forall params. Queue params
Queue.empty })
    Just ((Info, CriticalPair f, Active f, Active f)
overlap, Int64
n, Queue Params
queue) ->
      ((Info, CriticalPair f, Active f, Active f)
-> Maybe (Info, CriticalPair f, Active f, Active f)
forall a. a -> Maybe a
Just (Info, CriticalPair f, Active f, Active f)
overlap,
       State f
state { st_queue :: Queue Params
st_queue = Queue Params
queue, st_considered :: Int64
st_considered = Int64
st_considered Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
n })
  where
    deq :: Int64
-> Queue Params
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
deq !Int64
n Queue Params
queue = do
      (Passive Params
passive, Queue Params
queue) <- Queue Params -> Maybe (Passive Params, Queue Params)
forall params.
Params params =>
Queue params -> Maybe (Passive params, Queue params)
Queue.removeMin Queue Params
queue
      case State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
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})
          | Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe (Term f -> Bool)
cfg_accept_term Maybe (Term f -> Bool) -> Maybe (Term f) -> Maybe Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term f -> Maybe (Term f)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f
t),
            Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe (Term f -> Bool)
cfg_accept_term Maybe (Term f -> Bool) -> Maybe (Term f) -> Maybe Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term f -> Maybe (Term f)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f
u),
            CriticalPair f
cp <- Overlap (Active f) f -> CriticalPair f
forall f a.
(Function f, Has a (Rule f)) =>
Overlap a f -> CriticalPair f
makeCriticalPair Overlap (Active f) f
overlap ->
              ((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Info -> Info -> Info
combineInfo (Active f -> Info
forall f. Active f -> Info
active_info Active f
rule1) (Active f -> Info
forall f. Active f -> Info
active_info Active f
rule2), CriticalPair f
cp, Active f
rule1, Active f
rule2), Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1, Queue Params
queue)
        Maybe (Overlap (Active f) f)
_ -> Int64
-> Queue Params
-> Maybe
     ((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
deq (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Queue Params
queue

    combineInfo :: Info -> Info -> Info
combineInfo Info
i1 Info
i2 =
      Info :: Depth -> IntSet -> Info
Info {
        -- XXX factor out depth calculation
        info_depth :: Depth
info_depth = Depth -> Depth
forall a. Enum a => a -> a
succ (Depth -> Depth -> Depth
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 {
    Active f -> Id
active_id    :: {-# UNPACK #-} !Id,
    Active f -> Info
active_info  :: {-# UNPACK #-} !Info,
    Active f -> Rule f
active_rule  :: {-# UNPACK #-} !(Rule f),
    Active f -> Maybe (Term f)
active_top   :: !(Maybe (Term f)),
    Active f -> Proof f
active_proof :: {-# UNPACK #-} !(Proof f),
    -- A model in which the rule is false (used when reorienting)
    Active f -> Model f
active_model :: !(Model f),
    Active f -> Positions2 f
active_positions :: !(Positions2 f) }

active_cp :: Active f -> CriticalPair f
active_cp :: 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 :: forall f.
Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
    cp_eqn :: Equation f
cp_eqn = Rule f -> Equation f
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 = Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
active_proof }

activeRules :: Active f -> [Rule f]
activeRules :: 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, Rule f -> Rule f
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
(==) = Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Id -> Id -> Bool)
-> (Active f -> Id) -> Active f -> Active f -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Active f -> Id
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
..} =
    Id -> Doc
forall a. Pretty a => a -> Doc
pPrint Id
active_id Doc -> Doc -> Doc
<#> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> Rule f -> Doc
forall a. Pretty a => a -> Doc
pPrint (Rule f -> Rule f
forall a. Symbolic a => a -> a
canonicalise Rule f
active_rule)

instance Has (Active f) Id where the :: Active f -> Id
the = Active f -> Id
forall f. Active f -> Id
active_id
instance Has (Active f) Depth where the :: Active f -> Depth
the = Info -> Depth
info_depth (Info -> Depth) -> (Active f -> Info) -> Active f -> Depth
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Active f -> Info
forall f. Active f -> Info
active_info
instance f ~ g => Has (Active f) (Rule g) where the :: Active f -> Rule g
the = Active f -> Rule g
forall f. Active f -> Rule f
active_rule
instance f ~ g => Has (Active f) (Positions2 g) where the :: Active f -> Positions2 g
the = Active f -> Positions2 g
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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' =
      Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Active f -> Message f
forall f. Active f -> Message f
NewActive Active f
active) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
      State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
addActiveOnly State f
state{st_next_active :: Id
st_next_active = Id
st_next_activeId -> Id -> Id
forall a. Num a => a -> a -> a
+Id
1} Active f
active
  in if (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (Rule f) -> Equation f -> Bool
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 (Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
active_rule) then
    State f
state
  else
    Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
normaliseGoals Config f
config (State f -> State f) -> State f -> State f
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 =
      Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Int -> [Passive Params] -> State f -> State f
sample ([Passive Params] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Passive Params]
passives) [Passive Params]
passives (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
      State f -> Id -> [Passive Params] -> State f
forall f.
Function f =>
State f -> Id -> [Passive Params] -> State f
enqueue State f
state (Active f -> Id
forall a b. Has a b => a -> b
the Active f
rule) [Passive Params]
passives
      where
        passives :: [Passive Params]
passives = Config f -> State f -> Active f -> [Passive Params]
forall f.
Function f =>
Config f -> State f -> Active f -> [Passive Params]
makePassives Config f
config State f
state Active f
rule

-- Update the list of sampled critical pairs.
{-# INLINEABLE sample #-}
sample :: Function f => Int -> [Passive Params] -> State f -> State f
sample :: Int -> [Passive Params] -> State f -> State f
sample Int
m [Passive Params]
passives state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 = (Int, [Maybe (Overlap (Active f) f)])
-> Sample (Maybe (Overlap (Active f) f))
-> Sample (Maybe (Overlap (Active f) f))
forall a. (Int, [a]) -> Sample a -> Sample a
addSample (Int
m, (Passive Params -> Maybe (Overlap (Active f) f))
-> [Passive Params] -> [Maybe (Overlap (Active f) f)]
forall a b. (a -> b) -> [a] -> [b]
map Passive Params -> Maybe (Overlap (Active f) f)
find [Passive Params]
passives) Sample (Maybe (Overlap (Active f) f))
st_cp_sample}
  where
    find :: Passive Params -> Maybe (Overlap (Active f) f)
find Passive Params
passive = do
      Overlap (Active f) f
overlap <- State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
passive
      Index f (Rule f)
-> Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (RuleIndex f (Rule f) -> Index f (Rule f)
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 -> (Int, [Passive Params]) -> State f)
-> State f -> [(Int, [Passive Params])] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' State f -> (Int, [Passive Params]) -> State f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
 Labelled f) =>
State f -> (Int, [Passive Params]) -> State f
sample1 State f
state' (Queue Params -> [(Int, [Passive Params])]
forall params.
Params params =>
Queue params -> [(Int, [Passive params])]
Queue.toList Queue Params
st_queue)
  where
    state' :: State f
state' =
      State f
state {
        st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = Int -> Sample (Maybe (Overlap (Active f) f))
forall a. Int -> Sample a
emptySample Int
cfg_cp_sample_size }

    sample1 :: State f -> (Int, [Passive Params]) -> State f
sample1 State f
state (Int
n, [Passive Params]
passives) = Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Int -> [Passive Params] -> State f -> State f
sample Int
n [Passive Params]
passives 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 :: State f -> State f
simplifySample state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 = (Maybe (Overlap (Active f) f) -> Maybe (Overlap (Active f) f))
-> Sample (Maybe (Overlap (Active f) f))
-> Sample (Maybe (Overlap (Active f) f))
forall a b. (a -> b) -> Sample a -> Sample b
mapSample (Maybe (Overlap (Active f) f)
-> (Overlap (Active f) f -> Maybe (Overlap (Active f) f))
-> Maybe (Overlap (Active f) f)
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' <- Index f (Rule f)
-> Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Overlap (Active f) f -> Equation f
forall a f. Overlap a f -> Equation f
overlap_eqn Overlap (Active f) f
overlap Equation f -> Equation f -> Bool
forall a. Eq a => a -> a -> Bool
== Overlap (Active f) f -> Equation f
forall a f. Overlap a f -> Equation f
overlap_eqn Overlap (Active f) f
overlap')
      Overlap (Active f) f -> Maybe (Overlap (Active f) f)
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 :: State f -> Active f -> State f
addActiveOnly state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 = (RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f))
-> RuleIndex f (Rule f) -> [Rule f] -> RuleIndex f (Rule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
forall f. RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
insertRule RuleIndex f (Rule f)
st_rules (Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules Active f
active),
    st_active_set :: IntMap (Active f)
st_active_set = Int -> Active f -> IntMap (Active f) -> IntMap (Active f)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Id -> Int
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 =
      Term f -> Rule f -> RuleIndex f (Rule f) -> RuleIndex f (Rule f)
forall f a.
(Symbolic a, ConstantOf a ~ f, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
RuleIndex.insert (Rule f -> Term f
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 :: State f -> Active f -> State f
deleteActive state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 = (RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f))
-> RuleIndex f (Rule f) -> [Rule f] -> RuleIndex f (Rule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
forall f. RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
deleteRule RuleIndex f (Rule f)
st_rules (Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules Active f
active),
    st_active_set :: IntMap (Active f)
st_active_set = Int -> IntMap (Active f) -> IntMap (Active f)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete (Id -> Int
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 =
      Term f -> Rule f -> RuleIndex f (Rule f) -> RuleIndex f (Rule f)
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 (Rule f -> Term f
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 :: Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
info CriticalPair f
cp =
  RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing (State f -> RuleIndex f (Rule f)
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 =
  String -> State f -> State f
forall symbol a. symbol -> a -> a
stamp String
"consider critical pair" (State f -> State f) -> State f -> State f
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 = CriticalPair f -> CriticalPair f
forall a. Symbolic a => a -> a
canonicalise CriticalPair f
cp0 in
  case Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (Rule f)
-> Maybe (Model f)
-> CriticalPair f
-> Either
     (CriticalPair f, Model f)
     (Maybe (CriticalPair f), [CriticalPair f])
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 Maybe (Model f)
forall a. Maybe a
Nothing CriticalPair f
cp of
    Right (Maybe (CriticalPair f)
mcp, [CriticalPair f]
cps) ->
      let
        state' :: State f
state' = (State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
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 -> State f -> Equation f -> State f
forall f. Function f => State f -> Equation f -> State f
addJoinable State f
state' (CriticalPair f -> Equation f
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) ->
      (State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
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 (CriticalPair f -> [CriticalPair f]
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 = Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
cp_proof
    rule :: Rule f
rule = Equation f -> Proof f -> Rule f
forall f. Function f => Equation f -> Proof f -> Rule f
orient Equation f
cp_eqn Proof f
pf
  in
  Config f -> State f -> (Id -> Active f) -> State f
forall f.
Function f =>
Config f -> State f -> (Id -> Active f) -> State f
addActive Config f
config State f
state ((Id -> Active f) -> State f) -> (Id -> Active f) -> State f
forall a b. (a -> b) -> a -> b
$ \Id
n ->
  Active :: forall f.
Id
-> Info
-> Rule f
-> Maybe (Term f)
-> Proof f
-> Model f
-> Positions2 f
-> Active f
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 = Rule f -> Positions2 f
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 :: Config f -> State f -> Axiom f -> State f
addAxiom Config f
config State f
state Axiom f
axiom =
  Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state
    Info :: Depth -> IntSet -> Info
Info { info_depth :: Depth
info_depth = Depth
0, info_max :: IntSet
info_max = [Int] -> IntSet
IntSet.fromList [Axiom f -> Int
forall f. Axiom f -> Int
axiom_number Axiom f
axiom | Config f -> Bool
forall f. Config f -> Bool
cfg_complete_subsets Config f
config] }
    CriticalPair :: forall f.
Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
      cp_eqn :: Equation f
cp_eqn = Axiom f -> Equation f
forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom,
      cp_top :: Maybe (Term f)
cp_top = Maybe (Term f)
forall a. Maybe a
Nothing,
      cp_proof :: Derivation f
cp_proof = Axiom f -> Derivation f
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 :: State f -> Equation f -> State f
addJoinable State f
state eqn :: Equation f
eqn@(Term f
t :=: Term f
u) =
  Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Equation f -> Message f
forall f. Equation f -> Message f
NewEquation Equation f
eqn) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
  State f
state {
    st_joinable :: Index f (Equation f)
st_joinable =
      Term f
-> Equation f -> Index f (Equation f) -> Index f (Equation f)
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 Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u) (Index f (Equation f) -> Index f (Equation f))
-> Index f (Equation f) -> Index f (Equation f)
forall a b. (a -> b) -> a -> b
$
      Term f
-> Equation f -> Index f (Equation f) -> Index f (Equation f)
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 Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
t) (State f -> Index f (Equation f)
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 :: Config f -> State f -> State f
checkCompleteness Config f
_ state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 Id -> Id -> Bool
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 = (Rule f -> Term f) -> [Rule f] -> Index f (Rule f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
(a -> Term f) -> [a] -> Index f a
Index.fromListWith Rule f -> Term f
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 Int
forall a. Bounded a => a
minBound else IntSet -> Int
IntSet.findMax IntSet
s
    maxN :: Int
maxN = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [IntSet -> Int
maxSet (Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r)) | Active f
r <- IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
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 Int -> Int -> Bool
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 = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Int] -> Int) -> (Queue Params -> [Int]) -> Queue Params -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Passive Params -> Int) -> [Passive Params] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (IntSet -> Passive Params -> Int
passiveMax IntSet
excl) ([Passive Params] -> [Int])
-> (Queue Params -> [Passive Params]) -> Queue Params -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, [Passive Params]) -> [Passive Params])
-> [(Int, [Passive Params])] -> [Passive Params]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, [Passive Params]) -> [Passive Params]
forall a b. (a, b) -> b
snd ([(Int, [Passive Params])] -> [Passive Params])
-> (Queue Params -> [(Int, [Passive Params])])
-> Queue Params
-> [Passive Params]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Queue Params -> [(Int, [Passive Params])]
forall params.
Params params =>
Queue params -> [(Int, [Passive params])]
Queue.toList (Queue Params -> Int) -> Queue Params -> Int
forall a b. (a -> b) -> a -> b
$ State f -> Queue Params
forall f. State f -> Queue Params
st_queue State f
state

    passiveMax :: IntSet -> Passive Params -> Int
passiveMax IntSet
excl Passive Params
p = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. Bounded a => a
maxBound (Maybe Int -> Int) -> Maybe Int -> Int
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} <- State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
p
      let s :: IntSet
s = Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r1) IntSet -> IntSet -> IntSet
`IntSet.union` Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r2)
      Bool -> Maybe ()
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
      Int -> Maybe Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
    rules :: [Rule f]
rules = (Active f -> [Rule f]) -> [Active f] -> [Rule f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules ((Active f -> Bool) -> [Active f] -> [Active f]
forall a. (a -> Bool) -> [a] -> [a]
filter Active f -> Bool
ok (IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
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 (Active f -> Info
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 :: 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 = (Rule f -> Term f) -> [Rule f] -> Index f (Rule f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
(a -> Term f) -> [a] -> Index f a
Index.fromListWith Rule f -> Term f
forall f. Rule f -> Term f
lhs ((Active f -> [Rule f]) -> [Active f] -> [Rule f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules (IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
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 {
    Goal f -> String
goal_name         :: String,
    Goal f -> Int
goal_number       :: Int,
    Goal f -> Equation f
goal_eqn          :: Equation f,
    Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f),
    Goal f -> Map (Term f) (Derivation f)
goal_expanded_rhs :: Map (Term f) (Derivation f),
    Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs          :: Map (Term f) (Term f, Reduction f),
    Goal f -> Map (Term f) (Term f, Reduction f)
goal_rhs          :: Map (Term f) (Term f, Reduction f) }
  deriving Int -> Goal f -> ShowS
[Goal f] -> ShowS
Goal f -> String
(Int -> Goal f -> ShowS)
-> (Goal f -> String) -> ([Goal f] -> ShowS) -> Show (Goal f)
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 :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 =
  Config f -> State f -> State f
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
goalGoal f -> [Goal f] -> [Goal f]
forall a. a -> [a] -> [a]
:[Goal f]
st_goals }

-- Normalise all goals.
{-# INLINEABLE normaliseGoals #-}
normaliseGoals :: Function f => Config f -> State f -> State f
normaliseGoals :: 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
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 =
      (Goal f -> Goal f) -> [Goal f] -> [Goal f]
forall a b. (a -> b) -> [a] -> [b]
map ((Map (Term f) (Term f, Reduction f)
 -> Map (Term f) (Term f, Reduction f))
-> Goal f -> Goal f
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 ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f (Rule f) -> Index f (Rule f)
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) = ((Term f, Reduction f) -> Term f
forall a b. (a, b) -> a
fst (Map (Term f) (Term f, Reduction f)
goals Map (Term f) (Term f, Reduction f)
-> Term f -> (Term f, Reduction f)
forall k a. Ord k => Map k a -> k -> a
Map.! Term f
t), Reduction f
red) in
        ((Term f, Reduction f) -> (Term f, Reduction f))
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> (Term f, Reduction f)
pair (Map (Term f) (Term f, Reduction f)
 -> Map (Term f) (Term f, Reduction f))
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall a b. (a -> b) -> a -> b
$ Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
Rule.normalForms Strategy f
reduce (((Term f, Reduction f) -> Reduction f)
-> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> Reduction f
forall a b. (a, b) -> b
snd Map (Term f) (Term f, Reduction f)
goals)
      | Bool
otherwise =
        [(Term f, (Term f, Reduction f))]
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Term f, (Term f, Reduction f))]
 -> Map (Term f) (Term f, Reduction f))
-> [(Term f, (Term f, Reduction f))]
-> Map (Term f) (Term f, Reduction f)
forall a b. (a -> b) -> a -> b
$
          [ (Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
q, (Term f
u, Reduction f
r Reduction f -> Reduction f -> Reduction f
forall f. Reduction f -> Reduction f -> Reduction f
`trans` Reduction f
q))
          | (Term f
t, (Term f
u, Reduction f
r)) <- Map (Term f) (Term f, Reduction f)
-> [(Term f, (Term f, Reduction f))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Term f, Reduction f)
goals,
            let q :: Reduction f
q = (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
Rule.normaliseWith (Bool -> Term f -> Bool
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 :: Config f -> State f -> State f
recomputeGoals Config f
config State f
state =
  -- Make this strict so that newTask can time it correctly
  [Map (Term f) (Term f, Reduction f)] -> ()
forall a. [a] -> ()
forceList ((Goal f -> Map (Term f) (Term f, Reduction f))
-> [Goal f] -> [Map (Term f) (Term f, Reduction f)]
forall a b. (a -> b) -> [a] -> [b]
map Goal f -> Map (Term f) (Term f, Reduction f)
forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs (State f -> [Goal f]
forall f. State f -> [Goal f]
st_goals State f
state')) () -> State f -> State f
`seq`
  [Map (Term f) (Term f, Reduction f)] -> ()
forall a. [a] -> ()
forceList ((Goal f -> Map (Term f) (Term f, Reduction f))
-> [Goal f] -> [Map (Term f) (Term f, Reduction f)]
forall a b. (a -> b) -> [a] -> [b]
map Goal f -> Map (Term f) (Term f, Reduction f)
forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_rhs (State f -> [Goal f]
forall f. State f -> [Goal f]
st_goals State f
state')) () -> State f -> State f
`seq`
  State f
state'
  where
    state' :: State f
state' =
      Config f -> State f -> State f
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 -> Goal f) -> [Goal f] -> [Goal f]
forall a b. (a -> b) -> [a] -> [b]
map Goal f -> Goal f
forall f. Goal f -> Goal f
resetGoal (State f -> [Goal f]
forall f. State f -> [Goal f]
st_goals State f
state) })

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

resetGoal :: Goal f -> Goal f
resetGoal :: 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 = Map (Term f) (Derivation f) -> Map (Term f) (Term f, Reduction f)
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 = Map (Term f) (Derivation f) -> Map (Term f) (Term f, Reduction f)
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 =
      (a -> a -> (a, [a])) -> Map a a -> Map a (a, [a])
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 :: State f -> State f
rewriteGoalsBackwards State f
state =
  State f
state { st_goals :: [Goal f]
st_goals = (Goal f -> Goal f) -> [Goal f] -> [Goal f]
forall a b. (a -> b) -> [a] -> [b]
map Goal f -> Goal f
backwardsGoal (State f -> [Goal f]
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
..} =
      Goal f -> Goal f
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 =
      [(Term f, Derivation f)] -> Map (Term f) (Derivation f)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Term f, Derivation f)] -> Map (Term f) (Derivation f))
-> [(Term f, Derivation f)] -> Map (Term f) (Derivation f)
forall a b. (a -> b) -> a -> b
$
        Map (Term f) (Derivation f) -> [(Term f, Derivation f)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Derivation f)
m [(Term f, Derivation f)]
-> [(Term f, Derivation f)] -> [(Term f, Derivation f)]
forall a. [a] -> [a] -> [a]
++
        [ (Term f -> Rule f -> Term f
forall f. Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
r, Derivation f
p Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` Derivation f
q)
        | (Term f
t, Derivation f
p) <- Map (Term f) (Derivation f) -> [(Term f, Derivation f)]
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 = Term f -> Rule f -> Derivation f
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 <- (Rule f -> Rule f) -> Reduction f -> Reduction f
forall a b. (a -> b) -> [a] -> [b]
map Rule f -> Rule f
forall a b. Has a b => a -> b
the (Index f (Rule f) -> Reduction f
forall f a. Index f a -> [a]
Index.elems (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
RuleIndex.index_all (State f -> RuleIndex f (Rule f)
forall f. State f -> RuleIndex f (Rule f)
st_rules State f
state)))
      Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule)) [Var] -> [Var] -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars (Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule)))
      [Rule f
r] <- Strategy f -> Strategy f
forall f. Strategy f -> Strategy f
anywhere ((Rule f -> Subst f -> Bool) -> Rule f -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule (\Rule f
_ Subst f
_ -> Bool
True) (Rule f -> Rule f
forall f. Rule f -> Rule f
backwards Rule f
rule)) Term f
t
      Rule f -> Reduction f
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 :: Int -> String -> Equation f -> Goal f
goal Int
n String
name (Term f
t :=: Term f
u) =
  Goal :: forall f.
String
-> Int
-> Equation f
-> Map (Term f) (Derivation f)
-> Map (Term f) (Derivation f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Goal f
Goal {
    goal_name :: String
goal_name = String
name,
    goal_number :: Int
goal_number = Int
n,
    goal_eqn :: Equation f
goal_eqn = Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u,
    goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_expanded_lhs = Term f -> Derivation f -> Map (Term f) (Derivation f)
forall k a. k -> a -> Map k a
Map.singleton Term f
t (Term f -> Derivation f
forall f. Term f -> Derivation f
Proof.Refl Term f
t),
    goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_rhs = Term f -> Derivation f -> Map (Term f) (Derivation f)
forall k a. k -> a -> Map k a
Map.singleton Term f
u (Term f -> Derivation f
forall f. Term f -> Derivation f
Proof.Refl Term f
u),
    goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_lhs = Term f
-> (Term f, Reduction f) -> Map (Term f) (Term f, Reduction f)
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 = Term f
-> (Term f, Reduction f) -> Map (Term f) (Term f, Reduction f)
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 :: Config f -> State f -> State f
interreduce Config f
_ state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 Id -> Id -> Bool
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' =
      (State f -> Active f -> State f)
-> State f -> [Active f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Config f -> State f -> Active f -> State f
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 = Index f (Equation f)
forall f a. Index f a
Index.empty, st_complete :: Index f (Rule f)
st_complete = Index f (Rule f)
forall f a. Index f a
Index.empty }
        (IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
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 = State f -> Index f (Equation f)
forall f. State f -> Index f (Equation f)
st_joinable State f
state, st_complete :: Index f (Rule f)
st_complete = State f -> Index f (Rule f)
forall f. State f -> Index f (Rule f)
st_complete State f
state, st_simplified_at :: Id
st_simplified_at = State f -> Id
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 :: 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
    Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (Rule f)
-> Maybe (Model f)
-> CriticalPair f
-> Either
     (CriticalPair f, Model f)
     (Maybe (CriticalPair f), [CriticalPair f])
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)
forall f a. Index f a
Index.empty, Index f (Rule f)
forall f a. Index f a
Index.empty) -- (st_joinable state)
      (State f -> RuleIndex f (Rule f)
forall f. State f -> RuleIndex f (Rule f)
st_rules (State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active))
      (Model f -> Maybe (Model f)
forall a. a -> Maybe a
Just Model f
active_model) (Active f -> CriticalPair f
forall f. Active f -> CriticalPair f
active_cp Active f
active)
  of
    Right (Maybe (CriticalPair f)
_, [CriticalPair f]
cps) ->
      (State f -> [CriticalPair f] -> State f)
-> [CriticalPair f] -> State f -> State f
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> Config f -> State f -> Info -> CriticalPair f -> State f
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 (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
      Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Active f -> Message f
forall f. Active f -> Message f
DeleteActive Active f
active) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
      State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
    Left (CriticalPair f
cp, Model f
model)
      | CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn (Active f -> CriticalPair f
forall f. Active f -> CriticalPair f
active_cp Active f
active) ->
        (State f -> [CriticalPair f] -> State f)
-> [CriticalPair f] -> State f -> State f
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> Config f -> State f -> Info -> CriticalPair f -> State f
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 -> [CriticalPair f]
forall f. Function f => CriticalPair f -> [CriticalPair f]
split CriticalPair f
cp) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
        Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Active f -> Message f
forall f. Active f -> Message f
DeleteActive Active f
active) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
        State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
      | Model f
model Model f -> Model f -> Bool
forall a. Eq a => a -> a -> Bool
/= Model f
active_model ->
        (State f -> Active f -> State f) -> Active f -> State f -> State f
forall a b c. (a -> b -> c) -> b -> a -> c
flip State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
addActiveOnly Active f
active { active_model :: Model f
active_model = Model f
model } (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
        State f -> Active f -> State f
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 {
    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 :: 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 =
  (StateT (State f) m () -> State f -> m (State f))
-> State f -> StateT (State f) m () -> m (State f)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (State f) m () -> State f -> m (State f)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
StateM.execStateT State f
state (StateT (State f) m () -> m (State f))
-> StateT (State f) m () -> m (State f)
forall a b. (a -> b) -> a -> b
$ do
    [Task (StateT (State f) m) ()]
tasks <- [StateT (State f) m (Task (StateT (State f) m) ())]
-> StateT (State f) m [Task (StateT (State f) m) ()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
      [Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
10 (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
cfg_renormalise_percent Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
100) (StateT (State f) m ()
 -> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
         State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
         Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config f -> State f -> Bool
forall f. Function f => Config f -> State f -> Bool
shouldSimplifyQueue Config f
config State f
state) (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
           m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message Message f
forall f. Message f
SimplifyQueue
           State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
simplifyQueue Config f
config State f
state,
       Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.02 (StateT (State f) m ()
 -> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
         Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_complete_subsets (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
           State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
           let !state' :: State f
state' = Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
checkCompleteness Config f
config State f
state
           m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message (IntSet -> Message f
forall f. IntSet -> Message f
NotComplete (State f -> IntSet
forall f. State f -> IntSet
st_not_complete State f
state'))
           State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! State f
state',
       Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.05 (StateT (State f) m ()
 -> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
         Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_simplify (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
           m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message Message f
forall f. Message f
Interreduce
           State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
           State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! State f -> State f
forall f. Function f => State f -> State f
simplifySample (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
interreduce Config f
config State f
state,
       Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.02 (StateT (State f) m ()
 -> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
          State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
          State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
recomputeGoals Config f
config State f
state,
       Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
60 Double
0.01 (StateT (State f) m ()
 -> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
          State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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)
..} <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
          let !n :: Int
n = Queue Params -> Int
forall params. Params params => Queue params -> Int
Queue.queueSize Queue Params
st_queue
          m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message (Int -> Message f
forall f. Int -> Message f
Status Int
n)]

    let
      loop :: StateT (State f) m ()
loop = do
        Bool
progress <- (State f -> (Bool, State f)) -> StateT (State f) m Bool
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
StateM.state (Config f -> State f -> (Bool, State f)
forall f. Function f => Config f -> State f -> (Bool, State f)
complete1 Config f
config)
        Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_always_simplify (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
          m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message Message f
forall f. Message f
Interreduce
          State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
          State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! State f -> State f
forall f. Function f => State f -> State f
simplifySample (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
interreduce Config f
config State f
state
        State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
        m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ (Message f -> m ()) -> [Message f] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Message f -> m ()
output_message (State f -> [Message f]
forall f. State f -> [Message f]
messages State f
state)
        State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> State f
forall f. State f -> State f
clearMessages State f
state)
        (Task (StateT (State f) m) () -> StateT (State f) m (Maybe ()))
-> [Task (StateT (State f) m) ()] -> StateT (State f) m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Task (StateT (State f) m) () -> StateT (State f) m (Maybe ())
forall (m :: * -> *) a. MonadIO m => Task m a -> m (Maybe a)
checkTask [Task (StateT (State f) m) ()]
tasks
        Bool -> StateT (State f) m () -> StateT (State f) m ()
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 :: 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
  | State f -> Int64
forall f. State f -> Int64
st_considered State f
state Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int64
cfg_max_critical_pairs =
    (Bool
False, State f
state)
  | State f -> Bool
forall f. Function f => State f -> Bool
solved State f
state = (Bool
False, State f
state)
  | Bool
otherwise =
    case Config f
-> State f
-> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
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, Config f -> State f -> Info -> CriticalPair f -> State f
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 :: State f -> Bool
solved = Bool -> Bool
not (Bool -> Bool) -> (State f -> Bool) -> State f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ProvedGoal f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([ProvedGoal f] -> Bool)
-> (State f -> [ProvedGoal f]) -> State f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State f -> [ProvedGoal f]
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 :: State f -> [ProvedGoal f]
solutions State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 = Map (Term f) (Term f, Reduction f) -> [Term f]
forall k a. Map k a -> [k]
Map.keys (Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
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)
  Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ([Term f] -> Bool
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 Map (Term f) (Term f, Reduction f)
-> Term f -> (Term f, Reduction f)
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 Map (Term f) (Term f, Reduction f)
-> Term f -> (Term f, Reduction f)
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 =
        Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
Proof.certify (Derivation f -> Proof f) -> Derivation f -> Proof f
forall a b. (a -> b) -> a -> b
$
          Map (Term f) (Derivation f)
-> (Term f, Reduction f) -> Derivation f
forall f.
(Ordered f, Arity 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 Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans`
          Derivation f -> Derivation f
forall f. Derivation f -> Derivation f
Proof.symm (Map (Term f) (Derivation f)
-> (Term f, Reduction f) -> Derivation f
forall f.
(Ordered f, Arity 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)
  ProvedGoal f -> [ProvedGoal f]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> String -> Proof f -> ProvedGoal f
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 Map (Term f) (Derivation f) -> Term f -> Derivation f
forall k a. Ord k => Map k a -> k -> a
Map.! Term f
t Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` Term f -> Reduction f -> Derivation f
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 :: State f -> [Rule f]
rules = (Active f -> Rule f) -> [Active f] -> [Rule f]
forall a b. (a -> b) -> [a] -> [b]
map Active f -> Rule f
forall f. Active f -> Rule f
active_rule ([Active f] -> [Rule f])
-> (State f -> [Active f]) -> State f -> [Rule f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (IntMap (Active f) -> [Active f])
-> (State f -> IntMap (Active f)) -> State f -> [Active f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State f -> IntMap (Active f)
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 :: Config f -> State f -> State f
completePure Config f
cfg State f
state
  | Bool
progress = Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
completePure Config f
cfg (State f -> State f
forall f. State f -> State f
clearMessages State f
state')
  | Bool
otherwise = State f
state'
  where
    (Bool
progress, State f
state') = Config f -> State f -> (Bool, State f)
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 :: State f -> Term f -> Reduction f
normaliseTerm State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 =
  (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f (Rule f) -> Index f (Rule f)
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 :: State f -> Term f -> Map (Term f) (Reduction f)
normalForms State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 =
  ((Term f, Reduction f) -> Reduction f)
-> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> Reduction f
forall a b. (a, b) -> b
snd (Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f))
-> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f)
forall a b. (a -> b) -> a -> b
$
  Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
Rule.normalForms ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)) (Term f -> Reduction f -> Map (Term f) (Reduction f)
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 :: State f -> Term f -> Term f
simplifyTerm State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
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 Params
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 Params
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 =
  Index f (Rule f) -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Term f
t