diff --git a/Data/ChurchList.hs b/Data/ChurchList.hs --- a/Data/ChurchList.hs +++ b/Data/ChurchList.hs @@ -1,4 +1,4 @@ --- Church-encoded lists. Used in Twee.CP to make sure that fusion happens. +-- | Church-encoded lists. Used in Twee.CP to make sure that fusion happens. {-# LANGUAGE Rank2Types, BangPatterns #-} module Data.ChurchList where diff --git a/Data/DynamicArray.hs b/Data/DynamicArray.hs --- a/Data/DynamicArray.hs +++ b/Data/DynamicArray.hs @@ -19,16 +19,18 @@ -- | An array. data Array a = Array { - -- | The size of the array. - arraySize :: {-# UNPACK #-} !Int, + arrayStart :: {-# UNPACK #-} !Int, -- | The contents of the array. arrayContents :: {-# UNPACK #-} !(P.SmallArray a) } +arraySize :: Array a -> Int +arraySize = P.sizeofSmallArray . arrayContents + -- | Convert an array to a list of (index, value) pairs. {-# INLINE toList #-} toList :: Array a -> [(Int, a)] toList arr = - [ (i, x) + [ (i+arrayStart arr, x) | i <- [0..arraySize arr-1], let x = P.indexSmallArray (arrayContents arr) i ] @@ -41,12 +43,18 @@ "}" -- | Create an empty array. +{-# NOINLINE newArray #-} newArray :: Array a newArray = runST $ do marr <- P.newSmallArray 0 undefined arr <- P.unsafeFreezeSmallArray marr - return (Array 0 arr) + return (Array maxBound arr) +{-# INLINE singleton #-} +-- | Create an array with one element. +singleton :: Default a => Int -> a -> Array a +singleton i x = update i x newArray + -- | Index into an array. O(1) time. {-# INLINE (!) #-} (!) :: Default a => Array a -> Int -> a @@ -56,8 +64,8 @@ {-# INLINE getWithDefault #-} getWithDefault :: a -> Int -> Array a -> a getWithDefault def n arr - | 0 <= n && n < arraySize arr = - P.indexSmallArray (arrayContents arr) n + | arrayStart arr <= n && n < arrayStart arr + arraySize arr = + P.indexSmallArray (arrayContents arr) (n - arrayStart arr) | otherwise = def -- | Update the array. O(n) time. @@ -68,9 +76,10 @@ {-# INLINEABLE updateWithDefault #-} updateWithDefault :: a -> Int -> a -> Array a -> Array a updateWithDefault def n x arr = runST $ do - let size = arraySize arr `max` (n+1) + let size = if arraySize arr == 0 then 1 else if n < arrayStart arr then arraySize arr + (arrayStart arr - n) else arraySize arr `max` (n+1) + start = n `min` arrayStart arr marr <- P.newSmallArray size def - P.copySmallArray marr 0 (arrayContents arr) 0 (arraySize arr) - P.writeSmallArray marr n $! x + P.copySmallArray marr (arrayStart arr - start) (arrayContents arr) 0 (arraySize arr) + P.writeSmallArray marr (n - start) $! x arr' <- P.unsafeFreezeSmallArray marr - return (Array size arr') + return (Array start arr') diff --git a/Data/Label.hs b/Data/Label.hs new file mode 100644 --- /dev/null +++ b/Data/Label.hs @@ -0,0 +1,133 @@ +-- | Assignment of unique IDs to values. +-- Inspired by the 'intern' package. + +{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations #-} +module Data.Label(Label, unsafeMkLabel, labelNum, label, find) where + +import Data.IORef +import System.IO.Unsafe +import qualified Data.Map.Strict as Map +import Data.Map.Strict(Map) +import qualified Data.DynamicArray as DynamicArray +import Data.DynamicArray(Array) +import Data.Typeable +import GHC.Exts +import GHC.Int +import Unsafe.Coerce + +-- | A value of type @a@ which has been given a unique ID. +newtype Label a = + Label { + -- | The unique ID of a label. + labelNum :: Int32 } + deriving (Eq, Ord, Show) + +type role Label nominal + +-- | Construct a @'Label' a@ from its unique ID, which must be the 'labelNum' of +-- an already existing 'Label'. Extremely unsafe! +unsafeMkLabel :: Int32 -> Label a +unsafeMkLabel = Label + +-- The global cache of labels. +{-# NOINLINE cachesRef #-} +cachesRef :: IORef Caches +cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray)) + +data Caches = + Caches { + -- The next id number to assign. + caches_nextId :: {-# UNPACK #-} !Int32, + -- A map from values to labels. + caches_from :: !(Map TypeRep (Cache Any)), + -- The reverse map from labels 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 + -- compare-and-swap. This causes bad things to happen when 'label' + -- is used reentrantly (i.e. the Ord instance itself calls label). + -- This function only lets the swap happen if caches_nextId didn't + -- change (i.e., no new values were inserted). + !caches <- readIORef cachesRef + -- First compute the update. + let !(!caches', !x) = f caches + -- Now see if anyone else updated the cache in between + -- (can happen if f called 'label', or in a concurrent setting). + ok <- atomicModifyIORef' cachesRef $ \cachesNow -> + if caches_nextId caches == caches_nextId cachesNow + then (caches', True) + else (cachesNow, False) + if ok then return x else atomicModifyCaches f + +-- Versions of unsafeCoerce with slightly more type checking +toAnyCache :: Cache a -> Cache Any +toAnyCache = unsafeCoerce + +fromAnyCache :: Cache Any -> Cache a +fromAnyCache = unsafeCoerce + +toAny :: a -> Any +toAny = unsafeCoerce + +fromAny :: Any -> a +fromAny = unsafeCoerce + +-- | Assign a label to a value. +{-# NOINLINE label #-} +label :: forall a. (Typeable a, Ord a) => a -> Label a +label x = + unsafeDupablePerformIO $ do + -- Common case: label is already there. + caches <- readIORef cachesRef + case tryFind caches of + Just l -> return l + Nothing -> do + -- Rare case: label was not there. + x <- atomicModifyCaches $ \caches -> + case tryFind caches of + Just l -> (caches, l) + Nothing -> + insert caches + return x + + where + ty = typeOf x + + tryFind :: Caches -> Maybe (Label a) + tryFind Caches{..} = + Label <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache) + + insert :: Caches -> (Caches, Label 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_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to }, + Label n) + where + n = caches_nextId + cache = + fromAnyCache $ + Map.findWithDefault Map.empty ty caches_from + +-- | Recover the underlying value from a label. +find :: Label a -> a +-- N.B. must force n before calling readIORef, otherwise a call of +-- the form +-- find (label x) +-- doesn't work. +find (Label !(I32# n#)) = findWorker n# + +{-# NOINLINE findWorker #-} +findWorker :: Int# -> a +findWorker n# = + unsafeDupablePerformIO $ do + let n = I32# n# + Caches{..} <- readIORef cachesRef + x <- return $! fromAny (DynamicArray.getWithDefault undefined (fromIntegral n) caches_to) + return x diff --git a/Data/Numbered.hs b/Data/Numbered.hs new file mode 100644 --- /dev/null +++ b/Data/Numbered.hs @@ -0,0 +1,65 @@ +module Data.Numbered( + Numbered, + empty, fromList, singleton, toList, size, (!), + lookup, put, modify, filter, delete) where + +import Prelude hiding (filter, lookup) +import qualified Data.List as List +import Data.Primitive.ByteArray +import Data.Primitive.SmallArray +import Data.Int +import Data.Maybe + +data Numbered a = + Numbered + {-# UNPACK #-} !ByteArray + {-# UNPACK #-} !(SmallArray a) + +instance Show a => Show (Numbered a) where show = show . toList + +empty :: Numbered a +empty = fromList [] + +singleton :: Int -> a -> Numbered a +singleton i x = fromList [(i, x)] + +fromList :: [(Int, a)] -> Numbered a +fromList xs = + Numbered + (byteArrayFromList (map (fromIntegral . fst) xs :: [Int32])) + (smallArrayFromList (map snd xs)) + +toList :: Numbered a -> [(Int, a)] +toList num = + [num ! i | i <- [0..size num-1]] + +size :: Numbered a -> Int +size (Numbered _ elems) = sizeofSmallArray elems + +(!) :: Numbered a -> Int -> (Int, a) +Numbered idxs elems ! i = + (fromIntegral (indexByteArray idxs i :: Int32), + indexSmallArray elems i) + +lookup :: Int -> Numbered a -> Maybe a +lookup i num = + List.lookup i (toList num) + +put :: Int -> a -> Numbered a -> Numbered a +put i x num = + fromList $ lt ++ [(i, x)] ++ gt + where + xs = toList num + lt = List.filter ((< i) . fst) xs + gt = List.filter ((> i) . fst) xs + +delete :: Int -> Numbered a -> Numbered a +delete i = fromList . List.filter ((/= i) . fst) . toList + +modify :: Int -> a -> (a -> a) -> Numbered a -> Numbered a +modify i def f num = + put i (f (fromMaybe def (lookup i num))) num + +filter :: (a -> Bool) -> Numbered a -> Numbered a +filter p = fromList . List.filter (p . snd) . toList + diff --git a/Twee.hs b/Twee.hs --- a/Twee.hs +++ b/Twee.hs @@ -29,13 +29,13 @@ import qualified Data.Map.Strict as Map import Data.Map(Map) import Data.Int -import Data.Ord import Control.Monad import Control.Monad.IO.Class import Control.Monad.Trans.Class import qualified Control.Monad.Trans.State.Strict as StateM import qualified Data.IntSet as IntSet import Data.IntSet(IntSet) +import Twee.Profile ---------------------------------------------------------------------- -- * Configuration and prover state. @@ -61,19 +61,15 @@ -- | The prover state. data State f = State { - st_rules :: !(RuleIndex f (ActiveRule f)), - st_active_ids :: !(IntMap (Active f)), - st_rule_ids :: !(IntMap (ActiveRule f)), + st_rules :: !(RuleIndex f (Rule f)), + st_active_set :: !(IntMap (Active f)), st_joinable :: !(Index f (Equation f)), st_goals :: ![Goal f], st_queue :: !(Queue Params), st_next_active :: {-# UNPACK #-} !Id, - st_next_rule :: {-# UNPACK #-} !RuleId, st_considered :: {-# UNPACK #-} !Int64, st_simplified_at :: {-# UNPACK #-} !Id, - st_cp_sample :: ![Maybe (Overlap f)], - st_cp_next_sample :: ![(Integer, Int)], - st_num_cps :: !Integer, + st_cp_sample :: !(Sample (Maybe (Overlap (Active f) f))), st_not_complete :: !IntSet, st_complete :: !(Index f (Rule f)), st_messages_rev :: ![Message f] } @@ -108,18 +104,14 @@ initialState Config{..} = State { st_rules = RuleIndex.empty, - st_active_ids = IntMap.empty, - st_rule_ids = IntMap.empty, + st_active_set = IntMap.empty, st_joinable = Index.empty, st_goals = [], st_queue = Queue.empty, st_next_active = 1, - st_next_rule = 0, st_considered = 0, st_simplified_at = 1, - st_cp_sample = [], - st_cp_next_sample = reservoir cfg_cp_sample_size, - st_num_cps = 0, + st_cp_sample = emptySample cfg_cp_sample_size, st_not_complete = IntSet.empty, st_complete = Index.empty, st_messages_rev = [] } @@ -185,7 +177,7 @@ data Params instance Queue.Params Params where type Score Params = Int - type Id Params = RuleId + type Id Params = Id type PackedId Params = Int32 type PackedScore Params = Int32 packScore _ = fromIntegral @@ -195,49 +187,60 @@ -- | Compute all critical pairs from a rule. {-# INLINEABLE makePassives #-} -{-# SCC makePassives #-} -makePassives :: Function f => Config f -> State f -> ActiveRule f -> [Passive Params] -makePassives Config{..} State{..} rule = - [ Passive (fromIntegral (score cfg_critical_pairs o)) (rule_rid rule1) (rule_rid rule2) (fromIntegral (overlap_pos o)) - | (rule1, rule2, o) <- overlaps (Depth cfg_max_cp_depth) (index_oriented st_rules) rules rule ] +makePassives :: Function f => Config f -> State f -> Active f -> [Passive Params] +makePassives config@Config{..} State{..} rule = +-- XXX factor out depth calculation + stampWith "make critical pair" length + [ makePassive config overlap + | ok rule, + overlap <- overlaps (index_oriented st_rules) (filter ok rules) rule ] where - rules = IntMap.elems st_rule_ids + rules = IntMap.elems st_active_set + ok rule = the rule < Depth cfg_max_cp_depth +{-# INLINEABLE makePassive #-} +makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive Params +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 } + 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 #-} -{-# SCC findPassive #-} -findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (ActiveRule f, ActiveRule f, Overlap f) +findPassive :: forall f. Function f => State f -> Passive Params -> Maybe (Overlap (Active f) f) findPassive State{..} Passive{..} = do - rule1 <- IntMap.lookup (fromIntegral passive_rule1) st_rule_ids - rule2 <- IntMap.lookup (fromIntegral passive_rule2) st_rule_ids - let !depth = 1 + max (the rule1) (the rule2) - overlap <- - overlapAt (fromIntegral passive_pos) depth - (renameAvoiding (the rule2 :: Rule f) (the rule1)) (the rule2) - return (rule1, rule2, overlap) + rule1 <- IntMap.lookup (fromIntegral passive_rule1) st_active_set + rule2 <- IntMap.lookup (fromIntegral passive_rule2) st_active_set + overlapAt (unpackHow passive_pos) rule1 rule2 + (renameAvoiding (the rule2 :: Rule f) (the rule1)) (the rule2) -- | Renormalise a queued Passive. {-# INLINEABLE simplifyPassive #-} -{-# SCC simplifyPassive #-} simplifyPassive :: Function f => Config f -> State f -> Passive Params -> Maybe (Passive Params) simplifyPassive Config{..} state@State{..} passive = do - (_, _, overlap) <- findPassive state passive + overlap <- findPassive state passive overlap <- simplifyOverlap (index_oriented st_rules) overlap + let r1 = overlap_rule1 overlap + r2 = overlap_rule2 overlap return passive { passive_score = fromIntegral $ fromIntegral (passive_score passive) `intMin` - score cfg_critical_pairs overlap } + -- XXX factor out depth calculation + score cfg_critical_pairs (succ (the r1 `max` the r2)) overlap } -- | Check if we should renormalise the queue. {-# INLINEABLE shouldSimplifyQueue #-} shouldSimplifyQueue :: Function f => Config f -> State f -> Bool shouldSimplifyQueue Config{..} State{..} = - length (filter isNothing st_cp_sample) * 100 >= cfg_renormalise_threshold * cfg_cp_sample_size + length (filter isNothing (sampleValue st_cp_sample)) * 100 >= cfg_renormalise_threshold * cfg_cp_sample_size -- | Renormalise the entire queue. {-# INLINEABLE simplifyQueue #-} -{-# SCC simplifyQueue #-} simplifyQueue :: Function f => Config f -> State f -> State f simplifyQueue config state = resetSample config state { st_queue = simp (st_queue state) } @@ -247,8 +250,7 @@ -- | Enqueue a set of critical pairs. {-# INLINEABLE enqueue #-} -{-# SCC enqueue #-} -enqueue :: Function f => State f -> RuleId -> [Passive Params] -> State f +enqueue :: Function f => State f -> Id -> [Passive Params] -> State f enqueue state rule passives = state { st_queue = Queue.insert rule passives (st_queue state) } @@ -259,8 +261,7 @@ -- * removing any orphans from the head of the queue -- * ignoring CPs that are too big {-# INLINEABLE dequeue #-} -{-# SCC dequeue #-} -dequeue :: Function f => Config f -> State f -> (Maybe (CriticalPair f, ActiveRule f, ActiveRule f), State f) +dequeue :: Function f => Config f -> State f -> (Maybe (Info, CriticalPair f, Active f, Active f), State f) dequeue Config{..} state@State{..} = case deq 0 st_queue of -- Explicitly make the queue empty, in case it e.g. contained a @@ -273,13 +274,19 @@ deq !n queue = do (passive, queue) <- Queue.removeMin queue case findPassive state passive of - Just (rule1, rule2, overlap@Overlap{overlap_eqn = t :=: u}) + 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 rule1 rule2 overlap -> - return ((cp, rule1, rule2), n+1, queue) + cp <- makeCriticalPair overlap -> + return ((combineInfo (active_info rule1) (active_info rule2), cp, rule1, rule2), n+1, 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_max = IntSet.union (info_max i1) (info_max i2) } + ---------------------------------------------------------------------- -- * Active rewrite rules. ---------------------------------------------------------------------- @@ -287,117 +294,86 @@ data Active f = Active { active_id :: {-# UNPACK #-} !Id, - active_depth :: {-# UNPACK #-} !Depth, + active_info :: {-# UNPACK #-} !Info, active_rule :: {-# UNPACK #-} !(Rule f), active_top :: !(Maybe (Term f)), active_proof :: {-# UNPACK #-} !(Proof f), - active_max :: !Max, -- A model in which the rule is false (used when reorienting) active_model :: !(Model f), - active_rules :: ![ActiveRule f] } + active_positions :: !(Positions2 f) } active_cp :: Active f -> CriticalPair f active_cp Active{..} = CriticalPair { cp_eqn = unorient active_rule, - cp_depth = active_depth, - cp_max = active_max, cp_top = active_top, cp_proof = derivation active_proof } --- An active oriented in a particular direction. -data ActiveRule f = - ActiveRule { - rule_active :: {-# UNPACK #-} !Id, - rule_rid :: {-# UNPACK #-} !RuleId, - rule_depth :: {-# UNPACK #-} !Depth, - rule_max :: !Max, - rule_rule :: {-# UNPACK #-} !(Rule f), - rule_positions :: !(Positions f) } +activeRules :: Active f -> [Rule f] +activeRules Active{..} = + case active_positions of + ForwardsPos _ -> [active_rule] + BothPos _ _ -> [active_rule, backwards active_rule] -instance PrettyTerm f => Symbolic (ActiveRule f) where - type ConstantOf (ActiveRule f) = f - termsDL ActiveRule{..} = - termsDL rule_rule - subst_ sub r@ActiveRule{..} = - r { - rule_rule = rule', - rule_positions = positions (lhs rule') } - where - rule' = subst_ sub rule_rule +data Info = + Info { + info_depth :: {-# UNPACK #-} !Depth, + info_max :: !IntSet } instance Eq (Active f) where (==) = (==) `on` active_id -instance Eq (ActiveRule f) where - (==) = (==) `on` rule_rid - instance Function f => Pretty (Active f) where pPrint Active{..} = pPrint active_id <#> text "." <+> pPrint (canonicalise active_rule) -instance Has (ActiveRule f) Id where the = rule_active -instance Has (ActiveRule f) RuleId where the = rule_rid -instance Has (ActiveRule f) Depth where the = rule_depth -instance Has (ActiveRule f) Max where the = rule_max -instance f ~ g => Has (ActiveRule f) (Rule g) where the = rule_rule -instance f ~ g => Has (ActiveRule f) (Positions g) where the = rule_positions - -newtype RuleId = RuleId Id deriving (Eq, Ord, Show, Num, Real, Integral, Enum) +instance Has (Active f) Id where the = active_id +instance Has (Active f) Depth where the = info_depth . active_info +instance f ~ g => Has (Active f) (Rule g) where the = active_rule +instance f ~ g => Has (Active f) (Positions2 g) where the = active_positions -- Add a new active. {-# INLINEABLE addActive #-} -{-# SCC addActive #-} -addActive :: Function f => Config f -> State f -> (Id -> RuleId -> RuleId -> Active f) -> State f +addActive :: Function f => Config f -> State f -> (Id -> Active f) -> State f addActive config state@State{..} active0 = let - active@Active{..} = active0 st_next_active st_next_rule (succ st_next_rule) + active@Active{..} = active0 st_next_active state' = message (NewActive active) $ - addActiveOnly state{st_next_active = st_next_active+1, st_next_rule = st_next_rule+2} active + addActiveOnly state{st_next_active = st_next_active+1} active in if subsumed (st_joinable, st_complete) st_rules (unorient active_rule) then state else normaliseGoals config $ - foldl' enqueueRule state' active_rules + enqueueRule state' active where enqueueRule state rule = - sample config (length passives) passives $ + sample (length passives) passives $ enqueue state (the rule) passives where passives = makePassives config state rule -- Update the list of sampled critical pairs. {-# INLINEABLE sample #-} -sample :: Function f => Config f -> Int -> [Passive Params] -> State f -> State f -sample cfg m passives state@State{st_cp_next_sample = ((n, pos):rest), ..} - | idx < fromIntegral m = - sample cfg m passives state { - st_cp_next_sample = rest, - st_cp_sample = - take pos st_cp_sample ++ - [find (passives !! fromIntegral idx)] ++ - drop (pos+1) st_cp_sample } - | otherwise = state{st_num_cps = st_num_cps + fromIntegral m} +sample :: Function f => Int -> [Passive Params] -> State f -> State f +sample m passives state@State{..} = + state{st_cp_sample = addSample (m, map find passives) st_cp_sample} where - idx = n - st_num_cps find passive = do - (_, _, overlap) <- findPassive state passive + overlap <- findPassive state passive simplifyOverlap (index_oriented st_rules) overlap -- Reset the list of sampled critical pairs. {-# INLINEABLE resetSample #-} resetSample :: Function f => Config f -> State f -> State f -resetSample cfg@Config{..} state@State{..} = +resetSample Config{..} state@State{..} = foldl' sample1 state' (Queue.toList st_queue) where state' = state { - st_num_cps = 0, - st_cp_next_sample = reservoir cfg_cp_sample_size, - st_cp_sample = [] } + st_cp_sample = emptySample cfg_cp_sample_size } - sample1 state (n, passives) = sample cfg n passives state + sample1 state (n, passives) = sample n passives state -- Simplify the sampled critical pairs. -- (A sampled critical pair is replaced with Nothing if it can be @@ -405,7 +381,7 @@ {-# INLINEABLE simplifySample #-} simplifySample :: Function f => State f -> State f simplifySample state@State{..} = - state{st_cp_sample = map (>>= simp) st_cp_sample} + state{st_cp_sample = mapSample (>>= simp) st_cp_sample} where simp overlap = do overlap' <- simplifyOverlap (index_oriented st_rules) overlap @@ -417,97 +393,76 @@ addActiveOnly :: Function f => State f -> Active f -> State f addActiveOnly state@State{..} active@Active{..} = state { - st_rules = foldl' insertRule st_rules active_rules, - st_active_ids = IntMap.insert (fromIntegral active_id) active st_active_ids, - st_rule_ids = foldl' insertRuleId st_rule_ids active_rules } + st_rules = foldl' insertRule st_rules (activeRules active), + st_active_set = IntMap.insert (fromIntegral active_id) active st_active_set } where - insertRule rules rule@ActiveRule{..} = - RuleIndex.insert (lhs rule_rule) rule rules - insertRuleId rules rule@ActiveRule{..} = - IntMap.insert (fromIntegral rule_rid) rule rules + insertRule rules rule = + RuleIndex.insert (lhs rule) rule rules -- Delete an active. Used in interreduction, not suitable for general use. {-# INLINE deleteActive #-} deleteActive :: Function f => State f -> Active f -> State f -deleteActive state@State{..} Active{..} = +deleteActive state@State{..} active@Active{..} = state { - st_rules = foldl' deleteRule st_rules active_rules, - st_active_ids = IntMap.delete (fromIntegral active_id) st_active_ids, - st_rule_ids = foldl' deleteRuleId st_rule_ids active_rules } + st_rules = foldl' deleteRule st_rules (activeRules active), + st_active_set = IntMap.delete (fromIntegral active_id) st_active_set } where deleteRule rules rule = - RuleIndex.delete (lhs (rule_rule rule)) rule rules - deleteRuleId rules ActiveRule{..} = - IntMap.delete (fromIntegral rule_rid) rules + RuleIndex.delete (lhs rule) rule rules -- Try to join a critical pair. {-# INLINEABLE consider #-} -consider :: Function f => Config f -> State f -> CriticalPair f -> State f -consider config state cp = - considerUsing (st_rules state) config state cp +consider :: Function f => Config f -> State f -> Info -> CriticalPair f -> State f +consider config state info cp = + considerUsing (st_rules state) config state info cp -- Try to join a critical pair, but using a different set of critical -- pairs for normalisation. {-# INLINEABLE considerUsing #-} -{-# SCC considerUsing #-} considerUsing :: Function f => - RuleIndex f (ActiveRule f) -> Config f -> State f -> CriticalPair f -> State f -considerUsing rules config@Config{..} state@State{..} cp0 = + RuleIndex f (Rule f) -> Config f -> State f -> Info -> CriticalPair f -> State f +considerUsing rules config@Config{..} state@State{..} info cp0 = + stamp "consider critical pair" $ -- Important to canonicalise the rule so that we don't get -- bigger and bigger variable indices over time let cp = canonicalise cp0 in case joinCriticalPair cfg_join (st_joinable, st_complete) rules Nothing cp of Right (mcp, cps) -> let - state' = foldl' (considerUsing rules config) state cps + state' = foldl' (\state cp -> considerUsing rules config state info cp) state cps in case mcp of Just cp -> addJoinable state' (cp_eqn cp) Nothing -> state' Left (cp, model) -> - foldl' (addCP config model) state (split cp) + foldl' (\state cp -> addCP config model state info cp) state (split cp) {-# INLINEABLE addCP #-} -addCP :: Function f => Config f -> Model f -> State f -> CriticalPair f -> State f -addCP config model state@State{..} CriticalPair{..} = +addCP :: Function f => Config f -> Model f -> State f -> Info -> CriticalPair f -> State f +addCP config model state@State{..} info CriticalPair{..} = let pf = certify cp_proof rule = orient cp_eqn pf - - makeRule n k r = - ActiveRule { - rule_active = n, - rule_rid = k, - rule_depth = cp_depth, - rule_max = cp_max, - rule_rule = r rule, - rule_positions = positions (lhs (r rule)) } in - addActive config state $ \n k1 k2 -> + addActive config state $ \n -> Active { active_id = n, - active_depth = cp_depth, + active_info = info, active_rule = rule, active_model = model, active_top = cp_top, - active_max = cp_max, active_proof = pf, - active_rules = - usortBy (comparing (canonicalise . rule_rule)) $ - makeRule n k1 id: - [ makeRule n k2 backwards - | not (oriented (orientation rule)) ] } + active_positions = positionsRule rule } -- Add a new equation. {-# INLINEABLE addAxiom #-} addAxiom :: Function f => Config f -> State f -> Axiom f -> State f addAxiom config state axiom = - consider config state $ + consider config state + Info { info_depth = 0, info_max = IntSet.fromList [axiom_number axiom | cfg_complete_subsets config] } CriticalPair { cp_eqn = axiom_eqn axiom, - cp_depth = 0, - cp_max = Max $ IntSet.fromList [axiom_number axiom | cfg_complete_subsets config], cp_top = Nothing, cp_proof = Proof.axiom axiom } @@ -530,7 +485,7 @@ st_complete = Index.fromListWith lhs rules } where maxSet s = if IntSet.null s then minBound else IntSet.findMax s - maxN = maximum [maxSet (unMax (active_max r)) | r <- IntMap.elems (st_active_ids state)] + maxN = maximum [maxSet (info_max (active_info r)) | r <- IntMap.elems (st_active_set state)] excluded = go IntSet.empty go excl | m > maxN = excl @@ -541,20 +496,20 @@ bound excl = minimum . map (passiveMax excl) . concatMap snd . Queue.toList $ st_queue state passiveMax excl p = fromMaybe maxBound $ do - (r1, r2, _) <- findPassive state p - let s = unMax (rule_max r1) `IntSet.union` unMax (rule_max r2) + Overlap{overlap_rule1 = r1, overlap_rule2 = r2} <- findPassive state p + let s = info_max (active_info r1) `IntSet.union` info_max (active_info r2) guard (s `IntSet.disjoint` excl) (n, _) <- IntSet.maxView s return n - rules = map rule_rule (filter ok (IntMap.elems (st_rule_ids state))) - ok r = unMax (rule_max r) `IntSet.disjoint` excluded + rules = concatMap activeRules (filter ok (IntMap.elems (st_active_set state))) + ok r = info_max (active_info r) `IntSet.disjoint` excluded -- Assume that all rules form a confluent rewrite system. {-# INLINEABLE assumeComplete #-} assumeComplete :: Function f => State f -> State f assumeComplete state = state { st_not_complete = IntSet.empty, - st_complete = Index.fromListWith lhs (map rule_rule (IntMap.elems (st_rule_ids state))) } + st_complete = Index.fromListWith lhs (concatMap activeRules (IntMap.elems (st_active_set state))) } -- For goal terms we store the set of all their normal forms. -- Name and number are for information only. @@ -663,7 +618,6 @@ -- Simplify all rules. {-# INLINEABLE interreduce #-} -{-# SCC interreduce #-} interreduce :: Function f => Config f -> State f -> State f interreduce _ state@State{..} | st_simplified_at == st_next_active = state interreduce config@Config{..} state = @@ -673,30 +627,30 @@ -- Clear out st_joinable, since we don't know which -- equations have made use of each active. state { st_joinable = Index.empty, st_complete = Index.empty } - (IntMap.elems (st_active_ids state)) + (IntMap.elems (st_active_set state)) in state' { st_joinable = st_joinable state, st_complete = st_complete state, st_simplified_at = st_next_active state' } {-# INLINEABLE interreduce1 #-} interreduce1 :: Function f => Config f -> State f -> Active f -> State f -interreduce1 config@Config{..} state active = +interreduce1 config@Config{..} state active@Active{..} = -- Exclude the active from the rewrite rules when testing -- joinability, otherwise it will be trivially joinable. case joinCriticalPair cfg_join (Index.empty, Index.empty) -- (st_joinable state) (st_rules (deleteActive state active)) - (Just (active_model active)) (active_cp active) + (Just active_model) (active_cp active) of Right (_, cps) -> - flip (foldl' (consider config)) cps $ + 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 (foldl' (consider config)) (split cp) $ + flip (foldl' (\state cp -> consider config state active_info cp)) (split cp) $ message (DeleteActive active) $ deleteActive state active - | model /= active_model active -> + | model /= active_model -> flip addActiveOnly active { active_model = model } $ deleteActive state active | otherwise -> @@ -763,8 +717,8 @@ | otherwise = case dequeue config state of (Nothing, state) -> (False, state) - (Just (overlap, _, _), state) -> - (True, consider config state overlap) + (Just (info, overlap, _, _), state) -> + (True, consider config state info overlap) {-# INLINEABLE solved #-} solved :: Function f => State f -> Bool @@ -772,7 +726,6 @@ -- Return whatever goals we have proved and their proofs. {-# INLINEABLE solutions #-} -{-# SCC solutions #-} solutions :: Function f => State f -> [ProvedGoal f] solutions State{..} = do Goal{goal_lhs = ts, goal_rhs = us, ..} <- st_goals @@ -794,7 +747,7 @@ -- Return all current rewrite rules. {-# INLINEABLE rules #-} rules :: Function f => State f -> [Rule f] -rules = map active_rule . IntMap.elems . st_active_ids +rules = map active_rule . IntMap.elems . st_active_set ---------------------------------------------------------------------- -- For code which uses twee as a library. diff --git a/Twee/Base.hs b/Twee/Base.hs --- a/Twee/Base.hs +++ b/Twee/Base.hs @@ -25,7 +25,7 @@ import Twee.Constraints hiding (funs) import Data.DList(DList) import Data.Int -import Data.List +import Data.List hiding (singleton) import Data.Maybe import qualified Data.IntMap.Strict as IntMap @@ -120,9 +120,6 @@ class Has a b where -- | Get at the thing. the :: a -> b - -instance Has a a where - the = id -- | Find the variables occurring in the argument. {-# INLINE vars #-} diff --git a/Twee/CP.hs b/Twee/CP.hs --- a/Twee/CP.hs +++ b/Twee/CP.hs @@ -8,22 +8,20 @@ import Twee.Index(Index) import qualified Data.Set as Set import Control.Monad -import Data.List +import Data.List hiding (singleton) import qualified Data.ChurchList as ChurchList import Data.ChurchList (ChurchList(..)) import Twee.Utils import Twee.Equation import qualified Twee.Proof as Proof import Twee.Proof(Derivation, congPath) -import Data.IntSet(IntSet) -import qualified Data.IntSet as IntSet - -newtype Max = Max { unMax :: IntSet } - deriving (Eq, Ord, Show) +import Data.Bits -- | The set of positions at which a term can have critical overlaps. data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f) 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) instance Show (Positions f) where show = show . ChurchList.toList . positionsChurch @@ -39,6 +37,14 @@ | t `Set.member` m = aux (n+1) m u | otherwise = ConsP n (aux (n+1) (Set.insert t m) u) +-- | Calculate the set of positions for a rule. +positionsRule :: Rule f -> Positions2 f +positionsRule rule + | oriented (orientation rule) || + canonicalise rule == canonicalise (backwards rule) = + ForwardsPos (positions (lhs rule)) + | otherwise = BothPos (positions (lhs rule)) (positions (rhs rule)) + {-# INLINE positionsChurch #-} positionsChurch :: Positions f -> ChurchList Int positionsChurch posns = @@ -50,82 +56,117 @@ pos posns -- | A critical overlap of one rule with another. -data Overlap f = +data Overlap a f = Overlap { - -- | The depth (1 for CPs of axioms, 2 for CPs whose rules have depth 1, etc.) - overlap_depth :: {-# UNPACK #-} !Depth, - -- | The critical term. - overlap_top :: {-# UNPACK #-} !(Term f), - -- | The part of the critical term which the inner rule rewrites. - overlap_inner :: {-# UNPACK #-} !(Term f), + -- | The rule which applies at the root. + overlap_rule1 :: !a, + -- | The rule which applies at some subterm. + overlap_rule2 :: !a, -- | The position in the critical term which is rewritten. - overlap_pos :: {-# UNPACK #-} !Int, + overlap_how :: {-# UNPACK #-} !How, + -- | The top term of the critical pair + overlap_top :: {-# UNPACK #-} !(Term f), -- | The critical pair itself. overlap_eqn :: {-# UNPACK #-} !(Equation f) } deriving Show -type OverlapOf a = Overlap (ConstantOf a) +data Direction = Forwards | Backwards deriving (Eq, 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 + +unpackHow :: Int -> How +unpackHow n = + 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) -- | Compute all overlaps of a rule with a set of rules. {-# INLINEABLE overlaps #-} overlaps :: - forall a f. (Function f, Has a Id, Has a (Rule f), Has a (Positions f), Has a Depth) => - Depth -> Index f a -> [a] -> a -> [(a, a, Overlap f)] -overlaps max_depth idx rules r = - ChurchList.toList (overlapsChurch max_depth idx rules r) + forall a b f. (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) => + Index f a -> [b] -> b -> [Overlap b f] +overlaps idx rules r = + ChurchList.toList (overlapsChurch idx rules r) {-# INLINE overlapsChurch #-} -overlapsChurch :: forall f a. - (Function f, Has a (Rule f), Has a (Positions f), Has a Depth) => - Depth -> Index f a -> [a] -> a -> ChurchList (a, a, Overlap f) -overlapsChurch max_depth idx rules r1 = do - guard (the r1 < max_depth) +overlapsChurch :: forall f a b. + (Function f, Has a (Rule f), Has b (Rule f), Has b (Positions2 f)) => + Index f a -> [b] -> b -> ChurchList (Overlap b f) +overlapsChurch idx rules r1 = do + (d1, pos1, eq1) <- directions r1' (the r1) r2 <- ChurchList.fromList rules - guard (the r2 < max_depth) - let !depth = 1 + max (the r1) (the r2) - do { o <- asymmetricOverlaps idx depth (the r1) r1' (the r2); return (r1, r2, o) } `mplus` - do { o <- asymmetricOverlaps idx depth (the r2) (the r2) r1'; return (r2, r1, o) } + (d2, pos2, eq2) <- directions (the r2) (the r2) + asymmetricOverlaps idx r1 r2 d1 d2 pos1 eq1 eq2 `mplus` + asymmetricOverlaps idx r2 r1 d2 d1 pos2 eq2 eq1 where !r1' = renameAvoiding (map the rules :: [Rule f]) (the r1) +{-# INLINE directions #-} +directions :: Rule f -> Positions2 f -> ChurchList (Direction, Positions f, Equation f) +directions rule (ForwardsPos posf) = + return (Forwards, posf, lhs rule :=: rhs rule) +directions rule (BothPos posf posb) = + return (Forwards, posf, lhs rule :=: rhs rule) `mplus` + return (Backwards, posb, rhs rule :=: lhs rule) + {-# INLINE asymmetricOverlaps #-} asymmetricOverlaps :: - (Function f, Has a (Rule f), Has a Depth) => - Index f a -> Depth -> Positions f -> Rule f -> Rule f -> ChurchList (Overlap f) -asymmetricOverlaps idx depth posns r1 r2 = do + (Function f, Has a (Rule f)) => + Index f a -> b -> b -> Direction -> Direction -> Positions f -> Equation f -> Equation f -> ChurchList (Overlap b f) +asymmetricOverlaps idx r1 r2 d1 d2 posns eq1 eq2 = do n <- positionsChurch posns ChurchList.fromMaybe $ - overlapAt n depth r1 r2 >>= + overlapAt' (How d1 d2 n) r1 r2 eq1 eq2 >>= simplifyOverlap idx -- | Create an overlap at a particular position in a term. -- Doesn't simplify the overlap. {-# INLINE overlapAt #-} -{-# SCC overlapAt #-} -overlapAt :: Int -> Depth -> Rule f -> Rule f -> Maybe (Overlap f) -overlapAt !n !depth (Rule _ _ !outer !outer') (Rule _ _ !inner !inner') = do +overlapAt :: How -> a -> a -> Rule f -> Rule f -> Maybe (Overlap a f) +overlapAt how@(How d1 d2 _) x1 x2 r1 r2 = + overlapAt' how x1 x2 (unorient (direct r1 d1)) (unorient (direct r2 d2)) + +{-# INLINE overlapAt' #-} +overlapAt' :: How -> a -> a -> Equation f -> Equation f -> Maybe (Overlap a f) +overlapAt' how@How{how_pos = n} r1 r2 (!outer :=: (!outer')) (!inner :=: (!inner')) = do let t = at n (singleton outer) sub <- unifyTri inner t let - top = termSubst sub outer - innerTerm = termSubst sub inner -- Make sure to keep in sync with overlapProof + top = termSubst sub outer lhs = termSubst sub outer' rhs = buildReplacePositionSub sub n (singleton inner') (singleton outer) guard (lhs /= rhs) return Overlap { - overlap_depth = depth, + overlap_rule1 = r1, + overlap_rule2 = r2, + overlap_how = how, overlap_top = top, - overlap_inner = innerTerm, - overlap_pos = n, overlap_eqn = lhs :=: rhs } -- | Simplify an overlap and remove it if it's trivial. {-# INLINE simplifyOverlap #-} -simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap f -> Maybe (Overlap f) +simplifyOverlap :: (Function f, Has a (Rule f)) => Index f a -> Overlap b f -> Maybe (Overlap b f) simplifyOverlap idx overlap@Overlap{overlap_eqn = lhs :=: rhs, ..} | lhs == rhs = Nothing | lhs' == rhs' = Nothing @@ -172,9 +213,9 @@ -- 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 -> Overlap f -> Int -score Config{..} Overlap{..} = - fromIntegral overlap_depth * cfg_depthweight + +score :: Function f => Config -> Depth -> Overlap a f -> Int +score Config{..} depth Overlap{..} = + fromIntegral depth * cfg_depthweight + (m + n) * cfg_rhsweight + intMax m n * (cfg_lhsweight - cfg_rhsweight) where @@ -208,9 +249,6 @@ CriticalPair { -- | The critical pair itself. cp_eqn :: {-# UNPACK #-} !(Equation f), - -- | The depth of the critical pair. - cp_depth :: {-# UNPACK #-} !Depth, - cp_max :: !Max, -- | The critical term, if there is one. -- (Axioms do not have a critical term.) cp_top :: !(Maybe (Term f)), @@ -224,8 +262,6 @@ subst_ sub CriticalPair{..} = CriticalPair { cp_eqn = subst_ sub cp_eqn, - cp_depth = cp_depth, - cp_max = cp_max, cp_top = subst_ sub cp_top, cp_proof = subst_ sub cp_proof } @@ -264,22 +300,16 @@ -- The main rule l -> r' or r -> l' or l' = r' [ CriticalPair { cp_eqn = l :=: r', - cp_depth = cp_depth, - cp_max = cp_max, cp_top = eraseExcept (vars l) cp_top, cp_proof = eraseExcept (vars l) cp_proof } | ord == Just GT ] ++ [ CriticalPair { cp_eqn = r :=: l', - cp_depth = cp_depth, - cp_max = cp_max, cp_top = eraseExcept (vars r) cp_top, cp_proof = Proof.symm (eraseExcept (vars r) cp_proof) } | ord == Just LT ] ++ [ CriticalPair { cp_eqn = l' :=: r', - cp_depth = cp_depth, - cp_max = cp_max, cp_top = eraseExcept (vars l) $ eraseExcept (vars r) cp_top, cp_proof = eraseExcept (vars l) $ eraseExcept (vars r) cp_proof } | ord == Nothing ] ++ @@ -287,15 +317,11 @@ -- Weak rules l -> l' or r -> r' [ CriticalPair { cp_eqn = l :=: l', - cp_depth = cp_depth + 1, - cp_max = cp_max, cp_top = Nothing, cp_proof = cp_proof `Proof.trans` Proof.symm (erase ls cp_proof) } | not (null ls), ord /= Just GT ] ++ [ CriticalPair { cp_eqn = r :=: r', - cp_depth = cp_depth + 1, - cp_max = cp_max, cp_top = Nothing, cp_proof = Proof.symm cp_proof `Proof.trans` erase rs cp_proof } | not (null rs), ord /= Just LT ] @@ -311,28 +337,22 @@ -- | Make a critical pair from two rules and an overlap. {-# INLINEABLE makeCriticalPair #-} -makeCriticalPair :: - forall f a. (Has a (Rule f), Has a Id, Has a Max, Function f) => - a -> a -> Overlap f -> CriticalPair f -makeCriticalPair r1 r2 overlap@Overlap{..} = +makeCriticalPair :: (Function f, Has a (Rule f)) => Overlap a f -> CriticalPair f +makeCriticalPair Overlap{..} = CriticalPair overlap_eqn - overlap_depth - (Max (unMax (the r1) `IntSet.union` unMax (the r2))) (Just overlap_top) - (overlapProof r1 r2 overlap) - --- | Return a proof for a critical pair. -{-# INLINEABLE overlapProof #-} -overlapProof :: - forall a f. - (Has a (Rule f), Has a Id) => - a -> a -> Overlap f -> Derivation f -overlapProof left right Overlap{..} = - Proof.symm (ruleDerivation (subst leftSub (the left))) - `Proof.trans` - congPath path overlap_top (ruleDerivation (subst rightSub (the right))) + proof where - Just leftSub = match (lhs (the left)) overlap_top - Just rightSub = match (lhs (the right)) overlap_inner + left = direct (the overlap_rule1) (how_dir1 overlap_how) + right = direct (the overlap_rule2) (how_dir2 overlap_how) - path = positionToPath (lhs (the left) :: Term f) overlap_pos + Just leftSub = match (lhs left) overlap_top + Just rightSub = match (lhs right) inner + + path = positionToPath (lhs left) (how_pos overlap_how) + inner = at (pathToPosition overlap_top path) (singleton overlap_top) + + proof = + Proof.symm (ruleDerivation (subst leftSub left)) + `Proof.trans` + congPath path overlap_top (ruleDerivation (subst rightSub right)) diff --git a/Twee/Constraints.hs b/Twee/Constraints.hs --- a/Twee/Constraints.hs +++ b/Twee/Constraints.hs @@ -8,7 +8,7 @@ import Twee.Pretty hiding (equals) import Twee.Utils import Data.Maybe -import Data.List +import Data.List hiding (singleton) import Data.Function import Data.Graph import Data.Map.Strict(Map) diff --git a/Twee/Equation.hs b/Twee/Equation.hs --- a/Twee/Equation.hs +++ b/Twee/Equation.hs @@ -4,6 +4,8 @@ import Twee.Base import Control.Monad +import Data.List +import Data.Ord -------------------------------------------------------------------------------- -- * Equations. @@ -24,14 +26,29 @@ instance (Labelled f, PrettyTerm f) => Pretty (Equation f) where pPrint (x :=: y) = pPrint x <+> text "=" <+> pPrint y --- | Order an equation roughly left-to-right. --- However, there is no guarantee that the result is oriented. +-- | Order an equation roughly left-to-right, and +-- canonicalise its variables. +-- There is no guarantee that the result is oriented. order :: Function f => Equation f -> Equation f order (l :=: r) - | l == r = l :=: r - | lessEqSkolem l r = r :=: l + -- If the two terms have the same skeleton, + -- then take whichever orientation gives a simpler equation + | gl == gr = + let eq1 = canonicalise (l :=: r) + eq2 = canonicalise (r :=: l) in + if eq1 == eq2 || orderedSimplerThan eq1 eq2 then eq1 else eq2 + -- Otherwise, the LHS should be the term with the greater skeleton + | gl `lessEq` gr = r :=: l | otherwise = l :=: r + where + gl = ground l + gr = ground r +-- Helper for 'order' and 'simplerThan' +orderedSimplerThan :: Function f => Equation f -> Equation f -> Bool +orderedSimplerThan (t1 :=: u1) (t2 :=: u2) = + t1 `lessEqSkolem` t2 && (t1 /= t2 || ((u1 `lessEqSkolem` u2 && u1 /= u2))) + -- | Apply a function to both sides of an equation. bothSides :: (Term f -> Term f') -> Equation f -> Equation f' bothSides f (t :=: u) = f t :=: f u @@ -43,11 +60,7 @@ -- | A total order on equations. Equations with lesser terms are smaller. simplerThan :: Function f => Equation f -> Equation f -> Bool eq1 `simplerThan` eq2 = - --traceShow (hang (pPrint eq1) 2 (text "`simplerThan`" <+> pPrint eq2 <+> text "=" <+> pPrint res)) res - t1 `lessEqSkolem` t2 && (t1 /= t2 || ((u1 `lessEqSkolem` u2 && u1 /= u2))) - where - t1 :=: u1 = canonicalise (order eq1) - t2 :=: u2 = canonicalise (order eq2) + order eq1 `orderedSimplerThan` order eq2 -- | Match one equation against another. matchEquation :: Equation f -> Equation f -> Maybe (Subst f) diff --git a/Twee/Index.hs b/Twee/Index.hs --- a/Twee/Index.hs +++ b/Twee/Index.hs @@ -5,10 +5,11 @@ -- the search term is an instance of the key, and return the corresponding -- values. -{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP #-} +{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP, TupleSections, TypeFamilies #-} -- We get some bogus warnings because of pattern synonyms. {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-} +{-# OPTIONS_GHC -funfolding-use-threshold=1000 #-} #ifdef USE_LLVM {-# OPTIONS_GHC -fllvm #-} #endif @@ -21,153 +22,122 @@ delete, lookup, matches, - approxMatches, elems, - fromListWith) where + fromList, + fromListWith, + invariant) where import Prelude hiding (null, lookup) -import Data.Maybe -import Twee.Base hiding (var, fun, empty, singleton, prefix, funs, lookupList, lookup) +import Twee.Base hiding (var, fun, empty, singleton, prefix, funs, lookupList, lookup, at) import qualified Twee.Term as Term -import Data.DynamicArray +import Data.DynamicArray hiding (singleton) +import qualified Data.DynamicArray as Array import qualified Data.List as List +import Data.Numbered(Numbered) +import qualified Data.Numbered as Numbered +import qualified Data.IntMap.Strict as IntMap +import qualified Twee.Term.Core as Core +import Twee.Profile --- The term index in this module is an _imperfect discrimination tree_. --- This is a trie whose keys are terms, represented as flat lists of symbols, --- but where all variables have been replaced by a single don't-care variable '_'. --- That is, the edges of the trie can be either function symbols or '_'. --- To insert a key-value pair into the discrimination tree, we first replace all --- variables in the key with '_', and then do ordinary trie insertion. +-- 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 +-- (either functions or variables). -- --- Lookup maintains a term list, which is initially the search term. --- It proceeds down the trie, consuming bits of the term list as it goes. +-- To insert a key-value pair into the discrimination tree, we do +-- ordinary trie insertion, but first canonicalising the key-value +-- pair so that variables are introduced in ascending order. +-- This canonicalisation reduces the size of the trie, but is also +-- needed for our particular implementation of lookup to work correctly +-- (specifically the extendBindings function below). -- +-- Lookup maintains a term list, which is initially the search term, +-- and a substitution. It proceeds down the trie, consuming bits of +-- the term list as it goes. +-- -- If the current trie node has an edge for a function symbol f, and the term at -- the head of the term list is f(t1..tn), we can follow the f edge. We then -- delete f from the term list, but keep t1..tn at the front of the term list. -- (In other words we delete only the symbol f and not its arguments.) -- --- If the current trie node has an edge for '_', we can always follow that edge. --- We then remove the head term from the term list, as the '_' represents a --- variable that should match that whole term. +-- If the current trie node has a variable edge x, we can follow that edge. +-- We remove the head term from the term list, as 'x' matches that +-- whole term. We then add the binding x->t to the substitution. +-- If the substitution already has a binding x->u with u/=t, we can't +-- follow the edge. -- --- If the term list ever becomes empty, we have a possible match. We then --- do matching on the values stored at the current node to see if they are --- genuine matches. +-- If the term list ever becomes empty, we have a match, and return +-- the substitution. -- --- Often there are two edges we can follow (function symbol and '_'), and in --- that case the algorithm uses backtracking. +-- Often there are several edges we can follow (function symbol and +-- any number of variable edges), and in that case the algorithm uses +-- backtracking. +---------------------------------------------------------------------- +-- The term index. +---------------------------------------------------------------------- + -- | A term index: a multimap from @'Term' f@ to @a@. data Index f a = -- A non-empty index. Index { - -- Size of smallest term in index. - size :: {-# UNPACK #-} !Int, + -- The size of the smallest term in the index. + minSize_ :: {-# UNPACK #-} !Int, -- When all keys in the index start with the same sequence of symbols, we -- compress them into this prefix; the "fun" and "var" fields below refer to -- the first symbol _after_ the prefix, and the "here" field contains values -- whose remaining key is exactly this prefix. - prefix :: {-# UNPACK #-} !(TermList f), + prefix :: {-# UNPACK #-} !(TermList f), -- The values that are found at this node. - here :: [a], + here :: [a], -- Function symbol edges. -- The array is indexed by function number. - fun :: {-# UNPACK #-} !(Array (Index f a)), - -- Variable edge. - var :: !(Index f a) } | + fun :: {-# UNPACK #-} !(Array (Index f a)), + -- List of variable edges indexed by variable number. + -- Invariant: all edges present in the list are non-Nil. + -- + -- Invariant: variables in terms are introduced in ascending + -- order, with no gaps (i.e. if the term so far has the variables + -- x1..xn, then the edges here must be drawn from x1...x{n+1}). + var :: {-# UNPACK #-} !(Numbered (Index f a)) } | -- An empty index. Nil deriving Show -instance Default (Index f a) where def = Nil - --- To get predictable performance, the lookup function uses an explicit stack --- instead of a lazy list to control backtracking. -data Stack f a = - -- A normal stack frame: records the current index node and term. - Frame { - frame_term :: {-# UNPACK #-} !(TermList f), - frame_index :: !(Index f a), - frame_rest :: !(Stack f a) } - -- A stack frame which is used when we have found a match. - | Yield { - yield_found :: [a], - yield_rest :: !(Stack f a) } - -- End of stack. - | Stop - --- Turn a stack into a list of results. -{-# SCC run #-} -run :: Stack f a -> [a] -run Stop = [] -run Frame{..} = run (step frame_term frame_index frame_rest) -run Yield{..} = yield_found ++ run yield_rest +minSize :: Index f a -> Int +minSize Nil = maxBound +minSize idx = minSize_ idx --- Execute a single stack frame. -{-# INLINE step #-} -{-# SCC step #-} -step :: TermList f -> Index f a -> Stack f a -> Stack f a -step !_ _ _ | False = undefined -step t idx rest = - case idx of - Nil -> rest - Index{..} - | lenList t < size -> - rest -- the search term is smaller than any in this index - | otherwise -> - pref t prefix here fun var rest +-- | Check the invariant of an index. For debugging purposes. +invariant :: Index f a -> Bool +invariant Nil = True +invariant Index{..} = + nonEmpty && + noNilVars && + maxPrefix && + sizeCorrect && + all invariant (map snd (toList fun)) && + all invariant (map snd (Numbered.toList var)) + where + nonEmpty = -- Index should not be empty + not (List.null here) || + not (List.null (filter (not . null . snd) (toList fun))) || + not (List.null (Numbered.toList var)) + noNilVars = -- the var field should not contain any Nils + all (not . null . snd) (Numbered.toList var) + maxPrefix -- prefix should be used if possible + | List.null here = + length (filter (not . null . snd) (toList fun)) + + length (Numbered.toList var) > 1 + | otherwise = True + sizeCorrect -- size field must be correct + | List.null here = + (minSize_ - lenList prefix - 1) `elem` + map (minSize . snd) (toList fun) ++ + map (minSize . snd) (Numbered.toList var) + | otherwise = + minSize_ == lenList prefix --- The main work of 'step' goes on here. --- It is carefully tweaked to generate nice code, --- in particular casing on each term list exactly once. -pref :: TermList f -> TermList f -> [a] -> Array (Index f a) -> Index f a -> Stack f a -> Stack f a -pref !_ !_ _ !_ !_ _ | False = undefined -pref search prefix here fun var rest = - case search of - ConsSym{hd = t, tl = ts, rest = ts1} -> - case prefix of - ConsSym{hd = u, tl = us, rest = us1} -> - -- Check the search term against the prefix. - case (t, u) of - (_, Var _) -> - -- Prefix contains a variable - if there is a match, the - -- variable will be bound to t. - pref ts us here fun var rest - (App f _, App g _) | f == g -> - -- Term and prefix start with same symbol, chop them off. - pref ts1 us1 here fun var rest - _ -> - -- Term and prefix don't match. - rest - _ -> - -- We've exhausted the prefix, so let's descend into the tree. - -- Seems to work better to explore the function node first. - case t of - App f _ -> - case (fun ! fun_id f, var) of - (Nil, Nil) -> - rest - (Nil, Index{}) -> - step ts var rest - (idx, Nil) -> - step ts1 idx rest - (idx, Index{}) -> - step ts1 idx (Frame ts var rest) - _ -> - case var of - Nil -> rest - _ -> step ts var rest - Empty -> - case prefix of - Empty -> - -- The search term matches this node. - case here of - [] -> rest - _ -> Yield here rest - _ -> - -- We've run out of search term - it doesn't match this node. - rest +instance Default (Index f a) where def = Nil -- | An empty index. empty :: Index f a @@ -180,101 +150,123 @@ -- | An index with one entry. singleton :: Term f -> a -> Index f a -singleton !t x = singletonList (Term.singleton t) x +singleton !t x = leaf (Term.singleton t) [x] --- An index with one entry, giving a termlist instead of a term. -{-# INLINE singletonList #-} -singletonList :: TermList f -> a -> Index f a -singletonList t x = Index 0 t [x] newArray Nil +-- A leaf node, perhaps with a prefix. +leaf :: TermList f -> [a] -> Index f a +leaf !_ [] = Nil +leaf t xs = Index (lenList t) t xs newArray Numbered.empty --- | Insert an entry into the index. -{-# SCC insert #-} -insert :: Term f -> a -> Index f a -> Index f a -insert !t x !idx = aux (Term.singleton t) idx +-- Add a prefix (given as a list of symbols) to all terms in an index. +addPrefix :: [Term f] -> Index f a -> Index f a +addPrefix _ Nil = Nil +addPrefix [] idx = idx +addPrefix ts idx = + idx { + minSize_ = minSize_ idx + length ts, + prefix = buildList (mconcat (map atom ts) `mappend` builder (prefix idx)) } where - aux t Nil = singletonList t x - aux (Cons t ts) idx@Index{prefix = Cons u us} - | skeleton t == skeleton u = - withPrefix t (aux ts idx{prefix = us}) - aux (ConsSym{hd = t, rest = ts}) idx@Index{prefix = ConsSym{hd = u, rest = us}} - | t `sameSymbolAs` u = - withPrefix (build (atom t)) (aux ts idx{prefix = us}) - aux t idx@Index{prefix = Cons{}} = aux t (expand idx) + atom (Var x) = Term.var x + atom (App f _) = con f - aux Empty idx = - idx { size = 0, here = x:here idx } - aux t@ConsSym{hd = App f _, rest = u} idx = - idx { - size = lenList t `min` size idx, - fun = update (fun_id f) idx' (fun idx) } - where - idx' = aux u (fun idx ! fun_id f) - aux t@ConsSym{hd = Var _, rest = u} idx = - idx { - size = lenList t `min` size idx, - var = aux u (var idx) } +-- Smart constructor for Index. +index :: [a] -> Array (Index f a) -> Numbered (Index f a) -> Index f a +index here fun var = + case (here, fun', Numbered.toList var') of + ([], [], []) -> + Nil + ([], [(f, idx)], []) -> + idx{minSize_ = succ (minSize_ idx), + prefix = buildList (con (Core.F f) `mappend` builder (prefix idx))} + ([], [], [(x, idx)]) -> + idx{minSize_ = succ (minSize_ idx), + prefix = buildList (Term.var (V x) `mappend` builder (prefix idx))} + _ -> + Index { + minSize_ = size, + prefix = Term.empty, + here = here, + fun = fun, + var = var' } + where + var' = Numbered.filter (not . null) var + fun' = filter (not . null . snd) (toList fun) + size = + minimum $ + [0 | not (List.null here)] ++ + map (succ . minSize . snd) fun' ++ + map (succ . minSize . snd) (Numbered.toList var') - Var _ `sameSymbolAs` Var _ = True - App f _ `sameSymbolAs` App g _ = f == g - _ `sameSymbolAs` _ = False +-- | Insert an entry into the index. +insert :: (Symbolic a, ConstantOf a ~ f) => Term f -> a -> Index f a -> Index f a +insert = modify (:) - skeleton t = build (subst (const (Term.var (V 0))) t) +-- | Delete an entry from the index. +delete :: (Eq a, Symbolic a, ConstantOf a ~ f) => Term f -> a -> Index f a -> Index f a +delete = + modify $ \x xs -> + if x `List.elem` xs then List.delete x xs + else error "deleted term not found in index" - atom (Var x) = Term.var x - atom (App f _) = con f +-- General-purpose function for modifying the index. +modify :: (Symbolic a, ConstantOf a ~ f) => + (a -> [a] -> [a]) -> + Term f -> a -> Index f a -> Index f a +modify f !t0 !v0 !idx = aux [] (Term.singleton t) idx + where + (!t, !v) = canonicalise (t0, v0) --- Add a prefix to an index. --- Does not update the size field. -withPrefix :: Term f -> Index f a -> Index f a -withPrefix _ Nil = Nil -withPrefix t idx@Index{..} = - idx{prefix = buildList (builder t `mappend` builder prefix)} + aux [] t Nil = + leaf t (f v []) + -- Non-empty prefix + aux syms (ConsSym{hd = t@(Var x), rest = ts}) + idx@Index{prefix = ConsSym{hd = Var y, rest = us}} + | x == y = + aux (t:syms) ts idx{prefix = us, minSize_ = minSize_ idx-1} + aux syms (ConsSym{hd = t@(App f _), rest = ts}) + idx@Index{prefix = ConsSym{hd = App g _, rest = us}} + | f == g = + aux (t:syms) ts idx{prefix = us, minSize_ = minSize_ idx-1} + aux [] t idx@Index{prefix = Cons{}} = + aux [] t (expand idx) + aux syms@(_:_) t idx = + addPrefix (reverse syms) $ aux [] t idx + + -- Empty prefix + aux [] Empty idx = + index (f v (here idx)) (fun idx) (var idx) + aux [] ConsSym{hd = App f _, rest = u} idx = + index (here idx) + (update (fun_id f) idx' (fun idx)) + (var idx) + where + idx' = aux [] u (fun idx ! fun_id f) + aux [] ConsSym{hd = Var x, rest = u} idx = + index (here idx) (fun idx) + (Numbered.modify (var_id x) Nil (aux [] u) (var idx)) + +-- Helper for modify: -- Take an index with a prefix and pull out the first symbol of the prefix, -- giving an index which doesn't start with a prefix. {-# INLINE expand #-} expand :: Index f a -> Index f a -expand idx@Index{size = size, prefix = ConsSym{hd = t, rest = ts}} = +expand idx@Index{minSize_ = size, prefix = ConsSym{hd = t, rest = ts}} = case t of - Var _ -> + Var x -> Index { - size = size, + minSize_ = size, prefix = Term.empty, here = [], fun = newArray, - var = idx { prefix = ts, size = size - 1 } } + var = Numbered.singleton (var_id x) idx { prefix = ts, minSize_ = size - 1 }} App f _ -> Index { - size = size, + minSize_ = size, prefix = Term.empty, here = [], - fun = update (fun_id f) idx { prefix = ts, size = size - 1 } newArray, - var = Nil } - --- | Delete an entry from the index. -{-# INLINEABLE delete #-} -{-# SCC delete #-} -delete :: Eq a => Term f -> a -> Index f a -> Index f a -delete !t x !idx = aux (Term.singleton t) idx - where - aux _ Nil = Nil - aux (ConsSym{rest = ts}) idx@Index{prefix = u@ConsSym{rest = us}} = - -- The prefix must match, since the term ought to be in the index - -- (which is checked in the Empty case below). - case aux ts idx{prefix = us} of - Nil -> Nil - idx -> idx{prefix = u} - aux _ idx@Index{prefix = Cons{}} = idx - - aux Empty idx - | x `List.elem` here idx = - idx { here = List.delete x (here idx) } - | otherwise = - error "deleted term not found in index" - aux ConsSym{hd = App f _, rest = t} idx = - idx { fun = update (fun_id f) (aux t (fun idx ! fun_id f)) (fun idx) } - aux ConsSym{hd = Var _, rest = t} idx = - idx { var = aux t (var idx) } + fun = Array.singleton (fun_id f) idx { prefix = ts, minSize_ = size - 1 }, + var = Numbered.empty } -- | Look up a term in the index. Finds all key-value such that the search term -- is an instance of the key, and returns an instance of the the value which @@ -286,33 +278,19 @@ {-# INLINEABLE lookupList #-} lookupList :: (Has a b, Symbolic b, Has b (TermOf b)) => TermListOf b -> Index (ConstantOf b) a -> [b] lookupList t idx = - [ subst sub x - | x <- List.map the (approxMatchesList t idx), - sub <- maybeToList (matchList (Term.singleton (the x)) t)] + [ subst sub (the x) + | (sub, x) <- matchesList t idx ] -- | Look up a term in the index. Like 'lookup', but returns the exact value -- that was inserted into the index, not an instance. Also returns a substitution -- which when applied to the value gives you the matching instance. {-# INLINE matches #-} -matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)] +matches :: Term f -> Index f a -> [(Subst f, a)] matches t idx = matchesList (Term.singleton t) idx -{-# INLINEABLE matchesList #-} -matchesList :: Has a (Term f) => TermList f -> Index f a -> [(Subst f, a)] +matchesList :: TermList f -> Index f a -> [(Subst f, a)] matchesList t idx = - [ (sub, x) - | x <- approxMatchesList t idx, - sub <- maybeToList (matchList (Term.singleton (the x)) t)] - --- | Look up a term in the index, possibly returning spurious extra results. -{-# INLINE approxMatches #-} -approxMatches :: Term f -> Index f a -> [a] -approxMatches t idx = approxMatchesList (Term.singleton t) idx - -{-# SCC approxMatchesList #-} -approxMatchesList :: TermList f -> Index f a -> [a] -approxMatchesList t idx = - run (Frame t idx Stop) + run (search t emptyBindings idx Stop) -- | Return all elements of the index. elems :: Index f a -> [a] @@ -320,8 +298,188 @@ elems idx = here idx ++ concatMap elems (map snd (toList (fun idx))) ++ - elems (var idx) + concatMap elems (map snd (Numbered.toList (var idx))) -- | Create an index from a list of items -fromListWith :: (a -> Term f) -> [a] -> Index f a +fromList :: (Symbolic a, ConstantOf a ~ f) => [(Term f, a)] -> Index f a +fromList xs = foldr (uncurry insert) empty xs + +-- | Create an index from a list of items +fromListWith :: (Symbolic a, ConstantOf a ~ f) => (a -> Term f) -> [a] -> Index f a fromListWith f xs = foldr (\x -> insert (f x) x) empty xs + +---------------------------------------------------------------------- +-- Substitutions used internally during lookup. +---------------------------------------------------------------------- + +-- We represent a substitution as a list of terms, in +-- reverse order. That is, the substitution +-- {x1->t1, ..., xn->tn} is represented as +-- [xn, x{n-1}, ..., x1]. +data Bindings f = + Bindings + {-# UNPACK #-} !Int -- the highest-numbered variable (n) + !(BindList f) -- the list of terms ([xn, ..., x1]) + +data BindList f = NilB | ConsB {-# UNPACK #-} !(TermList f) !(BindList f) + +{-# INLINE emptyBindings #-} +-- An empty substitution +emptyBindings :: Bindings f +emptyBindings = Bindings (-1) NilB + +{-# INLINE extendBindings #-} +-- Extend a substitution. +-- The variable bound must either be present in the substitution, +-- or the current highest-numbered variable plus one. +extendBindings :: Var -> Term f -> Bindings f -> Maybe (Bindings f) +extendBindings (V x) t (Bindings n bs) + | x > n = Just (Bindings (n+1) (ConsB (Term.singleton t) bs)) + | bs `at` (n - x) == Term.singleton t = Just (Bindings n bs) + | otherwise = Nothing + +at :: BindList f -> Int -> TermList f +at (ConsB t _) 0 = t +at (ConsB _ b) n = at b (n-1) + +-- Convert a substitution into an ordinary Subst. +toSubst :: Bindings f -> Subst f +toSubst (Bindings n bs) = + Subst (IntMap.fromDistinctAscList (loop n bs [])) + where + loop !_ !_ !_ | False = undefined + loop _ NilB sub = sub + loop n (ConsB t bs) sub = + loop (n-1) bs ((n, t):sub) + +---------------------------------------------------------------------- +-- Lookup. +---------------------------------------------------------------------- + +-- To get predictable performance, lookup uses an explicit stack +-- instead of a lazy list to control backtracking. +data Stack f a = + -- We only ever backtrack into variable edges, not function edges. + -- This stack frame represents a search of the variable edges of a + -- node, starting at a particular variable. + Frame { + -- The term which should match the variable + frame_term :: {-# UNPACK #-} !(Term f), + -- The remainder of the search term + frame_terms :: {-# UNPACK #-} !(TermList f), + -- The current substitution + frame_bind :: {-# UNPACK #-} !(Bindings f), + -- The list of variable edges + frame_indexes :: {-# UNPACK #-} !(Numbered (Index f a)), + -- The starting variable number + frame_var :: {-# UNPACK #-} !Int, + -- The rest of the stack + frame_rest :: !(Stack f a) } | + -- A stack frame which is used when we have found a matching node. + Yield { + -- The list of values found at this node + yield_found :: [a], + -- The current substitution + yield_binds :: {-# UNPACK #-} !(Bindings f), + -- The rest of the stack + yield_rest :: !(Stack f a) } + -- End of stack. + | Stop + +-- Turn a stack into a list of results. +run :: Stack f a -> [(Subst f, a)] +run stack = stamp "index lookup" (run1 stack) + where + run1 Stop = [] + run1 Frame{..} = + run1 (searchVars frame_term frame_terms frame_bind frame_indexes frame_var frame_rest) + run1 Yield{..} = + map (toSubst yield_binds,) yield_found ++ run yield_rest + +-- Search starting with a given substitution. +{-# INLINE search #-} +search :: TermList f -> Bindings f -> Index f a -> Stack f a -> Stack f a +search !_ !_ !_ _ | False = undefined +search t binds idx rest = + case idx of + Nil -> rest + Index{..} + | lenList t < minSize idx -> + rest -- the search term is smaller than any in this index + | otherwise -> + searchLoop binds t prefix here fun var rest + +-- The main work of 'search' goes on here. +-- It is carefully tweaked to generate nice code, +-- in particular casing on each term list exactly once. +searchLoop :: + -- Search term and substitution + Bindings f -> TermList f -> + -- Contents of the relevant node of the index + TermList f -> [a] -> Array (Index f a) -> Numbered (Index f a) -> + Stack f a -> Stack f a +searchLoop !_ !_ !_ _ !_ !_ _ | False = undefined +searchLoop binds t prefix here fun var rest = + case t of + ConsSym{hd = thd, tl = ttl, rest = trest} -> + case prefix of + ConsSym{hd = phd, tl = ptl, rest = prest} -> + -- Check the search term against the prefix. + case (thd, phd) of + (_, Var x) -> + case extendBindings x thd binds of + Just binds' -> + searchLoop binds' ttl ptl here fun var rest + Nothing -> + rest + (App f _, App g _) | f == g -> + -- Term and prefix start with same symbol, chop them off. + searchLoop binds trest prest here fun var rest + _ -> + -- Term and prefix don't match. + rest + _ -> + -- We've exhausted the prefix, so let's descend into the tree. + -- Seems to work better to explore the function node first. + case thd of + App f _ | idx@Index{} <- fun ! fun_id f -> + -- Avoid creating a frame unnecessarily. + case Numbered.size var of + 0 -> search trest binds idx rest + _ -> search trest binds idx $! Frame thd ttl binds var 0 rest + _ -> -- no function match + case Numbered.size var of + 0 -> rest + _ -> searchVars thd ttl binds var 0 rest + _ -> + case prefix of + Empty -> + -- The search term matches this node. + case here of + [] -> rest + _ -> Yield here binds rest + _ -> + -- We've run out of search term - it doesn't match this node. + rest + +-- Search the variable-labelled edges of a node, +-- starting with a particular variable. +searchVars :: + -- Term (with head separate) and substitution + Term f -> TermList f -> Bindings f -> + -- Variable edges and starting variable + Numbered (Index f a) -> Int -> + Stack f a -> Stack f a +searchVars !_ !_ !_ !_ !_ _ | False = undefined +searchVars t ts binds var start rest + | start >= Numbered.size var = rest + | otherwise = + let (x, idx) = var Numbered.! start in + case extendBindings (V x) t binds of + Just binds' -> + search ts binds' idx $! + if start + 1 == Numbered.size var then rest + else Frame t ts binds var (start+1) rest + Nothing -> + searchVars t ts binds var (start+1) rest + diff --git a/Twee/Join.hs b/Twee/Join.hs --- a/Twee/Join.hs +++ b/Twee/Join.hs @@ -33,7 +33,6 @@ cfg_set_join = False } {-# INLINEABLE joinCriticalPair #-} -{-# SCC joinCriticalPair #-} joinCriticalPair :: (Function f, Has a (Rule f)) => Config -> @@ -154,8 +153,7 @@ -- No need to do this symmetrically because addJoinable adds -- both orientations of each equation | or [ u == subst sub u' - | t' :=: u' <- Index.approxMatches t eqns, - sub <- maybeToList (match t' t) ] = True + | (sub, t' :=: u') <- Index.matches t eqns ] = True subsumed1 eqns idx (App f ts :=: App g us) | f == g = let @@ -175,7 +173,7 @@ case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of ([], instances) -> let cps = [ subst sub cp | sub <- instances ] in - Right (Just cp, usortBy (comparing (canonicalise . order . cp_eqn)) cps) + Right (Just cp, usortBy (comparing (order . cp_eqn)) cps) (model:_, _) -> groundJoinFrom config eqns idx model ctx cp diff --git a/Twee/KBO.hs b/Twee/KBO.hs --- a/Twee/KBO.hs +++ b/Twee/KBO.hs @@ -38,7 +38,6 @@ in loop ts us -- | Check if one term is less than another in KBO. -{-# SCC lessEq #-} lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool lessEq (App f Empty) _ | f == minimal = True lessEq (Var x) (Var y) | x == y = True @@ -76,7 +75,6 @@ -- See "notes/kbo under assumptions" for how this works. -{-# SCC lessIn #-} lessIn :: (Function f, Sized f, Weighted f) => Model f -> Term f -> Term f -> Maybe Strictness lessIn model t u = case sizeLessIn model t u of diff --git a/Twee/Label.hs b/Twee/Label.hs deleted file mode 100644 --- a/Twee/Label.hs +++ /dev/null @@ -1,125 +0,0 @@ --- | Assignment of unique IDs to values. --- Inspired by the 'intern' package. - -{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns #-} -module Twee.Label(Label, unsafeMkLabel, labelNum, label, find) where - -import Data.IORef -import System.IO.Unsafe -import qualified Data.Map.Strict as Map -import Data.Map.Strict(Map) -import qualified Data.DynamicArray as DynamicArray -import Data.DynamicArray(Array) -import Data.Typeable -import GHC.Exts -import Unsafe.Coerce -import Data.Int - --- | A value of type @a@ which has been given a unique ID. -newtype Label a = - Label { - -- | The unique ID of a label. - labelNum :: Int32 } - deriving (Eq, Ord, Show) - --- | Construct a @'Label' a@ from its unique ID, which must be the 'labelNum' of --- an already existing 'Label'. Extremely unsafe! -unsafeMkLabel :: Int32 -> Label a -unsafeMkLabel = Label - --- The global cache of labels. -{-# NOINLINE cachesRef #-} -cachesRef :: IORef Caches -cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray)) - -data Caches = - Caches { - -- The next id number to assign. - caches_nextId :: {-# UNPACK #-} !Int32, - -- A map from values to labels. - caches_from :: !(Map TypeRep (Cache Any)), - -- The reverse map from labels 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 - -- compare-and-swap. This causes bad things to happen when 'label' - -- is used reentrantly (i.e. the Ord instance itself calls label). - -- This function only lets the swap happen if caches_nextId didn't - -- change (i.e., no new values were inserted). - !caches <- readIORef cachesRef - -- First compute the update. - let !(!caches', !x) = f caches - -- Now see if anyone else updated the cache in between - -- (can happen if f called 'label', or in a concurrent setting). - ok <- atomicModifyIORef' cachesRef $ \cachesNow -> - if caches_nextId caches == caches_nextId cachesNow - then (caches', True) - else (cachesNow, False) - if ok then return x else atomicModifyCaches f - --- Versions of unsafeCoerce with slightly more type checking -toAnyCache :: Cache a -> Cache Any -toAnyCache = unsafeCoerce - -fromAnyCache :: Cache Any -> Cache a -fromAnyCache = unsafeCoerce - -toAny :: a -> Any -toAny = unsafeCoerce - -fromAny :: Any -> a -fromAny = unsafeCoerce - --- | Assign a label to a value. -{-# NOINLINE label #-} -label :: forall a. (Typeable a, Ord a) => a -> Label a -label x = - unsafeDupablePerformIO $ do - -- Common case: label is already there. - caches <- readIORef cachesRef - case tryFind caches of - Just l -> return l - Nothing -> do - -- Rare case: label was not there. - x <- atomicModifyCaches $ \caches -> - case tryFind caches of - Just l -> (caches, l) - Nothing -> - insert caches - return x - - where - ty = typeOf x - - tryFind :: Caches -> Maybe (Label a) - tryFind Caches{..} = - Label <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache) - - insert :: Caches -> (Caches, Label 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_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to }, - Label n) - where - n = caches_nextId - cache = - fromAnyCache $ - Map.findWithDefault Map.empty ty caches_from - --- | Recover the underlying value from a label. -find :: Label a -> a --- N.B. must force n before calling readIORef, otherwise a call of --- the form --- find (label x) --- doesn't work. -find (Label !n) = unsafeDupablePerformIO $ do - Caches{..} <- readIORef cachesRef - x <- return $! fromAny (DynamicArray.getWithDefault undefined (fromIntegral n) caches_to) - return x diff --git a/Twee/Profile.hs b/Twee/Profile.hs new file mode 100644 --- /dev/null +++ b/Twee/Profile.hs @@ -0,0 +1,141 @@ +-- Basic support for profiling. +{-# LANGUAGE BangPatterns, RecordWildCards, CPP, OverloadedStrings #-} +module Twee.Profile(stamp, stampWith, stampM, profile) where + +#ifdef PROFILE +import System.IO.Unsafe +import Data.IORef +import System.CPUTime.Rdtsc +import Data.List +import Data.Ord +import Text.Printf +import GHC.Conc.Sync +import Data.Word +import Control.Monad.IO.Class +import qualified Data.HashMap.Strict as HashMap +import Data.HashMap.Strict(HashMap) +import Data.Symbol +import Data.Symbol.Unsafe +import Data.Hashable + +instance Hashable Symbol where + hashWithSalt s (Symbol n _) = hashWithSalt s n + +data Record = + Record { + rec_individual :: {-# UNPACK #-} !Word64, + rec_cumulative :: {-# UNPACK #-} !Word64, + rec_count :: {-# UNPACK #-} !Word64 } + +data Running = + Running { + run_started :: {-# UNPACK #-} !Word64, + run_skipped :: {-# UNPACK #-} !Word64, + run_overhead :: {-# UNPACK #-} !Word64 } + +data State = + State { + st_map :: !(HashMap Symbol Record), + st_overhead :: {-# UNPACK #-} !Word64, + st_running :: {-# UNPACK #-} !Running, + st_stack :: [Running] } + +{-# NOINLINE eventLog #-} +eventLog :: IORef State +eventLog = unsafePerformIO (newIORef (State HashMap.empty 0 (Running 0 0 0) [])) + +{-# NOINLINE enter #-} +enter :: IO (HashMap Symbol Record) +enter = do + State{..} <- readIORef eventLog + tsc <- rdtsc + let !running = Running tsc 0 0 + writeIORef eventLog (State st_map st_overhead running (st_running:st_stack)) + return st_map + +{-# NOINLINE exit #-} +exit :: HashMap Symbol Record -> Symbol -> IO () +exit old_st str = do + tsc <- rdtsc + State st_map st_overhead Running{..} st_stack <- readIORef eventLog + str `pseq` do + let cumulative = tsc - run_started - run_overhead + individual = cumulative - run_skipped + -- To make sure recursive functions are accounted for properly, + -- we reset cumulative time to what it was on entry + Record _ c2 _ = HashMap.lookupDefault (Record 0 0 0) str old_st + plus (Record i1 c1 m) (Record i2 _ n) = + Record (i1+i2) (c1+c2) (m+n) + rec = Record individual cumulative 1 + m = HashMap.insertWith plus str rec st_map + case st_stack of + [] -> error "mismatched enter/exit" + Running{..}:st_stack -> m `pseq` do + tsc' <- rdtsc + let overhead = tsc' - tsc + run = + Running run_started + (run_skipped+cumulative) + (run_overhead+overhead) + writeIORef eventLog $! State m (st_overhead + overhead) run st_stack + +{-# NOINLINE stamp #-} +stamp :: Symbol -> a -> a +stamp str x = + unsafePerformIO $ do + m <- enter + x `pseq` exit m str + return x + +stampWith :: Symbol -> (a -> b) -> a -> a +stampWith str f x = stamp str (f x) `pseq` x + +stampM :: MonadIO m => Symbol -> m a -> m a +stampM str mx = do + m <- liftIO enter + x <- mx + liftIO (exit m str) + return x + +report :: (Record -> Word64) -> HashMap Symbol Record -> IO () +report f cs = mapM_ pr ts + where + ts = + sortBy (comparing (negate . f . snd)) $ + sortBy (comparing fst) $ + HashMap.toList $ + {-HashMap.filter ((>= tot `div` 200) . f)-} cs + tot = sum (map rec_individual (HashMap.elems cs)) + pr (str, rec) = + printf "%10.2f Mclocks (%6.2f%% of total): %s, %d calls\n" + (fromIntegral n / 10^6 :: Double) + (100 * fromIntegral n / fromIntegral tot :: Double) + (unintern str) + (rec_count rec) + where + n = f rec + +profile :: IO () +profile = do + State{..} <- readIORef eventLog + let log = HashMap.insert "OVERHEAD" (Record st_overhead st_overhead 0) st_map + putStrLn "Individual time:" + report rec_individual log + putStrLn "" + putStrLn "Cumulative time:" + report rec_cumulative log +#else +import Control.Monad.IO.Class + +stamp :: symbol -> a -> a +stamp _ = id + +stampWith :: symbol -> (a -> b) -> a -> a +stampWith _ _ = id + +stampM :: MonadIO m => symbol -> m a -> m a +stampM _ = id + +profile :: IO () +profile = return () +#endif diff --git a/Twee/Proof.hs b/Twee/Proof.hs --- a/Twee/Proof.hs +++ b/Twee/Proof.hs @@ -1,5 +1,5 @@ -- | Equational proofs which are checked for correctedness. -{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables, OverloadedStrings #-} module Twee.Proof( -- * Constructing proofs Proof, Derivation(..), Axiom(..), @@ -22,7 +22,7 @@ import qualified Twee.Index as Index import Control.Monad import Data.Maybe -import Data.List +import Data.List hiding (singleton) import Data.Ord import qualified Data.Set as Set import Data.Set(Set) @@ -31,6 +31,7 @@ import qualified Data.IntMap.Strict as IntMap import Control.Monad.Trans.State.Strict import Data.Graph +import Twee.Profile ---------------------------------------------------------------------- -- Equational proofs. Only valid proofs can be constructed. @@ -85,9 +86,9 @@ -- This is the trusted core of the module. {-# INLINEABLE certify #-} -{-# SCC certify #-} certify :: Function f => Derivation f -> Proof f certify p = + stamp "certify proof" $ case check p of Nothing -> error ("Invalid proof created!\n" ++ prettyShow p) Just eqn -> Proof eqn p @@ -401,8 +402,8 @@ find t = listToMaybe $ do - Axiom{axiom_eqn = l :=: r} <- Index.approxMatches t idx - sub <- maybeToList (match l t) + (_, UseAxiom Axiom{axiom_eqn = l :=: r} _) <- Index.matches t idx + let Just sub = match l t return (r, sub) replace sub (Var (V x)) = @@ -411,7 +412,7 @@ cong f (map (replace sub) (unpack ts)) axSet = Set.fromList axioms - idx = Index.fromListWith (eqn_lhs . axiom_eqn) axioms + idx = Index.fromList [(eqn_lhs (axiom_eqn ax), axiom ax) | ax <- axioms] -- | Applies a derivation at a particular path in a term. congPath :: [Int] -> Term f -> Derivation f -> Derivation f diff --git a/Twee/Rule.hs b/Twee/Rule.hs --- a/Twee/Rule.hs +++ b/Twee/Rule.hs @@ -10,7 +10,7 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Data.Maybe -import Data.List +import Data.List hiding (singleton) import Twee.Utils import qualified Data.Map.Strict as Map import Data.Map(Map) @@ -46,6 +46,8 @@ x == y = compare x y == EQ instance Ord (Rule f) where compare = comparing (\rule -> (lhs rule, rhs rule)) +instance f ~ g => Has (Rule f) (Rule g) where + the = id type RuleOf a = Rule (ConstantOf a) ruleDerivation :: Rule f -> Derivation f @@ -186,7 +188,6 @@ -- | Compute the normal form of a term wrt only oriented rules. {-# INLINEABLE simplify #-} -{-# SCC simplify #-} simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f simplify = simplifyOutermost @@ -220,14 +221,13 @@ -- | Find a simplification step that applies to a term. {-# INLINEABLE simpleRewrite #-} -{-# SCC simpleRewrite #-} simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f) simpleRewrite idx t = -- Use instead of maybeToList to make fusion work foldr (\x _ -> Just x) Nothing $ do - rule <- the <$> Index.approxMatches t idx + (sub, rule0) <- Index.matches t idx + let rule = the rule0 guard (oriented (orientation rule)) - sub <- maybeToList (match (lhs rule) t) guard (reducesOriented rule sub) return (rule, sub) @@ -283,7 +283,6 @@ -- | Normalise a term wrt a particular strategy. {-# INLINE normaliseWith #-} -{-# SCC normaliseWith #-} normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f normaliseWith ok strat t = res where @@ -310,7 +309,6 @@ (qs, rs) = successorsAndNormalForms strat ps {-# INLINEABLE successorsAndNormalForms #-} -{-# SCC successorsAndNormalForms #-} successorsAndNormalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> (Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f)) successorsAndNormalForms strat ps = @@ -350,8 +348,9 @@ {-# INLINE rewrite #-} rewrite :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f rewrite p rules t = do - rule <- Index.approxMatches t rules - tryRule p rule t + (sub, rule) <- Index.matches t rules + guard (p (the rule) sub) + return [subst sub (the rule)] -- | A strategy which applies one rule only. {-# INLINEABLE tryRule #-} diff --git a/Twee/Rule/Index.hs b/Twee/Rule/Index.hs --- a/Twee/Rule/Index.hs +++ b/Twee/Rule/Index.hs @@ -1,8 +1,8 @@ -{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts #-} +{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts, TypeFamilies #-} module Twee.Rule.Index( RuleIndex(..), empty, insert, delete, - approxMatches, matches, lookup) where + matches, lookup) where import Prelude hiding (lookup) import Twee.Base hiding (lookup, empty) @@ -19,7 +19,7 @@ empty :: RuleIndex f a empty = RuleIndex Index.empty Index.empty -insert :: forall f a. Has a (Rule f) => Term f -> a -> RuleIndex f a -> RuleIndex f a +insert :: forall f a. (Symbolic a, ConstantOf a ~ f, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a insert t x RuleIndex{..} = RuleIndex { index_oriented = insertWhen (oriented or) index_oriented, @@ -30,7 +30,7 @@ insertWhen False idx = idx insertWhen True idx = Index.insert t x idx -delete :: forall f a. (Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a +delete :: forall f a. (Symbolic a, ConstantOf a ~ f, Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a delete t x RuleIndex{..} = RuleIndex { index_oriented = deleteWhen (oriented or) index_oriented, diff --git a/Twee/Term.hs b/Twee/Term.hs --- a/Twee/Term.hs +++ b/Twee/Term.hs @@ -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 #-} +{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables, CPP, DefaultSignatures #-} {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-} #ifdef USE_LLVM {-# OPTIONS_GHC -fllvm #-} @@ -26,7 +26,7 @@ pattern UnsafeCons, pattern UnsafeConsSym, uhd, utl, urest, empty, unpack, lenList, -- * Function symbols and variables - Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..), AutoLabel(..), + Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..), -- * Building terms Build(..), Builder, @@ -53,7 +53,7 @@ matchMany, matchManyIn, matchManyList, matchManyListIn, isInstanceOf, isVariantOf, -- * Unification - unify, unifyList, unifyMany, + unify, unifyList, unifyMany, unifyManyTri, unifyTri, unifyTriFrom, unifyListTri, unifyListTriFrom, TriangleSubst(..), emptyTriangleSubst, close, @@ -68,14 +68,14 @@ import Prelude hiding (lookup) import Twee.Term.Core hiding (F) import qualified Twee.Term.Core as Core -import Data.List hiding (lookup, find) +import Data.List hiding (lookup, find, singleton) import Data.Maybe import Data.Semigroup(Semigroup(..)) import Data.IntMap.Strict(IntMap) import qualified Data.IntMap.Strict as IntMap import Control.Arrow((&&&)) import Twee.Utils -import qualified Twee.Label as Label +import qualified Data.Label as Label import Data.Typeable -------------------------------------------------------------------------------- @@ -117,7 +117,6 @@ -- | Build a termlist. {-# INLINE buildList #-} -{-# SCC buildList #-} buildList :: Build a => a -> TermList (BuildFun a) buildList x = buildTermList (builder x) @@ -348,7 +347,6 @@ -- | A variant of 'match' which works on termlists -- and extends an existing substitution. -{-# SCC matchListIn #-} matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f) matchListIn !sub !pat !t | lenList t < lenList pat = Nothing @@ -437,10 +435,16 @@ -- | Unify a collection of pairs of terms. unifyMany :: [(Term f, Term f)] -> Maybe (Subst f) -unifyMany ts = unifyList us vs +unifyMany ts = close <$> unifyManyTri ts + +-- | Unify a collection of pairs of terms, returning a triangle substitution. +unifyManyTri :: [(Term f, Term f)] -> Maybe (TriangleSubst f) +unifyManyTri ts = loop ts (Triangle emptySubst) where - us = buildList (map fst ts) - vs = buildList (map snd ts) + loop [] sub = Just sub + loop ((t, u):ts) sub = do + sub <- unifyTriFrom t u sub + loop ts sub -- | Unify two terms, returning a triangle substitution. -- This is slightly faster than 'unify'. @@ -456,7 +460,6 @@ unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f) unifyListTri t u = unifyListTriFrom t u (Triangle emptySubst) -{-# SCC unifyListTriFrom #-} unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f) unifyListTriFrom !t !u (Triangle !sub) = fmap Triangle (loop sub t u) @@ -718,18 +721,12 @@ list (k+len t) u (n-1) ns class Labelled f where - -- | Labels should be small positive integers! - label :: f -> Int - find :: Int -> f + label :: f -> Label.Label f + default label :: (Ord f, Typeable f) => f -> Label.Label f + label = Label.label instance (Labelled f, Show f) => Show (Fun f) where show = show . fun_value --- | For "deriving via": a Labelled instance which uses Twee.Label. -newtype AutoLabel a = AutoLabel { unAutoLabel :: a } -instance (Ord a, Typeable a) => Labelled (AutoLabel a) where - label = fromIntegral . Label.labelNum . Label.label . unAutoLabel - find = AutoLabel . Label.find . Label.unsafeMkLabel . fromIntegral - -- | A pattern which extracts the 'fun_value' from a 'Fun'. pattern F :: Labelled f => Int -> f -> Fun f pattern F x y <- (fun_id &&& fun_value -> (x, y)) @@ -740,11 +737,11 @@ f << g = fun_value f < fun_value g -- | Construct a 'Fun' from a function symbol. -{-# INLINEABLE fun #-} +{-# NOINLINE fun #-} fun :: Labelled f => f -> Fun f -fun f = Core.F (fromIntegral (label f)) +fun f = Core.F (fromIntegral (Label.labelNum (label f))) -- | The underlying function symbol of a 'Fun'. -{-# INLINEABLE fun_value #-} +{-# INLINE fun_value #-} fun_value :: Labelled f => Fun f -> f -fun_value x = find (fun_id x) +fun_value x = Label.find (Label.unsafeMkLabel (fromIntegral (fun_id x))) diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs --- a/Twee/Term/Core.hs +++ b/Twee/Term/Core.hs @@ -3,7 +3,8 @@ -- and provides primitives for building higher-level stuff. {-# LANGUAGE CPP, PatternSynonyms, ViewPatterns, MagicHash, UnboxedTuples, BangPatterns, - RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving, CPP #-} + RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving, + OverloadedStrings, RoleAnnotations #-} {-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-} #ifdef USE_LLVM {-# OPTIONS_GHC -fllvm #-} @@ -24,6 +25,7 @@ import GHC.ST hiding (liftST) import Data.Ord import Data.Semigroup(Semigroup(..)) +import Twee.Profile -------------------------------------------------------------------------------- -- Symbols. A symbol is a single function or variable in a flatterm. @@ -62,6 +64,10 @@ fromIntegral index `unsafeShiftL` 32 + fromIntegral (fromEnum isFun) `unsafeShiftL` 31 +{-# INLINE symbolSize #-} +symbolSize :: Int +symbolSize = sizeOf (fromSymbol undefined) + -------------------------------------------------------------------------------- -- Flatterms, or rather lists of terms. -------------------------------------------------------------------------------- @@ -77,6 +83,8 @@ high :: {-# UNPACK #-} !Int, array :: {-# UNPACK #-} !ByteArray } +type role TermList nominal + -- | Index into a termlist. at :: Int -> TermList f -> Term f at n t @@ -104,6 +112,8 @@ root :: {-# UNPACK #-} !Int64, termlist :: {-# UNPACK #-} !(TermList f) } +type role Term nominal + instance Eq (Term f) where x == y = termlist x == termlist y @@ -184,6 +194,8 @@ fun_id :: Int } deriving (Eq, Ord) +type role Fun nominal + -- | A variable. newtype Var = V { @@ -220,17 +232,24 @@ singleton Term{..} = termlist instance Eq (TermList f) where - t == u = compare t u == EQ + t == u = + lenList t == lenList u && + compareSameLength t u == EQ instance Ord (TermList f) where {-# INLINE compare #-} compare t u = compare (lenList t) (lenList u) `mappend` - compareByteArrays (array t) (low t * k) - (array u) (low u * k) ((high t - low t) * k) - where - k = sizeOf (fromSymbol undefined) + compareSameLength t u +{-# INLINE compareSameLength #-} +compareSameLength :: TermList f -> TermList f -> Ordering +compareSameLength t u = + compareByteArrays (array t) (low t * k) + (array u) (low u * k) ((high t - low t) * k) + where + k = symbolSize + -------------------------------------------------------------------------------- -- Building terms. -------------------------------------------------------------------------------- @@ -240,12 +259,14 @@ newtype Builder f = Builder { unBuilder :: - -- Takes: the term array and size, and current position in the term. - -- Returns the final position, which may be out of bounds. + -- Takes: the term array, and current position in the term. + -- Returns the final array and position. forall s. Builder1 s f } -type Builder1 s f = State# s -> MutableByteArray# s -> Int# -> Int# -> (# State# s, Int# #) +type role Builder nominal +type Builder1 s f = State# s -> MutableByteArray# s -> Int# -> (# State# s, MutableByteArray# s, Int# #) + instance Semigroup (Builder f) where {-# INLINE (<>) #-} Builder m1 <> Builder m2 = Builder (m1 `then_` m2) @@ -256,89 +277,53 @@ mappend = (<>) -- Build a termlist from a Builder. --- Works by guessing an appropriate size, and retrying if that was too small. {-# INLINE buildTermList #-} buildTermList :: Builder f -> TermList f -buildTermList builder = runST $ do - let - Builder m = builder - loop n@(I# n#) = do - MutableByteArray mbytearray# <- - newByteArray (n * sizeOf (fromSymbol undefined)) - n' <- - ST $ \s -> - case m s mbytearray# n# 0# of - (# s, n# #) -> (# s, I# n# #) - if n' <= n then do - resizeMutableByteArray (MutableByteArray mbytearray#) (n' * sizeOf (fromSymbol undefined)) - !bytearray <- unsafeFreezeByteArray (MutableByteArray mbytearray#) - return (TermList 0 n' bytearray) - else loop (n'*2) - loop 128 - --- Get at the term array. -{-# INLINE getByteArray #-} -getByteArray :: (MutableByteArray s -> Builder1 s f) -> Builder1 s f -getByteArray k = \s bytearray n i -> k (MutableByteArray bytearray) s bytearray n i - --- Get at the array size. -{-# INLINE getSize #-} -getSize :: (Int -> Builder1 s f) -> Builder1 s f -getSize k = \s bytearray n i -> k (I# n) s bytearray n i - --- Get at the current array index. -{-# INLINE getIndex #-} -getIndex :: (Int -> Builder1 s f) -> Builder1 s f -getIndex k = \s bytearray n i -> k (I# i) s bytearray n i - --- Change the current array index. -{-# INLINE putIndex #-} -putIndex :: Int -> Builder1 s f -putIndex (I# i) = \s _ _ _ -> (# s, i #) - --- Lift an ST computation into a builder. -{-# INLINE liftST #-} -liftST :: ST s () -> Builder1 s f -liftST (ST m) = - \s _ _ i -> - case m s of - (# s, () #) -> (# s, i #) +buildTermList (Builder m) = stamp "build term" $ runST $ do + MutableByteArray marr# <- + -- Start with a capacity of 16 symbols (arbitrary choice) + newByteArray (16 * symbolSize) + (marr, n) <- + ST $ \s -> + case m s marr# 0# of + (# s, marr#, n# #) -> + (# s, (MutableByteArray marr#, I# n#) #) + shrinkMutableByteArray marr (n * symbolSize) + !arr <- unsafeFreezeByteArray marr + return (TermList 0 n arr) --- Finish building. +-- A builder which does nothing. {-# INLINE built #-} built :: Builder1 s f -built = \s _ _ i -> (# s, i #) +built s arr# n# = (# s, arr#, n# #) -- Sequence two builder operations. {-# INLINE then_ #-} then_ :: Builder1 s f -> Builder1 s f -> Builder1 s f -then_ m1 m2 = - \s bytearray n i -> - case m1 s bytearray n i of - (# s, i #) -> m2 s bytearray n i - --- checked j m executes m only if the array has room for j more symbols. -{-# INLINE checked #-} -checked :: Int -> Builder1 s f -> Builder1 s f -checked j m = - getSize $ \n -> - getIndex $ \i -> - if i + j <= n then m else putIndex (i + j) +m1 `then_` m2 = \s arr# n# -> + case m1 s arr# n# of + (# s, arr#, n# #) -> + m2 s arr# n# -- Emit an arbitrary symbol, with given arguments. {-# INLINE emitSymbolBuilder #-} emitSymbolBuilder :: Symbol -> Builder f -> Builder f -emitSymbolBuilder x inner = - Builder $ checked 1 $ - getByteArray $ \bytearray -> - -- Skip the symbol itself, then fill it in at the end, when we know the size - -- of the symbol's arguments. - getIndex $ \n -> - putIndex (n+1) `then_` - unBuilder inner `then_` - -- Fill in the symbol. - getIndex (\m -> - liftST $ writeByteArray bytearray n (fromSymbol x { size = m - n })) +emitSymbolBuilder x (Builder inner) = + Builder $ \s arr# n# -> + let n = I# n# in + -- Reserve space for the symbol + case reserve s arr# (unInt (n + 1)) of + (# s, arr# #) -> + -- Fill in the argument list + case inner s arr# (unInt (n + 1)) of + (# s, arr#, m# #) -> + let arr = MutableByteArray arr# + m = I# m# in + -- Check the length of the argument list in symbols, + -- then write the symbol, with the correct size + case unST (writeByteArray arr n (fromSymbol x { size = m - n })) s of + (# s, () #) -> + (# s, arr#, m# #) -- Emit a function application. {-# INLINE emitApp #-} @@ -354,12 +339,42 @@ {-# INLINE emitTermList #-} emitTermList :: TermList f -> Builder f emitTermList (TermList lo hi array) = - Builder $ checked (hi-lo) $ - getByteArray $ \mbytearray -> - getIndex $ \n -> - let k = sizeOf (fromSymbol undefined) in - liftST (copyByteArray mbytearray (n*k) array (lo*k) ((hi-lo)*k)) `then_` - putIndex (n + hi-lo) + Builder $ \s arr# n# -> + let n = I# n# in + -- Reserve space for the termlist + case reserve s arr# (unInt (n + hi - lo)) of + (# s, arr# #) -> + let k = symbolSize + arr = MutableByteArray arr# in + case unST (copyByteArray arr (n*k) array (lo*k) ((hi - lo)*k)) s of + (# s, () #) -> + (# s, arr#, unInt (n + hi - lo) #) + +-- Make sure that the term array has enough space to hold the given +-- number of additional symbols. +{-# NOINLINE reserve #-} +reserve :: State# s -> MutableByteArray# s -> Int# -> (# State# s, MutableByteArray# s #) +reserve s arr# n# = + case reserve' (MutableByteArray arr#) (I# n#) of + ST m -> + case m s of + (# s, MutableByteArray arr# #) -> + (# s, arr# #) + where + {-# INLINE reserve' #-} + reserve' arr n = do + let !m = n*symbolSize + size <- getSizeofMutableByteArray arr + if size >= m then return arr else expand arr (size*2) m + expand arr size m + | size >= m = resizeMutableByteArray arr size + | otherwise = expand arr (size*2) m + +unST :: ST s a -> State# s -> (# State# s, a #) +unST (ST m) = m + +unInt :: Int -> Int# +unInt (I# n) = n ---------------------------------------------------------------------- -- Efficient subterm testing. diff --git a/Twee/Utils.hs b/Twee/Utils.hs --- a/Twee/Utils.hs +++ b/Twee/Utils.hs @@ -141,6 +141,31 @@ gen w y = floor (log y / log (1-w)) + 1 prefix = [0..k-1] +data Sample a = Sample Integer [(Integer, Int)] [a] + +emptySample :: Int -> Sample a +emptySample k = Sample 0 (reservoir k) [] + +addSample :: (Int, [a]) -> Sample a -> Sample a +addSample (m, xs) (Sample total ((n, pos):ps) sample) + | idx < fromIntegral m = + addSample (m, xs) $ + Sample total ps $ + take pos sample ++ + [xs !! fromIntegral idx] ++ + drop (pos+1) sample + where + idx = n - total +addSample (m, _) (Sample total ps sample) = + Sample (total+fromIntegral m) ps sample + +sampleValue :: Sample a -> [a] +sampleValue (Sample _ _ sample) = sample + +mapSample :: (a -> b) -> Sample a -> Sample b +mapSample f (Sample total ps sample) = + Sample total ps (map f sample) + -- A combined inits/tails. splits :: [a] -> [([a], [a])] splits [] = [([], [])] diff --git a/twee-lib.cabal b/twee-lib.cabal --- a/twee-lib.cabal +++ b/twee-lib.cabal @@ -1,5 +1,5 @@ name: twee-lib -version: 2.3.1 +version: 2.4 synopsis: An equational theorem prover homepage: http://github.com/nick8325/twee license: BSD3 @@ -32,11 +32,18 @@ flag llvm description: Build using LLVM backend for faster code. default: False + manual: True flag bounds-checks description: Use bounds checks for all array operations. default: False + manual: True +flag profile + description: Print a profiling report after every prover run. + default: False + manual: True + library exposed-modules: Twee @@ -47,19 +54,21 @@ Twee.Index Twee.Join Twee.KBO - Twee.Label Twee.PassiveQueue Twee.Pretty + Twee.Profile Twee.Proof Twee.Rule Twee.Rule.Index Twee.Term Twee.Task Twee.Utils + Data.Label other-modules: Data.ChurchList Data.DynamicArray Data.Heap + Data.Numbered Twee.Term.Core build-depends: @@ -85,3 +94,6 @@ Data.Primitive.SmallArray.Checked Data.Primitive.ByteArray.Checked Data.Primitive.Checked + if flag(profile) + cpp-options: -DPROFILE + build-depends: symbol, hashable, unordered-containers, rdtsc