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. ›
🪙‹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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet am 2026-06-10)
¤
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.
