-- | 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 Data.Ord
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)

----------------------------------------------------------------------
-- * 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 (ActiveRule f)
st_rules          :: !(RuleIndex f (ActiveRule f)),
    State f -> IntMap (Active f)
st_active_ids     :: !(IntMap (Active f)),
    State f -> IntMap (ActiveRule f)
st_rule_ids       :: !(IntMap (ActiveRule 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 -> RuleId
st_next_rule      :: {-# UNPACK #-} !RuleId,
    State f -> Int64
st_considered     :: {-# UNPACK #-} !Int64,
    State f -> Id
st_simplified_at  :: {-# UNPACK #-} !Id,
    State f -> [Maybe (Overlap f)]
st_cp_sample      :: ![Maybe (Overlap f)],
    State f -> [(Integer, Int)]
st_cp_next_sample :: ![(Integer, Int)],
    State f -> Integer
st_num_cps        :: !Integer,
    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 (ActiveRule f)
-> IntMap (Active f)
-> IntMap (ActiveRule f)
-> Index f (Equation f)
-> [Goal f]
-> Queue Params
-> Id
-> RuleId
-> Int64
-> Id
-> [Maybe (Overlap f)]
-> [(Integer, Int)]
-> Integer
-> IntSet
-> Index f (Rule f)
-> [Message f]
-> State f
State {
    st_rules :: RuleIndex f (ActiveRule f)
st_rules = RuleIndex f (ActiveRule f)
forall f a. RuleIndex f a
RuleIndex.empty,
    st_active_ids :: IntMap (Active f)
st_active_ids = IntMap (Active f)
forall a. IntMap a
IntMap.empty,
    st_rule_ids :: IntMap (ActiveRule f)
st_rule_ids = IntMap (ActiveRule 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_next_rule :: RuleId
st_next_rule = RuleId
0,
    st_considered :: Int64
st_considered = Int64
0,
    st_simplified_at :: Id
st_simplified_at = Id
1,
    st_cp_sample :: [Maybe (Overlap f)]
st_cp_sample = [],
    st_cp_next_sample :: [(Integer, Int)]
st_cp_next_sample = Int -> [(Integer, Int)]
reservoir Int
cfg_cp_sample_size,
    st_num_cps :: Integer
st_num_cps = Integer
0,
    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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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 = RuleId
  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 #-}
{-# SCC makePassives #-}
makePassives :: Function f => Config f -> State f -> ActiveRule f -> [Passive Params]
makePassives :: Config f -> State f -> ActiveRule f -> [Passive Params]
makePassives 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} ActiveRule f
rule =
  [ Score Params -> Id Params -> Id Params -> Int -> Passive Params
forall params.
Score params -> Id params -> Id params -> Int -> Passive params
Passive (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Config -> Overlap f -> Int
forall f. Function f => Config -> Overlap f -> Int
score Config
cfg_critical_pairs Overlap f
o)) (ActiveRule f -> RuleId
forall f. ActiveRule f -> RuleId
rule_rid ActiveRule f
rule1) (ActiveRule f -> RuleId
forall f. ActiveRule f -> RuleId
rule_rid ActiveRule f
rule2) (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Overlap f -> Int
forall f. Overlap f -> Int
overlap_pos Overlap f
o))
  | (ActiveRule f
rule1, ActiveRule f
rule2, Overlap f
o) <- Depth
-> Index f (ActiveRule f)
-> [ActiveRule f]
-> ActiveRule f
-> [(ActiveRule f, ActiveRule f, Overlap f)]
forall a f.
(Function f, Has a Id, Has a (Rule f), Has a (Positions f),
 Has a Depth) =>
Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)]
overlaps (Int -> Depth
Depth Int
cfg_max_cp_depth) (RuleIndex f (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (ActiveRule f)
st_rules) [ActiveRule f]
rules ActiveRule f
rule ]
  where
    rules :: [ActiveRule f]
rules = IntMap (ActiveRule f) -> [ActiveRule f]
forall a. IntMap a -> [a]
IntMap.elems IntMap (ActiveRule f)
st_rule_ids

-- | Turn a Passive back into an overlap.
-- Doesn't try to simplify it.
{-# INLINEABLE findPassive #-}
{-# SCC findPassive #-}
findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
findPassive :: State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
findPassive State{Int64
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} Passive{Int
Score Params
Id 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
passive_pos :: Int
passive_rule2 :: Id Params
passive_rule1 :: Id Params
passive_score :: Score Params
..} = do
  ActiveRule f
rule1 <- Int -> IntMap (ActiveRule f) -> Maybe (ActiveRule f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (RuleId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id Params
RuleId
passive_rule1) IntMap (ActiveRule f)
st_rule_ids
  ActiveRule f
rule2 <- Int -> IntMap (ActiveRule f) -> Maybe (ActiveRule f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (RuleId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id Params
RuleId
passive_rule2) IntMap (ActiveRule f)
st_rule_ids
  let !depth :: Depth
depth = Depth
1 Depth -> Depth -> Depth
forall a. Num a => a -> a -> a
+ Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
max (ActiveRule f -> Depth
forall a b. Has a b => a -> b
the ActiveRule f
rule1) (ActiveRule f -> Depth
forall a b. Has a b => a -> b
the ActiveRule f
rule2)
  Overlap f
overlap <-
    Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
forall f. Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f)
overlapAt (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
passive_pos) Depth
depth
      (Rule f -> Rule f -> Rule f
forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding (ActiveRule f -> Rule f
forall a b. Has a b => a -> b
the ActiveRule f
rule2 :: Rule f) (ActiveRule f -> Rule f
forall a b. Has a b => a -> b
the ActiveRule f
rule1)) (ActiveRule f -> Rule f
forall a b. Has a b => a -> b
the ActiveRule f
rule2)
  (ActiveRule f, ActiveRule f, Overlap f)
-> Maybe (ActiveRule f, ActiveRule f, Overlap f)
forall (m :: * -> *) a. Monad m => a -> m a
return (ActiveRule f
rule1, ActiveRule f
rule2, Overlap f
overlap)

-- | Renormalise a queued Passive.
{-# INLINEABLE simplifyPassive #-}
{-# SCC 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} Passive Params
passive = do
  (ActiveRule f
_, ActiveRule f
_, Overlap f
overlap) <- State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
forall f.
Function f =>
State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
findPassive State f
state Passive Params
passive
  Overlap f
overlap <- Index f (ActiveRule f) -> Overlap f -> Maybe (Overlap f)
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap (RuleIndex f (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (ActiveRule f)
st_rules) Overlap 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`
      Config -> Overlap f -> Int
forall f. Function f => Config -> Overlap f -> Int
score Config
cfg_critical_pairs Overlap 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} =
  [Maybe (Overlap f)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Maybe (Overlap f) -> Bool)
-> [Maybe (Overlap f)] -> [Maybe (Overlap f)]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe (Overlap f) -> Bool
forall a. Maybe a -> Bool
isNothing [Maybe (Overlap 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 #-}
{-# SCC 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 #-}
{-# SCC enqueue #-}
enqueue :: Function f => State f -> RuleId -> [Passive Params] -> State f
enqueue :: State f -> RuleId -> [Passive Params] -> State f
enqueue State f
state RuleId
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
RuleId
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 #-}
{-# SCC dequeue #-}
dequeue :: Function f => Config f -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f), State f)
dequeue :: Config f
-> State f
-> (Maybe (CriticalPair f, ActiveRule f, ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} =
  case Int64
-> Queue Params
-> Maybe
     ((CriticalPair f, ActiveRule f, ActiveRule 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
  ((CriticalPair f, ActiveRule f, ActiveRule f), Int64, Queue Params)
Nothing -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f)
forall a. Maybe a
Nothing, State f
state { st_queue :: Queue Params
st_queue = Queue Params
forall params. Queue params
Queue.empty })
    Just ((CriticalPair f, ActiveRule f, ActiveRule f)
overlap, Int64
n, Queue Params
queue) ->
      ((CriticalPair f, ActiveRule f, ActiveRule f)
-> Maybe (CriticalPair f, ActiveRule f, ActiveRule f)
forall a. a -> Maybe a
Just (CriticalPair f, ActiveRule f, ActiveRule 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
     ((CriticalPair f, ActiveRule f, ActiveRule 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 (ActiveRule f, ActiveRule f, Overlap f)
forall f.
Function f =>
State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
findPassive State f
state Passive Params
passive of
        Just (ActiveRule f
rule1, ActiveRule f
rule2, overlap :: Overlap f
overlap@Overlap{overlap_eqn :: forall f. Overlap f -> Equation f
overlap_eqn = Term f
t :=: Term f
u})
          | 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 <- ActiveRule f -> ActiveRule f -> Overlap f -> CriticalPair f
forall f a.
(Has a (Rule f), Has a Id, Has a Max, Function f) =>
a -> a -> Overlap f -> CriticalPair f
makeCriticalPair ActiveRule f
rule1 ActiveRule f
rule2 Overlap f
overlap ->
              ((CriticalPair f, ActiveRule f, ActiveRule f), Int64, Queue Params)
-> Maybe
     ((CriticalPair f, ActiveRule f, ActiveRule f), Int64, Queue Params)
forall (m :: * -> *) a. Monad m => a -> m a
return ((CriticalPair f
cp, ActiveRule f
rule1, ActiveRule f
rule2), Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1, Queue Params
queue)
        Maybe (ActiveRule f, ActiveRule f, Overlap f)
_ -> Int64
-> Queue Params
-> Maybe
     ((CriticalPair f, ActiveRule f, ActiveRule f), Int64, Queue Params)
deq (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Queue Params
queue

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

data Active f =
  Active {
    Active f -> Id
active_id    :: {-# UNPACK #-} !Id,
    Active f -> Depth
active_depth :: {-# UNPACK #-} !Depth,
    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),
    Active f -> Max
active_max   :: !Max,
    -- A model in which the rule is false (used when reorienting)
    Active f -> Model f
active_model :: !(Model f),
    Active f -> [ActiveRule f]
active_rules :: ![ActiveRule f] }

active_cp :: Active f -> CriticalPair f
active_cp :: Active f -> CriticalPair f
active_cp Active{[ActiveRule f]
Maybe (Term f)
Model f
Id
Proof f
Rule f
Depth
Max
active_rules :: [ActiveRule f]
active_model :: Model f
active_max :: Max
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_depth :: Depth
active_id :: Id
active_rules :: forall f. Active f -> [ActiveRule f]
active_model :: forall f. Active f -> Model f
active_max :: forall f. Active f -> Max
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_depth :: forall f. Active f -> Depth
active_id :: forall f. Active f -> Id
..} =
  CriticalPair :: forall f.
Equation f
-> Depth -> Max -> 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_depth :: Depth
cp_depth = Depth
active_depth,
    cp_max :: Max
cp_max = Max
active_max,
    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 }

-- An active oriented in a particular direction.
data ActiveRule f =
  ActiveRule {
    ActiveRule f -> Id
rule_active    :: {-# UNPACK #-} !Id,
    ActiveRule f -> RuleId
rule_rid       :: {-# UNPACK #-} !RuleId,
    ActiveRule f -> Depth
rule_depth     :: {-# UNPACK #-} !Depth,
    ActiveRule f -> Max
rule_max       :: !Max,
    ActiveRule f -> Rule f
rule_rule      :: {-# UNPACK #-} !(Rule f),
    ActiveRule f -> Positions f
rule_positions :: !(Positions f) }

instance PrettyTerm f => Symbolic (ActiveRule f) where
  type ConstantOf (ActiveRule f) = f
  termsDL :: ActiveRule f -> DList (TermListOf (ActiveRule f))
termsDL ActiveRule{Id
Rule f
Depth
Positions f
Max
RuleId
rule_positions :: Positions f
rule_rule :: Rule f
rule_max :: Max
rule_depth :: Depth
rule_rid :: RuleId
rule_active :: Id
rule_positions :: forall f. ActiveRule f -> Positions f
rule_rule :: forall f. ActiveRule f -> Rule f
rule_max :: forall f. ActiveRule f -> Max
rule_depth :: forall f. ActiveRule f -> Depth
rule_active :: forall f. ActiveRule f -> Id
rule_rid :: forall f. ActiveRule f -> RuleId
..} =
    Rule f -> DList (TermListOf (Rule f))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL Rule f
rule_rule
  subst_ :: (Var -> BuilderOf (ActiveRule f)) -> ActiveRule f -> ActiveRule f
subst_ Var -> BuilderOf (ActiveRule f)
sub r :: ActiveRule f
r@ActiveRule{Id
Rule f
Depth
Positions f
Max
RuleId
rule_positions :: Positions f
rule_rule :: Rule f
rule_max :: Max
rule_depth :: Depth
rule_rid :: RuleId
rule_active :: Id
rule_positions :: forall f. ActiveRule f -> Positions f
rule_rule :: forall f. ActiveRule f -> Rule f
rule_max :: forall f. ActiveRule f -> Max
rule_depth :: forall f. ActiveRule f -> Depth
rule_active :: forall f. ActiveRule f -> Id
rule_rid :: forall f. ActiveRule f -> RuleId
..} =
    ActiveRule f
r {
      rule_rule :: Rule f
rule_rule = Rule f
rule',
      rule_positions :: Positions f
rule_positions = Term f -> Positions f
forall f. Term f -> Positions f
positions (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule') }
    where
      rule' :: Rule f
rule' = (Var -> BuilderOf (Rule f)) -> Rule f -> Rule f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Rule f)
Var -> BuilderOf (ActiveRule f)
sub Rule f
rule_rule

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 Eq (ActiveRule f) where
  == :: ActiveRule f -> ActiveRule f -> Bool
(==) = RuleId -> RuleId -> Bool
forall a. Eq a => a -> a -> Bool
(==) (RuleId -> RuleId -> Bool)
-> (ActiveRule f -> RuleId) -> ActiveRule f -> ActiveRule f -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ActiveRule f -> RuleId
forall f. ActiveRule f -> RuleId
rule_rid

instance Function f => Pretty (Active f) where
  pPrint :: Active f -> Doc
pPrint Active{[ActiveRule f]
Maybe (Term f)
Model f
Id
Proof f
Rule f
Depth
Max
active_rules :: [ActiveRule f]
active_model :: Model f
active_max :: Max
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_depth :: Depth
active_id :: Id
active_rules :: forall f. Active f -> [ActiveRule f]
active_model :: forall f. Active f -> Model f
active_max :: forall f. Active f -> Max
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_depth :: forall f. Active f -> Depth
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 (ActiveRule f) Id where the :: ActiveRule f -> Id
the = ActiveRule f -> Id
forall f. ActiveRule f -> Id
rule_active
instance Has (ActiveRule f) RuleId where the :: ActiveRule f -> RuleId
the = ActiveRule f -> RuleId
forall f. ActiveRule f -> RuleId
rule_rid
instance Has (ActiveRule f) Depth where the :: ActiveRule f -> Depth
the = ActiveRule f -> Depth
forall f. ActiveRule f -> Depth
rule_depth
instance Has (ActiveRule f) Max where the :: ActiveRule f -> Max
the = ActiveRule f -> Max
forall f. ActiveRule f -> Max
rule_max
instance f ~ g => Has (ActiveRule f) (Rule g) where the :: ActiveRule f -> Rule g
the = ActiveRule f -> Rule g
forall f. ActiveRule f -> Rule f
rule_rule
instance f ~ g => Has (ActiveRule f) (Positions g) where the :: ActiveRule f -> Positions g
the = ActiveRule f -> Positions g
forall f. ActiveRule f -> Positions f
rule_positions

newtype RuleId = RuleId Id deriving (RuleId -> RuleId -> Bool
(RuleId -> RuleId -> Bool)
-> (RuleId -> RuleId -> Bool) -> Eq RuleId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RuleId -> RuleId -> Bool
$c/= :: RuleId -> RuleId -> Bool
== :: RuleId -> RuleId -> Bool
$c== :: RuleId -> RuleId -> Bool
Eq, Eq RuleId
Eq RuleId
-> (RuleId -> RuleId -> Ordering)
-> (RuleId -> RuleId -> Bool)
-> (RuleId -> RuleId -> Bool)
-> (RuleId -> RuleId -> Bool)
-> (RuleId -> RuleId -> Bool)
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> RuleId)
-> Ord RuleId
RuleId -> RuleId -> Bool
RuleId -> RuleId -> Ordering
RuleId -> RuleId -> RuleId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RuleId -> RuleId -> RuleId
$cmin :: RuleId -> RuleId -> RuleId
max :: RuleId -> RuleId -> RuleId
$cmax :: RuleId -> RuleId -> RuleId
>= :: RuleId -> RuleId -> Bool
$c>= :: RuleId -> RuleId -> Bool
> :: RuleId -> RuleId -> Bool
$c> :: RuleId -> RuleId -> Bool
<= :: RuleId -> RuleId -> Bool
$c<= :: RuleId -> RuleId -> Bool
< :: RuleId -> RuleId -> Bool
$c< :: RuleId -> RuleId -> Bool
compare :: RuleId -> RuleId -> Ordering
$ccompare :: RuleId -> RuleId -> Ordering
$cp1Ord :: Eq RuleId
Ord, Int -> RuleId -> ShowS
[RuleId] -> ShowS
RuleId -> String
(Int -> RuleId -> ShowS)
-> (RuleId -> String) -> ([RuleId] -> ShowS) -> Show RuleId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RuleId] -> ShowS
$cshowList :: [RuleId] -> ShowS
show :: RuleId -> String
$cshow :: RuleId -> String
showsPrec :: Int -> RuleId -> ShowS
$cshowsPrec :: Int -> RuleId -> ShowS
Show, Integer -> RuleId
RuleId -> RuleId
RuleId -> RuleId -> RuleId
(RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId)
-> (RuleId -> RuleId)
-> (RuleId -> RuleId)
-> (Integer -> RuleId)
-> Num RuleId
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> RuleId
$cfromInteger :: Integer -> RuleId
signum :: RuleId -> RuleId
$csignum :: RuleId -> RuleId
abs :: RuleId -> RuleId
$cabs :: RuleId -> RuleId
negate :: RuleId -> RuleId
$cnegate :: RuleId -> RuleId
* :: RuleId -> RuleId -> RuleId
$c* :: RuleId -> RuleId -> RuleId
- :: RuleId -> RuleId -> RuleId
$c- :: RuleId -> RuleId -> RuleId
+ :: RuleId -> RuleId -> RuleId
$c+ :: RuleId -> RuleId -> RuleId
Num, Num RuleId
Ord RuleId
Num RuleId -> Ord RuleId -> (RuleId -> Rational) -> Real RuleId
RuleId -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: RuleId -> Rational
$ctoRational :: RuleId -> Rational
$cp2Real :: Ord RuleId
$cp1Real :: Num RuleId
Real, Enum RuleId
Real RuleId
Real RuleId
-> Enum RuleId
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> RuleId)
-> (RuleId -> RuleId -> (RuleId, RuleId))
-> (RuleId -> RuleId -> (RuleId, RuleId))
-> (RuleId -> Integer)
-> Integral RuleId
RuleId -> Integer
RuleId -> RuleId -> (RuleId, RuleId)
RuleId -> RuleId -> RuleId
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: RuleId -> Integer
$ctoInteger :: RuleId -> Integer
divMod :: RuleId -> RuleId -> (RuleId, RuleId)
$cdivMod :: RuleId -> RuleId -> (RuleId, RuleId)
quotRem :: RuleId -> RuleId -> (RuleId, RuleId)
$cquotRem :: RuleId -> RuleId -> (RuleId, RuleId)
mod :: RuleId -> RuleId -> RuleId
$cmod :: RuleId -> RuleId -> RuleId
div :: RuleId -> RuleId -> RuleId
$cdiv :: RuleId -> RuleId -> RuleId
rem :: RuleId -> RuleId -> RuleId
$crem :: RuleId -> RuleId -> RuleId
quot :: RuleId -> RuleId -> RuleId
$cquot :: RuleId -> RuleId -> RuleId
$cp2Integral :: Enum RuleId
$cp1Integral :: Real RuleId
Integral, Int -> RuleId
RuleId -> Int
RuleId -> [RuleId]
RuleId -> RuleId
RuleId -> RuleId -> [RuleId]
RuleId -> RuleId -> RuleId -> [RuleId]
(RuleId -> RuleId)
-> (RuleId -> RuleId)
-> (Int -> RuleId)
-> (RuleId -> Int)
-> (RuleId -> [RuleId])
-> (RuleId -> RuleId -> [RuleId])
-> (RuleId -> RuleId -> [RuleId])
-> (RuleId -> RuleId -> RuleId -> [RuleId])
-> Enum RuleId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: RuleId -> RuleId -> RuleId -> [RuleId]
$cenumFromThenTo :: RuleId -> RuleId -> RuleId -> [RuleId]
enumFromTo :: RuleId -> RuleId -> [RuleId]
$cenumFromTo :: RuleId -> RuleId -> [RuleId]
enumFromThen :: RuleId -> RuleId -> [RuleId]
$cenumFromThen :: RuleId -> RuleId -> [RuleId]
enumFrom :: RuleId -> [RuleId]
$cenumFrom :: RuleId -> [RuleId]
fromEnum :: RuleId -> Int
$cfromEnum :: RuleId -> Int
toEnum :: Int -> RuleId
$ctoEnum :: Int -> RuleId
pred :: RuleId -> RuleId
$cpred :: RuleId -> RuleId
succ :: RuleId -> RuleId
$csucc :: RuleId -> RuleId
Enum)

-- Add a new active.
{-# INLINEABLE addActive #-}
{-# SCC addActive #-}
addActive :: Function f => Config f -> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f
addActive :: Config f
-> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f
addActive Config f
config state :: State f
state@State{Int64
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} Id -> RuleId -> RuleId -> Active f
active0 =
  let
    active :: Active f
active@Active{[ActiveRule f]
Maybe (Term f)
Model f
Id
Proof f
Rule f
Depth
Max
active_rules :: [ActiveRule f]
active_model :: Model f
active_max :: Max
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_depth :: Depth
active_id :: Id
active_rules :: forall f. Active f -> [ActiveRule f]
active_model :: forall f. Active f -> Model f
active_max :: forall f. Active f -> Max
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_depth :: forall f. Active f -> Depth
active_id :: forall f. Active f -> Id
..} = Id -> RuleId -> RuleId -> Active f
active0 Id
st_next_active RuleId
st_next_rule (RuleId -> RuleId
forall a. Enum a => a -> a
succ RuleId
st_next_rule)
    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, st_next_rule :: RuleId
st_next_rule = RuleId
st_next_ruleRuleId -> RuleId -> RuleId
forall a. Num a => a -> a -> a
+RuleId
2} Active f
active
  in if (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (ActiveRule 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 (ActiveRule 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 -> ActiveRule f -> State f)
-> State f -> [ActiveRule f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' State f -> ActiveRule f -> State f
enqueueRule State f
state' [ActiveRule f]
active_rules
  where
    enqueueRule :: State f -> ActiveRule f -> State f
enqueueRule State f
state ActiveRule f
rule =
      Config f -> Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Config f -> Int -> [Passive Params] -> State f -> State f
sample Config f
config ([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 -> RuleId -> [Passive Params] -> State f
forall f.
Function f =>
State f -> RuleId -> [Passive Params] -> State f
enqueue State f
state (ActiveRule f -> RuleId
forall a b. Has a b => a -> b
the ActiveRule f
rule) [Passive Params]
passives
      where
        passives :: [Passive Params]
passives = Config f -> State f -> ActiveRule f -> [Passive Params]
forall f.
Function f =>
Config f -> State f -> ActiveRule f -> [Passive Params]
makePassives Config f
config State f
state ActiveRule f
rule

-- Update the list of sampled critical pairs.
{-# INLINEABLE sample #-}
sample :: Function f => Config f -> Int -> [Passive Params] -> State f -> State f
sample :: Config f -> Int -> [Passive Params] -> State f -> State f
sample Config f
cfg Int
m [Passive Params]
passives state :: State f
state@State{st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_next_sample = ((Integer
n, Int
pos):[(Integer, Int)]
rest), Int64
Integer
[Maybe (Overlap f)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..}
  | Integer
idx Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
m =
    Config f -> Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Config f -> Int -> [Passive Params] -> State f -> State f
sample Config f
cfg Int
m [Passive Params]
passives State f
state {
      st_cp_next_sample :: [(Integer, Int)]
st_cp_next_sample = [(Integer, Int)]
rest,
      st_cp_sample :: [Maybe (Overlap f)]
st_cp_sample =
        Int -> [Maybe (Overlap f)] -> [Maybe (Overlap f)]
forall a. Int -> [a] -> [a]
take Int
pos [Maybe (Overlap f)]
st_cp_sample [Maybe (Overlap f)] -> [Maybe (Overlap f)] -> [Maybe (Overlap f)]
forall a. [a] -> [a] -> [a]
++
        [Passive Params -> Maybe (Overlap f)
find ([Passive Params]
passives [Passive Params] -> Int -> Passive Params
forall a. [a] -> Int -> a
!! Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
idx)] [Maybe (Overlap f)] -> [Maybe (Overlap f)] -> [Maybe (Overlap f)]
forall a. [a] -> [a] -> [a]
++
        Int -> [Maybe (Overlap f)] -> [Maybe (Overlap f)]
forall a. Int -> [a] -> [a]
drop (Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [Maybe (Overlap f)]
st_cp_sample }
  | Bool
otherwise = State f
state{st_num_cps :: Integer
st_num_cps = Integer
st_num_cps Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
m}
  where
    idx :: Integer
idx = Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
st_num_cps
    find :: Passive Params -> Maybe (Overlap f)
find Passive Params
passive = do
      (ActiveRule f
_, ActiveRule f
_, Overlap f
overlap) <- State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
forall f.
Function f =>
State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
findPassive State f
state Passive Params
passive
      Index f (ActiveRule f) -> Overlap f -> Maybe (Overlap f)
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap (RuleIndex f (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (ActiveRule f)
st_rules) Overlap 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 cfg :: Config f
cfg@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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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
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_num_cps :: Integer
st_num_cps = Integer
0,
        st_cp_next_sample :: [(Integer, Int)]
st_cp_next_sample = Int -> [(Integer, Int)]
reservoir Int
cfg_cp_sample_size,
        st_cp_sample :: [Maybe (Overlap f)]
st_cp_sample = [] }

    sample1 :: State f -> (Int, [Passive Params]) -> State f
sample1 State f
state (Int
n, [Passive Params]
passives) = Config f -> Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Config f -> Int -> [Passive Params] -> State f -> State f
sample Config f
cfg 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} =
  State f
state{st_cp_sample :: [Maybe (Overlap f)]
st_cp_sample = (Maybe (Overlap f) -> Maybe (Overlap f))
-> [Maybe (Overlap f)] -> [Maybe (Overlap f)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe (Overlap f)
-> (Overlap f -> Maybe (Overlap f)) -> Maybe (Overlap f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Overlap f -> Maybe (Overlap f)
simp) [Maybe (Overlap f)]
st_cp_sample}
  where
    simp :: Overlap f -> Maybe (Overlap f)
simp Overlap f
overlap = do
      Overlap f
overlap' <- Index f (ActiveRule f) -> Overlap f -> Maybe (Overlap f)
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap f -> Maybe (Overlap f)
simplifyOverlap (RuleIndex f (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (ActiveRule f)
st_rules) Overlap f
overlap
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Overlap f -> Equation f
forall f. Overlap f -> Equation f
overlap_eqn Overlap f
overlap Equation f -> Equation f -> Bool
forall a. Eq a => a -> a -> Bool
== Overlap f -> Equation f
forall f. Overlap f -> Equation f
overlap_eqn Overlap f
overlap')
      Overlap f -> Maybe (Overlap f)
forall (m :: * -> *) a. Monad m => a -> m a
return Overlap 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} active :: Active f
active@Active{[ActiveRule f]
Maybe (Term f)
Model f
Id
Proof f
Rule f
Depth
Max
active_rules :: [ActiveRule f]
active_model :: Model f
active_max :: Max
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_depth :: Depth
active_id :: Id
active_rules :: forall f. Active f -> [ActiveRule f]
active_model :: forall f. Active f -> Model f
active_max :: forall f. Active f -> Max
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_depth :: forall f. Active f -> Depth
active_id :: forall f. Active f -> Id
..} =
  State f
state {
    st_rules :: RuleIndex f (ActiveRule f)
st_rules = (RuleIndex f (ActiveRule f)
 -> ActiveRule f -> RuleIndex f (ActiveRule f))
-> RuleIndex f (ActiveRule f)
-> [ActiveRule f]
-> RuleIndex f (ActiveRule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' RuleIndex f (ActiveRule f)
-> ActiveRule f -> RuleIndex f (ActiveRule f)
forall f.
RuleIndex f (ActiveRule f)
-> ActiveRule f -> RuleIndex f (ActiveRule f)
insertRule RuleIndex f (ActiveRule f)
st_rules [ActiveRule f]
active_rules,
    st_active_ids :: IntMap (Active f)
st_active_ids = 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_ids,
    st_rule_ids :: IntMap (ActiveRule f)
st_rule_ids = (IntMap (ActiveRule f) -> ActiveRule f -> IntMap (ActiveRule f))
-> IntMap (ActiveRule f) -> [ActiveRule f] -> IntMap (ActiveRule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' IntMap (ActiveRule f) -> ActiveRule f -> IntMap (ActiveRule f)
forall f.
IntMap (ActiveRule f) -> ActiveRule f -> IntMap (ActiveRule f)
insertRuleId IntMap (ActiveRule f)
st_rule_ids [ActiveRule f]
active_rules }
  where
    insertRule :: RuleIndex f (ActiveRule f)
-> ActiveRule f -> RuleIndex f (ActiveRule f)
insertRule RuleIndex f (ActiveRule f)
rules rule :: ActiveRule f
rule@ActiveRule{Id
Rule f
Depth
Positions f
Max
RuleId
rule_positions :: Positions f
rule_rule :: Rule f
rule_max :: Max
rule_depth :: Depth
rule_rid :: RuleId
rule_active :: Id
rule_positions :: forall f. ActiveRule f -> Positions f
rule_rule :: forall f. ActiveRule f -> Rule f
rule_max :: forall f. ActiveRule f -> Max
rule_depth :: forall f. ActiveRule f -> Depth
rule_active :: forall f. ActiveRule f -> Id
rule_rid :: forall f. ActiveRule f -> RuleId
..} =
      Term f
-> ActiveRule f
-> RuleIndex f (ActiveRule f)
-> RuleIndex f (ActiveRule f)
forall f a.
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) ActiveRule f
rule RuleIndex f (ActiveRule f)
rules
    insertRuleId :: IntMap (ActiveRule f) -> ActiveRule f -> IntMap (ActiveRule f)
insertRuleId IntMap (ActiveRule f)
rules rule :: ActiveRule f
rule@ActiveRule{Id
Rule f
Depth
Positions f
Max
RuleId
rule_positions :: Positions f
rule_rule :: Rule f
rule_max :: Max
rule_depth :: Depth
rule_rid :: RuleId
rule_active :: Id
rule_positions :: forall f. ActiveRule f -> Positions f
rule_rule :: forall f. ActiveRule f -> Rule f
rule_max :: forall f. ActiveRule f -> Max
rule_depth :: forall f. ActiveRule f -> Depth
rule_active :: forall f. ActiveRule f -> Id
rule_rid :: forall f. ActiveRule f -> RuleId
..} =
      Int
-> ActiveRule f -> IntMap (ActiveRule f) -> IntMap (ActiveRule f)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (RuleId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral RuleId
rule_rid) ActiveRule f
rule IntMap (ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} Active{[ActiveRule f]
Maybe (Term f)
Model f
Id
Proof f
Rule f
Depth
Max
active_rules :: [ActiveRule f]
active_model :: Model f
active_max :: Max
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_depth :: Depth
active_id :: Id
active_rules :: forall f. Active f -> [ActiveRule f]
active_model :: forall f. Active f -> Model f
active_max :: forall f. Active f -> Max
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_depth :: forall f. Active f -> Depth
active_id :: forall f. Active f -> Id
..} =
  State f
state {
    st_rules :: RuleIndex f (ActiveRule f)
st_rules = (RuleIndex f (ActiveRule f)
 -> ActiveRule f -> RuleIndex f (ActiveRule f))
-> RuleIndex f (ActiveRule f)
-> [ActiveRule f]
-> RuleIndex f (ActiveRule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' RuleIndex f (ActiveRule f)
-> ActiveRule f -> RuleIndex f (ActiveRule f)
forall f.
RuleIndex f (ActiveRule f)
-> ActiveRule f -> RuleIndex f (ActiveRule f)
deleteRule RuleIndex f (ActiveRule f)
st_rules [ActiveRule f]
active_rules,
    st_active_ids :: IntMap (Active f)
st_active_ids = 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_ids,
    st_rule_ids :: IntMap (ActiveRule f)
st_rule_ids = (IntMap (ActiveRule f) -> ActiveRule f -> IntMap (ActiveRule f))
-> IntMap (ActiveRule f) -> [ActiveRule f] -> IntMap (ActiveRule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' IntMap (ActiveRule f) -> ActiveRule f -> IntMap (ActiveRule f)
forall a f. IntMap a -> ActiveRule f -> IntMap a
deleteRuleId IntMap (ActiveRule f)
st_rule_ids [ActiveRule f]
active_rules }
  where
    deleteRule :: RuleIndex f (ActiveRule f)
-> ActiveRule f -> RuleIndex f (ActiveRule f)
deleteRule RuleIndex f (ActiveRule f)
rules ActiveRule f
rule =
      Term f
-> ActiveRule f
-> RuleIndex f (ActiveRule f)
-> RuleIndex f (ActiveRule f)
forall f a.
(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 (ActiveRule f -> Rule f
forall f. ActiveRule f -> Rule f
rule_rule ActiveRule f
rule)) ActiveRule f
rule RuleIndex f (ActiveRule f)
rules
    deleteRuleId :: IntMap a -> ActiveRule f -> IntMap a
deleteRuleId IntMap a
rules ActiveRule{Id
Rule f
Depth
Positions f
Max
RuleId
rule_positions :: Positions f
rule_rule :: Rule f
rule_max :: Max
rule_depth :: Depth
rule_rid :: RuleId
rule_active :: Id
rule_positions :: forall f. ActiveRule f -> Positions f
rule_rule :: forall f. ActiveRule f -> Rule f
rule_max :: forall f. ActiveRule f -> Max
rule_depth :: forall f. ActiveRule f -> Depth
rule_active :: forall f. ActiveRule f -> Id
rule_rid :: forall f. ActiveRule f -> RuleId
..} =
      Int -> IntMap a -> IntMap a
forall a. Int -> IntMap a -> IntMap a
IntMap.delete (RuleId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral RuleId
rule_rid) IntMap a
rules

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

-- Try to join a critical pair, but using a different set of critical
-- pairs for normalisation.
{-# INLINEABLE considerUsing #-}
{-# SCC considerUsing #-}
considerUsing ::
  Function f =>
  RuleIndex f (ActiveRule f) -> Config f -> State f -> CriticalPair f -> State f
considerUsing :: RuleIndex f (ActiveRule f)
-> Config f -> State f -> CriticalPair f -> State f
considerUsing RuleIndex f (ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} CriticalPair f
cp0 =
  -- 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 (ActiveRule 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 (ActiveRule 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' (RuleIndex f (ActiveRule f)
-> Config f -> State f -> CriticalPair f -> State f
forall f.
Function f =>
RuleIndex f (ActiveRule f)
-> Config f -> State f -> CriticalPair f -> State f
considerUsing RuleIndex f (ActiveRule f)
rules Config f
config) 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' (Config f -> Model f -> State f -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> Model f -> State f -> CriticalPair f -> State f
addCP Config f
config Model f
model) 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 -> CriticalPair f -> State f
addCP :: Config f -> Model f -> State f -> CriticalPair f -> State f
addCP Config f
config Model f
model state :: State f
state@State{Int64
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} CriticalPair{Maybe (Term f)
Equation f
Derivation f
Depth
Max
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_max :: Max
cp_depth :: Depth
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_max :: forall f. CriticalPair f -> Max
cp_depth :: forall f. CriticalPair f -> Depth
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

    makeRule :: Id -> RuleId -> (Rule f -> Rule f) -> ActiveRule f
makeRule Id
n RuleId
k Rule f -> Rule f
r =
      ActiveRule :: forall f.
Id
-> RuleId -> Depth -> Max -> Rule f -> Positions f -> ActiveRule f
ActiveRule {
        rule_active :: Id
rule_active = Id
n,
        rule_rid :: RuleId
rule_rid = RuleId
k,
        rule_depth :: Depth
rule_depth = Depth
cp_depth,
        rule_max :: Max
rule_max = Max
cp_max,
        rule_rule :: Rule f
rule_rule = Rule f -> Rule f
r Rule f
rule,
        rule_positions :: Positions f
rule_positions = Term f -> Positions f
forall f. Term f -> Positions f
positions (Rule f -> Term f
forall f. Rule f -> Term f
lhs (Rule f -> Rule f
r Rule f
rule)) }
  in
  Config f
-> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f
forall f.
Function f =>
Config f
-> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f
addActive Config f
config State f
state ((Id -> RuleId -> RuleId -> Active f) -> State f)
-> (Id -> RuleId -> RuleId -> Active f) -> State f
forall a b. (a -> b) -> a -> b
$ \Id
n RuleId
k1 RuleId
k2 ->
  Active :: forall f.
Id
-> Depth
-> Rule f
-> Maybe (Term f)
-> Proof f
-> Max
-> Model f
-> [ActiveRule f]
-> Active f
Active {
    active_id :: Id
active_id = Id
n,
    active_depth :: Depth
active_depth = Depth
cp_depth,
    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_max :: Max
active_max = Max
cp_max,
    active_proof :: Proof f
active_proof = Proof f
pf,
    active_rules :: [ActiveRule f]
active_rules =
      (ActiveRule f -> ActiveRule f -> Ordering)
-> [ActiveRule f] -> [ActiveRule f]
forall a. (a -> a -> Ordering) -> [a] -> [a]
usortBy ((ActiveRule f -> Rule f)
-> ActiveRule f -> ActiveRule f -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Rule f -> Rule f
forall a. Symbolic a => a -> a
canonicalise (Rule f -> Rule f)
-> (ActiveRule f -> Rule f) -> ActiveRule f -> Rule f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ActiveRule f -> Rule f
forall f. ActiveRule f -> Rule f
rule_rule)) ([ActiveRule f] -> [ActiveRule f])
-> [ActiveRule f] -> [ActiveRule f]
forall a b. (a -> b) -> a -> b
$
        Id -> RuleId -> (Rule f -> Rule f) -> ActiveRule f
makeRule Id
n RuleId
k1 Rule f -> Rule f
forall a. a -> a
idActiveRule f -> [ActiveRule f] -> [ActiveRule f]
forall a. a -> [a] -> [a]
:
        [ Id -> RuleId -> (Rule f -> Rule f) -> ActiveRule f
makeRule Id
n RuleId
k2 Rule f -> Rule f
forall f. Rule f -> Rule f
backwards
        | Bool -> Bool
not (Orientation f -> Bool
forall f. Orientation f -> Bool
oriented (Rule f -> Orientation f
forall f. Rule f -> Orientation f
orientation 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 -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> CriticalPair f -> State f
consider Config f
config State f
state (CriticalPair f -> State f) -> CriticalPair f -> State f
forall a b. (a -> b) -> a -> b
$
    CriticalPair :: forall f.
Equation f
-> Depth -> Max -> 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_depth :: Depth
cp_depth = Depth
0,
      cp_max :: Max
cp_max = IntSet -> Max
Max (IntSet -> Max) -> IntSet -> Max
forall a b. (a -> b) -> a -> b
$ [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],
      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 f a. 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 f a. 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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. (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 (Max -> IntSet
unMax (Active f -> Max
forall f. Active f -> Max
active_max 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_ids 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
      (ActiveRule f
r1, ActiveRule f
r2, Overlap f
_) <- State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
forall f.
Function f =>
State f
-> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f)
findPassive State f
state Passive Params
p
      let s :: IntSet
s = Max -> IntSet
unMax (ActiveRule f -> Max
forall f. ActiveRule f -> Max
rule_max ActiveRule f
r1) IntSet -> IntSet -> IntSet
`IntSet.union` Max -> IntSet
unMax (ActiveRule f -> Max
forall f. ActiveRule f -> Max
rule_max ActiveRule 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 = (ActiveRule f -> Rule f) -> [ActiveRule f] -> [Rule f]
forall a b. (a -> b) -> [a] -> [b]
map ActiveRule f -> Rule f
forall f. ActiveRule f -> Rule f
rule_rule ((ActiveRule f -> Bool) -> [ActiveRule f] -> [ActiveRule f]
forall a. (a -> Bool) -> [a] -> [a]
filter ActiveRule f -> Bool
ok (IntMap (ActiveRule f) -> [ActiveRule f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (ActiveRule f)
forall f. State f -> IntMap (ActiveRule f)
st_rule_ids State f
state)))
    ok :: ActiveRule f -> Bool
ok ActiveRule f
r = Max -> IntSet
unMax (ActiveRule f -> Max
forall f. ActiveRule f -> Max
rule_max ActiveRule 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. (a -> Term f) -> [a] -> Index f a
Index.fromListWith Rule f -> Term f
forall f. Rule f -> Term f
lhs ((ActiveRule f -> Rule f) -> [ActiveRule f] -> [Rule f]
forall a b. (a -> b) -> [a] -> [b]
map ActiveRule f -> Rule f
forall f. ActiveRule f -> Rule f
rule_rule (IntMap (ActiveRule f) -> [ActiveRule f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (ActiveRule f)
forall f. State f -> IntMap (ActiveRule f)
st_rule_ids 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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 (ActiveRule 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 (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (ActiveRule 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 <- (ActiveRule f -> Rule f) -> [ActiveRule f] -> Reduction f
forall a b. (a -> b) -> [a] -> [b]
map ActiveRule f -> Rule f
forall a b. Has a b => a -> b
the (Index f (ActiveRule f) -> [ActiveRule f]
forall f a. Index f a -> [a]
Index.elems (RuleIndex f (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
RuleIndex.index_all (State f -> RuleIndex f (ActiveRule f)
forall f. State f -> RuleIndex f (ActiveRule 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 #-}
{-# SCC 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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_ids 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 f
active =
  -- 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 (ActiveRule 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 (ActiveRule f)
forall f. State f -> RuleIndex f (ActiveRule 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 (Active f -> Model f
forall f. Active f -> Model f
active_model Active f
active)) (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' (Config f -> State f -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> CriticalPair f -> State f
consider Config f
config)) [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' (Config f -> State f -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> CriticalPair f -> State f
consider Config f
config)) (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
/= Active f -> Model f
forall f. Active f -> Model f
active_model Active f
active ->
        (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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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 (CriticalPair f, ActiveRule f, ActiveRule f), State f)
forall f.
Function f =>
Config f
-> State f
-> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f), State f)
dequeue Config f
config State f
state of
      (Maybe (CriticalPair f, ActiveRule f, ActiveRule f)
Nothing, State f
state) -> (Bool
False, State f
state)
      (Just (CriticalPair f
overlap, ActiveRule f
_, ActiveRule f
_), State f
state) ->
        (Bool
True, Config f -> State f -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> CriticalPair f -> State f
consider Config f
config State f
state 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 #-}
{-# SCC solutions #-}
solutions :: Function f => State f -> [ProvedGoal f]
solutions :: State f -> [ProvedGoal f]
solutions State{Int64
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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_ids

----------------------------------------------------------------------
-- 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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 (ActiveRule 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 (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule 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 (ActiveRule 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 (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (ActiveRule 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
Integer
[Maybe (Overlap f)]
[(Integer, Int)]
[Goal f]
[Message f]
IntMap (ActiveRule f)
IntMap (Active f)
IntSet
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (ActiveRule f)
RuleId
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_num_cps :: Integer
st_cp_next_sample :: [(Integer, Int)]
st_cp_sample :: [Maybe (Overlap f)]
st_simplified_at :: Id
st_considered :: Int64
st_next_rule :: RuleId
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_rule_ids :: IntMap (ActiveRule f)
st_active_ids :: IntMap (Active f)
st_rules :: RuleIndex f (ActiveRule 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_num_cps :: forall f. State f -> Integer
st_cp_next_sample :: forall f. State f -> [(Integer, Int)]
st_cp_sample :: forall f. State f -> [Maybe (Overlap f)]
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_rule :: forall f. State f -> RuleId
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_rule_ids :: forall f. State f -> IntMap (ActiveRule f)
st_active_ids :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (ActiveRule f)
..} Term f
t =
  Index f (ActiveRule f) -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify (RuleIndex f (ActiveRule f) -> Index f (ActiveRule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (ActiveRule f)
st_rules) Term f
t