From 50f28c7338bf1320567674a2952ab86ce3793e9e Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 23 Jul 2024 13:25:03 +0200
Subject: [PATCH 01/10] CHR: constraints allow hyps, not considered in the
 clique error check

The grammar has been extended to support the new behavior

A test has been added
---
 src/compiler.ml                        | 46 +++++++++++++++-----------
 src/data.ml                            | 18 ++++++----
 src/parser/ast.ml                      |  4 +--
 src/parser/ast.mli                     |  4 +--
 src/parser/grammar.mly                 |  3 +-
 src/trace_atd.ts                       |  2 ++
 tests/sources/chr_with_hypotheses.elpi | 33 ++++++++++++++++++
 tests/suite/correctness_HO.ml          |  7 ++++
 8 files changed, 86 insertions(+), 31 deletions(-)
 create mode 100644 tests/sources/chr_with_hypotheses.elpi

diff --git a/src/compiler.ml b/src/compiler.ml
index 0eed3ede3..cef2d4ff9 100644
--- a/src/compiler.ml
+++ b/src/compiler.ml
@@ -519,7 +519,11 @@ and block =
   | Clauses of (preterm,Ast.Structured.attribute) Ast.Clause.t list (* TODO: use a map : predicate -> clause list to speed up insertion *)
   | Namespace of string * pbody
   | Shorten of C.t Ast.Structured.shorthand list * pbody
-  | Constraints of constant list * prechr_rule list * pbody
+  | Constraints of constant list * constant list * prechr_rule list * pbody
+and typ = {
+  tindex : Ast.Structured.tattribute;
+  decl : type_declaration
+}
 [@@deriving show, ord]
 
 end
@@ -531,7 +535,7 @@ type program = {
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : (mode * Loc.t) C.Map.t;
   clauses : (preterm,Ast.Structured.attribute) Ast.Clause.t list;
-  chr : (constant list * prechr_rule list) list;
+  chr : (constant list * constant list * prechr_rule list) list;
   local_names : int;
   symbols : C.Set.t;
 
@@ -548,7 +552,7 @@ type program = {
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : (mode * Loc.t) C.Map.t;
   clauses_rev : (preterm,attribute) Ast.Clause.t list;
-  chr : (constant list * prechr_rule list) list;
+  chr : (constant list * constant list * prechr_rule list) list;
   local_names : int;
 
   toplevel_macros : macro_declaration;
@@ -591,7 +595,7 @@ type 'a query = {
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : mode C.Map.t;
   clauses_rev : (preterm,Assembled.attribute) Ast.Clause.t list;
-  chr : (constant list * prechr_rule list) list;
+  chr : (constant list * constant list * prechr_rule list) list;
   initial_depth : int;
   query : preterm;
   query_arguments : 'a Query.arguments [@opaque];
@@ -729,13 +733,13 @@ end = struct (* {{{ *)
             error "CHR cannot be declared inside an anonymous block";
           aux_end_block loc ns (Locals(locals1,p) :: cl2b clauses @ blocks)
             [] macros types tabbrs modes locals chr accs rest
-      | Program.Constraint (loc, f) :: rest ->
+      | Program.Constraint (loc, hyps, f) :: rest ->
           if chr <> [] then
             error "Constraint blocks cannot be nested";
           let p, locals1, chr, rest = aux ns [] [] [] [] [] [] [] [] accs rest in
           if locals1 <> [] then
             error "locals cannot be declared inside a Constraint block";
-          aux_end_block loc ns (Constraints(f,chr,p) :: cl2b clauses @ blocks)
+          aux_end_block loc ns (Constraints(hyps,f,chr,p) :: cl2b clauses @ blocks)
             [] macros types tabbrs modes locals [] accs rest
       | Program.Namespace (loc, n) :: rest ->
           let p, locals1, chr1, rest = aux (n::ns) [] [] [] [] [] [] [] [] StrSet.empty rest in
@@ -1468,9 +1472,10 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
           lcs, state, types, type_abbrevs, modes,
           C.Set.union defs (C.Set.diff p.Structured.symbols shorts),
           Structured.Shorten(shorthands, p) :: compiled_rest
-      | Constraints (clique, rules, p) :: rest ->
+      | Constraints (hyps, clique, rules, p) :: rest ->
           (* XXX missing check for nested constraints *)
           let state, clique = map_acc funct_of_ast state clique in
+          let state, hyps = map_acc funct_of_ast state hyps in
           let state, rules =
             map_acc (prechr_rule_of_ast lcs macros) state rules in
           let state, lcs, _, p = compile_program macros lcs state p in
@@ -1478,7 +1483,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
             compile_body macros types type_abbrevs modes lcs defs state rest in
           lcs, state, types, type_abbrevs, modes,
           C.Set.union defs p.Structured.symbols,
-          Structured.Constraints(clique, rules,p) :: compiled_rest
+          Structured.Constraints(hyps, clique, rules,p) :: compiled_rest
     in
     let state, local_names, toplevel_macros, pbody =
       compile_program toplevel_macros 0 state p in
@@ -1595,7 +1600,7 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
     let body1 = smart_map_preterm state f body in
     if body1 == body then x else { x with Ast.Clause.body = body1 }
 
-  let map_pair f g (x,y) = f x, g y
+  let map_triple f g h (x,y,z) = f x, g y, h z
 
   type subst = (string list * C.t C.Map.t)
 
@@ -1628,9 +1633,10 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
   let apply_subst_modes ?live_symbols s m =
     C.Map.fold (fun c v m -> C.Map.add (apply_subst_constant ?live_symbols s c) v m) m C.Map.empty
 
-  let apply_subst_chr ?live_symbols st s l =
-    map_pair (smart_map (apply_subst_constant ?live_symbols s))
-             (smart_map (map_chr st (apply_subst_constant ?live_symbols s))) l
+  let apply_subst_chr ?live_symbols st s (l: constant list * constant list * prechr_rule list) =
+    map_triple (smart_map (apply_subst_constant ?live_symbols s))
+               (smart_map (apply_subst_constant ?live_symbols s))
+               (smart_map (map_chr st (apply_subst_constant ?live_symbols s))) l
 
   let apply_subst_clauses ?live_symbols st s =
     smart_map (map_clause st (apply_subst_constant ?live_symbols s))
@@ -1673,11 +1679,11 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
         let cl = apply_subst_clauses ~live_symbols state subst cl in
         let clauses = clauses @ cl in
         compile_body live_symbols state lcs types type_abbrevs modes clauses chr subst rest
-    | Constraints (clique, rules, { types = t; type_abbrevs = ta; modes = m; body }) :: rest ->
+    | Constraints (hyps, clique, rules, { types = t; type_abbrevs = ta; modes = m; body }) :: rest ->
         let types = ToDBL.merge_types state (apply_subst_types ~live_symbols state subst t) types in
         let type_abbrevs = ToDBL.merge_type_abbrevs state (apply_subst_type_abbrevs ~live_symbols state subst ta) type_abbrevs in
         let modes = ToDBL.merge_modes state (apply_subst_modes ~live_symbols subst m) modes in
-        let chr = apply_subst_chr ~live_symbols state subst (clique,rules) :: chr in
+        let chr = apply_subst_chr ~live_symbols state subst (hyps,clique,rules) :: chr in
         let types, type_abbrevs, modes, clauses, chr =
           compile_body live_symbols state lcs types type_abbrevs modes clauses chr subst body in
         compile_body live_symbols state lcs types type_abbrevs modes clauses chr subst rest
@@ -1746,7 +1752,7 @@ module Spill : sig
 
   val spill_chr :
     State.t -> types:Types.types C.Map.t -> modes:(constant -> mode) ->
-      (constant list * prechr_rule list) -> (constant list * prechr_rule list)
+      (constant list * constant list * prechr_rule list) -> (constant list * constant list * prechr_rule list)
   
   (* Exported to compile the query *)
   val spill_preterm :
@@ -1994,9 +2000,9 @@ end = struct (* {{{ *)
       option_mapacc (spill_presequent state modes types pcloc) pamap pnew_goal in
     { r with pguard; pnew_goal; pamap }
 
-  let spill_chr state ~types ~modes (clique, rules) =
+  let spill_chr state ~types ~modes (hyps, clique, rules) =
     let rules = List.map (spill_rule state modes types) rules in
-    (clique, rules)
+    (hyps, clique, rules)
 
   let spill_clause state ~types ~modes ({ Ast.Clause.body = { term; amap; loc; spilling } } as x) =
     if not spilling then x
@@ -2092,7 +2098,7 @@ let assemble flags state code  (ul : compilation_unit list) =
   let chr = List.concat (code.Assembled.chr :: List.rev chr_rev) in
   let chr =
     let pifexpr { pifexpr } = pifexpr in
-    List.map (fun (symbs,rules) -> symbs, filter_if flags pifexpr rules) chr in
+    List.map (fun (hyps, symbs,rules) -> hyps, symbs, filter_if flags pifexpr rules) chr in
   state, { Assembled.clauses_rev; types; type_abbrevs; modes; chr; local_names = code.Assembled.local_names; toplevel_macros = code.Assembled.toplevel_macros }
 
 end (* }}} *)
@@ -2485,8 +2491,8 @@ let run
   check_no_regular_types_for_builtins state types;
   (* Real Arg nodes: from "Const '%Arg3'" to "Arg 3" *)
   let state, chr =
-    List.fold_left (fun (state, chr) (clique, rules) ->
-      let chr, clique = CHR.new_clique (Symbols.show state) clique chr in
+    List.fold_left (fun (state, chr) (hyps, clique, rules) ->
+      let chr, clique = CHR.new_clique (Symbols.show state) hyps clique chr in
       let state, rules = map_acc (compile_chr initial_depth) state rules in
       List.iter (check_rule_pattern_in_clique state clique) rules;
       state, List.fold_left (fun x y -> CHR.add_rule clique y x) chr rules)
diff --git a/src/data.ml b/src/data.ml
index e7a6632a1..ba715696c 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -589,7 +589,7 @@ module CHR : sig
 
   val empty : t
 
-  val new_clique : (constant -> string) -> constant list -> t -> t * clique
+  val new_clique : (constant -> string) -> constant list -> constant list -> t -> t * clique
   val clique_of : constant -> t -> Constants.Set.t option
   val add_rule : clique -> rule -> t -> t
   val in_clique : clique -> constant -> bool
@@ -597,10 +597,12 @@ module CHR : sig
   val rules_for : constant -> t -> rule list
 
   val pp : Fmt.formatter -> t -> unit
+  val pp_clique : Fmt.formatter -> clique -> unit
   val show : t -> string
 
 end = struct (* {{{ *)
 
+  type clique = Constants.Set.t [@@deriving show]
   type sequent = { eigen : term; context : term; conclusion : term }
   and rule = {
     to_match : sequent list;
@@ -615,27 +617,31 @@ end = struct (* {{{ *)
   }
   [@@ deriving show]
   type t = {
-    cliques : Constants.Set.t Constants.Map.t;
+    cliques : clique Constants.Map.t;
     rules : rule list Constants.Map.t
   }
   [@@ deriving show]
-  type clique = Constants.Set.t
 
   let empty = { cliques = Constants.Map.empty; rules = Constants.Map.empty }
 
   let in_clique m c = Constants.Set.mem c m
 
-  let new_clique show_constant cl ({ cliques } as chr) =
+  let new_clique show_constant hyps cl ({ cliques } as chr) =
     if cl = [] then error "empty clique";
-    let c = List.fold_right Constants.Set.add cl Constants.Set.empty in
+    let c = Constants.Set.of_list cl in
+    
+    (* Non overlapping clique check *)
     Constants.Map.iter (fun _ c' ->
       if not (Constants.Set.is_empty (Constants.Set.inter c c')) && not (Constants.Set.equal c c') then
         error ("overlapping constraint cliques: {" ^
           String.concat "," (List.map show_constant (Constants.Set.elements c))^"} {" ^
           String.concat "," (List.map show_constant (Constants.Set.elements c'))^ "}")
     ) cliques;
+
+    (* Add constants in the context (for hypotheses) *)
+    let c = List.fold_right Constants.Set.add hyps c in
     let cliques =
-      List.fold_right (fun x cliques -> Constants.Map.add x c cliques) cl cliques in
+      List.fold_right (fun x cliques -> Constants.Map.add x c cliques) (hyps @ cl) cliques in
     { chr with cliques }, c
 
   let clique_of c { cliques } =
diff --git a/src/parser/ast.ml b/src/parser/ast.ml
index 59e03b6c7..9c16a4140 100644
--- a/src/parser/ast.ml
+++ b/src/parser/ast.ml
@@ -221,7 +221,7 @@ module Program = struct
     (* Blocks *)
     | Begin of Loc.t
     | Namespace of Loc.t * Func.t
-    | Constraint of Loc.t * Func.t list
+    | Constraint of Loc.t * Func.t list * Func.t list
     | Shorten of Loc.t * (Func.t * Func.t) list (* prefix suffix *)
     | End of Loc.t
 
@@ -303,7 +303,7 @@ and block =
   | Clauses of (Term.t,attribute) Clause.t list
   | Namespace of Func.t * program
   | Shorten of Func.t shorthand list * program
-  | Constraints of Func.t list * cattribute Chr.t list * program
+  | Constraints of Func.t list * Func.t list * cattribute Chr.t list * program
 and attribute = {
   insertion : insertion option;
   id : string option;
diff --git a/src/parser/ast.mli b/src/parser/ast.mli
index 6ab2f10a8..a32a67f0f 100644
--- a/src/parser/ast.mli
+++ b/src/parser/ast.mli
@@ -147,7 +147,7 @@ module Program : sig
     (* Blocks *)
     | Begin of Loc.t
     | Namespace of Loc.t * Func.t
-    | Constraint of Loc.t * Func.t list
+    | Constraint of Loc.t * Func.t list * Func.t list
     | Shorten of Loc.t * (Func.t * Func.t) list (* prefix suffix *)
     | End of Loc.t
 
@@ -202,7 +202,7 @@ and block =
   | Clauses of (Term.t,attribute) Clause.t list
   | Namespace of Func.t * program
   | Shorten of Func.t shorthand list * program
-  | Constraints of Func.t list * cattribute Chr.t list * program
+  | Constraints of Func.t list * Func.t list * cattribute Chr.t list * program
 and attribute = {
   insertion : insertion option;
   id : string option;
diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly
index 3ce282967..befacdc4f 100644
--- a/src/parser/grammar.mly
+++ b/src/parser/grammar.mly
@@ -126,7 +126,8 @@ decl:
 | t = kind; FULLSTOP { Program.Type t }
 | m = mode; FULLSTOP { Program.Mode [m] }
 | m = macro; FULLSTOP { Program.Macro m }
-| CONSTRAINT; cl = list(constant); LCURLY { Program.Constraint(loc $sloc, cl) }
+| CONSTRAINT; hyps = list(constant); PIPE; MINUS; cl = list(constant); LCURLY { Program.Constraint(loc $sloc, hyps, cl) }
+| CONSTRAINT; cl = list(constant); LCURLY { Program.Constraint(loc $sloc, [], cl) }
 | NAMESPACE; c = constant; LCURLY { Program.Namespace(loc $sloc, c )}
 | SHORTEN; s = shorten; FULLSTOP { Program.Shorten(loc $sloc, s) }
 | a = typeabbrev; FULLSTOP { Program.TypeAbbreviation a }
diff --git a/src/trace_atd.ts b/src/trace_atd.ts
index 8d248245d..aebe96087 100644
--- a/src/trace_atd.ts
+++ b/src/trace_atd.ts
@@ -9,6 +9,8 @@
     of type 'Foo'.
 */
 
+// eslint-disable-next-line @typescript-eslint/ban-ts-comment
+// @ts-nocheck
 /* tslint:disable */
 /* eslint-disable */
 
diff --git a/tests/sources/chr_with_hypotheses.elpi b/tests/sources/chr_with_hypotheses.elpi
new file mode 100644
index 000000000..0be0336d4
--- /dev/null
+++ b/tests/sources/chr_with_hypotheses.elpi
@@ -0,0 +1,33 @@
+pred p i:int.
+pred trig.
+pred q i:int.
+pred trig1.
+
+pred acc i:int.
+
+pred tester i:string, i:list prop, i:int.
+tester Str Ctx Var :-
+  print "In" Str "ctx is" Ctx,
+  print "Doing acc with" Var,
+  Ctx => acc Var,
+  print "SUCCESS !!".
+
+% the syntax `acc |-` is used to load acc clauses as hypothesis in the context
+constraint acc |- p trig {
+  rule trig \ (Ctx ?- p A) <=> (tester "p" Ctx A).
+  rule \ trig.
+}
+
+% here again `acc |-` is used but the clique error message is not thrown, since,
+% again `acc` is loaded and supposed to be only used as hypotheses in the context
+constraint acc |- q trig1 {
+  rule trig1 \ (Ctx ?- q A) <=> (tester "q" Ctx A).
+  rule \ trig1.
+}
+
+main :- acc 3 => declare_constraint (p 3) [_], declare_constraint trig [_],
+        acc 4 => declare_constraint (q 4) [_], declare_constraint trig1 [_],
+        print "Constraint store is empty ?",
+        print_constraints, % Should be empty
+        print "End print Constraitn store",
+        acc 4 => declare_constraint (q 5) [_], not (declare_constraint trig1 [_]).
\ No newline at end of file
diff --git a/tests/suite/correctness_HO.ml b/tests/suite/correctness_HO.ml
index 4f1d1df1b..df45bfd04 100644
--- a/tests/suite/correctness_HO.ml
+++ b/tests/suite/correctness_HO.ml
@@ -341,3 +341,10 @@ let () = declare "chr-scope-change-err"
   ~typecheck:true
   ~expectation:(FailureOutput (Str.regexp "cannot be put in the desired context"))
   ()
+
+let () = declare "chr_with_hypotheses"
+  ~source_elpi:"chr_with_hypotheses.elpi"
+  ~description:"chr_with_hypotheses"
+  ~typecheck:true
+  ~expectation:Success
+  ()

From 496d8f5903a08bd4cd97b8ca518d6ff299f8db79 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 23 Jul 2024 13:54:31 +0200
Subject: [PATCH 02/10] |- moved to ?-

---
 src/parser/grammar.mly                 | 2 +-
 tests/sources/chr_with_hypotheses.elpi | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/parser/grammar.mly b/src/parser/grammar.mly
index befacdc4f..1e737bb71 100644
--- a/src/parser/grammar.mly
+++ b/src/parser/grammar.mly
@@ -126,7 +126,7 @@ decl:
 | t = kind; FULLSTOP { Program.Type t }
 | m = mode; FULLSTOP { Program.Mode [m] }
 | m = macro; FULLSTOP { Program.Macro m }
-| CONSTRAINT; hyps = list(constant); PIPE; MINUS; cl = list(constant); LCURLY { Program.Constraint(loc $sloc, hyps, cl) }
+| CONSTRAINT; hyps = list(constant); QDASH; cl = list(constant); LCURLY { Program.Constraint(loc $sloc, hyps, cl) }
 | CONSTRAINT; cl = list(constant); LCURLY { Program.Constraint(loc $sloc, [], cl) }
 | NAMESPACE; c = constant; LCURLY { Program.Namespace(loc $sloc, c )}
 | SHORTEN; s = shorten; FULLSTOP { Program.Shorten(loc $sloc, s) }
diff --git a/tests/sources/chr_with_hypotheses.elpi b/tests/sources/chr_with_hypotheses.elpi
index 0be0336d4..c50035d83 100644
--- a/tests/sources/chr_with_hypotheses.elpi
+++ b/tests/sources/chr_with_hypotheses.elpi
@@ -12,15 +12,15 @@ tester Str Ctx Var :-
   Ctx => acc Var,
   print "SUCCESS !!".
 
-% the syntax `acc |-` is used to load acc clauses as hypothesis in the context
-constraint acc |- p trig {
+% the syntax `acc ?-` is used to load acc clauses as hypothesis in the context
+constraint acc ?- p trig {
   rule trig \ (Ctx ?- p A) <=> (tester "p" Ctx A).
   rule \ trig.
 }
 
-% here again `acc |-` is used but the clique error message is not thrown, since,
+% here again `acc ?-` is used but the clique error message is not thrown, since,
 % again `acc` is loaded and supposed to be only used as hypotheses in the context
-constraint acc |- q trig1 {
+constraint acc ?- q trig1 {
   rule trig1 \ (Ctx ?- q A) <=> (tester "q" Ctx A).
   rule \ trig1.
 }

From 2f58507e45954bf4c6ab1fb204531e8da47c934d Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 23 Jul 2024 14:21:15 +0200
Subject: [PATCH 03/10] add type block_constraint

---
 src/compiler.ml    | 53 ++++++++++++++++++++++++++--------------------
 src/parser/ast.ml  | 15 ++++++++-----
 src/parser/ast.mli |  7 +++++-
 3 files changed, 46 insertions(+), 29 deletions(-)

diff --git a/src/compiler.ml b/src/compiler.ml
index cef2d4ff9..eda7fe291 100644
--- a/src/compiler.ml
+++ b/src/compiler.ml
@@ -447,6 +447,13 @@ type prechr_rule = {
 open Data
 module C = Constants
 
+type block_constraint = {
+   clique : constant list;
+   ctx_filter : constant list;
+   rules : prechr_rule list
+}
+[@@deriving show, ord]
+
 module Types = struct
 
 type typ = {
@@ -519,7 +526,7 @@ and block =
   | Clauses of (preterm,Ast.Structured.attribute) Ast.Clause.t list (* TODO: use a map : predicate -> clause list to speed up insertion *)
   | Namespace of string * pbody
   | Shorten of C.t Ast.Structured.shorthand list * pbody
-  | Constraints of constant list * constant list * prechr_rule list * pbody
+  | Constraints of block_constraint * pbody
 and typ = {
   tindex : Ast.Structured.tattribute;
   decl : type_declaration
@@ -535,7 +542,7 @@ type program = {
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : (mode * Loc.t) C.Map.t;
   clauses : (preterm,Ast.Structured.attribute) Ast.Clause.t list;
-  chr : (constant list * constant list * prechr_rule list) list;
+  chr : block_constraint list;
   local_names : int;
   symbols : C.Set.t;
 
@@ -552,7 +559,7 @@ type program = {
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : (mode * Loc.t) C.Map.t;
   clauses_rev : (preterm,attribute) Ast.Clause.t list;
-  chr : (constant list * constant list * prechr_rule list) list;
+  chr : block_constraint list;
   local_names : int;
 
   toplevel_macros : macro_declaration;
@@ -595,7 +602,7 @@ type 'a query = {
   type_abbrevs : type_abbrev_declaration C.Map.t;
   modes : mode C.Map.t;
   clauses_rev : (preterm,Assembled.attribute) Ast.Clause.t list;
-  chr : (constant list * constant list * prechr_rule list) list;
+  chr : block_constraint list;
   initial_depth : int;
   query : preterm;
   query_arguments : 'a Query.arguments [@opaque];
@@ -733,13 +740,13 @@ end = struct (* {{{ *)
             error "CHR cannot be declared inside an anonymous block";
           aux_end_block loc ns (Locals(locals1,p) :: cl2b clauses @ blocks)
             [] macros types tabbrs modes locals chr accs rest
-      | Program.Constraint (loc, hyps, f) :: rest ->
+      | Program.Constraint (loc, ctx_filter, clique) :: rest ->
           if chr <> [] then
             error "Constraint blocks cannot be nested";
           let p, locals1, chr, rest = aux ns [] [] [] [] [] [] [] [] accs rest in
           if locals1 <> [] then
             error "locals cannot be declared inside a Constraint block";
-          aux_end_block loc ns (Constraints(hyps,f,chr,p) :: cl2b clauses @ blocks)
+          aux_end_block loc ns (Constraints({ctx_filter;clique;rules=chr},p) :: cl2b clauses @ blocks)
             [] macros types tabbrs modes locals [] accs rest
       | Program.Namespace (loc, n) :: rest ->
           let p, locals1, chr1, rest = aux (n::ns) [] [] [] [] [] [] [] [] StrSet.empty rest in
@@ -1472,10 +1479,10 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
           lcs, state, types, type_abbrevs, modes,
           C.Set.union defs (C.Set.diff p.Structured.symbols shorts),
           Structured.Shorten(shorthands, p) :: compiled_rest
-      | Constraints (hyps, clique, rules, p) :: rest ->
+      | Constraints ({ctx_filter; clique; rules}, p) :: rest ->
           (* XXX missing check for nested constraints *)
           let state, clique = map_acc funct_of_ast state clique in
-          let state, hyps = map_acc funct_of_ast state hyps in
+          let state, ctx_filter = map_acc funct_of_ast state ctx_filter in
           let state, rules =
             map_acc (prechr_rule_of_ast lcs macros) state rules in
           let state, lcs, _, p = compile_program macros lcs state p in
@@ -1483,7 +1490,7 @@ let query_preterm_of_ast ~depth macros state (loc, t) =
             compile_body macros types type_abbrevs modes lcs defs state rest in
           lcs, state, types, type_abbrevs, modes,
           C.Set.union defs p.Structured.symbols,
-          Structured.Constraints(hyps, clique, rules,p) :: compiled_rest
+          Structured.Constraints({ctx_filter; clique; rules},p) :: compiled_rest
     in
     let state, local_names, toplevel_macros, pbody =
       compile_program toplevel_macros 0 state p in
@@ -1600,8 +1607,6 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
     let body1 = smart_map_preterm state f body in
     if body1 == body then x else { x with Ast.Clause.body = body1 }
 
-  let map_triple f g h (x,y,z) = f x, g y, h z
-
   type subst = (string list * C.t C.Map.t)
 
 
@@ -1633,10 +1638,12 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
   let apply_subst_modes ?live_symbols s m =
     C.Map.fold (fun c v m -> C.Map.add (apply_subst_constant ?live_symbols s c) v m) m C.Map.empty
 
-  let apply_subst_chr ?live_symbols st s (l: constant list * constant list * prechr_rule list) =
-    map_triple (smart_map (apply_subst_constant ?live_symbols s))
-               (smart_map (apply_subst_constant ?live_symbols s))
-               (smart_map (map_chr st (apply_subst_constant ?live_symbols s))) l
+  let apply_subst_chr ?live_symbols st s (l: (block_constraint)) =
+    let app_sub_const f = smart_map (f (apply_subst_constant ?live_symbols s)) in
+     (fun {ctx_filter; rules; clique} ->
+        { ctx_filter = app_sub_const Fun.id ctx_filter;
+          clique = app_sub_const Fun.id clique;
+          rules = app_sub_const (map_chr st) rules }) l
 
   let apply_subst_clauses ?live_symbols st s =
     smart_map (map_clause st (apply_subst_constant ?live_symbols s))
@@ -1679,11 +1686,11 @@ let subst_amap state f { nargs; c2i; i2n; n2t; n2i } =
         let cl = apply_subst_clauses ~live_symbols state subst cl in
         let clauses = clauses @ cl in
         compile_body live_symbols state lcs types type_abbrevs modes clauses chr subst rest
-    | Constraints (hyps, clique, rules, { types = t; type_abbrevs = ta; modes = m; body }) :: rest ->
+    | Constraints ({ctx_filter; clique; rules}, { types = t; type_abbrevs = ta; modes = m; body }) :: rest ->
         let types = ToDBL.merge_types state (apply_subst_types ~live_symbols state subst t) types in
         let type_abbrevs = ToDBL.merge_type_abbrevs state (apply_subst_type_abbrevs ~live_symbols state subst ta) type_abbrevs in
         let modes = ToDBL.merge_modes state (apply_subst_modes ~live_symbols subst m) modes in
-        let chr = apply_subst_chr ~live_symbols state subst (hyps,clique,rules) :: chr in
+        let chr = apply_subst_chr ~live_symbols state subst {ctx_filter;clique;rules} :: chr in
         let types, type_abbrevs, modes, clauses, chr =
           compile_body live_symbols state lcs types type_abbrevs modes clauses chr subst body in
         compile_body live_symbols state lcs types type_abbrevs modes clauses chr subst rest
@@ -1752,7 +1759,7 @@ module Spill : sig
 
   val spill_chr :
     State.t -> types:Types.types C.Map.t -> modes:(constant -> mode) ->
-      (constant list * constant list * prechr_rule list) -> (constant list * constant list * prechr_rule list)
+      block_constraint -> block_constraint
   
   (* Exported to compile the query *)
   val spill_preterm :
@@ -2000,9 +2007,9 @@ end = struct (* {{{ *)
       option_mapacc (spill_presequent state modes types pcloc) pamap pnew_goal in
     { r with pguard; pnew_goal; pamap }
 
-  let spill_chr state ~types ~modes (hyps, clique, rules) =
+  let spill_chr state ~types ~modes {ctx_filter; clique; rules} =
     let rules = List.map (spill_rule state modes types) rules in
-    (hyps, clique, rules)
+    {ctx_filter; clique; rules}
 
   let spill_clause state ~types ~modes ({ Ast.Clause.body = { term; amap; loc; spilling } } as x) =
     if not spilling then x
@@ -2098,7 +2105,7 @@ let assemble flags state code  (ul : compilation_unit list) =
   let chr = List.concat (code.Assembled.chr :: List.rev chr_rev) in
   let chr =
     let pifexpr { pifexpr } = pifexpr in
-    List.map (fun (hyps, symbs,rules) -> hyps, symbs, filter_if flags pifexpr rules) chr in
+    List.map (fun {ctx_filter;clique;rules} -> {ctx_filter;clique;rules=filter_if flags pifexpr rules}) chr in
   state, { Assembled.clauses_rev; types; type_abbrevs; modes; chr; local_names = code.Assembled.local_names; toplevel_macros = code.Assembled.toplevel_macros }
 
 end (* }}} *)
@@ -2491,8 +2498,8 @@ let run
   check_no_regular_types_for_builtins state types;
   (* Real Arg nodes: from "Const '%Arg3'" to "Arg 3" *)
   let state, chr =
-    List.fold_left (fun (state, chr) (hyps, clique, rules) ->
-      let chr, clique = CHR.new_clique (Symbols.show state) hyps clique chr in
+    List.fold_left (fun (state, chr) {ctx_filter; clique; rules} ->
+      let chr, clique = CHR.new_clique (Symbols.show state) ctx_filter clique chr in
       let state, rules = map_acc (compile_chr initial_depth) state rules in
       List.iter (check_rule_pattern_in_clique state clique) rules;
       state, List.fold_left (fun x y -> CHR.add_rule clique y x) chr rules)
diff --git a/src/parser/ast.ml b/src/parser/ast.ml
index 9c16a4140..5491db4dd 100644
--- a/src/parser/ast.ml
+++ b/src/parser/ast.ml
@@ -298,22 +298,27 @@ type program = {
   modes : Func.t Mode.t list;
   body : block list;
 }
+and cattribute = {
+  cid : string;
+  cifexpr : string option
+}
+and block_constraint = {
+   clique : Func.t list;
+   ctx_filter : Func.t list;
+   rules : cattribute Chr.t list
+}
 and block =
   | Locals of Func.t list * program
   | Clauses of (Term.t,attribute) Clause.t list
   | Namespace of Func.t * program
   | Shorten of Func.t shorthand list * program
-  | Constraints of Func.t list * Func.t list * cattribute Chr.t list * program
+  | Constraints of block_constraint * program
 and attribute = {
   insertion : insertion option;
   id : string option;
   ifexpr : string option;
 }
 and insertion = Before of string | After of string | Replace of string
-and cattribute = {
-  cid : string;
-  cifexpr : string option
-}
 and tattribute =
   | External
   | Index of int list * tindex option
diff --git a/src/parser/ast.mli b/src/parser/ast.mli
index a32a67f0f..0fea5a9fb 100644
--- a/src/parser/ast.mli
+++ b/src/parser/ast.mli
@@ -197,12 +197,17 @@ type program = {
   modes : Func.t Mode.t list;
   body : block list;
 }
+and block_constraint = {
+   clique : Func.t list;
+   ctx_filter : Func.t list;
+   rules : cattribute Chr.t list
+}
 and block =
   | Locals of Func.t list * program
   | Clauses of (Term.t,attribute) Clause.t list
   | Namespace of Func.t * program
   | Shorten of Func.t shorthand list * program
-  | Constraints of Func.t list * Func.t list * cattribute Chr.t list * program
+  | Constraints of block_constraint * program
 and attribute = {
   insertion : insertion option;
   id : string option;

From a725416e372014fe490d4cba5034ac0ee9daa93f Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 23 Jul 2024 16:29:48 +0200
Subject: [PATCH 04/10] ctx_filter union when same constants in the head of a
 constraint

---
 src/data.ml                            | 47 +++++++++++++++-----------
 src/runtime.ml                         |  5 +--
 tests/sources/chr_with_hypotheses.elpi | 25 +++++++++-----
 3 files changed, 46 insertions(+), 31 deletions(-)

diff --git a/src/data.ml b/src/data.ml
index ba715696c..8939c37a7 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -590,7 +590,7 @@ module CHR : sig
   val empty : t
 
   val new_clique : (constant -> string) -> constant list -> constant list -> t -> t * clique
-  val clique_of : constant -> t -> Constants.Set.t option
+  val clique_of : constant -> t -> (Constants.Set.t * Constants.Set.t) option
   val add_rule : clique -> rule -> t -> t
   val in_clique : clique -> constant -> bool
   
@@ -602,7 +602,7 @@ module CHR : sig
 
 end = struct (* {{{ *)
 
-  type clique = Constants.Set.t [@@deriving show]
+  type clique = {ctx_filter: Constants.Set.t; clique: Constants.Set.t} [@@deriving show]
   type sequent = { eigen : term; context : term; conclusion : term }
   and rule = {
     to_match : sequent list;
@@ -624,37 +624,44 @@ end = struct (* {{{ *)
 
   let empty = { cliques = Constants.Map.empty; rules = Constants.Map.empty }
 
-  let in_clique m c = Constants.Set.mem c m
+  let in_clique {clique; ctx_filter} c = Constants.Set.mem c clique
 
   let new_clique show_constant hyps cl ({ cliques } as chr) =
+    let open Constants in
     if cl = [] then error "empty clique";
-    let c = Constants.Set.of_list cl in
+    let c = Set.of_list cl in
+    let ctx_filter = Set.of_list hyps in
     
-    (* Non overlapping clique check *)
-    Constants.Map.iter (fun _ c' ->
-      if not (Constants.Set.is_empty (Constants.Set.inter c c')) && not (Constants.Set.equal c c') then
-        error ("overlapping constraint cliques: {" ^
-          String.concat "," (List.map show_constant (Constants.Set.elements c))^"} {" ^
-          String.concat "," (List.map show_constant (Constants.Set.elements c'))^ "}")
-    ) cliques;
-
-    (* Add constants in the context (for hypotheses) *)
-    let c = List.fold_right Constants.Set.add hyps c in
-    let cliques =
-      List.fold_right (fun x cliques -> Constants.Map.add x c cliques) (hyps @ cl) cliques in
-    { chr with cliques }, c
+    (* Check new inserted clique is valid *)
+    let build_clique_str c =
+      Printf.sprintf "{ %s }" @@ String.concat "," (List.map show_constant (Set.elements c)) 
+    in
+    let old_ctx_filter = ref None in
+    let exception Stop in
+    (try 
+      Map.iter (fun _ ({clique=c';ctx_filter=ctx_filter'}) ->
+        if Set.equal c c' then (old_ctx_filter := Some ctx_filter'; raise Stop)
+        else if not (Set.disjoint c c') then (* different, not disjoint clique *)
+          error ("overlapping constraint cliques:" ^ build_clique_str c ^ "and" ^ build_clique_str c')
+      ) cliques;
+    with Stop -> ());
+    let clique = 
+      {ctx_filter = Set.union ctx_filter (Option.value ~default:Set.empty !old_ctx_filter); clique=c} in
+    let (cliques: clique Constants.Map.t) =
+      List.fold_left (fun cliques x -> Constants.Map.add x clique cliques) cliques cl in
+    { chr with cliques }, clique
 
   let clique_of c { cliques } =
-    try Some (Constants.Map.find c cliques)
+    try Some (let res = Constants.Map.find c cliques in res.clique, res.ctx_filter)
     with Not_found -> None
 
-  let add_rule cl r ({ rules } as chr) =
+  let add_rule ({clique}: clique) r ({ rules } as chr) =
     let rules = Constants.Set.fold (fun c rules ->
       try
         let rs = Constants.Map.find c rules in
         Constants.Map.add c (rs @ [r]) rules
       with Not_found -> Constants.Map.add c [r] rules)
-      cl rules in
+      clique rules in
     { chr with rules }
 
 
diff --git a/src/runtime.ml b/src/runtime.ml
index 874412cef..9c6161f8d 100644
--- a/src/runtime.ml
+++ b/src/runtime.ml
@@ -3415,9 +3415,10 @@ let declare_constraint ~depth prog (gid[@trace]) args =
     | _ -> type_error "declare_constraint takes at least one argument"
   in 
   match CHR.clique_of (head_of g) !chrules with
-  | Some clique -> (* real constraint *)
+  | Some (clique, ctx_filter) -> (* real constraint *)
      (* XXX head_of is weak because no clausify ? XXX *)
-     delay_goal ~filter_ctx:(fun { hsrc = x } -> C.Set.mem (head_of x) clique)
+     delay_goal ~filter_ctx:(fun { hsrc = x } -> 
+        C.Set.mem (head_of x) clique || C.Set.mem (head_of x) ctx_filter)
        ~depth prog ~goal:g (gid[@trace]) ~on:keys
   | None -> delay_goal ~depth prog ~goal:g (gid[@trace]) ~on:keys
 
diff --git a/tests/sources/chr_with_hypotheses.elpi b/tests/sources/chr_with_hypotheses.elpi
index c50035d83..74320bf38 100644
--- a/tests/sources/chr_with_hypotheses.elpi
+++ b/tests/sources/chr_with_hypotheses.elpi
@@ -4,6 +4,7 @@ pred q i:int.
 pred trig1.
 
 pred acc i:int.
+pred acc1 i:int.
 
 pred tester i:string, i:list prop, i:int.
 tester Str Ctx Var :-
@@ -12,10 +13,14 @@ tester Str Ctx Var :-
   Ctx => acc Var,
   print "SUCCESS !!".
 
-% the syntax `acc ?-` is used to load acc clauses as hypothesis in the context
+% the syntax `acc ?-` is used to load acc1 clauses as hypothesis in the context
+constraint acc1 ?- p trig {
+  rule \ trig (Ctx ?- p A) | (std.mem! Ctx (acc 2)) <=> (Ctx => (acc 2, acc1 A)).
+}
+
+% this extends the previous constraint
 constraint acc ?- p trig {
-  rule trig \ (Ctx ?- p A) <=> (tester "p" Ctx A).
-  rule \ trig.
+  rule \ trig (Ctx ?- p A) <=> (Ctx => (acc A, acc1 A)).
 }
 
 % here again `acc ?-` is used but the clique error message is not thrown, since,
@@ -25,9 +30,11 @@ constraint acc ?- q trig1 {
   rule \ trig1.
 }
 
-main :- acc 3 => declare_constraint (p 3) [_], declare_constraint trig [_],
-        acc 4 => declare_constraint (q 4) [_], declare_constraint trig1 [_],
-        print "Constraint store is empty ?",
-        print_constraints, % Should be empty
-        print "End print Constraitn store",
-        acc 4 => declare_constraint (q 5) [_], not (declare_constraint trig1 [_]).
\ No newline at end of file
+main :- std.do![
+  acc 4 => declare_constraint (q 4) [_], declare_constraint trig1 [_],
+  acc 4 => declare_constraint (q 5) [_], not (declare_constraint trig1 [_]),
+  
+  acc 3 => acc1 3 => declare_constraint (p 3) [_], declare_constraint trig [_], !,
+  acc 4 => acc1 5 => declare_constraint (p 4) [_], not (declare_constraint trig [_]), 
+  acc 2 => acc1 4 => declare_constraint (p 4) [_], declare_constraint trig [_],
+].
\ No newline at end of file

From db0cd9fc9a318fd6f445779860df73ddb5748a34 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 24 Jul 2024 09:57:36 +0200
Subject: [PATCH 05/10] refactor test

---
 tests/sources/chr_with_hypotheses.elpi | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/tests/sources/chr_with_hypotheses.elpi b/tests/sources/chr_with_hypotheses.elpi
index 74320bf38..44d98cc37 100644
--- a/tests/sources/chr_with_hypotheses.elpi
+++ b/tests/sources/chr_with_hypotheses.elpi
@@ -1,5 +1,6 @@
 pred p i:int.
 pred trig.
+
 pred q i:int.
 pred trig1.
 
@@ -30,11 +31,16 @@ constraint acc ?- q trig1 {
   rule \ trig1.
 }
 
-main :- std.do![
+pred q&trig1.
+q&trig1 :-
   acc 4 => declare_constraint (q 4) [_], declare_constraint trig1 [_],
-  acc 4 => declare_constraint (q 5) [_], not (declare_constraint trig1 [_]),
-  
-  acc 3 => acc1 3 => declare_constraint (p 3) [_], declare_constraint trig [_], !,
+  acc 4 => declare_constraint (q 5) [_], not (declare_constraint trig1 [_]).
+
+pred p&trig.
+p&trig :-
+  acc 3 => acc1 3 => declare_constraint (p 3) [_], declare_constraint trig [_],
   acc 4 => acc1 5 => declare_constraint (p 4) [_], not (declare_constraint trig [_]), 
-  acc 2 => acc1 4 => declare_constraint (p 4) [_], declare_constraint trig [_],
-].
\ No newline at end of file
+  acc 2 => acc1 4 => declare_constraint (p 4) [_], declare_constraint trig [_].
+
+main :-
+  p&trig, q&trig1.
\ No newline at end of file

From 8c7f985711975b9e2e60cca240279769e7ce261c Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 24 Jul 2024 10:15:18 +0200
Subject: [PATCH 06/10] !!! THIS COMMIT SHOWS A BUG: the std.spy-do! seems to
 wrongly interact with the chr

---
 tests/sources/chr_with_hypotheses.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/sources/chr_with_hypotheses.elpi b/tests/sources/chr_with_hypotheses.elpi
index 44d98cc37..ee295003c 100644
--- a/tests/sources/chr_with_hypotheses.elpi
+++ b/tests/sources/chr_with_hypotheses.elpi
@@ -39,7 +39,7 @@ q&trig1 :-
 pred p&trig.
 p&trig :-
   acc 3 => acc1 3 => declare_constraint (p 3) [_], declare_constraint trig [_],
-  acc 4 => acc1 5 => declare_constraint (p 4) [_], not (declare_constraint trig [_]), 
+  std.spy-do![acc 4 => acc1 5 => declare_constraint (p 4) [_], not (declare_constraint trig [_])], 
   acc 2 => acc1 4 => declare_constraint (p 4) [_], declare_constraint trig [_].
 
 main :-

From 02a58dfef610ece50a4ec97d48107be2f89e75d0 Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Wed, 24 Jul 2024 10:26:11 +0200
Subject: [PATCH 07/10] update changelog

---
 CHANGES.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/CHANGES.md b/CHANGES.md
index 60a3f57b4..5f8925714 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,7 +2,13 @@
 
 - Compiler:
   - Improve performance of separate compilation
-  
+- CHR:
+  - Syntax extension for constraint declaration.
+  - This aims to avoid the `overlapping` clique error
+  - Example: `constraint c t x ?- p1 p2 { rule (Ctx ?- ...) <=> (Ctx => ...) }`
+  - `c`, `t` and `x` are the symbols which should be loaded in the rule of the
+    constraint and should be considered as symbols composing the context (`Ctx`)
+    under which `p1` and `p2` are used.
 
 # v1.19.4 (July 2024)
 

From 387e6fcd2c4ef15fb5fa06e5bd1c34f691f13b5c Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 30 Jul 2024 14:58:49 +0200
Subject: [PATCH 08/10] Revert "!!! THIS COMMIT SHOWS A BUG: the std.spy-do!
 seems to wrongly interact with the chr"

This reverts commit 8c7f985711975b9e2e60cca240279769e7ce261c.
---
 tests/sources/chr_with_hypotheses.elpi | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/sources/chr_with_hypotheses.elpi b/tests/sources/chr_with_hypotheses.elpi
index ee295003c..44d98cc37 100644
--- a/tests/sources/chr_with_hypotheses.elpi
+++ b/tests/sources/chr_with_hypotheses.elpi
@@ -39,7 +39,7 @@ q&trig1 :-
 pred p&trig.
 p&trig :-
   acc 3 => acc1 3 => declare_constraint (p 3) [_], declare_constraint trig [_],
-  std.spy-do![acc 4 => acc1 5 => declare_constraint (p 4) [_], not (declare_constraint trig [_])], 
+  acc 4 => acc1 5 => declare_constraint (p 4) [_], not (declare_constraint trig [_]), 
   acc 2 => acc1 4 => declare_constraint (p 4) [_], declare_constraint trig [_].
 
 main :-

From c85b39eb9723166b725b86371e520ee25833eeef Mon Sep 17 00:00:00 2001
From: Davide Fissore <fisso9900@gmail.com>
Date: Tue, 30 Jul 2024 15:14:27 +0200
Subject: [PATCH 09/10] ELPI.md explication of `?-` in the head a constraint
 for clause filtering

---
 ELPI.md | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 54 insertions(+), 6 deletions(-)

diff --git a/ELPI.md b/ELPI.md
index 6a1990fb7..b17aee63e 100644
--- a/ELPI.md
+++ b/ELPI.md
@@ -461,15 +461,62 @@ The `constraint` directive gives control on the hypothetical part of the
 program that is kept by the suspended goal and lets one express constraint
 handling rules.
 
-A "clique" of related predicates is declared with
+A new constraint can be declared with the following syntax:
 ```prolog
-constraint foo bar ... {
+constraint p1 p2 p3 ?- foo bar {
+  rule (Ctx ?- foo Arg1) | ... <=> (Ctx => bar Arg1)
+}
+```
+
+> [!IMPORTANT]
+> When a suspended goal (via `declare_constraint`) is resumed, only the rules
+implementing the symbols passed in the head of the constraint are kept. 
+
+In our example, only the rules for `p1, p2, p3, foo` and `bar` are kept.
+Therefore, if just before the suspension of the goal `foo x` a rule like `p4`
+exists, this rule will not be filtered out from the rules in the suspended goal.
+
+The symbol `?-` in the head of a constraint is used to separate two lists of
+predicate names, the former list represents predicate names to be loaded as a
+predicate filter to load the wanted rules as hypotheses in the context, whereas
+the latter list contains predicates to be used in the new premises to be solved.
+
+In the example above, the rules implementing `p1`, `p2` and `p3` are filtered in
+in the suspended goal, that is, they are loaded into `Ctx`. Therefore, when
+solving the goal  `Ctx => bar Arg1` all the rules for these three predicates are
+charged.
+
+The list of predicate names after the `?-` should form a "clique", a set of
+symbols disjoint from all the other cliques in the constraint store. If two
+overlapping cliques are detected, the fatal error *overlapping constraint
+cliques* is raised. The overlapping check is not applied to the list of
+hypotheses symbols before `?-`, that is, in the case of two constraints declared
+on two same cliques `c` with different hypothesis `h1` and `h2`, then the two
+set of hypotheses are merged and added to the clique `c`.
+
+For example, if we keep the example above, the following code snipped would
+correctly extend the previous constraint:
+
+```
+constraint p4 ?- foo bar {
   rule ...
 }
 ```
-The effect is that whenever a goal about `foo` or `bar`
-is suspended (via `declare_constraint`) only its hypothetical
-clauses about `foo` or `bar` are kept.
+
+From now on, all the goals suspended on the predicates `foo` and `bar` will see
+in their contexts the four all the rules implementing the predicates `p1, p2,
+p3, p4` = $\{$`p1,p2,p3`$\} \cup \{$`p4`$\}$.
+
+> [!NOTE]
+> If the list of predicate names before `?-` is empty, then the `?-` can be avoided  
+
+Example: `constraint foo bar { ... }`. In this case the new suspended goals
+talking about `foo` and `bar` will consider the rules for the predicates `p1,
+p2, p3` = $\{$`p1,p2,p3`$\} \cup \varnothing$.
+
+Finally `constraint foo bax { ... }.` raise the overlapping clique error, since
+this constraint set intersect with another clique, i.e. $\{$`foo,bax`$\} \cap
+\{$`foo, bar`$\} \neq \varnothing$. 
 
 When one or more goals are suspended on lists of unification
 variables with a non-empty intersection, 
@@ -519,7 +566,8 @@ Failure
 #### Syntax
 Here `+` means one or more, `*` zero or more
 ```
-CONSTRAINT ::= constraint CLIQUE { RULE* }
+CTX_FILTER ::= CLIQUE ?-
+CONSTRAINT ::= constraint CTX_FILTER? CLIQUE { RULE* }
 CLIQUE ::= NAME+
 RULE ::= rule TO-MATCH TO-REMOVE GUARD TO-ADD .
 TO-MATCH  ::= SEQUENT*

From 2e2eecdd07a4f4a68af0a8aae547db59c2b03141 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Tue, 30 Jul 2024 15:28:09 +0200
Subject: [PATCH 10/10] Apply suggestions from code review

---
 ELPI.md | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/ELPI.md b/ELPI.md
index b17aee63e..34dcdac3f 100644
--- a/ELPI.md
+++ b/ELPI.md
@@ -474,25 +474,24 @@ implementing the symbols passed in the head of the constraint are kept.
 
 In our example, only the rules for `p1, p2, p3, foo` and `bar` are kept.
 Therefore, if just before the suspension of the goal `foo x` a rule like `p4`
-exists, this rule will not be filtered out from the rules in the suspended goal.
+exists, this rule will be filtered out from the context of the suspended goal.
 
-The symbol `?-` in the head of a constraint is used to separate two lists of
-predicate names, the former list represents predicate names to be loaded as a
-predicate filter to load the wanted rules as hypotheses in the context, whereas
-the latter list contains predicates to be used in the new premises to be solved.
+The symbol `?-` separates two lists of
+predicate names: the former list is a predicate filter for the context;
+the latter list is a predicate filer for the goal.
 
-In the example above, the rules implementing `p1`, `p2` and `p3` are filtered in
-in the suspended goal, that is, they are loaded into `Ctx`. Therefore, when
+In the example above, the rules implementing `p1`, `p2` and `p3` are kep in
+in the suspended goal context. Therefore, when
 solving the goal  `Ctx => bar Arg1` all the rules for these three predicates are
-charged.
+part of `Ctx`.
 
 The list of predicate names after the `?-` should form a "clique", a set of
 symbols disjoint from all the other cliques in the constraint store. If two
 overlapping cliques are detected, the fatal error *overlapping constraint
-cliques* is raised. The overlapping check is not applied to the list of
-hypotheses symbols before `?-`, that is, in the case of two constraints declared
-on two same cliques `c` with different hypothesis `h1` and `h2`, then the two
-set of hypotheses are merged and added to the clique `c`.
+cliques* is raised. The overlapping check is not applied to the context filters,
+that is, in the case of two constraints declared
+on two same cliques `c` with different filters `h1` and `h2`, then the two
+filters are merged and added to the clique `c`.
 
 For example, if we keep the example above, the following code snipped would
 correctly extend the previous constraint:
@@ -504,11 +503,11 @@ constraint p4 ?- foo bar {
 ```
 
 From now on, all the goals suspended on the predicates `foo` and `bar` will see
-in their contexts the four all the rules implementing the predicates `p1, p2,
+in their contexts the all the rules implementing the predicates `p1, p2,
 p3, p4` = $\{$`p1,p2,p3`$\} \cup \{$`p4`$\}$.
 
 > [!NOTE]
-> If the list of predicate names before `?-` is empty, then the `?-` can be avoided  
+> If the list of predicate names before `?-` is empty, then the `?-` can be omitted  
 
 Example: `constraint foo bar { ... }`. In this case the new suspended goals
 talking about `foo` and `bar` will consider the rules for the predicates `p1,