import DocGen4
import Lean
import Cli

open DocGen4 Lean Cli

def getTopLevelModules (p : Parsed) : IO (List String) :=  do
  let topLevelModules := p.variableArgsAs! String |>.toList
  if topLevelModules.length == 0 then
    throw <| IO.userError "No topLevelModules provided."
  return topLevelModules

def runSingleCmd (p : Parsed) : IO UInt32 := do
  let relevantModules := #[p.positionalArg! "module" |>.as! String |> String.toName]
  let gitUrl := p.positionalArg! "gitUrl" |>.as! String
  let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
  let baseConfig ← getSimpleBaseContext hierarchy
  htmlOutputResults baseConfig doc (some gitUrl) (p.hasFlag "ink")
  return 0

def runIndexCmd (_p : Parsed) : IO UInt32 := do
  let hierarchy ← Hierarchy.fromDirectory Output.basePath
  let baseConfig ← getSimpleBaseContext hierarchy
  htmlOutputIndex baseConfig
  return 0

def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
  let (doc, hierarchy) ← loadCore
  let baseConfig ← getSimpleBaseContext hierarchy
  htmlOutputResults baseConfig doc none (ink := False) 
  return 0

def runDocGenCmd (_p : Parsed) : IO UInt32 := do
  IO.println "You most likely want to use me via Lake now, check my README on Github on how to:"
  IO.println "https://github.com/leanprover/doc-gen4"
  return 0

def singleCmd := `[Cli|
  single VIA runSingleCmd;
  "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated."

  FLAGS:
    ink; "Render the files with LeanInk in addition"

  ARGS:
    module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
    gitUrl : String; "The gitUrl as computed by the Lake facet"
]

def indexCmd := `[Cli|
  index VIA runIndexCmd;
  "Index the documentation that has been generated by single."
  ARGS:
    ...topLevelModule : String; "The top level modules this documentation will be for."
]

def genCoreCmd := `[Cli|
  genCore VIA runGenCoreCmd;
  "Generate documentation for the core Lean modules: Init and Lean since they are not Lake projects"
]

def docGenCmd : Cmd := `[Cli|
  "doc-gen4" VIA runDocGenCmd; ["0.1.0"]
  "A documentation generator for Lean 4."

  SUBCOMMANDS:
    singleCmd;
    indexCmd;
    genCoreCmd
]

def main (args : List String) : IO UInt32 :=
  docGenCmd.validate args