UpdateHEADmaster

1 files changed, 502 insertions, 363 deletions

diff --git a/Main.lean b/Main.lean
index 86206f1..7a2e4ac 100644
--- a/Main.lean
+++ b/Main.lean
@@ -4,10 +4,6 @@ open Lean IO
 
 --------------------------------------------------------------------------------
 -- 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
@@ -22,8 +18,11 @@ inductive KBCommand where
   | Remove      (name : String)
   | List        (what : String) (filter : Option String)
   | ShowDef     (name : String)
+  | Get         (expr : String)
+  | Search      (query : String)
+  | Deps        (name : String)
   | Eval        (expr : String)
-  | Query       (prop : String)
+  | Query       (prop : String) (tactics : Option String)
   | Check
   | Commit      (msg : String)
   | Status
@@ -33,154 +32,221 @@ inductive KBCommand where
   | Exit
 deriving Repr
 
+/-- A single KB declaration.
+    Written to disk as a structured metadata comment immediately before the Lean source:
+      --@kb kind=<k> name=<n> domain=<d>
+      <lean source line(s)>
+    This lets the tool reconstruct full state on startup by scanning domain files. -/
 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)
+  lean   : String   -- Lean 4 source (may be multi-line)
+  domain : String   -- stem of the .lean file (without extension)
 deriving Repr, Inhabited
 
 structure KBState where
   root  : System.FilePath
   decls : Array KBDecl
 
+/-- Result of a command — drives exit codes in non-interactive use. -/
+structure CmdResult where
+  ok       : Bool   -- false → exit code 1
+  continue : Bool   -- false → user typed 'exit', stop the REPL
+
+def cmdOk   : CmdResult := { ok := true,  continue := true  }
+def cmdErr  : CmdResult := { ok := false, continue := true  }
+def cmdQuit : CmdResult := { ok := true,  continue := false }
+
 --------------------------------------------------------------------------------
--- 2. Lean-4-safe utility functions
+-- 2. 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
 
+/-- Split on the LAST occurrence of `sep` and return (before, after). -/
+def splitOnLast (s sep : String) : Option (String × String) :=
+  let segs := s.splitOn sep
+  if segs.length < 2 then none
+  else some
+    ((segs.dropLast |> String.intercalate sep).trim,
+     segs.getLast!.trim)
+
 --------------------------------------------------------------------------------
--- 3. Command parsing
+-- 3. Metadata format and persistence
 --
--- Every `add` command requires an explicit `in <Domain>` suffix that names the
--- destination file.  Both `→` and `->` are accepted as type arrows.
+-- Every declaration on disk is stored as:
+--   --@kb kind=<k> name=<n> domain=<d>
+--   <lean source line 1>
+--   [<lean source line 2> ...]
+--   (blank line)
 --
--- 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>
+-- Parsing all domain files on startup fully reconstructs KBState.decls.
+--------------------------------------------------------------------------------
+
+def metaPrefix : String := "--@kb "
+
+def encodeMetaLine (d : KBDecl) : String :=
+  s!"{metaPrefix}kind={d.kind} name={d.name} domain={d.domain}"
+
+/-- Parse a "--@kb ..." header. Returns (kind, name, domain) or none. -/
+def parseMetaLine (line : String) : Option (String × String × String) := do
+  guard (line.startsWith metaPrefix)
+  let fields := (line.drop metaPrefix.length).splitOn " "
+  let mut kind := ""; let mut name := ""; let mut domain := ""
+  for f in fields do
+    if f.startsWith "kind="   then kind   := f.drop "kind=".length
+    if f.startsWith "name="   then name   := f.drop "name=".length
+    if f.startsWith "domain=" then domain := f.drop "domain=".length
+  if kind.isEmpty || name.isEmpty || domain.isEmpty then none
+  else some (kind, name, domain)
+
+/-- Extract all --@kb-annotated declarations from the text of one domain file. -/
+def parseDomainFile (contents : String) : Array KBDecl :=
+  let lines := contents.splitOn "\n"
+  let mut decls : Array KBDecl := #[]
+  let mut i := 0
+  while i < lines.length do
+    match parseMetaLine lines[i]! with
+    | none => i := i + 1
+    | some (kind, name, domain) =>
+        i := i + 1
+        let mut leanLines : List String := []
+        while i < lines.length && !(lines[i]!.startsWith metaPrefix) do
+          leanLines := leanLines ++ [lines[i]!]
+          i := i + 1
+        let lean :=
+          (leanLines.reverse.dropWhile String.isEmpty).reverse
+          |> String.intercalate "\n"
+        decls := decls.push { kind, name, lean, domain }
+  decls
+
+/-- Scan all domain .lean files in `root` and reconstruct the declaration list. -/
+def loadState (root : System.FilePath) : IO (Array KBDecl) := do
+  let reserved := ["KnowledgeBase", "lakefile", "_kb_tmp"]
+  let entries  ← System.FilePath.readDir root
+  let stems := entries.toList.filterMap fun e =>
+    let fname := e.fileName
+    if fname.endsWith ".lean" then
+      let stem := fname.dropRight ".lean".length
+      if reserved.contains stem then none else some stem
+    else none
+  let mut all : Array KBDecl := #[]
+  for stem in dedupStrings stems do
+    let path := root / (stem ++ ".lean")
+    if ← path.pathExists then
+      all := all ++ parseDomainFile (← IO.FS.readFile path)
+  return all
+
+--------------------------------------------------------------------------------
+-- 4. Command parsing
 --------------------------------------------------------------------------------
 
 def parseCommand (line : String) : Option KBCommand :=
-  -- 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
+  let raw   := line.trim
   match parts with
-  -- ── init ────────────────────────────────────────────────────────────────
   | ["init", dir] => some (.Init dir)
-  -- ── add type ────────────────────────────────────────────────────────────
+  -- 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
   | ["add", "instance", name, ":", ty, "in", dom] =>
       some (.AddInstance name ty dom)
-  -- ── add prop ────────────────────────────────────────────────────────────
+  -- add prop
   | ["add", "prop", name, ":", dt, "->", rng, "in", dom] =>
       some (.AddProp name dt rng dom)
-  -- ── add rel ─────────────────────────────────────────────────────────────
+  -- 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  (suffix style — last " in " is the domain separator)
   | "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) ─────────────────────────────────────────────
+      match splitOnLast (raw.drop "add fact ".length) " in " with
+      | some (fact, dom) => some (.AddFact fact dom)
+      | none             => none
+  -- add rule
   | "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>
+      match splitOnLast afterColon " in " with
+      | some (stmt, dom) => some (.AddRule name stmt dom)
+      | none             => none
+  -- add def
   | "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
+      let afterName := raw.drop ("add def " ++ name ++ " ").length
+      match splitOnLast afterName " in " with
+      | none => none
+      | some (defBody, dom) =>
+          match splitOnLast defBody " := " with
+          | none => none
+          | some (lhs, body) =>
+              match splitOnLast lhs " : " with
+              | none => none
+              | some (params, ty) => some (.AddDef name params ty body dom)
+  -- rm
+  | ["rm", name]            => some (.Remove name)
+  -- list
+  | ["list", what]          => some (.List what none)
+  | ["list", what, "of", f] => some (.List what (some f))
+  -- show / get / search / deps
+  | ["show", "def", name]   => some (.ShowDef name)
+  | "get" :: _              => some (.Get    (raw.drop "get ".length))
+  | "search" :: _           => some (.Search (raw.drop "search ".length))
+  | ["deps", name]          => some (.Deps name)
+  -- eval
+  | "eval" :: _             => some (.Eval (raw.drop "eval ".length))
+  -- query [using <tactics>]  — split on last " using "
+  | "query" :: _ =>
+      let body := raw.drop "query ".length
+      match splitOnLast body " using " with
+      | some (prop, tacs) => some (.Query prop (some tacs))
+      | none              => some (.Query body none)
+  -- build / git
+  | ["check"]               => some .Check
+  | "commit" :: _           => some (.Commit (raw.drop "commit ".length))
+  | ["status"]              => some .Status
+  -- domain info
+  | ["domains"]             => some .Domains
+  | ["domains", "stats"]    => some .DomainsStats
+  -- meta
+  | ["help"]                => some .Help
+  | ["exit"]                => some .Exit
+  | _                       => none
 
 --------------------------------------------------------------------------------
--- 4. File-system helpers
+-- 5. File-system helpers
 --------------------------------------------------------------------------------
 
 def domainPath (root : System.FilePath) (domain : String) : System.FilePath :=
   root / (domain ++ ".lean")
 
-/-- 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
+/-- Write a declaration to disk: metadata header then Lean source, then blank line. -/
+def appendToDomain (root : System.FilePath) (d : KBDecl) : IO Unit := do
+  let path := domainPath root d.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
+    IO.FS.writeFile path s!"-- Knowledge Base: {d.domain}\n\n"
+  let h ← IO.FS.Handle.mk path .append
+  h.putStrLn (encodeMetaLine d)
+  h.putStrLn d.lean
+  h.putStrLn ""
+  h.flush
 
 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
+    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
@@ -195,7 +261,7 @@ def runProcPrint (cmd : String) (args : Array String) (cwd : Option String := no
   return code
 
 --------------------------------------------------------------------------------
--- 5. Lean snippet generators
+-- 6. Lean snippet generators
 --------------------------------------------------------------------------------
 
 def genType (name : String) (parent : Option String) : String :=
@@ -215,190 +281,246 @@ def genProp (name domType range : String) : String :=
 def genRel (name dom1 dom2 : String) : String :=
   s!"opaque {name} : {dom1} → {dom2} → Prop"
 
-/-- 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 byParen := fact.splitOn "("
+  if byParen.length < 2 then
     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 s!"-- unrecognised fact: {fact}"
   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 funcName   := (byParen.headD "").trim
+    let afterOpen  := byParen.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 "="
+    let byEq       := afterClose.splitOn "="
     if byEq.length >= 2 then
-      let rhs := (byEq.tail.headD "").trim
-      s!"axiom fact_{tag} : {funcName} {argStr} = {rhs}"
+      s!"axiom fact_{tag} : {funcName} {argStr} = {(byEq.tail.headD "").trim}"
     else
       s!"axiom fact_{tag} : {funcName} {argStr}"
 
-def genRule (name stmt : String) : String :=
-  s!"axiom {name} : {stmt}"
-
-def genDef (name params type body : String) : String :=
+def genRule (name stmt : String) : String := s!"axiom {name} : {stmt}"
+def genDef  (name params type body : String) : String :=
   s!"def {name} ({params}) : {type} := {body}"
 
 --------------------------------------------------------------------------------
--- 6. Duplicate check
+-- 7. Duplicate check
 --------------------------------------------------------------------------------
 
 def isDuplicate (state : KBState) (kind name : String) : Bool :=
   state.decls.any (fun d => d.kind == kind && d.name == name)
 
 --------------------------------------------------------------------------------
--- 7. Add handlers  (domain is always explicit — no auto-classification)
+-- 8. Add handlers
 --------------------------------------------------------------------------------
 
 def addType (stateRef : IO.Ref KBState) (name : String) (parent : Option String)
-    (domain : String) : IO Unit := do
+    (domain : String) : IO CmdResult := 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"
+    println s!"Error: type '{name}' already exists."; return cmdErr
+  let d : KBDecl := { kind := "type", name, lean := genType name parent, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
+  println s!"Added type '{name}'{parent.map (" (extends " ++ · ++ ")") |>.getD ""}  →  {domain}.lean"
+  return cmdOk
 
-def addInstance (stateRef : IO.Ref KBState) (name typeName domain : String) : IO Unit := do
+def addInstance (stateRef : IO.Ref KBState) (name typeName domain : String) : IO CmdResult := 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!"Error: instance '{name}' already exists."; return cmdErr
+  let d : KBDecl := { kind := "instance", name, lean := genInstance name typeName, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
   println s!"Added instance '{name} : {typeName}'  →  {domain}.lean"
+  return cmdOk
 
-def addProp (stateRef : IO.Ref KBState) (name domType range domain : String) : IO Unit := do
+def addProp (stateRef : IO.Ref KBState) (name domType range domain : String) : IO CmdResult := 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!"Error: property '{name}' already exists."; return cmdErr
+  let d : KBDecl := { kind := "prop", name, lean := genProp name domType range, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
   println s!"Added property '{name} : {domType} → {range}'  →  {domain}.lean"
+  return cmdOk
 
-def addRel (stateRef : IO.Ref KBState) (name dom1 dom2 domain : String) : IO Unit := do
+def addRel (stateRef : IO.Ref KBState) (name dom1 dom2 domain : String) : IO CmdResult := 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!"Error: relation '{name}' already exists."; return cmdErr
+  let d : KBDecl := { kind := "rel", name, lean := genRel name dom1 dom2, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
   println s!"Added relation '{name} : {dom1} → {dom2} → Prop'  →  {domain}.lean"
+  return cmdOk
 
-def addFact (stateRef : IO.Ref KBState) (fact domain : String) : IO Unit := do
+def addFact (stateRef : IO.Ref KBState) (fact domain : String) : IO CmdResult := 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 }
+  -- The canonical name is the axiom name embedded in the generated source.
+  let axiomName :=
+    if lean.startsWith "axiom " then
+      (lean.drop "axiom ".length).splitOn " " |>.headD ("fact:" ++ fact)
+    else "fact:" ++ fact
+  if isDuplicate state "fact" axiomName then
+    println s!"Warning: fact '{axiomName}' already exists."; return cmdErr
+  let d : KBDecl := { kind := "fact", name := axiomName, lean, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
   println s!"Added fact: {fact}  →  {domain}.lean"
+  return cmdOk
 
-def addRule (stateRef : IO.Ref KBState) (name stmt domain : String) : IO Unit := do
+def addRule (stateRef : IO.Ref KBState) (name stmt domain : String) : IO CmdResult := 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!"Error: rule '{name}' already exists."; return cmdErr
+  let d : KBDecl := { kind := "rule", name, lean := genRule name stmt, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
   println s!"Added rule '{name}'  →  {domain}.lean"
+  return cmdOk
 
-def addDef (stateRef : IO.Ref KBState) (name params type body domain : String) : IO Unit := do
+def addDef (stateRef : IO.Ref KBState) (name params type body domain : String) : IO CmdResult := 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"
+    println s!"Error: definition '{name}' already exists. Use 'rm {name}' first."; return cmdErr
+  let d : KBDecl := { kind := "def", name, lean := genDef name params type body, domain }
+  appendToDomain state.root d
+  stateRef.modify fun s => { s with decls := s.decls.push d }
+  println s!"Added definition '{name}'  →  {domain}.lean"
+  return cmdOk
 
 --------------------------------------------------------------------------------
--- 8. Remove handler
+-- 9. Remove — metadata-block aware
+--
+-- Rewrites the domain file, skipping the entire --@kb block for the named decl.
+-- This is atomic and correct regardless of how many lines the Lean source spans.
 --------------------------------------------------------------------------------
 
-def removeDecl (stateRef : IO.Ref KBState) (name : String) : IO Unit := do
+def rewriteFileRemovingDecl (path : System.FilePath) (target : String) : IO Unit := do
+  if !(← path.pathExists) then return
+  let lines := (← IO.FS.readFile path).splitOn "\n"
+  let mut kept : List String := []
+  let mut i := 0
+  while i < lines.length do
+    match parseMetaLine lines[i]! with
+    | some (_, mname, _) =>
+        if mname == target then
+          -- Skip this metadata line and all following non-metadata content.
+          i := i + 1
+          while i < lines.length && !(lines[i]!.startsWith metaPrefix) do
+            i := i + 1
+          -- Skip exactly one trailing blank line if present.
+          if i < lines.length && lines[i]!.isEmpty then i := i + 1
+        else
+          kept := kept ++ [lines[i]!]
+          i := i + 1
+    | none =>
+        kept := kept ++ [lines[i]!]
+        i := i + 1
+  IO.FS.writeFile path (String.intercalate "\n" kept)
+
+def removeDecl (stateRef : IO.Ref KBState) (name : String) : IO CmdResult := 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
+    println s!"Error: '{name}' not found."; return cmdErr
   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."
+    println s!"Warning: the following declarations reference '{name}':"
+    for dep in dependents do println s!"  [{dep.kind}] {dep.name}  ({dep.domain})"
+    println "  Consider removing dependents first."
+  for domain in dedupStrings (targets.map (·.domain)).toList do
+    let _ ← rewriteFileRemovingDecl (domainPath state.root domain) name
   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}'."
+  return cmdOk
 
 --------------------------------------------------------------------------------
--- 9. List / ShowDef
+-- 10. List / ShowDef / Search / Deps / Get
 --------------------------------------------------------------------------------
 
 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
+  match w with
+  | "types" => "type" | "instances" => "instance" | "props" => "prop"
+  | "rels"  => "rel"  | "facts"     => "fact"      | "rules" => "rule"
+  | "defs"  => "def"  | _           => w
 
-def listDecls (stateRef : IO.Ref KBState) (what : String) (filter : Option String) : IO Unit := do
+def listDecls (stateRef : IO.Ref KBState) (what : String) (filter : Option String)
+    : IO CmdResult := do
   let state ← stateRef.get
   let nk := normKind what
-  let matchKind : KBDecl → Bool :=
+  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
+        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})"
+  else for d in hits do println s!"[{d.kind}]  {d.name}   ({d.domain})"
+  return cmdOk
 
-def showDef (stateRef : IO.Ref KBState) (name : String) : IO Unit := do
+def showDef (stateRef : IO.Ref KBState) (name : String) : IO CmdResult := 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
+  if hits.isEmpty then println s!"Error: '{name}' not found."; return cmdErr
+  for d in hits do
     println s!"-- [{d.kind}] {d.name}  (domain: {d.domain})"
     println d.lean
+  return cmdOk
+
+def searchDecls (stateRef : IO.Ref KBState) (query : String) : IO CmdResult := do
+  let state ← stateRef.get
+  let q := strToLower query
+  let hits := state.decls.filter fun d =>
+    strContains (strToLower d.name)   q ||
+    strContains (strToLower d.lean)   q ||
+    strContains (strToLower d.domain) q
+  if hits.isEmpty then
+    println s!"No results for '{query}'."
+  else do
+    println s!"{hits.size} result(s) for '{query}':"
+    for d in hits do
+      println s!"  [{d.kind}] {d.name}  ({d.domain})"
+      for l in d.lean.splitOn "\n" do
+        if strContains (strToLower l) q then println s!"    {l.trim}"
+  return cmdOk
+
+def showDeps (stateRef : IO.Ref KBState) (name : String) : IO CmdResult := do
+  let state ← stateRef.get
+  match state.decls.find? (fun d => d.name == name) with
+  | none => println s!"Error: '{name}' not found."; return cmdErr
+  | some d =>
+    let forward := state.decls.filter fun o =>
+      o.name != name && strContains d.lean o.name
+    let reverse := state.decls.filter fun o =>
+      o.name != name && strContains o.lean name
+    println s!"Dependencies of [{d.kind}] {name}  ({d.domain}):"
+    if forward.isEmpty then println "  uses:     (none)"
+    else do
+      println "  uses:"
+      for dep in forward do println s!"    [{dep.kind}] {dep.name}  ({dep.domain})"
+    if reverse.isEmpty then println "  used by:  (none)"
+    else do
+      println "  used by:"
+      for dep in reverse do println s!"    [{dep.kind}] {dep.name}  ({dep.domain})"
+    return cmdOk
 
 --------------------------------------------------------------------------------
--- 10. Eval / Query
+-- 11. Eval / Get / Query
 --------------------------------------------------------------------------------
 
 def buildImports (state : KBState) : IO String := do
@@ -411,272 +533,289 @@ def buildImports (state : KBState) : IO String := do
 
 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 ()
+  let tmp := state.root / "_kb_tmp.lean"
+  IO.FS.writeFile tmp (imports ++ "\n" ++ snippet ++ "\n")
+  let result ← runProc "lean" #[tmp.toString] (some state.root.toString)
+  try IO.FS.removeFile tmp catch _ => pure ()
   return result
 
-def evalExpr (stateRef : IO.Ref KBState) (expr : String) : IO Unit := do
+def evalExpr (stateRef : IO.Ref KBState) (expr : String) : IO CmdResult := 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
+  if code == 0 then println out.trim; return cmdOk
+  else do println s!"Lean error evaluating '{expr}':\n{out.trim}"; return cmdErr
 
-def queryProp (stateRef : IO.Ref KBState) (prop : String) : IO Unit := do
+/-- `get <prop>(<inst>)` — evaluate a property applied to an instance.
+    Parses "prop(inst1, inst2)" → `#eval prop inst1 inst2`. -/
+def getVal (stateRef : IO.Ref KBState) (expr : String) : IO CmdResult := 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
+  let evalStr :=
+    let byParen := expr.splitOn "("
+    if byParen.length >= 2 then
+      let func := (byParen.headD "").trim
+      let args := ((byParen.tail |> String.intercalate "(").splitOn ")").headD "" |>.trim
+      let argList := args.splitOn "," |>.map String.trim |> String.intercalate " "
+      s!"{func} {argList}"
+    else expr
+  let (code, out) ← runLeanSnippet state s!"#eval {evalStr}"
+  if code == 0 then println out.trim; return cmdOk
+  else do println s!"Error evaluating '{expr}':\n{out.trim}"; return cmdErr
+
+/-- Enhanced query with optional user-supplied tactic and proof term output.
+    Syntax: query <prop> [using <tactic-script>]
+    Default tactics: first | decide | aesop | simp
+    On success: prints "Status: Yes" and the proof term via #print.
+    On failure: prints "Status: No" or "Status: Unknown" with the Lean error. -/
+def queryProp (stateRef : IO.Ref KBState) (prop : String) (tactics : Option String)
+    : IO CmdResult := do
+  let state  ← stateRef.get
+  let tacs   := tactics.getD "first | decide | aesop | simp"
+  let pname  := "_kb_proof"
+  let thm    := s!"set_option maxHeartbeats 8000 in\ntheorem {pname} : {prop} := by {tacs}"
+  let (code, out) ← runLeanSnippet state thm
   if code == 0 then
-    println "Yes (provable)"
-  else if strContains out "false" || strContains out "False" then
-    println "No (contradiction found)"
+    -- Also fetch the proof term.
+    let (_, printOut) ← runLeanSnippet state (thm ++ s!"\n#print {pname}")
+    println s!"Status: Yes"
+    println s!"Tactic: {tacs}"
+    let proofLine := printOut.trim
+    unless proofLine.isEmpty do println s!"Proof:\n{proofLine}"
+    return cmdOk
+  else if strContains out "false" || strContains out "False" ||
+          strContains out "contradiction" then do
+    println s!"Status: No"
+    println s!"Tactic: {tacs}"
+    println s!"Lean output:\n{out.trim}"
+    return cmdErr
   else do
-    println "Unknown (could not prove or disprove with decide / aesop / simp)"
-    unless out.isEmpty do println out
+    println s!"Status: Unknown"
+    println s!"Tactic: {tacs}"
+    println s!"Lean output:\n{out.trim}"
+    return cmdErr
 
 --------------------------------------------------------------------------------
--- 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.
+-- 12. Build / Commit / Status
 --------------------------------------------------------------------------------
 
-/-- 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
+  let entries  ← System.FilePath.readDir root
+  return dedupStrings <| entries.toList.filterMap fun e =>
+    let fname := e.fileName
+    if fname.endsWith ".lean" then
+      let stem := fname.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 ownDecls := state.decls.filter (fun d => d.domain == domain)
+    let others   := allDomains.filter (· != domain)
     let mut needed : List String := []
-    for other in otherDomains do
+    for other in others 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 ownDecls.any fun od => otherDecls.any fun od2 => strContains od.lean od2.name then
+        needed := needed ++ [other]
     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
+          let header := missing.map (fun imp => s!"import {imp}") |> String.intercalate "\n"
+          IO.FS.writeFile path (header ++ "\n\n" ++ contents)
+  let mut root' := "-- KnowledgeBase root module (auto-generated)\n\n"
+  for stem in allDomains do root' := root' ++ s!"import {stem}\n"
+  IO.FS.writeFile (root / "KnowledgeBase.lean") root'
 
-def checkKB (stateRef : IO.Ref KBState) : IO Unit := do
+def checkKB (stateRef : IO.Ref KBState) : IO CmdResult := 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.")
+  if code == 0 then println "✓  Consistent (build succeeded)."; return cmdOk
+  else do println "✗  Build failed — see errors above."; return cmdErr
 
-def commitChanges (stateRef : IO.Ref KBState) (msg : String) : IO Unit := do
+def commitChanges (stateRef : IO.Ref KBState) (msg : String) : IO CmdResult := 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
+    println "Commit aborted: build failed."; return cmdErr
   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.)"
+  if code == 0 then println s!"Committed: \"{msg}\""; return cmdOk
+  else do println "(Nothing to commit — working tree clean.)"; return cmdOk
 
-def showStatus (stateRef : IO.Ref KBState) : IO Unit := do
+def showStatus (stateRef : IO.Ref KBState) : IO CmdResult := 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"
+  let _ ← runProcPrint "git" #["status", "--short"] (some state.root.toString)
+  println "\n=== knowledge base ==="
+  println s!"  root  : {state.root}"
+  println s!"  decls : {state.decls.size} loaded"
+  let domains := dedupStrings (state.decls.map (·.domain)).toList
+  for dom in domains do
+    let n := (state.decls.filter (fun d => d.domain == dom)).size
+    println s!"  {dom}: {n}"
+  return cmdOk
 
 --------------------------------------------------------------------------------
--- 12. Init
+-- 13. Init
 --------------------------------------------------------------------------------
 
-def initKB (dir : String) : IO Unit := do
+def initKB (dir : String) : IO CmdResult := 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
+  if (← runProcPrint "mkdir" #["-p", dir]) != 0 then
+    println s!"Error: could not create '{dir}'."; return cmdErr
   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)
+  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}'."
+  return cmdOk
 
 --------------------------------------------------------------------------------
--- 13. Domain listing / stats
+-- 14. Domain info
 --------------------------------------------------------------------------------
 
-def listDomains (stateRef : IO.Ref KBState) : IO Unit := do
-  let state ← stateRef.get
+def listDomains (stateRef : IO.Ref KBState) : IO CmdResult := 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)"
+  if domains.isEmpty then println "(no domains loaded — use 'add … in <Domain>' to create one)"
   else do
-    println "Domains active this session:"
+    println "Domains:"
     for dom in domains do
       let n := (state.decls.filter (fun d => d.domain == dom)).size
       println s!"  {dom}  ({n} declaration(s))"
+  return cmdOk
 
-def domainsStats (stateRef : IO.Ref KBState) : IO Unit := do
-  let state ← stateRef.get
+def domainsStats (stateRef : IO.Ref KBState) : IO CmdResult := 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) ==="
+  println "=== Domain statistics ==="
+  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}"
+    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 ==="
   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}"
+  return cmdOk
 
 --------------------------------------------------------------------------------
--- 14. Help text
+-- 15. Help
 --------------------------------------------------------------------------------
 
 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" ++
+  "All `add` commands require `in <Domain>` — each domain is a <Domain>.lean file.\n\n" ++
+  "ADD\n" ++
+  "  add type <n> [extends <Parent>] in <D>\n" ++
+  "  add instance <n> : <Type> in <D>\n" ++
+  "  add prop <n> : <DomType> -> <Range> in <D>\n" ++
+  "  add rel <n> : <D1> -> <D2> -> Prop in <D>\n" ++
+  "  add fact <fact> in <D>          prop(inst) = val  or  rel(a, b)\n" ++
+  "  add rule <n> : <statement> in <D>\n" ++
+  "  add def <n> <params> : <Type> := <body> in <D>\n\n" ++
+  "READ\n" ++
+  "  list <types|instances|props|rels|facts|rules|defs|all> [of <Domain>]\n" ++
+  "  show def <n>           Lean source of a declaration.\n" ++
+  "  get <prop>(<inst>)     Retrieve a property value (runs #eval).\n" ++
+  "  search <text>          Full-text search across names, Lean source, domains.\n" ++
+  "  deps <n>               Forward and reverse dependency graph for a declaration.\n" ++
+  "  eval <expr>            Run #eval on a Lean expression.\n\n" ++
+  "QUERY\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" ++
+  "  query <prop> using <tactic-script>\n" ++
+  "      Attempt to prove a proposition.  Default tactics: first | decide | aesop | simp\n" ++
+  "      Returns Status: Yes / No / Unknown and the proof term on success.\n\n" ++
+  "BUILD & GIT\n" ++
+  "  check                  Sync imports + lake build to verify whole KB.\n" ++
+  "  commit <message>       Verify then git-commit all changes.\n" ++
+  "  status                 git status + domain summary.\n" ++
+  "  rm <n>                 Remove a declaration (warns about dependents).\n\n" ++
+  "DOMAINS\n" ++
+  "  domains                List domains with declaration counts.\n" ++
+  "  domains stats          Breakdown per domain and kind.\n\n" ++
+  "  init <dir>             Create a new KB repository.\n" ++
+  "  help | exit\n\n" ++
+  "EXIT CODES  0 = success   1 = error\n\n" ++
+  "PERSISTENCE  State is stored as --@kb metadata in each domain file and\n" ++
+  "             reloaded automatically on startup.\n\n" ++
+  "EXAMPLE\n" ++
+  "  add type Entity in People\n" ++
+  "  add type Person extends Entity in People\n" ++
   "  add instance socrates : Person in People\n" ++
   "  add prop birthYear : Person -> Nat in People\n" ++
   "  add fact birthYear(socrates) = 470 in People\n" ++
+  "  get birthYear(socrates)\n" ++
+  "  deps birthYear\n" ++
+  "  search socrates\n" ++
+  "  query birthYear socrates = 470 using decide\n" ++
   "  check\n" ++
   "  commit \"Added Socrates\"\n"
 
 --------------------------------------------------------------------------------
--- 15. Main REPL loop
+-- 16. Main REPL loop
 --------------------------------------------------------------------------------
 
-partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Bool := do
+partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO CmdResult := do
   match parseCommand line with
   | none =>
-    println s!"Unknown command: '{line}'."
-    println "Type 'help' for usage, including required 'in <Domain>' syntax."
-    return true
+    println s!"Error: unknown command '{line}'."
+    println "  Hint: add commands require `in <Domain>`.  Run 'help' for usage."
+    return cmdErr
   | some cmd =>
     match cmd with
-    | .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
+    | .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
+    | .Get e                 => getVal      stateRef e
+    | .Search q              => searchDecls stateRef q
+    | .Deps n                => showDeps    stateRef n
+    | .Eval e                => evalExpr    stateRef e
+    | .Query p t             => queryProp   stateRef p t
+    | .Check                 => checkKB     stateRef
+    | .Commit m              => commitChanges stateRef m
+    | .Status                => showStatus  stateRef
+    | .Domains               => listDomains stateRef
+    | .DomainsStats          => domainsStats stateRef
+    | .Help                  => println helpText; return cmdOk
+    | .Exit                  => return cmdQuit
 
 partial def main : IO Unit := do
+  let root  : System.FilePath := System.FilePath.mk "."
+  let decls ← loadState root
+  let stateRef ← IO.mkRef (KBState.mk root decls)
+  if decls.size > 0 then
+    println s!"Loaded {decls.size} declaration(s) from KB."
   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
     unless trimmed.isEmpty do
-      let cont ← processCommand stateRef trimmed
-      unless cont do return
+      let result ← processCommand stateRef trimmed
+      unless result.continue do return
     loop
   loop