Lean.Elab.DeclModifiers

Lean.Elab.instInhabitedModifiers = { default := { docString? := default, visibility := default, isNoncomputable := default, recKind := default, isUnsafe := default, attrs := default } }

source

def Lean.Elab.Modifiers.isPrivate :

Lean.Elab.Modifiers → Bool

Equations

Lean.Elab.Modifiers.isPrivate x = match x with | { docString? := x, visibility := Lean.Elab.Visibility.private, isNoncomputable := x_1, recKind := x_2, isUnsafe := x_3, attrs := x_4 } => true | x => false

source

def Lean.Elab.Modifiers.isProtected :

Lean.Elab.Modifiers → Bool

Equations

Lean.Elab.Modifiers.isProtected x = match x with | { docString? := x, visibility := Lean.Elab.Visibility.protected, isNoncomputable := x_1, recKind := x_2, isUnsafe := x_3, attrs := x_4 } => true | x => false

source

def Lean.Elab.Modifiers.isPartial :

Lean.Elab.Modifiers → Bool

Equations

Lean.Elab.Modifiers.isPartial x = match x with | { docString? := x, visibility := x_1, isNoncomputable := x_2, recKind := Lean.Elab.RecKind.partial, isUnsafe := x_3, attrs := x_4 } => true | x => false

source

def Lean.Elab.Modifiers.isNonrec :

Lean.Elab.Modifiers → Bool

Equations

Lean.Elab.Modifiers.isNonrec x = match x with | { docString? := x, visibility := x_1, isNoncomputable := x_2, recKind := Lean.Elab.RecKind.nonrec, isUnsafe := x_3, attrs := x_4 } => true | x => false

source

def Lean.Elab.Modifiers.addAttribute (modifiers : Lean.Elab.Modifiers) (attr : Lean.Elab.Attribute) :

Lean.Elab.Modifiers

Equations

Lean.Elab.Modifiers.addAttribute modifiers attr = { docString? := modifiers.docString?, visibility := modifiers.visibility, isNoncomputable := modifiers.isNoncomputable, recKind := modifiers.recKind, isUnsafe := modifiers.isUnsafe, attrs := Array.push modifiers.attrs attr }

source

instance Lean.Elab.instToFormatModifiers :

Lean.ToFormat Lean.Elab.Modifiers

Equations

Lean.Elab.instToFormatModifiers = { format := fun m => let components := (((((match m.docString? with | some str => [Lean.format "/--" ++ Lean.format str ++ Lean.format "-/"] | none => []) ++ match m.visibility with | Lean.Elab.Visibility.regular => [] | Lean.Elab.Visibility.protected => [Lean.format "protected"] | Lean.Elab.Visibility.private => [Lean.format "private"]) ++ if m.isNoncomputable = true then [Lean.format "noncomputable"] else []) ++ match m.recKind with | Lean.Elab.RecKind.partial => [Lean.format "partial"] | Lean.Elab.RecKind.nonrec => [Lean.format "nonrec"] | x => []) ++ if m.isUnsafe = true then [Lean.format "unsafe"] else []) ++ List.map (fun attr => Lean.format attr) (Array.toList m.attrs); Lean.Format.bracket "{" (Lean.Format.joinSep components (Std.Format.text "," ++ Lean.Format.line)) "}" }

source

instance Lean.Elab.instToStringModifiers :

ToString Lean.Elab.Modifiers

Equations

Lean.Elab.instToStringModifiers = { toString := toString ∘ Lean.format }

source

def Lean.Elab.expandOptDocComment? {m : Type → Type} [inst : Monad m] [inst : Lean.MonadError m] (optDocComment : Lean.Syntax) :

m (Option String)

Equations

Lean.Elab.expandOptDocComment? optDocComment = match Lean.Syntax.getOptional? optDocComment with | none => pure none | some s => match Lean.Syntax.getOp s 1 with | Lean.Syntax.atom x val => pure (some (String.extract val 0 (String.bsize val - 2))) | x => Lean.throwErrorAt s (Lean.toMessageData "unexpected doc string" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.ofSyntax (Lean.Syntax.getOp s 1))) ++ Lean.toMessageData "")

source

def Lean.Elab.elabModifiers {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadResolveName m] [inst : Lean.MonadError m] [inst : Lean.Elab.MonadMacroAdapter m] [inst : Lean.MonadRecDepth m] [inst : Lean.MonadTrace m] [inst : Lean.MonadOptions m] [inst : Lean.AddMessageContext m] (stx : Lean.Syntax) :

m Lean.Elab.Modifiers

Equations

Lean.Elab.elabModifiers stx = let docCommentStx := Lean.Syntax.getOp stx 0; let attrsStx := Lean.Syntax.getOp stx 1; let visibilityStx := Lean.Syntax.getOp stx 2; let noncompStx := Lean.Syntax.getOp stx 3; let unsafeStx := Lean.Syntax.getOp stx 4; let recKind := if Lean.Syntax.isNone (Lean.Syntax.getOp stx 5) = true then Lean.Elab.RecKind.default else if (Lean.Syntax.getKind (Lean.Syntax.getOp (Lean.Syntax.getOp stx 5) 0) == `Lean.Parser.Command.partial) = true then Lean.Elab.RecKind.partial else Lean.Elab.RecKind.nonrec; let _do_jp := fun docString? => let _do_jp := fun visibility => let _do_jp := fun attrs => pure { docString? := docString?, visibility := visibility, isNoncomputable := !Lean.Syntax.isNone noncompStx, recKind := recKind, isUnsafe := !Lean.Syntax.isNone unsafeStx, attrs := attrs }; match Lean.Syntax.getOptional? attrsStx with | none => do let y ← pure #[] _do_jp y | some attrs => do let y ← Lean.Elab.elabDeclAttrs attrs _do_jp y; match Lean.Syntax.getOptional? visibilityStx with | none => do let y ← pure Lean.Elab.Visibility.regular _do_jp y | some v => let kind := Lean.Syntax.getKind v; if (kind == `Lean.Parser.Command.private) = true then do let y ← pure Lean.Elab.Visibility.private _do_jp y else if (kind == `Lean.Parser.Command.protected) = true then do let y ← pure Lean.Elab.Visibility.protected _do_jp y else do let y ← Lean.throwErrorAt v (Lean.toMessageData "unexpected visibility modifier") _do_jp y; match Lean.Syntax.getOptional? docCommentStx with | none => do let y ← pure none _do_jp y | some s => match Lean.Syntax.getOp s 1 with | Lean.Syntax.atom x val => do let y ← pure (some (String.extract val 0 (String.bsize val - 2))) _do_jp y | x => do let y ← Lean.throwErrorAt s (Lean.toMessageData "unexpected doc string" ++ Lean.toMessageData (Lean.indentD (Lean.MessageData.ofSyntax (Lean.Syntax.getOp s 1))) ++ Lean.toMessageData "") _do_jp y

source

def Lean.Elab.applyVisibility {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (visibility : Lean.Elab.Visibility) (declName : Lean.Name) :

m Lean.Name

Equations

Lean.Elab.applyVisibility visibility declName = match visibility with | Lean.Elab.Visibility.private => do let env ← Lean.getEnv let declName : Lean.Name := Lean.mkPrivateName env declName Lean.Elab.checkNotAlreadyDeclared declName pure declName | Lean.Elab.Visibility.protected => do Lean.Elab.checkNotAlreadyDeclared declName let env ← Lean.getEnv let env : Lean.Environment := Lean.addProtected env declName Lean.setEnv env pure declName | x => do Lean.Elab.checkNotAlreadyDeclared declName pure declName

source

def Lean.Elab.checkIfShadowingStructureField {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (declName : Lean.Name) :

m Unit

Equations

Lean.Elab.checkIfShadowingStructureField declName = match declName with | Lean.Name.str pre x x_1 => do let a ← Lean.getEnv if Lean.isStructure a pre = true then do let a ← Lean.getEnv let fieldNames : Array Lean.Name := Lean.getStructureFieldsFlattened a pre let r ← forIn fieldNames PUnit.unit fun fieldName r => if (pre ++ fieldName == declName) = true then do Lean.throwError (Lean.toMessageData "invalid declaration name '" ++ Lean.toMessageData declName ++ Lean.toMessageData "', structure '" ++ Lean.toMessageData pre ++ Lean.toMessageData "' has field '" ++ Lean.toMessageData fieldName ++ Lean.toMessageData "'") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit else pure PUnit.unit | x => pure ()

source

def Lean.Elab.mkDeclName {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (currNamespace : Lean.Name) (modifiers : Lean.Elab.Modifiers) (shortName : Lean.Name) :

m (Lean.Name × Lean.Name)

Equations

Lean.Elab.mkDeclName currNamespace modifiers shortName = let name := (Lean.extractMacroScopes shortName).name; let _do_jp := fun y => let declName := currNamespace ++ shortName; do Lean.Elab.checkIfShadowingStructureField declName let declName ← Lean.Elab.applyVisibility modifiers.visibility declName match modifiers.visibility with | Lean.Elab.Visibility.protected => match currNamespace with | Lean.Name.str x s x_1 => pure (declName, Lean.Name.mkSimple s ++ shortName) | x => Lean.throwError (Lean.toMessageData "protected declarations must be in a namespace") | x => pure (declName, shortName); if (Lean.Name.isAtomic name || Lean.Elab.isFreshInstanceName name) = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "atomic identifier expected '" ++ Lean.toMessageData shortName ++ Lean.toMessageData "'") _do_jp y

source

def Lean.Elab.expandDeclIdCore (declId : Lean.Syntax) :

Lean.Name × Lean.Syntax

Equations

Lean.Elab.expandDeclIdCore declId = if Lean.Syntax.isIdent declId = true then (Lean.Syntax.getId declId, Lean.mkNullNode) else let id := Lean.Syntax.getId (Lean.Syntax.getOp declId 0); let optUnivDeclStx := Lean.Syntax.getOp declId 1; (id, optUnivDeclStx)

source

structure Lean.Elab.ExpandDeclIdResult :

Type

shortName : Lean.Name
declName : Lean.Name
levelNames : List Lean.Name

source

def Lean.Elab.expandDeclId {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] (currNamespace : Lean.Name) (currLevelNames : List Lean.Name) (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) :

m Lean.Elab.ExpandDeclIdResult

Equations

Lean.Elab.expandDeclId currNamespace currLevelNames declId modifiers = let x := Lean.Elab.expandDeclIdCore declId; match x with | (shortName, optUnivDeclStx) => let _do_jp := fun levelNames => do let discr ← Lean.withRef declId (Lean.Elab.mkDeclName currNamespace modifiers shortName) let x : Lean.Name × Lean.Name := discr match x with | (declName, shortName) => do Lean.addDocString' declName modifiers.docString? pure { shortName := shortName, declName := declName, levelNames := levelNames }; if Lean.Syntax.isNone optUnivDeclStx = true then do let y ← pure currLevelNames _do_jp y else let extraLevels := Array.getEvenElems (Lean.Syntax.getArgs (Lean.Syntax.getOp optUnivDeclStx 1)); do let y ← Array.foldlM (fun levelNames idStx => let id := Lean.Syntax.getId idStx; if List.elem id levelNames = true then Lean.withRef idStx (Lean.Elab.throwAlreadyDeclaredUniverseLevel id) else pure (id :: levelNames)) currLevelNames extraLevels 0 (Array.size extraLevels) _do_jp y