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)"
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.
