Disconnected syntax

Stream: lean4

[Damiano Testa]

Dear All,

is it possible to throw an error at a disconnected syntax? Here is an example of what I would like to achieve:

import Lean.Elab.Tactic.Basic

open Lean

elab "twoErrors" e1:term "~" e2:term : tactic => do
  throwErrorAt e1 "Can there be a red squiggle also under {e2}"
  throwErrorAt e2 "I would like to also underline e2"

example : True := by
  twoErrors 0 ~ 1  -- Can there be a red squiggle also under 1

Thanks!

[Damiano Testa]

I see that it is possible:

#eval let x : List Nat := [0, 1, _, 4, _] -- both underscores are underlined, and nothing else

but I still do not know how to achieve it myself! :smile:

[Mario Carneiro]

don't use throwErrorAt, that has control flow effects. Use logError if you just want to add a squiggle

[Mario Carneiro]

note that I have said something along the lines of "logError considered harmful" in the past though, because it interacts in surprising ways with control flow combinators like try / repeat

[Mario Carneiro]

import Lean
open Lean

elab "foo" : tactic => do
  logError "you can't foo right now"

elab "bar" : tactic => do
  throwError "you can't bar right now"

-- one nice thing about `logError`
-- is that you can keep giving errors after the tactic
example : True := by
  foo -- error
  bar -- error
  foo

-- one not nice thing about `logError`
-- is that you can't suppress the error, at least with normal combinators
example : True := by
  try bar
  try foo -- error
  trivial

[Damiano Testa]

Mario, thank you very much! I like this and I am planning to then log the errors and then throw an error, since I do not want to continue!

[Damiano Testa]

Basically, my use-case is that I want to throw an error when the user passes a list of terms, some of which are not suitable, and underline the unsuitable ones, but definitely throw an error after underlining!

[Damiano Testa]

Here is a sample of something similar to what I had in mind:

import Lean

open Lean Elab TSyntax in
elab nm:"evens?" nats:(colGt num),* : tactic => do
  let odds := nats.getElems.filter (getNat · % 2 = 1)
  guard (odds.size = 0) *> logInfoAt nm "All even!" <|>
    odds.mapM (logErrorAt · .nil) *>
    throwErrorAt nm m!"The underlined numbers {odds} are odd!"

example : True := by
  evens? 0, 1, 2, 3, 4, 5, 10001  -- The underlined numbers [1, 3, 5, 10001] are odd!

example : True := by
  evens? 0, 2, 4, 1000    --  All even!
  trivial

[Damiano Testa]

Here is the "guess the sequence" version of the above:

import Lean

--  SPOILER ALERT: do not look at the implementation!  Go to the last line
open Lean in
elab nm:"guess_the_next_number!" nats:(colGt num),* : command => do
  let mut (data, incorrects) := (#[], #[])
  let mut con := 0
  for elt in nats.getElems do
    if elt.getNat != 2 ^ con then
      logErrorAt elt .nil
      if con ≤ 3 then data := data.push elt else incorrects := incorrects.push elt
    con := con + 1
  let init := if data.size ≤ 3 then m!"The sequence begins with 1, 2, 4, 8." else .nil
  match incorrects.size, nats.getElems.size with
    | 0, n => logInfoAt nm
                (if n ≤ 3 then init ++ " Make a guess!"
                 else if n = 4 then "Make a guess!"
                 else "🎉 Guess accomplished!  Keep guessing, if you want")
    | _, _ => incorrects.mapM (logErrorAt · .nil) *>
              throwErrorAt nm m!"The underlined numbers {data ++ incorrects} are wrong!"

-- avoid looking at the implementation above!

guess_the_next_number!