From 18b83f582ed5dfb9e99264fd1841f53b9ed40cf3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 11:12:13 -0400
Subject: [PATCH] feat: Add type_former_lint

---
 lakefile.toml                 |  6 +++++
 scripts/type_former_lint.lean | 49 +++++++++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 scripts/type_former_lint.lean

diff --git a/lakefile.toml b/lakefile.toml
index 0de577a..b29acd2 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -27,6 +27,12 @@ name = "HepLean"
 #git = "https://github.com/lean-dojo/LeanCopilot.git"
 #rev = "v1.2.2"
 
+# lean_exe commands defined specifically for HepLean.
+
 [[lean_exe]]
 name = "check_file_imports"
 srcDir = "scripts"
+
+[[lean_exe]]
+name = "type_former_lint"
+srcDir = "scripts"
diff --git a/scripts/type_former_lint.lean b/scripts/type_former_lint.lean
new file mode 100644
index 0000000..e5b8617
--- /dev/null
+++ b/scripts/type_former_lint.lean
@@ -0,0 +1,49 @@
+/-
+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
+/-!
+
+# Type former Lint
+
+This file checks that all definitions which form types start with a capital letter
+(or some non-latin character). This linter is not currently strictly enforced
+in HepLean.
+
+
+-/
+open Lean System Meta
+
+
+/-- A rough definition of Upper Camal, checking that if a string starts with a
+latin letter then that letter is captial.  -/
+def IsUpperCamal (s : String) : Bool :=
+  let parts := s.splitOn "."
+  let lastPart := parts.get! (parts.length - 1)
+  (¬ (lastPart.get 0 ≥ 'A' ∧ lastPart.get 0 ≤ 'z')) ∨ (lastPart.get 0 ≥ 'A' ∧ lastPart.get 0 ≤ 'Z')
+
+
+def main (_ : List String) : IO UInt32 := 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 mut warned := false
+  for imp in hepLeanMod.imports do
+    let mFile ← findOLean imp.module
+    let (modData, _) ← readModuleData mFile
+    let cons := modData.constants
+    for c in cons do
+      if c.hasValue ∧ ¬ Lean.Name.isInternal c.name ∧ Lean.Compiler.LCNF.isTypeFormerType c.type
+        ∧ ¬ IsUpperCamal c.name.toString then
+          warned := true
+          IO.println s!"name: #{c.name}"
+  if warned then
+    throw <| IO.userError s!"There are type former definitions not in upper camal style."
+  pure 0