From 91d41cdd6de50e3993645a0845ce4be356d3ef8c Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Mon, 28 Nov 2022 14:00:21 +0100
Subject: [PATCH] define paths

---
 server/leanserver/GameServer/Commands.lean      | 15 +++++++++++++++
 server/leanserver/GameServer/EnvExtensions.lean |  9 +++++++--
 server/testgame/TestGame/Metadata.lean          |  3 +++
 3 files changed, 25 insertions(+), 2 deletions(-)

diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 3e8ee72..893cd76 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -70,10 +70,25 @@ elab "Conclusion" t:str : command => do
 elab "PrintCurLevel" : command => do
   logInfo (repr (← getCurLevel))
 
+#check Syntax.SepArray
+
 -- /-- Print levels for debugging purposes. -/
 elab "PrintLevels" : command => do
   logInfo $ repr $ (← getCurWorld).levels.toArray
 
+def Parser.path := Parser.sepBy1Indent Parser.ident "→"
+
+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
+
 end metadata
 
 /-! ## Messages -/
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 794deaf..5ba1b6e 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -217,7 +217,7 @@ new.fold (fun acc a b =>
   else acc.insert a b) old
 
 def GameLevel.merge (old : GameLevel) (new : GameLevel) : GameLevel :=
-  new
+  new -- simply override old level
 
 def World.merge (old : World) (new : World) : World :=
 { new with
@@ -227,7 +227,12 @@ def Game.merge (old : Game) (new : Game) : Game :=
 { new with
   worlds := {
     nodes := HashMap.merge old.worlds.nodes new.worlds.nodes World.merge
-    edges := old.worlds.edges ++ new.worlds.edges
+    edges := Id.run do
+      let mut res := old.worlds.edges
+      for e in new.worlds.edges do
+        if ¬ res.contains e then
+          res := res.push e
+      return res
   } }
 
 initialize gameExt : PersistentEnvExtension (Name × Game) (Name × Game) (HashMap Name Game) ←
diff --git a/server/testgame/TestGame/Metadata.lean b/server/testgame/TestGame/Metadata.lean
index eb71ac5..6ae4946 100644
--- a/server/testgame/TestGame/Metadata.lean
+++ b/server/testgame/TestGame/Metadata.lean
@@ -19,3 +19,6 @@ with a level 1 spell book. Good luck."
 
 Conclusion
 "There is nothing else so far. Thanks for rescuing natural numbers!"
+
+Path w1 → w2 → w3
+Path w1 → v2 → w3
\ No newline at end of file