{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies #-}
module Twee where
import Twee.Base
import Twee.Rule hiding (normalForms)
import qualified Twee.Rule as Rule
import Twee.Equation
import qualified Twee.Proof as Proof
import Twee.Proof(Axiom(..), Proof(..), Derivation, ProvedGoal(..), provedGoal, certify, derivation)
import Twee.CP hiding (Config)
import qualified Twee.CP as CP
import Twee.Join hiding (Config, defaultConfig)
import qualified Twee.Join as Join
import qualified Twee.Rule.Index as RuleIndex
import Twee.Rule.Index(RuleIndex(..))
import qualified Twee.Index as Index
import Twee.Index(Index)
import Twee.Constraints
import Twee.Utils
import Twee.Task
import qualified Twee.PassiveQueue as Queue
import Twee.PassiveQueue(Queue, Passive(..))
import qualified Data.IntMap.Strict as IntMap
import Data.IntMap(IntMap)
import Data.Maybe
import Data.List
import Data.Function
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import Data.Int
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import qualified Control.Monad.Trans.State.Strict as StateM
import qualified Data.IntSet as IntSet
import Data.IntSet(IntSet)
import Twee.Profile
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 }
data State f =
State {
State f -> RuleIndex f (Rule f)
st_rules :: !(RuleIndex f (Rule f)),
State f -> IntMap (Active f)
st_active_set :: !(IntMap (Active f)),
State f -> Index f (Equation f)
st_joinable :: !(Index f (Equation f)),
State f -> [Goal f]
st_goals :: ![Goal f],
State f -> Queue Params
st_queue :: !(Queue Params),
State f -> Id
st_next_active :: {-# UNPACK #-} !Id,
State f -> Int64
st_considered :: {-# UNPACK #-} !Int64,
State f -> Id
st_simplified_at :: {-# UNPACK #-} !Id,
State f -> Sample (Maybe (Overlap (Active f) f))
st_cp_sample :: !(Sample (Maybe (Overlap (Active f) f))),
State f -> IntSet
st_not_complete :: !IntSet,
State f -> Index f (Rule f)
st_complete :: !(Index f (Rule f)),
State f -> [Message f]
st_messages_rev :: ![Message f] }
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 }
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
initialState :: Config f -> State f
initialState :: Config f -> State f
initialState Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} =
State :: forall f.
RuleIndex f (Rule f)
-> IntMap (Active f)
-> Index f (Equation f)
-> [Goal f]
-> Queue Params
-> Id
-> Int64
-> Id
-> Sample (Maybe (Overlap (Active f) f))
-> IntSet
-> Index f (Rule f)
-> [Message f]
-> State f
State {
st_rules :: RuleIndex f (Rule f)
st_rules = RuleIndex f (Rule f)
forall f a. RuleIndex f a
RuleIndex.empty,
st_active_set :: IntMap (Active f)
st_active_set = IntMap (Active f)
forall a. IntMap a
IntMap.empty,
st_joinable :: Index f (Equation f)
st_joinable = Index f (Equation f)
forall f a. Index f a
Index.empty,
st_goals :: [Goal f]
st_goals = [],
st_queue :: Queue Params
st_queue = Queue Params
forall params. Queue params
Queue.empty,
st_next_active :: Id
st_next_active = Id
1,
st_considered :: Int64
st_considered = Int64
0,
st_simplified_at :: Id
st_simplified_at = Id
1,
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = Int -> Sample (Maybe (Overlap (Active f) f))
forall a. Int -> Sample a
emptySample Int
cfg_cp_sample_size,
st_not_complete :: IntSet
st_not_complete = IntSet
IntSet.empty,
st_complete :: Index f (Rule f)
st_complete = Index f (Rule f)
forall f a. Index f a
Index.empty,
st_messages_rev :: [Message f]
st_messages_rev = [] }
data Message f =
NewActive !(Active f)
| NewEquation !(Equation f)
| DeleteActive !(Active f)
| SimplifyQueue
| NotComplete !IntSet
| Interreduce
| 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)"
message :: PrettyTerm f => Message f -> State f -> State f
message :: Message f -> State f -> State f
message !Message f
msg state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
State f
state { st_messages_rev :: [Message f]
st_messages_rev = Message f
msgMessage f -> [Message f] -> [Message f]
forall a. a -> [a] -> [a]
:[Message f]
st_messages_rev }
clearMessages :: State f -> State f
clearMessages :: State f -> State f
clearMessages state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
State f
state { st_messages_rev :: [Message f]
st_messages_rev = [] }
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)
data Params
instance Queue.Params Params where
type Score Params = Int
type Id Params = Id
type PackedId Params = Int32
type PackedScore Params = Int32
packScore :: proxy Params -> Score Params -> PackedScore Params
packScore proxy Params
_ = Score Params -> PackedScore Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
unpackScore :: proxy Params -> PackedScore Params -> Score Params
unpackScore proxy Params
_ = PackedScore Params -> Score Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
packId :: proxy Params -> Id Params -> PackedId Params
packId proxy Params
_ = Id Params -> PackedId Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
unpackId :: proxy Params -> PackedId Params -> Id Params
unpackId proxy Params
_ = PackedId Params -> Id Params
forall a b. (Integral a, Num b) => a -> b
fromIntegral
{-# INLINEABLE makePassives #-}
makePassives :: Function f => Config f -> State f -> Active f -> [Passive Params]
makePassives :: Config f -> State f -> Active f -> [Passive Params]
makePassives config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Active f
rule =
String
-> ([Passive Params] -> Int)
-> [Passive Params]
-> [Passive Params]
forall symbol a b. symbol -> (a -> b) -> a -> a
stampWith String
"make critical pair" [Passive Params] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
[ Config f -> Overlap (Active f) f -> Passive Params
forall f.
Function f =>
Config f -> Overlap (Active f) f -> Passive Params
makePassive Config f
config Overlap (Active f) f
overlap
| Active f -> Bool
ok Active f
rule,
Overlap (Active f) f
overlap <- Index f (Rule f)
-> [Active f] -> Active f -> [Overlap (Active f) f]
forall a b f.
(Function f, Has a (Rule f), Has b (Rule f),
Has b (Positions2 f)) =>
Index f a -> [b] -> b -> [Overlap b f]
overlaps (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) ((Active f -> Bool) -> [Active f] -> [Active f]
forall a. (a -> Bool) -> [a] -> [a]
filter Active f -> Bool
ok [Active f]
rules) Active f
rule ]
where
rules :: [Active f]
rules = IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems IntMap (Active f)
st_active_set
ok :: Active f -> Bool
ok Active f
rule = Active f -> Depth
forall a b. Has a b => a -> b
the Active f
rule Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Depth
Depth Int
cfg_max_cp_depth
{-# INLINEABLE makePassive #-}
makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Params
makePassive :: Config f -> Overlap (Active f) f -> Passive Params
makePassive Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} overlap :: Overlap (Active f) f
overlap@Overlap{Term f
Equation f
How
Active f
overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_top :: forall a f. Overlap a f -> Term f
overlap_how :: forall a f. Overlap a f -> How
overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule1 :: forall a f. Overlap a f -> a
overlap_eqn :: Equation f
overlap_top :: Term f
overlap_how :: How
overlap_rule2 :: Active f
overlap_rule1 :: Active f
..} =
Passive :: forall params.
Score params -> Id params -> Id params -> Int -> Passive params
Passive {
passive_score :: Score Params
passive_score = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Config -> Depth -> Overlap (Active f) f -> Int
forall f a. Function f => Config -> Depth -> Overlap a f -> Int
score Config
cfg_critical_pairs Depth
depth Overlap (Active f) f
overlap),
passive_rule1 :: Id Params
passive_rule1 = Active f -> Id
forall f. Active f -> Id
active_id Active f
overlap_rule1,
passive_rule2 :: Id Params
passive_rule2 = Active f -> Id
forall f. Active f -> Id
active_id Active f
overlap_rule2,
passive_pos :: Int
passive_pos = How -> Int
packHow How
overlap_how }
where
depth :: Depth
depth = Depth -> Depth
forall a. Enum a => a -> a
succ (Active f -> Depth
forall a b. Has a b => a -> b
the Active f
overlap_rule1 Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
`max` Active f -> Depth
forall a b. Has a b => a -> b
the Active f
overlap_rule2)
{-# INLINEABLE findPassive #-}
findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive :: State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Passive{Int
Score Params
Id Params
passive_pos :: Int
passive_rule2 :: Id Params
passive_rule1 :: Id Params
passive_score :: Score Params
passive_pos :: forall params. Passive params -> Int
passive_rule2 :: forall params. Passive params -> Id params
passive_rule1 :: forall params. Passive params -> Id params
passive_score :: forall params. Passive params -> Score params
..} = do
Active f
rule1 <- Int -> IntMap (Active f) -> Maybe (Active f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Id -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id Params
Id
passive_rule1) IntMap (Active f)
st_active_set
Active f
rule2 <- Int -> IntMap (Active f) -> Maybe (Active f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Id -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id Params
Id
passive_rule2) IntMap (Active f)
st_active_set
How
-> Active f
-> Active f
-> Rule f
-> Rule f
-> Maybe (Overlap (Active f) f)
forall a f.
How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)
overlapAt (Int -> How
unpackHow Int
passive_pos) Active f
rule1 Active f
rule2
(Rule f -> Rule f -> Rule f
forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding (Active f -> Rule f
forall a b. Has a b => a -> b
the Active f
rule2 :: Rule f) (Active f -> Rule f
forall a b. Has a b => a -> b
the Active f
rule1)) (Active f -> Rule f
forall a b. Has a b => a -> b
the Active f
rule2)
{-# INLINEABLE simplifyPassive #-}
simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)
simplifyPassive :: Config f -> State f -> Passive Params -> Maybe (Passive Params)
simplifyPassive Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Passive Params
passive = do
Overlap (Active f) f
overlap <- State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
passive
Overlap (Active f) f
overlap <- Index f (Rule f)
-> Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap
let r1 :: Active f
r1 = Overlap (Active f) f -> Active f
forall a f. Overlap a f -> a
overlap_rule1 Overlap (Active f) f
overlap
r2 :: Active f
r2 = Overlap (Active f) f -> Active f
forall a f. Overlap a f -> a
overlap_rule2 Overlap (Active f) f
overlap
Passive Params -> Maybe (Passive Params)
forall (m :: * -> *) a. Monad m => a -> m a
return Passive Params
passive {
passive_score :: Score Params
passive_score = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Passive Params -> Score Params
forall params. Passive params -> Score params
passive_score Passive Params
passive) Int -> Int -> Int
`intMin`
Config -> Depth -> Overlap (Active f) f -> Int
forall f a. Function f => Config -> Depth -> Overlap a f -> Int
score Config
cfg_critical_pairs (Depth -> Depth
forall a. Enum a => a -> a
succ (Active f -> Depth
forall a b. Has a b => a -> b
the Active f
r1 Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
`max` Active f -> Depth
forall a b. Has a b => a -> b
the Active f
r2)) Overlap (Active f) f
overlap }
{-# INLINEABLE shouldSimplifyQueue #-}
shouldSimplifyQueue :: Function f => Config f -> State f -> Bool
shouldSimplifyQueue :: Config f -> State f -> Bool
shouldSimplifyQueue Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
[Maybe (Overlap (Active f) f)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Maybe (Overlap (Active f) f) -> Bool)
-> [Maybe (Overlap (Active f) f)] -> [Maybe (Overlap (Active f) f)]
forall a. (a -> Bool) -> [a] -> [a]
filter Maybe (Overlap (Active f) f) -> Bool
forall a. Maybe a -> Bool
isNothing (Sample (Maybe (Overlap (Active f) f))
-> [Maybe (Overlap (Active f) f)]
forall a. Sample a -> [a]
sampleValue Sample (Maybe (Overlap (Active f) f))
st_cp_sample)) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
100 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
cfg_renormalise_threshold Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
cfg_cp_sample_size
{-# INLINEABLE simplifyQueue #-}
simplifyQueue :: Function f => Config f -> State f -> State f
simplifyQueue :: Config f -> State f -> State f
simplifyQueue Config f
config State f
state =
Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
resetSample Config f
config State f
state { st_queue :: Queue Params
st_queue = Queue Params -> Queue Params
simp (State f -> Queue Params
forall f. State f -> Queue Params
st_queue State f
state) }
where
simp :: Queue Params -> Queue Params
simp =
(Passive Params -> Maybe (Passive Params))
-> Queue Params -> Queue Params
forall params.
Params params =>
(Passive params -> Maybe (Passive params))
-> Queue params -> Queue params
Queue.mapMaybe (Config f -> State f -> Passive Params -> Maybe (Passive Params)
forall f.
Function f =>
Config f -> State f -> Passive Params -> Maybe (Passive Params)
simplifyPassive Config f
config State f
state)
{-# INLINEABLE enqueue #-}
enqueue :: Function f => State f -> Id -> [Passive Params] -> State f
enqueue :: State f -> Id -> [Passive Params] -> State f
enqueue State f
state Id
rule [Passive Params]
passives =
State f
state { st_queue :: Queue Params
st_queue = Id Params -> [Passive Params] -> Queue Params -> Queue Params
forall params.
Params params =>
Id params -> [Passive params] -> Queue params -> Queue params
Queue.insert Id Params
Id
rule [Passive Params]
passives (State f -> Queue Params
forall f. State f -> Queue Params
st_queue State f
state) }
{-# INLINEABLE dequeue #-}
dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
dequeue :: Config f
-> State f
-> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
dequeue Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
case Int64
-> Queue Params
-> Maybe
((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
deq Int64
0 Queue Params
st_queue of
Maybe
((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
Nothing -> (Maybe (Info, CriticalPair f, Active f, Active f)
forall a. Maybe a
Nothing, State f
state { st_queue :: Queue Params
st_queue = Queue Params
forall params. Queue params
Queue.empty })
Just ((Info, CriticalPair f, Active f, Active f)
overlap, Int64
n, Queue Params
queue) ->
((Info, CriticalPair f, Active f, Active f)
-> Maybe (Info, CriticalPair f, Active f, Active f)
forall a. a -> Maybe a
Just (Info, CriticalPair f, Active f, Active f)
overlap,
State f
state { st_queue :: Queue Params
st_queue = Queue Params
queue, st_considered :: Int64
st_considered = Int64
st_considered Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
n })
where
deq :: Int64
-> Queue Params
-> Maybe
((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
deq !Int64
n Queue Params
queue = do
(Passive Params
passive, Queue Params
queue) <- Queue Params -> Maybe (Passive Params, Queue Params)
forall params.
Params params =>
Queue params -> Maybe (Passive params, Queue params)
Queue.removeMin Queue Params
queue
case State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
passive of
Just (overlap :: Overlap (Active f) f
overlap@Overlap{overlap_eqn :: forall a f. Overlap a f -> Equation f
overlap_eqn = Term f
t :=: Term f
u, overlap_rule1 :: forall a f. Overlap a f -> a
overlap_rule1 = Active f
rule1, overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule2 = Active f
rule2})
| Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe (Term f -> Bool)
cfg_accept_term Maybe (Term f -> Bool) -> Maybe (Term f) -> Maybe Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term f -> Maybe (Term f)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f
t),
Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
True (Maybe (Term f -> Bool)
cfg_accept_term Maybe (Term f -> Bool) -> Maybe (Term f) -> Maybe Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term f -> Maybe (Term f)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term f
u),
CriticalPair f
cp <- Overlap (Active f) f -> CriticalPair f
forall f a.
(Function f, Has a (Rule f)) =>
Overlap a f -> CriticalPair f
makeCriticalPair Overlap (Active f) f
overlap ->
((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
-> Maybe
((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Info -> Info -> Info
combineInfo (Active f -> Info
forall f. Active f -> Info
active_info Active f
rule1) (Active f -> Info
forall f. Active f -> Info
active_info Active f
rule2), CriticalPair f
cp, Active f
rule1, Active f
rule2), Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1, Queue Params
queue)
Maybe (Overlap (Active f) f)
_ -> Int64
-> Queue Params
-> Maybe
((Info, CriticalPair f, Active f, Active f), Int64, Queue Params)
deq (Int64
nInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1) Queue Params
queue
combineInfo :: Info -> Info -> Info
combineInfo Info
i1 Info
i2 =
Info :: Depth -> IntSet -> Info
Info {
info_depth :: Depth
info_depth = Depth -> Depth
forall a. Enum a => a -> a
succ (Depth -> Depth -> Depth
forall a. Ord a => a -> a -> a
max (Info -> Depth
info_depth Info
i1) (Info -> Depth
info_depth Info
i2)),
info_max :: IntSet
info_max = IntSet -> IntSet -> IntSet
IntSet.union (Info -> IntSet
info_max Info
i1) (Info -> IntSet
info_max Info
i2) }
data Active f =
Active {
Active f -> Id
active_id :: {-# UNPACK #-} !Id,
Active f -> Info
active_info :: {-# UNPACK #-} !Info,
Active f -> Rule f
active_rule :: {-# UNPACK #-} !(Rule f),
Active f -> Maybe (Term f)
active_top :: !(Maybe (Term f)),
Active f -> Proof f
active_proof :: {-# UNPACK #-} !(Proof f),
Active f -> Model f
active_model :: !(Model f),
Active f -> Positions2 f
active_positions :: !(Positions2 f) }
active_cp :: Active f -> CriticalPair f
active_cp :: Active f -> CriticalPair f
active_cp Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
CriticalPair :: forall f.
Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
cp_eqn :: Equation f
cp_eqn = Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
active_rule,
cp_top :: Maybe (Term f)
cp_top = Maybe (Term f)
active_top,
cp_proof :: Derivation f
cp_proof = Proof f -> Derivation f
forall f. Proof f -> Derivation f
derivation Proof f
active_proof }
activeRules :: Active f -> [Rule f]
activeRules :: Active f -> [Rule f]
activeRules Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
case Positions2 f
active_positions of
ForwardsPos Positions f
_ -> [Rule f
active_rule]
BothPos Positions f
_ Positions f
_ -> [Rule f
active_rule, Rule f -> Rule f
forall f. Rule f -> Rule f
backwards Rule f
active_rule]
data Info =
Info {
Info -> Depth
info_depth :: {-# UNPACK #-} !Depth,
Info -> IntSet
info_max :: !IntSet }
instance Eq (Active f) where
== :: Active f -> Active f -> Bool
(==) = Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Id -> Id -> Bool)
-> (Active f -> Id) -> Active f -> Active f -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Active f -> Id
forall f. Active f -> Id
active_id
instance Function f => Pretty (Active f) where
pPrint :: Active f -> Doc
pPrint Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
Id -> Doc
forall a. Pretty a => a -> Doc
pPrint Id
active_id Doc -> Doc -> Doc
<#> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> Rule f -> Doc
forall a. Pretty a => a -> Doc
pPrint (Rule f -> Rule f
forall a. Symbolic a => a -> a
canonicalise Rule f
active_rule)
instance Has (Active f) Id where the :: Active f -> Id
the = Active f -> Id
forall f. Active f -> Id
active_id
instance Has (Active f) Depth where the :: Active f -> Depth
the = Info -> Depth
info_depth (Info -> Depth) -> (Active f -> Info) -> Active f -> Depth
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Active f -> Info
forall f. Active f -> Info
active_info
instance f ~ g => Has (Active f) (Rule g) where the :: Active f -> Rule g
the = Active f -> Rule g
forall f. Active f -> Rule f
active_rule
instance f ~ g => Has (Active f) (Positions2 g) where the :: Active f -> Positions2 g
the = Active f -> Positions2 g
forall f. Active f -> Positions2 f
active_positions
{-# INLINEABLE addActive #-}
addActive :: Function f => Config f -> State f -> (Id -> Active f) -> State f
addActive :: Config f -> State f -> (Id -> Active f) -> State f
addActive Config f
config state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Id -> Active f
active0 =
let
active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} = Id -> Active f
active0 Id
st_next_active
state' :: State f
state' =
Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Active f -> Message f
forall f. Active f -> Message f
NewActive Active f
active) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
addActiveOnly State f
state{st_next_active :: Id
st_next_active = Id
st_next_activeId -> Id -> Id
forall a. Num a => a -> a -> a
+Id
1} Active f
active
in if (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (Rule f) -> Equation f -> Bool
forall a f.
(Has a (Rule f), Function f) =>
(Index f (Equation f), Index f (Rule f))
-> RuleIndex f a -> Equation f -> Bool
subsumed (Index f (Equation f)
st_joinable, Index f (Rule f)
st_complete) RuleIndex f (Rule f)
st_rules (Rule f -> Equation f
forall f. Rule f -> Equation f
unorient Rule f
active_rule) then
State f
state
else
Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
normaliseGoals Config f
config (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f -> Active f -> State f
enqueueRule State f
state' Active f
active
where
enqueueRule :: State f -> Active f -> State f
enqueueRule State f
state Active f
rule =
Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Int -> [Passive Params] -> State f -> State f
sample ([Passive Params] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Passive Params]
passives) [Passive Params]
passives (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f -> Id -> [Passive Params] -> State f
forall f.
Function f =>
State f -> Id -> [Passive Params] -> State f
enqueue State f
state (Active f -> Id
forall a b. Has a b => a -> b
the Active f
rule) [Passive Params]
passives
where
passives :: [Passive Params]
passives = Config f -> State f -> Active f -> [Passive Params]
forall f.
Function f =>
Config f -> State f -> Active f -> [Passive Params]
makePassives Config f
config State f
state Active f
rule
{-# INLINEABLE sample #-}
sample :: Function f => Int -> [Passive Params] -> State f -> State f
sample :: Int -> [Passive Params] -> State f -> State f
sample Int
m [Passive Params]
passives state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
State f
state{st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = (Int, [Maybe (Overlap (Active f) f)])
-> Sample (Maybe (Overlap (Active f) f))
-> Sample (Maybe (Overlap (Active f) f))
forall a. (Int, [a]) -> Sample a -> Sample a
addSample (Int
m, (Passive Params -> Maybe (Overlap (Active f) f))
-> [Passive Params] -> [Maybe (Overlap (Active f) f)]
forall a b. (a -> b) -> [a] -> [b]
map Passive Params -> Maybe (Overlap (Active f) f)
find [Passive Params]
passives) Sample (Maybe (Overlap (Active f) f))
st_cp_sample}
where
find :: Passive Params -> Maybe (Overlap (Active f) f)
find Passive Params
passive = do
Overlap (Active f) f
overlap <- State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
passive
Index f (Rule f)
-> Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap
{-# INLINEABLE resetSample #-}
resetSample :: Function f => Config f -> State f -> State f
resetSample :: Config f -> State f -> State f
resetSample Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
(State f -> (Int, [Passive Params]) -> State f)
-> State f -> [(Int, [Passive Params])] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' State f -> (Int, [Passive Params]) -> State f
forall f.
(Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f,
Labelled f) =>
State f -> (Int, [Passive Params]) -> State f
sample1 State f
state' (Queue Params -> [(Int, [Passive Params])]
forall params.
Params params =>
Queue params -> [(Int, [Passive params])]
Queue.toList Queue Params
st_queue)
where
state' :: State f
state' =
State f
state {
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = Int -> Sample (Maybe (Overlap (Active f) f))
forall a. Int -> Sample a
emptySample Int
cfg_cp_sample_size }
sample1 :: State f -> (Int, [Passive Params]) -> State f
sample1 State f
state (Int
n, [Passive Params]
passives) = Int -> [Passive Params] -> State f -> State f
forall f.
Function f =>
Int -> [Passive Params] -> State f -> State f
sample Int
n [Passive Params]
passives State f
state
{-# INLINEABLE simplifySample #-}
simplifySample :: Function f => State f -> State f
simplifySample :: State f -> State f
simplifySample state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
State f
state{st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_cp_sample = (Maybe (Overlap (Active f) f) -> Maybe (Overlap (Active f) f))
-> Sample (Maybe (Overlap (Active f) f))
-> Sample (Maybe (Overlap (Active f) f))
forall a b. (a -> b) -> Sample a -> Sample b
mapSample (Maybe (Overlap (Active f) f)
-> (Overlap (Active f) f -> Maybe (Overlap (Active f) f))
-> Maybe (Overlap (Active f) f)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Overlap (Active f) f -> Maybe (Overlap (Active f) f)
simp) Sample (Maybe (Overlap (Active f) f))
st_cp_sample}
where
simp :: Overlap (Active f) f -> Maybe (Overlap (Active f) f)
simp Overlap (Active f) f
overlap = do
Overlap (Active f) f
overlap' <- Index f (Rule f)
-> Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall f a b.
(Function f, Has a (Rule f)) =>
Index f a -> Overlap b f -> Maybe (Overlap b f)
simplifyOverlap (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Overlap (Active f) f
overlap
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Overlap (Active f) f -> Equation f
forall a f. Overlap a f -> Equation f
overlap_eqn Overlap (Active f) f
overlap Equation f -> Equation f -> Bool
forall a. Eq a => a -> a -> Bool
== Overlap (Active f) f -> Equation f
forall a f. Overlap a f -> Equation f
overlap_eqn Overlap (Active f) f
overlap')
Overlap (Active f) f -> Maybe (Overlap (Active f) f)
forall (m :: * -> *) a. Monad m => a -> m a
return Overlap (Active f) f
overlap
{-# INLINEABLE addActiveOnly #-}
addActiveOnly :: Function f => State f -> Active f -> State f
addActiveOnly :: State f -> Active f -> State f
addActiveOnly state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
State f
state {
st_rules :: RuleIndex f (Rule f)
st_rules = (RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f))
-> RuleIndex f (Rule f) -> [Rule f] -> RuleIndex f (Rule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
forall f. RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
insertRule RuleIndex f (Rule f)
st_rules (Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules Active f
active),
st_active_set :: IntMap (Active f)
st_active_set = Int -> Active f -> IntMap (Active f) -> IntMap (Active f)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Id -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
active_id) Active f
active IntMap (Active f)
st_active_set }
where
insertRule :: RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
insertRule RuleIndex f (Rule f)
rules Rule f
rule =
Term f -> Rule f -> RuleIndex f (Rule f) -> RuleIndex f (Rule f)
forall f a.
(Symbolic a, ConstantOf a ~ f, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
RuleIndex.insert (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule) Rule f
rule RuleIndex f (Rule f)
rules
{-# INLINE deleteActive #-}
deleteActive :: Function f => State f -> Active f -> State f
deleteActive :: State f -> Active f -> State f
deleteActive state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
State f
state {
st_rules :: RuleIndex f (Rule f)
st_rules = (RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f))
-> RuleIndex f (Rule f) -> [Rule f] -> RuleIndex f (Rule f)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
forall f. RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
deleteRule RuleIndex f (Rule f)
st_rules (Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules Active f
active),
st_active_set :: IntMap (Active f)
st_active_set = Int -> IntMap (Active f) -> IntMap (Active f)
forall a. Int -> IntMap a -> IntMap a
IntMap.delete (Id -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
active_id) IntMap (Active f)
st_active_set }
where
deleteRule :: RuleIndex f (Rule f) -> Rule f -> RuleIndex f (Rule f)
deleteRule RuleIndex f (Rule f)
rules Rule f
rule =
Term f -> Rule f -> RuleIndex f (Rule f) -> RuleIndex f (Rule f)
forall f a.
(Symbolic a, ConstantOf a ~ f, Eq a, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
RuleIndex.delete (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule) Rule f
rule RuleIndex f (Rule f)
rules
{-# INLINEABLE consider #-}
consider :: Function f => Config f -> State f -> Info -> CriticalPair f -> State f
consider :: Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
info CriticalPair f
cp =
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing (State f -> RuleIndex f (Rule f)
forall f. State f -> RuleIndex f (Rule f)
st_rules State f
state) Config f
config State f
state Info
info CriticalPair f
cp
{-# INLINEABLE considerUsing #-}
considerUsing ::
Function f =>
RuleIndex f (Rule f) -> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing :: RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing RuleIndex f (Rule f)
rules config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Info
info CriticalPair f
cp0 =
String -> State f -> State f
forall symbol a. symbol -> a -> a
stamp String
"consider critical pair" (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
let cp :: CriticalPair f
cp = CriticalPair f -> CriticalPair f
forall a. Symbolic a => a -> a
canonicalise CriticalPair f
cp0 in
case Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (Rule f)
-> Maybe (Model f)
-> CriticalPair f
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> CriticalPair f
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
joinCriticalPair Config
cfg_join (Index f (Equation f)
st_joinable, Index f (Rule f)
st_complete) RuleIndex f (Rule f)
rules Maybe (Model f)
forall a. Maybe a
Nothing CriticalPair f
cp of
Right (Maybe (CriticalPair f)
mcp, [CriticalPair f]
cps) ->
let
state' :: State f
state' = (State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
RuleIndex f (Rule f)
-> Config f -> State f -> Info -> CriticalPair f -> State f
considerUsing RuleIndex f (Rule f)
rules Config f
config State f
state Info
info CriticalPair f
cp) State f
state [CriticalPair f]
cps
in case Maybe (CriticalPair f)
mcp of
Just CriticalPair f
cp -> State f -> Equation f -> State f
forall f. Function f => State f -> Equation f -> State f
addJoinable State f
state' (CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp)
Maybe (CriticalPair f)
Nothing -> State f
state'
Left (CriticalPair f
cp, Model f
model) ->
(State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addCP Config f
config Model f
model State f
state Info
info CriticalPair f
cp) State f
state (CriticalPair f -> [CriticalPair f]
forall f. Function f => CriticalPair f -> [CriticalPair f]
split CriticalPair f
cp)
{-# INLINEABLE addCP #-}
addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addCP :: Config f -> Model f -> State f -> Info -> CriticalPair f -> State f
addCP Config f
config Model f
model state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Info
info CriticalPair{Maybe (Term f)
Equation f
Derivation f
cp_proof :: Derivation f
cp_top :: Maybe (Term f)
cp_eqn :: Equation f
cp_proof :: forall f. CriticalPair f -> Derivation f
cp_top :: forall f. CriticalPair f -> Maybe (Term f)
cp_eqn :: forall f. CriticalPair f -> Equation f
..} =
let
pf :: Proof f
pf = Derivation f -> Proof f
forall f. Function f => Derivation f -> Proof f
certify Derivation f
cp_proof
rule :: Rule f
rule = Equation f -> Proof f -> Rule f
forall f. Function f => Equation f -> Proof f -> Rule f
orient Equation f
cp_eqn Proof f
pf
in
Config f -> State f -> (Id -> Active f) -> State f
forall f.
Function f =>
Config f -> State f -> (Id -> Active f) -> State f
addActive Config f
config State f
state ((Id -> Active f) -> State f) -> (Id -> Active f) -> State f
forall a b. (a -> b) -> a -> b
$ \Id
n ->
Active :: forall f.
Id
-> Info
-> Rule f
-> Maybe (Term f)
-> Proof f
-> Model f
-> Positions2 f
-> Active f
Active {
active_id :: Id
active_id = Id
n,
active_info :: Info
active_info = Info
info,
active_rule :: Rule f
active_rule = Rule f
rule,
active_model :: Model f
active_model = Model f
model,
active_top :: Maybe (Term f)
active_top = Maybe (Term f)
cp_top,
active_proof :: Proof f
active_proof = Proof f
pf,
active_positions :: Positions2 f
active_positions = Rule f -> Positions2 f
forall f. Rule f -> Positions2 f
positionsRule Rule f
rule }
{-# INLINEABLE addAxiom #-}
addAxiom :: Function f => Config f -> State f -> Axiom f -> State f
addAxiom :: Config f -> State f -> Axiom f -> State f
addAxiom Config f
config State f
state Axiom f
axiom =
Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state
Info :: Depth -> IntSet -> Info
Info { info_depth :: Depth
info_depth = Depth
0, info_max :: IntSet
info_max = [Int] -> IntSet
IntSet.fromList [Axiom f -> Int
forall f. Axiom f -> Int
axiom_number Axiom f
axiom | Config f -> Bool
forall f. Config f -> Bool
cfg_complete_subsets Config f
config] }
CriticalPair :: forall f.
Equation f -> Maybe (Term f) -> Derivation f -> CriticalPair f
CriticalPair {
cp_eqn :: Equation f
cp_eqn = Axiom f -> Equation f
forall f. Axiom f -> Equation f
axiom_eqn Axiom f
axiom,
cp_top :: Maybe (Term f)
cp_top = Maybe (Term f)
forall a. Maybe a
Nothing,
cp_proof :: Derivation f
cp_proof = Axiom f -> Derivation f
forall f. Axiom f -> Derivation f
Proof.axiom Axiom f
axiom }
{-# INLINEABLE addJoinable #-}
addJoinable :: Function f => State f -> Equation f -> State f
addJoinable :: State f -> Equation f -> State f
addJoinable State f
state eqn :: Equation f
eqn@(Term f
t :=: Term f
u) =
Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Equation f -> Message f
forall f. Equation f -> Message f
NewEquation Equation f
eqn) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f
state {
st_joinable :: Index f (Equation f)
st_joinable =
Term f
-> Equation f -> Index f (Equation f) -> Index f (Equation f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
Term f -> a -> Index f a -> Index f a
Index.insert Term f
t (Term f
t Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
u) (Index f (Equation f) -> Index f (Equation f))
-> Index f (Equation f) -> Index f (Equation f)
forall a b. (a -> b) -> a -> b
$
Term f
-> Equation f -> Index f (Equation f) -> Index f (Equation f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
Term f -> a -> Index f a -> Index f a
Index.insert Term f
u (Term f
u Term f -> Term f -> Equation f
forall f. Term f -> Term f -> Equation f
:=: Term f
t) (State f -> Index f (Equation f)
forall f. State f -> Index f (Equation f)
st_joinable State f
state) }
{-# INLINEABLE checkCompleteness #-}
checkCompleteness :: Function f => Config f -> State f -> State f
checkCompleteness :: Config f -> State f -> State f
checkCompleteness Config f
_ state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} | Id
st_simplified_at Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
st_next_active = State f
state
checkCompleteness Config f
_config State f
state =
State f
state { st_not_complete :: IntSet
st_not_complete = IntSet
excluded,
st_complete :: Index f (Rule f)
st_complete = (Rule f -> Term f) -> [Rule f] -> Index f (Rule f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
(a -> Term f) -> [a] -> Index f a
Index.fromListWith Rule f -> Term f
forall f. Rule f -> Term f
lhs [Rule f]
rules }
where
maxSet :: IntSet -> Int
maxSet IntSet
s = if IntSet -> Bool
IntSet.null IntSet
s then Int
forall a. Bounded a => a
minBound else IntSet -> Int
IntSet.findMax IntSet
s
maxN :: Int
maxN = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [IntSet -> Int
maxSet (Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r)) | Active f
r <- IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
forall f. State f -> IntMap (Active f)
st_active_set State f
state)]
excluded :: IntSet
excluded = IntSet -> IntSet
go IntSet
IntSet.empty
go :: IntSet -> IntSet
go IntSet
excl
| Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxN = IntSet
excl
| Bool
otherwise = IntSet -> IntSet
go (Int -> IntSet -> IntSet
IntSet.insert Int
m IntSet
excl)
where
m :: Int
m = IntSet -> Int
bound IntSet
excl
bound :: IntSet -> Int
bound IntSet
excl = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Int] -> Int) -> (Queue Params -> [Int]) -> Queue Params -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Passive Params -> Int) -> [Passive Params] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (IntSet -> Passive Params -> Int
passiveMax IntSet
excl) ([Passive Params] -> [Int])
-> (Queue Params -> [Passive Params]) -> Queue Params -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, [Passive Params]) -> [Passive Params])
-> [(Int, [Passive Params])] -> [Passive Params]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, [Passive Params]) -> [Passive Params]
forall a b. (a, b) -> b
snd ([(Int, [Passive Params])] -> [Passive Params])
-> (Queue Params -> [(Int, [Passive Params])])
-> Queue Params
-> [Passive Params]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Queue Params -> [(Int, [Passive Params])]
forall params.
Params params =>
Queue params -> [(Int, [Passive params])]
Queue.toList (Queue Params -> Int) -> Queue Params -> Int
forall a b. (a -> b) -> a -> b
$ State f -> Queue Params
forall f. State f -> Queue Params
st_queue State f
state
passiveMax :: IntSet -> Passive Params -> Int
passiveMax IntSet
excl Passive Params
p = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. Bounded a => a
maxBound (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ do
Overlap{overlap_rule1 :: forall a f. Overlap a f -> a
overlap_rule1 = Active f
r1, overlap_rule2 :: forall a f. Overlap a f -> a
overlap_rule2 = Active f
r2} <- State f -> Passive Params -> Maybe (Overlap (Active f) f)
forall f.
Function f =>
State f -> Passive Params -> Maybe (Overlap (Active f) f)
findPassive State f
state Passive Params
p
let s :: IntSet
s = Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r1) IntSet -> IntSet -> IntSet
`IntSet.union` Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r2)
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (IntSet
s IntSet -> IntSet -> Bool
`IntSet.disjoint` IntSet
excl)
(Int
n, IntSet
_) <- IntSet -> Maybe (Int, IntSet)
IntSet.maxView IntSet
s
Int -> Maybe Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
rules :: [Rule f]
rules = (Active f -> [Rule f]) -> [Active f] -> [Rule f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules ((Active f -> Bool) -> [Active f] -> [Active f]
forall a. (a -> Bool) -> [a] -> [a]
filter Active f -> Bool
ok (IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
forall f. State f -> IntMap (Active f)
st_active_set State f
state)))
ok :: Active f -> Bool
ok Active f
r = Info -> IntSet
info_max (Active f -> Info
forall f. Active f -> Info
active_info Active f
r) IntSet -> IntSet -> Bool
`IntSet.disjoint` IntSet
excluded
{-# INLINEABLE assumeComplete #-}
assumeComplete :: Function f => State f -> State f
assumeComplete :: State f -> State f
assumeComplete State f
state =
State f
state { st_not_complete :: IntSet
st_not_complete = IntSet
IntSet.empty,
st_complete :: Index f (Rule f)
st_complete = (Rule f -> Term f) -> [Rule f] -> Index f (Rule f)
forall a f.
(Symbolic a, ConstantOf a ~ f) =>
(a -> Term f) -> [a] -> Index f a
Index.fromListWith Rule f -> Term f
forall f. Rule f -> Term f
lhs ((Active f -> [Rule f]) -> [Active f] -> [Rule f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Active f -> [Rule f]
forall f. Active f -> [Rule f]
activeRules (IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
forall f. State f -> IntMap (Active f)
st_active_set State f
state))) }
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
{-# INLINEABLE addGoal #-}
addGoal :: Function f => Config f -> State f -> Goal f -> State f
addGoal :: Config f -> State f -> Goal f -> State f
addGoal Config f
config state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Goal f
goal =
Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
normaliseGoals Config f
config State f
state { st_goals :: [Goal f]
st_goals = Goal f
goalGoal f -> [Goal f] -> [Goal f]
forall a. a -> [a] -> [a]
:[Goal f]
st_goals }
{-# INLINEABLE normaliseGoals #-}
normaliseGoals :: Function f => Config f -> State f -> State f
normaliseGoals :: Config f -> State f -> State f
normaliseGoals Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} =
State f
state {
st_goals :: [Goal f]
st_goals =
(Goal f -> Goal f) -> [Goal f] -> [Goal f]
forall a b. (a -> b) -> [a] -> [b]
map ((Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f))
-> Goal f -> Goal f
forall f.
(Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f))
-> Goal f -> Goal f
goalMap (Strategy f
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
nf ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)))) [Goal f]
st_goals }
where
goalMap :: (Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f))
-> Goal f -> Goal f
goalMap Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
f goal :: Goal f
goal@Goal{Int
String
Map (Term f) (Term f, Reduction f)
Map (Term f) (Derivation f)
Equation f
goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} =
Goal f
goal { goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_lhs = Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
f Map (Term f) (Term f, Reduction f)
goal_lhs, goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_rhs = Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
f Map (Term f) (Term f, Reduction f)
goal_rhs }
nf :: Strategy f
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
nf Strategy f
reduce Map (Term f) (Term f, Reduction f)
goals
| Bool
cfg_set_join_goals =
let pair :: (Term f, Reduction f) -> (Term f, Reduction f)
pair (Term f
t, Reduction f
red) = ((Term f, Reduction f) -> Term f
forall a b. (a, b) -> a
fst (Map (Term f) (Term f, Reduction f)
goals Map (Term f) (Term f, Reduction f)
-> Term f -> (Term f, Reduction f)
forall k a. Ord k => Map k a -> k -> a
Map.! Term f
t), Reduction f
red) in
((Term f, Reduction f) -> (Term f, Reduction f))
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> (Term f, Reduction f)
pair (Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f))
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall a b. (a -> b) -> a -> b
$ Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
Rule.normalForms Strategy f
reduce (((Term f, Reduction f) -> Reduction f)
-> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> Reduction f
forall a b. (a, b) -> b
snd Map (Term f) (Term f, Reduction f)
goals)
| Bool
otherwise =
[(Term f, (Term f, Reduction f))]
-> Map (Term f) (Term f, Reduction f)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Term f, (Term f, Reduction f))]
-> Map (Term f) (Term f, Reduction f))
-> [(Term f, (Term f, Reduction f))]
-> Map (Term f) (Term f, Reduction f)
forall a b. (a -> b) -> a -> b
$
[ (Term f -> Reduction f -> Term f
forall f. Term f -> Reduction f -> Term f
result Term f
t Reduction f
q, (Term f
u, Reduction f
r Reduction f -> Reduction f -> Reduction f
forall f. Reduction f -> Reduction f -> Reduction f
`trans` Reduction f
q))
| (Term f
t, (Term f
u, Reduction f
r)) <- Map (Term f) (Term f, Reduction f)
-> [(Term f, (Term f, Reduction f))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Term f, Reduction f)
goals,
let q :: Reduction f
q = (Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
Rule.normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) Strategy f
reduce Term f
t ]
{-# 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 =
[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
{-# INLINEABLE rewriteGoalsBackwards #-}
rewriteGoalsBackwards :: Function f => State f -> State f
rewriteGoalsBackwards :: State f -> State f
rewriteGoalsBackwards State f
state =
State f
state { st_goals :: [Goal f]
st_goals = (Goal f -> Goal f) -> [Goal f] -> [Goal f]
forall a b. (a -> b) -> [a] -> [b]
map Goal f -> Goal f
backwardsGoal (State f -> [Goal f]
forall f. State f -> [Goal f]
st_goals State f
state) }
where
backwardsGoal :: Goal f -> Goal f
backwardsGoal goal :: Goal f
goal@Goal{Int
String
Map (Term f) (Term f, Reduction f)
Map (Term f) (Derivation f)
Equation f
goal_rhs :: Map (Term f) (Term f, Reduction f)
goal_lhs :: Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} =
Goal f -> Goal f
forall f. Goal f -> Goal f
resetGoal Goal f
goal {
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_expanded_lhs = Map (Term f) (Derivation f) -> Map (Term f) (Derivation f)
backwardsMap Map (Term f) (Derivation f)
goal_expanded_lhs,
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_rhs = Map (Term f) (Derivation f) -> Map (Term f) (Derivation f)
backwardsMap Map (Term f) (Derivation f)
goal_expanded_rhs }
backwardsMap :: Map (Term f) (Derivation f) -> Map (Term f) (Derivation f)
backwardsMap Map (Term f) (Derivation f)
m =
[(Term f, Derivation f)] -> Map (Term f) (Derivation f)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Term f, Derivation f)] -> Map (Term f) (Derivation f))
-> [(Term f, Derivation f)] -> Map (Term f) (Derivation f)
forall a b. (a -> b) -> a -> b
$
Map (Term f) (Derivation f) -> [(Term f, Derivation f)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Derivation f)
m [(Term f, Derivation f)]
-> [(Term f, Derivation f)] -> [(Term f, Derivation f)]
forall a. [a] -> [a] -> [a]
++
[ (Term f -> Rule f -> Term f
forall f. Term f -> Rule f -> Term f
ruleResult Term f
t Rule f
r, Derivation f
p Derivation f -> Derivation f -> Derivation f
forall f. Derivation f -> Derivation f -> Derivation f
`Proof.trans` Derivation f
q)
| (Term f
t, Derivation f
p) <- Map (Term f) (Derivation f) -> [(Term f, Derivation f)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Term f) (Derivation f)
m,
Rule f
r <- Term f -> Reduction f
backwardsTerm Term f
t,
let q :: Derivation f
q = Term f -> Rule f -> Derivation f
forall f. Function f => Term f -> Rule f -> Derivation f
ruleProof Term f
t Rule f
r ]
backwardsTerm :: Term f -> Reduction f
backwardsTerm Term f
t = do
Rule f
rule <- (Rule f -> Rule f) -> Reduction f -> Reduction f
forall a b. (a -> b) -> [a] -> [b]
map Rule f -> Rule f
forall a b. Has a b => a -> b
the (Index f (Rule f) -> Reduction f
forall f a. Index f a -> [a]
Index.elems (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
RuleIndex.index_all (State f -> RuleIndex f (Rule f)
forall f. State f -> RuleIndex f (Rule f)
st_rules State f
state)))
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars (Rule f -> Term f
forall f. Rule f -> Term f
lhs Rule f
rule)) [Var] -> [Var] -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (Term f -> [Var]
forall a. Symbolic a => a -> [Var]
vars (Rule f -> Term f
forall f. Rule f -> Term f
rhs Rule f
rule)))
[Rule f
r] <- Strategy f -> Strategy f
forall f. Strategy f -> Strategy f
anywhere ((Rule f -> Subst f -> Bool) -> Rule f -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> a -> Strategy f
tryRule (\Rule f
_ Subst f
_ -> Bool
True) (Rule f -> Rule f
forall f. Rule f -> Rule f
backwards Rule f
rule)) Term f
t
Rule f -> Reduction f
forall (m :: * -> *) a. Monad m => a -> m a
return Rule f
r
{-# 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, []) }
{-# INLINEABLE interreduce #-}
interreduce :: Function f => Config f -> State f -> State f
interreduce :: Config f -> State f -> State f
interreduce Config f
_ state :: State f
state@State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} | Id
st_simplified_at Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
st_next_active = State f
state
interreduce config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state =
let
state' :: State f
state' =
(State f -> Active f -> State f)
-> State f -> [Active f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Config f -> State f -> Active f -> State f
forall f. Function f => Config f -> State f -> Active f -> State f
interreduce1 Config f
config)
State f
state { st_joinable :: Index f (Equation f)
st_joinable = Index f (Equation f)
forall f a. Index f a
Index.empty, st_complete :: Index f (Rule f)
st_complete = Index f (Rule f)
forall f a. Index f a
Index.empty }
(IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (State f -> IntMap (Active f)
forall f. State f -> IntMap (Active f)
st_active_set State f
state))
in State f
state' { st_joinable :: Index f (Equation f)
st_joinable = State f -> Index f (Equation f)
forall f. State f -> Index f (Equation f)
st_joinable State f
state, st_complete :: Index f (Rule f)
st_complete = State f -> Index f (Rule f)
forall f. State f -> Index f (Rule f)
st_complete State f
state, st_simplified_at :: Id
st_simplified_at = State f -> Id
forall f. State f -> Id
st_next_active State f
state' }
{-# INLINEABLE interreduce1 #-}
interreduce1 :: Function f => Config f -> State f -> Active f -> State f
interreduce1 :: Config f -> State f -> Active f -> State f
interreduce1 config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state active :: Active f
active@Active{Maybe (Term f)
Model f
Id
Proof f
Rule f
Positions2 f
Info
active_positions :: Positions2 f
active_model :: Model f
active_proof :: Proof f
active_top :: Maybe (Term f)
active_rule :: Rule f
active_info :: Info
active_id :: Id
active_positions :: forall f. Active f -> Positions2 f
active_model :: forall f. Active f -> Model f
active_proof :: forall f. Active f -> Proof f
active_top :: forall f. Active f -> Maybe (Term f)
active_rule :: forall f. Active f -> Rule f
active_info :: forall f. Active f -> Info
active_id :: forall f. Active f -> Id
..} =
case
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f (Rule f)
-> Maybe (Model f)
-> CriticalPair f
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
forall f a.
(Function f, Has a (Rule f)) =>
Config
-> (Index f (Equation f), Index f (Rule f))
-> RuleIndex f a
-> Maybe (Model f)
-> CriticalPair f
-> Either
(CriticalPair f, Model f)
(Maybe (CriticalPair f), [CriticalPair f])
joinCriticalPair Config
cfg_join
(Index f (Equation f)
forall f a. Index f a
Index.empty, Index f (Rule f)
forall f a. Index f a
Index.empty)
(State f -> RuleIndex f (Rule f)
forall f. State f -> RuleIndex f (Rule f)
st_rules (State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active))
(Model f -> Maybe (Model f)
forall a. a -> Maybe a
Just Model f
active_model) (Active f -> CriticalPair f
forall f. Active f -> CriticalPair f
active_cp Active f
active)
of
Right (Maybe (CriticalPair f)
_, [CriticalPair f]
cps) ->
(State f -> [CriticalPair f] -> State f)
-> [CriticalPair f] -> State f -> State f
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
active_info CriticalPair f
cp)) [CriticalPair f]
cps (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Active f -> Message f
forall f. Active f -> Message f
DeleteActive Active f
active) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
Left (CriticalPair f
cp, Model f
model)
| CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn CriticalPair f
cp Equation f -> Equation f -> Bool
forall f. Function f => Equation f -> Equation f -> Bool
`simplerThan` CriticalPair f -> Equation f
forall f. CriticalPair f -> Equation f
cp_eqn (Active f -> CriticalPair f
forall f. Active f -> CriticalPair f
active_cp Active f
active) ->
(State f -> [CriticalPair f] -> State f)
-> [CriticalPair f] -> State f -> State f
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((State f -> CriticalPair f -> State f)
-> State f -> [CriticalPair f] -> State f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\State f
state CriticalPair f
cp -> Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
active_info CriticalPair f
cp)) (CriticalPair f -> [CriticalPair f]
forall f. Function f => CriticalPair f -> [CriticalPair f]
split CriticalPair f
cp) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
Message f -> State f -> State f
forall f. PrettyTerm f => Message f -> State f -> State f
message (Active f -> Message f
forall f. Active f -> Message f
DeleteActive Active f
active) (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
| Model f
model Model f -> Model f -> Bool
forall a. Eq a => a -> a -> Bool
/= Model f
active_model ->
(State f -> Active f -> State f) -> Active f -> State f -> State f
forall a b c. (a -> b -> c) -> b -> a -> c
flip State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
addActiveOnly Active f
active { active_model :: Model f
active_model = Model f
model } (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$
State f -> Active f -> State f
forall f. Function f => State f -> Active f -> State f
deleteActive State f
state Active f
active
| Bool
otherwise ->
State f
state
data Output m f =
Output {
Output m f -> Message f -> m ()
output_message :: Message f -> m () }
{-# INLINE complete #-}
complete :: (Function f, MonadIO m) => Output m f -> Config f -> State f -> m (State f)
complete :: Output m f -> Config f -> State f -> m (State f)
complete Output{Message f -> m ()
output_message :: Message f -> m ()
output_message :: forall (m :: * -> *) f. Output m f -> Message f -> m ()
..} config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state =
(StateT (State f) m () -> State f -> m (State f))
-> State f -> StateT (State f) m () -> m (State f)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (State f) m () -> State f -> m (State f)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
StateM.execStateT State f
state (StateT (State f) m () -> m (State f))
-> StateT (State f) m () -> m (State f)
forall a b. (a -> b) -> a -> b
$ do
[Task (StateT (State f) m) ()]
tasks <- [StateT (State f) m (Task (StateT (State f) m) ())]
-> StateT (State f) m [Task (StateT (State f) m) ()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
[Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
10 (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
cfg_renormalise_percent Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Double
100) (StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config f -> State f -> Bool
forall f. Function f => Config f -> State f -> Bool
shouldSimplifyQueue Config f
config State f
state) (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message Message f
forall f. Message f
SimplifyQueue
State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
simplifyQueue Config f
config State f
state,
Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.02 (StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_complete_subsets (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
let !state' :: State f
state' = Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
checkCompleteness Config f
config State f
state
m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message (IntSet -> Message f
forall f. IntSet -> Message f
NotComplete (State f -> IntSet
forall f. State f -> IntSet
st_not_complete State f
state'))
State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! State f
state',
Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.05 (StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_simplify (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message Message f
forall f. Message f
Interreduce
State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! State f -> State f
forall f. Function f => State f -> State f
simplifySample (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
interreduce Config f
config State f
state,
Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
1 Double
0.02 (StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
recomputeGoals Config f
config State f
state,
Double
-> Double
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall (m :: * -> *) a.
MonadIO m =>
Double -> Double -> m a -> m (Task m a)
newTask Double
60 Double
0.01 (StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ()))
-> StateT (State f) m ()
-> StateT (State f) m (Task (StateT (State f) m) ())
forall a b. (a -> b) -> a -> b
$ do
State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
let !n :: Int
n = Queue Params -> Int
forall params. Params params => Queue params -> Int
Queue.queueSize Queue Params
st_queue
m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message (Int -> Message f
forall f. Int -> Message f
Status Int
n)]
let
loop :: StateT (State f) m ()
loop = do
Bool
progress <- (State f -> (Bool, State f)) -> StateT (State f) m Bool
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
StateM.state (Config f -> State f -> (Bool, State f)
forall f. Function f => Config f -> State f -> (Bool, State f)
complete1 Config f
config)
Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
cfg_always_simplify (StateT (State f) m () -> StateT (State f) m ())
-> StateT (State f) m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ do
m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ Message f -> m ()
output_message Message f
forall f. Message f
Interreduce
State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> StateT (State f) m ())
-> State f -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$! State f -> State f
forall f. Function f => State f -> State f
simplifySample (State f -> State f) -> State f -> State f
forall a b. (a -> b) -> a -> b
$! Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
interreduce Config f
config State f
state
State f
state <- StateT (State f) m (State f)
forall (m :: * -> *) s. Monad m => StateT s m s
StateM.get
m () -> StateT (State f) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT (State f) m ()) -> m () -> StateT (State f) m ()
forall a b. (a -> b) -> a -> b
$ (Message f -> m ()) -> [Message f] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Message f -> m ()
output_message (State f -> [Message f]
forall f. State f -> [Message f]
messages State f
state)
State f -> StateT (State f) m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
StateM.put (State f -> State f
forall f. State f -> State f
clearMessages State f
state)
(Task (StateT (State f) m) () -> StateT (State f) m (Maybe ()))
-> [Task (StateT (State f) m) ()] -> StateT (State f) m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Task (StateT (State f) m) () -> StateT (State f) m (Maybe ())
forall (m :: * -> *) a. MonadIO m => Task m a -> m (Maybe a)
checkTask [Task (StateT (State f) m) ()]
tasks
Bool -> StateT (State f) m () -> StateT (State f) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
progress StateT (State f) m ()
loop
StateT (State f) m ()
loop
{-# INLINEABLE complete1 #-}
complete1 :: Function f => Config f -> State f -> (Bool, State f)
complete1 :: Config f -> State f -> (Bool, State f)
complete1 config :: Config f
config@Config{Bool
Int
Int64
Maybe (Term f -> Bool)
Config f
Config
Config
cfg_proof_presentation :: Config f
cfg_join :: Config
cfg_critical_pairs :: Config
cfg_complete_subsets :: Bool
cfg_always_simplify :: Bool
cfg_set_join_goals :: Bool
cfg_renormalise_threshold :: Int
cfg_cp_sample_size :: Int
cfg_renormalise_percent :: Int
cfg_simplify :: Bool
cfg_max_cp_depth :: Int
cfg_max_critical_pairs :: Int64
cfg_accept_term :: Maybe (Term f -> Bool)
cfg_proof_presentation :: forall f. Config f -> Config f
cfg_join :: forall f. Config f -> Config
cfg_critical_pairs :: forall f. Config f -> Config
cfg_complete_subsets :: forall f. Config f -> Bool
cfg_always_simplify :: forall f. Config f -> Bool
cfg_set_join_goals :: forall f. Config f -> Bool
cfg_renormalise_threshold :: forall f. Config f -> Int
cfg_cp_sample_size :: forall f. Config f -> Int
cfg_renormalise_percent :: forall f. Config f -> Int
cfg_simplify :: forall f. Config f -> Bool
cfg_max_cp_depth :: forall f. Config f -> Int
cfg_max_critical_pairs :: forall f. Config f -> Int64
cfg_accept_term :: forall f. Config f -> Maybe (Term f -> Bool)
..} State f
state
| State f -> Int64
forall f. State f -> Int64
st_considered State f
state Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
>= Int64
cfg_max_critical_pairs =
(Bool
False, State f
state)
| State f -> Bool
forall f. Function f => State f -> Bool
solved State f
state = (Bool
False, State f
state)
| Bool
otherwise =
case Config f
-> State f
-> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
forall f.
Function f =>
Config f
-> State f
-> (Maybe (Info, CriticalPair f, Active f, Active f), State f)
dequeue Config f
config State f
state of
(Maybe (Info, CriticalPair f, Active f, Active f)
Nothing, State f
state) -> (Bool
False, State f
state)
(Just (Info
info, CriticalPair f
overlap, Active f
_, Active f
_), State f
state) ->
(Bool
True, Config f -> State f -> Info -> CriticalPair f -> State f
forall f.
Function f =>
Config f -> State f -> Info -> CriticalPair f -> State f
consider Config f
config State f
state Info
info CriticalPair f
overlap)
{-# INLINEABLE solved #-}
solved :: Function f => State f -> Bool
solved :: State f -> Bool
solved = Bool -> Bool
not (Bool -> Bool) -> (State f -> Bool) -> State f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ProvedGoal f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([ProvedGoal f] -> Bool)
-> (State f -> [ProvedGoal f]) -> State f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State f -> [ProvedGoal f]
forall f. Function f => State f -> [ProvedGoal f]
solutions
{-# INLINEABLE solutions #-}
solutions :: Function f => State f -> [ProvedGoal f]
solutions :: State f -> [ProvedGoal f]
solutions State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} = do
Goal{goal_lhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_lhs = Map (Term f) (Term f, Reduction f)
ts, goal_rhs :: forall f. Goal f -> Map (Term f) (Term f, Reduction f)
goal_rhs = Map (Term f) (Term f, Reduction f)
us, Int
String
Map (Term f) (Derivation f)
Equation f
goal_expanded_rhs :: Map (Term f) (Derivation f)
goal_expanded_lhs :: Map (Term f) (Derivation f)
goal_eqn :: Equation f
goal_number :: Int
goal_name :: String
goal_expanded_rhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_expanded_lhs :: forall f. Goal f -> Map (Term f) (Derivation f)
goal_eqn :: forall f. Goal f -> Equation f
goal_number :: forall f. Goal f -> Int
goal_name :: forall f. Goal f -> String
..} <- [Goal f]
st_goals
let sols :: [Term f]
sols = Map (Term f) (Term f, Reduction f) -> [Term f]
forall k a. Map k a -> [k]
Map.keys (Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
-> Map (Term f) (Term f, Reduction f)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Map (Term f) (Term f, Reduction f)
ts Map (Term f) (Term f, Reduction f)
us)
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ([Term f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term f]
sols))
let Term f
sol:[Term f]
_ = [Term f]
sols
let t :: (Term f, Reduction f)
t = Map (Term f) (Term f, Reduction f)
ts Map (Term f) (Term f, Reduction f)
-> Term f -> (Term f, Reduction f)
forall k a. Ord k => Map k a -> k -> a
Map.! Term f
sol
u :: (Term f, Reduction f)
u = Map (Term f) (Term f, Reduction f)
us Map (Term f) (Term f, Reduction f)
-> Term f -> (Term f, Reduction f)
forall k a. Ord k => Map k a -> k -> a
Map.! Term f
sol
!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
{-# INLINEABLE rules #-}
rules :: Function f => State f -> [Rule f]
rules :: State f -> [Rule f]
rules = (Active f -> Rule f) -> [Active f] -> [Rule f]
forall a b. (a -> b) -> [a] -> [b]
map Active f -> Rule f
forall f. Active f -> Rule f
active_rule ([Active f] -> [Rule f])
-> (State f -> [Active f]) -> State f -> [Rule f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntMap (Active f) -> [Active f]
forall a. IntMap a -> [a]
IntMap.elems (IntMap (Active f) -> [Active f])
-> (State f -> IntMap (Active f)) -> State f -> [Active f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State f -> IntMap (Active f)
forall f. State f -> IntMap (Active f)
st_active_set
{-# INLINEABLE completePure #-}
completePure :: Function f => Config f -> State f -> State f
completePure :: Config f -> State f -> State f
completePure Config f
cfg State f
state
| Bool
progress = Config f -> State f -> State f
forall f. Function f => Config f -> State f -> State f
completePure Config f
cfg (State f -> State f
forall f. State f -> State f
clearMessages State f
state')
| Bool
otherwise = State f
state'
where
(Bool
progress, State f
state') = Config f -> State f -> (Bool, State f)
forall f. Function f => Config f -> State f -> (Bool, State f)
complete1 Config f
cfg State f
state
{-# INLINEABLE normaliseTerm #-}
normaliseTerm :: Function f => State f -> Term f -> Reduction f
normaliseTerm :: State f -> Term f -> Reduction f
normaliseTerm State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Term f
t =
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
forall f.
Function f =>
(Term f -> Bool) -> Strategy f -> Term f -> Reduction f
normaliseWith (Bool -> Term f -> Bool
forall a b. a -> b -> a
const Bool
True) ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)) Term f
t
{-# INLINEABLE normalForms #-}
normalForms :: Function f => State f -> Term f -> Map (Term f) (Reduction f)
normalForms :: State f -> Term f -> Map (Term f) (Reduction f)
normalForms State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Term f
t =
((Term f, Reduction f) -> Reduction f)
-> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Term f, Reduction f) -> Reduction f
forall a b. (a, b) -> b
snd (Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f))
-> Map (Term f) (Term f, Reduction f) -> Map (Term f) (Reduction f)
forall a b. (a -> b) -> a -> b
$
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
forall f.
Function f =>
Strategy f
-> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)
Rule.normalForms ((Rule f -> Subst f -> Bool) -> Index f (Rule f) -> Strategy f
forall f a.
(Function f, Has a (Rule f)) =>
(Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
rewrite Rule f -> Subst f -> Bool
forall f. Function f => Rule f -> Subst f -> Bool
reduces (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_all RuleIndex f (Rule f)
st_rules)) (Term f -> Reduction f -> Map (Term f) (Reduction f)
forall k a. k -> a -> Map k a
Map.singleton Term f
t [])
{-# INLINEABLE simplifyTerm #-}
simplifyTerm :: Function f => State f -> Term f -> Term f
simplifyTerm :: State f -> Term f -> Term f
simplifyTerm State{Int64
[Goal f]
[Message f]
IntMap (Active f)
IntSet
Sample (Maybe (Overlap (Active f) f))
Queue Params
Id
Index f (Equation f)
Index f (Rule f)
RuleIndex f (Rule f)
st_messages_rev :: [Message f]
st_complete :: Index f (Rule f)
st_not_complete :: IntSet
st_cp_sample :: Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: Id
st_considered :: Int64
st_next_active :: Id
st_queue :: Queue Params
st_goals :: [Goal f]
st_joinable :: Index f (Equation f)
st_active_set :: IntMap (Active f)
st_rules :: RuleIndex f (Rule f)
st_messages_rev :: forall f. State f -> [Message f]
st_complete :: forall f. State f -> Index f (Rule f)
st_not_complete :: forall f. State f -> IntSet
st_cp_sample :: forall f. State f -> Sample (Maybe (Overlap (Active f) f))
st_simplified_at :: forall f. State f -> Id
st_considered :: forall f. State f -> Int64
st_next_active :: forall f. State f -> Id
st_queue :: forall f. State f -> Queue Params
st_goals :: forall f. State f -> [Goal f]
st_joinable :: forall f. State f -> Index f (Equation f)
st_active_set :: forall f. State f -> IntMap (Active f)
st_rules :: forall f. State f -> RuleIndex f (Rule f)
..} Term f
t =
Index f (Rule f) -> Term f -> Term f
forall f a.
(Function f, Has a (Rule f)) =>
Index f a -> Term f -> Term f
simplify (RuleIndex f (Rule f) -> Index f (Rule f)
forall f a. RuleIndex f a -> Index f a
index_oriented RuleIndex f (Rule f)
st_rules) Term f
t