Stream: Elpi users & devs

Topic: use of copy with variables

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

Enrico Tassi (Oct 21 2022 at 15:09):

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

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

Enrico Tassi (Oct 21 2022 at 15:10):

(also nested app seem wrong)

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

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

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]).

Enzo Crance (Oct 24 2022 at 11:42):

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

Enrico Tassi (Oct 24 2022 at 11:47):

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

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)

Enrico Tassi (Oct 24 2022 at 12:23):

X2^6 does not see c9

Enrico Tassi (Oct 24 2022 at 12:23):

X2^6 = X2 c0 c1 c2 c3 c4 c5

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

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

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.

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 ;)

Enzo Crance (Oct 24 2022 at 13:10):

Thank you for your hints

Last updated: Oct 13 2024 at 01:02 UTC