doc: docstrings for decls and attributes

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

src/Lean/Attributes.lean

@@ -35,6 +35,7 @@ instance : ToString AttributeKind where
     | AttributeKind.scoped => "scoped"
 
 structure AttributeImpl extends AttributeImplCore where
+  /-- This is run when the attribute is applied to a declaration `decl`. `stx` is the syntax of the attribute including arguments. -/
   add (decl : Name) (stx : Syntax) (kind : AttributeKind) : AttrM Unit
   erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased"
   deriving Inhabited

src/Lean/CoreM.lean

@@ -31,6 +31,7 @@ structure Cache where
   instLevelValue : InstantiateLevelCache := {}
   deriving Inhabited
 
+/-- State for the CoreM monad. -/
 structure State where
   env             : Environment
   nextMacroScope  : MacroScope    := firstFrontendMacroScope + 1
@@ -39,6 +40,7 @@ structure State where
   cache           : Cache         := {}
   deriving Inhabited
 
+/-- Context for the CoreM monad. -/
 structure Context where
   options        : Options := {}
   currRecDepth   : Nat := 0
@@ -50,6 +52,14 @@ structure Context where
   maxHeartbeats  : Nat := getMaxHeartbeats options
   currMacroScope : MacroScope := firstFrontendMacroScope
 
+/-- CoreM is a monad for manipulating the Lean environment.
+It is the base monad for `MetaM`.
+The main features it provides are:
+- name generator state
+- environment state
+- Lean options context
+- the current open namespace
+-/
 abbrev CoreM := ReaderT Context <| StateRefT State (EIO Exception)
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the

src/Lean/Declaration.lean

@@ -192,13 +192,23 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool
     A series of checks are performed by the kernel to check whether a `inductiveDecls`
     is valid or not. -/
 structure InductiveVal extends ConstantVal where
-  numParams : Nat     -- Number of parameters
-  numIndices : Nat    -- Number of indices
-  all : List Name     -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
-  ctors : List Name   -- List of all constructors for this inductive datatype
-  isRec : Bool        -- `true` Iff it is recursive
+  /-- Number of parameters. A parameter is an argument to the defined type that is fixed over constructors.  -/
+  numParams : Nat
+  /-- Number of indices. An index is an argument that varies over constructors.
+
+  An example of this is the `n : Nat` argument in the vector constructor `cons : α → Vector α n → Vector α (n+1)` -/
+  numIndices : Nat
+  /-- List of all (including this one) inductive datatypes in the mutual declaration containing this one -/
+  all : List Name
+  /-- List of the names of the constructors for this inductive datatype. -/
+  ctors : List Name
+  /-- `true` when recursive (that is, the inductive type appears as an argument in a constructor). -/
+  isRec : Bool
+  /-- Whether the definition is flagged as unsafe. -/
   isUnsafe : Bool
   isReflexive : Bool
+  /-- An inductive definition `T` is nested when there is a constructor with an argument `x : F T`,
+   where `F : Type → Type` is some suitably behaved (ie strictly positive) function (Eg `Array T`, `List T`, `T × T`, ...). -/
   isNested : Bool
   deriving Inhabited
 
@@ -226,10 +236,14 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP
 def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length
 
 structure ConstructorVal extends ConstantVal where
-  induct  : Name    -- Inductive Type this Constructor is a member of
-  cidx    : Nat     -- Constructor index (i.e., Position in the inductive declaration)
-  numParams : Nat   -- Number of parameters in inductive datatype `induct`
-  numFields : Nat   -- Number of fields (i.e., arity - nparams)
+  /-- Inductive type this constructor is a member of -/
+  induct  : Name
+  /-- Constructor index (i.e., Position in the inductive declaration) -/
+  cidx    : Nat
+  /-- Number of parameters in inductive datatype. -/
+  numParams : Nat
+  /-- Number of fields (i.e., arity - nparams) -/
+  numFields : Nat
   isUnsafe : Bool
   deriving Inhabited
 
@@ -249,19 +263,29 @@ def mkConstructorValEx (name : Name) (levelParams : List Name) (type : Expr) (in
 
 /-- Information for reducing a recursor -/
 structure RecursorRule where
-  ctor : Name   -- Reduction rule for this Constructor
-  nfields : Nat -- Number of fields (i.e., without counting inductive datatype parameters)
-  rhs : Expr    -- Right hand side of the reduction rule
+  /-- Reduction rule for this Constructor -/
+  ctor : Name
+  /-- Number of fields (i.e., without counting inductive datatype parameters) -/
+  nfields : Nat
+  /-- Right hand side of the reduction rule -/
+  rhs : Expr
   deriving Inhabited
 
 structure RecursorVal extends ConstantVal where
-  all : List Name              -- List of all inductive datatypes in the mutual declaration that generated this recursor
-  numParams : Nat              -- Number of parameters
-  numIndices : Nat             -- Number of indices
-  numMotives : Nat             -- Number of motives
-  numMinors : Nat              -- Number of minor premises
-  rules : List RecursorRule    -- A reduction for each Constructor
-  k : Bool                     -- It supports K-like reduction
+  /-- List of all inductive datatypes in the mutual declaration that generated this recursor -/
+  all : List Name
+  /-- Number of parameters -/
+  numParams : Nat
+  /-- Number of indices -/
+  numIndices : Nat
+  /-- Number of motives -/
+  numMotives : Nat
+  /-- Number of minor premises -/
+  numMinors : Nat
+  /-- A reduction for each Constructor -/
+  rules : List RecursorRule
+  /-- It supports K-like reduction -/
+  k : Bool
   isUnsafe : Bool
   deriving Inhabited
 

src/Lean/Elab/DeclModifiers.lean

@@ -26,6 +26,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] (declName
     if env.contains declName then
       throwError "a non-private declaration '{declName}' has already been declared"
 
+/-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/
 inductive Visibility where
   | regular | «protected» | «private»
   deriving Inhabited
@@ -35,10 +36,12 @@ instance : ToString Visibility := ⟨fun
   | Visibility.«private»   => "private"
   | Visibility.«protected» => "protected"⟩
 
+/-- Whether a declaration is default, partial or nonrec. -/
 inductive RecKind where
   | «partial» | «nonrec» | default
   deriving Inhabited
 
+/-- Flags and data added to declarations (eg docstrings, attributes, `private`, `unsafe`, `partial`, ...). -/
 structure Modifiers where
   docString?      : Option String := none
   visibility      : Visibility := Visibility.regular

src/Lean/ResolveName.lean

@@ -141,7 +141,7 @@ def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDec
   | OpenDecl.simple ns [] :: ds =>  if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls env n ds
   | _ :: ds                     => resolveNamespaceUsingOpenDecls env n ds
 
-/-
+/--
 Given a name `id` try to find namespace it refers to. The resolution procedure works as follows
 1- If `id` is in the scope of `namespace` commands the namespace `s_1. ... . s_n`,
    then return `s_1 . ... . s_i ++ n` if it is the name of an existing namespace. We search "backwards".
@@ -170,7 +170,7 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
   getCurrNamespace := liftM (m:=m) getCurrNamespace
   getOpenDecls     := liftM (m:=m) getOpenDecls
 
-/-
+/--
   Given a name `n`, return a list of possible interpretations.
   Each interpretation is a pair `(declName, fieldList)`, where `declName`
   is the name of a declaration in the current environment, and `fieldList` are
@@ -187,6 +187,7 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
   - `resolveGlobalName x`     => `[(Foo.x, [])]`
   - `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
   - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w])]`
+
   After `open Foo open Boo`, we have
   - `resolveGlobalName x`     => `[(Foo.x, []), (Boo.x, [])]`
   - `resolveGlobalName x.y`   => `[(Foo.x.y, [])]`
@@ -195,12 +196,14 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
 def resolveGlobalName [Monad m] [MonadResolveName m] [MonadEnv m] (id : Name) : m (List (Name × List String)) := do
   return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id
 
+
 def resolveNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) : m Name := do
   match ResolveName.resolveNamespace? (← getEnv) (← getCurrNamespace) (← getOpenDecls) id with
   | some ns => return ns
   | none    => throwError s!"unknown namespace '{id}'"
 
-/--
+/-- Given a name `n`, return a list of possible interpretations for global constants.
+
 Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty.
 For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/
 def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do
@@ -216,6 +219,27 @@ def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m]
   | [c] => pure c
   | _   => throwError s!"ambiguous identifier '{mkConst n}', possible interpretations: {cs.map mkConst}"
 
+/-- Interpret the syntax `n` as an identifier for a global constant, and return a list of resolved
+constant names that it could be refering to based on the currently open namespaces.
+This should be used instead of `resolveGlobalConstCore` for identifiers taken from syntax
+because `Syntax` objects may have names that have already been resolved.
+
+## Example:
+```
+def Boo.x   := 1
+def Foo.x   := 2
+def Foo.x.y := 3
+```
+After `open Foo`, we have
+- `resolveGlobalConst x`     => `[Foo.x]`
+- `resolveGlobalConst x.y`   => `[Foo.x.y]`
+- `resolveGlobalConst x.z.w` => error: unknown constant
+
+After `open Foo open Boo`, we have
+- `resolveGlobalConst x`     => `[Foo.x, Boo.x]`
+- `resolveGlobalConst x.y`   => `[Foo.x.y]`
+- `resolveGlobalConst x.z.w` => error: unknown constant
+-/
 def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m (List Name)
   | stx@(Syntax.ident _ _ n pre) => do
     let pre := pre.filterMap fun (n, fields) => if fields.isEmpty then some n else none
@@ -225,6 +249,25 @@ def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m
       return pre
   | stx => throwErrorAt stx s!"expected identifier"
 
+/-- Interpret the syntax `n` as an identifier for a global constant, and return a resolved
+constant name. If there are multiple possible interpretations it will throw.
+
+## Example:
+```
+def Boo.x   := 1
+def Foo.x   := 2
+def Foo.x.y := 3
+```
+After `open Foo`, we have
+- `resolveGlobalConstNoOverload x`     => `Foo.x`
+- `resolveGlobalConstNoOverload x.y`   => `Foo.x.y`
+- `resolveGlobalConstNoOverload x.z.w` => error: unknown constant
+
+After `open Foo open Boo`, we have
+- `resolveGlobalConstNoOverload x`     => error: ambiguous identifier
+- `resolveGlobalConstNoOverload x.y`   => `Foo.x.y`
+- `resolveGlobalConstNoOverload x.z.w` => error: unknown constant
+-/
 def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do
   let cs ← resolveGlobalConst id
   match cs with