Replacing certain keywords during syntax evaluation

Stream: lean4

[Marx]

Hi everyone,

I’m working on defining a syntax that looks like this:

{x0 > 0}
or
{x1 = 2 /\ 0 <= x3 /\ x0 = 0}

The goal is for this syntax to evaluate to the following in the next step:

fun n : Nat => {(n.add 0) > 0}
or
fun n : Nat => {(n.add 0) = 2 /\ 0 <= (n.add 3) /\ (n.add 0) = 0}

So every occurence of any (xn) with n being a numeral literal gets replaced.

I’m trying to achieve this while adhering to the following constraints:

1. Preserve existing term syntax: Avoid polluting or modifying the existing syntax category for terms.
2. Reuse existing definitions: Ensure it’s not necessary to redefine all operations for natural numbers and propositions. However, if redefining them is unavoidable, I’d appreciate guidance on a simple, non-redundant approach to achieve this

This is what I have so far:

import Lean
open Lean Elab

declare_syntax_cat testSyntax
declare_syntax_cat toBeReplaced

syntax term: testSyntax
syntax "(x" num ")" : toBeReplaced
syntax toBeReplaced : testSyntax
syntax toBeReplaced testSyntax : testSyntax

def getNum (reg: TSyntax `toBeReplaced): Nat :=
  match reg with
  | `(toBeReplaced | (x$n:num)) => n.getNat
  | _ => 9999 -- This is bad but I am lazy

partial def testFun (term: TSyntax `testSyntax): TermElabM (TSyntax `term) := do
  match term with
  | `(testSyntax | $r:toBeReplaced) =>
    let t := getNum r
    return ←`(term | $(mkIdent s!"{t}".toName))
  | `(testSyntax | $r:toBeReplaced $t:testSyntax) =>
    let t1 := getNum r
    let t2 ← testFun t
    return ←`(term | $(mkIdent s!"{t1}".toName) $t2)
  | `(testSyntax | $t:term) =>
    let t1 ← `(term | term)
    return ←`(term | $t1)
  | _ => `(term | NOTHING)

elab "start" t:testSyntax "end" : term => do
  let processedTerm ← testFun t
  logInfo processedTerm
  -- let result ← Lean.Elab.Term.elabTerm processedTerm (some (.const ``Nat []))
  return mkNatLit 0 -- return result

However, this approach encounters the following issues:

• The toBeReplaced syntax is not replaced correctly when nested inside another term.
• Attempting to use individual components of the toBeReplaced syntax as operands in other expressions.

I would really appreciate any input.

[Sebastian Ullrich]

Likely you don't want a new syntax category but to parse a term and then recursively replace idents inside of it. See docs#Lean.Elab.Term.expandCDot? for a similar approach.

[Marx]

Thank you for the suggestion, I'm gonna give it a try

[Marx]

Sebastian Ullrich said:

Likely you don't want a new syntax category but to parse a term and then recursively replace idents inside of it. See docs#Lean.Elab.Term.expandCDot? for a similar approach.

So i've had a look at it and this look pretty much like what I could use. Unfortunately I find it very difficult to understand in detail. Could you provide me some further documentation or information about this. I would really appreciate that.