elaboration function has not been implemented

Stream: lean4

[Marcus Rossel]

In the following example:

declare_syntax_cat test
syntax "§" : test
macro num test : term => Lean.Macro.throwError "Test Error"

#check 1 §

The term 1 § produces the error:

elaboration function for 'term__' has not been implemented
  1§

I don't understand the error message, and was rather expecting to see Test Error.
What is going on here?

[Sebastian Ullrich]

The overloading is because macro is syntax+macro_rules. The wrong error message is... unfortunate.

[Marcus Rossel]

Sebastian Ullrich said:

The overloading is because macro is syntax+macro_rules. The wrong error message is... unfortunate.

Yeah I just noticed that, too :sweat_smile:
I've changed the post above accordingly.

[Marcus Rossel]

So just to make sure I understand correctly:
The elaboration function for 'term__' has not been implemented message is just the current state of Lean 4, but eventually it should show Test Error?

[Sebastian Ullrich]

I was looking at the wrong file yesterday. It's fixed now.

[Nicolas Rouquette]

Sebastian Ullrich said:

I was looking at the wrong file yesterday. It's fixed now.

What is fixed about it?

I am running into this problem for this DSL:

-- Arithmetic for dimensional calculus
inductive DCalc : Type
  | symbol : String -> DCalc
  | power : DCalc -> Int -> Int -> DCalc
  | mul : DCalc -> DCalc -> DCalc
  | div : DCalc -> DCalc -> DCalc

declare_syntax_cat dcalc

syntax ident : dcalc -- DCalc.symbol
syntax dcalc "^" num "/" num : dcalc -- DCalc.power
syntax dcalc "*" dcalc : dcalc -- DCalc.mul
syntax dcalc "/" dcalc : dcalc -- DCalc.div
syntax "(" dcalc ")" : dcalc

-- auxiliary notation for translating `dcalc` into `term`
syntax "`[DCalc| " dcalc "]" : term

macro_rules
  | `(`[DCalc| $x:ident ]) => `(DCalc.symbol $(Lean.quote (toString x.getId)))
  | `(`[DCalc| $x:dcalc ^ $n:numLit / $d:numLit ]) => `(DCalc.power $x $d $d)
  | `(`[DCalc| $x:dcalc * $y:dcalc ]) => `(DCalc.mul $x $y)
  | `(`[DCalc| $x:dcalc / $y:dcalc ]) => `(DCalc.div $x $y)
  | `(`[DCalc| ($x:dcalc) ]) => `(`[DCalc| $x ])

#check `[DCalc| x ]           -- DCalc.symbol "x" : DCalc
#check `[DCalc| (x) ]         -- DCalc.symbol "x" : DCalc
#check `[DCalc| ((x)) ]       -- DCalc.symbol "x" : DCalc
#check `[DCalc| x * y ]
#check `[DCalc| x / y ]
#check `[DCalc| x ^ 1 / 1 ]

The last 3 checks give me an error:

elaboration function for 'dcalc__' has not been implemented
  x

This example is a slight modification of the one in the source: doc/metaprogramming-arith.md
Why does it trigger this error?

• Nicolas.

[Sebastian Ullrich]

In

| `(`[DCalc| $x:dcalc * $y:dcalc ]) => `(DCalc.mul $x $y)

etc. you are transferring x from the category dcalc to term, in which it has no interpretation. You need to continue the translation recursively, like you did in the parenthesis case.

[Nicolas Rouquette]

Ops! Thanks for the feedback!