bool syntax

Stream: mathlib4

[Kenny Lau]

bool_lit is only found within aesop, how do other syntaxes handle bool?

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/369395703caee092690bfc992d66817da83b769d/Mathlib/Tactic/SudoSetOption.lean#L20 hmm... it's parsed as ident?

[Damiano Testa]

I am not sure that I understand the question, but, in a set_option, for example, the boolean is an atom:

---
set_option linter.all true in /-!-/

---

Syntax.node Parser.Command.in, none
|-Syntax.node Parser.Command.set_option, none
|   |-Syntax.atom original: ⟨⟩⟨ ⟩-- 'set_option'
|   |-Syntax.ident original: ⟨⟩⟨ ⟩-- (linter.all,linter.all)
|   |-Syntax.node null, none
|   |-Syntax.atom original: ⟨⟩⟨ ⟩-- 'true'
|-Syntax.atom original: ⟨⟩⟨ ⟩-- 'in'
|-Syntax.node Parser.Command.moduleDoc, none
    |-Syntax.atom original: ⟨⟩⟨⟩-- '/-!'
    |-Syntax.atom original: ⟨⟩⟨⏎⏎--inspect⏎⟩-- '-/'

[Kenny Lau]

is its type stored in some TSyntax type?

[Damiano Testa]

Well, in the set_option syntax, it is an atom.

[Kenny Lau]

so it's something like &"true"?

[Damiano Testa]

However, if you are referring to the term true, say in a theorem, then it would get parsed as an ident.

[Kenny Lau]

i'm referring to set_option

[Damiano Testa]

Ok, so in the position where you place the value of the option, the parser expects an atom.

[Kenny Lau]

so it doesn't go through the TSyntax stuff?

[Damiano Testa]

Let me find the source, but I don't think so.

[Damiano Testa]

For instance, in that position, there could be a natural number (parsed as an atom still, since an option need not be just a boolean).

[Kenny Lau]

hmm, but then how could i use it in a custom command syntax?

[Damiano Testa]

What do you mean?

[Damiano Testa]

I feel that I am not understanding where the question is coming from...

[Kenny Lau]

if i want to declare my own command to have syntax #asdf (foo := true), how should I do so?

[Damiano Testa]

https://github.com/leanprover/lean4/blob/919e297292280cdb27598edd4e03437be5850221/src/Lean/Elab/SetOption.lean#L64 is where you can see the true/false.

[Damiano Testa]

In your example, do you want writing something other than true/false be a parsing error?

[Kenny Lau]

yes

[Damiano Testa]

An alternative could be that you make the parser accept an ident, but, during elaboration, you throw an error if the ident is neither true nor false.

[Kenny Lau]

why not use Aesop.bool_lit?

[Damiano Testa]

You might, I am just not sure how much of that is intended to be "external".

[Kenny Lau]

right, so what i meant is, if Aesop.bool_lit is the best approach should we put it in lean core / batteries?

[Damiano Testa]

I don't know about that. I often find that elaboration errors are much "kinder" than parsing errors.

[Damiano Testa]

Here is something to play with:

declare_syntax_cat myStx

syntax "#asdf " "(" ident " := " (&"true" <|> &"false") ")" : myStx

run_cmd
  let _ ← `(myStx| #asdf (foo := true))
  let _ ← `(myStx| #asdf (foo := false))
  let _ ← `(myStx| #asdf (foo := neither))

[Damiano Testa]

I did not realize that, if you comment out the line with the parsing error, then you get an error because run_cmd is not implemented! :upside_down:

[Damiano Testa]

Here is a smaller example:

run_cmd
  -- comment the following line to notice that `run_cmd` has not been defined!
  let _ ← `(command| true)
  pure ()

[Kenny Lau]

import Lean

syntax "#asdf " "(" ident " := " (&"true" <|> &"false") ")" : command

#asdf (foo := true)
#asdf (foo := false)
#asdf (foo := neither)

syntax (name := fdsa) "#fdsa " "(" ident " := " ident ")" : command

open Lean Elab Command

@[command_elab fdsa] def fdsaElab : CommandElab := fun stx ↦ do
  match stx with
  | `(fdsa| #fdsa (foo := true)) => logInfo "1+2=3"
  | `(fdsa| #fdsa (foo := false)) => logInfo "1+2≠3"
  | `(fdsa| #fdsa (foo := $_:ident)) => log "yo you done messed up"
  | _ => log "watchu doing"

#fdsa (foo := true)
#fdsa (foo := false)
#fdsa (foo := neither)
#fdsa (asdf := neither)

[Kenny Lau]

@Damiano Testa I think I understand your point that elab error is kinder than parser error, but it also feels wrong to accept invalid syntax

[Damiano Testa]

Eventually it is a design decision and a parsing error, especially when you only have a couple of alternatives, can be pretty clear as well.

[Damiano Testa]

One reason to prefer (or at least to consider!) elaboration errors, is that Lean has some mechanisms to recover from elaboration errors. Parsing errors are total stops, however.

[Damiano Testa]

When designing the stacks attribute, for instance, it ended up being a better user experience to allow any "tag-looking" string, but then elaborate and produce meaningful reasons why the given string failed to be a stacks tag (e.g. too short, not consisting of uppercase letters or numbers,...).

[Damiano Testa]

In a different context, where you may only allow true or false, if the parser tell you so, it is probably good!

[Eric Wieser]

Parsing errors are total stops, however.

Is this true? I thought it was possible to error-yet-recover in a parser?

[Eric Wieser]

I'm sure @David Thrane Christiansen has plenty of thoughts here :)

[Damiano Testa]

Eric Wieser said:

Parsing errors are total stops, however.

Is this true? I thought it was possible to error-yet-recover in a parser?

That was probably excessive, there is some recovery. But elaboration errors are more compassionate.

[Jovan Gerbscheid]

Note that a big advantage of parsing and elaborating identifiers is that you get autocompletion that is aware of Lean identifiers:

afbeelding.png

[Aaron Liu]

Jovan Gerbscheid said:

Note that a big advantage of parsing and elaborating identifiers is that you get autocompletion that is aware of Lean identifiers:

afbeelding.png

But in this case you don't want all that right? You just want true and false as suggestions.

[Jovan Gerbscheid]

That's true, but I don't know how to implement that :)

[Aaron Liu]

Damiano Testa said:

Here is something to play with:

declare_syntax_cat myStx

syntax "#asdf " "(" ident " := " (&"true" <|> &"false") ")" : myStx

run_cmd
  let _ ← `(myStx| #asdf (foo := true))
  let _ ← `(myStx| #asdf (foo := false))
  let _ ← `(myStx| #asdf (foo := neither))

@Jovan Gerbscheid do you get any autocomplete suggestions here? I'm not at a computer so I can't check right now.

[Jovan Gerbscheid]

afbeelding.png
You do get suggestions. It's the kind that is not aware of lean identifiers.

[Aaron Liu]

But it only suggests true and false right

[Jovan Gerbscheid]

It suggests any word that exists anywhere
afbeelding.png

[Aaron Liu]

oh no that's not good

[Aaron Liu]

how do we fix it

[Aaron Liu]

where are these suggestions coming from

[Jovan Gerbscheid]

The lean-identifier aware ones come from the Lean language server via some fuzzy matching algorithm. And there word-based ones come with vscode automatically I think.

[Kyle Miller]

Do you need to roll your own syntax? You could use the tactic configuration system:

import Lean

open Lean Elab Command

structure AsdfConfig where
  foo : Bool := false
  deriving Repr

declare_command_config_elab elabAsdfConfig AsdfConfig

syntax (name := asdfStx) "#asdf " Parser.Tactic.optConfig : command

@[command_elab asdfStx] def asdfElab : CommandElab := fun stx ↦ do
  match stx with
  | `(#asdf $cfg:optConfig) =>
    let c ← elabAsdfConfig cfg
    logInfo m!"config is{indentD (repr c)}"
  | _ => log "watchu doing"

#asdf (foo := true)
#asdf (foo := false)
#asdf (foo := neither) -- unknown identifier `neither`

It's got completions too:

image.png

[Kenny Lau]

nice, thanks!

[Eric Wieser]

Does that syntax just parse terms? If not, where's the completion coming from?

[Aaron Liu]

yeah it's terms

[Aaron Liu]

you can have any expected type

[Aaron Liu]

For example if AsdfConfig had a bar : Finest Int field then it would take (bar := {1, 2, -4})

[David Thrane Christiansen]

Eric Wieser said:

Parsing errors are total stops, however.

Is this true? I thought it was possible to error-yet-recover in a parser?

This is in theory possible, but in practice it doesn't work for extensible parts of the syntax, because error recovery requires global knowledge. This means that we have some limited error recovery for a few parts, but it's quite limited.

Non-extensible syntax, like Verso's, can have error recovery, but it still requires some pretty low-level parsing code.

[David Thrane Christiansen]

If you really only want to allow Bool literals, and can't use the existing config system, I think this approach gives a pretty good UI. It takes local bindings and renamings into account, provides suggestions, and supports completion:

import Lean

open Lean Elab Term

syntax "bool_thing " ident : term
elab_rules : term
  | `(bool_thing $b) => do
    if let some n ← resolveId? b (withInfo := true) then
      if n matches .const ``true _ || n matches .const ``false _ then
        logInfoAt b m!"It is {n}"
        return n

    let t ← unresolveNameGlobalAvoidingLocals ``true
    let f ← unresolveNameGlobalAvoidingLocals ``false
    let h ← m!"Use a Bool literal:".hint #[t.toString, f.toString] (ref? := some b)
    throwErrorAt b m!"Boolean literal expected.{h}"

def x := bool_thing true

/--
error: Boolean literal expected.

Hint: Use a Bool literal:
  • x̵t̲r̲u̲e̲
  • x̵f̲a̲l̲s̲e̲
-/
#guard_msgs in
def y := bool_thing x

/--
error: Boolean literal expected.

Hint: Use a Bool literal:
  • B̲o̲o̲l̲.̲true
  • t̵r̵u̵f̲a̲l̲s̲e
---
warning: Local variable 'true' resembles constructor 'Bool.true' - write '.true' (with a dot) or 'Bool.true' to use the constructor.

Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
-/
#guard_msgs in
def z :=
  let true := false
  bool_thing true

def æ :=
  let true := false
  bool_thing Bool.true