From 1dd5442d9a8db94527fbd48cc939c27db12a5884 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 4 Dec 2023 23:16:40 +0100 Subject: [PATCH 1/5] Discrimination tree on multiple args --- src/compiler.ml | 9 +++-- src/data.ml | 8 ++-- src/discrimination_tree.ml | 70 +++++++++++++++++++---------------- src/runtime.ml | 54 +++++++++++++++++---------- src/trace_atd.ts | 48 ++++++++++++------------ tests/sources/dt_multi1.elpi | 19 ++++++++++ tests/sources/dt_multi2.elpi | 19 ++++++++++ tests/sources/dt_multi3.elpi | 19 ++++++++++ tests/suite/correctness_FO.ml | 28 ++++++++++++++ 9 files changed, 193 insertions(+), 81 deletions(-) create mode 100644 tests/sources/dt_multi1.elpi create mode 100644 tests/sources/dt_multi2.elpi create mode 100644 tests/sources/dt_multi3.elpi diff --git a/src/compiler.ml b/src/compiler.ml index 92190f80d..425b759c7 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -2394,11 +2394,12 @@ let chose_indexing state predicate l = (* 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 (argno+1) l - | 1 :: l when all_zero l -> MapOn argno - | path_depth :: l when all_zero l -> Trie { argno ; path_depth } - | _ -> Hash l + | 1 :: l when all_zero l -> argno + | _ -> -1 + (* | _ -> Hash l *) in - aux 0 l + let index = aux 0 l in + if index == (-1) then Trie l else MapOn index let check_rule_pattern_in_clique state clique { D.CHR.pattern; rule_name } = try diff --git a/src/data.ml b/src/data.ml index cb62d0304..449038952 100644 --- a/src/data.ml +++ b/src/data.ml @@ -170,8 +170,7 @@ and second_lvl_idx = } | 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 *) + 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 DT.t; } @@ -192,12 +191,13 @@ 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 - - [IndexWithTrie N D] -> N-th argument at D depth + - [Trie L] -> we use the same logic of Hash, except we use Trie to discriminate + clauses *) type indexing = | MapOn of int | Hash of int list - | Trie of { argno : int; path_depth : int } + | Trie of int list [@@deriving show] let mkLam x = Lam x [@@inline] diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml index a884750f8..f79a6ad7a 100644 --- a/src/discrimination_tree.ml +++ b/src/discrimination_tree.ml @@ -9,7 +9,6 @@ let kConstant = 0 let kPrimitive = 1 let kVariable = 2 let kOther = 3 - let k_lshift = Sys.int_size - k_bits let ka_lshift = Sys.int_size - k_bits - arity_bits let k_mask = ((1 lsl k_bits) - 1) lsl k_lshift @@ -25,20 +24,25 @@ let arity_of n = let mkConstant ~safe c a = let rc = encode kConstant c a in if safe && (abs c > data_mask || a >= 1 lsl arity_bits) then - Elpi_util.Util.anomaly (Printf.sprintf "Indexing at depth > 1 is unsupported since constant %d/%d is too large or wide" c a); + Elpi_util.Util.anomaly + (Printf.sprintf "Indexing at depth > 1 is unsupported since constant %d/%d is too large or wide" c a); rc + let mkVariable = encode kVariable 0 0 let mkOther = encode kOther 0 0 let mkPrimitive c = encode kPrimitive (Elpi_util.Util.CData.hash c lsl k_bits) 0 - -let () = assert(k_of (mkConstant ~safe:false ~-17 0) == kConstant) -let () = assert(k_of mkVariable == kVariable) -let () = assert(k_of mkOther == kOther) - -let isVariable x = k_of x == kVariable -let isOther x = k_of x == kOther +let mkInputMode = encode kOther 1 0 +let mkOutputMode = encode kOther 2 0 +let () = assert (k_of (mkConstant ~safe:false ~-17 0) == kConstant) +let () = assert (k_of mkVariable == kVariable) +let () = assert (k_of mkOther == kOther) +let isVariable x = x == mkVariable +let isOther x = x == kOther +let isInput x = x == mkInputMode +let isOutput x = x == mkOutputMode type cell = int + let pp_cell fmt n = let k = k_of n in if k == kConstant then @@ -46,12 +50,14 @@ let pp_cell fmt n = let arity = (arity_mask land n) lsr ka_lshift in Format.fprintf fmt "Constant(%d,%d)" data arity else if k == kVariable then Format.fprintf fmt "Variable" - else if k == kOther then Format.fprintf fmt "Other" + else if k == kOther then + if isInput n then Format.fprintf fmt "Input" + else if isOutput n then Format.fprintf fmt "Output" + else Format.fprintf fmt "Other" else if k == kPrimitive then Format.fprintf fmt "Primitive" else Format.fprintf fmt "%o" k -let show_cell n = - Format.asprintf "%a" pp_cell n +let show_cell n = Format.asprintf "%a" pp_cell n module Trie = struct (* @@ -84,9 +90,7 @@ module Trie = struct ['a t Ptmap.t]. The empty trie is just the empty map. *) type key = int list - - type 'a t = - | Node of { data : 'a list; other : 'a t option; map : 'a t Ptmap.t } + type 'a t = Node of { data : 'a list; other : 'a t option; map : 'a t Ptmap.t } let empty = Node { data = []; other = None; map = Ptmap.empty } @@ -131,7 +135,12 @@ module Trie = struct Format.fprintf fmt "} other:{"; (match other with None -> () | Some m -> pp ppelem fmt m); Format.fprintf fmt "} key:{"; - Ptmap.to_list map |> Elpi_util.Util.pplist (fun fmt (k,v) -> pp_cell fmt k; pp ppelem fmt v) "; " fmt; + Ptmap.to_list map + |> Elpi_util.Util.pplist + (fun fmt (k, v) -> + pp_cell fmt k; + pp ppelem fmt v) + "; " fmt; Format.fprintf fmt "}]" let show (fmt : Format.formatter -> 'a -> unit) (n : 'a t) : string = @@ -146,11 +155,7 @@ let compare x y = x - y let skip (path : path) : path = let rec aux arity path = - if arity = 0 then path - else - match path with - | [] -> assert false - | m :: tl -> aux (arity - 1 + arity_of m) tl + if arity = 0 then path else match path with [] -> assert false | m :: tl -> aux (arity - 1 + arity_of m) tl in match path with | [] -> Elpi_util.Util.anomaly "Skipping empty path is not possible" @@ -197,31 +202,34 @@ let rec merge (l1 : ('a * int) list) l2 = | ((_, tx) as x) :: xs, (_, ty) :: _ when tx > ty -> x :: merge xs l2 | _, y :: ys -> y :: merge l1 ys -let get_all_children v mode = isOther v || (isVariable v && Elpi_util.Util.Output == mode) +let get_all_children v mode = isOther v || (isVariable v && isOutput mode) (* get_all_children returns if a key should be unified with all the values of the current sub-tree. This key should be either K.to_unfy or K.variable. In the latter case, the mode boolean to be true (we are in output mode). *) -let rec retrieve_aux mode path = function +let rec retrieve_aux (mode : cell) path = function | [] -> [] | hd :: tl -> merge (retrieve mode path hd) (retrieve_aux mode path tl) and retrieve mode path tree = match (tree, path) with | Trie.Node { data }, [] -> data - | Trie.Node { other; map }, v :: path when get_all_children v mode -> - retrieve_aux mode path (all_children other map) + | node, hd :: tl when isInput hd || isOutput hd -> retrieve hd tl tree + | Trie.Node { other; map }, v :: path when get_all_children v mode -> retrieve_aux mode path (all_children other map) | Trie.Node { other = None; map }, node :: sub_path -> - if mode == Elpi_util.Util.Input && isVariable node then [] + if isInput mode && isVariable node then [] else let subtree = try Ptmap.find node map with Not_found -> Trie.empty in retrieve mode sub_path subtree | Trie.Node { other = Some other; map }, (node :: sub_path as path) -> merge - (if mode == Elpi_util.Util.Input && isVariable node then [] - else - let subtree = try Ptmap.find node map with Not_found -> Trie.empty in - retrieve mode sub_path subtree) + (if isInput mode && isVariable node then [] + else + let subtree = try Ptmap.find node map with Not_found -> Trie.empty in + retrieve mode sub_path subtree) (retrieve mode (skip path) other) -let retrieve mode path index = retrieve mode path index |> List.map fst +let retrieve path index = + match path with + | [] -> Elpi_util.Util.anomaly "A path should at least of length 2" + | mode :: tl -> retrieve mode tl index |> List.map fst diff --git a/src/runtime.ml b/src/runtime.ml index bde6bec62..a8acb1d21 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2449,7 +2449,7 @@ let rec arg_to_trie_path_aux ~safe ~depth t_list path_depth : Discrimination_tre and arg_to_trie_path ~safe ~depth t path_depth : Discrimination_tree.path = let open Discrimination_tree in if path_depth = 0 then [] - else + else let path_depth = path_depth - 1 in match deref_head ~depth t with | Const k when k == Global_symbols.uvarc -> [mkVariable] @@ -2475,11 +2475,30 @@ and arg_to_trie_path ~safe ~depth t path_depth : Discrimination_tree.path = mkConstant ~safe Global_symbols.consc (if path_depth = 0 then 0 else 2) :: hd_path @ tl_path (** - [arg_to_trie_path ~path_depth ~depth t] - Take a term and returns its path representation up to path_depth + [arg_to_trie_path ~safe ~depth is_goal args arg_depths mode] + returns the path represetation of a term to be used in indexing with trie. + args, args_depths and mode are the lists of respectively the arguments, the + depths and the modes of the current term to be indexed. + is_goal is used to know if we are encoding the path for instance retriaval or + for clause insertion in the trie. + 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 deal with the input/output mode of the considere argument *) -let arg_to_trie_path ~safe ~path_depth ~depth t = - arg_to_trie_path ~safe ~depth t path_depth +let rec build_arg_to_trie_path ~safe ~depth is_goal args arg_depths mode : Discrimination_tree.path = + let open Discrimination_tree in + let prepend_mode is_goal mode tl = if is_goal then mode :: tl else tl in + match args, arg_depths, mode with + | _, [], _ -> [] + | arg_hd :: arg_tl, arg_depth_hd :: arg_depth_tl, [] -> + let tl = arg_to_trie_path ~safe ~depth arg_hd arg_depth_hd @ + build_arg_to_trie_path ~safe ~depth is_goal arg_tl arg_depth_tl [] in + prepend_mode is_goal mkOutputMode tl + | arg_hd :: arg_tl, arg_depth_hd :: arg_depth_tl, mode_hd :: mode_tl -> + let tl = arg_to_trie_path ~safe ~depth arg_hd arg_depth_hd @ + build_arg_to_trie_path ~safe ~depth is_goal arg_tl arg_depth_tl mode_tl in + prepend_mode is_goal (match mode_hd with Input -> mkInputMode | _ -> mkOutputMode) tl + | _, _ :: _,_ -> anomaly "Invalid Index length" let add1clause ~depth m (predicate,clause) = match Ptmap.find predicate m with @@ -2528,11 +2547,11 @@ let add1clause ~depth m (predicate,clause) = time = time + 1; args_idx = Ptmap.add hash ((clause,time) :: clauses) args_idx }) m - | IndexWithTrie {mode; argno; args_idx; time; path_depth } -> - let path = arg_to_trie_path ~safe:true ~depth ~path_depth (match clause.args with [] -> Discard | l -> List.nth l argno) in + | IndexWithTrie {mode; arg_depths; args_idx; time } -> + let path = build_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 { - mode; argno; path_depth; + mode; arg_depths; time = time+1; args_idx = dt }) m @@ -2583,8 +2602,8 @@ let make_index ~depth ~indexing ~clauses_rev:p = flex_arg_clauses = []; arg_idx = Ptmap.empty; } - | Trie { argno; path_depth } -> IndexWithTrie { - argno; path_depth; mode; + | Trie arg_depths -> IndexWithTrie { + arg_depths; mode; args_idx = DT.empty; time = min_int; } @@ -2641,10 +2660,8 @@ let rec nth_not_bool_default l n = match l with | x :: _ when n = 0 -> x | _ :: l -> nth_not_bool_default l (n - 1) -let trie_goal_args goal argno : term = match goal with - | Const a when argno = 0 -> goal - | App(k, x, _) when argno = 0 -> x - | App (_, _, xs) -> nth_not_found xs (argno - 1) +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 } = @@ -2662,14 +2679,13 @@ 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 {argno; path_depth; mode; args_idx} -> - let mode_arg = nth_not_bool_default mode argno in - let path = arg_to_trie_path ~safe:false ~depth ~path_depth (trie_goal_args goal argno) in + | IndexWithTrie {arg_depths; mode; args_idx} -> + let path = build_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 - pp_int path_depth + (pplist pp_int ";") arg_depths (*Discrimination_tree.(pp pp_clause) args_idx*)]; - let candidates = DT.retrieve mode_arg path args_idx in + let candidates = DT.retrieve path args_idx in [%spy "dev:disc-tree:candidates" ~rid pp_int (List.length candidates)]; candidates diff --git a/src/trace_atd.ts b/src/trace_atd.ts index 7bf7fa827..8d248245d 100644 --- a/src/trace_atd.ts +++ b/src/trace_atd.ts @@ -1,18 +1,22 @@ -// 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'. +/* + 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'. +*/ + +/* tslint:disable */ +/* eslint-disable */ export type Item = { kind: Kind[]; - goal_id: Int; - runtime_id: Int; - step: Int; + goal_id: number /*int*/; + runtime_id: number /*int*/; + step: number /*int*/; name: string; payload: string[]; } @@ -89,9 +93,9 @@ export type Location = export type FileLocation = { filename: string; - line: Int; - column: Int; - character: Int; + line: number /*int*/; + column: number /*int*/; + character: number /*int*/; } export type Event = @@ -124,11 +128,11 @@ export type Frame = { runtime_id: RuntimeId; } -export type GoalId = Int +export type GoalId = number /*int*/ -export type StepId = Int +export type StepId = number /*int*/ -export type RuntimeId = Int +export type RuntimeId = number /*int*/ export type GoalText = string @@ -786,8 +790,6 @@ export function readChrText(x: any, context: any = x): ChrText { // Runtime library ///////////////////////////////////////////////////////////////////// -export type Int = number - export type Option = null | { value: T } function _atd_missing_json_field(type_name: string, json_field_name: string) { @@ -820,7 +822,7 @@ function _atd_bad_ts(expected_type: string, ts_value: any, context: any) { ` Occurs in '${JSON.stringify(context)}'.`) } -function _atd_check_json_tuple(len: Int, x: any, context: any) { +function _atd_check_json_tuple(len: number /*int*/, x: any, context: any) { if (! Array.isArray(x) || x.length !== len) _atd_bad_json('tuple of length ' + len, x, context); } @@ -843,7 +845,7 @@ function _atd_read_bool(x: any, context: any): boolean { } } -function _atd_read_int(x: any, context: any): Int { +function _atd_read_int(x: any, context: any): number /*int*/ { if (Number.isInteger(x)) return x else { @@ -1024,7 +1026,7 @@ function _atd_write_bool(x: any, context: any): boolean { } } -function _atd_write_int(x: any, context: any): Int { +function _atd_write_int(x: any, context: any): number /*int*/ { if (Number.isInteger(x)) return x else { @@ -1133,7 +1135,7 @@ function _atd_write_required_field(type_name: string, } function _atd_write_optional_field(write_elt: (x: T, context: any) => any, - x: T, + x: T | undefined, context: any): any { if (x === undefined || x === null) return x diff --git a/tests/sources/dt_multi1.elpi b/tests/sources/dt_multi1.elpi new file mode 100644 index 000000000..0a11a863d --- /dev/null +++ b/tests/sources/dt_multi1.elpi @@ -0,0 +1,19 @@ +% The indexing with trie is used and returns only +% one matching clause +:index (1 1) +pred p o:int, o:int. + +pred build_p i:int, i:int, i:int, o:list prop. +build_p _ 0 0 [p 0 0] :- !. +build_p Mem X 0 [p X 0 | TL] :- + X > 0, X' is X - 1, + build_p Mem X' Mem TL. +build_p Mem X Y [p X Y | TL] :- + Y > 0, Y' is Y - 1, + build_p Mem X Y' TL. + +main :- + N = 100, + build_p N N N L, + L => std.time (p 0 0) T, + print T. \ No newline at end of file diff --git a/tests/sources/dt_multi2.elpi b/tests/sources/dt_multi2.elpi new file mode 100644 index 000000000..619af6cf3 --- /dev/null +++ b/tests/sources/dt_multi2.elpi @@ -0,0 +1,19 @@ +% The indexing with trie is used and returns only +% one matching clause +:index (1 1) +pred p o:int, o:int. + +pred build_p i:int, i:int, i:int, o:list prop. +build_p _ 0 0 [p 0 0] :- !. +build_p Mem X 0 [p X 0 | TL] :- + X > 0, X' is X - 1, + build_p Mem X' Mem TL. +build_p Mem X Y [p X Y | TL] :- + Y > 0, Y' is Y - 1, + build_p Mem X Y' TL. + +main :- + N = 100, + build_p N N N L, + L => std.time (p 0 X) T, + print T. \ No newline at end of file diff --git a/tests/sources/dt_multi3.elpi b/tests/sources/dt_multi3.elpi new file mode 100644 index 000000000..5f7f7ecd0 --- /dev/null +++ b/tests/sources/dt_multi3.elpi @@ -0,0 +1,19 @@ +% The indexing with trie is used and returns only +% one matching clause +:index (1 1) +pred p i:int, o:int. + +pred build_p i:int, i:int, i:int, o:list prop. +build_p _ 0 0 [p 0 0] :- !. +build_p Mem X 0 [p X 0 | TL] :- + X > 0, X' is X - 1, + build_p Mem X' Mem TL. +build_p Mem X Y [p X Y | TL] :- + Y > 0, Y' is Y - 1, + build_p Mem X Y' TL. + +main :- + N = 100, + build_p N N N L, + L => std.time (p X 0) T, + print T. \ No newline at end of file diff --git a/tests/suite/correctness_FO.ml b/tests/suite/correctness_FO.ml index 4f33ae95f..94dac261a 100644 --- a/tests/suite/correctness_FO.ml +++ b/tests/suite/correctness_FO.ml @@ -110,6 +110,10 @@ let () = declare "conj2_legacy" ~legacy_parser:true () +(* + Note in the following tests with DT, we disable typecheck not to print the + number of candidates found in the search of clauses done by the elpi typechecker +*) let () = declare "dt_var" ~source_elpi:"dt_var.elpi" ~description:"discrimination_tree indexing flex" @@ -126,6 +130,30 @@ let () = declare "dt_var2" ~expectation:(SuccessOutput (Str.regexp "dev:disc-tree:candidates = 3")) () +let () = declare "dt_multi1" + ~source_elpi:"dt_multi1.elpi" + ~description:"discrimination_tree indexing multi argument" + ~typecheck:false + ~trace:(On["tty";"stdout";"-trace-at";"1";"9999999";"-trace-only";"dev:disc-tree:candidates"]) + ~expectation:(SuccessOutput (Str.regexp "dev:disc-tree:candidates = 1")) + () + +let () = declare "dt_multi2" + ~source_elpi:"dt_multi2.elpi" + ~description:"discrimination_tree indexing multi with flexible" + ~typecheck:false + ~trace:(On["tty";"stdout";"-trace-at";"1";"9999999";"-trace-only";"dev:disc-tree:candidates"]) + ~expectation:(SuccessOutput (Str.regexp "dev:disc-tree:candidates = 101")) + () + +let () = declare "dt_multi3" + ~source_elpi:"dt_multi3.elpi" + ~description:"discrimination_tree indexing multi with flexible in input mode" + ~typecheck:false + ~trace:(On["tty";"stdout";"-trace-at";"1";"9999999";"-trace-only";"dev:disc-tree:candidates"]) + ~expectation:(FailureOutput (Str.regexp "dev:disc-tree:candidates = 0")) + () + let () = declare "is" ~source_elpi:"is.elpi" ~description:"calc" From da78aa5b9b6931b9d9bb98ad8e427866ee5f2e82 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 4 Dec 2023 23:24:45 +0100 Subject: [PATCH 2/5] small bug --- src/discrimination_tree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/discrimination_tree.ml b/src/discrimination_tree.ml index f79a6ad7a..469c1b232 100644 --- a/src/discrimination_tree.ml +++ b/src/discrimination_tree.ml @@ -37,7 +37,7 @@ let () = assert (k_of (mkConstant ~safe:false ~-17 0) == kConstant) let () = assert (k_of mkVariable == kVariable) let () = assert (k_of mkOther == kOther) let isVariable x = x == mkVariable -let isOther x = x == kOther +let isOther x = x == mkOther let isInput x = x == mkInputMode let isOutput x = x == mkOutputMode From 31a97a50d0be518d220a5dc44d38d83310878987 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Tue, 5 Dec 2023 14:05:52 +0100 Subject: [PATCH 3/5] Indexing update perf --- src/compiler.ml | 9 ++-- src/runtime.ml | 119 ++++++++++++++++++++++++------------------------ 2 files changed, 63 insertions(+), 65 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 425b759c7..b1b3621d9 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -2394,12 +2394,11 @@ let chose_indexing state predicate l = (* 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 (argno+1) l - | 1 :: l when all_zero l -> argno - | _ -> -1 + | 1 :: l when all_zero l -> MapOn argno + | _ -> Trie l + (* TODO: @FissoreD we should add some syntax if we don't want to lose the indexing with Hash *) (* | _ -> Hash l *) - in - let index = aux 0 l in - if index == (-1) then Trie l else MapOn index + in aux 0 l let check_rule_pattern_in_clique state clique { D.CHR.pattern; rule_name } = try diff --git a/src/runtime.ml b/src/runtime.ml index a8acb1d21..de582c7c0 100644 --- a/src/runtime.ml +++ b/src/runtime.ml @@ -2428,77 +2428,75 @@ 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 -(** - [arg_to_trie_path_aux ~depth t_list path_depth] - Takes a list of terms and builds the path representing this list with - height limited to [depth]. -*) -let rec arg_to_trie_path_aux ~safe ~depth t_list path_depth : Discrimination_tree.path = - if path_depth = 0 then [] - else - match t_list with - | [] -> [] - | hd :: tl -> - let hd_path = arg_to_trie_path ~safe ~depth hd path_depth in - let tl_path = arg_to_trie_path_aux ~safe ~depth tl path_depth in - hd_path @ tl_path -(** - [arg_to_trie_path ~depth t path_depth] - Takes a [term] and returns it path representation with height bound by [path_depth] -*) -and arg_to_trie_path ~safe ~depth t path_depth : Discrimination_tree.path = - let open Discrimination_tree in - if path_depth = 0 then [] - else - let path_depth = path_depth - 1 in - match deref_head ~depth t with - | Const k when k == Global_symbols.uvarc -> [mkVariable] - | Const k when safe -> [mkConstant ~safe k 0] - | Const k -> [mkConstant ~safe k 0] - | CData d -> [mkPrimitive d] - | App (k,_,_) when k == Global_symbols.uvarc -> [mkVariable] - | App (k,a,_) when k == Global_symbols.asc -> arg_to_trie_path ~safe ~depth a (path_depth+1) - | Nil -> [mkConstant ~safe Global_symbols.nilc 0] - | Lam _ -> [mkOther] (* loose indexing to enable eta *) - | Arg _ | UVar _ | AppArg _ | AppUVar _ | Discard -> [mkVariable] - | Builtin (k,tl) -> - let path = arg_to_trie_path_aux ~safe ~depth tl path_depth in - mkConstant ~safe k (if path_depth = 0 then 0 else List.length tl) :: path - | App (k, x, xs) -> - let arg_length = if path_depth = 0 then 0 else List.length xs + 1 in - let hd_path = arg_to_trie_path ~safe ~depth x path_depth in - let tl_path = arg_to_trie_path_aux ~safe ~depth xs path_depth in - mkConstant ~safe k arg_length :: hd_path @ tl_path - | Cons (x,xs) -> - let hd_path = arg_to_trie_path ~safe ~depth x path_depth in - let tl_path = arg_to_trie_path ~safe ~depth xs path_depth in - mkConstant ~safe Global_symbols.consc (if path_depth = 0 then 0 else 2) :: hd_path @ tl_path - (** [arg_to_trie_path ~safe ~depth is_goal args arg_depths mode] returns the path represetation of a term to be used in indexing with trie. args, args_depths and mode are the lists of respectively the arguments, the depths and the modes of the current term to be indexed. is_goal is used to know if we are encoding the path for instance retriaval or - for clause insertion in the trie. + for clause insertion in the trie. 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 deal with the input/output mode of the considere argument *) -let rec build_arg_to_trie_path ~safe ~depth is_goal args arg_depths mode : Discrimination_tree.path = +let arg_to_trie_path ~safe ~depth is_goal args arg_depths mode : Discrimination_tree.path = let open Discrimination_tree in - let prepend_mode is_goal mode tl = if is_goal then mode :: tl else tl in - match args, arg_depths, mode with - | _, [], _ -> [] - | arg_hd :: arg_tl, arg_depth_hd :: arg_depth_tl, [] -> - let tl = arg_to_trie_path ~safe ~depth arg_hd arg_depth_hd @ - build_arg_to_trie_path ~safe ~depth is_goal arg_tl arg_depth_tl [] in - prepend_mode is_goal mkOutputMode tl - | arg_hd :: arg_tl, arg_depth_hd :: arg_depth_tl, mode_hd :: mode_tl -> + (** prepend the mode of the current argument if we are "pathifing" a goal *) + let prepend_mode is_goal mode tl = if is_goal then mode :: tl else tl in + (** gives the path representation of a list of sub-terms *) + let rec arg_to_trie_path_aux ~safe ~depth t_list path_depth : Discrimination_tree.path = + if path_depth = 0 then [] + else + match t_list with + | [] -> [] + | hd :: tl -> + let hd_path = arg_to_trie_path ~safe ~depth hd path_depth in + let tl_path = arg_to_trie_path_aux ~safe ~depth tl path_depth in + hd_path @ tl_path + (** gives the path representation of a term *) + and arg_to_trie_path ~safe ~depth t path_depth : Discrimination_tree.path = + let open Discrimination_tree in + if path_depth = 0 then [] + else + let path_depth = path_depth - 1 in + match deref_head ~depth t with + | Const k when k == Global_symbols.uvarc -> [mkVariable] + | Const k when safe -> [mkConstant ~safe k 0] + | Const k -> [mkConstant ~safe k 0] + | CData d -> [mkPrimitive d] + | App (k,_,_) when k == Global_symbols.uvarc -> [mkVariable] + | App (k,a,_) when k == Global_symbols.asc -> arg_to_trie_path ~safe ~depth a (path_depth+1) + | Nil -> [mkConstant ~safe Global_symbols.nilc 0] + | Lam _ -> [mkOther] (* loose indexing to enable eta *) + | Arg _ | UVar _ | AppArg _ | AppUVar _ | Discard -> [mkVariable] + | Builtin (k,tl) -> + let path = arg_to_trie_path_aux ~safe ~depth tl path_depth in + mkConstant ~safe k (if path_depth = 0 then 0 else List.length tl) :: path + | App (k, x, xs) -> + let arg_length = if path_depth = 0 then 0 else List.length xs + 1 in + let hd_path = arg_to_trie_path ~safe ~depth x path_depth in + let tl_path = arg_to_trie_path_aux ~safe ~depth xs path_depth in + mkConstant ~safe k arg_length :: hd_path @ tl_path + | Cons (x,xs) -> + let hd_path = arg_to_trie_path ~safe ~depth x path_depth in + let tl_path = arg_to_trie_path ~safe ~depth xs path_depth in + mkConstant ~safe Global_symbols.consc (if path_depth = 0 then 0 else 2) :: hd_path @ tl_path + (** 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 = let tl = arg_to_trie_path ~safe ~depth arg_hd arg_depth_hd @ - build_arg_to_trie_path ~safe ~depth is_goal arg_tl arg_depth_tl mode_tl in + aux ~safe ~depth is_goal arg_tl arg_depth_tl mode_tl in prepend_mode is_goal (match mode_hd with Input -> mkInputMode | _ -> mkOutputMode) tl - | _, _ :: _,_ -> anomaly "Invalid Index length" + (** main function: build the path of the arguments received in entry *) + and aux ~safe ~depth is_goal args arg_depths mode : Discrimination_tree.path = + match args, arg_depths, mode with + | _, [], _ -> [] + | arg_hd :: arg_tl, arg_depth_hd :: arg_depth_tl, [] -> + make_sub_path arg_hd arg_tl arg_depth_hd arg_depth_tl Output [] + | arg_hd :: arg_tl, arg_depth_hd :: arg_depth_tl, mode_hd :: mode_tl -> + make_sub_path arg_hd arg_tl arg_depth_hd arg_depth_tl mode_hd mode_tl + | _, _ :: _,_ -> anomaly "Invalid Index length" in + if args == [] then prepend_mode is_goal mkOutputMode [] + else aux ~safe ~depth is_goal args arg_depths mode let add1clause ~depth m (predicate,clause) = match Ptmap.find predicate m with @@ -2548,7 +2546,7 @@ let add1clause ~depth m (predicate,clause) = args_idx = Ptmap.add hash ((clause,time) :: clauses) args_idx }) m | IndexWithTrie {mode; arg_depths; args_idx; time } -> - let path = build_arg_to_trie_path ~depth ~safe:true false clause.args arg_depths mode in + 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 { mode; arg_depths; @@ -2661,6 +2659,7 @@ let rec nth_not_bool_default l n = match l with | _ :: l -> nth_not_bool_default l (n - 1) let trie_goal_args goal : term list = match goal with + | Const _ -> [] | App(_, x, xs) -> x :: xs | _ -> assert false @@ -2680,7 +2679,7 @@ let get_clauses ~depth predicate goal { index = m } = 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} -> - let path = build_arg_to_trie_path ~safe:false ~depth true (trie_goal_args goal) arg_depths mode in + 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 (pplist pp_int ";") arg_depths From 85eb8fb8584d72307c19fd0788f0d098e556fd8f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Dec 2023 15:56:40 +0100 Subject: [PATCH 4/5] :index takes an index type --- src/compiler.ml | 38 ++++++++++++++++++++++++------------ src/parser/ast.ml | 5 +++-- src/parser/ast.mli | 5 +++-- src/parser/grammar.mly | 2 +- src/parser/test_parser.ml | 31 ++++++++++++++++++++++------- tests/sources/bad_index.elpi | 2 ++ tests/suite/elpi_specific.ml | 9 ++++++++- 7 files changed, 66 insertions(+), 26 deletions(-) create mode 100644 tests/sources/bad_index.elpi diff --git a/src/compiler.ml b/src/compiler.ml index b1b3621d9..5a0d9fc26 100644 --- a/src/compiler.ml +++ b/src/compiler.ml @@ -632,9 +632,16 @@ end = struct (* {{{ *) | Some Structured.External -> duplicate_err "external" | Some _ -> error ~loc "external predicates cannot be indexed" end - | Index i :: rest -> + | Index(i,index_type) :: rest -> + let it = + match index_type with + | None -> None + | Some "Map" -> Some Map + | Some "Hash" -> Some HashMap + | Some "DTree" -> Some DiscriminationTree + | Some s -> error ~loc ("unknown indexing directive " ^ s) in begin match r with - | None -> aux (Some (Structured.Index i)) rest + | None -> aux (Some (Structured.Index(i,it))) rest | Some (Structured.Index _) -> duplicate_err "index" | Some _ -> error ~loc "external predicates cannot be indexed" end @@ -643,7 +650,7 @@ end = struct (* {{{ *) let attributes = aux None attributes in let attributes = match attributes with - | None -> Structured.Index [1] + | None -> Structured.Index([1],None) | Some x -> x in { Type.attributes; loc; name; ty } @@ -2388,17 +2395,22 @@ let compile_clause modes initial_depth state if morelcs <> 0 then error ~loc "sigma in a toplevel clause is not supported"; state, cl -let chose_indexing state predicate l = +let chose_indexing state predicate l k = let all_zero = List.for_all ((=) 0) in - let rec aux argno = function + 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) - | 0 :: l -> aux (argno+1) l + | [] -> 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 - | _ -> Trie l - (* TODO: @FissoreD we should add some syntax if we don't want to lose the indexing with Hash *) - (* | _ -> Hash l *) - in aux 0 l + | _ -> default () + in + match k with + | Some Ast.Structured.DiscriminationTree -> Trie l + | Some HashMap -> Hash l + | None -> check_map (fun () -> Trie 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 @@ -2436,8 +2448,8 @@ let run let mode = try C.Map.find name modes with Not_found -> [] in let declare_index, index = match tindex with - | Some (Ast.Structured.Index l) -> true, chose_indexing state name l - | _ -> false, chose_indexing state name [1] in + | 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 diff --git a/src/parser/ast.ml b/src/parser/ast.ml index b9dc05b06..12ebe8c1f 100644 --- a/src/parser/ast.ml +++ b/src/parser/ast.ml @@ -135,7 +135,7 @@ type raw_attribute = | Before of string | Replace of string | External - | Index of int list + | Index of int list * string option [@@deriving show] module Clause = struct @@ -307,7 +307,8 @@ and cattribute = { } and tattribute = | External - | Index of int list + | Index of int list * tindex option +and tindex = Map | HashMap | DiscriminationTree and 'a shorthand = { iloc : Loc.t; full_name : 'a; diff --git a/src/parser/ast.mli b/src/parser/ast.mli index e44625ee7..39b13a4e8 100644 --- a/src/parser/ast.mli +++ b/src/parser/ast.mli @@ -72,7 +72,7 @@ type raw_attribute = | Before of string | Replace of string | External - | Index of int list + | Index of int list * string option [@@ deriving show] module Clause : sig @@ -213,7 +213,8 @@ and cattribute = { } and tattribute = | External - | Index of int list + | Index of int list * tindex option +and tindex = Map | HashMap | DiscriminationTree and 'a shorthand = { iloc : Loc.t; full_name : 'a; diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly index d78ed9009..4773e8142 100644 --- a/src/parser/grammar.mly +++ b/src/parser/grammar.mly @@ -296,7 +296,7 @@ attribute: | BEFORE; s = STRING { Before s } | REPLACE; s = STRING { Replace s } | EXTERNAL { External } -| INDEX; LPAREN; l = nonempty_list(indexing) ; RPAREN { Index l } +| INDEX; LPAREN; l = nonempty_list(indexing) ; RPAREN; o = option(STRING) { Index (l,o) } indexing: | FRESHUV { 0 } diff --git a/src/parser/test_parser.ml b/src/parser/test_parser.ml index 81442c685..c22e361b6 100644 --- a/src/parser/test_parser.ml +++ b/src/parser/test_parser.ml @@ -9,9 +9,9 @@ let error s a1 a2 = let f2 = Filename.temp_file "parser_out" "txt" in let oc1 = open_out f1 in let oc2 = open_out f2 in - output_string oc1 "new:\n"; + output_string oc1 "\nnew:\n"; output_string oc1 (Program.show a1); - output_string oc2 "reference:\n"; + output_string oc2 "\nreference:\n"; output_string oc2 (Program.show a2); flush_all (); close_out oc1; @@ -43,9 +43,9 @@ let test s x y w z att b = let p = Parser.program_from ~loc lexbuf in if p <> exp then error s p exp - with Parse.ParseError(loc,message) -> - Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; - exit 1 + with Parse.ParseError(loc,message) -> + Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; + exit 1 let testR s x y w z attributes to_match to_remove guard new_goal = let exp = [Program.(Chr { Chr.to_match; to_remove; guard; new_goal; loc=(mkLoc x y w z); attributes })] in @@ -55,10 +55,25 @@ let testR s x y w z attributes to_match to_remove guard new_goal = let p = Parser.program_from ~loc lexbuf in if p <> exp then error s p exp - with Parse.ParseError(loc,message) -> + with Parse.ParseError(loc,message) -> + Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; + exit 1 + +let testT s x y w z attributes () = + let lexbuf = Lexing.from_string s in + let loc = Loc.initial "(input)" in + try + let p = Parser.program_from ~loc lexbuf in + match p with + | [Program.Pred _] -> () + | [Program.Type _] -> () + | _ -> + Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) "not a type declaration"; + exit 1 + with Parse.ParseError(loc,message) -> Printf.eprintf "error parsing '%s' at %s\n%s%!" s (Loc.show loc) message; exit 1 - + let testF s i msg = let lexbuf = Lexing.from_string s in let loc = Loc.initial "(input)" in @@ -136,6 +151,8 @@ let _ = testF "x. x]" 5 "unexpected keyword"; testF "x. +" 4 "unexpected start"; test ":name \"x\" x." 0 11 1 0 [Name "x"] (c"x"); + testT ":index (1) \"foobar\" pred x." 0 11 1 0 [Index ([1],Some "foobar")] (); + testT ":index (1) pred x." 0 11 1 0 [Index ([1], None)] (); testF "p :- g (f x) \\ y." 14 ".*bind.*must follow.*name.*"; testF "foo i:term, o:term. foo A B :- A = [B]." 6 "unexpected keyword"; (* 01234567890123456789012345 *) diff --git a/tests/sources/bad_index.elpi b/tests/sources/bad_index.elpi new file mode 100644 index 000000000..1dfdad4de --- /dev/null +++ b/tests/sources/bad_index.elpi @@ -0,0 +1,2 @@ +:index (1 1) "Map" +pred foo i:int, i:int. diff --git a/tests/suite/elpi_specific.ml b/tests/suite/elpi_specific.ml index 42bcc804a..a2760c832 100644 --- a/tests/suite/elpi_specific.ml +++ b/tests/suite/elpi_specific.ml @@ -437,4 +437,11 @@ let () = declare "trace-browser-elab-broken2" ~description:"fatal broken trace elaboration" ~expectation:(FailureOutput (Str.regexp "broken.*step_id 217.*json object 1857")) () - \ No newline at end of file + + +let () = declare "bad_index" + ~source_elpi:"bad_index.elpi" + ~description:"bad indexing directive" + ~expectation:Test.(FailureOutput (Str.regexp "Wrong indexing")) + () + \ No newline at end of file From 1350da778d940e8b905ba8068ae30a5730044d7b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Dec 2023 16:00:19 +0100 Subject: [PATCH 5/5] cleanup --- src/compiler.ml | 4 ++-- src/data.ml | 9 +++++---- src/runtime.ml | 10 +++++----- 3 files changed, 12 insertions(+), 11 deletions(-) diff --git a/src/compiler.ml b/src/compiler.ml index 5a0d9fc26..545e6ce4c 100644 --- a/src/compiler.ml +++ b/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 diff --git a/src/data.ml b/src/data.ml index 449038952..cec54b7c7 100644 --- a/src/data.ml +++ b/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] diff --git a/src/runtime.ml b/src/runtime.ml index de582c7c0..2226ee0d4 100644 --- a/src/runtime.ml +++ b/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 =