parsing with ad hoc namespace

Stream: metaprogramming / tactics

[Xavier Martinet]

Hey, this is somewhat related to my previous question "interactive tactic printer": I was wondering: how to parse a string with an ad hoc namespace ?

for instance, I would like to have some function such as :

meta def parse_expr_with_namespace (s : string) (namespace : name) : expr := sorry

set_option pp.full_names true

#eval tactic.trace $ parse_expr_with_namespace "div" `nat
-- nat.div

[Xavier Martinet]

I have tried stuff like this, to no avail:

import all

section run_with_state'

namespace interaction_monad
open interaction_monad.result
meta def run_with_state' {σ₁ σ₂ : Type} {α : Type*} (state : σ₁) (tac : interaction_monad σ₁ α) : interaction_monad σ₂ α :=
λ s, match (tac state) with
     | (success val _) := success val s
     | (exception fn pos _) := exception fn pos s
     end
end interaction_monad
end run_with_state'

meta def run_on_input {α} (p : lean.parser α) (nmspace : name)(s : string) : tactic α :=
lean.parser.run $ do
  interaction_monad.get_state >>= λ ps, lean.parser.of_tactic $ do
    let env := ps.env,
    let env :=  env.mark_namespace_as_open nmspace,
    let env :=  env.execute_open nmspace,
    tactic.set_env env,
    prod.fst <$> (@interaction_monad.run_with_state' lean.parser_state _ _ ps $ lean.parser.with_input p s)

#eval do e ← run_on_input lean.parser.pexpr `int "succ", tactic.trace e
-- tactic failed

open int
#eval do e ← run_on_input lean.parser.pexpr `int "succ", tactic.trace e
-- int.succ
#eval do e ← run_on_input lean.parser.pexpr `nat "succ", tactic.trace e
-- int.succ