From 5c919fb983250909e83f5454ed19693b099c090e Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 2 Oct 2023 12:50:19 +0200 Subject: [PATCH] Add NewHiddenTactic command Fixes #109 --- client/src/components/inventory.tsx | 2 +- client/src/state/api.ts | 3 ++- server/GameServer/Commands.lean | 20 +++++++++++++++++--- server/GameServer/EnvExtensions.lean | 4 ++++ 4 files changed, 24 insertions(+), 5 deletions(-) diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 23fc437..a11c750 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -87,7 +87,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine // For lemas, sort entries `available > disabled > locked` // otherwise alphabetically (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) - ).filter(item => ((tab ?? categories[0]) == item.category)).map((item, i) => { + ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => { return {openDoc({name: item.name, type: docType})}} name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false} diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 6b45915..524a5a4 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -20,7 +20,8 @@ export interface InventoryTile { category: string, disabled: boolean, locked: boolean, - new: boolean + new: boolean, + hidden: boolean } export interface LevelInfo { diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index a75d804..fdb2c6e 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -216,7 +216,13 @@ def getStatementString (name : Name) : CommandElabM String := do elab "NewTactic" args:ident* : command => do for name in ↑args do checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]") modifyCurLevel fun level => pure {level with - tactics := {level.tactics with new := args.map (·.getId)}} + tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId)}} + +/-- Declare tactics that are introduced by this level. -/ +elab "NewHiddenTactic" args:ident* : command => do + modifyCurLevel fun level => pure {level with + tactics := {level.tactics with new := level.tactics.new ++ args.map (·.getId), + hidden := level.tactics.hidden ++ args.map (·.getId)}} /-- Declare lemmas that are introduced by this level. -/ elab "NewLemma" args:ident* : command => do @@ -796,14 +802,19 @@ elab "MakeGame" : command => do -- For each `worldId` this contains a set of items newly defined in this world let mut newItemsInWorld : HashMap Name (HashSet Name) := {} + -- For each `worldId` this contains a set of items hidden in this world + let mut hiddenItemsInWorld : HashMap Name (HashSet Name) := {} + -- Calculate which "items" are used/new in which world for (worldId, world) in game.worlds.nodes.toArray do let mut usedItems : HashSet Name := {} let mut newItems : HashSet Name := {} + let mut hiddenItems : 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 + hiddenItems := newItems.insertMany (level.getInventory inventoryType).hidden -- if the previous level was named, we need to add it as a new lemma if inventoryType == .Lemma then @@ -831,6 +842,7 @@ elab "MakeGame" : command => do usedItemsInWorld := usedItemsInWorld.insert worldId usedItems newItemsInWorld := newItemsInWorld.insert worldId newItems + hiddenItemsInWorld := newItemsInWorld.insert worldId hiddenItems -- DEBUG: print new/used items -- logInfo m!"{worldId} uses: {usedItems.toList}" -- logInfo m!"{worldId} introduces: {newItems.toList}" @@ -986,7 +998,8 @@ elab "MakeGame" : command => do name := item displayName := data.displayName category := data.category - locked := false } + locked := false + hidden := (hiddenItemsInWorld.findD predWorldId {}).contains item } itemsInWorld := itemsInWorld.insert worldId items for (worldId, world) in game.worlds.nodes.toArray do @@ -1004,7 +1017,8 @@ elab "MakeGame" : command => do name := item displayName := data.displayName category := data.category - locked := false } + locked := false + hidden := levelInfo.hidden.contains item } -- add the exercise statement from the previous level -- if it was named diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index 400c4f5..2d88b35 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -104,6 +104,8 @@ structure InventoryTile where disabled := false /-- To mark an item that has been added freshly in this level. -/ new := false + /-- hide the item in the inventory display -/ + hidden := false deriving ToJson, FromJson, Repr, Inhabited /-- The extension that stores the doc templates. Note that you can only add, but never modify @@ -209,6 +211,8 @@ structure InventoryInfo where used : Array Name /-- new inventory items introduced by this level -/ new : Array Name + /-- inventory items that shall not be displayed in the inventory -/ + hidden : Array Name /-- inventory items exceptionally forbidden in this level -/ disabled : Array Name /-- only these inventory items are allowed in this level (ignored if empty) -/