diff --git a/lib/datastruct/deQueue.ml b/lib/datastruct/deQueue.ml
new file mode 100644
index 0000000000000000000000000000000000000000..71c30869d4705f0b7cbbeffb67f16cf189d82b64
--- /dev/null
+++ b/lib/datastruct/deQueue.ml
@@ -0,0 +1,76 @@
+module type DoubleEndedQueue = 
+sig 
+  type 'elt t 
+
+  val empty : 'elt t 
+
+  val is_empty : 'elt t -> bool 
+
+  val push_left : 'elt -> 'elt t -> 'elt t 
+
+  val push_right : 'elt t -> 'elt -> 'elt t 
+
+  val view_left : 'elt t -> ('elt * 'elt t) option 
+
+  val view_right : 'elt t -> ('elt t * 'elt) option
+
+  val to_list : 'elt t -> 'elt list 
+
+  val of_list : 'elt list -> 'elt t 
+
+  val reverse : 'elt t -> 'elt t 
+
+  val push_all_left : 'elt list -> 'elt t -> 'elt t 
+
+  val push_all_right : 'elt t -> 'elt list -> 'elt t 
+end 
+
+
+
+module NaiveQueue : DoubleEndedQueue = 
+struct 
+
+  type 'elt t = 'elt list * 'elt list 
+
+  let empty = ([], [])
+
+  let is_empty = function 
+  | ([], []) -> true
+  | _ -> false 
+
+  let push_left elt (prefix, suffix) = (elt::prefix, suffix)
+
+  let push_right  (prefix, suffix) elt = (prefix, elt::suffix)
+
+  let rec view_left = function 
+  | ([], []) -> None 
+  | (head::prefix, suffix) -> Some (head, (prefix, suffix))
+  | ([], suffix) -> view_left (List.rev suffix, [])
+
+  let rec view_right = function
+  | ([],[]) -> None 
+  | (prefix, last::suffix) -> Some ((prefix, suffix), last) 
+  | (prefix,[]) -> view_right ([], List.rev prefix)
+
+
+  let to_list (prefix, suffix) = prefix @ (List.rev suffix)
+
+  let of_list prefix = (prefix, [])
+
+  let reverse (prefix, suffix) = (suffix, prefix)
+
+  let push_all_left list queue =
+    List.fold_left (fun queue elt -> push_left elt queue) queue list 
+
+  let push_all_right queue list = 
+    List.fold_left push_right queue list
+end
+
+
+include NaiveQueue
+
+
+let singleton elt = push_right empty elt 
+
+let (@>) = push_all_left 
+let (@<) = push_all_right 
diff --git a/lib/datastruct/deQueue.mli b/lib/datastruct/deQueue.mli
new file mode 100644
index 0000000000000000000000000000000000000000..068e1ac96a803b7b6b22954c97bd46c9a11ed777
--- /dev/null
+++ b/lib/datastruct/deQueue.mli
@@ -0,0 +1,30 @@
+type 'elt t 
+
+val empty : 'elt t 
+
+val is_empty : 'elt t -> bool 
+
+val push_left : 'elt -> 'elt t -> 'elt t 
+
+val push_right : 'elt t -> 'elt -> 'elt t 
+
+val view_left : 'elt t -> ('elt * 'elt t) option 
+
+val view_right : 'elt t -> ('elt t * 'elt) option
+
+val to_list : 'elt t -> 'elt list 
+
+val of_list : 'elt list -> 'elt t 
+
+val reverse : 'elt t -> 'elt t 
+
+val push_all_left : 'elt list -> 'elt t -> 'elt t 
+
+val push_all_right : 'elt t -> 'elt list -> 'elt t 
+
+
+val singleton : 'elt -> 'elt t 
+
+val (@>) :  'elt list -> 'elt t -> 'elt t 
+
+val (@<) : 'elt t -> 'elt list -> 'elt t 
diff --git a/lib/dune b/lib/dune
index 9642e1e8eda13d3bb983d3a54a71f62818180580..92523746f0ebf6d05c3811def6dae42024daf52c 100644
--- a/lib/dune
+++ b/lib/dune
@@ -3,3 +3,5 @@
  (libraries fix feat)
  (instrumentation (backend landmarks))
 )
+
+(env (dev (flags :standard -warn-error -27-32-33)))
diff --git a/lib/pqtree/functionalBL.mli b/lib/pqtree/functionalBL.mli
index fc9a9e55ae422b20ac3100acb9f253a5123bebf5..c26e89f01c04e62d6778cffbfedfa7c7cd2d85f5 100644
--- a/lib/pqtree/functionalBL.mli
+++ b/lib/pqtree/functionalBL.mli
@@ -1,7 +1,14 @@
 
-(** [add_interval is_in_interval interval_length pq_tree] returns a
+(** [add_interval is_in_subset subset_cardinal pq_tree] returns a
    PQ-tree obtained from [pq_tree] by adding an interval described by
    [is_in_interval] and containing [interval_length] elements.
+
+   @param is_in_subset a subset of elements represented as a predicate,
+     [true] for any element in the subset
+   @param subset_cardinal the number of elements in the subset
+   @param tree a PQ-tree
+   @return Some PQ-tree representing the set of permutations that are represented in [tree] and admits the subset as an interval, [None] if no such permutation exists.
+
  *)
 val add_interval : ('elt -> bool) -> int -> 'elt PqTree.t -> 'elt PqTree.t option
 
diff --git a/lib/pqtree/pqChainInsertion.ml b/lib/pqtree/pqChainInsertion.ml
index 7c98da6162b4ff3d96c82007fa03d1bf227e86f4..c5f626b6d3dc9ddad8a72605a531166abef2c5fe 100644
--- a/lib/pqtree/pqChainInsertion.ml
+++ b/lib/pqtree/pqChainInsertion.ml
@@ -114,6 +114,7 @@ module Make =
 
     let sort_children_of_p_node children =
       let group = function 
+      | [ ConstantSubtree _ as tree ] -> [ Single tree ]
       | (ConstantSubtree (delta,_)::_) as trees -> [ Group (delta, List.map tree_of_external_tree trees) ]
       | trees -> List.map (fun t -> Single t) trees
       in
@@ -137,11 +138,11 @@ module Make =
 
     type centered_subtree =
     | Balanced of int * pqtree
-    | Skew of int * pqtree list * int 
+    | Skew of int * pqtree DeQueue.t * int 
 
     let tree_of_centered_tree = function 
     | Balanced (_, tree) -> tree
-    | Skew (_,children,_) -> q children
+    | Skew (_,children,_) -> q (DeQueue.to_list children)
 
     let bounds_centered = function 
     | Balanced (delta,_) -> (delta, delta)
@@ -149,7 +150,7 @@ module Make =
 
     let contract_centered = function
     | Balanced (_,single) -> [ single ]
-    | Skew (_,children,_) -> children
+    | Skew (_,children,_) -> DeQueue.to_list children
 
 
     type result = 
@@ -183,58 +184,66 @@ module Make =
 
     type queue = 
       { left_bound : int;
-        left_trees : pqtree list;
-        right_trees : pqtree list;
+        trees : pqtree DeQueue.t;
         right_bound : int
       }
 
     let init_queue = function 
     | Balanced (bound, tree) -> 
-        { left_bound = bound; left_trees = []; right_trees = [tree]; right_bound = bound }
-    | Skew (left_bound, right_trees, right_bound) ->
-        { left_bound; left_trees = []; right_trees; right_bound }
+        { left_bound = bound; trees = DeQueue.(push_left tree empty); right_bound = bound }
+    | Skew (left_bound, trees, right_bound) ->
+        { left_bound; trees; right_bound }
                    
     let is_balanced queue = queue.left_bound = queue.right_bound
 
-    let compact queue = 
-      match List.rev_append queue.left_trees queue.right_trees with 
-      | [single_child] when is_balanced queue -> Balanced (queue.left_bound, single_child)
-      | children when is_balanced queue -> Balanced (queue.left_bound, q children)
-      | children -> Skew (queue.left_bound, children, queue.right_bound)
+    let collapse queue = 
+      match DeQueue.view_left queue.trees with 
+      | Some (child, trees) when DeQueue.is_empty trees && is_balanced queue -> 
+          (queue.left_bound, child)
+      | _ -> 
+          (max queue.left_bound queue.right_bound, q (DeQueue.to_list queue.trees))
 
     let enqueue_right group queue = 
-      let (right_trees, right_bound) = match group with  
-      | Group (bound, children) -> (P children :: queue.right_trees, bound)
-      | Single (ConstantSubtree (bound, subtree)) -> (subtree :: queue.right_trees, bound)
-      | Single (IncreasingSubtree (_, subtrees, bound)) -> (List.rev_append subtrees queue.right_trees, bound)
+      let (trees, right_bound) = match group with  
+      | Group (bound, children) -> (DeQueue.push_right queue.trees (P children), bound)
+      | Single (ConstantSubtree (bound, subtree)) -> (DeQueue.push_right queue.trees subtree, bound)
+      | Single (IncreasingSubtree (_, subtrees, bound)) -> (DeQueue.push_all_right queue.trees subtrees, bound)
       in 
-      { queue with right_trees; right_bound }
+      { queue with trees; right_bound }
 
     let enqueue_left group queue = 
-      let (left_trees, left_bound) = match group with 
-      | Group (bound, children) -> (P children :: queue.left_trees, bound)
-      | Single (ConstantSubtree (bound, subtree)) -> (subtree :: queue.left_trees, bound)
-      | Single (IncreasingSubtree (_,subtrees, bound)) -> (List.rev_append subtrees queue.left_trees, bound)
+      let (trees, left_bound) = match group with 
+      | Group (bound, children) -> (DeQueue.push_left (P children) queue.trees, bound)
+      | Single (ConstantSubtree (bound, subtree)) -> (DeQueue.push_left subtree queue.trees, bound)
+      | Single (IncreasingSubtree (_,subtrees, bound)) -> (DeQueue.push_all_left subtrees queue.trees, bound)
       in
-      { queue with left_trees; left_bound }
-
+      { queue with trees; left_bound }
+
+    let finalize queue = 
+      match DeQueue.view_left queue.trees with
+      | Some (single, others) when DeQueue.is_empty others && is_balanced queue ->
+          Balanced (queue.left_bound, single)
+      | _ when is_balanced queue ->
+        Balanced (queue.left_bound, q (DeQueue.to_list queue.trees))
+      | _ ->
+        Skew (queue.left_bound, queue.trees, queue.right_bound)
     
+
     let rec enqueue groups queue = 
       let max_bound = max queue.left_bound queue.right_bound in 
       match groups with 
       | [] -> 
-          CenteredSubtree (compact queue)
+          CenteredSubtree (finalize queue)
       | Group (dist,children) :: groups when dist >= max_bound -> 
           queue 
-          |> compact 
-          |> tree_of_centered_tree 
-          |> (fun tree -> Balanced (dist, P (tree :: children)))
+          |> collapse
+          |> (fun (_,tree) -> Balanced (dist, P (tree :: children)))
           |> init_queue
           |> enqueue groups
       | single :: groups when group_d_min single >= max_bound -> 
           queue 
-          |> compact 
-          |> init_queue
+          |> collapse
+          |> (fun (delta, tree) -> init_queue (Balanced (delta, tree)))
           |> enqueue_right single 
           |> enqueue groups 
       | any :: groups when group_d_min any >= queue.right_bound -> 
@@ -267,24 +276,24 @@ module Make =
         let rights = expand_increasing_sequence right_subtrees in 
         let centered_subtree left_bound trees right_bound = 
           if left_bound = right_bound then 
-            CenteredSubtree (Balanced (left_bound, q trees))
+            CenteredSubtree (Balanced (left_bound, q (DeQueue.to_list trees)))
           else 
             CenteredSubtree (Skew (left_bound, trees, right_bound))
         in 
-        if max(min_center, max_center) <= min (min_left, min_right) then 
+        if max min_center max_center <= min min_left min_right then 
           centered_subtree 
             max_left 
-            (List.rev lefts @ [tree_of_centered_tree s_subtree] @ rights)
+            DeQueue.(lefts @> singleton (tree_of_centered_tree s_subtree) @< rights)
             max_right
         else if min_left >= min_center && max_center <= min_right then 
           centered_subtree
             max_left
-            (List.rev lefts @ contract_centered s_subtree @ rights)
+            DeQueue.(lefts @> of_list (contract_centered s_subtree) @< rights)
             max_right
         else if min_right >= min_center && max_center <= min_left then 
           centered_subtree
             max_right
-            (List.rev rights @ contract_centered s_subtree @ lefts)
+            DeQueue.(rights @> of_list (contract_centered s_subtree) @< lefts)
             max_left
         else NotRepresentable
 
@@ -321,7 +330,6 @@ module Make =
           )
 
 
-
     let dispatch root children =
       match root, classify children with 
       | Leaf x, _ when x = s -> 
@@ -353,9 +361,22 @@ module Make =
       match solve tree with 
       | NotRepresentable -> None 
       | CenteredSubtree (Balanced (_,tree)) -> Some tree 
-      | CenteredSubtree (Skew (_,trees,_)) -> Some (q trees)
+      | CenteredSubtree (Skew (_,trees,_)) -> Some (q (DeQueue.to_list trees))
       | ExternalSubtree (ConstantSubtree (_, tree)) -> Some tree 
       | ExternalSubtree (IncreasingSubtree (_, trees, _)) -> Some (q trees)
 
 
   end
+
+
+let refine_by_distances (type elt) source dist tree = 
+  let module Chain = 
+  struct 
+    type t = elt
+    let s = source
+    let d = dist 
+  end 
+  in
+  let module I = Make(Chain) in 
+  I.insert_chain tree 
+    
diff --git a/lib/pqtree/pqChainInsertion.mli b/lib/pqtree/pqChainInsertion.mli
index f79fb5011d6be5c2e7618f451f746133277dc889..7be1df77f13c0835fb4098935c8e78cc7661e092 100644
--- a/lib/pqtree/pqChainInsertion.mli
+++ b/lib/pqtree/pqChainInsertion.mli
@@ -3,3 +3,5 @@ module Make :
   sig 
     val insert_chain : Chain.t PqTree.t -> Chain.t PqTree.t option
   end
+
+val refine_by_distances : 'elt -> ('elt -> int) -> 'elt PqTree.t -> 'elt PqTree.t option  
diff --git a/lib/pqtree/pqTree.ml b/lib/pqtree/pqTree.ml
index 8f6436c3a72eed5b3beb045a4b709796020468a0..6884682e7f838f3a4589abb228ff3a00657ccaa6 100644
--- a/lib/pqtree/pqTree.ml
+++ b/lib/pqtree/pqTree.ml
@@ -298,10 +298,10 @@ end
 module type CheckPermutationSig = 
   sig
     type elt 
+    val contains_permutation : elt t -> elt list -> bool
     type checker
     val checker : elt t -> checker
     val checks : checker -> elt list -> bool 
-    val contains_permutation : elt t -> elt list -> bool
   end 
 
 
diff --git a/test/unit/chainInsertionTest.ml b/test/unit/chainInsertionTest.ml
new file mode 100644
index 0000000000000000000000000000000000000000..855a86d02c515782417fc816fcc14c8ba527cae6
--- /dev/null
+++ b/test/unit/chainInsertionTest.ml
@@ -0,0 +1,71 @@
+open PqTreeLib
+open PqTree 
+open PqChainInsertion 
+open RobinsonTest 
+
+open IntPqTree 
+
+
+let output result = 
+  result
+  |> Option.map Canonical.canonical
+  |> Option.map to_string
+  |> Option.value ~default:"not an interval"
+  |> print_endline
+
+
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n/2) (P [Leaf 6; Leaf 3])
+  |> output; [%expect{|P[Leaf 3;Leaf 6]|}]
+
+
+
+let tree1 = P [Leaf 5; Leaf 2; Leaf 0; Leaf 1; Leaf 3; Leaf 1; Leaf 4]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n) tree1
+  |> output; [%expect{|P[P[P[P[P[Leaf 0;Leaf 1;Leaf 1];Leaf 2];Leaf 3];Leaf 4];Leaf 5]|}]
+    
+
+let %expect_test _ = 
+  refine_by_distances 0 (fun n -> n/2) tree1 
+  |> output; [%expect{|P[P[P[Leaf 0;Leaf 1;Leaf 1];Leaf 2;Leaf 3];Leaf 4;Leaf 5]|}]
+
+
+
+let tree2 = P [ P [Leaf 5; Leaf 2]; P [Leaf 0; Leaf 1]; P [Leaf 6; Leaf 3]; Leaf 4]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n) tree2
+  |> output; [%expect{|not an interval|}]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n/2) tree2
+  |> output; [%expect{|Q[Leaf 4;Leaf 5;Leaf 2;P[Leaf 0;Leaf 1];Leaf 3;Leaf 6]|}]
+
+
+
+let tree3 = Q [ P [ Leaf 1; Leaf 2; Leaf 3]; P [Leaf 1; Leaf 0; Leaf 1]; P [ Leaf 1; Leaf 2; Leaf 3] ]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n) tree3
+  |> output; [%expect{|Q[Leaf 3;Leaf 2;Leaf 1;P[Leaf 0;Leaf 1;Leaf 1];Leaf 1;Leaf 2;Leaf 3]|}]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n/2) tree3
+  |> output; [%expect{|Q[P[Leaf 2;Leaf 3];Leaf 1;P[Leaf 0;Leaf 1;Leaf 1];Leaf 1;P[Leaf 2;Leaf 3]]|}]
+
+
+
+let tree4 = Q [ Q [Leaf 3; Leaf 6; Leaf 9]; Leaf 0; Q [ Leaf 3; Leaf 4; Leaf 5 ]; Q [ Leaf 6; Leaf 8; Leaf 9]]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n/3) tree4
+  |> output; [%expect{|Q[Leaf 9;Leaf 6;Leaf 3;Leaf 0;Q[Leaf 3;Leaf 4;Leaf 5];Leaf 6;Leaf 8;Leaf 9]|}]
+
+let tree5 = Q [ Q [Leaf 3; Leaf 6; Leaf 9]; Leaf 0; Q [ Leaf 3; Leaf 4; Leaf 5 ]; P [ Leaf 6; Leaf 8; Leaf 9]]
+
+let%expect_test _ = 
+  refine_by_distances 0 (fun n -> n/3) tree5
+  |> output; [%expect{|Q[Leaf 9;Leaf 6;Leaf 3;Leaf 0;Q[Leaf 3;Leaf 4;Leaf 5];P[Leaf 6;Leaf 8];Leaf 9]|}]