Stack.pec

module Data.Stack

// explicit export list

exports
  Stack
  any
  empty
  filter
  find
  find_idx
  fold
  foreach
  foreach_idx
  is_empty
  is_full
  map
  pop
  push
  put
  stack

imports
  Prelude
  Data.Array as A

where

// BAL: some Ptr's can be changed to Load Pointers

type Stack cnt a =
  { height :: W32
  , data :: Array #cnt a
  }
// stacks are polymorphic in their size and what they contain

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

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

find :: (a -> Bool) -> Ptr (Stack #cnt a) -> Maybe (Ptr a)
find f p => case new (find_idx f p) of
  Nothing -> Nothing
  Just i -> Just p.data[@i]

find_idx :: (a -> Bool) -> Ptr (Stack #cnt a) -> Maybe (Idx #cnt)
find_idx f p => A.unsafe_find_idx @p.height f p.data

any :: (a -> Bool) -> Ptr (Stack #cnt a) -> Bool
any f p => case new (find_idx f p) of
  Nothing -> False
  Just _ -> True

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

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

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

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

stack :: #cnt -> Stack #cnt a
stack _ => do
  p = unsafe_alloca
  empty p
  load p

push :: a -> Ptr (Stack #cnt a) -> Bool
push a p => branch
  is_full p -> False
  | do
      p.data[unsafe_to_idx @p.height] <- a
      inc p.height
      True

pop :: Ptr (Stack #cnt a) -> Maybe a
pop p => branch
  del p -> Just @p.data[unsafe_to_idx @p.height]
  | Nothing

del :: Ptr (Stack #cnt a) -> Bool
del p => branch
  is_empty p -> False
  | do
      dec p.height
      True

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

is_full :: { Load p } => Pointer p (Stack #cnt a) -> Bool
is_full p => @p.height > unsafe_cast (A.max_idx p.data)

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

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