feat: elaborate autoParams

cc @Kha

src/Init/Lean/Elab/App.lean

@@ -99,8 +99,7 @@ structure ElabAppArgsCtx :=
 (foundExplicit : Bool := false)       -- true if an explicit argument has already been processed
 
 private def isAutoOrOptParam (type : Expr) : Bool :=
--- TODO: add auto param
-type.getOptParamDefault?.isSome
+type.getOptParamDefault?.isSome || type.getAutoParamTactic?.isSome
 
 /- Auxiliary function for retrieving the resulting type of a function application.
    See `propagateExpectedType`. -/
@@ -227,10 +226,25 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
         if h : ctx.argIdx < ctx.args.size then do
           argElab ← elabArg ctx.ref e (ctx.args.get ⟨ctx.argIdx, h⟩) d;
           elabAppArgsAux { argIdx := ctx.argIdx + 1, .. ctx } (mkApp e argElab) (b.instantiate1 argElab)
-        else match ctx.explicit, d.getOptParamDefault? with
-          | false, some defVal => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
-          | _, _               =>
-            -- TODO: tactic auto param
+        else match ctx.explicit, d.getOptParamDefault?, d.getAutoParamTactic? with
+          | false, some defVal, _                      => elabAppArgsAux ctx (mkApp e defVal) (b.instantiate1 defVal)
+          | false, _, some (Expr.const tacticDecl _ _) => do
+            env ← getEnv;
+            match evalSyntaxConstant env tacticDecl with
+            | Except.error err       => throwError ctx.ref err
+            | Except.ok tacticSyntax => do
+              tacticBlock ← `(begin $(tacticSyntax.getArgs)* end);
+              -- tacticBlock does not have any position information
+              -- use ctx.ref.getHeadInfo if available
+              let tacticBlock := match ctx.ref.getHeadInfo with
+                | some info => tacticBlock.replaceInfo info
+                | _         => tacticBlock;
+              let d := d.getArg! 0; -- `autoParam type := by tactic` ==> `type`
+              argElab ← elabArg ctx.ref e (Arg.stx tacticBlock) d;
+              elabAppArgsAux ctx (mkApp e argElab) (b.instantiate1 argElab)
+          | false, _, some _ =>
+            throwError ctx.ref "invalid autoParam, argument must be a constant"
+          | _, _, _ =>
             if ctx.namedArgs.isEmpty then
               finalize ()
             else

src/Init/Lean/Elab/Binders.lean

@@ -52,7 +52,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
         arg ← quoteAutoTactic arg;
         `(Array.push $args $arg)) empty;
     `(Syntax.node $(quote k) $args)
-| Syntax.atom info val => `(Syntax.missing) -- atoms are irrelevant for auto tactics, we only care about `Syntax.node`s
+| Syntax.atom info val => `(Syntax.atom none $(quote val))
 | Syntax.missing       => unreachable!
 
 def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
@@ -62,6 +62,7 @@ withFreshMacroScope $ do
   tactic ← quoteAutoTactic tactic;
   val ← elabTerm tactic type;
   val ← instantiateMVars tactic val;
+  trace `Elab.autoParam tactic $ fun _ => val;
   let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
   addDecl tactic decl;
   compileDecl tactic decl;
@@ -81,8 +82,9 @@ else
     let defaultVal := modifier.getArg 1;
     `(optParam $type $defaultVal)
   else if kind == `Lean.Parser.Term.binderTactic then do
-    name ← declareTacticSyntax (modifier.getArg 2);
-    `(autoParam $type $(quote name))
+    let tac := modifier.getArg 2;
+    name ← declareTacticSyntax tac;
+    `(autoParam $type $(mkTermIdFrom tac name))
   else
     throwUnsupportedSyntax
 

src/Init/Lean/Elab/Util.lean

@@ -107,7 +107,7 @@ pure { table := table }
 private def throwUnexpectedElabType {γ} (typeName : Name) (constName : Name) : ExceptT String Id γ :=
 throw ("unexpected elaborator type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")
 
-private unsafe def mkElabFnOfConstantUnsafe (γ) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ :=
+private unsafe def evalConstantUnsafe (γ) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ :=
 match env.find? constName with
 | none      => throw ("unknow constant '" ++ toString constName ++ "'")
 | some info =>
@@ -117,8 +117,12 @@ match env.find? constName with
     else env.evalConst γ constName
   | _ => throwUnexpectedElabType typeName constName
 
-@[implementedBy mkElabFnOfConstantUnsafe]
-constant mkElabFnOfConstant (γ : Type) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ := throw ""
+-- We mark `evalConstant` as private because it is only safe if `mkConst typeName` is definitionally equal to `γ`.
+@[implementedBy evalConstantUnsafe]
+private constant evalConstant (γ : Type) (env : Environment) (typeName : Name) (constName : Name) : ExceptT String Id γ := throw ""
+
+def evalSyntaxConstant (env : Environment) (constName : Name) : ExceptT String Id Syntax :=
+evalConstant Syntax env `Lean.Syntax constName
 
 private def ElabAttribute.addImportedParsers {γ} (typeName : Name) (builtinTableRef : IO.Ref (ElabFnTable γ))
     (env : Environment) (es : Array (Array ElabAttributeOLeanEntry)) : IO (ElabAttributeExtensionState γ) := do
@@ -127,7 +131,7 @@ table ← es.foldlM
   (fun table entries =>
     entries.foldlM
       (fun (table : ElabFnTable γ) entry =>
-        match mkElabFnOfConstant γ env typeName entry.constName with
+        match evalConstant γ env typeName entry.constName with
         | Except.ok f     => pure $ table.insert entry.kind f
         | Except.error ex => throw (IO.userError ex))
       table)
@@ -139,7 +143,7 @@ private def ElabAttribute.addExtensionEntry {γ} (s : ElabAttributeExtensionStat
 
 private def ElabAttribute.add {γ} (parserNamespace : Name) (typeName : Name) (ext : ElabAttributeExtension γ)
     (env : Environment) (constName : Name) (arg : Syntax) (persistent : Bool) : IO Environment := do
-match mkElabFnOfConstant γ env typeName constName with
+match evalConstant γ env typeName constName with
 | Except.error ex => throw (IO.userError ex)
 | Except.ok f     => do
   kind ← IO.ofExcept $ syntaxNodeKindOfAttrParam env parserNamespace arg;

src/Init/Lean/Expr.lean

@@ -733,6 +733,12 @@ if e.isAppOfArity `optParam 2 then
 else
   none
 
+def getAutoParamTactic? (e : Expr) : Option Expr :=
+if e.isAppOfArity `autoParam 2 then
+  some e.appArg!
+else
+  none
+
 @[specialize] private partial def hasAnyFVarAux (p : FVarId → Bool) : Expr → Bool
 | e => if !e.hasFVar then false else
   match e with

src/Init/Lean/Parser/Term.lean

@@ -86,7 +86,7 @@ def optType : Parser := optional typeSpec
 @[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
-def binderTactic  := parser! try (" := " >> " by ") >> tacticParser
+def binderTactic  := parser! try (" := " >> " by ") >> Tactic.nonEmptySeq
 def binderDefault := parser! " := " >> termParser
 def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
 def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"

src/Init/LeanInit.lean

@@ -168,6 +168,8 @@ structure SourceInfo :=
 (pos      : String.Pos)
 (trailing : Substring)
 
+instance SourceInfo.inhabited : Inhabited SourceInfo := ⟨⟨"".toSubstring, arbitrary _, "".toSubstring⟩⟩
+
 abbrev SyntaxNodeKind := Name
 
 /- Syntax AST -/
@@ -181,13 +183,6 @@ inductive Syntax
 instance Syntax.inhabited : Inhabited Syntax :=
 ⟨Syntax.missing⟩
 
-/--
-  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
-  the tactic described by the syntax object stored at `tacDeclName`.
-  Like `optParam`, this gadget only affects elaboration.
-  For example, the tactic will *not* be invoked during type class resolution. -/
-abbrev autoParam.{u} (α : Sort u) (tacDeclName : Name) : Sort u := α
-
 /- Builtin kinds -/
 def choiceKind : SyntaxNodeKind := `choice
 def nullKind : SyntaxNodeKind := `null
@@ -814,3 +809,10 @@ def mapSepElems (a : Array Syntax) (f : Syntax → Syntax) : Array Syntax :=
 Id.run $ a.mapSepElemsM f
 
 end Array
+
+/--
+  Gadget for automatic parameter support. This is similar to the `optParam` gadget, but it uses
+  the given tactic.
+  Like `optParam`, this gadget only affects elaboration.
+  For example, the tactic will *not* be invoked during type class resolution. -/
+abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α

tests/lean/run/autoparam.lean

@@ -0,0 +1,7 @@
+new_frontend
+
+def f (x y : Nat) (h : x = y := by assumption) : Nat :=
+x + x
+
+def g (x y z : Nat) (h : x = y) : Nat :=
+f x y