max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: predictable naming for elab_rules

Browse source
This commit is contained in:
Gabriel Ebner 2021-10-25 15:00:10 +02:00 • committed by Sebastian Ullrich
parent ce15ea98c5
commit 422f808bf2
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Elab/ElabRules.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.MacroArgUtil
import Lean.Elab.AuxDef
namespace Lean.Elab.Command
open Lean.Syntax
@ -42,20 +43,24 @@ def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeK
| _, _ => throwError "invalid elab_rules command, specify category using `elab_rules : <cat> ...`"
if let some expId := expty? then
if catName == `term then
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Term.TermElab :=
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with
$alts:matchAlt* | _ => throwUnsupportedSyntax)
else
throwErrorAt expId "syntax category '{catName}' does not support expected type specification"
else if catName == `term then
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Term.TermElab :=
`($[$doc?:docComment]? @[termElab $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab :=
fun stx _ => match stx with
$alts:matchAlt* | _ => throwUnsupportedSyntax)
else if catName == `command then
`($[$doc?:docComment]? @[commandElab $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Command.CommandElab :=
`($[$doc?:docComment]? @[commandElab $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Command.CommandElab :=
fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
else if catName == `tactic then
`($[$doc?:docComment]? @[tactic $(← mkIdentFromRef k):ident] def elabFn : Lean.Elab.Tactic.Tactic :=
`($[$doc?:docComment]? @[tactic $(← mkIdentFromRef k):ident]
aux_def elabRules $(mkIdent k) : Lean.Elab.Tactic.Tactic :=
fun $alts:matchAlt* | _ => throwUnsupportedSyntax)
else
-- We considered making the command extensible and support new user-defined categories. We think it is unnecessary.