Skip to content

Introduce mem-rel! function in builtin_stdlib.elpi #381

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
+5 −2
Open

Introduce mem-rel! function in builtin_stdlib.elpi #381

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions src/builtin_stdlib.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,10 @@ mem [_|L] X :- mem L X.

func exists! list A, (pred A).
exists! [X| _] P :- P X, !.
exists! [_|XS] P :- exists! XS P.
exists! [_|XS] P :- exists! XS P.

func mem-rel! A, (pred A B), list B.
mem-rel! A R L :- exists! L (B\ R A B).
Copy link
Contributor

@gares gares Oct 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm a bit lost, the implementation of mem-rel! A R L is literally exists! L (R A), I don't get what one gains by using the new API.

In particular I don't get the example with map and swap. The {{ are the Rocq ones?

Copy link
Author

@patrick-nicodemus patrick-nicodemus Oct 29, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In particular I don't get the example with map and swap. The {{ are the Rocq ones?

Sorry, I mixed up the notation with Rocq quotation and spilling. I meant spilling. I have edited my comment.

I'm a bit lost, the implementation of mem-rel! A R L is literally exists! L (R A), I don't get what one gains by using the new API.

You are probably right, maybe it is not useful. My point is that:

  • if I want to check if A is an element of a list L, I can do mem! A L
  • if I want to check if f A is an element of a list L, I can do mem! {f A} L
  • if I want to check if A is an element of map g L, my first instinct is to write it as mem! A {map g L}, but this is inefficient.

I guess this solution is obvious but I am suggesting that it is a special case of exists! that could be more commonly used, for example we could define mem! X L as exists! L (Y\ X = Y) but it has its own name mem! instead.

Maybe it would be more useful if R was flipped,
something like

mem-map! A G L :- exists! L (Y\ G Y A).

so that
mem-map! A G L iff mem! A {map G L}

Copy link
Contributor

@gares gares Oct 30, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see. In this case I usually prefer the non-cutting (relational) combinators (some of which are not even in elpi stdlib) and write mem X L, g X Y, !. It is really generate + test (and commit if cut).

It seems more of a "style" than an API to me. So I'm happy to add all the APIs to make the style comfortable.

Maybe generate-test P Q could be an idiomatic way to express that, but I'm not so sure it is as flexible as just putting two relational predicates together with ,. Maybe some logic-programming DSL for functional languages like minikaren found a good set of APIs for that, but I'm a little ignorant there.


pred exists list A, (pred A).
exists [X|_] P :- P X.
Expand Down Expand Up @@ -318,4 +321,4 @@ max _ M M.
func findall prop -> list prop.
findall P L :- findall_solutions P L.

}
}