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