From 92aa04ba5a317fa6a2eafd03fe16ce3696d70703 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 13 Mar 2025 07:37:30 +0000
Subject: [PATCH] refactor: Update todo list

---
 PhysLean/Meta/Informal/Post.lean      |   8 ++
 scripts/MetaPrograms/TODO_to_yml.lean | 125 ++++++++++++++++++++++++--
 2 files changed, 127 insertions(+), 6 deletions(-)

diff --git a/PhysLean/Meta/Informal/Post.lean b/PhysLean/Meta/Informal/Post.lean
index fbeb424..1db5e45 100644
--- a/PhysLean/Meta/Informal/Post.lean
+++ b/PhysLean/Meta/Informal/Post.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import PhysLean.Meta.Basic
 import PhysLean.Meta.Informal.Basic
+import PhysLean.Meta.TODO.Basic
 /-!
 
 ## Informal definitions and lemmas
@@ -61,4 +62,11 @@ def noInformalDefs : CoreM Nat := do
   let x ← imports.mapM Imports.getUserConsts
   x.flatFilterSizeM fun c => return Informal.isInformalDef c
 
+/-- All informal results. -/
+def AllInformal : CoreM (Array ConstantInfo) := do
+  let imports ← allImports
+  let x ← (imports.mapM Imports.getUserConsts)
+  let y := x.flatten.filter fun c => Informal.isInformal c
+  return y
+
 end PhysLean
diff --git a/scripts/MetaPrograms/TODO_to_yml.lean b/scripts/MetaPrograms/TODO_to_yml.lean
index becd617..ef06839 100644
--- a/scripts/MetaPrograms/TODO_to_yml.lean
+++ b/scripts/MetaPrograms/TODO_to_yml.lean
@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import PhysLean.Meta.Basic
 import PhysLean.Meta.TODO.Basic
 import Mathlib.Lean.CoreM
+import PhysLean.Meta.Informal.Post
 /-!
 
 # Turning TODOs into YAML
@@ -15,25 +16,137 @@ import Mathlib.Lean.CoreM
 open Lean System Meta PhysLean
 
 
-unsafe def getTodoInfo : MetaM (List todoInfo) := do
+/-!
+
+## PhysLean categories.
+
+To be moved.
+
+-/
+inductive PhysLeanCategory
+  | ClassicalMechanics
+  | CondensedMatter
+  | Cosmology
+  | Elctromagnetism
+  | Mathematics
+  | Meta
+  | Optics
+  | Particles
+  | QFT
+  | QuantumMechanics
+  | Relativity
+  | StatisticalMechanics
+  | Thermodynamics
+  | Other
+
+def PhysLeanCategory.string :  PhysLeanCategory → String
+  | ClassicalMechanics => "Classical Mechanics"
+  | CondensedMatter => "Condensed Matter"
+  | Cosmology => "Cosmology"
+  | Elctromagnetism => "Electromagnetism"
+  | Mathematics => "Mathematics"
+  | Meta => "Meta"
+  | Optics => "Optics"
+  | Particles => "Particles"
+  | QFT => "QFT"
+  | QuantumMechanics => "Quantum Mechanics"
+  | Relativity => "Relativity"
+  | StatisticalMechanics => "Statistical Mechanics"
+  | Thermodynamics => "Thermodynamics"
+  | Other => "Other"
+
+instance : ToString PhysLeanCategory where
+  toString := PhysLeanCategory.string
+
+def PhysLeanCategory.ofFileName (n : Name) : PhysLeanCategory :=
+  if n.toString.startsWith "PhysLean.ClassicalMechanics"  then
+    PhysLeanCategory.ClassicalMechanics
+  else if n.toString.startsWith "PhysLean.CondensedMatter" then
+    PhysLeanCategory.CondensedMatter
+  else if n.toString.startsWith "PhysLean.Cosmology" then
+    PhysLeanCategory.Cosmology
+  else if n.toString.startsWith "PhysLean.Electromagnetism" then
+    PhysLeanCategory.Elctromagnetism
+  else if n.toString.startsWith "PhysLean.Mathematics" then
+    PhysLeanCategory.Mathematics
+  else if n.toString.startsWith "PhysLean.Meta" then
+    PhysLeanCategory.Meta
+  else if n.toString.startsWith "PhysLean.Optics" then
+    PhysLeanCategory.Optics
+  else if n.toString.startsWith "PhysLean.Particles" then
+    PhysLeanCategory.Particles
+  else if n.toString.startsWith "PhysLean.QFT" then
+    PhysLeanCategory.QFT
+  else if n.toString.startsWith "PhysLean.QuantumMechanics" then
+    PhysLeanCategory.QuantumMechanics
+  else if n.toString.startsWith "PhysLean.Relativity" then
+    PhysLeanCategory.Relativity
+  else if n.toString.startsWith "PhysLean.StatisticalMechanics" then
+    PhysLeanCategory.StatisticalMechanics
+  else if n.toString.startsWith "PhysLean.Thermodynamics" then
+    PhysLeanCategory.Thermodynamics
+  else
+    PhysLeanCategory.Other
+
+/-########################-/
+
+structure FullTODOInfo where
+  content : String
+  fileName : Name
+  line : Nat
+  isInformalDef : Bool
+  isInformalLemma : Bool
+  category : PhysLeanCategory
+
+def FullTODOInfo.ofTODO (t : todoInfo) : FullTODOInfo :=
+  {content := t.content, fileName := t.fileName, line := t.line,
+   isInformalDef := false, isInformalLemma := false, category := PhysLeanCategory.ofFileName t.fileName}
+
+unsafe def getTodoInfo : MetaM (Array FullTODOInfo) := do
   let env ← getEnv
   let todoInfo := (todoExtension.getState env)
-  pure (todoInfo.qsort (fun x y => x.fileName.toString < y.fileName.toString)).toList
+  -- pure (todoInfo.qsort (fun x y => x.fileName.toString < y.fileName.toString)).toList
+  pure (todoInfo.map FullTODOInfo.ofTODO)
 
-def todoToYAML (todo : todoInfo) : MetaM String := do
+def informalTODO (x : ConstantInfo) : CoreM FullTODOInfo := do
+  let name := x.name
+  let lineNo ← Name.lineNumber name
+  let docString ← Name.getDocString name
+  let file ← Name.fileName name
+  let isInformalDef := Informal.isInformalDef x
+  let isInformalLemma := Informal.isInformalLemma x
+  let category := PhysLeanCategory.ofFileName file
+  return {content := docString, fileName := file, line := lineNo,
+          isInformalDef := isInformalDef, isInformalLemma := isInformalLemma, category := category}
+
+def allInformalTODO : CoreM (Array FullTODOInfo) := do
+  let x ← AllInformal
+  x.mapM informalTODO
+
+def FullTODOInfo.toYAML (todo : FullTODOInfo) : MetaM String := do
   return s!"
 - content: \"{todo.content}\"
   file: {todo.fileName}
   githubLink: {Name.toGitHubLink todo.fileName todo.line}
-  line: {todo.line}"
+  line: {todo.line}
+  isInformalDef: {todo.isInformalDef}
+  isInformalLemma: {todo.isInformalLemma}
+  category: {todo.category}"
+
+unsafe def allTODOs : MetaM (List FullTODOInfo) := do
+  let todos ← getTodoInfo
+  let informalTODOs ← allInformalTODO
+  let all := todos ++ informalTODOs
+  return  (all.qsort (fun x y => x.fileName.toString < y.fileName.toString)).toList
 
 unsafe def todosToYAML : MetaM String := do
-  let todos ← getTodoInfo
-  let todosYAML ← todos.mapM todoToYAML
+  let todos ← allTODOs
+  let todosYAML ← todos.mapM FullTODOInfo.toYAML
   return String.intercalate "\n" todosYAML
 
 unsafe def main (args : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
+  println! "Generating TODO list."
   let ymlString ← CoreM.withImportModules #[`PhysLean] (todosToYAML).run'
   println! ymlString
   let fileOut : System.FilePath := {toString := "./docs/_data/TODO.yml"}