Extracting entries from a literal list

Stream: lean4

[Bhavik Mehta]

I have an expression of type List Nat, and I want to get the underlying actual List Nat, failing if the expression is not a literal list of literal naturals. What I have so far works iff the list has <= 32 elements:

import Lean

open Lean

def myList : List Nat :=
  [1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0,
   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

#eval myList.length

open Elab Command

def getEntries (e : Expr) : CommandElabM (List Nat) := do
  let some (ty, entries) := e.listLit? | throwError "not a list"
  unless ty == (mkConst `Nat []) do throwError "expected List ℕ but got List {ty}"
  entries.mapM fun e ↦ do
  let some i := e.nat? | throwError "expected natural literal but got {e}"
  pure i

elab "test" n:ident : command => do
  let env ← getEnv
  let some valuesC := env.find? n.getId | throwError "declaration {n} not found"
  let some valuesE := valuesC.value? | throwError "declaration {n} not defined"
  let l ← getEntries valuesE
  logInfo m!"values: {l}"

test myList

But because of docs#«term%[_|_]», this doesn't work if the list has at least 33 elements. (The implementation seems to cut off at 64, not sure where the discrepancy here is...).
Is there a nice way I can make this work through that notation? Note I need to be careful reducing the expression, since I want to fail if the entries are not natural literals. But maybe there's a particular choice of reduction I can do that's safe?

[Bhavik Mehta]

Ah, doing

let some (ty, entries) := (← liftTermElabM (Meta.zetaReduce e)).listLit? | throwError "not a list"

seems to work. (I'm reminded of why making MWEs helps so much, when writing the last question of the last message I realised that picking the right reduction is what I actually needed to do, and that was the key I missed!)

[Eric Wieser]

A very different approach would be to reimeplement docs#Lean.Expr.listLit? with reducible-defeq matching (possibly with Qq), otherwise you won't see through abbrev

[Bhavik Mehta]

Eric Wieser said:

A very different approach would be to reimeplement docs#Expr.listLit? with reducible-defeq matching (possibly with Qq), otherwise you won't see through abbrev

I think that would go too far, since it would permit 1+0 as an entry, right? If I'm understanding correctly, 1+0 is reducible-defeq to a natural lit

[Eric Wieser]

I mean the list constructor matching not the nat constructor

[Eric Wieser]

Either way, I think this should be a bug report as Expr.listLit?

[Bhavik Mehta]

Oh, okay! I'm happy to make this bug report, but my example above feels a little silly since I'm querying the environment to find the expression - can you point me to a slightly more sensible way of illustrating the problem?

[Eric Wieser]

import Lean
import Qq
open Qq

-- some _
#eval Lean.Expr.listLit? q([1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] : List Nat)
-- none
#eval Lean.Expr.listLit? q([1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] : List Nat)

[Eric Wieser]

But Qq doesn't exist in lean core of course, so I think your approach is what a unit test there would have to use

[Eric Wieser]

Oh, actually there is a clean enough way...

[Eric Wieser]

import Lean

elab "#test" t:term : command => do
  let e ← Lean.Elab.Command.liftTermElabM do
    Lean.Elab.Term.elabTerm t none
  if let .none := e.listLit? then
    throwError "Not a list literal"

#test [1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] -- ok
#test [1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1] -- fails
#test (by_elab
  return Lean.toExpr
      [1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]) -- ok

[Bhavik Mehta]

Thank you!

[Mario Carneiro]

Bhavik Mehta said:

But because of docs#«term%[_|_]», this doesn't work if the list has at least 33 elements. (The implementation seems to cut off at 64, not sure where the discrepancy here is...).

The discrepancy is because it's counting the length of the syntax array, which alternates between elements and commas

[Eric Wieser]

Edited above; interestingly the result of toExpr on list returns something that is considered a literal, even though an actual literal is not considered a literal

[Bhavik Mehta]

That's because the toExpr means the macro_rules (which is the one making the let expressions) don't get used, right?

[Bhavik Mehta]

lean4#7730

[Eric Wieser]

More precisely its because the ToExpr instance isn't following the same rules that the macro is

[Eric Wieser]

Maybe this is working as intended though, as listLit? does seem to agree with the infoview

[Bhavik Mehta]

Do you mean getListLit?, I can't find anything called toListLit?

[Eric Wieser]

That was a typo, I hadn't even realized the identical getListLit? existed