Zulip Chat Archive

Stream: general

Topic: parsing a bool


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 11 2020 at 11:54):

doesn’t iterate parse a (small) nat

view this post on Zulip Mario Carneiro (Apr 11 2020 at 11:55):

You could parse an expression and match against the result

view this post on Zulip 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)))

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:57):

is my attempt so far

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:58):

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

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:58):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:02):

eval_expr'

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:02):

also of_tactic'

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:06):

Can't find of_tactic'

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:06):

But it looks like it's not needed.

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:06):

Perhaps that's been patched in core already.

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:07):

eval_expr' does the trick... :-(

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:07):

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

view this post on Zulip 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.)

view this post on Zulip 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"?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:14):

because tk only works on keywords

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:20):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:28):

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

view this post on Zulip Simon Hudon (Apr 11 2020 at 12:29):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:29):

What about using the ident parser?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:29):

that won't read any more than it has to

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 11 2020 at 12:35):

let_option

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:36):

or even better, with_option { tac }

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:38):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 11 2020 at 12:47):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:47):

pretty sure

view this post on Zulip Mario Carneiro (Apr 11 2020 at 12:48):

confirmed, it works just like other interactive tactics

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 11 2020 at 13:19):

yes, but via tactics

view this post on Zulip Mario Carneiro (Apr 11 2020 at 13:20):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 13:20):

In fact, #help should be a user command

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 11 2020 at 13:37):

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

view this post on Zulip Reid Barton (Apr 11 2020 at 13:38):

to achieve the originally desired result, I mean

view this post on Zulip Mario Carneiro (Apr 11 2020 at 13:39):

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

view this post on Zulip Reid Barton (Apr 11 2020 at 14:02):

A set_option tactic

view this post on Zulip Reid Barton (Apr 11 2020 at 14:02):

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

view this post on Zulip Mario Carneiro (Apr 11 2020 at 14:05):

there is already a set_option tactic

view this post on Zulip Mario Carneiro (Apr 11 2020 at 14:05):

I used it above

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 11 2020 at 14:15):

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


Last updated: May 18 2021 at 16:25 UTC