cleanup

src/compiler.ml

@@ -2405,9 +2405,9 @@ let chose_indexing state predicate l k =
     | _ -> default ()
   in
   match k with
-  | Some Ast.Structured.DiscriminationTree -> Trie l
+  | Some Ast.Structured.DiscriminationTree -> DiscriminationTree l
   | Some HashMap -> Hash l
-  | None -> check_map (fun () -> Trie l) 0 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

src/data.ml

@@ -168,7 +168,7 @@ and second_lvl_idx =
     time : int;                             (* time is used to recover the total order *)
     args_idx : (clause * int) list Ptmap.t; (* clause, insertion time *)
   }
-| IndexWithTrie of {
+| 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 *)
@@ -191,13 +191,14 @@ type suspended_goal = {
                  P. Indexing is done by hashing all the parameters with a non
                  zero depth and comparing it with the hashing of the parameters
                  of the query
-  - [Trie L] -> we use the same logic of Hash, except we use Trie to discriminate
-                clauses
+  - [DiscriminationTree L] ->
+            we use the same logic of Hash, except we use DiscriminationTree to discriminate
+            clauses
 *)
 type indexing =
   | MapOn of int
   | Hash of int list
-  | Trie of int list
+  | DiscriminationTree of int list
 [@@deriving show]
 
 let mkLam x = Lam x [@@inline]

src/runtime.ml

@@ -2545,10 +2545,10 @@ let add1clause ~depth m (predicate,clause) =
          time = time + 1;
          args_idx = Ptmap.add hash ((clause,time) :: clauses) args_idx
        }) m
-  | IndexWithTrie {mode; arg_depths; args_idx; time } ->
+  | IndexWithDiscriminationTree {mode; arg_depths; args_idx; time } ->
       let path = arg_to_trie_path ~depth ~safe:true false clause.args arg_depths mode in
       let dt = DT.index args_idx path clause ~time in
-        Ptmap.add predicate (IndexWithTrie {
+        Ptmap.add predicate (IndexWithDiscriminationTree {
           mode; arg_depths;
           time = time+1;
           args_idx = dt
@@ -2600,7 +2600,7 @@ let make_index ~depth ~indexing ~clauses_rev:p =
           flex_arg_clauses = [];
           arg_idx = Ptmap.empty;
         }
-      | Trie arg_depths -> IndexWithTrie {
+      | DiscriminationTree arg_depths -> IndexWithDiscriminationTree {
           arg_depths;  mode; 
           args_idx = DT.empty;
           time = min_int;
@@ -2678,7 +2678,7 @@ let get_clauses ~depth predicate goal { index = m } =
        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))
-     | IndexWithTrie {arg_depths; mode; args_idx} ->
+     | IndexWithDiscriminationTree {arg_depths; mode; args_idx} ->
         let path = arg_to_trie_path ~safe:false ~depth true (trie_goal_args goal) arg_depths mode in
         [%spy "dev:disc-tree:path" ~rid 
           Discrimination_tree.pp_path path
@@ -2906,7 +2906,7 @@ let clausify ~loc { index } ~depth t =
     match Ptmap.find x index with
     | TwoLevelIndex { mode } -> mode
     | BitHash { mode } -> mode
-    | IndexWithTrie { mode } -> mode
+    | IndexWithDiscriminationTree { mode } -> mode
     | exception Not_found -> [] in
   let l = split_conj ~depth t in
   let clauses, program, lcs =