/-
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

/-- The number of TODO items. -/
def noTODOs : IO Nat := do
  let imports ← HepLean.allImports
  let x ← imports.mapM HepLean.Imports.getLines
  let x := x.flatten
  let x := x.filter fun l => l.startsWith "/-! TODO:"
  pure x.size

/-- The number of files with a TODO item. -/
def noFilesWithTODOs : IO Nat := do
  let imports ← HepLean.allImports
  let x ← imports.mapM HepLean.Imports.getLines
  let x := x.filter (fun M => M.any fun l => l.startsWith "/-! TODO:")
  pure x.size

end HepLean