From 0a2c4552bfc6d1b9af8ae94f9b5c6953073cd79c Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 14 Jul 2023 19:15:25 +0200 Subject: [PATCH] unlock items of previous worlds --- server/GameServer/Commands.lean | 106 ++++++++++++++++---------------- 1 file changed, 53 insertions(+), 53 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index e2dc042..de61116 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -710,11 +710,60 @@ elab "MakeGame" : command => do }) + -- 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 + + -- which world depends on which world? + 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))}} + -- 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 newItemsInWorld : HashMap Name (HashSet Name) := {} + let mut newItemsInWorld' : HashMap Name (HashSet Name) := {} let mut lemmaStatements : HashMap (Name × Nat) Name := {} let mut allItems : HashSet Name := {} for (worldId, world) in game.worlds.nodes.toArray do @@ -749,7 +798,7 @@ elab "MakeGame" : command => do let name := Name.str pre s newItems := newItems.insert name allItems := allItems.insert name - newItemsInWorld := newItemsInWorld.insert worldId newItems + newItemsInWorld' := newItemsInWorld'.insert worldId newItems -- Basic inventory item availability: all locked. let Availability₀ : HashMap Name InventoryTile := @@ -767,9 +816,9 @@ elab "MakeGame" : command => do for (worldId, _) in game.worlds.nodes.toArray do -- Unlock all items from previous worlds let mut items := Availability₀ - let predecessors := game.worlds.predecessors worldId + let predecessors := worldDependsOnWorlds.find! worldId for predWorldId in predecessors do - for item in newItemsInWorld.find! predWorldId do + for item in newItemsInWorld'.find! predWorldId do let data := (← getInventoryItem? item inventoryType).get! items := items.insert item { name := item @@ -825,55 +874,6 @@ elab "MakeGame" : command => do return level.setComputedInventory inventoryType itemsArray - -- 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 - - -- which world depends on which world? - 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))}} - /-! # Debugging tools -/ -- /-- Print current game for debugging purposes. -/