Merge pull request #294 from HEPLean/Docs

refactor: Docs and note

HepLean.lean

@@ -117,6 +117,8 @@ import HepLean.Meta.Notes.Basic
 import HepLean.Meta.Notes.HTMLNote
 import HepLean.Meta.Notes.NoteFile
 import HepLean.Meta.Notes.ToHTML
+import HepLean.Meta.Remark.Basic
+import HepLean.Meta.Remark.Properties
 import HepLean.Meta.TODO.Basic
 import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic

HepLean/Meta/Basic.lean

@@ -123,6 +123,14 @@ def Name.hasDocString (c : Name) : MetaM Bool := do
   | some _ => pure true
   | none => pure false
 
+/-- The doc string from a name. -/
+def Name.getDocString (c : Name) : MetaM String := do
+  let env ← getEnv
+  let doc ← Lean.findDocString? env c
+  match doc with
+  | some doc => pure doc
+  | none => pure ""
+
 /-- Given a name, returns the source code defining that name. -/
 def Name.getDeclString (name : Name) : MetaM String := do
   let env ← getEnv

HepLean/Meta/Remark/Basic.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Batteries.Lean.HashSet
+import Mathlib.Lean.Expr.Basic
+import Mathlib.Lean.CoreM
+import ImportGraph.RequiredModules
+/-!
+
+## Underlying structure for remarks
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-- The information from a `remark ...` command. To be used in a note file-/
+structure RemarkInfo where
+  /-- The content of the remark. -/
+  content : String
+  /-- The file name where the remark came from. -/
+  fileName : Name
+  /-- The line from where the remark came from. -/
+  line : Nat
+  /-- The name of the remark. -/
+  name : Name
+  /-- The namespace of the remark. -/
+  nameSpace : Name
+
+/-- Environment extension to store `remark ...`. -/
+initialize remarkExtension : SimplePersistentEnvExtension RemarkInfo (Array RemarkInfo) ←
+  registerSimplePersistentEnvExtension {
+    name := `remarkExtension
+    addEntryFn := fun arr remarkInfoT => arr.push remarkInfoT
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
+  }
+
+/-- A remark is a string used for important information. -/
+syntax (name := remark_syntax) "remark " ident ":=" str : command
+
+/-- Elaborator for the `note ...` command -/
+@[command_elab remark_syntax]
+def elabRemark : Lean.Elab.Command.CommandElab := fun stx =>
+  match stx with
+  | `(remark $n := $s) => do
+    let str : String := s.getString
+    let pos := stx.getPos?
+    match pos with
+    | some pos => do
+      let env ← getEnv
+      let fileMap ← getFileMap
+      let filePos := fileMap.toPosition pos
+      let line := filePos.line
+      let modName := env.mainModule
+      let nameSpace := (← getCurrNamespace)
+
+      let noteInfo : RemarkInfo := {
+          content := str,
+          fileName := modName,
+          line := line,
+          name := n.getId,
+          nameSpace := nameSpace}
+      modifyEnv fun env => remarkExtension.addEntry env noteInfo
+    | none => throwError "Invalid syntax for `note` command"
+  | _ => throwError "Invalid syntax for `note` command"
+
+end HepLean

HepLean/Meta/Remark/Properties.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Remark.Basic
+/-!
+
+## Underlying structure for remarks
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-- All remarks in the enviroment. -/
+def Name.allRemarkInfo : MetaM (List RemarkInfo) := do
+  let env ← getEnv
+  let allRemarks := (remarkExtension.getState env)
+  pure allRemarks.toList
+
+/-- The full name of a remark (name and namespace). -/
+def RemarkInfo.toFullName (r : RemarkInfo) : Name :=
+  if r.nameSpace != .anonymous then
+    (r.nameSpace.toString ++ "." ++ r.name.toString).toName
+  else
+    r.name
+
+/-- A Bool which is true if a name correponds to a remark. -/
+def RemarkInfo.IsRemark (n : Name) : MetaM Bool := do
+  let allRemarks ← Name.allRemarkInfo
+  let r := allRemarks.find? (fun r => r.toFullName = n)
+  match r with
+  | some _ => pure true
+  | none => pure false
+
+/-- Gets the remarkInfo from a name corresponding to a remark.. -/
+def RemarkInfo.getRemarkInfo (n : Name) : MetaM RemarkInfo := do
+  let allRemarks ← Name.allRemarkInfo
+  let r := allRemarks.find? (fun r => r.toFullName = n)
+  match r with
+  | some r => pure r
+  | none => throwError s!"No remark named {n}"
+
+end HepLean

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean

@@ -132,13 +132,13 @@ lemma ofStateList_sum (φs : List 𝓕.States) :
 def crPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
   FreeAlgebra.lift ℂ fun φ =>
   match φ with
-  | States.negAsymp φ => ofCrAnState ⟨States.negAsymp φ, ()⟩
+  | States.inAsymp φ => ofCrAnState ⟨States.inAsymp φ, ()⟩
   | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩
-  | States.posAsymp _ => 0
+  | States.outAsymp _ => 0
 
 @[simp]
-lemma crPart_negAsymp (φ : 𝓕.AsymptoticNegTime) :
-    crPart (StateAlgebra.ofState (States.negAsymp φ)) = ofCrAnState ⟨States.negAsymp φ, ()⟩ := by
+lemma crPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+    crPart (StateAlgebra.ofState (States.inAsymp φ)) = ofCrAnState ⟨States.inAsymp φ, ()⟩ := by
   simp [crPart, StateAlgebra.ofState]
 
 @[simp]
@@ -148,8 +148,8 @@ lemma crPart_position (φ : 𝓕.PositionStates) :
   simp [crPart, StateAlgebra.ofState]
 
 @[simp]
-lemma crPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
-    crPart (StateAlgebra.ofState (States.posAsymp φ)) = 0 := by
+lemma crPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+    crPart (StateAlgebra.ofState (States.outAsymp φ)) = 0 := by
   simp [crPart, StateAlgebra.ofState]
 
 /-- The algebra map taking an element of the free-state algbra to
@@ -158,13 +158,13 @@ lemma crPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
 def anPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
   FreeAlgebra.lift ℂ fun φ =>
   match φ with
-  | States.negAsymp _ => 0
+  | States.inAsymp _ => 0
   | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.annihilate⟩
-  | States.posAsymp φ => ofCrAnState ⟨States.posAsymp φ, ()⟩
+  | States.outAsymp φ => ofCrAnState ⟨States.outAsymp φ, ()⟩
 
 @[simp]
-lemma anPart_negAsymp (φ : 𝓕.AsymptoticNegTime) :
-    anPart (StateAlgebra.ofState (States.negAsymp φ)) = 0 := by
+lemma anPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+    anPart (StateAlgebra.ofState (States.inAsymp φ)) = 0 := by
   simp [anPart, StateAlgebra.ofState]
 
 @[simp]
@@ -174,17 +174,17 @@ lemma anPart_position (φ : 𝓕.PositionStates) :
   simp [anPart, StateAlgebra.ofState]
 
 @[simp]
-lemma anPart_posAsymp (φ : 𝓕.AsymptoticPosTime) :
-    anPart (StateAlgebra.ofState (States.posAsymp φ)) = ofCrAnState ⟨States.posAsymp φ, ()⟩ := by
+lemma anPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+    anPart (StateAlgebra.ofState (States.outAsymp φ)) = ofCrAnState ⟨States.outAsymp φ, ()⟩ := by
   simp [anPart, StateAlgebra.ofState]
 
 lemma ofState_eq_crPart_add_anPart (φ : 𝓕.States) :
     ofState φ = crPart (StateAlgebra.ofState φ) + anPart (StateAlgebra.ofState φ) := by
   rw [ofState]
   cases φ with
-  | negAsymp φ => simp [statesToCrAnType]
+  | inAsymp φ => simp [statesToCrAnType]
   | position φ => simp [statesToCrAnType, CreateAnnihilate.sum_eq]
-  | posAsymp φ => simp [statesToCrAnType]
+  | outAsymp φ => simp [statesToCrAnType]
 
 /-!
 

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean

@@ -97,23 +97,23 @@ lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
     normalOrder (crPart (StateAlgebra.ofState φ) * a) =
     crPart (StateAlgebra.ofState φ) * normalOrder a := by
   match φ with
-  | .negAsymp φ =>
+  | .inAsymp φ =>
     rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
-    exact normalOrder_create_mul ⟨States.negAsymp φ, ()⟩ rfl a
+    exact normalOrder_create_mul ⟨States.inAsymp φ, ()⟩ rfl a
   | .position φ =>
     rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
     exact normalOrder_create_mul _ rfl _
-  | .posAsymp φ => simp
+  | .outAsymp φ => simp
 
 lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
     normalOrder (a * anPart (StateAlgebra.ofState φ)) =
     normalOrder a * anPart (StateAlgebra.ofState φ) := by
   match φ with
-  | .negAsymp φ => simp
+  | .inAsymp φ => simp
   | .position φ =>
     rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
     exact normalOrder_mul_annihilate _ rfl _
-  | .posAsymp φ =>
+  | .outAsymp φ =>
     rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
     refine normalOrder_mul_annihilate _ rfl _
 
@@ -191,24 +191,24 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 
     normalOrder (a * (anPart (StateAlgebra.ofState φ')) *
       (crPart (StateAlgebra.ofState φ)) * b) := by
   match φ, φ' with
-  | _, .negAsymp φ' => simp
-  | .posAsymp φ, _ => simp
+  | _, .inAsymp φ' => simp
+  | .outAsymp φ, _ => simp
   | .position φ, .position φ' =>
     simp only [crPart_position, anPart_position, instCommGroup.eq_1]
     rw [normalOrder_swap_create_annihlate]
     simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
     rfl; rfl
-  | .negAsymp φ, .posAsymp φ' =>
+  | .inAsymp φ, .outAsymp φ' =>
     simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1]
     rw [normalOrder_swap_create_annihlate]
     simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
     rfl; rfl
-  | .negAsymp φ, .position φ' =>
+  | .inAsymp φ, .position φ' =>
     simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1]
     rw [normalOrder_swap_create_annihlate]
     simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
     rfl; rfl
-  | .position φ, .posAsymp φ' =>
+  | .position φ, .outAsymp φ' =>
     simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1]
     rw [normalOrder_swap_create_annihlate]
     simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnStatesToStates_prod]
@@ -232,37 +232,37 @@ lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnA
     normalOrder (a * superCommute
     (crPart (StateAlgebra.ofState φ)) (anPart (StateAlgebra.ofState φ')) * b) = 0 := by
   match φ, φ' with
-  | _, .negAsymp φ' => simp
-  | .posAsymp φ', _ => simp
+  | _, .inAsymp φ' => simp
+  | .outAsymp φ', _ => simp
   | .position φ, .position φ' =>
     rw [crPart_position, anPart_position]
     exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
-  | .negAsymp φ, .posAsymp φ' =>
+  | .inAsymp φ, .outAsymp φ' =>
     rw [crPart_negAsymp, anPart_posAsymp]
     exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
-  | .negAsymp φ, .position φ' =>
+  | .inAsymp φ, .position φ' =>
     rw [crPart_negAsymp, anPart_position]
     exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
-  | .position φ, .posAsymp φ' =>
+  | .position φ, .outAsymp φ' =>
     rw [crPart_position, anPart_posAsymp]
     exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..
 
 lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
     normalOrder (a * superCommute
     (anPart (StateAlgebra.ofState φ)) (crPart (StateAlgebra.ofState φ')) * b) = 0 := by
   match φ, φ' with
-  | .negAsymp φ', _ => simp
-  | _, .posAsymp φ' => simp
+  | .inAsymp φ', _ => simp
+  | _, .outAsymp φ' => simp
   | .position φ, .position φ' =>
     rw [anPart_position, crPart_position]
     exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
-  | .posAsymp φ', .negAsymp φ =>
+  | .outAsymp φ', .inAsymp φ =>
     simp only [anPart_posAsymp, crPart_negAsymp]
     exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
-  | .position φ', .negAsymp φ =>
+  | .position φ', .inAsymp φ =>
     simp only [anPart_position, crPart_negAsymp]
     exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
-  | .posAsymp φ, .position φ' =>
+  | .outAsymp φ, .position φ' =>
     simp only [anPart_posAsymp, crPart_position]
     exact normalOrder_superCommute_annihilate_create _ _ rfl rfl ..
 
@@ -510,9 +510,9 @@ lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
     + ⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs')⟩ₛca := by
   rw [normalOrder_mul_anPart]
   match φ with
-  | .negAsymp φ => simp
+  | .inAsymp φ => simp
   | .position φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]
-  | .posAsymp φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]
+  | .outAsymp φ => simp [ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute, crAnStatistics]
 
 end