Skip to content

Commit

Permalink
Move some files around.
Browse files Browse the repository at this point in the history
  • Loading branch information
nick8325 committed Sep 15, 2017
1 parent 6a47ee8 commit 79d383b
Show file tree
Hide file tree
Showing 8 changed files with 71 additions and 45 deletions.
2 changes: 1 addition & 1 deletion src/Twee/ChurchList.hs → src/Data/ChurchList.hs
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Twee/Array.hs → src/Data/DynamicArray.hs
Original file line number Diff line number Diff line change
@@ -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
Expand Down
90 changes: 57 additions & 33 deletions src/Twee/Heap.hs → src/Data/Heap.hs
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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)

Expand Down Expand Up @@ -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 $
Expand Down
4 changes: 2 additions & 2 deletions src/Twee/CP.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Twee/Index.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Twee/Index/Lookup.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion src/Twee/PassiveQueue.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
12 changes: 7 additions & 5 deletions twee.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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,
Expand Down

0 comments on commit 79d383b

Please sign in to comment.