## Stream: general

### Topic: declaration inspection

#### Patrick Massot (Aug 15 2018 at 16:34):

I'm still trying to discover what a Lean file can reveal about itself. I found https://github.com/leanprover/lean/blob/master/library/init/meta/environment.lean and https://github.com/leanprover/lean/blob/master/library/init/meta/declaration.lean but there still very basic questions I can't answer. Say I have an environment and a declaration name. I can distinguish a lemma/theorem from a definition or constant (although I'm not sure what's the difference between definition and constant). But how can I distinguish between def, class, instance, structure, inductive? I saw the series of functions around https://github.com/leanprover/lean/blob/master/library/init/meta/environment.lean#L47 but trying them on examples only confuses me.

#### Mario Carneiro (Aug 15 2018 at 16:37):

class means @[class] structure so you can use the attribute

#### Mario Carneiro (Aug 15 2018 at 16:37):

similarly @[instance] is an attribute

#### Patrick Massot (Aug 15 2018 at 16:38):

How do you get attributes of a declaration?

#### Patrick Massot (Aug 15 2018 at 16:40):

Can one strip off Pi from an expr and get to the first function appearing next? (This would be to understand what an instance declaration is an instance of)

#### Mario Carneiro (Aug 15 2018 at 16:42):

tactic.has_attribute

#### Patrick Massot (Aug 15 2018 at 16:46):

Is it possible do use this outside of a tactic? (in meta land of course)

#### Mario Carneiro (Aug 15 2018 at 16:48):

I doubt it, it looks like environment doesn't know anything about attributes

#### Patrick Massot (Aug 15 2018 at 16:53):

Do you see away to get the list of classes defined in the currently opened file then?

#### Edward Ayers (Aug 15 2018 at 16:54):

It also doesn't seem possible to get any information on what notation is defined.

#### Mario Carneiro (Aug 15 2018 at 17:00):

import tactic.basic

class foo : Type.
structure bar : Type.
@[class] def baz : Type := nat

open tactic
run_cmd do
env ← get_env,
env.fold skip $λ d t, do when (env.in_current_file' d.to_name)$ try $tactic.has_attribute class d.to_name >> trace d.to_name, t -- foo baz  #### Mario Carneiro (Aug 15 2018 at 17:01): alternatively: run_cmd do env ← get_env, l ← attribute.get_instances class, l.mmap'$ λ n, do
when (env.in_current_file' n) (trace n)
-- baz foo


#### Mario Carneiro (Aug 15 2018 at 17:05):

as I'm sure you've heard by now, this introspection stuff is getting an overhaul in lean 4, so fingers crossed

Thanks!

#### Patrick Massot (Aug 15 2018 at 17:12):

What is the difference between run_cmd and #eval here?

#### Patrick Massot (Aug 15 2018 at 17:27):

Inside a function which will ultimately return a tactic unit can I have some if consuming a tactic Prop or tactic bool?

#### Mario Carneiro (Aug 15 2018 at 17:37):

there is mcond as a shortcut for this, but you can always do b <- tac, if b then ... else ...

thanks

#### Patrick Massot (Aug 15 2018 at 17:38):

I'm sorry I'm very slowly getting used to monads

#### Patrick Massot (Aug 15 2018 at 17:39):

Do you have ideas to traverse an expr until you see what an instance is an instance of?

#### Mario Carneiro (Aug 15 2018 at 17:43):

meta def expr.get_pi_app_fn : expr → expr
| (expr.pi _ _ _ e) := e.get_pi_app_fn
| e                 := e.get_app_fn

run_cmd do
d ← get_decl option.decidable_eq,
expr.const n _ ← return d.type.get_pi_app_fn,
trace n
-- decidable_eq


great!

#### Patrick Massot (Aug 15 2018 at 17:50):

I think I even understand this code (but wouldn't have none where to search)

#### Patrick Massot (Aug 15 2018 at 17:57):

Two last questions and then I cook dinner: how would you distinguish between inductive and structure declarations? What does constant mean in the definition of the declaration type? How is is more constant than a definition?

#### Patrick Massot (Aug 15 2018 at 20:09):

Mario, do you also have hints for me?

#### Rob Lewis (Aug 15 2018 at 20:12):

declaration.cnst is the kind of declaration you get if you write constant A : ℕ. It's an undefined constant, basically the same as an axiom.

#### Rob Lewis (Aug 15 2018 at 20:13):

You can have a meta constant but not a meta axiom. I'm not sure if there are any other differences between the two.

#### Patrick Massot (Aug 15 2018 at 20:14):

I'm sorry but this doesn't match what I'm seeing

#### Mario Carneiro (Aug 15 2018 at 20:15):

I think constant is to axiom as def is to theorem

#### Rob Lewis (Aug 15 2018 at 20:16):

What are you seeing?

#### Rob Lewis (Aug 15 2018 at 20:17):

The differences between def and theorem are when the bodies get elaborated, right? But there are no bodies in a constant or axiom.

#### Rob Lewis (Aug 15 2018 at 20:18):

And you can have axioms with non-Prop type.

#### Rob Lewis (Aug 15 2018 at 20:21):

Actually, it looks like using the axiom command with a non-Prop type creates a declaration.cnst in the end. (edit- scratch that, typo)

#### Mario Carneiro (Aug 15 2018 at 20:22):

I'm going through the code now, trying to figure out the difference

#### Mario Carneiro (Aug 15 2018 at 20:22):

it is disambiguated in loads of places just so it can print constant instead of axiom but that's not so helpful

#### Patrick Massot (Aug 15 2018 at 20:30):

Sorry I was interrupted. Maybe there is a misunderstanding, I'm talking about https://github.com/leanprover/lean/blob/master/library/init/meta/declaration.lean#L67

#### Patrick Massot (Aug 15 2018 at 20:30):

See

import tactic
open tactic environment declaration

structure toto :=
(tata : Type)

#eval
do curr_env ← get_env,
let decls := curr_env.fold [] list.cons,
let local_decls := decls.filter
(λ x, environment.in_current_file' curr_env (to_name x) && not (to_name x).is_internal),
local_decls.mmap' (λ decl : declaration,
match decl with
| (thm _ _ _ _) := do trace "theorem"
| (defn _ _ _ _ _ _) := do trace "def"
| (cnst _ _ _ _) := do trace "cnst"
| (ax _ _ _) := do trace "ax"
end)


lots of cnst there

#### Rob Lewis (Aug 15 2018 at 20:34):

"Built-ins" are implemented as constants too. So when you declare an inductive type, the constructors, recursor, etc. are constants.

#### Rob Lewis (Aug 15 2018 at 20:35):

If you change a line to | (cnst nm _ _ _) := do trace "cnst", trace nm you can see what the constants are called.

#### Mario Carneiro (Aug 15 2018 at 20:35):

Did you know about #print definition?

#### Mario Carneiro (Aug 15 2018 at 20:36):

I just discovered that you can print definitions with #print definition foo. it's the same as #print foo but the printout is slightly different and it doesn't work on constants

#### Patrick Massot (Aug 15 2018 at 20:40):

I know, maybe it's clearer with

import tactic
open tactic environment declaration

structure toto :=
(tata : Type)

#eval
do curr_env ← get_env,
let decls := curr_env.fold [] list.cons,
let local_decls := decls.filter
(λ x, environment.in_current_file' curr_env (to_name x) && not (to_name x).is_internal),
local_decls.mmap' (λ decl : declaration,
match decl with
| (cnst _ _ _ _) := do trace decl.to_name
| _ := do skip
end)


#### Patrick Massot (Aug 15 2018 at 20:41):

you see that toto is also cnst

#### Mario Carneiro (Aug 15 2018 at 20:41):

Oh, @Patrick Massot I found out that even lean internally doesn't store the list of attributes associated to a definition. When printing a definition with #print, it gets the list of all attributes and just asks for each whether foo has that attribute

#### Patrick Massot (Aug 15 2018 at 20:42):

but where does the answer come from then?

#### Rob Lewis (Aug 15 2018 at 20:43):

Yeah. When you declare an inductive type T, you're basically saying, "there is a type T. This is how you create a T (the constructors). This is how you use a T (the recursors)."

#### Rob Lewis (Aug 15 2018 at 20:43):

You're not defining T in terms of something else, so there's no value for the declaration T to have.

#### Patrick Massot (Aug 15 2018 at 20:44):

Makes sense, thanks

#### Patrick Massot (Aug 15 2018 at 20:45):

Do you have an idea to distinguish between inductive and structure?

#### Mario Carneiro (Aug 15 2018 at 20:47):

I'm working on it

#### Mario Carneiro (Aug 15 2018 at 20:48):

in the meantime, I found something odd:

structure foo : Type.
#print foo
-- inductive foo : Type
-- constructors:
-- foo.mk : foo


#### Mario Carneiro (Aug 15 2018 at 20:48):

lean does not remember structureness

#### Mario Carneiro (Aug 15 2018 at 20:50):

or at least, nullary structures don't count as structures

#### Patrick Massot (Aug 15 2018 at 20:51):

structure toto :=
(tata : Type)
#print toto


#### Patrick Massot (Aug 15 2018 at 20:52):

structure toto : Type 1
fields:
toto.tata : toto → Type


#### Mario Carneiro (Aug 15 2018 at 20:53):

Lean reconstructs structurehood based on structure like things

#### Mario Carneiro (Aug 15 2018 at 20:53):

specifically, the projections

#### Patrick Massot (Aug 15 2018 at 21:04):

where do you see the code of #print?

#### Mario Carneiro (Aug 15 2018 at 21:30):

I think this replicates lean's is_structure function

meta def name.deinternalize_field : name → name
| (name.mk_string s name.anonymous) :=
let i := s.mk_iterator in
if i.curr = '_' then i.next.next_to_string else s
| n := n

meta def environment.is_structure (env : environment) (n : name) : bool :=
option.is_some $do guardb (env.is_inductive n), d ← (env.get n).to_option, [intro] ← pure (env.constructors_of n) | none, guard (env.inductive_num_indices n = 0), let nparams := env.inductive_num_params n, di ← (env.get intro).to_option, @nat.iterate (expr → option unit) (λ f e, do expr.pi _ _ _ body ← pure e | none, f body) nparams (λ e, do expr.pi x _ _ _ ← pure e | none, let f := n ++ x.deinternalize_field, env.is_projection f$> ())
di.type


Nice!

#### Patrick Massot (Aug 20 2018 at 23:26):

I think this replicates lean's is_structure function

I'm sorry, I wasted your time. For some mysterious reason I missed https://github.com/leanprover/lean/blob/776b440d5595e5eaa3f16e633c9ca85a834f147a/library/init/meta/environment.lean#L87 (and its implementation https://github.com/leanprover/lean/blob/776b440d5595e5eaa3f16e633c9ca85a834f147a/src/library/vm/vm_environment.cpp#L227)

#### Patrick Massot (Aug 21 2018 at 21:14):

Does Lean keep any trace of whether something was declared as a lemma or a theorem? Or are they purely synonym from the parsing stage on?

pure synonyms

#### Patrick Massot (Aug 21 2018 at 21:18):

thanks

Last updated: May 17 2021 at 21:12 UTC