(* -*- coq-prog-args: ("-emacs-U" "-R" "." "FingerTree" "-R" "../safe" "Safe" "-R" "../monads" "Monad") -*- *)
Require Import FingerTree.Reduce.
Require Import FingerTree.Digit.
Require Import Coq.subtac.Utils.
Require Import Safe.List.
Set Implicit Arguments.

Section Nodes.
  Inductive node(A : Type) : Type :=
  | Node2 : A -> A -> node A
  | Node3 : A -> A -> A -> node A.

  Definition node_to_digit (A : Type) (n : node A) : digit A :=
    match n with
      | Node2 x y => Two x y
      | Node3 x y z => Three x y z
    end.

  Section NodesReduce.
    Variables X Y : Type.
    Variable reducer : X -> Y -> Y.
    Variable reducel : Y -> X -> Y.
    Notation " x <_n y " := (reducer x y) (right associativity, at level 30).
    Notation " x >_n y " := (reducel x y) (left associativity, at level 21).
    
    Definition node_reducer n w :=
      match n with
        | Node2 x y => x <_n y <_n w
        | Node3 x y z => x <_n y <_n z <_n w
      end.
    
    
    Definition node_reducel w n :=
      match n with
        | Node2 x y => w >_n y >_n x
        | Node3 x y z => w >_n z >_n y >_n x
      end.
  End NodesReduce.
  
  Definition nodeReduce := mkReduce node_reducer node_reducel.
End Nodes.

Section Tree.

  Inductive fingertree (A : Type) : Type :=
  | Empty : fingertree A
  | Single : A -> fingertree A
  | Deep : digit A -> fingertree (node A) -> digit A -> fingertree A.
  
  Notation empty := (Empty _).

  Section TreeReduce.
    
    Program Fixpoint tree_reducer (X Y : Type) (redr : X -> Y -> Y) (n : fingertree X) (w : Y) {struct n} : Y :=
      match n with
        | Empty => w
        | Single x => redr x w
        | Deep pr m sf => 
          let rd := reducer digitReduce redr in
            let rt := tree_reducer (reducer nodeReduce redr) in
              rd pr (rt m (rd sf w))
      end.

    Program Fixpoint tree_reducel (X Y : Type) (redl : Y -> X -> Y) (w : Y) (n : fingertree X) {struct n} : Y :=
      match n with
        | Empty => w
        | Single x => redl w x
        | Deep pr m sf => 
          let rd := reducel digitReduce redl in
            let rt := tree_reducel (reducel nodeReduce redl) in
              rd (rt (rd w pr) m) sf
      end.
    
    Definition treeReduce := mkReduce tree_reducer tree_reducel.

  End TreeReduce.

  Section add.
    
    Program Fixpoint add_left A (a : A) (t : fingertree A) {struct t} : fingertree A :=
      match t with
        | Empty => Single a
        | Single b => Deep (One a) empty (One b)
        | Deep pr m sf => 
          match pr with
            | Four b c d e => Deep (Two a b) (add_left (Node3 c d e) m) sf
            | x => Deep (add_digit_left a pr) m sf
          end
      end.

    Next Obligation.
    Proof.
      intros.
      destruct pr ; simpl ; auto.
      elim H0 with a0 a1 a2 a3 ; eauto.
    Defined.

    Solve Obligations using red ; intros ; discriminate.

    Program Fixpoint add_right A (t : fingertree A) (a : A) {struct t} : fingertree A :=
      match t with
        | Empty => Single a
        | Single b => Deep (One b) empty (One a)
        | Deep pr m sf =>
          match sf with
            | Four b c d e => Deep pr (add_right m (Node3 b c d)) (Two e a)
            | _ => Deep pr m (add_digit_right sf a)
          end
      end.

    Next Obligation.
    Proof.
      intros.
      red ; intros.
      destruct sf ; simpl in * ; auto.
      apply H0 with a0 a1 a2 a3 ; eauto.
    Defined.
    
    Solve Obligations using red ; intros ; discriminate.

    Section add_reduce.
      Variable f : Type -> Type.
      Variable red : Reduce f.
      Variable A : Type.

      Definition add_left_red := reducer red (@add_left A).
      Definition add_right_red := reducel red (@add_right A).

      Definition toTree s := add_left_red s empty.

    End add_reduce.

  End add.

  Section view_L.
    Inductive View_L (s : Type -> Type) (a : Type) : Type := 
    | nil_L : View_L s a
    | cons_L : a -> s a -> View_L s a.

    Notation " 'nilL' " := (@nil_L _ _) (at level 30).
    Notation " 'consL' " := (@cons_L _ _) (at level 30).

    Program Fixpoint view_L (A : Type) (t : fingertree A) { struct t } : View_L fingertree A := 
      match t with
        | Empty => nilL
        | Single x => consL x empty
        | Deep pr m sf => 
          match pr with
            | One x => match view_L m with
                         | nil_L => consL x (toTree digitReduce _ sf)
                         | cons_L a m' => consL x (Deep (node_to_digit a) m' sf)
                       end
            | y => consL (digit_head y) (Deep (digit_tail y) m sf)
          end
      end.
    
    Next Obligation.
    Proof.
      intros.
      destruct pr ; simpl in * ; auto.
      red ; intros.
      apply H0 with a ; auto.
    Defined.

    Solve Obligations using red ; intros ; discriminate.

  End view_L.

  Section view_R.

    Inductive View_R (s : Type -> Type) (a : Type) : Type := 
    | nil_R : View_R s a
    | cons_R : s a -> a -> View_R s a.

    Notation " 'nilR' " := (@nil_R _ _) (at level 30).
    Notation " 'consR' " := (@cons_R _ _) (at level 30).

    Program Fixpoint view_R (A : Type) (t : fingertree A) { struct t } : View_R fingertree A := 
      match t with
        | Empty => nilR
        | Single x => consR empty x
        | Deep pr m sf => 
          match sf with
            | One x => consR (match view_R m with
                                | nil_R => toTree digitReduce _ pr
                                | cons_R m' a => Deep pr m' (node_to_digit a)
                              end) x
            | y => consR (Deep pr m (digit_liat y)) (digit_last y) 
          end
      end.

    Next Obligation.
    Proof.
      intros.
      destruct sf ; simpl in * ; auto. 
      elim H0 with a ; auto.
    Defined.

    Solve Obligations using red ; intros ; discriminate.

  End view_R.

  Section View.
    Variable A : Type.

    Definition isEmpty t := match @view_L A t with
                              | nil_L => true
                              | cons_L _ _ => false
                            end.
    Require Import Coq.subtac.Utils.
    
    Program Definition head (t : fingertree A | isEmpty t = false) : A := 
      match @view_L A t with
        | cons_L hd _ => hd
        | nil_L => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d ; simpl in * ; try discriminate.
      destruct (view_L x) ; discriminate.
    Qed.
    
    Program Definition tail (t : fingertree A | isEmpty t = false) : fingertree A := 
      match @view_L A t with
        | cons_L _ tl => tl
        | nil_L => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d ; simpl in * ; try discriminate.
      destruct (view_L x) ; discriminate.
    Qed.

    Program Definition last (t : fingertree A | isEmpty t = false) : A :=
      match @view_R A t with
        | cons_R _ x => x
        | nil_R => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d0 ; simpl in * ; try discriminate.
    Qed.
    
    Program Definition liat (t : fingertree A | isEmpty t = false) : fingertree A := 
      match @view_R A t with
        | cons_R prev last => prev
        | nil_R => !
      end.

    Next Obligation.
    Proof.
      intros.
      destruct x ; unfold isEmpty in * ;  simpl in * ; try discriminate.
      destruct d0 ; simpl in * ; try discriminate.
    Qed.

  End View.

  Section CatList.
    (** Concatenation using lists *)
    Program Fixpoint nodes_right (A : Type) (m : list A | m <> nil) (r : digit A) {measure length m} : list (node A) :=
      match m with
        | (cons x (cons y (cons z m'))) => Node2 x y :: nodes_right (cons z m') r
        | (cons u (cons v nil)) =>
          match r with
            | One w => [Node3 u v w]
            | Two w x => Node2 u v :: [Node2 w x]
            | Three w x y => Node3 u v w :: [Node2 x y]
            | Four w x y z => Node3 u v w :: [Node3 x y z]
          end
        | cons u nil =>
          match r with
            | One v => [Node2 u v]
            | Two v w => [Node3 u v w]
            | Three v w x => Node2 u v :: [Node2 w x]
            | Four v w x y => Node3 u v w :: [Node2 x y]
          end
        | nil => !
      end.

    Program Definition nodes (A : Type) (l : digit A) (m : list A) (r : digit A) : list (node A) :=
      nodes_right (toList digitReduce _ l ++ m) r.

    Next Obligation.
    Proof.
      intros.
      induction l ; simpl ; red ; intros ; discriminate.
    Qed.          

    Fixpoint app3 (A : Type) (xs : fingertree A) (ts : list A) (ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => add_left_red listReduce ts ys
        | xs, Empty => add_right_red listReduce xs ts
        | Single x, ys => add_left x (add_left_red listReduce ts ys)
        | xs, Single y => add_right (add_right_red listReduce xs ts) y
        | Deep pr m sf, Deep pr' m' sf' => Deep pr (app3 m (nodes sf ts pr') m') sf'

      end.

    Definition concat (A : Type) (x y : fingertree A) : fingertree A := 
      app3 x [] y.

  End CatList.
  
  Section Cat.
    (** Concatenation still using digits. *)
    Notation " x <_i y " := (add_right_red idReduce x y) (left associativity, at level 22).
    Notation " x >_i y " := (add_left_red idReduce x y) (right associativity, at level 30).

    Fixpoint appendTree0 (A : Type) (xs ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => ys
        | xs, Empty => xs
        | Single x, ys => add_left x ys
        | xs, Single y => add_right xs y
        | Deep pr m sf, Deep pr' m' sf' => 
          let f := 
            fun (A : Type) (xs : fingertree (node A)) (dl : digit A) (dr : digit A) (ys : fingertree (node A)) =>
              match dl with
                | One a => 
                  match dr with
                    | One b => appendTree1 xs (Node2 a b) ys
                    | Two b c => appendTree1 xs (Node3 a b c) ys
                    | Three b c d => appendTree2 xs (Node2 a b) (Node2 c d) ys
                    | Four b c d e => appendTree2 xs (Node3 a b c) (Node2 d e) ys
                  end
                | Two a b =>
                  match dr with
                    | One c => appendTree1 xs (Node3 a b c) ys
                    | Two c d => appendTree2 xs (Node2 a b) (Node2 c d) ys
                    | Three c d e => appendTree2 xs (Node3 a b c) (Node2 d e) ys
                    | Four c d e f => appendTree2 xs (Node3 a b c) (Node3 d e f) ys
                  end
                | Three a b c =>
                  match dr with
                    | One d => appendTree2 xs (Node2 a b) (Node2 c d) ys
                    | Two d e => appendTree2 xs (Node3 a b c) (Node2 d e) ys
                    | Three d e f => appendTree2 xs (Node3 a b c) (Node3 d e f) ys
                    | Four d e f g => appendTree3 xs (Node3 a b c) (Node2 d e) (Node2 f g) ys
                  end
                | Four a b c d =>
                  match dr with
                    | One e => appendTree2 xs (Node3 a b c) (Node2 d e) ys
                    | Two e f => appendTree2 xs (Node3 a b c) (Node3 d e f) ys
                    | Three e f g => appendTree3 xs (Node3 a b c) (Node2 d e) (Node2 f g) ys
                    | Four e f g h => appendTree3 xs (Node3 a b c) (Node3 d e f) (Node2 g h) ys
                  end
              end
              in
              Deep pr (f _ m sf pr' m') sf'
      end

    with appendTree1 (A : Type) (xs : fingertree A) (d : A) (ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => d >_i ys
        | xs, Empty => xs <_i d
        | Single x, ys => add_left x (d >_i ys)
        | xs, Single y => add_right (xs <_i d) y
        | Deep pr m sf, Deep pr' m' sf' => 
          let addDigits1 := 
            fun (A : Type) (xs : fingertree (node A)) (dl : digit A) (x : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree1 xs (Node3 a x b) ys
            | Two b c => appendTree2 xs (Node2 a x) (Node2 b c) ys
            | Three b c d => appendTree2 xs (Node3 a x b) (Node2 c d) ys
            | Four b c d e => appendTree2 xs (Node3 a x b) (Node3 c d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree2 xs (Node2 a b) (Node2 x c) ys
            | Two c d => appendTree2 xs (Node3 a b x) (Node2 c d) ys
            | Three c d e => appendTree2 xs (Node3 a b x) (Node3 c d e) ys
            | Four c d e f => appendTree3 xs (Node3 a b x) (Node2 c d) (Node2 e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree2 xs (Node3 a b c) (Node2 x d) ys
            | Two d e => appendTree2 xs (Node3 a b c) (Node3 x d e) ys
            | Three d e f => appendTree3 xs (Node3 a b c) (Node2 x d) (Node2 e f) ys
            | Four d e f g => appendTree3 xs (Node3 a b c) (Node3 x d e) (Node2 f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree2 xs (Node3 a b c) (Node3 d x e) ys
            | Two e f => appendTree3 xs (Node3 a b c) (Node2 d x) (Node2 e f) ys
            | Three e f g => appendTree3 xs (Node3 a b c) (Node3 d x e) (Node2 f g) ys
            | Four e f g h => appendTree3 xs (Node3 a b c) (Node3 d x e) (Node3 f g h) ys
          end
      end
      in Deep pr (addDigits1 _ m sf d pr' m') sf'
      end


    with appendTree2 (A : Type) (xs : fingertree A) (a b : A) (ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => a >_i b >_i ys
        | xs, Empty => xs <_i a <_i b
        | Single x, ys => add_left x (a >_i b >_i ys)
        | xs, Single y => add_right (xs <_i a <_i b) y
        | Deep pr m sf, Deep pr' m' sf' => 
          let addDigits2 := fun (A : Type) (xs : fingertree (node A)) (dl : digit A) (x y : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree2 xs (Node2 a x) (Node2 y b) ys
            | Two b c => appendTree2 xs (Node3 a x y) (Node2 b c) ys
            | Three b c d => appendTree2 xs (Node3 a x y) (Node3 b c d) ys
            | Four b c d e => appendTree3 xs (Node3 a x y) (Node2 b c) (Node2 d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree2 xs (Node3 a b x) (Node2 y c) ys
            | Two c d => appendTree2 xs (Node3 a b x) (Node3 y c d) ys
            | Three c d e => appendTree3 xs (Node3 a b x) (Node2 y c) (Node2 d e) ys
            | Four c d e f => appendTree3 xs (Node3 a b x) (Node3 y c d) (Node2 e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree2 xs (Node3 a b c) (Node3 x y d) ys
            | Two d e => appendTree3 xs (Node3 a b c) (Node2 x y) (Node2 d e) ys
            | Three d e f => appendTree3 xs (Node3 a b c) (Node3 x y d) (Node2 e f) ys
            | Four d e f g => appendTree3 xs (Node3 a b c) (Node3 x y d) (Node3 e f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree3 xs (Node3 a b c) (Node2 d x) (Node2 y e) ys
            | Two e f => appendTree3 xs (Node3 a b c) (Node3 d x y) (Node2 e f) ys
            | Three e f g => appendTree3 xs (Node3 a b c) (Node3 d x y) (Node3 e f g) ys
            | Four e f g h => appendTree4 xs (Node3 a b c) (Node3 d x y) (Node2 e f) (Node2 g h) ys
          end
      end
      in Deep pr (addDigits2 _ m sf a b pr' m') sf'
      end


    with appendTree3 (A : Type) (xs : fingertree A) (a b c : A) (ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => a >_i b >_i c >_i ys
        | xs, Empty => xs <_i a <_i b <_i c
        | Single x, ys => add_left x (a >_i b >_i c >_i ys)
        | xs, Single y => add_right (xs <_i a <_i b <_i c) y
        | Deep pr m sf, Deep pr' m' sf' =>
          let addDigits3 := fun (A : Type) (xs : fingertree (node A)) (dl : digit A) (x y z : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree2 xs (Node3 a x y) (Node2 z b) ys
            | Two b c => appendTree2 xs (Node3 a x y) (Node3 z b c) ys
            | Three b c d => appendTree3 xs (Node3 a x y) (Node2 z b) (Node2 c d) ys
            | Four b c d e => appendTree3 xs (Node3 a x y) (Node3 z b c) (Node2 d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree2 xs (Node3 a b x) (Node3 y z c) ys
            | Two c d => appendTree3 xs (Node3 a b x) (Node2 y z) (Node2 c d) ys
            | Three c d e => appendTree3 xs (Node3 a b x) (Node3 y z c) (Node2 d e) ys
            | Four c d e f => appendTree3 xs (Node3 a b x) (Node3 y z c) (Node3 d e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree3 xs (Node3 a b c) (Node2 x y) (Node2 z d) ys
            | Two d e => appendTree3 xs (Node3 a b c) (Node3 x y z) (Node2 d e) ys
            | Three d e f => appendTree3 xs (Node3 a b c) (Node3 x y z) (Node3 d e f) ys
            | Four d e f g => appendTree4 xs (Node3 a b c) (Node3 x y z) (Node2 d e) (Node2 f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree3 xs (Node3 a b c) (Node3 d x y) (Node2 z e) ys
            | Two e f => appendTree3 xs (Node3 a b c) (Node3 d x y) (Node3 z e f) ys
            | Three e f g => appendTree4 xs (Node3 a b c) (Node3 d x y) (Node2 z e) (Node2 f g) ys
            | Four e f g h => appendTree4 xs (Node3 a b c) (Node3 d x y) (Node3 z e f) (Node2 g h) ys
          end
      end
      in Deep pr (addDigits3 _ m sf a b c pr' m') sf'
      end

    with appendTree4 (A : Type) (xs : fingertree A) (a b c d : A) (ys : fingertree A) {struct xs} : fingertree A :=
      match xs, ys with
        | Empty, ys => a >_i b >_i c >_i d >_i ys
        | xs, Empty => xs <_i a <_i b <_i c <_i d 
        | Single x, ys => add_left x (a >_i b >_i c >_i d >_i ys)
        | xs, Single y => add_right (xs <_i a <_i b <_i c <_i d) y
        | Deep pr m sf, Deep pr' m' sf' =>
          let addDigits4 := fun (A : Type) (xs : fingertree (node A)) (dl : digit A) (x y z w : A) (dr : digit A) (ys : fingertree (node A)) =>
      match dl with
        | One a => 
          match dr with
            | One b => appendTree2 xs (Node3 a x y) (Node3 z w b) ys
            | Two b c => appendTree3 xs (Node3 a x y) (Node2 z w) (Node2 b c) ys
            | Three b c d => appendTree3 xs (Node3 a x y) (Node3 z w b) (Node2 c d) ys
            | Four b c d e => appendTree3 xs (Node3 a x y) (Node3 z w b) (Node3 c d e) ys
          end
        | Two a b =>
          match dr with
            | One c => appendTree3 xs (Node3 a b x) (Node2 y z) (Node2 w c) ys
            | Two c d => appendTree3 xs (Node3 a b x) (Node3 y z w) (Node2 c d) ys
            | Three c d e => appendTree3 xs (Node3 a b x) (Node3 y z w) (Node3 c d e) ys
            | Four c d e f => appendTree4 xs (Node3 a b x) (Node3 y z w) (Node2 c d) (Node2 e f) ys
          end
        | Three a b c =>
          match dr with
            | One d => appendTree3 xs (Node3 a b c) (Node3 x y z) (Node2 w d) ys
            | Two d e => appendTree3 xs (Node3 a b c) (Node3 x y z) (Node3 w d e) ys
            | Three d e f => appendTree4 xs (Node3 a b c) (Node3 x y z) (Node2 w d) (Node2 e f) ys
            | Four d e f g => appendTree4 xs (Node3 a b c) (Node3 x y z) (Node3 w d e) (Node2 f g) ys
          end
        | Four a b c d =>
          match dr with
            | One e => appendTree3 xs (Node3 a b c) (Node3 d x y) (Node3 z w e) ys
            | Two e f => appendTree4 xs (Node3 a b c) (Node3 d x y) (Node2 z w) (Node2 e f) ys
            | Three e f g => appendTree4 xs (Node3 a b c) (Node3 d x y) (Node3 z w e) (Node2 f g) ys
            | Four e f g h => appendTree4 xs (Node3 a b c) (Node3 d x y) (Node3 z w e) (Node3 f g h) ys
          end
      end in Deep pr (addDigits4 _ m sf a b c d pr' m') sf'
      end.

    Definition app (A : Type) (x y : fingertree A) : fingertree A := appendTree0 x y.
  
  End Cat.

End Tree.

Module Type Dequeue.
  Parameter elt : Type.
  Parameter t : Type.
  
  (* The empty dequeue *)
  Parameter empty : t.
  Notation " 'emptyset' " := empty.

  (* Test emptyness *)
  Parameter is_empty : t -> bool.
  
  Definition Empty t := is_empty t = true.

  (* Construct the singleton dequeue. *)
  Parameter tip : elt -> t.  

  (* Stack interface. *)
  Parameter push : elt -> t -> t.
  Parameter pop : forall x : t, (elt * t) + {Empty x}.

  (* Heap interface. *)
  Parameter queue : t -> elt -> t.
  Parameter dequeue : forall x : t, (t * elt) + {Empty x}.

  (* Concatenation. *)
  Parameter app : t -> t -> t.

End Dequeue.

Module Type Elt.
  Parameter t : Type.
End Elt.

Module FingerTreeDequeue(E : Elt) <: Dequeue.

  Definition elt := E.t.

  Definition t := fingertree elt.
  
  Definition empty := Empty elt.

  Definition is_empty (tree : t) := match tree with Empty => true | _ => false end.

  Definition Empty x := is_empty x = true.

  Definition tip (e : elt) := Single e.

  Definition push (e : elt) (tree : t) := add_left e tree.

  Program Definition pop (tree : t) : (elt * t) + {Empty tree} :=
    match view_L tree with
      | cons_L x y => inleft _ (x, y)
      | nil_L => inright _ _
    end.

  Next Obligation.
  Proof.
    intros.
    destruct tree ; unfold Empty ; simpl in * ; intuition ; try discriminate.
    destruct d ; simpl in * ; try discriminate.
    destruct (view_L tree) ; simpl in * ; try discriminate.
  Qed.

  Definition queue (tree : t) (e : elt) := add_right tree e.

  Program Definition dequeue (tree : t) : (t * elt) + {Empty tree} :=
    match view_R tree with
      | cons_R x y => inleft _ (x, y)
      | nil_R => inright _ _
    end.

  Next Obligation.
  Proof.
    intros.
    destruct tree ; unfold Empty ; simpl in * ; intuition ; try discriminate.
    destruct d0 ; simpl in * ; try discriminate.
  Qed.

  Definition app (x y : t) : t := app x y.

End FingerTreeDequeue.

Extraction "FingerTree.ml" FingerTreeDequeue pair.