Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Building derive_handlers


Eric Wieser (Mar 28 2022 at 12:10):

What's going wrong here? How can I get to the point where I can at least see my trace output?

@[derive_handler] meta def decidable_rel_derive_handler : derive_handler :=
instance_derive_handler ``decidable_rel $
do env  tactic.get_env,
   tactic.fail format!"Not implemented"

set_option trace.app_builder true

@[derive decidable_rel]
inductive both_zero :     Prop
| zero : both_zero 0 0

(fails with

[app_builder] failed to create an 'decidable_rel'-application, failed to solve unification constraint for #1 argument (?x_0  ?x_0  Prop =?= Prop)

which I don't know the origin of)

Alex J. Best (Mar 28 2022 at 13:08):

You need to go one level deeper, into docs#instance_derive_handler

open tactic
/-- Given a tactic `tac` that can solve an application of `cls` in the right context,
    `instance_derive_handler` uses it to build an instance declaration of `cls n`. -/
meta def instance_derive_handler' (cls : name) (tac : tactic unit) (univ_poly := tt)
  (modify_target : name  list expr  expr  tactic expr := λ _ _, pure) : derive_handler :=
λ p n,
if p.is_constant_of cls then
do decl  get_decl n,
   cls_decl  get_decl cls,
   env  get_env,
   guard (env.is_inductive n) <|> fail format!"failed to derive '{cls}', '{n}' is not an inductive type",
   let ls := decl.univ_params.map $ λ n, if univ_poly then level.param n else level.zero,
   -- incrementally build up target expression `Π (hp : p) [cls hp] ..., cls (n.{ls} hp ...)`
   -- where `p ...` are the inductive parameter types of `n`
   let tgt : expr := expr.const n ls,
   params, _  mk_local_pis (decl.type.instantiate_univ_params (decl.univ_params.zip ls)),
   trace ">>>>>",
   let tgt := tgt.mk_app params,
   trace "###########",
   tgt  mk_app cls [tgt],
   trace "!!!!!!!!!!!",
   tgt  modify_target n params tgt,
   tgt  params.enum.mfoldr (λ i, param tgt,
   do -- add typeclass hypothesis for each inductive parameter
      tgt  do {
        guard $ i < env.inductive_num_params n,
        param_cls  mk_app cls [param],
        -- TODO(sullrich): omit some typeclass parameters based on usage of `param`?
        pure $ expr.pi `a binder_info.inst_implicit param_cls tgt
      } <|> pure tgt,
      pure $ tgt.bind_pi param
   ) tgt,
   (_, val)  tactic.solve_aux tgt (intros >> tac),
   val  instantiate_mvars val,
   let trusted := decl.is_trusted  cls_decl.is_trusted,
   add_protected_decl
     (declaration.defn (n ++ cls)
             (if univ_poly then decl.univ_params else [])
             tgt val reducibility_hints.abbrev trusted),
   set_basic_attribute `instance (n ++ cls) tt,
   pure true
else pure false
@[derive_handler] meta def decidable_rel_derive_handler : derive_handler :=
instance_derive_handler' ``decidable_rel $
do env  tactic.get_env,
   tactic.fail format!"Not implemented"

set_option trace.app_builder true

@[derive decidable_rel]
inductive both_zero :     Prop
| zero : both_zero 0 0

Alex J. Best (Mar 28 2022 at 13:08):

The error is coming from the line between ##### and !!!!!!!!!!

Alex J. Best (Mar 28 2022 at 13:14):

Commenting out let tgt := tgt.mk_app params, gets me to your not implemented FWIW


Last updated: Dec 20 2023 at 11:08 UTC