swap blocks

server/GameServer/Commands.lean

@@ -709,6 +709,54 @@ elab "MakeGame" : command => do
         content := content
       })
 
+  -- Calculate which items are used/new in which world
+  let mut usedItemsInWorld : HashMap Name (HashSet Name) := {}
+  let mut newItemsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, world) in game.worlds.nodes.toArray 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
+    usedItemsInWorld := usedItemsInWorld.insert worldId usedItems
+    newItemsInWorld := newItemsInWorld.insert worldId newItems
+
+  let mut worldsWithNewItem : HashMap Name (HashSet Name) := {}
+  for (worldId, world) in game.worlds.nodes.toArray do
+    for newItem in newItemsInWorld.find! worldId do
+      worldsWithNewItem := worldsWithNewItem.insert newItem $
+        (worldsWithNewItem.findD newItem {}).insert worldId
+
+  -- Calculate world dependency graph `game.worlds`
+  let mut worldDependsOnWorlds : HashMap Name (HashSet Name) := {}
+  let mut dependencyReason : HashMap (Name × Name) Name := {}
+  for (dependentWorldId, dependentWorld) in game.worlds.nodes.toArray do
+    let mut dependsOnWorlds : HashSet Name := {}
+    for usedItem in usedItemsInWorld.find! dependentWorldId do
+      match worldsWithNewItem.find? usedItem with
+      | some worldIds =>
+        if !worldIds.contains dependentWorldId then
+          dependsOnWorlds := dependsOnWorlds.insertMany worldIds
+          for worldId in worldIds do
+            dependencyReason := dependencyReason.insert (dependentWorldId, worldId) usedItem
+      | none => logWarning m!"No world introducing {usedItem}, but required by {dependentWorldId}"
+    worldDependsOnWorlds := worldDependsOnWorlds.insert dependentWorldId dependsOnWorlds
+  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]!
+      let item := dependencyReason.find! (w1, w2)
+      logError m!"{w1} depends on {w2} because of {item}"
+  else
+    worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds
+    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))}}
+
 
   -- Which items are used/new in which world?
   let mut usedItemsInWorld : HashMap Name (HashSet Name) := {}