Commit 2022-11-29 19:28 24ac0e45

feat: better name guessing for to_additive (#779)

• @[to_additive] will now correctly guess names with CoeTC, CoeT and CoeHTCT in it
• rewrite function targetName.
  • It will now warn the user if it gives a composite name that can be auto-generated (before to_additive would never warn if a composite name was given).
  • the logic when allowAutoName = true now corresponds to the docstring
  • Fix a bug where declarations were silently allowed to translate to itself (maybe because the return statements returned a value for the whole function?)
  • Add some more tracing
  • The behavior of namespaces when giving a composite name has been changed. It will always generate a name with the same number of components. Example:

namespace MeasureTheory.MulMeasure
@[to_additive AddMeasure.myOperation] def myOperation := ...
-- before: generates `AddMeasure.myOperation` (and never gives a warning)
-- after: generates `MeasureTheory.AddMeasure.myOperation` (and probably warns that the name can be auto-generated)
end MeasureTheory.MulMeasure

• This should fix all problems in #659 other than #660 Minor changes:
• When applying @[to_additive] to a structure, add a trace message if no translation is inserted for a field.
• Define Name.fromComponents and Name.splitAt
• Reduce transitive imports of Tactic/toAdditive
• Move some auxiliary declarations from Tactic/Simps to more appropriate places
  • swap arguments of String.isPrefixOf?
  • improve Name.getString