Lean 4 (Meta)programming Cookbook

Adding Syntax for terms🔗

Contributors: ajay-k-nair, Siddhartha Gadgil

Syntax for Python for loop🔗

We will improve upon the macro that we defined in the recipe A macro that parses Python-like for loop, for parsing Python for loop syntax. Here we use an elaborator (elab) instead of a macro to parse the same syntax. Thus, rather than just doing a simple syntactic transformation, we generate an expression from the syntax. This lets us perform more complex transformations and checks during elaboration.

This version checks whether the collection being iterated over is a List or an Array and handles each case accordingly. This also gives a more informative error message when the collection is of an unexpected type.

An elaborator that parses Python-like for loop🔗

Here is a more robust and complete implementation using an elaborator (elab). This version checks whether the collection being iterated over is a List or an Array and handles each case accordingly:

elab "[" t:term "py_for" x:ident "in" l:term "]" : term => do let fnStx ← `(fun $x => $t) let lExpr ← elabTerm l none let fn ← elabTerm fnStx none let ltype ← inferType lExpr Term.synthesizeSyntheticMVarsNoPostponing if ltype.isAppOf ``List then mkAppM ``List.map #[fn, lExpr] else if ltype.isAppOf ``Array then mkAppM ``Array.map #[fn, lExpr] else throwError "Expected a List or Array in py_for comprehension, got {ltype}" #eval [x * 2 py_for x in [1, 2, 3, 4]] --> [2, 4, 6, 8] #eval [x * 2 py_for x in #[1, 2, 3, 4]] --> #[2, 4, 6, 8] /-- error: Expected a List or Array in py_for comprehension, got String -/ #guard_msgs in #eval [x * 2 py_for x in "List"]

Let's break down the specific metaprogramming functions used in the elaborator above:

  • Term.elabTerm is used to elaborate the syntax of the collection l and the function fnStx into actual Lean expressions, while Meta.inferType is used to determine the type of the collection.

  • Term.synthesizeSyntheticMVarsNoPostponing is called to ensure that any metavariables generated during elaboration are fully resolved before we attempt to check the type. If the term l is a List, ltype will have the form List ?m, where ?m is a metavariable representing the element type. Calling Term.synthesizeSyntheticMVarsNoPostponing ensures that ?m is resolved to a concrete type, allowing us to proceed with the application of mkAppM without running into issues caused by unresolved metavariables.

  • Expr.isAppOf is used to check whether the type of l is a List or an Array. Depending on the result, we use mkAppM to construct the appropriate List.map or Array.map expression. If the type is neither, we throw a custom error.