aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorPetri Hienonen <petri.hienonen@gmail.com>2026-02-15 14:36:34 +0200
committerPetri Hienonen <petri.hienonen@gmail.com>2026-02-15 14:36:34 +0200
commit5f787f25cc5caf4ba388734d96ff9205739504cb (patch)
tree68669970637eed4aad94ead6e6020b155b6e1f2b
parentbb570329a9265891e01d8fedb903ca4715dad316 (diff)
downloadkb-5f787f25cc5caf4ba388734d96ff9205739504cb.tar.zst
Update
-rw-r--r--Main.lean66
1 files changed, 63 insertions, 3 deletions
diff --git a/Main.lean b/Main.lean
index dbaa997..17e0ea0 100644
--- a/Main.lean
+++ b/Main.lean
@@ -23,6 +23,8 @@ inductive KBCommand where
| Check
| Commit (msg : String)
| Status
+ | Domains -- new: show domain hierarchy
+ | DomainsStats -- new: show statistics per domain (stub)
| Help
| Exit
deriving Repr
@@ -59,6 +61,8 @@ def parseCommand (line : String) : Option KBCommand :=
| ["check"] => some .Check
| ["commit", msg] => some (.Commit msg)
| ["status"] => some .Status
+ | ["domains"] => some .Domains -- new
+ | ["domains", "stats"] => some .DomainsStats -- new
| ["help"] => some .Help
| ["exit"] => some .Exit
| _ => none
@@ -129,7 +133,50 @@ def initKB (dir : String) : IO Unit := do
println " Would create directory structure and lakefile.lean."
--------------------------------------------------------------------------------
--- 4. Help text with hierarchical classification (RESTORED)
+-- 4. Domain hierarchy (extracted from the original help text)
+--------------------------------------------------------------------------------
+
+def domainHierarchy : String :=
+ "Domain classification (initial curated structure):\n" ++
+ "- Mathematics\n" ++
+ " • Elementary Math (Arithmetic, Fractions, Percentages)\n" ++
+ " • Algebra\n" ++
+ " • Geometry (Plane, Solid, Coordinate, Transformations, High‑D, Packing, Curves, Polyforms, Topology, Tilings)\n" ++
+ " • Plotting (Functions, Equations, Parametric, Inequalities, Number Lines, Polar)\n" ++
+ " • Calculus (Integrals, Derivatives, Limits, Sequences, Products, Series, Sums, Vector Analysis, Transforms, Applications, Continuity, Domain/Range)\n" ++
+ " • Differential Equations\n" ++
+ " • Statistics (Descriptive, Inference, Regression, Random Variables)\n" ++
+ " • Functions (Domain/Range, Injectivity/Surjectivity, Continuity, Periodic, Odd/Even, Special, Number Theoretic, Representation)\n" ++
+ "- Science & Technology\n" ++
+ " • Physics (Mechanics, Oscillations, Statistical Physics, Thermodynamics, Electricity & Magnetism, Optics, Relativity, Nuclear, Quantum, Particle, Astrophysics, Constants, Principles, Effects, Fluid Mechanics)\n" ++
+ " • Chemistry\n" ++
+ " • Units & Measures\n" ++
+ " • Engineering (Aerospace, Energy, Electrical, Control Systems, Mechanical, Civil, Fluid Mechanics, Sound, Steam Tables, Measurement)\n" ++
+ " • Computational Sciences (Cellular Automata, Substitution Systems, Turing Machines, Complexity, Algebraic Codes, Fractals, Image Processing, Hashing)\n" ++
+ " • Earth Sciences\n" ++
+ " • Life Sciences (Human Anatomy, Animal Anatomy, Neuroscience, Genomics, Molecular Biology, Animals & Plants)\n" ++
+ " • Space & Astronomy\n" ++
+ "- Society & Culture\n" ++
+ " • People\n" ++
+ " • Arts & Media\n" ++
+ " • History\n" ++
+ " • Words & Linguistics (Word Properties, Languages, Document Length, Notable Texts, Transliterations, Morse, Soundex, Encodings, Emotions)\n" ++
+ " • Money & Finance (Stock Data, Mortgages, Salaries, Bonds, Derivatives, Income Tax, Sales Tax)\n" ++
+ " • Dates & Times\n" ++
+ " • Food & Nutrition\n" ++
+ " • Demographics (Health, Age/Sex, Gender, Business, Citizenship, Crime, Education, Income, Language, Race, Marriage, Mobility, Religion, Military, HDI)\n" ++
+ "- Everyday Life\n" ++
+ " • Personal Health (Exercise, Nutrition, Child Growth)\n" ++
+ " • Personal Finance (Mortgages, Stocks, Currency, Cost of Living, Gas, Food, Electricity)\n" ++
+ " • Entertainment\n" ++
+ " • Household Science\n" ++
+ " • Household Math\n" ++
+ " • Programming\n" ++
+ " • Hobbies\n" ++
+ " • Today's World (Economy, Finland Economy, Weather)\n"
+
+--------------------------------------------------------------------------------
+-- 5. Help text (now includes the new commands)
--------------------------------------------------------------------------------
def helpText : String :=
@@ -152,11 +199,23 @@ def helpText : String :=
" check Run `lake build` to verify consistency.\n" ++
" commit <message> Commit all changes.\n" ++
" status Show git status.\n" ++
+ " domains Show the hierarchical domain classification.\n" ++
+ " domains stats Show statistics per domain (stub).\n" ++
" help Show this help.\n" ++
" exit Exit the CLI.\n"
--------------------------------------------------------------------------------
--- 5. Main loop
+-- 6. Domain command handlers
+--------------------------------------------------------------------------------
+
+def listDomains : IO Unit := do
+ println domainHierarchy
+
+def domainsStats : IO Unit := do
+ println "[Stub] Domain statistics (would show counts of types/instances per domain)"
+
+--------------------------------------------------------------------------------
+-- 7. Main loop
--------------------------------------------------------------------------------
partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Unit := do
@@ -181,6 +240,8 @@ partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Unit
| .Check => checkKB
| .Commit msg => commitChanges msg
| .Status => status
+ | .Domains => listDomains
+ | .DomainsStats => domainsStats
| .Help => println helpText
| .Exit => throw (IO.userError "exit")
@@ -205,4 +266,3 @@ partial def main : IO Unit := do
println s!"Error: {e}"
loop
loop
-