qname keyword

[FissoreD]

the goal is to extend the syntax with a qname keyword
this keyword works similarly to uvar during matching
the idea is shortcut:
p X :- name X into p (qname X)
this also gives benefit to mutual exclusion checker:
qname is different from any other rigid constructors

• fix all 3 indexes with qname
• fix mut-excl checker
• in rocq-elpi refactor copy, fold-map etc..
• check is_eigen_variable

[gares]

Do some benchmarks this way:

make git/master
make tests

[gares]

why q?

[FissoreD]

It is for quantified names.
I don't like it, and should be changed
In this first setup i didn't want to make collision with the already existsing name predicate

[gares]

I think we can make it collide. I did not want to use var because "variable" is very generic, not necessarily unification. But I don't see any confusion with name. Also, I should have added a uvar builtin predicate, synonym of var.

[FissoreD]

make tests gives me the following error
test not available, some build dependencies are missing
I tried the same command on master and get the same error.
This same error is thrown from launching the file ./tests/test.exe

EDIT: I found the problem, I should have installed ANSITerminal in my opam. With this dep it now works.
Should not opam install . -deps-only install this dep ?

[FissoreD]

I think we can make it collide. I did not want to use var because "variable" is very generic, not necessarily unification. But I don't see any confusion with name. Also, I should have added a uvar builtin predicate, synonym of var.

Going back to your comment, I'm not sure the typechecker is happy with this choice,
var is a predicate with at least one argument. While uvar can be used with 0 arguments.
Is this a source of problem?