Stream: Elpi users & devs

Topic: ✔ Spilling under a binder


view this post on Zulip James Wood (May 10 2022 at 12:30):

What is the elaboration of the spilling ({ ... }) in this predicate?

  pred foo  i:(C -> (A -> B) -> B), i:list C, i:(list A -> B), o:B.
  foo _C [] B (B []).
  foo C [X|Xs] B (C X y\ {foo C Xs ys\ B [y|ys]}).

view this post on Zulip Enrico Tassi (May 10 2022 at 13:00):

You shouldn't be allowed to spill in the head of a clause, IIRC.

elpi -print foo.elpi should answer the question. I'm away from my pc sorry.

view this post on Zulip James Wood (May 10 2022 at 13:13):

Aha, the error is shown lazily (even if I do Elpi Typecheck.). Is there a way to achieve what I intended, then? I can write a rough equivalent in Gallina or OCaml or whatever, but I don't know how I'd do it in λProlog.

view this post on Zulip James Wood (May 10 2022 at 13:14):

(Also, this error message Conjunction in the head of a clause is not supported makes a bit more sense now. Thanks!)

view this post on Zulip James Wood (May 10 2022 at 13:20):

Maybe to give some more context of what I'm trying to do: I'm trying to produce an inductive type declaration whose uniform parameters have types given by a list. So my declaration looks like parameter "A" explicit {{Set}} a\ parameter "B" explicity {{Set}} b\ ... parameter "Z" explicit {{Set}} z\ inductive ...[a, b, ..., z], with the inductive ... part playing the role of B above, and the parameter stuff playing the role of C.

view this post on Zulip James Wood (May 10 2022 at 13:26):

Okay, I can do an easy change to get the spilling to work, and it does what I intended:

  pred foo  i:(C -> (A -> B) -> B), i:list C, i:(list A -> B), o:B.
  foo _C [] B (B []).
  foo C [X|Xs] B R :-
    R = C X y\ {foo C Xs ys\ B [y|ys]}.

view this post on Zulip James Wood (May 10 2022 at 14:04):

Aha, I think I've worked out a possible elaboration. It does the right thing on my one test case, anyway.

  pred foo  i:(C -> (A -> B) -> B), i:list C, i:(list A -> B), o:B.
  foo _C [] B (B []).
  foo C [X|Xs] B R :-
    (pi y\ foo C Xs (ys\ B [y|ys]) (TMP y)),
    R = C X TMP.

view this post on Zulip Enrico Tassi (May 10 2022 at 20:28):

OK, I'm back at my computer but it seems you figured it out.
FTR, Elpi Print ... can generate an HTML file with the clauses in elaborated form, so that you can check your spilling is right.

About your foo predicate, I did too have a reflex (from FP I guess) of writing HO iterators, but clauses are so compact that I often just rewrite the loop. But well, your code, your style ;-)

view this post on Zulip James Wood (May 11 2022 at 08:09):

By the way, what's the history of spilling? Do any other logic programming languages have something like it?

view this post on Zulip Enrico Tassi (May 11 2022 at 08:31):

No that I know of, it just felt natural to implement it in Elpi. Later Dale and Ulisses did something similar, but in the reasoning logic of Abella here. Since there are too many "not implemented" in my code, I never tried to publish it.

On the side, the feature is quite advanced wrt the coq embedding, for example if you spill under a coq binder you get the expected context, eg

R = {{ forall x : nat, lp:{{   {foo}  }}  }}

you should get something like

(pi x\ decl x `x` {{ nat }} => foo (TMP x)),
R = {{ forall x : nat, lp:(TMP x) }}

view this post on Zulip Enrico Tassi (May 11 2022 at 08:32):

But I rarely use that feature myself, while @Cyril Cohen does.

view this post on Zulip Enrico Tassi (May 11 2022 at 08:34):

Anyway, feedback on the feature is welcome. Even more understanding/implementing the missing cases ;-)

view this post on Zulip James Wood (May 11 2022 at 08:42):

Interesting, thanks!

view this post on Zulip Notification Bot (May 11 2022 at 08:42):

James Wood has marked this topic as resolved.


Last updated: Mar 29 2024 at 12:02 UTC