diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 8146389..e2dc042 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -49,26 +49,6 @@ elab "Conclusion" t:str : command => do | .World => modifyCurWorld fun world => pure {world with conclusion := t.getString} | .Game => modifyCurGame fun game => pure {game with conclusion := t.getString} -/-! ## World Paths -/ - -/-- The worlds of a game are joint by paths. These are defined with the syntax -`Path World₁ → World₂ → World₃`. -/ -def Parser.path := Parser.sepBy1Indent Parser.ident "→" - -/-- The worlds of a game are joint by paths. These are defined with the syntax -`Path World₁ → World₂ → World₃`. -/ -elab "Path" s:Parser.path : command => do - let mut last : Option Name := none - for stx in s.raw.getArgs.getEvenElems do - let some l := last - | do - last := some stx.getId - continue - modifyCurGame fun game => - pure {game with worlds := {game.worlds with edges := game.worlds.edges.push (l, stx.getId)}} - last := some stx.getId - - /-! # Inventory @@ -698,10 +678,6 @@ tactics are available in each level etc. -/ elab "MakeGame" : command => do let game ← getCurGame - -- Check for loops in world graph - if game.worlds.hasLoops then - throwError "World graph must not contain loops! Check your `Path` declarations." - let env ← getEnv -- Now create The doc entries from the templates @@ -893,8 +869,10 @@ elab "MakeGame" : command => do 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)}" - + 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 -/ diff --git a/server/GameServer/Graph.lean b/server/GameServer/Graph.lean index faf826e..0cd5f63 100644 --- a/server/GameServer/Graph.lean +++ b/server/GameServer/Graph.lean @@ -23,41 +23,6 @@ instance : EmptyCollection (Graph α β) := ⟨default⟩ def Graph.insertNode (g : Graph α β) (a : α) (b : β) := {g with nodes := g.nodes.insert a b} -/-- Check if graph contains loops -/ -partial def Graph.hasLoops (g : Graph α β) (visited0 : HashSet α := {}): Bool := Id.run do - let mut visited : HashSet α := visited0 - let all : Array α := g.nodes.toArray.map (·.1) - - -- find some node that we haven't visited - let some x := all.find? fun x => ¬ visited.contains x - | return false -- 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 - | some visited' => visited := visited' - | none => return true -- none means a loop has been found - - g.hasLoops visited -- continue looking for unvisited nodes - -where - visitSuccessors (x : α) (x0 : α) (visited0 : HashSet α) : Option (HashSet α) := Id.run do - let mut visited : HashSet α := visited0 - - let directSuccessors := (g.edges.filter (·.1 == x)).map (·.2) - for y in directSuccessors do - if y == x0 then - return none -- 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 - | some visited' => visited := visited' - | none => return none - - return some visited - --- #eval Graph.hasLoops ⟨HashMap.ofList [(2,2), (1,1)], #[(2,1)]⟩ - partial def Graph.predecessors (g : Graph α β) (x : α) (acc : HashSet α := {}) : HashSet α := Id.run do let mut res := acc let directPredecessors := (g.edges.filter (·.2 == x)).map (·.1)