Works

1 files changed, 208 insertions, 0 deletions

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 <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" ++
+  "  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
+