From da3bf54ec74d8dd0d8f76a43c48ae3a6c826c023 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Feb 2020 16:24:50 -0800 Subject: [PATCH] feat: elaborate `autoParam`s cc @Kha --- src/Init/Lean/Elab/App.lean | 26 ++++++++++++++++++++------ src/Init/Lean/Elab/Binders.lean | 8 +++++--- src/Init/Lean/Elab/Util.lean | 14 +++++++++----- src/Init/Lean/Expr.lean | 6 ++++++ src/Init/Lean/Parser/Term.lean | 2 +- src/Init/LeanInit.lean | 16 +++++++++------- tests/lean/run/autoparam.lean | 7 +++++++ 7 files changed, 57 insertions(+), 22 deletions(-) create mode 100644 tests/lean/run/autoparam.lean diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean index 57e574ec53..a31baa4f67 100644 --- a/src/Init/Lean/Elab/App.lean +++ b/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 diff --git a/src/Init/Lean/Elab/Binders.lean b/src/Init/Lean/Elab/Binders.lean index fb85c35425..20f39d6251 100644 --- a/src/Init/Lean/Elab/Binders.lean +++ b/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 diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean index 4ddc1c76cc..97feb5e7e9 100644 --- a/src/Init/Lean/Elab/Util.lean +++ b/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; diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean index 3552cc9118..d49d471354 100644 --- a/src/Init/Lean/Expr.lean +++ b/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 diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 1c06791cf2..e43221a92d 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/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 >> "}" diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 7620e97069..6e03a2aab0 100644 --- a/src/Init/LeanInit.lean +++ b/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 := α diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean new file mode 100644 index 0000000000..4e35e1296f --- /dev/null +++ b/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