Stream: Elpi users & devs

Topic: use of copy with variables


view this post on Zulip Enzo Crance (Oct 21 2022 at 14:16):

Hello. I would like to replace a record projection with a custom term, i.e. for p (f args) x with p a field, f a function giving a record when applied, args some arguments required to get the record, and x a value, how can I change this term with g args x, g being a custom function I give?

I tried to use copy for that:

copy (app [app [pglobal P _, _, _], app [F|Args], X]) (app [G|ArgsX]) :- !,
  std.append Args [X] ArgsX.

(the underscores are the universe instance for the field and 2 type arguments that are implicit, but as I remove this idc about their value)
but it looks like it does not work. The following term is left as is:

app [
  app [pglobal (const «f») (X6^7 c8), X16 c0 c1 c2 c3 c4 c5 c6 c8, X17 c0 c1 c2 c3 c4 c5 c6 c8],
  app [c6, c3, c4, c5],
  c9
]

whereas I would expect

app [G, c3, c4, c5, c9]

I think it's because of the binders and the fact the undefined variables depend on the binders... Do you have a suggestion?
NB: the nested apps are normal, it's a temporary forged term, not something I read from Coq, eventually I will use coq.mk-app

view this post on Zulip Enrico Tassi (Oct 21 2022 at 15:09):

Did you put the clause :before "copy:start"?

view this post on Zulip Enzo Crance (Oct 21 2022 at 15:10):

Do you mean the arrow actually adds predicates at the end by default? I thought it was at the beginning

view this post on Zulip Enrico Tassi (Oct 21 2022 at 15:10):

(also nested app seem wrong)

view this post on Zulip Enzo Crance (Oct 21 2022 at 15:12):

Enzo Crance said:

Do you mean the arrow actually adds predicates at the end by default? I thought it was at the beginning

Sorry for lack of context, I am saying this because I am adding the instance of copy with => before the copy call, and IIUC it's added at the top, otherwise the copy ... => copy ... paradigm wouldn't work

view this post on Zulip Enzo Crance (Oct 21 2022 at 15:12):

I can fix the nested app issue first but I thought it did not interfere with this

view this post on Zulip Enrico Tassi (Oct 21 2022 at 18:08):

Hum, note that copy is in input mode (on the first argument). So X16 does not match (app [F|Args]).

view this post on Zulip Enzo Crance (Oct 24 2022 at 11:42):

X16 ... should match _ and I think that's what does not work, but cannot find why

view this post on Zulip Enrico Tassi (Oct 24 2022 at 11:47):

I can only suggest Elpi Trace "copy". and see what fails.

view this post on Zulip Enzo Crance (Oct 24 2022 at 12:12):

Found the weird unification failure...

rid:0 step:654 gid:725 user:backchain:fail-to =
  match
    app [
      pglobal (const «f») «Test.799»,
      app [pglobal (indt «list») «Test.783», c3],
      app [pglobal (indt «list») «Test.783», c4],
      app [c6, c3, c4, c5],
      c9
    ]
  with
    app [
      pglobal (const «f») _,
      _,
      _,
      app [c6, c3, c4, c5],
      X2^6
    ]

(reformatted for readability)

view this post on Zulip Enrico Tassi (Oct 24 2022 at 12:23):

X2^6 does not see c9

view this post on Zulip Enrico Tassi (Oct 24 2022 at 12:23):

X2^6 = X2 c0 c1 c2 c3 c4 c5

view this post on Zulip Enzo Crance (Oct 24 2022 at 12:26):

Ok thanks for the notation unfolding. I did not know about this ^6 meaning has the 6 variables in its scope. I will investigate further

view this post on Zulip Enrico Tassi (Oct 24 2022 at 12:40):

I've never seen you code, maybe you forgot to (pi Args\ in front of the clause or something like that

view this post on Zulip Enzo Crance (Oct 24 2022 at 12:45):

I don't think so, but the clause for copy is added under a lambda given to std.map, with an output expressed as a function of several variables. I think I am mixing a lot of binding logic and I should try to write my code in separate predicates.

view this post on Zulip Enzo Crance (Oct 24 2022 at 13:09):

Ok I understood the bug. It is indeed a pi Args\ ... problem. The variables I use in the clause I add are not really fresh, I cannot write the predicate like I am at toplevel, because the clause is added from somewhere, so all the variables are specific variables instantiated at the place I add the copy instance. It means that if I copy a term that is under further binders, as the variable is not really universal, it has been instantiated higher so it does not see all binders.

TLDR: when adding a predicate clause to the context, quantify explicitly all the variables that must not be local to the call site with pi. I will add this to the list of warnings I want to give to future Elpi users ;)

view this post on Zulip Enzo Crance (Oct 24 2022 at 13:10):

Thank you for your hints


Last updated: Feb 05 2023 at 15:03 UTC