From 20d7ee66a5c84468221c7cedbec500a5e0aa050d Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 19 Jul 2023 14:29:27 +0200 Subject: [PATCH] fix MakeGame to include named statements --- server/GameServer/Commands.lean | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 49695ae..18022de 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -717,8 +717,33 @@ elab "MakeGame" : command => do let mut newItems : HashSet Name := {} for inventoryType in #[.Tactic, .Definition, .Lemma] do for (levelId, level) in world.levels.toArray do - usedItems := usedItems.insertMany (level.getInventory inventoryType).used - newItems := newItems.insertMany (level.getInventory inventoryType).new + usedItems := usedItems.insertMany (level.getInventory inventoryType).used + newItems := newItems.insertMany (level.getInventory inventoryType).new + + -- if the previous level was named, we need to add it as a new lemma + if inventoryType == .Lemma then + match levelId with + | 0 => pure () + | 1 => pure () -- level ids start with 1, so we need to skip 1, too + | i₀ + 1 => + match (world.levels.find! (i₀)).statementName with + | .anonymous => pure () + | .num _ _ => panic "Did not expect to get a numerical statement name!" + | .str pre s => + let name := Name.str pre s + newItems := newItems.insert name + + if inventoryType == .Lemma then + + -- if the last level was named, we need to add it as a new lemma + let i₀ := world.levels.size + match (world.levels.find! (i₀)).statementName with + | .anonymous => pure () + | .num _ _ => panic "Did not expect to get a numerical statement name!" + | .str pre s => + let name := Name.str pre s + newItems := newItems.insert name + usedItemsInWorld := usedItemsInWorld.insert worldId usedItems newItemsInWorld := newItemsInWorld.insert worldId newItems