Deque.pec

module Data.Deque

exports
  Deque
  any
  del_back
  deque
  empty
  filter
  find
  find_idx
  fold
  foreach
  foreach_idx
  is_empty
  is_full
  map
  pop_back
  pop_front
  push_back
  push_front
  put

imports
  Prelude
  Data.Array as A

where

type Deque cnt a =
  { back :: Idx #cnt
  , height :: W32
  , data :: Array #cnt a
  }

filter :: (a -> Bool) -> Ptr (Deque #cnt a) -> ()
filter f p => do
  h = @p.height
  empty p
  unsafe_foreach_idx (back p) h (filter_elem f p)

filter_elem :: (a -> Bool) -> Ptr (Deque #cnt a) -> Idx #cnt -> ()
filter_elem f p i => do
  a = @p.data[i]
  when (f a) (assert (push_front a p))

any :: { Load p } => (a -> Bool) -> Pointer p (Deque #cnt a) -> Bool
any f p => case new (find_idx f p) of
  Nothing -> False
  Just _ -> True

find :: { Load p } =>
  (a -> Bool) -> Pointer p (Deque #cnt a) -> Maybe (Pointer p a)
find f p => case new (find_idx f p) of
  Nothing -> Nothing
  Just i -> Just p.data[@i]

find_idx :: { Load p } =>
  (a -> Bool) -> Pointer p (Deque #cnt a) -> Maybe (Idx #cnt)
find_idx f p => unsafe_find_idx (back p) @p.height f p.data

unsafe_find_idx :: { Load p } =>
  Idx #cnt -> W32 -> (a -> Bool) -> Pointer p (Array #cnt a) ->
  Maybe (Idx #cnt)
unsafe_find_idx b j f p => do
  i = new (0 :: W32)
  while ((@i < j) && (not (f @p[wrap_add b @i]))) (inc i)
  branch
    @i == j -> Nothing
    | Just (unsafe_to_idx @i)

map :: (a -> b) -> Ptr (Deque #cnt a) -> Deque #cnt b
map f p => do
  q = unsafe_alloca
  foreach_idx (A.map_idx f p.data q.data) p
  q.height <- @p.height
  q.back <- @p.back
  load q

foreach :: { Load p } =>
  (Pointer p a -> ()) -> Pointer p (Deque #cnt a) -> ()
foreach f p => foreach_idx (A.apply_at_idx f p.data) p

foreach_idx :: { Load p } =>
  (Idx #cnt -> ()) -> Pointer p (Deque #cnt a) -> ()
foreach_idx f p => unsafe_foreach_idx (back p) @p.height f

unsafe_foreach_idx :: Idx #cnt -> W32 -> (Idx #cnt -> ()) -> ()
unsafe_foreach_idx b h f => times h (\i -> f (wrap_add b i))

deque :: #cnt -> Deque #cnt a
deque _ => do
  p = unsafe_alloca
  p.back <- 0
  empty p
  load p

empty :: Ptr (Deque #cnt a) -> ()
empty p => p.height <- 0

push_front :: a -> Ptr (Deque #cnt a) -> Bool
push_front a p => branch
  is_full p -> False
  | do
      p.data[front p] <- a
      inc p.height
      True

pop_front :: Ptr (Deque #cnt a) -> Maybe a
pop_front p => branch
  is_empty p -> Nothing
  | do
      dec p.height
      Just @p.data[front p]

push_back :: a -> Ptr (Deque #cnt a) -> Bool
push_back a p => branch
  is_full p -> False
  | do
      p.data[@p.back] <- a
      p.back <- wrap_dec @p.back
      inc p.height
      True

pop_back :: Ptr (Deque #cnt a) -> Maybe a
pop_back p => branch
  del_back p -> Just @p.data[@p.back]
  | Nothing

del_back :: Ptr (Deque #cnt a) -> Bool
del_back p => branch
  is_empty p -> False
  | do
      p.back <- wrap_add @p.back 1
      dec p.height
      True

is_empty :: { Load p } => Pointer p (Deque #cnt a) -> Bool
is_empty p => @p.height == 0

is_full :: { Load p } => Pointer p (Deque #cnt a) -> Bool
is_full p => @p.height == count p.data

front :: { Load p } => Pointer p (Deque #cnt a) -> Idx #cnt
front p => wrap_add (back p) @p.height

back :: { Load p } => Pointer p (Deque #cnt a) -> Idx #cnt
back p => wrap_add @p.back 1

wrap_op :: (W32 -> W32) -> Idx #cnt -> Idx #cnt
wrap_op f a => unsafe_to_idx ((f (from_idx a)) % (count_idx a))

wrap_add :: Idx #cnt -> W32 -> Idx #cnt
wrap_add a b => wrap_op (add b) a

wrap_dec :: Idx #cnt -> Idx #cnt
wrap_dec a => wrap_add a (count_idx a - 1)

put :: { Load p } =>
  (a -> ()) -> Pointer p (Deque #cnt a) -> ()
put f p => putBrackets (foreach (putElem f) p)

fold :: { Load p } => (b -> a -> b) -> b -> Pointer p (Deque #cnt a) -> b
fold f b deq => do
  pb = new b
  foreach (fold_ptr f pb) deq
  @pb