Metaprogramming DSL to extract out rewrite rules

Stream: general

[l1mey]

I've been reading the Lean4 metaprogramming book and I'm stuck on a DSL I want to implement, which is for simple term rewriting. I can change the syntax if it makes parsing easier.

declare_syntax_cat rewrite
syntax num   : rewrite
syntax ident : rewrite

inductive Inst : Type where
  | const : Inst
  | add : Nat → Nat → Inst
  | sub : Nat → Nat → Inst

open Lean Elab Meta in
partial def elabIntoRewrite : Lean.Syntax → MetaM Expr
  | `(rewrite| $n:num) => mkAppM ``Inst.const #[mkNatLit n.getNat]
  | _ => throwUnsupportedSyntax

elab "[rewrite| " syn:rewrite "]" : term => elabIntoRewrite syn

#reduce [rewrite|{
  %0:u = const c
  %2:u = add %0
  =>
  %2:u = add %1 %0
}]

#reduce [rewrite|{
  %0:u
  =>
  %0:u = const c
}]

It would be nice if there was more resources on implementing complex macros like this, maybe it would be better to use a more complex function and not simple pattern matching. Though using an external tool to generate the rewrite rules might be fine also.

[Robin Arnez]

Hmm this is currently a syntax error; is this more like what you want?

declare_syntax_cat rewrite
syntax num   : rewrite
syntax "const " ident : rewrite
syntax "add " "%" noWs num : rewrite
syntax "add " "%" noWs num " %" noWs num : rewrite
syntax "sub " "%" noWs num : rewrite
syntax "sub " "%" noWs num " %" noWs num : rewrite

syntax rule := "%" noWs num noWs ":" noWs &"u" (" = " rewrite)?

syntax rewriteSeq := "{" withPosition(many(ppLine colEq rule) ppLine colEq "=>" ppLine colEq rule ppDedent(ppLine)) "}"

syntax "[rewrite| " rewriteSeq "]" : term

#reduce [rewrite|{
  %0:u = const c
  %2:u = add %0
  =>
  %2:u = add %1 %0
}]

#reduce [rewrite|{
  %0:u
  =>
  %0:u = const c
}]