Merge branch 'dev' of github.com:leanprover-community/lean4game into dev

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 -/
 

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)