diff options
| -rw-r--r-- | Main.lean | 66 |
1 files changed, 63 insertions, 3 deletions
@@ -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 - |