path: root/Main.lean

import Lean

open Lean IO

--------------------------------------------------------------------------------
-- 1. Data structures for commands and knowledge base state
--------------------------------------------------------------------------------

inductive KBCommand where
  | Init (dir : String)
  | AddType (name : String) (parent : Option String)
  | AddInstance (name : String) (typeName : String)
  | AddProp (name : String) (domain : String) (range : String)
  | AddRel (name : String) (dom1 : String) (dom2 : String)
  | AddFact (fact : String)
  | AddRule (name : String) (statement : String)
  | AddDef (name : String) (params : String) (type : String) (body : String)
  | Remove (name : String)
  | List (what : String) (filter : Option String)
  | ShowDef (name : String)
  | Eval (expr : String)
  | Query (prop : String)
  | Check
  | Commit (msg : String)
  | Status
  | Domains                -- new: show domain hierarchy
  | DomainsStats           -- new: show statistics per domain (stub)
  | Help
  | Exit
deriving Repr

structure KBState where
  root : System.FilePath

--------------------------------------------------------------------------------
-- 2. Command parsing (simple, based on whitespace)
--------------------------------------------------------------------------------

def parseCommand (line : String) : Option KBCommand :=
  let parts := line.trim.splitOn " " |>.filter (not ∘ String.isEmpty)
  match parts with
  | ["init", dir] => some (.Init dir)
  | ["add", "type", name] => some (.AddType name none)
  | ["add", "type", name, "extends", parent] => some (.AddType name (some parent))
  | ["add", "instance", name, ":", typeName] => some (.AddInstance name typeName)
  | ["add", "prop", name, ":", domain, "->", range] => some (.AddProp name domain range)
  | ["add", "rel", name, ":", dom1, "->", dom2, "->", "Prop"] => some (.AddRel name dom1 dom2)
  | ["add", "fact", _] =>
      some (.AddFact (line.drop 9)) -- drop "add fact "
  | ["add", "rule", name, ":", _] =>
      let n := 9 + name.length + 2
      some (.AddRule name (line.drop n))
  | ["add", "def", name, params, ":", type, ":=", body] =>
      some (.AddDef name params type body)
  | ["rm", name] => some (.Remove name)
  | ["list", what] => some (.List what none)
  | ["list", what, "of", filter] => some (.List what (some filter))
  | ["show", "def", name] => some (.ShowDef name)
  | ["eval", expr] => some (.Eval expr)
  | ["query", prop] => some (.Query prop)
  | ["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

--------------------------------------------------------------------------------
-- 3. Handlers (stubs with informative output)
--------------------------------------------------------------------------------

def addType (name : String) (parent : Option String) : IO Unit := do
  let parentMsg := match parent with | some p => s!" extending '{p}'" | none => ""
  println s!"[Stub] Adding type '{name}'{parentMsg}"
  println "  Would append to appropriate .lean file and run `lake build`."

def addInstance (name : String) (typeName : String) : IO Unit := do
  println s!"[Stub] Adding instance '{name} : {typeName}'"

def addProp (name domain range : String) : IO Unit := do
  println s!"[Stub] Adding property '{name} : {domain} -> {range}'"

def addRel (name dom1 dom2 : String) : IO Unit := do
  println s!"[Stub] Adding relation '{name} : {dom1} -> {dom2} -> Prop'"

def addFact (fact : String) : IO Unit := do
  println s!"[Stub] Adding fact: {fact}"

def addRule (name stmt : String) : IO Unit := do
  println s!"[Stub] Adding rule '{name} : {stmt}'"

def addDef (name params type body : String) : IO Unit := do
  println s!"[Stub] Adding definition '{name} {params} : {type} := {body}'"

def removeDecl (name : String) : IO Unit := do
  println s!"[Stub] Removing declaration '{name}' (checking dependencies)"

def listDecls (what : String) (filter : Option String) : IO Unit := do
  let filterMsg := match filter with | some f => s!" of {f}" | none => ""
  println s!"[Stub] Listing {what}{filterMsg}"

def showDef (name : String) : IO Unit := do
  println s!"[Stub] Showing definition of '{name}'"

def evalExpr (expr : String) : IO Unit := do
  println s!"[Stub] Evaluating: {expr}"
  println "  Would run `#eval` in a temporary Lean file and return result."

def queryProp (prop : String) : IO Unit := do
  println s!"[Stub] Querying: {prop}"
  println "  Would attempt to prove with `aesop` and return Yes/No/Unknown."

def checkKB : IO Unit := do
  println "Running `lake build` to verify knowledge base..."
  let child ← IO.Process.spawn { cmd := "lake", args := #["build"] }
  let exitCode ← child.wait
  if exitCode == 0 then
    println "Consistent (build succeeded)."
  else
    println "Inconsistent! Build failed."

def commitChanges (msg : String) : IO Unit := do
  println s!"[Stub] Committing with message: {msg}"
  println "  Would run `git add . && git commit -m \"...\"` after `kb check`."

def status : IO Unit := do
  println "[Stub] Showing git status and unverified changes."

def initKB (dir : String) : IO Unit := do
  println s!"[Stub] Initializing new knowledge base in '{dir}'"
  println "  Would create directory structure and lakefile.lean."

--------------------------------------------------------------------------------
-- 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 :=
  "Lean4 Knowledge Base CLI (kb)\n" ++
  "Usage: kb <command> [arguments]\n\n" ++
  "Commands:\n" ++
  "  init <dir>                    Create a new knowledge base repository.\n" ++
  "  add type <name> [extends <p>] Define a new type.\n" ++
  "  add instance <name> : <type>  Declare an instance.\n" ++
  "  add prop <name> : <d> -> <r>  Add a property.\n" ++
  "  add rel <name> : <d1> -> <d2> -> Prop  Add a relation.\n" ++
  "  add fact <fact>                Add a fact.\n" ++
  "  add rule <name> : <statement>  Add a logical rule.\n" ++
  "  add def <name> <params> : <t> := <body>  Define a shortcut.\n" ++
  "  rm <name>                      Remove a declaration.\n" ++
  "  list <types|instances|props|rels|facts|defs> [of <filter>]  List.\n" ++
  "  show def <name>                 Show a shortcut definition.\n" ++
  "  eval <expr>                     Evaluate a computable expression.\n" ++
  "  query <prop>                    Ask whether a proposition is provable.\n" ++
  "  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"

--------------------------------------------------------------------------------
-- 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
  let _ := stateRef -- silence unused warning
  match parseCommand line with
  | none => println "Invalid command. Type 'help' for usage."
  | some cmd =>
    match cmd with
    | .Init dir => initKB dir
    | .AddType name parent => addType name parent
    | .AddInstance name ty => addInstance name ty
    | .AddProp name dom ran => addProp name dom ran
    | .AddRel name d1 d2 => addRel name d1 d2
    | .AddFact fact => addFact fact
    | .AddRule name stmt => addRule name stmt
    | .AddDef name params ty body => addDef name params ty body
    | .Remove name => removeDecl name
    | .List what filt => listDecls what filt
    | .ShowDef name => showDef name
    | .Eval expr => evalExpr expr
    | .Query prop => queryProp prop
    | .Check => checkKB
    | .Commit msg => commitChanges msg
    | .Status => status
    | .Domains => listDomains
    | .DomainsStats => domainsStats
    | .Help => println helpText
    | .Exit => throw (IO.userError "exit")

partial def main : IO Unit := do
  println "Lean4 Knowledge Base CLI"
  println "Type 'help' for commands."
  let initialState : KBState := { root := System.FilePath.mk "." }
  let stateRef ← IO.mkRef initialState
  let rec loop : IO Unit := do
    IO.print "kb> "
    let line ← (← IO.getStdin).getLine
    let trimmed := line.trim
    if trimmed.isEmpty then loop
    else
      try
        processCommand stateRef trimmed
        if trimmed == "exit" then return ()
        else loop
      catch e =>
        if e.toString == "exit" then return ()
        else do
          println s!"Error: {e}"
          loop
  loop