perfect discrimination tree fixes (weight + trace)

[petarvukmirovic]

perfect discrimination tree fixes (weight + trace)

[petarvukmirovic]

In HOL (even if you are limited only to pattern matching), larger terms can match smaller ones :

^[x,y,z]. F x z y matches ^[x,y,z]. G x

To circumvent this problem, there is a simple solution: do not calculate the actual exact weight, but whenever you have an applied variable you act as if it was a variable (and do not count argument terms). Also, to deal with eta-normalization, we consider all terms eta-expanded. However, we do not directly eta-expand them but just add the weight of extra db variables as needed.

[petarvukmirovic]

I am on it today.