declaration inspection

Stream: general

[Patrick Massot]

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]

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

[Mario Carneiro]

similarly @[instance] is an attribute

[Patrick Massot]

How do you get attributes of a declaration?

[Patrick Massot]

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]

tactic.has_attribute

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Edward Ayers]

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

[Mario Carneiro]

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]

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]

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

[Patrick Massot]

Thanks!

[Patrick Massot]

What is the difference between run_cmd and #eval here?

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

thanks

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Patrick Massot]

great!

[Patrick Massot]

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

[Patrick Massot]

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]

Mario, do you also have hints for me?

[Rob Lewis]

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]

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]

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

[Mario Carneiro]

I think constant is to axiom as def is to theorem

[Rob Lewis]

What are you seeing?

[Rob Lewis]

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]

And you can have axioms with non-Prop type.

[Rob Lewis]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

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]

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

[Rob Lewis]

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

[Mario Carneiro]

Did you know about #print definition?

[Mario Carneiro]

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

[Rob Lewis]

I had no idea, heh.

[Patrick Massot]

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]

you see that toto is also cnst

[Mario Carneiro]

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]

but where does the answer come from then?

[Rob Lewis]

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]

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

[Patrick Massot]

Makes sense, thanks

[Patrick Massot]

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

[Mario Carneiro]

I'm working on it

[Mario Carneiro]

in the meantime, I found something odd:

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

[Mario Carneiro]

lean does not remember structureness

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

Lean reconstructs structurehood based on structure like things

[Mario Carneiro]

specifically, the projections

[Patrick Massot]

where do you see the code of #print?

[Patrick Massot]

are you looking at https://github.com/leanprover/lean/blob/703d12d594f1591296d529e72794a00ba42dbade/src/frontends/lean/structure_cmd.cpp#L111?

[Mario Carneiro]

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

[Patrick Massot]

Nice!

[Patrick Massot]

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]

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?

[Mario Carneiro]

pure synonyms

[Patrick Massot]

thanks