From f6211b1a74690daadce3f1466127d06fbc97a287 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 22 Jul 2022 21:05:31 +0200 Subject: [PATCH] chore: convert doc/mod comments from `/-` to `/--`/`/-!` (#1354) --- src/Init/Classical.lean | 4 +- src/Init/Coe.lean | 10 +- src/Init/Control/Basic.lean | 2 +- src/Init/Control/ExceptCps.lean | 2 +- src/Init/Control/Lawful.lean | 10 +- src/Init/Control/StateCps.lean | 2 +- src/Init/Control/StateRef.lean | 2 +- src/Init/Core.lean | 58 +++++----- src/Init/Data/Array/Basic.lean | 20 ++-- src/Init/Data/ByteArray/Basic.lean | 12 +- src/Init/Data/Fin/Basic.lean | 2 +- src/Init/Data/FloatArray/Basic.lean | 15 +-- src/Init/Data/Format/Basic.lean | 4 +- src/Init/Data/Int/Basic.lean | 4 +- src/Init/Data/List/BasicAux.lean | 2 +- src/Init/Data/List/Control.lean | 2 +- src/Init/Data/Nat/Basic.lean | 26 ++--- src/Init/Data/Nat/Linear.lean | 2 +- src/Init/Data/OfScientific.lean | 6 +- src/Init/Data/Random.lean | 14 +-- src/Init/Data/Repr.lean | 2 +- src/Init/Data/Stream.lean | 4 +- src/Init/Meta.lean | 17 +-- src/Init/Notation.lean | 14 +-- src/Init/NotationExtra.lean | 4 +- src/Init/Prelude.lean | 59 +++++----- src/Init/SizeOf.lean | 8 +- src/Init/System/IO.lean | 18 +-- src/Init/System/IOError.lean | 2 +- src/Init/System/ST.lean | 4 +- src/Init/Util.lean | 5 +- src/Lean/Attributes.lean | 12 +- src/Lean/Compiler/ConstFolding.lean | 2 +- src/Lean/Compiler/ExternAttr.lean | 4 +- src/Lean/Compiler/IR/Basic.lean | 104 +++++++++--------- src/Lean/Compiler/IR/Borrow.lean | 20 ++-- src/Lean/Compiler/IR/Boxing.lean | 10 +- src/Lean/Compiler/IR/CompilerM.lean | 2 +- src/Lean/Compiler/IR/EmitC.lean | 2 +- src/Lean/Compiler/IR/EmitUtil.lean | 8 +- src/Lean/Compiler/IR/ExpandResetReuse.lean | 24 ++-- src/Lean/Compiler/IR/FreeVars.lean | 6 +- src/Lean/Compiler/IR/LiveVars.lean | 8 +- src/Lean/Compiler/IR/NormIds.lean | 8 +- src/Lean/Compiler/IR/RC.lean | 16 +-- src/Lean/Compiler/IR/ResetReuse.lean | 8 +- src/Lean/Compiler/Util.lean | 6 +- src/Lean/Data/FuzzyMatching.lean | 18 +-- src/Lean/Data/Json/FromToJson.lean | 2 +- src/Lean/Data/JsonRpc.lean | 2 +- src/Lean/Data/KVMap.lean | 2 +- src/Lean/Data/Lsp/Basic.lean | 2 +- src/Lean/Data/Lsp/InitShutdown.lean | 2 +- src/Lean/Data/Lsp/Internal.lean | 2 +- src/Lean/Data/Lsp/TextSync.lean | 2 +- src/Lean/Data/Name.lean | 4 +- src/Lean/Data/Options.lean | 2 +- src/Lean/Data/SMap.lean | 6 +- src/Lean/Data/SSet.lean | 5 +- src/Lean/Declaration.lean | 2 +- src/Lean/Elab/App.lean | 26 ++--- src/Lean/Elab/Attributes.lean | 2 +- src/Lean/Elab/AutoBound.lean | 4 +- src/Lean/Elab/Binders.lean | 6 +- src/Lean/Elab/BindersUtil.lean | 4 +- src/Lean/Elab/BuiltinNotation.lean | 2 +- src/Lean/Elab/BuiltinTerm.lean | 4 +- src/Lean/Elab/Command.lean | 2 +- src/Lean/Elab/Config.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 2 +- src/Lean/Elab/Declaration.lean | 4 +- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/Deriving/SizeOf.lean | 2 +- src/Lean/Elab/Do.lean | 64 +++++------ src/Lean/Elab/Extra.lean | 6 +- src/Lean/Elab/Inductive.lean | 6 +- src/Lean/Elab/MacroArgUtil.lean | 2 +- src/Lean/Elab/MacroRules.lean | 2 +- src/Lean/Elab/Match.lean | 24 ++-- src/Lean/Elab/MatchAltView.lean | 2 +- src/Lean/Elab/MutualDef.lean | 16 +-- src/Lean/Elab/Notation.lean | 6 +- src/Lean/Elab/PatternVar.lean | 8 +- src/Lean/Elab/PreDefinition/Basic.lean | 2 +- src/Lean/Elab/PreDefinition/MkInhabitant.lean | 1 - .../Elab/PreDefinition/Structural/BRecOn.lean | 8 +- .../Elab/PreDefinition/Structural/Basic.lean | 31 ++++-- .../PreDefinition/WF/TerminationHint.lean | 4 +- src/Lean/Elab/Quotation.lean | 60 +++++----- src/Lean/Elab/StructInst.lean | 6 +- src/Lean/Elab/Structure.lean | 2 +- src/Lean/Elab/Syntax.lean | 8 +- src/Lean/Elab/SyntheticMVars.lean | 4 +- src/Lean/Elab/Tactic/Basic.lean | 16 +-- src/Lean/Elab/Tactic/BuiltinTactic.lean | 2 +- src/Lean/Elab/Tactic/ElabTerm.lean | 6 +- src/Lean/Elab/Tactic/Induction.lean | 10 +- src/Lean/Elab/Term.lean | 18 +-- src/Lean/Elab/Util.lean | 3 +- src/Lean/Environment.lean | 23 ++-- src/Lean/Exception.lean | 4 +- src/Lean/HeadIndex.lean | 4 +- src/Lean/Hygiene.lean | 2 +- src/Lean/ImportingFlag.lean | 2 +- src/Lean/KeyedDeclsAttribute.lean | 2 +- src/Lean/LocalContext.lean | 2 +- src/Lean/Meta/Basic.lean | 14 +-- src/Lean/Meta/Check.lean | 8 +- src/Lean/Meta/Closure.lean | 2 +- src/Lean/Meta/DecLevel.lean | 2 +- src/Lean/Meta/DiscrTree.lean | 6 +- src/Lean/Meta/DiscrTreeTypes.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 34 +++--- src/Lean/Meta/Inductive.lean | 4 +- src/Lean/Meta/InferType.lean | 4 +- src/Lean/Meta/Instances.lean | 2 +- src/Lean/Meta/Match/Basic.lean | 4 +- src/Lean/Meta/Match/MVarRenaming.lean | 2 +- src/Lean/Meta/Match/Match.lean | 14 +-- src/Lean/Meta/Match/MatchEqsExt.lean | 2 +- src/Lean/Meta/Offset.lean | 2 +- src/Lean/Meta/PPGoal.lean | 12 +- src/Lean/Meta/RecursorInfo.lean | 2 +- src/Lean/Meta/SizeOf.lean | 17 +-- src/Lean/Meta/SynthInstance.lean | 12 +- src/Lean/Meta/Tactic/Apply.lean | 2 +- src/Lean/Meta/Tactic/Cases.lean | 4 +- src/Lean/Meta/Tactic/Cleanup.lean | 2 +- src/Lean/Meta/Tactic/Delta.lean | 2 +- src/Lean/Meta/Tactic/FVarSubst.lean | 4 +- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 6 +- src/Lean/Meta/Tactic/Split.lean | 2 +- src/Lean/Meta/Tactic/UnifyEq.lean | 2 +- src/Lean/Meta/WHNF.lean | 39 +++---- src/Lean/MetavarContext.lean | 12 +- src/Lean/Modifiers.lean | 2 +- src/Lean/MonadEnv.lean | 2 +- src/Lean/Parser/Attr.lean | 4 +- src/Lean/Parser/Basic.lean | 64 +++++------ src/Lean/Parser/Command.lean | 2 +- src/Lean/Parser/Do.lean | 4 +- src/Lean/Parser/Extension.lean | 10 +- src/Lean/Parser/Term.lean | 12 +- src/Lean/ProjFns.lean | 2 +- src/Lean/ResolveName.lean | 16 +-- src/Lean/Server/Completion.lean | 2 +- src/Lean/Server/FileWorker.lean | 3 +- src/Lean/Server/FileWorker/Utils.lean | 2 +- src/Lean/Server/InfoUtils.lean | 2 +- src/Lean/Server/References.lean | 6 +- src/Lean/Server/Requests.lean | 2 +- src/Lean/Server/Watchdog.lean | 20 ++-- src/Lean/Syntax.lean | 4 +- src/Lean/Util/ForEachExpr.lean | 2 +- src/Lean/Util/SCC.lean | 2 +- src/Lean/Widget/InteractiveDiagnostic.lean | 14 +-- src/Std/Data/AssocList.lean | 2 +- src/Std/Data/BinomialHeap.lean | 28 ++--- src/Std/ShareCommon.lean | 4 +- tests/lean/interactive/533.lean.expected.out | 11 +- 161 files changed, 750 insertions(+), 739 deletions(-) diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean index be8d65f609..83e72ce853 100644 --- a/src/Init/Classical.lean +++ b/src/Init/Classical.lean @@ -9,7 +9,7 @@ import Init.NotationExtra universe u v -/- Classical reasoning support -/ +/-! # Classical reasoning support -/ namespace Classical @@ -65,7 +65,7 @@ noncomputable def inhabited_of_nonempty {α : Sort u} (h : Nonempty α) : Inhabi noncomputable def inhabited_of_exists {α : Sort u} {p : α → Prop} (h : ∃ x, p x) : Inhabited α := inhabited_of_nonempty (Exists.elim h (fun w _ => ⟨w⟩)) -/- all propositions are Decidable -/ +/-- All propositions are `Decidable`. -/ noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a := choice <| match em a with | Or.inl h => ⟨isTrue h⟩ diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean index 4bfcc0fe85..19599db9c7 100644 --- a/src/Init/Coe.lean +++ b/src/Init/Coe.lean @@ -15,11 +15,11 @@ class Coe (α : Sort u) (β : Sort v) where class CoeTC (α : Sort u) (β : Sort v) where coe : α → β -/- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/ +/-- Expensive coercion that can only appear at the beginning of a sequence of coercions. -/ class CoeHead (α : Sort u) (β : Sort v) where coe : α → β -/- Expensive coercion that can only appear at the end of a sequence of coercions. -/ +/-- Expensive coercion that can only appear at the end of a sequence of coercions. -/ class CoeTail (α : Sort u) (β : Sort v) where coe : α → β @@ -30,7 +30,7 @@ class CoeHTCT (α : Sort u) (β : Sort v) where class CoeDep (α : Sort u) (_ : α) (β : Sort v) where coe : β -/- Combines CoeHead, CoeTC, CoeTail, CoeDep -/ +/-- Combines CoeHead, CoeTC, CoeTail, CoeDep -/ class CoeT (α : Sort u) (_ : α) (β : Sort v) where coe : β @@ -81,7 +81,7 @@ instance coeId {α : Sort u} (a : α) : CoeT α a α where instance coeSortToCoeTail [inst : CoeSort α β] : CoeTail α β where coe := inst.coe -/- Basic instances -/ +/-! # Basic instances -/ @[inline] instance boolToProp : Coe Bool Prop where coe b := Eq b true @@ -98,7 +98,7 @@ instance optionCoe {α : Type u} : CoeTail α (Option α) where instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead (Subtype p) α where coe v := v.val -/- Coe bridge -/ +/-! # Coe bridge -/ -- Helper definition used by the elaborator. It is not meant to be used directly by users @[inline] def Lean.Internal.liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean index 23394c7b76..84db5c300b 100644 --- a/src/Init/Control/Basic.lean +++ b/src/Init/Control/Basic.lean @@ -217,7 +217,7 @@ def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α := controlAt m f -/- +/-- Typeclass for the polymorphic `forM` operation described in the "do unchained" paper. Remark: - `γ` is a "container" type of elements of type `α`. diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean index 7c2a859d03..a8ed4413df 100644 --- a/src/Init/Control/ExceptCps.lean +++ b/src/Init/Control/ExceptCps.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Control.Lawful -/- +/-! The Exception monad transformer using CPS style. -/ diff --git a/src/Init/Control/Lawful.lean b/src/Init/Control/Lawful.lean index ccca583101..caced776b6 100644 --- a/src/Init/Control/Lawful.lean +++ b/src/Init/Control/Lawful.lean @@ -90,7 +90,7 @@ theorem seqRight_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x *> theorem seqLeft_eq_bind [Monad m] [LawfulMonad m] (x : m α) (y : m β) : x <* y = x >>= fun a => y >>= fun _ => pure a := by rw [seqLeft_eq]; simp [map_eq_pure_bind, seq_eq_bind_map] -/- Id -/ +/-! # Id -/ namespace Id @@ -103,7 +103,7 @@ instance : LawfulMonad Id := by end Id -/- ExceptT -/ +/-! # ExceptT -/ namespace ExceptT @@ -179,7 +179,7 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ExceptT ε m) where end ExceptT -/- ReaderT -/ +/-! # ReaderT -/ namespace ReaderT @@ -225,12 +225,12 @@ instance [Monad m] [LawfulMonad m] : LawfulMonad (ReaderT ρ m) where end ReaderT -/- StateRefT -/ +/-! # StateRefT -/ instance [Monad m] [LawfulMonad m] : LawfulMonad (StateRefT' ω σ m) := inferInstanceAs (LawfulMonad (ReaderT (ST.Ref ω σ) m)) -/- StateT -/ +/-! # StateT -/ namespace StateT diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean index ca5f9e50f9..2747b258e8 100644 --- a/src/Init/Control/StateCps.lean +++ b/src/Init/Control/StateCps.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Control.Lawful -/- +/-! The State monad transformer using CPS style. -/ diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean index 7c4e92f3bc..fd05a47bd4 100644 --- a/src/Init/Control/StateRef.lean +++ b/src/Init/Control/StateRef.lean @@ -11,7 +11,7 @@ import Init.Control.State def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α -/- Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/ +/-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/ @[inline] def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ) := do let ref ← ST.mkRef s diff --git a/src/Init/Core.lean b/src/Init/Core.lean index e927945b19..28031221f6 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -79,7 +79,7 @@ structure PSigma {α : Sort u} (β : α → Sort v) where inductive Exists {α : Sort u} (p : α → Prop) : Prop where | intro (w : α) (h : p w) : Exists p -/- Auxiliary type used to compile `for x in xs` notation. -/ +/-- Auxiliary type used to compile `for x in xs` notation. -/ inductive ForInStep (α : Type u) where | done : α → ForInStep α | yield : α → ForInStep α @@ -95,24 +95,24 @@ class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v) export ForIn' (forIn') -/- Auxiliary type used to compile `do` notation. -/ +/-- Auxiliary type used to compile `do` notation. -/ inductive DoResultPRBC (α β σ : Type u) where | «pure» : α → σ → DoResultPRBC α β σ | «return» : β → σ → DoResultPRBC α β σ | «break» : σ → DoResultPRBC α β σ | «continue» : σ → DoResultPRBC α β σ -/- Auxiliary type used to compile `do` notation. -/ +/-- Auxiliary type used to compile `do` notation. -/ inductive DoResultPR (α β σ : Type u) where | «pure» : α → σ → DoResultPR α β σ | «return» : β → σ → DoResultPR α β σ -/- Auxiliary type used to compile `do` notation. -/ +/-- Auxiliary type used to compile `do` notation. -/ inductive DoResultBC (σ : Type u) where | «break» : σ → DoResultBC σ | «continue» : σ → DoResultBC σ -/- Auxiliary type used to compile `do` notation. -/ +/-- Auxiliary type used to compile `do` notation. -/ inductive DoResultSBC (α σ : Type u) where | «pureReturn» : α → σ → DoResultSBC α σ | «break» : σ → DoResultSBC α σ @@ -129,7 +129,7 @@ class EmptyCollection (α : Type u) where notation "{" "}" => EmptyCollection.emptyCollection notation "∅" => EmptyCollection.emptyCollection -/- Remark: tasks have an efficient implementation in the runtime. -/ +/-- Remark: tasks have an efficient implementation in the runtime. -/ structure Task (α : Type u) : Type u where pure :: (get : α) deriving Inhabited @@ -166,11 +166,11 @@ protected def bind {α : Type u} {β : Type v} (x : Task α) (f : α → Task β end Task -/- Some type that is not a scalar value in our runtime. -/ +/-- Some type that is not a scalar value in our runtime. -/ structure NonScalar where val : Nat -/- Some type that is not a scalar value in our runtime and is universe polymorphic. -/ +/-- Some type that is not a scalar value in our runtime and is universe polymorphic. -/ inductive PNonScalar : Type u where | mk (v : Nat) : PNonScalar @@ -178,7 +178,7 @@ inductive PNonScalar : Type u where theorem optParam_eq (α : Sort u) (default : α) : optParam α default = α := rfl -/- Boolean operators -/ +/-! # Boolean operators -/ @[extern c inline "#1 || #2"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ @[extern c inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ @@ -205,7 +205,7 @@ instance : LawfulBEq Char := inferInstance instance : LawfulBEq String := inferInstance -/- Logical connectives an equality -/ +/-! # Logical connectives and equality -/ def implies (a b : Prop) := a → b @@ -359,14 +359,14 @@ theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) := theorem And.comm : a ∧ b ↔ b ∧ a := by constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩ -/- Exists -/ +/-! # Exists -/ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : Exists (fun x => p x)) (h₂ : ∀ (a : α), p a → b) : b := match h₁ with | intro a h => h₂ a h -/- Decidable -/ +/-! # Decidable -/ theorem decide_true_eq_true (h : Decidable True) : @decide True h = true := match h with @@ -457,7 +457,7 @@ instance {p q} [Decidable p] [Decidable q] : Decidable (p ↔ q) := else isTrue ⟨fun h => absurd h hp, fun h => absurd h hq⟩ -/- if-then-else expression theorems -/ +/-! # if-then-else expression theorems -/ theorem if_pos {c : Prop} {h : Decidable c} (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t := match h with @@ -495,7 +495,7 @@ instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : | isTrue hc => dT hc | isFalse hc => dE hc -/- Auxiliary definitions for generating compact `noConfusion` for enumeration types -/ +/-- Auxiliary definitions for generating compact `noConfusion` for enumeration types -/ abbrev noConfusionTypeEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : α → β) (P : Sort w) (x y : α) : Sort w := Decidable.casesOn (motive := fun _ => Sort w) (inst (f x) (f y)) (fun _ => P) @@ -508,7 +508,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f : (fun h' => False.elim (h' (congrArg f h))) (fun _ => fun x => x) -/- Inhabited -/ +/-! # Inhabited -/ instance : Inhabited Prop where default := True @@ -518,7 +518,7 @@ deriving instance Inhabited for NonScalar, PNonScalar, True, ForInStep theorem nonempty_of_exists {α : Sort u} {p : α → Prop} : Exists (fun x => p x) → Nonempty α | ⟨w, _⟩ => ⟨w⟩ -/- Subsingleton -/ +/-! # Subsingleton -/ class Subsingleton (α : Sort u) : Prop where intro :: allEq : (a b : α) → a = b @@ -572,7 +572,7 @@ inductive TC {α : Sort u} (r : α → α → Prop) : α → α → Prop where | base : ∀ a b, r a b → TC r a b | trans : ∀ a b c, TC r a b → TC r b c → TC r a c -/- Subtype -/ +/-! # Subtype -/ namespace Subtype def existsOfSubtype {α : Type u} {p : α → Prop} : { x // p x } → Exists (fun x => p x) @@ -597,7 +597,7 @@ instance {α : Type u} {p : α → Prop} [DecidableEq α] : DecidableEq {x : α end Subtype -/- Sum -/ +/-! # Sum -/ section variable {α : Type u} {β : Type v} @@ -621,7 +621,7 @@ instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : Decidab end -/- Product -/ +/-! # Product -/ instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where default := (default, default) @@ -657,7 +657,7 @@ def Prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂ | (a, b) => (f a, g b) -/- Dependent products -/ +/-! # Dependent products -/ theorem ex_of_PSigma {α : Type u} {p : α → Prop} : (PSigma (fun x => p x)) → Exists (fun x => p x) | ⟨x, hx⟩ => ⟨x, hx⟩ @@ -668,7 +668,7 @@ protected theorem PSigma.eta {α : Sort u} {β : α → Sort v} {a₁ a₂ : α} subst h₂ exact rfl -/- Universe polymorphic unit -/ +/-! # Universe polymorphic unit -/ theorem PUnit.subsingleton (a b : PUnit) : a = b := by cases a; cases b; exact rfl @@ -685,7 +685,7 @@ instance : Inhabited PUnit where instance : DecidableEq PUnit := fun a b => isTrue (PUnit.subsingleton a b) -/- Setoid -/ +/-! # Setoid -/ class Setoid (α : Sort u) where r : α → α → Prop @@ -710,7 +710,7 @@ theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c := end Setoid -/- Propositional extensionality -/ +/-! # Propositional extensionality -/ axiom propext {a b : Prop} : (a ↔ b) → a = b @@ -742,9 +742,9 @@ gen_injective_theorems% Lean.Syntax @[simp] theorem beq_iff_eq [BEq α] [LawfulBEq α] (a b : α) : a == b ↔ a = b := ⟨eq_of_beq, by intro h; subst h; exact LawfulBEq.rfl⟩ -/- Quotients -/ +/-! # Quotients -/ --- Iff can now be used to do substitutions in a calculation +/-- Iff can now be used to do substitutions in a calculation -/ theorem Iff.subst {a b : Prop} {p : Prop → Prop} (h₁ : a ↔ b) (h₂ : p a) : p b := Eq.subst (propext h₁) h₂ @@ -1018,7 +1018,7 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ (a b : α), Decidable (a ≈ b)] | isTrue h₁ => isTrue (Quotient.sound h₁) | isFalse h₂ => isFalse fun h => absurd (Quotient.exact h) h₂ -/- Function extensionality -/ +/-! # Function extensionality -/ namespace Function variable {α : Sort u} {β : α → Sort v} @@ -1067,7 +1067,7 @@ instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsi allEq f₁ f₂ := funext (fun a => Subsingleton.elim (f₁ a) (f₂ a)) -/- Squash -/ +/-! # Squash -/ def Squash (α : Type u) := Quot (fun (_ _ : α) => True) @@ -1086,13 +1086,13 @@ instance : Subsingleton (Squash α) where apply Quot.sound trivial -/- Relations -/ +/-! # Relations -/ class Antisymm {α : Sort u} (r : α → α → Prop) where antisymm {a b : α} : r a b → r b a → a = b namespace Lean -/- Kernel reduction hints -/ +/-! # Kernel reduction hints -/ /-- When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`. diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 16732966b6..b41dab9d48 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -34,7 +34,7 @@ def isEmpty (a : Array α) : Bool := def singleton (v : α) : Array α := mkArray 1 v -/- Low-level version of `fget` which is as fast as a C array read. +/-- Low-level version of `fget` which is as fast as a C array read. `Fin` values are represented as tag pointers in the Lean runtime. Thus, `fget` may be slightly slower than `uget`. -/ @[extern "lean_array_uget"] @@ -64,7 +64,7 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = @[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 := List.length_concat .. -/- Low-level version of `fset` which is as fast as a C array fset. +/-- Low-level version of `fset` which is as fast as a C array fset. `Fin` values are represented as tag pointers in the Lean runtime. Thus, `fset` may be slightly slower than `uset`. -/ @[extern "lean_array_uset"] @@ -141,7 +141,7 @@ def modify (a : Array α) (i : Nat) (f : α → α) : Array α := def modifyOp (self : Array α) (idx : Nat) (f : α → α) : Array α := self.modify idx f -/- +/-- We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime. This kind of low level trick can be removed with a little bit of compiler support. For example, if the compiler simplifies `as.size < usizeSz` to true. -/ @@ -157,7 +157,7 @@ def modifyOp (self : Array α) (idx : Nat) (f : α → α) : Array α := pure b loop 0 b -/- Reference implementation for `forIn` -/ +/-- Reference implementation for `forIn` -/ @[implementedBy Array.forInUnsafe] protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (b : β) (f : α → β → m (ForInStep β)) : m β := let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do @@ -175,7 +175,7 @@ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m instance : ForIn m (Array α) α where forIn := Array.forIn -/- See comment at forInUnsafe -/ +/-- See comment at `forInUnsafe` -/ @[inline] unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β := let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do @@ -191,7 +191,7 @@ unsafe def foldlMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon else pure init -/- Reference implementation for `foldlM` -/ +/-- Reference implementation for `foldlM` -/ @[implementedBy foldlMUnsafe] def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Array α) (start := 0) (stop := as.size) : m β := let fold (stop : Nat) (h : stop ≤ as.size) := @@ -210,7 +210,7 @@ def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β else fold as.size (Nat.le_refl _) -/- See comment at forInUnsafe -/ +/-- See comment at `forInUnsafe` -/ @[inline] unsafe def foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m β := let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do @@ -228,7 +228,7 @@ unsafe def foldrMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Mon else pure init -/- Reference implementation for `foldrM` -/ +/-- Reference implementation for `foldrM` -/ @[implementedBy foldrMUnsafe] def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Array α) (start := as.size) (stop := 0) : m β := let rec fold (i : Nat) (h : i ≤ as.size) (b : β) : m β := do @@ -249,7 +249,7 @@ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α else pure init -/- See comment at forInUnsafe -/ +/-- See comment at `forInUnsafe` -/ @[inline] unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) := let sz := USize.ofNat as.size @@ -266,7 +266,7 @@ unsafe def mapMUnsafe {α : Type u} {β : Type v} {m : Type v → Type w} [Monad pure (unsafeCast r) unsafeCast <| map 0 (unsafeCast as) -/- Reference implementation for `mapM` -/ +/-- Reference implementation for `mapM` -/ @[implementedBy mapMUnsafe] def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (as : Array α) : m (Array β) := as.foldlM (fun bs a => do let b ← f a; pure (bs.push b)) (mkEmpty as.size) diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean index 4c7f861c68..52b22c535f 100644 --- a/src/Init/Data/ByteArray/Basic.lean +++ b/src/Init/Data/ByteArray/Basic.lean @@ -102,7 +102,7 @@ partial def toList (bs : ByteArray) : List UInt8 := none loop start -/- +/-- We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime. This is similar to the `Array` version. @@ -120,7 +120,7 @@ partial def toList (bs : ByteArray) : List UInt8 := pure b loop 0 b -/- Reference implementation for `forIn` -/ +/-- Reference implementation for `forIn` -/ @[implementedBy ByteArray.forInUnsafe] protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β := let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do @@ -138,10 +138,8 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteAr instance : ForIn m ByteArray UInt8 where forIn := ByteArray.forIn -/- - See comment at forInUnsafe - TODO: avoid code duplication. --/ +/-- See comment at `forInUnsafe` -/ +-- TODO: avoid code duplication. @[inline] unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β := let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do @@ -157,7 +155,7 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β else pure init -/- Reference implementation for `foldlM` -/ +/-- Reference implementation for `foldlM` -/ @[implementedBy foldlMUnsafe] def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start := 0) (stop := as.size) : m β := let fold (stop : Nat) (h : stop ≤ as.size) := diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index 5c4827521d..69c70b926c 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -44,7 +44,7 @@ protected def mul : Fin n → Fin n → Fin n protected def sub : Fin n → Fin n → Fin n | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩ -/- +/-! Remark: mod/div/modn/land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to boostrap Lean. diff --git a/src/Init/Data/FloatArray/Basic.lean b/src/Init/Data/FloatArray/Basic.lean index b35f2a38ee..eef9c53b49 100644 --- a/src/Init/Data/FloatArray/Basic.lean +++ b/src/Init/Data/FloatArray/Basic.lean @@ -84,12 +84,11 @@ partial def toList (ds : FloatArray) : List Float := r.reverse loop 0 [] -/- +/-- We claim this unsafe implementation is correct because an array cannot have more than `usizeSz` elements in our runtime. This is similar to the `Array` version. - - TODO: avoid code duplication in the future after we improve the compiler. -/ +-- TODO: avoid code duplication in the future after we improve the compiler. @[inline] unsafe def forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatArray) (b : β) (f : Float → β → m (ForInStep β)) : m β := let sz := USize.ofNat as.size let rec @[specialize] loop (i : USize) (b : β) : m β := do @@ -102,7 +101,7 @@ partial def toList (ds : FloatArray) : List Float := pure b loop 0 b -/- Reference implementation for `forIn` -/ +/-- Reference implementation for `forIn` -/ @[implementedBy FloatArray.forInUnsafe] protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatArray) (b : β) (f : Float → β → m (ForInStep β)) : m β := let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do @@ -120,10 +119,8 @@ protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : FloatA instance : ForIn m FloatArray Float where forIn := FloatArray.forIn -/- - See comment at forInUnsafe - TODO: avoid code duplication. --/ +/-- See comment at `forInUnsafe` -/ +-- TODO: avoid code duplication. @[inline] unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float → m β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : m β := let rec @[specialize] fold (i : USize) (stop : USize) (b : β) : m β := do @@ -139,7 +136,7 @@ unsafe def foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β else pure init -/- Reference implementation for `foldlM` -/ +/-- Reference implementation for `foldlM` -/ @[implementedBy foldlMUnsafe] def foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → Float → m β) (init : β) (as : FloatArray) (start := 0) (stop := as.size) : m β := let fold (stop : Nat) (h : stop ≤ as.size) := diff --git a/src/Init/Data/Format/Basic.lean b/src/Init/Data/Format/Basic.lean index 480d330924..b84a453bfd 100644 --- a/src/Init/Data/Format/Basic.lean +++ b/src/Init/Data/Format/Basic.lean @@ -23,8 +23,8 @@ inductive Format where | nest (indent : Int) : Format → Format | append : Format → Format → Format | group : Format → (behavior : FlattenBehavior := FlattenBehavior.allOrNone) → Format - /- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/ - | tag : Nat → Format → Format + | /-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects. -/ + tag : Nat → Format → Format deriving Inhabited namespace Format diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean index 763d196d00..d073f1bc83 100644 --- a/src/Init/Data/Int/Basic.lean +++ b/src/Init/Data/Int/Basic.lean @@ -11,7 +11,7 @@ import Init.Data.Nat.Div import Init.Data.List.Basic open Nat -/- the Type, coercions, and notation -/ +/-! # the Type, coercions, and notation -/ inductive Int : Type where | ofNat : Nat → Int @@ -62,7 +62,7 @@ protected def mul (m n : @& Int) : Int := | negSucc m, ofNat n => negOfNat (succ m * n) | negSucc m, negSucc n => ofNat (succ m * succ n) -/- +/-- The `Neg Int` default instance must have priority higher than `low` since the default instance `OfNat Nat n` has `low` priority. ``` diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 942dd1bbcb..3cbffb0a70 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -11,7 +11,7 @@ import Init.Util universe u namespace List -/- The following functions can't be defined at `Init.Data.List.Basic`, because they depend on `Init.Util`, +/-! The following functions can't be defined at `Init.Data.List.Basic`, because they depend on `Init.Util`, and `Init.Util` depends on `Init.Data.List.Basic`. -/ def get! [Inhabited α] : List α → Nat → α diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean index ab5d3bcb0a..2c47270291 100644 --- a/src/Init/Data/List/Control.lean +++ b/src/Init/Data/List/Control.lean @@ -10,7 +10,7 @@ import Init.Data.List.Basic namespace List universe u v w u₁ u₂ -/- +/-! Remark: we can define `mapM`, `mapM₂` and `forM` using `Applicative` instead of `Monad`. Example: ``` diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index 271aa24329..eb6d9aa6d6 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -26,7 +26,7 @@ namespace Nat | 0 => false | succ n => f (s - (succ n)) || anyAux f s n -/- `any f n = true` iff there is `i in [0, n-1]` s.t. `f i = true` -/ +/-- `any f n = true` iff there is `i in [0, n-1]` s.t. `f i = true` -/ @[inline] def any (f : Nat → Bool) (n : Nat) : Bool := anyAux f n n @@ -44,7 +44,7 @@ def blt (a b : Nat) : Bool := attribute [simp] Nat.zero_le -/- Helper "packing" theorems -/ +/-! # Helper "packing" theorems -/ @[simp] theorem zero_eq : Nat.zero = 0 := rfl @[simp] theorem add_eq : Nat.add x y = x + y := rfl @@ -53,7 +53,7 @@ attribute [simp] Nat.zero_le @[simp] theorem lt_eq : Nat.lt x y = (x < y) := rfl @[simp] theorem le_eq : Nat.le x y = (x ≤ y) := rfl -/- Helper Bool relation theorems -/ +/-! # Helper Bool relation theorems -/ @[simp] theorem beq_refl (a : Nat) : Nat.beq a a = true := by induction a with simp [Nat.beq] @@ -75,7 +75,7 @@ instance : LawfulBEq Nat where have : ¬ ((a == b) = true) := fun h' => absurd (eq_of_beq h') h by simp [this]) -/- Nat.add theorems -/ +/-! # Nat.add theorems -/ @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n | 0 => rfl @@ -120,7 +120,7 @@ protected theorem add_right_cancel {n m k : Nat} (h : n + m = k + m) : n = k := rw [Nat.add_comm n m, Nat.add_comm k m] at h apply Nat.add_left_cancel h -/- Nat.mul theorems -/ +/-! # Nat.mul theorems -/ @[simp] protected theorem mul_zero (n : Nat) : n * 0 = 0 := rfl @@ -168,7 +168,7 @@ protected theorem mul_assoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k) protected theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k) := by rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc] -/- Inequalities -/ +/-! # Inequalities -/ attribute [simp] Nat.le_refl @@ -379,7 +379,7 @@ protected theorem le_of_add_le_add_right {a b c : Nat} : a + b ≤ c + b → a rw [Nat.add_comm _ b, Nat.add_comm _ b] apply Nat.le_of_add_le_add_left -/- Basic theorems for comparing numerals -/ +/-! # Basic theorems for comparing numerals -/ theorem ctor_eq_zero : Nat.zero = 0 := rfl @@ -393,7 +393,7 @@ protected theorem zero_ne_one : 0 ≠ (1 : Nat) := theorem succ_ne_zero (n : Nat) : succ n ≠ 0 := fun h => Nat.noConfusion h -/- mul + order -/ +/-! # mul + order -/ theorem mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m := match le.dest h with @@ -429,7 +429,7 @@ protected theorem eq_of_mul_eq_mul_left {m k n : Nat} (hn : 0 < n) (h : n * m = theorem eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) : n = k := by rw [Nat.mul_comm n m, Nat.mul_comm k m] at h; exact Nat.eq_of_mul_eq_mul_left hm h -/- power -/ +/-! # power -/ theorem pow_succ (n m : Nat) : n^(succ m) = n^m * n := rfl @@ -455,7 +455,7 @@ theorem pow_le_pow_of_le_right {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ theorem pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) : 0 < n^m := pow_le_pow_of_le_right h (Nat.zero_le _) -/- min/max -/ +/-! # min/max -/ protected def min (n m : Nat) : Nat := if n ≤ m then n else m @@ -463,7 +463,7 @@ protected def min (n m : Nat) : Nat := protected def max (n m : Nat) : Nat := if n ≤ m then m else n -/- Auxiliary theorems for well-founded recursion -/ +/-! # Auxiliary theorems for well-founded recursion -/ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by cases a @@ -473,7 +473,7 @@ theorem not_eq_zero_of_lt (h : b < a) : a ≠ 0 := by theorem pred_lt' {n m : Nat} (h : m < n) : pred n < n := pred_lt (not_eq_zero_of_lt h) -/- sub/pred theorems -/ +/-! # sub/pred theorems -/ theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by induction a with @@ -656,7 +656,7 @@ protected theorem mul_sub_right_distrib (n m k : Nat) : (n - m) * k = n * k - m protected theorem mul_sub_left_distrib (n m k : Nat) : n * (m - k) = n * m - n * k := by rw [Nat.mul_comm, Nat.mul_sub_right_distrib, Nat.mul_comm m n, Nat.mul_comm n k] -/- Helper normalization theorems -/ +/-! # Helper normalization theorems -/ theorem not_le_eq (a b : Nat) : (¬ (a ≤ b)) = (b + 1 ≤ a) := propext <| Iff.intro (fun h => Nat.gt_of_not_le h) (fun h => Nat.not_le_of_gt h) diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index b00538b402..9115fbf392 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -13,7 +13,7 @@ import Init.Data.Prod namespace Nat.Linear -/--! +/-! Helper definitions and theorems for constructing linear arithmetic proofs. -/ diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean index f110518107..584bec1c3c 100644 --- a/src/Init/Data/OfScientific.lean +++ b/src/Init/Data/OfScientific.lean @@ -8,7 +8,7 @@ import Init.Meta import Init.Data.Float import Init.Data.Nat -/- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`). +/-- For decimal and scientific numbers (e.g., `1.23`, `3.12e10`). Examples: - `OfScientific.ofScientific 123 true 2` represents `1.23` - `OfScientific.ofScientific 121 false 100` represents `121e100` @@ -31,8 +31,8 @@ protected opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float := else Float.ofBinaryScientific (m * 5^e) e -/- - The `OfScientifi Float` must have priority higher than `mid` since +/-- + The `OfScientific Float` must have priority higher than `mid` since the default instance `Neg Int` has `mid` priority. ``` #check -42.0 -- must be Float diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index b00e375163..dba66d541a 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -8,27 +8,27 @@ import Init.System.IO import Init.Data.Int universe u -/- +/-! Basic random number generator support based on the one available on the Haskell library -/ -/- Interface for random number generators. -/ +/-- Interface for random number generators. -/ class RandomGen (g : Type u) where - /- `range` returns the range of values returned by + /-- `range` returns the range of values returned by the generator. -/ range : g → Nat × Nat - /- `next` operation returns a natural number that is uniformly distributed + /-- `next` operation returns a natural number that is uniformly distributed the range returned by `range` (including both end points), and a new generator. -/ next : g → Nat × g - /- + /-- The 'split' operation allows one to obtain two distinct random number generators. This is very useful in functional programs (for example, when passing a random number generator down to recursive calls). -/ split : g → g × g -/- "Standard" random number generator. -/ +/-- "Standard" random number generator. -/ structure StdGen where s1 : Nat s2 : Nat @@ -76,7 +76,7 @@ def mkStdGen (s : Nat := 0) : StdGen := let s2 := q % 2147483398 ⟨s1 + 1, s2 + 1⟩ -/- +/-- Auxiliary function for randomNatVal. Generate random values until we exceed the target magnitude. `genLo` and `genMag` are the generator lower bound and magnitude. diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index db7b519797..8e10b7499c 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -27,7 +27,7 @@ abbrev reprStr [Repr α] (a : α) : String := abbrev reprArg [Repr α] (a : α) : Format := reprPrec a max_prec -/- Auxiliary class for marking types that should be considered atomic by `Repr` methods. +/-- Auxiliary class for marking types that should be considered atomic by `Repr` methods. We use it at `Repr (List α)` to decide whether `bracketFill` should be used or not. -/ class ReprAtom (α : Type u) diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean index 7a68b62a53..2eb2fb5143 100644 --- a/src/Init/Data/Stream.lean +++ b/src/Init/Data/Stream.lean @@ -7,7 +7,7 @@ prelude import Init.Data.Array.Subarray import Init.Data.Range -/- +/-! Remark: we considered using the following alternative design ``` structure Stream (α : Type u) where @@ -22,7 +22,7 @@ The key problem is that the type `Stream α` "lives" in a universe higher than ` This is a problem because we want to use `Stream`s in monadic code. -/ -/- +/-- Streams are used to implement parallel `for` statements. Example: ``` diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 5995ef1c12..154ed3a6b8 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -64,7 +64,7 @@ def toolchain := @[extern c inline "LEAN_IS_STAGE0"] opaque Internal.isStage0 (u : Unit) : Bool -/- Valid identifier names -/ +/-- Valid identifier names -/ def isGreek (c : Char) : Bool := 0x391 ≤ c.val && c.val ≤ 0x3dd @@ -448,7 +448,7 @@ end Syntax @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : TSyntax k := ⟨Syntax.node SourceInfo.none k args⟩ -/- Syntax objects for a Lean module. -/ +/-- Syntax objects for a Lean module. -/ structure Module where header : Syntax commands : Array Syntax @@ -491,7 +491,7 @@ partial def expandMacros (stx : Syntax) (p : SyntaxNodeKind → Bool := fun k => return stx | stx => return stx -/- Helper functions for processing Syntax programmatically -/ +/-! # Helper functions for processing Syntax programmatically -/ /-- Create an identifier copying the position from `src`. @@ -588,7 +588,7 @@ def mkScientificLit (val : String) (info := SourceInfo.none) : TSyntax scientifi def mkNameLit (val : String) (info := SourceInfo.none) : NameLit := mkLit nameLitKind val info -/- Recall that we don't have special Syntax constructors for storing numeric and string atoms. +/-! Recall that we don't have special Syntax constructors for storing numeric and string atoms. The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or different ways of representing them. So, our atoms contain just the parsed string. The main Lean parser uses the kind `numLitKind` for storing natural numbers that can be encoded @@ -966,7 +966,7 @@ instance Option.hasQuote {α : Type} [Quote α `term] : Quote (Option α) `term | (some x) => Syntax.mkCApp ``some #[quote x] -/- Evaluator for `prec` DSL -/ +/-- Evaluator for `prec` DSL -/ def evalPrec (stx : Syntax) : MacroM Nat := Macro.withIncRecDepth stx do let stx ← expandMacros stx @@ -982,7 +982,7 @@ macro_rules macro "eval_prec " p:prec:max : term => return quote (k := `term) (← evalPrec p) -/- Evaluator for `prio` DSL -/ +/-- Evaluator for `prio` DSL -/ def evalPrio (stx : Syntax) : MacroM Nat := Macro.withIncRecDepth stx do let stx ← expandMacros stx @@ -1064,7 +1064,7 @@ def TSepArray.getElems (sa : TSepArray k sep) : TSyntaxArray k := def TSepArray.push (sa : TSepArray k sep) (e : TSyntax k) : TSepArray k sep := if sa.elemsAndSeps.isEmpty then { elemsAndSeps := #[e] } - else + else { elemsAndSeps := sa.elemsAndSeps.push (mkAtom sep) |>.push e } instance : EmptyCollection (SepArray sep) where @@ -1106,7 +1106,8 @@ set_option linter.unusedVariables.funArgs false in For example, the tactic will *not* be invoked during type class resolution. -/ abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α -/- Helper functions for manipulating interpolated strings -/ +/-! # Helper functions for manipulating interpolated strings -/ + namespace Lean.Syntax private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index c704923c1f..d212fea88a 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -37,7 +37,7 @@ macro "lead" : prec => `(1022) -- precedence used for terms not supposed to be u macro "(" p:prec ")" : prec => return p macro "min" : prec => `(10) -- minimum precedence used in term parsers macro "min1" : prec => `(11) -- `(min+1) we can only `min+1` after `Meta.lean` -/- +/-- `max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`. We use `max_prec` to workaround bootstrapping issues. -/ macro "max_prec" : term => `(1024) @@ -61,10 +61,10 @@ macro_rules | `(stx| $p ?) => `(stx| optional($p)) | `(stx| $p₁ <|> $p₂) => `(stx| orelse($p₁, $p₂)) -/- Comma-separated sequence. -/ +/-- Comma-separated sequence. -/ macro:arg x:stx:max ",*" : stx => `(stx| sepBy($x, ",", ", ")) macro:arg x:stx:max ",+" : stx => `(stx| sepBy1($x, ",", ", ")) -/- Comma-separated sequence with optional trailing comma. -/ +/-- Comma-separated sequence with optional trailing comma. -/ macro:arg x:stx:max ",*,?" : stx => `(stx| sepBy($x, ",", ", ", allowTrailingSep)) macro:arg x:stx:max ",+,?" : stx => `(stx| sepBy1($x, ",", ", ", allowTrailingSep)) @@ -89,7 +89,7 @@ infixr:80 " ^ " => HPow.hPow infixl:65 " ++ " => HAppend.hAppend prefix:100 "-" => Neg.neg prefix:100 "~~~" => Complement.complement -/- +/-! Remark: the infix commands above ensure a delaborator is generated for each relations. We redefine the macros below to be able to use the auxiliary `binop%` elaboration helper for binary operators. It addresses issue #382. -/ @@ -113,7 +113,7 @@ infix:50 " ≥ " => GE.ge infix:50 " > " => GT.gt infix:50 " = " => Eq infix:50 " == " => BEq.beq -/- +/-! Remark: the infix commands above ensure a delaborator is generated for each relations. We redefine the macros below to be able to use the auxiliary `binrel%` elaboration helper for binary relations. It has better support for applying coercions. For example, suppose we have `binrel% Eq n i` where `n : Nat` and @@ -189,7 +189,7 @@ macro_rules | `($a |> $f $args*) => `($f $args* $a) | `($a |> $f) => `($f $a) --- Haskell-like pipe <| +/-- Haskell-like pipe `<|` -/ -- Note that we have a whitespace after `$` to avoid an ambiguity with the antiquotations. syntax:min term atomic(" $" ws) term:min : term @@ -203,7 +203,7 @@ macro_rules | `({ $x : $type // $p }) => ``(Subtype (fun ($x:ident : $type) => $p)) | `({ $x // $p }) => ``(Subtype (fun ($x:ident : _) => $p)) -/- +/-- `without_expected_type t` instructs Lean to elaborate `t` without an expected type. Recall that terms such as `match ... with ...` and `⟨...⟩` will postpone elaboration until expected type is known. So, `without_expected_type` is not effective in this case. -/ diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index d5b66bd939..b9cc5e0e6c 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -207,7 +207,7 @@ macro_rules `(let y := %[ $[$y],* | $k ] %[ $[$z],* | y ]) -/- +/-- Expands ``` class abbrev C := D_1, ..., D_n @@ -241,7 +241,7 @@ macro_rules | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*) namespace Lean -/- `repeat` and `while` notation -/ +/-! # `repeat` and `while` notation -/ inductive Loop where | mk diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 8b0dcc06c0..507fca5fc4 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -86,9 +86,9 @@ theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ : theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) := h ▸ rfl -/- +/-! Initialize the Quotient Module, which effectively adds the following definitions: - +``` opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r @@ -98,6 +98,7 @@ opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} : (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q +``` -/ init_quot @@ -156,7 +157,7 @@ inductive Bool : Type where export Bool (false true) -/- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/ +/-- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/ structure Subtype {α : Sort u} (p : α → Prop) where val : α property : p val @@ -175,7 +176,7 @@ set_option linter.unusedVariables.funArgs false in /-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/ @[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a -/- Auxiliary axiom used to implement `sorry`. -/ +/-- Auxiliary axiom used to implement `sorry`. -/ @[extern "lean_sorry", neverExtract] axiom sorryAx (α : Sort u) (synthetic := false) : α @@ -236,14 +237,14 @@ deriving instance Inhabited for Bool structure PLift (α : Sort u) : Type u where up :: (down : α) -/- Bijection between α and PLift α -/ +/-- Bijection between α and PLift α -/ theorem PLift.up_down {α : Sort u} : ∀ (b : PLift α), Eq (up (down b)) b | up _ => rfl theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a := rfl -/- Pointed types -/ +/-- Pointed types -/ def NonemptyType := Subtype fun α : Type u => Nonempty α abbrev NonemptyType.type (type : NonemptyType.{u}) : Type u := @@ -256,7 +257,7 @@ instance : Inhabited NonemptyType.{u} where structure ULift.{r, s} (α : Type s) : Type (max s r) where up :: (down : α) -/- Bijection between α and ULift.{v} α -/ +/-- Bijection between α and ULift.{v} α -/ theorem ULift.up_down {α : Type u} : ∀ (b : ULift.{v} α), Eq (up (down b)) b | up _ => rfl @@ -329,7 +330,7 @@ instance [DecidableEq α] : BEq α where @[macroInline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α := Decidable.casesOn (motive := fun _ => α) h e t -/- if-then-else -/ +/-! # if-then-else -/ @[macroInline] def ite {α : Sort u} (c : Prop) [h : Decidable c] (t e : α) : α := Decidable.casesOn (motive := fun _ => α) h (fun _ => e) (fun _ => t) @@ -359,7 +360,7 @@ instance [dp : Decidable p] : Decidable (Not p) := | isTrue hp => isFalse (absurd hp) | isFalse hp => isTrue hp -/- Boolean operators -/ +/-! # Boolean operators -/ @[macroInline] def cond {α : Type u} (c : Bool) (x y : α) : α := match c with @@ -388,7 +389,7 @@ inductive Nat where instance : Inhabited Nat where default := Nat.zero -/- For numeric literals notation -/ +/-- For numeric literals notation -/ class OfNat (α : Type u) (_ : Nat) where ofNat : α @@ -1229,7 +1230,7 @@ unsafe def unsafeCast {α : Sort u} {β : Sort v} (a : α) : β := @[neverExtract, extern "lean_panic_fn"] opaque panicCore {α : Type u} [Inhabited α] (msg : String) : α -/- +/-- This is workaround for `panic` occurring in monadic code. See issue #695. The `panicCore` definition cannot be specialized since it is an extern. When `panic` occurs in monadic code, the `Inhabited α` parameter depends on a `[inst : Monad m]` instance. @@ -1249,7 +1250,7 @@ class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : o export GetElem (getElem) -/- +/-- The Compiler has special support for arrays. They are implemented using dynamic arrays: https://en.wikipedia.org/wiki/Dynamic_array -/ @@ -1259,7 +1260,7 @@ structure Array (α : Type u) where attribute [extern "lean_array_data"] Array.data attribute [extern "lean_array_mk"] Array.mk -/- The parameter `c` is the initial capacity -/ +/-- The parameter `c` is the initial capacity -/ @[extern "lean_mk_empty_array_with_capacity"] def Array.mkEmpty {α : Type u} (c : @& Nat) : Array α := { data := List.nil @@ -1279,7 +1280,7 @@ def Array.get {α : Type u} (a : @& Array α) (i : @& Fin a.size) : α := @[inline] abbrev Array.getD (a : Array α) (i : Nat) (v₀ : α) : α := dite (LT.lt i a.size) (fun h => a.get ⟨i, h⟩) (fun _ => v₀) -/- "Comfortable" version of `fget`. It performs a bound check at runtime. -/ +/-- "Comfortable" version of `fget`. It performs a bound check at runtime. -/ @[extern "lean_array_get"] def Array.get! {α : Type u} [Inhabited α] (a : @& Array α) (i : @& Nat) : α := Array.getD a i default @@ -1577,14 +1578,14 @@ instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadWithReaderOf ρ In contrast to the Haskell implementation, we use overlapping instances to derive instances automatically from `monadLift`. -/ class MonadStateOf (σ : Type u) (m : Type u → Type v) where - /- Obtain the top-most State of a Monad stack. -/ + /-- Obtain the top-most State of a Monad stack. -/ get : m σ - /- Set the top-most State of a Monad stack. -/ + /-- Set the top-most State of a Monad stack. -/ set : σ → m PUnit - /- Map the top-most State of a Monad stack. + /-- Map the top-most State of a Monad stack. - Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a` - because the latter does not use the State linearly (without sufficient inlining). -/ + Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a` + because the latter does not use the State linearly (without sufficient inlining). -/ modifyGet {α : Type u} : (σ → Prod α σ) → m α export MonadStateOf (set) @@ -1730,7 +1731,7 @@ instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where @[inline] def dummyRestore : σ → PUnit → σ := fun s _ => s -/- Dummy default instance -/ +/-- Dummy default instance -/ instance nonBacktrackable : Backtrackable PUnit σ where save := dummySave restore := dummyRestore @@ -1854,7 +1855,7 @@ instance : Append Name where end Name -/- Syntax -/ +/-! # Syntax -/ /-- Source information of tokens. -/ inductive SourceInfo where @@ -1889,7 +1890,7 @@ end SourceInfo abbrev SyntaxNodeKind := Name -/- Syntax AST -/ +/-! # Syntax AST -/ /-- Syntax objects used by the parser, macro expander, delaborator, etc. @@ -1915,7 +1916,7 @@ inductive Syntax where For example, both `a` and `a + b` have the same first identifier, and so their infos got mixed up.) - -/ + -/ node (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax | atom (info : SourceInfo) (val : String) : Syntax | ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Prod Name (List String))) : Syntax @@ -2098,7 +2099,7 @@ def mkAtom (val : String) : Syntax := def mkAtomFrom (src : Syntax) (val : String) : Syntax := Syntax.atom (SourceInfo.fromRef src) val -/- Parser descriptions -/ +/-! # Parser descriptions -/ inductive ParserDescr where | const (name : Name) @@ -2119,7 +2120,7 @@ instance : Inhabited ParserDescr where abbrev TrailingParserDescr := ParserDescr -/- +/-! Runtime support for making quotation terms auto-hygienic, by mangling identifiers introduced by them with a "macro scope" supplied by the context. Details to appear in a paper soon. @@ -2163,7 +2164,7 @@ class MonadQuotation (m : Type → Type) extends MonadRef m where /-- Get the fresh scope of the current macro invocation -/ getCurrMacroScope : m MacroScope getMainModule : m Name - /-- + /-- Execute action in a new macro invocation context. This transformer should be used at all places that morally qualify as the beginning of a "macro call", e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it @@ -2187,7 +2188,7 @@ instance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotatio getMainModule := liftM (m := m) getMainModule withFreshMacroScope := monadMap (m := m) withFreshMacroScope -/- +/-! We represent a name with macro scopes as ``` ._@.(.)*.._hyg. @@ -2230,7 +2231,7 @@ private def simpMacroScopesAux : Name → Name | .num p i => Name.mkNum (simpMacroScopesAux p) i | n => eraseMacroScopesAux n -/- Helper function we use to create binder names that do not need to be unique. -/ +/-- Helper function we use to create binder names that do not need to be unique. -/ @[export lean_simp_macro_scopes] def Name.simpMacroScopes (n : Name) : Name := match n.hasMacroScopes with @@ -2341,7 +2342,7 @@ end Syntax namespace Macro -/- References -/ +/-- References -/ private opaque MethodsRefPointed : NonemptyType.{0} private def MethodsRef : Type := MethodsRefPointed.type diff --git a/src/Init/SizeOf.lean b/src/Init/SizeOf.lean index 17682469ec..2aaf0e8891 100644 --- a/src/Init/SizeOf.lean +++ b/src/Init/SizeOf.lean @@ -6,19 +6,19 @@ Authors: Leonardo de Moura prelude import Init.Tactics -/- SizeOf -/ +/-! # SizeOf -/ class SizeOf (α : Sort u) where sizeOf : α → Nat export SizeOf (sizeOf) -/- +/-! Declare sizeOf instances and theorems for types declared before SizeOf. From now on, the inductive Compiler will automatically generate sizeOf instances and theorems. -/ -/- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/ +/-- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/ protected def default.sizeOf (α : Sort u) : α → Nat | _ => 0 @@ -62,7 +62,7 @@ deriving instance SizeOf for EStateM.Result namespace Lean -/- We manually define `Lean.Name` instance because we use +/-- We manually define `Lean.Name` instance because we use an opaque function for computing the hashcode field. -/ protected noncomputable def Name.sizeOf : Name → Nat | anonymous => 1 diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 1e62b8e42d..1919b54d67 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -91,7 +91,7 @@ set_option compiler.extract_closed false in @[extern "lean_io_timeit"] opaque timeit (msg : @& String) (fn : IO α) : IO α @[extern "lean_io_allocprof"] opaque allocprof (msg : @& String) (fn : IO α) : IO α -/- Programs can execute IO actions during initialization that occurs before +/-- Programs can execute IO actions during initialization that occurs before the `main` function is executed. The attribute `[init ]` specifies which IO action is executed to set the value of an opaque constant. @@ -511,21 +511,21 @@ def Stdio.toHandleType : Stdio → Type | Stdio.null => Unit structure StdioConfig where - /- Configuration for the process' stdin handle. -/ + /-- Configuration for the process' stdin handle. -/ stdin := Stdio.inherit - /- Configuration for the process' stdout handle. -/ + /-- Configuration for the process' stdout handle. -/ stdout := Stdio.inherit - /- Configuration for the process' stderr handle. -/ + /-- Configuration for the process' stderr handle. -/ stderr := Stdio.inherit structure SpawnArgs extends StdioConfig where - /- Command name. -/ + /-- Command name. -/ cmd : String - /- Arguments for the process -/ + /-- Arguments for the process -/ args : Array String := #[] - /- Working directory for the process. Inherit from current process if `none`. -/ + /-- Working directory for the process. Inherit from current process if `none`. -/ cwd : Option FilePath := none - /- Add or remove environment variables for the process. -/ + /-- Add or remove environment variables for the process. -/ env : Array (String × Option String) := #[] -- TODO(Sebastian): constructor must be private @@ -599,7 +599,7 @@ def FileRight.flags (acc : FileRight) : UInt32 := def setAccessRights (filename : FilePath) (mode : FileRight) : IO Unit := Prim.setAccessRights filename mode.flags -/- References -/ +/-- References -/ abbrev Ref (α : Type) := ST.Ref IO.RealWorld α instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩ diff --git a/src/Init/System/IOError.lean b/src/Init/System/IOError.lean index 91229e0702..63ad083a02 100644 --- a/src/Init/System/IOError.lean +++ b/src/Init/System/IOError.lean @@ -10,7 +10,7 @@ import Init.Data.UInt import Init.Data.ToString.Basic import Init.Data.String.Basic -/- +/-- Imitate the structure of IOErrorType in Haskell: https://hackage.haskell.org/package/base-4.12.0.0/docs/System-IO-Error.html#t:IOErrorType -/ diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean index f5550bcb56..106dd06704 100644 --- a/src/Init/System/ST.lean +++ b/src/Init/System/ST.lean @@ -41,7 +41,7 @@ instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s => namespace ST -/- References -/ +/-- References -/ opaque RefPointed : NonemptyType.{0} structure Ref (σ : Type) (α : Type) : Type where @@ -53,7 +53,7 @@ instance {σ α} [s : Nonempty α] : Nonempty (Ref σ α) := namespace Prim -/- Auxiliary definition for showing that `ST σ α` is inhabited when we have a `Ref σ α` -/ +/-- Auxiliary definition for showing that `ST σ α` is inhabited when we have a `Ref σ α` -/ private noncomputable def inhabitedFromRef {σ α} (r : Ref σ α) : ST σ α := let _ : Inhabited α := Classical.inhabited_of_nonempty r.h pure default diff --git a/src/Init/Util.lean b/src/Init/Util.lean index b092ac9afb..d023c2c784 100644 --- a/src/Init/Util.lean +++ b/src/Init/Util.lean @@ -10,14 +10,15 @@ import Init.Data.ToString.Basic universe u v set_option linter.unusedVariables.funArgs false -/- debugging helper functions -/ +/-! # Debugging helper functions -/ + @[neverExtract, extern "lean_dbg_trace"] def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α := f () def dbgTraceVal {α : Type u} [ToString α] (a : α) : α := dbgTrace (toString a) (fun _ => a) -/- Display the given message if `a` is shared, that is, RC(a) > 1 -/ +/-- Display the given message if `a` is shared, that is, RC(a) > 1 -/ @[neverExtract, extern "lean_dbg_trace_if_shared"] def dbgTraceIfShared {α : Type u} (s : String) (a : α) : α := a diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 51956c2638..6bdb1875cf 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -55,7 +55,7 @@ open Std (PersistentHashMap) builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) ← IO.mkRef {} -/- Low level attribute registration function. -/ +/-- Low level attribute registration function. -/ def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do let m ← attributeMapRef.get if m.contains attr.name then throw (IO.userError ("invalid builtin attribute declaration, '" ++ toString attr.name ++ "' has already been used")) @@ -63,7 +63,7 @@ def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do throw (IO.userError "failed to register attribute, attributes can only be registered during initialization") attributeMapRef.modify fun m => m.insert attr.name attr -/- +/-! Helper methods for decoding the parameters of builtin attributes that are defined before `Lean.Parser`. We have the following ones: ``` @@ -235,7 +235,7 @@ def setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (de end ParametricAttribute -/- +/-- Given a list `[a₁, ..., a_n]` of elements of type `α`, `EnumAttributes` provides an attribute `Attr_i` for associating a value `a_i` with an declaration. `α` is usually an enumeration type. Note that whenever we register an `EnumAttributes`, we create `n` attributes, but only one environment extension. -/ @@ -294,7 +294,7 @@ def setValue {α : Type} (attrs : EnumAttributes α) (env : Environment) (decl : end EnumAttributes -/- +/-! Attribute extension and builders. We use builders to implement attribute factories for parser categories. -/ @@ -371,12 +371,12 @@ builtin_initialize attributeExtension : AttributeExtension ← statsFn := fun s => format "number of local entries: " ++ format s.newEntries.length } -/- Return true iff `n` is the name of a registered attribute. -/ +/-- Return true iff `n` is the name of a registered attribute. -/ @[export lean_is_attribute] def isBuiltinAttribute (n : Name) : IO Bool := do let m ← attributeMapRef.get; pure (m.contains n) -/- Return the name of all registered attributes. -/ +/-- Return the name of all registered attributes. -/ def getBuiltinAttributeNames : IO (List Name) := return (← attributeMapRef.get).foldl (init := []) fun r n _ => n::r diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean index f249789bc1..350663d9a0 100644 --- a/src/Lean/Compiler/ConstFolding.lean +++ b/src/Lean/Compiler/ConstFolding.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura import Lean.Expr import Lean.Compiler.Util -/- Constant folding for primitives that have special runtime support. -/ +/-! Constant folding for primitives that have special runtime support. -/ namespace Lean.Compiler diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index 3095d13e53..8e456e0887 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/src/Lean/Compiler/ExternAttr.lean @@ -17,7 +17,7 @@ inductive ExternEntry where | standard (backend : Name) (fn : String) | foreign (backend : Name) (fn : String) -/- +/-- - `@[extern]` encoding: ```.entries = [adhoc `all]``` - `@[extern "level_hash"]` @@ -123,7 +123,7 @@ def getExternEntryFor (d : ExternAttrData) (backend : Name) : Option ExternEntry def isExtern (env : Environment) (fn : Name) : Bool := getExternAttrData env fn |>.isSome -/- We say a Lean function marked as `[extern ""]` is for all backends, and it is implemented using `extern "C"`. +/-- We say a Lean function marked as `[extern ""]` is for all backends, and it is implemented using `extern "C"`. Thus, there is no name mangling. -/ def isExternC (env : Environment) (fn : Name) : Bool := match getExternAttrData env fn with diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 16199b9730..2702889daa 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -7,7 +7,7 @@ import Lean.Data.KVMap import Lean.Data.Name import Lean.Data.Format import Lean.Compiler.ExternAttr -/- +/-! Implements (extended) λPure and λRc proposed in the article "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura. @@ -17,15 +17,15 @@ above are implemented in Lean. -/ namespace Lean.IR -/- Function identifier -/ +/-- Function identifier -/ abbrev FunId := Name abbrev Index := Nat -/- Variable identifier -/ +/-- Variable identifier -/ structure VarId where idx : Index deriving Inhabited -/- Join point identifier -/ +/-- Join point identifier -/ structure JoinPointId where idx : Index deriving Inhabited @@ -45,7 +45,7 @@ instance : Hashable JoinPointId := ⟨fun a => hash a.idx⟩ abbrev MData := KVMap abbrev MData.empty : MData := {} -/- Low Level IR types. Most are self explanatory. +/-- Low Level IR types. Most are self explanatory. - `usize` represents the C++ `size_t` Type. We have it here because it is 32-bit in 32-bit machines, and 64-bit in 64-bit machines, @@ -130,7 +130,7 @@ def isUnion : IRType → Bool end IRType -/- Arguments to applications, constructors, etc. +/-- Arguments to applications, constructors, etc. We use `irrelevant` for Lean types, propositions and proofs that have been erased. Recall that for a Function `f`, we also generate `f._rarg` which does not take `irrelevant` arguments. However, `f._rarg` is only safe to be used in full applications. -/ @@ -159,7 +159,7 @@ def LitVal.beq : LitVal → LitVal → Bool instance : BEq LitVal := ⟨LitVal.beq⟩ -/- Constructor information. +/-- Constructor information. - `name` is the Name of the Constructor in Lean. - `cidx` is the Constructor index (aka tag). @@ -191,36 +191,36 @@ def CtorInfo.isScalar (info : CtorInfo) : Bool := !info.isRef inductive Expr where - /- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime. - This instruction is also used to creat `struct` and `union` return values. - For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant. -/ - | ctor (i : CtorInfo) (ys : Array Arg) + | /-- We use `ctor` mainly for constructing Lean object/tobject values `lean_ctor_object` in the runtime. + This instruction is also used to creat `struct` and `union` return values. + For `union`, only `i.cidx` is relevant. For `struct`, `i` is irrelevant. -/ + ctor (i : CtorInfo) (ys : Array Arg) | reset (n : Nat) (x : VarId) - /- `reuse x in ctor_i ys` instruction in the paper. -/ - | reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg) - /- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`. - We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/ - | proj (i : Nat) (x : VarId) - /- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/ - | uproj (i : Nat) (x : VarId) - /- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/ - | sproj (n : Nat) (offset : Nat) (x : VarId) - /- Full application. -/ - | fap (c : FunId) (ys : Array Arg) - /- Partial application that creates a `pap` value (aka closure in our nonstandard terminology). -/ - | pap (c : FunId) (ys : Array Arg) - /- Application. `x` must be a `pap` value. -/ - | ap (x : VarId) (ys : Array Arg) - /- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`. + | /-- `reuse x in ctor_i ys` instruction in the paper. -/ + reuse (x : VarId) (i : CtorInfo) (updtHeader : Bool) (ys : Array Arg) + | /-- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`. + We also use `proj` for extracting fields from `struct` return values, and casting `union` return values. -/ + proj (i : Nat) (x : VarId) + | /-- Extract the `Usize` value at Position `sizeof(void*)*i` from `x`. -/ + uproj (i : Nat) (x : VarId) + | /-- Extract the scalar value at Position `sizeof(void*)*n + offset` from `x`. -/ + sproj (n : Nat) (offset : Nat) (x : VarId) + | /-- Full application. -/ + fap (c : FunId) (ys : Array Arg) + | /-- Partial application that creates a `pap` value (aka closure in our nonstandard terminology). -/ + pap (c : FunId) (ys : Array Arg) + | /-- Application. `x` must be a `pap` value. -/ + ap (x : VarId) (ys : Array Arg) + | /-- Given `x : ty` where `ty` is a scalar type, this operation returns a value of Type `tobject`. For small scalar values, the Result is a tagged pointer, and no memory allocation is performed. -/ - | box (ty : IRType) (x : VarId) - /- Given `x : [t]object`, obtain the scalar value. -/ - | unbox (x : VarId) + box (ty : IRType) (x : VarId) + | /-- Given `x : [t]object`, obtain the scalar value. -/ + unbox (x : VarId) | lit (v : LitVal) - /- Return `1 : uint8` Iff `RC(x) > 1` -/ - | isShared (x : VarId) - /- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/ - | isTaggedPtr (x : VarId) + | /-- Return `1 : uint8` Iff `RC(x) > 1` -/ + isShared (x : VarId) + | /-- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/ + isTaggedPtr (x : VarId) @[export lean_ir_mk_ctor_expr] def mkCtorExpr (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (ys : Array Arg) : Expr := Expr.ctor ⟨n, cidx, size, usize, ssize⟩ ys @@ -247,31 +247,31 @@ inductive AltCore (FnBody : Type) : Type where | default (b : FnBody) : AltCore FnBody inductive FnBody where - /- `let x : ty := e; b` -/ - | vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) - /- Join point Declaration `block_j (xs) := e; b` -/ - | jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody) - /- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. - This operation is not part of λPure is only used during optimization. -/ - | set (x : VarId) (i : Nat) (y : Arg) (b : FnBody) + | /-- `let x : ty := e; b` -/ + vdecl (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) + | /-- Join point Declaration `block_j (xs) := e; b` -/ + jdecl (j : JoinPointId) (xs : Array Param) (v : FnBody) (b : FnBody) + | /-- Store `y` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. + This operation is not part of λPure is only used during optimization. -/ + set (x : VarId) (i : Nat) (y : Arg) (b : FnBody) | setTag (x : VarId) (cidx : Nat) (b : FnBody) - /- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/ - | uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody) - /- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. + | /-- Store `y : Usize` at Position `sizeof(void*)*i` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. -/ + uset (x : VarId) (i : Nat) (y : VarId) (b : FnBody) + | /-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1. `ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/ - | sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) - /- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. + sset (x : VarId) (i : Nat) (offset : Nat) (y : VarId) (ty : IRType) (b : FnBody) + | /-- RC increment for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. If `persistent == true` then `x` is statically known to be a persistent object. -/ - | inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) - /- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. + inc (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) + | /-- RC decrement for `object`. If c == `true`, then `inc` must check whether `x` is a tagged pointer or not. If `persistent == true` then `x` is statically known to be a persistent object. -/ - | dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) + dec (x : VarId) (n : Nat) (c : Bool) (persistent : Bool) (b : FnBody) | del (x : VarId) (b : FnBody) | mdata (d : MData) (b : FnBody) | case (tid : Name) (x : VarId) (xType : IRType) (cs : Array (AltCore FnBody)) | ret (x : Arg) - /- Jump to join point `j` -/ - | jmp (j : JoinPointId) (ys : Array Arg) + | /-- Jump to join point `j` -/ + jmp (j : JoinPointId) (ys : Array Arg) | unreachable instance : Inhabited FnBody := ⟨FnBody.unreachable⟩ @@ -331,7 +331,7 @@ def FnBody.setBody : FnBody → FnBody → FnBody @[inline] def FnBody.resetBody (b : FnBody) : FnBody := b.setBody FnBody.nil -/- If b is a non terminal, then return a pair `(c, b')` s.t. `b == c <;> b'`, +/-- If b is a non terminal, then return a pair `(c, b')` s.t. `b == c <;> b'`, and c.body == FnBody.nil -/ @[inline] def FnBody.split (b : FnBody) : FnBody × FnBody := let b' := b.body diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index 56988b9d79..591a4eb9f3 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/src/Lean/Compiler/IR/Borrow.lean @@ -29,7 +29,7 @@ abbrev OwnedSet := Std.HashMap Key Unit def OwnedSet.insert (s : OwnedSet) (k : OwnedSet.Key) : OwnedSet := Std.HashMap.insert s k () def OwnedSet.contains (s : OwnedSet) (k : OwnedSet.Key) : Bool := Std.HashMap.contains s k -/- We perform borrow inference in a block of mutually recursive functions. +/-! We perform borrow inference in a block of mutually recursive functions. Join points are viewed as local functions, and are identified using their local id + the name of the surrounding function. We keep a mapping from function and joint points to parameters (`Array Param`). @@ -63,11 +63,11 @@ instance : ToFormat ParamMap := ⟨ParamMap.fmt⟩ instance : ToString ParamMap := ⟨fun m => Format.pretty (format m)⟩ namespace InitParamMap -/- Mark parameters that take a reference as borrow -/ +/-- Mark parameters that take a reference as borrow -/ def initBorrow (ps : Array Param) : Array Param := ps.map fun p => { p with borrow := p.ty.isObj } -/- We do perform borrow inference for constants marked as `export`. +/-- We do perform borrow inference for constants marked as `export`. Reason: we current write wrappers in C++ for using exported functions. These wrappers use smart pointers such as `object_ref`. When writing a new wrapper we need to know whether an argument is a borrow @@ -100,7 +100,7 @@ end InitParamMap def mkInitParamMap (env : Environment) (decls : Array Decl) : ParamMap := (InitParamMap.visitDecls env decls *> get).run' {} -/- Apply the inferred borrow annotations stored at `ParamMap` to a block of mutually +/-! Apply the inferred borrow annotations stored at `ParamMap` to a block of mutually recursive functions. -/ namespace ApplyParamMap @@ -141,7 +141,7 @@ structure BorrowInfCtx where paramSet : IndexSet := {} -- Set of all function parameters in scope. This is used to implement the heuristic at `ownArgsUsingParams` structure BorrowInfState where - /- Set of variables that must be `owned`. -/ + /-- Set of variables that must be `owned`. -/ owned : OwnedSet := {} modified : Bool := false paramMap : ParamMap @@ -174,7 +174,7 @@ def isOwned (x : VarId) : M Bool := do let s ← get return s.owned.contains (currFn, x.idx) -/- Updates `map[k]` using the current set of `owned` variables. -/ +/-- Updates `map[k]` using the current set of `owned` variables. -/ def updateParamMap (k : ParamMap.Key) : M Unit := do let s ← get match s.paramMap.find? k with @@ -202,14 +202,14 @@ def getParamInfo (k : ParamMap.Key) : M (Array Param) := do | none => unreachable! | _ => unreachable! -/- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/ +/-- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/ def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit := xs.size.forM fun i => do let x := xs[i]! let p := ps[i]! unless p.borrow do ownArg x -/- For each xs[i], if xs[i] is owned, then mark ps[i] as owned. +/-- For each xs[i], if xs[i] is owned, then mark ps[i] as owned. We use this action to preserve tail calls. That is, if we have a tail call `f xs`, if the i-th parameter is borrowed, but `xs[i]` is owned we would have to insert a `dec xs[i]` after `f xs` and consequently @@ -222,7 +222,7 @@ def ownParamsUsingArgs (xs : Array Arg) (ps : Array Param) : M Unit := | Arg.var x => if (← isOwned x) then ownVar p.x | _ => pure () -/- Mark `xs[i]` as owned if it is one of the parameters `ps`. +/-- Mark `xs[i]` as owned if it is one of the parameters `ps`. We use this action to mark function parameters that are being "packed" inside constructors. This is a heuristic, and is not related with the effectiveness of the reset/reuse optimization. It is useful for code such as @@ -287,7 +287,7 @@ partial def collectDecl : Decl → M Unit updateParamMap (ParamMap.Key.decl f) | _ => pure () -/- Keep executing `x` until it reaches a fixpoint -/ +/-- Keep executing `x` until it reaches a fixpoint -/ @[inline] partial def whileModifing (x : M Unit) : M Unit := do modify fun s => { s with modified := false } x diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean index 8fae3896e3..ddddb66e79 100644 --- a/src/Lean/Compiler/IR/Boxing.lean +++ b/src/Lean/Compiler/IR/Boxing.lean @@ -12,7 +12,7 @@ import Lean.Compiler.IR.FreeVars import Lean.Compiler.IR.ElimDeadVars namespace Lean.IR.ExplicitBoxing -/- +/-! Add explicit boxing and unboxing instructions. Recall that the Lean to λ_pure compiler produces code without these instructions. @@ -74,7 +74,7 @@ def addBoxedVersions (env : Environment) (decls : Array Decl) : Array Decl := if requiresBoxedVersion env decl then newDecls.push (mkBoxedVersion decl) else newDecls decls ++ boxedDecls -/- Infer scrutinee type using `case` alternatives. +/-- Infer scrutinee type using `case` alternatives. This can be done whenever `alts` does not contain an `Alt.default _` value. -/ def getScrutineeType (alts : Array Alt) : IRType := let isScalar := @@ -103,7 +103,7 @@ structure BoxingContext where structure BoxingState where nextIdx : Index - /- We create auxiliary declarations when boxing constant and literals. + /-- We create auxiliary declarations when boxing constant and literals. The idea is to avoid code such as ``` let x1 := Uint64.inhabited; @@ -155,7 +155,7 @@ def getDecl (fid : FunId) : M Decl := do @[inline] def withJDecl {α : Type} (j : JoinPointId) (xs : Array Param) (v : FnBody) (k : M α) : M α := withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addJP j xs v }) k -/- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c #[]`, +/-- If `x` declaration is of the form `x := Expr.lit _` or `x := Expr.fap c #[]`, and `x`'s type is not cheap to box (e.g., it is `UInt64), then return its value. -/ private def isExpensiveConstantValueBoxing (x : VarId) (xType : IRType) : M (Option Expr) := if !xType.isScalar then @@ -173,7 +173,7 @@ private def isExpensiveConstantValueBoxing (x : VarId) (xType : IRType) : M (Opt | _ => return none | _ => return none -/- Auxiliary function used by castVarIfNeeded. +/-- Auxiliary function used by castVarIfNeeded. It is used when the expected type does not match `xType`. If `xType` is scalar, then we need to "box" it. Otherwise, we need to "unbox" it. -/ def mkCast (x : VarId) (xType : IRType) (expectedType : IRType) : M Expr := do diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean index 0c0d39af90..e4cecf98f6 100644 --- a/src/Lean/Compiler/IR/CompilerM.lean +++ b/src/Lean/Compiler/IR/CompilerM.lean @@ -73,7 +73,7 @@ open Std (HashMap) abbrev DeclMap := SMap Name Decl -/- Create an array of decls to be saved on .olean file. +/-- Create an array of decls to be saved on .olean file. `decls` may contain duplicate entries, but we assume the one that occurs last is the most recent one. -/ private def mkEntryArray (decls : List Decl) : Array Decl := /- Remove duplicates by adding decls into a map -/ diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean index b680be6a44..874e9f96f5 100644 --- a/src/Lean/Compiler/IR/EmitC.lean +++ b/src/Lean/Compiler/IR/EmitC.lean @@ -530,7 +530,7 @@ def paramEqArg (p : Param) (x : Arg) : Bool := | Arg.var x => p.x == x | _ => false -/- +/-- Given `[p_0, ..., p_{n-1}]`, `[y_0, ..., y_{n-1}]`, representing the assignments ``` p_0 := y_0, diff --git a/src/Lean/Compiler/IR/EmitUtil.lean b/src/Lean/Compiler/IR/EmitUtil.lean index 86b1922ae0..bcce85879d 100644 --- a/src/Lean/Compiler/IR/EmitUtil.lean +++ b/src/Lean/Compiler/IR/EmitUtil.lean @@ -6,10 +6,10 @@ Authors: Leonardo de Moura import Lean.Compiler.InitAttr import Lean.Compiler.IR.CompilerM -/- Helper functions for backend code generators -/ +/-! # Helper functions for backend code generators -/ namespace Lean.IR -/- Return true iff `b` is of the form `let x := g ys; ret x` -/ +/-- Return true iff `b` is of the form `let x := g ys; ret x` -/ def isTailCallTo (g : Name) (b : FnBody) : Bool := match b with | FnBody.vdecl x _ (Expr.fap f _) (FnBody.ret (Arg.var y)) => x == y && f == g @@ -62,7 +62,7 @@ def collectParams (ps : Array Param) : Collector := @[inline] def collectJP (j : JoinPointId) (xs : Array Param) : Collector | (vs, js) => (vs, js.insert j xs) -/- `collectFnBody` assumes the variables in -/ +/-- `collectFnBody` assumes the variables in -/ partial def collectFnBody : FnBody → Collector | FnBody.vdecl x t _ b => collectVar x t ∘ collectFnBody b | FnBody.jdecl j xs v b => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b @@ -75,7 +75,7 @@ def collectDecl : Decl → Collector end CollectMaps -/- Return a pair `(v, j)`, where `v` is a mapping from variable/parameter to type, +/-- Return a pair `(v, j)`, where `v` is a mapping from variable/parameter to type, and `j` is a mapping from join point to parameters. This function assumes `d` has normalized indexes (see `normids.lean`). -/ def mkVarJPMaps (d : Decl) : VarTypeMap × JPParamsMap := diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean index feb2201b11..9d7363e2f8 100644 --- a/src/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean @@ -8,7 +8,7 @@ import Lean.Compiler.IR.NormIds import Lean.Compiler.IR.FreeVars namespace Lean.IR.ExpandResetReuse -/- Mapping from variable to projections -/ +/-- Mapping from variable to projections -/ abbrev ProjMap := Std.HashMap VarId Expr namespace CollectProjMap abbrev Collector := ProjMap → ProjMap @@ -26,7 +26,7 @@ partial def collectFnBody : FnBody → Collector | e => if e.isTerminal then id else collectFnBody e.body end CollectProjMap -/- Create a mapping from variables to projections. +/-- Create a mapping from variables to projections. This function assumes variable ids have been normalized -/ def mkProjMap (d : Decl) : ProjMap := match d with @@ -36,7 +36,7 @@ def mkProjMap (d : Decl) : ProjMap := structure Context where projMap : ProjMap -/- Return true iff `x` is consumed in all branches of the current block. +/-- Return true iff `x` is consumed in all branches of the current block. Here consumption means the block contains a `dec x` or `reuse x ...`. -/ partial def consumed (x : VarId) : FnBody → Bool | FnBody.vdecl _ _ v b => @@ -49,7 +49,7 @@ partial def consumed (x : VarId) : FnBody → Bool abbrev Mask := Array (Option VarId) -/- Auxiliary function for eraseProjIncFor -/ +/-- Auxiliary function for eraseProjIncFor -/ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (keep : Array FnBody) : Array FnBody × Mask := let done (_ : Unit) := (bs ++ keep.reverse, mask) let keepInstr (b : FnBody) := eraseProjIncForAux y bs.pop mask (keep.push b) @@ -81,12 +81,12 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke | _ => done () | _ => done () -/- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`. +/-- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`. Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/ def eraseProjIncFor (n : Nat) (y : VarId) (bs : Array FnBody) : Array FnBody × Mask := eraseProjIncForAux y bs (mkArray n none) #[] -/- Replace `reuse x ctor ...` with `ctor ...`, and remoce `dec x` -/ +/-- Replace `reuse x ctor ...` with `ctor ...`, and remoce `dec x` -/ partial def reuseToCtor (x : VarId) : FnBody → FnBody | FnBody.dec y n c p b => if x == y then b -- n must be 1 since `x := reset ...` @@ -109,7 +109,7 @@ partial def reuseToCtor (x : VarId) : FnBody → FnBody let b := reuseToCtor x b instr.setBody b -/- +/-- replace ``` x := reset y; b @@ -143,7 +143,7 @@ def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody := def setFields (y : VarId) (zs : Array Arg) (b : FnBody) : FnBody := zs.size.fold (init := b) fun i b => FnBody.set y i (zs.get! i) b -/- Given `set x[i] := y`, return true iff `y := proj[i] x` -/ +/-- Given `set x[i] := y`, return true iff `y := proj[i] x` -/ def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool := match y with | Arg.var y => @@ -152,19 +152,19 @@ def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool := | _ => false | _ => false -/- Given `uset x[i] := y`, return true iff `y := uproj[i] x` -/ +/-- Given `uset x[i] := y`, return true iff `y := uproj[i] x` -/ def isSelfUSet (ctx : Context) (x : VarId) (i : Nat) (y : VarId) : Bool := match ctx.projMap.find? y with | some (Expr.uproj j w) => j == i && w == x | _ => false -/- Given `sset x[n, i] := y`, return true iff `y := sproj[n, i] x` -/ +/-- Given `sset x[n, i] := y`, return true iff `y := sproj[n, i] x` -/ def isSelfSSet (ctx : Context) (x : VarId) (n : Nat) (i : Nat) (y : VarId) : Bool := match ctx.projMap.find? y with | some (Expr.sproj m j w) => n == m && j == i && w == x | _ => false -/- Remove unnecessary `set/uset/sset` operations -/ +/-- Remove unnecessary `set/uset/sset` operations -/ partial def removeSelfSet (ctx : Context) : FnBody → FnBody | FnBody.set x i y b => if isSelfSet ctx x i y then removeSelfSet ctx b @@ -208,7 +208,7 @@ partial def reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody let b := reuseToSet ctx x y b instr.setBody b -/- +/-- replace ``` x := reset y; b diff --git a/src/Lean/Compiler/IR/FreeVars.lean b/src/Lean/Compiler/IR/FreeVars.lean index 4b5c4a395a..848fce0309 100644 --- a/src/Lean/Compiler/IR/FreeVars.lean +++ b/src/Lean/Compiler/IR/FreeVars.lean @@ -8,7 +8,7 @@ import Lean.Compiler.IR.Basic namespace Lean.IR namespace MaxIndex -/- Compute the maximum index `M` used in a declaration. +/-! Compute the maximum index `M` used in a declaration. We `M` to initialize the fresh index generator used to create fresh variable and join point names. @@ -85,7 +85,7 @@ def Decl.maxIndex (d : Decl) : Index := MaxIndex.collectDecl d 0 namespace FreeIndices -/- We say a variable (join point) index (aka name) is free in a function body +/-! We say a variable (join point) index (aka name) is free in a function body if there isn't a `FnBody.vdecl` (`Fnbody.jdecl`) binding it. -/ abbrev Collector := IndexSet → IndexSet → IndexSet @@ -177,7 +177,7 @@ def FnBody.freeIndices (b : FnBody) : IndexSet := b.collectFreeIndices {} namespace HasIndex -/- In principle, we can check whether a function body `b` contains an index `i` using +/-! In principle, we can check whether a function body `b` contains an index `i` using `b.freeIndices.contains i`, but it is more efficient to avoid the construction of the set of freeIndices and just search whether `i` occurs in `b` or not. -/ diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index d83ff85765..bbdaa02d0b 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ b/src/Lean/Compiler/IR/LiveVars.lean @@ -8,7 +8,7 @@ import Lean.Compiler.IR.FreeVars namespace Lean.IR -/- Remark: in the paper "Counting Immutable Beans" the concepts of +/-! Remark: in the paper "Counting Immutable Beans" the concepts of free and live variables coincide because the paper does *not* consider join points. For example, consider the function body `B` ``` @@ -20,13 +20,13 @@ namespace Lean.IR block_1 (x : obj) : obj := let z := ctor_0 x y; ret z - `` + ``` The variable `y` is live in the function body `B` since it occurs in `block_1` which is "invoked" by `B`. -/ namespace IsLive -/- +/-- We use `State Context` instead of `ReaderT Context Id` because we remove non local joint points from `Context` whenever we visit them instead of maintaining a set of visited non local join points. @@ -69,7 +69,7 @@ partial def visitFnBody (w : Index) : FnBody → M Bool end IsLive -/- Return true if `x` is live in the function body `b` in the context `ctx`. +/-- Return true if `x` is live in the function body `b` in the context `ctx`. Remark: the context only needs to contain all (free) join point declarations. diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean index b71d961385..02ee71405d 100644 --- a/src/Lean/Compiler/IR/NormIds.lean +++ b/src/Lean/Compiler/IR/NormIds.lean @@ -29,7 +29,7 @@ partial def checkDecl : Decl → M Bool end UniqueIds -/- Return true if variable, parameter and join point ids are unique -/ +/-- Return true if variable, parameter and join point ids are unique -/ def Decl.uniqueIds (d : Decl) : Bool := (UniqueIds.checkDecl d).run' {} @@ -119,11 +119,11 @@ def normDecl (d : Decl) : N Decl := end NormalizeIds -/- Create a declaration equivalent to `d` s.t. `d.normalizeIds.uniqueIds == true` -/ +/-- Create a declaration equivalent to `d` s.t. `d.normalizeIds.uniqueIds == true` -/ def Decl.normalizeIds (d : Decl) : Decl := (NormalizeIds.normDecl d {}).run' 1 -/- Apply a function `f : VarId → VarId` to variable occurrences. +/-! Apply a function `f : VarId → VarId` to variable occurrences. The following functions assume the IR code does not have variable shadowing. -/ namespace MapVars @@ -171,7 +171,7 @@ end MapVars @[inline] def FnBody.mapVars (f : VarId → VarId) (b : FnBody) : FnBody := MapVars.mapFnBody f b -/- Replace `x` with `y` in `b`. This function assumes `b` does not shadow `x` -/ +/-- Replace `x` with `y` in `b`. This function assumes `b` does not shadow `x` -/ def FnBody.replaceVar (x y : VarId) (b : FnBody) : FnBody := b.mapVars fun z => if x == z then y else z diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 7b4a7b0515..c45b640251 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -8,7 +8,7 @@ import Lean.Compiler.IR.CompilerM import Lean.Compiler.IR.LiveVars namespace Lean.IR.ExplicitRC -/- Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions. +/-! Insert explicit RC instructions. So, it assumes the input code does not contain `inc` nor `dec` instructions. This transformation is applied before lower level optimizations that introduce the instructions `release` and `set` -/ @@ -74,12 +74,12 @@ private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) caseLiveVars.fold (init := b) fun b x => if !altLiveVars.contains x && mustConsume ctx x then addDec ctx x b else b -/- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/ +/-- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/ private def isFirstOcc (xs : Array Arg) (i : Nat) : Bool := let x := xs[i]! i.all fun j => xs[j]! != x -/- Return true if `x` also occurs in `ys` in a position that is not consumed. +/-- Return true if `x` also occurs in `ys` in a position that is not consumed. That is, it is also passed as a borrow reference. -/ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Nat → Bool) : Bool := ys.size.any fun i => @@ -91,7 +91,7 @@ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Na private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool := isBorrowParamAux x ys fun i => not ps[i]!.borrow -/- +/-- Return `n`, the number of times `x` is consumed. - `ys` is a sequence of instruction parameters where we search for `x`. - `consumeParamPred i = true` if parameter `i` is consumed. @@ -124,7 +124,7 @@ private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred : private def addIncBefore (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody := addIncBeforeAux ctx xs (fun i => not ps[i]!.borrow) b liveVarsAfter -/- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application. -/ +/-- See `addIncBeforeAux`/`addIncBefore` for the procedure that inserts `inc` operations before an application. -/ private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody := xs.size.fold (init := b) fun i b => match xs[i]! with @@ -141,7 +141,7 @@ xs.size.fold (init := b) fun i b => private def addIncBeforeConsumeAll (ctx : Context) (xs : Array Arg) (b : FnBody) (liveVarsAfter : LiveVarSet) : FnBody := addIncBeforeAux ctx xs (fun _ => true) b liveVarsAfter -/- Add `dec` instructions for parameters that are references, are not alive in `b`, and are not borrow. +/-- Add `dec` instructions for parameters that are references, are not alive in `b`, and are not borrow. That is, we must make sure these parameters are consumed. -/ private def addDecForDeadParams (ctx : Context) (ps : Array Param) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody := ps.foldl (init := b) fun b p => @@ -151,14 +151,14 @@ private def isPersistent : Expr → Bool | Expr.fap _ xs => xs.isEmpty -- all global constants are persistent objects | _ => false -/- We do not need to consume the projection of a variable that is not consumed -/ +/-- We do not need to consume the projection of a variable that is not consumed -/ private def consumeExpr (m : VarMap) : Expr → Bool | Expr.proj _ x => match m.find? x with | some info => info.consume | none => true | _ => true -/- Return true iff `v` at runtime is a scalar value stored in a tagged pointer. +/-- Return true iff `v` at runtime is a scalar value stored in a tagged pointer. We do not need RC operations for this kind of value. -/ private def isScalarBoxedInTaggedPtr (v : Expr) : Bool := match v with diff --git a/src/Lean/Compiler/IR/ResetReuse.lean b/src/Lean/Compiler/IR/ResetReuse.lean index 0e519ef415..2793c7e402 100644 --- a/src/Lean/Compiler/IR/ResetReuse.lean +++ b/src/Lean/Compiler/IR/ResetReuse.lean @@ -8,11 +8,11 @@ import Lean.Compiler.IR.LiveVars import Lean.Compiler.IR.Format namespace Lean.IR.ResetReuse -/- Remark: the insertResetReuse transformation is applied before we have +/-! Remark: the insertResetReuse transformation is applied before we have inserted `inc/dec` instructions, and perfomed lower level optimizations that introduce the instructions `release` and `set`. -/ -/- Remark: the functions `S`, `D` and `R` defined here implement the +/-! Remark: the functions `S`, `D` and `R` defined here implement the corresponding functions in the paper "Counting Immutable Beans" Here are the main differences: @@ -50,7 +50,7 @@ private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody (instr, b) := b.split instr.setBody (S w c b) -/- We use `Context` to track join points in scope. -/ +/-- We use `Context` to track join points in scope. -/ abbrev M := ReaderT LocalContext (StateT Index Id) private def mkFresh : M VarId := do @@ -77,7 +77,7 @@ private def isCtorUsing (b : FnBody) (x : VarId) : Bool := | (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x | _ => false -/- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`, +/-- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`, and `flag == true` if `x` is live in `b`. Note that, in the function `D` defined in the paper, for each `let x := e; F`, diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean index 9f825302d2..421733fac7 100644 --- a/src/Lean/Compiler/Util.lean +++ b/src/Lean/Compiler/Util.lean @@ -57,7 +57,7 @@ def atMostOnce (e : Expr) (x : FVarId) : Bool := let {result := result, ..} := visit x e {found := false, result := true} result -/- Helper functions for creating auxiliary names used in compiler passes. -/ +/-! Helper functions for creating auxiliary names used in compiler passes. -/ @[export lean_mk_eager_lambda_lifting_name] def mkEagerLambdaLiftingName (n : Name) (idx : Nat) : Name := @@ -104,14 +104,14 @@ end Compiler namespace Environment -/- +/-- Compile the given block of mutual declarations. Assumes the declarations have already been added to the environment using `addDecl`. -/ @[extern "lean_compile_decls"] opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment -/- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/ +/-- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/ def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := compileDecls env opt (Compiler.getDeclNamesForCodeGen decl) diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index 8915f0f881..d9878ead31 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/src/Lean/Data/FuzzyMatching.lean @@ -42,7 +42,7 @@ private def containsInOrderLower (a b : String) : Bool := Id.run do end Utils -/- Represents the type of a single character. -/ +/-- Represents the type of a single character. -/ inductive CharType where | lower | upper | separator @@ -55,7 +55,7 @@ def charType (c : Char) : CharType := CharType.separator -/- Represents the role of a character inside a word. -/ +/-- Represents the role of a character inside a word. -/ inductive CharRole where | head | tail | separator deriving Inhabited @@ -72,7 +72,7 @@ inductive CharRole where else CharRole.head -/- Add additional information to each character in a string. -/ +/-- Add additional information to each character in a string. -/ private def stringInfo (s : String) : Array CharRole := iterateLookaround (string := s) fun (prev?, curr, next?) => charRole (prev?.map charType) (charType curr) (next?.map charType) @@ -85,7 +85,7 @@ private def selectBest (missScore? matchScore? : Option Int) : Option Int := | (some missScore, some matchScore) => some <| max missScore matchScore -/- Match the given pattern with the given word. The algorithm uses dynamic +/-- Match the given pattern with the given word. The algorithm uses dynamic programming to find the best scores. In addition to the current characters in the pattern and the word, the @@ -145,7 +145,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr let idx := patternIdx * (word.length + 1) * 2 + wordIdx * 2 result |>.set! idx missValue |>.set! (idx + 1) matchValue - /- Heuristic to penalize skipping characters in the word. -/ + /-- Heuristic to penalize skipping characters in the word. -/ skipPenalty (wordRole : CharRole) (patternComplete : Bool) (wordStart : Bool) : Int := Id.run do /- Skipping characters if the match is already completed is free. -/ if patternComplete then @@ -159,7 +159,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr return 0 - /- Whether characters from the pattern and the word match. -/ + /-- Whether characters from the pattern and the word match. -/ allowMatch (patternChar wordChar : Char) (patternRole wordRole : CharRole) : Bool := Id.run do /- Different characters do not match. -/ if patternChar.toLower != wordChar.toLower then @@ -170,7 +170,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr return true - /- Heuristic to rate a match. -/ + /-- Heuristic to rate a match. -/ matchResult (patternChar wordChar : Char) (patternRole wordRole : CharRole) (consecutive : Bool) (wordStart : Bool) : Int := Id.run do let mut score := 1 /- Case-sensitive equality or beginning of a segment in pattern and word. -/ @@ -185,7 +185,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr return score -/- Match the given pattern with the given word using a fuzzy matching +/-- Match the given pattern with the given word using a fuzzy matching algorithm. The resulting scores are in the interval `[0, 1]` or `none` if no match was found. -/ def fuzzyMatchScore? (pattern word : String) : Option Float := Id.run do @@ -214,7 +214,7 @@ def fuzzyMatchScore? (pattern word : String) : Option Float := Id.run do def fuzzyMatchScoreWithThreshold? (pattern word : String) (threshold := 0.2) : Option Float := fuzzyMatchScore? pattern word |>.filter (· > threshold) -/- Match the given pattern with the given word using a fuzzy matching +/-- Match the given pattern with the given word using a fuzzy matching algorithm. Return `false` if no match was found or the found match received a score below the given threshold. -/ def fuzzyMatch (pattern word : String) (threshold := 0.2) : Bool := diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index accf79ebfa..34dc91118b 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -88,7 +88,7 @@ instance : FromJson Name where instance : ToJson Name where toJson n := toString n -/- Note that `USize`s and `UInt64`s are stored as strings because JavaScript +/-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript cannot represent 64-bit numbers. -/ def bignumFromJson? (j : Json) : Except String Nat := do let s ← j.getStr? diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index a72d739c82..dc42ce3611 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -78,7 +78,7 @@ instance : ToJson ErrorCode := ⟨fun | ErrorCode.workerExited => (-32901 : Int) | ErrorCode.workerCrashed => (-32902 : Int)⟩ -/- Uses separate constructors for notifications and errors because client and server +/-- Uses separate constructors for notifications and errors because client and server behavior is expected to be wildly different for both. -/ inductive Message where | request (id : RequestID) (method : String) (params? : Option Structured) diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean index 6a674566d5..4908974b8e 100644 --- a/src/Lean/Data/KVMap.lean +++ b/src/Lean/Data/KVMap.lean @@ -53,7 +53,7 @@ instance : Coe Int DataValue := ⟨DataValue.ofInt⟩ instance : Coe Syntax DataValue := ⟨DataValue.ofSyntax⟩ -/- Remark: we do not use RBMap here because we need to manipulate KVMap objects in +/-- 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 diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index e2db6ff3d0..1e85a2c082 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -61,7 +61,7 @@ structure LocationLink where -- NOTE: Diagnostic defined in Diagnostics.lean -/- NOTE: No specific commands are specified by LSP, hence +/-- NOTE: No specific commands are specified by LSP, hence possible commands need to be announced as capabilities. -/ structure Command where title : String diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean index eff005e2a3..732f9854a1 100644 --- a/src/Lean/Data/Lsp/InitShutdown.lean +++ b/src/Lean/Data/Lsp/InitShutdown.lean @@ -58,7 +58,7 @@ structure InitializeParams where rootUri? : Option String := none initializationOptions? : Option InitializationOptions := none capabilities : ClientCapabilities - /- If omitted, we default to off. -/ + /-- If omitted, we default to off. -/ trace : Trace := Trace.off workspaceFolders? : Option (Array WorkspaceFolder) := none deriving ToJson diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index a69a2cc686..d82a9dae57 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -15,7 +15,7 @@ workers. These messages are not visible externally to users of the LSP server. namespace Lean.Lsp open Std -/- Most reference-related types have custom FromJson/ToJson implementations to +/-! Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON. -/ inductive RefIdent where diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean index 99d61ead33..96b796d8b7 100644 --- a/src/Lean/Data/Lsp/TextSync.lean +++ b/src/Lean/Data/Lsp/TextSync.lean @@ -78,7 +78,7 @@ structure DidCloseTextDocumentParams where -- TODO: TextDocumentSyncClientCapabilities -/- NOTE: This is defined twice in the spec. The latter version has more fields. -/ +/-- NOTE: This is defined twice in the spec. The latter version has more fields. -/ structure TextDocumentSyncOptions where openClose : Bool change : TextDocumentSyncKind diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean index dcc554cd1b..a60c037cce 100644 --- a/src/Lean/Data/Name.lean +++ b/src/Lean/Data/Name.lean @@ -100,14 +100,14 @@ def quickCmp (n₁ n₂ : Name) : Ordering := def quickLt (n₁ n₂ : Name) : Bool := quickCmp n₁ n₂ == Ordering.lt -/- Alternative HasLt instance. -/ +/-- Alternative HasLt instance. -/ @[inline] protected def hasLtQuick : LT Name := ⟨fun a b => Name.quickLt a b = true⟩ @[inline] instance : DecidableRel (@LT.lt Name Name.hasLtQuick) := inferInstanceAs (DecidableRel (fun a b => Name.quickLt a b = true)) -/- The frontend does not allow user declarations to start with `_` in any of its parts. +/-- The frontend does not allow user declarations to start with `_` in any of its parts. We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/ def isInternal : Name → Bool | str p s => s.get 0 == '_' || isInternal p diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 3a65a921e8..e2ba13b3fd 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -107,7 +107,7 @@ export MonadWithOptions (withOptions) instance [MonadFunctor m n] [MonadWithOptions m] : MonadWithOptions n where withOptions f x := monadMap (m := m) (withOptions f) x -/- Remark: `_inPattern` is an internal option for communicating to the delaborator that +/-! Remark: `_inPattern` is an internal option for communicating to the delaborator that the term being delaborated should be treated as a pattern. -/ def withInPattern [MonadWithOptions m] (x : m α) : m α := diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index 966fc8acf4..38d9e1a4d3 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -11,7 +11,7 @@ namespace Lean open Std (HashMap PHashMap) -/- Staged map for implementing the Environment. The idea is to store +/-- Staged map for implementing the Environment. The idea is to store imported entries into a hashtable and local entries into a persistent hashtable. Hypotheses: @@ -65,7 +65,7 @@ def empty : SMap α β := {} | ⟨true, m₁, _⟩, k => m₁.contains k | ⟨false, m₁, m₂⟩, k => m₁.contains k || m₂.contains k -/- Similar to `find?`, but searches for result in the hashmap first. +/-- Similar to `find?`, but searches for result in the hashmap first. So, the result is correct only if we never "overwrite" `map₁` entries using `map₂`. -/ @[specialize] def find?' : SMap α β → α → Option β | ⟨true, m₁, _⟩, k => m₁.find? k @@ -75,7 +75,7 @@ def forM [Monad m] (s : SMap α β) (f : α → β → m PUnit) : m PUnit := do s.map₁.forM f s.map₂.forM f -/- Move from stage 1 into stage 2. -/ +/-- Move from stage 1 into stage 2. -/ def switch (m : SMap α β) : SMap α β := if m.stage₁ then { m with stage₁ := false } else m diff --git a/src/Lean/Data/SSet.lean b/src/Lean/Data/SSet.lean index de5ff9540f..578340f864 100644 --- a/src/Lean/Data/SSet.lean +++ b/src/Lean/Data/SSet.lean @@ -7,8 +7,7 @@ import Lean.Data.SMap namespace Lean -/- Staged set. It is just a simple wrapper on top of Staged maps. -/ - +/-- Staged set. It is just a simple wrapper on top of Staged maps. -/ def SSet (α : Type u) [BEq α] [Hashable α] := SMap α Unit namespace SSet @@ -27,7 +26,7 @@ abbrev contains (s : SSet α) (a : α) : Bool := abbrev forM [Monad m] (s : SSet α) (f : α → m PUnit) : m PUnit := SMap.forM s fun a _ => f a -/- Move from stage 1 into stage 2. -/ +/-- Move from stage 1 into stage 2. -/ abbrev switch (s : SSet α) : SSet α := SMap.switch s diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean index b54eac4f34..06411490d8 100644 --- a/src/Lean/Declaration.lean +++ b/src/Lean/Declaration.lean @@ -121,7 +121,7 @@ structure TheoremVal extends ConstantVal where all : List Name := [name] deriving Inhabited -/- Value for an opaque constant declaration `opaque x : t := e` -/ +/-- Value for an opaque constant declaration `opaque x : t := e` -/ structure OpaqueVal extends ConstantVal where value : Expr isUnsafe : Bool diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 6b092d1a05..38ca824bcb 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -53,7 +53,7 @@ private def mkProjAndCheck (structName : Name) (idx : Nat) (e : Expr) : MetaM Ex throwError "invalid projection, the expression{indentExpr e}\nis a proposition and has type{indentExpr eType}\nbut the projected value is not, it has type{indentExpr rType}" return r -/- +/-- Relevant definitions: ``` class CoeFun (α : Sort u) (γ : α → outParam (Sort v)) @@ -125,7 +125,7 @@ structure Context where -/ resultIsOutParamSupport : Bool -/- Auxiliary structure for elaborating the application `f args namedArgs`. -/ +/-- Auxiliary structure for elaborating the application `f args namedArgs`. -/ structure State where f : Expr fType : Expr @@ -465,7 +465,7 @@ where | .bvar idx => idx == i | _ => false - /- (quick filter) Return true if `type` constains a binder `[C ...]` where `C` is a class containing outparams. -/ + /-- (quick filter) Return true if `type` constains a binder `[C ...]` where `C` is a class containing outparams. -/ hasLocalInstaceWithOutParams (type : Expr) : CoreM Bool := do let .forallE _ d b bi := type | return false if bi.isInstImplicit then @@ -497,7 +497,7 @@ where return false mutual - /- + /-- Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`, and then execute the main loop.-/ private partial def addEtaArg (argName : Name) : M Expr := do @@ -524,7 +524,7 @@ mutual addNewArg argName arg main - /- + /-- Process a `fType` of the form `(x : A) → B x`. This method assume `fType` is a function type -/ private partial def processExplictArg (argName : Name) : M Expr := do @@ -568,7 +568,7 @@ mutual else finalize - /- + /-- Process a `fType` of the form `{x : A} → B x`. This method assume `fType` is a function type -/ private partial def processImplicitArg (argName : Name) : M Expr := do @@ -577,7 +577,7 @@ mutual else addImplicitArg argName - /- + /-- Process a `fType` of the form `{{x : A}} → B x`. This method assume `fType` is a function type -/ private partial def processStrictImplicitArg (argName : Name) : M Expr := do @@ -588,7 +588,7 @@ mutual else finalize - /- + /-- Process a `fType` of the form `[x : A] → B x`. This method assume `fType` is a function type -/ private partial def processInstImplicitArg (argName : Name) : M Expr := do @@ -608,7 +608,7 @@ mutual addNewArg argName arg main - /- Elaborate function application arguments. -/ + /-- Elaborate function application arguments. -/ partial def main : M Expr := do let fType ← normalizeFunType if fType.isForall then @@ -768,7 +768,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L throwInvalidFieldNotation e eType | _, _ => throwInvalidFieldNotation e eType -/- whnfCore + implicit consumption. +/-- whnfCore + implicit consumption. Example: given `e` with `eType := {α : Type} → (fun β => List β) α `, it produces `(e ?m, List ?m)` where `?m` is fresh metavariable. -/ private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × Expr) := do let eType ← whnfCore eType @@ -832,7 +832,7 @@ private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := else return (← whnfR type).isAppOf baseName -/- Auxiliary method for field notation. It tries to add `e` as a new argument to `args` or `namedArgs`. +/-- Auxiliary method for field notation. It tries to add `e` as a new argument to `args` or `namedArgs`. This method first finds the parameter with a type of the form `(baseName ...)`. When the parameter is found, if it an explicit one and `args` is big enough, we add `e` to `args`. Otherwise, if there isn't another parameter with the same name, we add `e` to `namedArgs`. @@ -932,8 +932,8 @@ private def elabAppLVals (f : Expr) (lvals : List LVal) (namedArgs : Array Named def elabExplicitUnivs (lvls : Array Syntax) : TermElabM (List Level) := do lvls.foldrM (init := []) fun stx lvls => return (← elabLevel stx)::lvls -/- -Interaction between `errToSorry` and `observing`. +/-! +# Interaction between `errToSorry` and `observing`. - The method `elabTerm` catches exceptions, log them, and returns a synthetic sorry (IF `ctx.errToSorry` == true). diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean index 5d2666e85c..1045f027aa 100644 --- a/src/Lean/Elab/Attributes.lean +++ b/src/Lean/Elab/Attributes.lean @@ -23,7 +23,7 @@ instance : ToFormat Attribute where | AttributeKind.scoped => "scoped " Format.bracket "@[" f!"{kindStr}{attr.name}{toString attr.stx}" "]" -/- +/-- ``` attrKind := leading_parser optional («scoped» <|> «local») ``` diff --git a/src/Lean/Elab/AutoBound.lean b/src/Lean/Elab/AutoBound.lean index 132680d439..7887d73f25 100644 --- a/src/Lean/Elab/AutoBound.lean +++ b/src/Lean/Elab/AutoBound.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Data.Options -/- Basic support for auto bound implicit local names -/ +/-! # Basic support for auto bound implicit local names -/ namespace Lean.Elab @@ -23,7 +23,7 @@ register_builtin_option relaxedAutoImplicit : Bool := { private def isValidAutoBoundSuffix (s : String) : Bool := s.toSubstring.drop 1 |>.all fun c => c.isDigit || isSubScriptAlnum c || c == '_' || c == '\'' -/- +/-! Remark: Issue #255 exposed a nasty interaction between macro scopes and auto-bound-implicit names. ``` local notation "A" => id x diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 1f868114e5..d696daf643 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -75,7 +75,7 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name := compileDecl decl return name -/- +/-- Expand `optional (binderTactic <|> binderDefault)` def binderTactic := leading_parser " := " >> " by " >> tacticParser def binderDefault := leading_parser " := " >> termParser @@ -419,7 +419,7 @@ def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax else expandWhereDecls whereDeclsOpt[0] body -/- Helper function for `expandMatchAltsIntoMatch` -/ +/-- Helper function for `expandMatchAltsIntoMatch` -/ private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (matchTactic : Bool) : Nat → Array Syntax → MacroM Syntax | 0, discrs => do if matchTactic then @@ -583,7 +583,7 @@ open Lean.Elab.Term.Quotation in mkLambdaFVars xs e | _ => throwUnsupportedSyntax -/- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created. +/-- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created. Otherwise, we create a term of the form `(fun (x : type) => body) val` The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`. diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean index 2c08ecac7a..b6dc925fde 100644 --- a/src/Lean/Elab/BindersUtil.lean +++ b/src/Lean/Elab/BindersUtil.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura import Lean.Parser.Term namespace Lean.Elab.Term -/- +/-- Recall that ``` def typeSpec := leading_parser " : " >> termParser @@ -21,7 +21,7 @@ def expandOptType (ref : Syntax) (optType : Syntax) : Syntax := open Lean.Parser.Term -/- Helper function for `expandEqnsIntoMatch` -/ +/-- Helper function for `expandEqnsIntoMatch` -/ def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat := let alt0 := matchAlts[0][0] let pats := alt0[1][0].getSepArgs diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index bff865e8ee..cae20f5348 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -242,7 +242,7 @@ where | _ => Term.expandCDot? stx -/- +/-- Try to expand `·` notation. Recall that in Lean the `·` notation must be surrounded by parentheses. We may change this is the future, but right now, here are valid examples diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 037deca1c6..8aaa295092 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -26,7 +26,7 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level := @[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ => return mkSort (mkLevelSucc (← elabOptLevel stx[1])) -/- +/-! the method `resolveName` adds a completion point for it using the given expected type. Thus, we propagate the expected type if `stx[0]` is an identifier. It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case. @@ -205,7 +205,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do | some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkRawNatLit val.toNat) | none => throwIllFormedSyntax -/- A literal of type `Name`. -/ +/-- A literal of type `Name`. -/ @[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ => match stx[0].isNameLit? with | some val => pure $ toExpr val diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index a92f47af92..2254b7f50e 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -239,7 +239,7 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttrib (withInfoTreeContext (mkInfoTree := mkInfoTree elabFn.declName stx) <| elabFn.value stx) (fun _ => do set s; elabCommandUsing s stx elabFns) -/- Elaborate `x` with `stx` on the macro stack -/ +/-- Elaborate `x` with `stx` on the macro stack -/ def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α := withInfoContext (mkInfo := pure <| .ofMacroExpansionInfo { stx := beforeStx, output := afterStx, lctx := .empty }) do withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x diff --git a/src/Lean/Elab/Config.lean b/src/Lean/Elab/Config.lean index 2f497c7b64..f7ad2d85ca 100644 --- a/src/Lean/Elab/Config.lean +++ b/src/Lean/Elab/Config.lean @@ -7,7 +7,7 @@ import Lean.Meta.Basic namespace Lean.Elab.Term -/- +/-- Set `isDefEq` configuration for the elaborator. Note that we enable all approximations but `quasiPatternApprox` diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 2ba71001e7..ae9899a942 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -183,7 +183,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) | _ => throwError "protected declarations must be in a namespace" | _ => pure (declName, shortName) -/- +/-- `declId` is of the form ``` leading_parser ident >> optional (".{" >> sepBy1 ident ", " >> "}") diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean index afe1a87950..4952d0a005 100644 --- a/src/Lean/Elab/Declaration.lean +++ b/src/Lean/Elab/Declaration.lean @@ -201,7 +201,7 @@ def elabDeclaration : CommandElab := fun stx => do else throwError "unexpected declaration" -/- Return true if all elements of the mutual-block are inductive declarations. -/ +/-- Return true if all elements of the mutual-block are inductive declarations. -/ private def isMutualInductive (stx : Syntax) : Bool := stx[1].getArgs.all fun elem => let decl := elem[1] @@ -214,7 +214,7 @@ private def elabMutualInductive (elems : Array Syntax) : CommandElabM Unit := do inductiveSyntaxToView modifiers stx[1] elabInductiveViews views -/- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/ +/-- Return true if all elements of the mutual-block are definitions/theorems/abbrevs. -/ private def isMutualDef (stx : Syntax) : Bool := stx[1].getArgs.all fun elem => let decl := elem[1] diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index b4677459df..e85736038f 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -56,7 +56,7 @@ where | _ => pure () runST (fun _ => visit |>.run usedInstIdxs) |>.2 - /- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters + /-- Create an `instance` command using the constructor `ctorName` with a hypothesis `Inhabited α` when `α` is one of the inductive type parameters at position `i` and `i ∈ assumingParamIdxs`. -/ mkInstanceCmdWith (assumingParamIdxs : IndexSet) : TermElabM Syntax := do let indVal ← getConstInfoInduct inductiveTypeName diff --git a/src/Lean/Elab/Deriving/SizeOf.lean b/src/Lean/Elab/Deriving/SizeOf.lean index c681a3da81..f57f360f1a 100644 --- a/src/Lean/Elab/Deriving/SizeOf.lean +++ b/src/Lean/Elab/Deriving/SizeOf.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura import Lean.Meta.SizeOf import Lean.Elab.Deriving.Basic -/- +/-! Remark: `SizeOf` instances are automatically generated. We add support for `deriving instance` for `SizeOf` just to be able to use them to define instances for types defined at `Prelude.lean` -/ diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index bbb25ade1d..7ae5e7cddd 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -128,7 +128,7 @@ namespace Do abbrev Var := Syntax -- TODO: should be `Ident` -/- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/ +/-- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/ structure Alt (σ : Type) where ref : Syntax vars : Array Var @@ -136,7 +136,7 @@ structure Alt (σ : Type) where rhs : σ deriving Inhabited -/- +/-- Auxiliary datastructure for representing a `do` code block, and compiling "reassignments" (e.g., `x := x + 1`). We convert `Code` into a `Syntax` term representing the: - `do`-block, or @@ -187,22 +187,22 @@ structure Alt (σ : Type) where inductive Code where | decl (xs : Array Var) (doElem : Syntax) (k : Code) | reassign (xs : Array Var) (doElem : Syntax) (k : Code) - /- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not -/ - | joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code) + | /-- The Boolean value in `params` indicates whether we should use `(x : typeof! x)` when generating term Syntax or not -/ + joinpoint (name : Name) (params : Array (Var × Bool)) (body : Code) (k : Code) | seq (action : Syntax) (k : Code) | action (action : Syntax) | «break» (ref : Syntax) | «continue» (ref : Syntax) | «return» (ref : Syntax) (val : Syntax) - /- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/ - | ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code) + | /-- Recall that an if-then-else may declare a variable using `optIdent` for the branches `thenBranch` and `elseBranch`. We store the variable name at `var?`. -/ + ite (ref : Syntax) (h? : Option Var) (optIdent : Syntax) (cond : Syntax) (thenBranch : Code) (elseBranch : Code) | «match» (ref : Syntax) (gen : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt Code)) | jmp (ref : Syntax) (jpName : Name) (args : Array Syntax) deriving Inhabited abbrev VarSet := Std.RBMap Name Syntax Name.cmp -/- A code block, and the collection of variables updated by it. -/ +/-- A code block, and the collection of variables updated by it. -/ structure CodeBlock where code : Code uvars : VarSet := {} -- set of variables updated by `code` @@ -231,7 +231,7 @@ partial def CodeBlocl.toMessageData (codeBlock : CodeBlock) : MessageData := ++ alts.foldl (init := m!"") fun acc alt => acc ++ m!"\n| {alt.patterns} => {loop alt.rhs}" loop codeBlock.code -/- Return true if the give code contains an exit point that satisfies `p` -/ +/-- Return true if the give code contains an exit point that satisfies `p` -/ partial def hasExitPointPred (c : Code) (p : Code → Bool) : Bool := let rec loop : Code → Bool | Code.decl _ _ k => loop k @@ -278,7 +278,7 @@ def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax let k ← mkCont y return Code.decl #[y] doElem k -/- Convert `action _ e` instructions in `c` into `let y ← e; jmp _ jp (xs y)`. -/ +/-- Convert `action _ e` instructions in `c` into `let y ← e; jmp _ jp (xs y)`. -/ partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array Var) : MacroM Code := let rec loop : Code → MacroM Code | Code.decl xs stx k => return Code.decl xs stx (← loop k) @@ -334,7 +334,7 @@ def eraseOptVar (rs : VarSet) (x? : Option Var) : VarSet := | none => rs | some x => rs.insert x.getId x -/- Create a new jointpoint for `c`, and jump to it with the variables `rs` -/ +/-- Create a new jointpoint for `c`, and jump to it with the variables `rs` -/ def mkSimpleJmp (ref : Syntax) (rs : VarSet) (c : Code) : StateRefT (Array JPDecl) TermElabM Code := do let xs := varSetToArray rs let jp ← addFreshJP (xs.map fun x => (x, true)) c @@ -344,7 +344,7 @@ def mkSimpleJmp (ref : Syntax) (rs : VarSet) (c : Code) : StateRefT (Array JPDec else return Code.jmp ref jp xs -/- Create a new joinpoint that takes `rs` and `val` as arguments. `val` must be syntax representing a pure value. +/-- Create a new joinpoint that takes `rs` and `val` as arguments. `val` must be syntax representing a pure value. The body of the joinpoint is created using `mkJPBody yFresh`, where `yFresh` is a fresh variable created by this method. -/ def mkJmp (ref : Syntax) (rs : VarSet) (val : Syntax) (mkJPBody : Syntax → MacroM Code) : StateRefT (Array JPDecl) TermElabM Code := do @@ -357,7 +357,7 @@ def mkJmp (ref : Syntax) (rs : VarSet) (val : Syntax) (mkJPBody : Syntax → Mac let jp ← addFreshJP ps jpBody return Code.jmp ref jp args -/- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path. -/ +/-- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path. -/ partial def pullExitPointsAux : VarSet → Code → StateRefT (Array JPDecl) TermElabM Code | rs, Code.decl xs stx k => return Code.decl xs stx (← pullExitPointsAux (eraseVars rs xs) k) | rs, Code.reassign xs stx k => return Code.reassign xs stx (← pullExitPointsAux (insertVars rs xs) k) @@ -375,7 +375,7 @@ partial def pullExitPointsAux : VarSet → Code → StateRefT (Array JPDecl) Ter let ref := e mkJmp ref rs y (fun yFresh => return Code.action (← ``(Pure.pure $yFresh))) -/- +/-- Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock. When a new variable is not already in the collection, but is shadowed by some declaration in `c`, we create auxiliary join points to make sure we preserve the semantics of the code block. @@ -458,7 +458,7 @@ partial def extendUpdatedVarsAux (c : Code) (ws : VarSet) : TermElabM Code := | c => return c update c -/- +/-- Extend the set of updated variables. It assumes `ws` is a super set of `c.uvars`. We **cannot** simply update the field `c.uvars`, because `c` may have shadowed some variable in `ws`. See discussion at `pullExitPoints`. @@ -473,7 +473,7 @@ partial def extendUpdatedVars (c : CodeBlock) (ws : VarSet) : TermElabM CodeBloc private def union (s₁ s₂ : VarSet) : VarSet := s₁.fold (·.insert ·) s₂ -/- +/-- Given two code blocks `c₁` and `c₂`, make sure they have the same set of updated variables. Let `ws` the union of the updated variables in `c₁‵ and ‵c₂`. We use `extendUpdatedVars c₁ ws` and `extendUpdatedVars c₂ ws` @@ -484,7 +484,7 @@ def homogenize (c₁ c₂ : CodeBlock) : TermElabM (CodeBlock × CodeBlock) := d let c₂ ← extendUpdatedVars c₂ ws pure (c₁, c₂) -/- +/-- Extending code blocks with variable declarations: `let x : t := v` and `let x : t ← v`. We remove `x` from the collection of updated varibles. Remark: `stx` is the syntax for the declaration (e.g., `letDecl`), and `xs` are the variables @@ -496,7 +496,7 @@ def mkVarDeclCore (xs : Array Var) (stx : Syntax) (c : CodeBlock) : CodeBlock := uvars := eraseVars c.uvars xs } -/- +/-- Extending code blocks with reassignments: `x : t := v` and `x : t ← v`. Remark: `stx` is the syntax for the declaration (e.g., `letDecl`), and `xs` are the variables declared by it. It is an array because we have let-declarations that declare multiple variables. @@ -554,7 +554,7 @@ def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Sy return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code } return { code := Code.«match» ref genParam discrs optMotive alts, uvars := ws } -/- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`. +/-- Return a code block that executes `terminal` and then `k` with the value produced by `terminal`. This method assumes `terminal` is a terminal -/ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlock) : TermElabM CodeBlock := do unless hasTerminalAction terminal.code do @@ -669,7 +669,7 @@ def mkDoSeq (doElems : Array Syntax) : Syntax := def mkSingletonDoSeq (doElem : Syntax) : Syntax := mkDoSeq #[doElem] -/- +/-- If the given syntax is a `doIf`, return an equivalente `doIf` that has an `else` but no `else if`s or `if let`s. -/ private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx with | `(doElem|if $_:doIfProp then $_ else $_) => pure none @@ -694,7 +694,7 @@ structure DoIfView where thenBranch : Syntax elseBranch : Syntax -/- This method assumes `expandDoIf?` is not applicable. -/ +/-- This method assumes `expandDoIf?` is not applicable. -/ private def mkDoIfView (doIf : Syntax) : MacroM DoIfView := do pure { ref := doIf, @@ -704,7 +704,7 @@ private def mkDoIfView (doIf : Syntax) : MacroM DoIfView := do elseBranch := doIf[5][1] } -/- +/-- We use `MProd` instead of `Prod` to group values when expanding the `do` notation. `MProd` is a universe monomorphic product. The motivation is to generate simpler universe constraints in code @@ -722,7 +722,7 @@ private def mkTuple (elems : Array Syntax) : MacroM Syntax := do elems.extract 0 (elems.size - 1) |>.foldrM (init := elems.back) fun elem tuple => ``(MProd.mk $elem $tuple) -/- Return `some action` if `doElem` is a `doExpr `-/ +/-- Return `some action` if `doElem` is a `doExpr `-/ def isDoExpr? (doElem : Syntax) : Option Syntax := if doElem.getKind == ``Lean.Parser.Term.doExpr then some doElem[0] @@ -764,7 +764,7 @@ where `(let $a:ident := $x.1; let x := $x.2; $rest) | _ => unreachable! -/- +/-! The procedure `ToTerm.run` converts a `CodeBlock` into a `Syntax` term. We use this method to convert 1- The `CodeBlock` for a root `do ...` term into a `Syntax` term. This kind of @@ -1037,7 +1037,7 @@ partial def toTerm (c : Code) : M Syntax := do def run (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax := toTerm code { m, returnType, kind, uvars } -/- Given +/-- Given - `a` is true if the code block has a `Code.action _` exit point - `r` is true if the code block has a `Code.return _ _` exit point - `bc` is true if the code block has a `Code.break _` or `Code.continue _` exit point @@ -1057,7 +1057,7 @@ def mkNestedKind (a r bc : Bool) : Kind := def mkNestedTerm (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var) (a r bc : Bool) : MacroM Syntax := do ToTerm.run code m returnType uvars (mkNestedKind a r bc) -/- Given a term `term` produced by `ToTerm.run`, pattern match on its result. +/-- Given a term `term` produced by `ToTerm.run`, pattern match on its result. See comment at the beginning of the `ToTerm` namespace. - `a` is true if the code block has a `Code.action _` exit point @@ -1208,7 +1208,7 @@ def checkLetArrowRHS (doElem : Syntax) : M Unit := do kind == ``Lean.Parser.Term.doReassignArrow then throwErrorAt doElem "invalid kind of value '{kind}' in an assignment" -/- Generate `CodeBlock` for `doReturn` which is of the form +/-- Generate `CodeBlock` for `doReturn` which is of the form ``` "return " >> optional termParser ``` @@ -1240,7 +1240,7 @@ def tryCatchPred (tryCode : CodeBlock) (catches : Array Catch) (finallyCode? : O | some finallyCode => p finallyCode.code mutual - /- "Concatenate" `c` with `doSeqToCode doElems` -/ + /-- "Concatenate" `c` with `doSeqToCode doElems` -/ partial def concatWith (c : CodeBlock) (doElems : List Syntax) : M CodeBlock := match doElems with | [] => pure c @@ -1249,7 +1249,7 @@ mutual let ref := nextDoElem concat c ref none k - /- Generate `CodeBlock` for `doLetArrow; doElems` + /-- Generate `CodeBlock` for `doLetArrow; doElems` `doLetArrow` is of the form ``` "let " >> optional "mut " >> (doIdDecl <|> doPatDecl) @@ -1304,7 +1304,7 @@ mutual let auxDo ← `(do let discr := $val; match discr with | $pattern:term => $contSeq | _ => $elseSeq) doSeqToCode <| getDoSeqElems (getDoSeq auxDo) - /- Generate `CodeBlock` for `doReassignArrow; doElems` + /-- Generate `CodeBlock` for `doReassignArrow; doElems` `doReassignArrow` is of the form ``` (doIdDecl <|> doPatDecl) @@ -1329,7 +1329,7 @@ mutual else throwError "unexpected kind of 'do' reassignment" - /- Generate `CodeBlock` for `doIf; doElems` + /-- Generate `CodeBlock` for `doIf; doElems` `doIf` is of the form ``` "if " >> optIdent >> termParser >> " then " >> doSeq @@ -1343,7 +1343,7 @@ mutual let ite ← mkIte view.ref view.optIdent view.cond thenBranch elseBranch concatWith ite doElems - /- Generate `CodeBlock` for `doUnless; doElems` + /-- Generate `CodeBlock` for `doUnless; doElems` `doUnless` is of the form ``` "unless " >> termParser >> "do " >> doSeq @@ -1355,7 +1355,7 @@ mutual let unlessCode ← liftMacroM <| mkUnless cond body concatWith unlessCode doElems - /- Generate `CodeBlock` for `doFor; doElems` + /-- Generate `CodeBlock` for `doFor; doElems` `doFor` is of the form ``` def doForDecl := leading_parser termParser >> " in " >> withForbidden "do" termParser diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 3f78ad6ecc..644f1e52bd 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -5,9 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Elab.App -/- -Auxiliary elaboration functions: AKA custom elaborators --/ +/-! # Auxiliary elaboration functions: AKA custom elaborators -/ namespace Lean.Elab.Term open Meta @@ -78,7 +76,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr := | _ => throwUnsupportedSyntax namespace BinOp -/- +/-! The elaborator for `binop%` terms works as follows: diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 65bed617de..7221dd3377 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -173,7 +173,7 @@ private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHead checkHeaders rs numParams 0 none return rs -/- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and +/-- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and `indFVars` are the new local declarations. We use the local context/instances and parameters of rs[0]. Note that this method is executed after we executed `checkHeaders` and established all @@ -295,7 +295,7 @@ private def withExplicitToImplicit (xs : Array Expr) (k : TermElabM α) : TermEl toImplicit := toImplicit.push (x.fvarId!, BinderInfo.implicit) withNewBinderInfos toImplicit k -/- +/-- Elaborate constructor types. Remark: we check whether the resulting type is correct, and the parameter occurrences are consistent, but @@ -615,7 +615,7 @@ private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr m := m.insert indFVar (mkConst view.declName levelParams) return m -/- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration, +/-- Remark: `numVars <= numParams`. `numVars` is the number of context `variables` used in the inductive declaration, and `numParams` is `numVars` + number of explicit parameters provided in the declaration. -/ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) (numVars : Nat) (numParams : Nat) (indTypes : List InductiveType) : TermElabM (List InductiveType) := diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean index 4f605981a2..16e84d9dbc 100644 --- a/src/Lean/Elab/MacroArgUtil.lean +++ b/src/Lean/Elab/MacroArgUtil.lean @@ -10,7 +10,7 @@ open Lean.Syntax open Lean.Parser.Term hiding macroArg open Lean.Parser.Command -/- Convert `macro` arg into a `syntax` command item and a pattern element -/ +/-- Convert `macro` arg into a `syntax` command item and a pattern element -/ partial def expandMacroArg (stx : TSyntax ``macroArg) : CommandElabM (TSyntax `stx × Term) := do let (id?, id, stx) ← match (← liftMacroM <| expandMacros stx) with | `(macroArg| $id:ident:$stx) => pure (some id, (id : Term), stx) diff --git a/src/Lean/Elab/MacroRules.lean b/src/Lean/Elab/MacroRules.lean index f3e964809c..57c0f5e524 100644 --- a/src/Lean/Elab/MacroRules.lean +++ b/src/Lean/Elab/MacroRules.lean @@ -11,7 +11,7 @@ open Lean.Syntax open Lean.Parser.Term hiding macroArg open Lean.Parser.Command -/- +/-- Remark: `k` is the user provided kind with the current namespace included. Recall that syntax node kinds contain the current namespace. -/ diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 8c9cbd8b5d..dc239f1441 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -76,7 +76,7 @@ structure Discr where structure ElabMatchTypeAndDiscrsResult where discrs : Array Discr matchType : Expr - /- `true` when performing dependent elimination. We use this to decide whether we optimize the "match unit" case. + /-- `true` when performing dependent elimination. We use this to decide whether we optimize the "match unit" case. See `isMatchUnit?`. -/ isDep : Bool alts : Array MatchAltView @@ -92,7 +92,7 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptM let (discrs, isDep) ← elabDiscrsWitMatchType matchType return { discrs := discrs, matchType := matchType, isDep := isDep, alts := matchAltViews } where - /- Easy case: elaborate discriminant when the match-type has been explicitly provided by the user. -/ + /-- Easy case: elaborate discriminant when the match-type has been explicitly provided by the user. -/ elabDiscrsWitMatchType (matchType : Expr) : TermElabM (Array Discr × Bool) := do let mut discrs := #[] let mut i := 0 @@ -116,7 +116,7 @@ where markIsDep (r : ElabMatchTypeAndDiscrsResult) := { r with isDep := true } - /- Elaborate discriminants inferring the match-type -/ + /-- Elaborate discriminants inferring the match-type -/ elabDiscrs (i : Nat) (discrs : Array Discr) : TermElabM ElabMatchTypeAndDiscrsResult := do if h : i < discrStxs.size then let discrStx := discrStxs.get ⟨i, h⟩ @@ -153,7 +153,7 @@ private def getMatchGeneralizing? : Syntax → Option Bool | `(match (generalizing := false) $[$motive]? $_discrs,* with $_alts:matchAlt*) => some false | _ => none -/- Given `stx` a match-expression, return its alternatives. -/ +/-- Given `stx` a match-expression, return its alternatives. -/ private def getMatchAlts : Syntax → Array MatchAltView | `(match $[$gen]? $[$motive]? $_discrs,* with $alts:matchAlt*) => alts.filterMap fun alt => match alt with @@ -180,7 +180,7 @@ open Lean.Elab.Term.Quotation in Quotation.withNewLocals (getPatternVarNames vars) <| precheck rhs | _ => throwUnsupportedSyntax -/- We convert the collected `PatternVar`s intro `PatternVarDecl` -/ +/-- We convert the collected `PatternVar`s intro `PatternVarDecl` -/ structure PatternVarDecl where fvarId : FVarId @@ -195,7 +195,7 @@ private partial def withPatternVars {α} (pVars : Array PatternVar) (k : Array P k decls loop 0 #[] #[] -/- +/-! Remark: when performing dependent pattern matching, we often had to write code such as ```lean @@ -217,7 +217,7 @@ try to "sort" the new discriminants. If the refinement process fails, we report the original error message. -/ -/- Auxiliary structure for storing an type mismatch exception when processing the +/-- Auxiliary structure for storing an type mismatch exception when processing the pattern #`idx` of some alternative. -/ structure PatternElabException where ex : Exception @@ -646,7 +646,7 @@ where partial def savePatternInfo (p : Expr) : TermElabM Expr := go p |>.run false where - /- The `Bool` context is true iff we are inside of an "inaccessible" pattern. -/ + /-- The `Bool` context is true iff we are inside of an "inaccessible" pattern. -/ go (p : Expr) : ReaderT Bool TermElabM Expr := do match p with | .forallE n d b bi => withLocalDecl n bi (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x)) @@ -896,7 +896,7 @@ private def generalize (discrs : Array Discr) (matchType : Expr) (altViews : Arr private partial def elabMatchAltViews (generalizing? : Option Bool) (discrs : Array Discr) (matchType : Expr) (altViews : Array MatchAltView) : TermElabM (Array Discr × Expr × Array (AltLHS × Expr) × Bool) := do loop discrs #[] matchType altViews none where - /- + /-- "Discriminant refinement" main loop. `first?` contains the first error message we found before updated the `discrs`. -/ loop (discrs : Array Discr) (toClear : Array FVarId) (matchType : Expr) (altViews : Array MatchAltView) (first? : Option (SavedState × Exception)) @@ -953,7 +953,7 @@ where containsFVar (es : Array Expr) (fvarId : FVarId) : Bool := es.any fun e => e.isFVar && e.fvarId! == fvarId - /- Update `indices` by including any free variable `x` s.t. + /-- Update `indices` by including any free variable `x` s.t. - Type of some `discr` depends on `x`. - Type of `x` depends on some free variable in `indices`. @@ -1176,7 +1176,7 @@ private def tryPostponeIfDiscrTypeIsMVar (matchStx : Syntax) : TermElabM Unit := trace[Elab.match] "discr {d} : {dType}" tryPostponeIfMVar dType -/- +/-- We (try to) elaborate a `match` only when the expected type is available. If the `matchType` has not been provided by the user, we also try to postpone elaboration if the type of a discriminant is not available. That is, it is of the form `(?m ...)`. @@ -1213,7 +1213,7 @@ private def waitExpectedTypeAndDiscrs (matchStx : Syntax) (expectedType? : Optio | some expectedType => return expectedType | none => mkFreshTypeMVar -/- +/-- ``` leading_parser "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >> " with " >> ppDedent matchAlts ``` diff --git a/src/Lean/Elab/MatchAltView.lean b/src/Lean/Elab/MatchAltView.lean index 40c47578c9..30ae0b6766 100644 --- a/src/Lean/Elab/MatchAltView.lean +++ b/src/Lean/Elab/MatchAltView.lean @@ -7,7 +7,7 @@ import Lean.Elab.Term namespace Lean.Elab.Term -/- This modules assumes "match"-expressions use the following syntax. +/-! This module assumes `match`-expressions use the following syntax. ```lean def matchDiscr := leading_parser optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 7d0eccf1c1..b3671dd93e 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -16,7 +16,7 @@ import Lean.Elab.DeclarationRange namespace Lean.Elab open Lean.Parser.Term -/- DefView after elaborating the header. -/ +/-- `DefView` after elaborating the header. -/ structure DefViewElabHeader where ref : Syntax modifiers : Modifiers @@ -263,7 +263,7 @@ private def getFunName (fvarId : FVarId) (letRecsToLift : List LetRecToLift) : T | none => throwError "unknown function" | some n => pure n -/- +/-- Ensures that the of let-rec definition types do not contain functions being defined. In principle, this test can be improved. We could perform it after we separate the set of functions is strongly connected components. However, this extra complication doesn't seem worth it. @@ -278,10 +278,10 @@ private def checkLetRecsToLiftTypes (funVars : Array Expr) (letRecsToLift : List namespace MutualClosure -/- A mapping from FVarId to Set of FVarIds. -/ +/-- A mapping from FVarId to Set of FVarIds. -/ abbrev UsedFVarsMap := FVarIdMap FVarIdSet -/- +/-- Create the `UsedFVarsMap` mapping that takes the variable id for the mutually recursive functions being defined to the set of free variables in its definition. @@ -348,7 +348,7 @@ private def mkInitialUsedFVarsMap [Monad m] [MonadMCtx m] (sectionVars : Array E usedFVarMap := usedFVarMap.insert toLift.fvarId set return usedFVarMap -/- +/-! The let-recs may invoke each other. Example: ``` let rec @@ -456,7 +456,7 @@ private def preprocess (e : Expr) : TermElabM Expr := do Meta.check e pure e -/- Push free variables in `s` to `toProcess` if they are not already there. -/ +/-- Push free variables in `s` to `toProcess` if they are not already there. -/ private def pushNewVars (toProcess : Array FVarId) (s : CollectFVars.State) : Array FVarId := s.fvarSet.fold (init := toProcess) fun toProcess fvarId => if toProcess.contains fvarId then toProcess else toProcess.push fvarId @@ -551,7 +551,7 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa result := result.push (← mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!) return result.toList -/- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/ +/-- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/ abbrev Replacement := FVarIdMap Expr def insertReplacementForMainFns (r : Replacement) (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mainFVars : Array Expr) : Replacement := @@ -610,7 +610,7 @@ def getModifiersForLetRecs (mainHeaders : Array DefViewElabHeader) : Modifiers : isUnsafe := mainHeaders.any fun h => h.modifiers.isUnsafe } -/- +/-- - `sectionVars`: The section variables used in the `mutual` block. - `mainHeaders`: The elaborated header of the top-level definitions being defined by the mutual block. - `mainFVars`: The auxiliary variables used to represent the top-level definitions being defined by the mutual block. diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean index 68f9f03281..be2205c7c2 100644 --- a/src/Lean/Elab/Notation.lean +++ b/src/Lean/Elab/Notation.lean @@ -12,7 +12,7 @@ open Lean.Syntax open Lean.Parser.Term hiding macroArg open Lean.Parser.Command -/- Wrap all occurrences of the given `ident` nodes in antiquotations -/ +/-- Wrap all occurrences of the given `ident` nodes in antiquotations -/ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax | stx => match stx with | `($id:ident) => @@ -24,13 +24,13 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax | Syntax.node i k args => Syntax.node i k (args.map (antiquote vars)) | stx => stx -/- Convert `notation` command lhs item into a `syntax` command item -/ +/-- Convert `notation` command lhs item into a `syntax` command item -/ def expandNotationItemIntoSyntaxItem : TSyntax ``notationItem → MacroM (TSyntax `stx) | `(notationItem| $_:ident$[:$prec?]?) => `(stx| term $[:$prec?]?) | `(notationItem| $s:str) => `(stx| $s:str) | _ => Macro.throwUnsupported -/- Convert `notation` command lhs item into a pattern element -/ +/-- Convert `notation` command lhs item into a pattern element -/ def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax := let k := stx.getKind if k == `Lean.Parser.Command.identPrec then diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 78807b63a7..db85be5760 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -13,7 +13,7 @@ open Meta abbrev PatternVar := Syntax -- TODO: should be `Ident` -/- +/-! Patterns define new local variables. This module collect them and preprocess `_` occurring in patterns. Recall that an `_` may represent anonymous variables or inaccessible terms @@ -49,7 +49,7 @@ private def throwCtorExpected {α} : M α := private def throwInvalidPattern {α} : M α := throwError "invalid pattern" -/- +/-! An application in a pattern can be 1- A constructor application @@ -231,7 +231,7 @@ where processCtor (stx : Syntax) : M Syntax := do processCtorAppCore stx #[] #[] false - /- Check whether `stx` is a pattern variable or constructor-like (i.e., constructor or constant tagged with `[matchPattern]` attribute) -/ + /-- Check whether `stx` is a pattern variable or constructor-like (i.e., constructor or constant tagged with `[matchPattern]` attribute) -/ processId (stx : Syntax) : M Syntax := do match (← resolveId? stx "pattern") with | none => processVar stx @@ -324,7 +324,7 @@ def collectPatternVars (alt : MatchAltView) : TermElabM (Array PatternVar × Mat let (alt, s) ← (CollectPatternVars.main alt).run {} return (s.vars, alt) -/- Return the pattern variables in the given pattern. +/-- 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 diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index cdc955f3a3..bc75208e54 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -74,7 +74,7 @@ def abstractNestedProofs (preDef : PreDefinition) : MetaM PreDefinition := let value ← Meta.abstractNestedProofs preDef.declName preDef.value pure { preDef with value := value } -/- Auxiliary method for (temporarily) adding pre definition as an axiom -/ +/-- Auxiliary method for (temporarily) adding pre definition as an axiom -/ def addAsAxiom (preDef : PreDefinition) : MetaM Unit := do withRef preDef.ref do addDecl <| Declaration.axiomDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe } diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean index 5050baa096..1ed531927f 100644 --- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean +++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean @@ -31,7 +31,6 @@ private def mkFnInhabitant? (xs : Array Expr) (type : Expr) (useOfNonempty : Boo loop xs.size type /- TODO: add a global IO.Ref to let users customize/extend this procedure -/ - def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr := do let go? (useOfNonempty : Bool) : MetaM (Option Expr) := do match (← mkInhabitant? type useOfNonempty) with diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 92659fa214..2fc755fd4f 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -16,7 +16,7 @@ open Meta private def throwToBelowFailed : MetaM α := throwError "toBelow failed" -/- See toBelow -/ +/-- See `toBelow` -/ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : Expr) : MetaM Expr := do let belowDict ← whnf belowDict trace[Elab.definition.structural] "belowDict: {belowDict}, arg: {arg}" @@ -43,7 +43,7 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E pure (mkAppN F argTailArgs) | _ => throwToBelowFailed -/- See toBelow -/ +/-- See `toBelow` -/ private def withBelowDict (below : Expr) (numIndParams : Nat) (k : Expr → Expr → MetaM α) : MetaM α := do let belowType ← inferType below trace[Elab.definition.structural] "belowType: {belowType}" @@ -59,7 +59,7 @@ private def withBelowDict (below : Expr) (numIndParams : Nat) (k : Expr → Expr let belowDict := mkAppN belowDict (args.extract (numIndParams + 1) args.size) k C belowDict -/- +/-- `below` is a free variable with type of the form `I.below indParams motive indices major`, where `I` is the name of an inductive datatype. @@ -148,7 +148,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then processApp e else - /- Here is an example we currently not handle + /- Here is an example we currently do not handle ``` def g (xs : List Nat) : Nat := match xs with diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean index ff7f265b0e..c3f392129e 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Basic.lean @@ -9,23 +9,32 @@ import Lean.Meta.ForEachExpr namespace Lean.Elab.Structural structure RecArgInfo where - /- `fixedParams ++ ys` are the arguments of the function we are trying to justify termination using structural recursion. -/ + /-- `fixedParams ++ ys` are the arguments of the function we are trying to justify termination using structural recursion. -/ fixedParams : Array Expr - ys : Array Expr -- recursion arguments - pos : Nat -- position in `ys` of the argument we are recursing on - indicesPos : Array Nat -- position in `ys` of the inductive datatype indices we are recursing on - indName : Name -- inductive datatype name of the argument we are recursing on - indLevels : List Level -- inductice datatype universe levels of the argument we are recursing on - indParams : Array Expr -- inductive datatype parameters of the argument we are recursing on - indIndices : Array Expr -- inductive datatype indices of the argument we are recursing on, it is equal to `indicesPos.map fun i => ys.get! i` - reflexive : Bool -- true if we are recursing over a reflexive inductive datatype - indPred : Bool -- true if the type is an inductive predicate + /-- recursion arguments -/ + ys : Array Expr + /-- position in `ys` of the argument we are recursing on -/ + pos : Nat + /-- position in `ys` of the inductive datatype indices we are recursing on -/ + indicesPos : Array Nat + /-- inductive datatype name of the argument we are recursing on -/ + indName : Name + /-- inductive datatype universe levels of the argument we are recursing on -/ + indLevels : List Level + /-- inductive datatype parameters of the argument we are recursing on -/ + indParams : Array Expr + /-- inductive datatype indices of the argument we are recursing on, it is equal to `indicesPos.map fun i => ys.get! i` -/ + indIndices : Array Expr + /-- true if we are recursing over a reflexive inductive datatype -/ + reflexive : Bool + /-- true if the type is an inductive predicate -/ + indPred : Bool def RecArgInfo.recArgPos (info : RecArgInfo) : Nat := info.fixedParams.size + info.pos structure State where - /- As part of the inductive predicates case, we keep adding more and more discriminants from the + /-- As part of the inductive predicates case, we keep adding more and more discriminants from the local context and build up a bigger matcher application until we reach a fixed point. As a side-effect, this creates matchers. Here we capture all these side-effects, because the construction rolls back any changes done to the environment and the side-effects diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean index 9b17b636e6..ec13ac67c5 100644 --- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean @@ -7,7 +7,7 @@ import Lean.Parser.Command namespace Lean.Elab.WF -/- Support for `decreasing_by` and `termination_by'` notations -/ +/-! # Support for `decreasing_by` and `termination_by'` notations -/ structure TerminationHintValue where ref : Syntax @@ -73,7 +73,7 @@ def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do | TerminationHint.many m => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element" | _ => pure () -/- Support for `termination_by` notation -/ +/-! # Support for `termination_by` notation -/ structure TerminationByElement where ref : Syntax diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 971555aa0a..0cf443a916 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -234,9 +234,9 @@ elab_stx_quot Parser.Term.doElem.quot elab_stx_quot Parser.Term.dynamicQuot elab_stx_quot Parser.Command.quot -/- match -/ +/-! # match -/ --- an "alternative" of patterns plus right-hand side +/-- an "alternative" of patterns plus right-hand side -/ private abbrev Alt := List Term × Term /-- @@ -244,45 +244,45 @@ private abbrev Alt := List Term × Term alternative. This datatype describes what kind of check this involves, which helps other patterns decide if they are covered by the same check and don't have to be checked again (see also `MatchResult`). -/ inductive HeadCheck where - -- match step that always succeeds: _, x, `($x), ... - | unconditional - -- match step based on kind and, optionally, arity of discriminant - -- If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the - -- same number of new patterns. - -- We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by - -- the node kind. - -- without arity: `($x:k) - -- with arity: any quotation without an antiquotation head pattern - | shape (k : List SyntaxNodeKind) (arity : Option Nat) - -- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants - -- for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children. - -- example: `([$x, $xs,*, $y]) is `slice 2 2` - | slice (numPrefix numSuffix : Nat) - -- other, complicated match step that will probably only cover identical patterns - -- example: antiquotation splices `($[...]*) - | other (pat : Syntax) + | /-- match step that always succeeds: _, x, `($x), ... -/ + unconditional + | /-- match step based on kind and, optionally, arity of discriminant + If `arity` is given, that number of new discriminants is introduced. `covered` patterns should then introduce the + same number of new patterns. + We actually check the arity at run time only in the case of `null` nodes since it should otherwise by implied by + the node kind. + without arity: `($x:k) + with arity: any quotation without an antiquotation head pattern -/ + shape (k : List SyntaxNodeKind) (arity : Option Nat) + | /-- Match step that succeeds on `null` nodes of arity at least `numPrefix + numSuffix`, introducing discriminants + for the first `numPrefix` children, one `null` node for those in between, and for the `numSuffix` last children. + example: `([$x, $xs,*, $y]) is `slice 2 2` -/ + slice (numPrefix numSuffix : Nat) + | /-- other, complicated match step that will probably only cover identical patterns + example: antiquotation splices `($[...]*) -/ + other (pat : Syntax) open HeadCheck /-- Describe whether a pattern is covered by a head check (induced by the pattern itself or a different pattern). -/ inductive MatchResult where - -- Pattern agrees with head check, remove and transform remaining alternative. - -- If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch. - | covered (f : Alt → TermElabM Alt) (exhaustive : Bool) - -- Pattern disagrees with head check, include in "no" branch only - | uncovered - -- Pattern is not quite sure yet; include unchanged in both branches - | undecided + | /-- Pattern agrees with head check, remove and transform remaining alternative. + If `exhaustive` is `false`, *also* include unchanged alternative in the "no" branch. -/ + covered (f : Alt → TermElabM Alt) (exhaustive : Bool) + | /-- Pattern disagrees with head check, include in "no" branch only -/ + uncovered + | /-- Pattern is not quite sure yet; include unchanged in both branches -/ + undecided open MatchResult /-- All necessary information on a pattern head. -/ structure HeadInfo where - -- check induced by the pattern + /-- check induced by the pattern -/ check : HeadCheck - -- compute compatibility of pattern with given head check + /-- compute compatibility of pattern with given head check -/ onMatch (taken : HeadCheck) : MatchResult - -- actually run the specified head check, with the discriminant bound to `discr` + /-- actually run the specified head check, with the discriminant bound to `discr` -/ doMatch (yes : (newDiscrs : List Term) → TermElabM Term) (no : TermElabM Term) : TermElabM Term /-- Adapt alternatives that do not introduce new discriminants in `doMatch`, but are covered by those that do so. -/ @@ -475,7 +475,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := | r => r } | _ => throwErrorAt pat "match (syntax) : unexpected pattern kind {pat}" --- Bind right-hand side to new `let_delayed` decl in order to prevent code duplication +/-- Bind right-hand side to new `let_delayed` decl in order to prevent code duplication -/ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Array Syntax × Alt) -- NOTE: new macro scope so that introduced bindings do not collide | (pats, rhs) => do diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 1e3dabb88f..7747b9498f 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -254,8 +254,8 @@ def Field.isSimple {σ} : Field σ → Bool | _ => false inductive Struct where - /- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/ - | mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source) + | /-- Remark: the field `params` is use for default value propagation. It is initially empty, and then set at `elabStruct`. -/ + mk (ref : Syntax) (structName : Name) (params : Array (Name × Expr)) (fields : List (Field Struct)) (source : Source) deriving Inhabited abbrev Fields := List (Field Struct) @@ -393,7 +393,7 @@ private def expandNumLitFields (s : Struct) : TermElabM Struct := else return { field with lhs := .fieldName ref fieldNames[idx - 1]! :: rest } | _ => return field -/- For example, consider the following structures: +/-- For example, consider the following structures: ``` structure A where x : Nat diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 8496c9d5a3..e2750400c1 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -21,7 +21,7 @@ namespace Lean.Elab.Command open Meta open TSyntax.Compat -/- Recall that the `structure command syntax is +/-! Recall that the `structure command syntax is ``` leading_parser (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields) ``` diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 56e77d5b9f..b2d4349b27 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -8,7 +8,7 @@ import Lean.Parser.Syntax import Lean.Elab.Util namespace Lean.Elab.Term -/- +/-- Expand `optional «precedence»` where «precedence» := leading_parser " : " >> precedenceParser -/ def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) := @@ -33,7 +33,7 @@ structure ToParserDescrContext where catName : Name first : Bool leftRec : Bool -- true iff left recursion is allowed - /- See comment at `Parser.ParserCategory`. -/ + /-- See comment at `Parser.ParserCategory`. -/ behavior : Parser.LeadingIdentBehavior abbrev ToParserDescrM := ReaderT ToParserDescrContext (StateRefT (Option Nat) TermElabM) @@ -126,7 +126,7 @@ where | some stxNew => process stxNew | none => throwErrorAt stx "unexpected syntax kind of category `syntax`: {kind}" - /- Sequence (aka NullNode) -/ + /-- Sequence (aka NullNode) -/ processSeq (stx : Syntax) := do let args := stx.getArgs if (← checkLeftRec stx[0]) then @@ -300,7 +300,7 @@ where | .str _ s => s ++ str | _ => str -/- We assume a new syntax can be treated as an atom when it starts and ends with a token. +/-- We assume a new syntax can be treated as an atom when it starts and ends with a token. Here are examples of atom-like syntax. ``` syntax "(" term ")" : term diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 5ef71672f2..bd8adccaa3 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -203,7 +203,7 @@ where let some mvarIds ← synthesizeSomeUsingDefault? mvarIds | return false synthesizePending mvarIds -/- Used to implement `synthesizeUsingDefault`. This method only consider default instances with the given priority. -/ +/-- Used to implement `synthesizeUsingDefault`. This method only consider default instances with the given priority. -/ private def synthesizeSomeUsingDefaultPrio (prio : Nat) : TermElabM Bool := do let rec visit (pendingMVars : List MVarId) (pendingMVarsNew : List MVarId) : TermElabM Bool := do match pendingMVars with @@ -423,7 +423,7 @@ end def synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := false) : TermElabM Unit := synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := ignoreStuckTC) -/- Keep invoking `synthesizeUsingDefault` until it returns false. -/ +/-- Keep invoking `synthesizeUsingDefault` until it returns false. -/ private partial def synthesizeUsingDefaultLoop : TermElabM Unit := do if (← synthesizeUsingDefault) then synthesizeSyntheticMVars (mayPostpone := true) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 4d58822f1d..6415fdb772 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -19,7 +19,7 @@ import Lean.Elab.Binders namespace Lean.Elab open Meta -/- Assign `mvarId := sorry` -/ +/-- Assign `mvarId := sorry` -/ def admitGoal (mvarId : MVarId) : MetaM Unit := withMVarContext mvarId do let mvarType ← inferType (mkMVar mvarId) @@ -130,7 +130,7 @@ def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do @[inline] def withTacticInfoContext (stx : Syntax) (x : TacticM α) : TacticM α := do withInfoContext x (← mkInitialTacticInfo stx) -/- +/-! Important: we must define `evalTactic` before we define the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages, and this is bad when rethrowing the exception at the `catch` block in these methods. @@ -160,7 +160,7 @@ partial def evalTactic (stx : Syntax) : TacticM Unit := expandEval s macros evalFns #[] | .missing => pure () | _ => throwError m!"unexpected tactic{indentD stx}" -where +where throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do if let some fail := failures[0]? then -- Recall that `failures[0]` is the highest priority evalFn/macro @@ -187,8 +187,8 @@ where else throw ex -- (*) - expandEval (s : SavedState) (macros : List _) (evalFns : List _) (failures : Array EvalTacticFailure) : TacticM Unit := - match macros with + expandEval (s : SavedState) (macros : List _) (evalFns : List _) (failures : Array EvalTacticFailure) : TacticM Unit := + match macros with | [] => eval s evalFns failures | m :: ms => try @@ -229,7 +229,7 @@ def focusAndDone (tactic : TacticM α) : TacticM α := done pure a -/- Close the main goal using the given tactic. If it fails, log the error and `admit` -/ +/-- Close the main goal using the given tactic. If it fails, log the error and `admit` -/ def closeUsingOrAdmit (tac : TacticM Unit) : TacticM Unit := do /- Important: we must define `closeUsingOrAdmit` before we define the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages. -/ @@ -270,7 +270,7 @@ instance : Alternative TacticM where failure := fun {_} => throwError "failed" orElse := Tactic.orElse -/- +/-- Save the current tactic state for a token `stx`. This method is a no-op if `stx` has no position information. We use this method to save the tactic state at punctuation such as `;` @@ -279,7 +279,7 @@ def saveTacticInfoForToken (stx : Syntax) : TacticM Unit := do unless stx.getPos?.isNone do withTacticInfoContext stx (pure ()) -/- Elaborate `x` with `stx` on the macro stack -/ +/-- Elaborate `x` with `stx` on the macro stack -/ @[inline] def withMacroExpansion (beforeStx afterStx : Syntax) (x : TacticM α) : TacticM α := withMacroExpansionInfo beforeStx afterStx do diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index ae2d4c4a0c..78de6362e1 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -64,7 +64,7 @@ where else return result ++ acc -/- Evaluate `many (group (tactic >> optional ";")) -/ +/-- Evaluate `many (group (tactic >> optional ";")) -/ def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do for seqElem in (← addCheckpoints stx.getArgs) do evalTactic seqElem[0] diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index d105d3b19b..a656a2478e 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -14,7 +14,7 @@ import Lean.Elab.SyntheticMVars namespace Lean.Elab.Tactic open Meta -/- `elabTerm` for Tactics and basic tactics that use it. -/ +/-! # `elabTerm` for Tactics and basic tactics that use it. -/ def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/ @@ -42,7 +42,7 @@ def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpo Term.throwTypeMismatchError none expectedType eType e return e -/- Try to close main goal using `x target`, where `target` is the type of the main goal. -/ +/-- Try to close main goal using `x target`, where `target` is the type of the main goal. -/ def closeMainGoalUsing (x : Expr → TacticM Expr) (checkUnassigned := true) : TacticM Unit := withMainContext do closeMainGoal (checkUnassigned := checkUnassigned) (← x (← getMainTarget)) @@ -81,7 +81,7 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds pure (val, newMVarIds) -/- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables. +/-- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables. Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be filled by typing constraints. "Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?`. -/ diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 8a9c2df512..1acf41703a 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -68,7 +68,7 @@ def evalAlt (mvarId : MVarId) (alt : Syntax) (remainingGoals : Array MVarId) : T closeUsingOrAdmit (withTacticInfoContext alt (evalTactic rhs)) return remainingGoals -/- +/-! Helper method for creating an user-defined eliminator/recursor application. -/ namespace ElimApp @@ -90,9 +90,9 @@ abbrev M := ReaderT Context $ StateRefT State TermElabM private def addNewArg (arg : Expr) : M Unit := modify fun s => { s with argPos := s.argPos+1, f := mkApp s.f arg, fType := s.fType.bindingBody!.instantiate1 arg } -/- Return the binder name at `fType`. This method assumes `fType` is a function type. -/ +/-- Return the binder name at `fType`. This method assumes `fType` is a function type. -/ private def getBindingName : M Name := return (← get).fType.bindingName! -/- Return the next argument expected type. This method assumes `fType` is a function type. -/ +/-- Return the next argument expected type. This method assumes `fType` is a function type. -/ private def getArgExpectedType : M Expr := return (← get).fType.bindingDomain! private def getFType : M Expr := do @@ -164,7 +164,7 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) let alts ← s.alts.filterM fun alt => return !(← isExprMVarAssigned alt.2) return { elimApp := (← instantiateMVars s.f), alts, others := others } -/- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign +/-- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign `motiveArg := fun targets => C[targets]` -/ def setMotiveArg (mvarId : MVarId) (motiveArg : MVarId) (targets : Array FVarId) : MetaM Unit := do let type ← inferType (mkMVar mvarId) @@ -441,7 +441,7 @@ private def expandCases? (induction : Syntax) : Option Syntax := do let inductionAlts' ← expandInductionAlts? optInductionAlts[0] return induction.setArg 3 (mkNullNode #[inductionAlts']) -/- +/-- We may have at most one `| _ => ...` (wildcard alternative), and it must not set variable names. The idea is to make sure users do not write unstructured tactics. -/ private def checkAltsOfOptInductionAlts (optInductionAlts : Syntax) : TacticM Unit := diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 50c6eab784..56757f9141 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -382,9 +382,9 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl -/ inductive LVal where | fieldIdx (ref : Syntax) (i : Nat) - /- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name. + | /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name. `ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/ - | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax) + fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax) def LVal.getRef : LVal → Syntax | .fieldIdx ref _ => ref @@ -461,12 +461,12 @@ def liftLevelM (x : LevelElabM α) : TermElabM α := do def elabLevel (stx : Syntax) : TermElabM Level := liftLevelM <| Level.elabLevel stx -/- Elaborate `x` with `stx` on the macro stack -/ +/-- Elaborate `x` with `stx` on the macro stack -/ def withMacroExpansion (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α := withMacroExpansionInfo beforeStx afterStx do withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x -/- +/-- Add the given metavariable to the list of pending synthetic metavariables. The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/ def registerSyntheticMVar (stx : Syntax) (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do @@ -495,7 +495,7 @@ def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) | Expr.mvar mvarId => registerMVarErrorCustomInfo mvarId ref msgData | _ => pure () -/- +/-- Auxiliary method for reporting errors of the form "... contains metavariables ...". This kind of error is thrown, for example, at `Match.lean` where elaboration cannot continue if there are metavariables in patterns. @@ -571,7 +571,7 @@ def ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit := do if (← logUnassignedUsingErrorInfos pendingMVarIds) then throwAbortCommand -/- +/-- Execute `x` without allowing it to postpone elaboration tasks. That is, `tryPostpone` is a noop. -/ def withoutPostponing (x : TermElabM α) : TermElabM α := @@ -1126,7 +1126,7 @@ def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → Term else Elab.withInfoContext' x mkInfo -/- +/-- Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or an error is found. -/ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) @@ -1312,7 +1312,7 @@ where | type, fvars => elabImplicitLambdaAux stx catchExPostpone type fvars -/- Main loop for `elabTerm` -/ +/-- Main loop for `elabTerm` -/ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr | .missing => mkSyntheticSorryFor expectedType? | stx => withFreshMacroScope <| withIncRecDepth do @@ -1544,7 +1544,7 @@ def mkAuxName (suffix : Name) : TermElabM Name := do builtin_initialize registerTraceClass `Elab.letrec -/- Return true if mvarId is an auxiliary metavariable created for compiling `let rec` or it +/-- Return true if mvarId is an auxiliary metavariable created for compiling `let rec` or it is delayed assigned to one. -/ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do trace[Elab.letrec] "mvarId: {mkMVar mvarId} letrecMVars: {(← get).letRecsToLift.map (mkMVar $ ·.mvarId)}" diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index c551733386..96fa3b626b 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -8,6 +8,7 @@ import Lean.Parser.Syntax import Lean.Parser.Extension import Lean.KeyedDeclsAttribute import Lean.Elab.Exception +import Lean.Elab.InfoTree import Lean.DocString import Lean.DeclarationRange import Lean.Compiler.InitAttr @@ -44,7 +45,7 @@ structure MacroStackElem where abbrev MacroStack := List MacroStackElem -/- If `ref` does not have position information, then try to use macroStack -/ +/-- If `ref` does not have position information, then try to use macroStack -/ def getBetterRef (ref : Syntax) (macroStack : MacroStack) : Syntax := match ref.getPos? with | some _ => ref diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 048fe30174..388890eb17 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -13,7 +13,7 @@ import Lean.Util.FindExpr import Lean.Util.Profile namespace Lean -/- Opaque environment extension state. -/ +/-- Opaque environment extension state. -/ opaque EnvExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩ def EnvExtensionState : Type := EnvExtensionStateSpec.fst instance : Inhabited EnvExtensionState := EnvExtensionStateSpec.snd @@ -44,12 +44,12 @@ opaque CompactedRegion.isMemoryMapped : CompactedRegion → Bool @[extern "lean_compacted_region_free"] unsafe opaque CompactedRegion.free : CompactedRegion → IO Unit -/- Opaque persistent environment extension entry. -/ +/-- Opaque persistent environment extension entry. -/ opaque EnvExtensionEntrySpec : NonemptyType.{0} def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property -/- Content of a .olean file. +/-- Content of a .olean file. We use `compact.cpp` to generate the image of this object in disk. -/ structure ModuleData where imports : Array Import @@ -57,7 +57,7 @@ structure ModuleData where entries : Array (Name × Array EnvExtensionEntry) deriving Inhabited -/- Environment fields that are not used often. -/ +/-- Environment fields that are not used often. -/ structure EnvironmentHeader where trustLevel : UInt32 := 0 quotInit : Bool := false @@ -145,13 +145,13 @@ inductive KernelException where namespace Environment -/- Type check given declaration and add it to the environment -/ +/-- Type check given declaration and add it to the environment -/ @[extern "lean_add_decl"] opaque addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment end Environment -/- Interface for managing environment extensions. -/ +/-- Interface for managing environment extensions. -/ structure EnvExtensionInterface where ext : Type → Type inhabitedExt {σ} : Inhabited σ → Inhabited (ext σ) @@ -174,7 +174,7 @@ instance : Inhabited EnvExtensionInterface where mkInitialExtStates := pure #[] } -/- Unsafe implementation of `EnvExtensionInterface` -/ +/-! # Unsafe implementation of `EnvExtensionInterface` -/ namespace EnvExtensionInterfaceUnsafe structure Ext (σ : Type) where @@ -272,7 +272,7 @@ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ def getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) : σ := EnvExtensionInterfaceImp.getState ext env end EnvExtension -/- Environment extensions can only be registered during initialization. +/-- Environment extensions can only be registered during initialization. Reasons: 1- Our implementation assumes the number of extensions does not change after an environment object is created. 2- We do not use any synchronization primitive to access `envExtensionsRef`. @@ -304,7 +304,7 @@ structure ImportM.Context where abbrev ImportM := ReaderT Lean.ImportM.Context IO -/- An environment extension with support for storing/retrieving entries from a .olean file. +/-- An environment extension with support for storing/retrieving entries from a .olean file. - α is the type of the entries that are stored in .olean files. - β is the type of values used to update the state. - σ is the actual state. @@ -396,8 +396,7 @@ unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ] @[implementedBy registerPersistentEnvExtensionUnsafe] opaque registerPersistentEnvExtension {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) : IO (PersistentEnvExtension α β σ) -/- Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries. -/ - +/-- Simple `PersistentEnvExtension` that implements `exportEntriesFn` using a list of entries. -/ def SimplePersistentEnvExtension (α σ : Type) := PersistentEnvExtension α α (List α × σ) @[specialize] def mkStateFromImportedEntries {α σ : Type} (addEntryFn : σ → α → σ) (initState : σ) (as : Array (Array α)) : σ := @@ -761,7 +760,7 @@ def hasUnsafe (env : Environment) (e : Expr) : Bool := end Environment namespace Kernel -/- Kernel API -/ +/-! # Kernel API -/ /-- Kernel isDefEq predicate. We use it mainly for debugging purposes. diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index bd9839db9c..a15ef5992c 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -10,7 +10,7 @@ import Lean.Util.MonadCache namespace Lean -/- Exception type used in most Lean monads -/ +/-- Exception type used in most Lean monads -/ inductive Exception where | error (ref : Syntax) (msg : MessageData) | internal (id : InternalExceptionId) (extra : KVMap := {}) @@ -25,7 +25,7 @@ def Exception.getRef : Exception → Syntax instance : Inhabited Exception := ⟨Exception.error default default⟩ -/- Similar to `AddMessageContext`, but for error messages. +/-- Similar to `AddMessageContext`, but for error messages. The default instance just uses `AddMessageContext`. In error messages, we may want to provide additional information (e.g., macro expansion stack), and refine the `(ref : Syntax)`. -/ diff --git a/src/Lean/HeadIndex.lean b/src/Lean/HeadIndex.lean index 57f1c51e7e..ebea4bf733 100644 --- a/src/Lean/HeadIndex.lean +++ b/src/Lean/HeadIndex.lean @@ -51,7 +51,7 @@ private def headNumArgsAux : Expr → Nat → Nat def headNumArgs (e : Expr) : Nat := headNumArgsAux e 0 -/- +/-- Quick version that may fail if it "hits" a loose bound variable. This can happen, for example, if the input expression is of the form. ``` @@ -73,7 +73,7 @@ private def toHeadIndexQuick? : Expr → Option HeadIndex | mdata _ e => toHeadIndexQuick? e | _ => none -/- +/-- Slower version of `toHeadIndexQuick?` that "expands" let-declarations to make sure we never hit a loose bound variable. The performance of the `letE` alternative can be improved, but this function should not be in the hotpath diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean index cda2e1a112..efa8f2eb56 100644 --- a/src/Lean/Hygiene.lean +++ b/src/Lean/Hygiene.lean @@ -8,7 +8,7 @@ import Lean.Data.Options import Lean.Data.Format namespace Lean -/- Remark: `MonadQuotation` class is part of the `Init` package and loaded by default since it is used in the builtin command `macro`. -/ +/-! Remark: `MonadQuotation` class is part of the `Init` package and loaded by default since it is used in the builtin command `macro`. -/ structure Unhygienic.Context where ref : Syntax diff --git a/src/Lean/ImportingFlag.lean b/src/Lean/ImportingFlag.lean index 3fc36632fa..9107ffd27c 100644 --- a/src/Lean/ImportingFlag.lean +++ b/src/Lean/ImportingFlag.lean @@ -27,7 +27,7 @@ unsafe def enableInitializersExecution : IO Unit := def isInitializerExecutionEnabled : IO Bool := runInitializersRef.get -/- We say Lean is "initializing" when it is executing `builtin_initialize` declarations or importing modules. +/-- We say Lean is "initializing" when it is executing `builtin_initialize` declarations or importing modules. Recall that Lean excutes `initialize` declarations while importing modules. -/ def initializing : IO Bool := IO.initializing <||> importingRef.get diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index be9855988a..29dd7360ff 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -44,7 +44,7 @@ structure OLeanEntry where deriving Inhabited structure AttributeEntry (γ : Type) extends OLeanEntry where - /- Recall that we cannot store `γ` into .olean files because it is a closure. + /-- Recall that we cannot store `γ` into .olean files because it is a closure. Given `OLeanEntry.declName`, we convert it into a `γ` by using the unsafe function `evalConstCheck`. -/ value : γ diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index f82ffda85a..8bc8898d5c 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -341,7 +341,7 @@ partial def isSubPrefixOfAux (a₁ a₂ : PArray (Option LocalDecl)) (exceptFVar else false else true -/- Given `lctx₁ - exceptFVars` of the form `(x_1 : A_1) ... (x_n : A_n)`, then return true +/-- Given `lctx₁ - exceptFVars` of the form `(x_1 : A_1) ... (x_n : A_n)`, then return true iff there is a local context `B_1* (x_1 : A_1) ... B_n* (x_n : A_n)` which is a prefix of `lctx₂` where `B_i`'s are (possibly empty) sequences of local declarations. -/ def isSubPrefixOf (lctx₁ lctx₂ : LocalContext) (exceptFVars : Array Expr := #[]) : Bool := diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 48a6a0daad..cf80353b6d 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -19,7 +19,7 @@ import Lean.Meta.DiscrTreeTypes import Lean.Eval import Lean.CoreM -/- +/-! This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks. 1- Weak head normal form computation with support for metavariables and transparency modes. 2- Definitionally equality checking with support for metavariables (aka unification modulo definitional equality). @@ -424,7 +424,7 @@ def useEtaStruct (inductName : Name) : MetaM Bool := do | .all => return true | .notClasses => return !isClass (← getEnv) inductName -/- WARNING: The following 4 constants are a hack for simulating forward declarations. +/-! WARNING: The following 4 constants are a hack for simulating forward declarations. They are defined later using the `export` attribute. This is hackish because we have to hard-code the true arity of these definitions here, and make sure the C names match. We have used another hack based on `IO.Ref`s in the past, it was safer but less efficient. -/ @@ -481,7 +481,7 @@ def mkFreshTypeMVar (kind := MetavarKind.natural) (userName := Name.anonymous) : let u ← mkFreshLevelMVar mkFreshExprMVar (mkSort u) kind userName -/- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create +/-- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create the metavar using this method. -/ private def mkFreshExprMVarWithIdCore (mvarId : MVarId) (type : Expr) (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0) @@ -537,7 +537,7 @@ def isSyntheticMVar (e : Expr) : MetaM Bool := do def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit := modifyMCtx fun mctx => mctx.setMVarKind mvarId kind -/- Update the type of the given metavariable. This function assumes the new type is +/-- Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one -/ def setMVarType (mvarId : MVarId) (type : Expr) : MetaM Unit := do modifyMCtx fun mctx => mctx.setMVarType mvarId type @@ -690,7 +690,7 @@ private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) : else return none -/- Remark: we later define `getConst?` at `GetConst.lean` after we define `Instances.lean`. +/-- Remark: we later define `getConst?` at `GetConst.lean` after we define `Instances.lean`. This method is only used to implement `isClassQuickConst?`. It is very similar to `getConst?`, but it returns none when `TransparencyMode.instances` and `constName` is an instance. This difference should be irrelevant for `isClassQuickConst?`. -/ @@ -1265,7 +1265,7 @@ private partial def instantiateForallAux (ps : Array Expr) (i : Nat) (e : Expr) else pure e -/- Given `e` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `B[p_1, ..., p_n]`. -/ +/-- Given `e` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `B[p_1, ..., p_n]`. -/ def instantiateForall (e : Expr) (ps : Array Expr) : MetaM Expr := instantiateForallAux ps 0 e @@ -1278,7 +1278,7 @@ private partial def instantiateLambdaAux (ps : Array Expr) (i : Nat) (e : Expr) else pure e -/- Given `e` of the form `fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `t[p_1, ..., p_n]`. +/-- Given `e` of the form `fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `t[p_1, ..., p_n]`. It uses `whnf` to reduce `e` if it is not a lambda -/ def instantiateLambda (e : Expr) (ps : Array Expr) : MetaM Expr := instantiateLambdaAux ps 0 e diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index 241e79d0a2..e4b99a578a 100644 --- a/src/Lean/Meta/Check.lean +++ b/src/Lean/Meta/Check.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ import Lean.Meta.InferType -/- +/-! This is not the Kernel type checker, but an auxiliary method for checking whether terms produced by tactics and `isDefEq` are type correct. -/ @@ -35,8 +35,8 @@ private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do | Expr.forallE _ d _ c => return (d, c) | _ => throwFunctionExpected f -/- -Given to expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true` to +/-- +Given two expressions `a` and `b`, this method tries to annotate terms with `pp.explicit := true` to expose "implicit" differences. For example, suppose `a` and `b` are of the form ```lean @HashMap Nat Nat eqInst hasInst1 @@ -111,7 +111,7 @@ where return some (as.set! i ai, bs.set! i bi) return none -/- +/-- Return error message "has type{givenType}\nbut is expected to have type{expectedType}" -/ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageData := do diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index d8e52610c8..3a9a52a716 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -10,7 +10,7 @@ import Lean.Util.FoldConsts import Lean.Meta.Basic import Lean.Meta.Check -/- +/-! This module provides functions for "closing" open terms and creating auxiliary definitions. Here, we say a term is "open" if diff --git a/src/Lean/Meta/DecLevel.lean b/src/Lean/Meta/DecLevel.lean index c535289d52..565147f10e 100644 --- a/src/Lean/Meta/DecLevel.lean +++ b/src/Lean/Meta/DecLevel.lean @@ -63,7 +63,7 @@ def decLevel (u : Level) : MetaM Level := do | some u => return u | none => throwError "invalid universe level, {u} is not greater than 0" -/- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`. +/-- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`. Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level, and then decrement 1 to obtain `u`. -/ def getDecLevel (type : Expr) : MetaM Level := do diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index 379de67392..b068fe00a6 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -10,7 +10,7 @@ import Lean.Meta.WHNF import Lean.Meta.Match.MatcherInfo namespace Lean.Meta.DiscrTree -/- +/-! (Imperfect) discrimination trees. We use a hybrid representation. - A `PersistentHashMap` for the root node which usually contains many children. @@ -108,7 +108,7 @@ partial def format [ToFormat α] (d : DiscrTree α) : Format := instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩ -/- The discrimination tree ignores implicit arguments and proofs. +/-- The discrimination tree ignores implicit arguments and proofs. We use the following auxiliary id as a "mark". -/ private def tmpMVarId : MVarId := { name := `_discr_tree_tmp } private def tmpStar := mkMVar tmpMVarId @@ -205,7 +205,7 @@ private def isOffset (fName : Name) (e : Expr) : MetaM Bool := do else return fName == ``Nat.succ && e.getAppNumArgs == 1 -/- +/-- TODO: add hook for users adding their own functions for controlling `shouldAddAsStar` Different `DiscrTree` users may populate this set using, for example, attributes. diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index 07a6ceff7f..5300aa4d77 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/src/Lean/Meta/DiscrTreeTypes.lean @@ -7,7 +7,7 @@ import Lean.Expr namespace Lean.Meta -/- See file `DiscrTree.lean` for the actual implementation and documentation. -/ +/-! See file `DiscrTree.lean` for the actual implementation and documentation. -/ namespace DiscrTree diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 47bb528b06..154cf2ff2e 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -289,7 +289,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta k loop 0 -/- Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`. +/-- Auxiliary function for `isDefEqBinding` for handling binders `forall/fun`. It accumulates the new free variables in `fvars`, and declare them at `lctx`. We use the domain types of `e₁` to create the new free variables. We store the domain types of `e₂` at `ds₂`. -/ @@ -368,7 +368,7 @@ private partial def mkLambdaFVarsWithLetDeps (xs : Array Expr) (v : Expr) : Meta mkLambdaFVars ys v where - /- Return true if there are let-declarions between `xs[0]` and `xs[xs.size-1]`. + /-- Return true if there are let-declarions between `xs[0]` and `xs[xs.size-1]`. We use it a quick-check to avoid the more expensive collection procedure. -/ hasLetDeclsInBetween : MetaM Bool := do let check (lctx : LocalContext) : Bool := Id.run do @@ -386,7 +386,7 @@ where else return check (← getLCtx) - /- Traverse `e` and stores in the state `NameHashSet` any let-declaration with index greater than `(← read)`. + /-- Traverse `e` and stores in the state `NameHashSet` any let-declaration with index greater than `(← read)`. The context `Nat` is the position of `xs[0]` in the local context. -/ collectLetDeclsFrom (e : Expr) : ReaderT Nat (StateRefT FVarIdHashSet MetaM) Unit := do let rec visit (e : Expr) : MonadCacheT Expr Unit (ReaderT Nat (StateRefT FVarIdHashSet MetaM)) Unit := @@ -405,7 +405,7 @@ where | _ => pure () visit (← instantiateMVars e) |>.run - /- + /-- Auxiliary definition for traversing all declarations between `xs[0]` ... `xs.back` backwards. The `Nat` argument is the current position in the local context being visited, and it is less than or equal to the position of `xs.back` in the local context. @@ -427,7 +427,7 @@ where | _ => pure () collectLetDepsAux i - /- Computes the set `ys`. It is a set of `FVarId`s, -/ + /-- Computes the set `ys`. It is a set of `FVarId`s, -/ collectLetDeps : MetaM FVarIdHashSet := do let lctx ← getLCtx let start := lctx.getFVar! xs[0]! |>.index @@ -436,7 +436,7 @@ where let (_, s) ← collectLetDepsAux stop |>.run start |>.run s return s - /- Computes the array `ys` containing let-decls between `xs[0]` and `xs.back` that + /-- Computes the array `ys` containing let-decls between `xs[0]` and `xs.back` that some `x` in `xs` depends on. -/ addLetDeps : MetaM (Array Expr) := do let lctx ← getLCtx @@ -453,7 +453,7 @@ where ys := ys.push localDecl.toExpr return ys -/- +/-! Each metavariable is declared in a particular local context. We use the notation `C |- ?m : t` to denote a metavariable `?m` that was declared at the local context `C` with type `t` (see `MetavarDecl`). @@ -739,7 +739,7 @@ mutual traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId) throwCheckAssignmentFailure - /- + /-- Auxiliary function used to "fix" subterms of the form `?m x_1 ... x_n` where `x_i`s are free variables, and one of them is out-of-scope. See `Expr.app` case at `check`. @@ -898,7 +898,7 @@ private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f | _ => pure false -/- +/-- Auxiliary method for applying first-order unification. It is an approximation. Remark: this method is trying to solve the unification constraint: @@ -939,14 +939,14 @@ private partial def simpAssignmentArgAux : Expr → MetaM Expr | _ => pure e | e => pure e -/- Auxiliary procedure for processing `?m a₁ ... aₙ =?= v`. +/-- Auxiliary procedure for processing `?m a₁ ... aₙ =?= v`. We apply it to each `aᵢ`. It instantiates assigned metavariables if `aᵢ` is of the form `f[?n] b₁ ... bₘ`, and then removes metadata, and zeta-expand let-decls. -/ private def simpAssignmentArg (arg : Expr) : MetaM Expr := do let arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg simpAssignmentArgAux arg -/- Assign `mvar := fun a_1 ... a_{numArgs} => v`. +/-- Assign `mvar := fun a_1 ... a_{numArgs} => v`. We use it at `processConstApprox` and `isDefEqMVarSelf` -/ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do let mvarDecl ← getMVarDecl mvar.mvarId! @@ -1389,7 +1389,7 @@ private def isDefEqProofIrrel (t s : Expr) : MetaM LBool := do else pure LBool.undef -/- Try to solve constraint of the form `?m args₁ =?= ?m args₂`. +/-- Try to solve constraint of the form `?m args₁ =?= ?m args₂`. - First try to unify `args₁` and `args₂`, and return true if successful - Otherwise, try to assign `?m` to a constant function of the form `fun x_1 ... x_n => ?n` where `?n` is a fresh metavariable. See `assignConst`. -/ @@ -1411,7 +1411,7 @@ private def isDefEqMVarSelf (mvar : Expr) (args₁ args₂ : Array Expr) : MetaM else pure false -/- Remove unnecessary let-decls -/ +/-- Remove unnecessary let-decls -/ private def consumeLet : Expr → Expr | e@(Expr.letE _ _ _ b _) => if b.hasLooseBVars then e else consumeLet b | e => e @@ -1561,7 +1561,7 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do else isDefEqQuickMVarMVar t s --- Both `t` and `s` are terms of the form `?m ...` +/-- Both `t` and `s` are terms of the form `?m ...` -/ private partial def isDefEqQuickMVarMVar (t s : Expr) : MetaM LBool := do if s.isMVar && !t.isMVar then /- Solve `?m t =?= ?n` by trying first `?n := ?m t`. @@ -1608,7 +1608,7 @@ private def isDefEqProj : Expr → Expr → MetaM Bool | v, Expr.proj structName 0 s => isDefEqSingleton structName s v | _, _ => pure false where - /- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve contraint as `?m ... =?= ⟨v⟩` -/ + /-- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve contraint as `?m ... =?= ⟨v⟩` -/ isDefEqSingleton (structName : Name) (s : Expr) (v : Expr) : MetaM Bool := do let ctorVal := getStructureCtor (← getEnv) structName if ctorVal.numFields != 1 then @@ -1627,7 +1627,7 @@ where else return false -/- +/-- Given applications `t` and `s` that are in WHNF (modulo the current transparency setting), check whether they are definitionally equal or not. -/ @@ -1656,7 +1656,7 @@ private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do else return false -/- +/-- The `whnf` procedure has support for unfolding class projections when the transparency mode is set to `.instances`. This method ensures the behavior of `whnf` and `isDefEq` is consistent in this transparency mode. diff --git a/src/Lean/Meta/Inductive.lean b/src/Lean/Meta/Inductive.lean index 84e5a2c865..25ba641af1 100644 --- a/src/Lean/Meta/Inductive.lean +++ b/src/Lean/Meta/Inductive.lean @@ -5,11 +5,11 @@ Authors: Leonardo de Moura -/ import Lean.Meta.Basic -/- Helper methods for inductive datatypes -/ +/-! # Helper methods for inductive datatypes -/ namespace Lean.Meta -/- Return true if the types of the given constructors are compatible. -/ +/-- Return true if the types of the given constructors are compatible. -/ def compatibleCtors (ctorName₁ ctorName₂ : Name) : MetaM Bool := do let ctorInfo₁ ← getConstInfoCtor ctorName₁ let ctorInfo₂ ← getConstInfoCtor ctorName₂ diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 69b8f7db2c..d4336e7648 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -8,7 +8,7 @@ import Lean.Meta.Basic namespace Lean -/- +/-- Auxiliary function for instantiating the loose bound variables in `e` with `args[start:stop]`. This function is similar to `instantiateRevRange`, but it applies beta-reduction when we instantiate a bound variable with a lambda expression. @@ -145,7 +145,7 @@ private def inferForallType (e : Expr) : MetaM Expr := return mkLevelIMax' xTypeLvl lvl return mkSort lvl.normalize -/- Infer type of lambda and let expressions -/ +/-- Infer type of lambda and let expressions -/ private def inferLambdaType (e : Expr) : MetaM Expr := lambdaLetTelescope e fun xs e => do let type ← inferType e diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 853895d3b7..ba760dd3cd 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -81,7 +81,7 @@ def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) := def getErasedInstances : CoreM (Std.PHashSet Name) := return Meta.instanceExtension.getState (← getEnv) |>.erased -/- Default instance support -/ +/-! # Default instance support -/ structure DefaultInstanceEntry where className : Name diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean index ed9fad00d4..c507a34813 100644 --- a/src/Lean/Meta/Match/Basic.lean +++ b/src/Lean/Meta/Match/Basic.lean @@ -65,7 +65,7 @@ where let fields ← fields.mapM visit pure $ mkAppN (mkConst ctorName us) (params ++ fields).toArray -/- Apply the free variable substitution `s` to the given pattern -/ +/-- Apply the free variable substitution `s` to the given pattern -/ partial def applyFVarSubst (s : FVarSubst) : Pattern → Pattern | inaccessible e => inaccessible $ s.apply e | ctor n us ps fs => ctor n us (ps.map s.apply) $ fs.map (applyFVarSubst s) @@ -157,7 +157,7 @@ def replaceFVarId (fvarId : FVarId) (v : Expr) (alt : Alt) : Alt := decls.map $ replaceFVarIdAtLocalDecl fvarId v, rhs := alt.rhs.replaceFVarId fvarId v } -/- +/-- Similar to `checkAndReplaceFVarId`, but ensures type of `v` is definitionally equal to type of `fvarId`. This extra check is necessary when performing dependent elimination and inaccessible terms have been used. For example, consider the following code fragment: diff --git a/src/Lean/Meta/Match/MVarRenaming.lean b/src/Lean/Meta/Match/MVarRenaming.lean index 0dc7ee9ca7..366ad65e34 100644 --- a/src/Lean/Meta/Match/MVarRenaming.lean +++ b/src/Lean/Meta/Match/MVarRenaming.lean @@ -7,7 +7,7 @@ import Lean.Util.ReplaceExpr namespace Lean.Meta -/- A mapping from MVarId to MVarId -/ +/-- A mapping from MVarId to MVarId -/ structure MVarRenaming where map : MVarIdMap MVarId := {} diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index c3f9aa9378..02bdc4c5d1 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -392,7 +392,7 @@ private def hasRecursiveType (x : Expr) : MetaM Bool := do | some val => return val.isRec | _ => return false -/- Given `alt` s.t. the next pattern is an inaccessible pattern `e`, +/-- Given `alt` s.t. the next pattern is an inaccessible pattern `e`, try to normalize `e` into a constructor application. If it is not a constructor, throw an error. Otherwise, if it is a constructor application of `ctorName`, @@ -688,7 +688,7 @@ private def moveToFront (p : Problem) (i : Nat) : Problem := private partial def process (p : Problem) : StateRefT State MetaM Unit := search 0 where - /- If `p.vars` is empty, then we are done. Otherwise, we process `p.vars[0]`. -/ + /-- If `p.vars` is empty, then we are done. Otherwise, we process `p.vars[0]`. -/ tryToProcess (p : Problem) : StateRefT State MetaM Unit := withIncRecDepth do traceState p let isInductive ← isCurrVarInductive p @@ -727,7 +727,7 @@ where checkNextPatternTypes p throwNonSupported p - /- Return `true` if `type` does not depend on the first `i` elements in `xs` -/ + /-- Return `true` if `type` does not depend on the first `i` elements in `xs` -/ checkVarDeps (xs : List Expr) (i : Nat) (type : Expr) : MetaM Bool := do match i, xs with | 0, _ => return true @@ -787,7 +787,7 @@ register_builtin_option bootstrap.genMatcherCode : Bool := { builtin_initialize matcherExt : EnvExtension (Std.PHashMap (Expr × Bool) Name) ← registerEnvExtension (pure {}) -/- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`. +/-- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`. It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × Option (MatcherInfo → MetaM Unit)) := do trace[Meta.Match.debug] "{name} : {type} := {value}" @@ -985,7 +985,7 @@ def getMkMatcherInputInContext (matcherApp : MatcherApp) : MetaM MkMatcherInput return { matcherName, matchType, discrInfos := matcherInfo.discrInfos, lhss := lhss.toList } -/- This function is only used for testing purposes -/ +/-- This function is only used for testing purposes -/ def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput → MetaM α) : MetaM α := do let some matcherInfo ← getMatcherInfo? matcherName | throwError "not a matcher: {matcherName}" let matcherConst ← getConstInfo matcherName @@ -998,7 +998,7 @@ def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput → MetaM α) : end Match -/- Auxiliary function for MatcherApp.addArg -/ +/-- Auxiliary function for MatcherApp.addArg -/ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (i : Nat) : MetaM (Array Nat × Array Expr) := do if h : i < alts.size then let alt := alts.get ⟨i, h⟩ @@ -1016,7 +1016,7 @@ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts else return (altNumParams, alts) -/- Given +/-- Given - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - expression `e : B[discrs]`, Construct the term diff --git a/src/Lean/Meta/Match/MatchEqsExt.lean b/src/Lean/Meta/Match/MatchEqsExt.lean index 6484dbc3b7..0fa05e6c2c 100644 --- a/src/Lean/Meta/Match/MatchEqsExt.lean +++ b/src/Lean/Meta/Match/MatchEqsExt.lean @@ -27,7 +27,7 @@ builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ← def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit := modifyEnv fun env => matchEqnsExt.modifyState env fun s => { s with map := s.map.insert matchDeclName matchEqns } -/- +/-- Forward definition. We want to use `getEquationsFor` in the simplifier, `getEquationsFor` depends on `mkEquationsfor` which uses the simplifier. -/ @[extern "lean_get_match_equations_for"] diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index e3eb148cd2..71ecc0196a 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -59,7 +59,7 @@ where failure | _ => failure -/- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/ +/-- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/ private partial def getOffsetAux : Expr → Bool → OptionT MetaM (Expr × Nat) | e@(Expr.app _ a), top => do let f := e.getAppFn diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean index 8addf605b5..829255cec0 100644 --- a/src/Lean/Meta/PPGoal.lean +++ b/src/Lean/Meta/PPGoal.lean @@ -43,12 +43,12 @@ structure Context where abbrev M := ReaderT Context $ StateRefT State MetaM -/- Return true if `fvarId` is marked as an hidden inaccessible or inaccessible proposition -/ +/-- Return true if `fvarId` is marked as an hidden inaccessible or inaccessible proposition -/ def isMarked (fvarId : FVarId) : M Bool := do let s ← get return s.hiddenInaccessible.contains fvarId || s.hiddenInaccessibleProp.contains fvarId -/- If `fvarId` isMarked, then unmark it. -/ +/-- If `fvarId` isMarked, then unmark it. -/ def unmark (fvarId : FVarId) : M Unit := do modify fun s => { hiddenInaccessible := s.hiddenInaccessible.erase fvarId @@ -63,7 +63,7 @@ def moveToHiddeProp (fvarId : FVarId) : M Unit := do modified := true } -/- Return true if the given local declaration has a "visible dependency", that is, it contains +/-- Return true if the given local declaration has a "visible dependency", that is, it contains a free variable that is `hiddenInaccessible` Recall that hiddenInaccessibleProps are visible, only their names are hidden -/ @@ -71,14 +71,14 @@ def hasVisibleDep (localDecl : LocalDecl) : M Bool := do let s ← get findLocalDeclDependsOn localDecl (!s.hiddenInaccessible.contains ·) -/- Return true if the given local declaration has a "nonvisible dependency", that is, it contains +/-- Return true if the given local declaration has a "nonvisible dependency", that is, it contains a free variable that is `hiddenInaccessible` or `hiddenInaccessibleProp` -/ def hasInaccessibleNameDep (localDecl : LocalDecl) : M Bool := do let s ← get findLocalDeclDependsOn localDecl fun fvarId => s.hiddenInaccessible.contains fvarId || s.hiddenInaccessibleProp.contains fvarId -/- If `e` is visible, then any inaccessible in `e` marked as hidden should be unmarked. -/ +/-- If `e` is visible, then any inaccessible in `e` marked as hidden should be unmarked. -/ partial def visitVisibleExpr (e : Expr) : M Unit := do visit (← instantiateMVars e) |>.run where @@ -128,7 +128,7 @@ private def getInitialHiddenInaccessible (propOnly : Bool) : MetaM FVarIdSet := return r.insert localDecl.fvarId return r -/- +/-- If pp.inaccessibleNames == false, then collect two sets of `FVarId`s : `hiddenInaccessible` and `hiddenInaccessibleProp` 1- `hiddenInaccessible` contains `FVarId`s of free variables with inaccessible names that a) are not propositions or diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index bf790bf899..8b48ca96e6 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -107,7 +107,7 @@ private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Ex unless motive.isFVar && motiveArgs.all Expr.isFVar do throwError "invalid user defined recursor '{declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables" -/- Compute number of parameters for (user-defined) recursor. +/-- Compute number of parameters for (user-defined) recursor. We assume a parameter is anything that occurs before the motive -/ private partial def getNumParams (xs : Array Expr) (motive : Expr) (i : Nat) : Nat := if h : i < xs.size then diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 3cb1d16864..fe00dcdb12 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -190,7 +190,7 @@ def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr := let lemmaArgMask := lemmaArgMask ++ ctorFields.toArray.map some mkAppOptM lemmaName lemmaArgMask -/- SizeOf spec theorem for nested inductive types -/ +/-! # SizeOf spec theorem for nested inductive types -/ namespace SizeOfSpecNested structure Context where @@ -259,13 +259,14 @@ mutual let sizeOfBaseArgs := lhsArgs[:lhsArgs.size - info.numIndices - 1] let indicesMajor := lhsArgs[lhsArgs.size - info.numIndices - 1:] let sizeOfLevels := lhs.getAppFn.constLevels! - /- Auxiliary function for constructing an `_sizeOf_` for `ys`, - where `ys` are the indices + major. - Recall that if `info.name` is part of a mutually inductive declaration, then the resulting application - is not necessarily a `lhs.getAppFn` application. - The result is an application of one of the `(← read),sizeOfFns` functions. - We use this auxiliary function to builtin the motive of the recursor. -/ - let rec mkSizeOf (ys : Array Expr) : M Expr := do + let rec + /-- Auxiliary function for constructing an `_sizeOf_` for `ys`, + where `ys` are the indices + major. + Recall that if `info.name` is part of a mutually inductive declaration, then the resulting application + is not necessarily a `lhs.getAppFn` application. + The result is an application of one of the `(← read),sizeOfFns` functions. + We use this auxiliary function to builtin the motive of the recursor. -/ + mkSizeOf (ys : Array Expr) : M Expr := do for sizeOfFn in (← read).sizeOfFns do let candidate := mkAppN (mkAppN (mkConst sizeOfFn sizeOfLevels) sizeOfBaseArgs) ys if (← isTypeCorrect candidate) then diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index fb49e5c731..57d39fcdfc 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -60,7 +60,7 @@ def Waiter.isRoot : Waiter → Bool | Waiter.consumerNode _ => false | Waiter.root => true -/- +/-! In tabled resolution, we creating a mapping from goals (e.g., `Coe Nat ?x`) to answers and waiters. Waiters are consumer nodes that are waiting for answers for a particular node. @@ -141,7 +141,7 @@ partial def normExpr (e : Expr) : M Expr := do end MkTableKey -/- Remark: `mkTableKey` assumes `e` does not contain assigned metavariables. -/ +/-- Remark: `mkTableKey` assumes `e` does not contain assigned metavariables. -/ def mkTableKey [Monad m] [MonadMCtx m] (e : Expr) : m Expr := do let (r, s) := MkTableKey.normExpr e |>.run { mctx := (← getMCtx) } setMCtx s.mctx @@ -161,7 +161,7 @@ structure Context where maxResultSize : Nat maxHeartbeats : Nat -/- +/-- Remark: the SynthInstance.State is not really an extension of `Meta.State`. The field `postponed` is not needed, and the field `mctx` is misleading since `synthInstance` methods operate over different `MetavarContext`s simultaneously. @@ -259,7 +259,7 @@ def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : SynthM Expr := let mvarType ← instantiateMVars mvarType mkTableKey mvarType -/- See `getSubgoals` and `getSubgoalsAux` +/-- See `getSubgoals` and `getSubgoalsAux` We use the parameter `j` to reduce the number of `instantiate*` invocations. It is the same approach we use at `forallTelescope` and `lambdaTelescope`. @@ -597,7 +597,7 @@ def main (type : Expr) (maxResultSize : Nat) : MetaM (Option AbstractMVarsResult end SynthInstance -/- +/-! Type class parameters can be annotated with `outParam` annotations. Given `C a_1 ... a_n`, we replace `a_i` with a fresh metavariable `?m_i` IF @@ -656,7 +656,7 @@ private def preprocessOutParam (type : Expr) : MetaM Expr := | _ => return type -/- +/-! Remark: when `maxResultSize? == none`, the configuration option `synthInstance.maxResultSize` is used. Remark: we use a different option for controlling the maximum result size for coercions. -/ diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index b81c48b0d5..32d8dc69fd 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -10,7 +10,7 @@ import Lean.Meta.Tactic.Util namespace Lean.Meta -/- +/-- Compute the number of expected arguments and whether the result type is of the form (?m ...) where ?m is an unassigned metavariable. -/ diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index c4f3928078..d87d57864a 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -155,7 +155,7 @@ private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := d } | _ => pure none -/- +/-- We say the major premise has independent indices IF 1- its type is *not* an indexed inductive family, OR 2- its type is an indexed inductive family, but all indices are distinct free variables, and @@ -187,7 +187,7 @@ private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array Cases (pure s) | _ => pure s -/- +/-- Convert `s` into an array of `CasesSubgoal`, by attaching the corresponding constructor name, and adding the substitution `majorFVarId -> ctor_i us params fields` into each subgoal. -/ private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name) (majorFVarId : FVarId) (us : List Level) (params : Array Expr) diff --git a/src/Lean/Meta/Tactic/Cleanup.lean b/src/Lean/Meta/Tactic/Cleanup.lean index 1eb8d43478..4c7dc621ed 100644 --- a/src/Lean/Meta/Tactic/Cleanup.lean +++ b/src/Lean/Meta/Tactic/Cleanup.lean @@ -44,7 +44,7 @@ where modify fun (_, s) => (true, s.insert fvarId) addDeps fvarId - /- We include `p` in the used-set, if `p` is a proposition that contains a `x` that is in the used-set. -/ + /-- We include `p` in the used-set, if `p` is a proposition that contains a `x` that is in the used-set. -/ collectPropsStep : StateRefT (Bool × FVarIdSet) MetaM Unit := do let usedSet := (← get).2 for localDecl in (← getLCtx) do diff --git a/src/Lean/Meta/Tactic/Delta.lean b/src/Lean/Meta/Tactic/Delta.lean index c231d88ecf..afd7ba8216 100644 --- a/src/Lean/Meta/Tactic/Delta.lean +++ b/src/Lean/Meta/Tactic/Delta.lean @@ -16,7 +16,7 @@ def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr) else return none -/- Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions. -/ +/-- Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions. -/ def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr := Core.transform e fun e => do match (← delta? e p) with diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean index 9293126dd2..e502987efc 100644 --- a/src/Lean/Meta/Tactic/FVarSubst.lean +++ b/src/Lean/Meta/Tactic/FVarSubst.lean @@ -9,7 +9,7 @@ import Lean.LocalContext import Lean.Util.ReplaceExpr namespace Lean.Meta -/- +/-- Some tactics substitute hypotheses with expressions. We track these substitutions using `FVarSubst`. It is just a mapping from the original FVarId (internal) name @@ -29,7 +29,7 @@ def isEmpty (s : FVarSubst) : Bool := def contains (s : FVarSubst) (fvarId : FVarId) : Bool := s.map.contains fvarId -/- Add entry `fvarId |-> v` to `s` if `s` does not contain an entry for `fvarId`. -/ +/-- Add entry `fvarId |-> v` to `s` if `s` does not contain an entry for `fvarId`. -/ def insert (s : FVarSubst) (fvarId : FVarId) (v : Expr) : FVarSubst := if s.contains fvarId then s else diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index 0384c3663e..9a2bba2be4 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -123,7 +123,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt tryTheoremCore lhs xs bis val type e thm (eNumArgs - lhsNumArgs) discharge? else return none -/- +/-- Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise. -/ def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Name) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index a4922676a2..783dc02c54 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -333,7 +333,7 @@ def getSimpExtension? (attrName : Name) : IO (Option SimpExtension) := def getSimpTheorems : CoreM SimpTheorems := simpExtension.getTheorems -/- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/ +/-- Auxiliary method for adding a global declaration to a `SimpTheorems` datastructure. -/ def SimpTheorems.addConst (s : SimpTheorems) (declName : Name) (post : Bool := true) (inv : Bool := false) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do let s := { s with erased := s.erased.erase declName } let simpThms ← mkSimpTheoremsFromConst declName post inv prio @@ -356,12 +356,12 @@ private def preprocessProof (val : Expr) (inv : Bool) : MetaM (Array Expr) := do let ps ← preprocess val type inv (isGlobal := false) return ps.toArray.map fun (val, _) => val -/- Auxiliary method for creating simp theorems from a proof term `val`. -/ +/-- Auxiliary method for creating simp theorems from a proof term `val`. -/ def mkSimpTheorems (levelParams : Array Name) (proof : Expr) (post : Bool := true) (inv : Bool := false) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM (Array SimpTheorem) := withReducible do (← preprocessProof proof inv).mapM fun val => mkSimpTheoremCore val levelParams val post prio name? -/- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/ +/-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/ def SimpTheorems.add (s : SimpTheorems) (levelParams : Array Name) (proof : Expr) (inv : Bool := false) (post : Bool := true) (prio : Nat := eval_prio default) (name? : Option Name := none): MetaM SimpTheorems := do if proof.isConst then s.addConst proof.constName! post inv prio diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 64b5b923e5..3fd3ca6a9c 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -152,7 +152,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N let (discrEqs, mvarId') ← introNP mvarId' discrs.size return (discrs', discrEqs, mvarId') where - /- + /-- - `eqs` are free variables `h_eq : discr = discrVar`. `eqs.size == discrs.size` - `altEqs` are free variables of the form `h_altEq : discr = pattern`. `altEqs.size = numDiscrEqs ≤ discrs.size` This method executes `k altEqsNew subst` where diff --git a/src/Lean/Meta/Tactic/UnifyEq.lean b/src/Lean/Meta/Tactic/UnifyEq.lean index 7e6234b294..0dad193463 100644 --- a/src/Lean/Meta/Tactic/UnifyEq.lean +++ b/src/Lean/Meta/Tactic/UnifyEq.lean @@ -7,7 +7,7 @@ import Lean.Meta.Tactic.Injection namespace Lean.Meta -/- Convert heterogeneous equality into a homegeneous one -/ +/-- Convert heterogeneous equality into a homegeneous one -/ private def heqToEq' (mvarId : MVarId) (eqDecl : LocalDecl) : MetaM MVarId := do /- Convert heterogeneous equality into a homegeneous one -/ let prf ← mkEqOfHEq (mkFVar eqDecl.fvarId) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 273c5ed7e8..db2066943b 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -15,11 +15,11 @@ import Lean.Meta.Match.MatchPatternAttr namespace Lean.Meta -/- =========================== - Smart unfolding support - =========================== -/ +-- =========================== +/-! # Smart unfolding support -/ +-- =========================== -/- +/-- Forward declaration. It is defined in the module `src/Lean/Elab/PreDefinition/Structural/Eqns.lean`. It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structural.eqnInfoExt` to this module. @@ -54,9 +54,10 @@ def markSmartUnfoldingMatchAlt (e : Expr) : Expr := def smartUnfoldingMatchAlt? (e : Expr) : Option Expr := annotation? `sunfoldMatchAlt e -/- =========================== - Helper methods - =========================== -/ +-- =========================== +/-! # Helper methods -/ +-- =========================== + def isAuxDef (constName : Name) : MetaM Bool := do let env ← getEnv return isAuxRecursor env constName || isNoConfusion env constName @@ -68,9 +69,9 @@ def isAuxDef (constName : Name) : MetaM Bool := do k cinfo lvls | _ => failK () -/- =========================== - Helper functions for reducing recursors - =========================== -/ +-- =========================== +/-! # Helper functions for reducing recursors -/ +-- =========================== private def getFirstCtor (d : Name) : MetaM (Option Name) := do let some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) ← getConstNoEx? d | pure none @@ -195,9 +196,9 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A else failK () -/- =========================== - Helper functions for reducing Quot.lift and Quot.ind - =========================== -/ +-- =========================== +/-! # Helper functions for reducing Quot.lift and Quot.ind -/ +-- =========================== /-- Auxiliary function for reducing `Quot.lift` and `Quot.ind` applications. -/ private def reduceQuotRec (recVal : QuotVal) (recLvls : List Level) (recArgs : Array Expr) (failK : Unit → MetaM α) (successK : Expr → MetaM α) : MetaM α := @@ -220,9 +221,9 @@ private def reduceQuotRec (recVal : QuotVal) (recLvls : List Level) (recArgs : | QuotKind.ind => process 4 3 | _ => failK () -/- =========================== - Helper function for extracting "stuck term" - =========================== -/ +-- =========================== +/-! # Helper function for extracting "stuck term" -/ +-- =========================== mutual private partial def isRecStuck? (recVal : RecursorVal) (recArgs : Array Expr) : MetaM (Option MVarId) := @@ -275,9 +276,9 @@ mutual | _ => return none end -/- =========================== - Weak Head Normal Form auxiliary combinators - =========================== -/ +-- =========================== +/-! # Weak Head Normal Form auxiliary combinators -/ +-- =========================== /-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/ @[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index cd76382a57..9299d79c33 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -8,7 +8,7 @@ import Lean.LocalContext namespace Lean -/- +/-! The metavariable context stores metavariable declarations and their assignments. It is used in the elaborator, tactic framework, unifier (aka `isDefEq`), and type class resolution (TC). First, we list all @@ -319,7 +319,7 @@ def getDelayedMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Opt markUsedAssignment return result? -/- Given a sequence of delayed assignments +/-- Given a sequence of delayed assignments ``` mvarId₁ := mvarId₂ ...; ... @@ -432,7 +432,7 @@ def assignExprMVar [MonadMCtx m] (mvarId : MVarId) (val : Expr) : m Unit := def assignDelayedMVar [MonadMCtx m] (mvarId : MVarId) (fvars : Array Expr) (mvarIdPending : MVarId) : m Unit := modifyMCtx fun m => { m with dAssignment := m.dAssignment.insert mvarId { fvars, mvarIdPending }, usedAssignment := true } -/- +/-- Notes on artificial eta-expanded terms due to metavariables. We try avoid synthetic terms such as `((fun x y => t) a b)` in the output produced by the elaborator. This kind of term may be generated when instantiating metavariable assignments. @@ -711,7 +711,7 @@ instance : Inhabited MetavarContext := ⟨{}⟩ @[export lean_mk_metavar_ctx] def mkMetavarContext : Unit → MetavarContext := fun _ => {} -/- Low level API for adding/declaring metavariable declarations. +/-- Low level API for adding/declaring metavariable declarations. It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`. It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/ def addExprMVarDecl (mctx : MetavarContext) @@ -739,7 +739,7 @@ def addExprMVarDeclExp (mctx : MetavarContext) (mvarId : MVarId) (userName : Nam (type : Expr) (kind : MetavarKind) : MetavarContext := addExprMVarDecl mctx mvarId userName lctx localInstances type kind -/- Low level API for adding/declaring universe level metavariable declarations. +/-- Low level API for adding/declaring universe level metavariable declarations. It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`. It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique". -/ def addLevelMVarDecl (mctx : MetavarContext) (mvarId : MVarId) : MetavarContext := @@ -776,7 +776,7 @@ def setMVarUserNameTemporarily (mctx : MetavarContext) (mvarId : MVarId) (userNa let decl := mctx.getDecl mvarId { mctx with decls := mctx.decls.insert mvarId { decl with userName := userName } } -/- Update the type of the given metavariable. This function assumes the new type is +/-- Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one -/ def setMVarType (mctx : MetavarContext) (mvarId : MVarId) (type : Expr) : MetavarContext := let decl := mctx.getDecl mvarId diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean index 46000614dd..3048be1280 100644 --- a/src/Lean/Modifiers.lean +++ b/src/Lean/Modifiers.lean @@ -17,7 +17,7 @@ def addProtected (env : Environment) (n : Name) : Environment := def isProtected (env : Environment) (n : Name) : Bool := protectedExt.isTagged env n -/- Private name support. +/-! # Private name support. Suppose the user marks as declaration `n` as private. Then, we create the name: `_private..0 ++ n`. diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 7837c6ec34..fce70f9271 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -138,7 +138,7 @@ def addDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] [MonadLog m] private def supportedRecursors := #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn] -/- This is a temporary workaround for generating better error messages for the compiler. It can be deleted after we +/-- This is a temporary workaround for generating better error messages for the compiler. It can be deleted after we rewrite the remaining parts of the compiler in Lean. -/ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Declaration) : m Unit := do let env ← getEnv diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean index 69785a09dc..7d037d3325 100644 --- a/src/Lean/Parser/Attr.lean +++ b/src/Lean/Parser/Attr.lean @@ -33,11 +33,11 @@ end Priority namespace Attr @[builtinAttrParser] def simple := leading_parser ident >> optional (priorityParser <|> ident) -/- Remark, We can't use `simple` for `class`, `instance`, `export`, and `macro` because they are keywords. -/ +/- Remark, We can't use `simple` for `class`, `instance`, `export`, and `macro` because they are keywords. -/ @[builtinAttrParser] def «macro» := leading_parser "macro " >> ident @[builtinAttrParser] def «export» := leading_parser "export " >> ident -/- We don't use `simple` for recursor because the argument is not a priority-/ +/- We don't use `simple` for recursor because the argument is not a priority -/ @[builtinAttrParser] def recursor := leading_parser nonReservedSymbol "recursor " >> numLit @[builtinAttrParser] def «class» := leading_parser "class" @[builtinAttrParser] def «instance» := leading_parser "instance" >> optional priorityParser diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index d595ee7ed4..26a491ca80 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -74,11 +74,11 @@ abbrev mkAtom (info : SourceInfo) (val : String) : Syntax := abbrev mkIdent (info : SourceInfo) (rawVal : Substring) (val : Name) : Syntax := Syntax.ident info rawVal val [] -/- Return character after position `pos` -/ +/-- Return character after position `pos` -/ def getNext (input : String) (pos : String.Pos) : Char := input.get (input.next pos) -/- Maximal (and function application) precedence. +/-- Maximal (and function application) precedence. In the standard lean language, no parser has precedence higher than `maxPrec`. Note that nothing prevents users from using a higher precedence, but we strongly @@ -109,7 +109,7 @@ abbrev SyntaxNodeKindSet := Std.PersistentHashMap SyntaxNodeKind Unit def SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet := Std.PersistentHashMap.insert s k () -/- +/-- Input string and related data. Recall that the `FileMap` is a helper structure for mapping `String.Pos` in the input string to line/column information. -/ structure InputContext where @@ -410,14 +410,14 @@ def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s => match s with | ⟨stack, lhsPrec, _, cache, _⟩ => ⟨stack.push Syntax.missing, lhsPrec, pos, cache, some { unexpected := msg }⟩ -/- Generate an error at the position saved with the `withPosition` combinator. +/-- Generate an error at the position saved with the `withPosition` combinator. If `delta == true`, then it reports at saved position+1. This useful to make sure a parser consumed at least one character. -/ @[inline] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := { fn := errorAtSavedPosFn msg delta } -/- Succeeds if `c.prec <= prec` -/ +/-- Succeeds if `c.prec <= prec` -/ def checkPrecFn (prec : Nat) : ParserFn := fun c s => if c.prec <= prec then s else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term" @@ -427,7 +427,7 @@ def checkPrecFn (prec : Nat) : ParserFn := fun c s => fn := checkPrecFn prec } -/- Succeeds if `c.lhsPrec >= prec` -/ +/-- Succeeds if `c.lhsPrec >= prec` -/ def checkLhsPrecFn (prec : Nat) : ParserFn := fun _ s => if s.lhsPrec >= prec then s else s.mkUnexpectedError "unexpected token at this precedence level; consider parenthesizing the term" @@ -680,7 +680,7 @@ def sepBy1Fn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) : ParserF fn := sepBy1Fn allowTrailingSep p.fn sep.fn } -/- Apply `f` to the syntax object produced by `p` -/ +/-- Apply `f` to the syntax object produced by `p` -/ def withResultOfFn (p : ParserFn) (f : Syntax → Syntax) : ParserFn := fun c s => let s := p c s if s.hasError then s @@ -745,7 +745,7 @@ partial def finishCommentBlock (nesting : Nat) : ParserFn := fun c s => where eoi s := s.mkUnexpectedError "unterminated comment" -/- Consume whitespace and comments -/ +/-- Consume whitespace and comments -/ partial def whitespace : ParserFn := fun c s => let input := c.input let i := s.pos @@ -1107,7 +1107,7 @@ def peekToken (c : ParserContext) (s : ParserState) : ParserState × Except Pars else peekTokenAux c s -/- Treat keywords as identifiers. -/ +/-- Treat keywords as identifiers. -/ def rawIdentFn : ParserFn := fun c s => let input := c.input let i := s.pos @@ -1561,26 +1561,12 @@ structure PrattParsingTables where instance : Inhabited PrattParsingTables := ⟨{}⟩ -/- +/-- The type `leadingIdentBehavior` specifies how the parsing table lookup function behaves for identifiers. The function `prattParser` uses two tables `leadingTable` and `trailingTable`. They map tokens to parsers. - - `LeadingIdentBehavior.default`: if the leading token - is an identifier, then `prattParser` just executes the parsers - associated with the auxiliary token "ident". - - - `LeadingIdentBehavior.symbol`: if the leading token is - an identifier ``, and there are parsers `P` associated with - the toek ``, then it executes `P`. Otherwise, it executes - only the parsers associated with the auxiliary token "ident". - - - `LeadingIdentBehavior.both`: if the leading token - an identifier ``, the it executes the parsers associated - with token `` and parsers associated with the auxiliary - token "ident". - We use `LeadingIdentBehavior.symbol` and `LeadingIdentBehavior.both` and `nonReservedSymbol` parser to implement the `tactic` parsers. The idea is to avoid creating a reserved symbol for each @@ -1588,11 +1574,21 @@ instance : Inhabited PrattParsingTables := ⟨{}⟩ may still use these symbols as identifiers (e.g., naming a function). -/ - inductive LeadingIdentBehavior where - | default - | symbol - | both + | /-- `LeadingIdentBehavior.default`: if the leading token + is an identifier, then `prattParser` just executes the parsers + associated with the auxiliary token "ident". -/ + default + | /-- `LeadingIdentBehavior.symbol`: if the leading token is + an identifier ``, and there are parsers `P` associated with + the toek ``, then it executes `P`. Otherwise, it executes + only the parsers associated with the auxiliary token "ident". -/ + symbol + | /-- `LeadingIdentBehavior.both`: if the leading token + an identifier ``, the it executes the parsers associated + with token `` and parsers associated with the auxiliary + token "ident". -/ + both deriving Inhabited, BEq, Repr /-- @@ -1661,9 +1657,9 @@ def categoryParser (catName : Name) (prec : Nat) : Parser := { @[inline] def termParser (prec : Nat := 0) : Parser := categoryParser `term prec -/- ============== -/ -/- Antiquotations -/ -/- ============== -/ +-- ================== +/-! # Antiquotations -/ +-- ================== /-- Fail if previous token is immediately followed by ':'. -/ def checkNoImmediateColon : Parser := { @@ -1796,9 +1792,9 @@ def withAntiquotSpliceAndSuffix (kind : SyntaxNodeKind) (p suffix : Parser) := def nodeWithAntiquot (name : String) (kind : SyntaxNodeKind) (p : Parser) (anonymous := false) : Parser := withAntiquot (mkAntiquot name kind anonymous) $ node kind p -/- ===================== -/ -/- End of Antiquotations -/ -/- ===================== -/ +-- ========================= +/-! # End of Antiquotations -/ +-- ========================= def sepByElemParser (p : Parser) (sep : String) : Parser := withAntiquotSpliceAndSuffix `sepBy p (symbol (sep.trim ++ "*")) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 54c4bb73d7..4d41c87f68 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -137,7 +137,7 @@ def initializeKeyword := leading_parser "initialize " <|> "builtin_initialize " @[builtinCommandParser] def «in» := trailing_parser withOpen (" in " >> commandParser) -/- +/-- This is an auxiliary command for generation constructor injectivity theorems for inductive types defined at `Prelude.lean`. It is meant for bootstrapping purposes only. -/ @[builtinCommandParser] def genInjectiveTheorems := leading_parser "gen_injective_theorems% " >> ident diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 3975b6b416..fe662ee6fe 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -50,7 +50,7 @@ def letIdDeclNoBinders := node `Lean.Parser.Term.letIdDecl $ atomic (ident >> pu @[builtinDoElemParser] def doReassign := leading_parser notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl) @[builtinDoElemParser] def doReassignArrow := leading_parser notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl) @[builtinDoElemParser] def doHave := leading_parser "have " >> Term.haveDecl -/- +/-- In `do` blocks, we support `if` without an `else`. Thus, we use indentation to prevent examples such as ``` if c_1 then @@ -108,7 +108,7 @@ def doFinally := leading_parser "finally " >> doSeq @[builtinDoElemParser] def doDbgTrace := leading_parser:leadPrec "dbg_trace " >> ((interpolatedStr termParser) <|> termParser) @[builtinDoElemParser] def doAssert := leading_parser:leadPrec "assert! " >> termParser -/- +/-- We use `notFollowedBy` to avoid counterintuitive behavior. For example, the `if`-term parser diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 3edef816d1..5472544f43 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -164,7 +164,7 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State := | Except.ok categories => { s with categories := categories } | _ => unreachable! -/- Parser aliases for making `ParserDescr` extensible -/ +/-- Parser aliases for making `ParserDescr` extensible -/ inductive AliasValue (α : Type) where | const (p : α) | unary (p : α → α) @@ -294,7 +294,7 @@ def mkParserOfConstant (categories : ParserCategories) (constName : Name) : Impo mkParserOfConstantAux constName (compileParserDescr categories) structure ParserAttributeHook where - /- Called after a parser attribute is applied to a declaration. -/ + /-- Called after a parser attribute is applied to a declaration. -/ postAdd (catName : Name) (declName : Name) (builtin : Bool) : AttrM Unit builtin_initialize parserAttributeHooks : IO.Ref (List ParserAttributeHook) ← IO.mkRef {} @@ -451,7 +451,7 @@ def mkParserContext (ictx : InputContext) (pmctx : ParserModuleContext) : Parser def mkParserState (input : String) : ParserState := { cache := initCacheForInput input } -/- convenience function for testing -/ +/-- convenience function for testing -/ def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "") : Except String Syntax := let c := mkParserContext (mkInputContext input fileName) { env := env, options := {} } let s := mkParserState input @@ -499,7 +499,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name) declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges]) runParserAttributeHooks catName declName (builtin := true) -/- +/-- The parsing tables for builtin parsers are "stored" in the extracted source code. -/ def registerBuiltinParserAttribute (attrName : Name) (catName : Name) (behavior := LeadingIdentBehavior.default) : IO Unit := do @@ -539,7 +539,7 @@ def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl whe add declName stx attrKind := ParserAttribute.add attrName catName declName stx attrKind applicationTime := AttributeApplicationTime.afterCompilation -/- A builtin parser attribute that can be extended by users. -/ +/-- A builtin parser attribute that can be extended by users. -/ def registerBuiltinDynamicParserAttribute (attrName : Name) (catName : Name) : IO Unit := do registerBuiltinAttribute (mkParserAttributeImpl attrName catName) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 29ff0373ce..3154db96f3 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -38,7 +38,7 @@ def tacticSeqBracketed : Parser := def tacticSeq := leading_parser tacticSeqBracketed <|> tacticSeq1Indented -/- Raw sequence for quotation and grouping -/ +/-- Raw sequence for quotation and grouping -/ def seq1 := node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" (allowTrailingSep := true) @@ -49,7 +49,7 @@ def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone namespace Term -/- Built-in parsers -/ +/-! # Built-in parsers -/ @[builtinTermParser] def byTactic := leading_parser:leadPrec ppAllowUngrouped >> "by " >> Tactic.tacticSeq @@ -114,7 +114,7 @@ def instBinder := ppGroup $ leading_parser "[" >> optIdent >> termParser >> "]" def bracketedBinder (requireType := false) := withAntiquot (mkAntiquot "bracketedBinder" `Lean.Parser.Term.bracketedBinder (isPseudoKind := true)) <| explicitBinder requireType <|> strictImplicitBinder requireType <|> implicitBinder requireType <|> instBinder -/- +/-- It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case. `{α} → α → α` would be short for `{α : Type} → α → α` Here is the encoding: @@ -178,11 +178,11 @@ def withAnonymousAntiquot := leading_parser atomic ("(" >> nonReservedSymbol "wi @[builtinTermParser] def doubleQuotedName := leading_parser "`" >> checkNoWsBefore >> rawCh '`' (trailingWs := false) >> ident def letIdBinder := withAntiquot (mkAntiquot "letIdBinder" `Lean.Parser.Term.letIdBinder (isPseudoKind := true)) (binderIdent <|> bracketedBinder) -/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/ +/-- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/ def letIdLhs : Parser := ident >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >> many (ppSpace >> letIdBinder) >> optType def letIdDecl := leading_parser (withAnonymousAntiquot := false) atomic (letIdLhs >> " := ") >> termParser def letPatDecl := leading_parser (withAnonymousAntiquot := false) atomic (termParser >> pushNone >> optType >> " := ") >> termParser -/- +/-- Remark: the following `(" := " <|> matchAlts)` is a hack we use to produce a better error message at `letDecl`. Consider this following example ``` @@ -206,7 +206,7 @@ def letDecl := leading_parser (withAnonymousAntiquot := false) notFollowedBy instance : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) where coe stx := ⟨stx⟩ --- like `let_fun` but with optional name +/-- like `let_fun` but with optional name -/ def haveIdLhs := optional (ident >> many (ppSpace >> letIdBinder)) >> optType def haveIdDecl := leading_parser (withAnonymousAntiquot := false) atomic (haveIdLhs >> " := ") >> termParser def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false) haveIdLhs >> matchAlts diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean index 9f2f866cea..0814a01ad8 100644 --- a/src/Lean/ProjFns.lean +++ b/src/Lean/ProjFns.lean @@ -7,7 +7,7 @@ import Lean.Environment namespace Lean -/- Given a structure `S`, Lean automatically creates an auxiliary definition (projection function) +/-- Given a structure `S`, Lean automatically creates an auxiliary definition (projection function) for each field. This structure caches information about these auxiliary definitions. -/ structure ProjectionFunctionInfo where ctorName : Name -- Constructor associated with the auxiliary projection function. diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 624eb3ed7d..abdbe3e026 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -29,14 +29,14 @@ builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry Alia addImportedFn := fun es => mkStateFromImportedEntries addAliasEntry {} es |>.switch } -/- Add alias `a` for `e` -/ +/-- Add alias `a` for `e` -/ @[export lean_add_alias] def addAlias (env : Environment) (a : Name) (e : Name) : Environment := aliasExtension.addEntry env (a, e) def getAliasState (env : Environment) : AliasState := aliasExtension.getState env -/- +/-- Retrieve aliases for `a`. If `skipProtected` is `true`, then the resulting list only includes declarations that are not marked as `proctected`. -/ @@ -53,10 +53,10 @@ def getAliases (env : Environment) (a : Name) (skipProtected : Bool) : List Name def getRevAliases (env : Environment) (e : Name) : List Name := (aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) [] -/- Global name resolution -/ +/-! # Global name resolution -/ namespace ResolveName -/- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/ +/-- Check whether `ns ++ id` is a valid namepace name and/or there are aliases names `ns ++ id`. -/ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name := let resolvedId := ns ++ id -- We ignore protected aliases if `id` is atomic. @@ -69,7 +69,7 @@ private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : L if env.contains resolvedIdPrv then resolvedIdPrv :: resolvedIds else resolvedIds -/- Check surrounding namespaces -/ +/-- Check surrounding namespaces -/ private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name | ns@(.str p _) => match resolveQualifiedName env ns id with @@ -77,7 +77,7 @@ private def resolveUsingNamespace (env : Environment) (id : Name) : Name → Lis | resolvedIds => resolvedIds | _ => [] -/- Check exact name -/ +/-- Check exact name -/ private def resolveExact (env : Environment) (id : Name) : Option Name := if id.isAtomic then none else @@ -90,7 +90,7 @@ private def resolveExact (env : Environment) (id : Name) : Option Name := if env.contains resolvedIdPrv then some resolvedIdPrv else none -/- Check `OpenDecl`s -/ +/-- Check `OpenDecl`s -/ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name | [], resolvedIds => resolvedIds | OpenDecl.simple ns exs :: openDecls, resolvedIds => @@ -138,7 +138,7 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl | _ => [] loop extractionResult.name [] -/- Namespace resolution -/ +/-! # Namespace resolution -/ def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name | .anonymous => if env.isNamespace n then some n else none diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 658ea76972..58359cd3ad 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -166,7 +166,7 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : else return none -/- +/-- Truncate the given identifier and make sure it has length `≤ newLength`. This function assumes `id` does not contain `Name.num` constructors. -/ diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 9ad6ca5337..29170d366c 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -65,7 +65,8 @@ structure WorkerContext where initParams : InitializeParams clientHasWidgets : Bool -/- Asynchronous snapshot elaboration. -/ +/-! # Asynchronous snapshot elaboration -/ + section Elab structure AsyncElabState where snaps : Array Snapshot diff --git a/src/Lean/Server/FileWorker/Utils.lean b/src/Lean/Server/FileWorker/Utils.lean index ef5996e918..e065bd1392 100644 --- a/src/Lean/Server/FileWorker/Utils.lean +++ b/src/Lean/Server/FileWorker/Utils.lean @@ -50,7 +50,7 @@ and parser state after each command so that edits can be applied without recompiling code appearing earlier in the file. -/ structure EditableDocument where meta : DocumentMeta - /- State snapshots after header and each command. -/ + /-- State snapshots after header and each command. -/ cmdSnaps : AsyncList ElabTaskError Snapshot cancelTk : CancelToken diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 099fe6d1c0..dc24e93183 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -244,7 +244,7 @@ structure GoalsAtResult where -- for overlapping goals, only keep those of the highest reported priority priority : Nat -/- +/-- Try to retrieve `TacticInfo` for `hoverPos`. We retrieve all `TacticInfo` nodes s.t. `hoverPos` is inside the node's range plus trailing whitespace. We usually prefer the innermost such nodes so that for composite tactics such as `induction`, we show the nested proofs' states. diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index d3b86b3395..078f51fee0 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -13,7 +13,7 @@ import Lean.Server.Utils import Lean.Server.InfoUtils import Lean.Server.Snapshots -/- Representing collected and deduplicated definitions and usages -/ +/-! # Representing collected and deduplicated definitions and usages -/ namespace Lean.Server open Lsp Lean.Elab Std @@ -127,7 +127,7 @@ def load (path : System.FilePath) : IO Ilean := do | Except.error msg => throwServerError s!"Failed to load ilean at {path}: {msg}" end Ilean -/- Collecting and deduplicating definitions and usages -/ +/-! # Collecting and deduplicating definitions and usages -/ def identOf : Info → Option (RefIdent × Bool) | Info.ofTermInfo ti => match ti.expr with @@ -220,7 +220,7 @@ def findModuleRefs (text : FileMap) (trees : Array InfoTree) (localVars : Bool : | _ => true refs.foldl (init := HashMap.empty) fun m ref => m.addRef ref -/- Collecting and maintaining reference info from different sources -/ +/-! # Collecting and maintaining reference info from different sources -/ structure References where /-- References loaded from ilean files -/ diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index cd034d4fc5..8a2e03022f 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -121,7 +121,7 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool) end RequestM -/- The global request handlers table. -/ +/-! # The global request handlers table -/ section HandlerTable open Lsp diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 9831d6d31c..73d5e5f243 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -83,21 +83,21 @@ section Utils /-- Events that worker-specific tasks signal to the main thread. -/ inductive WorkerEvent where - /- A synthetic event signalling that the grouped edits should be processed. -/ - | processGroupedEdits + | /-- A synthetic event signalling that the grouped edits should be processed. -/ + processGroupedEdits | terminated | crashed (e : IO.Error) | ioError (e : IO.Error) inductive WorkerState where - /- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker - and when reading a request reply. - In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. - Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored. - Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded - to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file - worker arrives. -/ - | crashed (queuedMsgs : Array JsonRpc.Message) + | /-- The watchdog can detect a crashed file worker in two places: When trying to send a message to the file worker + and when reading a request reply. + In the latter case, the forwarding task terminates and delegates a `crashed` event to the main task. + Then, in both cases, the file worker has its state set to `crashed` and requests that are in-flight are errored. + Upon receiving the next packet for that file worker, the file worker is restarted and the packet is forwarded + to it. If the crash was detected while writing a packet, we queue that packet until the next packet for the file + worker arrives. -/ + crashed (queuedMsgs : Array JsonRpc.Message) | running abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message compare diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 24fc5ba7c2..26ff877bdb 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -12,7 +12,7 @@ def SourceInfo.updateTrailing (trailing : Substring) : SourceInfo → SourceInfo | SourceInfo.original leading pos _ endPos => SourceInfo.original leading pos trailing endPos | info => info -/- Syntax AST -/ +/-! # Syntax AST -/ inductive IsNode : Syntax → Prop where | mk (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : IsNode (Syntax.node info kind args) @@ -123,7 +123,7 @@ private def updateInfo : SourceInfo → String.Pos → String.Pos → SourceInfo private def chooseNiceTrailStop (trail : Substring) : String.Pos := trail.startPos + trail.posOf '\n' -/- Remark: the State `String.Pos` is the `SourceInfo.trailing.stopPos` of the previous token, +/-- Remark: the State `String.Pos` is the `SourceInfo.trailing.stopPos` of the previous token, or the beginning of the String. -/ @[inline] private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax) diff --git a/src/Lean/Util/ForEachExpr.lean b/src/Lean/Util/ForEachExpr.lean index 43ba068054..d8902efe40 100644 --- a/src/Lean/Util/ForEachExpr.lean +++ b/src/Lean/Util/ForEachExpr.lean @@ -7,7 +7,7 @@ import Lean.Expr import Lean.Util.MonadCache namespace Lean -/- +/-! Remark: we cannot use the caching trick used at `FindExpr` and `ReplaceExpr` because they may visit the same expression multiple times if they are stored in different memory addresses. Note that the following code is parametric in a monad `m`. diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean index b5de260964..93884e7534 100644 --- a/src/Lean/Util/SCC.lean +++ b/src/Lean/Util/SCC.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ import Std.Data.HashMap namespace Lean.SCC -/- +/-! Very simple implementation of Tarjan's SCC algorithm. Performance is not a goal here since we use this module to compiler mutually recursive definitions, where each function diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 74265f3b99..2de55833e2 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -53,14 +53,14 @@ private def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPCo } private inductive EmbedFmt - /- Tags denote `Info` objects. -/ - | expr (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) + | /-- Tags denote `Info` objects. -/ + expr (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId) - /- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow - the user to expand sub-traces interactively. -/ - | lazyTrace (nCtx : NamingContext) (ctx? : Option MessageDataContext) (cls : Name) (m : MessageData) - /- Ignore any tags in this subtree. -/ - | ignoreTags + | /-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow + the user to expand sub-traces interactively. -/ + lazyTrace (nCtx : NamingContext) (ctx? : Option MessageDataContext) (cls : Name) (m : MessageData) + | /-- Ignore any tags in this subtree. -/ + ignoreTags deriving Inhabited private abbrev MsgFmtM := StateT (Array EmbedFmt) IO diff --git a/src/Std/Data/AssocList.lean b/src/Std/Data/AssocList.lean index 0a829930e2..a0cd18f01e 100644 --- a/src/Std/Data/AssocList.lean +++ b/src/Std/Data/AssocList.lean @@ -6,7 +6,7 @@ Author: Leonardo de Moura universe u v w w' namespace Std -/- List-like type to avoid extra level of indirection -/ +/-- List-like type to avoid extra level of indirection -/ inductive AssocList (α : Type u) (β : Type v) where | nil : AssocList α β | cons (key : α) (value : β) (tail : AssocList α β) : AssocList α β diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean index 791033adc0..e062dcd6a5 100644 --- a/src/Std/Data/BinomialHeap.lean +++ b/src/Std/Data/BinomialHeap.lean @@ -173,65 +173,65 @@ variable {α : Type u} {le : α → α → Bool} @[inline] def isEmpty : BinomialHeap α le → Bool | ⟨b, _⟩ => BinomialHeapImp.isEmpty b -/- O(1) -/ +/-- O(1) -/ @[inline] def singleton (a : α) : BinomialHeap α le := ⟨BinomialHeapImp.singleton a, WellFormed.singleton a⟩ -/- O(log n) -/ +/-- O(log n) -/ @[inline] def merge : BinomialHeap α le → BinomialHeap α le → BinomialHeap α le | ⟨b₁, h₁⟩, ⟨b₂, h₂⟩ => ⟨BinomialHeapImp.merge le b₁ b₂, WellFormed.merge b₁ b₂ h₁ h₂⟩ -/- O(log n) -/ +/-- O(log n) -/ @[inline] def insert (a : α) (h : BinomialHeap α le) : BinomialHeap α le := merge (singleton a) h -/- O(n log n) -/ +/-- O(n log n) -/ def ofList (le : α → α → Bool) (as : List α) : BinomialHeap α le := as.foldl (flip insert) empty -/- O(n log n) -/ +/-- O(n log n) -/ def ofArray (le : α → α → Bool) (as : Array α) : BinomialHeap α le := as.foldl (flip insert) empty -/- O(log n) -/ +/-- O(log n) -/ @[inline] def deleteMin : BinomialHeap α le → Option (α × BinomialHeap α le) | ⟨b, h⟩ => match eq: BinomialHeapImp.deleteMin le b with | none => none | some (a, tl) => some (a, ⟨tl, WellFormed.deleteMin a b tl h eq⟩) -/- O(log n) -/ +/-- O(log n) -/ @[inline] def head [Inhabited α] : BinomialHeap α le → α | ⟨b, _⟩ => BinomialHeapImp.head le b -/- O(log n) -/ +/-- O(log n) -/ @[inline] def head? : BinomialHeap α le → Option α | ⟨b, _⟩ => BinomialHeapImp.head? le b -/- O(log n) -/ +/-- O(log n) -/ @[inline] def tail? : BinomialHeap α le → Option (BinomialHeap α le) | ⟨b, h⟩ => match eq: BinomialHeapImp.tail? le b with | none => none | some tl => some ⟨tl, WellFormed.tail? b tl h eq⟩ -/- O(log n) -/ +/-- O(log n) -/ @[inline] def tail : BinomialHeap α le → BinomialHeap α le | ⟨b, h⟩ => ⟨BinomialHeapImp.tail le b, WellFormed.tail b h⟩ -/- O(n log n) -/ +/-- O(n log n) -/ @[inline] def toList : BinomialHeap α le → List α | ⟨b, _⟩ => BinomialHeapImp.toList le b -/- O(n log n) -/ +/-- O(n log n) -/ @[inline] def toArray : BinomialHeap α le → Array α | ⟨b, _⟩ => BinomialHeapImp.toArray le b -/- O(n) -/ +/-- O(n) -/ @[inline] def toListUnordered : BinomialHeap α le → List α | ⟨b, _⟩ => BinomialHeapImp.toListUnordered b -/- O(n) -/ +/-- O(n) -/ @[inline] def toArrayUnordered : BinomialHeap α le → Array α | ⟨b, _⟩ => BinomialHeapImp.toArrayUnordered b diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean index d10a871793..de4dec84af 100644 --- a/src/Std/ShareCommon.lean +++ b/src/Std/ShareCommon.lean @@ -85,7 +85,7 @@ unsafe def ObjectPersistentSet.find? (s : ObjectPersistentSet) (o : Object) : Op unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : ObjectPersistentSet := @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o -/- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/ +/-- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/ opaque StatePointed : NonemptyType abbrev State : Type u := StatePointed.type @[extern "lean_sharecommon_mk_state"] @@ -93,7 +93,7 @@ opaque mkState : Unit → State := fun _ => Classical.choice StatePointed.proper def State.empty : State := mkState () instance State.inhabited : Inhabited State := ⟨State.empty⟩ -/- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/ +/-- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/ opaque PersistentStatePointed : NonemptyType abbrev PersistentState : Type u := PersistentStatePointed.type @[extern "lean_sharecommon_mk_pstate"] diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index d7c0ffa2a3..1307149e12 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -21,9 +21,18 @@ "kind": 7, "detail": "(Type u₁ → Type u₂) →\n (ρ : Type u) → (α : outParam (Type v)) → outParam (Membership α ρ) → Type (max (max (max u (u₁ + 1)) u₂) v)"}, - {"label": "ForInStep", "kind": 22, "detail": "Type u → Type u"}, + {"label": "ForInStep", + "kind": 22, + "documentation": + {"value": "Auxiliary type used to compile `for x in xs` notation. ", + "kind": "markdown"}, + "detail": "Type u → Type u"}, {"label": "ForM", "kind": 7, + "documentation": + {"value": + "Typeclass for the polymorphic `forM` operation described in the \"do unchained\" paper.\nRemark:\n- `γ` is a \"container\" type of elements of type `α`.\n- `α` is treated as an output parameter by the typeclass resolution procedure.\n That is, it tries to find an instance using only `m` and `γ`.\n", + "kind": "markdown"}, "detail": "(Type u → Type v) → Type w₁ → outParam (Type w₂) → Type (max (max (max (u + 1) v) w₁) w₂)"}, {"label": "Function", "kind": 9, "detail": "namespace"},