twee-lib 2.6.1 → 2.7.1

raw patch · 28 files changed

+1060/−247 lines, 28 filesdep +binarydep +deepseqdep −cerealdep ~randomPVP ok

version bump matches the API change (PVP)

Dependencies added: binary, deepseq

Dependencies removed: cereal

Dependency ranges changed: random

API changes (from Hackage documentation)

Files

• Data/BatchedQueue.hs +6/−5
• Data/Binary/Sharing.hs +424/−0
• Data/ChurchList.hs +1/−1
• Data/DynamicArray.hs +4/−1
• Data/Heap.hs +5/−2
• Data/Intern.hs +21/−15
• Data/Numbered.hs +6/−0
• Data/PackedSequence.hs +14/−9
• Data/Primitive/ByteArray/Checked.hs +0/−1
• Twee.hs +184/−45
• Twee/Base.hs +15/−6
• Twee/CP.hs +41/−41
• Twee/Constraints.hs +10/−5
• Twee/Equation.hs +6/−2
• Twee/Generate.hs +2/−2
• Twee/Index.hs +26/−1
• Twee/Join.hs +1/−2
• Twee/KBO.hs +12/−13
• Twee/LPO.hs +107/−0
• Twee/Profile.hs +1/−1
• Twee/Proof.hs +75/−29
• Twee/Rule.hs +11/−9
• Twee/Rule/Index.hs +4/−2
• Twee/Task.hs +0/−1
• Twee/Term.hs +41/−5
• Twee/Term/Core.hs +2/−2
• Twee/Utils.hs +18/−37
• twee-lib.cabal +23/−10

@@ -1,5 +1,5 @@ -- | A queue where entries can be added in batches and stored compactly.-{-# LANGUAGE TypeFamilies, RecordWildCards, FlexibleContexts, ScopedTypeVariables #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-} module Data.BatchedQueue(   Queue, Batch(..), StandardBatch, unbatch, empty, insert, removeMin, removeMinFilter, mapMaybe, toBatches, toList, size) where @@ -8,11 +8,12 @@ import qualified Data.Maybe import Data.PackedSequence(PackedSequence) import qualified Data.PackedSequence as PackedSequence-import Data.Serialize+import qualified Data.Binary as Cereal+import Data.Binary.Sharing import Data.Ord  -- | A queue of batches.-newtype Queue a = Queue (Heap.Heap (Best a))+newtype Queue a = Queue (Heap.Heap (Best a)) deriving Binary  -- | The type of batches must be a member of this class. class Ord (Entry a) => Batch a where@@ -47,7 +48,7 @@   type Label a = ()  -- A newtype wrapper for batches which compares the smallest entry.-newtype Best a = Best { unBest :: a }+newtype Best a = Best { unBest :: a } deriving Binary instance Batch a => Eq (Best a) where x == y = compare x y == EQ instance Batch a => Ord (Best a) where   {-# INLINEABLE compare #-}@@ -130,7 +131,7 @@ instance Ord a => Ord (StandardBatch a) where   compare = comparing batch_best -instance (Ord a, Serialize a) => Batch (StandardBatch a) where+instance (Ord a, Cereal.Binary a) => Batch (StandardBatch a) where   type Label (StandardBatch a) = ()   type Entry (StandardBatch a) = a 

@@ -0,0 +1,424 @@+-- | A serialisation library with support for sharing. Built on top of binary.++{-# LANGUAGE ConstraintKinds, GADTs, DerivingVia, TypeSynonymInstances, FlexibleInstances, DefaultSignatures, DeriveAnyClass, DeriveFunctor, TupleSections #-}+module Data.Binary.Sharing(Binary(..), Shared(..), Put, PutM, encode, encodeFile, runPut, liftPut, unliftPut, Get, decode, decodeFile, runGet, liftGet, unliftGet, putList, getList, putWord8, getWord8, putInt8, getInt8, putIntegral, getIntegral, ReadShowBinary(..)) where+import qualified Data.Binary as S+import qualified Data.Binary.Get as S+import qualified Data.Binary.Put as S+import Data.Typeable+import qualified Data.HashMap.Strict as HashMap+import Data.HashMap.Strict(HashMap)+import Data.Maybe+import GHC.Generics+import Data.Hashable+import Control.Monad+import Data.Bits+import Data.Word+import Data.Int+import Data.Char+import qualified Data.ByteString.Lazy as BS+import qualified Data.ByteString as BSS+import Control.Monad.Trans.State.Strict hiding (get, put)+import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Primitive.SmallArray as SmallArray+import qualified Data.Foldable as Foldable+import qualified Data.Map as Map+import qualified Data.IntMap as IntMap+import qualified Data.Set as Set+import qualified Data.IntSet as IntSet+import qualified Data.HashSet as HashSet++----------------------------------------------------------------------+-- The basic serialiser/deserialiser types.+--+-- The idea is that both serialisation and deserialisation maintain a+-- store of shared values we have already seen (each associated with an+-- ID). When we emit a value we have already seen, we instead just emit+-- its ID. This is handled in the "Binary (Shared a)" instance.+----------------------------------------------------------------------++-- | A serialiser.+newtype PutM a = PutM { unPutM :: Store -> S.PutM (a, Store) } deriving Functor+-- Note we can't use StateT because then generalised newtype deriving doesn't work+instance Applicative PutM where+  pure x = PutM $ \store -> pure (x, store)+  mf <*> mx = mf >>= \f -> mx >>= \x -> pure (f x)+instance Monad PutM where+  mx >>= f =+    PutM $ \store -> do+      (x, store) <- unPutM mx store+      unPutM (f x) store+type Put = PutM ()++instance Semigroup Put where+  mx <> my = do { mx; my }++instance Monoid Put where+  mempty = pure mempty++-- Lift a state-monadic computation into Put.+liftStatePut :: State Store a -> PutM a+liftStatePut act = PutM $ \store -> return (runState act store)++-- | Lift a binary serialiser into Put.+liftPut :: S.PutM a -> PutM a+liftPut putter = PutM $ \store -> (, store) <$> putter++-- | Convert a 'Put' back into a binary serialiser.+unliftPut :: PutM a -> S.PutM a+unliftPut (PutM putter) = fst <$> putter emptyStore++-- | Serialise a value.+runPut :: Put -> BS.ByteString+runPut = S.runPut . unliftPut++-- | Serialise a value.+encode :: Binary a => a -> BS.ByteString+encode = runPut . put++-- | Serialise a value to a file.+encodeFile :: Binary a => FilePath -> a -> IO ()+encodeFile path = BS.writeFile path . encode++-- | A deserialiser.+newtype Get a = Get { unGet :: Store -> S.Get (a, Store) } deriving Functor+instance Applicative Get where+  pure x = Get $ \store -> pure (x, store)+  mf <*> mx = mf >>= \f -> mx >>= \x -> pure (f x)+instance Monad Get where+  mx >>= f =+    Get $ \store -> do+      (x, store) <- unGet mx store+      unGet (f x) store++-- Lift a state-monadic computation into Get.+liftStateGet :: State Store a -> Get a+liftStateGet act = Get $ \store -> return (runState act store)++-- | Lift a binary serialiser into Get.+liftGet :: S.Get a -> Get a+liftGet getter = Get $ \store -> (, store) <$> getter++-- | Convert a 'Get' back into a binary serialiser.+unliftGet :: Get a -> S.Get a+unliftGet (Get getter) = fst <$> getter emptyStore++-- | Deserialise a value.+runGet :: Get a -> BS.ByteString -> a+runGet = S.runGet . unliftGet++-- | Deserialise a value.+decode :: Binary a => BS.ByteString -> a+decode = runGet get++-- | Deserialise a value from a file.+decodeFile :: Binary a => FilePath -> IO a+decodeFile path = decode <$> BS.readFile path++----------------------------------------------------------------------+-- The sharing primitive.+----------------------------------------------------------------------++-- | A newtype wrapper which uses sharing on serialisation.+-- If the same 'Shared' value is 'put' multiple times, only the first+-- occurrence will be serialised in full and the later ones will+-- instead serialise as a "pointer" to the first one. The test for+-- whether a value is the same as a previous one uses '(==)'.+newtype Shared a = Shared { getShared :: a } deriving (Eq, Show)++-- The binary format for a "Shared a".+-- The first time a given Shared value appears, we allocate a key (ID) for+-- it and emit it as a 'Let'; if it reoccurs, we emit a 'Ref' to the existing ID.+data SharedEncoding a = Let Key a | Ref Key++instance Binary a => Binary (SharedEncoding a) where+  put (Let key x) = do+    put (key `unsafeShiftL` 1)+    put x+  put (Ref key) = do+    put (key `unsafeShiftL` 1 + 1)++  get = do+    keyTag <- get+    let key = keyTag `unsafeShiftR` 1+    case testBit keyTag 0 of+      False -> do -- Let+        x <- get+        return (Let key x)+      True -> -- Ref+        return (Ref key)++instance (Typeable a, Eq a, Hashable a, Binary a) => Binary (Shared a) where+  put (Shared x) = do+    mkey <- liftStatePut (lookupValue x)+    case mkey of+      Just key ->+        put (Ref key :: SharedEncoding a)+      Nothing -> do+        key <- liftStatePut reserveKey+        put (Let key x)+        liftStatePut (addValue key x)++  get = Shared <$> do+    value <- get+    case value of+      Let key x -> do+        liftStateGet (addValue key x)+        return x+      Ref key ->+        liftStateGet (lookupKey key)++----------------------------------------------------------------------+-- The store of previously-seen values.+----------------------------------------------------------------------++data Store =+  Store {+    -- Maps between values and ID numbers.+    store_keys :: HashMap Key Value,+    store_values :: HashMap Value Key,+    -- The next available ID number.+    store_next_key :: Key }+type Key = Integer++-- Useful for making heterogeneous maps.+data Value where+  Value :: (Eq a, Hashable a, Typeable a) => a -> Value++instance Eq Value where+  Value x == Value y =+    case cast x of+      Just x' -> x' == y+      Nothing -> error "type error"++instance Hashable Value where+  hashWithSalt s (Value x) = hashWithSalt s (typeOf x, x)++emptyStore :: Store+emptyStore = Store HashMap.empty HashMap.empty 0++-- Check if an existing value exists in the store.+lookupValue :: (Eq a, Hashable a, Typeable a) => a -> State Store (Maybe Key)+lookupValue x = do+  let value = Value x+  Store{..} <- State.get+  return (fromIntegral <$> HashMap.lookup value store_values)++-- Allocate a new key.+reserveKey :: Monad m => StateT Store m Key+reserveKey = do+  store@Store{..} <- State.get+  State.put store{store_next_key = store_next_key+1}+  return (fromIntegral store_next_key)++-- Add a new value to the store.+addValue :: (Eq a, Hashable a, Typeable a) => Key -> a -> State Store ()+addValue key x = do+  let value = Value x+  store@Store{..} <- State.get+  when (HashMap.member key store_keys) $ error "key already found"+  when (HashMap.member value store_values) $ error "value already found"+  State.put store{+    store_keys = HashMap.insert key value store_keys,+    store_values = HashMap.insert value key store_values }++-- Find a value by ID number.+lookupKey :: Typeable a => Key -> State Store a+lookupKey key = do+  Store{..} <- State.get+  case HashMap.lookup key store_keys of+    Just (Value x) -> return (fromJust (cast x))+    Nothing -> error ("invalid value " ++ show key ++ " " ++ show store_next_key)++----------------------------------------------------------------------+-- Primitive serialisers.+----------------------------------------------------------------------++putWord8 = liftPut . S.putWord8+getWord8 = liftGet S.getWord8+putInt8 = liftPut . S.putInt8+getInt8 = liftGet S.getInt8++putIntegral :: (Integral a, Bits a) => a -> Put+putIntegral n+  | toInteger n >= -1 && toInteger n < 126 =+    putWord8 (clearBit (fromIntegral n) 7)+  | otherwise = do+    putWord8 (setBit (fromIntegral n) 7)+    putIntegral (n `shiftR` 7)++getIntegral :: (Integral a, Bits a) => Get a+getIntegral = getIntegral' 0 0++getIntegral' :: (Integral a, Bits a) => Int -> a -> Get a+getIntegral' !k !n = do+  x <- getWord8+  let !n' = n + fromIntegral (clearBit x 7) `shiftL` k+  if testBit x 7 then getIntegral' (k+7) n'+    else if x == 127 then return (n' - (1 `shiftL` (k+7)))+    else return n'++-- QuickCheck property:+-- quickCheck (withNumTests 1000000 (withMaxSize 100000 (\x -> runGet getIntegral (runPut (putIntegral (x :: Int))) === Right x)))+-- TODO: add to test suite++putList :: (a -> Put) -> [a] -> Put+putList putter xs = do+  put (length xs)+  mapM_ putter xs++getList :: Get a -> Get [a]+getList getter = do+  len <- get+  replicateM len getter++----------------------------------------------------------------------+-- A class for serialisation/deserialisation.+----------------------------------------------------------------------++class Binary a where+  put :: a -> Put+  get :: Get a++  default put :: (Generic a, GBinary (Rep a)) => a -> Put+  put x = gput (from x)++  default get :: (Generic a, GBinary (Rep a)) => Get a+  get = to <$> gget++instance Binary Int where { put = putIntegral; get = getIntegral }+instance Binary Int8 where { put = putInt8; get = getInt8 }+instance Binary Int16 where { put = putIntegral; get = getIntegral }+instance Binary Int32 where { put = putIntegral; get = getIntegral }+instance Binary Int64 where { put = putIntegral; get = getIntegral }+instance Binary Word where { put = putIntegral; get = getIntegral }+instance Binary Word8 where { put = putWord8; get = getWord8 }+instance Binary Word16 where { put = putIntegral; get = getIntegral }+instance Binary Word32 where { put = putIntegral; get = getIntegral }+instance Binary Word64 where { put = putIntegral; get = getIntegral }+instance Binary Integer where { put = putIntegral; get = getIntegral }+instance Binary Char where { put = putIntegral . ord; get = chr <$> getIntegral }+instance Binary BS.ByteString where { put = liftPut . S.put; get = liftGet S.get }+instance Binary BSS.ByteString where { put = liftPut . S.put; get = liftGet S.get }+instance Binary Float where { put = liftPut. S.put; get = liftGet S.get }+instance Binary Double where { put = liftPut . S.put; get = liftGet S.get }+deriving instance Binary Bool+deriving instance Binary ()+deriving instance (Binary a, Binary b) => Binary (a, b)+deriving instance (Binary a, Binary b, Binary c) => Binary (a, b, c)+deriving instance (Binary a, Binary b, Binary c, Binary d) => Binary (a, b, c, d)+deriving instance (Binary a, Binary b, Binary c, Binary d, Binary e) => Binary (a, b, c, d, e)+deriving instance Binary a => Binary (Maybe a)+deriving instance (Binary a, Binary b) => Binary (Either a b)+instance Binary a => Binary (SmallArray.SmallArray a) where+  put = put . Foldable.toList+  get = SmallArray.smallArrayFromList <$> get++-- | Serialise a value via read/show.+newtype ReadShowBinary a = ReadShowBinary { getReadShowBinary :: a }+instance (Show a, Read a) => Binary (ReadShowBinary a) where+  put = put . show . getReadShowBinary+  get = ReadShowBinary . read <$> get++instance Binary a => Binary [a] where+  put = putList put+  get = getList get++instance (Binary k, Binary v, Ord k) => Binary (Map.Map k v) where+  put = put . Map.toList+  get = Map.fromList <$> get++instance (Binary k, Binary v, Hashable k) => Binary (HashMap k v) where+  put = put . HashMap.toList+  get = HashMap.fromList <$> get++instance Binary v => Binary (IntMap.IntMap v) where+  put = put . IntMap.toList+  get = IntMap.fromList <$> get++instance (Binary k, Ord k) => Binary (Set.Set k) where+  put = put . Set.toList+  get = Set.fromList <$> get++instance (Binary k, Hashable k) => Binary (HashSet.HashSet k) where+  put = put . HashSet.toList+  get = HashSet.fromList <$> get++instance Binary IntSet.IntSet where+  put = put . IntSet.toList+  get = IntSet.fromList <$> get++----------------------------------------------------------------------+-- Generic instances.+----------------------------------------------------------------------++class GBinary f where+  gput :: f a -> Put+  gget :: Get (f a)++  gconstructors :: proxy (f a) -> Int+  gconstructors _ = 1++  gconstructor :: f a -> Int+  gconstructor _ = 0++  gputConstructor :: f a -> Put+  gputConstructor = gput++  ggetConstructor :: Int -> Get (f a)+  ggetConstructor 0 = gget+  ggetConstructor _ = error "ggetConstructor: out of bounds"++instance (GBinary f, GBinary g) => GBinary (f :*: g) where+  gput (x :*: y) = do+    gput x+    gput y+  gget = liftM2 (:*:) gget gget++instance (GBinary f, GBinary g) => GBinary (f :+: g) where+  gput x = do+    put (gconstructor x)+    gputConstructor x++  gget = do+    tag <- get+    ggetConstructor tag++  gconstructors _ =+    gconstructors (Proxy :: Proxy (f a)) + gconstructors (Proxy :: Proxy (g a))++  gconstructor (L1 x) = gconstructor x+  gconstructor (R1 x) = gconstructor x + gconstructors (Proxy :: Proxy (f a))++  gputConstructor (L1 x) = gputConstructor x+  gputConstructor (R1 x) = gputConstructor x++  ggetConstructor n+    | n < m = L1 <$> ggetConstructor n+    | otherwise = R1 <$> ggetConstructor (n-m)+    where+      m = gconstructors (Proxy :: Proxy (f a))++instance GBinary f => GBinary (M1 i c f) where+  gput (M1 x) = gput x+  gget = M1 <$> gget+  gconstructors _ = gconstructors (Proxy :: Proxy (f a))+  gconstructor (M1 x) = gconstructor x+  gputConstructor (M1 x) = gputConstructor x+  ggetConstructor n = M1 <$> ggetConstructor n++instance Binary a => GBinary (K1 i a) where+  gput (K1 x) = put x+  gget = K1 <$> get++instance GBinary U1 where+  gput U1 = return ()+  gget = return U1++instance GBinary V1 where+  gput _ = error "gput: void"+  gget = error "gget: void"+  gconstructors _ = 0+  gconstructor _ = error "gconstructor: void"+  gputConstructor = error "gputConstructor: void"+  ggetConstructor _ = error "ggetConstructor: void"

@@ -1,5 +1,5 @@ -- | Church-encoded lists. Used in Twee.CP to make sure that fusion happens.-{-# LANGUAGE Rank2Types, BangPatterns #-}+{-# LANGUAGE Rank2Types #-} module Data.ChurchList where  import Prelude(Functor(..), Applicative(..), Monad(..), Bool(..), Maybe(..), (.), ($), id)

@@ -1,6 +1,6 @@ -- | Zero-indexed dynamic arrays, optimised for lookup. -- Modification is slow. Uninitialised indices have a default value.-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, DeriveAnyClass #-} module Data.DynamicArray where  #ifdef BOUNDS_CHECKS@@ -10,6 +10,8 @@ #endif import Control.Monad.ST import Data.List+import Data.Binary.Sharing+import GHC.Generics  -- | A type which has a default value. class Default a where@@ -22,6 +24,7 @@     arrayStart    :: {-# UNPACK #-} !Int,     -- | The contents of the array.     arrayContents :: {-# UNPACK #-} !(P.SmallArray a) }+  deriving (Generic, Binary)  arraySize :: Array a -> Int arraySize = P.sizeofSmallArray . arrayContents

@@ -1,15 +1,18 @@ -- | Skew heaps. -{-# LANGUAGE BangPatterns, ScopedTypeVariables #-}+{-# LANGUAGE DeriveAnyClass #-} module Data.Heap(   Heap, empty, singleton, insert, removeMin, union, mapMaybe, size, toList) where +import Data.Binary.Sharing+import GHC.Generics+ -- | A heap.  -- N.B.: arguments are not strict so code has to take care -- to force stuff appropriately. -- The Int field is the size of the heap.-data Heap a = Nil | Node {-# UNPACK #-} !Int a (Heap a) (Heap a) deriving Show+data Heap a = Nil | Node {-# UNPACK #-} !Int a (Heap a) (Heap a) deriving (Show, Generic, Binary)  -- | Take the union of two heaps. {-# INLINEABLE union #-}

@@ -1,28 +1,30 @@ -- | Interning, annotating values with unique IDs. -{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP, PatternSynonyms, ViewPatterns, ConstraintKinds #-}+{-# LANGUAGE MagicHash, RoleAnnotations, CPP, PatternSynonyms, ViewPatterns, ConstraintKinds, GeneralizedNewtypeDeriving #-} module Data.Intern(Intern, Sym, pattern Sym, intern, unintern, unsafeMkSym, symId) where  import Data.IORef import System.IO.Unsafe-import qualified Data.Map.Strict as Map-import Data.Map.Strict(Map)+import qualified Data.HashMap.Strict as HashMap+import Data.HashMap.Strict(HashMap) import qualified Data.DynamicArray as DynamicArray import Data.DynamicArray(Array) import Data.Typeable import GHC.Exts import GHC.Int import Unsafe.Coerce+import Data.Hashable+import Data.Binary.Sharing  -- | Type class constraints for a value to be internable.-type Intern a = (Typeable a, Ord a)+type Intern a = (Typeable a, Eq a, Hashable a)  -- | An interned value of type @a@. newtype Sym a = MkSym Int32-  deriving (Eq, Ord)+  deriving (Eq, Ord, Hashable)  instance Show a => Show (Sym a) where-  show = show . unintern+  showsPrec n = showsPrec n . unintern  -- | The unique ID of a symbol. symId :: Sym a -> Int@@ -38,19 +40,17 @@ -- The global cache of interned values. {-# NOINLINE cachesRef #-} cachesRef :: IORef Caches-cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray))+cachesRef = unsafePerformIO (newIORef (Caches 0 HashMap.empty DynamicArray.newArray))  data Caches =   Caches {     -- The next id number to assign.     caches_nextId :: {-# UNPACK #-} !Int32,     -- A map from values to IDs.-    caches_from   :: !(Map TypeRep (Cache Any)),+    caches_from   :: !(HashMap TypeRep (HashMap Any Int32)),     -- The reverse map from IDs to values.     caches_to     :: !(Array Any) } -type Cache a = Map a Int32- atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a atomicModifyCaches f = do   -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the@@ -70,10 +70,10 @@   if ok then return x else atomicModifyCaches f  -- Versions of unsafeCoerce with slightly more type checking-toAnyCache :: Cache a -> Cache Any+toAnyCache :: HashMap a Int32 -> HashMap Any Int32 toAnyCache = unsafeCoerce -fromAnyCache :: Cache Any -> Cache a+fromAnyCache :: HashMap Any Int32 -> HashMap a Int32 fromAnyCache = unsafeCoerce  toAny :: a -> Any@@ -86,6 +86,7 @@ {-# NOINLINE intern #-} intern :: forall a. Intern a => a -> Sym a intern x =+  hash x `seq`   unsafeDupablePerformIO $ do     -- Common case: symbol is already interned.     caches <- readIORef cachesRef@@ -105,21 +106,21 @@      tryFind :: Caches -> Maybe (Sym a)     tryFind Caches{..} =-      MkSym <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)+      MkSym <$> (HashMap.lookup ty caches_from >>= HashMap.lookup x . fromAnyCache)      insert :: Caches -> (Caches, Sym a)     insert caches@Caches{..} =       if n < 0 then error "label overflow" else       (caches {          caches_nextId = n+1,-         caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,+         caches_from = HashMap.insert ty (toAnyCache (HashMap.insert x n cache)) caches_from,          caches_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to },        MkSym n)       where         n = caches_nextId         cache =           fromAnyCache $-          Map.findWithDefault Map.empty ty caches_from+          HashMap.findWithDefault HashMap.empty ty caches_from  -- | Recover the underlying value from a 'Sym'. unintern :: Sym a -> a@@ -145,3 +146,8 @@ pattern Sym :: Intern a => a -> Sym a pattern Sym x <- (unintern -> x) where   Sym x = intern x++-- Serialise a Sym as the underlying value, because it needs to be interned on deserialisation.+instance (Intern a, Binary a) => Binary (Sym a) where+  put = put . Shared . unintern+  get = intern . getShared <$> get

@@ -13,6 +13,8 @@ import Data.Primitive.SmallArray import Data.Int import Data.Maybe+import qualified Data.Binary.Sharing as Binary+import Data.Binary.Sharing(Binary)  -- | An array of key-value pairs. data Numbered a =@@ -21,6 +23,10 @@     {-# UNPACK #-} !(SmallArray a)  instance Show a => Show (Numbered a) where show = show . toList++instance Binary a => Binary (Numbered a) where+  put = Binary.put . toList+  get = fromList <$> Binary.get  -- | An empty array. empty :: Numbered a

@@ -1,17 +1,22 @@ -- | Sequences which are stored compactly in memory -- by serialising their contents as a @ByteString@.+{-# LANGUAGE DeriveAnyClass #-} module Data.PackedSequence(PackedSequence, empty, null, size, fromList, toList, uncons) where  import Prelude hiding (null)-import Data.Serialize+import Data.Binary+import Data.Binary.Get+import Data.Binary.Put+import qualified Data.Binary.Sharing as Sharing import Data.ByteString(ByteString) import qualified Data.ByteString as BS import Data.List(unfoldr)+import GHC.Generics  -- | A sequence, stored in a serialised form data PackedSequence a =   Seq {-# UNPACK #-} !Int {-# UNPACK #-} !ByteString-  deriving Eq+  deriving (Eq, Generic, Sharing.Binary)  -- | An empty sequence. empty :: PackedSequence a@@ -27,19 +32,19 @@  -- | Convert a list into a sequence. {-# INLINEABLE fromList #-}-fromList :: Serialize a => [a] -> PackedSequence a-fromList xs = Seq (length xs) (runPut (mapM_ put xs))+fromList :: Binary a => [a] -> PackedSequence a+fromList xs = Seq (length xs) (BS.toStrict (runPut (mapM_ put xs)))  -- | Convert a sequence into a list. {-# INLINEABLE toList #-}-toList :: Serialize a => PackedSequence a -> [a]+toList :: Binary 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 :: Binary 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)+  Just $ case runGetOrFail get (BS.fromStrict bs) of+    Left (_, _, err) -> error err+    Right (bs, _, x) -> (x, Seq (n-1) (BS.toStrict bs))

@@ -1,7 +1,6 @@ -- | A bounds-checked version of 'Data.Primitive.ByteArray'. -- See that module for documentation. -{-# LANGUAGE ScopedTypeVariables #-} module Data.Primitive.ByteArray.Checked(   module Data.Primitive.ByteArray,   module Data.Primitive.ByteArray.Checked) where

@@ -1,5 +1,5 @@ -- | The main prover loop.-{-# LANGUAGE RecordWildCards, MultiParamTypeClasses, GADTs, BangPatterns, OverloadedStrings, ScopedTypeVariables, GeneralizedNewtypeDeriving, PatternGuards, TypeFamilies, FlexibleInstances, RankNTypes, TupleSections #-}+{-# LANGUAGE MultiParamTypeClasses, GADTs, OverloadedStrings, GeneralizedNewtypeDeriving, FlexibleInstances, RankNTypes, TupleSections, DeriveAnyClass, CPP #-} module Twee where  import Twee.Base@@ -41,9 +41,11 @@ import qualified Data.PackedSequence as PackedSequence import Test.QuickCheck.Gen hiding (sample) import Test.QuickCheck.Random-import Debug.Trace+--import Debug.Trace import Twee.Generate import qualified System.Random as Random+import GHC.Generics+import Data.Binary.Sharing  ---------------------------------------------------------------------- -- * Configuration and prover state.@@ -64,7 +66,8 @@     cfg_set_join_goals            :: Bool,     cfg_always_simplify           :: Bool,     cfg_complete_subsets          :: Bool,-    cfg_score_cp                  :: Depth -> Index f (Hint f) -> Equation f -> Float,+    cfg_hint_func                 :: Int -> Float -> Sym f,+    cfg_cp_config                 :: !CP.Config,     cfg_join                      :: Join.Config,     cfg_proof_presentation        :: Proof.Config f,     cfg_eliminate_axioms          :: [Axiom f],@@ -86,7 +89,7 @@     st_joinable       :: !(Index f (Equation f)),     st_goals          :: ![Goal f],     st_queue          :: !(Queue Batch),-    st_hints          :: !(Index f (Hint f)),+    st_hints          :: {-# UNPACK #-} !(Hints f),     st_next_active    :: {-# UNPACK #-} !Id,     st_considered     :: {-# UNPACK #-} !Int64,     st_simplified_at  :: {-# UNPACK #-} !Id,@@ -94,8 +97,9 @@     st_not_complete   :: !IntSet,     st_complete       :: !(Index f (Rule f)),     st_messages_rev   :: ![Message f],-    st_random_seed    :: Maybe QCGen,+    st_random_seed    :: Maybe (ReadShowBinary QCGen),     st_problem_term   :: Maybe (ConfluenceFailure f) }+  deriving (Generic, Binary)  -- | The default prover configuration. defaultConfig :: Function f => Config f@@ -113,7 +117,8 @@     cfg_set_join_goals = True,     cfg_always_simplify = False,     cfg_complete_subsets = False,-    cfg_score_cp = \d hints eqn -> score CP.defaultConfig d hints eqn,+    cfg_hint_func = \_ _ -> error "cfg_hint_func not configured",+    cfg_cp_config = CP.defaultConfig,     cfg_join = Join.defaultConfig,     cfg_proof_presentation = Proof.defaultConfig,     cfg_eliminate_axioms = [],@@ -126,6 +131,21 @@     cfg_hint_skel_factor = 0,     cfg_print_score = False } +-- | Compute cfg_score_cp from the CP configuration.+{-# INLINE scoreCP #-}+scoreCP :: Function f => Config f -> Depth -> Hints f -> Equation f -> Float+scoreCP config@Config{..} d hints eqn =+  let s1 = score cfg_cp_config d (scoreTerm config hints) eqn+      -- s2 = score cfg_cp_config d (scoreTerm config (Hints [] Index.empty 0)) eqn+  {-+  in if s1 /= s2 then trace ("used hint for " ++ prettyShow eqn) (trace (prettyShow eqn ++ " => " ++ prettyShow (bothSides (applyHints hints) eqn)) s1) else s1+  -}+  in s1++{-# INLINE scoreTerm #-}+scoreTerm :: Function f => Config f -> Hints f -> Term f -> Float+scoreTerm Config{..} hints t = termScore cfg_cp_config (applyHints hints t)+ -- | Does this configuration run the prover in a complete mode? configIsComplete :: Config f -> Bool configIsComplete Config{..} =@@ -145,7 +165,11 @@     st_joinable = Index.empty,     st_goals = [],     st_queue = Queue.empty,-    st_hints = Index.empty,+    st_hints =+      Hints {+        hints_list = [],+        hints_index = Index.empty,+        hints_next = 0 },     st_next_active = 1,     st_considered = 0,     st_simplified_at = 1,@@ -156,7 +180,7 @@     st_random_seed =       case cfg_random_mode of         False -> Nothing-        True -> Just (mkQCGen 12345),+        True -> Just (ReadShowBinary (mkQCGen 12345)),     st_problem_term = Nothing }  ----------------------------------------------------------------------@@ -169,6 +193,8 @@     NewActive !(Maybe Float) !(Active f)     -- | A new joinable equation.   | NewEquation !(Equation f)+    -- | A new hint was added.+  | NewHint !(Rule f) !HintKind     -- | A rule was deleted.   | DeleteActive !(Active f)     -- | The CP queue was simplified.@@ -181,6 +207,7 @@   | Status !Int     -- | New problem term discovered.   | NewProblemTerm !(ConfluenceFailure f)+  deriving (Generic, Binary)  instance Function f => Pretty (Message f) where   pPrint (NewActive mscore rule) =@@ -190,6 +217,8 @@  --   $$ case cp_top (active_cp rule) of { Just t -> text "  (normal forms of term" <+> pPrint t <#> text ")"; Nothing -> pPrintEmpty }   pPrint (NewEquation eqn) =     text "  (hard)" <+> pPrint eqn+  pPrint (NewHint rule kind) =+    text "  (" <#> pPrint kind <+> text "hint)" <+> pPrint rule   pPrint (DeleteActive rule) =     text "  (delete rule " <#> pPrint (active_id rule) <#> text ")"   pPrint SimplifyQueue =@@ -255,7 +284,7 @@     passive_rule1 :: {-# UNPACK #-} !Id,     passive_rule2 :: {-# UNPACK #-} !Id,     passive_how   :: !How }-  deriving Eq+  deriving (Eq, Generic, Binary)  instance Ord Passive where   compare = comparing f@@ -272,8 +301,9 @@     batch_rule      :: {-# UNPACK #-} !Id,     batch_best      :: {-# UNPACK #-} !Passive,     batch_rest      :: {-# UNPACK #-} !(PackedSequence (Float, Id, How)) }+  deriving (Eq, Generic, Binary) -data BatchKind = Rule1 | Rule2 deriving Eq+data BatchKind = Rule1 | Rule2 deriving (Eq, Generic, Binary)  instance Queue.Batch Batch where   type Label Batch = Id@@ -311,14 +341,14 @@  {-# INLINEABLE makePassive #-} makePassive :: Function f => Config f -> State f -> Overlap (Active f) f -> Passive-makePassive Config{..} State{..} Overlap{..} =+makePassive config@Config{..} State{..} Overlap{..} =   Passive {-    passive_score = cfg_score_cp depth st_hints overlap_eqn,+    passive_score = scoreCP config depth st_hints overlap_eqn,     passive_rule1 = active_id overlap_rule1,     passive_rule2 = active_id overlap_rule2,     passive_how   = overlap_how }   where-    depth = succ (the overlap_rule1 `max` the overlap_rule2)+    depth = Depth (succ (getDepth (the overlap_rule1) `max` getDepth (the overlap_rule2)))  -- | Turn a Passive back into an overlap. -- Doesn't try to simplify it.@@ -333,16 +363,18 @@ -- | Renormalise a queued Passive. {-# INLINEABLE simplifyPassive #-} simplifyPassive :: Function f => Config f -> State f -> Passive -> Maybe (Passive)-simplifyPassive Config{..} state@State{..} passive = do+simplifyPassive config@Config{..} state@State{..} passive = do   overlap <- findPassive state passive   overlap <- simplifyOverlap (index_oriented st_rules) overlap   let r1 = overlap_rule1 overlap       r2 = overlap_rule2 overlap   return passive {     passive_score =+#ifndef USE_LPO       passive_score passive `min`+#endif       -- XXX factor out depth calculation-      cfg_score_cp (succ (the r1 `max` the r2)) st_hints (overlap_eqn overlap) }+      scoreCP config (Depth (succ (getDepth (the r1) `max` getDepth (the r2)))) st_hints (overlap_eqn overlap) }  -- | Check if we should renormalise the queue. {-# INLINEABLE shouldSimplifyQueue #-}@@ -371,9 +403,10 @@ -- --   * removing any orphans from the head of the queue --   * ignoring CPs that are too big+--   * putting back any CPs whose score got bigger since they were enqueued {-# INLINEABLE dequeue #-} dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f)-dequeue Config{..} state@State{..} =+dequeue config@Config{..} state@State{..} =   case deq 0 st_queue of     -- Explicitly make the queue empty, in case it e.g. contained a     -- lot of orphans@@ -389,14 +422,19 @@         Just (overlap@Overlap{overlap_eqn = t :=: u, overlap_rule1 = rule1, overlap_rule2 = rule2})           | fromMaybe True (cfg_accept_term <*> pure t),             fromMaybe True (cfg_accept_term <*> pure u),-            cp <- makeCriticalPair overlap ->-              return ((combineInfo (active_info rule1) (active_info rule2), cp, rule1, rule2), n+1, queue)+            cp <- makeCriticalPair overlap,+            Just newPassive <- simplifyPassive config state passive ->+              if passive_score newPassive <= passive_score passive then+                return ((combineInfo (active_info rule1) (active_info rule2), cp, rule1, rule2), n+1, queue)+              else+                deq (n+1) (Queue.insert (passive_rule1 newPassive) [newPassive] queue)+         _ -> deq (n+1) queue      combineInfo i1 i2 =       Info {         -- XXX factor out depth calculation-        info_depth = succ (max (info_depth i1) (info_depth i2)),+        info_depth = Depth (succ (max (getDepth (info_depth i1)) (getDepth (info_depth i2)))),         info_max = IntSet.union (info_max i1) (info_max i2) }  ----------------------------------------------------------------------@@ -413,6 +451,7 @@     -- A model in which the rule is false (used when reorienting)     active_model :: !(Model f),     active_positions :: !(Positions2 f) }+  deriving (Generic, Binary)  active_cp :: Active f -> CriticalPair f active_cp Active{..} =@@ -421,9 +460,9 @@     cp_top = active_top,     cp_proof = derivation active_proof } -activeScore :: Config f -> State f -> Active f -> Float-activeScore Config{..} State{..} Active{..} =-  cfg_score_cp (info_depth active_info) st_hints (equation active_proof)+activeScore :: Function f => Config f -> State f -> Active f -> Float+activeScore config@Config{..} State{..} Active{..} =+  scoreCP config (info_depth active_info) st_hints (equation active_proof)  activeRules :: Active f -> [Rule f] activeRules Active{..} =@@ -435,6 +474,7 @@   Info {     info_depth :: {-# UNPACK #-} !Depth,     info_max   :: !IntSet }+  deriving (Generic, Binary)  instance Eq (Active f) where   (==) = (==) `on` active_id@@ -459,7 +499,7 @@       | otherwise = Nothing     state' =       message (NewActive mscore active) $-      addActiveOnly state{st_next_active = st_next_active+1} active+      addActiveOnly config state{st_next_active = st_next_active+1} active   in if subsumed (st_joinable, st_complete) st_rules (unorient active_rule) then     state   else@@ -509,8 +549,9 @@  -- Add an active without generating critical pairs. Used in interreduction. {-# INLINEABLE addActiveOnly #-}-addActiveOnly :: Function f => State f -> Active f -> State f-addActiveOnly state@State{..} active@Active{..} =+addActiveOnly :: Function f => Config f -> State f -> Active f -> State f+addActiveOnly config state@State{..} active@Active{..} =+  addHintsRulePairs config active $   state {     st_rules = foldl' insertRule st_rules (activeRules active),     st_active_set = IntMap.insert (fromIntegral active_id) active st_active_set }@@ -520,8 +561,9 @@  -- Add an active without generating critical pairs. Used in interreduction. {-# INLINEABLE addActiveSimp #-}-addActiveSimp :: Function f => State f -> Active f -> State f-addActiveSimp state@State{..} active@Active{..} =+addActiveSimp :: Function f => Config f -> State f -> Active f -> State f+addActiveSimp config state@State{..} active@Active{..} =+  addHintsRulePairs config active $   state {     st_rules = foldl' insertRule st_rules (activeRules active) }   where@@ -603,22 +645,12 @@ addAxiom :: Function f => Config f -> State f -> Axiom f -> State f addAxiom config state axiom =   consider config state{st_axioms = axiom:st_axioms state}-    Info { info_depth = 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] }+    Info { info_depth = Depth 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] }     CriticalPair {       cp_eqn = axiom_eqn axiom,       cp_top = Nothing,       cp_proof = Proof.axiom axiom } --- Add a new hint.-{-# INLINEABLE addHint #-}-addHint :: Function f => Config f -> State f -> Term f -> State f-addHint Config{..} state@State{..} hint =-  state { st_hints = Index.insert hint (Hint hint cost) st_hints }-  where-    cost = fromIntegral (len hint - length (vars hint)) * cfg_hint_skel_factor + cfg_hint_skel_cost +-      -- Add a cost for duplicated variables (since they only get counted once otherwise)-      fromIntegral (length (vars hint) - length (usort (vars hint)))- -- Record an equation as being joinable. {-# INLINEABLE addJoinable #-} addJoinable :: Function f => State f -> Equation f -> State f@@ -675,7 +707,7 @@     goal_expanded_rhs :: Map (Term f) (Derivation f),     goal_lhs          :: Map (Term f) (Term f, Reduction f),     goal_rhs          :: Map (Term f) (Term f, Reduction f) }-  deriving Show+  deriving (Show, Generic, Binary)  -- Add a new goal. {-# INLINEABLE addGoal #-}@@ -766,6 +798,113 @@     goal_rhs = Map.singleton u (u, []) }  ----------------------------------------------------------------------+-- Hints.+----------------------------------------------------------------------++data Hints f =+  Hints {+    -- contains only user-provided hints+    hints_list  :: ![Rule f],+    -- also contains hints formed through CPs+    hints_index :: !(Index f (Rule f)),+    hints_next   :: !Int }+  deriving (Generic, Binary)++data HintKind = UserHint | DerivedHint deriving (Eq, Show, Generic, Binary)++instance Pretty HintKind where+  pPrint UserHint = text "show"+  pPrint DerivedHint = text "auto"++-- Add a new hint.+{-# INLINEABLE addHint #-}+addHint :: Function f => Config f -> State f -> Term f -> State f+addHint config@Config{..} state@State{..} hint =+  addHint' config state hint UserHint cost+  where+    cost = fromIntegral (len hint - length (vars hint)) * cfg_hint_skel_factor + cfg_hint_skel_cost++-- Add a new hint, with a specified kind and cost.+{-# INLINEABLE addHint' #-}+addHint' :: Function f => Config f -> State f -> Term f -> HintKind -> Float -> State f+addHint' config@Config{..} state@State{st_hints = Hints{..}, ..} hint kind cost =+  (if kind == UserHint then addHintRulesPairs config rule . addHintHintsPairs config rule else id) $+  {-+  trace ("hint: " ++ prettyShow hint) $+  trace ("kind: " ++ show kind) $+  trace ("cost: " ++ show cost) $+  trace ("hint term: " ++ prettyShow hintTerm) $+  trace "" $+  -}+  message (NewHint rule kind) $+  state {+    st_hints = Hints {+      hints_list = if kind == UserHint then rule:hints_list else hints_list,+      hints_index = Index.insert hint rule hints_index,+      hints_next = hints_next + 1 } }+  where+    args = usort (vars hint)++    hintTerm = build (app (cfg_hint_func hints_next cost) (map var args))++    -- A rule expressing applying the hint. Uses a dummy value for the proof+    -- field since this rule should never be used in a proof anyway. +    rule = Rule Oriented (certify (Proof.Refl hintTerm)) hint hintTerm++-- Add various kiknds of derived hints.+{-# INLINEABLE addHintsRulePairs #-}+addHintsRulePairs :: Function f => Config f -> Active f -> State f -> State f+addHintsRulePairs config active state =+  foldl' (\state rule -> addHintRulePairs config rule active state) state (hints_list (st_hints state))++{-# INLINEABLE addHintRulesPairs #-}+addHintRulesPairs :: Function f => Config f -> Rule f -> State f -> State f+addHintRulesPairs config rule state =+  foldl' (\state active -> addHintRulePairs config rule active state) state (IntMap.elems (st_active_set state))++{-# INLINEABLE addHintRulePairs #-}+addHintRulePairs :: Function f => Config f -> Rule f -> Active f -> State f -> State f+addHintRulePairs config rule active state =+  foldl' considerOverlap state (overlaps (Index.empty :: Index f (Rule f)) [makeActive rule] active)+    where+      -- hack: need to turn the turn into an Active to invoke 'overlaps'+      makeActive rule = Active 0 (Info (Depth 0) IntSet.empty) rule Nothing (rule_proof rule) (modelFromOrder []) (positionsRule rule)+      considerOverlap state Overlap{..} = considerNorm (simplifyTerm state) t u state+        where+          t = eqn_lhs overlap_eqn+          u = eqn_rhs overlap_eqn++      -- t: term we are considering adding a hint for+      -- u: version of the term where perhaps a hint has already been added+      considerNorm norm t u state+        | st > su =+        {-+          trace ("rule: " ++ prettyShow rule) $+          trace ("active: " ++ prettyShow (active_id active)) $+          trace ("term: " ++ prettyShow t) $+          trace ("norm first: " ++ prettyShow t' ++ " (cost " ++ show st ++ ")") $+          trace ("hint first: " ++ prettyShow u' ++ " (cost " ++ show su ++ ")") $+        -}+          addHint' config state t' DerivedHint su+        | otherwise = state+        where+          t' = norm t+          u' = norm u+          st = scoreTerm config (st_hints state) t'+          su = scoreTerm config (st_hints state) u'++{-# INLINEABLE addHintHintsPairs #-}+addHintHintsPairs :: Function f => Config f -> Rule f -> State f -> State f+addHintHintsPairs _ _ state = state++-- Apply hints to a term.+applyHints :: Function f => Hints f -> Term f -> Term f+applyHints Hints{..} t =+  {-let u = simplify idx t in+  if t == u then u else traceShow ("hint: " ++ prettyShow t ++ " => " ++ prettyShow u) u-}+  simplify hints_index t++---------------------------------------------------------------------- -- Interreduction. ---------------------------------------------------------------------- @@ -795,18 +934,18 @@       (Just active_model) (active_cp active)   of     Right (_, cps) ->-      flip addActiveSimp active $+      flip (addActiveSimp config) active $       flip (foldl' (\state cp -> consider config state active_info cp)) cps $       message (DeleteActive active) $       deleteActive state active     Left (cp, model)       | cp_eqn cp `simplerThan` cp_eqn (active_cp active) ->-        flip addActiveSimp active $+        flip (addActiveSimp config) active $         flip (foldl' (\state cp -> consider config state active_info cp)) (split cp) $         message (DeleteActive active) $         deleteActive state active       | model /= active_model ->-        flip addActiveOnly active { active_model = model } $+        flip (addActiveOnly config) active { active_model = model } $         deleteActive state active       | otherwise ->         state@@ -886,9 +1025,9 @@           (Nothing, state) -> (False, state)           (Just (info, overlap, _, _), state) ->             (True, consider config state info overlap)-      Just g -> -- random mode+      Just (ReadShowBinary g) -> -- random mode         let (g1, g2) = Random.split g in-        let state' = state { st_random_seed = Just g2 } in+        let state' = state { st_random_seed = Just (ReadShowBinary g2) } in         case findCriticalPair config state' g1 of           Nothing -> (True, state'{st_problem_term = Nothing})           Just (info, overlap, changed, cf) ->@@ -949,7 +1088,7 @@         Nothing ->           trace ("Overlap " ++ prettyShow (overlap_eqn o) ++ " was spurious") Nothing -- should be rare         Just o' ->-          Just (cfg_score_cp config 0 (st_hints state) (overlap_eqn o'), (Info 0 IntSet.empty, makeCriticalPair o, changed, cf))+          Just (scoreCP config (Depth 0) (st_hints state) (overlap_eqn o'), (Info (Depth 0) IntSet.empty, makeCriticalPair o, changed, cf))  -- Return all goal terms. Handles the $equals coding. goalTerms :: Function f => State f -> [Term f]

@@ -1,7 +1,7 @@ -- | Useful operations on terms and similar. Also re-exports some generally -- useful modules such as 'Twee.Term' and 'Twee.Pretty'. -{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns, PatternSynonyms #-}+{-# LANGUAGE FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, PatternSynonyms, RankNTypes #-} module Twee.Base(   -- * Re-exported functionality   module Twee.Term, module Twee.Pretty,@@ -14,7 +14,7 @@   -- * Typeclasses   Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground, skolemise,   Ordered(..), lessThan, orientTerms,-  EqualsBonus(..), isTrueTerm, isFalseTerm, decodeEquality,+  EqualsBonus(..), Weighted(..), isTrueTerm, isFalseTerm, decodeEquality,   Strictness(..), Function) where  import Prelude hiding (lookup)@@ -30,12 +30,13 @@ import Data.List hiding (singleton) import Data.Maybe import qualified Data.IntMap.Strict as IntMap-import Data.Serialize+import Data.Binary.Sharing+import qualified Data.Binary as Cereal import Data.Intern  -- | Represents a unique identifier (e.g., for a rule). newtype Id = Id { unId :: Int32 }-  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral, Serialize)+  deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral, Binary, Cereal.Binary)  instance Pretty Id where   pPrint = text . show . unId@@ -244,10 +245,18 @@ skolemise :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a skolemise t = subst (\(V x) -> con (skolem x)) t --- | For types which have a notion of size. -- | The collection of constraints which the type of function symbols must -- satisfy in order to be used by twee.-type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Intern f)+type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Intern f, Weighted f)++-- | For functions which have a notion of weight.+-- Used for weighing terms in CP selection.+class Weighted f where+  weight :: f -> Float+  weight _ = 1++instance Weighted f => Weighted (Sym f) where+  weight = weight . unintern  -- | A hack for encoding Horn clauses. See 'Twee.CP.Score'. -- The default implementation of 'hasEqualsBonus' should work OK.

@@ -1,12 +1,12 @@ -- | Critical pair generation.-{-# LANGUAGE BangPatterns, FlexibleContexts, ScopedTypeVariables, MultiParamTypeClasses, RecordWildCards, OverloadedStrings, TypeFamilies, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses, OverloadedStrings, DeriveAnyClass #-}+{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} module Twee.CP where  import qualified Twee.Term as Term import Twee.Base import Twee.Rule import Twee.Index(Index)-import qualified Twee.Index as Index import qualified Data.Set as Set import Control.Monad import Data.List hiding (singleton)@@ -17,15 +17,24 @@ import qualified Twee.Proof as Proof import Twee.Proof(Derivation, congPath) import Data.Bits-import Data.Serialize+import Data.Binary.Sharing+import qualified Data.Binary as Cereal import Data.Int --import Debug.Trace+import GHC.Generics  -- | The set of positions at which a term can have critical overlaps. data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)+instance Binary (Positions f) where+  put = put . unfoldr op+    where+      op NilP = Nothing+      op (ConsP x xs) = Just (x, xs)+  get = foldr ConsP NilP <$> (get :: Get [Int])+ type PositionsOf a = Positions (ConstantOf a) -- | Like Positions but for an equation (one set of positions per term).-data Positions2 f = ForwardsPos !(Positions f) | BothPos !(Positions f) !(Positions f)+data Positions2 f = ForwardsPos !(Positions f) | BothPos !(Positions f) !(Positions f) deriving (Generic, Binary)  instance Show (Positions f) where   show = show . ChurchList.toList . positionsChurch@@ -73,7 +82,7 @@     overlap_top   :: {-# UNPACK #-} !(Term f),     -- | The critical pair itself.     overlap_eqn   :: {-# UNPACK #-} !(Equation f) }-  deriving Show+  deriving (Show, Generic, Binary)  data How =   How {@@ -82,14 +91,14 @@     how_dir2 :: !Direction }   deriving (Eq, Ord, Show) -data Direction = Forwards | Backwards deriving (Eq, Ord, Enum, Show)+data Direction = Forwards | Backwards deriving (Eq, Ord, Enum, Show, Generic, Binary)  direct :: Rule f -> Direction -> Rule f direct rule Forwards = rule direct rule Backwards = backwards rule -instance Serialize How where-  put = put . packHow+instance Cereal.Binary How where+  put = Cereal.put . packHow     where       packHow :: How -> Int32       packHow How{..} =@@ -98,7 +107,7 @@         fromEnum how_dir2 `shiftL` 1 +         how_pos `shiftL` 2 -  get = fmap unpackHow get+  get = fmap unpackHow Cereal.get     where       unpackHow :: Int32 -> How       unpackHow n0 =@@ -108,8 +117,12 @@           how_dir2 = toEnum ((n `shiftR` 1) .&. 1),           how_pos  = n `shiftR` 2 } +instance Binary How where+  put = liftPut . Cereal.put+  get = liftGet Cereal.get+ -- | Represents the depth of a critical pair.-newtype Depth = Depth Int deriving (Eq, Ord, Num, Real, Enum, Integral, Show)+newtype Depth = Depth { getDepth :: Int } deriving (Eq, Ord, Show, Generic, Binary)  -- | Compute all overlaps of a rule with a set of rules. {-# INLINEABLE overlaps #-}@@ -200,22 +213,10 @@   Config {     cfg_lhsweight :: !Float,     cfg_rhsweight :: !Float,-    cfg_funweight :: !Float,     cfg_varweight :: !Float,     cfg_depthweight :: !Float,     cfg_dupcost :: !Float,-    cfg_dupfactor :: !Float,-    cfg_resonance :: !Bool }--data Hint f =-  Hint {-    hint_term :: {-# UNPACK #-} !(Term f),-    hint_cost :: {-# UNPACK #-} !Float }--instance Symbolic (Hint f) where-  type ConstantOf (Hint f) = f-  termsDL Hint{..} = termsDL hint_term-  subst_ sub (Hint t c) = Hint (subst_ sub t) c+    cfg_dupfactor :: !Float }  -- | The default heuristic configuration. defaultConfig :: Config@@ -223,29 +224,33 @@   Config {     cfg_lhsweight = 4,     cfg_rhsweight = 1,-    cfg_funweight = 1,     cfg_varweight = 6/7,     cfg_depthweight = 2,     cfg_dupcost = 1,-    cfg_dupfactor = 0,-    cfg_resonance = False }+    cfg_dupfactor = 0 }  -- | Compute a score for a critical pair.  -- We compute: --   cfg_lhsweight * size l + cfg_rhsweight * size r -- where l is the biggest term and r is the smallest,--- and variables have weight 1 and functions have weight cfg_funweight.-{-# INLINEABLE score #-}-score :: Function f => Config -> Depth -> Index f (Hint f) -> Equation f -> Float-score Config{..} depth hints (l :=: r) =-  fromIntegral depth * cfg_depthweight ++-- and variables have weight cfg_varweight.+{-# INLINE score #-}+score :: Function f => Config -> Depth -> (Term f -> Float) -> Equation f -> Float+score Config{..} depth termScore (l :=: r) =+  fromIntegral (getDepth depth) * cfg_depthweight +   (m + n) * cfg_rhsweight +   max m n * (cfg_lhsweight - cfg_rhsweight)   where-    m = size' 0 (singleton l) []-    n = size' 0 (singleton r) []+    m = termScore l+    n = termScore r +-- | Compute a score for a single term.+{-# INLINEABLE termScore #-}+termScore :: Function f => Config -> Term f -> Float+termScore Config{..} t =+  size' 0 (singleton t) []+  where     size' !_ !_ !_ | False = undefined     size' n Nil ts =       case ts of@@ -254,23 +259,18 @@     size' n (Cons t ts) us       | len t > 1, t `isSubtermOfList` ts || any (t `isSubtermOfList`) us =         size' (n+cfg_dupcost+cfg_dupfactor*fromIntegral (len t)) ts us-    size' n (Cons t ts) us-      | len t > 1, (sub, Hint{..}):_ <- Index.matches t hints,-        not cfg_resonance || allSubst (\_ t -> case t of { UnsafeCons (Var _) _ -> True; _ -> False }) sub =-        size' (n + hint_cost) ts (map snd (Term.substToList' sub) ++ us)-        --trace ("hint: len " ++ show (len t) ++ ", new cost " ++ show new_cost ++ ": " ++ prettyShow t) $     size' n ts xs       | Cons (App f ws@(Cons a (Cons b us))) vs <- ts,         not (isVar a),         not (isVar b),         hasEqualsBonus f,         Just sub <- unify a b =-        size' (n+cfg_funweight) ws xs `min`+        size' (n+weight f) ws xs `min`         size' (n+1) (subst sub us) (subst sub (vs:xs))     size' n (Cons (Var _) ts) us =       size' (n+cfg_varweight) ts us-    size' n ConsSym{hd = App{}, rest = ts} us =-      size' (n+cfg_funweight) ts us+    size' n ConsSym{hd = App f _, rest = ts} us =+      size' (n+weight f) ts us  ---------------------------------------------------------------------- -- * Higher-level handling of critical pairs.

@@ -1,4 +1,4 @@-{-# LANGUAGE FlexibleContexts, UndecidableInstances, RecordWildCards #-}+{-# LANGUAGE DeriveAnyClass #-} -- | Solving constraints on variable ordering. module Twee.Constraints where @@ -18,8 +18,10 @@ import Test.QuickCheck.Gen(unGen) import Test.QuickCheck.Random(mkQCGen) import Data.Intern+import GHC.Generics+import Data.Binary.Sharing -data Atom f = Constant (Sym f) | Variable Var deriving (Show, Eq, Ord)+data Atom f = Constant (Sym f) | Variable Var deriving (Show, Eq, Ord, Generic, Binary)  {-# INLINE atoms #-} atoms :: Term f -> [Atom f]@@ -188,7 +190,7 @@ addTerm _ b = b  newtype Model f = Model (Map (Atom f) (Int, Int))-  deriving (Eq, Show)+  deriving (Eq, Ord, Show, Generic, Binary) -- Representation: map from atom to (major, minor) -- x <  y if major x < major y -- x <= y if major x = major y and minor x < minor y@@ -215,8 +217,11 @@         rel = if i == j then LessEq else Less  modelFromOrder :: (Minimal f, Ord f) => [Atom f] -> Model f-modelFromOrder xs =-  Model (Map.fromList [(x, (i, i)) | (x, i) <- zip xs [0..]])+modelFromOrder xs = modelFromOrder' [[x] | x <- xs]++modelFromOrder' :: (Minimal f, Ord f) => [[Atom f]] -> Model f+modelFromOrder' xss =+  Model (Map.fromList [(x, (i, j)) | (xs, i) <- zip xss [0..], (x, j) <- zip xs [0..]])  weakenModel :: Model f -> [Model f] weakenModel (Model m) =

@@ -1,9 +1,12 @@ -- | Equations.-{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE DeriveAnyClass #-} module Twee.Equation where  import Twee.Base import Control.Monad+import GHC.Generics+import Data.Binary.Sharing+import Data.Hashable  -------------------------------------------------------------------------------- -- * Equations.@@ -13,7 +16,8 @@   (:=:) {     eqn_lhs :: {-# UNPACK #-} !(Term f),     eqn_rhs :: {-# UNPACK #-} !(Term f) }-  deriving (Eq, Ord, Show)+  deriving (Eq, Ord, Show, Generic, Hashable, Binary)+ type EquationOf a = Equation (ConstantOf a)  instance Symbolic (Equation f) where

@@ -7,7 +7,7 @@ import Data.Maybe import Twee.Profile import Twee.Utils-import Debug.Trace+--import Debug.Trace  type Pat f = Term f type LHS f = Term f@@ -31,7 +31,7 @@   [ (1, return sub) ] ++   -- commit to top-level function...   [ (n, genList (reduce n (length ps)) lhss ps sub)-  | App f psl <- [p]+  | App _f psl <- [p]   , let ps = unpack psl   ] ++   -- ...or use a LHS for inspiration

@@ -5,7 +5,7 @@ -- the search term is an instance of the key, and return the corresponding -- values. -{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP, TupleSections, TypeFamilies #-}+{-# LANGUAGE OverloadedStrings, CPP, TupleSections, DeriveAnyClass #-} -- We get some bogus warnings because of pattern synonyms. {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}@@ -40,6 +40,8 @@ import qualified Data.IntMap.Strict as IntMap import Twee.Profile import Data.Intern+import Data.Binary.Sharing+import GHC.Generics  -- The term index in this module is a _perfect discrimination tree_. -- This is a trie whose keys are terms, represented as flat lists of symbols@@ -489,3 +491,26 @@       Nothing ->         searchVars t ts binds var (start+1) rest +----------------------------------------------------------------------+-- Serialisation.+----------------------------------------------------------------------++-- When serialising, we must change the 'fun' array to index by function and not function number.+data  SIndex f a = SIndex Int (TermList f) [a] [(Sym f, Index f a)] (Numbered (Index f a)) | SEmpty+  deriving (Generic, Binary)++toSerialised :: Index f a -> SIndex f a+toSerialised Empty = SEmpty+toSerialised (Index minSize prefix here funs vars) = SIndex minSize prefix here funs' vars+  where+    funs' = [(unsafeMkSym f, idx) | (f, idx) <- Array.toList funs, not (null idx)]++fromSerialised :: SIndex f a -> Index f a+fromSerialised SEmpty = Empty+fromSerialised (SIndex minSize prefix here funs vars) = Index minSize prefix here funs' vars+  where+    funs' = foldr (uncurry Array.update) newArray [(symId f, idx) | (f, idx) <- funs]++instance (Intern f, Binary f, Binary a) => Binary (Index f a) where+  put = put . toSerialised+  get = fromSerialised <$> get

@@ -1,5 +1,4 @@ -- | Tactics for joining critical pairs.-{-# LANGUAGE FlexibleContexts, BangPatterns, RecordWildCards, TypeFamilies, ScopedTypeVariables #-} module Twee.Join where  import Twee.Base@@ -220,7 +219,7 @@         _ -> normaliseWith (const True) (rewrite (ok t u m) (index_all idx)) t     ok t u m rule sub =       case cp_top of-        Just top | cfg_use_connectedness_in_ground_joining ->+        Just _top | cfg_use_connectedness_in_ground_joining ->           reducesWith lessEqSkolemModel rule sub &&           unorient rule `simplerThan` (t :=: u)         _ ->

@@ -1,7 +1,6 @@ -- | An implementation of Knuth-Bendix ordering. -{-# LANGUAGE PatternGuards, BangPatterns #-}-module Twee.KBO(lessEq, lessIn, lessEqSkolem, Sized(..), Weighted(..)) where+module Twee.KBO(lessEq, lessIn, lessEqSkolem, Sized(..), ArgWeighted(..)) where  import Twee.Base hiding (lessEq, lessIn, lessEqSkolem) import Twee.Equation@@ -13,7 +12,7 @@ import Twee.Utils import Data.Intern -lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool+lessEqSkolem :: (Function f, Sized f, ArgWeighted f) => Term f -> Term f -> Bool lessEqSkolem !t !u   | m < n = True   | m > n = False@@ -39,7 +38,7 @@       in loop ts us  -- | Check if one term is less than another in KBO.-lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool+lessEq :: (Function f, Sized f, ArgWeighted f) => Term f -> Term f -> Bool lessEq (App f Nil) _ | f == minimal = True lessEq (Var x) (Var y) | x == y = True lessEq _ (Var _) = False@@ -76,14 +75,14 @@  -- See "notes/kbo under assumptions" for how this works. -lessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness+lessIn :: (Function f, Sized f, ArgWeighted f) => Model f -> Term f -> Term f -> Maybe Strictness lessIn model t u =   case sizeLessIn model t u of     Nothing -> Nothing     Just Strict -> Just Strict     Just Nonstrict -> lexLessIn model t u -sizeLessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness+sizeLessIn :: (Function f, Sized f, ArgWeighted f) => Model f -> Term f -> Term f -> Maybe Strictness sizeLessIn model t u =   case minimumIn model m of     Just l@@ -123,7 +122,7 @@       | k < 0 = Nothing       | otherwise = Just k -lexLessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness+lexLessIn :: (Function f, Sized f, ArgWeighted f) => Model f -> Term f -> Term f -> Maybe Strictness lexLessIn _ t u | t == u = Just Nonstrict lexLessIn cond t u   | Just a <- fromTerm t,@@ -157,13 +156,13 @@   -- | Compute the size.   size  :: a -> Integer -class Weighted f where+class ArgWeighted f where   argWeight :: f -> Integer -instance (Weighted f, Intern f) => Weighted (Sym f) where+instance (ArgWeighted f, Intern f) => ArgWeighted (Sym f) where   argWeight = argWeight . unintern -weightedVars :: (Weighted f, Intern f) => Term f -> [(Var, Integer)]+weightedVars :: (ArgWeighted f, Intern f) => Term f -> [(Var, Integer)] weightedVars t = collate sum (loop 1 t)   where     loop k (Var x) = [(x, k)]@@ -173,7 +172,7 @@ instance (Intern f, Sized f) => Sized (Sym f) where   size = size . unintern -instance (Intern f, Sized f, Weighted f) => Sized (TermList f) where+instance (Intern f, Sized f, ArgWeighted f) => Sized (TermList f) where   size = aux 0     where       aux n Nil = n@@ -181,9 +180,9 @@         aux (n + size f + argWeight f * size t) u       aux n (Cons (Var _) t) = aux (n+1) t -instance (Intern f, Sized f, Weighted f) => Sized (Term f) where+instance (Intern f, Sized f, ArgWeighted f) => Sized (Term f) where   size = size . singleton -instance (Intern f, Sized f, Weighted f) => Sized (Equation f) where+instance (Intern f, Sized f, ArgWeighted f) => Sized (Equation f) where   size (x :=: y) = size x + size y 

@@ -0,0 +1,107 @@+-- | An implementation of lexicographic path ordering.++module Twee.LPO(lessEqBasic, lessEq, lessIn, lessEqSkolem) where++import Twee.Base hiding (lessEq, lessIn, lessEqSkolem)+import Twee.Constraints hiding (lessEq, lessIn, lessEqSkolem)+import Data.Maybe+import Control.Monad++lessEqSkolem :: Function f => Term f -> Term f -> Bool+lessEqSkolem (App f Nil) _ | f == minimal = True+lessEqSkolem _ (App f Nil) | f == minimal = False+lessEqSkolem (Var x) (Var y) = x <= y+lessEqSkolem _ (Var _) = False+lessEqSkolem (Var _) _ = True+lessEqSkolem t@(App f ts) u@(App g us)+  | f == g = lexMA ts us+  | f << g = majo ts u+  | otherwise = alpha t us+  where+    lexMA Nil Nil = True+    lexMA (Cons t' ts) (Cons u' us)+      | t' == u' = lexMA ts us+      | lessEqSkolem t' u' = majo ts u+      | otherwise = alpha t us++    majo ts u = and [t /= u && lessEqSkolem t u | t <- unpack ts]+    alpha t us = or [lessEqSkolem t u | u <- unpack us]++-- For testing+lessEqBasic :: Function f => Term f -> Term f -> Bool+lessEqBasic t u = eqModErasure t u || lessBasic t u+  where+    eqModErasure (App f _) _ | f == minimal = True+    eqModErasure (Var x) (Var y) = x == y+    eqModErasure (App f ts) (App g us) =+      f == g && and (zipWith eqModErasure (unpack ts) (unpack us))+    eqModErasure _ _ = False++lessBasic :: Function f => Term f -> Term f -> Bool+lessBasic (App f Nil) (App g _) | f == minimal && g /= minimal = True+lessBasic (Var _) (Var _) = False+lessBasic (Var x) (App _ ts) = x `elem` vars ts+lessBasic t@(App f ts) u@(App g us)+  | or [lessEqBasic t u' | u' <- unpack us] = True+  | f << g && and [lessBasic t' u | t' <- unpack ts] = True+  | f == g = and [lessBasic t' u | t' <- unpack ts] && loop ts us+  where+    loop Nil Nil = False+    loop (Cons t ts) (Cons u us) =+      if t == u then loop ts us else lessBasic t u+lessBasic _ _ = False++-- | Check if one term is less than another in LPO.+lessEq :: Function f => Term f -> Term f -> Bool+lessEq (App f Nil) _ | f == minimal = True+lessEq (Var x) (Var y) = x == y+lessEq _ (Var _) = False+lessEq (Var x) t = x `elem` vars t+lessEq t@(App f ts) u@(App g us)+  | f == g = lexMA ts us+  | f << g = majo ts u+  | otherwise = alpha t us+  where+    lexMA Nil Nil = True+    lexMA (Cons t' ts) (Cons u' us)+      | t' == u' = lexMA ts us+      | lessEq t' u' =+        case unify t' u' of+          Just sub -> majo ts u && lexMA (subst sub ts) (subst sub us)+          Nothing -> majo ts u+      | otherwise = alpha t us++    majo ts u = and [isNothing (unify t u) && lessEq t u | t <- unpack ts]+    alpha t us = or [lessEq t u | u <- unpack us]++lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness+lessIn model t u+  | Just a <- fromTerm t,+    Just b <- fromTerm u,+    Just s <- lessEqInModel model a b = Just s+lessIn _ _ (Var _) = Nothing+lessIn model (Var x) t+  | any isJust [lessEqInModel model (Variable x) a | a <- catMaybes (map fromTerm (subterms t))] = Just Strict+  | otherwise = Nothing+lessIn model t@(App f ts) u@(App g us)+  | f == g = lexMA ts us+  | f << g = majo ts u+  | otherwise = alpha t us+  where+    lexMA Nil Nil = Just Nonstrict+    lexMA (Cons t' ts) (Cons u' us) =+      case lessIn model t' u' of+        Just Nonstrict ->+          case (let Just sub = unify t' u' in lexMA (subst sub ts) (subst sub us), majo ts u) of+            (Just Strict, Just Strict) -> Just Strict+            (Just _, Just _) -> Just Nonstrict+            _ -> Nothing+        Just Strict -> majo ts u+        Nothing -> alpha t us++    majo ts u = do+      guard (and [lessIn model t u == Just Strict | t <- unpack ts])+      return Strict+    alpha t us = do+      guard (or [isJust (lessIn model t u) | u <- unpack us])+      return Strict

@@ -1,5 +1,5 @@ -- Basic support for profiling.-{-# LANGUAGE BangPatterns, RecordWildCards, CPP, OverloadedStrings #-}+{-# LANGUAGE CPP, OverloadedStrings #-} module Twee.Profile(stamp, stampWith, stampM, stampGen, stampGen', profile) where  #ifdef PROFILE

@@ -1,5 +1,5 @@--- | Equational proofs which are checked for correctedness.-{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables, OverloadedStrings #-}+-- | Equational proofs which are checked for correctness.+{-# LANGUAGE OverloadedStrings, DeriveAnyClass #-} module Twee.Proof(   -- * Constructing proofs   Proof, Derivation(..), Axiom(..),@@ -33,6 +33,10 @@ import Control.Monad.Trans.State.Strict import Data.Graph import Twee.Profile+import qualified Data.Binary.Sharing as Binary+import Data.Binary.Sharing(Binary, Shared(..))+import GHC.Generics+import Data.Hashable  ---------------------------------------------------------------------- -- Equational proofs. Only valid proofs can be constructed.@@ -65,7 +69,7 @@     -- Parallel, i.e., takes a function symbol and one derivation for each     -- argument of that function.   | Cong {-# UNPACK #-} !(Sym f) ![Derivation f]-  deriving (Eq, Show)+  deriving (Eq, Show, Generic, Hashable, Binary)  --  | An axiom, which comes without proof. data Axiom f =@@ -76,9 +80,12 @@     -- | A description of the axiom.     -- Has no semantic meaning; for convenience only.     axiom_name :: !String,+    -- | Human-readable names for the variables of the axiom.+    -- Has no semantic meaning; for convenience only.+    axiom_vars :: !(Maybe (Map Var String)),     -- | The equation which the axiom asserts.     axiom_eqn :: !(Equation f) }-  deriving (Eq, Ord, Show)+  deriving (Eq, Ord, Show, Generic, Hashable)  -- | Checks a 'Derivation' and, if it is correct, returns a -- certified 'Proof'.@@ -87,11 +94,11 @@  -- This is the trusted core of the module. {-# INLINEABLE certify #-}-certify :: Function f => Derivation f -> Proof f+certify :: Derivation f -> Proof f certify p =   stamp "certify proof" $   case check p of-    Nothing -> error ("Invalid proof created!\n" ++ prettyShow p)+    Nothing -> error "Invalid proof created!"     Just eqn -> Proof eqn p   where     check (UseLemma proof sub) =@@ -129,6 +136,8 @@   -- Don't look at the proof itself, to prevent exponential blowup   -- when a proof contains UseLemma   compare = comparing equation+instance Hashable (Proof f) where+  hashWithSalt s = hashWithSalt s . equation  instance Symbolic (Derivation f) where   type ConstantOf (Derivation f) = f@@ -167,6 +176,16 @@     text "axiom" <#>     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn] +instance (Intern f, Binary f) => Binary (Axiom f) where+  put Axiom{..} = Binary.put (Shared (axiom_number, axiom_name, axiom_vars, axiom_eqn))+  get = do+    Shared (num, name, vars, eqn) <- Binary.get+    return (Axiom num name vars eqn)++instance (Intern f, Binary f) => Binary (Proof f) where+  put = Binary.put . Shared . derivation+  get = certify . getShared <$> Binary.get+ foldLemmas :: (Intern f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a foldLemmas op ds =   execState (mapM_ foldGoal ds) Map.empty@@ -498,7 +517,7 @@     pres_lemmas :: [Proof f],     -- | The goals proved.     pres_goals  :: [ProvedGoal f] }-  deriving Show+  deriving (Show, Generic, Binary)  -- Note: only the pg_proof field should be trusted! -- The remaining fields are for information only.@@ -515,9 +534,10 @@     -- In general, subst pg_witness_hint pg_goal_hint == equation pg_proof.     -- For non-existential goals, pg_goal_hint == equation pg_proof     -- and pg_witness_hint is the empty substitution.+    pg_vars         :: Maybe (Map Var String),     pg_goal_hint    :: Equation f,     pg_witness_hint :: Subst f }-  deriving Show+  deriving (Show, Generic, Binary)  -- | Construct a @ProvedGoal@. provedGoal :: Int -> String -> Proof f -> ProvedGoal f@@ -526,6 +546,7 @@     pg_number = number,     pg_name = name,     pg_proof = proof,+    pg_vars = Nothing,     pg_goal_hint = equation proof,     pg_witness_hint = emptySubst } @@ -731,8 +752,11 @@       Symm <$> generaliseStep p     generaliseStep (Trans p q) =       liftM2 Trans (generaliseStep p) (generaliseStep q)-    generaliseStep (Cong f ps) =-      Cong f <$> mapM generaliseStep ps+    generaliseStep (Cong f ps) = do+      q <- cong f <$> mapM generaliseStep ps+      case q of+        Refl{} -> generaliseStep q+        _ -> return q      freshen xs f = do       n <- get@@ -842,19 +866,19 @@ pPrintPresentation :: forall f. Function f => Config f -> Presentation f -> Doc pPrintPresentation config (Presentation axioms lemmas goals) =   vcat $ intersperse (text "") $-    vcat [ describeEquation "Axiom" (axiomNum axiom) (Just name) eqn $$+    vcat [ describeEquation "Axiom" (axiomNum axiom) (Just name) vars eqn $$            ppAxiomUses axiom-         | axiom@(Axiom _ name eqn) <- axioms,+         | axiom@(Axiom _ name vars eqn) <- axioms,            not (invisible eqn) ]:-    [ pp "Lemma" (lemmaNum p) Nothing (equation p) emptySubst p+    [ pp "Lemma" (lemmaNum p) Nothing (equation p) Nothing emptySubst p     | p <- lemmas,       not (invisible (equation p)) ] ++-    [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_witness_hint pg_proof+    [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_vars pg_witness_hint pg_proof     | (num, ProvedGoal{..}) <- zip [1..] goals ]   where-    pp kind n mname eqn witness p =-      describeEquation kind n mname eqn $$-      ppWitness witness $$+    pp kind n mname eqn names witness p =+      describeEquation kind n mname names eqn $$+      ppWitness names witness $$       text "Proof:" $$       pPrintLemma config axiomNum lemmaNum p @@ -863,14 +887,18 @@     axiomNum x = show (fromJust (Map.lookup x axiomNums))     lemmaNum x = show (fromJust (Map.lookup x lemmaNums)) -    ppWitness sub+    ppWitness names sub       | sub == emptySubst = pPrintEmpty       | otherwise =           vcat [             text "The goal is true when:",             nest 2 $ vcat-              [ pPrint x <+> text "=" <+> pPrint t-              | (x, t) <- substToList sub ],+              [ text name <+> text "=" <+> pPrint t+              | (x, t) <- substToList sub,+                let name =+                      case names of+                        Nothing -> prettyShow x+                        Just names -> fromJust (Map.lookup x names) ],             if minimal `elem` funs sub then               text "where" <+> doubleQuotes (pPrint (minimal :: Sym f)) <+>               text "stands for an arbitrary term of your choice."@@ -900,14 +928,31 @@ -- Used both here and in the main file. describeEquation ::   Function f =>-  String -> String -> Maybe String -> Equation f -> Doc-describeEquation kind num mname eqn =+  String -> String -> Maybe String -> Maybe (Map Var String) -> Equation f -> Doc+describeEquation kind num mname mvars eqn =   text kind <+> text num <#>   (case mname of      Nothing -> text ""      Just name -> text (" (" ++ name ++ ")")) <#>-  text ":" <+> pPrint eqn <#> text "."+  text ":" <+> pPrint (prettyVars eqn) <#> text "."+  where+    var x =+      case mvars of+        Nothing -> prettyShow x+        Just vars -> fromJust (Map.lookup x vars)+    prettyVars (t :=: u) = build (pv t) :=: build (pv u)+    pv (Var x) = con (Sym (PrettyVar (var x)))+    pv (App (Sym f) ts) = app (Sym (PrettyFunc f)) (map pv (unpack ts)) +data PrettyVars f = PrettyVar String | PrettyFunc f+  deriving (Eq, Generic, Hashable)+instance Pretty f => Pretty (PrettyVars f) where+  pPrint (PrettyVar x) = text x+  pPrint (PrettyFunc f) = pPrint f+instance PrettyTerm f => PrettyTerm (PrettyVars f) where+  termStyle (PrettyVar _) = uncurried+  termStyle (PrettyFunc f) = termStyle f+ ---------------------------------------------------------------------- -- Making proofs of existential goals more readable. ----------------------------------------------------------------------@@ -945,16 +990,17 @@ decodeGoal config pg =   case maybeDecodeGoal config pg of     Nothing -> pg-    Just (name, witness, goal, deriv) ->+    Just (name, vars, witness, goal, deriv) ->       checkProvedGoal $       pg {         pg_name = name,         pg_proof = certify deriv,+        pg_vars = vars,         pg_goal_hint = goal,         pg_witness_hint = witness }  maybeDecodeGoal :: forall f. Function f =>-  Config f -> ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)+  Config f -> ProvedGoal f -> Maybe (String, Maybe (Map Var String), Subst f, Equation f, Derivation f) maybeDecodeGoal Config{..} ProvedGoal{..}   | not cfg_eliminate_existentials_coding = Nothing   --  N.B. presentWithGoals takes care of expanding any lemma which mentions@@ -977,11 +1023,11 @@     decodeReflexivity _ = Nothing      -- Detect $equals(t, u) = $false.-    decodeConjecture :: Derivation f -> Maybe (String, Equation f, Subst f)+    decodeConjecture :: Derivation f -> Maybe (String, Maybe (Map Var String), Equation f, Subst f)     decodeConjecture (UseAxiom Axiom{..} sub) = do       guard (isFalseTerm (eqn_rhs axiom_eqn))       (t, u) <- decodeEquality (eqn_lhs axiom_eqn)-      return (axiom_name, t :=: u, sub)+      return (axiom_name, axiom_vars, t :=: u, sub)     decodeConjecture _ = Nothing      extract (p:ps) = do@@ -993,10 +1039,10 @@     cont p1 p2 (p:ps)       | Just t <- decodeReflexivity p =         cont (Refl t) (Refl t) ps-      | Just (name, eqn, sub) <- decodeConjecture p =+      | Just (name, vars, eqn, sub) <- decodeConjecture p =         -- If p1: s=t and p2: s=u         -- then symm p1 `trans` p2: t=u.-        return (name, sub, eqn, symm p1 `trans` p2)+        return (name, vars, sub, eqn, symm p1 `trans` p2)       | Cong eq [p1', p2'] <- p, isEquals eq =         cont (p1 `trans` p1') (p2 `trans` p2') ps     cont _ _ _ = Nothing

@@ -1,5 +1,5 @@ -- | Term rewriting.-{-# LANGUAGE TypeFamilies, FlexibleContexts, RecordWildCards, BangPatterns, OverloadedStrings, MultiParamTypeClasses, ScopedTypeVariables, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings, MultiParamTypeClasses, DeriveAnyClass #-} module Twee.Rule where  import Twee.Base@@ -22,17 +22,16 @@ import Data.Tuple import Twee.Profile import Data.MemoUgly-import Debug.Trace-import Twee.Pretty-import Data.Function+--import Debug.Trace import Control.Arrow((***)) import GHC.Stack import Test.QuickCheck hiding (Function, subterms, Fun)-import Twee.Profile import Test.QuickCheck.Gen import Data.Semigroup import qualified Data.List.NonEmpty as NonEmpty import Test.QuickCheck.Random+import GHC.Generics+import Data.Binary.Sharing  -------------------------------------------------------------------------------- -- * Rewrite rules.@@ -48,13 +47,15 @@     -- For unoriented rules: vars lhs == vars rhs          -- | A proof that the rule holds.+    -- For efficiency, is not updated on substitution or on using 'backwards'.+    -- Use 'ruleDerivation' to extract a proof which accounts for this.     rule_proof :: !(Proof f),      -- | The left-hand side of the rule.     lhs :: {-# UNPACK #-} !(Term f),     -- | The right-hand side of the rule.     rhs :: {-# UNPACK #-} !(Term f) }-  deriving Show+  deriving (Show, Generic, Binary) instance Eq (Rule f) where   x == y = compare x y == EQ instance Ord (Rule f) where@@ -92,7 +93,7 @@   | Permutative [(Term f, Term f)]     -- | An unoriented rule.   | Unoriented-  deriving Show+  deriving (Show, Generic, Binary)  instance Eq (Orientation f) where _ == _ = True instance Ord (Orientation f) where compare _ _ = EQ@@ -542,6 +543,7 @@     cf_right :: Reduction1 f,     cf_orig_term :: Term f,     cf_orig_left :: Reduction1 f }+  deriving (Generic, Binary)  cf_left_term, cf_right_term :: ConfluenceFailure f -> Term f cf_left_term ConfluenceFailure{..} = result1 cf_term cf_left@@ -628,7 +630,7 @@     trace _ x = x     --normFirstStep t = trace (prettyShow (t, take 1 $ anywhere1 strat t)) $ head (head (anywhere1 strat t))     normSteps t = normaliseWith1 (const True) strat t-    normStepsVia r t = r `trans1` normSteps (result1 t r)+    --normStepsVia r t = r `trans1` normSteps (result1 t r)     norm =       memo $ \t ->         stamp "hasUNF.norm" $@@ -660,7 +662,7 @@     -- precondition: normR t r1 /= normR t r2     --conflict, conflict' :: Term f -> Reduction1 f -> Term f -> Reduction1 f -> Term f -> UNF f     conflict t rs1 u rs2 v = stamp "conflict" (conflict' t rs1 u rs2 v)-    conflict' t (r1:rs1) u (r2:rs2) v+    conflict' t (r1:_rs1) _u (r2:_rs2) _v       | trace "" $         trace ("Conflicting term: " ++ prettyShow t) $         trace ("Rule 1: " ++ prettyShow r1) $

@@ -1,4 +1,4 @@-{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts, TypeFamilies #-}+{-# LANGUAGE DeriveAnyClass #-} module Twee.Rule.Index(   RuleIndex(..),   empty, insert, delete,@@ -9,12 +9,14 @@ import Twee.Rule import Twee.Index hiding (insert, delete, empty) import qualified Twee.Index as Index+import GHC.Generics+import Data.Binary.Sharing(Binary)  data RuleIndex f a =   RuleIndex {     index_oriented :: !(Index f a),     index_all      :: !(Index f a) }-  deriving Show+  deriving (Show, Generic, Binary)  empty :: RuleIndex f a empty = RuleIndex Index.empty Index.empty

@@ -1,5 +1,4 @@ -- | A module which can run housekeeping tasks every so often.-{-# LANGUAGE RecordWildCards #-} module Twee.Task(Task, newTask, checkTask) where  import System.CPUTime

@@ -1,4 +1,4 @@--- | Terms and substitutions.+-- | Terms and substitutions -- -- Terms in twee are represented as arrays rather than as an algebraic data -- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Nil')@@ -13,7 +13,7 @@ --   * substitutions ('Substitution', 'Subst', 'subst'); --   * unification ('unify') and matching ('match'); --   * miscellaneous useful functions on terms.-{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables, CPP, DefaultSignatures #-}+{-# LANGUAGE PatternSynonyms, ViewPatterns, OverloadedStrings, CPP, DefaultSignatures, TypeApplications, GeneralizedNewtypeDeriving #-} {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-} #ifdef USE_LLVM {-# OPTIONS_GHC -fllvm #-}@@ -65,7 +65,6 @@  import Prelude hiding (lookup) import Twee.Term.Core hiding (F)-import qualified Twee.Term.Core as Core import Data.List hiding (lookup, find, singleton) import Data.Maybe #if __GLASGOW_HASKELL__ < 804@@ -73,10 +72,11 @@ #endif import Data.IntMap.Strict(IntMap) import qualified Data.IntMap.Strict as IntMap-import Control.Arrow((&&&)) import Twee.Utils import Data.Intern import GHC.Stack+import Data.Binary.Sharing+import Data.Hashable  -------------------------------------------------------------------------------- -- * A type class for builders@@ -211,6 +211,8 @@   Subst {     unSubst :: IntMap (TermList f) }   deriving (Eq, Ord)+instance Hashable (Subst f) where+  hashWithSalt s = hashWithSalt s . substToList  -- | Return the highest-number variable in a substitution plus 1. {-# INLINE substSize #-}@@ -351,7 +353,7 @@ matchListIn !sub !pat !t   | lenList t < lenList pat = Nothing   | otherwise =-    let +    let         loop !sub ConsSym{hd = pat, tl = pats, rest = pats1} !ts = do           ConsSym{hd = t, tl = ts, rest = ts1} <- Just ts           case (pat, t) of@@ -510,6 +512,34 @@     occurs _ _ _ = Just ()  --------------------------------------------------------------------------------+-- Serialisation.+--------------------------------------------------------------------------------++instance (Intern f, Binary f) => Binary (TermList f) where+  put t = put (unpack t)+  get = buildList <$> getList getTerm++type BinarydTerm f = Either Var (Sym f, TermList f)++instance (Intern f, Binary f) => Binary (Term f) where+  put (Var x) = put (Left x :: BinarydTerm f)+  put (App f ts) = put (Right (f, ts) :: BinarydTerm f)+  get = build <$> getTerm++getTerm :: forall f. (Intern f, Binary f) => Get (Builder f)+getTerm = do+  val <- get :: Get (BinarydTerm f)+  case val of+    Left x -> return (var x)+    Right (f, ts) -> return (app f ts)++instance (Intern f, Binary f) => Binary (Subst f) where+  put = put . substToList+  get = fromJust . listToSubst <$> get++deriving instance Binary Var++-------------------------------------------------------------------------------- -- Miscellaneous stuff. -------------------------------------------------------------------------------- @@ -731,3 +761,9 @@ -- | Compare the values of two 'Sym's. (<<) :: (Intern f, Ord f) => Sym f -> Sym f -> Bool f << g = unintern f < unintern g++instance Hashable (Term f) where+  hashWithSalt s = hashWithSalt s . singleton+instance Hashable (TermList f) where+  hashWithSalt s = hashWithSalt s . map root . subtermsList+deriving instance Hashable Var

@@ -2,8 +2,8 @@ -- This module contains all the low-level icky bits -- and provides primitives for building higher-level stuff. {-# LANGUAGE CPP, PatternSynonyms, ViewPatterns,-    MagicHash, UnboxedTuples, BangPatterns,-    RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving,+    MagicHash, UnboxedTuples,+    RankNTypes, GeneralizedNewtypeDeriving,     OverloadedStrings, RoleAnnotations #-} {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-} #ifdef USE_LLVM

@@ -1,6 +1,6 @@ -- | Miscellaneous utility functions. -{-# LANGUAGE CPP, MagicHash, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE CPP, MagicHash #-} module Twee.Utils where  import Control.Arrow((&&&))@@ -12,8 +12,9 @@ import GHC.Types import Data.Bits import System.Random-import Data.Serialize+import qualified Data.Set as Set --import Test.QuickCheck hiding ((.&.))+import Data.Binary.Sharing  repeatM :: Monad m => m a -> m [a] repeatM = sequence . repeat@@ -48,6 +49,15 @@ usortBy' :: Ord b => (a -> b) -> [a] -> [a] usortBy' f = map snd . usortBy (comparing fst) . map (\x -> (f x, x)) +-- Like usort but preserves order+fastNub :: Ord a => [a] -> [a]+fastNub xs = collect Set.empty xs+  where+    collect _ [] = []+    collect seen (x:xs)+      | x `Set.member` seen = collect seen xs+      | otherwise = x:collect (Set.insert x seen) xs+ orElse :: Ordering -> Ordering -> Ordering EQ `orElse` x = x x  `orElse` _ = x@@ -143,6 +153,12 @@     prefix = [0..k-1]  data Sample a = Sample Integer [(Integer, Int)] [a]+-- TODO serialise properly+instance Binary a => Binary (Sample a) where+  put _ = put ()+  get = do+    () <- get+    return (emptySample 10)  emptySample :: Int -> Sample a emptySample k = Sample 0 (reservoir k) []@@ -178,41 +194,6 @@ 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

@@ -1,7 +1,7 @@ name:                twee-lib-version:             2.6.1+version:             2.7.1 synopsis:            An equational theorem prover-homepage:            http://github.com/nick8325/twee+homepage:            http://smallbone.se license:             BSD3 license-file:        LICENSE author:              Nick Smallbone@@ -26,8 +26,8 @@  source-repository head   type:     git-  location: https://github.com/nick8325/twee.git-  branch:   master+  location: https://codeberg.org/nick8325/twee+  branch:   main  flag llvm   description: Build using LLVM backend for faster code.@@ -55,6 +55,7 @@     Twee.Index     Twee.Join     Twee.KBO+    Twee.LPO     Twee.Pretty     Twee.Profile     Twee.Proof@@ -65,7 +66,7 @@     Twee.Utils     Twee.Term.Core     Data.Intern-  other-modules:+    Data.Binary.Sharing     Data.BatchedQueue     Data.ChurchList     Data.DynamicArray@@ -83,14 +84,26 @@     ghc-prim,     primitive >= 0.7.1.0,     uglymemo,-    random,+    random >= 1.2,     bytestring,-    cereal,-    QuickCheck+    binary,+    QuickCheck,+    deepseq >= 1.4.0.0,+    unordered-containers,+    hashable   hs-source-dirs:      .-  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports -fno-warn-x-partial+  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports -fno-warn-deprecations   default-language:    Haskell2010-  default-extensions:  TypeOperators+  default-extensions:+    BangPatterns+    DeriveGeneric+    FlexibleContexts+    PatternGuards+    RecordWildCards+    ScopedTypeVariables+    StandaloneDeriving+    TypeFamilies+    TypeOperators    if flag(llvm)     cpp-options: -DUSE_LLVM