Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: tactic parser


Heather Macbeth (Jan 11 2022 at 02:24):

Simple question, but how do I write a tactic taking two arguments?

import tactic

namespace tactic.interactive

setup_tactic_parser

meta def foo (p : parse (parser.pexpr 0)) : tactic unit :=
do trace p

meta def foo₂ (p q : parse (parser.pexpr 0)) : tactic unit :=
do trace p,
   trace q

end tactic.interactive

example : true :=
begin
  foo 3, -- fine
  foo₂ 3 4, -- error "expression expected"
end

Kyle Miller (Jan 11 2022 at 02:30):

If I'm understanding what's going on, it's parsing 3 4 as one expression (a function application with one argument).

Kyle Miller (Jan 11 2022 at 02:31):

If you have it use the default highest precedence, it works

import tactic

namespace tactic.interactive

setup_tactic_parser

meta def foo (p : parse (parser.pexpr 0)) : tactic unit :=
do trace p

meta def foo₂ (p q : parse parser.pexpr) : tactic unit :=
do trace p,
   trace q

end tactic.interactive

example : true :=
begin
  foo (3 + 2) 4, -- fine
  foo₂ (3 + 2) 4, -- fine
end

Heather Macbeth (Jan 11 2022 at 02:31):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC