Zulip Chat Archive

Stream: general

Topic: parsing a bool


Scott Morrison (Apr 11 2020 at 11:51):

I would like to have a tactic argument which could a bool (or perhaps a true or false), or a nat. Can someone show me how to construct the appropriate parser?

Kenny Lau (Apr 11 2020 at 11:54):

doesn’t iterate parse a (small) nat

Mario Carneiro (Apr 11 2020 at 11:55):

You could parse an expression and match against the result

Scott Morrison (Apr 11 2020 at 11:57):

private meta def bool_or_nat : parser (bool  ) :=
(sum.inr <$> small_nat) <|>
(sum.inl <$> (texpr >>= (λ e, of_tactic $ to_expr e >>= eval_expr bool)))

Scott Morrison (Apr 11 2020 at 11:57):

is my attempt so far

Scott Morrison (Apr 11 2020 at 11:58):

but I get VM does not have code for 'bool.tt'

Scott Morrison (Apr 11 2020 at 11:58):

(when I try to actually use it; compiles fine)

Mario Carneiro (Apr 11 2020 at 12:02):

eval_expr'

Mario Carneiro (Apr 11 2020 at 12:02):

also of_tactic'

Scott Morrison (Apr 11 2020 at 12:06):

Can't find of_tactic'

Scott Morrison (Apr 11 2020 at 12:06):

But it looks like it's not needed.

Scott Morrison (Apr 11 2020 at 12:06):

Perhaps that's been patched in core already.

Scott Morrison (Apr 11 2020 at 12:07):

eval_expr' does the trick... :-(

Scott Morrison (Apr 11 2020 at 12:07):

Hmm.. and what if I want to all true?

Scott Morrison (Apr 11 2020 at 12:08):

(I'm trying to allow something close to set_option pp.all true inside a tactic block.)

Simon Hudon (Apr 11 2020 at 12:13):

For parsing a bool, it's starting to look pretty complicated. Why not just do tt <$ tk "tt" <|> ff <$ tk "ff"?

Mario Carneiro (Apr 11 2020 at 12:14):

because tk only works on keywords

Mario Carneiro (Apr 11 2020 at 12:15):

and if you declare tt as a keyword then it won't work as the actual expression

Mario Carneiro (Apr 11 2020 at 12:18):

If you parse an expression, use to_expr `(%%e: bool) and then evaluate it, then this will also work on boolean expressions as well as true and false which will be interpreted via to_bool

Mario Carneiro (Apr 11 2020 at 12:19):

If you want a more syntactic interpretation, you can pattern match the pre-expression you get from texpr and just see if it is the constants tt, true, ff or false (or numerals) and dispatch accordingly

Mario Carneiro (Apr 11 2020 at 12:20):

I do something like this for being able to recognize the non-keyword SOP in ring

Simon Hudon (Apr 11 2020 at 12:27):

That's disappointing. parsing an expressing seems overkill and if you have to parse something after the bool and that it could be read as an expression, it will just mix up the parser

Scott Morrison (Apr 11 2020 at 12:28):

In fact, the most disappointing thing is that you can't have an interactive tactic called set_option anyway.

Scott Morrison (Apr 11 2020 at 12:28):

So this is all a moot point, I think. :-)

Simon Hudon (Apr 11 2020 at 12:29):

That could be an argument for having a bool parser like small_nat

Mario Carneiro (Apr 11 2020 at 12:29):

What about using the ident parser?

Mario Carneiro (Apr 11 2020 at 12:29):

that won't read any more than it has to

Mario Carneiro (Apr 11 2020 at 12:31):

Actually I think this is the right answer, since true and false are definitely treated as identifiers by the lean parser

Simon Hudon (Apr 11 2020 at 12:32):

about pp.all, try:

meta def set_pp_all : tactic unit := do
opt  get_options,
set_options (opt.set_bool `pp.all tt)

example : 1 + 1 = 1 :=
begin
  do { set_pp_all }
end

Mario Carneiro (Apr 11 2020 at 12:35):

You can't use set_option because that's a command keyword, but you could use any variation on that like set_opt or option

Reid Barton (Apr 11 2020 at 12:35):

let_option

Mario Carneiro (Apr 11 2020 at 12:36):

or even better, with_option { tac }

Mario Carneiro (Apr 11 2020 at 12:37):

Alternatively, you could just declare every option name as an interactive tactic so that pp.all true is a tactic

Mario Carneiro (Apr 11 2020 at 12:38):

strangely enough, I don't think there are any conflicts that arise this way

Mario Carneiro (Apr 11 2020 at 12:40):

You can even generate them with metaprogramming so that boolean options parse a boolean and numeric options parse a nat

Reid Barton (Apr 11 2020 at 12:42):

Mario Carneiro said:

or even better, with_option { tac }

Perhaps whether one wants this scoped syntax depends on whether the set_option tactic is intended to remain in the final version of the proof. For pp options it would probably just be annoying to have to use {} most of the time (if you really want to scope the option, then you can probably achieve it with {} anyways).

Mario Carneiro (Apr 11 2020 at 12:46):

another benefit of having options-as-tactics is that you can copy the docstring of the option to the tactic so that you get a nice hover, while set_opt pp.all true wouldn't be able to provide that

Reid Barton (Apr 11 2020 at 12:47):

If you write pp.all in an interactive tactic does it mean tactic.interactive.pp.all?

Mario Carneiro (Apr 11 2020 at 12:47):

pretty sure

Mario Carneiro (Apr 11 2020 at 12:48):

confirmed, it works just like other interactive tactics

Simon Hudon (Apr 11 2020 at 12:54):

Maybe something like pretty_print all would be more in line with the kind of naming conventions that we follow

Mario Carneiro (Apr 11 2020 at 13:01):

I think it would be better to stick to the naming convention used by options so that people don't have to learn both

Mario Carneiro (Apr 11 2020 at 13:03):

I thought there was an API for querying the list of all options, but I can't find one. options.fold only gives you the options that have been set on the current object

Mario Carneiro (Apr 11 2020 at 13:03):

there is also no way to ask what type an option has, you just use get_string or get_nat and hope you got it right

Mario Carneiro (Apr 11 2020 at 13:18):

In the absence of an API for this, we can still just make a list of options and their types. Here's a plausible metaprogram for building these option tactics:

open lean.parser lean
namespace tactic
open interactive

meta def pbool : parser bool :=
do n  ident, match n with
| `tt := return tt
| `true := return tt
| `ff := return ff
| `false := return ff
| _ := failure
end

meta def set_option_bool (n : name) (b : parse pbool) : tactic unit :=
do opt  get_options, set_options (opt.set_bool n b)

run_cmd [(`pp.all, ``set_option_bool)].mmap $ λ e:name × name, do
  let v := (@expr.const tt e.2 []).app (reflect e.1),
  t  infer_type v,
  tactic.add_decl $ declaration.defn
    (`tactic.interactive ++ e.1) [] t v (reducibility_hints.regular 1 tt) ff

example : 0 = 1 :=
begin
  -- ⊢ 0 = 1
  pp.all true,
  -- ⊢ @eq.{1} nat (@has_zero.zero.{0} nat nat.has_zero) (@has_one.one.{0} nat nat.has_one)
end

Kevin Buzzard (Apr 11 2020 at 13:19):

Mario Carneiro said:

I thought there was an API for querying the list of all options, but I can't find one. options.fold only gives you the options that have been set on the current object

Do you mean #help options?

Mario Carneiro (Apr 11 2020 at 13:19):

yes, but via tactics

Mario Carneiro (Apr 11 2020 at 13:20):

In fact, everything you can get to via #help should be available to tactics

Mario Carneiro (Apr 11 2020 at 13:20):

In fact, #help should be a user command

Mario Carneiro (Apr 11 2020 at 13:26):

Another possible tactic name is set_option.pp.all; this does not run afoul of the command keyword and puts all the option tactics in one namespace

Reid Barton (Apr 11 2020 at 13:37):

Mario Carneiro said:

I thought there was an API for querying the list of all options, but I can't find one. options.fold only gives you the options that have been set on the current object

But we could add one.

Reid Barton (Apr 11 2020 at 13:37):

Although at that point maybe it makes more sense to just add a new core tactic

Reid Barton (Apr 11 2020 at 13:38):

to achieve the originally desired result, I mean

Mario Carneiro (Apr 11 2020 at 13:39):

a new core tactic for what? your two proposals sound the same

Reid Barton (Apr 11 2020 at 14:02):

A set_option tactic

Reid Barton (Apr 11 2020 at 14:02):

Versus a method that just returns the list of all options and their arguments

Mario Carneiro (Apr 11 2020 at 14:05):

there is already a set_option tactic

Mario Carneiro (Apr 11 2020 at 14:05):

I used it above

Mario Carneiro (Apr 11 2020 at 14:07):

in order to implement the metaprogram though, I need to be able to list all options a la #help options. From there we can create tactics that use set_options to set any individual option as desired

Reid Barton (Apr 11 2020 at 14:15):

oh okay, I guess I don't understand what I meant either, then


Last updated: Aug 03 2023 at 10:10 UTC