✔ When does coq.elpi.accumulate take effect? · Elpi users & devs

Stream: Elpi users & devs

Topic: ✔ When does coq.elpi.accumulate take effect?

Michael Soegtrop (Nov 10 2022 at 14:47):

Building on the age example from the tutorial I wrote this code:

Require Import elpi.elpi.

Elpi Db age.db lp:{{
  pred age o:string, o:int.
  :name "age.fail"
  age Name _ :- coq.error "I don't know who" Name "is!".
}}.

Elpi Command set_age.
Elpi Accumulate Db age.db.
Elpi Accumulate lp:{{
  main [str Name, int Age] :-
    coq.say "Pre" Name Age,
    coq.elpi.accumulate _ "age.db" (clause _ (before "age.fail") (age Name Age)),
    age Name AgeDb,
    coq.say "Post" Name AgeDb.
}}.
Elpi Typecheck.

Elpi set_age "alice" 21.

The age query in the set_age main function fails, so obviously the statement has not yet been added at this point. I wonder what the rules are here.

Enrico Tassi (Nov 10 2022 at 15:07):

Accumulation happens when the program ends, the doc is a bit short:
https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L1644

This is how I usually do:

Require Import elpi.elpi.

Elpi Db age.db lp:{{
  pred age o:string, o:int.
  :name "age.fail"
  age Name _ :- coq.error "I don't know who" Name "is!".
}}.

Elpi Command set_age.
Elpi Accumulate Db age.db.
Elpi Accumulate lp:{{
  main [str Name, int Age] :-
    coq.say "Pre" Name Age,
    Clause = (age Name Age),
    coq.elpi.accumulate _ "age.db" (clause _ (before "age.fail") Clause),
    Clause => (
      age Name AgeDb,
      coq.say "Post" Name AgeDb
   ).
}}.
Elpi Typecheck.

Elpi set_age "alice" 21.

Enrico Tassi (Nov 10 2022 at 15:08):

In some sense coq.elpi.accumulate is "at compile time" what => is at runtime.

Notification Bot (Nov 10 2022 at 15:48):

Michael Soegtrop has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC