recreating `trace_state`

Stream: general

[Jason Rute]

A meta programming question: How would one recreate trace_state without using the built in formatter for the tactic_state type? I'm mostly interested in getting information found in trace_state, i.e. the context and targets for the other goals besides the current one, and not in the actual recreation of the trace_state. This code for example gets all the information for the current goal, but not for the other goals:

meta def trace_current_goal : tactic unit :=
do
 goal ← tactic.target,
 local_cxt ← tactic.local_context,
 local_cxt_types ← list.mmap tactic.infer_type local_cxt,
 let s := "Goal: " ++ (to_string goal) ++ "\nLocal Context: "++ (to_string local_cxt) ++ "\nLocal Context Types: " ++(to_string local_cxt_types),
 tractic.trace s,
return ()

[Mario Carneiro]

@Jason Rute tactic.target is a shorthand for (list.head <$> get_goals) >>= infer_type. If you want the other goals, call get_goals directly

[Jason Rute]

@Mario Carneiro how do I get the local_context for the other goals? What is tactic.local_context shorthand for? Is this documented anywhere?

[Rob Lewis]

local_context is implemented in c++, it's hard coded to give the context of the first goal. I'm not 100% sure this is robust, but you can typically do something like this (build whatever data structure you want instead of tracing).

example : true ∧ ∀ x : ℕ, true :=
by do
  `[refine ⟨_, λ i, _⟩], -- give ourselves two goals with different local contexts
  trace_state,
  gs ← get_goals,
  gs.mmap' $ λ g, set_goals [g] >> local_context >>= trace,
  set_goals gs,
  trace_state