Indexing via discrimination tree (#205)

Author: FissoreD

.github/workflows/main.yml

@@ -83,13 +83,12 @@ jobs:
           opam exec -- cygpath -m ${{ github.workspace }} | % {$_ -replace "^","workspace=" }  | Out-File -FilePath $Env:GITHUB_ENV -Encoding utf8 -Append
           opam exec -- cygpath -m "$Env:CYGWIN_ROOT" | % {$_ -replace "^","cygwin_root=" }  | Out-File -FilePath $Env:GITHUB_ENV -Encoding utf8 -Append
           opam exec -- sed -i ' ' tests/sources/*.elpi
-          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -q -P time
-          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -q -P which
-          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -q -P wdiff
-          opam exec -- which which
-          opam exec -- time which
-          opam exec -- which time
-          opam exec -- which wdiff
+          & "$Env:CYGWIN_ROOT/setup-x86_64.exe" -v -q -P time,which,wdiff
+
+#          opam exec -- which which
+#          opam exec -- time which
+#          opam exec -- which time
+#          opam exec -- which wdiff
 
 # Build ######################################################################
 #

.ocamlformat

@@ -7,6 +7,10 @@ API:
 Library:
   - New `std.fold-right`
 
+Runtime:
+  - New clause retrieval through discrimination tree. This new index is enabled
+    whenever the `:index` directive selects only one argument  with a depth `> 1`.
+
 # v1.18.0 (October 2023)
 
 Requires Menhir 20211230 and OCaml 4.08 or above.

CHANGES.md

@@ -66,7 +66,7 @@ trivial-facts :-
 ```
 
 Side note: no solution is computed for goals like `_ = something`.
-On the contrary a problem like `DummyNameUsedOnlyOnce = somthing` demands the
+On the contrary a problem like `DummyNameUsedOnlyOnce = something` demands the
 computation of the solution (even if it is not used), and hence can *fail* if
 some variable occurring in something is out of scope for `DummyNameUsedOnlyOnce`.
 
@@ -308,8 +308,20 @@ If only one argument is indexed, and it is indexed at depth one, then Elpi uses
 a standard indexing technique based on a perfect (for depth 1) search tree. This
 means that no false positives are returned by the index.
 
-If more than one argument is indexed, or if some argument is indexed at depth
-greater than 1, then Elpi uses an index based on the idea of
+### Discrimination tree index
+
+If only one argument is indexed at depth greater than one, then Elpi uses
+a [discrimination tree](https://www.cs.cmu.edu/~fp/courses/99-atp/lectures/lecture28.html).
+Both the rule argument and the goal argument are
+indexed up to the given depth. The indexing is not perfect, false positives may
+be returned and ruled out by unification.
+
+Indexed terms are linearized into paths. Paths are inserted into a trie data
+structure sharing common prefixes.
+
+### Hash based index
+
+If more than one argument is indexed then Elpi uses an index based on the idea of
 [unification hashes](http://blog.ndrix.com/2013/03/prolog-unification-hashes.html).
 
 ```prolog
@@ -618,7 +630,7 @@ syntax `{{:name` .. `}}` where `name` is any non-space or `\n` character.
 Quotations are elaborated before run-time.
 
 The [coq-elpi](https://github.com/LPCIC/coq-elpi) software embeds elpi 
-in Coq and provides a quatation for its terms. For example
+in Coq and provides a quotation for its terms. For example
 ```prolog
 {{ nat -> bool }}
 ```

ELPI.md

@@ -1,7 +1,7 @@
 Known incompatibilities with Teyjus
 ===================================
 
-This file tries to summarise known incompatibilities between Elpi and Teyjus.
+This file tries to summarize known incompatibilities between Elpi and Teyjus.
 
 # Semantics
 
@@ -37,7 +37,7 @@ This file tries to summarise known incompatibilities between Elpi and Teyjus.
 - Module signatures are ignored.
 - Elpi accumulates each file once; Teyjus does it multiple times, that is
   always bad (all clauses are duplicated and tried multiple times, that is
-  rarely the expected behaviour).
+  rarely the expected behavior).
 - Elpi understands relative paths as in `accumulate "../foo"`: resolution
   of relative paths is done according to the path of the accumulating file
   first or, if it fails, according to the TJPATH.

INCOMPATIBILITIES.md

@@ -134,7 +134,7 @@ The elaborator manipulates terms with binders and holes
 (unification variables) representing missing piece of 
 information.  Some of them have to be filled in order 
 to make the term well typed. Some others are filled in because 
-the user has programmed the eleborator to do so, e.g. ad-hoc polymorphism.
+the user has programmed the elaborator to do so, e.g. ad-hoc polymorphism.
 
 Such software component is characterized by an high complexity
 coming from the interplay of binders, reduction and unification,

README.md

@@ -1233,6 +1233,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
          Loc.show (snd (C.Map.find name map)) ^ ")")
 
   let compile_mode (state, modes) { Ast.Mode.name; args; loc } =
+    let args = List.map to_mode args in
     let state, mname = funct_of_ast state name in
     check_duplicate_mode state mname (args,loc) modes;
     state, C.Map.add mname (args,loc) modes
@@ -1356,7 +1357,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
       (state : State.t), lcs, active_macros,
       { Structured.types; type_abbrevs; modes; body; symbols }
 
-    and compile_body macros types type_abbrevs modes lcs defs state = function
+    and compile_body macros types type_abbrevs (modes : (mode * Loc.t) C.Map.t) lcs defs state = function
       | [] -> lcs, state, types, type_abbrevs, modes, defs, []
       | Locals (nlist, p) :: rest ->
           let orig_varmap = get_varmap state in
@@ -1673,11 +1674,11 @@ module Spill : sig
 
 
   val spill_clause :
-    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> bool list) ->
+    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> mode) ->
       (preterm, 'a) Ast.Clause.t -> (preterm, 'a) Ast.Clause.t
 
   val spill_chr :
-    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> bool list) ->
+    State.t -> types:Structured.typ list C.Map.t -> modes:(constant -> mode) ->
       (constant list * prechr_rule list) -> (constant list * prechr_rule list)
 
   (* Exported to compile the query *)
@@ -1727,7 +1728,7 @@ end = struct (* {{{ *)
       | `Arrow(arity,_),_ ->
           let missing = arity - nargs in
           let output_suffix =
-            let rec aux = function false :: l -> 1 + aux l | _ -> 0 in
+            let rec aux = function Output :: l -> 1 + aux l | _ -> 0 in
             aux (List.rev mode) in
           if missing > output_suffix then
             error ~loc Printf.(sprintf
@@ -2358,14 +2359,13 @@ let compile_clause modes initial_depth state
   state, cl
 
 let chose_indexing state predicate l =
-  let rec all_zero = function
-    | [] -> true
-    | 0 :: l -> all_zero l
-    | _ -> false in
-  let rec aux n = function
+  let all_zero = List.for_all ((=) 0) in
+  let rec aux argno = function
+    (* TODO: @FissoreD here we should raise an error if n > arity of the predicate? *)
     | [] -> error ("Wrong indexing for " ^ Symbols.show state predicate)
-    | 0 :: l -> aux (n+1) l
-    | 1 :: l when all_zero l -> MapOn n
+    | 0 :: l -> aux (argno+1) l
+    | 1 :: l when all_zero l -> MapOn argno
+    | path_depth :: l when all_zero l -> Trie { argno ; path_depth }
     | _ -> Hash l
   in
     aux 0 l

src/compiler.ml

@@ -53,6 +53,7 @@ module Constants : sig
   module Set : Set.S with type elt = constant
   val pp : Format.formatter -> t -> unit
   val show : t -> string
+  val compare : t -> t -> int
 end = struct
 
 module Self = struct
@@ -115,6 +116,25 @@ let uvar_isnt_a_blocker { uid_private } = uid_private > 0 [@@inline];;
 let uvar_set_blocker r   = r.uid_private <- -(uvar_id r) [@@inline];;
 let uvar_unset_blocker r = r.uid_private <-  (uvar_id r) [@@inline];;
 
+type arg_mode = Util.arg_mode = Input | Output [@@deriving show]
+
+type clause = {
+    depth : int;
+    args : term list;
+    hyps : term list;
+    vars : int;
+    mode : mode;        (* CACHE to avoid allocation in get_clauses *)
+    loc : Loc.t option; (* debug *)
+}
+and 
+mode = arg_mode list
+[@@deriving show]
+
+let to_mode = function true -> Input | false -> Output
+
+
+module DT = Discrimination_tree
+
 type stuck_goal = {
   mutable blockers : blockers;
   kind : unification_def stuck_goal_kind;
@@ -138,25 +158,23 @@ 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 *)
+    time : int;                             (* time is used to recover the total order *)
     args_idx : (clause * int) list Ptmap.t; (* clause, insertion time *)
   }
-and clause = {
-    depth : int;
-    args : term list;
-    hyps : term list;
-    vars : int;
-    mode : mode; (* CACHE to avoid allocation in get_clauses *)
-    loc : Loc.t option; (* debug *)
+| IndexWithTrie of {
+    mode : mode;
+    argno : int;        (* position of argument on which the trie is built *)
+    path_depth : int;   (* depth bound at which the term is inspected *)
+    time : int;         (* time is used to recover the total order *)
+    args_idx : clause DT.t; 
 }
-and mode = bool list (* true=input, false=output *)
 [@@deriving show]
 
 type constraints = stuck_goal list
@@ -167,9 +185,19 @@ type suspended_goal = {
   goal : int * term
 }
 
+(** 
+  Used to index the parameters of a predicate P
+  - [MapOn N] -> N-th argument at depth 1 (head symbol only)
+  - [Hash L]  -> L is the list of depths given by the urer for the parameters of
+                 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
+  - [IndexWithTrie N D] -> N-th argument at D depth
+*)
 type indexing =
   | MapOn of int
   | Hash of int list
+  | Trie of { argno : int; path_depth : int }
 [@@deriving show]
 
 let mkLam x = Lam x [@@inline]