feat: Stats page

HepLean/Meta/Basic.lean

@@ -0,0 +1,178 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Batteries.Lean.HashSet
+import Lean
+import Mathlib.Lean.Expr.Basic
+import Mathlib.Lean.CoreM
+import ImportGraph.RequiredModules
+import HepLean.Meta.Informal
+/-!
+
+## Basic Lean meta programming commands
+
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-!
+
+## Imports
+
+-/
+
+/-- Gets all imports within HepLean. -/
+def allImports : IO (Array Import) := do
+  initSearchPath (← findSysroot)
+  let mods : Name := `HepLean
+  let imp : Import := {module := mods}
+  let mFile ← findOLean imp.module
+  unless (← mFile.pathExists) do
+        throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"
+  let (hepLeanMod, _) ← readModuleData mFile
+  let imports := hepLeanMod.imports.filter (fun c => c.module ≠ `Init)
+  return imports
+
+/-- Number of files within HepLean. -/
+def noImports : IO Nat := do
+  let imports ← allImports
+  pure imports.size
+
+/-- Gets all constants from an import. -/
+def Imports.getConsts (imp : Import) : IO (Array ConstantInfo) := do
+  let mFile ← findOLean imp.module
+  let (modData, _) ← readModuleData mFile
+  pure modData.constants
+
+/-- Gets all user defined constants from an import. -/
+def Imports.getUserConsts (imp : Import) : MetaM (Array ConstantInfo) := do
+  let env ← getEnv
+  let x := (← Imports.getConsts imp).filter (fun c => ¬ c.name.isInternal)
+  let x := x.filter (fun c => ¬ Lean.isCasesOnRecursor env c.name)
+  let x := x.filter (fun c => ¬ Lean.isRecOnRecursor env c.name)
+  let x := x.filter (fun c => ¬ Lean.isNoConfusion env c.name)
+  let x := x.filter (fun c => ¬ Lean.isBRecOnRecursor env c.name)
+  let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.binductionOnSuffix)
+  let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.belowSuffix)
+  let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.ibelowSuffix)
+  /- Removing syntax category declarations. -/
+  let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot" )
+  let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot" )
+  let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot" )
+  pure x
+
+/-- Lines from import. -/
+def Imports.getLines (imp : Import) : IO (Array String) := do
+  let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
+  let lines ← IO.FS.lines filePath
+  return lines
+
+/-!
+
+## Name
+
+-/
+
+
+/-- Turns a name into a Lean file. -/
+def Name.toFile (c : Name) : MetaM String := do
+  return s!"./{c.toString.replace "." "/" ++ ".lean"}"
+
+/-- Given a name, returns the line number. -/
+def Name.lineNumber (c : Name) : MetaM Nat := do
+  match ← findDeclarationRanges? c  with
+  | some decl => pure decl.range.pos.line
+  | none => panic! s!"{c} is a declaration without position"
+
+/-- Returns the location of a name. -/
+def Name.location (c : Name) : MetaM String := do
+  let env ← getEnv
+  let x := env.getModuleFor?  c
+  match x with
+  | some decl => pure ((← Name.toFile decl) ++ ":" ++ toString (← Name.lineNumber c) ++ " "
+    ++ c.toString)
+  | none => panic! s!"{c} is a declaration without position"
+
+/-- Determines if a name has a location. -/
+def Name.hasPos (c : Name) : MetaM Bool := do
+  match ← findDeclarationRanges? c  with
+  | some _ => pure true
+  | none => pure false
+
+/-- Determines if a name has a doc string. -/
+def Name.hasDocString (c : Name) : MetaM Bool := do
+  let env ← getEnv
+  let doc ← Lean.findDocString? env c
+  match doc with
+  | some _ => pure true
+  | none => pure false
+
+/-- Number of definitions. -/
+def noDefs : MetaM Nat := do
+  let imports ← allImports
+  let x ← imports.mapM Imports.getUserConsts
+  let x := x.flatten
+  let x := x.filter (fun c => c.isDef)
+  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  pure x.toList.length
+
+/-- Number of definitions. -/
+def noLemmas : MetaM Nat := do
+  let imports ← allImports
+  let x ← imports.mapM Imports.getUserConsts
+  let x := x.flatten
+  let x := x.filter (fun c => ¬ c.isDef)
+  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  pure x.toList.length
+
+/-- Number of definitions without a doc-string. -/
+def noDefsNoDocString : MetaM Nat := do
+  let imports ← allImports
+  let x ← imports.mapM Imports.getUserConsts
+  let x := x.flatten
+  let x := x.filter (fun c => c.isDef)
+  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  let x ← x.filterM (fun c => do
+    return Bool.not (← (Name.hasDocString c.name)))
+  pure x.toList.length
+
+/-- Number of definitions without a doc-string. -/
+def noLemmasNoDocString : MetaM Nat := do
+  let imports ← allImports
+  let x ← imports.mapM Imports.getUserConsts
+  let x := x.flatten
+  let x := x.filter (fun c => ¬ c.isDef)
+  let x ←  x.filterM (fun c => (Name.hasPos c.name))
+  let x ← x.filterM (fun c => do
+    return Bool.not (← (Name.hasDocString c.name)))
+  pure x.toList.length
+
+/-- The number of lines in HepLean. -/
+def noLines : IO Nat := do
+  let imports ← HepLean.allImports
+  let x ← imports.mapM HepLean.Imports.getLines
+  let x := x.flatten
+  pure x.toList.length
+
+/-- The number of informal lemmas in HepLean. -/
+def noInformalLemmas : MetaM Nat := do
+  let imports ← allImports
+  let x ← imports.mapM Imports.getUserConsts
+  let x := x.flatten
+  let x := x.filter (Informal.isInformal)
+  let x := x.filter (Informal.isInformalLemma)
+  pure x.toList.length
+
+/-- The number of informal definitions in HepLean. -/
+def noInformalDefs : MetaM Nat := do
+  let imports ← allImports
+  let x ← imports.mapM Imports.getUserConsts
+  let x := x.flatten
+  let x := x.filter (Informal.isInformal)
+  let x := x.filter (Informal.isInformalDef)
+  pure x.toList.length
+
+end HepLean