From 79d383bee98ed3123b1373f23f531f9cdce25f13 Mon Sep 17 00:00:00 2001 From: Nick Smallbone Date: Fri, 15 Sep 2017 17:00:59 +0200 Subject: [PATCH] Move some files around. --- src/{Twee => Data}/ChurchList.hs | 2 +- src/{Twee/Array.hs => Data/DynamicArray.hs} | 2 +- src/{Twee => Data}/Heap.hs | 90 +++++++++++++-------- src/Twee/CP.hs | 4 +- src/Twee/Index.hs | 2 +- src/Twee/Index/Lookup.hs | 2 +- src/Twee/PassiveQueue.hs | 2 +- twee.cabal | 12 +-- 8 files changed, 71 insertions(+), 45 deletions(-) rename src/{Twee => Data}/ChurchList.hs (98%) rename src/{Twee/Array.hs => Data/DynamicArray.hs} (98%) rename src/{Twee => Data}/Heap.hs (55%) diff --git a/src/Twee/ChurchList.hs b/src/Data/ChurchList.hs similarity index 98% rename from src/Twee/ChurchList.hs rename to src/Data/ChurchList.hs index 6971464..32485c7 100644 --- a/src/Twee/ChurchList.hs +++ b/src/Data/ChurchList.hs @@ -1,6 +1,6 @@ -- Church-encoded lists. Used in Twee.CP to make sure that fusion happens. {-# LANGUAGE Rank2Types, BangPatterns #-} -module Twee.ChurchList where +module Data.ChurchList where import Prelude(Functor(..), Applicative(..), Monad(..), Bool(..), Maybe(..), (.), ($), id) import qualified Prelude diff --git a/src/Twee/Array.hs b/src/Data/DynamicArray.hs similarity index 98% rename from src/Twee/Array.hs rename to src/Data/DynamicArray.hs index e33f892..dbf2210 100644 --- a/src/Twee/Array.hs +++ b/src/Data/DynamicArray.hs @@ -1,7 +1,7 @@ -- | Zero-indexed dynamic arrays, optimised for lookup. -- Modification is slow. Uninitialised indices have a default value. {-# LANGUAGE CPP #-} -module Twee.Array where +module Data.DynamicArray where #ifdef BOUNDS_CHECKS import qualified Data.Primitive.SmallArray.Checked as P diff --git a/src/Twee/Heap.hs b/src/Data/Heap.hs similarity index 55% rename from src/Twee/Heap.hs rename to src/Data/Heap.hs index f1b281d..fe2f904 100644 --- a/src/Twee/Heap.hs +++ b/src/Data/Heap.hs @@ -1,75 +1,99 @@ +-- | Skew heaps. + {-# LANGUAGE BangPatterns, ScopedTypeVariables #-} --- Skew heaps. -module Twee.Heap( - Heap, empty, insert, removeMin, mapMaybe, size) where +module Data.Heap( + Heap, empty, singleton, insert, removeMin, union, mapMaybe, size) where + +-- | A heap. +-- Representation: the size of the heap, and the heap itself. data Heap a = Heap {-# UNPACK #-} !Int !(Heap1 a) deriving Show +-- N.B.: arguments are not strict so code has to take care +-- to force stuff appropriately. data Heap1 a = Nil | Node a (Heap1 a) (Heap1 a) deriving Show -{-# INLINEABLE merge #-} -merge :: Ord a => Heap a -> Heap a -> Heap a -merge (Heap n1 h1) (Heap n2 h2) = Heap (n1+n2) (merge1 h1 h2) +-- | Take the union of two heaps. +{-# INLINEABLE union #-} +union :: Ord a => Heap a -> Heap a -> Heap a +union (Heap n1 h1) (Heap n2 h2) = Heap (n1+n2) (union1 h1 h2) -{-# INLINEABLE merge1 #-} -merge1 :: forall a. Ord a => Heap1 a -> Heap1 a -> Heap1 a -merge1 = m1 +{-# INLINEABLE union1 #-} +union1 :: forall a. Ord a => Heap1 a -> Heap1 a -> Heap1 a +union1 = u1 where - -- For some reason using m1 improves the code generation... - m1 :: Heap1 a -> Heap1 a -> Heap1 a - m1 Nil h = h - m1 h Nil = h - m1 h1@(Node x1 l1 r1) h2@(Node x2 l2 r2) - | x1 <= x2 = (Node x1 $! m1 r1 h2) l1 - | otherwise = (Node x2 $! m1 r2 h1) l2 - -{-# INLINE unit #-} -unit :: a -> Heap a -unit !x = Heap 1 (Node x Nil Nil) - + -- The generated code is better when we do everything + -- through this u1 function instead of union1... + -- This is because u1 has no Ord constraint in its type. + u1 :: Heap1 a -> Heap1 a -> Heap1 a + u1 Nil h = h + u1 h Nil = h + u1 h1@(Node x1 l1 r1) h2@(Node x2 l2 r2) + | x1 <= x2 = (Node x1 $! u1 r1 h2) l1 + | otherwise = (Node x2 $! u1 r2 h1) l2 + +-- | A singleton heap. +{-# INLINE singleton #-} +singleton :: a -> Heap a +singleton !x = Heap 1 (Node x Nil Nil) + +-- | The empty heap. {-# INLINE empty #-} empty :: Heap a empty = Heap 0 Nil +-- | Insert an element. {-# INLINEABLE insert #-} insert :: Ord a => a -> Heap a -> Heap a -insert x h = merge (unit x) h +insert x h = union (singleton x) h +-- | Find and remove the minimum element. {-# INLINEABLE removeMin #-} removeMin :: Ord a => Heap a -> Maybe (a, Heap a) removeMin (Heap _ Nil) = Nothing -removeMin (Heap n (Node x l r)) = Just (x, Heap (n-1) (merge1 l r)) +removeMin (Heap n (Node x l r)) = Just (x, Heap (n-1) (union1 l r)) +-- | Map a function over a heap, removing all values which +-- map to 'Nothing'. May be more efficient when the function +-- being mapped is mostly monotonic. {-# INLINEABLE mapMaybe #-} mapMaybe :: Ord b => (a -> Maybe b) -> Heap a -> Heap b mapMaybe f (Heap _ h) = Heap (sz 0 h') h' where + -- Compute the size fairly efficiently. sz !n Nil = n sz !n (Node _ l r) = sz (sz (n+1) l) r - h' = go h + h' = mm h - go Nil = Nil - go (Node x l r) = + mm Nil = Nil + mm (Node x l r) = case f x of - Nothing -> merge1 l' r' + -- If the value maps to Nothing, get rid of it. + Nothing -> union1 l' r' + -- Otherwise, check if the heap invariant still holds + -- and sift downwards to restore it. Just !y -> down y l' r' where - !l' = go l - !r' = go r + !l' = mm l + !r' = mm r down x l@(Node y ll lr) r@(Node z rl rr) + -- Put the smallest of x, y and z at the root. | y < x && y <= z = (Node y $! down x ll lr) r | z < x && z <= y = Node z l $! down x rl rr down x Nil (Node y l r) + -- Put the smallest of x and y at the root. | y < x = Node y Nil $! down x l r down x (Node y l r) Nil + -- Put the smallest of x and y at the root. | y < x = (Node y $! down x l r) Nil down x l r = Node x l r +-- | The number of elements in the heap. {-# INLINE size #-} size :: Heap a -> Int size (Heap n _) = n @@ -85,8 +109,8 @@ size (Heap n _) = n -- arb 0 = return empty -- arb n = -- frequency --- [(1, unit <$> arbitrary), --- (n-1, merge <$> arb' <*> arb')] +-- [(1, singleton <$> arbitrary), +-- (n-1, union <$> arb' <*> arb')] -- where -- arb' = arb (n `div` 2) @@ -118,9 +142,9 @@ size (Heap n _) = n -- Nothing -> discard -- Just (x, h') -> toList h == List.insert x (toList h') -- prop_7 h1 h2 = withMaxSuccess 10000 $ --- invariant (merge h1 h2) +-- invariant (union h1 h2) -- prop_8 h1 h2 = withMaxSuccess 10000 $ --- toList (merge h1 h2) == List.sort (toList h1 ++ toList h2) +-- toList (union h1 h2) == List.sort (toList h1 ++ toList h2) -- prop_9 (Blind f) h = withMaxSuccess 10000 $ -- invariant (mapMaybe f h) -- prop_10 (Blind f) h = withMaxSuccess 1000000 $ diff --git a/src/Twee/CP.hs b/src/Twee/CP.hs index fa8f86a..235e1fb 100644 --- a/src/Twee/CP.hs +++ b/src/Twee/CP.hs @@ -10,8 +10,8 @@ import qualified Data.Set as Set import Control.Monad import Data.Maybe import Data.List -import qualified Twee.ChurchList as ChurchList -import Twee.ChurchList (ChurchList(..)) +import qualified Data.ChurchList as ChurchList +import Data.ChurchList (ChurchList(..)) import Twee.Utils import Twee.Equation import qualified Twee.Proof as Proof diff --git a/src/Twee/Index.hs b/src/Twee/Index.hs index 7b7bd1d..cab10e9 100644 --- a/src/Twee/Index.hs +++ b/src/Twee/Index.hs @@ -13,7 +13,7 @@ import Prelude hiding (filter, map, null) import Data.Maybe import Twee.Base hiding (var, fun, empty, size, singleton, prefix, funs, lookupList) import qualified Twee.Term as Term -import Twee.Array +import Data.DynamicArray import qualified Data.List as List import Twee.Utils import Twee.Index.Lookup diff --git a/src/Twee/Index/Lookup.hs b/src/Twee/Index/Lookup.hs index bc3051d..d862e38 100644 --- a/src/Twee/Index/Lookup.hs +++ b/src/Twee/Index/Lookup.hs @@ -10,7 +10,7 @@ module Twee.Index.Lookup where import Twee.Base hiding (var, fun, empty, size, singleton, prefix, funs) import qualified Twee.Term as Term import Twee.Term.Core(TermList(..)) -import Twee.Array +import Data.DynamicArray data Index f a = Index { diff --git a/src/Twee/PassiveQueue.hs b/src/Twee/PassiveQueue.hs index a802f05..e236d95 100644 --- a/src/Twee/PassiveQueue.hs +++ b/src/Twee/PassiveQueue.hs @@ -6,7 +6,7 @@ module Twee.PassiveQueue( Passive(..), empty, insert, removeMin, mapMaybe) where -import qualified Twee.Heap as Heap +import qualified Data.Heap as Heap import qualified Data.Vector.Unboxed as Vector import Data.Int import Data.List hiding (insert) diff --git a/twee.cabal b/twee.cabal index d443631..503f567 100644 --- a/twee.cabal +++ b/twee.cabal @@ -47,15 +47,11 @@ flag bounds-checks library exposed-modules: Twee - Twee.Array Twee.Base - Twee.ChurchList Twee.Constraints Twee.CP Twee.Equation - Twee.Heap Twee.Index - Twee.Index.Lookup Twee.Join Twee.KBO Twee.Label @@ -65,9 +61,15 @@ library Twee.Rule Twee.Rule.Index Twee.Term - Twee.Term.Core Twee.Task Twee.Utils + other-modules: + Data.ChurchList + Data.DynamicArray + Data.Heap + Twee.Index.Lookup + Twee.Term.Core + build-depends: base >= 4 && < 5, containers,