Find declaration kind

decl_kind.lean

import meta.expr data.rat


inductive declaration.kind
| Lemma : declaration.kind
| Definition : declaration.kind
| Instance : declaration.kind
| Structure : declaration.kind
| Structure_field : declaration.kind
| Class : declaration.kind
| Inductive : declaration.kind
| Axiom : declaration.kind
| Constant : declaration.kind

open declaration.kind

instance : has_to_string declaration.kind := ⟨λ k, match k with
| Lemma := "lemma"
| Definition := "definition"
| Instance := "instance"
| Structure := "structure"
| Structure_field := "structure field"
| Class := "class"
| Inductive := "inductive"
| Axiom := "axiom"
| Constant := "constant"
end⟩

open  tactic declaration environment

meta def environment.get_kind (env : environment) : declaration → tactic declaration.kind
| (thm _ _ _ _) := return Lemma
| (defn n _ _ _ _ _) := do
    (tactic.has_attribute `instance n >> return Instance) <|>
      match env.is_projection n with
      | some info := return Structure_field
      | none := return Definition
      end
| (cnst n _ _ _) := do
    (tactic.has_attribute `class n >> return Class) <|>
    match env.structure_fields n with
    | some l := return Structure
    | none   := do if is_ginductive env n then return Inductive else
                   return Constant
    end
| (ax _ _ _) := return Axiom

meta def name.kind (n : name): tactic unit :=
do
  env ← get_env,
  decl ← env.get n,
  kind ← env.get_kind decl,
  trace (to_string kind)

run_cmd name.kind `ring
run_cmd name.kind `ring.mul
run_cmd name.kind `comm_ring.to_ring
run_cmd name.kind `nat
run_cmd name.kind `rat
run_cmd name.kind `nat.add
run_cmd name.kind `rat
run_cmd name.kind `nat.rec