Update

1 files changed, 614 insertions, 200 deletions

diff --git a/Main.lean b/Main.lean
index 17e0ea0..86206f1 100644
--- a/Main.lean
+++ b/Main.lean
@@ -3,266 +3,680 @@ import Lean
 open Lean IO
 
 --------------------------------------------------------------------------------
--- 1. Data structures for commands and knowledge base state
+-- 1. Data structures
+--
+-- Every declaration carries an explicit `domain` chosen by the user.
+-- Domains are arbitrary identifiers (e.g. "Ontology", "Physics", "Finance").
+-- Each domain maps to a single <domain>.lean file in the KB root.
 --------------------------------------------------------------------------------
 
 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)
+  | Init        (dir : String)
+  | AddType     (name : String) (parent : Option String) (domain : String)
+  | AddInstance (name : String) (typeName : String)      (domain : String)
+  | AddProp     (name : String) (domType : String) (range : String) (domain : String)
+  | AddRel      (name : String) (dom1 : String) (dom2 : String)     (domain : String)
+  | AddFact     (fact : String)                                      (domain : String)
+  | AddRule     (name : String) (statement : String)                 (domain : String)
+  | AddDef      (name : String) (params : String) (type : String) (body : String) (domain : String)
+  | Remove      (name : String)
+  | List        (what : String) (filter : Option String)
+  | ShowDef     (name : String)
+  | Eval        (expr : String)
+  | Query       (prop : String)
   | Check
-  | Commit (msg : String)
+  | Commit      (msg : String)
   | Status
-  | Domains                -- new: show domain hierarchy
-  | DomainsStats           -- new: show statistics per domain (stub)
+  | Domains
+  | DomainsStats
   | Help
   | Exit
 deriving Repr
 
+structure KBDecl where
+  kind   : String   -- "type" | "instance" | "prop" | "rel" | "fact" | "rule" | "def"
+  name   : String
+  lean   : String   -- Lean 4 source text emitted to disk
+  domain : String   -- user-chosen domain stem (becomes <domain>.lean)
+deriving Repr, Inhabited
+
 structure KBState where
-  root : System.FilePath
+  root  : System.FilePath
+  decls : Array KBDecl
+
+--------------------------------------------------------------------------------
+-- 2. Lean-4-safe utility functions
+--------------------------------------------------------------------------------
+
+/-- True when `needle` appears anywhere in `haystack`. -/
+def strContains (haystack needle : String) : Bool :=
+  if needle.isEmpty then true
+  else (haystack.splitOn needle).length > 1
+
+/-- Remove duplicate strings from a list, keeping first occurrence. -/
+def dedupStrings (xs : List String) : List String :=
+  xs.foldl (fun acc x => if acc.contains x then acc else acc ++ [x]) []
+
+/-- ASCII-only lowercase. -/
+def strToLower (s : String) : String :=
+  s.map fun c =>
+    if c.toNat >= 'A'.toNat && c.toNat <= 'Z'.toNat
+    then Char.ofNat (c.toNat + 32) else c
 
 --------------------------------------------------------------------------------
--- 2. Command parsing (simple, based on whitespace)
+-- 3. Command parsing
+--
+-- Every `add` command requires an explicit `in <Domain>` suffix that names the
+-- destination file.  Both `→` and `->` are accepted as type arrows.
+--
+-- Syntax:
+--   add type   <Name> [extends <Parent>] in <Domain>
+--   add instance <name> : <Type>          in <Domain>
+--   add prop   <name> : <DomType> -> <Range> in <Domain>
+--   add rel    <name> : <D1> -> <D2> -> Prop in <Domain>
+--   add fact   <fact>                      in <Domain>
+--   add rule   <name> : <statement>        in <Domain>
+--   add def    <name> <params> : <T> := <body> in <Domain>
 --------------------------------------------------------------------------------
 
 def parseCommand (line : String) : Option KBCommand :=
-  let parts := line.trim.splitOn " " |>.filter (not ∘ String.isEmpty)
+  -- Normalise Unicode → so either arrow style works.
+  let normalised := line.trim.replace "→" "->"
+  let parts := normalised.splitOn " " |>.filter (not ∘ String.isEmpty)
+  let raw   := line.trim   -- used for suffix-style extraction
   match parts with
+  -- ── init ────────────────────────────────────────────────────────────────
   | ["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
+  -- ── add type ────────────────────────────────────────────────────────────
+  | ["add", "type", name, "in", dom] =>
+      some (.AddType name none dom)
+  | ["add", "type", name, "extends", par, "in", dom] =>
+      some (.AddType name (some par) dom)
+  -- ── add instance ────────────────────────────────────────────────────────
+  | ["add", "instance", name, ":", ty, "in", dom] =>
+      some (.AddInstance name ty dom)
+  -- ── add prop ────────────────────────────────────────────────────────────
+  | ["add", "prop", name, ":", dt, "->", rng, "in", dom] =>
+      some (.AddProp name dt rng dom)
+  -- ── add rel ─────────────────────────────────────────────────────────────
+  | ["add", "rel", name, ":", d1, "->", d2, "->", "Prop", "in", dom] =>
+      some (.AddRel name d1 d2 dom)
+  -- ── add fact  (suffix style: everything between "add fact " and " in <D>")
+  | "add" :: "fact" :: _ =>
+      -- Find " in " as a domain separator (last occurrence wins).
+      let body := raw.drop "add fact ".length
+      let segs := body.splitOn " in "
+      if segs.length >= 2 then
+        let dom  := segs.getLast!.trim
+        -- Rejoin all but the last segment in case the fact itself contains " in "
+        let fact := (segs.dropLast |> String.intercalate " in ").trim
+        some (.AddFact fact dom)
+      else none
+  -- ── add rule  (suffix style) ─────────────────────────────────────────────
+  | "add" :: "rule" :: name :: ":" :: _ =>
+      let afterColon := raw.drop ("add rule " ++ name ++ " : ").length
+      let segs := afterColon.splitOn " in "
+      if segs.length >= 2 then
+        let dom  := segs.getLast!.trim
+        let stmt := (segs.dropLast |> String.intercalate " in ").trim
+        some (.AddRule name stmt dom)
+      else none
+  -- ── add def  ─────────────────────────────────────────────────────────────
+  -- Syntax: add def <n> <params> : <type> := <body> in <Domain>
+  | "add" :: "def" :: name :: _ =>
+      let afterName  := raw.drop ("add def " ++ name ++ " ").length
+      let domSegs    := afterName.splitOn " in "
+      if domSegs.length < 2 then none
+      else
+        let dom      := domSegs.getLast!.trim
+        let defBody  := (domSegs.dropLast |> String.intercalate " in ").trim
+        let colonSegs := defBody.splitOn " : "
+        if colonSegs.length < 2 then none
+        else
+          let params   := (colonSegs.headD "").trim
+          let typeBody := (colonSegs.tail |> String.intercalate " : ").trim
+          let assignSegs := typeBody.splitOn " := "
+          if assignSegs.length < 2 then none
+          else
+            let ty   := (assignSegs.headD "").trim
+            let body := (assignSegs.tail |> String.intercalate " := ").trim
+            some (.AddDef name params ty body dom)
+  -- ── other commands (no domain argument) ──────────────────────────────────
+  | ["rm", name]             => some (.Remove name)
+  | ["list", what]           => some (.List what none)
+  | ["list", what, "of", f]  => some (.List what (some f))
+  | ["show", "def", name]    => some (.ShowDef name)
+  | "eval" :: _              => some (.Eval   (raw.drop "eval ".length))
+  | "query" :: _             => some (.Query  (raw.drop "query ".length))
+  | ["check"]                => some .Check
+  | "commit" :: _            => some (.Commit (raw.drop "commit ".length))
+  | ["status"]               => some .Status
+  | ["domains"]              => some .Domains
+  | ["domains", "stats"]     => some .DomainsStats
+  | ["help"]                 => some .Help
+  | ["exit"]                 => some .Exit
+  | _                        => none
 
 --------------------------------------------------------------------------------
--- 3. Handlers (stubs with informative output)
+-- 4. File-system helpers
 --------------------------------------------------------------------------------
 
-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 domainPath (root : System.FilePath) (domain : String) : System.FilePath :=
+  root / (domain ++ ".lean")
 
-def addInstance (name : String) (typeName : String) : IO Unit := do
-  println s!"[Stub] Adding instance '{name} : {typeName}'"
+/-- Append `decl` to a domain file, creating it with a module header if new. -/
+def appendToDomain (root : System.FilePath) (domain decl : String) : IO Unit := do
+  let path := domainPath root domain
+  unless (← path.pathExists) do
+    IO.FS.writeFile path s!"-- Knowledge Base: {domain}\n\n"
+  let handle ← IO.FS.Handle.mk path .append
+  handle.putStrLn decl
+  handle.flush
 
-def addProp (name domain range : String) : IO Unit := do
-  println s!"[Stub] Adding property '{name} : {domain} -> {range}'"
+def runProc (cmd : String) (args : Array String) (cwd : Option String := none)
+    : IO (UInt32 × String) := do
+  let child ← IO.Process.spawn {
+    cmd    := cmd
+    args   := args
+    cwd    := cwd
+    stdout := .piped
+    stderr := .piped
+  }
+  let stdoutTask ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
+  let stderrOut  ← child.stderr.readToEnd
+  let stdoutOut  ← IO.ofExcept stdoutTask.get
+  let code       ← child.wait
+  return (code, stdoutOut ++ stderrOut)
 
-def addRel (name dom1 dom2 : String) : IO Unit := do
-  println s!"[Stub] Adding relation '{name} : {dom1} -> {dom2} -> Prop'"
+def runProcPrint (cmd : String) (args : Array String) (cwd : Option String := none)
+    : IO UInt32 := do
+  let (code, out) ← runProc cmd args cwd
+  unless out.isEmpty do println out
+  return code
 
-def addFact (fact : String) : IO Unit := do
-  println s!"[Stub] Adding fact: {fact}"
+--------------------------------------------------------------------------------
+-- 5. Lean snippet generators
+--------------------------------------------------------------------------------
 
-def addRule (name stmt : String) : IO Unit := do
-  println s!"[Stub] Adding rule '{name} : {stmt}'"
+def genType (name : String) (parent : Option String) : String :=
+  match parent with
+  | none   => s!"opaque {name} : Type"
+  | some p =>
+      s!"opaque {name} : Type\n" ++
+      s!"-- {name} extends {p}\n" ++
+      s!"axiom {name}.val : {name} → {p}"
 
-def addDef (name params type body : String) : IO Unit := do
-  println s!"[Stub] Adding definition '{name} {params} : {type} := {body}'"
+def genInstance (name typeName : String) : String :=
+  s!"opaque {name} : {typeName}"
 
-def removeDecl (name : String) : IO Unit := do
-  println s!"[Stub] Removing declaration '{name}' (checking dependencies)"
+def genProp (name domType range : String) : String :=
+  s!"opaque {name} : {domType} → {range}"
 
-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 genRel (name dom1 dom2 : String) : String :=
+  s!"opaque {name} : {dom1} → {dom2} → Prop"
 
-def showDef (name : String) : IO Unit := do
-  println s!"[Stub] Showing definition of '{name}'"
+/-- Parse a fact string and produce a Lean axiom.
+    Accepted syntax:
+      `prop(inst) = value`    →  `axiom fact_prop_inst : prop inst = value`
+      `rel(inst1, inst2)`     →  `axiom fact_rel_inst1_inst2 : rel inst1 inst2` -/
+def genFact (fact : String) : String :=
+  let byOpenParen := fact.splitOn "("
+  if byOpenParen.length < 2 then
+    -- No parentheses: bare `lhs = rhs`
+    let byEq := fact.splitOn "="
+    if byEq.length >= 2 then
+      let lhs := (byEq.headD "").trim
+      let rhs := (byEq.tail.headD "").trim
+      s!"axiom fact_{lhs} : {lhs} = {rhs}"
+    else
+      s!"-- unrecognised fact: {fact}\n-- expected: prop(inst) = val  or  rel(a, b)"
+  else
+    let funcName  := (byOpenParen.headD "").trim
+    let afterOpen := byOpenParen.tail |> String.intercalate "("
+    let byClose   := afterOpen.splitOn ")"
+    let argsStr   := (byClose.headD "").trim
+    let args      := argsStr.splitOn "," |>.map String.trim
+    let tag       := args.foldl (· ++ "_" ++ ·) funcName
+    let argStr    := String.intercalate " " args
+    let afterClose := byClose.tail |> String.intercalate ")"
+    let byEq      := afterClose.splitOn "="
+    if byEq.length >= 2 then
+      let rhs := (byEq.tail.headD "").trim
+      s!"axiom fact_{tag} : {funcName} {argStr} = {rhs}"
+    else
+      s!"axiom fact_{tag} : {funcName} {argStr}"
 
-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 genRule (name stmt : String) : String :=
+  s!"axiom {name} : {stmt}"
 
-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 genDef (name params type body : String) : String :=
+  s!"def {name} ({params}) : {type} := {body}"
 
-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."
+--------------------------------------------------------------------------------
+-- 6. Duplicate check
+--------------------------------------------------------------------------------
 
-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 isDuplicate (state : KBState) (kind name : String) : Bool :=
+  state.decls.any (fun d => d.kind == kind && d.name == name)
 
-def status : IO Unit := do
-  println "[Stub] Showing git status and unverified changes."
+--------------------------------------------------------------------------------
+-- 7. Add handlers  (domain is always explicit — no auto-classification)
+--------------------------------------------------------------------------------
 
-def initKB (dir : String) : IO Unit := do
-  println s!"[Stub] Initializing new knowledge base in '{dir}'"
-  println "  Would create directory structure and lakefile.lean."
+def addType (stateRef : IO.Ref KBState) (name : String) (parent : Option String)
+    (domain : String) : IO Unit := do
+  let state ← stateRef.get
+  if isDuplicate state "type" name then
+    println s!"Error: type '{name}' already exists."; return
+  let lean := genType name parent
+  appendToDomain state.root domain lean
+  stateRef.modify fun s => { s with decls := s.decls.push { kind := "type", name, lean, domain } }
+  let ext := parent.map (fun p => s!" (extends {p})") |>.getD ""
+  println s!"Added type '{name}'{ext}  →  {domain}.lean"
+
+def addInstance (stateRef : IO.Ref KBState) (name typeName domain : String) : IO Unit := do
+  let state ← stateRef.get
+  if isDuplicate state "instance" name then
+    println s!"Error: instance '{name}' already exists."; return
+  let lean := genInstance name typeName
+  appendToDomain state.root domain lean
+  stateRef.modify fun s => { s with decls := s.decls.push { kind := "instance", name, lean, domain } }
+  println s!"Added instance '{name} : {typeName}'  →  {domain}.lean"
+
+def addProp (stateRef : IO.Ref KBState) (name domType range domain : String) : IO Unit := do
+  let state ← stateRef.get
+  if isDuplicate state "prop" name then
+    println s!"Error: property '{name}' already exists."; return
+  let lean := genProp name domType range
+  appendToDomain state.root domain lean
+  stateRef.modify fun s => { s with decls := s.decls.push { kind := "prop", name, lean, domain } }
+  println s!"Added property '{name} : {domType} → {range}'  →  {domain}.lean"
+
+def addRel (stateRef : IO.Ref KBState) (name dom1 dom2 domain : String) : IO Unit := do
+  let state ← stateRef.get
+  if isDuplicate state "rel" name then
+    println s!"Error: relation '{name}' already exists."; return
+  let lean := genRel name dom1 dom2
+  appendToDomain state.root domain lean
+  stateRef.modify fun s => { s with decls := s.decls.push { kind := "rel", name, lean, domain } }
+  println s!"Added relation '{name} : {dom1} → {dom2} → Prop'  →  {domain}.lean"
+
+def addFact (stateRef : IO.Ref KBState) (fact domain : String) : IO Unit := do
+  let state ← stateRef.get
+  let declName := "fact:" ++ fact
+  if isDuplicate state "fact" declName then
+    println s!"Warning: fact already exists: {fact}"; return
+  let lean := genFact fact
+  appendToDomain state.root domain lean
+  let newDecl : KBDecl := { kind := "fact", name := declName, lean, domain }
+  stateRef.modify fun s => { s with decls := s.decls.push newDecl }
+  println s!"Added fact: {fact}  →  {domain}.lean"
+
+def addRule (stateRef : IO.Ref KBState) (name stmt domain : String) : IO Unit := do
+  let state ← stateRef.get
+  if isDuplicate state "rule" name then
+    println s!"Error: rule '{name}' already exists."; return
+  let lean := genRule name stmt
+  appendToDomain state.root domain lean
+  stateRef.modify fun s => { s with decls := s.decls.push { kind := "rule", name, lean, domain } }
+  println s!"Added rule '{name}'  →  {domain}.lean"
+
+def addDef (stateRef : IO.Ref KBState) (name params type body domain : String) : IO Unit := do
+  let state ← stateRef.get
+  if isDuplicate state "def" name then
+    println s!"Error: definition '{name}' already exists. Use 'rm {name}' first."; return
+  let lean := genDef name params type body
+  appendToDomain state.root domain lean
+  stateRef.modify fun s => { s with decls := s.decls.push { kind := "def", name, lean, domain } }
+  println s!"Added definition '{name} ({params}) : {type} := {body}'  →  {domain}.lean"
 
 --------------------------------------------------------------------------------
--- 4. Domain hierarchy (extracted from the original help text)
+-- 8. Remove handler
 --------------------------------------------------------------------------------
 
-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"
+def removeDecl (stateRef : IO.Ref KBState) (name : String) : IO Unit := do
+  let state ← stateRef.get
+  let targets := state.decls.filter (fun d => d.name == name)
+  if targets.isEmpty then
+    println s!"Error: '{name}' not found."; return
+  let dependents := state.decls.filter (fun d =>
+    d.name != name && strContains d.lean name)
+  unless dependents.isEmpty do
+    println s!"Warning: these declarations reference '{name}':"
+    for dep in dependents do
+      println s!"  [{dep.kind}] {dep.name}"
+    println "Remove dependents first for a consistent KB."
+  stateRef.modify fun s => { s with decls := s.decls.filter (fun d => d.name != name) }
+  let domains := dedupStrings (targets.map (·.domain)).toList
+  for domain in domains do
+    let path := domainPath state.root domain
+    if ← path.pathExists then
+      let contents ← IO.FS.readFile path
+      let kept := contents.splitOn "\n" |>.filter (fun l => !strContains l name)
+      IO.FS.writeFile path (String.intercalate "\n" kept)
+  println s!"Removed '{name}'."
 
 --------------------------------------------------------------------------------
--- 5. Help text (now includes the new commands)
+-- 9. List / ShowDef
 --------------------------------------------------------------------------------
 
-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"
+def normKind (w : String) : String :=
+  if      w == "types"     then "type"
+  else if w == "instances" then "instance"
+  else if w == "props"     then "prop"
+  else if w == "rels"      then "rel"
+  else if w == "facts"     then "fact"
+  else if w == "rules"     then "rule"
+  else if w == "defs"      then "def"
+  else w
+
+def listDecls (stateRef : IO.Ref KBState) (what : String) (filter : Option String) : IO Unit := do
+  let state ← stateRef.get
+  let nk := normKind what
+  let matchKind : KBDecl → Bool :=
+    if nk == "all" then fun _ => true else fun d => d.kind == nk
+  let matchFilter : KBDecl → Bool :=
+    match filter with
+    | none   => fun _ => true
+    | some f =>
+        let fl := strToLower f
+        fun d =>
+          strContains (strToLower d.name)   fl ||
+          strContains (strToLower d.domain) fl ||
+          strContains (strToLower d.lean)   fl
+  let hits := state.decls.filter (fun d => matchKind d && matchFilter d)
+  if hits.isEmpty then println s!"(no {what} found)"
+  else for d in hits do
+    println s!"[{d.kind}]  {d.name}   ({d.domain})"
+
+def showDef (stateRef : IO.Ref KBState) (name : String) : IO Unit := do
+  let state ← stateRef.get
+  let hits := state.decls.filter (fun d => d.name == name)
+  if hits.isEmpty then println s!"'{name}' not found."
+  else for d in hits do
+    println s!"-- [{d.kind}] {d.name}  (domain: {d.domain})"
+    println d.lean
 
 --------------------------------------------------------------------------------
--- 6. Domain command handlers
+-- 10. Eval / Query
 --------------------------------------------------------------------------------
 
-def listDomains : IO Unit := do
-  println domainHierarchy
+def buildImports (state : KBState) : IO String := do
+  let domains := dedupStrings (state.decls.map (·.domain)).toList
+  let mut imports := ""
+  for domain in domains do
+    if ← (domainPath state.root domain).pathExists then
+      imports := imports ++ s!"import {domain}\n"
+  return imports
 
-def domainsStats : IO Unit := do
-  println "[Stub] Domain statistics (would show counts of types/instances per domain)"
+def runLeanSnippet (state : KBState) (snippet : String) : IO (UInt32 × String) := do
+  let imports ← buildImports state
+  let tmpPath : System.FilePath := state.root / "_kb_tmp.lean"
+  IO.FS.writeFile tmpPath (imports ++ "\n" ++ snippet ++ "\n")
+  let result ← runProc "lean" #[tmpPath.toString] (some state.root.toString)
+  try IO.FS.removeFile tmpPath catch _ => pure ()
+  return result
+
+def evalExpr (stateRef : IO.Ref KBState) (expr : String) : IO Unit := do
+  let state ← stateRef.get
+  let (code, out) ← runLeanSnippet state s!"#eval {expr}"
+  if code == 0 then println out
+  else do
+    println s!"Lean error evaluating `{expr}`:"
+    println out
+
+def queryProp (stateRef : IO.Ref KBState) (prop : String) : IO Unit := do
+  let state ← stateRef.get
+  let snippet :=
+    "set_option maxHeartbeats 4000 in\n" ++
+    s!"#check (by first | decide | aesop | simp : {prop})"
+  let (code, out) ← runLeanSnippet state snippet
+  if code == 0 then
+    println "Yes (provable)"
+  else if strContains out "false" || strContains out "False" then
+    println "No (contradiction found)"
+  else do
+    println "Unknown (could not prove or disprove with decide / aesop / simp)"
+    unless out.isEmpty do println out
+
+--------------------------------------------------------------------------------
+-- 11. Build / commit / status
+--
+-- syncRootModule rewrites KnowledgeBase.lean to import every domain file that
+-- currently exists on disk, then injects `import <base>` into any domain file
+-- that references names from another domain file it knows about.
+-- This ensures `lake build` compiles the entire KB, not just the root stub.
+--------------------------------------------------------------------------------
+
+/-- Collect all domain stems that have a .lean file in the KB root. -/
+def existingDomains (root : System.FilePath) : IO (List String) := do
+  let reserved := ["KnowledgeBase", "lakefile", "_kb_tmp"]
+  let entries ← System.FilePath.readDir root
+  let stems := entries.toList.filterMap fun e =>
+    let name := e.fileName
+    if name.endsWith ".lean" then
+      let stem := name.dropRight ".lean".length
+      if reserved.contains stem then none else some stem
+    else none
+  return dedupStrings stems
+
+/-- Rewrite KnowledgeBase.lean to import all existing domain files.
+    Also prepend cross-domain imports into domain files that need them,
+    based on which domains are known to this session. -/
+def syncRootModule (root : System.FilePath) (state : KBState) : IO Unit := do
+  let allDomains ← existingDomains root
+  -- Build a mapping: domain → set of other domains it directly references.
+  -- A domain file references another if any of the *other* domain's declared
+  -- names appear in its own declaration texts.
+  for domain in allDomains do
+    let ownDecls  := state.decls.filter (fun d => d.domain == domain)
+    let otherDomains := allDomains.filter (· != domain)
+    let mut needed : List String := []
+    for other in otherDomains do
+      let otherDecls := state.decls.filter (fun d => d.domain == other)
+      -- Does any own decl's lean text mention a name from `other`?
+      let referenced := ownDecls.any fun od =>
+        otherDecls.any fun od2 => strContains od.lean od2.name
+      if referenced then needed := needed ++ [other]
+    -- Inject missing imports at the top of the domain file.
+    if !needed.isEmpty then
+      let path := domainPath root domain
+      if ← path.pathExists then
+        let contents ← IO.FS.readFile path
+        let missing := needed.filter (fun imp => !strContains contents s!"import {imp}")
+        unless missing.isEmpty do
+          let newHeader := (missing.map (fun imp => s!"import {imp}")).foldl
+            (· ++ "\n" ++ ·) ""
+          IO.FS.writeFile path (newHeader ++ "\n" ++ contents)
+  -- Rewrite the root module.
+  let mut rootContent := "-- KnowledgeBase root module (auto-generated by kb)\n\n"
+  for stem in allDomains do
+    rootContent := rootContent ++ s!"import {stem}\n"
+  IO.FS.writeFile (root / "KnowledgeBase.lean") rootContent
+
+def checkKB (stateRef : IO.Ref KBState) : IO Unit := do
+  let state ← stateRef.get
+  syncRootModule state.root state
+  println "Running `lake build`…"
+  let code ← runProcPrint "lake" #["build"] (some state.root.toString)
+  println (if code == 0 then "✓  Consistent (build succeeded)."
+                         else "✗  Build failed — see errors above.")
+
+def commitChanges (stateRef : IO.Ref KBState) (msg : String) : IO Unit := do
+  let state ← stateRef.get
+  let dir := state.root.toString
+  syncRootModule state.root state
+  println "Verifying before commit…"
+  let buildCode ← runProcPrint "lake" #["build"] (some dir)
+  if buildCode != 0 then
+    println "Commit aborted: build failed. Fix errors and retry."; return
+  let _ ← runProcPrint "git" #["add", "."] (some dir)
+  let code ← runProcPrint "git" #["commit", "-m", msg] (some dir)
+  if code == 0 then println s!"Committed: \"{msg}\""
+  else println "(Nothing new to commit — working tree clean.)"
+
+def showStatus (stateRef : IO.Ref KBState) : IO Unit := do
+  let state ← stateRef.get
+  let dir := state.root.toString
+  println "=== git status ==="
+  let _ ← runProcPrint "git" #["status", "--short"] (some dir)
+  println "\n=== session summary ==="
+  println s!"  KB root : {state.root}"
+  println s!"  decls   : {state.decls.size} declaration(s) in memory this session"
+
+--------------------------------------------------------------------------------
+-- 12. Init
+--------------------------------------------------------------------------------
+
+def initKB (dir : String) : IO Unit := do
+  let root : System.FilePath := System.FilePath.mk dir
+  let mkCode ← runProcPrint "mkdir" #["-p", dir]
+  if mkCode != 0 then println s!"Error: could not create '{dir}'."; return
+  IO.FS.writeFile (root / "lakefile.lean")
+    "import Lake\nopen Lake DSL\n\npackage KnowledgeBase where\n\nlean_lib KnowledgeBase where\n"
+  IO.FS.writeFile (root / "KnowledgeBase.lean")
+    "-- KnowledgeBase root module\n-- Run `kb check` to populate this file.\n"
+  let _ ← runProcPrint "git" #["init"]                                    (some dir)
+  let _ ← runProcPrint "git" #["add", "."]                                (some dir)
+  let _ ← runProcPrint "git" #["commit", "-m", "Initial kb scaffold"]     (some dir)
+  println s!"Initialised knowledge base in '{dir}'."
 
 --------------------------------------------------------------------------------
--- 7. Main loop
+-- 13. Domain listing / stats
 --------------------------------------------------------------------------------
 
-partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Unit := do
-  let _ := stateRef -- silence unused warning
+def listDomains (stateRef : IO.Ref KBState) : IO Unit := do
+  let state ← stateRef.get
+  let domains := dedupStrings (state.decls.map (·.domain)).toList
+  if domains.isEmpty then
+    println "(no domains in current session — use 'add … in <Domain>' to create one)"
+  else do
+    println "Domains active this session:"
+    for dom in domains do
+      let n := (state.decls.filter (fun d => d.domain == dom)).size
+      println s!"  {dom}  ({n} declaration(s))"
+
+def domainsStats (stateRef : IO.Ref KBState) : IO Unit := do
+  let state ← stateRef.get
+  let domains := dedupStrings (state.decls.map (·.domain)).toList
+  println "=== Domain statistics (current session) ==="
+  if domains.isEmpty then
+    println "  (none)"
+  else
+    for dom in domains do
+      let ds := state.decls.filter (fun d => d.domain == dom)
+      println s!"  {dom}: {ds.size} declaration(s)"
+      for k in ["type","instance","prop","rel","fact","rule","def"] do
+        let n := (ds.filter (fun d => d.kind == k)).size
+        if n > 0 then println s!"    {k}: {n}"
+  println "\n=== By kind (all domains) ==="
+  for k in ["type","instance","prop","rel","fact","rule","def"] do
+    let n := (state.decls.filter (fun d => d.kind == k)).size
+    if n > 0 then println s!"  {k}: {n}"
+  println s!"\n  Total: {state.decls.size}"
+
+--------------------------------------------------------------------------------
+-- 14. Help text
+--------------------------------------------------------------------------------
+
+def helpText : String :=
+  "Lean4 Knowledge Base CLI (kb)\n" ++
+  "Usage: <command> [arguments]\n\n" ++
+  "Every declaration must specify its destination domain file explicitly\n" ++
+  "with `in <Domain>`.  Domain names are arbitrary identifiers; each becomes\n" ++
+  "a <Domain>.lean file in the KB root.\n\n" ++
+  "Commands:\n" ++
+  "  init <dir>\n" ++
+  "      Create a new knowledge base repository in <dir>.\n\n" ++
+  "  add type <Name> [extends <Parent>] in <Domain>\n" ++
+  "      Declare a new type, optionally as a subtype of <Parent>.\n\n" ++
+  "  add instance <name> : <Type> in <Domain>\n" ++
+  "      Declare a named individual of the given type.\n\n" ++
+  "  add prop <name> : <DomType> -> <Range> in <Domain>\n" ++
+  "      Add a property mapping a type to a value type.\n\n" ++
+  "  add rel <name> : <D1> -> <D2> -> Prop in <Domain>\n" ++
+  "      Add a binary relation between two types.\n\n" ++
+  "  add fact <fact> in <Domain>\n" ++
+  "      Assert a fact.  Syntax: prop(inst) = val  or  rel(a, b).\n\n" ++
+  "  add rule <name> : <statement> in <Domain>\n" ++
+  "      Add a universally quantified axiom.\n\n" ++
+  "  add def <name> <params> : <Type> := <body> in <Domain>\n" ++
+  "      Define a reusable computed shortcut.\n\n" ++
+  "  rm <name>\n" ++
+  "      Remove a declaration (warns about dependents).\n\n" ++
+  "  list <types|instances|props|rels|facts|rules|defs|all> [of <filter>]\n" ++
+  "      List declarations, optionally filtered by name/domain/content.\n\n" ++
+  "  show def <name>\n" ++
+  "      Print the Lean source of a named declaration.\n\n" ++
+  "  eval <expr>\n" ++
+  "      Evaluate a computable Lean expression via #eval.\n\n" ++
+  "  query <prop>\n" ++
+  "      Try to prove a proposition (Yes / No / Unknown).\n\n" ++
+  "  check\n" ++
+  "      Sync imports and run lake build to verify the whole KB.\n\n" ++
+  "  commit <message>\n" ++
+  "      Verify then git-commit all changes.\n\n" ++
+  "  status\n" ++
+  "      Show git status and session summary.\n\n" ++
+  "  domains\n" ++
+  "      List all domains active in this session with declaration counts.\n\n" ++
+  "  domains stats\n" ++
+  "      Detailed breakdown of declarations per domain and kind.\n\n" ++
+  "  help    Show this message.\n" ++
+  "  exit    Quit.\n\n" ++
+  "Example workflow:\n" ++
+  "  add type Entity in Ontology\n" ++
+  "  add type Person extends Entity in Ontology\n" ++
+  "  add type Place extends Entity in Ontology\n" ++
+  "  add instance socrates : Person in People\n" ++
+  "  add prop birthYear : Person -> Nat in People\n" ++
+  "  add fact birthYear(socrates) = 470 in People\n" ++
+  "  check\n" ++
+  "  commit \"Added Socrates\"\n"
+
+--------------------------------------------------------------------------------
+-- 15. Main REPL loop
+--------------------------------------------------------------------------------
+
+partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Bool := do
   match parseCommand line with
-  | none => println "Invalid command. Type 'help' for usage."
+  | none =>
+    println s!"Unknown command: '{line}'."
+    println "Type 'help' for usage, including required 'in <Domain>' syntax."
+    return true
   | 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")
+    | .Init dir            => initKB dir
+    | .AddType n p dom     => addType     stateRef n p dom
+    | .AddInstance n t dom => addInstance stateRef n t dom
+    | .AddProp n dt rng dom => addProp    stateRef n dt rng dom
+    | .AddRel n d1 d2 dom  => addRel      stateRef n d1 d2 dom
+    | .AddFact f dom       => addFact     stateRef f dom
+    | .AddRule n s dom     => addRule     stateRef n s dom
+    | .AddDef n p t b dom  => addDef      stateRef n p t b dom
+    | .Remove n            => removeDecl  stateRef n
+    | .List w f            => listDecls   stateRef w f
+    | .ShowDef n           => showDef     stateRef n
+    | .Eval e              => evalExpr    stateRef e
+    | .Query p             => queryProp   stateRef p
+    | .Check               => checkKB     stateRef
+    | .Commit m            => commitChanges stateRef m
+    | .Status              => showStatus  stateRef
+    | .Domains             => listDomains stateRef
+    | .DomainsStats        => domainsStats stateRef
+    | .Help                => println helpText
+    | .Exit                => return false
+    return true
 
 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
+  println "Lean4 Knowledge Base CLI — type 'help' for commands, 'exit' to quit."
+  let stateRef ← IO.mkRef (KBState.mk (System.FilePath.mk ".") #[])
   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
+    unless trimmed.isEmpty do
+      let cont ← processCommand stateRef trimmed
+      unless cont do return
+    loop
   loop