Michael Soegtrop (Jan 17 2024 at 14:21): Michael Soegtrop (Jan 17 2024 at 14:21):I have a question on decl and pi. When going under a binder I use constructs like defined with macro @pi-decl N T F :- pi x\ decl x N T => F x.. I figured out that if I want to check if a term X is a variable bound this way, I just check if there is a decl X _ _ in the database.
I am wondering if using the specific predicate decl has any significance here (sort of special handling in some way), or if I can use any other predicate, say with additional arguments to keep track of indices or whatever. Apparently this does work, but I wanted to double check before I write a lot of code using this.
Enrico Tassi (Jan 17 2024 at 22:41):decl is special in the sense that APIs like coq.typecheck use these clauses to build a proof context under which a term is processed.
But you can do @pi-decl N T x\ nice-variable x => bla (or pi x\ decl x N Ty => nice-variable x => .... bla), these extra rules are visible while running bla.
It's really how lambda Prolog works, I just "standardized" decl and def for attaching variables a type. Any other info is up to you (and is ignored by the existing APIs). FTR, there is also cache x NF (used next to def) to cache the normal form of the let-in value. So just avoid def, decl and cache.
Enrico Tassi (Jan 17 2024 at 22:47):It is used everywhere, see for one example https://github.com/LPCIC/coq-elpi/blob/75b619727c7ae8e22e79b1a70331afa9c47f8eba/apps/derive/elpi/param1.elpi#L27
Michael Soegtrop (Jan 18 2024 at 08:37):Thanks, interesting! One more thought: would it work to use a different predicate than decl in pi with additional arguments and then add a clause to the decl database which redirects to this other predicate via decl x N T :- my_decl x N T _ . ?
Enrico Tassi (Jan 18 2024 at 09:09):nope, the "context readback" function is very simple, it looks for decl verbatim.
Imo you should my-extra-decl x Extra => and then have a clause my-decl x Ty Extra :- decl x _ Ty, my-extra-decl x Extra.
Michael Soegtrop (Jan 18 2024 at 10:12):Thanks, I will try this!
Last updated: Oct 13 2024 at 01:02 UTC