[dt] (rename mkLam -> mkAny) + some comments

src/discrimination_tree.ml

@@ -45,7 +45,7 @@ let mkConstant ~safe ~data ~arity =
 let mkPrimitive c = encode ~k:kPrimitive ~data:(CData.hash c lsl k_bits) ~arity:0
 
 let mkVariable = encode ~k:kVariable ~data:0 ~arity:0
-let mkLam = encode ~k:kOther ~data:0 ~arity:0
+let mkAny = encode ~k:kOther ~data:0 ~arity:0
 
 (* each argument starts with its mode *)
 let mkInputMode = encode ~k:kOther ~data:1 ~arity:0
@@ -58,7 +58,7 @@ let mkListTailVariableUnif = encode ~k:kOther ~data:7 ~arity:0
 
 
 let isVariable x = x == mkVariable
-let isLam x = x == mkLam
+let isAny x = x == mkAny
 let isInput x = x == mkInputMode
 let isOutput x = x == mkOutputMode
 let isListHead x = x == mkListHead
@@ -85,7 +85,7 @@ let pp_cell fmt n =
        else if isListEnd n then "ListEnd"
        else if isPathEnd n then "PathEnd"
        else if isListTailVariableUnif n then "ListTailVariableUnif"
-       else if isLam n then "Other"
+       else if isAny n then "Other"
        else failwith "Invalid path construct...")
   else if k == kPrimitive then Format.fprintf fmt "Primitive"
   else Format.fprintf fmt "%o" k
@@ -184,7 +184,7 @@ module Trie = struct
     let max = ref 0 in
     let rec ins ~pos = let x = Path.get a pos in function
       | Node ({ data } as t) when isPathEnd x -> max := pos; Node { t with data = v :: data }
-      | Node ({ other } as t) when isVariable x || isLam x ->
+      | Node ({ other } as t) when isVariable x || isAny x ->
           let t' = match other with None -> empty | Some x -> x in
           let t'' = ins ~pos:(pos+1) t' in
           Node { t with other = Some t'' }
@@ -328,7 +328,7 @@ 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 get_all_children v mode = isLam v || (isVariable v && isOutput mode)
+let get_all_children v mode = isAny v || (isVariable v && isOutput mode)
 
 let rec retrieve ~pos ~add_result mode path tree : unit =
   let hd = Path.get path pos in
@@ -412,7 +412,7 @@ module Internal = struct
   let data_of = data_of
 
   let isVariable = isVariable
-  let isLam = isLam
+  let isAny = isAny
   let isInput = isInput
   let isOutput = isOutput
   let isListHead = isListHead

src/discrimination_tree.mli

@@ -13,25 +13,63 @@ end
 
 val mkConstant : safe:bool -> data:int -> arity:int -> cell
 val mkPrimitive : Elpi_util.Util.CData.t -> cell
+
+(** This is for: unification variables, discard *)
 val mkVariable : cell
-val mkLam : cell
+
+(** This is for: 
+  - lambda-abstractions: DT does not perform HO unification, nor βη-redex unif
+  - too big terms: if the path of the goal is bigger then the max path in the
+                   rules, each term is replaced with this constructor. Note that
+                   we do not use mkVariable, since in input mode a variable
+                   cannot be unified with non-flex terms. In DT, mkAny is
+                   unified with anything
+*)
+val mkAny : cell
 val mkInputMode : cell
 val mkOutputMode : cell
+
+(** This is for the last term of opened lists.
+
+  If the list ends is [1,2|X] == Cons (CData'1',Cons(CData'2',Arg (_, _)))
+
+  The corresponding path will be: ListHead, Primitive, Primitive,
+  ListTailVariable
+
+  ListTailVariable is considered as a variable, and if it appears in a goal in
+  input position, it cannot be unified with non-flex terms
+*)
 val mkListTailVariable : cell
+
+(** This is used for capped lists.
+
+  If the length of the maximal list in the rules of a predicate is N, then any
+  (sub-)list in the goal longer then N encodes the first N elements in the path
+  and the last are replaced with ListTailVariableUnif.
+
+  The main difference with ListTailVariable is that DT will unify this symbol to
+  both flex and non-flex terms in the path of rules
+*)
 val mkListTailVariableUnif : cell
 val mkListHead : cell
 val mkListEnd : cell
+
+(** This is padding used to fill the array in paths and indicate the retrieve
+      function to stop making unification. 
+
+    Note that the array for the path has a length which is doubled each time the
+    terms in it are larger then the forseen length. Each time the array is
+    doubled, the new cells are filled with PathEnd.
+*)
 val mkPathEnd : cell
 
 type 'a t
 
-(** [index dt path value ~time] returns a new discrimination tree starting from [dt]
-      where [value] is added wrt its [path]. [~time] is used as a priority
-      marker between two rules.
-
-    A rule with a given [~time] has higher priority on other rules with lower [~time]
+(** [index dt ~max_list_length path value] returns a new discrimination tree
+      starting from [dt] where [value] is added wrt its [path].
 
-    @note: in the elpi runtime, there are no two rule having the same [~time]
+    [max_list_length] is provided and used to update (if needed) the length of
+    the longest list in the received path.
 *)
 val index : 'a t -> max_list_length:int -> Path.t -> 'a -> 'a t
 
@@ -41,16 +79,15 @@ val max_depths : 'a t -> int array
 
 val empty_dt : 'b list -> 'a t
 
-(** [retrive path dt] Retrives all values in a discrimination tree [dt] from a given path [p].
+(** [retrive cmp path dt] Retrives all values in a discrimination tree [dt] from
+    a given path [p].
 
-  The retrival algorithm performs a light unification between [p] and the 
-  nodes in the discrimination tree. This light unification takes care of
-  unification variables that can be either in the path or in the nodes of [dt]
+  The retrival algorithm performs a light unification between [p] and the nodes
+  in the discrimination tree. This light unification takes care of unification
+  variables that can be either in the path or in the nodes of [dt]
 
-  The returned list of values are sorted wrt to the order in which values are
-  added in the tree: given two rules r_1 and r_2 with same path, if r_1
-  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
+  The returned list is sorted wrt [cmp] so that rules are given in the expected
+  order
 *)
 val retrieve : ('a -> 'a -> int) -> Path.t -> 'a t -> 'a Bl.scan
 
@@ -82,7 +119,7 @@ module Internal: sig
   val data_of : cell -> int
 
   val isVariable : cell -> bool
-  val isLam : cell -> bool
+  val isAny : cell -> bool
   val isInput : cell -> bool
   val isOutput : cell -> bool
   val isListHead : cell -> bool

src/runtime.ml

@@ -2607,7 +2607,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m
   and main ~safe ~depth t path_depth : unit =
     if path_depth = 0 then update_current_min_depth path_depth
     else if is_goal && Path.get_builder_pos path >= path_length then 
-      (Path.emit path mkLam; update_current_min_depth path_depth)
+      (Path.emit path mkAny; update_current_min_depth path_depth)
     else
       let path_depth = path_depth - 1 in 
       match deref_head ~depth t with 
@@ -2617,7 +2617,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m
       | CData d -> Path.emit path @@ mkPrimitive d; update_current_min_depth path_depth
       | App (k,_,_) when k == Global_symbols.uvarc -> Path.emit path @@ mkVariable; update_current_min_depth path_depth
       | App (k,a,_) when k == Global_symbols.asc -> main ~safe ~depth a (path_depth+1)
-      | Lam _ -> Path.emit path @@ mkLam; update_current_min_depth path_depth (* loose indexing to enable eta *)
+      | Lam _ -> Path.emit path mkAny; update_current_min_depth path_depth (* loose indexing to enable eta *)
       | Arg _ | UVar _ | AppArg _ | AppUVar _ | Discard -> Path.emit path @@ mkVariable; update_current_min_depth path_depth
       | Builtin (k,tl) ->
         Path.emit path @@ mkConstant ~safe ~data:k ~arity:(if path_depth = 0 then 0 else List.length tl);

src/test_discrimination_tree.ml

@@ -8,7 +8,7 @@ let test ~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)
+let () = assert (k_of mkAny == kOther)
 let () =
   let open Elpi.API in
   match RawData.look ~depth:0 (RawOpaqueData.of_int 4) with
@@ -18,7 +18,7 @@ let () =
 
 let () = assert (arity_of (mkConstant ~safe:false ~data:~-17 ~arity:3) == 3)
 let () = assert (arity_of mkVariable == 0)
-let () = assert (arity_of mkLam == 0)
+let () = assert (arity_of mkAny == 0)
 let () = assert (arity_of mkInputMode == 0)
 let () = assert (arity_of mkOutputMode == 0)
 let () = assert (arity_of mkListTailVariable == 0)
@@ -67,7 +67,7 @@ let () =
   let p2 = [mkListHead; constA; mkName 0; mkName 1; mkName 2; mkListEnd; constA], 2 in                    (* 2: [a,x0,x1,x3] a *)
   let p3 = [mkListHead; constA; mkName 0; mkName 1; mkName 2; mkListEnd; mkVariable], 3 in                (* 3: [a,x0,x1,x3] X *)
   let p4 = [mkListHead; constA; mkName 0; mkName 1; mkName 2; constA; mkListEnd], 4 in                    (* 4: [a,x0,x1,x3,a] *)
-  let p5 = [mkLam; mkVariable], 5 in                                                                    (* 5: (x\ ...) X *)
+  let p5 = [mkAny; mkVariable], 5 in                                                                    (* 5: (x\ ...) X *)
   let p6 = [mkListHead; constF; mkListHead; mkName 1; mkName 2; mkListTailVariable; constA; mkListEnd], 6 in (* 6: [f [x1, x2 | _] a] f *)
   let p7 = [mkListHead; constA; mkVariable; mkListEnd; constA], 7 in                                      (* 7: [a,X] a *)
   let p8 = [mkListHead; constA; mkName 0; mkListEnd; mkVariable], 8 in                                    (* 8: [a,x0] X *)