I am quite new to metaprogramming in Lean and have been experimenting with using macros on undefined identifiers to convert it into other types. However, I have been stuck with converting a two character identifier (e.g. ab) which may not have defined type into two identifiers of a specified form (in this case a and b).
I have reviewed the rather incomplete documentation and the community resources but failed to find any example that resembled what I desired.
Assuming that the variables a and b are defined to have some arbitrary type. I want to write a macro (or if not sufficient an elab) which takes the identifier ab and splits it into an expression containing the two predefined variables. Suppose the macro name is split, I essentially want to do this in Lean:
variable (a b : Type')
#check Eq (split ab) -- This should output a = b : Prop
Note that I am making the assumption that the variable names are always one character long.
I had attempted converting the identifier into a List Char and then into a Name type using String interpolation followed by a mkStr1 application but was unable to represent the result in the desired form Lean.MacroM (Lean.TSyntax `term) that macro_rules typically demands.
I am unsure whether Lean4 is capable of such an operation as typically identifiers must be separated by some sort of delimiter (by default whitespace). Would appreciate if someone who has an understanding of parsing and elaboration in this language could help out.
This is a bit of a hack, but seems to work in the given example.
open Lean Name Macro in
macro t:term "(" "split" id:ident ")" : term =>
match id.getId.toString.toList with
| [a, b] =>
let a := mkIdent (mkStr1 ("".push a))
let b := mkIdent (mkStr1 ("".push b))
`($t $a $b)
| _ => throwUnsupported
variable (a b : Type') [LE Type'] [Mul Type']
/-- info: a = b : Prop-/
#guard_msgs in #check Eq (split ab)
/-- info: a ≤ b : Prop -/
#guard_msgs in #check LE.le (split ab)
/-- info: a * b : Type' -/
#guard_msgs in #check HMul.hMul (split ab)
/--
error: elaboration function for '«term_(Split_)»' has not been implemented
Eq(split abc)
-/
#guard_msgs in #check Eq (split abc)