Zulip Chat Archive

Stream: lean4

Topic: implementing `(x)


Mario Carneiro (May 01 2021 at 03:38):

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 (May 01 2021 at 05:03):

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 (May 01 2021 at 05:15):

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 (May 01 2021 at 05:27):

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 (May 01 2021 at 05:52):

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 (May 01 2021 at 06:06):

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 (May 01 2021 at 07:06):

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 (May 01 2021 at 09:05):

@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 (May 01 2021 at 09:06):

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 (May 01 2021 at 11:52):

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 (May 01 2021 at 11:53):

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

Mario Carneiro (May 01 2021 at 11:55):

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 (May 01 2021 at 11:59):

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

Mario Carneiro (May 01 2021 at 12:08):

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 (May 01 2021 at 12:30):

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 (May 01 2021 at 12:32):

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

Mario Carneiro (May 01 2021 at 12:39):

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 (May 01 2021 at 12:42):

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 (May 01 2021 at 12:46):

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 (May 01 2021 at 13:00):

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 (May 01 2021 at 13:01):

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 (May 01 2021 at 13:03):

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 (May 01 2021 at 13:06):

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

Mario Carneiro (May 01 2021 at 13:06):

or maybe reflect is able to do this?

Mario Carneiro (May 01 2021 at 13:07):

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

Mario Carneiro (May 01 2021 at 13:23):

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

Sebastian Ullrich (May 01 2021 at 13:24):

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

Sebastian Ullrich (May 01 2021 at 13:26):

import Lean
open Lean
open Lean.Elab.Term

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

Sebastian Ullrich (May 01 2021 at 13:27):

elab is a macro for syntax + @[termElab]

Mario Carneiro (May 01 2021 at 13:27):

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 (May 01 2021 at 13:28):

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

Sebastian Ullrich (May 01 2021 at 13:29):

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

Mario Carneiro (May 01 2021 at 13:30):

where is the expectedType? argument in elab?

Mario Carneiro (May 01 2021 at 13:30):

does it just call ensureHasType on the result?

Sebastian Ullrich (May 01 2021 at 13:30):

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

Mario Carneiro (May 01 2021 at 13:31):

I'll worry about antiquotations later

Mario Carneiro (May 01 2021 at 13:31):

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

Sebastian Ullrich (May 01 2021 at 13:32):

Yeah, it should be the latter, I just noticed

Mario Carneiro (May 01 2021 at 13:33):

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 (May 01 2021 at 13:33):

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

Sebastian Ullrich (May 01 2021 at 13:35):

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 (May 01 2021 at 14:32):

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 (May 01 2021 at 14:42):

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 (May 01 2021 at 14:46):

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

Daniel Selsam (May 01 2021 at 15:38):

@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 (May 01 2021 at 15:39):

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

Sebastian Ullrich (May 01 2021 at 15:40):

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

Mario Carneiro (May 01 2021 at 15:41):

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

Mario Carneiro (May 01 2021 at 15:41):

In what setting is the identity function the right behavior?

Mario Carneiro (May 01 2021 at 15:43):

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

Daniel Selsam (May 01 2021 at 15:45):

The ToExpr Expr instance is not being used currently.

Mario Carneiro (May 01 2021 at 15:46):

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

Daniel Selsam (May 01 2021 at 15:47):

I agree.

Yakov Pechersky (May 02 2021 at 20:41):

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 (May 02 2021 at 20:59):

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 (May 02 2021 at 21:01):

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


Last updated: Dec 20 2023 at 11:08 UTC