diff --git a/doc/declarations.md b/doc/declarations.md index 0ffce145a2..e22e3582ae 100644 --- a/doc/declarations.md +++ b/doc/declarations.md @@ -228,7 +228,7 @@ end Hide Note that in the syntax of the inductive definition ``Foo``, the context ``(a : α)`` is left implicit. In other words, constructors and recursive arguments are written as though they have return type ``Foo`` rather than ``Foo a``. -Elements of the context ``(a : α)`` can be marked implicit as described in [Implicit Arguments](#implicit.md#implicit_arguments). These annotations bear only on the type former, ``Foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[matchPattern]`` [attribute](TODO: missing link) to ensure that these will be used appropriately by the [Equation Compiler](#the-equation-compiler). +Elements of the context ``(a : α)`` can be marked implicit as described in [Implicit Arguments](#implicit.md#implicit_arguments). These annotations bear only on the type former, ``Foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[match_pattern]`` [attribute](TODO: missing link) to ensure that these will be used appropriately by the [Equation Compiler](#the-equation-compiler). There are restrictions on the universe ``u`` in the return type ``Sort u`` of the type former. There are also restrictions on the universe ``u`` in the return type ``Sort u`` of the motive of the eliminator. These will be discussed in the next section in the more general setting of inductive families. @@ -251,7 +251,7 @@ inductive List (α : Type u) | nil : List α | cons (a : α) (l : List α) : List α -@[matchPattern] +@[match_pattern] def List.nil' (α : Type u) : List α := List.nil def length {α : Type u} : List α → Nat @@ -457,7 +457,7 @@ In the last case, the pattern must be enclosed in parentheses. Each term ``tᵢ`` is an expression in the context ``(a : α)`` together with the variables introduced on the left-hand side of the token ``=>``. The term ``tᵢ`` can also include recursive calls to ``foo``, as described below. The equation compiler does case splitting on the variables ``(b : β)`` as necessary to match the patterns, and defines ``foo`` so that it has the value ``tᵢ`` in each of the cases. In ideal circumstances (see below), the equations hold definitionally. Whether they hold definitionally or only propositionally, the equation compiler proves the relevant equations and assigns them internal names. They are accessible by the ``rewrite`` and ``simp`` tactics under the name ``foo`` (see [Rewrite](tactics.md#rewrite) and _[TODO: where is simplifier tactic documented?]_. If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case. Thus, if the last pattern is a variable, it covers all the remaining cases. If the patterns that are presented do not cover all possible cases, the equation compiler raises an error. -When identifiers are marked with the ``[matchPattern]`` attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write ``n+1`` and ``0`` instead of ``Nat.succ n`` and ``Nat.zero`` in patterns. +When identifiers are marked with the ``[match_pattern]`` attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write ``n+1`` and ``0`` instead of ``Nat.succ n`` and ``Nat.zero`` in patterns. For a nonrecursive definition involving case splits, the defining equations will hold definitionally. With inductive types like ``Char``, ``String``, and ``Fin n``, a case split would produce definitions with an inordinate number of cases. To avoid this, the equation compiler uses ``if ... then ... else`` instead of ``casesOn`` when defining the function. In this case, the defining equations hold definitionally as well. diff --git a/doc/dev/ffi.md b/doc/dev/ffi.md index 0f0dd66723..3c6329db25 100644 --- a/doc/dev/ffi.md +++ b/doc/dev/ffi.md @@ -45,7 +45,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se * it has a single constructor with a single parameter of *relevant* type is represented by the representation of that parameter's type. - + For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`. * `Nat` is represented by `lean_object *`. Its runtime value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`). @@ -70,13 +70,13 @@ When including Lean code as part of a larger program, modules must be *initializ Module initialization entails * initialization of all "constants" (nullary functions), including closed terms lifted out of other functions * execution of all `[init]` functions -* execution of all `[builtinInit]` functions, if the `builtin` parameter of the module initializer has been set +* execution of all `[builtin_init]` functions, if the `builtin` parameter of the module initializer has been set The module initializer is automatically run with the `builtin` flag for executables compiled from Lean code and for "plugins" loaded with `lean --plugin`. For all other modules imported by `lean`, the initializer is run without `builtin`. -Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtinInit]` functions are only run for native executable or plugins, regardless of whether their module is imported or not. +Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not. `lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping). - + The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules. Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe. Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations: diff --git a/doc/examples/widgets.lean b/doc/examples/widgets.lean index f9047c068a..ce5c0bd43d 100644 --- a/doc/examples/widgets.lean +++ b/doc/examples/widgets.lean @@ -106,7 +106,7 @@ more information for us, in the form of a `snap : Snapshot`. With this in hand, -/ open Server RequestM in -@[serverRpcMethod] +@[server_rpc_method] def getType (params : GetTypeParams) : RequestM (RequestTask CodeWithInfos) := withWaitFindSnapAtPos params.pos fun snap => do runTermElabM snap do diff --git a/doc/lean3changes.md b/doc/lean3changes.md index 895347706d..bd93321c7b 100644 --- a/doc/lean3changes.md +++ b/doc/lean3changes.md @@ -287,11 +287,11 @@ Lean execution runtime. For example, we cannot prove in Lean that arrays have a the runtime used to execute Lean programs guarantees that an array cannot have more than 2^64 (2^32) elements in a 64-bit (32-bit) machine. We can take advantage of this fact to provide a more efficient implementation for array functions. However, the efficient version would not be very useful if it can only be used in -unsafe code. Thus, Lean 4 provides the attribute `@[implementedBy functionName]`. The idea is to provide +unsafe code. Thus, Lean 4 provides the attribute `@[implemented_by functionName]`. The idea is to provide an unsafe (and potentially more efficient) version of a safe definition or constant. The function `f` -at the attribute `@[implementedBy f]` is very similar to an extern/foreign function, +at the attribute `@[implemented_by f]` is very similar to an extern/foreign function, the key difference is that it is implemented in Lean itself. Again, the logical soundness of the system -cannot be compromised by using the attribute `implementedBy`, but if the implementation is incorrect your +cannot be compromised by using the attribute `implemented_by`, but if the implementation is incorrect your program may crash at runtime. In the following example, we define `withPtrUnsafe a k h` which executes `k` using the memory address where `a` is stored in memory. The argument `h` is proof that `k` is a constant function. Then, we "seal" this unsafe implementation at `withPtr`. The proof `h` @@ -302,7 +302,7 @@ unsafe def withPtrUnsafe {α β : Type} (a : α) (k : USize → β) (h : ∀ u, k u = k 0) : β := k (ptrAddrUnsafe a) -@[implementedBy withPtrUnsafe] +@[implemented_by withPtrUnsafe] def withPtr {α β : Type} (a : α) (k : USize → β) (h : ∀ u, k u = k 0) : β := k 0 ``` diff --git a/doc/typeclass.md b/doc/typeclass.md index fece6f9002..e0aec37590 100644 --- a/doc/typeclass.md +++ b/doc/typeclass.md @@ -382,7 +382,7 @@ class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where export HMul (hMul) -@[defaultInstance] +@[default_instance] instance : HMul Int Int Int where hMul := Int.mul @@ -391,7 +391,7 @@ def xs : List Int := [1, 2, 3] #check fun y => xs.map (fun x => hMul x y) -- Int -> List Int # end Ex ``` -By tagging the instance above with the attribute `defaultInstance`, we are instructing Lean +By tagging the instance above with the attribute `default_instance`, we are instructing Lean to use this instance on pending type class synthesis problems. The actual Lean implementation defines homogeneous and heterogeneous classes for arithmetical operators. Moreover, `a+b`, `a*b`, `a-b`, `a/b`, and `a%b` are notations for the heterogeneous versions. @@ -404,7 +404,7 @@ structure Rational where den : Nat inv : den ≠ 0 -@[defaultInstance 200] +@[default_instance 200] instance : OfNat Rational n where ofNat := { num := n, den := 1, inv := by decide } @@ -423,7 +423,7 @@ Now, we reveal how the notation `a*b` is defined in Lean. class OfNat (α : Type u) (n : Nat) where ofNat : α -@[defaultInstance] +@[default_instance] instance (n : Nat) : OfNat Nat n where ofNat := n @@ -433,7 +433,7 @@ class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where class Mul (α : Type u) where mul : α → α → α -@[defaultInstance 10] +@[default_instance 10] instance [Mul α] : HMul α α α where hMul a b := Mul.mul a b diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 33572129ae..fd21f37ba8 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -1618,7 +1618,7 @@ external type checkers (e.g., Trepplein) that do not implement this feature. Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter. So, you are mainly losing the capability of type checking your development using external checkers. -Recall that the compiler trusts the correctness of all `[implementedBy ...]` and `[extern ...]` annotations. +Recall that the compiler trusts the correctness of all `[implemented_by ...]` and `[extern ...]` annotations. If an extern function is executed, then the trusted code base will also include the implementation of the associated foreign function. -/ diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 0c45882ab5..76d1f5d6d1 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2396,7 +2396,7 @@ and returns `default`. It is primarily intended for debugging in pure contexts, and assertion failures. Because this is a pure function with side effects, it is marked as -`@[neverExtract]` so that the compiler will not perform common sub-expression +`@[never_extract]` so that the compiler will not perform common sub-expression elimination and other optimizations that assume that the expression is pure. -/ @[noinline, neverExtract] diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index 59382d1095..cc563ba458 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/src/Lean/Compiler/ExternAttr.lean @@ -37,7 +37,7 @@ structure ExternAttrData where deriving Inhabited -- def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit --- @[builtinAttrParser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry +-- @[builtin_attr_parser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do let arity? := if stx[1].isNone then none else some <| stx[1][0].isNatLit?.getD 0 let entriesStx := stx[2].getArgs diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index fff3039ed3..237434c7a3 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -438,7 +438,7 @@ end Decl @[export lean_ir_mk_extern_decl] def mkExternDecl (f : FunId) (xs : Array Param) (ty : IRType) (e : ExternAttrData) : Decl := Decl.extern f xs ty e --- Hack: we use this declaration as a stub for declarations annotated with `implementedBy` or `init` +-- Hack: we use this declaration as a stub for declarations annotated with `implemented_by` or `init` @[export lean_ir_mk_dummy_extern_decl] def mkDummyExternDecl (f : FunId) (xs : Array Param) (ty : IRType) : Decl := Decl.fdecl f xs ty FnBody.unreachable {} diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean index cc017e309d..bd3a93322f 100644 --- a/src/Lean/Compiler/ImplementedByAttr.lean +++ b/src/Lean/Compiler/ImplementedByAttr.lean @@ -11,7 +11,7 @@ import Lean.Elab.InfoTree namespace Lean.Compiler builtin_initialize implementedByAttr : ParametricAttribute Name ← registerParametricAttribute { - name := `implementedBy + name := `implemented_by descr := "name of the Lean (probably unsafe) function that implements opaque constant" getParam := fun declName stx => do let decl ← getConstInfo declName @@ -19,13 +19,13 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara let fnName ← Elab.resolveGlobalConstNoOverloadWithInfo fnNameStx let fnDecl ← getConstInfo fnName unless decl.levelParams.length == fnDecl.levelParams.length do - throwError "invalid 'implementedBy' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}" + throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has {fnDecl.levelParams.length} universe level parameter(s), but '{declName}' has {decl.levelParams.length}" let declType := decl.type let fnType := fnDecl.instantiateTypeLevelParams (decl.levelParams.map mkLevelParam) unless declType == fnType do - throwError "invalid 'implementedBy' argument '{fnName}', '{fnName}' has type{indentExpr fnType}\nbut '{declName}' has type{indentExpr declType}" + throwError "invalid 'implemented_by' argument '{fnName}', '{fnName}' has type{indentExpr fnType}\nbut '{declName}' has type{indentExpr declType}" if decl.name == fnDecl.name then - throwError "invalid 'implementedBy' argument '{fnName}', function cannot be implemented by itself" + throwError "invalid 'implemented_by' argument '{fnName}', function cannot be implemented by itself" return fnName } diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 2b3f6c93b1..16d7a5c859 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -77,7 +77,7 @@ def registerInitAttr (attrName : Name) (runAfterImport : Bool) (ref : Name := by registerInitAttrInner attrName runAfterImport ref builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init true -builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit false +builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtin_init false def getInitFnNameForCore? (env : Environment) (attr : ParametricAttribute Name) (fn : Name) : Option Name := match attr.getParam? env fn with diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean index b8ca115822..79a84bf694 100644 --- a/src/Lean/Compiler/InlineAttrs.lean +++ b/src/Lean/Compiler/InlineAttrs.lean @@ -13,13 +13,13 @@ inductive InlineAttributeKind where deriving Inhabited, BEq, Hashable /-- - This is an approximate test for testing whether `declName` can be annotated with the `[macroInline]` attribute or not. + This is an approximate test for testing whether `declName` can be annotated with the `[macro_inline]` attribute or not. -/ private def isValidMacroInline (declName : Name) : CoreM Bool := do let .defnInfo info ← getConstInfo declName | return false unless info.all.length = 1 do - -- We do not allow `[macroInline]` attributes at mutual recursive definitions + -- We do not allow `[macro_inline]` attributes at mutual recursive definitions return false let env ← getEnv let isRec (declName' : Name) : Bool := @@ -34,10 +34,10 @@ private def isValidMacroInline (declName : Name) : CoreM Bool := do builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ← registerEnumAttributes [(`inline, "mark definition to be inlined", .inline), - (`inlineIfReduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", .inlineIfReduce), + (`inline_if_reduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", .inlineIfReduce), (`noinline, "mark definition to never be inlined", .noinline), - (`macroInline, "mark definition to always be inlined before ANF conversion", .macroInline), - (`alwaysInline, "mark definition to be always inlined", .alwaysInline)] + (`macro_inline, "mark definition to always be inlined before ANF conversion", .macroInline), + (`always_inline, "mark definition to be always inlined", .alwaysInline)] fun declName kind => do ofExcept <| checkIsDefinition (← getEnv) declName if kind matches .macroInline then diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index 7cbfbb94d6..3dfb6aa42b 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -421,7 +421,7 @@ def Decl.inlineIfReduceAttr (decl : Decl) : Bool := def Decl.alwaysInlineAttr (decl : Decl) : Bool := decl.inlineAttr? matches some .alwaysInline -/-- Return `true` if the given declaration has been annotated with `[inline]`, `[inlineIfReduce]`, `[macroInline]`, or `[alwaysInline]` -/ +/-- Return `true` if the given declaration has been annotated with `[inline]`, `[inline_if_reduce]`, `[macro_inline]`, or `[always_inline]` -/ def Decl.inlineable (decl : Decl) : Bool := match decl.inlineAttr? with | some .noinline => false @@ -439,7 +439,7 @@ def f (a_0 ... a_i ...) := ``` That is, `f` is a sequence of declarations followed by a `cases` on the parameter `i`. We use this function to decide whether we should inline a declaration tagged with -`[inlineIfReduce]` or not. +`[inline_if_reduce]` or not. -/ def Decl.isCasesOnParam? (decl : Decl) : Option Nat := go decl.value diff --git a/src/Lean/Compiler/LCNF/ConfigOptions.lean b/src/Lean/Compiler/LCNF/ConfigOptions.lean index a9bfc7c42c..91c0a1d30d 100644 --- a/src/Lean/Compiler/LCNF/ConfigOptions.lean +++ b/src/Lean/Compiler/LCNF/ConfigOptions.lean @@ -22,7 +22,7 @@ structure ConfigOptions where -/ maxRecInline : Nat := 1 /-- - Maximum number of times a recursive definition tagged with `[inlineIfReduce]` can be recursively inlined + Maximum number of times a recursive definition tagged with `[inline_if_reduce]` can be recursively inlined before generating an error during compilation. -/ maxRecInlineIfReduce : Nat := 16 @@ -43,7 +43,7 @@ register_builtin_option compiler.maxRecInline : Nat := { register_builtin_option compiler.maxRecInlineIfReduce : Nat := { defValue := 16 group := "compiler" - descr := "(compiler) maximum number of times a recursive definition tagged with `[inlineIfReduce]` can be recursively inlined before generating an error during compilation." + descr := "(compiler) maximum number of times a recursive definition tagged with `[inline_if_reduce]` can be recursively inlined before generating an error during compilation." } def toConfigOptions (opts : Options) : ConfigOptions := { @@ -52,4 +52,4 @@ def toConfigOptions (opts : Options) : ConfigOptions := { maxRecInlineIfReduce := compiler.maxRecInlineIfReduce.get opts } -end Lean.Compiler.LCNF \ No newline at end of file +end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index f0b75177b6..8776e19cb8 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -18,7 +18,7 @@ namespace Lean.Compiler.LCNF We do not generate code for `declName` if - Its type is a proposition. - Its type is a type former. -- It is tagged as `[macroInline]`. +- It is tagged as `[macro_inline]`. - It is a type class instance. Remark: we still generate code for declarations tagged as `[inline]` diff --git a/src/Lean/Compiler/LCNF/Simp/Config.lean b/src/Lean/Compiler/LCNF/Simp/Config.lean index 438ca49e4a..d68c894e1d 100644 --- a/src/Lean/Compiler/LCNF/Simp/Config.lean +++ b/src/Lean/Compiler/LCNF/Simp/Config.lean @@ -24,7 +24,7 @@ structure Config where -/ inlinePartial := false /-- - If `implementedBy` is `true`, we apply the `implementedBy` replacements. + If `implementedBy` is `true`, we apply the `implemented_by` replacements. Remark: we only apply `casesOn` replacements at phase 2 because `cases` constructor may not have enough information for reconstructing the original `casesOn` application at phase 1. diff --git a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean index 2bbc4b61bc..5b26014eb1 100644 --- a/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean +++ b/src/Lean/Compiler/LCNF/Simp/InlineCandidate.lean @@ -19,7 +19,7 @@ structure InlineCandidateInfo where value : Code f : Expr args : Array Expr - /-- `ifReduce = true` if the declaration being inlined was tagged with `inlineIfReduce`. -/ + /-- `ifReduce = true` if the declaration being inlined was tagged with `inline_if_reduce`. -/ ifReduce : Bool /-- `recursive = true` if the declaration being inline is in a mutually recursive block. -/ recursive : Bool := false @@ -47,7 +47,7 @@ def inlineCandidate? (e : Expr) : SimpM (Option InlineCandidateInfo) := do if !decl.inlineIfReduceAttr && decl.recursive then return false if mustInline then return true /- - We don't inline instances tagged with `[inline]/[alwaysInline]/[inlineIfReduce]` at the base phase + We don't inline instances tagged with `[inline]/[always_inline]/[inline_if_reduce]` at the base phase We assume that at the base phase these annotations are for the instance methods that have been lambda lifted. -/ if (← inBasePhase <&&> Meta.isInstance decl.name) then diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean index 3200d13f23..2b6ae4d157 100644 --- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean +++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean @@ -136,7 +136,7 @@ where let numOccs := numOccs + 1 let inlineIfReduce ← if let some decl ← getDecl? declName then pure decl.inlineIfReduceAttr else pure false if recursive && inlineIfReduce && numOccs > (← getConfig).maxRecInlineIfReduce then - throwError "function `{declName}` has been recursively inlined more than #{(← getConfig).maxRecInlineIfReduce}, consider removing the attribute `[inlineIfReduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce `" + throwError "function `{declName}` has been recursively inlined more than #{(← getConfig).maxRecInlineIfReduce}, consider removing the attribute `[inline_if_reduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce `" return numOccs /-- diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean index eaaafc036f..0bc2e4a3f5 100644 --- a/src/Lean/Compiler/LCNF/ToDecl.lean +++ b/src/Lean/Compiler/LCNF/ToDecl.lean @@ -10,7 +10,7 @@ import Lean.Compiler.LCNF.ToLCNF namespace Lean.Compiler.LCNF /-- -Inline constants tagged with the `[macroInline]` attribute occurring in `e`. +Inline constants tagged with the `[macro_inline]` attribute occurring in `e`. -/ def macroInline (e : Expr) : CoreM Expr := Core.transform e fun e => do @@ -89,7 +89,7 @@ The steps for this are roughly: - partially erasing type information of the declaration - eta-expanding the declaration value. - if the declaration has an unsafe-rec version, use it. -- expand declarations tagged with the `[macroInline]` attribute +- expand declarations tagged with the `[macro_inline]` attribute - turn the resulting term into LCNF declaration -/ def toDecl (declName : Name) : CompilerM Decl := do @@ -101,9 +101,9 @@ def toDecl (declName : Name) : CompilerM Decl := do let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body) let value ← replaceUnsafeRecNames value let value ← macroInline value - /- Recall that some declarations tagged with `macroInline` contain matchers. -/ + /- Recall that some declarations tagged with `macro_inline` contain matchers. -/ let value ← inlineMatchers value - /- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macroInline]`. -/ + /- Recall that `inlineMatchers` may have exposed `ite`s and `dite`s which are tagged as `[macro_inline]`. -/ let value ← macroInline value /- Remark: we have disabled the following transformation, we will perform it at phase 2, after code specialization. diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index 32c7b60b98..e3aab073c9 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -129,7 +129,7 @@ partial def Code.toMono (code : Code) : ToMonoM Code := do else if let some info ← hasTrivialStructure? c.typeName then trivialStructToMono info c else - -- TODO: `casesOn` `[implementedBy]` support + -- TODO: `casesOn` `[implemented_by]` support let type ← toMonoType c.resultType let alts ← c.alts.mapM fun alt => match alt with @@ -170,4 +170,4 @@ def toMono : Pass where builtin_initialize registerTraceClass `Compiler.toMono (inherited := true) -end Lean.Compiler.LCNF \ No newline at end of file +end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/NeverExtractAttr.lean b/src/Lean/Compiler/NeverExtractAttr.lean index 9a185da074..7868c72a4c 100644 --- a/src/Lean/Compiler/NeverExtractAttr.lean +++ b/src/Lean/Compiler/NeverExtractAttr.lean @@ -9,7 +9,7 @@ import Lean.Attributes namespace Lean builtin_initialize neverExtractAttr : TagAttribute ← - registerTagAttribute `neverExtract "instruct the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, nor common subexpression should be performed. This is useful for declarations that have implicit effects." + registerTagAttribute `never_extract "instruct the compiler that function applications using the tagged declaration should not be extracted when they are closed terms, nor common subexpression should be performed. This is useful for declarations that have implicit effects." @[export lean_has_never_extract_attribute] partial def hasNeverExtractAttribute (env : Environment) (n : Name) : Bool := diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index d734281580..142491c2fc 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -17,7 +17,7 @@ namespace Lean.Elab.Term open Meta builtin_initialize elabWithoutExpectedTypeAttr : TagAttribute ← - registerTagAttribute `elabWithoutExpectedType "mark that applications of the given declaration should be elaborated without the expected type" + registerTagAttribute `elab_without_expected_type "mark that applications of the given declaration should be elaborated without the expected type" def hasElabWithoutExpectedType (env : Environment) (declName : Name) : Bool := elabWithoutExpectedTypeAttr.hasTag env declName @@ -637,7 +637,7 @@ end end ElabAppArgs builtin_initialize elabAsElim : TagAttribute ← - registerTagAttribute `elabAsElim + registerTagAttribute `elab_as_elim "instructs elaborator that the arguments of the function application should be elaborated as were an eliminator" fun declName => do let go : MetaM Unit := do diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 4ff7c4450e..c06fe78f8b 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -220,7 +220,7 @@ instance : MonadQuotation CommandElabM where withFreshMacroScope := Command.withFreshMacroScope unsafe def mkCommandElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute CommandElab) := - mkElabAttribute CommandElab `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" ref + mkElabAttribute CommandElab `builtin_command_elab `command_elab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command" ref @[implementedBy mkCommandElabAttributeUnsafe] opaque mkCommandElabAttribute (ref : Name) : IO (KeyedDeclsAttribute CommandElab) diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean index 0f8299e38d..552145c4a8 100644 --- a/src/Lean/Elab/ComputedFields.lean +++ b/src/Lean/Elab/ComputedFields.lean @@ -26,16 +26,16 @@ with ``` This file implements the computed fields feature by simulating it via -`implementedBy`. The main function is `setComputedFields`. +`implemented_by`. The main function is `setComputedFields`. -/ namespace Lean.Elab.ComputedFields open Meta builtin_initialize computedFieldAttr : TagAttribute ← - registerTagAttribute `computedField "Marks a function as a computed field of an inductive" fun _ => do + registerTagAttribute `computed_field "Marks a function as a computed field of an inductive" fun _ => do unless (← getOptions).getBool `elaboratingComputedFields do - throwError "The @[computedField] attribute can only be used in the with-block of an inductive" + throwError "The @[computed_field] attribute can only be used in the with-block of an inductive" def mkUnsafeCastTo (expectedType : Expr) (e : Expr) : MetaM Expr := mkAppOptM ``unsafeCast #[none, expectedType, e] @@ -188,7 +188,7 @@ def mkComputedFieldOverrides (declName : Name) (compFields : Array Name) : MetaM /-- Sets the computed fields for a block of mutual inductives, -adding the implementation via `implementedBy`. +adding the implementation via `implemented_by`. The `computedFields` argument contains a pair for every inductive in the mutual block, @@ -202,7 +202,7 @@ def setComputedFields (computedFields : Array (Name × Array Name)) : MetaM Unit logError m!"'{computedFieldName}' must be tagged with @[computedField]" mkComputedFieldOverrides indName computedFieldNames - -- Once all the implementedBy infrastructure is set up, compile everything. + -- Once all the implemented_by infrastructure is set up, compile everything. compileDecls <| computedFields.toList.map fun (indName, _) => mkCasesOnName indName ++ `_override diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index 699abf33d7..1b471f9e93 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -360,7 +360,7 @@ def elabMutual : CommandElab := fun stx => do if isAttribute (← getEnv) attrName then toErase := toErase.push attrName else - logErrorAt attrKindStx "unknown attribute [{attrName}]" + logErrorAt attrKindStx m!"unknown attribute [{attrName}]" else attrInsts := attrInsts.push attrKindStx let attrs ← elabAttrs attrInsts @@ -373,7 +373,7 @@ def elabMutual : CommandElab := fun stx => do @[builtinMacro Lean.Parser.Command.«initialize»] def expandInitialize : Macro | stx@`($declModifiers:declModifiers $kw:initializeKeyword $[$id? : $type? ←]? $doSeq) => do - let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtinInit + let attrId := mkIdentFrom stx <| if kw.raw[0].isToken "initialize" then `init else `builtin_init if let (some id, some type) := (id?, type?) then let `(Parser.Command.declModifiersT| $[$doc?:docComment]? $[@[$attrs?,*]]? $(vis?)? $[unsafe%$unsafe?]?) := stx[0] | Macro.throwErrorAt declModifiers "invalid initialization command, unexpected modifiers" diff --git a/src/Lean/Elab/Deriving/TypeName.lean b/src/Lean/Elab/Deriving/TypeName.lean index 17a0cc896a..2253090f6f 100644 --- a/src/Lean/Elab/Deriving/TypeName.lean +++ b/src/Lean/Elab/Deriving/TypeName.lean @@ -16,7 +16,7 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool throwError m!"{mkConst declName} has universe level parameters" elabCommand <| ← withFreshMacroScope `( unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName) - @[implementedBy instImpl] opaque inst : TypeName @$(mkCIdent declName) + @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName) instance : TypeName @$(mkCIdent declName) := inst ) return true diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index fab756a4ce..87582e3172 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -52,19 +52,19 @@ def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) | none => #[attr] if let some expId := expty? then if catName == `term then - `($[$doc?:docComment]? @[$(← mkAttrs `termElab),*] + `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*] aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab := fun stx expectedType? => Lean.Elab.Command.withExpectedType expectedType? fun $expId => match stx with $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax) else throwErrorAt expId "syntax category '{catName}' does not support expected type specification" else if catName == `term then - `($[$doc?:docComment]? @[$(← mkAttrs `termElab),*] + `($[$doc?:docComment]? @[$(← mkAttrs `term_elab),*] aux_def elabRules $(mkIdent k) : Lean.Elab.Term.TermElab := fun stx _ => match stx with $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax) else if catName == `command then - `($[$doc?:docComment]? @[$(← mkAttrs `commandElab),*] + `($[$doc?:docComment]? @[$(← mkAttrs `command_elab),*] aux_def elabRules $(mkIdent k) : Lean.Elab.Command.CommandElab := fun $alts:matchAlt* | _ => no_error_if_unused% throwUnsupportedSyntax) else if catName == `tactic then diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean index 61393813e3..a4d3464671 100644 --- a/src/Lean/Elab/InheritDoc.lean +++ b/src/Lean/Elab/InheritDoc.lean @@ -10,20 +10,20 @@ namespace Lean builtin_initialize registerBuiltinAttribute { - name := `inheritDoc + name := `inherit_doc descr := "inherit documentation from a specified declaration" add := fun decl stx kind => do unless kind == AttributeKind.global do - throwError "invalid `[inheritDoc]` attribute, must be global" + throwError "invalid `[inherit_doc]` attribute, must be global" match stx with - | `(attr| inheritDoc $[$id?:ident]?) => + | `(attr| inherit_doc $[$id?:ident]?) => let some id := id? - | throwError "invalid `[inheritDoc]` attribute, could not infer doc source" + | throwError "invalid `[inherit_doc]` attribute, could not infer doc source" let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id if (← findDocString? (← getEnv) decl).isSome then logWarningAt id m!"{← mkConstWithLevelParams decl} already has a doc string" let some doc ← findDocString? (← getEnv) declName | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string" addDocString decl doc - | _ => throwError "invalid `[inheritDoc]` attribute" + | _ => throwError "invalid `[inherit_doc]` attribute" } diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean index 072628dcfb..a25fe92e54 100644 --- a/src/Lean/Elab/Notation.lean +++ b/src/Lean/Elab/Notation.lean @@ -31,7 +31,7 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax | `($f:ident $_args*) | `($f:ident) => attrs.getElems.map fun stx => Unhygienic.run do if let `(attrInstance| $attr:ident) := stx then - if attr.getId.eraseMacroScopes == `inheritDoc then + if attr.getId.eraseMacroScopes == `inherit_doc then return ← `(attrInstance| $attr:ident $f:ident) pure ⟨stx⟩ | _ => attrs @@ -106,7 +106,7 @@ def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Ma -- The reference is attached to the syntactic representation of the called function itself, not the entire function application let lhs ← `($$f:ident) let lhs := Syntax.mkApp lhs (.mk args) - `(@[$attrKind appUnexpander $(mkIdent c)] + `(@[$attrKind app_unexpander $(mkIdent c)] aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun | `($lhs) => withRef f `($pat) -- must be a separate case as the LHS and RHS above might not be `app` nodes diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 3dabeae54c..462407dc77 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -24,7 +24,7 @@ abbrev PatternVar := Syntax -- TODO: should be `Ident` Macros occurring in patterns are expanded before the `collectPatternVars` method is executed. The following kinds of Syntax are handled by this module - Constructor applications - - Applications of functions tagged with the `[matchPattern]` attribute + - Applications of functions tagged with the `[match_pattern]` attribute - Identifiers - Anonymous constructors - Structure instances @@ -47,7 +47,7 @@ structure State where abbrev M := StateRefT State TermElabM private def throwCtorExpected {α} : M α := - throwError "invalid pattern, constructor or constant marked with '[matchPattern]' expected" + throwError "invalid pattern, constructor or constant marked with '[match_pattern]' expected" private def throwInvalidPattern {α} : M α := throwError "invalid pattern" @@ -58,7 +58,7 @@ An application in a pattern can be 1- A constructor application The elaborator assumes fields are accessible and inductive parameters are not accessible. -2- A regular application `(f ...)` where `f` is tagged with `[matchPattern]`. +2- A regular application `(f ...)` where `f` is tagged with `[match_pattern]`. The elaborator assumes implicit arguments are not accessible and explicit ones are accessible. -/ @@ -90,7 +90,7 @@ private def isNextArgAccessible (ctx : Context) : Bool := | some ctorVal => i ≥ ctorVal.numParams -- For constructor applications only fields are accessible | none => if h : i < ctx.paramDecls.size then - -- For `[matchPattern]` applications, only explicit parameters are accessible. + -- For `[match_pattern]` applications, only explicit parameters are accessible. let d := ctx.paramDecls.get ⟨i, h⟩ d.2.isExplicit else @@ -235,7 +235,7 @@ where processCtor (stx : Syntax) : M Syntax := do processCtorAppCore stx #[] #[] false - /-- Check whether `stx` is a pattern variable or constructor-like (i.e., constructor or constant tagged with `[matchPattern]` attribute) -/ + /-- Check whether `stx` is a pattern variable or constructor-like (i.e., constructor or constant tagged with `[match_pattern]` attribute) -/ processId (stx : Syntax) : M Syntax := do match (← resolveId? stx "pattern") with | none => processVar stx diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index 3e44fc9061..aeaecd46a6 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/src/Lean/Elab/Quotation/Precheck.lean @@ -38,11 +38,11 @@ register_builtin_option quotPrecheck.allowSectionVars : Bool := { unsafe def mkPrecheckAttribute : IO (KeyedDeclsAttribute Precheck) := KeyedDeclsAttribute.init { - builtinName := `builtinQuotPrecheck, - name := `quotPrecheck, + builtinName := `builtin_quot_precheck, + name := `quot_precheck, descr := "Register a double backtick syntax quotation pre-check. -[quotPrecheck k] registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the `SyntaxNodeKind` `k`. +[quot_precheck k] registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the `SyntaxNodeKind` `k`. It should implement eager name analysis on the passed syntax by throwing an exception on unbound identifiers, and calling `precheck` recursively on nested terms, potentially with an extended local context (`withNewLocal`). Macros without registered precheck hook are unfolded, and identifier-less syntax is ultimately assumed to be well-formed.", @@ -61,7 +61,7 @@ partial def precheck : Precheck := fun stx => do if let some stx' ← liftMacroM <| expandMacro? stx then precheck stx' return - throwErrorAt stx "no macro or `[quotPrecheck]` instance for syntax kind '{stx.getKind}' found{indentD stx} + throwErrorAt stx "no macro or `[quot_precheck]` instance for syntax kind '{stx.getKind}' found{indentD stx} This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check." where hasQuotedIdent diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index b499f4d223..40fc670a6f 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -251,7 +251,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d let quotSymbol := "`(" ++ suffix ++ "|" let name := catName ++ `quot let cmd ← `( - @[termParser] def $(mkIdent name) : Lean.ParserDescr := + @[term_parser] def $(mkIdent name) : Lean.ParserDescr := Lean.ParserDescr.node `Lean.Parser.Term.quot $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.node $(quote name) $(quote Lean.Parser.maxPrec) (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) @@ -270,7 +270,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d Parser.LeadingIdentBehavior.both else Parser.LeadingIdentBehavior.symbol - let attrName := catName.appendAfter "Parser" + let attrName := catName.appendAfter "_parser" let catDeclName := ``Lean.Parser.Category ++ catName setEnv (← Parser.registerParserCategory (← getEnv) attrName catName catBehavior catDeclName) let cmd ← `($[$docString?]? def $(mkIdentFrom stx[2] (`_root_ ++ catDeclName) (canonical := true)) : Lean.Parser.Category := {}) @@ -353,7 +353,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do let prio ← liftMacroM <| evalOptPrio prio? let idRef := (name?.map (·.raw)).getD tk let stxNodeKind := (← getCurrNamespace) ++ name - let catParserId := mkIdentFrom idRef (cat.appendAfter "Parser") + let catParserId := mkIdentFrom idRef (cat.appendAfter "_parser") let (val, lhsPrec?) ← runTermElabM fun _ => Term.toParserDescr syntaxParser cat let declName := name?.getD (mkIdentFrom idRef name (canonical := true)) let attrInstance ← `(attrInstance| $attrKind:attrKind $catParserId:ident $(quote prio):num) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 7f51f629c4..e71788181e 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -103,7 +103,7 @@ protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Cor protected def getMainModule : TacticM Name := do pure (← getEnv).mainModule unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) := - mkElabAttribute Tactic `builtinTactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" `Lean.Elab.Tactic.tacticElabAttribute + mkElabAttribute Tactic `builtin_tactic `tactic `Lean.Parser.Tactic `Lean.Elab.Tactic.Tactic "tactic" `Lean.Elab.Tactic.tacticElabAttribute @[builtinInit mkTacticAttribute] opaque tacticElabAttribute : KeyedDeclsAttribute Tactic diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 0bdcd91df2..503a342b86 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -369,7 +369,7 @@ def withoutSavingRecAppSyntax (x : TermElabM α) : TermElabM α := withReader (fun ctx => { ctx with saveRecAppSyntax := false }) x unsafe def mkTermElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute TermElab) := - mkElabAttribute TermElab `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" ref + mkElabAttribute TermElab `builtin_term_elab `term_elab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" ref @[implementedBy mkTermElabAttributeUnsafe] opaque mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab) diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index a7e9387a48..0ca9269cd5 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -119,7 +119,7 @@ unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespa } attrDeclName unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro) := - mkElabAttribute Macro `builtinMacro `macro Name.anonymous `Lean.Macro "macro" ref + mkElabAttribute Macro `builtin_macro `macro Name.anonymous `Lean.Macro "macro" ref @[implementedBy mkMacroAttributeUnsafe] opaque mkMacroAttribute (ref : Name) : IO (KeyedDeclsAttribute Macro) diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index d6dccb9dc9..79b2a58157 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -27,9 +27,9 @@ abbrev Key := Name Important: `mkConst valueTypeName` and `γ` must be definitionally equal. -/ structure Def (γ : Type) where - /-- Builtin attribute name, if any (e.g., `builtinTermElab) -/ + /-- Builtin attribute name, if any (e.g., `builtin_term_elab) -/ builtinName : Name := Name.anonymous - /-- Attribute name (e.g., `termElab) -/ + /-- Attribute name (e.g., `term_elab) -/ name : Name /-- Attribute description -/ descr : String diff --git a/src/Lean/Linter/Builtin.lean b/src/Lean/Linter/Builtin.lean index e1f10a05cf..eb9d469ba0 100644 --- a/src/Lean/Linter/Builtin.lean +++ b/src/Lean/Linter/Builtin.lean @@ -13,10 +13,10 @@ def suspiciousUnexpanderPatterns : Linter := fun cmdStx => do unless getLinterSuspiciousUnexpanderPatterns (← getOptions) do return - -- check `[appUnexpander _]` defs defined by pattern matching + -- check `[app_unexpander _]` defs defined by pattern matching let `($[$_:docComment]? @[$[$attrs:attr],*] $(_vis)? def $_ : $_ $[| $pats => $_]*) := cmdStx | return - unless attrs.any (· matches `(attr| appUnexpander $_)) do + unless attrs.any (· matches `(attr| app_unexpander $_)) do return for pat in pats do diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index ed129e66bd..0c151d8ecf 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -96,8 +96,8 @@ builtin_initialize else setEnv <| missingDocsExt.addEntry env (declName, key, ← mkHandler declName) } - mkAttr true `builtinMissingDocsHandler - mkAttr false `missingDocsHandler + mkAttr true `builtin_missing_docs_handler + mkAttr false `missing_docs_handler def lint (stx : Syntax) (msg : String) : CommandElabM Unit := logLint linter.missingDocs stx m!"missing doc string for {msg}" @@ -114,7 +114,7 @@ def lintStructField (parent stx : Syntax) (msg : String) : CommandElabM Unit := def hasInheritDoc (attrs : Syntax) : Bool := attrs[0][1].getSepArgs.any fun attr => attr[1].isOfKind ``Parser.Attr.simple && - attr[1][0].getId.eraseMacroScopes == `inheritDoc + attr[1][0].getId.eraseMacroScopes == `inherit_doc def declModifiersPubNoDoc (mods : Syntax) : Bool := mods[2][0].getKind != ``«private» && mods[0].isNone && !hasInheritDoc mods[1] diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 1cae988271..c287efa153 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -67,7 +67,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ => stx.isOfKind ``Lean.Parser.Command.declSig) && (stack.get? 5 |>.any fun (stx, _) => match stx[0] with | `(Lean.Parser.Command.declModifiersT| $[$_:docComment]? @[$[$attrs:attr],*] $[$vis]? $[noncomputable]?) => - attrs.any (fun attr => attr.raw.isOfKind ``Parser.Attr.extern || attr matches `(attr| implementedBy $_)) + attrs.any (fun attr => attr.raw.isOfKind ``Parser.Attr.extern || attr matches `(attr| implemented_by $_)) | _ => false)) -- is in dependent arrow @@ -110,13 +110,13 @@ builtin_initialize unusedVariablesIgnoreFnsExt : SimplePersistentEnvExtension Na builtin_initialize registerBuiltinAttribute { - name := `unusedVariablesIgnoreFn + name := `unused_variables_ignore_fn descr := "Marks a function of type `Lean.Linter.IgnoreFunction` for suppressing unused variable warnings" add := fun decl stx kind => do Attribute.Builtin.ensureNoArgs stx - unless kind == AttributeKind.global do throwError "invalid attribute 'unusedVariablesIgnoreFn', must be global" + unless kind == AttributeKind.global do throwError "invalid attribute 'unused_variables_ignore_fn', must be global" unless (← getConstInfo decl).type.isConstOf ``IgnoreFunction do - throwError "invalid attribute 'unusedVariablesIgnoreFn', must be of type `Lean.Linter.IgnoreFunction`" + throwError "invalid attribute 'unused_variables_ignore_fn', must be of type `Lean.Linter.IgnoreFunction`" let env ← getEnv setEnv <| unusedVariablesIgnoreFnsExt.addEntry env decl } diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index f3bb6a2d15..149baa4750 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -123,11 +123,11 @@ def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do builtin_initialize registerBuiltinAttribute { - name := `defaultInstance + name := `default_instance descr := "type class default instance" add := fun declName stx kind => do let prio ← getAttrParamOptPrio stx[1] - unless kind == AttributeKind.global do throwError "invalid attribute 'defaultInstance', must be global" + unless kind == AttributeKind.global do throwError "invalid attribute 'default_instance', must be global" discard <| addDefaultInstance declName prio |>.run {} {} } diff --git a/src/Lean/Meta/Match/MatchPatternAttr.lean b/src/Lean/Meta/Match/MatchPatternAttr.lean index bd5367b4e3..fb6044fb41 100644 --- a/src/Lean/Meta/Match/MatchPatternAttr.lean +++ b/src/Lean/Meta/Match/MatchPatternAttr.lean @@ -8,7 +8,7 @@ import Lean.Attributes namespace Lean builtin_initialize matchPatternAttr : TagAttribute ← - registerTagAttribute `matchPattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)" + registerTagAttribute `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)" @[export lean_has_match_pattern_attribute] def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool := diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 6b2940cef4..19d37e2a5f 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -30,7 +30,7 @@ def getMaxHeartbeats (opts : Options) : Nat := synthInstance.maxHeartbeats.get opts * 1000 builtin_initialize inferTCGoalsRLAttr : TagAttribute ← - registerTagAttribute `inferTCGoalsRL "instruct type class resolution procedure to solve goals from right to left for this instance" + registerTagAttribute `infer_tc_goals_rl "instruct type class resolution procedure to solve goals from right to left for this instance" def hasInferTCGoalsRLAttribute (env : Environment) (constName : Name) : Bool := inferTCGoalsRLAttr.hasTag env constName diff --git a/src/Lean/Meta/UnificationHint.lean b/src/Lean/Meta/UnificationHint.lean index 6fb958b229..9d2a8384f8 100644 --- a/src/Lean/Meta/UnificationHint.lean +++ b/src/Lean/Meta/UnificationHint.lean @@ -80,7 +80,7 @@ def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit := builtin_initialize registerBuiltinAttribute { - name := `unificationHint + name := `unification_hint descr := "unification hint" add := fun declName stx kind => do Attribute.Builtin.ensureNoArgs stx diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean index e34be60fb3..6a1044a4e5 100644 --- a/src/Lean/Parser/Attr.lean +++ b/src/Lean/Parser/Attr.lean @@ -9,12 +9,12 @@ import Lean.Parser.Extra namespace Lean.Parser builtin_initialize - registerBuiltinParserAttribute `builtinPrioParser ``Category.prio .both - registerBuiltinDynamicParserAttribute `prioParser `prio + registerBuiltinParserAttribute `builtin_prio_parser ``Category.prio .both + registerBuiltinDynamicParserAttribute `prio_parser `prio builtin_initialize - registerBuiltinParserAttribute `builtinAttrParser ``Category.attr .symbol - registerBuiltinDynamicParserAttribute `attrParser `attr + registerBuiltinParserAttribute `builtin_attr_parser ``Category.attr .symbol + registerBuiltinDynamicParserAttribute `attr_parser `attr @[inline] def priorityParser (rbp : Nat := 0) : Parser := categoryParser `prio rbp @@ -38,11 +38,11 @@ namespace Attr @[builtinAttrParser] def «export» := leading_parser "export " >> ident /- We don't use `simple` for recursor because the argument is not a priority -/ -@[builtinAttrParser] def recursor := leading_parser nonReservedSymbol "recursor " >> numLit -@[builtinAttrParser] def «class» := leading_parser "class" -@[builtinAttrParser] def «instance» := leading_parser "instance" >> optional priorityParser -@[builtinAttrParser] def defaultInstance := leading_parser nonReservedSymbol "defaultInstance " >> optional priorityParser -@[builtinAttrParser] def «specialize» := leading_parser (nonReservedSymbol "specialize") >> many (ident <|> numLit) +@[builtinAttrParser] def recursor := leading_parser nonReservedSymbol "recursor " >> numLit +@[builtinAttrParser] def «class» := leading_parser "class" +@[builtinAttrParser] def «instance» := leading_parser "instance" >> optional priorityParser +@[builtinAttrParser] def default_instance := leading_parser nonReservedSymbol "default_instance " >> optional priorityParser +@[builtinAttrParser] def «specialize» := leading_parser (nonReservedSymbol "specialize") >> many (ident <|> numLit) def externEntry := leading_parser optional ident >> optional (nonReservedSymbol "inline ") >> strLit @[builtinAttrParser] def extern := leading_parser nonReservedSymbol "extern " >> optional numLit >> many externEntry diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 3de10b9d8e..202124b462 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -8,8 +8,8 @@ import Lean.Parser.Term namespace Lean namespace Parser -builtin_initialize registerBuiltinParserAttribute `builtinDoElemParser ``Category.doElem -builtin_initialize registerBuiltinDynamicParserAttribute `doElemParser `doElem +builtin_initialize registerBuiltinParserAttribute `builtin_doElem_parser ``Category.doElem +builtin_initialize registerBuiltinDynamicParserAttribute `doElem_parser `doElem @[inline] def doElemParser (rbp : Nat := 0) : Parser := categoryParser `doElem rbp diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 424ebdc74e..6d5611281e 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -313,7 +313,7 @@ def runParserAttributeHooks (catName : Name) (declName : Name) (builtin : Bool) builtin_initialize registerBuiltinAttribute { - name := `runBuiltinParserAttributeHooks + name := `run_builtin_parser_attribute_hooks descr := "explicitly run hooks normally activated by builtin parser attributes" add := fun decl stx _ => do Attribute.Builtin.ensureNoArgs stx @@ -322,7 +322,7 @@ builtin_initialize builtin_initialize registerBuiltinAttribute { - name := `runParserAttributeHooks + name := `run_parser_attribute_hooks descr := "explicitly run hooks normally activated by parser attributes" add := fun decl stx _ => do Attribute.Builtin.ensureNoArgs stx @@ -564,16 +564,16 @@ def registerParserCategory (env : Environment) (attrName catName : Name) let env ← IO.ofExcept $ addParserCategory env catName ref behavior registerAttributeOfBuilder env `parserAttr ref [DataValue.ofName attrName, DataValue.ofName catName] --- declare `termParser` here since it is used everywhere via antiquotations +-- declare `term_parser` here since it is used everywhere via antiquotations -builtin_initialize registerBuiltinParserAttribute `builtinTermParser ``Category.term +builtin_initialize registerBuiltinParserAttribute `builtin_term_parser ``Category.term -builtin_initialize registerBuiltinDynamicParserAttribute `termParser `term +builtin_initialize registerBuiltinDynamicParserAttribute `term_parser `term --- declare `commandParser` to break cyclic dependency -builtin_initialize registerBuiltinParserAttribute `builtinCommandParser ``Category.command +-- declare `command_parser` to break cyclic dependency +builtin_initialize registerBuiltinParserAttribute `builtin_command_parser ``Category.command -builtin_initialize registerBuiltinDynamicParserAttribute `commandParser `command +builtin_initialize registerBuiltinDynamicParserAttribute `command_parser `command @[inline] def commandParser (rbp : Nat := 0) : Parser := categoryParser `command rbp diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean index a23b5de1a2..f2e93bc836 100644 --- a/src/Lean/Parser/Level.lean +++ b/src/Lean/Parser/Level.lean @@ -9,7 +9,7 @@ namespace Lean namespace Parser builtin_initialize - registerBuiltinParserAttribute `builtinLevelParser ``Category.level + registerBuiltinParserAttribute `builtin_level_parser ``Category.level @[inline] def levelParser (rbp : Nat := 0) : Parser := categoryParser `level rbp diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 1a9fb66df2..e5a96fc3f5 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -9,12 +9,12 @@ namespace Lean namespace Parser builtin_initialize - registerBuiltinParserAttribute `builtinSyntaxParser ``Category.stx .both - registerBuiltinDynamicParserAttribute `stxParser `stx + registerBuiltinParserAttribute `builtin_syntax_parser ``Category.stx .both + registerBuiltinDynamicParserAttribute `stx_parser `stx builtin_initialize - registerBuiltinParserAttribute `builtinPrecParser ``Category.prec .both - registerBuiltinDynamicParserAttribute `precParser `prec + registerBuiltinParserAttribute `builtin_prec_parser ``Category.prec .both + registerBuiltinDynamicParserAttribute `prec_parser `prec @[inline] def precedenceParser (rbp : Nat := 0) : Parser := categoryParser `prec rbp diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 21a2643716..8e138893c4 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -20,8 +20,8 @@ def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> p end Command builtin_initialize - registerBuiltinParserAttribute `builtinTacticParser ``Category.tactic .both - registerBuiltinDynamicParserAttribute `tacticParser `tactic + registerBuiltinParserAttribute `builtin_tactic_parser ``Category.tactic .both + registerBuiltinDynamicParserAttribute `tactic_parser `tactic @[inline] def tacticParser (rbp : Nat := 0) : Parser := categoryParser `tactic rbp diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 2811a8386d..1128960b99 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -88,7 +88,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do let some value ← pure cinfo.value? | throwError "don't know how to generate {ctx.varName} for non-definition '{e}'" unless (env.getModuleIdxFor? c).isNone || force do - throwError "refusing to generate code for imported parser declaration '{c}'; use `@[runParserAttributeHooks]` on its definition instead." + throwError "refusing to generate code for imported parser declaration '{c}'; use `@[run_parser_attribute_hooks]` on its definition instead." let value ← compileParserExpr <| replaceParserTy ctx value let ty ← forallTelescope cinfo.type fun params _ => params.foldrM (init := mkConst ctx.tyName) fun param ty => do @@ -147,7 +147,7 @@ unsafe def registerParserCompiler {α} (ctx : Context α) : IO Unit := do evalConstCheck TrailingParserDescr `Lean.TrailingParserDescr constName compileEmbeddedParsers ctx d (builtin := builtin) |>.run' else - -- `[runBuiltinParserAttributeHooks]` => force compilation even if imported, do not apply `ctx.categoryAttr`. + -- `[run_builtin_parser_attribute_hooks]` => force compilation even if imported, do not apply `ctx.categoryAttr`. let force := catName.isAnonymous discard (compileParserExpr ctx (mkConst constName) (builtin := builtin) (force := force)).run' } diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 619fe11461..f1f9a0ef46 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -95,7 +95,7 @@ instance : MonadQuotation DelabM := { unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) := KeyedDeclsAttribute.init { - builtinName := `builtinDelab, + builtinName := `builtin_delab, name := `delab, descr := "Register a delaborator. @@ -253,10 +253,10 @@ partial def delab : Delab := do unsafe def mkAppUnexpanderAttribute : IO (KeyedDeclsAttribute Unexpander) := KeyedDeclsAttribute.init { - name := `appUnexpander, + name := `app_unexpander, descr := "Register an unexpander for applications of a given constant. -[appUnexpander c] registers a `Lean.PrettyPrinter.Unexpander` for applications of the constant `c`. The unexpander is +[app_unexpander c] registers a `Lean.PrettyPrinter.Unexpander` for applications of the constant `c`. The unexpander is passed the result of pre-pretty printing the application *without* implicitly passed arguments. If `pp.explicit` is set to true or `pp.notation` is set to false, it will not be called at all.", valueTypeName := `Lean.PrettyPrinter.Unexpander diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index d570549d33..284d52b02d 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -57,7 +57,7 @@ abbrev Formatter := FormatterM Unit unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) := KeyedDeclsAttribute.init { - builtinName := `builtinFormatter, + builtinName := `builtin_formatter, name := `formatter, descr := "Register a formatter for a parser. @@ -75,10 +75,10 @@ unsafe def mkFormatterAttribute : IO (KeyedDeclsAttribute Formatter) := unsafe def mkCombinatorFormatterAttribute : IO ParserCompiler.CombinatorAttribute := ParserCompiler.registerCombinatorAttribute - `combinatorFormatter + `combinator_formatter "Register a formatter for a parser combinator. - [combinatorFormatter c] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `Parser` declaration `c`. + [combinator_formatter c] registers a declaration of type `Lean.PrettyPrinter.Formatter` for the `Parser` declaration `c`. Note that, unlike with [formatter], this is not a node kind since combinators usually do not introduce their own node kinds. The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced with `Formatter` in the parameter types." diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 6e2ceb910d..2e284b9051 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -112,7 +112,7 @@ instance : OrElse (ParenthesizerM α) := ⟨ParenthesizerM.orElse⟩ unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) := KeyedDeclsAttribute.init { - builtinName := `builtinParenthesizer, + builtinName := `builtin_parenthesizer, name := `parenthesizer, descr := "Register a parenthesizer for a parser. @@ -132,11 +132,11 @@ abbrev CategoryParenthesizer := (prec : Nat) → Parenthesizer unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryParenthesizer) := KeyedDeclsAttribute.init { - builtinName := `builtinCategoryParenthesizer, - name := `categoryParenthesizer, + builtinName := `builtin_category_parenthesizer, + name := `category_parenthesizer, descr := "Register a parenthesizer for a syntax category. - [categoryParenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`, + [category_parenthesizer cat] registers a declaration of type `Lean.PrettyPrinter.CategoryParenthesizer` for the category `cat`, which is used when parenthesizing calls of `categoryParser cat prec`. Implementations should call `maybeParenthesize` with the precedence and `cat`. If no category parenthesizer is registered, the category will never be parenthesized, but still be traversed for parenthesizing nested categories.", @@ -145,16 +145,16 @@ unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryPa let env ← getEnv let id ← Attribute.Builtin.getId stx if Parser.isParserCategory env id then pure id - else throwError "invalid [categoryParenthesizer] argument, unknown parser category '{toString id}'" + else throwError "invalid [category_parenthesizer] argument, unknown parser category '{toString id}'" } `Lean.PrettyPrinter.categoryParenthesizerAttribute @[builtinInit mkCategoryParenthesizerAttribute] opaque categoryParenthesizerAttribute : KeyedDeclsAttribute CategoryParenthesizer unsafe def mkCombinatorParenthesizerAttribute : IO ParserCompiler.CombinatorAttribute := ParserCompiler.registerCombinatorAttribute - `combinatorParenthesizer + `combinator_parenthesizer "Register a parenthesizer for a parser combinator. - [combinatorParenthesizer c] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `Parser` declaration `c`. + [combinator_parenthesizer c] registers a declaration of type `Lean.PrettyPrinter.Parenthesizer` for the `Parser` declaration `c`. Note that, unlike with [parenthesizer], this is not a node kind since combinators usually do not introduce their own node kinds. The tagged declaration may optionally accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced with `Parenthesizer` in the parameter types." diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 6aaad08984..01d7649435 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -126,7 +126,7 @@ def registerRpcProcedure (method : Name) : CoreM Unit := do setEnv <| userRpcProcedures.insert (← getEnv) method wrappedName builtin_initialize registerBuiltinAttribute { - name := `serverRpcMethod + name := `server_rpc_method descr := "Marks a function as a Lean server RPC method. Shorthand for `registerRpcProcedure`. The function must have type `α → RequestM (RequestTask β)` with diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index 7d99d265d1..01569e1bf4 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -377,13 +377,13 @@ class erase_irrelevant_fn { } else if (optional n = get_implemented_by_attribute(env(), fn)) { if (is_cases_on_recursor(env(), fn) || has_inline_attribute(env(), *n)) { // casesOn has a different representation in the LCNF than applications, - // so we can't just replace the constant by the implementedBy override. + // so we can't just replace the constant by the implemented_by override. // Additionally, csimp ignores inline annotation after erase so inline now. expr e2 = mk_app(mk_const(mk_cstage1_name(*n), const_levels(f)), to_list(args)); if (optional e3 = unfold_app(env(), e2)) { return visit(*e3); } else { - throw exception(sstream() << "code generation failed, unsupported implementedBy for '" << fn << "'"); + throw exception(sstream() << "code generation failed, unsupported implemented_by for '" << fn << "'"); } } else { f = mk_const(*n, const_levels(f)); diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp index 551fb41f55..66fe766585 100644 --- a/src/library/compiler/ir.cpp +++ b/src/library/compiler/ir.cpp @@ -499,7 +499,7 @@ public: if (optional attr = get_extern_attr_data(env(), fn)) { return ir::mk_extern_decl(fn, xs, result_type, *attr); } else { - // Hack: `fn` is marked with `implementedBy` or `init` + // Hack: `fn` is marked with `implemented_by` or `init` return ir::mk_dummy_extern_decl(fn, xs, result_type); } } diff --git a/tests/compiler/StackOverflow.lean b/tests/compiler/StackOverflow.lean index e495adbe68..9a0468e7cb 100644 --- a/tests/compiler/StackOverflow.lean +++ b/tests/compiler/StackOverflow.lean @@ -1,3 +1,3 @@ partial def foo : Nat → Nat | n => foo n + 1 -@[neverExtract] +@[never_extract] def main : IO Unit := IO.println $ foo 0 diff --git a/tests/compiler/StackOverflowTask.lean b/tests/compiler/StackOverflowTask.lean index cbbc961cba..87e7ab9dde 100644 --- a/tests/compiler/StackOverflowTask.lean +++ b/tests/compiler/StackOverflowTask.lean @@ -1,3 +1,3 @@ partial def foo : Nat → Nat | n => foo n + 1 -@[neverExtract] +@[never_extract] def main : IO Unit := IO.println $ Task.get $ Task.spawn fun _ => foo 0 diff --git a/tests/compiler/computedFieldsExtern.lean b/tests/compiler/computedFieldsExtern.lean index b8898dd683..0be4797b8d 100644 --- a/tests/compiler/computedFieldsExtern.lean +++ b/tests/compiler/computedFieldsExtern.lean @@ -2,7 +2,7 @@ inductive Exp | var (i : Nat) | app (a b : Exp) with - @[computedField, extern c inline "(lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*)) + 40)"] + @[computed_field, extern c inline "(lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*)) + 40)"] hash : Exp → UInt64 | .var i => Hashable.hash i | .app a b => a.hash + b.hash diff --git a/tests/lean/1007.lean b/tests/lean/1007.lean index 2ea5230f4f..1f3c28d6f6 100644 --- a/tests/lean/1007.lean +++ b/tests/lean/1007.lean @@ -30,7 +30,7 @@ class SemiInner (X : Type u) (R : Type v) where class SemiHilbert (X) (R : Type u) [Vec R] extends Vec X, SemiInner X R -@[inferTCGoalsRL] +@[infer_tc_goals_rl] instance (X R) [Trait X] [Vec R] [SemiHilbert X R] (ι : Type v) : SemiHilbert (ι → X) R := sorry instance : SemiHilbert ℝ ℝ := sorry diff --git a/tests/lean/1021.lean.expected.out b/tests/lean/1021.lean.expected.out index fa65c2e4f5..12fdf9d22a 100644 --- a/tests/lean/1021.lean.expected.out +++ b/tests/lean/1021.lean.expected.out @@ -1,8 +1,8 @@ -some { range := { pos := { line := 128, column := 41 }, - charUtf16 := 41, +some { range := { pos := { line := 128, column := 42 }, + charUtf16 := 42, endPos := { line := 134, column := 31 }, endCharUtf16 := 31 }, - selectionRange := { pos := { line := 128, column := 45 }, - charUtf16 := 45, - endPos := { line := 128, column := 57 }, - endCharUtf16 := 57 } } + selectionRange := { pos := { line := 128, column := 46 }, + charUtf16 := 46, + endPos := { line := 128, column := 58 }, + endCharUtf16 := 58 } } diff --git a/tests/lean/1039.lean b/tests/lean/1039.lean index e158c6225c..345f10eca7 100644 --- a/tests/lean/1039.lean +++ b/tests/lean/1039.lean @@ -21,7 +21,7 @@ namespace Something namespace MyNamespace -@[local commandElab Lean.Parser.Command.end] def elabEnd' : CommandElab := fun stx => +@[local command_elab Lean.Parser.Command.end] def elabEnd' : CommandElab := fun stx => match stx with | `(end $id:ident) => do println!"boo" diff --git a/tests/lean/1298.lean b/tests/lean/1298.lean index 26c885dc49..9c9848623c 100644 --- a/tests/lean/1298.lean +++ b/tests/lean/1298.lean @@ -6,7 +6,7 @@ instance [Semiring R] : OfNat R n where def Nat.cast [Semiring R] (n : Nat) : R := let _ := n = n; Semiring.zero -@[defaultInstance high] instance [Semiring R] : HPow R Nat R := inferInstance +@[default_instance high] instance [Semiring R] : HPow R Nat R := inferInstance instance [Semiring R] : CoeTail Nat R where coe n := n.cast diff --git a/tests/lean/1363.lean b/tests/lean/1363.lean index 543a6db5e9..8fe0cd2165 100644 --- a/tests/lean/1363.lean +++ b/tests/lean/1363.lean @@ -1,24 +1,24 @@ import Lean.Data.Parsec open Lean Parsec -@[macroInline] -- Error +@[macro_inline] -- Error def f : Nat → Nat | 0 => 0 | n + 1 => f n -@[macroInline] -- Error +@[macro_inline] -- Error def g : Nat → Nat | 0 => 0 | n + 1 => g n termination_by g x => x -@[macroInline] -- Error +@[macro_inline] -- Error def h : Nat → Nat → Nat | 0, _ => 0 | n + 1, m => h n m termination_by h x y => x -@[macroInline] -- Error +@[macro_inline] -- Error partial def skipMany (p : Parsec α) (it : String.Iterator) : Parsec PUnit := do match p it with | .success it _ => skipMany p it diff --git a/tests/lean/1363.lean.expected.out b/tests/lean/1363.lean.expected.out index b9c1a7cad7..65f8ff7f6d 100644 --- a/tests/lean/1363.lean.expected.out +++ b/tests/lean/1363.lean.expected.out @@ -1,5 +1,5 @@ -1363.lean:4:2-4:13: error: invalid use of `[macro_inline]` attribute at `f`, it is not supported in this kind of declaration, declaration must be a non-recursive definition -1363.lean:9:2-9:13: error: invalid use of `[macro_inline]` attribute at `g`, it is not supported in this kind of declaration, declaration must be a non-recursive definition -1363.lean:15:2-15:13: error: invalid use of `[macro_inline]` attribute at `h._unary`, it is not supported in this kind of declaration, declaration must be a non-recursive definition -1363.lean:15:2-15:13: error: invalid use of `[macro_inline]` attribute at `h`, it is not supported in this kind of declaration, declaration must be a non-recursive definition -1363.lean:21:2-21:13: error: invalid use of `[macro_inline]` attribute at `skipMany`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:4:2-4:14: error: invalid use of `[macro_inline]` attribute at `f`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:9:2-9:14: error: invalid use of `[macro_inline]` attribute at `g`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:15:2-15:14: error: invalid use of `[macro_inline]` attribute at `h._unary`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:15:2-15:14: error: invalid use of `[macro_inline]` attribute at `h`, it is not supported in this kind of declaration, declaration must be a non-recursive definition +1363.lean:21:2-21:14: error: invalid use of `[macro_inline]` attribute at `skipMany`, it is not supported in this kind of declaration, declaration must be a non-recursive definition diff --git a/tests/lean/1657.lean b/tests/lean/1657.lean index ff753d0b0f..51f008bcc1 100644 --- a/tests/lean/1657.lean +++ b/tests/lean/1657.lean @@ -11,7 +11,7 @@ def natrec_int {C} (n: Option Nat) -- ERROR := n.bind (λn => natrec_inner n z s) -@[inlineIfReduce] +@[inline_if_reduce] def foo (xs : List Nat) := match xs with | [] => 0 diff --git a/tests/lean/1657.lean.expected.out b/tests/lean/1657.lean.expected.out index ed8cbc34bd..fd1d8d9be1 100644 --- a/tests/lean/1657.lean.expected.out +++ b/tests/lean/1657.lean.expected.out @@ -1 +1 @@ -1657.lean:20:4-20:9: error: function `foo` has been recursively inlined more than #16, consider removing the attribute `[inlineIfReduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce ` +1657.lean:20:4-20:9: error: function `foo` has been recursively inlined more than #16, consider removing the attribute `[inline_if_reduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce ` diff --git a/tests/lean/248.lean b/tests/lean/248.lean index ee79549664..4cdb5193be 100644 --- a/tests/lean/248.lean +++ b/tests/lean/248.lean @@ -1 +1 @@ -@[implementedBy foo] opaque foo (x : Nat) : Nat +@[implemented_by foo] opaque foo (x : Nat) : Nat diff --git a/tests/lean/248.lean.expected.out b/tests/lean/248.lean.expected.out index 2444eeee1a..467c482161 100644 --- a/tests/lean/248.lean.expected.out +++ b/tests/lean/248.lean.expected.out @@ -1 +1 @@ -248.lean:1:2-1:19: error: invalid 'implementedBy' argument 'foo', function cannot be implemented by itself +248.lean:1:2-1:20: error: invalid 'implemented_by' argument 'foo', function cannot be implemented by itself diff --git a/tests/lean/353.lean b/tests/lean/353.lean index bc3ffd78ef..d98ee9b01d 100644 --- a/tests/lean/353.lean +++ b/tests/lean/353.lean @@ -3,7 +3,7 @@ class ArrSort (α : Sort u1) where class Arr (α : Sort u1) (γ : Sort u2) where Arr : α → α → γ infix:70 " ~> " => Arr.Arr -@[defaultInstance] +@[default_instance] instance inst1 {α : Sort _} [ArrSort α] : Arr α (Sort _) := { Arr := ArrSort.Arr } instance inst2 : ArrSort Prop := { Arr := λ a b => a → b } diff --git a/tests/lean/625.lean b/tests/lean/625.lean index b40c72c613..40cc37780e 100644 --- a/tests/lean/625.lean +++ b/tests/lean/625.lean @@ -4,7 +4,7 @@ open Lean Lean.PrettyPrinter def foo : PUnit → PUnit := id def x : PUnit := () -@[appUnexpander foo] def unexpandFoo : Unexpander := fun _ => `(sorry) +@[app_unexpander foo] def unexpandFoo : Unexpander := fun _ => `(sorry) #eval do let e : Expr := mkApp (mkMData {} $ mkConst `foo [levelOne]) (mkConst `x) diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out index 9f480013f9..c8e6218cd3 100644 --- a/tests/lean/Reformat.lean.expected.out +++ b/tests/lean/Reformat.lean.expected.out @@ -30,7 +30,7 @@ def idDelta {α : Sort u} (a : α) : α := a /- `idRhs` is an auxiliary declaration used to implement "smart unfolding". It is used as a marker. -/ -@[macroInline, reducible] +@[macro_inline, reducible] def idRhs (α : Sort u) (a : α) : α := a @@ -56,7 +56,7 @@ set_option bootstrap.inductiveCheckResultingUniverse false in abbrev Unit : Type := PUnit -@[matchPattern] +@[match_pattern] abbrev Unit.unit : Unit := PUnit.unit @@ -76,11 +76,11 @@ inductive Empty : Type def Not (a : Prop) : Prop := a → False -@[macroInline] +@[macro_inline] def False.elim {C : Sort u} (h : False) : C := False.rec (fun _ => C) h -@[macroInline] +@[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b := False.elim (h₂ h₁) @@ -90,7 +90,7 @@ inductive Eq : α → α → Prop abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b := Eq.rec (motive := fun α _ => motive α) m h -@[matchPattern] +@[match_pattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a @@ -100,7 +100,7 @@ theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a := h ▸ rfl -@[macroInline] +@[macro_inline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β := Eq.rec (motive := fun α _ => α) a h @@ -125,7 +125,7 @@ init_quot inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop | refl (a : α) : HEq a a -@[matchPattern] +@[match_pattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a := HEq.refl a @@ -255,7 +255,7 @@ class inductive Decidable (p : Prop) | isFalse (h : Not p) : Decidable p | isTrue (h : p) : Decidable p -@[inlineIfReduce, nospecialize] +@[inline_if_reduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool := Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true) @@ -313,7 +313,7 @@ instance {α : Type u} [DecidableEq α] : BEq α := -- We use "dependent" if-then-else to be able to communicate the if-then-else condition -- to the branches -@[macroInline] +@[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α := Decidable.casesOn (motive := fun _ => α) h e t diff --git a/tests/lean/Reformat/Input.lean b/tests/lean/Reformat/Input.lean index 43649bfc63..624ba69d4d 100644 --- a/tests/lean/Reformat/Input.lean +++ b/tests/lean/Reformat/Input.lean @@ -26,7 +26,7 @@ theorems generated by the equation Compiler. @[inline] def idDelta {α : Sort u} (a : α) : α := a /- `idRhs` is an auxiliary declaration used to implement "smart unfolding". It is used as a marker. -/ -@[macroInline, reducible] def idRhs (α : Sort u) (a : α) : α := a +@[macro_inline, reducible] def idRhs (α : Sort u) (a : α) : α := a abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (g : α → β) : α → δ := fun x => f (g x) @@ -46,7 +46,7 @@ inductive PUnit : Sort u unnecessary universe parameters. -/ abbrev Unit : Type := PUnit -@[matchPattern] abbrev Unit.unit : Unit := PUnit.unit +@[match_pattern] abbrev Unit.unit : Unit := PUnit.unit /-- Auxiliary unsafe constant used by the Compiler when erasing proofs from code. -/ unsafe axiom lcProof {α : Prop} : α @@ -63,10 +63,10 @@ inductive Empty : Type def Not (a : Prop) : Prop := a → False -@[macroInline] def False.elim {C : Sort u} (h : False) : C := +@[macro_inline] def False.elim {C : Sort u} (h : False) : C := False.rec (fun _ => C) h -@[macroInline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b := +@[macro_inline] def absurd {a : Prop} {b : Sort v} (h₁ : a) (h₂ : Not a) : b := False.elim (h₂ h₁) inductive Eq : α → α → Prop @@ -75,7 +75,7 @@ inductive Eq : α → α → Prop abbrev Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} (m : motive a) {b : α} (h : Eq a b) : motive b := Eq.rec (motive := fun α _ => motive α) m h -@[matchPattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a +@[match_pattern] def rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) (h₂ : motive a) : motive b := Eq.ndrec h₂ h₁ @@ -83,7 +83,7 @@ theorem Eq.subst {α : Sort u} {motive : α → Prop} {a b : α} (h₁ : Eq a b) theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a := h ▸ rfl -@[macroInline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β := +@[macro_inline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β := Eq.rec (motive := fun α _ => α) a h theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) := @@ -107,7 +107,7 @@ init_quot inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop | refl (a : α) : HEq a a -@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a := +@[match_pattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a := HEq.refl a theorem eqOfHEq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' := @@ -223,7 +223,7 @@ class inductive Decidable (p : Prop) | isFalse (h : Not p) : Decidable p | isTrue (h : p) : Decidable p -@[inlineIfReduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool := +@[inline_if_reduce, nospecialize] def Decidable.decide (p : Prop) [h : Decidable p] : Bool := Decidable.casesOn (motive := fun _ => Bool) h (fun _ => false) (fun _ => true) export Decidable (isTrue isFalse decide) @@ -278,5 +278,5 @@ instance {α : Type u} [DecidableEq α] : BEq α := -- We use "dependent" if-then-else to be able to communicate the if-then-else condition -- to the branches -@[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α := +@[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α := Decidable.casesOn (motive := fun _ => α) h e t diff --git a/tests/lean/computedFieldsCode.lean b/tests/lean/computedFieldsCode.lean index fd12fca632..5f306667cb 100644 --- a/tests/lean/computedFieldsCode.lean +++ b/tests/lean/computedFieldsCode.lean @@ -11,7 +11,7 @@ inductive Exp | a4 | a5 with - @[computedField] hash : Exp → UInt64 + @[computed_field] hash : Exp → UInt64 | .var i => Hashable.hash i + 1000 | .app a b => mixHash (hash a) (hash b) | _ => 42 diff --git a/tests/lean/defaultInstance.lean b/tests/lean/defaultInstance.lean index ea026696af..885d52b5ce 100644 --- a/tests/lean/defaultInstance.lean +++ b/tests/lean/defaultInstance.lean @@ -3,12 +3,12 @@ class Foo (α β : Type) := export Foo (f) -@[defaultInstance] +@[default_instance] instance : Foo Nat Nat := { f := id } -@[defaultInstance] +@[default_instance] instance : Foo String String := { f := id } diff --git a/tests/lean/defaultInstanceWithPrio.lean b/tests/lean/defaultInstanceWithPrio.lean index 144a85c496..a538f0d33d 100644 --- a/tests/lean/defaultInstanceWithPrio.lean +++ b/tests/lean/defaultInstanceWithPrio.lean @@ -3,7 +3,7 @@ structure Rational where den : Nat inv : den ≠ 0 -@[defaultInstance 200] +@[default_instance 200] instance : OfNat Rational n where ofNat := { num := n, den := 1, inv := by decide } diff --git a/tests/lean/delabUnexpand.lean b/tests/lean/delabUnexpand.lean index eea0f8505f..8d83b2944c 100644 --- a/tests/lean/delabUnexpand.lean +++ b/tests/lean/delabUnexpand.lean @@ -4,21 +4,21 @@ structure Foo where macro a:term " ♬ " b:term : term => `(Foo.mk $a $b) -@[appUnexpander Foo.mk] def unexpandFooFailure1 : Lean.PrettyPrinter.Unexpander +@[app_unexpander Foo.mk] def unexpandFooFailure1 : Lean.PrettyPrinter.Unexpander | _ => throw () -@[appUnexpander Foo.mk] def unexpandFoo : Lean.PrettyPrinter.Unexpander +@[app_unexpander Foo.mk] def unexpandFoo : Lean.PrettyPrinter.Unexpander | `(Foo.mk $a $b) => `($a ♬ $b) | _ => throw () -@[appUnexpander Foo.mk] def unexpandFooFailure2 : Lean.PrettyPrinter.Unexpander +@[app_unexpander Foo.mk] def unexpandFooFailure2 : Lean.PrettyPrinter.Unexpander | _ => throw () #check 3 ♬ 4 def foo (k : Nat → Nat) (n : Nat) : Nat := k (n+1) -@[appUnexpander foo] def unexpandFooApp : Lean.PrettyPrinter.Unexpander +@[app_unexpander foo] def unexpandFooApp : Lean.PrettyPrinter.Unexpander | `(foo $k $a) => `(My.foo $k $a) | _ => throw () diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean index 18c97c027d..2582321b69 100644 --- a/tests/lean/elabAsElim.lean +++ b/tests/lean/elabAsElim.lean @@ -34,7 +34,7 @@ def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 := example (h₁ : a = b) (h₂ : b = c) : a = c := Eq.rec h₂ h₁.symm -@[elabAsElim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by +@[elab_as_elim] theorem subst {p : (b : α) → a = b → Prop} (h₁ : a = b) (h₂ : p a rfl) : p b h₁ := by cases h₁ assumption diff --git a/tests/lean/funParen.lean.expected.out b/tests/lean/funParen.lean.expected.out index c53c244d45..ff14986b4a 100644 --- a/tests/lean/funParen.lean.expected.out +++ b/tests/lean/funParen.lean.expected.out @@ -1,4 +1,4 @@ fun α [Repr α] => repr : (α : Type u_1) → [inst : Repr α] → α → Std.Format fun x y => x : (x : ?m) → ?m x → ?m -funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[matchPattern]' expected +funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected fun x => ?m x : (x : ?m) → ?m x diff --git a/tests/lean/implementedByIssue.lean b/tests/lean/implementedByIssue.lean index 3ee6de2f1f..7b0e6aeb39 100644 --- a/tests/lean/implementedByIssue.lean +++ b/tests/lean/implementedByIssue.lean @@ -8,12 +8,12 @@ def get {α} {n : Nat} (A : Array α n) (i : Fin n) : α := A.data i -attribute [implementedBy get] Array.data -- ok +attribute [implemented_by get] Array.data -- ok def get_2 {α : Type} {n : Nat} (A : Array α n) (i : Fin n) : α := A.data i -attribute [implementedBy get_2] Array.data -- error, number of universe parameters do not match +attribute [implemented_by get_2] Array.data -- error, number of universe parameters do not match def get_3 {α} {n : Nat} (i : Fin n) (A : Array α n) : α := A.data i -attribute [implementedBy get_3] Array.data -- error, types do not match +attribute [implemented_by get_3] Array.data -- error, types do not match diff --git a/tests/lean/implementedByIssue.lean.expected.out b/tests/lean/implementedByIssue.lean.expected.out index 060227cb8c..52d36ea869 100644 --- a/tests/lean/implementedByIssue.lean.expected.out +++ b/tests/lean/implementedByIssue.lean.expected.out @@ -1,5 +1,5 @@ -implementedByIssue.lean:15:11-15:30: error: invalid 'implementedBy' argument 'Hidden.get_2', 'Hidden.get_2' has 0 universe level parameter(s), but 'Hidden.Array.data' has 1 -implementedByIssue.lean:19:11-19:30: error: invalid 'implementedBy' argument 'Hidden.get_3', 'Hidden.get_3' has type +implementedByIssue.lean:15:11-15:31: error: invalid 'implemented_by' argument 'Hidden.get_2', 'Hidden.get_2' has 0 universe level parameter(s), but 'Hidden.Array.data' has 1 +implementedByIssue.lean:19:11-19:31: error: invalid 'implemented_by' argument 'Hidden.get_3', 'Hidden.get_3' has type {α : Type u} → {n : Nat} → Fin n → Array α n → α but 'Hidden.Array.data' has type {α : Type u} → {n : Nat} → Array α n → Fin n → α diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index 05506aaa6e..b8c9e593d0 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -12,7 +12,7 @@ "kind": 3, "documentation": {"value": - "`and x y`, or `x && y`, is the boolean \"and\" operation (not to be confused\nwith `And : Prop → Prop → Prop`, which is the propositional connective).\nIt is `@[macroInline]` because it has C-like short-circuiting behavior:\nif `x` is false then `y` is not evaluated.\n", + "`and x y`, or `x && y`, is the boolean \"and\" operation (not to be confused\nwith `And : Prop → Prop → Prop`, which is the propositional connective).\nIt is `@[macro_inline]` because it has C-like short-circuiting behavior:\nif `x` is false then `y` is not evaluated.\n", "kind": "markdown"}, "detail": "Bool → Bool → Bool"}, {"label": "AndOp", diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean index d2b46ff20a..16581f4382 100644 --- a/tests/lean/interactive/goTo.lean +++ b/tests/lean/interactive/goTo.lean @@ -36,7 +36,7 @@ def mkFoo₂ := mkFoo₁ syntax (name := elabTest) "test" : term -@[termElab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun _ _ => do +@[term_elab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun _ _ => do let stx ← `(2) Lean.Elab.Term.elabTerm stx none diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out index 1fa1263dea..0799a12b12 100644 --- a/tests/lean/interactive/goTo.lean.expected.out +++ b/tests/lean/interactive/goTo.lean.expected.out @@ -89,10 +89,10 @@ "position": {"line": 43, "character": 7}} [{"targetUri": "file://goTo.lean", "targetSelectionRange": - {"start": {"line": 38, "character": 25}, - "end": {"line": 38, "character": 37}}, + {"start": {"line": 38, "character": 26}, + "end": {"line": 38, "character": 38}}, "targetRange": - {"start": {"line": 38, "character": 21}, + {"start": {"line": 38, "character": 22}, "end": {"line": 40, "character": 34}}, "originSelectionRange": {"start": {"line": 43, "character": 7}, diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index f28ac46826..f726eadd9a 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -70,7 +70,7 @@ elab_rules : term #check mynota' 1 --^ textDocument/hover -@[inheritDoc] +@[inherit_doc] infix:65 (name := myInfix) " >+< " => Nat.add --^ textDocument/hover --^ textDocument/hover @@ -78,7 +78,7 @@ infix:65 (name := myInfix) " >+< " => Nat.add #check 1 >+< 2 --^ textDocument/hover -@[inheritDoc] notation "ℕ" => Nat +@[inherit_doc] notation "ℕ" => Nat #check ℕ --^ textDocument/hover diff --git a/tests/lean/keyAttrErase.lean b/tests/lean/keyAttrErase.lean index 9a530e576b..b6862ddcc3 100644 --- a/tests/lean/keyAttrErase.lean +++ b/tests/lean/keyAttrErase.lean @@ -1,6 +1,6 @@ theorem ex {i j : Fin n} (h : i = j) : i.val = j.val := h ▸ rfl -attribute [-appUnexpander] unexpandEqNDRec +attribute [-app_unexpander] unexpandEqNDRec #print ex diff --git a/tests/lean/linterMissingDocs.lean b/tests/lean/linterMissingDocs.lean index 20c9629a03..e0e8730a24 100644 --- a/tests/lean/linterMissingDocs.lean +++ b/tests/lean/linterMissingDocs.lean @@ -43,7 +43,7 @@ inductive Ind where | ind2 : Ind → Ind /-- A doc string -/ | doc : Ind with - @[computedField] field : Ind → Nat + @[computed_field] field : Ind → Nat | _ => 1 structure Foo where @@ -96,7 +96,7 @@ elab (name := myCmd) (docComment)? "my_command" ident : command => pure () my_command x open Lean.Linter.MissingDocs in -@[missingDocsHandler myCmd] +@[missing_docs_handler myCmd] def handleMyCmd : SimpleHandler := fun | `(my_command $x:ident) => lintNamed x "my_command" | _ => pure () diff --git a/tests/lean/linterMissingDocs.lean.expected.out b/tests/lean/linterMissingDocs.lean.expected.out index 56d70ac9ec..ba55c4705b 100644 --- a/tests/lean/linterMissingDocs.lean.expected.out +++ b/tests/lean/linterMissingDocs.lean.expected.out @@ -6,7 +6,7 @@ linterMissingDocs.lean:39:4-39:11: warning: missing doc string for public def li linterMissingDocs.lean:41:10-41:13: warning: missing doc string for public inductive Ind [linter.missingDocs] linterMissingDocs.lean:42:4-42:8: warning: missing doc string for public constructor Ind.ind1 [linter.missingDocs] linterMissingDocs.lean:43:4-43:8: warning: missing doc string for public constructor Ind.ind2 [linter.missingDocs] -linterMissingDocs.lean:46:19-46:24: warning: missing doc string for computed field Ind.field [linter.missingDocs] +linterMissingDocs.lean:46:20-46:25: warning: missing doc string for computed field Ind.field [linter.missingDocs] linterMissingDocs.lean:49:10-49:13: warning: missing doc string for public structure Foo [linter.missingDocs] linterMissingDocs.lean:50:2-50:5: warning: missing doc string for public field Foo.mk1 [linter.missingDocs] linterMissingDocs.lean:53:3-53:6: warning: missing doc string for public field Foo.mk4 [linter.missingDocs] diff --git a/tests/lean/linterSuspiciousUnexpanderPatterns.lean b/tests/lean/linterSuspiciousUnexpanderPatterns.lean index 3dc3961b94..fe3cd7909a 100644 --- a/tests/lean/linterSuspiciousUnexpanderPatterns.lean +++ b/tests/lean/linterSuspiciousUnexpanderPatterns.lean @@ -2,11 +2,11 @@ import Lean set_option linter.suspiciousUnexpanderPatterns true -@[appUnexpander List.nil] def unexpandListNilBad : Lean.PrettyPrinter.Unexpander +@[app_unexpander List.nil] def unexpandListNilBad : Lean.PrettyPrinter.Unexpander | `(List.nil) => `([]) | _ => throw () /--hey-/ -@[appUnexpander List.cons] private def unexpandListConsBad : Lean.PrettyPrinter.Unexpander +@[app_unexpander List.cons] private def unexpandListConsBad : Lean.PrettyPrinter.Unexpander | `(List.cons $x []) => `([$x]) | _ => throw () diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean index 16c09d892d..926d319416 100644 --- a/tests/lean/linterUnusedVariables.lean +++ b/tests/lean/linterUnusedVariables.lean @@ -191,7 +191,7 @@ variable {α β} [inst : ToString α] @[specialize] def specializeDef (x : Nat) : Nat := 3 -@[implementedBy specializeDef] +@[implemented_by specializeDef] def implementedByDef (x : Nat) : Nat := let y := 3 5 @@ -236,7 +236,7 @@ def Nat.discriminate (n : Nat) (H1 : n = 0 → α) (H2 : ∀ m, n = succ m → | 0 => H1 rfl | succ m => H2 m rfl -@[unusedVariablesIgnoreFn] +@[unused_variables_ignore_fn] def ignoreEverything : Lean.Linter.IgnoreFunction := fun _ _ _ => true diff --git a/tests/lean/matchOrIssue.lean.expected.out b/tests/lean/matchOrIssue.lean.expected.out index 20bf424518..18593dbf4b 100644 --- a/tests/lean/matchOrIssue.lean.expected.out +++ b/tests/lean/matchOrIssue.lean.expected.out @@ -1 +1 @@ -matchOrIssue.lean:7:10-7:13: error: invalid pattern, constructor or constant marked with '[matchPattern]' expected +matchOrIssue.lean:7:10-7:13: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected diff --git a/tests/lean/notationPrecheck.lean.expected.out b/tests/lean/notationPrecheck.lean.expected.out index 5caf532ffc..5efe2b55c6 100644 --- a/tests/lean/notationPrecheck.lean.expected.out +++ b/tests/lean/notationPrecheck.lean.expected.out @@ -1,5 +1,5 @@ notationPrecheck.lean:1:25-1:26: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. -notationPrecheck.lean:4:16-4:19: error: no macro or `[quotPrecheck]` instance for syntax kind 'termB_' found +notationPrecheck.lean:4:16-4:19: error: no macro or `[quot_precheck]` instance for syntax kind 'termB_' found b x This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check. notationPrecheck.lean:8:7-8:8: error: elaboration function for 'termB_' has not been implemented diff --git a/tests/lean/resolveGlobalName.lean b/tests/lean/resolveGlobalName.lean index 267d9531f6..5733d3f615 100644 --- a/tests/lean/resolveGlobalName.lean +++ b/tests/lean/resolveGlobalName.lean @@ -16,7 +16,7 @@ open Lean.Elab.Command syntax (name := resolveKind) "#resolve " ident : command -@[commandElab resolveKind] def elabResolve : CommandElab := +@[command_elab resolveKind] def elabResolve : CommandElab := fun stx => liftTermElabM do let cs ← resolveGlobalName $ stx.getIdAt 1; Lean.logInfo $ toString cs; diff --git a/tests/lean/run/1308.lean b/tests/lean/run/1308.lean index 86f28e6f18..29bd8c11d2 100644 --- a/tests/lean/run/1308.lean +++ b/tests/lean/run/1308.lean @@ -1,2 +1,2 @@ -@[defaultInstance high] instance : HPow R Nat R where hPow a _ := a +@[default_instance high] instance : HPow R Nat R where hPow a _ := a example (x y : Nat) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * (x * y ^ 2 + x ^ 2 * y) := sorry diff --git a/tests/lean/run/175.lean b/tests/lean/run/175.lean index e78a4bb1de..712fd0c379 100644 --- a/tests/lean/run/175.lean +++ b/tests/lean/run/175.lean @@ -6,7 +6,7 @@ open Lean.Elab.Term syntax (name := fooKind) "foo!" term : term -@[termElab fooKind] def elabFoo : TermElab := +@[term_elab fooKind] def elabFoo : TermElab := fun stx expectedType? => elabTerm (stx.getArg 1) expectedType? #check foo! 10 @@ -18,7 +18,7 @@ namespace Elab namespace Tactic open Meta -@[builtinTactic clear] def myEvalClear : Tactic := -- this fails in the old-frontend because it eagerly resolves `clear` as `Lean.Meta.clear`. +@[builtin_tactic clear] def myEvalClear : Tactic := -- this fails in the old-frontend because it eagerly resolves `clear` as `Lean.Meta.clear`. fun _ => pure () end Tactic diff --git a/tests/lean/run/602.lean b/tests/lean/run/602.lean index f71fe9e02d..f7e9509295 100644 --- a/tests/lean/run/602.lean +++ b/tests/lean/run/602.lean @@ -18,7 +18,7 @@ instance Ring.toSemiring [instR : Ring α] : Semiring α := { add := instR.add } instance NormedField.toRing [instNF : NormedField α] : Ring α := { add := instNF.add } --- @[inferTCGoalsRL] +-- @[infer_tc_goals_rl] instance SemiNormedSpace.toModule [NormedField α] [SemiNormedGroup β] [SemiNormedSpace α β] : Module α β := {} opaque R : Type := Unit diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean index 10fb741b21..e6171660b2 100644 --- a/tests/lean/run/KyleAlg.lean +++ b/tests/lean/run/KyleAlg.lean @@ -245,7 +245,7 @@ where | Expr.mdata _ b => visit b | _ => return () -@[implementedBy Expr.dagSizeUnsafe] +@[implemented_by Expr.dagSizeUnsafe] opaque Expr.dagSize (e : Expr) : IO Nat def getDeclTypeValueDagSize (declName : Name) : CoreM Nat := do diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index d7a001c02d..eebdf764b8 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -39,7 +39,7 @@ def checkDelab (e : Expr) (tgt? : Option Term) (name? : Option Name := none) : T syntax (name := testDelabTD) "#testDelab " term " expecting " term : command -@[commandElab testDelabTD] def elabTestDelabTD : CommandElab +@[command_elab testDelabTD] def elabTestDelabTD : CommandElab | `(#testDelab $stx:term expecting $tgt:term) => liftTermElabM do withDeclName `delabTD do let e ← elabTerm stx none let e ← levelMVarToParam e @@ -49,7 +49,7 @@ syntax (name := testDelabTD) "#testDelab " term " expecting " term : command syntax (name := testDelabTDN) "#testDelabN " ident : command -@[commandElab testDelabTDN] def elabTestDelabTDN : CommandElab +@[command_elab testDelabTDN] def elabTestDelabTDN : CommandElab | `(#testDelabN $name:ident) => liftTermElabM do withDeclName `delabTD do let name := name.getId let [name] ← resolveGlobalConst (mkIdent name) | throwError "cannot resolve name" diff --git a/tests/lean/run/addDecorationsWithoutPartial.lean b/tests/lean/run/addDecorationsWithoutPartial.lean index 73fa0aa512..4c9910c72e 100644 --- a/tests/lean/run/addDecorationsWithoutPartial.lean +++ b/tests/lean/run/addDecorationsWithoutPartial.lean @@ -48,7 +48,7 @@ end ReplaceImpl' local macro "dec " h:ident : term => `(by apply Nat.le_trans _ $h; simp_arith) -@[implementedBy ReplaceImpl'.replaceUnsafe] +@[implemented_by ReplaceImpl'.replaceUnsafe] def replace' (e0 : Expr) (f? : (e : Expr) → sizeOf e ≤ sizeOf e0 → Option Expr) : Expr := let rec go (e : Expr) (h : sizeOf e ≤ sizeOf e0) : Expr := match f? e h with diff --git a/tests/lean/run/choiceExpectedTypeBug.lean b/tests/lean/run/choiceExpectedTypeBug.lean index 490925dcfd..f2fd7f915e 100644 --- a/tests/lean/run/choiceExpectedTypeBug.lean +++ b/tests/lean/run/choiceExpectedTypeBug.lean @@ -19,7 +19,7 @@ open Lean open Lean.Elab open Lean.Elab.Term -@[termElab emptyS] def elabEmptyS : TermElab := +@[term_elab emptyS] def elabEmptyS : TermElab := fun stx expectedType? => do tryPostponeIfNoneOrMVar expectedType? let stxNew ← `(Nat.zero) diff --git a/tests/lean/run/computedFields.lean b/tests/lean/run/computedFields.lean index 735d60cdbf..c67f895da1 100644 --- a/tests/lean/run/computedFields.lean +++ b/tests/lean/run/computedFields.lean @@ -3,7 +3,7 @@ inductive Exp | var (i : UInt32) | app (a b : Exp) with - /-- Computes the hash -/ @[simp, computedField] protected hash : Exp → UInt64 + /-- Computes the hash -/ @[simp, computed_field] protected hash : Exp → UInt64 | .var i => Hashable.hash i | .app a b => mixHash a.hash b.hash | .hole => 32 @@ -30,7 +30,7 @@ inductive B.C (α : Type u) : Nat → Type u | a : C α 0 | b (c : C α n) {d : C α (n-1)} : C α (n+1) with - @[computedField] hash : ∀ α i, C α i → UInt64 + @[computed_field] hash : ∀ α i, C α i → UInt64 | _, _, .a => 1 | _, _, .b c => 42 + c.hash @@ -50,7 +50,7 @@ mutual | a (b : B) | b (b : B) with - @[computedField] f : A → Nat + @[computed_field] f : A → Nat | .a c => 32 + c.f | .b c => 42 + 2*c.f @@ -58,7 +58,7 @@ mutual | c (a : A) | d with - @[computedField] f : B → Nat + @[computed_field] f : B → Nat | .c a => a.f | .d => 0 end diff --git a/tests/lean/run/constantCompilerBug.lean b/tests/lean/run/constantCompilerBug.lean index df2f6cb9d8..e622f51f03 100644 --- a/tests/lean/run/constantCompilerBug.lean +++ b/tests/lean/run/constantCompilerBug.lean @@ -6,7 +6,7 @@ open Lean open Lean.Parser def regBlaParserAttribute : IO Unit := -registerBuiltinDynamicParserAttribute (Name.mkSimple "blaParser") (Name.mkSimple "bla") +registerBuiltinDynamicParserAttribute (Name.mkSimple "bla_parser") (Name.mkSimple "bla") @[inline] def parser : Parser := categoryParser (Name.mkSimple "bla") 0 diff --git a/tests/lean/run/defaultInstBacktrackIssue.lean b/tests/lean/run/defaultInstBacktrackIssue.lean index 236e10f67d..73c290f1a0 100644 --- a/tests/lean/run/defaultInstBacktrackIssue.lean +++ b/tests/lean/run/defaultInstBacktrackIssue.lean @@ -4,7 +4,7 @@ class LOp (α β) where lOp : α → β → β class Op (α) where op : α → α → α -@[defaultInstance] +@[default_instance] instance inst1 [LOp α β] : HOp α β β := ⟨LOp.lOp⟩ instance inst2 [Op α] : LOp α α := ⟨Op.op⟩ @@ -19,7 +19,7 @@ example : n ⋆ x = z := sorry -- TC works example : 1 ⋆ x = z := sorry -- TC works -attribute [defaultInstance] inst2 +attribute [default_instance] inst2 example : n ⋆ x = z := sorry -- TC works diff --git a/tests/lean/run/evalBuiltinInit.lean b/tests/lean/run/evalBuiltinInit.lean index 1f028ca33a..8db8697c1c 100644 --- a/tests/lean/run/evalBuiltinInit.lean +++ b/tests/lean/run/evalBuiltinInit.lean @@ -1,5 +1,5 @@ import Lean --- option should be ignored when evaluating a `[builtinInit]` decl +-- option should be ignored when evaluating a `[builtin_init]` decl set_option interpreter.prefer_native false #eval toString Lean.PrettyPrinter.formatterAttribute.defn.name diff --git a/tests/lean/run/fieldTypeBug.lean b/tests/lean/run/fieldTypeBug.lean index 51da442627..f6d6a6573e 100644 --- a/tests/lean/run/fieldTypeBug.lean +++ b/tests/lean/run/fieldTypeBug.lean @@ -2,8 +2,8 @@ import Lean def HList (αs : List (Type u)) : Type u := αs.foldr Prod.{u, u} PUnit -@[matchPattern] def HList.nil : HList [] := ⟨⟩ -@[matchPattern] def HList.cons (a : α) (as : HList αs): HList (α :: αs) := (a, as) +@[match_pattern] def HList.nil : HList [] := ⟨⟩ +@[match_pattern] def HList.cons (a : α) (as : HList αs): HList (α :: αs) := (a, as) def HList.set {αs : List (Type u)} (as : HList αs) (i : Fin αs.length) (v : αs.get i) : HList αs := match αs, as, i, v with diff --git a/tests/lean/run/frontend_meeting_2022_09_13.lean b/tests/lean/run/frontend_meeting_2022_09_13.lean index 4f217134d1..17ff94dca1 100644 --- a/tests/lean/run/frontend_meeting_2022_09_13.lean +++ b/tests/lean/run/frontend_meeting_2022_09_13.lean @@ -50,15 +50,15 @@ where def commandCommentBody : Parser := { fn := rawFn commandCommentBodyFn (trailingWs := true) } -@[combinatorParenthesizer commandCommentBody] def commandCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken -@[combinatorFormatter commandCommentBody] def commandCommentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous +@[combinator_parenthesizer commandCommentBody] def commandCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken +@[combinator_formatter commandCommentBody] def commandCommentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous -@[commandParser] def commandComment := leading_parser "//-" >> commandCommentBody >> ppLine +@[command_parser] def commandComment := leading_parser "//-" >> commandCommentBody >> ppLine end open Lean Elab Command in -@[commandElab commandComment] def elabCommandComment : CommandElab := fun stx => do +@[command_elab commandComment] def elabCommandComment : CommandElab := fun stx => do let .atom _ val := stx[1] | return () let str := val.extract 0 (val.endPos - ⟨3⟩) IO.println s!"str := {repr str}" diff --git a/tests/lean/run/hmul2.lean b/tests/lean/run/hmul2.lean index e6fe11f4ab..e71af86b9d 100644 --- a/tests/lean/run/hmul2.lean +++ b/tests/lean/run/hmul2.lean @@ -1,4 +1,4 @@ -@[defaultInstance] +@[default_instance] instance [Mul α] : HMul α (Array α) (Array α) where hMul a as := as.map (a * ·) diff --git a/tests/lean/run/impByNameResolution.lean b/tests/lean/run/impByNameResolution.lean index bbe6f6cd89..0408550923 100644 --- a/tests/lean/run/impByNameResolution.lean +++ b/tests/lean/run/impByNameResolution.lean @@ -4,6 +4,6 @@ namespace Foo def f (x : Nat) : Nat := x + 1 -@[implementedBy f] opaque g : Nat → Nat +@[implemented_by f] opaque g : Nat → Nat end Foo diff --git a/tests/lean/run/matchEqs.lean b/tests/lean/run/matchEqs.lean index 23c5c3f6b8..ab9f46048a 100644 --- a/tests/lean/run/matchEqs.lean +++ b/tests/lean/run/matchEqs.lean @@ -4,7 +4,7 @@ syntax (name := test) "test%" ident : command open Lean.Elab open Lean.Elab.Command -@[commandElab test] def elabTest : CommandElab := fun stx => do +@[command_elab test] def elabTest : CommandElab := fun stx => do let id ← resolveGlobalConstNoOverloadWithInfo stx[1] liftTermElabM do IO.println (repr (← Lean.Meta.Match.getEquationsFor id)) diff --git a/tests/lean/run/matchEqsBug.lean b/tests/lean/run/matchEqsBug.lean index e69b414c2d..44884f6f99 100644 --- a/tests/lean/run/matchEqsBug.lean +++ b/tests/lean/run/matchEqsBug.lean @@ -4,7 +4,7 @@ syntax (name := test) "test%" ident : command open Lean.Elab open Lean.Elab.Command -@[commandElab test] def elabTest : CommandElab := fun stx => do +@[command_elab test] def elabTest : CommandElab := fun stx => do let id ← resolveGlobalConstNoOverloadWithInfo stx[1] liftTermElabM do IO.println (repr (← Lean.Meta.Match.getEquationsFor id)) diff --git a/tests/lean/run/nativeReflBackdoor.lean b/tests/lean/run/nativeReflBackdoor.lean index 08ad3f7da4..555c697d61 100644 --- a/tests/lean/run/nativeReflBackdoor.lean +++ b/tests/lean/run/nativeReflBackdoor.lean @@ -2,24 +2,24 @@ /- This example demonstratea that when we are using `native_decide`, -we are also trusting the correctness of `implementedBy` annotations, +we are also trusting the correctness of `implemented_by` annotations, foreign functions (i.e., `[extern]` annotations), etc. -/ def g (b : Bool) := false /- -The following `implementedBy` is telling the compiler +The following `implemented_by` is telling the compiler "trust me, `g` does implement `f`" which is clearly false in this example. -/ -@[implementedBy g] +@[implemented_by g] def f (b : Bool) := b theorem fConst (b : Bool) : f b = false := match b with | true => /- The following `native_decide` is going to use `g` to evaluate `f` - because of the `implementedBy` directive. -/ + because of the `implemented_by` directive. -/ have : (f true) = false := by native_decide this | false => rfl @@ -30,7 +30,7 @@ have h₂ : f true = false := fConst true; Eq.trans h₁.symm h₂ /- -We managed to prove `False` using the unsound annotation `implementedBy` above. +We managed to prove `False` using the unsound annotation `implemented_by` above. -/ theorem unsound : False := Bool.noConfusion trueEqFalse diff --git a/tests/lean/run/offsetIssue.lean b/tests/lean/run/offsetIssue.lean index 7bbc89a73d..8f92ca0d85 100644 --- a/tests/lean/run/offsetIssue.lean +++ b/tests/lean/run/offsetIssue.lean @@ -5,7 +5,7 @@ axiom foo {n m : Nat} (a : BV n) (b : BV m) : BV (n - m) def test (x1 : BV 30002) (x2 : BV 30001) (y1 : BV 60004) (y2 : BV 60003) : Prop := foo x1 x2 = without_expected_type foo y1 y2 -@[elabWithoutExpectedType] +@[elab_without_expected_type] axiom foo2 {n m : Nat} (a : BV n) (b : BV m) : BV (n - m) def test2 (x1 : BV 30002) (x2 : BV 30001) (y1 : BV 60004) (y2 : BV 60003) : Prop := diff --git a/tests/lean/run/smartUnfoldingBug.lean b/tests/lean/run/smartUnfoldingBug.lean index bf9d90e768..36439c6915 100644 --- a/tests/lean/run/smartUnfoldingBug.lean +++ b/tests/lean/run/smartUnfoldingBug.lean @@ -181,7 +181,7 @@ open Lean.Meta open Lean.Elab.Term syntax (name:= nrmlform)"whnf!" term : term -@[termElab nrmlform] def normalformImpl : TermElab := +@[term_elab nrmlform] def normalformImpl : TermElab := fun stx expectedType? => match stx with | `(whnf! $s) => diff --git a/tests/lean/run/structPerfIssue.lean b/tests/lean/run/structPerfIssue.lean index 16e09c28be..917bc3f0d7 100644 --- a/tests/lean/run/structPerfIssue.lean +++ b/tests/lean/run/structPerfIssue.lean @@ -10,7 +10,7 @@ attribute [eliminator] Id.casesOn infix:50 (priority := high) " = " => Id -@[matchPattern] abbrev idp {A : Type u} (a : A) : a = a := Id.refl +@[match_pattern] abbrev idp {A : Type u} (a : A) : a = a := Id.refl def Id.symm {A : Type u} {a b : A} (p : a = b) : b = a := by { induction p; apply idp } diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index 1053b01c29..aa63738d01 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -14,11 +14,11 @@ pure () open Lean.Parser -@[termParser] def tst := leading_parser "(|" >> termParser >> Parser.optional (symbol ", " >> termParser) >> "|)" +@[term_parser] def tst := leading_parser "(|" >> termParser >> Parser.optional (symbol ", " >> termParser) >> "|)" def tst2 : Parser := symbol "(||" >> termParser >> symbol "||)" -@[termParser] def boo : ParserDescr := +@[term_parser] def boo : ParserDescr := ParserDescr.node `boo 10 (ParserDescr.binary `andthen (ParserDescr.symbol "[|") @@ -26,21 +26,21 @@ ParserDescr.node `boo 10 (ParserDescr.cat `term 0) (ParserDescr.symbol "|]"))) -@[termParser] def boo2 : ParserDescr := +@[term_parser] def boo2 : ParserDescr := ParserDescr.node `boo2 10 (ParserDescr.parser `tst2) open Lean.Elab.Term -@[termElab tst] def elabTst : TermElab := +@[term_elab tst] def elabTst : TermElab := adaptExpander $ fun stx => match stx with | `((| $e |)) => pure e | _ => throwUnsupportedSyntax -@[termElab boo] def elabBoo : TermElab := +@[term_elab boo] def elabBoo : TermElab := fun stx expected? => elabTerm (stx.getArg 1) expected? -@[termElab boo2] def elabBool2 : TermElab := +@[term_elab boo2] def elabBool2 : TermElab := adaptExpander $ fun stx => match stx with | `((|| $e ||)) => `($e + 1) | _ => throwUnsupportedSyntax @@ -52,7 +52,7 @@ adaptExpander $ fun stx => match stx with -- #eval run "#check (| id 1, id 1 |)" -- it will fail -@[termElab tst] def elabTst2 : TermElab := +@[term_elab tst] def elabTst2 : TermElab := adaptExpander $ fun stx => match stx with | `((| $e1, $e2 |)) => `(($e1, $e2)) | _ => throwUnsupportedSyntax diff --git a/tests/lean/run/wfEqnsIssue.lean b/tests/lean/run/wfEqnsIssue.lean index 1f74010b00..1f81042bec 100644 --- a/tests/lean/run/wfEqnsIssue.lean +++ b/tests/lean/run/wfEqnsIssue.lean @@ -1,7 +1,7 @@ def HList (αs : List (Type u)) : Type u := αs.foldr Prod.{u, u} PUnit -@[matchPattern] def HList.nil : HList [] := ⟨⟩ -@[matchPattern] def HList.cons (a : α) (as : HList αs): HList (α :: αs) := (a, as) +@[match_pattern] def HList.nil : HList [] := ⟨⟩ +@[match_pattern] def HList.cons (a : α) (as : HList αs): HList (α :: αs) := (a, as) def HList.set : {αs : _} → HList αs → (i : Fin αs.length) → αs.get i → HList αs | _ :: _, cons a as, ⟨0, h⟩, b => cons b as diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out index c1626128b6..c98c3b5894 100644 --- a/tests/lean/syntaxPrec.lean.expected.out +++ b/tests/lean/syntaxPrec.lean.expected.out @@ -1,6 +1,6 @@ syntaxPrec.lean:1:18: error: expected ':' [Elab.command] syntax "foo"("*" <|> term,+) : term -[Elab.command] @[termParser 1000] +[Elab.command] @[term_parser 1000] def «termFoo*_» : Lean.ParserDescr✝ := ParserDescr.node✝ `«termFoo*_» 1022 (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") diff --git a/tests/lean/unexpander.lean b/tests/lean/unexpander.lean index 02f385f952..54240010a7 100644 --- a/tests/lean/unexpander.lean +++ b/tests/lean/unexpander.lean @@ -3,13 +3,13 @@ open Lean PrettyPrinter namespace ns inductive Foo | mk: Foo -@[appUnexpander Foo.mk] +@[app_unexpander Foo.mk] def unexpadFoo : Lean.PrettyPrinter.Unexpander | `($x) => `(unexpand) def foo := Foo.mk #print foo -@[appUnexpander ns.Foo.mk] +@[app_unexpander ns.Foo.mk] def unexpadFoo' : Lean.PrettyPrinter.Unexpander | `($x) => `(unexpand) def bar := ns.Foo.mk diff --git a/tests/playground/deriving.lean b/tests/playground/deriving.lean index 5fd55065e2..d5076ea999 100644 --- a/tests/playground/deriving.lean +++ b/tests/playground/deriving.lean @@ -303,7 +303,7 @@ def mkDerivingToString (typeName : Name) : CommandElabM Unit := do syntax[runTstKind] "runTst" : command -@[commandElab runTstKind] def elabTst : CommandElab := fun stx => +@[command_elab runTstKind] def elabTst : CommandElab := fun stx => mkDerivingToString `Test.Foo set_option trace.Meta.debug true diff --git a/tests/playground/flat_parser.lean b/tests/playground/flat_parser.lean index de34ff60d9..784366aad2 100644 --- a/tests/playground/flat_parser.lean +++ b/tests/playground/flat_parser.lean @@ -111,8 +111,8 @@ abbreviation trailingParser := Syntax → Parser | ⟨Result.ok _ it c s _, h⟩ := Result.ok a it c s true | ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h -@[inlineIfReduce] def eagerOr (b₁ b₂ : Bool) := b₁ || b₂ -@[inlineIfReduce] def eagerAnd (b₁ b₂ : Bool) := b₁ && b₂ +@[inline_if_reduce] def eagerOr (b₁ b₂ : Bool) := b₁ || b₂ +@[inline_if_reduce] def eagerAnd (b₁ b₂ : Bool) := b₁ && b₂ @[inline] def parserM.bind {α β : Type} (x : parserM α) (f : α → parserM β) : parserM β := λ ps cfg r, diff --git a/tests/playground/flat_parser2.lean b/tests/playground/flat_parser2.lean index 790edd21da..44708caf52 100644 --- a/tests/playground/flat_parser2.lean +++ b/tests/playground/flat_parser2.lean @@ -106,8 +106,8 @@ abbrev parserCore := parserCoreM Syntax | ⟨Result.ok _ it c s _, h⟩ := Result.ok a it c s tt | ⟨Result.error _ _ _ _ _, h⟩ := unreachableError h -@[inlineIfReduce] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ -@[inlineIfReduce] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ +@[inline_if_reduce] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ +@[inline_if_reduce] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ @[inline] def parserCoreM.bind {α β : Type} (x : parserCoreM α) (f : α → parserCoreM β) : parserCoreM β := λ r, diff --git a/tests/playground/forthelean/ForTheLean/Demo.lean b/tests/playground/forthelean/ForTheLean/Demo.lean index d116a5a624..22a45092e0 100644 --- a/tests/playground/forthelean/ForTheLean/Demo.lean +++ b/tests/playground/forthelean/ForTheLean/Demo.lean @@ -8,7 +8,7 @@ open Prelim -- {{{ [synonym] syntax variant := "-"? wlexem syntax [synonym] "[synonym " wlexem ("/" (wlexem <|> variant))+ "]" : command -@[commandElab synonym] +@[command_elab synonym] def elabSynonym : CommandElab := fun stx => match_syntax stx with | `([synonym $w:ident/ -$w':ident]) => modifyEnv $ fun env => addSynonym env w.getId (w.getId.appendAfter w'.getId.toString) diff --git a/tests/playground/forthelean/ForTheLean/Prelim.lean b/tests/playground/forthelean/ForTheLean/Prelim.lean index 4c22f1ebd2..39e843e16e 100644 --- a/tests/playground/forthelean/ForTheLean/Prelim.lean +++ b/tests/playground/forthelean/ForTheLean/Prelim.lean @@ -11,7 +11,7 @@ open Lean open Lean.Parser -- for declaring simple parsers I can still use within other `syntax` -@[commandParser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser +@[command_parser] def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser @[macro syntaxAbbrev] def elabSyntaxAbbrev : Macro := fun stx => match_syntax stx with | `(syntax $id := $p*) => `(declare_syntax_cat $id syntax:0 $p* : $id) @@ -48,7 +48,7 @@ open Lean.Elab.Command open Prelim syntax [type_of] "type_of" term:max : term -@[termElab «type_of»] +@[term_elab «type_of»] def elabTypeOf : Term.TermElab := fun stx _ => match_syntax stx with | `(type_of $e) => @@ -56,7 +56,7 @@ fun stx _ => match_syntax stx with | _ => Term.throwUnsupportedSyntax syntax [syntax_synonyms] "syntax_synonyms" "[" ident "]" «syntax»+ ":" ident : command -@[commandElab «syntax_synonyms»] def elabSyntaxSynonyms : CommandElab := +@[command_elab «syntax_synonyms»] def elabSyntaxSynonyms : CommandElab := fun stx => match_syntax stx with | `(syntax_synonyms [$kind] $stxs* : $cat) => -- TODO: do notation diff --git a/tests/playground/hashable.lean b/tests/playground/hashable.lean index 7dd4893172..185faf32f2 100644 --- a/tests/playground/hashable.lean +++ b/tests/playground/hashable.lean @@ -5,30 +5,30 @@ inductive SimpleInd | B deriving Hashable -theorem «inductive fields have different base hashes» : ∀ x, hash x = +theorem «inductive fields have different base hashes» : ∀ x, hash x = match x with | SimpleInd.A => 0 | SimpleInd.B => 1 := λ x => rfl -mutual +mutual inductive Foo : Type → Type | A : Int → (3 = 3) → String → Foo Int -| B : Bar → Foo String +| B : Bar → Foo String deriving Hashable inductive Bar | C -| D : Foo String → Bar +| D : Foo String → Bar deriving Hashable end #eval hash (Foo.A 3 rfl "bla") #eval hash (Foo.B $ Bar.D $ Foo.B Bar.C) -inductive ManyConstructors | A | B | C | D | E | F | G | H | I | J | K | L +inductive ManyConstructors | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z deriving Hashable -theorem «Each constructor is hashed as a different number to make mixing better» : ∀ x, hash x = -match x with +theorem «Each constructor is hashed as a different number to make mixing better» : ∀ x, hash x = +match x with | ManyConstructors.A => 0 | ManyConstructors.B => 1 | ManyConstructors.C => 2 @@ -56,7 +56,7 @@ match x with | ManyConstructors.Y => 24 | ManyConstructors.Z => 25 := λ x => rfl -structure Person := +structure Person := FirstName : String LastName : String Age : Nat @@ -68,16 +68,16 @@ structure Company := NumberOfEmployees : Nat deriving Hashable --- structures hash just fine -#eval hash { - Name := "Microsoft" - CEO := { FirstName := "Satya", LastName := "Nadella", Age := 53 } +-- structures hash just fine +#eval hash { + Name := "Microsoft" + CEO := { FirstName := "Satya", LastName := "Nadella", Age := 53 } NumberOfEmployees := 165000 : Company } -- 10875484723257753924 -- syntax(name := tst) "tst" : command --- @[commandElab «tst»] def elab_tst : CommandElab := fun stx => do +-- @[command_elab «tst»] def elab_tst : CommandElab := fun stx => do -- let declNames := #[`Foo, `Bar] -- let declNames := #[`Foo] -- discard $ mkHashableHandler declNames --- pure () \ No newline at end of file +-- pure () diff --git a/tests/playground/matchEqs.lean b/tests/playground/matchEqs.lean index a4c5186d62..6fab337f2e 100644 --- a/tests/playground/matchEqs.lean +++ b/tests/playground/matchEqs.lean @@ -4,7 +4,7 @@ syntax (name := test) "test%" ident : command open Lean.Elab open Lean.Elab.Command -@[commandElab test] def elabTest : CommandElab := fun stx => do +@[command_elab test] def elabTest : CommandElab := fun stx => do let id ← resolveGlobalConstNoOverloadWithInfo stx[1] liftTermElabM none do Lean.Meta.Match.mkEquationsFor id diff --git a/tests/playground/pldi/array_map.lean b/tests/playground/pldi/array_map.lean index 2cc438efe5..11e15d4931 100644 --- a/tests/playground/pldi/array_map.lean +++ b/tests/playground/pldi/array_map.lean @@ -13,7 +13,7 @@ @[inline] unsafe partial def umap {α β : Type} (f : α → β) (as : Array α) : Array β := unsafeCast (umapAux f 0 (unsafeCast as)) -@[implementedBy umap] def map {α β : Type} (f : α → β) (as : Array α) : Array β := +@[implemented_by umap] def map {α β : Type} (f : α → β) (as : Array α) : Array β := as.foldl (fun bs a => bs.push (f a)) (Array.mkEmpty as.size) set_option compiler.extract_closed false diff --git a/tests/playground/pldi/ptreq.lean b/tests/playground/pldi/ptreq.lean index 5d17c6c0f3..f24558a6c2 100644 --- a/tests/playground/pldi/ptreq.lean +++ b/tests/playground/pldi/ptreq.lean @@ -6,7 +6,7 @@ unsafe def ptrAddrUnsafe {α : Type} (a : @& α) : USize := 0 @[inline] unsafe def withPtrEqUnsafe {α : Type} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool := if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k () -@[implementedBy withPtrEqUnsafe] +@[implemented_by withPtrEqUnsafe] def withPtrEq {α : Type} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool := k () diff --git a/tests/playground/termParserAttr.lean b/tests/playground/termParserAttr.lean index 4219d7823c..648e585fd4 100644 --- a/tests/playground/termParserAttr.lean +++ b/tests/playground/termParserAttr.lean @@ -12,9 +12,9 @@ do env ← MetaIO.getEnv; pure () open Lean.Parser -@[termParser] def tst := parser! "(|" >> termParser >> "|)" +@[term_parser] def tst := parser! "(|" >> term_parser >> "|)" -@[termParser] def boo : ParserDescr := +@[term_parser] def boo : ParserDescr := ParserDescr.node `boo (ParserDescr.andthen (ParserDescr.symbol "[|" 0) @@ -24,11 +24,11 @@ ParserDescr.node `boo open Lean.Elab.Term -@[termElab tst] def elabTst : TermElab := +@[term_elab tst] def elabTst : TermElab := fun stx expected? => elabTerm (stx.getArg 1) expected? -@[termElab boo] def elabBoo : TermElab := +@[term_elab boo] def elabBoo : TermElab := fun stx expected? => elabTerm (stx.getArg 1) expected? diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean index 55dafc7e9c..4aee963cbb 100644 --- a/tests/playground/webserver/Webserver.lean +++ b/tests/playground/webserver/Webserver.lean @@ -104,8 +104,8 @@ def text : Parser := -- {{{ let s := takeWhile1Fn (not ∘ "{<>}$".contains) "HTML text" c s mkNodeToken `LX.text startPos c s } -- }}} -@[combinatorFormatter text] def text.formatter : Formatter := pure () -@[combinatorParenthesizer text] def text.parenthesizer : Parenthesizer := pure () +@[combinator_formatter text] def text.formatter : Formatter := pure () +@[combinator_parenthesizer text] def text.parenthesizer : Parenthesizer := pure () syntax text : child syntax "{" term "}" : child @@ -138,8 +138,8 @@ def pathLiteral : Parser := -- {{{ let s := takeWhile1Fn (fun c => c == '/' || c.isAlphanum) "URL path" c s mkNodeToken `pathLiteral startPos c s } -- }}} -@[combinatorFormatter pathLiteral] def pathLiteral.formatter : Formatter := pure () -@[combinatorParenthesizer pathLiteral] def pathLiteral.parenthesizer : Parenthesizer := pure () +@[combinator_formatter pathLiteral] def pathLiteral.formatter : Formatter := pure () +@[combinator_parenthesizer pathLiteral] def pathLiteral.parenthesizer : Parenthesizer := pure () declare_syntax_cat pathItem syntax pathLiteral : pathItem @@ -168,7 +168,7 @@ macro v:verb p:path " => " t:term : command => do -- {{{ GET / => redirect "/greet/stranger" -GET /greet/{name} => write +GET /greet/{name} => write

Hello, {name}!