match in quasiquotation

Stream: lean4

[Simon Hudon]

I'm trying to build the syntax tree for

match List.get? [1,2,3] with
| none => 2
| some x => x

Here is the code I wrote for that (based on the Lean 4 code base):

def test' : TermElabM Expr := do
let discr ← `(List.get? [1,2,3])
let p1 ← `( none )
let p2 ← `( some x )
let br1 ← `(matchAltExpr| | $p1 => 3)
let br2 ← `(matchAltExpr| | $p2 => x)
let brs := #[br1, br2]
let e ← `(match $discr:term with $brs:matchAlt*)
elabTerm e (some (mkConst `Nat))

It fails to elaborate. He is what happens when I print it out:

let _discr := List.get? [1, 2, 3];
sorryAx Nat

What am I missing?

[Simon Hudon]

Actually the following is closer to what I've seen in the Lean 4 code base but it has the same effect:

def test' : TermElabM Expr := do
let discr ← `(List.get? [1,2,3])
let discr := #[discr]
let p1 ← `( none )
let p1 := #[p1]
let p2 ← `( some x )
let p2 := #[p2]
let br1 ← `(matchAltExpr| | $[$p1:term],* => 3)
let br2 ← `(matchAltExpr| | $[$p2:term],* => x)
let brs := #[br1, br2]
let e ← `(match $[$discr:term],* with $brs:matchAlt*)
elabTerm e (some (mkConst `Nat))

[Mac]

My first thought would be that the x in `( some x ) is likely not the same as the x in `(matchAltExpr| | $p2 => x) due to hygiene.

[Simon Hudon]

replacing that x with 2 doesn't help

[Mario Carneiro]

the easy way to fix that is to do let x <- `(x) and then use $x in its occurrences

[Mario Carneiro]

Could you post a #mwe?

[Mario Carneiro]

I get unknown parser matchAltExpr when parsing test and test'

[Mario Carneiro]

Here's an MWE of your first example:

import Lean
open Lean Parser Term Elab Term

def test' : TermElabM Expr := do
  let discr ← `(List.get? [1,2,3])
  let p1 ← `( none )
  let p2 ← `( some x )
  let br1 ← `(matchAltExpr| | $p1 => 3)
  let br2 ← `(matchAltExpr| | $p2 => x)
  let brs := #[br1, br2]
  let e ← `(match $discr:term with $brs:matchAlt*)
  elabTerm e (some (mkConst `Nat))

#eval test'

<TermElabM>:0:0: error: type mismatch
  none
has type
  Option ?m.60 : Type ?u.59
but is expected to have type
  Nat → Option ?m.47 : Type ?u.46

let _discr._@.Test._hyg.3 : Nat -> (Option.{?_uniq.46} ?_uniq.47) := List.get?.{?_uniq.3} ?_uniq.47 (List.cons.{?_uniq.7} ?_uniq.47 (OfNat.ofNat.{?_uniq.7} ?_uniq.47 1 ?_uniq.12) (List.cons.{?_uniq.20} ?_uniq.47 (OfNat.ofNat.{?_uniq.20} ?_uniq.47 2 ?_uniq.25) (List.cons.{?_uniq.33} ?_uniq.47 (OfNat.ofNat.{?_uniq.33} ?_uniq.47 3 ?_uniq.38) (List.nil.{?_uniq.46} ?_uniq.47)))); sorryAx.{1} Nat Bool.true

The latter part matches the expression you claim (although printed less clearly), but this also comes with an error message that indicates more of the problem

[Mario Carneiro]

Note that you get the same error even without any of the syntax construction stuff:

#check
  match List.get? [1,2,3] with
  | none => 3
  | some x => x

type mismatch
  none
has type
  Option ?m.2251 : Type ?u.2250
but is expected to have type
  Nat → Option Nat : Type

[Mario Carneiro]

the problem being that List.get? [1,2,3] is an unapplied function, you need to get a specific index before it will yield an option

[Mario Carneiro]

Fixed:

import Lean
open Lean Parser Term Elab Term

def test' : TermElabM Expr := do
  let discr ← `(List.get? [1,2,3] 0)
  let x ← `(x)
  let p1 ← `( none )
  let p2 ← `( some $x )
  let br1 ← `(matchAltExpr| | $p1 => 3)
  let br2 ← `(matchAltExpr| | $p2 => x)
  let brs := #[br1, br2]
  let e ← `(match $discr:term with $brs:matchAlt*)
  elabTerm e (some (mkConst `Nat))

#eval show TermElabM _ from do
  let e ← withDeclName `foo test'
  Meta.ppExpr e

let _discr := List.get? [1, 2, 3] 0;
match List.get? [1, 2, 3] 0 with
| none => 3
| some x => x

Not sure what's up with the dead let expression. It seems like a bug in match elaboration

[Simon Hudon]

Thank you!

It seems that let x ← `(x) can be dropped and it still works

[Simon Hudon]

What remains is:

1. List.get? [1, 2, 3] -> List.get? [1, 2, 3] 0 so that we pattern match on Option Nat instead of Nat -> Option Nat
2. Run the elaborator from within a call to withDeclName.

Item 2. I'm not sure why it matters. Can you explain?

[Mario Carneiro]

You can try it without and see the error message

[Mario Carneiro]

match generates auxiliary definitions, and it needs a base declaration name to do that. When using this as part of a tactic that will not be a problem, but in testing code such as this (in the scope of an #eval) there is no declaration name so we have to give it a dummy name

[Simon Hudon]

I wasn't getting an error message without it. The elaboration would only be incomplete

[Simon Hudon]

I see! Thanks for the explanation!

[Mario Carneiro]

are you using the same MWE as me? when I remove the withDeclName I get an error

[Mario Carneiro]

<TermElabM>:0:0: error: auxiliary declaration cannot be created when declaration name is not available

[Mario Carneiro]

certainly I wouldn't have added that part otherwise

[Mario Carneiro]

If you are testing it in the real context and don't get that error, that's fine and you don't need it

[Mario Carneiro]

although the error seems to be reported through a side channel, there is no red squiggle on the #eval and it just evaluates to something containing a sorryAx nat

[Simon Hudon]

Yes I see. I was calling it from within MetaM and the error seems to get discarded. If I eval the TermElabM, I see the error. That's going to make things easier

[Gabriel Ebner]

Mac said:

My first thought would be that the x in `( some x ) is likely not the same as the x in `(matchAltExpr| | $p2 => x) due to hygiene.

It is exactly the same x. You only get a new x if you're inside a withFreshMacroScope.

[Simon Hudon]

Thanks for the clarification!