From 69921e00c12d76fa496e86bd4312ee10c1c8fd01 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 30 Jul 2026 16:47:28 +0200 Subject: [PATCH] fix #429 --- src/compiler/compiler.ml | 19 ++++++++++--------- tests/sources/functionality/test120.elpi | 9 +++++++++ tests/suite/correctness_FO.ml | 6 +++--- 3 files changed, 22 insertions(+), 12 deletions(-) create mode 100644 tests/sources/functionality/test120.elpi diff --git a/src/compiler/compiler.ml b/src/compiler/compiler.ml index d05c2cdae..df7cd79ce 100644 --- a/src/compiler/compiler.ml +++ b/src/compiler/compiler.ml @@ -1981,12 +1981,16 @@ end = struct match cl_overlap with | None -> () | Some cl_overlap -> - let rec filter_overlaps (arg_nb:int) has_cut : overlap_clause list -> 'a list = function + let rec filter_overlaps (arg_nb:int) : overlap_clause list -> 'a list = function | [] -> [] - | x::xs when x.timestamp = cl.timestamp -> if x.has_cut then [] else filter_overlaps arg_nb has_cut xs + | x::xs when x.timestamp = cl.timestamp -> + (* we have found the rule cl in the list, if it has no cut, all + rules coming after are valid choice points *) + if x.has_cut then [] else xs | x::xs -> - if not x.has_cut && arg_nb = x.arg_nb then (x::filter_overlaps arg_nb has_cut xs) - else filter_overlaps arg_nb has_cut xs + (*the test arg_nb = x.arg_nb is to recognize variadic functions*) + if not x.has_cut && arg_nb = x.arg_nb then (x::filter_overlaps arg_nb xs) + else filter_overlaps arg_nb xs in let all_input_eigen_vars, all_input_catchall, hd = hd_query ~loc ~min_depth ~depth p args in (* Format.eprintf "Is_local:%b -- Has bang? %b -- rig_occ:%b -- is_chatchall:%b@." is_local cl_overlap.has_cut has_input_w_eigen_var is_catchall; *) @@ -2004,13 +2008,11 @@ end = struct add_pred_w_eigen_var_no_cut p loc; if not is_local || (is_local && not cl_overlap.has_cut) then let all_overlapping = get_overlapping index p hd in - let overlapping = filter_overlaps cl_overlap.arg_nb cl_overlap.has_cut all_overlapping in + let overlapping = filter_overlaps cl_overlap.arg_nb all_overlapping in if overlapping <> [] then error_overlapping ~loc ~is_local p overlapping h in - (* Inspect the a local premise. If a local clause is found - it is added to the index and it check_clause is launched on it - *) + (* If a local clause is found it is added to the index and check_clause is launched on it *) let rec check_local ~min_depth ~depth ~loc ~lcs index amap (t : term) : unit = let t = to_heap ~depth t in (* let t = R.hmove ~from:depth ~to_:(depth+lcs) t in *) @@ -2053,7 +2055,6 @@ end = struct if not @@ can_overlap p then check_overlaps ~is_local ~loc ~min_depth ~depth cl (h,depth) cl_overlap p cl.args (0, C.Map.find p index); List.iter (check_local ~min_depth:depth ~loc ~depth ~lcs index amap) cl.hyps in -(* state symbols ~loc pred_info cl body overlap_clause p amap *) check_clause ~min_depth:0 ~loc ~is_local:false ~lcs:0 ~depth:0 pred_info cl cl_st oc p amap; let pred_info = C.Map.fold (fun k v -> C.Map.add k {(C.Map.find k pred_info) with has_local_without_cut = Some v}) !preds_w_eigen_var_no_cut pred_info in pred_info diff --git a/tests/sources/functionality/test120.elpi b/tests/sources/functionality/test120.elpi new file mode 100644 index 000000000..21287d011 --- /dev/null +++ b/tests/sources/functionality/test120.elpi @@ -0,0 +1,9 @@ +func p int -> int. +func q -> int. + +p X 3 :- !. + +q X :- !, pi x\ p x 5 => p x X. + +main :- + std.findall (q X) L, print L. \ No newline at end of file diff --git a/tests/suite/correctness_FO.ml b/tests/suite/correctness_FO.ml index e94cb1e93..dd0aff5fe 100644 --- a/tests/suite/correctness_FO.ml +++ b/tests/suite/correctness_FO.ml @@ -225,7 +225,7 @@ let () = declare "trie" let () = let (!) x = Test.FailureOutput (Str.regexp x) in let mut_excl l1 l2 = !(Format.asprintf "line %d.*\n.*\n.*\n.*\n+.*line %d" l1 l2) in - let mut_excl_no_loc t = !("Mutual exclusion violated for rules of predicate " ^ t ^ ".\n.*\nThis rule overlaps with") in + let mut_excl_no_loc t b = !(Format.asprintf "Mutual exclusion violated for rules of predicate %s.\n.*\nThis %srule overlaps with"t (if b then "local " else "")) in let det_check l c = !(Format.asprintf "line %d, column %d.*\nDetCheck.*relational atom" l c) in let out_err l c = !(Format.asprintf "line %d, column %d.*\nDetCheck.*output" l c) in let mode_err l c = !(Format.asprintf "line %d, column %d.*\nTypechecker.*" l c) in @@ -255,8 +255,8 @@ let () = (* 96*) mut_excl_eigen 6 "foo"; mut_excl_eigen 6 "foo"; mut_excl_eigen 6 "foo"; Success; Success; (*100*) (*101*) Success; mut_excl_eigen 5 "f"; duplicate_err 2 1; Success; Success;(*105*) (*106*) Success; constr_error 14 13; constr_error 14 13; mut_excl_eigen 9 "f"; Success; (*110*) - (*111*) mut_excl_eigen 5 "foo"; Success; mut_excl_no_loc "f"; Success; det_check 5 19; - (*116*) Success; det_check 5 2; det_check 7 2; Success + (*111*) mut_excl_eigen 5 "foo"; Success; mut_excl_no_loc "f" false; Success; det_check 5 19; + (*116*) Success; det_check 5 2; det_check 7 2; Success; mut_excl_no_loc "p" true |] in for i = 0 to Array.length status - 1 do let name = Printf.sprintf "functionality/test%d.elpi" (i+1) in