remove path command

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
 

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)