Kinds of declarations

Stream: general

[Patrick Massot]

Still coming back to meta-code, I'd like to clean up leancrawler a bit, and maybe PR part of it to mathlib for general use. The very first step is to triage declaration by kind (I would say type but that would be very confusing). Can anyone comment on https://gist.github.com/PatrickMassot/64167b3fce4b3f07c556328c1ffa683b? Would mathlib be interested in that?

[Floris van Doorn]

I think that could be useful.
Some comments:

• Theorems can be instances when you write @[instance] theorem ...
• Definitions can be classes when you write @[class] def .... I believe this actually happens in mathlib.
• This is the first time that I see the declaration environment.structure_fields. That is useful. There are some declarations in meta.expr that mimic this built-in declaration. I will PR a change that removes those.

[Floris van Doorn]

Also, if you want to golf the function a bit, you can write return $ if (env.is_projection n).is_some then Structure_field else Definition

[Patrick Massot]

Thanks a lot! New version:

meta def environment.get_kind (env : environment) : declaration → tactic declaration.kind
| (thm n _ _ _) := do (tactic.has_attribute `class n >> return Instance) <|> return Lemma
| (defn n _ _ _ _ _) := do
    (has_attribute `class n >> return Class) <|>
    (has_attribute `instance n >> return Instance) <|>
    return (if (env.is_projection n).is_some then Structure_field else Definition)
| (cnst n _ _ _) := do
    (has_attribute `class n >> return Class) <|>
    return (if (env.structure_fields n).is_some then Structure
              else if is_ginductive env n then Inductive else Constant)
| (ax _ _ _) := return Axiom

[Patrick Massot]

Is it better?

[Floris van Doorn]

Line 2: `class -> `instance

Suggestion: maybe first case on whether it has certain attributes, and only then case on the declaration-constructor (using declaration.is_theorem and friends from meta.expr)

[Patrick Massot]

oops

[Patrick Massot]

Do we have a nice way to do case analysis not based on constructors of inductive types?

[Patrick Massot]

Already in my version the nested if/then/else look ugly, for lack of elif.

[Floris van Doorn]

Not really...

[Patrick Massot]

I'll still try, so we'll be able to compare.

[Floris van Doorn]

You can still do a match d with ... in the middle of the expression.

[Patrick Massot]

How do you like

meta def environment.get_kind' (env : environment) (decl : declaration) : tactic declaration.kind :=
do
  let n := decl.to_name,
  (has_attribute `instance n >> return Instance) <|>
  (has_attribute `class n >> return Class) <|>
  return (
    if (env.structure_fields n).is_some then Structure else
    if (env.is_projection n).is_some then Structure_field else
    if is_ginductive env n then Inductive else
    if decl.is_definition then Definition else
    if decl.is_theorem then Lemma else
    if decl.is_constant then Constant else Axiom

[Patrick Massot]

Writing a proof that it's the same function (or not, I guess there is 50% change) would be a fun challenge.

[Patrick Massot]

I think it's more readable. I hope it's the same result.

[Floris van Doorn]

I think this definition looks good.
What are you going to use this data for though? The datastructure declaration.kind assumes that the classes are disjoint, which is not true.
In addition to the previous mentioned cases (classes can be either structures or definitions, instances can be theorems or definitions), there are also structure fields that are instances. You lose this "secondary" information. This is fine, but depends on the application.

[Patrick Massot]

A version of this was used to create the graph at https://leanprover-community.github.io/lean-perfectoid-spaces/

[Patrick Massot]

But ideally I'd like a general purpose version.

[Patrick Massot]

So I don't want to lose anything I could keep.

[Patrick Massot]

So I choose probably use a more elaborate type.

[Floris van Doorn]

If you don't want to lose information, you indeed want a more elaborate type. You could have a type with 4 constructors, corresponding to the constructors of declaration and then some boolean values whether it is a field/structure/class/instance.