From 6e8a47b1a7280372b1308257bc8173d6db9ad9a3 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Thu, 9 Feb 2023 13:25:40 +0100 Subject: [PATCH] lemma inventory --- client/src/components/LeftPanel.tsx | 25 +++++++----- client/src/components/Level.tsx | 8 +--- client/src/components/inventory.css | 8 ++-- client/src/state/api.ts | 2 +- server/leanserver/GameServer/Commands.lean | 39 ++++++++++++++++--- .../leanserver/GameServer/EnvExtensions.lean | 6 +-- server/leanserver/GameServer/Game.lean | 4 +- 7 files changed, 61 insertions(+), 31 deletions(-) diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx index 0e75963..ecc3754 100644 --- a/client/src/components/LeftPanel.tsx +++ b/client/src/components/LeftPanel.tsx @@ -5,23 +5,30 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons' import Markdown from './Markdown'; - -function LeftPanel({ tactics, inventory, showSidePanel, setShowSidePanel }) { +function LeftPanel({ tactics, lemmas } : + {lemmas: {name: string, locked: boolean, disabled: boolean}[], + tactics: {name: string, locked: boolean, disabled: boolean}[]}) { return ( <> -
- { tactics.map (({name, locked, disabled}) => { - const icon = locked ? : - disabled ? : "" - const className = locked ? "locked" : disabled ? "disabled" : "" - return
{icon} {name}
- })} +
+ { tactics.map(tac => ) } {/* TODO: Click on Tactic: show info TODO: click on paste icon -> paste into command line */}
+ +
+ { lemmas.map(lem => ) } +
) } +function InventoryItem({name, locked, disabled}) { + const icon = locked ? : + disabled ? : "" + const className = locked ? "locked" : disabled ? "disabled" : "" + return
{icon} {name}
+} + export default LeftPanel; diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 77134bc..4b1e597 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -67,13 +67,8 @@ function Level() { const [commandLineMode, setCommandLineMode] = useState(true) const [commandLineInput, setCommandLineInput] = useState("") - const [showSidePanel, setShowSidePanel] = useState(true) const [canUndo, setCanUndo] = useState(initialCode.trim() !== "") - const toggleSidePanel = () => { - setShowSidePanel(!showSidePanel) - } - const theme = useTheme(); useEffect(() => { @@ -184,8 +179,7 @@ function Level() {
- {!level.isLoading && } + {!level.isLoading && }
diff --git a/client/src/components/inventory.css b/client/src/components/inventory.css index 40f98c1..0cd3c44 100644 --- a/client/src/components/inventory.css +++ b/client/src/components/inventory.css @@ -1,16 +1,16 @@ -.tactic-inventory { +.inventory { display: flex; gap: .5em; flex-wrap : wrap; padding: 1em } -.tactic-inventory .tactic { +.inventory .item { border: solid 1px #aaa; padding: .1em .5em; } -.tactic-inventory .tactic.locked, -.tactic-inventory .tactic.disabled { +.inventory .item.locked, +.inventory .item.disabled { color: #aaa; } diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 23e3de1..5fb947c 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -15,7 +15,7 @@ interface LevelInfo { introduction: null|string, index: number, tactics: {name: string, disabled: boolean, locked: boolean}[], - lemmas: any[], + lemmas: {name: string, disabled: boolean, locked: boolean}[], descrText: null|string, descrFormat: null|string, } diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index d0174dc..6e3085e 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -264,32 +264,50 @@ elab "MakeGame" : command => do if game.worlds.hasLoops then throwError "World graph has loops!" - -- Compute which tactics are available in which level: + -- Compute which tactics/lemmas are available in which level: let mut newTacticsInWorld : HashMap Name (HashSet Name) := {} let mut allTactics : HashSet Name := {} + let mut newLemmasInWorld : HashMap Name (HashSet Name) := {} + let mut allLemmas : HashSet Name := {} for (worldId, world) in game.worlds.nodes.toArray do let mut newTactics : HashSet Name:= {} + let mut newLemmas : HashSet Name:= {} for (_, level) in world.levels.toArray do newTactics := newTactics.insertMany level.newTactics allTactics := allTactics.insertMany level.newTactics + newLemmas := newLemmas.insertMany level.newLemmas + allLemmas := allLemmas.insertMany level.newLemmas newTacticsInWorld := newTacticsInWorld.insert worldId newTactics + newLemmasInWorld := newLemmasInWorld.insert worldId newLemmas - let tacticAvailability₀ : HashMap Name TacticAvailability := + -- Basic tactic/lemma availability: all locked, none disabled. + let Availability₀ : HashMap Name Availability := HashMap.ofList $ allTactics.toList.map fun name => (name, {name, locked := true, disabled := false}) + let lemmaAvailability₀ : HashMap Name Availability := + HashMap.ofList $ + allLemmas.toList.map fun name => + (name, {name, locked := true, disabled := false}) - let mut tacticsInWorld : HashMap Name (HashMap Name TacticAvailability) := {} + -- Availability after a given world + let mut tacticsInWorld : HashMap Name (HashMap Name Availability) := {} + let mut lemmasInWorld : HashMap Name (HashMap Name Availability) := {} for (worldId, _) in game.worlds.nodes.toArray do - let mut tactics : HashMap Name TacticAvailability := tacticAvailability₀ + let mut tactics := Availability₀ + let mut lemmas := lemmaAvailability₀ let predecessors := game.worlds.predecessors worldId for predWorldId in predecessors do for tac in newTacticsInWorld.find! predWorldId do tactics := tactics.insert tac {name := tac, locked := false, disabled := false} + for lem in newLemmasInWorld.find! predWorldId do + lemmas := lemmas.insert lem {name := lem, locked := false, disabled := false} tacticsInWorld := tacticsInWorld.insert worldId tactics + lemmasInWorld := lemmasInWorld.insert worldId lemmas for (worldId, world) in game.worlds.nodes.toArray do let mut tactics := tacticsInWorld.find! worldId + let mut lemmas := lemmasInWorld.find! worldId let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1 @@ -298,9 +316,20 @@ elab "MakeGame" : command => do tactics := tactics.insert tac {name := tac, locked := false, disabled := false} for tac in level.disabledTactics do tactics := tactics.insert tac {name := tac, locked := false, disabled := true} + for lem in level.newLemmas do + lemmas := lemmas.insert lem {name := lem, locked := false, disabled := false} + for lem in level.disabledLemmas do + lemmas := lemmas.insert lem {name := lem, locked := false, disabled := true} let tacticArray := tactics.toArray |>.insertionSort (fun a b => a.1.toString < b.1.toString) |>.map (·.2) + + let lemmaArray := lemmas.toArray + |>.insertionSort (fun a b => a.1.toString < b.1.toString) + |>.map (·.2) + modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do - return {level with tactics := tacticArray} + return {level with + tactics := tacticArray + lemmas := lemmaArray} diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 9b5aa67..1dc476c 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -144,7 +144,7 @@ structure LevelId where level : Nat deriving Inhabited -structure TacticAvailability where +structure Availability where name : Name locked : Bool disabled : Bool @@ -176,7 +176,7 @@ structure GameLevel where -- only these tactics are allowed in this level (ignore if empty): onlyTactics: Array Name := default -- tactics in this level (computed by `MakeGame`): - tactics: Array TacticAvailability := default + tactics: Array Availability := default -- new lemmas introduces by this level: newLemmas: Array Name := default -- lemmas exceptionally forbidden in this level: @@ -184,7 +184,7 @@ structure GameLevel where -- only these lemmas are allowed in this level (ignore if empty): onlyLemmas: Array Name := default -- lemmas in this level (computed by `MakeGame`): - lemmas: Array LemmaDocEntry := default + lemmas: Array Availability := default hints: Array GoalHintEntry := default goal : TSyntax `Lean.Parser.Command.declSig := default descrText: String := default diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index 9959d48..4cedcda 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -41,8 +41,8 @@ Fields: structure LevelInfo where index : Nat title : String - tactics: Array TacticAvailability - lemmas: Array LemmaDocEntry + tactics: Array Availability + lemmas: Array Availability introduction : String descrText : String := "" descrFormat : String := ""