diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx new file mode 100644 index 0000000..e90ac1e --- /dev/null +++ b/client/src/components/Inventory.tsx @@ -0,0 +1,64 @@ +import * as React from 'react'; +import { useState, useEffect } from 'react'; +import './inventory.css' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-solid-svg-icons' +import Markdown from './Markdown'; +import { useLoadDocQuery } from '../state/api'; + +function Inventory({ tactics, lemmas } : + {lemmas: {name: string, locked: boolean, disabled: boolean}[], + tactics: {name: string, locked: boolean, disabled: boolean}[]}) { + + const [docName, setDocName] = useState(null) + const [docType, setDocType] = useState(null) + + + return ( +
+

Tactics

+
+ { tactics.map(tac => + {setDocName(tac.name); setDocType("tactic")}} + name={tac.name} locked={tac.locked} disabled={tac.disabled} />) } + {/* TODO: Click on Tactic: show info + TODO: click on paste icon -> paste into command line */} +
+ +

Lemmas

+
+ { lemmas.map(lem => + {setDocName(lem.name); setDocType("lemma")}} + name={lem.name} locked={lem.locked} disabled={lem.disabled} />) } +
+ + {docName && } +
+ ) +} + +function InventoryItem({name, locked, disabled, showDoc}) { + const icon = locked ? : + disabled ? : "" + const className = locked ? "locked" : disabled ? "disabled" : "" + + const handleClick = () => { + if (!locked && !disabled) { + showDoc() + } + } + + return
{icon} {name}
+} + +function Documentation({name, type}) { + + const doc = useLoadDocQuery({type: type, name: name}) + + return <> +

{doc.data?.name}

+ {doc.data?.text} + +} + +export default Inventory; diff --git a/client/src/components/LeftPanel.tsx b/client/src/components/LeftPanel.tsx deleted file mode 100644 index 1cc3156..0000000 --- a/client/src/components/LeftPanel.tsx +++ /dev/null @@ -1,104 +0,0 @@ -import * as React from 'react'; -import { useState, useEffect } from 'react'; -import ReactMarkdown from 'react-markdown'; -import '@fontsource/roboto/300.css'; -import '@fontsource/roboto/400.css'; -import '@fontsource/roboto/500.css'; -import '@fontsource/roboto/700.css'; - -import { Paper, Box, Typography, Accordion, AccordionSummary, AccordionDetails, Tabs, Tab, Divider, Button, List, ListItem, ListItemButton, ListItemIcon, ListItemText } from '@mui/material'; -import ExpandMoreIcon from '@mui/icons-material/ExpandMore'; - -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faUpload, faArrowRotateRight, faChevronLeft, faChevronRight, faBook, faHammer } from '@fortawesome/free-solid-svg-icons' -import Markdown from './Markdown'; - -function TacticDoc(props) { - return ( - - }> - {props.tactic.name} - - - {props.tactic.content} - - ) -} - -function LemmaDoc({ lemma }) { - return ( - - }> - {lemma.userName} - - - {lemma.content} - - ) -} - -function LemmaDocs({ lemmas }) { - const [categories, setCategories] = useState(new Map()) - const [curCategory, setCurCategory] = useState("") - - const changeTab = (event: React.SyntheticEvent, newValue : string) => { - setCurCategory(newValue); - }; - - useEffect(() => { - const cats = new Map() - lemmas.forEach(function (item) { - const category = item.category - cats.set(category, (cats.get(category) || []).concat([item])) - }); - setCategories(cats) - setCurCategory(cats.keys().next().value) - }, [lemmas]); - - return ( -
- - - {(Array.from(categories)).map(([category, _]) => )} - - - {curCategory && categories.get(curCategory).map((lemma) => )} -
) -} - -function LeftPanel({ spells, inventory, showSidePanel, setShowSidePanel }) { - - return ( - - - setShowSidePanel(true)}> - - - - - - {spells && spells.length > 0 && - - {spells.map((spell) => )} - } - - - - - - - - - {inventory && inventory.length > 0 && - - - } - - - ) -} - -export default LeftPanel; diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 8743d72..0159d28 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -9,7 +9,7 @@ import { Link, useParams } from 'react-router-dom'; import { Box, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material'; import MuiDrawer from '@mui/material/Drawer'; import Grid from '@mui/material/Unstable_Grid2'; -import LeftPanel from './LeftPanel'; +import Inventory from './Inventory'; import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter'; import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; import 'lean4web/client/src/editor/vscode.css'; @@ -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 && }
diff --git a/client/src/components/infoview/CommandLine.tsx b/client/src/components/infoview/CommandLine.tsx index 45ef83c..b565761 100644 --- a/client/src/components/infoview/CommandLine.tsx +++ b/client/src/components/infoview/CommandLine.tsx @@ -195,7 +195,7 @@ export function CommandLine() {
- +
} diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css index e91bc49..6a03114 100644 --- a/client/src/components/infoview/infoview.css +++ b/client/src/components/infoview/infoview.css @@ -48,19 +48,24 @@ display: flex; } -.command-line form>input{ +.command-line button { display: block; + white-space: nowrap; + flex: 0; } .command-line .command-line-input-wrapper{ + min-width: 0; flex: 1; padding: 0.4em .6em 0; font-size: 1rem; background: white; + display: flex; + flex-direction: column; } .command-line .command-line-input{ - height: 1.2em; + flex: 1; } /* Turn off some monaco decorations: */ diff --git a/client/src/components/inventory.css b/client/src/components/inventory.css new file mode 100644 index 0000000..3637093 --- /dev/null +++ b/client/src/components/inventory.css @@ -0,0 +1,38 @@ +.inventory { + padding: 0 1em; +} + +.inventory h2 { + font-size: 1.5em; + margin-top: 1em; + margin-bottom: .2em; +} + + +.inventory h2.doc { + margin-top: 1.5em; + font-weight: 900; +} + +.inventory-list { + display: flex; + gap: .5em; + flex-wrap : wrap; +} + +.inventory .item { + background: #fff; + border: solid 1px #777; + padding: .1em .5em; +} + +.inventory .item.locked, +.inventory .item.disabled { + border: solid 1px #ccc; + color: #ccc; +} + + +.inventory .item:not(.locked):not(.disabled) { + cursor: pointer; +} diff --git a/client/src/components/level.css b/client/src/components/level.css index 3386146..2e08a53 100644 --- a/client/src/components/level.css +++ b/client/src/components/level.css @@ -72,12 +72,16 @@ gap: 1em; } +.doc-panel { + background: #fafafa; +} + .doc-panel li { - border-bottom: 1px solid rgba(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in LeftPanel.tsx */ + border-bottom: 1px solid rgba(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in Inventory.tsx */ } .doc-panel li:first-of-type { - border-top: 1px solid rgb(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in LeftPanel.tsx */ + border-top: 1px solid rgb(0, 0, 0, 0.12); /* This should be teh same colour as `divider` in Inventory.tsx */ } /* fix as Mui seems to set this to `nowrap`. */ diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 082fe53..0d94ba2 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -14,12 +14,18 @@ interface LevelInfo { title: null|string, introduction: null|string, index: number, - tactics: any[], - lemmas: any[], + tactics: {name: string, disabled: boolean, locked: boolean}[], + lemmas: {name: string, disabled: boolean, locked: boolean}[], descrText: null|string, descrFormat: null|string, } +interface Doc { + name: string, + text: string +} + + const customBaseQuery = async ( args : {method: string, params?: any}, { signal, dispatch, getState, extra }, @@ -48,9 +54,12 @@ export const apiSlice = createApi({ loadLevel: builder.query({ query: ({world, level}) => {return {method: "loadLevel", params: {world, level}}}, }), + loadDoc: builder.query({ + query: ({name, type}) => {return {method: "loadDoc", params: {name, type}}}, + }), }), }) // Export hooks for usage in functional components, which are // auto-generated based on the defined endpoints -export const { useGetGameInfoQuery, useLoadLevelQuery } = apiSlice +export const { useGetGameInfoQuery, useLoadLevelQuery, useLoadDocQuery } = apiSlice diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 231a9a9..9068e41 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -250,11 +250,6 @@ elab "NewLemmas" args:ident* : command => do /-! ## Make Game -/ -def getTacticDoc! (tac : Name) : CommandElabM TacticDocEntry := do - match (tacticDocExt.getState (← getEnv)).find? (·.name = tac) with - | some doc => return doc - | none => throwError "Tactic documentation not found: {tac}" - /-- Make the final Game. This command will precompute various things about the game, such as which tactics are available in each level etc. -/ elab "MakeGame" : command => do @@ -264,30 +259,72 @@ 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 - - let mut tacticsInWorld : HashMap Name (HashSet Name) := {} + newLemmasInWorld := newLemmasInWorld.insert worldId newLemmas + + -- 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}) + + -- 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 : HashSet Name:= {} + let mut tactics := Availability₀ + let mut lemmas := lemmaAvailability₀ let predecessors := game.worlds.predecessors worldId for predWorldId in predecessors do - tactics := tactics.insertMany (newTacticsInWorld.find! predWorldId) + 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 - logInfo m!"{tactics.toArray}" + let mut lemmas := lemmasInWorld.find! worldId let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1 for (levelId, level) in levels do - tactics := tactics.insertMany level.newTactics + for tac in level.newTactics 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 := ← tactics.toArray.mapM getTacticDoc!} + return {level with + tactics := tacticArray + lemmas := lemmaArray} diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 6e726f5..9c1f13d 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -41,6 +41,10 @@ initialize tacticDocExt : SimplePersistentEnvExtension TacticDocEntry (Array Tac addImportedFn := Array.concatMap id } +def getTacticDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) : + m (Option TacticDocEntry) := do + return (tacticDocExt.getState (← getEnv)).find? (·.name = tac) + open Elab Command in /-- Print a registered tactic doc for debugging purposes. -/ elab "#print_tactic_doc" : command => do @@ -64,6 +68,10 @@ initialize lemmaDocExt : SimplePersistentEnvExtension LemmaDocEntry (Array Lemma addImportedFn := Array.concatMap id } +def getLemmaDoc? {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) : + m (Option LemmaDocEntry) := do + return (lemmaDocExt.getState (← getEnv)).find? (·.name = tac) + open Elab Command in /-- Print a lemma doc for debugging purposes. -/ elab "#print_lemma_doc" : command => do @@ -144,6 +152,12 @@ structure LevelId where level : Nat deriving Inhabited +structure Availability where + name : Name + locked : Bool + disabled : Bool +deriving ToJson, FromJson, Repr + def getCurLevelId [MonadError m] : m LevelId := do return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx} @@ -170,7 +184,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 TacticDocEntry := default + tactics: Array Availability := default -- new lemmas introduces by this level: newLemmas: Array Name := default -- lemmas exceptionally forbidden in this level: @@ -178,7 +192,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/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean index 88c7d61..75e5166 100644 --- a/server/leanserver/GameServer/FileWorker.lean +++ b/server/leanserver/GameServer/FileWorker.lean @@ -76,7 +76,8 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameL findForbiddenTactics inputCtx level arg | .atom info val => -- ignore syntax elements that do not start with a letter - if 0 < val.length ∧ val.data[0]!.isAlpha then + -- and ignore "with" keyword + if 0 < val.length ∧ val.data[0]!.isAlpha ∧ val != "with" then if ¬ ((level.tactics.map (·.name.toString))).contains val then addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!" else if level.disabledTactics.contains val diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index cea1e91..9c0b073 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 TacticDocEntry - lemmas: Array LemmaDocEntry + tactics: Array Availability + lemmas: Array Availability introduction : String descrText : String := "" descrFormat : String := "" @@ -53,6 +53,32 @@ structure LoadLevelParams where level : Nat deriving ToJson, FromJson +structure Doc where + name: String + text: String +deriving ToJson + +inductive TacOrLem := | tactic | «lemma» +deriving ToJson, FromJson + +structure LoadDocParams where + name : Name + type : TacOrLem +deriving ToJson, FromJson + +def mkDoc (name : Name) (type : TacOrLem) : GameServerM (Option Doc) := do + match type with + | .tactic => do + let doc ← getTacticDoc? name + return doc.map fun doc => + { name := doc.name.toString + text := doc.content } + | .lemma => do + let doc ← getLemmaDoc? name + return doc.map fun doc => + { name := doc.name.toString + text := doc.content } + partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do match ev with | ServerEvent.clientMsg msg => @@ -68,8 +94,9 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do let c ← read let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level} | do - c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩ - return true + c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩ + return true + let levelInfo : LevelInfo := { index := lvl.index, title := lvl.title, @@ -80,6 +107,16 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do introduction := lvl.introduction } c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩ return true + | Message.request id "loadDoc" params => + let p ← parseParams LoadDocParams (toJson params) + let s ← get + let c ← read + let some doc ← mkDoc p.name p.type + | do + c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Documentation not found: {p.name}", none⟩ + return true + c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩ + return true | _ => return false | _ => return false