Theory Big

section ‹Bigger End of Deque›

theory Big
imports Common
begin

text ‹⇤ The bigger end of the deque during rebalancing can be in two phases:

 ➧ ‹Big1›: Using the ‹step› function the originally contained elements, 
    which will be kept in this end, are reversed.
 ➧ ‹Big2›: Specified in theory ‹Common›. Is used to reverse the elements from the previous phase 
    again to get them in the original order.

⇤ Each phase contains a ‹current› state, which holds the original elements of the deque end. 
›

datatype (plugins del: size) 'a big_state = 
     Big1 "'a current" "'a stack" "'a list" nat
   | Big2 "'a common_state"

text ‹⇤ Functions:

➧ ‹push›, ‹pop›: Add and remove elements using the ‹current› state.
➧ ‹step›: Executes one step of the rebalancing›

instantiation big_state ::(type) step
begin

fun step_big_state :: "'a big_state ⇒ 'a big_state" where
  "step (Big2 state) = Big2 (step state)"
| "step (Big1 current _ aux 0) = Big2 (normalize (Copy current aux [] 0))"
| "step (Big1 current big aux count) = 
     Big1 current (Stack.pop big) ((Stack.first big)#aux) (count - 1)"

instance..
end

fun push :: "'a ⇒ 'a big_state ⇒ 'a big_state" where
  "push x (Big2 state) = Big2 (Common.push x state)"
| "push x (Big1 current big aux count) = Big1 (Current.push x current) big aux count"

fun pop :: "'a big_state ⇒ 'a * 'a big_state" where
  "pop (Big2 state) = (let (x, state) = Common.pop state in (x, Big2 state))"
| "pop (Big1 current big aux count) = 
    (first current, Big1 (drop_first current) big aux count)"

end