twee-lib 2.3.1 → 2.4
raw patch · 21 files changed
+1146/−737 lines, 21 filesdep +hashabledep +rdtscdep +symboldep ~base
Dependencies added: hashable, rdtsc, symbol, unordered-containers
Dependency ranges changed: base
Files
- Data/ChurchList.hs +1/−1
- Data/DynamicArray.hs +19/−10
- Data/Label.hs +133/−0
- Data/Numbered.hs +65/−0
- Twee.hs +115/−162
- Twee/Base.hs +1/−4
- Twee/CP.hs +100/−80
- Twee/Constraints.hs +1/−1
- Twee/Equation.hs +22/−9
- Twee/Index.hs +367/−209
- Twee/Join.hs +2/−4
- Twee/KBO.hs +0/−2
- Twee/Label.hs +0/−125
- Twee/Profile.hs +141/−0
- Twee/Proof.hs +7/−6
- Twee/Rule.hs +8/−9
- Twee/Rule/Index.hs +4/−4
- Twee/Term.hs +21/−24
- Twee/Term/Core.hs +100/−85
- Twee/Utils.hs +25/−0
- twee-lib.cabal +14/−2
Data/ChurchList.hs view
@@ -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
Data/DynamicArray.hs view
@@ -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')
+ Data/Label.hs view
@@ -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
+ Data/Numbered.hs view
@@ -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+
Twee.hs view
@@ -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.
Twee/Base.hs view
@@ -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 #-}
Twee/CP.hs view
@@ -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))
Twee/Constraints.hs view
@@ -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)
Twee/Equation.hs view
@@ -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)
Twee/Index.hs view
@@ -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+
Twee/Join.hs view
@@ -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
Twee/KBO.hs view
@@ -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
− Twee/Label.hs
@@ -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
+ Twee/Profile.hs view
@@ -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
Twee/Proof.hs view
@@ -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
Twee/Rule.hs view
@@ -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 #-}
Twee/Rule/Index.hs view
@@ -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,
Twee/Term.hs view
@@ -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)))
Twee/Term/Core.hs view
@@ -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.
Twee/Utils.hs view
@@ -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 [] = [([], [])]
twee-lib.cabal view
@@ -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