Zulip Chat Archive

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

Patrick Massot (Aug 15 2018 at 17:11):

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 ...

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

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

Patrick Massot (Aug 15 2018 at 17:49):

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

Rob Lewis (Aug 15 2018 at 20:38):

I had no idea, heh.

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?

Patrick Massot (Aug 15 2018 at 21:24):

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

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

Patrick Massot (Aug 16 2018 at 08:46):

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?

Mario Carneiro (Aug 21 2018 at 21:17):

pure synonyms

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

thanks


Last updated: Dec 20 2023 at 11:08 UTC