From 957538dcb29e9cb8d30c50767ba908f40edbcaf0 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Tue, 6 Dec 2022 11:09:58 +0100
Subject: [PATCH] make sure that variables are only used once for messages

---
 server/leanserver/GameServer/RpcHandlers.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
index 1902311..1f08a72 100644
--- a/server/leanserver/GameServer/RpcHandlers.lean
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -77,14 +77,19 @@ def getLevelByFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String)
 def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := do
   -- We iterate through the array backwards hoping that this will find us faster results
   -- TODO: implement backtracking
+  let mut usedFvars := (List.replicate declFvars.size false).toArray
+  -- `usedFvars` keeps track of the fvars that were already used to match an mvar.
   for i in [:declMvars.size] do
     let declMvar := declMvars[declMvars.size - i - 1]!
     let mut found := false
     for j in [:declFvars.size] do
       let declFvar := declFvars[declFvars.size - j - 1]!
-      if ← isDefEq declMvar declFvar then
-        found := true
-        break
+      let usedFvar := usedFvars[declFvars.size - j - 1]!
+      if ¬ usedFvar then
+        if ← isDefEq declMvar declFvar then
+          usedFvars := usedFvars.set! (declFvars.size - j - 1) true
+          found := true
+          break
       else
         continue
     if ¬ found then return false