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?
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) }}
But I rarely use that feature myself, while @Cyril Cohen does.
Enrico Tassi (May 11 2022 at 08:34):Anyway, feedback on the feature is welcome. Even more understanding/implementing the missing cases ;-)
James Wood (May 11 2022 at 08:42):Interesting, thanks!
Notification Bot (May 11 2022 at 08:42):James Wood has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC