observe

Stream: metaprogramming / tactics

[Johan Commelin]

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]

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

[Johan Commelin]

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]

This works, but looks very asymmetrical:

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

[Johan Commelin]

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]

Johan Commelin said:

This works, but looks very asymmetrical:

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