doc: some doc strings

src/Lean/Class.lean

@@ -7,7 +7,9 @@ import Lean.Attributes
 
 namespace Lean
 
+/-- An entry for the persistent environment extension for declared type classes -/
 structure ClassEntry where
+  /-- Class name. -/
   name      : Name
   /--
     Position of the class `outParams`.
@@ -26,6 +28,7 @@ def lt (a b : ClassEntry) : Bool :=
 
 end ClassEntry
 
+/-- State of the type class environment extension. -/
 structure ClassState where
   outParamMap : SMap Name (Array Nat) := SMap.empty
   deriving Inhabited
@@ -35,29 +38,37 @@ namespace ClassState
 def addEntry (s : ClassState) (entry : ClassEntry) : ClassState :=
   { s with outParamMap := s.outParamMap.insert entry.name entry.outParams }
 
+/--
+Switch the state into persistent mode. We switch to this mode after
+we read all imported .olean files.
+Recall that we use a `SMap` for implementing the state of the type class environment extension.
+-/
 def switch (s : ClassState) : ClassState :=
   { s with outParamMap := s.outParamMap.switch }
 
 end ClassState
 
-/- TODO: add support for scoped instances -/
+/--
+Type class environment extension
+-/
+-- TODO: add support for scoped instances
 builtin_initialize classExtension : SimplePersistentEnvExtension ClassEntry ClassState ←
   registerSimplePersistentEnvExtension {
     name          := `classExt
     addEntryFn    := ClassState.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries ClassState.addEntry {} es).switch
   }
 
+/-- Return `true` if `n` is the name of type class in the given environment. -/
 @[export lean_is_class]
 def isClass (env : Environment) (n : Name) : Bool :=
   (classExtension.getState env).outParamMap.contains n
 
-/--
-  If `declName` is a class, return the position of its `outParams`.
--/
+/-- If `declName` is a class, return the position of its `outParams`. -/
 def getOutParamPositions? (env : Environment) (declName : Name) : Option (Array Nat) :=
   (classExtension.getState env).outParamMap.find? declName
 
+/-- Return `true` if the given `declName` is a type class with output parameters. -/
 @[export lean_has_out_params]
 def hasOutParams (env : Environment) (declName : Name) : Bool :=
   match getOutParamPositions? env declName with
@@ -90,6 +101,13 @@ private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (ou
       checkOutParam (i+1) outParamFVarIds outParams b
   | _ => return outParams
 
+/--
+Add a new type class with the given name to the environment.
+`declName` must not be the name of an existing type class,
+and it must be the name of constant in `env`.
+`declName` must be a inductive datatype or axiom.
+Recall that all structures are inductive datatypes.
+-/
 def addClass (env : Environment) (clsName : Name) : Except String Environment := do
   if isClass env clsName then
     throw s!"class has already been declared '{clsName}'"
@@ -100,24 +118,6 @@ def addClass (env : Environment) (clsName : Name) : Except String Environment :=
   let outParams ← checkOutParam 0 #[] #[] decl.type
   return classExtension.addEntry env { name := clsName, outParams }
 
-private def consumeNLambdas : Nat → Expr → Option Expr
-  | 0,   e            => some e
-  | i+1, .lam _ _ b _ => consumeNLambdas i b
-  | _,   _            => none
-
-partial def getClassName (env : Environment) : Expr → Option Name
-  | .forallE _ _ b _ => getClassName env b
-  | e                => do
-    let Expr.const c _ ← pure e.getAppFn | none
-    let info ← env.find? c
-    match info.value? with
-    | some val => do
-      let body ← consumeNLambdas e.getAppNumArgs val
-      getClassName env body
-    | none =>
-      if isClass env c then some c
-      else none
-
 builtin_initialize
   registerBuiltinAttribute {
     name  := `class

src/Lean/CoreM.lean

@@ -28,19 +28,27 @@ def getMaxHeartbeats (opts : Options) : Nat :=
 
 abbrev InstantiateLevelCache := Std.PersistentHashMap Name (List Level × Expr)
 
+/-- Cache for the `CoreM` monad -/
 structure Cache where
   instLevelType  : InstantiateLevelCache := {}
   instLevelValue : InstantiateLevelCache := {}
   deriving Inhabited
 
 /-- State for the CoreM monad. -/
 structure State where
+  /-- Current environment. -/
   env             : Environment
+  /-- Next macro scope. We use macro scopes to avoid accidental name capture. -/
   nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1
+  /-- Name generator for producing unique `FVarId`s, `MVarId`s, and `LMVarId`s -/
   ngen            : NameGenerator  := {}
+  /-- Trace messages -/
   traceState      : TraceState     := {}
+  /-- Cache for instantiating universe polymorphic declarations. -/
   cache           : Cache          := {}
+  /-- Message log. -/
   messages        : MessageLog     := {}
+  /-- Info tree. We have the info tree here because we want to update it while adding attributes. -/
   infoState       : Elab.InfoState := {}
   deriving Inhabited
 

src/Lean/Data/KVMap.lean

@@ -7,6 +7,7 @@ import Lean.Data.Name
 
 namespace Lean
 
+/-- Value stored in a key-value map. -/
 inductive DataValue where
   | ofString (v : String)
   | ofBool   (v : Bool)
@@ -26,36 +27,40 @@ def DataValue.beqExp (a b : DataValue) : Bool :=
   | _                  => false
 
 def DataValue.sameCtor : DataValue → DataValue → Bool
-  | DataValue.ofString _, DataValue.ofString _ => true
-  | DataValue.ofBool _,   DataValue.ofBool _   => true
-  | DataValue.ofName _,   DataValue.ofName _   => true
-  | DataValue.ofNat _,    DataValue.ofNat _    => true
-  | DataValue.ofInt _,    DataValue.ofInt _    => true
-  | DataValue.ofSyntax _, DataValue.ofSyntax _ => true
-  | _,                    _                    => false
+  | .ofString _, .ofString _ => true
+  | .ofBool _,   .ofBool _   => true
+  | .ofName _,   .ofName _   => true
+  | .ofNat _,    .ofNat _    => true
+  | .ofInt _,    .ofInt _    => true
+  | .ofSyntax _, .ofSyntax _ => true
+  | _,           _           => false
 
 @[export lean_data_value_to_string]
 def DataValue.str : DataValue → String
-  | DataValue.ofString v => v
-  | DataValue.ofBool v   => toString v
-  | DataValue.ofName v   => toString v
-  | DataValue.ofNat v    => toString v
-  | DataValue.ofInt v    => toString v
-  | DataValue.ofSyntax v => toString v
+  | .ofString v => v
+  | .ofBool v   => toString v
+  | .ofName v   => toString v
+  | .ofNat v    => toString v
+  | .ofInt v    => toString v
+  | .ofSyntax v => toString v
 
 instance : ToString DataValue := ⟨DataValue.str⟩
 
-instance : Coe String DataValue := ⟨DataValue.ofString⟩
-instance : Coe Bool DataValue   := ⟨DataValue.ofBool⟩
-instance : Coe Name DataValue   := ⟨DataValue.ofName⟩
-instance : Coe Nat DataValue    := ⟨DataValue.ofNat⟩
-instance : Coe Int DataValue    := ⟨DataValue.ofInt⟩
-instance : Coe Syntax DataValue := ⟨DataValue.ofSyntax⟩
+instance : Coe String DataValue := ⟨.ofString⟩
+instance : Coe Bool DataValue   := ⟨.ofBool⟩
+instance : Coe Name DataValue   := ⟨.ofName⟩
+instance : Coe Nat DataValue    := ⟨.ofNat⟩
+instance : Coe Int DataValue    := ⟨.ofInt⟩
+instance : Coe Syntax DataValue := ⟨.ofSyntax⟩
 
 
-/-- Remark: we do not use RBMap here because we need to manipulate KVMap objects in
-   C++ and RBMap is implemented in Lean. So, we use just a List until we can
-   generate C++ code from Lean code. -/
+/--
+A key-value map. We use it to represent user-selected options and `Expr.mdata`.
+
+Remark: we do not use `RBMap` here because we need to manipulate `KVMap` objects in
+C++ and `RBMap` is implemented in Lean. So, we use just a `List` until we can
+generate C++ code from Lean code.
+-/
 structure KVMap where
   entries : List (Name × DataValue) := []
   deriving Inhabited, Repr

src/Lean/Data/LOption.lean

@@ -15,16 +15,16 @@ inductive LOption (α : Type u) where
 
 instance [ToString α] : ToString (LOption α) where
   toString
-    | LOption.none   => "none"
-    | LOption.undef  => "undef"
-    | LOption.some a => "(some " ++ toString a ++ ")"
+    | .none   => "none"
+    | .undef  => "undef"
+    | .some a => "(some " ++ toString a ++ ")"
 
 end Lean
 
 def Option.toLOption {α : Type u} : Option α → Lean.LOption α
-  | none   => Lean.LOption.none
-  | some a => Lean.LOption.some a
+  | none   => .none
+  | some a => .some a
 
 @[inline] def toLOptionM {α} {m : Type → Type} [Monad m] (x : m (Option α)) : m (Lean.LOption α) := do
   let b ← x
-  pure b.toLOption
+  return b.toLOption

src/Lean/Data/OpenDecl.lean

@@ -7,6 +7,7 @@ import Lean.Data.Name
 
 namespace Lean
 
+/-- Data for representing `open` commands -/
 inductive OpenDecl where
   | simple   (ns : Name) (except : List Name)
   | explicit (id : Name) (declName : Name)

src/Lean/DeclarationRange.lean

@@ -9,6 +9,7 @@ import Lean.ToExpr
 
 namespace Lean
 
+/-- Store position information for declarations. -/
 structure DeclarationRange where
   pos          : Position
   /-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this

src/Lean/Elab/PatternVar.lean

@@ -36,8 +36,11 @@ abbrev PatternVar := Syntax  -- TODO: should be `Ident`
 -/
 namespace CollectPatternVars
 
+/-- State for the pattern variable collector monad. -/
 structure State where
+  /-- Pattern variables found so far. -/
   found     : NameSet := {}
+  /-- Pattern variables found so far as an array. It contains the order they were found. -/
   vars      : Array PatternVar := #[]
   deriving Inhabited
 
@@ -321,17 +324,27 @@ def main (alt : MatchAltView) : M MatchAltView := do
 
 end CollectPatternVars
 
+/--
+Collect pattern variables occurring in the `match`-alternative object views.
+It also returns the updated views.
+-/
 def collectPatternVars (alt : MatchAltView) : TermElabM (Array PatternVar × MatchAltView) := do
   let (alt, s) ← (CollectPatternVars.main alt).run {}
   return (s.vars, alt)
 
-/-- Return the pattern variables in the given pattern.
-   Remark: this method is not used by the main `match` elaborator, but in the precheck hook and other macros (e.g., at `Do.lean`). -/
+/--
+Return the pattern variables in the given pattern.
+Remark: this method is not used by the main `match` elaborator, but in the precheck hook and other macros (e.g., at `Do.lean`).
+-/
 def getPatternVars (patternStx : Syntax) : TermElabM (Array PatternVar) := do
   let patternStx ← liftMacroM <| expandMacros patternStx
   let (_, s) ← (CollectPatternVars.collect patternStx).run {}
   return s.vars
 
+/--
+Return the pattern variables occurring in the given patterns.
+This method is used in the `match` and `do` notation elaborators
+-/
 def getPatternsVars (patterns : Array Syntax) : TermElabM (Array PatternVar) := do
   let collect : CollectPatternVars.M Unit := do
     for pattern in patterns do

src/Lean/Eval.lean

@@ -9,9 +9,11 @@ namespace Lean
 
 universe u
 
-/-- `Eval` extension that gives access to the current environment & options.
-    The basic `Eval` class is in the prelude and should not depend on these
-    types. -/
+/--
+`Eval` extension that gives access to the current environment & options.
+The basic `Eval` class is in the prelude and should not depend on these
+types.
+-/
 class MetaEval (α : Type u) where
   eval : Environment → Options → α → (hideUnit : Bool) → IO Environment