Use "string" instead of "parse texpr" in interactive tactics

Stream: Is there code for X?

[Tsuru]

Is it possible to parse string during tactic execution? For example, can string be used instead of parse texpr in tactics like exact?
I was able to parse string with lean.parser.with_input, if the expressions depend only on environment (outside of begin ~ end block). However, for expressions with variables from local context (inside begin ~ end block), parser produces "unknown identifier" error.

example (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
begin
  (do
    lc ← tactic.local_context,
  tactic.trace lc, -- [p, q, hp, hq]
  lean.parser.run $ lean.parser.with_local_scope (
    do
    lc2 ← tactic.local_context,
    tactic.trace lc2, -- []
    p_pexpr ← lean.parser.with_input (lean.parser.pexpr 0 tt) "p", -- (if tt is changed to ff, "unknown identifier" occurs here)
    tactic.trace p_pexpr.1,
    p_expr ← tactic.to_expr p_pexpr.1, -- "unknown identifier" occurs here
    tactic.trace p_expr
  )),
  split, exact hp, exact hq
end

Apparently, parser monad does not refer to local context.
I tried to use some seemingly relevant functions such as lean.parser.with_local_scopeor environment.add, but not successful.
If I use environment.add for declarations including variables from local context, it produces "failed to add declaration to environment, it contains local constants
state" error.
Also, I cannot figure out how to use interactive.parse with string (not texpr).

[Tsuru]

Oh, I should not have run tactic.to_expr inside parser monad.

example (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
begin
  (do
    lc ← tactic.local_context,
  tactic.trace lc, -- [p, q, hp, hq]
    p_pexpr ← lean.parser.run $ lean.parser.with_local_scope (
    do
    lc2 ← tactic.local_context,
    tactic.trace lc2, -- []
    lean.parser.with_input (lean.parser.pexpr 0 tt) "p∨q" -- if tt is changed to ff, "unknown identifier" occurs here
    ),
    tactic.trace p_pexpr.1,
    p_expr ← tactic.to_expr p_pexpr.1, -- "p ∨ q"
    tactic.trace p_expr
    ),
  split, exact hp, exact hq
end

This works.