Zulip Chat Archive

Stream: general

Topic: declaration inspection


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:37):

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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:37):

similarly @[instance] is an attribute

view this post on Zulip Patrick Massot (Aug 15 2018 at 16:38):

How do you get attributes of a declaration?

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:42):

tactic.has_attribute

view this post on Zulip Patrick Massot (Aug 15 2018 at 16:46):

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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:48):

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

view this post on Zulip 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?

view this post on Zulip Edward Ayers (Aug 15 2018 at 16:54):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 15 2018 at 17:11):

Thanks!

view this post on Zulip Patrick Massot (Aug 15 2018 at 17:12):

What is the difference between run_cmd and #eval here?

view this post on Zulip 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?

view this post on Zulip 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 ...

view this post on Zulip Patrick Massot (Aug 15 2018 at 17:38):

thanks

view this post on Zulip Patrick Massot (Aug 15 2018 at 17:38):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 15 2018 at 17:49):

great!

view this post on Zulip Patrick Massot (Aug 15 2018 at 17:50):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:09):

Mario, do you also have hints for me?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:14):

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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:15):

I think constant is to axiom as def is to theorem

view this post on Zulip Rob Lewis (Aug 15 2018 at 20:16):

What are you seeing?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Aug 15 2018 at 20:18):

And you can have axioms with non-Prop type.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:22):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:35):

Did you know about #print definition?

view this post on Zulip 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

view this post on Zulip Rob Lewis (Aug 15 2018 at 20:38):

I had no idea, heh.

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:41):

you see that toto is also cnst

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:42):

but where does the answer come from then?

view this post on Zulip 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)."

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:44):

Makes sense, thanks

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:45):

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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:47):

I'm working on it

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:48):

lean does not remember structureness

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:50):

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

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:51):

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

view this post on Zulip Patrick Massot (Aug 15 2018 at 20:52):

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

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:53):

Lean reconstructs structurehood based on structure like things

view this post on Zulip Mario Carneiro (Aug 15 2018 at 20:53):

specifically, the projections

view this post on Zulip Patrick Massot (Aug 15 2018 at 21:04):

where do you see the code of #print?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 16 2018 at 08:46):

Nice!

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 21 2018 at 21:17):

pure synonyms

view this post on Zulip Patrick Massot (Aug 21 2018 at 21:18):

thanks


Last updated: May 17 2021 at 21:12 UTC