implementing `(x)

Stream: lean4

[Mario Carneiro]

Regarding the purity of macro expansion: Is it possible to implement something like lean 3's `(expr) notation? For easy mode let's assume there are no antiquotations. Here the idea is that at parse time we typecheck expr, and we insert a literal or as close as we can get to one. For example turning `(True.intro) into mkConst `True.intro and `(2 + 2 : Nat) into mkApp5 (mkConst `Add.add) (mkConst `Nat) (mkConst `instAddNat) <2...> <2...>

[Mac]

Since that is almost what `(x) already does, I assume you are just looking for a pure version of `(x) ? For that, you would just need to duplicate `(x) 's behavior, but stripping it of its state (which also include hygiene). It would be cool though if `(x) was intelligent enough to not add state for expressions that don't need it.

[Mac]

The main mechanism of the current quotation syntax can be found here in the Lean 4 source: https://github.com/leanprover/lean4/blob/e70e924327c3b42d28dd8a59340a89cbafb3d5b6/src/Lean/Elab/Quotation.lean#L128

[Mac]

In fact, here is a quick example that does just that:

import Lean
open Lean

partial def pureQuoteSyntax : Syntax → MacroM Syntax
  | Syntax.ident _ rawVal val preresolved => do
    `(Syntax.ident SourceInfo.none $(quote rawVal) $(quote val) $(quote preresolved))
  | stx@(Syntax.node k _) => do
      let empty ← `(Array.empty)
      let args ←
        stx.getArgs.foldlM
          (fun args arg => do
            let arg ← pureQuoteSyntax arg;
            `(Array.push $args $arg))
          empty
      `(Syntax.node $(quote k) $args)
  | Syntax.atom info val =>
    `(Syntax.atom SourceInfo.none $(quote val))
  | Syntax.missing => Macro.throwUnsupported

macro "pureQuote" x:term : term => pureQuoteSyntax x

#check pureQuote (2 + 2 : Nat)
/-
Syntax.node (Name.mkStr (Name.mkStr (Name.mkStr (Name.mkStr Name.anonymous "Lean") "Parser") "Term") "paren")
  (Array.push
    (Array.push (Array.push Array.empty (Syntax.atom SourceInfo.none "("))
      (Syntax.node (Name.mkStr Name.anonymous "null")
        (Array.push
          (Array.push Array.empty
            (Syntax.node (Name.mkStr Name.anonymous "term_+_")
              (Array.push
                (Array.push
                  (Array.push Array.empty
                    (Syntax.node (Name.mkStr Name.anonymous "numLit")
                      (Array.push Array.empty (Syntax.atom SourceInfo.none "2"))))
                  (Syntax.atom SourceInfo.none "+"))
                (Syntax.node (Name.mkStr Name.anonymous "numLit")
                  (Array.push Array.empty (Syntax.atom SourceInfo.none "2"))))))
          (Syntax.node (Name.mkStr Name.anonymous "null")
            (Array.push Array.empty
              (Syntax.node
                (Name.mkStr (Name.mkStr (Name.mkStr (Name.mkStr Name.anonymous "Lean") "Parser") "Term")
                  "typeAscription")
                (Array.push (Array.push Array.empty (Syntax.atom SourceInfo.none ":"))
                  (Syntax.ident SourceInfo.none (String.toSubstring "Nat") (Name.mkStr Name.anonymous "Nat") []))))))))
    (Syntax.atom SourceInfo.none ")")) : Syntax
-/

Note that this example does not preserve source info but that could be easily resolved (by writing a Quote SourceInfo instance and splicing inquote info in the place of SourceInfo.none

[Mac]

And because I was for some reason having fun doing this, here is a version that does that (and doesn't even need MacroM):

import Lean
open Lean Syntax

instance : Quote SourceInfo :=
  Quote.mk fun info =>
    match info with
    | SourceInfo.original leading pos trailing =>
      mkCApp ``SourceInfo.original #[quote leading, quote pos, quote trailing]
    | SourceInfo.synthetic pos endPos =>
      mkCApp ``SourceInfo.synthetic #[quote pos, quote endPos]
    | SourceInfo.none =>
      mkCIdent ``SourceInfo.none

partial def pureQuoteSyntax : Syntax -> Syntax
  | Syntax.ident info rawVal val preresolved =>
    mkCApp ``Lean.Syntax.ident
      #[quote info, quote rawVal, quote val, quote preresolved]
  | stx@(Syntax.node k _) =>
      let args :=
        stx.getArgs.foldl
          (fun args arg =>
            mkCApp ``Array.push #[args, pureQuoteSyntax arg])
          (mkCIdent ``Array.empty)
      mkCApp ``Syntax.node #[quote k, args]
  | Syntax.atom info val =>
    mkCApp ``Syntax.atom #[quote info, quote val]
  | Syntax.missing =>
    mkCIdent ``Syntax.missing

macro "pureQuote" x:term : term => pureQuoteSyntax x

#check pureQuote (2 + 2 : Nat)

[Mac]

Note that, unfortunately, the built-in Quote Syntax instance is just id, so we can't just use quote on Syntax directly.

In fact, @Sebastian Ullrich , I feel like the fact that Quote Syntax is defined as id is incorrect. After all the whole point of Quote is for $(quote x) = x to hold, correct? The id definition violates this. It also means that complex structures with nested Syntax (such as Arrays) won't properly quote either.

[Mac]

For some reason, I even decided to go whole hog and adapt the antiquote code as well: https://gist.github.com/tydeu/bc706963b4e965901abbf44007f9c748

Everything seems like it migrated properly into a Macro which produces pure syntax (I get no type errors and the macro still works), but I did not test it rigorously (or at all, really). So just take it as a proof of concept.

[Sebastian Ullrich]

@Mac I think this topic is about Lean 3's ```(e)
@Mario Carneiro That should definitely be an elaborator, but with that you can certainly implement the Lean 3 semantics: replace antiquotations with fresh mvar-typed locals, elabTermAndSynthesize, reflect resulting Expr into Syntax, substitute back antiquotations (may be fused with previous step)

[Sebastian Ullrich]

Mac said:

It also means that complex structures with nested Syntax (such as Arrays) won't properly quote either.

This is actually exactly how we use the current Quote Syntax instance. There may be use cases for the other definition, but this one works for us.

[Mario Carneiro]

Sebastian Ullrich said:

Mac I think this topic is about Lean 3's ```(e)

No, it's about lean 3's `(e) , the one that produces an expr not a pexpr

[Mario Carneiro]

Lean 4's `(e) produces a Syntax (actually a MacroM Syntax) so it's closer to lean 3's ``(e)

[Mario Carneiro]

The distinction between ``(e) and ```(e) seems to depend on what you do with the macro that you get - you can embed it in another or execute it on the spot

[Mario Carneiro]

The main point is that it should return an Expr, not a Syntax like lean 4 `(e)

[Mario Carneiro]

In lean3, there was a macro (I know, more name overloading) which directly implemented expr literals, so you wouldn't need to actually generate an expression like mkApp (mkConst ...) like I showed, you could instead just hold on to the expr itself (which is easy to generate using the elaborator) and then the "expr literal" macro would be an expr that means "e, as an expr" where e is an actual expr like 2 + 2. In lean 4, I don't know how one could even express such a thing: ideally we would just precalculate an expr static and insert the code "load this static expr" rather than building it on the spot with all those mkApp calls

[Sebastian Ullrich]

Mario Carneiro said:

Sebastian Ullrich said:

Mac I think this topic is about Lean 3's ```(e)

No, it's about lean 3's `(e) , the one that produces an expr not a pexpr

Right, more backticks in Lean 3 made quotations less specific and name literals more specific... whoever thought that was a good idea :halo: . In the/my Lean 4 convention, this macro/elaborator should be called `[Expr|e] .

[Sebastian Ullrich]

I don't think there is any practical need for the "expr literal" macro optimization

[Mario Carneiro]

Sebastian Ullrich said:

I don't think there is any practical need for the "expr literal" macro optimization

It is very important for high performance tactics like normNum that they can use pre-constructed exprs when building things as much as possible. In a perfect world this would be essentially "constant folding" but I don't know to what extent lean supports constant folding of exprs and other inductive types

[Mario Carneiro]

If I put it in an auxiliary def myExpr : Expr := `[Expr| 2 + 2 : Nat], will the code that constructs myExpr be run once or every time myExpr is referenced? If once, is it done at compile time or on first use with a thunk setup? Do I need initialize to do this?

[Sebastian Ullrich]

Currently, closed terms are evaluated exactly once, at startup. We are planning to refine this compilation step in the future so that they are either compiled in as constants (i.e. "evaluated at compile time") or, if they are too costly for that, which shouldn't be an issue for terms already in normal form like this macro, as thunks. So yes, this should be and should keep being essentially free.

[Mario Carneiro]

Does that apply also to closed subterms of an open term, or is the usage of a myExpr auxiliary important to get the optimization?

[Mario Carneiro]

That is, if I have `[Expr|(2 + 2) + $x] then I'd like to compile that to mkApp <+ constant> <nat constant> <instNatAdd constant> <2+2 constant> x

[Sebastian Ullrich]

Yes, that should work. You can give it a try using set_option trace.compiler.ir.result true (run on cmdline). The nat constant will be compiled in directly, there are a few special cases.

[Mario Carneiro]

Great. So the only missing ingredient is translating Expr.app -> mkApp and friends

[Mario Carneiro]

or maybe reflect is able to do this?

[Mario Carneiro]

You say "this should be an elaborator", could you show a simple example of an elaborator so I know what you mean?

[Mario Carneiro]

Is there an equivalent of has_reflect in lean 4? I didn't see a deriving Reflect on Expr

[Sebastian Ullrich]

No, we had no need for it yet, just like the quotation

[Sebastian Ullrich]

import Lean
open Lean
open Lean.Elab.Term

elab "`[Expr|" stx:incQuotDepth(term) "]" : term => do
  let e ← elabTermAndSynthesize stx (expectedType? := none)
  _

[Sebastian Ullrich]

elab is a macro for syntax + @[termElab]

[Mario Carneiro]

That's what I did, but now I'm stuck with e : Expr and want a Syntax (or rather an Expr from it) to insert in the expression

[Mario Carneiro]

That will give me the expr 2 + 2 and I want the expr mkApp ... mk2 mk2

[Sebastian Ullrich]

Yes, the _ is where you fill in the missing implementation of reflect : Expr -> Expr :)

[Mario Carneiro]

where is the expectedType? argument in elab?

[Mario Carneiro]

does it just call ensureHasType on the result?

[Sebastian Ullrich]

Oh, I guess it should be an instance Quote Expr? Depending on how you want to handle antiquotations

[Mario Carneiro]

I'll worry about antiquotations later

[Mario Carneiro]

Do you think it would be better to write Expr -> Syntax or Expr -> Expr for the quote function?

[Sebastian Ullrich]

Yeah, it should be the latter, I just noticed

[Mario Carneiro]

I suppose the former is a bit more versatile and also hooks in to the Quote typeclass, but it needs an elaboration afterward that isn't quite necessary here

[Mario Carneiro]

I take it deriving Quote isn't a thing yet?

[Sebastian Ullrich]

You can access the expected type like this (this will postpone the elaborator until the type is available): https://github.com/leanprover/lean4/blob/e70e924327c3b42d28dd8a59340a89cbafb3d5b6/tests/lean/run/elabCmd.lean#L27-L28
But you shouldn't need to just for checking, the outer expression should take care of that

[Mario Carneiro]

import Lean
open Lean Elab Term

namespace Lean
class Reflect (α : Type) where
  reflectTy : Expr
  reflect : α → Expr

open Reflect

instance : Reflect Bool where
  reflectTy := mkConst ``Bool
  reflect b := if b then mkConst ``true else mkConst ``false

instance : Reflect Nat := ⟨mkConst ``Nat, mkNatLit⟩

instance : Reflect Int where
  reflectTy := mkConst ``Int
  reflect n := if n < 0 then
    mkApp (mkConst ``Int.negOfNat) (mkNatLit n.natAbs)
  else mkApp (mkConst ``Int.ofNat) (mkNatLit n.natAbs)

instance {α : Type} [Reflect α] : Reflect (List α) :=
  ⟨mkApp (mkConst ``List us) (reflectTy α), f⟩
where
  e := reflectTy α
  us := [levelZero]
  f : List α → Expr
  | [] => mkApp (mkConst ``List.nil us) e
  | h::t => mkApp3 (mkConst ``List.cons us) e (reflect h) (f t)

def Name.reflect : Name → Expr
  | anonymous => mkConst ``anonymous
  | str anonymous s _ => mkApp (mkConst ``mkSimple) (mkStrLit s)
  | str p s _ => mkApp2 (mkConst ``mkStr) p.reflect (mkStrLit s)
  | num p v _ => mkApp2 (mkConst ``mkNum) p.reflect (mkNatLit v)

instance : Reflect Name := ⟨mkConst ``Name, Name.reflect⟩

def Level.reflect : Level → Expr
  | zero _       => mkConst ``levelZero
  | succ l _     => mkApp (mkConst ``mkLevelSucc) l.reflect
  | max l₁ l₂ _  => mkApp2 (mkConst ``mkLevelMax) l₁.reflect l₂.reflect
  | imax l₁ l₂ _ => mkApp2 (mkConst ``mkLevelIMax) l₁.reflect l₂.reflect
  | param n _    => mkApp (mkConst ``mkLevelParam) n.reflect
  | mvar n _     => mkApp (mkConst ``mkLevelMVar) n.reflect

instance : Reflect Level := ⟨mkConst ``Level, Level.reflect⟩

instance : Reflect BinderInfo where
  reflectTy := mkConst ``BinderInfo
  reflect
  | BinderInfo.default        => mkConst ``BinderInfo.default
  | BinderInfo.implicit       => mkConst ``BinderInfo.implicit
  | BinderInfo.strictImplicit => mkConst ``BinderInfo.strictImplicit
  | BinderInfo.instImplicit   => mkConst ``BinderInfo.instImplicit
  | BinderInfo.auxDecl        => mkConst ``BinderInfo.auxDecl

open DataValue in
def MData.reflect (md : MData) : Expr := do
  let mut e := mkConst ``MData.empty
  for (k, v) in md do
    let k := k.reflect
    e := match v with
    | ofString v => mkApp3 (mkConst ``KVMap.setString) e k (mkStrLit v)
    | ofBool v   => mkApp3 (mkConst ``KVMap.setBool) e k (Reflect.reflect v)
    | ofName v   => mkApp3 (mkConst ``KVMap.setName) e k v.reflect
    | ofNat v    => mkApp3 (mkConst ``KVMap.setNat) e k (mkNatLit v)
    | ofInt v    => mkApp3 (mkConst ``KVMap.setInt) e k (Reflect.reflect v)
  e

instance : Reflect MData := ⟨mkConst ``MData, MData.reflect⟩

open Literal in
def Expr.reflect : Expr → Expr
  | bvar n _        => mkApp (mkConst ``mkBVar) (mkNatLit n)
  | fvar n _        => mkApp (mkConst ``mkFVar) n.reflect
  | mvar n _        => mkApp (mkConst ``mkMVar) n.reflect
  | sort l _        => mkApp (mkConst ``mkSort) l.reflect
  | const n ls _    => mkApp2 (mkConst ``mkConst) n.reflect (Reflect.reflect ls)
  | app f x _       => mkApp2 (mkConst ``mkApp) f.reflect x.reflect
  | lam x d b c     => mkApp4 (mkConst ``mkLambda)
    x.reflect (Reflect.reflect c.binderInfo) d.reflect b.reflect
  | forallE x d b c => mkApp4 (mkConst ``mkForall)
    x.reflect (Reflect.reflect c.binderInfo) d.reflect b.reflect
  | letE x t v b c  => mkApp5 (mkConst ``mkLet)
    x.reflect t.reflect v.reflect b.reflect (Reflect.reflect c.nonDepLet)
  | lit (natVal n) _ => mkApp (mkConst ``mkNatLit) (mkNatLit n)
  | lit (strVal s) _ => mkApp (mkConst ``mkStrLit) (mkStrLit s)
  | mdata md e _    => mkApp2 (mkConst ``mkMData) md.reflect e.reflect
  | proj s i e _    => mkApp3 (mkConst ``mkProj) s.reflect (mkNatLit i) e.reflect

end Lean

elab "`[Expr|" stx:term "]" : term => do
  let e ← elabTermAndSynthesize stx (expectedType? := none)
  e.reflect

elab "two_plus_two" : term => `[Expr| 2 + 2]

def bar : Nat := two_plus_two

#print bar -- def bar : Nat := 2 + 2

[Mario Carneiro]

Does ForIn provide a fold function? It is a little cumbersome to have to write a do block with a for loop in order to fold over KVMap

[Mario Carneiro]

Also the use of [levelZero] in the reflect instance for List is questionable. The reflect typeclass could come with a level argument

[Daniel Selsam]

@Mario Carneiro FYI a Reflectalready exists (ToExpr https://github.com/leanprover/lean4/blob/master/src/Lean/ToExpr.lean) but it is missing some instances.

[Daniel Selsam]

Actually, it may be designed for a different purpose, since Exprs toExpr to themselves.

[Sebastian Ullrich]

Oh, right! So in that regard it is just like Quote.

[Mario Carneiro]

I don't think either behavior is correct (Mac already observed this for Quote above)

[Mario Carneiro]

In what setting is the identity function the right behavior?

[Mario Carneiro]

For example one reasonable constraint is that inferType (toExpr x) = toTypeExpr, and all instances satisfy this except ToExpr Expr

[Daniel Selsam]

The ToExpr Expr instance is not being used currently.

[Mario Carneiro]

I also slightly prefer the Reflect name because ToExpr suggests a "coercion" like behavior such that the identity function is defensible

[Daniel Selsam]

I agree.

[Yakov Pechersky]

So, if I understand correctly, something that is phrased as

t ← mk_mvar
to_expr ``(false.elim %%t) tt ff >>= exact

or

exact `(True)

in Lean 3 is not yet possible because there is no Quote Expr?

[Sebastian Ullrich]

No, Quote is about reflection at run time. Your first example is covered by the stdlib, your second one by Mario's macro.

[Yakov Pechersky]

Thanks for the clarification. Could you please share a stub showing how the first example is expressed in the stdlib?