Merge pull request #246 from FissoreD/constraint-store-hypotheses

CHR: constraints allow hyps, not considered in the clique error check

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)
 

ELPI.md

@@ -461,15 +461,61 @@ 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 be filtered out from the context of the suspended goal.
+
+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 kep in
+in the suspended goal context. Therefore, when
+solving the goal  `Ctx => bar Arg1` all the rules for these three predicates are
+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 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:
+
+```
+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 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 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,
+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 +565,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*

src/compiler.ml

@@ -458,6 +458,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 = {
@@ -530,7 +537,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 block_constraint * pbody
+and typ = {
+  tindex : Ast.Structured.tattribute;
+  decl : type_declaration
+}
 [@@deriving show, ord]
 
 end
@@ -542,7 +553,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 : block_constraint list;
   local_names : int;
 }
 [@@deriving show]
@@ -556,7 +567,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 : block_constraint list;
   local_names : int;
 
   toplevel_macros : macro_declaration;
@@ -599,7 +610,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 : block_constraint list;
   initial_depth : int;
   query : preterm;
   query_arguments : 'a Query.arguments [@opaque];
@@ -737,13 +748,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, 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(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
@@ -1476,17 +1487,18 @@ 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 ({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, 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
           let lcs, state, types, type_abbrevs, modes, defs, compiled_rest =
             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({ctx_filter; clique; rules},p) :: compiled_rest
     in
     let state, local_names, toplevel_macros, pbody =
       compile_program toplevel_macros 0 state p in
@@ -1603,8 +1615,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_pair f g (x,y) = f x, g y
-
   type subst = (string list * C.t C.Map.t)
 
 
@@ -1636,9 +1646,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 =
-    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: (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))
@@ -1681,11 +1694,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 ({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 (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
@@ -1748,7 +1761,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)
+      block_constraint -> block_constraint
 
   (* Exported to compile the query *)
   val spill_preterm :
@@ -1996,9 +2009,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 {ctx_filter; clique; rules} =
     let rules = List.map (spill_rule state modes types) rules in
-    (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
@@ -2094,7 +2107,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 {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 (* }}} *)
@@ -2486,8 +2499,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) {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)

src/data.ml

@@ -589,18 +589,20 @@ module CHR : sig
 
   val empty : t
 
-  val new_clique : (constant -> string) -> constant list -> t -> t * clique
-  val clique_of : constant -> t -> Constants.Set.t option
+  val new_clique : (constant -> string) -> constant list -> constant list -> t -> t * clique
+  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
 
   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 = {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;
@@ -615,40 +617,51 @@ 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 in_clique {clique; ctx_filter} c = Constants.Set.mem c clique
 
-  let new_clique show_constant cl ({ cliques } as chr) =
+  let new_clique show_constant hyps cl ({ cliques } as chr) =
+    let open Constants in
     if cl = [] then error "empty clique";
-    let c = List.fold_right Constants.Set.add cl Constants.Set.empty in
-    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;
-    let cliques =
-      List.fold_right (fun x cliques -> Constants.Map.add x c cliques) cl cliques in
-    { chr with cliques }, c
+    let c = Set.of_list cl in
+    let ctx_filter = Set.of_list hyps in
+
+    (* 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 }
 
 

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
 
@@ -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 * 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