Printing of metavariable names

[thiagofelicissimo]

There used to be a time in which, when lambdapi failed to verify that a rule preserves typing, the error message would show the metavariables with their actual names in the file. Since then, this has been changed and now metavariable names are replaced by numbers. Why has this change been made? Having the metavariable names is much more user-friendly and helpful in order to understand why the rule does not preserve typing.

[fblanqui]

Could you please provide an example?

[thiagofelicissimo]

constant symbol N : TYPE;
constant symbol 0 : N;

constant symbol P : N → TYPE;
constant symbol p0 : P 0;

symbol c (x : N) : P x;
rule c $x ↪ p0;

When typechecking this with Lambdapi (2.4.0) we get the message Cannot solve $1 ≡ 0 Unable to prove type preservation., so $x is replaced by $1. This is a toy example, but I have files in which my rules have many metavariables and knowing which one is which in the error message would much help.

[fblanqui]

Strictly speaking, expressions like $x are not metavariables; they are pattern variables. They have user-defined names. Metavariables have no user-defined names. Metavariables are generated by the system. Some long time ago, metavariables could have user-defined names. This has been removed long ago by Gabriel when introducing elaboration. See https://github.com/Deducteam/lambdapi/pull/696. For checking SR, pattern variables are replaced by metavariables. Therefore each user-defined pattern variable name is replaced by a number. Moreover, after that, to implement local confluence checking in https://github.com/Deducteam/lambdapi/pull/824/, I internally renamed pattern variables into indexes. In your example, $x is renamed into $0. Indeed, it would be nice for the user to know how their pattern variables are renamed. You can however already see it by adding debug +s; before the rule:

debug +s
[file:///home/blanqui/src/lambdapi/tmp/1021.lp:9:7-9]
Pattern variable x can be replaced by a '_'.
[subj] c $0 ↪ p0
[subj] replace pattern variables by metavariables: c ?9 ↪ p0
[subj] LHS type: P ?9
       LHS constraints: 
       c ?9 ↪ p0
[subj] replace LHS metavariables by function symbols: c $9 ↪ p0
Cannot solve $9 ≡ 0
Unable to prove type preservation.

[thiagofelicissimo]

I see, thanks for the debug +s; tip, it's already quite helpful. But are you planning on re-adding names in the future? I think it would be much better for the user experience, especially for those who don't know this debug flag.

[fblanqui]

Not immediately but feel free to make a PR ;-) It shouldn't be too difficult. At the end of sr.ml, in the constraints, you need to replace function symbols $i by the corresponding user-defined pattern variable name if it exists.