packages feed

twee-lib 2.4.1 → 2.4.2

raw patch · 15 files changed

+393/−270 lines, 15 filesdep +bytestringdep +cerealdep −vectordep ~basedep ~containers

Dependencies added: bytestring, cereal

Dependencies removed: vector

Dependency ranges changed: base, containers

Files

+ Data/BatchedQueue.hs view
@@ -0,0 +1,145 @@+-- | A queue where entries can be added in batches and stored compactly.+{-# LANGUAGE TypeFamilies, RecordWildCards, FlexibleContexts, ScopedTypeVariables #-}+module Data.BatchedQueue(+  Queue, Batch(..), StandardBatch, unbatch, empty, insert, removeMin, removeMinFilter, mapMaybe, toBatches, toList, size) where++import qualified Data.Heap as Heap+import Data.List(unfoldr, sort, foldl')+import qualified Data.Maybe+import Data.PackedSequence(PackedSequence)+import qualified Data.PackedSequence as PackedSequence+import Data.Serialize+import Data.Ord++-- | A queue of batches.+newtype Queue a = Queue (Heap.Heap (Best a))++-- | The type of batches must be a member of this class.+class Ord (Entry a) => Batch a where+  -- | Each batch can have an associated label,+  -- which is specified when calling 'insert'.+  -- A label represents a piece of information which is+  -- shared in common between all entries in a batch,+  -- and which might be used to store that batch more+  -- efficiently. +  -- Labels are optional, and by default @Label a = ()@.+  type Label a++  -- | Individual entries in the batch.+  type Entry a++  -- | Given a label, and a non-empty list of entries,+  -- sorted in ascending order, produce a list of batches.+  makeBatch :: Label a -> [Entry a] -> [a]++  -- | Remove the smallest entry from a batch.+  unconsBatch :: a -> (Entry a, Maybe a)+  +  -- | Return the label of a batch.+  batchLabel :: a -> Label a++  -- | Compute the size of a batch. Used in 'size'.+  -- The default implementation works by repeatedly calling+  -- 'unconsBatch'.+  batchSize :: a -> Int+  batchSize = length . unbatch++  type Label a = ()++-- A newtype wrapper for batches which compares the smallest entry.+newtype Best a = Best { unBest :: a }+instance Batch a => Eq (Best a) where x == y = compare x y == EQ+instance Batch a => Ord (Best a) where+  {-# INLINEABLE compare #-}+  compare = comparing (fst . unconsBatch . unBest)++-- | Convert a batch into a list of entries.+{-# INLINEABLE unbatch #-}+unbatch :: Batch a => a -> [Entry a]+unbatch batch = unfoldr (fmap unconsBatch) (Just batch)++-- | The empty queue.+empty :: Queue a+empty = Queue Heap.empty++-- | Add entries to the queue.+{-# INLINEABLE insert #-}+insert :: forall a. Batch a => Label a -> [Entry a] -> Queue a -> Queue a+insert _ [] q = q+insert l is (Queue q) =+  Queue $ foldl' (flip (Heap.insert . Best)) q (makeBatch l (sort is))++-- | Remove the minimum entry from the queue.+{-# INLINEABLE removeMin #-}+removeMin :: Batch a => Queue a -> Maybe (Entry a, Queue a)+removeMin q = removeMinFilter (const True) q++-- | Remove the minimum entry from the queue, discarding any+-- batches that do not satisfy the predicate.+{-# INLINEABLE removeMinFilter #-}+removeMinFilter :: Batch a => (Label a -> Bool) -> Queue a -> Maybe (Entry a, Queue a)+removeMinFilter ok (Queue q) = do+  (Best batch, q) <- Heap.removeMin q+  if not (ok (batchLabel batch)) then removeMinFilter ok (Queue q) else+    case unconsBatch batch of+      (entry, Just batch') ->+        Just (entry, Queue (Heap.insert (Best batch') q))+      (entry, Nothing) ->+        Just (entry, Queue q)++-- | Map a function over all entries.+-- The function must preserve the label of each batch,+-- and must not split existing batches into two.+{-# INLINEABLE mapMaybe #-}+mapMaybe :: Batch a => (Entry a -> Maybe (Entry a)) -> Queue a -> Queue a+mapMaybe f (Queue q) = Queue (Heap.mapMaybe g q)+  where+    g (Best batch) =+      case Data.Maybe.mapMaybe f (unbatch batch) of+        [] -> Nothing+        is ->+          case makeBatch (batchLabel batch) (sort is) of+            [] -> Nothing+            [batch'] -> Just (Best batch')+            _ -> error "multiple batches produced"++-- | Convert a queue into a list of batches, in unspecified order.+{-# INLINEABLE toBatches #-}+toBatches :: Queue a -> [a]+toBatches (Queue q) = map unBest (Heap.toList q)++-- | Convert a queue into a list of entries, in unspecified order.+{-# INLINEABLE toList #-}+toList :: Batch a => Queue a -> [Entry a]+toList q = concatMap unbatch (toBatches q)++{-# INLINEABLE size #-}+size :: Batch a => Queue a -> Int+size = sum . map batchSize . toBatches++-- | A "standard" type of batches. By using @Queue (StandardBatch a)@,+-- you will get a queue where entries have type @a@ and labels have+-- type @()@.+data StandardBatch a =+  StandardBatch {+    batch_best :: !a,+    batch_rest :: {-# UNPACK #-} !(PackedSequence a) }++instance Ord a => Eq (StandardBatch a) where+  x == y = compare x y == EQ+instance Ord a => Ord (StandardBatch a) where+  compare = comparing batch_best++instance (Ord a, Serialize a) => Batch (StandardBatch a) where+  type Label (StandardBatch a) = ()+  type Entry (StandardBatch a) = a++  makeBatch _ (x:xs) = [StandardBatch x (PackedSequence.fromList xs)]+  unconsBatch StandardBatch{..} =+    (batch_best,+     case PackedSequence.uncons batch_rest of+       Nothing -> Nothing+       Just (x, xs) -> Just (StandardBatch x xs))+  batchLabel _ = ()+  batchSize StandardBatch{..} = 1 + PackedSequence.size batch_rest+
Data/ChurchList.hs view
@@ -48,13 +48,11 @@  instance Applicative ChurchList where   {-# INLINE pure #-}-  pure = return+  pure = unit   {-# INLINE (<*>) #-}   (<*>) = liftM2 ($)  instance Monad ChurchList where-  {-# INLINE return #-}-  return = unit   {-# INLINE (>>=) #-}   xs >>= f = join (fmap f xs)
Data/Label.hs view
@@ -1,7 +1,7 @@ -- | Assignment of unique IDs to values. -- Inspired by the 'intern' package. -{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations #-}+{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP #-} module Data.Label(Label, unsafeMkLabel, labelNum, label, find) where  import Data.IORef@@ -124,7 +124,11 @@ find (Label !(I32# n#)) = findWorker n#  {-# NOINLINE findWorker #-}+#if __GLASGOW_HASKELL__ >= 902+findWorker :: Int32# -> a+#else findWorker :: Int# -> a+#endif findWorker n# =   unsafeDupablePerformIO $ do     let n = I32# n#
Data/Numbered.hs view
@@ -1,3 +1,7 @@+-- | An array of key-value pairs, where the keys are integers.+-- Can be accessed both as a map ("give me the value corresponding+-- to the key 2") and as an array ("give me the 3rd key-value pair").+-- Array-like access is fast; everything else is slow. module Data.Numbered(   Numbered,   empty, fromList, singleton, toList, size, (!),@@ -10,6 +14,7 @@ import Data.Int import Data.Maybe +-- | An array of key-value pairs. data Numbered a =   Numbered     {-# UNPACK #-} !ByteArray@@ -17,34 +22,46 @@  instance Show a => Show (Numbered a) where show = show . toList +-- | An empty array. empty :: Numbered a empty = fromList [] +-- | A singleton array. singleton :: Int -> a -> Numbered a singleton i x = fromList [(i, x)] +-- | Convert a list of pairs to an array.+-- Duplicate keys are allowed. fromList :: [(Int, a)] -> Numbered a fromList xs =   Numbered     (byteArrayFromList (map (fromIntegral . fst) xs :: [Int32]))     (smallArrayFromList (map snd xs)) +-- | Convert an array to a list. toList :: Numbered a -> [(Int, a)] toList num =   [num ! i | i <- [0..size num-1]] +-- | Get the number of key-value pairs in an array. O(1) time. size :: Numbered a -> Int size (Numbered _ elems) = sizeofSmallArray elems +-- | Index into the array. O(1) time. (!) :: Numbered a -> Int -> (Int, a) Numbered idxs elems ! i =   (fromIntegral (indexByteArray idxs i :: Int32),    indexSmallArray elems i) +-- | Look up the value associated with a particular key.+-- If the key occurs multiple times, any of its values+-- may be returned. O(n) time. lookup :: Int -> Numbered a -> Maybe a lookup i num =   List.lookup i (toList num) +-- | Associate a value with a key. Any existing occurences+-- of the key are removed. O(n) time. put :: Int -> a -> Numbered a -> Numbered a put i x num =   fromList $ lt ++ [(i, x)] ++ gt@@ -53,13 +70,20 @@     lt = List.filter ((< i) . fst) xs     gt = List.filter ((> i) . fst) xs +-- | Remove a given key. O(n) time. delete :: Int -> Numbered a -> Numbered a delete i = fromList . List.filter ((/= i) . fst) . toList +-- | Modify the value associated with a given key.+-- If the key occurs multiple times, one of its values+-- is chosen and the others deleted. In the call+-- @modify k def f@, if the key @k@ is not present,+-- the entry @k -> f def@ is added. O(n) time. modify :: Int -> a -> (a -> a) -> Numbered a -> Numbered a modify i def f num =   put i (f (fromMaybe def (lookup i num))) num +-- | Keep only keys satisfying a predicate. filter :: (a -> Bool) -> Numbered a -> Numbered a filter p = fromList . List.filter (p . snd) . toList
+ Data/PackedSequence.hs view
@@ -0,0 +1,45 @@+-- | Sequences which are stored compactly in memory+-- by serialising their contents as a @ByteString@.+module Data.PackedSequence(PackedSequence, empty, null, size, fromList, toList, uncons) where++import Prelude hiding (null)+import Data.Serialize+import Data.ByteString(ByteString)+import qualified Data.ByteString as BS+import Data.List(unfoldr)++-- | A sequence, stored in a serialised form+data PackedSequence a =+  Seq {-# UNPACK #-} !Int {-# UNPACK #-} !ByteString+  deriving Eq++-- | An empty sequence.+empty :: PackedSequence a+empty = Seq 0 BS.empty++-- | Is a given sequency empty?+null :: PackedSequence a -> Bool+null s = size s == 0++-- | Find the number of items in a sequence.+size :: PackedSequence a -> Int+size (Seq n _) = n++-- | Convert a list into a sequence.+{-# INLINEABLE fromList #-}+fromList :: Serialize a => [a] -> PackedSequence a+fromList xs = Seq (length xs) (runPut (mapM_ put xs))++-- | Convert a sequence into a list.+{-# INLINEABLE toList #-}+toList :: Serialize a => PackedSequence a -> [a]+toList = unfoldr uncons++-- | Find and remove the first value from a sequence.+{-# INLINEABLE uncons #-}+uncons :: Serialize a => PackedSequence a -> Maybe (a, PackedSequence a)+uncons (Seq 0 _) = Nothing+uncons (Seq n bs) =+  Just $ case runGetState get bs 0 of+    Left err -> error err+    Right (x, bs) -> (x, Seq (n-1) bs)
Twee.hs view
@@ -1,5 +1,5 @@ -- | The main prover loop.-{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies #-}+{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances #-} module Twee where  import Twee.Base@@ -19,8 +19,8 @@ import Twee.Constraints import Twee.Utils import Twee.Task-import qualified Twee.PassiveQueue as Queue-import Twee.PassiveQueue(Queue, Passive(..))+import qualified Data.BatchedQueue as Queue+import Data.BatchedQueue(Queue) import qualified Data.IntMap.Strict as IntMap import Data.IntMap(IntMap) import Data.Maybe@@ -36,6 +36,9 @@ import qualified Data.IntSet as IntSet import Data.IntSet(IntSet) import Twee.Profile+import Data.Ord+import Data.PackedSequence(PackedSequence)+import qualified Data.PackedSequence as PackedSequence  ---------------------------------------------------------------------- -- * Configuration and prover state.@@ -65,7 +68,7 @@     st_active_set     :: !(IntMap (Active f)),     st_joinable       :: !(Index f (Equation f)),     st_goals          :: ![Goal f],-    st_queue          :: !(Queue Params),+    st_queue          :: !(Queue Batch),     st_next_active    :: {-# UNPACK #-} !Id,     st_considered     :: {-# UNPACK #-} !Int64,     st_simplified_at  :: {-# UNPACK #-} !Id,@@ -174,20 +177,9 @@ -- * The CP queue. ---------------------------------------------------------------------- -data Params-instance Queue.Params Params where-  type Score Params = Int-  type Id Params = Id-  type PackedId Params = Int32-  type PackedScore Params = Int32-  packScore _ = fromIntegral-  unpackScore _ = fromIntegral-  packId _ = fromIntegral-  unpackId _ = fromIntegral- -- | Compute all critical pairs from a rule. {-# INLINEABLE makePassives #-}-makePassives :: Function f => Config f -> State f -> Active f -> [Passive Params]+makePassives :: Function f => Config f -> State f -> Active f -> [Passive] makePassives config@Config{..} State{..} rule = -- XXX factor out depth calculation   stampWith "make critical pair" length@@ -198,30 +190,90 @@     rules = IntMap.elems st_active_set     ok rule = the rule < Depth cfg_max_cp_depth +data Passive =+  Passive {+    passive_score :: {-# UNPACK #-} !Int32,+    passive_rule1 :: {-# UNPACK #-} !Id,+    passive_rule2 :: {-# UNPACK #-} !Id,+    passive_how   :: !How }+  deriving Eq++instance Ord Passive where+  compare = comparing f+    where+      f Passive{..} =+        (passive_score,+         intMax (fromIntegral passive_rule1) (fromIntegral passive_rule2),+         intMin (fromIntegral passive_rule1) (fromIntegral passive_rule2),+         passive_how)++data Batch =+  Batch {+    batch_kind      :: !BatchKind,+    batch_rule      :: {-# UNPACK #-} !Id,+    batch_best      :: {-# UNPACK #-} !Passive,+    batch_rest      :: {-# UNPACK #-} !(PackedSequence (Int32, Id, How)) }++data BatchKind = Rule1 | Rule2 deriving Eq++instance Queue.Batch Batch where+  type Label Batch = Id+  type Entry Batch = Passive++  makeBatch rule ps =+    make1 Rule1 ps1 ++ make1 Rule2 ps2+    where+      (ps1, ps2) = partition isRule1 ps+      isRule1 Passive{..} = rule == passive_rule1++      make1 _ [] = []+      make1 kind (p:ps) =+        [Batch {+           batch_kind = kind,+           batch_rule = rule,+           batch_best = p,+           batch_rest = +             PackedSequence.fromList $+               [ (passive_score, if kind == Rule1 then passive_rule2 else passive_rule1, passive_how)+               | Passive{..} <- ps ] }]++  unconsBatch batch@Batch{..} =+    (batch_best,+     do (p, ps) <- PackedSequence.uncons batch_rest+        return batch{batch_best = unpack batch_kind p, batch_rest = ps})+    where+      unpack Rule1 (score, rule2, how) =+        Passive score batch_rule rule2 how+      unpack Rule2 (score, rule1, how) =+        Passive score rule1 batch_rule how++  batchLabel Batch{..} = batch_rule+  batchSize Batch{..} = 1 + PackedSequence.size batch_rest+ {-# INLINEABLE makePassive #-}-makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Params+makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive makePassive Config{..} overlap@Overlap{..} =   Passive {     passive_score = fromIntegral (score cfg_critical_pairs depth overlap),     passive_rule1 = active_id overlap_rule1,     passive_rule2 = active_id overlap_rule2,-    passive_pos   = packHow overlap_how }+    passive_how   = overlap_how }   where     depth = succ (the overlap_rule1 `max` the overlap_rule2)  -- | Turn a Passive back into an overlap. -- Doesn't try to simplify it. {-# INLINEABLE findPassive #-}-findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (Overlap (Active f) f)+findPassive :: forall f. Function f => State f -> Passive -> Maybe (Overlap (Active f) f) findPassive State{..} Passive{..} = do   rule1 <- IntMap.lookup (fromIntegral passive_rule1) st_active_set   rule2 <- IntMap.lookup (fromIntegral passive_rule2) st_active_set-  overlapAt (unpackHow passive_pos) rule1 rule2+  overlapAt passive_how rule1 rule2     (renameAvoiding (the rule2 :: Rule f) (the rule1)) (the rule2)  -- | Renormalise a queued Passive. {-# INLINEABLE simplifyPassive #-}-simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params)+simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe (Passive) simplifyPassive Config{..} state@State{..} passive = do   overlap <- findPassive state passive   overlap <- simplifyOverlap (index_oriented st_rules) overlap@@ -250,7 +302,7 @@  -- | Enqueue a set of critical pairs. {-# INLINEABLE enqueue #-}-enqueue :: Function f => State f -> Id -> [Passive Params] -> State f+enqueue :: Function f => State f -> Id -> [Passive] -> State f enqueue state rule passives =   state { st_queue = Queue.insert rule passives (st_queue state) } @@ -272,7 +324,8 @@        state { st_queue = queue, st_considered = st_considered + n })   where     deq !n queue = do-      (passive, queue) <- Queue.removeMin queue+      let ok id = fromIntegral id `IntMap.member` st_active_set+      (passive, queue) <- Queue.removeMinFilter ok queue       case findPassive state passive of         Just (overlap@Overlap{overlap_eqn = t :=: u, overlap_rule1 = rule1, overlap_rule2 = rule2})           | fromMaybe True (cfg_accept_term <*> pure t),@@ -355,7 +408,7 @@  -- Update the list of sampled critical pairs. {-# INLINEABLE sample #-}-sample :: Function f => Int -> [Passive Params] -> State f -> State f+sample :: Function f => Int -> [Passive] -> State f -> State f sample m passives state@State{..} =   state{st_cp_sample = addSample (m, map find passives) st_cp_sample}   where@@ -367,13 +420,13 @@ {-# INLINEABLE resetSample #-} resetSample :: Function f => Config f -> State f -> State f resetSample Config{..} state@State{..} =-  foldl' sample1 state' (Queue.toList st_queue)+  foldl' sample1 state' (Queue.toBatches st_queue)   where     state' =       state {         st_cp_sample = emptySample cfg_cp_sample_size } -    sample1 state (n, passives) = sample n passives state+    sample1 state batch = sample (Queue.batchSize batch) (Queue.unbatch batch) state  -- Simplify the sampled critical pairs. -- (A sampled critical pair is replaced with Nothing if it can be@@ -493,7 +546,7 @@       where         m = bound excl -    bound excl = minimum . map (passiveMax excl) . concatMap snd . Queue.toList $ st_queue state+    bound excl = minimum . map (passiveMax excl) . Queue.toList $ st_queue state      passiveMax excl p = fromMaybe maxBound $ do       Overlap{overlap_rule1 = r1, overlap_rule2 = r2} <- findPassive state p@@ -690,7 +743,7 @@           StateM.put $! recomputeGoals config state,        newTask 60 0.01 $ do           State{..} <- StateM.get-          let !n = Queue.queueSize st_queue+          let !n = Queue.size st_queue           lift $ output_message (Status n)]      let
Twee/Base.hs view
@@ -28,10 +28,11 @@ import Data.List hiding (singleton) import Data.Maybe import qualified Data.IntMap.Strict as IntMap+import Data.Serialize  -- | Represents a unique identifier (e.g., for a rule). newtype Id = Id { unId :: Int32 }-  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral)+  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral, Serialize)  instance Pretty Id where   pPrint = text . show . unId
Twee/CP.hs view
@@ -16,6 +16,8 @@ import qualified Twee.Proof as Proof import Twee.Proof(Derivation, congPath) import Data.Bits+import Data.Serialize+import Data.Int  -- | The set of positions at which a term can have critical overlaps. data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)@@ -62,7 +64,8 @@     overlap_rule1 :: !a,     -- | The rule which applies at some subterm.     overlap_rule2 :: !a,-    -- | The position in the critical term which is rewritten.+    -- | The position in the critical term which is rewritten,+    -- together with the direction of the two rules.     overlap_how   :: {-# UNPACK #-} !How,     -- | The top term of the critical pair     overlap_top   :: {-# UNPACK #-} !(Term f),@@ -70,31 +73,38 @@     overlap_eqn   :: {-# UNPACK #-} !(Equation f) }   deriving Show -data Direction = Forwards | Backwards deriving (Eq, Enum, Show)+data How =+  How {+    how_pos  :: {-# UNPACK #-} !Int,+    how_dir1 :: !Direction,+    how_dir2 :: !Direction }+  deriving (Eq, Ord, Show) +data Direction = Forwards | Backwards deriving (Eq, Ord, Enum, Show)+ direct :: Rule f -> Direction -> Rule f direct rule Forwards = rule direct rule Backwards = backwards rule -data How =-  How {-    how_dir1 :: !Direction,-    how_dir2 :: !Direction,-    how_pos  :: {-# UNPACK #-} !Int }-  deriving Show--packHow :: How -> Int-packHow How{..} =-  fromEnum how_dir1 +-  fromEnum how_dir2 `shiftL` 1 +-  how_pos `shiftL` 2+instance Serialize How where+  put = put . packHow+    where+      packHow :: How -> Int32+      packHow How{..} =+        fromIntegral $+        fromEnum how_dir1 ++        fromEnum how_dir2 `shiftL` 1 ++        how_pos `shiftL` 2 -unpackHow :: Int -> How-unpackHow n =-  How {-    how_dir1 = toEnum (n .&. 1),-    how_dir2 = toEnum ((n `shiftR` 1) .&. 1),-    how_pos  = n `shiftR` 2 }+  get = fmap unpackHow get+    where+      unpackHow :: Int32 -> How+      unpackHow n0 =+        let n = fromIntegral n0 in+        How {+          how_dir1 = toEnum (n .&. 1),+          how_dir2 = toEnum ((n `shiftR` 1) .&. 1),+          how_pos  = n `shiftR` 2 }  -- | Represents the depth of a critical pair. newtype Depth = Depth Int deriving (Eq, Ord, Num, Real, Enum, Integral, Show)@@ -135,14 +145,14 @@ asymmetricOverlaps idx r1 r2 d1 d2 posns eq1 eq2 = do   n <- positionsChurch posns   ChurchList.fromMaybe $-    overlapAt' (How d1 d2 n) r1 r2 eq1 eq2 >>=+    overlapAt' (How n d1 d2) r1 r2 eq1 eq2 >>=     simplifyOverlap idx  -- | Create an overlap at a particular position in a term. -- Doesn't simplify the overlap. {-# INLINE overlapAt #-} overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f)-overlapAt how@(How d1 d2 _) x1 x2 r1 r2 =+overlapAt how@(How _ d1 d2) x1 x2 r1 r2 =   overlapAt' how x1 x2 (unorient (direct r1 d1)) (unorient (direct r2 d2))  {-# INLINE overlapAt' #-}
Twee/Equation.hs view
@@ -4,8 +4,6 @@  import Twee.Base import Control.Monad-import Data.List-import Data.Ord  -------------------------------------------------------------------------------- -- * Equations.
Twee/Join.hs view
@@ -153,7 +153,7 @@     -- No need to do this symmetrically because addJoinable adds     -- both orientations of each equation   | or [ u == subst sub u'-       | (sub, t' :=: u') <- Index.matches t eqns ] = True+       | (sub, _ :=: u') <- Index.matches t eqns ] = True subsumed1 eqns idx (App f ts :=: App g us)   | f == g =     let
− Twee/PassiveQueue.hs 
@@ -1,201 +0,0 @@--- | A queue of passive critical pairs, using a memory-efficient representation.-{-# LANGUAGE TypeFamilies, RecordWildCards, FlexibleContexts, ScopedTypeVariables, StandaloneDeriving #-}-module Twee.PassiveQueue(-  Params(..),-  Queue,-  Passive(..),-  empty, insert, removeMin, mapMaybe, toList, queueSize) where--import qualified Data.Heap as Heap-import qualified Data.Vector.Unboxed as Vector-import Data.Int-import Data.List hiding (insert)-import qualified Data.Maybe-import Data.Ord-import Data.Proxy-import Twee.Utils---- | A datatype representing all the type parameters of the queue.-class (Eq (Id params), Integral (Id params), Ord (Score params), Vector.Unbox (PackedScore params), Vector.Unbox (PackedId params)) => Params params where-  -- | The score assigned to critical pairs. Smaller scores are better.-  type Score params-  -- | The type of ID numbers used to name rules.-  type Id params--  -- | A 'Score' packed for storage into a 'Vector.Vector'. Must be an instance of 'Vector.Unbox'.-  type PackedScore params-  -- | An 'Id' packed for storage into a 'Vector.Vector'. Must be an instance of 'Vector.Unbox'.-  type PackedId params--  -- | Pack a 'Score'.-  packScore :: proxy params -> Score params -> PackedScore params-  -- | Unpack a 'PackedScore'.-  unpackScore :: proxy params -> PackedScore params -> Score params-  -- | Pack an 'Id'.-  packId :: proxy params -> Id params -> PackedId params-  -- | Unpack a 'PackedId'.-  unpackId :: proxy params -> PackedId params -> Id params---- | A critical pair queue.-newtype Queue params =-  Queue (Heap.Heap (PassiveSet params))---- All passive CPs generated from one given rule.-data PassiveSet params =-  PassiveSet {-    passiveset_best  :: {-# UNPACK #-} !(Passive params),-    passiveset_rule  :: !(Id params),-    -- CPs where the rule is the left-hand rule-    passiveset_left  :: {-# UNPACK #-} !(Vector.Vector (PackedScore params, PackedId params, Int32)),-    -- CPs where the rule is the right-hand rule-    passiveset_right :: {-# UNPACK #-} !(Vector.Vector (PackedScore params, PackedId params, Int32)) }-instance Params params => Eq (PassiveSet params) where-  x == y = compare x y == EQ-instance Params params => Ord (PassiveSet params) where-  compare = comparing passiveset_best---- A smart-ish constructor.-{-# INLINEABLE mkPassiveSet #-}-mkPassiveSet ::-  Params params =>-  Proxy params ->-  Id params ->-  Vector.Vector (PackedScore params, PackedId params, Int32) ->-  Vector.Vector (PackedScore params, PackedId params, Int32) ->-  Maybe (PassiveSet params)-mkPassiveSet proxy rule left right-  | Vector.null left && Vector.null right = Nothing-  | not (Vector.null left) &&-    (Vector.null right || l <= r) =-    Just PassiveSet {-      passiveset_best  = l,-      passiveset_rule  = rule,-      passiveset_left  = Vector.tail left,-      passiveset_right = right }-    -- In this case we must have not (Vector.null right).-  | otherwise =-    Just PassiveSet {-      passiveset_best  = r,-      passiveset_rule  = rule,-      passiveset_left  = left,-      passiveset_right = Vector.tail right }-  where-    l = unpack proxy rule True (Vector.head left)-    r = unpack proxy rule False (Vector.head right)---- Unpack a triple into a Passive.-{-# INLINEABLE unpack #-}-unpack :: Params params => Proxy params -> Id params -> Bool -> (PackedScore params, PackedId params, Int32) -> Passive params-unpack proxy rule isLeft (score, id, pos) =-  Passive {-    passive_score = unpackScore proxy score,-    passive_rule1 = if isLeft then rule else rule',-    passive_rule2 = if isLeft then rule' else rule,-    passive_pos = fromIntegral pos }-  where-    rule' = unpackId proxy id---- Make a PassiveSet from a list of Passives.-{-# INLINEABLE makePassiveSet #-}-makePassiveSet :: forall params. Params params => Id params -> [Passive params] -> Maybe (PassiveSet params)-makePassiveSet _ [] = Nothing-makePassiveSet rule ps-  | and [passive_rule2 p == rule | p <- right] =-    mkPassiveSet proxy rule-      (Vector.fromList (map (pack True) (sort left)))-      (Vector.fromList (map (pack False) (sort right)))-  | otherwise = error "rule id does not occur in passive"-  where-    proxy :: Proxy params-    proxy = Proxy-    -    (left, right) = partition (\p -> passive_rule1 p == rule) ps-    pack isLeft Passive{..} =-      (packScore proxy passive_score,-       packId proxy (if isLeft then passive_rule2 else passive_rule1),-       fromIntegral passive_pos)---- Convert a PassiveSet back into a list of Passives.-{-# INLINEABLE unpackPassiveSet #-}-unpackPassiveSet :: forall params.Params params => PassiveSet params -> (Int, [Passive params])-unpackPassiveSet PassiveSet{..} =-  (1 + Vector.length passiveset_left + Vector.length passiveset_right,-   passiveset_best:-   map (unpack proxy passiveset_rule True) (Vector.toList passiveset_left) ++-   map (unpack proxy passiveset_rule False) (Vector.toList passiveset_right))-  where-    proxy :: Proxy params-    proxy = Proxy---- Find and remove the best element from a PassiveSet.-{-# INLINEABLE unconsPassiveSet #-}-unconsPassiveSet :: forall params. Params params => PassiveSet params -> (Passive params, Maybe (PassiveSet params))-unconsPassiveSet PassiveSet{..} =-  (passiveset_best, mkPassiveSet (Proxy :: Proxy params) passiveset_rule passiveset_left passiveset_right)---- | A queued critical pair.-data Passive params =-  Passive {-    -- | The score of this critical pair.-    passive_score :: !(Score params),-    -- | The rule which does the outermost rewrite in this critical pair.-    passive_rule1 :: !(Id params),-    -- | The rule which does the innermost rewrite in this critical pair.-    passive_rule2 :: !(Id params),-    -- | The position of the overlap. See 'Twee.CP.overlap_pos'.-    passive_pos   :: {-# UNPACK #-} !Int }--instance Params params => Eq (Passive params) where-  x == y = compare x y == EQ--instance Params params => Ord (Passive params) where-  compare = comparing f-    where-      f Passive{..} =-        (passive_score,-         intMax (fromIntegral passive_rule1) (fromIntegral passive_rule2),-         intMin (fromIntegral passive_rule1) (fromIntegral passive_rule2),-         passive_pos)---- | The empty queue.-empty :: Queue params-empty = Queue Heap.empty---- | Add a set of 'Passive's to the queue.-{-# INLINEABLE insert #-}-insert :: Params params => Id params -> [Passive params] -> Queue params -> Queue params-insert rule passives (Queue q) =-  Queue $-  case makePassiveSet rule passives of-    Nothing -> q-    Just p -> Heap.insert p q---- | Remove the minimum 'Passive' from the queue.-{-# INLINEABLE removeMin #-}-removeMin :: Params params => Queue params -> Maybe (Passive params, Queue params)-removeMin (Queue q) = do-  (passiveset, q) <- Heap.removeMin q-  case unconsPassiveSet passiveset of-    (passive, Just passiveset') ->-      Just (passive, Queue (Heap.insert passiveset' q))-    (passive, Nothing) ->-      Just (passive, Queue q)---- | Map a function over all 'Passive's.-{-# INLINEABLE mapMaybe #-}-mapMaybe :: Params params => (Passive params -> Maybe (Passive params)) -> Queue params -> Queue params-mapMaybe f (Queue q) = Queue (Heap.mapMaybe g q)-  where-    g passiveSet@PassiveSet{..} =-      makePassiveSet passiveset_rule $ Data.Maybe.mapMaybe f $-        snd (unpackPassiveSet passiveSet)---- | Convert a queue into a list of 'Passive's.--- The 'Passive's are produced in batches, with each batch labelled--- with its size.-{-# INLINEABLE toList #-}-toList :: Params params => Queue params -> [(Int, [Passive params])]-toList (Queue h) = map unpackPassiveSet (Heap.toList h)--queueSize :: Params params => Queue params -> Int-queueSize = sum . map fst . toList
Twee/Term.hs view
@@ -70,7 +70,9 @@ import qualified Twee.Term.Core as Core import Data.List hiding (lookup, find, singleton) import Data.Maybe+#if __GLASGOW_HASKELL__ < 804 import Data.Semigroup(Semigroup(..))+#endif import Data.IntMap.Strict(IntMap) import qualified Data.IntMap.Strict as IntMap import Control.Arrow((&&&))@@ -300,7 +302,7 @@         -- (n = minBound, m = maxBound), which is OK.         mconcat [emitVar (V x) | x <- [0..n-m+1]] -    loop !_ !_ !_ !_ | False = undefined+    loop !_ !_ !_ !_ | never = undefined     loop sub _ Empty [] = sub     loop sub Empty _ _ = sub     loop sub vs Empty (t:ts) = loop sub vs t ts@@ -464,7 +466,7 @@ unifyListTriFrom !t !u (Triangle !sub) =   fmap Triangle (loop sub t u)   where-    loop !_ !_ !_ | False = undefined+    loop !_ !_ !_ | never = undefined     loop sub (ConsSym{hd = t, tl = ts, rest = ts1}) u = do       ConsSym{hd = u, tl = us, rest =  us1} <- Just u       case (t, u) of@@ -668,7 +670,7 @@ replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f replacePosition n !x = aux n   where-    aux !_ !_ | False = undefined+    aux !_ !_ | never = undefined     aux _ Empty = mempty     aux 0 (Cons _ t) = builder x `mappend` builder t     aux n (Cons (Var x) t) = var x `mappend` aux (n-1) t@@ -684,7 +686,7 @@ replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f replacePositionSub sub n !x = aux n   where-    aux !_ !_ | False = undefined+    aux !_ !_ | never = undefined     aux _ Empty = mempty     aux n (Cons t u)       | n < len t = inside n t `mappend` outside u
Twee/Term/Core.hs view
@@ -24,7 +24,6 @@ import GHC.Prim import GHC.ST hiding (liftST) import Data.Ord-import Data.Semigroup(Semigroup(..)) import Twee.Profile  --------------------------------------------------------------------------------
Twee/Utils.hs view
@@ -1,6 +1,6 @@ -- | Miscellaneous utility functions. -{-# LANGUAGE CPP, MagicHash #-}+{-# LANGUAGE CPP, MagicHash, GeneralizedNewtypeDeriving #-} module Twee.Utils where  import Control.Arrow((&&&))@@ -12,6 +12,7 @@ import GHC.Types import Data.Bits import System.Random+import Data.Serialize --import Test.QuickCheck hiding ((.&.))  repeatM :: Monad m => m a -> m [a]@@ -177,3 +178,45 @@ foldn :: (a -> a) -> a -> Int -> a foldn _ e 0 = e foldn op e n | n > 0 = op (foldn op e (n-1))++newtype U8 = U8 Int deriving (Eq, Ord, Num, Real, Enum, Integral)++-- Untested!+instance Serialize U8 where+  put (U8 n)+    | n < 0x80 = putWord8 (fromIntegral n)+    | n < 0x4000 = do+      putWord16be (fromIntegral n + 0x8000)+    | otherwise = do+      putWord32be (fromIntegral n + 0xc0000000)+  get = do+    x <- lookAhead getWord8+    if x < 0x80 then fromIntegral <$> getWord8+    else if x < 0xc0 then do+      n <- getWord16be+      return (fromIntegral (n - 0x8000))+    else do+      n <- getWord32be+      return (fromIntegral (n - 0xc0000000))++-- Untested!+newtype U16 = U16 Int deriving (Eq, Ord, Num, Real, Enum, Integral)+instance Serialize U16 where+  put (U16 n)+    | n < 0x8000 = do+      putWord16be (fromIntegral n)+    | otherwise = do+      putWord32be (fromIntegral n + 0x80000000)+  get = do+    x <- lookAhead getWord8+    if x < 0x80 then fromIntegral <$> getWord16be+    else do+      n <- getWord32be+      return (fromIntegral (n - 0x80000000))++-- Can be used to write strictness annotations e.g.+-- f !_ !_ | never = undefined+-- which otherwise trigger a spurious warning from GHC.+{-# INLINE never #-}+never :: Bool+never = False
twee-lib.cabal view
@@ -1,5 +1,5 @@ name:                twee-lib-version:             2.4.1+version:             2.4.2 synopsis:            An equational theorem prover homepage:            http://github.com/nick8325/twee license:             BSD3@@ -54,7 +54,6 @@     Twee.Index     Twee.Join     Twee.KBO-    Twee.PassiveQueue     Twee.Pretty     Twee.Profile     Twee.Proof@@ -65,10 +64,12 @@     Twee.Utils     Data.Label   other-modules:+    Data.BatchedQueue     Data.ChurchList     Data.DynamicArray     Data.Heap     Data.Numbered+    Data.PackedSequence     Twee.Term.Core    build-depends:@@ -79,11 +80,12 @@     pretty >= 1.1.2.0,     ghc-prim,     primitive >= 0.7.1.0,-    vector,     uglymemo,-    random+    random,+    bytestring,+    cereal   hs-source-dirs:      .-  ghc-options:         -W -fno-warn-incomplete-patterns+  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports   default-language:    Haskell2010    if flag(llvm)