From d7865f890667e633512abffd9ff384ae7b5157f4 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 22 Oct 2024 23:10:48 +0200 Subject: [PATCH 1/5] Fix bug #272 (forgot parens...) --- src/runtime.ml | 4 ++-- tests/sources/dt_bug272.elpi | 23 +++++++++++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) create mode 100644 tests/sources/dt_bug272.elpi diff --git a/src/runtime.ml b/src/runtime.ml index f1e45a9fc..8d5557deb 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2508,8 +2508,8 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar arg_mo (* up to the 30^th elemebt *) if h > 30 then (Path.emit path mkListEnd; update_current_min_depth path_depth) else - main ~safe ~depth a path_depth; - list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b + (main ~safe ~depth a path_depth; + list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b) (* These cases can come from terms like `[_ | _]`, `[_ | A]` ... *) | UVar _ | AppUVar _ | Arg _ | AppArg _ | Discard -> Path.emit path mkListTailVariable; update_current_min_depth path_depth diff --git a/tests/sources/dt_bug272.elpi b/tests/sources/dt_bug272.elpi new file mode 100644 index 000000000..ba127e691 --- /dev/null +++ b/tests/sources/dt_bug272.elpi @@ -0,0 +1,23 @@ +:index(1 1) +pred map2 i:list A, i:list B, i:(A -> B -> C -> o), o:list C. +map2 [] [] _ []. +map2 [A|As] [B|Bs] F [C|Cs] :- F A B C, map2 As Bs F Cs. + +pred any_list i:int, o:list int. +any_list 0 [] :- !. +any_list N [N|L] :- any_list {calc (N - 1)} L. + +pred any_pred i:int, i:int, o:int. +any_pred A B R :- R is A + B. + +pred test i:int, o:list int. +test N R :- any_list N L, map2 L L any_pred R. + +pred loop i:int, i:int. +loop N N :- !. +loop N M :- + test N _, + N1 is N + 1, + loop N1 M. + +main :- loop 1 100. \ No newline at end of file From df4e7ff0111738a150d424a5377c26a477b7cb10 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Oct 2024 09:34:30 +0200 Subject: [PATCH 2/5] Update correctness_HO.ml --- tests/suite/correctness_HO.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tests/suite/correctness_HO.ml b/tests/suite/correctness_HO.ml index df45bfd04..d30df9eae 100644 --- a/tests/suite/correctness_HO.ml +++ b/tests/suite/correctness_HO.ml @@ -348,3 +348,11 @@ let () = declare "chr_with_hypotheses" ~typecheck:true ~expectation:Success () + +let () = declare "bug_272" + ~source_elpi:"dt_bug272.elpi" + ~description:"dt list truncation heuristic" + ~typecheck:true + ~expectation:Success + () + From cd96e8e80869b1e422cda287cc7e86f3094042b7 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Wed, 23 Oct 2024 14:04:28 +0200 Subject: [PATCH 3/5] [dt] heuristic on list length in paths --- src/discrimination_tree.ml | 24 ++++++--------- src/discrimination_tree.mli | 4 ++- src/runtime.ml | 53 ++++++++++++++++++++++++++------- src/test_discrimination_tree.ml | 2 +- 4 files changed, 56 insertions(+), 27 deletions(-) diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml index ecede752a..ca2a3295b 100644 --- a/src/discrimination_tree.ml +++ b/src/discrimination_tree.ml @@ -87,21 +87,14 @@ let pp_cell fmt n = else Format.fprintf fmt "%o" k let show_cell n = Format.asprintf "%a" pp_cell n -module Path : sig - type t - val pp : Format.formatter -> t -> unit - val get : t -> int -> cell - type builder - val make : int -> cell -> builder - val emit : builder -> cell -> unit - val stop : builder -> t - val of_list : cell list -> t - -end = struct + +module Path = struct type t = cell array [@@deriving show] let get a i = a.(i) + type builder = { mutable pos : int; mutable path : cell array } + let get_builder_pos {pos} = pos let make size e = { pos = 0; path = Array.make size e } let rec emit p e = let len = Array.length p.path in @@ -285,17 +278,18 @@ let skip_listTailVariable ~pos path : 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 Trie.t; max_size : int; max_depths : int array } +type 'a t = {t: 'a Trie.t; max_size : int; max_depths : int array; max_list_length: int } 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 = +let index { t; max_size; max_depths; max_list_length = mll } ~max_list_length path data = let t, m = Trie.add path data t in - { t; max_size = max max_size m; max_depths } + { t; max_size = max max_size m; max_depths; max_list_length = max max_list_length mll } let max_path { max_size } = max_size let max_depths { max_depths } = max_depths +let max_list_length { max_list_length } = max_list_length (* the equivalent of skip, but on the index, thus the list of trees that are rooted just after the term represented by the tree root @@ -389,7 +383,7 @@ and on_all_children ~pos ~add_result mode path map = let empty_dt args_depth : 'a t = let max_depths = Array.make (List.length args_depth) 0 in - {t = Trie.empty; max_depths; max_size = 0} + {t = Trie.empty; max_depths; max_size = 0; max_list_length=0} let retrieve ~pos ~add_result path index = let mode = Path.get path pos in diff --git a/src/discrimination_tree.mli b/src/discrimination_tree.mli index f4ca6c2bf..6e7597bbb 100644 --- a/src/discrimination_tree.mli +++ b/src/discrimination_tree.mli @@ -4,6 +4,7 @@ module Path : sig val pp : Format.formatter -> t -> unit val get : t -> int -> cell type builder + val get_builder_pos : builder -> int val make : int -> cell -> builder val emit : builder -> cell -> unit val stop : builder -> t @@ -31,9 +32,10 @@ type 'a t @note: in the elpi runtime, there are no two rule having the same [~time] *) -val index : 'a t -> Path.t -> 'a -> 'a t +val index : 'a t -> max_list_length:int -> Path.t -> 'a -> 'a t val max_path : 'a t -> int +val max_list_length : 'a t -> int val max_depths : 'a t -> int array val empty_dt : 'b list -> 'a t diff --git a/src/runtime.ml b/src/runtime.ml index 493a284f7..eb03d25dc 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2507,8 +2507,33 @@ let hash_arg_list is_goal hd ~depth args mode spec = let hash_clause_arg_list = hash_arg_list false let hash_goal_arg_list = hash_arg_list true +(* returns the maximal length of any sub_list + this operation is done at compile time per each clause being index + for example the term (app['a','b',app['c','d','e'], 'f', app['a','b','c','d','e','f']]) + has three lists L1 = ['a','b',app['c','d','e'], 'f', app['a','b','c','d','e','f'] + L2 = ['c','d','e'] + L3 = app['a','b','c','d','e','f'] + and the longest one has length 6 +*) +let rec max_list_length acc = function + | Nil -> acc + | Cons (a, (UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _)|AppArg (_, _))) -> + let alen = max_list_length 0 a in + max (acc+2) alen + | Cons (a, b)-> + let alen = max_list_length 0 a in + let blen = max_list_length (acc+1) b in + max blen alen + | App (_,x,xs) -> List.fold_left (fun acc x -> max acc (max_list_length 0 x)) acc (x::xs) + | Builtin (_, xs) -> List.fold_left (fun acc x -> max acc (max_list_length 0 x)) acc xs + | Lam t -> max_list_length acc t + | Discard | Const _ |CData _ -> acc + | UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _)|AppArg (_, _) -> acc + +let max_lists_length = List.fold_left (fun acc e -> max (max_list_length 0 e) acc) 0 + (** - [arg_to_trie_path ~safe ~depth ~is_goal args arg_depths arg_modes] + [arg_to_trie_path ~safe ~depth ~is_goal args arg_depths arg_modes mp max_list_length] returns the path represetation of a term to be used in indexing with trie. args, args_depths and arg_modes are the lists of respectively the arguments, the depths and the modes of the current term to be indexed. @@ -2517,10 +2542,14 @@ let hash_goal_arg_list = hash_arg_list true In the former case, each argument we add a special mkInputMode/mkOutputMode node before each argument to be indexed. This special node is used during instance retrival to know the mode of the current argument + - mp is the max_path size of any path in the index used to truncate the goal + - max_list_length is the length of the longest sublist in each term of args *) -let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode mp : Discrimination_tree.Path.t = +let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode mp (max_list_length':int) : Discrimination_tree.Path.t = let open Discrimination_tree in - let path = Path.make (max mp 8) mkPathEnd in + + let path_length = mp + Array.length args_depths_ar + 1 in + let path = Path.make path_length mkPathEnd in let current_ar_pos = ref 0 in let current_user_depth = ref 0 in @@ -2537,7 +2566,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m end in - let rec list_to_trie_path ~safe ~depth ?(h=0) path_depth (len: int) (t: term) : unit = + let rec list_to_trie_path ~safe ~depth ~h path_depth (len: int) (t: term) : unit = match deref_head ~depth t with | Nil -> Path.emit path mkListEnd; update_current_min_depth path_depth | Cons (a, b) -> @@ -2549,7 +2578,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m (* has the node `app` with arity `1` as first*) (* cell, then come the elment of the list *) (* up to the 30^th elemebt *) - if h > 30 then (Path.emit path mkListEnd; update_current_min_depth path_depth) + if is_goal && h >= max_list_length' then (Path.emit path mkListEnd; update_current_min_depth path_depth) else (main ~safe ~depth a path_depth; list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b) @@ -2578,6 +2607,8 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m (** gives the path representation of a term *) and main ~safe ~depth t path_depth : unit = if path_depth = 0 then update_current_min_depth path_depth + else if Path.get_builder_pos path >= path_length then + (Path.emit path mkVariable; update_current_min_depth path_depth) else let path_depth = path_depth - 1 in match deref_head ~depth t with @@ -2601,7 +2632,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m | Cons (x,xs) -> Path.emit path mkListHead; main ~safe ~depth x (path_depth + 1); - list_to_trie_path ~safe ~depth (path_depth + 1) 0 xs + list_to_trie_path ~safe ~depth ~h:1 (path_depth + 1) 0 xs (** builds the sub-path of a sublist of arguments of the current clause *) and make_sub_path arg_hd arg_tl arg_depth_hd arg_depth_tl mode_hd mode_tl = @@ -2689,9 +2720,10 @@ let add_clause_to_snd_lvl_idx ~depth ~insert predicate clause = function | 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 + let max_list_length = max_lists_length clause.args in + let path = arg_to_trie_path ~depth ~safe:true ~is_goal:false clause.args arg_depths max_depths mode max_path max_list_length 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 + let args_idx = Discrimination_tree.index args_idx path clause ~max_list_length in IndexWithDiscriminationTree { mode; arg_depths; args_idx = args_idx @@ -2899,8 +2931,9 @@ let get_clauses ~depth predicate goal { index = { idx = m } } = | 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 - let (path: Discrimination_tree.Path.t) = arg_to_trie_path ~safe:false ~depth ~is_goal:true (trie_goal_args goal) arg_depths max_depths mode max_path in - [%spy "dev:disc-tree:depth-path" ~rid pp_string "Goal: MaxDepths " (pplist pp_int ";") (Array.to_list max_depths)]; + let max_list_length = Discrimination_tree.max_list_length args_idx in + let path = arg_to_trie_path ~safe:false ~depth ~is_goal:true (trie_goal_args goal) arg_depths max_depths mode max_path max_list_length in + [%spy "dev:disc-tree:depth-path" ~rid pp_string "Goal: MaxDepths " (pplist pp_int ";") (Array.to_list max_depths) pp_int (max_path) pp_int max_list_length]; (* Format.(printf "Goal: MaxDepth is %a\n" (pp_print_list ~pp_sep:(fun fmt _ -> pp_print_string fmt " ") pp_print_int) (Discrimination_tree.max_depths args_idx |> Array.to_list)); *) [%spy "dev:disc-tree:path" ~rid Discrimination_tree.Path.pp path diff --git a/src/test_discrimination_tree.ml b/src/test_discrimination_tree.ml index 4669150b6..593a9b39a 100644 --- a/src/test_discrimination_tree.ml +++ b/src/test_discrimination_tree.ml @@ -52,7 +52,7 @@ 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 in + index t (Path.of_list key) ~max_list_length:1000 value in let trie = List.fold_left add_to_trie (empty_dt []) pathInsts in let retrived = retrieve (fun x y -> y - x) pathGoal trie in let retrived_nb = Elpi.Internal.Bl.length retrived in From 5b8c96a6f05ac8b0df08f2220a841b846f2580df Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Wed, 23 Oct 2024 17:54:45 +0200 Subject: [PATCH 4/5] [dt] ListTailVariableUnif + max_term_width (all tests pass) --- src/discrimination_tree.ml | 15 ++++++++++----- src/discrimination_tree.mli | 2 ++ src/runtime.ml | 15 ++++++++------- src/test_discrimination_tree.ml | 2 +- tests/suite/correctness_HO.ml | 2 +- 5 files changed, 22 insertions(+), 14 deletions(-) diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml index ca2a3295b..926ea031c 100644 --- a/src/discrimination_tree.ml +++ b/src/discrimination_tree.ml @@ -54,6 +54,7 @@ let mkListTailVariable = encode ~k:kOther ~data:3 ~arity:0 let mkListHead = encode ~k:kOther ~data:4 ~arity:0 let mkListEnd = encode ~k:kOther ~data:5 ~arity:0 let mkPathEnd = encode ~k:kOther ~data:6 ~arity:0 +let mkListTailVariableUnif = encode ~k:kOther ~data:7 ~arity:0 let isVariable x = x == mkVariable @@ -63,6 +64,7 @@ let isOutput x = x == mkOutputMode let isListHead x = x == mkListHead let isListEnd x = x == mkListEnd let isListTailVariable x = x == mkListTailVariable +let isListTailVariableUnif x = x == mkListTailVariableUnif let isPathEnd x = x == mkPathEnd type cell = int @@ -82,7 +84,9 @@ let pp_cell fmt n = else if isListHead n then "ListHead" else if isListEnd n then "ListEnd" else if isPathEnd n then "PathEnd" - else "Other") + else if isListTailVariableUnif n then "ListTailVariableUnif" + else if isLam 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 +188,7 @@ module Trie = struct 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'' } - | Node ({ listTailVariable } as t) when isListTailVariable x -> + | Node ({ listTailVariable } as t) when isListTailVariable x || isListTailVariableUnif x -> let t' = match listTailVariable with None -> empty | Some x -> x in let t'' = ins ~pos:(pos+1) t' in Node { t with listTailVariable = Some t'' } @@ -222,7 +226,7 @@ end let update_par_count n k = if isListHead k then n + 1 else - if isListEnd k || isListTailVariable k then n - 1 else n + if isListEnd k || isListTailVariable k || isListTailVariableUnif k then n - 1 else n let skip ~pos path (*hd tl*) : int = let rec aux_list acc p = @@ -335,8 +339,8 @@ let rec retrieve ~pos ~add_result mode path tree : unit = else if isInput hd || isOutput hd then (* next argument, we update the mode *) retrieve ~pos:(pos+1) ~add_result hd path tree - else if isListTailVariable hd then - let sub_tries = skip_to_listEnd mode tree in + else if isListTailVariable hd || isListTailVariableUnif hd then + let sub_tries = skip_to_listEnd (if isListTailVariableUnif hd then mkOutputMode else mode) tree in List.iter (retrieve ~pos:(pos+1) ~add_result mode path) sub_tries else begin (* Here the constructor can be Constant, Primitive, Variable, Other, ListHead, ListEnd *) @@ -414,6 +418,7 @@ module Internal = struct let isListHead = isListHead let isListEnd = isListEnd let isListTailVariable = isListTailVariable + let isListTailVariableUnif = isListTailVariableUnif let isPathEnd = isPathEnd end \ No newline at end of file diff --git a/src/discrimination_tree.mli b/src/discrimination_tree.mli index 6e7597bbb..d3892e2d2 100644 --- a/src/discrimination_tree.mli +++ b/src/discrimination_tree.mli @@ -18,6 +18,7 @@ val mkLam : cell val mkInputMode : cell val mkOutputMode : cell val mkListTailVariable : cell +val mkListTailVariableUnif : cell val mkListHead : cell val mkListEnd : cell val mkPathEnd : cell @@ -87,5 +88,6 @@ module Internal: sig val isListHead : cell -> bool val isListEnd : cell -> bool val isListTailVariable : cell -> bool + val isListTailVariableUnif : cell -> bool val isPathEnd : cell -> bool end \ No newline at end of file diff --git a/src/runtime.ml b/src/runtime.ml index eb03d25dc..b720f9e73 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2517,7 +2517,7 @@ let hash_goal_arg_list = hash_arg_list true *) let rec max_list_length acc = function | Nil -> acc - | Cons (a, (UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _)|AppArg (_, _))) -> + | Cons (a, (UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _) | AppArg (_, _) | Discard)) -> let alen = max_list_length 0 a in max (acc+2) alen | Cons (a, b)-> @@ -2527,8 +2527,7 @@ let rec max_list_length acc = function | App (_,x,xs) -> List.fold_left (fun acc x -> max acc (max_list_length 0 x)) acc (x::xs) | Builtin (_, xs) -> List.fold_left (fun acc x -> max acc (max_list_length 0 x)) acc xs | Lam t -> max_list_length acc t - | Discard | Const _ |CData _ -> acc - | UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _)|AppArg (_, _) -> acc + | Discard | Const _ |CData _ | UVar (_, _, _) | AppUVar (_, _, _) | Arg (_, _) | AppArg (_, _) -> acc let max_lists_length = List.fold_left (fun acc e -> max (max_list_length 0 e) acc) 0 @@ -2578,7 +2577,7 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m (* has the node `app` with arity `1` as first*) (* cell, then come the elment of the list *) (* up to the 30^th elemebt *) - if is_goal && h >= max_list_length' then (Path.emit path mkListEnd; update_current_min_depth path_depth) + if is_goal && h >= max_list_length' then (Path.emit path mkListTailVariableUnif; update_current_min_depth path_depth) else (main ~safe ~depth a path_depth; list_to_trie_path ~depth ~safe ~h:(h+1) path_depth (len+1) b) @@ -2607,8 +2606,8 @@ let arg_to_trie_path ~safe ~depth ~is_goal args arg_depths args_depths_ar mode m (** gives the path representation of a term *) and main ~safe ~depth t path_depth : unit = if path_depth = 0 then update_current_min_depth path_depth - else if Path.get_builder_pos path >= path_length then - (Path.emit path mkVariable; 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) else let path_depth = path_depth - 1 in match deref_head ~depth t with @@ -2721,6 +2720,7 @@ let add_clause_to_snd_lvl_idx ~depth ~insert predicate clause = function let max_depths = Discrimination_tree.max_depths args_idx in let max_path = Discrimination_tree.max_path args_idx in let max_list_length = max_lists_length clause.args in + (* Format.printf "[%d] Going to index [%a]\n%!" max_list_length (pplist pp_term ",") clause.args; *) let path = arg_to_trie_path ~depth ~safe:true ~is_goal:false clause.args arg_depths max_depths mode max_path max_list_length 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 ~max_list_length in @@ -2933,7 +2933,8 @@ let get_clauses ~depth predicate goal { index = { idx = m } } = let max_path = Discrimination_tree.max_path args_idx in let max_list_length = Discrimination_tree.max_list_length args_idx in let path = arg_to_trie_path ~safe:false ~depth ~is_goal:true (trie_goal_args goal) arg_depths max_depths mode max_path max_list_length in - [%spy "dev:disc-tree:depth-path" ~rid pp_string "Goal: MaxDepths " (pplist pp_int ";") (Array.to_list max_depths) pp_int (max_path) pp_int max_list_length]; + [%spy "dev:disc-tree:depth-path" ~rid pp_string "Goal: MaxDepths " (pplist pp_int ";") (Array.to_list max_depths)]; + [%spy "dev:disc-tree:list-size-path" ~rid pp_string "Goal: MaxListSize " pp_int max_list_length]; (* Format.(printf "Goal: MaxDepth is %a\n" (pp_print_list ~pp_sep:(fun fmt _ -> pp_print_string fmt " ") pp_print_int) (Discrimination_tree.max_depths args_idx |> Array.to_list)); *) [%spy "dev:disc-tree:path" ~rid Discrimination_tree.Path.pp path diff --git a/src/test_discrimination_tree.ml b/src/test_discrimination_tree.ml index 593a9b39a..dde0f5427 100644 --- a/src/test_discrimination_tree.ml +++ b/src/test_discrimination_tree.ml @@ -80,7 +80,7 @@ let () = 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 index dt path v = dt := DT.index !dt path ~max_list_length:1000 v in let constA = mkConstant ~safe:false ~data:~-1 ~arity:~-0 in (* a *) let p1 = [mkListHead; constA; mkListTailVariable; constA] in diff --git a/tests/suite/correctness_HO.ml b/tests/suite/correctness_HO.ml index 0174121a1..009c78ec9 100644 --- a/tests/suite/correctness_HO.ml +++ b/tests/suite/correctness_HO.ml @@ -349,7 +349,7 @@ let () = declare "chr_with_hypotheses" ~expectation:Success () -let () = declare "bug_272" +let () = declare "dt_bug_272" ~source_elpi:"dt_bug272.elpi" ~description:"dt list truncation heuristic" ~typecheck:true From 888ef246b6c4f5e43148fa09664e914fc2e186d0 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 24 Oct 2024 09:11:11 +0200 Subject: [PATCH 5/5] [dt] (rename mkLam -> mkAny) + some comments --- src/discrimination_tree.ml | 12 +++--- src/discrimination_tree.mli | 69 +++++++++++++++++++++++++-------- src/runtime.ml | 4 +- src/test_discrimination_tree.ml | 6 +-- 4 files changed, 64 insertions(+), 27 deletions(-) diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml index 926ea031c..b04c62885 100644 --- a/src/discrimination_tree.ml +++ b/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 diff --git a/src/discrimination_tree.mli b/src/discrimination_tree.mli index d3892e2d2..84a018b6f 100644 --- a/src/discrimination_tree.mli +++ b/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 diff --git a/src/runtime.ml b/src/runtime.ml index b720f9e73..c32bce2f9 100644 --- a/src/runtime.ml +++ b/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); diff --git a/src/test_discrimination_tree.ml b/src/test_discrimination_tree.ml index dde0f5427..3a6c320b3 100644 --- a/src/test_discrimination_tree.ml +++ b/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 *)