Fix some performance issues in reification

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components

33 stars 2 forks source link

Fix some performance issues in reification #26

Closed pi8027 closed 3 years ago

pi8027 commented 3 years ago

The bidirectional nat-constant predicate was too slow. Now we have two predicates:
```
pred int->nat i:int, o:term.
pred nat->int i:term, o:int.
```
The quote.nat predicate now reifies {{ S (S (..(S lp:N)..)) }} to {{ NatAdd (NatX lp:M) lp:N' }} where M is the number of nested successors in the input and N' is the reified term of N. This way, we can avoid vm_compute to detect constants of type nat. Note that this translation heavily relies on the specific implementation of addn.

gares commented 3 years ago

@pi8027 If conversions between Elpi's int and Coq's nat, positive, Z are a bottleneck, I can surely add them to the API (and implement these functions in OCaml). Would that help? As well as APIs to test if a term is a literal (eg, you find {{ S lp:X }} and you want to know if X is a closed nat fast).

pi8027 commented 3 years ago

@pi8027 If conversions between Elpi's int and Coq's nat, positive, Z are a bottleneck, I can surely add them to the API (and implement these functions in OCaml). Would that help?

Thanks, but I think we first have to identify some real bottlenecks. I don't think these conversions are not a bottleneck now. FYI, there is a performance issue worth investigating in apery.

As well as APIs to test if a term is a literal (eg, you find {{ S lp:X }} and you want to know if X is a closed nat fast).

I think this one is very useful to normalize exponents!