Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: observe


Johan Commelin (Nov 24 2021 at 13:04):

Here's my next attempt at observe (yes, I'm giving a talk again tomorrow)

import tactic

namespace tactic
namespace interactive
setup_tactic_parser

meta def observe (trc : parse $ optional (tk "?"))
  (h : parse ident?) (t : parse (tk ":" *> texpr)) : tactic unit := do
  let h' := h.get_or_else `this,
  t  to_expr ``(%%t : Prop),
  ppt  pp t,
  assert h' t,
  s  focus1 (tactic.library_search { try_this := ff }) <|> fail "observe failed",
  s  s.get_rest "Try this: ",
  let pph : string := (h.map (λ n : name, n.to_string ++ " ")).get_or_else "",
  when trc.is_some $ trace! "Try this: have {pph}: {ppt.to_string}, {s}"

end interactive
end tactic

(Big thanks to Mario for the initial skeleton!)

Johan Commelin (Nov 24 2021 at 13:04):

My question is: how do I print { in a format string?

Johan Commelin (Nov 24 2021 at 13:05):

In the line when trc.is_some $ trace! "Try this: have {pph}: {ppt.to_string}, {s}" I want to surround s by braces,
so that the output looks like { exact foo.bar }.

Johan Commelin (Nov 24 2021 at 13:13):

This works, but looks very asymmetrical:

  when trc.is_some $ trace! "Try this: have {pph}: {ppt.to_string}, {{ {s} }"

Johan Commelin (Nov 24 2021 at 13:22):

I now have

meta def observe (trc : parse $ optional (tk "?"))
  (h : parse ident?) (t : parse (tk ":" *> texpr)) : tactic unit := do
  let h' := h.get_or_else `this,
  t  to_expr ``(%%t : Prop),
  ppt  pp t,
  assert h' t,
  s  focus1 (tactic.library_search { try_this := ff }) <|> fail "observe failed",
  s  s.get_rest "Try this: exact ",
  let pph : string := (h.map (λ n : name, n.to_string ++ " ")).get_or_else "",
  when trc.is_some $ trace! "Try this: have {pph}: {ppt.to_string} := {s}"

which I'm quite happy with.

Floris van Doorn (Nov 24 2021 at 14:02):

Johan Commelin said:

This works, but looks very asymmetrical:

This will be fixed in the next release of Lean: lean#650


Last updated: Dec 20 2023 at 11:08 UTC