import Lean 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 .lean file in the KB root. -------------------------------------------------------------------------------- inductive KBCommand where | 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) | Status | 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 .lean) deriving Repr, Inhabited structure KBState where 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 -------------------------------------------------------------------------------- -- 3. Command parsing -- -- Every `add` command requires an explicit `in ` suffix that names the -- destination file. Both `→` and `->` are accepted as type arrows. -- -- Syntax: -- add type [extends ] in -- add instance : in -- add prop : -> in -- add rel : -> -> Prop in -- add fact in -- add rule : in -- add def : := in -------------------------------------------------------------------------------- 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 match parts with -- ── init ──────────────────────────────────────────────────────────────── | ["init", dir] => some (.Init dir) -- ── 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 ") | "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 : := in | "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 -------------------------------------------------------------------------------- -- 4. 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 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 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 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 -------------------------------------------------------------------------------- -- 5. Lean snippet generators -------------------------------------------------------------------------------- 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 genInstance (name typeName : String) : String := s!"opaque {name} : {typeName}" def genProp (name domType range : String) : String := s!"opaque {name} : {domType} → {range}" 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 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 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 -------------------------------------------------------------------------------- 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) -------------------------------------------------------------------------------- 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" -------------------------------------------------------------------------------- -- 8. Remove handler -------------------------------------------------------------------------------- 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}'." -------------------------------------------------------------------------------- -- 9. List / ShowDef -------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------- -- 10. Eval / Query -------------------------------------------------------------------------------- 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 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 ` 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}'." -------------------------------------------------------------------------------- -- 13. Domain listing / stats -------------------------------------------------------------------------------- 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 ' 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: [arguments]\n\n" ++ "Every declaration must specify its destination domain file explicitly\n" ++ "with `in `. Domain names are arbitrary identifiers; each becomes\n" ++ "a .lean file in the KB root.\n\n" ++ "Commands:\n" ++ " init \n" ++ " Create a new knowledge base repository in .\n\n" ++ " add type [extends ] in \n" ++ " Declare a new type, optionally as a subtype of .\n\n" ++ " add instance : in \n" ++ " Declare a named individual of the given type.\n\n" ++ " add prop : -> in \n" ++ " Add a property mapping a type to a value type.\n\n" ++ " add rel : -> -> Prop in \n" ++ " Add a binary relation between two types.\n\n" ++ " add fact in \n" ++ " Assert a fact. Syntax: prop(inst) = val or rel(a, b).\n\n" ++ " add rule : in \n" ++ " Add a universally quantified axiom.\n\n" ++ " add def : := in \n" ++ " Define a reusable computed shortcut.\n\n" ++ " rm \n" ++ " Remove a declaration (warns about dependents).\n\n" ++ " list [of ]\n" ++ " List declarations, optionally filtered by name/domain/content.\n\n" ++ " show def \n" ++ " Print the Lean source of a named declaration.\n\n" ++ " eval \n" ++ " Evaluate a computable Lean expression via #eval.\n\n" ++ " query \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 \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 s!"Unknown command: '{line}'." println "Type 'help' for usage, including required 'in ' syntax." return true | 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 partial def main : IO Unit := do 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 loop loop