Stream: Elpi users & devs

Topic: Analogous of `(DB => Clause)` on CHR


view this post on Zulip Enrico Tassi (Jan 17 2024 at 22:54):

rules do have a guard (IIRC the right syntax is rule ... | guard <=> new_goal

view this post on Zulip Enrico Tassi (Jan 17 2024 at 22:55):

so you can enable/diable them. But the chr program runs in the "global" program, so a Db will work, but not a flag => declare_constraint ... (on anything along these lines)

view this post on Zulip Notification Bot (Jan 17 2024 at 22:57):

Enrico Tassi has marked this topic as unresolved.

view this post on Zulip Enrico Tassi (Jan 17 2024 at 23:00):

But I'd say the most orthodoxe way is to declare a constraint, e.g.phase-1, and have (some) rules match for its presence, and then load phase-2 (with a rule like phase-2 \ phase-1 to change phase when phase-2 is declared).

view this post on Zulip Cyril Cohen (Jan 18 2024 at 10:26):

I'm not sure I understand your last remark. I actually have two usecases:

  1. I have entries stuff X Y in my global db but I want to "activate them", so I store them with in an alternative db known-stuff Key X Y and when the user provides a SelectedKey argument to the tactic want to activate the known-stuff, so I translate known-stuff SelectedKey X Y to a list of prop DB of the shape stuff X Y and I use an implication, but for the CHR I need the trick we were discussing, so I "bulk-load" my new stuff in a dedicated predicate, I declare the constraint, and then I do the rule I was mentioning (if I switch to the guard as you suggested, then it stops working). For this there might be another solution but since I may have several SelectedKey active, and several X known for inactive known-stuff _ X Y , I do not know how to inform elpi to look only for X only in the SelectedKey entries without spending time exhausting the non selected ones.
  2. Anyway, I want to allow user to add stuff X Y on the fly, so I need the DB =>to work in some way inside CHR, so I reduced 1. to 2. and it worked well enough.

Last updated: Oct 13 2024 at 01:02 UTC