Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Std.Lean.TagAttribute
open Lean

namespace Lean

/--
`TagAttributeExtra` works around a limitation of `TagAttribute`, which is that definitions
must be tagged in the same file that declares the definition.
This works well for definitions in lean core, but for attributes declared outside the core
this is problematic because we may want to tag declarations created before the attribute
was defined.

To resolve this, we allow a one-time exception to the rule that attributes must be applied
in the same file as the declaration: During the declaration of the attribute itself,
we can tag arbitrary other definitions, but once the attribute is declared we must tag things
in the same file as normal.
-/
structure 
TagAttributeExtra: PersistentEnvExtension Name Name NameSet β†’ NameHashSet β†’ TagAttributeExtra
TagAttributeExtra where
  /-- The environment extension for the attribute. -/
  
ext: TagAttributeExtra β†’ PersistentEnvExtension Name Name NameSet
ext : 
PersistentEnvExtension: Type β†’ Type β†’ Type β†’ Type
PersistentEnvExtension 
Name: Type
Name 
Name: Type
Name 
NameSet: Type
NameSet
  /-- A list of "base" declarations which have been pre-tagged. -/
  
base: TagAttributeExtra β†’ NameHashSet
base : 
NameHashSet: Type
NameHashSet
  deriving 
Inhabited: Sort u β†’ Sort (max1u)
Inhabited

/--
Registers a new tag attribute. The `extra` field is a list of definitions from other modules
which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same
file as the declaration.

Note: The `extra` fields bypass the `validate` function -
we assume the builtins are also pre-validated.
-/
def 
registerTagAttributeExtra: Name β†’
  String β†’ List Name β†’ (optParam (Name β†’ AttrM Unit) fun x => pure ()) β†’ autoParam Name _auto✝ β†’ IO TagAttributeExtra
registerTagAttributeExtra (
name: Name
name : 
Name: Type
Name) (
descr: String
descr : 
String: Type
String) (
extra: List Name
extra : 
List: Type ?u.849 β†’ Type ?u.849
List 
Name: Type
Name)
    (
validate: optParam (Name β†’ AttrM Unit) fun x => pure ()
validate : 
Name: Type
Name β†’ 
AttrM: Type β†’ Type
AttrM 
Unit: Type
Unit := fun 
_: ?m.857
_ => 
pure: {f : Type ?u.860 β†’ Type ?u.859} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.860} β†’ Ξ± β†’ f Ξ±
pure 
(): Unit
()) (
ref: autoParam Name _auto✝
ref : 
Name: Type
Name := by exact decl_name%) :
    
IO: Type β†’ Type
IO 
TagAttributeExtra: Type
TagAttributeExtra := do
  let { 
ext: PersistentEnvExtension Name Name NameSet
ext, .. } ← 
registerTagAttribute: Name β†’
  String β†’
    (optParam (Name β†’ AttrM Unit) fun x => pure ()) β†’
      autoParam Name _auto✝ β†’
        optParam AttributeApplicationTime AttributeApplicationTime.afterTypeChecking β†’ IO TagAttribute
registerTagAttribute 
name: Name
name 
descr: String
descr 
validate: optParam (Name β†’ AttrM Unit) fun x => pure ()
validate 
ref: autoParam Name _auto✝
ref
  
pure: {f : Type ?u.1086 β†’ Type ?u.1085} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.1086} β†’ Ξ± β†’ f Ξ±
pure { ext, base := 
extra: List Name
extra.
foldl: {Ξ± : Type ?u.1111} β†’ {Ξ² : Type ?u.1110} β†’ (Ξ± β†’ Ξ² β†’ Ξ±) β†’ Ξ± β†’ List Ξ² β†’ Ξ±
foldl (Β·.
insert: NameHashSet β†’ Name β†’ HashSet Name
insert Β·) 
{}: ?m.1132
{} }

namespace TagAttributeExtra

/-- Does declaration `decl` have the tag `attr`? -/
def 
hasTag: TagAttributeExtra β†’ Environment β†’ Name β†’ Bool
hasTag (
attr: TagAttributeExtra
attr : 
TagAttributeExtra: Type
TagAttributeExtra) (
env: Environment
env : 
Environment: Type
Environment) (
decl: Name
decl : 
Name: Type
Name) : 
Bool: Type
Bool :=
  match 
env: Environment
env.
getModuleIdxFor?: Environment β†’ Name β†’ Option ModuleIdx
getModuleIdxFor? 
decl: Name
decl with
  | 
some: {Ξ± : Type ?u.1753} β†’ Ξ± β†’ Option Ξ±
some 
modIdx: ModuleIdx
modIdx => (
attr: TagAttributeExtra
attr.
ext: TagAttributeExtra β†’ PersistentEnvExtension Name Name NameSet
ext.
getModuleEntries: {Ξ± Ξ² Οƒ : Type} β†’ [inst : Inhabited Οƒ] β†’ PersistentEnvExtension Ξ± Ξ² Οƒ β†’ Environment β†’ ModuleIdx β†’ Array Ξ±
getModuleEntries 
env: Environment
env 
modIdx: ModuleIdx
modIdx).
binSearchContains: {Ξ± : Type} β†’ (as : Array Ξ±) β†’ Ξ± β†’ (Ξ± β†’ Ξ± β†’ Bool) β†’ optParam Nat 0 β†’ optParam Nat (Array.size as - 1) β†’ Bool
binSearchContains 
decl: Name
decl 
Name.quickLt: Name β†’ Name β†’ Bool
Name.quickLt
  | 
none: {Ξ± : Type ?u.1801} β†’ Option Ξ±
none        => (
attr: TagAttributeExtra
attr.
ext: TagAttributeExtra β†’ PersistentEnvExtension Name Name NameSet
ext.
getState: {Ξ± Ξ² Οƒ : Type} β†’ [inst : Inhabited Οƒ] β†’ PersistentEnvExtension Ξ± Ξ² Οƒ β†’ Environment β†’ Οƒ
getState 
env: Environment
env).
contains: NameSet β†’ Name β†’ Bool
contains 
decl: Name
decl
  || 
attr: TagAttributeExtra
attr.
base: TagAttributeExtra β†’ NameHashSet
base.
contains: NameHashSet β†’ Name β†’ Bool
contains 
decl: Name
decl

/-- Get the list of declarations tagged with the tag attribute `attr`. -/
def 
getDecls: TagAttributeExtra β†’ Environment β†’ Array Name
getDecls (
attr: TagAttributeExtra
attr : 
TagAttributeExtra: Type
TagAttributeExtra) (
env: Environment
env : 
Environment: Type
Environment) : 
Array: Type ?u.2263 β†’ Type ?u.2263
Array 
Name: Type
Name := 
Id.run: {Ξ± : Type ?u.2267} β†’ Id Ξ± β†’ Ξ±
Id.run do
  let 
decls: ?m.2288
decls := 
TagAttribute.getDecls.core: PersistentEnvExtensionState Name NameSet β†’ Array Name
TagAttribute.getDecls.core <| 
attr: TagAttributeExtra
attr.
ext: TagAttributeExtra β†’ PersistentEnvExtension Name Name NameSet
ext.
toEnvExtension: {Ξ± Ξ² Οƒ : Type} β†’ PersistentEnvExtension Ξ± Ξ² Οƒ β†’ EnvExtension (PersistentEnvExtensionState Ξ± Οƒ)
toEnvExtension.
getState: {Οƒ : Type} β†’ [inst : Inhabited Οƒ] β†’ EnvExtension Οƒ β†’ Environment β†’ Οƒ
getState 
env: Environment
env
  
attr: TagAttributeExtra
attr.
base: TagAttributeExtra β†’ NameHashSet
base.
fold: {Ξ± : Type ?u.2316} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ {Ξ΄ : Type ?u.2315} β†’ (Ξ΄ β†’ Ξ± β†’ Ξ΄) β†’ Ξ΄ β†’ HashSet Ξ± β†’ Ξ΄
fold (Β·.
push: {Ξ± : Type ?u.2334} β†’ Array Ξ± β†’ Ξ± β†’ Array Ξ±
push Β·) 
decls: ?m.2288
decls

end TagAttributeExtra

/--
`ParametricAttributeExtra` works around a limitation of `ParametricAttribute`, which is that
definitions must be tagged in the same file that declares the definition.
This works well for definitions in lean core, but for attributes declared outside the core
this is problematic because we may want to tag declarations created before the attribute
was defined.

To resolve this, we allow a one-time exception to the rule that attributes must be applied
in the same file as the declaration: During the declaration of the attribute itself,
we can tag arbitrary other definitions, but once the attribute is declared we must tag things
in the same file as normal.
-/
structure 
ParametricAttributeExtra: Type β†’ Type
ParametricAttributeExtra (
Ξ±: Type
Ξ± : 
Type: Type 1
Type) where
  /-- The underlying `ParametricAttribute`. -/
  
attr: {Ξ± : Type} β†’ ParametricAttributeExtra Ξ± β†’ ParametricAttribute Ξ±
attr : 
ParametricAttribute: Type β†’ Type
ParametricAttribute 
Ξ±: Type
Ξ±
  /-- A list of pre-tagged declarations with their values. -/
  
base: {Ξ± : Type} β†’ ParametricAttributeExtra Ξ± β†’ HashMap Name Ξ±
base : 
HashMap: (Ξ± : Type ?u.2841) β†’ Type ?u.2840 β†’ [inst : BEq Ξ±] β†’ [inst : Hashable Ξ±] β†’ Type (max0?u.2841?u.2840)
HashMap 
Name: Type
Name 
Ξ±: Type
Ξ±
  deriving 
Inhabited: Sort u β†’ Sort (max1u)
Inhabited

/--
Registers a new parametric attribute. The `extra` field is a list of definitions from other modules
which will be "pre-tagged" and are not subject to the usual restriction on tagging in the same
file as the declaration.
-/
def 
registerParametricAttributeExtra: {Ξ± : Type} β†’ [inst : Inhabited Ξ±] β†’ ParametricAttributeImpl Ξ± β†’ List (Name Γ— Ξ±) β†’ IO (ParametricAttributeExtra Ξ±)
registerParametricAttributeExtra [
Inhabited: Sort ?u.4008 β†’ Sort (max1?u.4008)
Inhabited 
Ξ±: ?m.4005
Ξ±] (
impl: ParametricAttributeImpl Ξ±
impl : 
ParametricAttributeImpl: Type β†’ Type
ParametricAttributeImpl 
Ξ±: ?m.4005
Ξ±)
    (
extra: List (Name Γ— Ξ±)
extra : 
List: Type ?u.4013 β†’ Type ?u.4013
List (
Name: Type
Name Γ— 
Ξ±: ?m.4005
Ξ±)) : 
IO: Type β†’ Type
IO (
ParametricAttributeExtra: Type β†’ Type
ParametricAttributeExtra 
Ξ±: ?m.4005
Ξ±) := do
  let 
attr: ?m.4158
attr ← 
registerParametricAttribute: {Ξ± : Type} β†’ [inst : Inhabited Ξ±] β†’ ParametricAttributeImpl Ξ± β†’ IO (ParametricAttribute Ξ±)
registerParametricAttribute 
impl: ParametricAttributeImpl Ξ±
impl
  
pure: {f : Type ?u.4161 β†’ Type ?u.4160} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.4161} β†’ Ξ± β†’ f Ξ±
pure { 
attr: ?m.4158
attr, base := 
extra: List (Name Γ— Ξ±)
extra.
foldl: {Ξ± : Type ?u.4189} β†’ {Ξ² : Type ?u.4188} β†’ (Ξ± β†’ Ξ² β†’ Ξ±) β†’ Ξ± β†’ List Ξ² β†’ Ξ±
foldl (fun 
s: ?m.4198
s (
a: Name
a, 
b: Ξ±
b) => 
s: ?m.4198
s.
insert: {Ξ± : Type ?u.4285} β†’ {Ξ² : Type ?u.4284} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ HashMap Ξ± Ξ² β†’ Ξ± β†’ Ξ² β†’ HashMap Ξ± Ξ²
insert 
a: Name
a 
b: Ξ±
b) 
{}: ?m.4210
{} }

namespace ParametricAttributeExtra

/--
Gets the parameter of attribute `attr` associated to declaration `decl`,
or `none` if `decl` is not tagged.
-/
def 
getParam?: {Ξ± : Type} β†’ [inst : Inhabited Ξ±] β†’ ParametricAttributeExtra Ξ± β†’ Environment β†’ Name β†’ Option Ξ±
getParam? [
Inhabited: Sort ?u.4615 β†’ Sort (max1?u.4615)
Inhabited 
Ξ±: ?m.4612
Ξ±] (
attr: ParametricAttributeExtra Ξ±
attr : 
ParametricAttributeExtra: Type β†’ Type
ParametricAttributeExtra 
Ξ±: ?m.4612
Ξ±)
    (
env: Environment
env : 
Environment: Type
Environment) (
decl: Name
decl : 
Name: Type
Name) : 
Option: Type ?u.4624 β†’ Type ?u.4624
Option 
Ξ±: ?m.4612
Ξ± :=
  
attr: ParametricAttributeExtra Ξ±
attr.
attr: {Ξ± : Type} β†’ ParametricAttributeExtra Ξ± β†’ ParametricAttribute Ξ±
attr.
getParam?: {Ξ± : Type} β†’ [inst : Inhabited Ξ±] β†’ ParametricAttribute Ξ± β†’ Environment β†’ Name β†’ Option Ξ±
getParam? 
env: Environment
env 
decl: Name
decl <|> 
attr: ParametricAttributeExtra Ξ±
attr.
base: {Ξ± : Type} β†’ ParametricAttributeExtra Ξ± β†’ HashMap Name Ξ±
base.
find?: {Ξ± : Type ?u.4650} β†’ {Ξ² : Type ?u.4649} β†’ {x : BEq Ξ±} β†’ {x_1 : Hashable Ξ±} β†’ HashMap Ξ± Ξ² β†’ Ξ± β†’ Option Ξ²
find? 
decl: Name
decl

/-- Applies attribute `attr` to declaration `decl`, given a value for the parameter. -/
def 
setParam: {Ξ± : Type} β†’ ParametricAttributeExtra Ξ± β†’ Environment β†’ Name β†’ Ξ± β†’ Except String Environment
setParam (
attr: ParametricAttributeExtra Ξ±
attr : 
ParametricAttributeExtra: Type β†’ Type
ParametricAttributeExtra 
Ξ±: ?m.4807
Ξ±)
    (
env: Environment
env : 
Environment: Type
Environment) (
decl: Name
decl : 
Name: Type
Name) (
param: Ξ±
param : 
Ξ±: ?m.4807
Ξ±) : 
Except: Type ?u.4819 β†’ Type ?u.4818 β†’ Type (max?u.4819?u.4818)
Except 
String: Type
String 
Environment: Type
Environment :=
  
attr: ParametricAttributeExtra Ξ±
attr.
attr: {Ξ± : Type} β†’ ParametricAttributeExtra Ξ± β†’ ParametricAttribute Ξ±
attr.
setParam: {Ξ± : Type} β†’ ParametricAttribute Ξ± β†’ Environment β†’ Name β†’ Ξ± β†’ Except String Environment
setParam 
env: Environment
env 
decl: Name
decl 
param: Ξ±
param

end ParametricAttributeExtra