From 0d242326852d795178261d815050654933fb1e1f Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 10 Jul 2023 15:30:38 +0200 Subject: [PATCH] calculate dependencies --- server/GameServer/Commands.lean | 134 ++++++++++++++++++++++++++------ 1 file changed, 112 insertions(+), 22 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 0a31838..8146389 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -628,6 +628,71 @@ def getDocstring (env : Environment) (name : Name) (type : InventoryType) : -- TODO: for definitions not implemented yet, does it work? | .Definition => findDocString? env name + +partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name)) + (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) : + HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do + match (newArrows.find? id, decendants.find? id) with + | (some _, some _) => return (newArrows, decendants) + | _ => + let mut newArr := newArrows + let mut desc := decendants + desc := desc.insert id {} -- mark as worked in case of loops + newArr := newArr.insert id {} -- mark as worked in case of loops + let children := arrows.find! id + let mut trimmedChildren := children + let mut theseDescs := children + for child in children do + (newArr, desc) := removeTransitiveAux child arrows newArr desc + let childDescs := desc.find! child + theseDescs := theseDescs.insertMany childDescs + for d in childDescs do + trimmedChildren := trimmedChildren.erase d + desc := desc.insert id theseDescs + newArr := newArr.insert id trimmedChildren + return (newArr, desc) + +def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do + let mut newArr := {} + let mut desc := {} + for id in arrows.toArray.map Prod.fst do + (newArr, desc) := removeTransitiveAux id arrows newArr desc + if (desc.find! id).contains id then logWarning m!"Loop at {id}" + return newArr + + +/-- Check if graph contains loops -/ +partial def findLoops (arrows : HashMap Name (HashSet Name)) (visited0 : HashSet Name := {}): List Name := Id.run do + let mut visited : HashSet Name := visited0 + let all : Array Name := arrows.toArray.map (·.1) + + -- find some node that we haven't visited + let some x := all.find? fun x => ¬ visited.contains x + | return [] -- We have visted all nodes and found no loops + visited := visited.insert x + + match visitSuccessors x x visited with -- visit all recursive successors of x + | .inl visited' => visited := visited' + | .inr l => return l -- a loop has been found + + findLoops arrows visited -- continue looking for unvisited nodes +where + visitSuccessors (x : Name) (x0 : Name) (visited0 : HashSet Name) : Sum (HashSet Name) (List Name) := Id.run do + let mut visited : HashSet Name := visited0 + + let directSuccessors := arrows.findD x {} + for y in directSuccessors do + if y == x0 then + return .inr [x] -- loop found + if visited.contains y then + continue -- no loop possible here because the visited nodes do not lead to x0 + visited := visited.insert y + match visitSuccessors y x0 visited with + | .inl visited' => visited := visited' + | .inr l => return .inr (x :: l) + + return .inl visited + /-- 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 @@ -668,12 +733,12 @@ elab "MakeGame" : command => do content := content }) + -- 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 worldsWithNewItem : 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 @@ -709,27 +774,6 @@ elab "MakeGame" : command => do newItems := newItems.insert name allItems := allItems.insert name newItemsInWorld := newItemsInWorld.insert worldId newItems - for newItem in newItems do - worldsWithNewItem := worldsWithNewItem.insert newItem $ - (worldsWithNewItem.findD newItem {}).insert worldId - - -- Which items are used in which world? - let mut usedItemsInWorld : HashMap Name (HashSet Name) := {} - for (worldId, world) in game.worlds.nodes.toArray do - let mut usedItems : HashSet Name := {} - for (levelId, level) in world.levels.toArray do - usedItems := usedItems.insertMany (level.getInventory inventoryType).used - usedItemsInWorld := usedItemsInWorld.insert worldId usedItems - - let mut worldDependsOnWorlds : HashMap Name (HashSet 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 worldId => dependsOnWorlds := dependsOnWorlds.insertMany worldId - | none => logWarning m!"No world introducing {usedItem}, but required by {dependentWorldId}" - worldDependsOnWorlds := worldDependsOnWorlds.insert dependentWorldId dependsOnWorlds - logInfo m!"World {dependentWorldId} depends on {dependsOnWorlds.toArray}" -- Basic inventory item availability: all locked. let Availability₀ : HashMap Name InventoryTile := @@ -805,6 +849,52 @@ 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 + logInfo m!"Dependencies: {worldDependsOnWorlds.toArray.map fun (a,b) => (a,b.toArray)}" + /-! # Debugging tools -/