## Stream: general

### Topic: Kinds of declarations

#### Patrick Massot (Dec 02 2019 at 19:19):

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 (Dec 02 2019 at 20:17):

I think that could be useful.

• 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 (Dec 02 2019 at 20:20):

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 (Dec 02 2019 at 20:26):

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


Is it better?

#### Floris van Doorn (Dec 02 2019 at 20:28):

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)

oops

#### Patrick Massot (Dec 02 2019 at 20:30):

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

#### Patrick Massot (Dec 02 2019 at 20:30):

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

Not really...

#### Patrick Massot (Dec 02 2019 at 20:36):

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

#### Floris van Doorn (Dec 02 2019 at 20:36):

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

#### Patrick Massot (Dec 02 2019 at 20:39):

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 (Dec 02 2019 at 20:40):

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

#### Patrick Massot (Dec 02 2019 at 20:40):

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

#### Floris van Doorn (Dec 02 2019 at 21:13):

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 (Dec 02 2019 at 21:19):

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

#### Patrick Massot (Dec 02 2019 at 21:19):

But ideally I'd like a general purpose version.

#### Patrick Massot (Dec 02 2019 at 21:20):

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

#### Patrick Massot (Dec 02 2019 at 21:20):

So I choose probably use a more elaborate type.

#### Floris van Doorn (Dec 02 2019 at 21:22):

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.

Last updated: May 11 2021 at 02:05 UTC