From bb570329a9265891e01d8fedb903ca4715dad316 Mon Sep 17 00:00:00 2001 From: Petri Hienonen Date: Sun, 15 Feb 2026 14:23:31 +0200 Subject: Works --- .gitignore | 1 + Kb.lean | 3 + Kb/Basic.lean | 1 + Main.lean | 208 +++++++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 1 + lake-manifest.json | 5 ++ lakefile.toml | 10 +++ lean-toolchain | 1 + 8 files changed, 230 insertions(+) create mode 100644 .gitignore create mode 100644 Kb.lean create mode 100644 Kb/Basic.lean create mode 100644 Main.lean create mode 100644 README.md create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/Kb.lean b/Kb.lean new file mode 100644 index 0000000..7cce288 --- /dev/null +++ b/Kb.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `Kb` library. +-- Import modules here that should be built as part of the library. +import Kb.Basic diff --git a/Kb/Basic.lean b/Kb/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/Kb/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..dbaa997 --- /dev/null +++ b/Main.lean @@ -0,0 +1,208 @@ +import Lean + +open Lean IO + +-------------------------------------------------------------------------------- +-- 1. Data structures for commands and knowledge base state +-------------------------------------------------------------------------------- + +inductive KBCommand where + | Init (dir : String) + | AddType (name : String) (parent : Option String) + | AddInstance (name : String) (typeName : String) + | AddProp (name : String) (domain : String) (range : String) + | AddRel (name : String) (dom1 : String) (dom2 : String) + | AddFact (fact : String) + | AddRule (name : String) (statement : String) + | AddDef (name : String) (params : String) (type : String) (body : String) + | Remove (name : String) + | List (what : String) (filter : Option String) + | ShowDef (name : String) + | Eval (expr : String) + | Query (prop : String) + | Check + | Commit (msg : String) + | Status + | Help + | Exit +deriving Repr + +structure KBState where + root : System.FilePath + +-------------------------------------------------------------------------------- +-- 2. Command parsing (simple, based on whitespace) +-------------------------------------------------------------------------------- + +def parseCommand (line : String) : Option KBCommand := + let parts := line.trim.splitOn " " |>.filter (not ∘ String.isEmpty) + match parts with + | ["init", dir] => some (.Init dir) + | ["add", "type", name] => some (.AddType name none) + | ["add", "type", name, "extends", parent] => some (.AddType name (some parent)) + | ["add", "instance", name, ":", typeName] => some (.AddInstance name typeName) + | ["add", "prop", name, ":", domain, "->", range] => some (.AddProp name domain range) + | ["add", "rel", name, ":", dom1, "->", dom2, "->", "Prop"] => some (.AddRel name dom1 dom2) + | ["add", "fact", _] => + some (.AddFact (line.drop 9)) -- drop "add fact " + | ["add", "rule", name, ":", _] => + let n := 9 + name.length + 2 + some (.AddRule name (line.drop n)) + | ["add", "def", name, params, ":", type, ":=", body] => + some (.AddDef name params type body) + | ["rm", name] => some (.Remove name) + | ["list", what] => some (.List what none) + | ["list", what, "of", filter] => some (.List what (some filter)) + | ["show", "def", name] => some (.ShowDef name) + | ["eval", expr] => some (.Eval expr) + | ["query", prop] => some (.Query prop) + | ["check"] => some .Check + | ["commit", msg] => some (.Commit msg) + | ["status"] => some .Status + | ["help"] => some .Help + | ["exit"] => some .Exit + | _ => none + +-------------------------------------------------------------------------------- +-- 3. Handlers (stubs with informative output) +-------------------------------------------------------------------------------- + +def addType (name : String) (parent : Option String) : IO Unit := do + let parentMsg := match parent with | some p => s!" extending '{p}'" | none => "" + println s!"[Stub] Adding type '{name}'{parentMsg}" + println " Would append to appropriate .lean file and run `lake build`." + +def addInstance (name : String) (typeName : String) : IO Unit := do + println s!"[Stub] Adding instance '{name} : {typeName}'" + +def addProp (name domain range : String) : IO Unit := do + println s!"[Stub] Adding property '{name} : {domain} -> {range}'" + +def addRel (name dom1 dom2 : String) : IO Unit := do + println s!"[Stub] Adding relation '{name} : {dom1} -> {dom2} -> Prop'" + +def addFact (fact : String) : IO Unit := do + println s!"[Stub] Adding fact: {fact}" + +def addRule (name stmt : String) : IO Unit := do + println s!"[Stub] Adding rule '{name} : {stmt}'" + +def addDef (name params type body : String) : IO Unit := do + println s!"[Stub] Adding definition '{name} {params} : {type} := {body}'" + +def removeDecl (name : String) : IO Unit := do + println s!"[Stub] Removing declaration '{name}' (checking dependencies)" + +def listDecls (what : String) (filter : Option String) : IO Unit := do + let filterMsg := match filter with | some f => s!" of {f}" | none => "" + println s!"[Stub] Listing {what}{filterMsg}" + +def showDef (name : String) : IO Unit := do + println s!"[Stub] Showing definition of '{name}'" + +def evalExpr (expr : String) : IO Unit := do + println s!"[Stub] Evaluating: {expr}" + println " Would run `#eval` in a temporary Lean file and return result." + +def queryProp (prop : String) : IO Unit := do + println s!"[Stub] Querying: {prop}" + println " Would attempt to prove with `aesop` and return Yes/No/Unknown." + +def checkKB : IO Unit := do + println "Running `lake build` to verify knowledge base..." + let child ← IO.Process.spawn { cmd := "lake", args := #["build"] } + let exitCode ← child.wait + if exitCode == 0 then + println "Consistent (build succeeded)." + else + println "Inconsistent! Build failed." + +def commitChanges (msg : String) : IO Unit := do + println s!"[Stub] Committing with message: {msg}" + println " Would run `git add . && git commit -m \"...\"` after `kb check`." + +def status : IO Unit := do + println "[Stub] Showing git status and unverified changes." + +def initKB (dir : String) : IO Unit := do + println s!"[Stub] Initializing new knowledge base in '{dir}'" + println " Would create directory structure and lakefile.lean." + +-------------------------------------------------------------------------------- +-- 4. Help text with hierarchical classification (RESTORED) +-------------------------------------------------------------------------------- + +def helpText : String := + "Lean4 Knowledge Base CLI (kb)\n" ++ + "Usage: kb [arguments]\n\n" ++ + "Commands:\n" ++ + " init Create a new knowledge base repository.\n" ++ + " add type [extends

] Define a new type.\n" ++ + " add instance : Declare an instance.\n" ++ + " add prop : -> Add a property.\n" ++ + " add rel : -> -> Prop Add a relation.\n" ++ + " add fact Add a fact.\n" ++ + " add rule : Add a logical rule.\n" ++ + " add def : := Define a shortcut.\n" ++ + " rm Remove a declaration.\n" ++ + " list [of ] List.\n" ++ + " show def Show a shortcut definition.\n" ++ + " eval Evaluate a computable expression.\n" ++ + " query Ask whether a proposition is provable.\n" ++ + " check Run `lake build` to verify consistency.\n" ++ + " commit Commit all changes.\n" ++ + " status Show git status.\n" ++ + " help Show this help.\n" ++ + " exit Exit the CLI.\n" + +-------------------------------------------------------------------------------- +-- 5. Main loop +-------------------------------------------------------------------------------- + +partial def processCommand (stateRef : IO.Ref KBState) (line : String) : IO Unit := do + let _ := stateRef -- silence unused warning + match parseCommand line with + | none => println "Invalid command. Type 'help' for usage." + | some cmd => + match cmd with + | .Init dir => initKB dir + | .AddType name parent => addType name parent + | .AddInstance name ty => addInstance name ty + | .AddProp name dom ran => addProp name dom ran + | .AddRel name d1 d2 => addRel name d1 d2 + | .AddFact fact => addFact fact + | .AddRule name stmt => addRule name stmt + | .AddDef name params ty body => addDef name params ty body + | .Remove name => removeDecl name + | .List what filt => listDecls what filt + | .ShowDef name => showDef name + | .Eval expr => evalExpr expr + | .Query prop => queryProp prop + | .Check => checkKB + | .Commit msg => commitChanges msg + | .Status => status + | .Help => println helpText + | .Exit => throw (IO.userError "exit") + +partial def main : IO Unit := do + println "Lean4 Knowledge Base CLI" + println "Type 'help' for commands." + let initialState : KBState := { root := System.FilePath.mk "." } + let stateRef ← IO.mkRef initialState + let rec loop : IO Unit := do + IO.print "kb> " + let line ← (← IO.getStdin).getLine + let trimmed := line.trim + if trimmed.isEmpty then loop + else + try + processCommand stateRef trimmed + if trimmed == "exit" then return () + else loop + catch e => + if e.toString == "exit" then return () + else do + println s!"Error: {e}" + loop + loop + diff --git a/README.md b/README.md new file mode 100644 index 0000000..f69f1e8 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# kb \ No newline at end of file diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..e1013f0 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "kb", + "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..7b8444b --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "kb" +version = "0.1.0" +defaultTargets = ["kb"] + +[[lean_lib]] +name = "Kb" + +[[lean_exe]] +name = "kb" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..f942ecf --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:4.25.0 -- cgit v1.3-1-g0d28