lean4game/server/GameServer/Commands.lean

import GameServer.Helpers
import GameServer.Inventory
import GameServer.Options
import GameServer.SaveData

open Lean Meta Elab Command

set_option autoImplicit false

/-! # Game metadata -/

/-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
elab "Game" n:str : command => do
  let name := n.getString
  setCurGameId name
  if (← getGame? name).isNone then
    insertGame name {name}

/-- Create a new world in the active game. Example: `World "Addition"` -/
elab "World" n:str : command => do
  let name := n.getString
  setCurWorldId name
  if ¬ (← getCurGame).worlds.nodes.contains name then
    addWorld {name}

/-- Define the current level number. Levels inside a world must be
numbered consecutive starting with `1`. Example: `Level 1` -/
elab "Level" level:num : command => do
  let level := level.getNat
  setCurLevelIdx level
  addLevel {index := level}

/-- Define the title of the current game/world/level. -/
elab "Title" t:str : command => do
  match ← getCurLayer with
  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
  | .Game => modifyCurGame  fun game => pure {game with
      title := t.getString
      tile := {game.tile with title := t.getString}}

/-- Define the introduction of the current game/world/level. -/
elab "Introduction" t:str : command => do
  let intro := t.getString
  match ← getCurLayer with
  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
  | .Game => modifyCurGame  fun game => pure {game with introduction := intro}

/-- Define the info of the current game. Used for e.g. credits -/
elab "Info" t:str : command => do
  let info:= t.getString
  match ← getCurLayer with
  | .Level =>
    logError "Can't use `Info` in a level!"
    pure ()
  | .World =>
    logError "Can't use `Info` in a world"
    pure ()
  | .Game => modifyCurGame  fun game => pure {game with info := info}

/-- Provide the location of the image for the current game/world/level.
Paths are relative to the lean project's root. -/
elab "Image" t:str : command => do
  let file := t.getString
  if not <| ← System.FilePath.pathExists file then
    logWarningAt t s!"Make sure the cover image '{file}' exists."
  if not <| file.startsWith "images/" then
    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."

  match ← getCurLayer with
  | .Level =>
    logWarning "Level-images not implemented yet" -- TODO
    modifyCurLevel fun level => pure {level with image := file}
  | .World =>
    modifyCurWorld  fun world => pure {world with image := file}
  | .Game =>
    logWarning "Main image of the game not implemented yet" -- TODO
    modifyCurGame  fun game => pure {game with image := file}

/-- Define the conclusion of the current game or current level if some
building a level. -/
elab "Conclusion" t:str : command => do
  let conclusion := t.getString
  match ← getCurLayer with
  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
  | .Game => modifyCurGame  fun game => pure {game with conclusion := conclusion}

/-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/
elab "Prerequisites" t:str* : command => do
  modifyCurGame fun game => pure {game with
    tile := {game.tile with prerequisites := t.map (·.getString) |>.toList}}

/-- Short caption for the game (1 sentence) -/
elab "CaptionShort" t:str : command => do
  let caption := t.getString
  modifyCurGame fun game => pure {game with
    tile := {game.tile with short := caption}}

/-- More detailed description what the game is about (2-4 sentences). -/
elab "CaptionLong" t:str : command => do
  let caption := t.getString
  modifyCurGame fun game => pure {game with
    tile := {game.tile with long := caption}}

/-- A list of Languages the game is translated to. For example `Languages "German" "English"`.
NOTE: For the time being, only a single language is supported.
 -/
elab "Languages" t:str* : command => do
  modifyCurGame fun game => pure {game with
    tile := {game.tile with languages := t.map (·.getString) |>.toList}}

/-- The Image of the game (optional). TODO: Not impementeds -/
elab "CoverImage" t:str : command => do
  let file := t.getString
  if not <| ← System.FilePath.pathExists file then
    logWarningAt t s!"Make sure the cover image '{file}' exists."
  if not <| file.startsWith "images/" then
    logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder."

  modifyCurGame fun game => pure {game with
    tile := {game.tile with image := file}}

/-! # Inventory

The inventory contains docs for tactics, theorems, and definitions. These are all locked
in the first level and get enabled during the game.
-/

/-! ## Doc entries -/

/-- Documentation entry of a tactic. Example:

```
TacticDoc rw "`rw` stands for rewrite, etc. "
```

* The identifier is the tactics name. Some need to be escaped like `«have»`.
* The description is a string supporting Markdown.
 -/
elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
  let doc ← parseDocCommentLegacy doc content
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Tactic
    name := name.getId
    displayName := name.getId.toString
    content := doc })

/-- Documentation entry of a theorem. Example:

```
TheoremDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
```

* The first identifier is used in the commands `[New/Only/Disabled]Theorem`.
  It is preferably the true name of the theorem. However, this is not required.
* The string following `as` is the displayed name (in the Inventory).
* The identifier after `in` is the category to group theorems by (in the Inventory).
* The description is a string supporting Markdown.

Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
The theorem/definition to have the same fully qualified name as in mathlib.
 -/
elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
    command => do
  let doc ← parseDocCommentLegacy doc content
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Lemma
    name := name.getId
    category := category.getString
    displayName := displayName.getString
    content := doc })
-- TODO: Catch the following behaviour.
-- 1. if `TheoremDoc` appears in the same file as `Statement`, it will silently use
-- it but display the info that it wasn't found in `Statement`
-- 2. if it appears in a later file, however, it will silently not do anything and keep
-- the first one.


/-- Documentation entry of a definition. Example:

```
DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Surjective`, etc."
```

* The first identifier is used in the commands `[New/Only/Disabled]Definition`.
  It is preferably the true name of the definition. However, this is not required.
* The string following `as` is the displayed name (in the Inventory).
* The description is a string supporting Markdown.

Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires
The theorem/definition to have the same fully qualified name as in mathlib.
 -/
elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
  let doc ← parseDocCommentLegacy doc template
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Definition
    name := name.getId,
    displayName := displayName.getString,
    content := doc })

/-! ## Add inventory items -/

def checkCommandNotDuplicated (items : Array Name) (cmd := "Command") : CommandElabM Unit := do
  if ¬ items.isEmpty then
    logWarning s!"You should only use one `{cmd}` per level, but it takes multiple arguments: `{cmd} obj₁ obj₂ obj₃`!"

/-- Declare tactics that are introduced by this level. -/
elab "NewTactic" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).tactics.new) "NewTactic"
  for name in ↑args do
    checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]")
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId)}}

/-- Declare tactics that are introduced by this level but do not show up in inventory. -/
elab "NewHiddenTactic" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic"
  for name in ↑args do
    checkInventoryDoc .Tactic name (template := "")
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId),
                                   hidden := level.tactics.hidden ++ args.map (·.getId)}}

/-- Declare theorems that are introduced by this level. -/
elab "NewTheorem" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewTheorem"
  for name in ↑args do
    try let _decl ← getConstInfo name.getId catch
      | _ => logErrorAt name m!"unknown identifier '{name}'."
    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with new := args.map (·.getId)}}

/-- Declare definitions that are introduced by this level. -/
elab "NewDefinition" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).definitions.new) "NewDefinition"
  for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]")
  modifyCurLevel fun level => pure {level with
    definitions := {level.definitions with new := args.map (·.getId)}}

/-- Declare tactics that are temporarily disabled in this level.
This is ignored if `OnlyTactic` is set. -/
elab "DisabledTactic" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).tactics.disabled) "DisabledTactic"
  for name in ↑args do checkInventoryDoc .Tactic name
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with disabled := args.map (·.getId)}}

/-- Declare theorems that are temporarily disabled in this level.
This is ignored if `OnlyTheorem` is set. -/
elab "DisabledTheorem" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledTheorem"
  for name in ↑args  do checkInventoryDoc .Lemma name
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with disabled := args.map (·.getId)}}

/-- Declare definitions that are temporarily disabled in this level -/
elab "DisabledDefinition" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).definitions.disabled) "DisabledDefinition"
  for name in ↑args do checkInventoryDoc .Definition name
  modifyCurLevel fun level => pure {level with
    definitions := {level.definitions with disabled := args.map (·.getId)}}

/-- Temporarily disable all tactics except the ones declared here -/
elab "OnlyTactic" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).tactics.only) "OnlyTactic"
  for name in ↑args do checkInventoryDoc .Tactic name
  modifyCurLevel fun level => pure {level with
    tactics := {level.tactics with only := args.map (·.getId)}}

/-- Temporarily disable all theorems except the ones declared here -/
elab "OnlyTheorem" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyTheorem"
  for name in ↑args do checkInventoryDoc .Lemma name
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with only := args.map (·.getId)}}

/-- Temporarily disable all definitions except the ones declared here.
This is ignored if `OnlyDefinition` is set. -/
elab "OnlyDefinition" args:ident* : command => do
  checkCommandNotDuplicated ((←getCurLevel).definitions.only) "OnlyDefinition"
  for name in ↑args do checkInventoryDoc .Definition name
  modifyCurLevel fun level => pure {level with
    definitions := {level.definitions with only := args.map (·.getId)}}

/-- Define which tab of Lemmas is opened by default. Usage: `TheoremTab "Nat"`.
If omitted, the current tab will remain open. -/
elab "TheoremTab"  category:str : command =>
  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}


/-! DEPRECATED -/

elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? :
    command => do
  logWarning "Deprecated. Has been renamed to `TheoremDoc`"
  let doc ← parseDocCommentLegacy doc content
  modifyEnv (inventoryTemplateExt.addEntry · {
    type := .Lemma
    name := name.getId
    category := category.getString
    displayName := displayName.getString
    content := doc })

elab "NewLemma" args:ident* : command => do
  logWarning "Deprecated. Has been renamed to `NewTheorem`"
  checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewLemma"
  for name in ↑args do
    try let _decl ← getConstInfo name.getId catch
      | _ => logErrorAt name m!"unknown identifier '{name}'."
    checkInventoryDoc .Lemma name -- TODO: Add (template := "[mathlib]")
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with new := args.map (·.getId)}}

elab "DisabledLemma" args:ident* : command => do
  logWarning "Deprecated. Has been renamed to `DisabledTheorem`"
  checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledLemma"
  for name in ↑args  do checkInventoryDoc .Lemma name
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with disabled := args.map (·.getId)}}

elab "OnlyLemma" args:ident* : command => do
  logWarning "Deprecated. Has been renamed to `OnlyTheorem`"
  checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyLemma"
  for name in ↑args do checkInventoryDoc .Lemma name
  modifyCurLevel fun level => pure {level with
    lemmas := {level.lemmas with only := args.map (·.getId)}}

elab "LemmaTab"  category:str : command => do
  logWarning "Deprecated. Has been renamed to `TheoremTab`"
  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}

/-! # Exercise Statement -/

/-- Define the statement of the current level. -/
elab doc:docComment ? attrs:Parser.Term.attributes ?
    "Statement" statementName:ident ? sig:declSig val:declVal : command => do
  let lvlIdx ← getCurLevelIdx

  let docContent ← parseDocComment doc

  -- Save the messages before evaluation of the proof.
  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })

  -- The default name of the statement is `[Game].[World].level[no.]`, e.g. `NNG.Addition.level1`
  -- However, this should not be used when designing the game.
  let defaultDeclName : Ident := mkIdent <| (← getCurGame).name ++ (← getCurWorld).name ++
    ("level" ++ toString lvlIdx : String)

  -- Collect all used tactics/lemmas in the sample proof:
  let usedInventory ← match val with
  | `(Parser.Command.declVal| := $proof:term) => do
    collectUsedInventory proof
  | _ => throwError "expected `:=`"

  -- Add theorem to context.
  match statementName with
  | some name =>
    let env ← getEnv

    let fullName := (← getCurrNamespace) ++ name.getId

    if env.contains fullName then
      let origType := (env.constants.map₁.find! fullName).type
      -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
      -- in that case.
      logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
      m!"statement will be available in later levels:\n\n{origType}")
      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
      elabCommand thmStatement
      -- Check that statement has a docs entry.
      checkInventoryDoc .Lemma name (name := fullName) (template := docContent)

    else
      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $val)
      elabCommand thmStatement
      -- Check that statement has a docs entry.
      checkInventoryDoc .Lemma name (name := fullName) (template := docContent)

  | none =>
    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
    elabCommand thmStatement

  let msgs := (← get).messages

  let mut hints := #[]
  let mut nonHintMsgs := #[]
  for msg in msgs.msgs do
    -- Look for messages produced by the `Hint` tactic. They are used to pass information about the
    -- intermediate goal state
    if let MessageData.withNamingContext _ $ MessageData.withContext ctx $
        .tagged `Hint $
        .nest strict $
        .nest hidden $
        .compose (.ofGoal text) (.ofGoal goal) := msg.data then
      let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
        return {
          goal := ← abstractCtx goal
          text := ← instantiateMVars (mkMVar text)
          strict := strict == 1
          hidden := hidden == 1
        }
      hints := hints.push hint
    else
      nonHintMsgs := nonHintMsgs.push msg

  -- restore saved messages and non-hint messages
  modify fun st => { st with
    messages := initMsgs ++ ⟨nonHintMsgs.toPArray'⟩
  }

  let scope ← getScope
  let env ← getEnv

  -- TODO: Is this desired or would it be better to get `elabCommand` above to ignore
  -- the namespace?
  let currNamespace ← getCurrNamespace

  -- Format theorem statement for displaying
  let sigString := sig.raw.reprint.getD ""
  let descrFormat : String := match statementName with
  | some name =>  s!"theorem {name.getId} {sigString} := by"
  | none => s!"example {sigString} := by"

  modifyCurLevel fun level => pure { level with
    module := env.header.mainModule
    goal := sig,
    scope := scope,
    descrText := docContent
    statementName := match statementName with
    | none => default
    | some name => currNamespace ++ name.getId
    descrFormat := descrFormat
    hints := hints
    tactics := {level.tactics with used := usedInventory.tactics.toArray}
    definitions := {level.definitions with used := usedInventory.definitions.toArray}
    lemmas := {level.lemmas with used := usedInventory.lemmas.toArray} }

/-! # Hints -/

/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
see hints. The tactic does not affect the goal state.
-/
elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
  let mut strict := false
  let mut hidden := false

  -- remove spaces at the beginning of new lines
  let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
    match m with
    | Syntax.node info k args =>
      if k == interpolatedStrLitKind && args.size == 1 then
        match args.get! 0 with
        | (Syntax.atom info' val) =>
          let val := removeIndentation val
          return Syntax.node info k #[Syntax.atom info' val]
        | _ => return m
      else
        return m
    | _ => return m

  for arg in args do
    match arg with
    | `(hintArg| (strict := true)) => strict := true
    | `(hintArg| (strict := false)) => strict := false
    | `(hintArg| (hidden := true)) => hidden := true
    | `(hintArg| (hidden := false)) => hidden := false
    | _ => throwUnsupportedSyntax

  let goal ← Tactic.getMainGoal
  goal.withContext do
    -- We construct an expression that can produce the hint text. The difficulty is that we
    -- want the text to possibly contain quotation of the local variables which might have been
    -- named differently by the player.
    let varsName := `vars
    let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
      let mut text ← `(m! $msg)
      let goalDecl ← goal.getDecl
      let decls := goalDecl.lctx.decls.toArray.filterMap id
      for i in [:decls.size] do
        text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
      return ← mkLambdaFVars #[vars] $ ← Term.elabTermAndSynthesize text none
    let textmvar ← mkFreshExprMVar none
    guard $ ← isDefEq textmvar text -- Store the text in a mvar.
    -- The information about the hint is logged as a message using `logInfo` to transfer it to the
    -- `Statement` command:
    logInfo $
      .tagged `Hint $
      .nest (if strict then 1 else 0) $
      .nest (if hidden then 1 else 0) $
      .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)

/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
proof state. We use it to define Hints for alternative proof methods or dead ends. -/
elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
  let b ← saveState
  Tactic.evalTactic t

  -- Show an info whether the branch proofs all remaining goals.
  let gs ← Tactic.getUnsolvedGoals
  if gs.isEmpty then
    trace[debug] "This branch finishes the proof."
  else
    trace[debug] "This branch leaves open goals."

  let msgs ← Core.getMessageLog
  b.restore
  Core.setMessageLog msgs

/-- A hole inside a template proof that will be replaced by `sorry`. -/
elab (name := GameServer.Tactic.Hole) "Hole" t:tacticSeq : tactic => do
  Tactic.evalTactic t

/--
Iterate recursively through the Syntax, replace `Hole` with `sorry` and remove all
`Hint`/`Branch` occurrences.
-/
def replaceHoles (tacs : Syntax) : Syntax :=
  match tacs with
  | Syntax.node info kind ⟨args⟩ =>
    let newArgs := filterArgs args
    Syntax.node info kind ⟨newArgs⟩
  | other => other
where filterArgs (args : List Syntax) : List Syntax :=
  match args with
    | [] => []
    -- replace `Hole` with `sorry`.
    | Syntax.node info `GameServer.Tactic.Hole _ :: r =>
      Syntax.node info `Lean.Parser.Tactic.tacticSorry #[Syntax.atom info "sorry"] :: filterArgs r
    -- delete all `Hint` and `Branch` occurrences in the middle.
    | Syntax.node _ `GameServer.Tactic.Hint _ :: _ :: r
    | Syntax.node _ `GameServer.Tactic.Branch _ :: _ :: r =>
      filterArgs r
    -- delete `Hint` and `Branch` occurence at the end of the tactic sequence.
    | Syntax.node _ `GameServer.Tactic.Hint _ :: []
    | Syntax.node _ `GameServer.Tactic.Branch _ :: [] =>
        []
    -- Recurse on all other Syntax.
    | a :: rest =>
      replaceHoles a :: filterArgs rest

/-- The tactic block inside `Template` will be copied into the users editor.
Use `Hole` inside the template for a part of the proof that should be replaced
with `sorry`. -/
elab "Template" tacs:tacticSeq : tactic => do
  Tactic.evalTactic tacs
  let newTacs : TSyntax `Lean.Parser.Tactic.tacticSeq := ⟨replaceHoles tacs.raw⟩
  let template ← PrettyPrinter.ppCategory `Lean.Parser.Tactic.tacticSeq newTacs
  trace[debug] s!"Template:\n{template}"
  modifyLevel (←getCurLevelId) fun level => do
    return {level with template := s!"{template}"}


-- TODO: Notes for testing if a declaration has the simp attribute

-- -- Test: From zulip
-- section test

-- open Lean Meta Elab Command Tactic Simp

-- def Lean.Meta.SimpTheorems.hasAttribute (d : SimpTheorems) (decl : Name) :=
--   d.isLemma (.decl decl) || d.isDeclToUnfold decl

-- def isInSimpset (simpAttr decl: Name) : CoreM Bool := do
--   let .some simpDecl ←getSimpExtension? simpAttr | return false
--   return (← simpDecl.getTheorems).hasAttribute decl

-- end test

/-! # Make Game -/

/-- The worlds of a game are joint by dependencies. These are
automatically computed but can also be defined with the syntax
`Dependency World₁ → World₂ → World₃`. -/
def Parser.dependency := Parser.sepBy1Indent Parser.ident "→"

/-- Manually add a dependency between two worlds.

Normally, the dependencies are computed automatically by the
tactics & lemmas used in the example
proof and the ones introduced by `NewLemma`/`NewTactic`.
Use the command `Dependency World₁ → World₂` to add a manual edge to the graph,
for example if the only dependency between the worlds is given by
the narrative. -/
elab "Dependency" s:Parser.dependency : command => do
  let mut source? : Option Name := none
  for stx in s.raw.getArgs.getEvenElems do
    let some source := source?
      | do
          source? := some stx.getId
          continue
    let target := stx.getId
    match (← getCurGame).worlds.nodes.find? target with
    | some _ => pure ()
    | none => logErrorAt stx m!"World `{target}` seems not to exist"

    modifyCurGame fun game =>
      pure {game with worlds := {game.worlds with edges := game.worlds.edges.push (source, target)}}
    source? := some target

/-- Build the game. This command will precompute various things about the game, such as which
tactics are available in each level etc. -/
elab "MakeGame" : command => do
  let game ← getCurGame

  let env ← getEnv

  -- Now create The doc entries from the templates
  for item in inventoryTemplateExt.getState env do
    let name := item.name

    let content : String ← match item.content with
    | "" =>
      -- If documentation is missing, try using the docstring instead.
      let docstring ← getDocstring env name item.type
      match docstring with
      | some ds => pure s!"*(lean docstring)*\\\n{ds}"
      | none => pure "(missing)"
    | template =>
      -- TODO: Process content template.
      -- TODO: Add information about inventory items
      pure $ template.replace "[[mathlib_doc]]"
        s!"[mathlib doc](https://leanprover-community.github.io/mathlib4_docs/find/?pattern={name}#doc)"

    match item.type with
    | .Lemma =>
      modifyEnv (inventoryExt.addEntry · { item with
        content := content
        -- Add the lemma statement to the doc
        statement := (← getStatementString name)
      })
    | _ =>
      modifyEnv (inventoryExt.addEntry · { item with
        content := content
      })

  -- For each `worldId` this contains a set of items used in this world
  let mut usedItemsInWorld : HashMap Name (HashSet Name) := {}

  -- For each `worldId` this contains a set of items newly defined in this world
  let mut newItemsInWorld : HashMap Name (HashSet Name) := {}

  -- Items that should not be displayed in inventory
  let mut hiddenItems : HashSet Name := {}

  let allWorlds := game.worlds.nodes.toArray
  let nrWorlds := allWorlds.size
  let mut nrLevels := 0

  -- Calculate which "items" are used/new in which world
  for (worldId, world) in allWorlds do
    let mut usedItems : HashSet Name := {}
    let mut newItems : HashSet Name := {}
    for inventoryType in #[.Tactic, .Definition, .Lemma] do
      for (levelId, level) in world.levels.toArray do
        usedItems := usedItems.insertMany (level.getInventory inventoryType).used
        newItems := newItems.insertMany (level.getInventory inventoryType).new
        hiddenItems := hiddenItems.insertMany (level.getInventory inventoryType).hidden

        -- if the previous level was named, we need to add it as a new lemma
        if inventoryType == .Lemma then
          match levelId with
          | 0 => pure ()
          | 1 => pure () -- level ids start with 1, so we need to skip 1, too
          | i₀ + 1 =>
            match (world.levels.find! (i₀)).statementName with
            | .anonymous => pure ()
            | .num _ _ => panic "Did not expect to get a numerical statement name!"
            | .str pre s =>
              let name := Name.str pre s
              newItems := newItems.insert name

          if inventoryType == .Lemma then

      -- if the last level was named, we need to add it as a new lemma
      let i₀ := world.levels.size
        match (world.levels.find! (i₀)).statementName with
        | .anonymous => pure ()
        | .num _ _ => panic "Did not expect to get a numerical statement name!"
        | .str pre s =>
          let name := Name.str pre s
          newItems := newItems.insert name

    usedItemsInWorld := usedItemsInWorld.insert worldId usedItems
    newItemsInWorld := newItemsInWorld.insert worldId newItems
    -- DEBUG: print new/used items
    -- logInfo m!"{worldId} uses: {usedItems.toList}"
    -- logInfo m!"{worldId} introduces: {newItems.toList}"

    -- Moreover, count the number of levels in the game
    nrLevels := nrLevels + world.levels.toArray.size

  /- for each "item" this is a HashSet of `worldId`s that introduce this item -/
  let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
  for (worldId, _world) in allWorlds do
    for newItem in newItemsInWorld.findD worldId {} do
      worldsWithNewItem := worldsWithNewItem.insert newItem $
        (worldsWithNewItem.findD newItem {}).insert worldId

  -- For each `worldId` this is a HashSet of `worldId`s that this world depends on.
  let mut worldDependsOnWorlds : HashMap Name (HashSet Name) := {}

  -- For a pair of `worldId`s `(id₁, id₂)` this is a HasSet of "items" why `id₁` depends on `id₂`.
  let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {}

  -- Calculate world dependency graph `game.worlds`
  for (dependentWorldId, _dependentWorld) in allWorlds do
    let mut dependsOnWorlds : HashSet Name := {}
    -- Adding manual dependencies that were specified via the `Dependency` command.
    for (sourceId, targetId) in game.worlds.edges do
      if targetId = dependentWorldId then
        dependsOnWorlds := dependsOnWorlds.insert sourceId

    for usedItem in usedItemsInWorld.findD dependentWorldId {} do
      match worldsWithNewItem.find? usedItem with
      | none => logWarning m!"No world introducing {usedItem}, but required by {dependentWorldId}"
      | some worldIds =>
        -- Only need a new dependency if the world does not introduce an item itself
        if !worldIds.contains dependentWorldId then
          -- Add all worlds as dependencies which introduce this item
          -- TODO: Could do something more clever here.
          dependsOnWorlds := dependsOnWorlds.insertMany worldIds
          -- Store the dependency reasons for debugging
          for worldId in worldIds do
            let tmp := (dependencyReasons.findD (dependentWorldId, worldId) {}).insert usedItem
            dependencyReasons := dependencyReasons.insert (dependentWorldId, worldId) tmp
    worldDependsOnWorlds := worldDependsOnWorlds.insert dependentWorldId dependsOnWorlds

  -- Debugging: show all dependency reasons if the option `lean4game.showDependencyReasons` is set
  if lean4game.showDependencyReasons.get (← getOptions) then
    for (world, dependencies) in worldDependsOnWorlds.toArray do
      if dependencies.isEmpty then
        logInfo m!"Dependencies of '{world}': none"
      else
        let mut msg := m!"Dependencies of '{world}':"
        for dep in dependencies do
          match dependencyReasons.find? (world, dep) with
          | none =>
            msg := msg ++ m!"\n· '{dep}': no reason found (manually added?)"
          | some items =>
            msg := msg ++ m!"\n· '{dep}' because of:\n  {items.toList}"
        logInfo msg

  -- Check graph for loops and remove transitive edges
  let loop := findLoops worldDependsOnWorlds
  if loop != [] then
    logError m!"Loop: Dependency graph has a loop: {loop}"
    for i in [:loop.length] do
      let w1 := loop[i]!
      let w2 := loop[if i == loop.length - 1 then 0 else i + 1]!
      match dependencyReasons.find? (w1, w2) with
      -- This should not happen. Could use `find!` again...
      | none => logError m!"Did not find a reason why {w1} depends on {w2}."
      | some items =>
        logError m!"{w1} depends on {w2} because of {items.toList}."
  else
    worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds

    -- need to delete all existing edges as they are already present in `worldDependsOnWorlds`.
    modifyCurGame fun game =>
      pure {game with worlds := {game.worlds with edges := Array.empty}}

    for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do
      modifyCurGame fun game =>
        pure {game with worlds := {game.worlds with
          edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}}

  -- Add the number of levels and worlds to the tile for the landing page
  modifyCurGame fun game => pure {game with tile := {game.tile with
    levels := nrLevels
    worlds := nrWorlds }}

  -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made
  let game ← getCurGame

  let mut allItemsByType : HashMap InventoryType (HashSet Name) := {}
  -- Compute which inventory items are available in which level:
  for inventoryType in #[.Tactic, .Definition, .Lemma] do

    -- Which items are introduced in which world?
    let mut lemmaStatements : HashMap (Name × Nat) Name := {}
    -- TODO: I believe `newItemsInWorld` has way to many elements in it which we iterate over
    -- e.g. we iterate over `ring` for `Lemma`s as well, but so far that seems to cause no problems
    let mut allItems : HashSet Name := {}
    for (worldId, world) in game.worlds.nodes.toArray do
      let mut newItems : HashSet Name := {}
      for (levelId, level) in world.levels.toArray do
        let newLemmas := (level.getInventory inventoryType).new
        newItems := newItems.insertMany newLemmas
        allItems := allItems.insertMany newLemmas
        if inventoryType == .Lemma then
          -- For levels `2, 3, …` we check if the previous level was named
          -- in which case we add it as available lemma.
          match levelId with
          | 0 => pure ()
          | 1 => pure () -- level ids start with 1, so we need to skip 1, too.
          | i₀ + 1 =>
            -- add named statement from previous level to the available lemmas.
            match (world.levels.find! (i₀)).statementName with
            | .anonymous => pure ()
            | .num _ _ => panic "Did not expect to get a numerical statement name!"
            | .str pre s =>
              let name := Name.str pre s
              newItems := newItems.insert name
              allItems := allItems.insert name
              lemmaStatements := lemmaStatements.insert (worldId, levelId) name
      if inventoryType == .Lemma then
        -- if named, add the lemma from the last level of the world to the inventory
        let i₀ := world.levels.size
        match i₀ with
        | 0 => logWarning m!"World `{worldId}` contains no levels."
        | i₀ =>
          match (world.levels.find! (i₀)).statementName with
          | .anonymous => pure ()
          | .num _ _ => panic "Did not expect to get a numerical statement name!"
          | .str pre s =>
            let name := Name.str pre s
            newItems := newItems.insert name
            allItems := allItems.insert name
      newItemsInWorld := newItemsInWorld.insert worldId newItems

    -- Basic inventory item availability: all locked.
    let Availability₀ : HashMap Name InventoryTile :=
      HashMap.ofList $
        ← allItems.toList.mapM fun item => do
          -- Using a match statement because the error message of `Option.get!` is not helpful.
          match (← getInventoryItem? item inventoryType) with
          | none =>
            -- Note: we did have a panic here before because lemma statement and doc entry
            -- had mismatching namespaces
            logError m!"There is no inventory item ({inventoryType}) for: {item}."
            panic s!"Inventory item {item} not found!"
          | some data =>
            return (item, {
              name := item
              displayName := data.displayName
              category := data.category
              altTitle := data.statement
              hidden := hiddenItems.contains item })



    -- Availability after a given world
    let mut itemsInWorld : HashMap Name (HashMap Name InventoryTile) := {}
    for (worldId, _) in game.worlds.nodes.toArray do
      -- Unlock all items from previous worlds
      let mut items := Availability₀
      let predecessors := game.worlds.predecessors worldId
      -- logInfo m!"Predecessors: {predecessors.toArray.map fun (a) => (a)}"
      for predWorldId in predecessors do
        for item in newItemsInWorld.findD predWorldId {} do
          let data := (← getInventoryItem? item inventoryType).get!
          items := items.insert item {
            name := item
            displayName := data.displayName
            category := data.category
            locked := false
            altTitle := data.statement
            hidden := hiddenItems.contains item }
      itemsInWorld := itemsInWorld.insert worldId items

    for (worldId, world) in game.worlds.nodes.toArray do
      let mut items := itemsInWorld.findD worldId {}

      let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1

      for (levelId, level) in levels do
        let levelInfo := level.getInventory inventoryType

        -- unlock items that are unlocked in this level
        for item in levelInfo.new do
          let data := (← getInventoryItem? item inventoryType).get!
          items := items.insert item {
            name := item
            displayName := data.displayName
            category := data.category
            locked := false
            altTitle := data.statement
            hidden := hiddenItems.contains item }

        -- add the exercise statement from the previous level
        -- if it was named
        if inventoryType == .Lemma then
          match lemmaStatements.find? (worldId, levelId) with
          | none => pure ()
          | some name =>
            let data := (← getInventoryItem? name inventoryType).get!
            items := items.insert name {
              name := name
              displayName := data.displayName
              category := data.category
              altTitle := data.statement
              locked := false }

        -- add marks for `disabled` and `new` lemmas here, so that they only apply to
        -- the current level.
        let itemsArray := items.toArray
          |>.insertionSort (fun a b => a.1.toString < b.1.toString)
          |>.map (·.2)
          |>.map (fun item => { item with
            disabled := if levelInfo.only.size == 0 then
                levelInfo.disabled.contains item.name
              else
                not (levelInfo.only.contains item.name)
            new := levelInfo.new.contains item.name
            })

        modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
          return level.setComputedInventory inventoryType itemsArray
    allItemsByType := allItemsByType.insert inventoryType allItems

  let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do
    (allItemsByType.findD type {}).toArray.mapM (fun name => do
      let some item ← getInventoryItem? name type
        | throwError "Expected item to exist: {name}"
      return item.toTile)
  let inventory : InventoryOverview := {
    lemmas := (← getTiles .Lemma).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
    tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
    definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name})
    lemmaTab := none
  }

  saveGameData allItemsByType inventory