James Wood (May 10 2022 at 12:30): 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]}).
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.
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.
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!)
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.
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]}.
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.
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 ;-)
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?
Last updated: Feb 04 2023 at 02:03 UTC