parsing a bool

Stream: general

[Scott Morrison]

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]

doesn’t iterate parse a (small) nat

[Mario Carneiro]

You could parse an expression and match against the result

[Scott Morrison]

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]

is my attempt so far

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

eval_expr'

[Mario Carneiro]

also of_tactic'

[Scott Morrison]

Can't find of_tactic'

[Scott Morrison]

But it looks like it's not needed.

[Scott Morrison]

Perhaps that's been patched in core already.

[Scott Morrison]

eval_expr' does the trick... :-(

[Scott Morrison]

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

[Scott Morrison]

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

[Simon Hudon]

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

[Mario Carneiro]

because tk only works on keywords

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Simon Hudon]

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]

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

[Scott Morrison]

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

[Simon Hudon]

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

[Mario Carneiro]

What about using the ident parser?

[Mario Carneiro]

that won't read any more than it has to

[Mario Carneiro]

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

[Simon Hudon]

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]

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]

let_option

[Mario Carneiro]

or even better, with_option { tac }

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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]

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

[Mario Carneiro]

pretty sure

[Mario Carneiro]

confirmed, it works just like other interactive tactics

[Simon Hudon]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

yes, but via tactics

[Mario Carneiro]

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

[Mario Carneiro]

In fact, #help should be a user command

[Mario Carneiro]

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]

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]

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

[Reid Barton]

to achieve the originally desired result, I mean

[Mario Carneiro]

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

[Reid Barton]

A set_option tactic

[Reid Barton]

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

[Mario Carneiro]

there is already a set_option tactic

[Mario Carneiro]

I used it above

[Mario Carneiro]

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]

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