List of projections of structure

Stream: metaprogramming / tactics

[Eric Wieser]

What's the easiest way to fill this sorry:

def get_projections (t : expr) : list expr := sorry

such that get_projections `(prod X Y) = [`(@prod.fst X Y), `(@prod.snd X Y)]

[Floris van Doorn]

You can use docs#environment.structure_fields to the (name of the) head of the expression, and then apply each of them to the same arguments as the original expression. You'd have to wrap it inside a tactic though.

[Floris van Doorn]

import tactic.core
open tactic

meta def get_projections (t : expr) : tactic (list expr) := do
  env ← get_env,
  let str_nm := t.get_app_fn.const_name,
  proj_nms ← env.structure_fields_full str_nm,
  let univs := t.get_app_fn.univ_levels,
  let args := t.get_app_args,
  let projs := proj_nms.map (λ proj_nm, (expr.const proj_nm univs).mk_app args),
  return projs

#eval get_projections `(bool × nat) >>= trace -- [prod.fst, prod.snd]
#eval get_projections `(bool × nat) >>= (λ x, trace $ x.map expr.to_raw_fmt)
#eval get_projections `(bool × nat) >>= (λ x, x.mmap infer_type >>= trace) -- [bool × ℕ → bool, bool × ℕ → ℕ]

(not extensively tested)
You might want to apply instantiate_mvars and whnf tot first, in case t is not exactly in the right form.
EDIT: fixed bug

[Eric Wieser]

In #15207 I ended up with

/-- ``(s_name, (c_name, c_fun), [(p_name, p_fun), ...]) ← get_constructor_and_projections `(struct n)``
gets the names and partial invocations of the constructor and projections of a structure -/
meta def get_constructor_and_projections (t : expr) :
  tactic (name × (name × expr) × list (name × expr)):=
do
  (const I ls, args) ← pure (get_app_fn_args t),
  env ← get_env,
  [ctor] ← pure (env.constructors_of I),
  ctor ← do
  { d ← get_decl ctor,
    let a := @expr.const tt ctor $ d.univ_params.map level.param,
    pure (ctor, a.mk_app args) },
  ctor_type ← infer_type ctor.2,
  tt ← pure ctor_type.is_pi | pure (I, ctor, []),
  some fields ← pure (env.structure_fields I) | fail!"Not a structure",
  projs ← fields.mmap $ λ f, do
  { d ← get_decl (I ++ f),
    let a := @expr.const tt (I ++ f) $ d.univ_params.map level.param,
    pure (f, a.mk_app args) },
  pure (I, ctor, projs)

[Yury G. Kudryashov]

What do you want to get in case of docs#monoid? Should it include to_semigroup?

[Eric Wieser]

Good question, I think for my use-case I don't really care that much