diff options
Diffstat (limited to '')
| -rw-r--r-- | Main.lean | 814 |
1 files changed, 614 insertions, 200 deletions
@@ -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 |