Theory Current

section ‹Current Stack›

theory Current
imports Stack
begin

text ‹
\noindent This data structure is composed of:
▪ the newly added elements to one end of a deque during the rebalancing phase
▪ the number of these newly added elements 
▪ the originally contained elements
▪ the number of elements which will be contained after the rebalancing is finished.
›

datatype (plugins del: size) 'a current = Current "'a list" nat "'a stack" nat

fun push :: "'a ⇒ 'a current ⇒ 'a current" where
  "push x (Current extra added old remained) = Current (x#extra) (added + 1) old remained"

fun pop :: "'a current ⇒ 'a * 'a current" where
  "pop (Current [] added old remained)     = 
    (first old, Current [] added (Stack.pop old) (remained - 1))"
| "pop (Current (x#xs) added old remained) = 
    (x, Current xs (added - 1) old remained)"

fun first :: "'a current ⇒ 'a" where
  "first current = fst (pop current)"

abbreviation drop_first :: "'a current ⇒ 'a current" where
  "drop_first current ≡ snd (pop current)"

end