diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml
index 132fc124..0bac7a0c 100644
--- a/.github/workflows/doc.yml
+++ b/.github/workflows/doc.yml
@@ -14,7 +14,7 @@ jobs:
 
     steps:
       - name: Checkout code
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
 
       - name: Install sphinx
         run: |
@@ -33,7 +33,7 @@ jobs:
           make doc-build
 
       - name: Save doc artifact
-        uses: actions/upload-artifact@v2
+        uses: actions/upload-artifact@v3
         with:
           name: doc
           path: docs/build
diff --git a/AUTHORS.md b/AUTHORS.md
index 889d23d1..27e703d6 100644
--- a/AUTHORS.md
+++ b/AUTHORS.md
@@ -1,10 +1,12 @@
-ELPI is copyright 2014-2017 by:
+ELPI is copyright 2014-2024 by:
   - Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
   - Enrico Tassi <Enrico.Tassi@inria.fr>
 
-Patricia trees (elpi_ptmap.ml) is copyright by Jean-Christophe Filliatre.
+Patricia trees (elpi_ptmap.ml) and persistent arrays (part of Bl.ml) are
+copyright by Jean-Christophe Filliatre.
 
 We thank the following people for their contributions to ELPI:
   - Cvetan Dunchev
   - Ferruccio Guidi
   - Marco Maggesi
+  - Davide Fissore
diff --git a/ELPI.md b/ELPI.md
index 34dcdac3..eea36fd2 100644
--- a/ELPI.md
+++ b/ELPI.md
@@ -241,10 +241,10 @@ such clause using the `:before` attribute.
 fatal-error Msg :- !, M is "elpi: " ^ Msg, coq-err M.
 ```
 
-The `:after` and `:replace` attributes is also available.
+The `:after`, `:replace` and `:remove` attributes is also available.
 
-The `:replace` attribute cannot be given to a named clause. This is to avoid
-the following ambiguity:
+The `:replace` and `:remove` attribute cannot be given to a named clause.
+This is to avoid the following ambiguity:
 
 ```prolog
 :name "replace-me"
@@ -260,6 +260,16 @@ p 3.
 ```
 Here the order in which replacement is performed would matter.
 
+Both `:replace:` and `:remove` can only apply to rules for the same predicate.
+Example:
+
+```prolog
+:name "this" p 1.
+
+:remove "this" p _. % OK
+:remove "this" q _. % Error
+```
+
 
 ## Conditional compilation
 
diff --git a/src/API.ml b/src/API.ml
index 60fb0229..2490d0c0 100644
--- a/src/API.ml
+++ b/src/API.ml
@@ -1381,6 +1381,7 @@ module Utils = struct
         | Some (`After,x) -> [After x]
         | Some (`Before,x) -> [Before x]
         | Some (`Replace,x) -> [Replace x]
+        | Some (`Remove,x) -> [Remove x]
         | None -> []) in
     [Program.Clause {
       Clause.loc = loc;
diff --git a/src/API.mli b/src/API.mli
index 7da0a5f0..835b453e 100644
--- a/src/API.mli
+++ b/src/API.mli
@@ -1243,7 +1243,7 @@ module Utils : sig
 
   (** Hackish, in particular the output should be a compiled program *)
   val clause_of_term :
-    ?name:string -> ?graft:([`After | `Before | `Replace] * string) ->
+    ?name:string -> ?graft:([`After | `Before | `Replace | `Remove] * string) ->
     depth:int -> Ast.Loc.t -> Data.term -> Ast.program
 
   (** Lifting/restriction/beta (LOW LEVEL, don't use) *)
diff --git a/src/bl.ml b/src/bl.ml
new file mode 100644
index 00000000..1d30191a
--- /dev/null
+++ b/src/bl.ml
@@ -0,0 +1,203 @@
+(* elpi: embedded lambda prolog interpreter                                  *)
+(* license: GNU Lesser General Public License Version 2.1 or later           *)
+(* ------------------------------------------------------------------------- *)
+
+module Array = struct
+  (* Main code taken from OCaml-bazaar, Library General
+     Public License version 2. *)
+  type 'a t = 'a data ref
+
+  and 'a data =
+    | Array of 'a array
+    | Diff of int * 'a * 'a t
+    [@@deriving show]
+  
+  let empty () = ref @@ Array [||]
+
+  let make n v =
+    ref (Array (Array.make n v))
+  
+  let init n f =
+    ref (Array (Array.init n f))
+  
+  (* `reroot t` ensures that `t` becomes an `Array` node.
+      This is written in CPS to avoid any stack overflow. *)
+  let rec rerootk t k = match !t with
+    | Array _ -> k ()
+    | Diff (i, v, t') ->
+        rerootk t' (fun () ->
+            (match !t' with
+       | Array a as n ->
+           let v' = a.(i) in
+           a.(i) <- v;
+           t := n;
+           t' := Diff (i, v', t)
+       | Diff _ -> assert false
+            );
+            k()
+          )
+  
+  let reroot t = rerootk t (fun () -> ())
+
+  let get t i =
+    match !t with
+    | Array a ->
+        a.(i)
+    | Diff _ ->
+        reroot t;
+        (match !t with Array a -> a.(i) | Diff _ -> assert false)
+  
+  let set t i v =
+    reroot t;
+    match !t with
+    | Array a as n ->
+        let old = a.(i) in
+        if old == v then
+    t
+        else (
+    a.(i) <- v;
+    let res = ref n in
+    t := Diff (i, old, res);
+    res
+        )
+    | Diff _ ->
+        assert false
+
+  (* New code, all bugs are mine ;-) *)
+  let extend len t a =
+    let data = reroot t; match ! t with Array x -> x | Diff _ -> assert false in
+    let newdata = Array.make (2*(max 1 len)) a in
+    if len > 0 then
+      Array.blit data 0 newdata 0 len;
+    ref @@ Array newdata
+      
+      
+  let shift_right t i len =
+    let rec shift t j =
+      if j < i then t
+      else shift (set t (j+1) (get t j)) (j-1)
+    in
+      shift t (i+len-1)
+
+  let shift_left t i len =
+    let rec shift t j =
+      if j = len-1 then t
+      else shift (set t j (get t (j+1))) (j + 1)
+    in
+      shift t i
+
+  let rec length t = match !t with Diff(_,_,x) -> length x | Array a -> Array.length a
+
+  let of_list l = ref @@ Array (Array.of_list l)
+end
+
+type 'a t =
+  | BArray of { len : int; data : 'a Array.t }
+  | BCons of 'a * 'a t
+  [@@deriving show]
+
+let empty () = BArray { len = 0; data = Array.empty () }
+
+let extendk len data a k =
+  let newdata = Array.extend len data a in
+  BArray { len = len + 1; data = k newdata }
+let extend len data a = extendk len data a (fun x -> x)
+  
+let cons head tail = BCons(head,tail)
+
+let rec rcons elt l =
+  match l with
+  | BCons(x,xs) -> BCons(x,rcons elt xs)
+  | BArray { len; data } when len < Array.length data -> BArray { len = len + 1; data = Array.set data len elt }
+  | BArray { len; data } -> extend len data elt
+
+let rec replace f x = function
+  | BCons (head,tail) when f head -> BCons(x,tail)
+  | BCons (head, tail) -> BCons (head, replace f x tail)
+  | BArray { len; data } as a ->
+      let rec aux i =
+        if i < len then
+          if f data.(i) then BArray { len; data = Array.set data i x }
+          else aux (i+1)
+        else
+          a
+      in
+        aux 0
+
+let rec remove f = function
+  | BCons (head,tail) when f head -> tail
+  | BCons (head, tail) -> BCons (head, remove f tail)
+  | BArray { len; data } as a ->
+      let rec aux i =
+        if i < len then
+          if f data.(i) then BArray { len = len-1; data = Array.shift_left data i len }
+          else aux (i+1)
+        else 
+          a
+      in
+        aux 0
+
+let rec insert f x = function
+  | BCons (head, tail) when f head > 0 -> BCons (head, BCons(x,tail))
+  | BCons (head, tail) -> BCons (head, insert f x tail)
+  | BArray { len; data } ->
+    let rec aux i =
+      if i < len then
+        if f data.(i) > 0 then
+          if len < Array.length data then begin
+            let data = Array.shift_right data i (len-i) in
+            BArray { len = len + 1; data = Array.set data i x }
+          end else
+            extendk len data x (fun data ->
+              let data = Array.shift_right data i (len-i) in
+              Array.set data i x)
+        else
+          aux (i+1)
+      else
+          if len < Array.length data then begin
+            BArray { len = len + 1; data = Array.set data len x }
+          end else
+            extendk len data x (fun data -> Array.set data len x)
+
+    in
+      aux 0
+          
+type 'a scan = 'a t * int
+let to_scan x = x, 0
+let is_empty (x,n) =
+  match x with
+  | BArray { len } -> len = n
+  | BCons _ -> false
+
+let next (x,n) =
+  match x with
+  | BArray { len; data } -> assert(n < len); data.(n), (x,n+1)
+  | BCons (a,xs) -> a, (xs,n)
+
+(* ocaml >= 4.14
+let[@tail_mod_cons] rec to_list_aux i len data =
+  if i = len then []
+  else data.(i) :: to_list_aux (i+1) len data *)
+
+let rec to_list_aux i len data acc =
+  if i = len then List.rev acc
+  else to_list_aux (i+1) len data (data.(i) :: acc)
+
+let rec to_list = function
+  | BCons(x,xs) -> x :: to_list xs
+  | BArray { len; data } -> to_list_aux 0 len data []
+
+let to_list (x,n) =
+  if n = 0 then to_list x else
+  match x with
+  | BCons _ -> assert false
+  | BArray { len; data } -> to_list_aux n len data []
+
+let of_list l = let data = Array.of_list l in BArray { len = Array.length data; data }, 0
+
+let length (x,i) =
+  let rec aux i = function
+    | BCons (_,l) -> aux (i+1) l
+    | BArray { len } -> i + len
+  in
+  aux (-i) x
diff --git a/src/bl.mli b/src/bl.mli
new file mode 100644
index 00000000..29ff6df5
--- /dev/null
+++ b/src/bl.mli
@@ -0,0 +1,29 @@
+(* elpi: embedded lambda prolog interpreter                                  *)
+(* license: GNU Lesser General Public License Version 2.1 or later           *)
+(* ------------------------------------------------------------------------- *)
+
+(* functional lists with O(1) rcons *)
+
+type 'a t
+val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+val show : (Format.formatter -> 'a -> unit) -> 'a t -> string
+
+val empty : unit -> 'a t
+val cons : 'a -> 'a t -> 'a t
+val rcons : 'a -> 'a t -> 'a t
+
+val replace : ('a -> bool) -> 'a -> 'a t -> 'a t
+val remove : ('a -> bool) -> 'a t -> 'a t
+
+(* [insert f x l] inserts before y in l if f y > 0 *)
+val insert : ('a -> int) -> 'a -> 'a t -> 'a t
+val remove : ('a -> bool) -> 'a t -> 'a t
+
+type 'a scan
+val to_scan : 'a t -> 'a scan
+val is_empty : 'a scan -> bool
+val next : 'a scan -> 'a * 'a scan
+val to_list : 'a scan -> 'a list
+val of_list : 'a list -> 'a scan
+val length : 'a scan -> int
+
diff --git a/src/compiler.ml b/src/compiler.ml
index bda10da5..6fe85fe5 100644
--- a/src/compiler.ml
+++ b/src/compiler.ml
@@ -566,7 +566,9 @@ type program = {
   types : Types.types C.Map.t;
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : (mode * Loc.t) C.Map.t;
-  clauses_rev : (preterm,attribute) Ast.Clause.t list;
+  clauses : (preterm,attribute) Ast.Clause.t list;
+  prolog_program : index;
+  indexing : (mode * indexing) C.Map.t;
   chr : block_constraint list;
   local_names : int;
 
@@ -574,14 +576,18 @@ type program = {
 }
 and attribute = {
   id : string option;
+  timestamp : grafting_time;
+  insertion : Ast.Structured.insertion option;
 }
 [@@deriving show]
 
-let empty = {
+let empty () = {
   types = C.Map.empty;
   type_abbrevs = C.Map.empty;
   modes = C.Map.empty;
-  clauses_rev = [];
+  clauses = [];
+  prolog_program = { idx = Ptmap.empty; time = 0; times = StrMap.empty };
+  indexing = C.Map.empty;
   chr = [];
   local_names = 0;
   toplevel_macros = F.Map.empty;
@@ -609,7 +615,8 @@ type 'a query = {
   types : Types.types C.Map.t;
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : mode C.Map.t;
-  clauses_rev : (preterm,Assembled.attribute) Ast.Clause.t list;
+  clauses : (preterm,Assembled.attribute) Ast.Clause.t list;
+  prolog_program : index;
   chr : block_constraint list;
   initial_depth : int;
   query : preterm;
@@ -649,29 +656,35 @@ end = struct (* {{{ *)
       error ~loc ("illegal attribute " ^ show_raw_attribute a) in
     let illegal_replace s =
       error ~loc ("replacing clause for "^ s ^" cannot have a name attribute") in
-    let rec aux r = function
+    let illegal_remove_id s =
+      error ~loc ("remove clause for "^ s ^" cannot have a name attribute") in
+    let rec aux_attrs r = function
       | [] -> r
       | Name s :: rest ->
          if r.id <> None then duplicate_err "name";
-         aux { r with id = Some s } rest
+         aux_attrs { r with id = Some s } rest
       | After s :: rest ->
          if r.insertion <> None then duplicate_err "insertion";
-         aux { r with insertion = Some (After s) } rest
+         aux_attrs { r with insertion = Some (Insert (After s)) } rest
       | Before s :: rest ->
          if r.insertion <> None then duplicate_err "insertion";
-         aux { r with insertion = Some (Before s) } rest
+         aux_attrs { r with insertion = Some (Insert (Before s)) } rest
       | Replace s :: rest ->
           if r.insertion <> None then duplicate_err "insertion";
-          aux { r with insertion = Some (Replace s) } rest
+          aux_attrs { r with insertion = Some (Replace s) } rest
+      | Remove s :: rest ->
+          if r.insertion <> None then duplicate_err "insertion";
+          aux_attrs { r with insertion = Some (Remove s) } rest
       | If s :: rest ->
          if r.ifexpr <> None then duplicate_err "if";
-         aux { r with ifexpr = Some s } rest
+         aux_attrs { r with ifexpr = Some s } rest
       | (External | Index _) as a :: _-> illegal_err a
     in
-    let attributes = aux { insertion = None; id = None; ifexpr = None } attributes in
+    let attributes = aux_attrs { insertion = None; id = None; ifexpr = None } attributes in
     begin
       match attributes.insertion, attributes.id with
       | Some (Replace x), Some _ -> illegal_replace x
+      | Some (Remove x), Some _ -> illegal_remove_id x
       | _ -> ()
     end;
     { c with Clause.attributes }
@@ -681,28 +694,28 @@ end = struct (* {{{ *)
       error ~loc ("duplicate attribute " ^ s) in
     let illegal_err a =
       error ~loc ("illegal attribute " ^ show_raw_attribute a) in
-    let rec aux r = function
+    let rec aux_chr r = function
       | [] -> r
       | Name s :: rest ->
-         aux { r with cid = s } rest
+         aux_chr { r with cid = s } rest
       | If s :: rest ->
          if r.cifexpr <> None then duplicate_err "if";
-         aux { r with cifexpr = Some s } rest
-      | (Before _ | After _ | Replace _ | External | Index _) as a :: _ -> illegal_err a 
+         aux_chr { r with cifexpr = Some s } rest
+      | (Before _ | After _ | Replace _ | Remove _ | External | Index _) as a :: _ -> illegal_err a 
     in
     let cid = Loc.show loc in 
-    { c with Chr.attributes = aux { cid; cifexpr = None } attributes }
+    { c with Chr.attributes = aux_chr { cid; cifexpr = None } attributes }
 
   let structure_type_attributes { Type.attributes; loc; name; ty } =
     let duplicate_err s =
       error ~loc ("duplicate attribute " ^ s) in
     let illegal_err a =
       error ~loc ("illegal attribute " ^ show_raw_attribute a) in
-    let rec aux r = function
+    let rec aux_tatt r = function
       | [] -> r
       | External :: rest ->
          begin match r with
-           | None -> aux (Some Structured.External) rest
+           | None -> aux_tatt (Some Structured.External) rest
            | Some Structured.External -> duplicate_err "external"
            | Some _ -> error ~loc "external predicates cannot be indexed"
          end
@@ -713,15 +726,15 @@ end = struct (* {{{ *)
            | Some "Map" -> Some Map
            | Some "Hash" -> Some HashMap
            | Some "DTree" -> Some DiscriminationTree
-           | Some s -> error ~loc ("unknown indexing directive " ^ s) in
+           | Some s -> error ~loc ("unknown indexing directive " ^ s ^ ". Valid ones are: Map, Hash, DTree.") in
          begin match r with
-           | None -> aux (Some (Structured.Index(i,it))) rest
+           | None -> aux_tatt (Some (Structured.Index(i,it))) rest
            | Some (Structured.Index _) -> duplicate_err "index"
            | Some _ -> error ~loc "external predicates cannot be indexed"
          end
-      | (Before _ | After _ | Replace _ | Name _ | If _) as a :: _ -> illegal_err a 
+      | (Before _ | After _ | Replace _ | Remove _ | Name _ | If _) as a :: _ -> illegal_err a 
     in
-    let attributes = aux None attributes in
+    let attributes = aux_tatt None attributes in
     let attributes =
       match attributes with
       | None -> Structured.Index([1],None)
@@ -730,9 +743,9 @@ end = struct (* {{{ *)
 
 
   let run _ dl =
-    let rec aux ns blocks clauses macros types tabbrs modes locals chr accs = function
+    let rec aux_run ns blocks clauses macros types tabbrs modes locals chr accs = function
       | Program.Ignored _ :: rest ->
-          aux ns blocks clauses macros types tabbrs modes locals chr accs rest
+          aux_run ns blocks clauses macros types tabbrs modes locals chr accs rest
       | (Program.End _ :: _ | []) as rest ->
           { body = List.rev (cl2b clauses @ blocks);
             types = List.rev types;
@@ -743,7 +756,7 @@ end = struct (* {{{ *)
           List.rev chr,
           rest
       | Program.Begin loc :: rest ->
-          let p, locals1, chr1, rest = aux ns [] [] [] [] [] [] [] [] accs rest in
+          let p, locals1, chr1, rest = aux_run ns [] [] [] [] [] [] [] [] accs rest in
           if chr1 <> [] then
             error "CHR cannot be declared inside an anonymous block";
           aux_end_block loc ns (Locals(locals1,p) :: cl2b clauses @ blocks)
@@ -751,13 +764,13 @@ end = struct (* {{{ *)
       | Program.Constraint (loc, ctx_filter, clique) :: rest ->
           if chr <> [] then
             error "Constraint blocks cannot be nested";
-          let p, locals1, chr, rest = aux ns [] [] [] [] [] [] [] [] accs rest in
+          let p, locals1, chr, rest = aux_run ns [] [] [] [] [] [] [] [] accs rest in
           if locals1 <> [] then
             error "locals cannot be declared inside a Constraint block";
           aux_end_block loc ns (Constraints({ctx_filter;clique;rules=chr},p) :: cl2b clauses @ blocks)
             [] macros types tabbrs modes locals [] accs rest
       | Program.Namespace (loc, n) :: rest ->
-          let p, locals1, chr1, rest = aux (n::ns) [] [] [] [] [] [] [] [] StrSet.empty rest in
+          let p, locals1, chr1, rest = aux_run (n::ns) [] [] [] [] [] [] [] [] StrSet.empty rest in
           if chr1 <> [] then
             error "CHR cannot be declared inside a namespace block";
           if locals1 <> [] then
@@ -769,60 +782,60 @@ end = struct (* {{{ *)
       | Program.Shorten (loc,directives) :: rest ->
           let shorthand (full_name,short_name) = { iloc = loc; full_name; short_name } in
           let shorthands = List.map shorthand directives in
-          let p, locals1, chr1, rest = aux ns [] [] [] [] [] [] [] [] accs rest in
+          let p, locals1, chr1, rest = aux_run ns [] [] [] [] [] [] [] [] accs rest in
           if locals1 <> [] then
             error "locals cannot be declared after a shorthand";
           if chr1 <> [] then
             error "CHR cannot be declared after a shorthand";
-          aux ns ((Shorten(shorthands,p) :: cl2b clauses @ blocks))
+          aux_run ns ((Shorten(shorthands,p) :: cl2b clauses @ blocks))
             [] macros types tabbrs modes locals chr accs rest
 
       | Program.Accumulated (_,[]) :: rest ->
-          aux ns blocks clauses macros types tabbrs modes locals chr accs rest
+          aux_run ns blocks clauses macros types tabbrs modes locals chr accs rest
 
       | Program.Accumulated (loc,(digest,a) :: more) :: rest ->
           let rest = Program.Accumulated (loc, more) :: rest in
           let digest = String.concat "." (digest :: List.map F.show ns) in
           if StrSet.mem digest accs then
-            aux ns blocks clauses macros types tabbrs modes locals chr accs rest
+            aux_run ns blocks clauses macros types tabbrs modes locals chr accs rest
           else
-            aux ns blocks clauses macros types tabbrs modes locals chr
+            aux_run ns blocks clauses macros types tabbrs modes locals chr
               (StrSet.add digest accs)
               (Program.Begin loc :: a @ Program.End loc :: rest)
 
       | Program.Clause c :: rest ->
           let c = structure_clause_attributes c in
-          aux ns blocks (c::clauses) macros types tabbrs modes locals chr accs rest
+          aux_run ns blocks (c::clauses) macros types tabbrs modes locals chr accs rest
       | Program.Macro m :: rest ->
-          aux ns blocks clauses (m::macros) types tabbrs modes locals chr accs rest
+          aux_run ns blocks clauses (m::macros) types tabbrs modes locals chr accs rest
       | Program.Pred (t,m) :: rest ->
-          aux ns blocks clauses macros types tabbrs modes locals chr accs
+          aux_run ns blocks clauses macros types tabbrs modes locals chr accs
             (Program.Mode [m] :: Program.Type [t] :: rest)
       | Program.Mode ms :: rest ->
-          aux ns blocks clauses macros types tabbrs (ms @ modes) locals chr accs rest
+          aux_run ns blocks clauses macros types tabbrs (ms @ modes) locals chr accs rest
       | Program.Type [] :: rest ->
-          aux ns blocks clauses macros types tabbrs modes locals chr accs rest
+          aux_run ns blocks clauses macros types tabbrs modes locals chr accs rest
       | Program.Type (t::ts) :: rest ->
           let t = structure_type_attributes t in
           let types = if List.mem t types then types else t :: types in
-          aux ns blocks clauses macros types tabbrs modes locals chr accs
+          aux_run ns blocks clauses macros types tabbrs modes locals chr accs
             (Program.Type ts :: rest)
       | Program.TypeAbbreviation abbr :: rest ->
-          aux ns blocks clauses macros types (abbr :: tabbrs) modes locals chr accs rest
+          aux_run ns blocks clauses macros types (abbr :: tabbrs) modes locals chr accs rest
       | Program.Local l :: rest ->
-          aux ns blocks clauses macros types tabbrs modes (l@locals) chr accs rest
+          aux_run ns blocks clauses macros types tabbrs modes (l@locals) chr accs rest
       | Program.Chr r :: rest ->
           let r = structure_chr_attributes r in
-          aux ns blocks clauses macros types tabbrs modes locals (r::chr) accs rest
+          aux_run ns blocks clauses macros types tabbrs modes locals (r::chr) accs rest
 
     and aux_end_block loc ns blocks clauses macros types tabbrs modes locals chr accs rest =
       match rest with
       | Program.End _ :: rest ->
-          aux ns blocks clauses macros types tabbrs modes locals chr accs rest
+          aux_run ns blocks clauses macros types tabbrs modes locals chr accs rest
       | _ -> error ~loc "matching } is missing"
 
     in
-    let blocks, locals, chr, rest = aux [] [] [] [] [] [] [] [] [] StrSet.empty dl in
+    let blocks, locals, chr, rest = aux_run [] [] [] [] [] [] [] [] [] StrSet.empty dl in
     begin match rest with
     | [] -> ()
     | Program.End loc :: _ -> error ~loc "extra }"
@@ -1531,42 +1544,42 @@ end = struct (* {{{ *)
      builtins since it is (also) used to apply a compilation unit relocation *)
 
   let smart_map_term ?(on_type=false) state f t =
-    let rec aux = function
+    let rec aux_sm = function
       | Const c ->
           let c1 = f c in
           if not on_type && Builtins.is_declared state c1 then Builtin(c1,[])
           else Symbols.get_canonical state c1
       | Lam t as x ->
-          let t1 = aux t in
+          let t1 = aux_sm t in
           if t == t1 then x else Lam t1
       | AppArg(i,ts) as x ->
-          let ts1 = smart_map aux ts in
+          let ts1 = smart_map aux_sm ts in
           if ts == ts1 then x else AppArg(i,ts1)
       | AppUVar(r,lvl,ts) as x ->
           assert(!!r == D.dummy);
-          let ts1 = smart_map aux ts in
+          let ts1 = smart_map aux_sm ts in
           if ts == ts1 then x else AppUVar(r,lvl,ts1)
       | Builtin(c,ts) ->
           let c1 = f c in
-          let ts1 = smart_map aux ts in
+          let ts1 = smart_map aux_sm ts in
           if not on_type && Builtins.is_declared state c1 then Builtin(c,ts1)
           else if ts1 = [] then Symbols.get_canonical state c1 else App(c,List.hd ts1,List.tl ts1)
       | App(c,t,ts) ->
           let c1 = f c in
-          let t1 = aux t in
-          let ts1 = smart_map aux ts in
+          let t1 = aux_sm t in
+          let ts1 = smart_map aux_sm ts in
           if not on_type && Builtins.is_declared state c1 then Builtin (c1,t1 :: ts1)
           else App(c1,t1,ts1)
       | Cons(hd,tl) as x ->
-          let hd1 = aux hd in
-          let tl1 = aux tl in
+          let hd1 = aux_sm hd in
+          let tl1 = aux_sm tl in
           if hd == hd1 && tl == tl1 then x else Cons(hd1,tl1)
       | UVar(r,_,_) as x ->
           assert(!!r == D.dummy);
           x
       | (Arg _ | CData _ | Nil | Discard) as x -> x
     in
-      aux t
+      aux_sm t
 
 let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
   let c2i = Constants.Map.fold (fun k v m -> Constants.Map.add (f k) v m) c2i Constants.Map.empty in
@@ -1788,16 +1801,16 @@ end = struct (* {{{ *)
 
   let missing_args_of state loc modes types t =
     let c, args =
-      let rec aux = function
-        | App (c,_,[x]) when c == D.Global_symbols.implc -> aux x
+      let rec aux_mia = function
+        | App (c,_,[x]) when c == D.Global_symbols.implc -> aux_mia x
         | App (c,x,xs) when c == D.Global_symbols.andc ->
-            aux List.(hd (rev (x :: xs)))
+            aux_mia List.(hd (rev (x :: xs)))
         | App (c,x,xs) -> c, x :: xs
         | Const c -> c, []
         | Builtin(c,args) -> c, args
         | _ -> error ~loc "Only applications can be spilled"
       in
-        aux t in
+        aux_mia t in
     let ty = type_of_const types c in
     let ty_mode, mode =
       match modes c with
@@ -1810,8 +1823,8 @@ end = struct (* {{{ *)
       | `Arrow(arity,_),_ ->
           let missing = arity - nargs in
           let output_suffix =
-            let rec aux = function Output :: l -> 1 + aux l | _ -> 0 in
-            aux (List.rev mode) in
+            let rec aux_output = function Output :: l -> 1 + aux_output l | _ -> 0 in
+            aux_output (List.rev mode) in
           if missing > output_suffix then
             error ~loc Printf.(sprintf
               "Cannot spill %s: only %d out of %d missing arguments are output"
@@ -1851,14 +1864,14 @@ end = struct (* {{{ *)
 
     let mkSpilled =
       let spilled = ref 0 in
-      let rec aux vars n =
+      let rec aux_mks vars n =
         if n == 0 then []
         else begin
           incr spilled;
           mkApp (mk_Arg ("Spilled_" ^ string_of_int !spilled)) vars ::
-            aux vars (n-1)
+            aux_mks vars (n-1)
         end in
-      fun vars n -> List.rev (aux vars n) in
+      fun vars n -> List.rev (aux_mks vars n) in
 
     let mkAppSpilled fcall args =
       let rec on_last f = function
@@ -1866,14 +1879,14 @@ end = struct (* {{{ *)
         | [x] -> [f x]
         | x::xs -> x :: on_last f xs
       in
-      let rec aux = function
+      let rec aux_mka = function
         | App(c,x,[y]) when c == D.Global_symbols.implc ->
-            mkAppC c [x;aux y]
+            mkAppC c [x;aux_mka y]
         | App (c,x,xs) when c == D.Global_symbols.andc ->
-            mkAppC c (on_last aux (x::xs))
+            mkAppC c (on_last aux_mka (x::xs))
         | t -> mkApp t args
       in
-        aux fcall in
+        aux_mka fcall in
 
     let equal_term c = function
       | Const d -> c == d
@@ -1938,20 +1951,20 @@ end = struct (* {{{ *)
          let args = x :: xs in
          let spills, args, is_prop =
            let (@@@) (s1,a1) (s2,a2,b) = s1 @ s2, a1 @ a2, b in
-           let rec aux ty args = match ty, args with
+           let rec aux_spaux ty args = match ty, args with
              | (`Variadic(_,`Prop) | `Arrow([],`Prop)), [] -> [],[],true
              | _, [] -> [],[],false
              | `Variadic(`Prop,_), a1 :: an ->
-                   ([],spaux1_prop ctx a1) @@@ aux ty an
+                   ([],spaux1_prop ctx a1) @@@ aux_spaux ty an
              | `Arrow(`Prop :: ty,c), a1 :: an ->
-                   ([],spaux1_prop ctx a1) @@@ aux (`Arrow(ty,c)) an
+                   ([],spaux1_prop ctx a1) @@@ aux_spaux (`Arrow(ty,c)) an
              | `Arrow((_ :: _ as ty),c), a1 :: an ->
                    let spills, a1 = spaux ctx a1 in
                    let ty = drop (size_outermost_spill spills ~default:1) ty in
-                   (spills, a1) @@@ aux (`Arrow(ty,c)) an
-             | _, a1 :: an -> spaux ctx a1 @@@ aux ty an
+                   (spills, a1) @@@ aux_spaux (`Arrow(ty,c)) an
+             | _, a1 :: an -> spaux ctx a1 @@@ aux_spaux ty an
            in
-             aux (type_of_const types hd) args in
+             aux_spaux (type_of_const types hd) args in
          if is_prop then [], [add_spilled spills (mkAppC hd args)]
          else spills, [mkAppC hd args]
       | (CData _ | Const _ | Discard | Nil) as x -> [],[x]
@@ -2027,6 +2040,45 @@ end = struct (* {{{ *)
 
 end (* }}} *)
 
+
+
+let stack_term_of_preterm ~depth:arg_lvl state { term = t; amap = { c2i } } =
+  let state = ref state in
+  let get_global_or_allocate_bound_symbol n =
+    let s, t = Symbols.get_global_or_allocate_bound_symbol !state n in
+    state := s;
+    t in
+  let rec stack_term_of_preterm = function
+    | Const c when C.Map.mem c c2i ->
+        let argno = C.Map.find c c2i in
+        R.mkAppArg argno arg_lvl []
+    | Const c -> get_global_or_allocate_bound_symbol c
+    | App(c, x, xs) when C.Map.mem c c2i ->
+        let argno = C.Map.find c c2i in
+        R.mkAppArg argno arg_lvl (List.map stack_term_of_preterm (x::xs))
+    | App(c, x, xs) as app ->
+        let x1 = stack_term_of_preterm x in
+        let xs1 = smart_map stack_term_of_preterm xs in
+        if x1 == x && xs1 == xs then app else App(c, x1, xs1)
+    | Lam t as x ->
+        let t1 = stack_term_of_preterm  t in
+        if t1 == t then x else Lam t1
+    | CData _ as x -> x
+    | Builtin(c, args) as x ->
+        let args1 = smart_map stack_term_of_preterm args in
+        if args1 == args then x else Builtin(c, args1)
+    | UVar _ | AppUVar _ | Arg _ | AppArg _ -> anomaly "preterm containing a variable"
+    | Nil as x -> x
+    | Discard as x -> x
+    | Cons(hd, tl) as x ->
+        let hd1 = stack_term_of_preterm hd in
+        let tl1 = stack_term_of_preterm tl in
+        if hd == hd1 && tl == tl1 then x else Cons(hd1,tl1)
+  in
+  let t = stack_term_of_preterm t in
+  !state, t
+;;
+
 (* This is marshalable *)
 
 module Assemble : sig
@@ -2035,46 +2087,8 @@ module Assemble : sig
 
 end = struct (* {{{ *)
 
-  let sort_insertion ~old_rev ~extra:l =
-    let add s { Ast.Clause.attributes = { Assembled.id }; loc } =
-      match id with
-      | None -> s
-      | Some n ->
-          if StrMap.mem n s then
-            error ~loc ("a clause named " ^ n ^
-                   " already exists at " ^ Loc.show (StrMap.find n s))
-          else
-            StrMap.add n loc s in
-    let compile_clause ({ Ast.Clause.attributes = { Ast.Structured.id }} as c) =
-      { c with Ast.Clause.attributes = { Assembled.id }}
-    in
-    let rec insert loc_name c l =
-      match l, loc_name with
-      | [],_ -> error ~loc:c.Ast.Clause.loc ("unable to graft this clause: no clause named " ^
-             match loc_name with
-             | Ast.Structured.Replace x -> x
-             | Ast.Structured.After x -> x
-             | Ast.Structured.Before x -> x)
-      | { Ast.Clause.attributes = { Assembled.id = Some n }} :: xs,
-        Ast.Structured.Replace name when n = name ->
-           c :: xs
-      | { Ast.Clause.attributes = { Assembled.id = Some n }} as x :: xs,
-        Ast.Structured.After name when n = name ->
-           c :: x :: xs
-      | { Ast.Clause.attributes = { Assembled.id = Some n }} as x :: xs,
-        Ast.Structured.Before name when n = name ->
-           x :: c :: xs
-      | x :: xs, _ -> x :: insert loc_name c xs in
-    let rec aux seen acc = function
-      | [] -> acc
-      | { Ast.Clause.attributes = { Ast.Structured.insertion = Some i }} as x :: xs ->
-          let x = compile_clause x in
-          aux (add seen x) (insert i x acc) xs
-      | x :: xs ->
-          let x = compile_clause x in
-          aux (add seen x) (x :: acc) xs
-    in
-    aux StrMap.empty old_rev l
+let compile_clause_attributes ({ Ast.Clause.attributes = { Ast.Structured.id }} as c) timestamp insertion =
+  { c with Ast.Clause.attributes = { Assembled.id; timestamp; insertion }}
 
   (* let shift_pp fmt ({ Data.Constants.c2s},s,{ Data.Constants.c2s = c2s2 }) =
     Format.fprintf fmt "{{ @[<hov 2>";
@@ -2082,12 +2096,84 @@ end = struct (* {{{ *)
       Format.fprintf fmt "(%s)%a ->@ (%s)%a;@ "
         (Hashtbl.find c2s k) Int.pp k (Hashtbl.find c2s2 v) Int.pp v) s;
     Format.fprintf fmt "@] }}" *)
-  let clause_name { Ast.Clause.attributes = { Ast.Structured.ifexpr } } = ifexpr
+  let clause_ifexpr { Ast.Clause.attributes = { Ast.Structured.ifexpr } } = ifexpr
+
+  let chose_indexing state predicate l k =
+    let all_zero = List.for_all ((=) 0) in
+    let rec check_map default argno = function
+      (* TODO: @FissoreD here we should raise an error if n > arity of the predicate? *)
+      | [] -> error ("Wrong indexing for " ^ Symbols.show state predicate ^ ": no argument selected.")
+      | 0 :: l -> check_map default (argno+1) l
+      | 1 :: l when all_zero l -> MapOn argno
+      | _ -> default ()
+    in
+    match k with
+    | Some Ast.Structured.DiscriminationTree -> DiscriminationTree l
+    | Some HashMap -> Hash l
+    | None -> check_map (fun () -> DiscriminationTree l) 0 l
+    | Some Map -> check_map (fun () ->
+        error ("Wrong indexing for " ^ Symbols.show state predicate ^
+                ": Map indexes exactly one argument at depth 1")) 0 l
+  
+  let update_indexing state index modes types old_idx =
+    let check_if_some_clauses_already_in ~loc predicate =
+      if Ptmap.mem predicate index then
+         error ~loc @@ "Some clauses for " ^ Symbols.show state predicate ^
+           " are already in the program, changing the indexing a posteriori is not allowed."
+      in  
+    let add_indexing_for ~loc name tindex map =
+      let mode = try fst @@ C.Map.find name modes with Not_found -> [] in
+      let declare_index, index =
+        match tindex with
+        | Some (Ast.Structured.Index(l,k)) -> true, chose_indexing state name l k
+        | _ -> false, chose_indexing state name [1] None in
+      try
+        let _, old_tindex =
+          try C.Map.find name map
+          with Not_found -> C.Map.find name old_idx in
+        if old_tindex <> index then
+          if old_tindex <> MapOn 1 && declare_index then
+            error ~loc ("multiple and inconsistent indexing attributes for " ^
+                      Symbols.show state name)
+          else
+            if declare_index then begin
+              check_if_some_clauses_already_in ~loc name;
+              C.Map.add name (mode,index) map
+            end else map
+        else
+          map
+      with Not_found ->
+        check_if_some_clauses_already_in ~loc name;
+        C.Map.add name (mode,index) map in
+        
+    let map = C.Map.fold (fun tname l acc -> Types.fold (fun acc { Types.tindex; decl = { tloc } } -> add_indexing_for ~loc:tloc tname (Some tindex) acc) acc l) types C.Map.empty in
+    let map = C.Map.fold (fun k (_,loc) m -> add_indexing_for ~loc k None m) modes map in
+    map, C.Map.union (fun _ _ _ -> assert false) map old_idx
+     
+let compile_clause modes initial_depth (state, index, clauses)
+    ({ Ast.Clause.body = ({ amap = { nargs }} as body); loc; attributes } as c)
+  =
+  let state, body = stack_term_of_preterm ~depth:0 state body in
+  let modes x = try fst @@ C.Map.find x modes with Not_found -> [] in
+  let name = attributes.Ast.Structured.id in
+  let (p,cl), _, morelcs =
+    try R.CompileTime.clausify1 ~loc ~modes ~nargs ~depth:initial_depth body
+    with D.CannotDeclareClauseForBuiltin(loc,c) ->
+      error ?loc ("Declaring a clause for built in predicate " ^ Symbols.show state c)
+    in
+  if morelcs <> 0 then error ~loc "sigma in a toplevel clause is not supported";
+  let graft = attributes.Ast.Structured.insertion in
+   (* Printf.eprintf "adding clause from %s %s\n" (Loc.show loc) (Option.fold ~none:"" ~some:String.show name);  *)
+  let index = R.CompileTime.add_to_index ~depth:initial_depth ~predicate:p ~graft cl name index in
+  state, index, (compile_clause_attributes c cl.timestamp graft) :: clauses
+
 
 let assemble flags state code  (ul : compilation_unit list) =
 
-  let state, clauses_rev, types, type_abbrevs, modes, chr_rev =
-    List.fold_left (fun (state, cl1, t1, ta1, m1, c1) ({ symbol_table; code }  as _u) ->
+  let local_names = code.Assembled.local_names in
+
+  let state, index, indexing, clauses, types, type_abbrevs, modes, chr_rev =
+    List.fold_left (fun (state, index, idx1, clauses, t1, ta1, m1, c1) ({ symbol_table; code }  as _u) ->
       let state, { Flat.clauses = cl2; types = t2; type_abbrevs = ta2; modes = m2; chr = c2; } =
         let state, shift = Stdlib.Result.get_ok @@ Symbols.build_shift ~flags ~base:state symbol_table in
         let code =
@@ -2097,18 +2183,28 @@ let assemble flags state code  (ul : compilation_unit list) =
       let modes = ToDBL.merge_modes state m1 m2 in
       let type_abbrevs = ToDBL.merge_type_abbrevs state ta1 ta2 in
       let types = ToDBL.merge_types state t1 t2 in
-      let cl2 = filter_if flags clause_name cl2 in
+
+      (* no mode discrepancy tested by merge_modes/types *)
+      let new_indexing, idx2 = update_indexing state index.idx m2 t2 idx1 in
+
+      let index = R.CompileTime.update_indexing new_indexing index in
+
+      let cl2 = filter_if flags clause_ifexpr cl2 in
       let cl2 = List.map (Spill.spill_clause state ~types ~modes:(fun c -> fst @@ C.Map.find c modes)) cl2 in
       let c2 = List.map (Spill.spill_chr state ~types ~modes:(fun c -> fst @@ C.Map.find c modes)) c2 in
-      state, cl2 :: cl1, types, type_abbrevs, modes, c2 :: c1
-    ) (state, [], code.Assembled.types, code.Assembled.type_abbrevs, code.Assembled.modes, []) ul in
-  let clauses = List.concat (List.rev clauses_rev) in
-  let clauses_rev = sort_insertion ~old_rev:code.clauses_rev ~extra:clauses in
+  
+      let state, index,clauses =
+        List.fold_left (compile_clause modes local_names) (state,index,clauses) cl2 in
+      
+      state, index, idx2, clauses, types, type_abbrevs, modes, c2 :: c1
+    ) (state, code.Assembled.prolog_program, code.Assembled.indexing, code.clauses, code.Assembled.types, code.Assembled.type_abbrevs, code.Assembled.modes, []) ul in
+  let prolog_program = index in
+
   let chr = List.concat (code.Assembled.chr :: List.rev chr_rev) in
   let chr =
     let pifexpr { pifexpr } = pifexpr in
     List.map (fun {ctx_filter;clique;rules} -> {ctx_filter;clique;rules=filter_if flags pifexpr rules}) chr in
-  state, { Assembled.clauses_rev; types; type_abbrevs; modes; chr; local_names = code.Assembled.local_names; toplevel_macros = code.Assembled.toplevel_macros }
+  state, { Assembled.clauses; indexing; prolog_program; types; type_abbrevs; modes; chr; local_names = code.Assembled.local_names; toplevel_macros = code.Assembled.toplevel_macros }
 
 end (* }}} *)
 
@@ -2139,7 +2235,7 @@ let rec constants_of acc = function
 let w_symbol_table s f x =
   let table = Symbols.compile_table @@ State.get Symbols.table s in
   let pp_ctx = { table; uv_names = ref (IntMap.empty,0) } in
-  Util.set_spaghetti_printer Data.pp_const (R.Pp.pp_constant ~pp_ctx);
+  Util.set_spaghetti_printer pp_const (R.Pp.pp_constant ~pp_ctx);
   f x
 
 (* Compiler passes *)
@@ -2231,7 +2327,7 @@ let assemble_units ~flags ~header:(s,h,toplevel_macros) units : program =
   if nunits_with_locals > 0 then
     error "Only 1 compilation unit is supported when local directives are used";
 
-  let init = { Assembled.empty with toplevel_macros; local_names = h.code.local_names } in
+  let init = { (Assembled.empty ()) with toplevel_macros; local_names = h.code.local_names } in
 
   let s, p = Assemble.assemble flags s init (h :: units) in
 
@@ -2282,42 +2378,6 @@ let check_no_regular_types_for_builtins state types =
             Symbols.show state tname ^ " must be flagged as external");
  )) types
 
-let stack_term_of_preterm ~depth:arg_lvl state { term = t; amap = { c2i } } =
-  let state = ref state in
-  let get_global_or_allocate_bound_symbol n =
-    let s, t = Symbols.get_global_or_allocate_bound_symbol !state n in
-    state := s;
-    t in
-  let rec stack_term_of_preterm = function
-    | Const c when C.Map.mem c c2i ->
-        let argno = C.Map.find c c2i in
-        R.mkAppArg argno arg_lvl []
-    | Const c -> get_global_or_allocate_bound_symbol c
-    | App(c, x, xs) when C.Map.mem c c2i ->
-        let argno = C.Map.find c c2i in
-        R.mkAppArg argno arg_lvl (List.map stack_term_of_preterm (x::xs))
-    | App(c, x, xs) as app ->
-        let x1 = stack_term_of_preterm x in
-        let xs1 = smart_map stack_term_of_preterm xs in
-        if x1 == x && xs1 == xs then app else App(c, x1, xs1)
-    | Lam t as x ->
-        let t1 = stack_term_of_preterm  t in
-        if t1 == t then x else Lam t1
-    | CData _ as x -> x
-    | Builtin(c, args) as x ->
-        let args1 = smart_map stack_term_of_preterm args in
-        if args1 == args then x else Builtin(c, args1)
-    | UVar _ | AppUVar _ | Arg _ | AppArg _ -> anomaly "preterm containing a variable"
-    | Nil as x -> x
-    | Discard as x -> x
-    | Cons(hd, tl) as x ->
-        let hd1 = stack_term_of_preterm hd in
-        let tl1 = stack_term_of_preterm tl in
-        if hd == hd1 && tl == tl1 then x else Cons(hd1,tl1)
-  in
-  let t = stack_term_of_preterm t in
-  !state, t
-;;
 
 let uvbodies_of_assignments assignments =
   (* Clients may add spurious args that, not occurring in the query,
@@ -2334,7 +2394,7 @@ let query_of_ast (compiler_state, assembled_program) t state_update =
   let initial_depth = assembled_program.Assembled.local_names in
   let types = assembled_program.Assembled.types in
   let type_abbrevs = assembled_program.Assembled.type_abbrevs in
-  let modes = C.Map.map fst assembled_program.Assembled.modes in
+  let modes = C.Map.map fst @@ assembled_program.Assembled.modes in
   let active_macros = assembled_program.Assembled.toplevel_macros in
   let state, query =
     ToDBL.query_preterm_of_ast ~depth:initial_depth active_macros compiler_state t in
@@ -2349,7 +2409,8 @@ let query_of_ast (compiler_state, assembled_program) t state_update =
     WithMain.types;
     modes;
     type_abbrevs;
-    clauses_rev = assembled_program.Assembled.clauses_rev;
+    prolog_program = assembled_program.Assembled.prolog_program;
+    clauses = assembled_program.Assembled.clauses;
     chr = assembled_program.Assembled.chr;
     initial_depth;
     query;
@@ -2380,7 +2441,8 @@ let query_of_term (compiler_state, assembled_program) f =
     WithMain.types;
     type_abbrevs;
     modes;
-    clauses_rev = assembled_program.Assembled.clauses_rev;
+    prolog_program = assembled_program.Assembled.prolog_program;
+    clauses = assembled_program.Assembled.clauses;
     chr = assembled_program.Assembled.chr;
     initial_depth;
     query;
@@ -2445,34 +2507,7 @@ let compile_chr depth state
       }
 ;;
 
-let compile_clause modes initial_depth state
-    { Ast.Clause.body = ({ amap = { nargs }} as body); loc }
-=
-  let state, body = stack_term_of_preterm ~depth:0 state body in
-  let cl, _, morelcs =
-    try R.clausify1 ~loc modes ~nargs ~depth:initial_depth body
-    with D.CannotDeclareClauseForBuiltin(loc,c) ->
-      error ?loc ("Declaring a clause for built in predicate " ^ Symbols.show state c)
-    in
-  if morelcs <> 0 then error ~loc "sigma in a toplevel clause is not supported";
-  state, cl
-
-let chose_indexing state predicate l k =
-  let all_zero = List.for_all ((=) 0) in
-  let rec check_map default argno = function
-    (* TODO: @FissoreD here we should raise an error if n > arity of the predicate? *)
-    | [] -> error ("Wrong indexing for " ^ Symbols.show state predicate ^ ": no argument selected.")
-    | 0 :: l -> check_map default (argno+1) l
-    | 1 :: l when all_zero l -> MapOn argno
-    | _ -> default ()
-  in
-  match k with
-  | Some Ast.Structured.DiscriminationTree -> DiscriminationTree l
-  | Some HashMap -> Hash l
-  | None -> check_map (fun () -> DiscriminationTree l) 0 l
-  | Some Map -> check_map (fun () ->
-      error ("Wrong indexing for " ^ Symbols.show state predicate ^
-             ": Map indexes exactly one argument at depth 1")) 0 l
+
 
 let check_rule_pattern_in_clique state clique { D.CHR.pattern; rule_name } =
   try
@@ -2486,7 +2521,8 @@ let run
   {
     WithMain.types;
     modes;
-    clauses_rev;
+    clauses = _;
+    prolog_program;
     chr;
     initial_depth;
     initial_goal;
@@ -2505,32 +2541,6 @@ let run
       List.iter (check_rule_pattern_in_clique state clique) rules;
       state, List.fold_left (fun x y -> CHR.add_rule clique y x) chr rules)
     (state, CHR.empty) chr in
-  let indexing =
-    let add_indexing_for name tindex map =
-      let mode = try C.Map.find name modes with Not_found -> [] in
-      let declare_index, index =
-        match tindex with
-        | Some (Ast.Structured.Index(l,k)) -> true, chose_indexing state name l k
-        | _ -> false, chose_indexing state name [1] None in
-      try
-        let _, old_tindex = C.Map.find name map in
-        if old_tindex <> index then
-          if old_tindex <> MapOn 1 && declare_index then
-            error ("multiple and inconsistent indexing attributes for " ^
-                      Symbols.show state name)
-          else
-            if declare_index then C.Map.add name (mode,index) map
-            else map
-        else
-          map
-      with Not_found ->
-        C.Map.add name (mode,index) map in
-    let map = C.Map.fold (fun tname l acc -> Types.fold (fun acc { Types.tindex } -> add_indexing_for tname (Some tindex) acc) acc l) types C.Map.empty in
-    let map = C.Map.fold (fun k _ m -> add_indexing_for k None m) modes map in
-    map in
-  let state, clauses_rev =
-    map_acc (compile_clause modes initial_depth) state clauses_rev in
-  let prolog_program = R.make_index ~depth:initial_depth ~indexing ~clauses_rev in
   let compiler_symbol_table = State.get Symbols.table state in
   let builtins = Hashtbl.create 17 in
   let pred_list = (State.get Builtins.builtins state).code in
@@ -2541,7 +2551,7 @@ let run
     pred_list;
   let symbol_table = Symbols.compile_table compiler_symbol_table in
   {
-    D.compiled_program = prolog_program;
+    D.compiled_program = { index = close_index prolog_program; src = [] };
     chr;
     initial_depth;
     initial_goal;
@@ -2556,21 +2566,35 @@ end (* }}} *)
 
 let optimize_query = Compiler.run
 
+let removals l =
+  l |> List.filter_map (fun c -> match c.Ast.Clause.attributes.Assembled.insertion with Some (Remove x) -> Some x | Some (Replace x) -> Some x| _ -> None)
+
+let handle_clause_graftin clauses =
+  let clauses = clauses |> List.sort (fun c1 c2 -> R.lex_insertion c1.Ast.Clause.attributes.Assembled.timestamp c2.Ast.Clause.attributes.Assembled.timestamp) in
+  let removals = removals clauses in
+  let clauses = clauses |> List.filter (fun c -> let id = c.Ast.Clause.attributes.Assembled.id in id = None || not(List.exists (fun x -> id = Some x) removals)) in
+  let clauses = clauses |> List.filter (fun c -> match c.Ast.Clause.attributes.Assembled.insertion with Some (Remove _) -> false | _ -> true) in
+  clauses
+
 let pp_program pp fmt {
-    WithMain.clauses_rev;
+    WithMain.clauses;
     initial_depth;
     compiler_state; } =
-  let clauses = List.rev clauses_rev in
+
+  let clauses = handle_clause_graftin clauses in
+
   let compiler_state, clauses =
-    map_acc (fun state { Ast.Clause.body } ->
-       stack_term_of_preterm ~depth:initial_depth state body)
-       compiler_state clauses in
+    map_acc (fun state { Ast.Clause.body; loc; attributes = { Assembled.id; timestamp } } ->
+       let state, c = stack_term_of_preterm ~depth:initial_depth state body in
+       state, (c,loc,id,timestamp))
+    compiler_state clauses in
   let pp_ctx = {
     uv_names = ref (IntMap.empty, 0);
     table = Symbols.compile_table (State.get Symbols.table compiler_state);
   } in
   Format.fprintf fmt "@[<v>";
-  List.iter (fun body ->
+  List.iter (fun (body,loc,name,timestamp) ->
+    Format.fprintf fmt "@[<h>%% [%a] %a %a@]@;" Format.(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt "; ") pp_print_int) timestamp Loc.pp loc Format.(pp_print_option (fun fmt x -> pp_print_string fmt x)) name ;
     Format.fprintf fmt "%a.@;" (pp ~pp_ctx ~depth:initial_depth) body)
     clauses;
   Format.fprintf fmt "@]"
@@ -2630,19 +2654,19 @@ let quote_preterm time ~compiler_state new_state ?(on_type=false) { term; amap }
     let n, x = mkQCon time ~compiler_state !new_state ~on_type ~amap c in
     new_state := n;
     x in
-  let rec aux depth term = match term with
+  let rec aux_quote depth term = match term with
     | App(c,CData s,[])
       when on_type && c == D.Global_symbols.ctypec && D.C.is_string s -> term
     | App(c,s,[t]) when on_type && c == D.Global_symbols.arrowc ->
-        App(arrowc,aux depth s,[aux depth t])
+        App(arrowc,aux_quote depth s,[aux_quote depth t])
     | Const n when on_type && Symbols.show compiler_state n = "prop" -> term
 
     | Const n -> mkQCon n
     | Builtin(c,[]) -> mkQCon c
-    | Lam x -> App(lamc,Lam (aux (depth+1) x),[])
+    | Lam x -> App(lamc,Lam (aux_quote (depth+1) x),[])
     | App(c,x,xs) ->
-        mkQApp (mkQCon c :: List.(map (aux depth) (x :: xs)))
-    | Builtin(c,args) -> mkQApp (mkQCon c :: List.map (aux depth) args)
+        mkQApp (mkQCon c :: List.(map (aux_quote depth) (x :: xs)))
+    | Builtin(c,args) -> mkQApp (mkQCon c :: List.map (aux_quote depth) args)
 
 (*
     | Arg(id,0) -> D.mkConst id
@@ -2660,11 +2684,11 @@ let quote_preterm time ~compiler_state new_state ?(on_type=false) { term; amap }
     | UVar _ | AppUVar _ -> assert false
 
     | CData _ as x -> App(cdatac,x,[])
-    | Cons(hd,tl) -> mkQApp [mkQCon D.Global_symbols.consc; aux depth hd; aux depth tl]
+    | Cons(hd,tl) -> mkQApp [mkQCon D.Global_symbols.consc; aux_quote depth hd; aux_quote depth tl]
     | Nil -> mkQCon D.Global_symbols.nilc
     | Discard -> mkQCon discardc
   in
-  let term = aux amap.nargs term in
+  let term = aux_quote amap.nargs term in
   !new_state, term
 
 (* FIXME : close_with_pis already exists but unused *)
@@ -2704,9 +2728,10 @@ let rec lam2forall = function
   | UVar _ | AppUVar _ -> assert false
   | Arg _ | AppArg _ -> assert false
 
-let quote_syntax time new_state { WithMain.clauses_rev; query; compiler_state } =
+let quote_syntax time new_state { WithMain.clauses; query; compiler_state } =
   let names = sorted_names_of_argmap query.amap in
-  let new_state, clist = map_acc (quote_clause time ~compiler_state) new_state (List.rev clauses_rev) in
+  let clauses = handle_clause_graftin clauses in
+  let new_state, clist = map_acc (quote_clause time ~compiler_state) new_state clauses in
   let new_state, queryt = quote_preterm time ~on_type:false ~compiler_state new_state query in
   let q =
     App(clausec,CData (quote_loc ~id:"query" query.loc),
@@ -2717,7 +2742,7 @@ let quote_syntax time new_state { WithMain.clauses_rev; query; compiler_state }
 let unfold_type_abbrevs ~compiler_state lcs type_abbrevs { term; loc; amap } =
   let find_opt c =
     try Some (C.Map.find c type_abbrevs) with Not_found -> None in
-  let rec aux seen = function
+  let rec aux_tabbrv seen = function
     | Const c as x ->
         begin match find_opt c with
         | Some { tavalue; taparams } ->
@@ -2727,7 +2752,7 @@ let unfold_type_abbrevs ~compiler_state lcs type_abbrevs { term; loc; amap } =
           if C.Set.mem c seen then
             error ~loc
               ("looping while unfolding type abbreviation for "^ Symbols.show compiler_state c);
-          aux (C.Set.add c seen) tavalue.term
+          aux_tabbrv (C.Set.add c seen) tavalue.term
         | None -> x
         end
     | App(c,t,ts) as x ->
@@ -2741,16 +2766,16 @@ let unfold_type_abbrevs ~compiler_state lcs type_abbrevs { term; loc; amap } =
           if C.Set.mem c seen then
             error ~loc
               ("looping while unfolding type abbreviation for "^ Symbols.show compiler_state c);
-          aux (C.Set.add c seen) (R.deref_appuv ~from:lcs ~to_:lcs (t::ts) tavalue.term)
+          aux_tabbrv (C.Set.add c seen) (R.deref_appuv ~from:lcs ~to_:lcs (t::ts) tavalue.term)
         | None ->
-          let t1 = aux seen t in
-          let ts1 = smart_map (aux seen) ts in
+          let t1 = aux_tabbrv seen t in
+          let ts1 = smart_map (aux_tabbrv seen) ts in
           if t1 == t && ts1 == ts then x
           else App(c,t1,ts1)
         end
     | x -> x
   in
-    { term = aux C.Set.empty term; loc; amap; spilling = false }
+    { term = aux_tabbrv C.Set.empty term; loc; amap; spilling = false }
 
 let term_of_ast ~depth state text =
  if State.get D.while_compiling state then
diff --git a/src/data.ml b/src/data.ml
index 8939c37a..db6eaaad 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -125,6 +125,7 @@ type clause = {
     vars : int;
     mode : mode;        (* CACHE to avoid allocation in get_clauses *)
     loc : Loc.t option; (* debug *)
+    mutable timestamp : int list; (* for grafting *)
 }
 and 
 mode = arg_mode list
@@ -132,6 +133,10 @@ mode = arg_mode list
 
 let to_mode = function true -> Input | false -> Output
 
+type grafting_time = int list
+[@@deriving show, ord]
+type times = (grafting_time * constant) StrMap.t
+[@@deriving show, ord]
 
 type stuck_goal = {
   mutable blockers : blockers;
@@ -151,29 +156,40 @@ and prolog_prog = {
   src : clause_src list; (* hypothetical context in original form, for CHR *)
   index : index;
 }
-and index = second_lvl_idx Ptmap.t
+
+(* These two are the same, but the latter should not be mutated *)
+
+and clause_list = clause Bl.t
+and index = first_lvl_idx
+and first_lvl_idx = {
+  idx : second_lvl_idx Ptmap.t;
+  time : int; (* ticking clock, to timestamp clauses so to recover total order after retrieval if necessary. positive at compile time, negative at run time *)
+  times : times; (* timestamp of named clauses, for grafting at compile time *)
+}
 and second_lvl_idx =
 | TwoLevelIndex of {
     mode : mode;
     argno : int;
-    all_clauses : clause list;        (* when the query is flexible *)
-    flex_arg_clauses : clause list;   (* when the query is rigid but arg_id ha nothing *)
-    arg_idx : clause list Ptmap.t;    (* when the query is rigid (includes in each binding flex_arg_clauses) *)
+    all_clauses : clause_list;        (* when the query is flexible *)
+    flex_arg_clauses : clause_list;   (* when the query is rigid but arg_id ha nothing *)
+    arg_idx : clause_list Ptmap.t;    (* when the query is rigid (includes in each binding flex_arg_clauses) *)
   }
 | BitHash of {
     mode : mode;
     args : int list;
-    time : int;                             (* time is used to recover the total order *)
-    args_idx : (clause * int) list Ptmap.t; (* clause, insertion time *)
+    args_idx : clause_list Ptmap.t; (* clause, insertion time *)
   }
 | IndexWithDiscriminationTree of {
     mode : mode;
     arg_depths : int list;   (* the list of args on which the trie is built *)
-    time : int;         (* time is used to recover the total order *)
     args_idx : clause Discrimination_tree.t; 
 }
 [@@deriving show]
 
+let stop = ref false
+let close_index ({idx; time; times} : index) : index =
+  { idx =idx; time = 0; times = StrMap.empty }
+
 type constraints = stuck_goal list
 type hyps = clause_src list
 
diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml
index 6d6e56f0..ecede752 100644
--- a/src/discrimination_tree.ml
+++ b/src/discrimination_tree.ml
@@ -165,6 +165,23 @@ module Trie = struct
 
   let is_empty x = x == empty
 
+  let rec replace p x = function
+    | Node { data; other; listTailVariable; map } ->
+        Node {
+          data = data |> List.map (fun y -> if p y then x else y);
+          other = other |> Option.map (replace p x);
+          listTailVariable = listTailVariable |> Option.map (replace p x);
+          map = map |> Ptmap.map (replace p x);
+        }
+      
+  let rec remove f = function
+    | Node { data; other; listTailVariable; map } ->
+        Node {
+          data = data |> List.filter (fun x -> not (f x));
+          other = other |> Option.map (remove f);
+          listTailVariable = listTailVariable |> Option.map (remove f);
+          map = map |> Ptmap.map (remove f);
+        }
 
   let add (a : Path.t) v t =
     let max = ref 0 in
@@ -240,8 +257,6 @@ let skip_listTailVariable ~pos path : int =
     else aux (i+1) (update_par_count pc (Path.get path i)) in
   aux (pos + 1) (update_par_count 1 (Path.get path pos))
 
-type 'a data = { data : 'a; time : int }
-
 (* A discrimination tree is a record {t; max_size; max_depths } where
    - t is a Trie for instance retrival 
    - max_size is a int representing the max size of a path in the Trie
@@ -270,13 +285,13 @@ type 'a data = { data : 'a; time : int }
     In the example it is no needed to index the goal path to depth 100, but rather considering
     the maximal depth of the first argument, which 4 << 100
   *)
-type 'a t = {t: 'a data Trie.t; max_size : int;  max_depths : int array } 
+type 'a t = {t: 'a Trie.t; max_size : int;  max_depths : int array } 
 
-let pp pp_a fmt { t } : unit = Trie.pp (fun fmt { data } -> pp_a fmt data) fmt t
-let show pp_a { t } : string = Trie.show (fun fmt { data } -> pp_a fmt data) t
+let pp pp_a fmt { t } : unit = Trie.pp (fun fmt data -> pp_a fmt data) fmt t
+let show pp_a { t } : string = Trie.show (fun fmt data -> pp_a fmt data) t
 
-let index { t; max_size; max_depths } path data ~time =
-  let t, m = Trie.add path { data ; time } t in
+let index { t; max_size; max_depths } path data =
+  let t, m = Trie.add path data t in
   { t; max_size = max max_size m; max_depths }
 
 let max_path { max_size } = max_size
@@ -286,7 +301,7 @@ let max_depths { max_depths } = max_depths
     that are rooted just after the term represented by the tree root
     are returned (we are skipping the root) *)
 let call f =
-  let res = ref [] in
+  let res = ref @@ [] in
   let add_result x = res := x :: !res in
   f ~add_result; !res
   
@@ -315,8 +330,6 @@ let skip_to_listEnd ~add_result mode (Trie.Node { other; map; listTailVariable }
 
 let skip_to_listEnd mode t = call (skip_to_listEnd mode t)
 
-let cmp_data { time = tx } { time = ty } = ty - tx
-
 let get_all_children v mode = isLam v || (isVariable v && isOutput mode)
 
 let rec retrieve ~pos ~add_result mode path tree : unit =
@@ -383,10 +396,12 @@ let retrieve ~pos ~add_result path index =
   assert(isInput mode || isOutput mode);
   retrieve ~add_result mode ~pos:(pos+1) path index
   
-let retrieve path { t } = 
+let retrieve cmp_data path { t } = 
   let r = call (retrieve ~pos:0 path t) in
-  List.sort cmp_data r |> List.map (fun x -> x.data)
+  Bl.of_list @@ List.sort cmp_data r
 
+let replace p x i = { i with t = Trie.replace p x i.t }
+let remove keep dt = { dt with t = Trie.remove keep dt.t}
 
 module Internal = struct
   let kConstant = kConstant
diff --git a/src/discrimination_tree.mli b/src/discrimination_tree.mli
index ba483379..f4ca6c2b 100644
--- a/src/discrimination_tree.mli
+++ b/src/discrimination_tree.mli
@@ -21,7 +21,6 @@ val mkListHead : cell
 val mkListEnd : cell
 val mkPathEnd : cell
 
-type 'a data
 type 'a t
 
 (** [index dt path value ~time] returns a new discrimination tree starting from [dt]
@@ -32,7 +31,7 @@ type 'a t
 
     @note: in the elpi runtime, there are no two rule having the same [~time]
 *)
-val index : 'a t -> Path.t -> 'a -> time:int -> 'a t
+val index : 'a t -> Path.t -> 'a -> 'a t
 
 val max_path : 'a t -> int
 val max_depths : 'a t -> int array
@@ -50,7 +49,10 @@ val empty_dt : 'b list -> 'a t
   has been added at time [t] and r_2 been added at time [t+1] then
   r_2 will appear before r_1 in the final result
 *)
-val retrieve : Path.t -> 'a t -> 'a list
+val retrieve : ('a -> 'a -> int) -> Path.t -> 'a t -> 'a Bl.scan
+
+val replace : ('a -> bool) -> 'a -> 'a t -> 'a t
+val remove  : ('a -> bool) -> 'a t -> 'a t
 
 (***********************************************************)
 (* Printers                                                *)
diff --git a/src/dune b/src/dune
index b20135ec..89df953e 100644
--- a/src/dune
+++ b/src/dune
@@ -1,7 +1,7 @@
 (library
   (public_name elpi)
   (preprocess (per_module
-    ((pps ppx_deriving.std) API data compiler discrimination_tree)
+    ((pps ppx_deriving.std) API data compiler discrimination_tree bl)
     ((pps ppx_deriving.std elpi.trace.ppx -- --cookie "elpi_trace=\"true\"") runtime)
     ((pps ppx_deriving.std elpi.trace.ppx -- --cookie "elpi_trace=\"false\"") runtime_trace_off)
     ))
@@ -14,11 +14,11 @@
     ; ----- public API ---------------------------------
     elpi API builtin builtin_checker
     ; ----- internal stuff -----------------------------
-    compiler data ptmap discrimination_tree runtime_trace_off runtime
+    compiler data ptmap discrimination_tree bl runtime_trace_off runtime
     builtin_stdlib builtin_map builtin_set
     legacy_parser_proxy)
   (private_modules
-    compiler data ptmap runtime_trace_off runtime
+    compiler data ptmap runtime_trace_off
     builtin_stdlib builtin_map builtin_set
     legacy_parser_proxy)
 )
@@ -84,3 +84,5 @@
   (action (run atdts %{dep:trace.atd})))
 
 (test (name test_discrimination_tree) (libraries elpi) (modules test_discrimination_tree) (preprocess (pps ppx_deriving.std)))
+(test (name test_bl) (libraries elpi) (modules test_bl) (preprocess (pps ppx_deriving.std)))
+(test (name test_lex) (libraries elpi) (modules test_lex) (preprocess (pps ppx_deriving.std)))
diff --git a/src/elpi.ml b/src/elpi.ml
index 35dff962..fc757d9b 100644
--- a/src/elpi.ml
+++ b/src/elpi.ml
@@ -3,4 +3,6 @@ module Builtin = Builtin
 module Builtin_checker = Builtin_checker
 module Internal = struct
   module Discrimination_tree = Discrimination_tree
+  module Bl = Bl
+  module Runtime = Runtime
 end
\ No newline at end of file
diff --git a/src/parser/ast.ml b/src/parser/ast.ml
index 5491db4d..03afff79 100644
--- a/src/parser/ast.ml
+++ b/src/parser/ast.ml
@@ -143,6 +143,7 @@ type raw_attribute =
   | After of string
   | Before of string
   | Replace of string
+  | Remove of string
   | External
   | Index of int list * string option
 [@@deriving show]
@@ -318,7 +319,8 @@ and attribute = {
   id : string option;
   ifexpr : string option;
 }
-and insertion = Before of string | After of string | Replace of string
+and insertion = Insert of insertion_place | Replace of string | Remove of string
+and insertion_place = Before of string | After of string
 and tattribute =
   | External
   | Index of int list * tindex option
diff --git a/src/parser/ast.mli b/src/parser/ast.mli
index 0fea5a9f..d1ce0d3f 100644
--- a/src/parser/ast.mli
+++ b/src/parser/ast.mli
@@ -73,6 +73,7 @@ type raw_attribute =
   | After of string
   | Before of string
   | Replace of string
+  | Remove of string
   | External
   | Index of int list * string option
 [@@ deriving show]
@@ -213,7 +214,8 @@ and attribute = {
   id : string option;
   ifexpr : string option;
 }
-and insertion = Before of string | After of string | Replace of string
+and insertion = Insert of insertion_place | Replace of string | Remove of string
+and insertion_place = Before of string | After of string
 and cattribute = {
   cid : string;
   cifexpr : string option
diff --git a/src/parser/error_messages.txt b/src/parser/error_messages.txt
index 8f376624..4a030e0a 100644
--- a/src/parser/error_messages.txt
+++ b/src/parser/error_messages.txt
@@ -298,10 +298,13 @@ Malformed 'if' attribute. Example:
 
 program: COLON BEFORE VDASH
 program: COLON AFTER VDASH
+program: COLON REMOVE VDASH
 
 Malformed grafting attribute. Example:
 :before "some name"
 :after "some other name"
+:replace "some other name"
+:remove "some other name"
 
 program: COLON EXTERNAL VDASH
 program: COLON EXTERNAL COLON VDASH
@@ -411,6 +414,8 @@ kind list  type -> type.
 
 program: CONSTRAINT VDASH
 program: CONSTRAINT AFTER VDASH
+program: CONSTRAINT QDASH VDASH
+program: CONSTRAINT QDASH AFTER QDASH
 
 Constraint Handling Rule header expected. Examples:
 constraint foo {
diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly
index 1e737bb7..25c8d375 100644
--- a/src/parser/grammar.mly
+++ b/src/parser/grammar.mly
@@ -300,6 +300,7 @@ attribute:
 | AFTER; s = STRING { After s }
 | BEFORE; s = STRING { Before s }
 | REPLACE; s = STRING { Replace s }
+| REMOVE; s = STRING { Remove s }
 | EXTERNAL { External }
 | INDEX; LPAREN; l = nonempty_list(indexing) ; RPAREN; o = option(STRING) { Index (l,o) }
 
@@ -400,6 +401,7 @@ constant:
 | BEFORE { Func.from_string "before" }
 | AFTER { Func.from_string "after" }
 | REPLACE { Func.from_string "replace" }
+| REMOVE { Func.from_string "remove" }
 | INDEX { Func.from_string "index" }
 | c = IO { Func.from_string @@ String.make 1 c }
 | CUT { Func.cutf }
diff --git a/src/parser/lexer.mll.in b/src/parser/lexer.mll.in
index 2b731cec..57b0b034 100644
--- a/src/parser/lexer.mll.in
+++ b/src/parser/lexer.mll.in
@@ -165,6 +165,7 @@ and token = parse
 | "after" { AFTER }
 | "before" { BEFORE }
 | "replace" { REPLACE }
+| "remove" { REMOVE }
 | "name" { NAME }
 | "if" { IF }
 | "index" { INDEX }
diff --git a/src/parser/test_lexer.ml b/src/parser/test_lexer.ml
index 2895675f..c972ec2d 100644
--- a/src/parser/test_lexer.ml
+++ b/src/parser/test_lexer.ml
@@ -15,6 +15,7 @@ type t = Tokens.token =
   | RULE
   | RPAREN
   | REPLACE
+  | REMOVE
   | RCURLY
   | RBRACKET
   | QUOTED of ( string )
diff --git a/src/parser/tokens.mly b/src/parser/tokens.mly
index f4e919b5..c1331ac4 100644
--- a/src/parser/tokens.mly
+++ b/src/parser/tokens.mly
@@ -58,6 +58,7 @@
 %token BEFORE
 %token AFTER
 %token REPLACE
+%token REMOVE
 %token NAME 
 %token INDEX 
 %token CONS
diff --git a/src/runtime.ml b/src/runtime.ml
index 0a90304f..ad39813d 100644
--- a/src/runtime.ml
+++ b/src/runtime.ml
@@ -2335,6 +2335,39 @@ let output arguments assignments state =
 
 module Indexing = struct (* {{{ *)
 
+(* These are sorted wrt lex_insertion
+ -2
+ -1
+  0
+  1.-1
+  1.-2
+  1
+  1.+2
+  1.+1
+  2
+
+  The idea being that clause "a" to be inserted w.r.t. "b" takes
+  as timestamp the one of "b" followerd by the timestamp. If "a"
+  has to be before, the timestamp is made negative.
+*)
+let lex_insertion l1 l2 =
+  let rec lex_insertion fst l1 l2 =
+  match l1, l2 with
+  | [], [] -> 0
+  | x :: l1, y :: l2  when not fst ->
+      let r =
+        if x < 0 && y < 0 || x > 0 && y > 0
+          then y - x else x - y in
+      if r = 0 then lex_insertion false l1 l2
+      else r
+  | x1 :: l1, x2 :: l2 ->
+      let x = x1 - x2 in
+      if x = 0 then lex_insertion false l1 l2
+      else x
+  | [], ys -> lex_insertion false [0] ys
+  | xs, [] -> lex_insertion false xs [0]
+  in
+  lex_insertion true l1 l2
 let mustbevariablec = min_int (* uvar or uvar t or uvar l t *)
 
 let ppclause f ~hd { depth; args = args; hyps = hyps } =
@@ -2598,128 +2631,203 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar arg_mo
     if args == [] then emit_mode is_goal mkOutputMode
     else aux ~safe ~depth is_goal args (if is_goal then Array.to_list args_depths_ar else arg_depths) arg_modes
   end;
-  Path.stop path
-
-let add1clause ~depth m (predicate,clause) =
-  match Ptmap.find predicate m with
-  | TwoLevelIndex { all_clauses; argno; mode; flex_arg_clauses; arg_idx } ->
-      begin match classify_clause_argno ~depth argno mode clause.args with
+  Path.stop path  
+
+let make_new_Map_snd_level_index argno mode =
+  TwoLevelIndex {
+    argno;
+    mode;
+    all_clauses = Bl.empty ();
+    flex_arg_clauses = Bl.empty ();
+    arg_idx = Ptmap.empty;
+  }
+        
+let add_clause_to_snd_lvl_idx ~depth ~insert predicate clause = function
+  | TwoLevelIndex { all_clauses; argno; mode; flex_arg_clauses; arg_idx; } ->
+    begin match classify_clause_argno ~depth argno mode clause.args with
+    | Variable ->
       (* X: matches both rigid and flexible terms *)
-      | Variable ->
-        Ptmap.add predicate (TwoLevelIndex {
-          argno; mode;
-          all_clauses = clause :: all_clauses;
-          flex_arg_clauses = clause :: flex_arg_clauses;
-          arg_idx = Ptmap.map (fun l_rev -> clause :: l_rev) arg_idx;
-        }) m
-      | MustBeVariable ->
+      TwoLevelIndex {
+        argno; mode;
+        all_clauses = insert clause all_clauses;
+        flex_arg_clauses = insert clause flex_arg_clauses;
+        arg_idx = Ptmap.map (fun l_rev -> insert clause l_rev) arg_idx;
+      }
+    | MustBeVariable ->
       (* uvar: matches only flexible terms (or itself at the meta level) *)
-        let l_rev =
-          try Ptmap.find mustbevariablec arg_idx
-          with Not_found -> flex_arg_clauses in
-        Ptmap.add predicate (TwoLevelIndex {
-            argno; mode;
-          all_clauses = clause :: all_clauses;
-          flex_arg_clauses;
-          arg_idx = Ptmap.add mustbevariablec (clause::l_rev) arg_idx;
-        }) m
-      | Rigid (arg_hd,arg_mode) ->
+      let clauses =
+        try Ptmap.find mustbevariablec arg_idx
+        with Not_found -> flex_arg_clauses in
+      TwoLevelIndex {
+          argno; mode;
+        all_clauses = insert clause all_clauses;
+        flex_arg_clauses;
+        arg_idx = Ptmap.add mustbevariablec (insert clause clauses) arg_idx;
+      }
+    | Rigid (arg_hd,arg_mode) ->
       (* t: a rigid term matches flexible terms only in unification mode *)
-        let l_rev =
-          try Ptmap.find arg_hd arg_idx
-          with Not_found -> flex_arg_clauses in
-        let all_clauses =
-          if arg_mode = Input then all_clauses else clause :: all_clauses in
-        Ptmap.add predicate (TwoLevelIndex {
-            argno; mode;
-          all_clauses;
-          flex_arg_clauses;
-          arg_idx = Ptmap.add arg_hd (clause::l_rev) arg_idx;
-        }) m
-      end
-  | BitHash { mode; args; time; args_idx } ->
-      let hash = hash_clause_arg_list predicate ~depth clause.args mode args in
       let clauses =
-        try Ptmap.find hash args_idx
-        with Not_found -> [] in
-      Ptmap.add predicate (BitHash {
-         mode; args;
-         time = time + 1;
-         args_idx = Ptmap.add hash ((clause,time) :: clauses) args_idx
-       }) m
-  | IndexWithDiscriminationTree {mode; arg_depths; args_idx; time } ->
+        try Ptmap.find arg_hd arg_idx
+        with Not_found -> flex_arg_clauses in
+      let all_clauses =
+        if arg_mode = Input then all_clauses else insert clause all_clauses in
+      TwoLevelIndex {
+        argno; mode;
+        all_clauses;
+        flex_arg_clauses;
+        arg_idx = Ptmap.add arg_hd (insert clause clauses) arg_idx;
+      }
+    end
+| BitHash { mode; args; args_idx } ->
+    let hash = hash_clause_arg_list predicate ~depth clause.args mode args in
+    let clauses =
+      try Ptmap.find hash args_idx
+      with Not_found -> Bl.empty () in
+    BitHash {
+       mode; args;
+       args_idx = Ptmap.add hash (insert clause clauses) args_idx
+    }
+| IndexWithDiscriminationTree {mode; arg_depths; args_idx; } ->
     let max_depths = Discrimination_tree.max_depths args_idx in
     let max_path = Discrimination_tree.max_path args_idx in
-      let path = arg_to_trie_path ~depth ~safe:true ~is_goal:false clause.args arg_depths max_depths mode max_path in
-      [%spy "dev:disc-tree:depth-path" ~rid pp_string "Inst: MaxDepths " (pplist pp_int "") (Array.to_list max_depths)];
-      let args_idx = Discrimination_tree.index args_idx path clause ~time in
-        Ptmap.add predicate (IndexWithDiscriminationTree {
-          mode; arg_depths;
-          time = time+1;
-          args_idx = args_idx
-        }) m
-  | exception Not_found ->
-      match classify_clause_argno ~depth 0 [] clause.args with
-      | Variable ->
-      Ptmap.add predicate (TwoLevelIndex {
-        argno = 0; mode = [];
-        all_clauses = [clause];
-        flex_arg_clauses = [clause];
-        arg_idx =Ptmap.empty;
-      }) m
-      | MustBeVariable ->
-      Ptmap.add predicate (TwoLevelIndex {
-        argno = 0;mode = [];
-        all_clauses = [clause];
-        flex_arg_clauses = [];
-        arg_idx = Ptmap.add mustbevariablec [clause] Ptmap.empty;
-      }) m
-      | Rigid (arg_hd,arg_mode) ->
-      let all_clauses = if arg_mode == Input then [] else [clause] in
-      Ptmap.add predicate (TwoLevelIndex {
-        argno = 0;mode = [];
-        all_clauses;
-        flex_arg_clauses = [];
-        arg_idx = Ptmap.add arg_hd [clause] Ptmap.empty;
-      }) m
-
-let add_clauses ~depth clauses p =
+    let path = arg_to_trie_path ~depth ~safe:true ~is_goal:false clause.args arg_depths max_depths mode max_path in
+    [%spy "dev:disc-tree:depth-path" ~rid pp_string "Inst: MaxDepths " (pplist pp_int "") (Array.to_list max_depths)];
+    let args_idx = Discrimination_tree.index args_idx path clause in
+    IndexWithDiscriminationTree {
+      mode; arg_depths;
+      args_idx = args_idx
+    }
+
+let compile_time_tick x = x + 1
+let run_time_tick x = x - 1
+    
+let rec add1clause_runtime ~depth { idx; time; times } predicate clause =
+  try
+    let snd_lvl_idx = Ptmap.find predicate idx in
+    let time = run_time_tick time in
+    clause.timestamp <- [time];
+    let snd_lvl_idx = add_clause_to_snd_lvl_idx ~depth ~insert:Bl.cons predicate clause snd_lvl_idx in
+    { times; time; idx = Ptmap.add predicate snd_lvl_idx idx }
+  with
+  | Not_found ->
+      (* Unknown predicate, we could detect this statically and forbid it *)
+      let idx = Ptmap.add predicate (make_new_Map_snd_level_index 0 []) idx in
+      add1clause_runtime ~depth { idx; time; times } predicate clause
+
+let add_clauses ~depth clauses idx =
   (* pplist (fun fmt (hd, b) -> ppclause fmt hd b) ";" Fmt.std_formatter clauses; *)
   (* let t1 = Unix.gettimeofday () in *)
-  let p = List.fold_left (add1clause ~depth) p clauses in
+  let idx = List.fold_left (fun m (p,c) -> add1clause_runtime ~depth m p c) idx clauses in
   (* let t2 = Unix.gettimeofday () in  *)
   (* pp_string Fmt.std_formatter (Printf.sprintf "\nTime taken by add_clauses is %f\n" (t2-.t1)); *)
-  p
-
-let make_index ~depth ~indexing ~clauses_rev:p =
-  let m = C.Map.fold (fun predicate (mode, indexing) m ->
-    Ptmap.add predicate 
-    begin
-      match indexing with
-      | Hash args -> BitHash {
-          args;
-          mode;
-          time = min_int;
-          args_idx = Ptmap.empty;
-        }
-      | MapOn argno -> TwoLevelIndex {
-          argno;
-          mode;
-          all_clauses = [];
-          flex_arg_clauses = [];
-          arg_idx = Ptmap.empty;
-        }
-      | DiscriminationTree arg_depths -> IndexWithDiscriminationTree {
-          arg_depths;  mode; 
-          args_idx = Discrimination_tree.empty_dt arg_depths;
-          time = min_int;
-        }
-    end m) indexing Ptmap.empty in
-  { index = add_clauses ~depth p m; src = [] }
-
+  idx
+  
 let add_clauses ~depth clauses clauses_src { index; src } =
   { index = add_clauses ~depth clauses index; src = List.rev clauses_src @ src }
 
+let add_to_times loc name time predicate times =
+  match name with
+  | None -> times
+  | Some id ->
+    if StrMap.mem id times then
+      error ?loc ("duplicate clause name " ^ id)
+    else
+      StrMap.add id (time,predicate) times
+
+let time_of loc x times =
+  try StrMap.find x times
+  with Not_found -> error ?loc ("cannot graft, clause " ^ x ^ " not found")
+
+let remove_from_times id times = StrMap.remove id times
+    
+let remove_clause_in_snd_lvl_idx p = function
+| TwoLevelIndex { argno; mode; all_clauses; flex_arg_clauses; arg_idx; } ->
+  TwoLevelIndex {
+    argno; mode;
+    all_clauses = Bl.remove p all_clauses;
+    flex_arg_clauses = Bl.remove p flex_arg_clauses;
+    arg_idx = Ptmap.map (Bl.remove p) arg_idx;
+   }
+| BitHash { mode; args; args_idx } ->
+  BitHash {
+    mode; args;
+    args_idx = Ptmap.map (Bl.remove p) args_idx
+  }
+| IndexWithDiscriminationTree {mode; arg_depths; args_idx; } ->
+  IndexWithDiscriminationTree {
+    mode; arg_depths;
+    args_idx = Discrimination_tree.remove p args_idx;
+  }
+
+let rec add1clause_compile_time ~depth { idx; time; times } ~graft predicate clause name =
+  try
+    let snd_lvl_idx = Ptmap.find predicate idx in
+    let time = compile_time_tick time in
+    match graft with
+    | None ->
+        let timestamp = [time] in
+        let times = add_to_times clause.loc name timestamp predicate times in
+        clause.timestamp <- timestamp;
+        let snd_lvl_idx = add_clause_to_snd_lvl_idx ~depth ~insert:Bl.rcons predicate clause snd_lvl_idx in
+        { times; time; idx = Ptmap.add predicate snd_lvl_idx idx }
+    | Some (Ast.Structured.Remove x) ->
+        let reference, predicate1 = time_of clause.loc x times in
+        if predicate1 <> predicate then
+          error ?loc:clause.loc ("cannot remove a clause for another predicate");
+        let times = remove_from_times x times in
+        clause.timestamp <- reference;
+        let snd_lvl_idx = remove_clause_in_snd_lvl_idx (fun x -> x.timestamp = reference) snd_lvl_idx in
+        { times; time; idx = Ptmap.add predicate snd_lvl_idx idx }
+    | Some (Ast.Structured.Replace x) ->
+        let reference, predicate1 = time_of clause.loc x times in
+        if predicate1 <> predicate then
+          error ?loc:clause.loc ("cannot replace a clause for another predicate");
+        let times = remove_from_times x times in
+        clause.timestamp <- reference;
+        let snd_lvl_idx = remove_clause_in_snd_lvl_idx (fun x -> x.timestamp = reference) snd_lvl_idx in
+        let snd_lvl_idx = add_clause_to_snd_lvl_idx ~depth ~insert:Bl.(insert (fun x -> lex_insertion x.timestamp reference)) predicate clause snd_lvl_idx in
+        { times; time; idx = Ptmap.add predicate snd_lvl_idx idx }
+    | Some (Ast.Structured.Insert gr) ->
+        let timestamp =
+          match gr with
+          | Ast.Structured.Before x -> (fst @@ time_of clause.loc x times) @ [-time]
+          | Ast.Structured.After x  -> (fst @@ time_of clause.loc x times) @ [+time] in
+        let times = add_to_times clause.loc name timestamp predicate times in
+        clause.timestamp <- timestamp;
+        let snd_lvl_idx = add_clause_to_snd_lvl_idx ~depth ~insert:Bl.(insert (fun x -> lex_insertion x.timestamp timestamp)) predicate clause snd_lvl_idx in
+        { times; time; idx = Ptmap.add predicate snd_lvl_idx idx }
+  with Not_found ->
+      let idx = Ptmap.add predicate (make_new_Map_snd_level_index 0 []) idx in
+      add1clause_compile_time ~depth { idx; time; times } ~graft predicate clause name
+
+let update_indexing (indexing : (mode * indexing) Constants.Map.t) (index : index) : index =
+  let idx =
+    C.Map.fold (fun predicate (mode, indexing) m ->
+      Ptmap.add predicate 
+      begin
+        match indexing with
+        | Hash args -> BitHash {
+            args;
+            mode;
+            args_idx = Ptmap.empty;
+          }
+        | MapOn argno -> make_new_Map_snd_level_index argno mode
+        | DiscriminationTree arg_depths -> IndexWithDiscriminationTree {
+            arg_depths;  mode; 
+            args_idx = Discrimination_tree.empty_dt arg_depths;
+          }
+      end m) indexing index.idx
+    in
+      { index with idx }
+
+let add_to_index ~depth ~predicate ~graft clause name index : index =
+  add1clause_compile_time ~depth ~graft index predicate clause name
+
+let make_empty_index ~depth ~indexing =
+  let index = update_indexing indexing { idx = Ptmap.empty; time = 0; times = StrMap.empty } in
+  let index = close_index index in
+  { index; src = [] }
+
 type goal_arg_classification =
   | Variable
   | Rigid of constant
@@ -2772,7 +2880,9 @@ let trie_goal_args goal : term list = match goal with
   | App(_, x, xs) -> x :: xs
   | _ -> assert false
 
-let get_clauses ~depth predicate goal { index = m } =
+let cmp_timestamp { timestamp = tx } { timestamp = ty } = lex_insertion tx ty
+
+let get_clauses ~depth predicate goal { index = { idx = m } } =
  let rc =
    try
      match Ptmap.find predicate m with
@@ -2782,11 +2892,11 @@ let get_clauses ~depth predicate goal { index = m } =
        | Rigid arg_hd ->
           try Ptmap.find arg_hd arg_idx
           with Not_found -> flex_arg_clauses
-       end
+       end |> Bl.to_scan
      | BitHash { args; mode; args_idx } ->
        let hash = hash_goal_args ~depth mode args goal in
-       let cl = List.flatten (Ptmap.find_unifiables hash args_idx) in
-       List.(map fst (sort (fun (_,cl1) (_,cl2) -> cl2 - cl1) cl))
+       let cl = Ptmap.find_unifiables hash args_idx |> List.map Bl.to_scan |> List.map Bl.to_list |> List.flatten in
+       Bl.of_list @@ List.sort cmp_timestamp cl
      | IndexWithDiscriminationTree {arg_depths; mode; args_idx} ->
         let max_depths = Discrimination_tree.max_depths args_idx in
         let max_path = Discrimination_tree.max_path args_idx in
@@ -2797,14 +2907,14 @@ let get_clauses ~depth predicate goal { index = m } =
           Discrimination_tree.Path.pp path
           (pplist pp_int ";") arg_depths
           (*Discrimination_tree.(pp (fun fmt x -> pp_string fmt "+")) args_idx*)];
-        let candidates = Discrimination_tree.retrieve path args_idx in 
+        let candidates = Discrimination_tree.retrieve cmp_timestamp path args_idx in 
           [%spy "dev:disc-tree:candidates" ~rid 
-            pp_int (List.length candidates)];
+            pp_int (Bl.length candidates)];
         candidates
-   with Not_found -> []
+   with Not_found -> Bl.of_list []
  in
- [%log "get_clauses" ~rid (C.show predicate) (List.length rc)];
- [%spy "dev:get_clauses" ~rid C.pp predicate pp_int (List.length rc)];
+ [%log "get_clauses" ~rid (C.show predicate) (Bl.length rc)];
+ [%spy "dev:get_clauses" ~rid C.pp predicate pp_int (Bl.length rc)];
  rc
 
 (* flatten_snd = List.flatten o (List.map ~~snd~~) *)
@@ -2858,7 +2968,7 @@ end (* }}} *)
 open Indexing
 
 (* Used to pass the program to the CHR runtime *)
-let orig_prolog_program = Fork.new_local (make_index ~depth:0 ~indexing:C.Map.empty ~clauses_rev:[])
+let orig_prolog_program = Fork.new_local (make_empty_index ~depth:0 ~indexing:C.Map.empty)
 
 (******************************************************************************
   Dynamic Prolog program
@@ -2868,7 +2978,7 @@ module Clausify : sig
 
   val clausify : loc:Loc.t option -> prolog_prog -> depth:int -> term -> (constant*clause) list * clause_src list * int
 
-  val clausify1 : loc:Loc.t -> mode C.Map.t -> nargs:int -> depth:int -> term -> (constant*clause) * clause_src * int
+  val clausify1 : loc:Loc.t -> modes:(constant -> mode) -> nargs:int -> depth:int -> term -> (constant*clause) * clause_src * int
   
   (* Utilities that deref on the fly *)
   val lp_list_to_list : depth:int -> term -> term list
@@ -2996,7 +3106,7 @@ let rec claux1 loc get_mode vars depth hyps ts lts lcs t =
            type_error ?loc "The head of a clause cannot be a builtin data type"
        | Cons _ | Nil -> assert false
      in
-     let c = { depth = depth+lcs; args; hyps; mode = get_mode hd; vars; loc } in
+     let c = { depth = depth+lcs; args; hyps; mode = get_mode hd; vars; loc; timestamp = [] } in
      [%spy "dev:claudify:extra-clause" ~rid (ppclause ~hd) c];
      (hd,c), { hdepth = depth; hsrc = g }, lcs
   | UVar ({ contents=g },from,args) when g != C.dummy ->
@@ -3014,7 +3124,7 @@ let rec claux1 loc get_mode vars depth hyps ts lts lcs t =
   | Nil | Cons _ -> error ?loc "ill-formed hypothetical clause"
   end]
 
-let clausify ~loc { index } ~depth t =
+let clausify ~loc { index = { idx = index } } ~depth t =
   let get_mode x =
     match Ptmap.find x index with
     | TwoLevelIndex { mode } -> mode
@@ -3033,9 +3143,8 @@ let clausify ~loc { index } ~depth t =
   clauses, program, lcs
 ;;
 
-let clausify1 ~loc m ~nargs ~depth t =
-  claux1 (Some loc) (fun x -> try C.Map.find x m with Not_found -> [])
-    nargs depth [] [] 0 0 t
+let clausify1 ~loc ~modes ~nargs ~depth t =
+  claux1 (Some loc) modes nargs depth [] [] 0 0 t
 
 end (* }}} *)
 open Clausify
@@ -3081,7 +3190,7 @@ and alternative = {
   stack : frame;
   trail : T.trail;
   state : State.t;
-  clauses : clause list;
+  clauses : clause Bl.scan;
   next : alternative;
 }
 let noalts : alternative = Obj.magic (Sys.opaque_identity 0)
@@ -3852,12 +3961,12 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
     | Const k ->
        let clauses = get_clauses ~depth k g p in
        [%spy "user:rule" ~rid ~gid pp_string "backchain"];
-       [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
+       [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) (Bl.to_list clauses)];
        [%tcall backchain depth p (k, C.dummy, [], gs) (gid[@trace]) next alts cutto_alts clauses]
     | App (k,x,xs) ->
        let clauses = get_clauses ~depth k g p in
        [%spy "user:rule" ~rid ~gid pp_string "backchain"];
-       [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
+       [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) (Bl.to_list clauses)];
        [%tcall backchain depth p (k, x, xs, gs) (gid[@trace]) next alts cutto_alts clauses]
     | Builtin(c, args) -> [%spy "user:rule" ~rid ~gid pp_string "builtin"]; [%spy "user:rule:builtin:name" ~rid ~gid pp_string (C.show c)];
        let once ~depth g state =
@@ -3884,13 +3993,14 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
 
   (* We pack some arguments into a tuple otherwise we consume too much stack *)
   and backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cp = [%trace "select" ~rid begin
-    match cp with
-      | [] -> [%spy "user:rule:backchain" ~rid ~gid pp_string "fail"];
+    if Bl.is_empty cp then begin
+        [%spy "user:rule:backchain" ~rid ~gid pp_string "fail"];
         [%tcall next_alt alts]
-      | { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc } :: cs ->
-        [%spy "user:rule:backchain:try" ~rid ~gid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin loc) (ppclause ~hd:k) { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc }];
+    end else
+      let { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc }, cs = Bl.next cp in
+        [%spy "user:rule:backchain:try" ~rid ~gid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin loc) (ppclause ~hd:k) { depth = c_depth; mode = c_mode; args = c_args; hyps = c_hyps; vars = c_vars; loc; timestamp = [] }];
         let old_trail = !T.trail in
-        T.last_call := alts == noalts && cs == [];
+        T.last_call := alts == noalts && Bl.is_empty cs;
         let env = Array.make c_vars C.dummy in
         match
           match c_args with
@@ -3904,7 +4014,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
             T.undo ~old_trail (); [%tcall backchain depth p (k, arg, args_of_g, gs) (gid[@trace]) next alts cutto_alts cs]
         | true ->
            let oldalts = alts in
-           let alts = if cs = [] then alts else
+           let alts = if Bl.is_empty cs then alts else
              { program = p; adepth = depth; agoal_hd = k; ogoal_arg = arg; ogoal_args = args_of_g; agid = gid[@trace]; goals = gs; stack = next;
                trail = old_trail;
                state = !CS.state;
@@ -3934,7 +4044,7 @@ let make_runtime : ?max_steps: int -> ?delay_outside_fragment: bool -> 'x execut
         if alts != cutto_alts then begin
           List.iter (fun c -> 
             [%spy "user:rule:cut:branch" ~rid UUID.pp agid (pp_option Util.CData.pp) (Util.option_map Ast.cloc.Util.CData.cin c.loc) (ppclause ~hd) c])
-          clauses;
+          (clauses |> Bl.to_list);
           prune alts.next
         end
       in
@@ -4090,7 +4200,7 @@ end;*)
     [%cur_pred (Some (C.show k))];
     [%spyl "user:curgoal" ~rid ~gid (uppterm depth [] ~argsdepth:0 empty_env) [Const k;App(k,arg,args)]];
     [%spy "user:rule" ~rid ~gid pp_string "backchain"];
-    [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) clauses];
+    [%spyl "user:rule:backchain:candidates" ~rid ~gid (pp_candidate ~depth ~k) (Bl.to_list clauses)];
     [%tcall backchain depth p (k, arg, args, gs) (gid[@trace]) next alts cutto_alts clauses]
     end]
   in
@@ -4209,10 +4319,9 @@ let mkAppArg = HO.mkAppArg
 let subst ~depth = HO.subst depth
 let move = HO.move
 let hmove = HO.hmove
-let make_index = make_index
-let clausify1 = Clausify.clausify1
 let mkinterval = C.mkinterval
 let mkAppL = C.mkAppL
+let lex_insertion = lex_insertion
 
 let expand_uv ~depth r ~lvl ~ano =
   let t, assignment = HO.expand_uv ~depth r ~lvl ~ano in
@@ -4223,5 +4332,8 @@ let expand_appuv ~depth r ~lvl ~args =
   option_iter (fun (r,_,assignment) -> r @:= assignment) assignment;
   t
 
-
-(* vim: set foldmethod=marker: *)
+module CompileTime = struct
+  let update_indexing = update_indexing
+  let add_to_index = add_to_index
+  let clausify1 = Clausify.clausify1  
+end
\ No newline at end of file
diff --git a/src/runtime.mli b/src/runtime.mli
index 5d6be243..5a087517 100644
--- a/src/runtime.mli
+++ b/src/runtime.mli
@@ -61,19 +61,32 @@ val hmove :
   from:int -> to_:int -> term -> term
 val subst: depth:int -> term list -> term -> term
 
-val make_index :
-  depth:int ->
-  indexing:(mode * indexing) Constants.Map.t ->
-  clauses_rev:(constant * clause) list ->
-    prolog_prog
-
 (* The projection from the internal notion of constraints in the API one *)
 val get_suspended_goal : 'a stuck_goal_kind -> suspended_goal option
 
-(* can raise CannotDeclareClauseForBuiltin *)
-val clausify1 :
-  loc:Loc.t ->
-  mode Constants.Map.t -> (* for caching it in the clause *)
-  nargs:int -> depth:int -> term -> (constant * clause) * clause_src * int
-
 val full_deref : depth:int -> term -> term
+
+(* for testing *)
+val lex_insertion : int list -> int list -> int
+
+(* Some parts of the runtime are needed at compile time, like indexing *)
+module CompileTime : sig
+  (* updates how predicates are indexed *)
+  val update_indexing :
+    (mode * indexing) Constants.Map.t ->
+      index -> index
+
+  (* adds 1 clause to its index *)
+  val add_to_index :
+    depth:int ->
+    predicate:constant ->
+    graft:Elpi_parser.Ast.Structured.insertion option ->
+    clause -> string option -> index -> index
+
+  (* can raise CannotDeclareClauseForBuiltin *)
+  val clausify1 :
+    loc:Loc.t ->
+    modes:(constant -> mode) -> (* for caching it in the clause *)
+    nargs:int -> depth:int -> term -> (constant * clause) * clause_src * int
+
+end
diff --git a/src/test_bl.ml b/src/test_bl.ml
new file mode 100644
index 00000000..a74732b1
--- /dev/null
+++ b/src/test_bl.ml
@@ -0,0 +1,27 @@
+open Elpi.Internal.Bl
+let size = 9999999
+
+let test_build () =
+  Gc.minor (); Gc.major ();
+
+  let t0 = Unix.gettimeofday () in
+  let rec aux n acc =
+    (* Format.eprintf "bl before adding %d = %a\n" n pp acc; *)
+    if n = 0 then acc else aux (n-1) (rcons n acc) in
+  let r1 = aux size (empty ()) in
+  let t1 = Unix.gettimeofday () in
+
+  Gc.minor (); Gc.major ();
+
+  let t2 = Unix.gettimeofday () in
+  let rec aux n acc =
+    if n = 0 then acc else aux (n-1) (n :: acc) in
+  let r2 = List.rev @@ aux size [] in
+  let t3 = Unix.gettimeofday () in
+
+  Format.eprintf "build: bl=%4f l=%4f\n" (t1-.t0) (t3-.t2);
+  (* Format.eprintf "bl=%a\n" pp r1; *)
+  r1, r2
+;;
+
+let _ = test_build ()
\ No newline at end of file
diff --git a/src/test_discrimination_tree.ml b/src/test_discrimination_tree.ml
index 5da2ef4b..4669150b 100644
--- a/src/test_discrimination_tree.ml
+++ b/src/test_discrimination_tree.ml
@@ -1,6 +1,11 @@
 open Elpi.Internal.Discrimination_tree
+module DT = Elpi.Internal.Discrimination_tree
 open Internal
 
+let test ~expected found = 
+  if expected <> found then failwith (Format.asprintf "Test DT error: Expected %d, but found %d" expected found)
+
+
 let () = assert (k_of (mkConstant ~safe:false ~data:~-17 ~arity:0) == kConstant)
 let () = assert (k_of mkVariable == kVariable)
 let () = assert (k_of mkLam == kOther)
@@ -47,15 +52,15 @@ let () =
     (* Format.printf "%a\n" pp_path pathGoal; *)
     let pathInsts = List.map (fun (x,y) -> x @ [mkPathEnd], y) pathInsts in
     let add_to_trie t (key,value) = 
-      index t (Path.of_list key) value ~time:value in
+      index t (Path.of_list key) value in
     let trie = List.fold_left add_to_trie (empty_dt []) pathInsts in 
-    let retrived = retrieve pathGoal trie in
-    let retrived_nb = List.length retrived in 
+    let retrived = retrieve (fun x y -> y - x) pathGoal trie in
+    let retrived_nb = Elpi.Internal.Bl.length retrived in 
     Format.printf " Retrived clause number is %d\n%!" retrived_nb;
-    let pp_sep = fun f _ -> Format.pp_print_string f " " in
-    Format.printf " Found instances are %a\n%!" (Format.pp_print_list ~pp_sep Format.pp_print_int) retrived;
-    if retrived_nb <> nb then failwith (Format.asprintf "Test DT error: Expected %d clauses, %d found" nb retrived_nb);
-    if List.sort Int.compare retrived |> List.rev <> retrived then failwith "Test DT error: resultin list is not correctly ordered"
+    (* let pp_sep = fun f _ -> Format.pp_print_string f " " in *)
+    (* Format.printf " Found instances are %a\n%!" (Format.pp_print_list ~pp_sep Format.pp_print_int) retrived; *)
+    test retrived_nb nb;
+    if (Elpi.Internal.Bl.to_list retrived |> List.sort Int.compare |> List.rev) <> (retrived |> Elpi.Internal.Bl.to_list) then failwith "Test DT error: resultin list is not correctly ordered"
   in
   
   let p1 = [mkListHead; constA; mkListTailVariable; constA], 1 in                                         (* 1: [a | _] a *)
@@ -70,4 +75,40 @@ let () =
   test [p2; p3; p4; p5; p6] p1 mkOutputMode 3;
   test [p2; p3; p4; p5; p6] p1 mkInputMode 1;
   test [p1; p2; p3; p4; p5; p6; p8] p7 mkOutputMode 3;
-  test [p1; p2; p3; p4; p5; p6; p8] p7 mkInputMode 2;
+  test [p1; p2; p3; p4; p5; p6; p8] p7 mkInputMode 2
+
+let () =  
+  let get_length dt path = DT.retrieve compare path !dt |> Elpi.Internal.Bl.length in
+  let remove dt e = dt := DT.remove (fun x -> x = e) !dt in
+  let index dt path v = dt := DT.index !dt path v in 
+
+  let constA = mkConstant ~safe:false ~data:~-1 ~arity:~-0 in (* a *)
+  let p1 = [mkListHead; constA; mkListTailVariable; constA] in
+  let p2 = [mkListHead; constA; mkListTailVariable; constA; constA] in
+  
+  let p1Index = Path.of_list p1 in (* path for indexing *)
+  let p1Retr = mkInputMode :: p1 |> Path.of_list in (* path for retrival *)
+
+  let p2Index = Path.of_list p2 in (* path for indexing *)
+  let p2Retr = mkInputMode :: p2 |> Path.of_list in (* path for retrival *)
+
+  let dt = DT.empty_dt (List.init 0 Fun.id) |> ref in
+  index dt p1Index 100; index dt p1Index 200;
+  index dt p2Index 200; index dt p2Index 200;
+
+  Printf.printf "Test remove 1\n";
+  test ~expected:2 (get_length dt p1Retr);
+  test ~expected:2 (get_length dt p2Retr);
+
+  Printf.printf "Test remove 2\n";
+  remove dt 100;
+  test ~expected:1 (get_length dt p1Retr);
+  test ~expected:2 (get_length dt p2Retr);
+  
+  Printf.printf "Test remove 3\n";
+  remove dt 100;
+  test ~expected:1 (get_length dt p1Retr);
+
+  Printf.printf "Test remove 4\n";
+  remove dt 200;
+  test ~expected:0 (get_length dt p1Retr)
diff --git a/src/test_lex.ml b/src/test_lex.ml
new file mode 100644
index 00000000..bd074ab1
--- /dev/null
+++ b/src/test_lex.ml
@@ -0,0 +1,30 @@
+open Elpi.Internal.Runtime
+
+let rec sorted = function
+  | [] -> true
+  | [ _ ] -> true
+  | x :: (y :: _ as l) ->
+      let r = lex_insertion x y < 0 in
+      if not r then Format.(eprintf "Not sorted [%a] [%a]\n" (pp_print_list pp_print_int) x (pp_print_list pp_print_int) y);
+      r && sorted l
+
+let () =
+  assert (lex_insertion [] [] = 0);
+
+  (* test 1 *)
+  assert( sorted [ [-1] ; [0]   ; [1;-1]; [1;-2];         [1]   ; [1;2] ; [1;1] ; [2]   ; ]);
+  assert( sorted [ [-1] ; [0]   ; [1;-1]; [1;-2]; [1;-3]; [1]   ; [1;2] ; [1;1] ; [2]   ; ]);
+
+  assert( sorted [ [1;-1]; [2;-2]; ]);
+  assert( sorted [ [-1]; [0]; [1] ]);
+  assert( sorted [ [-2]; [-1]; [0] ]);
+  assert( sorted [ [241]; [242;-1]; [243] ]);
+
+  assert(lex_insertion[243] [242;-1] > 0);
+  assert(lex_insertion [242;-1] [241] > 0);
+  assert(lex_insertion [241] [242;-1] < 0);
+
+  assert(lex_insertion [242;0;9] [242;-1;9] > 0);
+  assert(lex_insertion [242;0;9] [242;-1;8] > 0);
+;; 
+
diff --git a/src/trace_atd.ts b/src/trace_atd.ts
index aebe9608..7bf7fa82 100644
--- a/src/trace_atd.ts
+++ b/src/trace_atd.ts
@@ -1,24 +1,18 @@
-/*
-  Generated by atdts from type definitions in 'trace.atd'.
+// Generated by atdts from type definitions in 'trace.atd'.
+//
+// Type-safe translations from/to JSON
+//
+// For each type 'Foo', there is a pair of functions:
+// - 'writeFoo': convert a 'Foo' value into a JSON-compatible value.
+// - 'readFoo': convert a JSON-compatible value into a TypeScript value
+//   of type 'Foo'.
 
-  Type-safe translations from/to JSON
-
-  For each type 'Foo', there is a pair of functions:
-  - 'writeFoo': convert a 'Foo' value into a JSON-compatible value.
-  - 'readFoo': convert a JSON-compatible value into a TypeScript value
-    of type 'Foo'.
-*/
-
-// eslint-disable-next-line @typescript-eslint/ban-ts-comment
-// @ts-nocheck
-/* tslint:disable */
-/* eslint-disable */
 
 export type Item = {
   kind: Kind[];
-  goal_id: number /*int*/;
-  runtime_id: number /*int*/;
-  step: number /*int*/;
+  goal_id: Int;
+  runtime_id: Int;
+  step: Int;
   name: string;
   payload: string[];
 }
@@ -95,9 +89,9 @@ export type Location =
 
 export type FileLocation = {
   filename: string;
-  line: number /*int*/;
-  column: number /*int*/;
-  character: number /*int*/;
+  line: Int;
+  column: Int;
+  character: Int;
 }
 
 export type Event =
@@ -130,11 +124,11 @@ export type Frame = {
   runtime_id: RuntimeId;
 }
 
-export type GoalId = number /*int*/
+export type GoalId = Int
 
-export type StepId = number /*int*/
+export type StepId = Int
 
-export type RuntimeId = number /*int*/
+export type RuntimeId = Int
 
 export type GoalText = string
 
@@ -792,6 +786,8 @@ export function readChrText(x: any, context: any = x): ChrText {
 // Runtime library
 /////////////////////////////////////////////////////////////////////
 
+export type Int = number
+
 export type Option<T> = null | { value: T }
 
 function _atd_missing_json_field(type_name: string, json_field_name: string) {
@@ -824,7 +820,7 @@ function _atd_bad_ts(expected_type: string, ts_value: any, context: any) {
                   ` Occurs in '${JSON.stringify(context)}'.`)
 }
 
-function _atd_check_json_tuple(len: number /*int*/, x: any, context: any) {
+function _atd_check_json_tuple(len: Int, x: any, context: any) {
   if (! Array.isArray(x) || x.length !== len)
     _atd_bad_json('tuple of length ' + len, x, context);
 }
@@ -847,7 +843,7 @@ function _atd_read_bool(x: any, context: any): boolean {
   }
 }
 
-function _atd_read_int(x: any, context: any): number /*int*/ {
+function _atd_read_int(x: any, context: any): Int {
   if (Number.isInteger(x))
     return x
   else {
@@ -1028,7 +1024,7 @@ function _atd_write_bool(x: any, context: any): boolean {
   }
 }
 
-function _atd_write_int(x: any, context: any): number /*int*/ {
+function _atd_write_int(x: any, context: any): Int {
   if (Number.isInteger(x))
     return x
   else {
@@ -1137,7 +1133,7 @@ function _atd_write_required_field<T>(type_name: string,
 }
 
 function _atd_write_optional_field<T>(write_elt: (x: T, context: any) => any,
-                                      x: T | undefined,
+                                      x: T,
                                       context: any): any {
   if (x === undefined || x === null)
     return x
diff --git a/tests/sources/dt_order.elpi b/tests/sources/dt_order.elpi
new file mode 100644
index 00000000..71bb658d
--- /dev/null
+++ b/tests/sources/dt_order.elpi
@@ -0,0 +1,11 @@
+:index(1 1 _)
+pred f i:bool, i:string, o:int.
+
+:name "a"
+f tt X _ :- halt "what is" X.
+
+:before "a"
+f tt "1" 1.
+
+main :-
+  f tt "1" N.
\ No newline at end of file
diff --git a/tests/sources/dune b/tests/sources/dune
index 21153ec2..26b4643a 100644
--- a/tests/sources/dune
+++ b/tests/sources/dune
@@ -5,7 +5,11 @@
 (executable (name sepcomp4) (modules sepcomp4) (libraries sepcomp))
 (executable (name sepcomp5) (modules sepcomp5) (libraries sepcomp))
 (executable (name sepcomp6) (modules sepcomp6) (libraries sepcomp))
+(executable (name sepcomp7) (modules sepcomp7) (libraries sepcomp))
+(executable (name sepcomp8) (modules sepcomp8) (libraries sepcomp))
+(executable (name sepcomp9) (modules sepcomp9) (libraries sepcomp))
 (executable (name sepcomp_perf1) (modules sepcomp_perf1) (libraries sepcomp))
 (executable (name sepcomp_perf2) (modules sepcomp_perf2) (libraries sepcomp))
 (executable (name sepcomp_perf3) (modules sepcomp_perf3) (libraries sepcomp))
 (executable (name sepcomp_perf4) (modules sepcomp_perf4) (libraries sepcomp))
+(executable (name sepcomp_perf5) (modules sepcomp_perf5) (libraries sepcomp))
diff --git a/tests/sources/findall.elpi b/tests/sources/findall.elpi
index 2bc02d7f..3b7083a7 100644
--- a/tests/sources/findall.elpi
+++ b/tests/sources/findall.elpi
@@ -1,4 +1,5 @@
 pred p o:int, o:int.
+pred q o:int, o:int.
 p 1 1.
 p 1 2.
 p 2 2.
diff --git a/tests/sources/graft_before.elpi b/tests/sources/graft_before.elpi
new file mode 100644
index 00000000..934dc13a
--- /dev/null
+++ b/tests/sources/graft_before.elpi
@@ -0,0 +1,12 @@
+pred p o:int, o:int.
+pred q o:int.
+
+p 0 0.
+
+:name "0" q 0.
+
+p 0 2.
+
+:before "0" p 0 1.
+
+main :- std.findall (p X Y) [p 0 0, p 0 1, p 0 2].
\ No newline at end of file
diff --git a/tests/sources/graft_before_same.elpi b/tests/sources/graft_before_same.elpi
new file mode 100644
index 00000000..bd94d4b7
--- /dev/null
+++ b/tests/sources/graft_before_same.elpi
@@ -0,0 +1,11 @@
+pred p o:int, o:int.
+
+p 0 0.
+
+:name "0" p 0 10.
+
+p 0 2.
+
+:before "0" p 0 1.
+
+main :- std.findall (p X Y) [p 0 0, p 0 1, p 0 10, p 0 2].
\ No newline at end of file
diff --git a/tests/sources/graft_remove.elpi b/tests/sources/graft_remove.elpi
new file mode 100644
index 00000000..be34a57e
--- /dev/null
+++ b/tests/sources/graft_remove.elpi
@@ -0,0 +1,30 @@
+% Classic index
+:index (1) "Map"
+pred p o:int.
+
+:name "p0" p 0.
+
+:remove "p0" p _.
+
+% Dtree
+:index (1) "DTree" 
+pred q o:int.
+
+:name "q0" q 0.
+
+:remove "q0" q _.
+
+% Hmap
+:index (1) "Hash" 
+pred r o:int.
+
+:name "r0" r 0.
+
+:remove "r0" r _.
+
+
+main :- 
+  std.findall (p _) LP, std.assert! (LP = []) "wrong",
+  std.findall (q _) LQ, std.assert! (LQ = []) "wrong",
+  std.findall (r _) LR, std.assert! (LR = []) "wrong",
+  true.
\ No newline at end of file
diff --git a/tests/sources/graft_replace_ok.elpi b/tests/sources/graft_replace_ok.elpi
index ffec625a..718ec402 100644
--- a/tests/sources/graft_replace_ok.elpi
+++ b/tests/sources/graft_replace_ok.elpi
@@ -1,3 +1,4 @@
+:index (1) % "Hash" "DTree"
 pred p o:int.
 :name "replace_me"
 p 1.
@@ -6,4 +7,5 @@ p 1.
 p 2.
 
 main :-
-  std.findall (p _) [p 2].
\ No newline at end of file
+  std.findall (p _) [p 2],
+  std.findall (p 1) [].
\ No newline at end of file
diff --git a/tests/sources/named_clauses00.elpi b/tests/sources/named_clauses00.elpi
index aba6ac6b..2f751656 100644
--- a/tests/sources/named_clauses00.elpi
+++ b/tests/sources/named_clauses00.elpi
@@ -2,6 +2,6 @@
 c1.
 
 :name "name1"
-c2.
+c1.
 
 main.
diff --git a/tests/sources/sepcomp7.ml b/tests/sources/sepcomp7.ml
new file mode 100644
index 00000000..629ba8c5
--- /dev/null
+++ b/tests/sources/sepcomp7.ml
@@ -0,0 +1,14 @@
+let u = {|
+
+:name "this" p 1.
+
+|}
+;;
+
+let () =
+  let open Sepcomp.Sepcomp_template in
+  let elpi = init () in
+  let flags = Elpi.API.Compile.default_flags in
+  let u = cc ~elpi ~flags 0 u in
+  Marshal.to_channel (open_out_bin "_log/sepcomp7.unit") u [];
+  exit 0
diff --git a/tests/sources/sepcomp8.ml b/tests/sources/sepcomp8.ml
new file mode 100644
index 00000000..6b377c5b
--- /dev/null
+++ b/tests/sources/sepcomp8.ml
@@ -0,0 +1,16 @@
+let u = {|
+
+:remove "this" p _.
+
+p 2.
+
+|}
+;;
+
+let () =
+  let open Sepcomp.Sepcomp_template in
+  let elpi = init () in
+  let flags = Elpi.API.Compile.default_flags in
+  let u = cc ~elpi ~flags 0 u in
+  Marshal.to_channel (open_out_bin "_log/sepcomp8.unit") u [];
+  exit 0
diff --git a/tests/sources/sepcomp9.ml b/tests/sources/sepcomp9.ml
new file mode 100644
index 00000000..5360f830
--- /dev/null
+++ b/tests/sources/sepcomp9.ml
@@ -0,0 +1,16 @@
+let u = {|
+
+main :- not(p 1), p 2.
+
+|};
+;;
+
+let () =
+  let open Sepcomp.Sepcomp_template in
+  let elpi = init () in
+  let flags = Elpi.API.Compile.default_flags in
+  let u0 = Marshal.from_channel (open_in_bin "_log/sepcomp7.unit") in
+  let u1 = Marshal.from_channel (open_in_bin "_log/sepcomp8.unit") in
+  let u2 = cc ~elpi ~flags 0 u in
+  let p = link ~elpi [u0;u1;u2] in
+  exec  p
diff --git a/tests/sources/sepcomp_perf5.ml b/tests/sources/sepcomp_perf5.ml
new file mode 100644
index 00000000..98cc2807
--- /dev/null
+++ b/tests/sources/sepcomp_perf5.ml
@@ -0,0 +1,61 @@
+let us = {|
+
+main :- p0.
+
+|}
+
+let ex = {|
+
+p0 :- print "ok".
+p1 :- print "ok".
+p2 :- print "ok".
+p3 :- print "ok".
+p4 :- print "ok".
+p5 :- print "ok".
+p6 :- print "ok".
+p7 :- print "ok".
+p8 :- print "ok".
+p9 :- print "ok".
+
+|}
+
+open Elpi.API
+
+(* XXX 4.06: List.init *)
+let rec list_init i n f =
+  if i >= n then [] else
+  f i :: list_init (i+1) n f
+
+let () =
+  let open Sepcomp.Sepcomp_template in
+  let t0 = Unix.gettimeofday () in
+  let elpi = init () in
+  let flags = Compile.default_flags in
+  let us = cc ~elpi ~flags 1 us in
+  let ex = cc ~elpi ~flags 2 ex in
+  let p = Compile.assemble ~elpi [us] in
+  let t1 = Unix.gettimeofday () in
+  Printf.printf "base: %f\n%!" (t1 -. t0);
+  let exs = list_init 0 50000 (fun _ -> ex) in
+  let rec extend i p =
+    if i = 0 then p
+    else extend (i-1) (Compile.extend ~base:p exs) in
+  let p = extend 2 p in
+  let t2 = Unix.gettimeofday () in
+  Printf.printf "extend: %f\n%!" (t2 -. t1);
+  let q = Compile.query p (Parse.goal_from ~elpi ~loc:(Ast.Loc.initial "g") (Lexing.from_string "main")) in
+  let t3 = Unix.gettimeofday () in
+  Printf.printf "query: %f\n%!" (t3 -. t2);
+  let exe = Compile.optimize q in
+  let t4 = Unix.gettimeofday () in
+  Printf.printf "optimize: %f\n%!" (t4 -. t3);
+  match Execute.once exe with
+  | Execute.Failure -> exit 1
+  | Execute.Success _ ->
+       let t5 = Unix.gettimeofday () in
+       Printf.printf "exec: %f\n%!" (t5 -. t4);
+       exit 0
+  | Execute.NoMoreSteps -> assert false
+
+
+  
\ No newline at end of file
diff --git a/tests/suite/elpi_api.ml b/tests/suite/elpi_api.ml
index 8ebfa76b..e207f39f 100644
--- a/tests/suite/elpi_api.ml
+++ b/tests/suite/elpi_api.ml
@@ -20,7 +20,7 @@ let () = declare "sepcomp2"
 let () = declare "sepcomp3"
   ~source_dune:"sepcomp3.ml"
   ~description:"separate compilation double naming"
-  ~expectation:Test.(FailureOutput (Str.regexp "a clause named xxx already exists"))
+  ~expectation:Test.(FailureOutput (Str.regexp "duplicate clause name xxx"))
   ()
 
 let () = declare "sepcomp4"
@@ -42,3 +42,21 @@ let () = declare "sepcomp6"
   ~expectation:Test.(SuccessOutput (Str.regexp "ok"))
   ()
 
+  let () = declare "sepcomp7"
+  ~source_dune:"sepcomp7.ml"
+  ~description:"separate compilation different processes, with remove (step 1)"
+  ~expectation:Test.Success
+  ()
+
+  let () = declare "sepcomp8"
+  ~source_dune:"sepcomp8.ml"
+  ~description:"separate compilation different processes, with remove (step 2)"
+  ~expectation:Test.Success
+  ()
+
+  let () = declare "sepcomp9"
+  ~source_dune:"sepcomp9.ml"
+  ~description:"separate compilation different processes, with remove (step 3)"
+  ~expectation:Test.Success
+  ()
+
diff --git a/tests/suite/elpi_api_performance.ml b/tests/suite/elpi_api_performance.ml
index 67acd64c..93315c46 100644
--- a/tests/suite/elpi_api_performance.ml
+++ b/tests/suite/elpi_api_performance.ml
@@ -32,3 +32,10 @@ let () = declare "sepcomp_perf4"
   ~description:"separate compilation linker perf"
   ~expectation:Test.Success
   ()
+
+let () = declare "sepcomp_perf5"
+  ~source_dune:"sepcomp_perf5.ml"
+  ~after:"sepcomp_perf5"
+  ~description:"separate compilation linker perf and time distribution"
+  ~expectation:Test.Success
+  ()
diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml
index 5aa3b6e1..6c8ba6ac 100644
--- a/tests/suite/elpi_specific.ml
+++ b/tests/suite/elpi_specific.ml
@@ -311,6 +311,25 @@ let () = declare "graft_replace_err"
   ~expectation:Test.(FailureOutput (Str.regexp "name attribute"))
   ()
 
+let () = declare "graft_remove"
+  ~source_elpi:"graft_remove.elpi"
+  ~description:"remove a clase"
+  ~typecheck:true
+  ()
+
+
+let () = declare "graft_before"
+  ~source_elpi:"graft_before.elpi"
+  ~description:"grafting a clause before the clause of another predicate"
+  ~typecheck:true
+  ()
+
+let () = declare "graft_before_same"
+  ~source_elpi:"graft_before_same.elpi"
+  ~description:"grafting a clause before the clause of the same predicate"
+  ~typecheck:true
+  ()
+
 let () = declare "mk_uv_meta"
   ~source_elpi:"mk-evar-meta.elpi"
   ~description:"uvar surgery at the meta level"
diff --git a/tests/suite/performance_FO.ml b/tests/suite/performance_FO.ml
index eeef8a06..c33e234a 100644
--- a/tests/suite/performance_FO.ml
+++ b/tests/suite/performance_FO.ml
@@ -103,3 +103,7 @@ let () = declare "dt_off"
   ~source_elpi:"dt_bench.elpi"
   ~description:"discrimination_tree on trees"
   ()
+  let () = declare "dt_order"
+  ~source_elpi:"dt_order.elpi"
+  ~description:"discrimination_tree grafting"
+  ()