Documentation

Lean.Hygiene

structure Lean.Unhygienic.Context :

Type

ref : Lean.Syntax
scope : Lean.MacroScope

@[inline]

abbrev Lean.Unhygienic (α : Type) :

Type

Equations

Lean.Unhygienic = ReaderT Lean.Unhygienic.Context (StateM Lean.MacroScope)

instance Lean.Unhygienic.instMonadQuotationUnhygienic :

Lean.MonadQuotation Lean.Unhygienic

Equations

Lean.Unhygienic.instMonadQuotationUnhygienic = Lean.MonadQuotation.mk (do let a ← read pure a.scope) (pure `UnhygienicMain) fun {α} x => do let fresh ← modifyGet fun n => (n, n + 1) withReader (fun a => { ref := a.ref, scope := fresh }) x

def Lean.Unhygienic.run {α : Type} (x : Lean.Unhygienic α) :

α

Equations

Lean.Unhygienic.run x = StateT.run' (x { ref := Lean.Syntax.missing, scope := Lean.firstFrontendMacroScope }) (Lean.firstFrontendMacroScope + 1)

def Lean.sanitizeNamesDefault :

Equations

Lean.sanitizeNamesDefault = true

def Lean.getSanitizeNames (o : Lean.Options) :

Equations

Lean.getSanitizeNames o = Lean.KVMap.get o `pp.sanitizeNames Lean.sanitizeNamesDefault

structure Lean.NameSanitizerState :

Type

options : Lean.Options
nameStem2Idx : Lean.NameMap Nat
userName2Sanitized : Lean.NameMap Lean.Name

def Lean.sanitizeName (userName : Lean.Name) :

StateM Lean.NameSanitizerState Lean.Name

Equations

Lean.sanitizeName userName = let stem := Lean.Name.eraseMacroScopes userName; do let a ← get let idx : Nat := Option.getD (Lean.NameMap.find? a.nameStem2Idx stem) 0 let san ← Lean.mkFreshInaccessibleUserName stem idx modify fun s => { options := s.options, nameStem2Idx := s.nameStem2Idx, userName2Sanitized := Lean.NameMap.insert s.userName2Sanitized userName san } pure san

def Lean.sanitizeSyntax (stx : Lean.Syntax) :

StateM Lean.NameSanitizerState Lean.Syntax

Equations

Lean.sanitizeSyntax stx = do let a ← get if Lean.getSanitizeNames a.options = true then Lean.sanitizeSyntaxAux stx else pure stx