section ‹Smaller End of Deque›
theory Small
imports Common
begin
text ‹
🚫 The smaller end of the deque during ‹Rebalancing› can be in one three phases:
🚫 ‹Small1›: Using the ‹step› function the originally contained elements are reversed.
🚫 ‹Small2›: Using the ‹step› function the newly obtained elements from the bigger end are reversed on top of the ones reversed in the previous phase.
🚫 ‹Small3›: See theory ‹Common›. Is used to reverse the elements from the two previous phases again to get them again in the original order.
🚫 Each phase contains a ‹current› state, which holds the original elements of the deque end.
›
datatype (plugins del: size) 'a small_state =
Small1 "'a current" "'a stack" "'a list"
| Small2 "'a current" "'a list" "'a stack" "'a list" nat
| Small3 "'a common_state"
text ‹🚫 Functions:
🚫 ‹push›, ‹pop›: Add and remove elements using the ‹current› state.
🚫 ‹step›: Executes one step of the rebalancing, while keeping the invariant.›
instantiation small_state::(type) step
begin
fun step_small_state :: "'a small_state → 'a small_state" where
"step (Small3 state) = Small3 (step state)"
| "step (Small1 current small auxS) = (
if is_empty small
then Small1 current small auxS
else Small1 current (Stack.pop small) ((Stack.first small)#auxS)
)"
| "step (Small2 current auxS big newS count) = (
if is_empty big
then Small3 (normalize (Copy current auxS newS count))
else Small2 current auxS (Stack.pop big) ((Stack.first big)#newS) (count + 1)
)"
instance..
end
fun push :: "'a → 'a small_state → 'a small_state" where
"push x (Small3 state) = Small3 (Common.push x state)"
| "push x (Small1 current small auxS) = Small1 (Current.push x current) small auxS"
| "push x (Small2 current auxS big newS count) =
Small2 (Current.push x current) auxS big newS count"
fun pop :: "'a small_state → 'a * 'a small_state" where
"pop (Small3 state) = (
let (x, state) = Common.pop state
in (x, Small3 state)
)"
| "pop (Small1 current small auxS) =
(first current, Small1 (drop_first current) small auxS)"
| "pop (Small2 current auxS big newS count) =
(first current, Small2 (drop_first current) auxS big newS count)"
end
¤ Dauer der Verarbeitung: 0.33 Sekunden
¤
*© Formatika GbR, Deutschland
