path: root/Main.lean

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