text‹ 🪙 The last two phases of both deque ends during rebalancing:
🪙‹Copy›: Using the ‹step› function the new elements of this deque end are brought back into the original order. 🪙‹Idle›: The rebalancing of the deque end is finished.
🪙 Each phase contains a ‹current› state, that holds the original elements of the deque end. ›
🪙‹push›, ‹pop›: Add and remove elements using the ‹current› state. 🪙‹step›: Executes one step of the rebalancing, while keeping the invariant.›
(* TODO: Maybe inline function? *) fun normalize :: "'a common_state ==> 'a common_state"where "normalize (Copy current old new moved) = ( case current of Current extra added _ remained ==> if moved ≥ remained then Idle current (idle.Idle (Stack extra new) (added + moved)) else Copy current old new moved )"
instantiation common_state ::(type) step begin
fun step_common_state :: "'a common_state ==> 'a common_state"where "step (Idle current idle) = Idle current idle"
| "step (Copy current aux new moved) = ( case current of Current _ _ _ remained ==> normalize ( if moved < remained then Copy current (tl aux) ((hd aux)#new) (moved + 1) else Copy current aux new moved ) )"
instance.. end
fun push :: "'a ==> 'a common_state ==> 'a common_state"where "push x (Idle current (idle.Idle stack stackSize)) = Idle (Current.push x current) (idle.Idle (Stack.push x stack) (Suc stackSize))"
| "push x (Copy current aux new moved) = Copy (Current.push x current) aux new moved"
fun pop :: "'a common_state ==> 'a * 'a common_state"where "pop (Idle current idle) = (let (x, idle) = Idle.pop idle in (x, Idle (drop_first current) idle))"
| "pop (Copy current aux new moved) = (first current, normalize (Copy (drop_first current) aux new moved))"
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
