rewrite a tactic to a command

Stream: metaprogramming / tactics

[knowaywood]

def traceTactic (tac : Syntax) : TacticM Unit := do
  let gsBefore ← getGoals
  logInfo m!"TacticBefore: {gsBefore}"
  evalTactic tac
  let gsAfter ← getGoals
  for g in gsBefore do
    let type ← g.getType
    let checkgoal : checkAssign := ⟨ g.name,←  g.isAssigned, ← ppExpr type⟩
    logInfo m!"BEFORE: {checkgoal}"
  logInfo m!"TacticAfter: {gsAfter}"
  for g in gsAfter do
    let type ← g.getType
    let checkgoal : checkAssign := ⟨ g.name,←  g.isAssigned, ← ppExpr type⟩
    logInfo m!"AFTER: {checkgoal}"


elab "trace" tacs:tacticSeq : tactic => do
  withMainContext do
    let tacsArray := getSepTactics tacs
    for tac in tacsArray do
      let children ← traceTactic tac
      IO.println children


example (p q : Prop) :p ∧ q → q ∧ p  := by
    trace
    intro h
    constructor
    exact h.2
    sorry

I defind a tactic which can read the other tactics, and print their loginfo.

and now i want to use it as a command, i don't know to read the prop,and process it.

elab "trace" "example" ":" prop:term " :=" "by" tac:tacticSeq : command => do
  traceHelper "example" none prop tac

elab "trace" "theorem" n:ident ":" prop:term " :=" "by" tac:tacticSeq : command => do
  traceHelper "theorem" (some n) prop tac

-- i want use it like
trace example (p q : Prop) :p ∧ q → q ∧ p  := by
    intro h
    constructor
    exact h.2
    sorry

thanks for your help

[Siddhartha Gadgil]

It will help if you give a self-contained example so others can experiment (checkAssign is not defined). In any case, some hints I hope:

• Lean.Elab.Command.liftTermElabM before the do will lift you to TermElab level.
• Lean.Meta.mkFreshExprMVar will let you make a goal mVar
• Lean.Elab.runTactic will let you run your tactic (use mvar.withContext in place of withMainContext)