From d0b7838564d3050942ca5093905881a2a8f435de Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 16 Mar 2023 13:23:10 +0100 Subject: [PATCH] add display names for definitions and lemmas --- client/src/components/Inventory.tsx | 8 +- client/src/state/api.ts | 2 + server/leanserver/GameServer/Commands.lean | 78 +++++++++++---- .../leanserver/GameServer/EnvExtensions.lean | 3 +- server/leanserver/GameServer/Game.lean | 6 +- server/testgame/TestGame/LemmaDocs.lean | 94 +++++++++---------- 6 files changed, 118 insertions(+), 73 deletions(-) diff --git a/client/src/components/Inventory.tsx b/client/src/components/Inventory.tsx index bde6c8e..df5410c 100644 --- a/client/src/components/Inventory.tsx +++ b/client/src/components/Inventory.tsx @@ -55,14 +55,14 @@ function InventoryList({items, docType, openDoc} : {items: ComputedInventoryItem ).map(item => { if (tab == item.category) { return {openDoc(item.name, docType)}} - name={item.name} locked={item.locked} disabled={item.disabled} /> + name={item.name} displayName={item.displayName} locked={item.locked} disabled={item.disabled} /> } }) } } -function InventoryItem({name, locked, disabled, showDoc}) { +function InventoryItem({name, displayName, locked, disabled, showDoc}) { const icon = locked ? : disabled ? : "" const className = locked ? "locked" : disabled ? "disabled" : "" @@ -73,7 +73,7 @@ function InventoryItem({name, locked, disabled, showDoc}) { } } - return
{icon} {name}
+ return
{icon} {displayName}
} export function Documentation({name, type}) { @@ -81,7 +81,7 @@ export function Documentation({name, type}) { const doc = useLoadDocQuery({type: type, name: name}) return <> -

{doc.data?.name}

+

{doc.data?.displayName}

{doc.data?.text} } diff --git a/client/src/state/api.ts b/client/src/state/api.ts index bd5268c..581823c 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -12,6 +12,7 @@ interface GameInfo { export interface ComputedInventoryItem { name: string, + displayName: string, category: string, disabled: boolean, locked: boolean @@ -31,6 +32,7 @@ interface LevelInfo { interface Doc { name: string, + displayName: string, text: string } diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 9004c62..9b4c716 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -303,14 +303,21 @@ def checkInventoryDoc (type : InventoryType) (name : Name) : CommandElabM Unit : /-! ### Tactics -/ -/-- Declare a documentation entry for some tactic. -Expect an identifier and then a string literal. -/ +/-- Documentation entry of a tactic. Example: + +``` +TacticDoc rw "`rw` stands for rewrite, etc. " +``` + +* The identifier is the tactics name. Some need to be escaped like `«have»`. +* The description is a string supporting Markdown. + -/ elab "TacticDoc" name:ident content:str : command => modifyEnv (inventoryDocExt.addEntry · { category := default type := .Tactic name := name.getId, - userName := name.getId, + displayName := name.getId.toString, content := content.getString }) /-- Declare tactics that are introduced by this level. -/ @@ -333,14 +340,23 @@ elab "OnlyTactic" args:ident* : command => do /-! ### Definitions -/ -/-- Declare a documentation entry for some definition. -Expect an identifier and then a string literal. -/ -elab "DefinitionDoc" name:ident content:str : command => +/-- Documentation entry of a definition. Example: + +``` +DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Surjective`, etc." +``` + +* The first identifier is used in the commands `[New/Only/Disabled]Definition`. + It is preferably the true name of the definition. However, this is not required. +* The string following `as` is the displayed name (in the Inventory). +* The description is a string supporting Markdown. + -/ +elab "DefinitionDoc" name:ident "as" displayName:str content:str : command => modifyEnv (inventoryDocExt.addEntry · { category := default type := .Definition name := name.getId, - userName := name.getId, + displayName := displayName.getString, content := content.getString }) /-- Declare definitions that are introduced by this level. -/ @@ -364,15 +380,23 @@ elab "OnlyDefinition" args:ident* : command => do /-! ### Lemmas -/ -/-- Declare a documentation entry for some lemma. -Expect two identifiers and then a string literal. The first identifier is meant -as the real name of the lemma while the second is the displayed name. Currently -the real name isn't used. -/ -elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : command => +/-- Documentation entry of a lemma. Example: + +``` +LemmaDoc Nat.succ_pos as "succ_pos" in Nat "says `0 < n.succ`, etc." +``` + +* The first identifier is used in the commands `[New/Only/Disabled]Lemma`. + It is preferably the true name of the lemma. However, this is not required. +* The string following `as` is the displayed name (in the Inventory). +* The identifier after `in` is the category to group lemmas by (in the Inventory). +* The description is a string supporting Markdown. + -/ +elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command => modifyEnv (inventoryDocExt.addEntry · { name := name.getId, type := .Lemma - userName := userName.getId, + displayName := displayName.getString, category := category.getString, content := content.getString }) @@ -430,9 +454,11 @@ elab "MakeGame" : command => do let Availability₀ : HashMap Name ComputedInventoryItem := HashMap.ofList $ ← allItems.toList.mapM fun name => do + let data := (← getInventoryDoc? name inventoryType).get! return (name, { name - category := (← getInventoryDoc? name inventoryType).get!.category + displayName := data.displayName + category := data.category locked := true disabled := false}) @@ -443,9 +469,11 @@ elab "MakeGame" : command => do let predecessors := game.worlds.predecessors worldId for predWorldId in predecessors do for item in newItemsInWorld.find! predWorldId do + let data := (← getInventoryDoc? item inventoryType).get! items := items.insert item { name := item - category := (← getInventoryDoc? item inventoryType).get!.category + displayName := data.displayName + category := data.category locked := false disabled := false } @@ -458,13 +486,25 @@ elab "MakeGame" : command => do for (levelId, level) in levels do for item in (level.getInventory inventoryType).new do - let category := (← getInventoryDoc? item inventoryType).get!.category - items := items.insert item {name := item, category, locked := false, disabled := false} + let data := (← getInventoryDoc? item inventoryType).get! + items := items.insert item { + name := item + displayName := data.displayName + category := data.category + locked := false + disabled := false + } let mut disabled : HashSet Name := {} for item in (level.getInventory inventoryType).disabled do - let category := (← getInventoryDoc? item inventoryType).get!.category - items := items.insert item {name := item, category, locked := false, disabled := false} + let data := (← getInventoryDoc? item inventoryType).get! + items := items.insert item { + name := item + displayName := data.displayName + category := data.category + locked := false + disabled := false + } -- (we set disabled to false at first because it applies only to the current level) disabled := disabled.insert item diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 95a2976..e6fd7a0 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -43,7 +43,7 @@ instance : ToString InventoryType := ⟨fun t => match t with structure InventoryDocEntry where name : Name type : InventoryType - userName : Name + displayName : String category : String content : String deriving ToJson, Repr, Inhabited @@ -122,6 +122,7 @@ deriving Inhabited structure ComputedInventoryItem where name : Name + displayName : String category : String locked : Bool disabled : Bool diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index 123269d..95942e3 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -66,6 +66,7 @@ structure DidOpenLevelParams where structure Doc where name: String + displayName: String text: String deriving ToJson @@ -80,7 +81,7 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do -- Execute the regular handling of the `didOpen` event handleDidOpen p let fw ← findFileWorker! m.uri - let s ← get + -- let s ← get let c ← read let some lvl ← GameServer.getLevelByFileName? ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString) | do @@ -132,7 +133,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do return true | Message.request id "loadDoc" params => let p ← parseParams LoadDocParams (toJson params) - let s ← get + -- let s ← get let c ← read let some doc ← getInventoryDoc? p.name p.type | do @@ -140,6 +141,7 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do return true let doc : Doc := { name := doc.name.toString + displayName := doc.displayName text := doc.content } c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩ return true diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean index 3898ba9..d4af11a 100644 --- a/server/testgame/TestGame/LemmaDocs.lean +++ b/server/testgame/TestGame/LemmaDocs.lean @@ -1,7 +1,7 @@ import GameServer.Commands -- Wird im Level "Implication 11" ohne Beweis angenommen. -LemmaDoc not_not as not_not in "Logic" +LemmaDoc not_not as "not_not" in "Logic" " ### Aussage @@ -13,7 +13,7 @@ LemmaDoc not_not as not_not in "Logic" " -- Wird im Level "Implication 10" ohne Beweis angenommen. -LemmaDoc not_or_of_imp as not_or_of_imp in "Logic" +LemmaDoc not_or_of_imp as "not_or_of_imp" in "Logic" " ### Aussage @@ -26,7 +26,7 @@ LemmaDoc not_or_of_imp as not_or_of_imp in "Logic" " -- Wird im Level "Implication 12" bewiesen. -LemmaDoc imp_iff_not_or as imp_iff_not_or in "Logic" +LemmaDoc imp_iff_not_or as "imp_iff_not_or" in "Logic" " ### Aussage @@ -38,42 +38,42 @@ LemmaDoc imp_iff_not_or as imp_iff_not_or in "Logic" " -LemmaDoc Nat.succ_pos as Nat.succ_pos in "Nat" +LemmaDoc Nat.succ_pos as "Nat.succ_pos" in "Nat" " " -LemmaDoc Nat.pos_iff_ne_zero as Nat.pos_iff_ne_zero in "Nat" +LemmaDoc Nat.pos_iff_ne_zero as "Nat.pos_iff_ne_zero" in "Nat" " " -LemmaDoc zero_add as zero_add in "Addition" +LemmaDoc zero_add as "zero_add" in "Addition" "This lemma says `∀ a : ℕ, 0 + a = a`." -LemmaDoc add_zero as add_zero in "Addition" +LemmaDoc add_zero as "add_zero" in "Addition" "This lemma says `∀ a : ℕ, a + 0 = a`." -LemmaDoc add_succ as add_succ in "Addition" +LemmaDoc add_succ as "add_succ" in "Addition" "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`." -LemmaDoc not_forall as not_forall in "Logic" +LemmaDoc not_forall as "not_forall" in "Logic" "`∀ (A : Prop), ¬(∀ x, A) ↔ ∃x, (¬A)`." -LemmaDoc not_exists as not_exists in "Logic" +LemmaDoc not_exists as "not_exists" in "Logic" "`∀ (A : Prop), ¬(∃ x, A) ↔ ∀x, (¬A)`." -DefinitionDoc Even +DefinitionDoc Even as "Even" " `even n` ist definiert als `∃ r, a = 2 * r`. Die Definition kann man mit `unfold even at *` einsetzen. " -DefinitionDoc Odd +DefinitionDoc Odd as "Odd" " `odd n` ist definiert als `∃ r, a = 2 * r + 1`. Die Definition kann man mit `unfold odd at *` einsetzen. " -DefinitionDoc Injective +DefinitionDoc Injective as "Injective" " `Injective f` ist definiert als @@ -83,7 +83,7 @@ DefinitionDoc Injective definiert. " -DefinitionDoc Surjective +DefinitionDoc Surjective as "Surjective" " `Surjective f` ist definiert als @@ -92,19 +92,19 @@ DefinitionDoc Surjective ``` " -DefinitionDoc Bijective +DefinitionDoc Bijective as "Bijective" " " -DefinitionDoc LeftInverse +DefinitionDoc LeftInverse as "LeftInverse" " " -DefinitionDoc RightInverse +DefinitionDoc RightInverse as "RightInverse" " " -DefinitionDoc StrictMono +DefinitionDoc StrictMono as "StrictMono" " `StrictMono f` ist definiert als @@ -114,93 +114,93 @@ DefinitionDoc StrictMono " -LemmaDoc even_iff_not_odd as even_iff_not_odd in "Nat" +LemmaDoc even_iff_not_odd as "even_iff_not_odd" in "Nat" "`Even n ↔ ¬ (Odd n)`" -LemmaDoc odd_iff_not_even as odd_iff_not_even in "Nat" +LemmaDoc odd_iff_not_even as "odd_iff_not_even" in "Nat" "`Odd n ↔ ¬ (Even n)`" -LemmaDoc even_square as even_square in "Nat" +LemmaDoc even_square as "even_square" in "Nat" "`∀ (n : ℕ), Even n → Even (n ^ 2)`" -LemmaDoc mem_univ as mem_univ in "Set" +LemmaDoc mem_univ as "mem_univ" in "Set" "x ∈ @univ α" -LemmaDoc not_mem_empty as not_mem_empty in "Set" +LemmaDoc not_mem_empty as "not_mem_empty" in "Set" "" -LemmaDoc empty_subset as empty_subset in "Set" +LemmaDoc empty_subset as "empty_subset" in "Set" "" -LemmaDoc Subset.antisymm_iff as Subset.antisymm_iff in "Set" +LemmaDoc Subset.antisymm_iff as "Subset.antisymm_iff" in "Set" "" -LemmaDoc Nat.prime_def_lt'' as Nat.prime_def_lt'' in "Nat" +LemmaDoc Nat.prime_def_lt'' as "Nat.prime_def_lt''" in "Nat" "" -LemmaDoc Finset.sum_add_distrib as Finset.sum_add_distrib in "Sum" +LemmaDoc Finset.sum_add_distrib as "Finset.sum_add_distrib" in "Sum" "" -LemmaDoc Fin.sum_univ_castSucc as Fin.sum_univ_castSucc in "Sum" +LemmaDoc Fin.sum_univ_castSucc as "Fin.sum_univ_castSucc" in "Sum" "" -LemmaDoc Nat.succ_eq_add_one as Nat.succ_eq_add_one in "Sum" +LemmaDoc Nat.succ_eq_add_one as "Nat.succ_eq_add_one" in "Sum" "" -LemmaDoc add_comm as add_comm in "Nat" +LemmaDoc add_comm as "add_comm" in "Nat" "" -LemmaDoc mul_add as mul_add in "Nat" +LemmaDoc mul_add as "mul_add" in "Nat" "" -LemmaDoc add_mul as add_mul in "Nat" +LemmaDoc add_mul as "add_mul" in "Nat" "" -LemmaDoc arithmetic_sum as arithmetic_sum in "Sum" +LemmaDoc arithmetic_sum as "arithmetic_sum" in "Sum" "" -LemmaDoc add_pow_two as add_pow_two in "Nat" +LemmaDoc add_pow_two as "add_pow_two" in "Nat" "" -LemmaDoc Finset.sum_comm as Finset.sum_comm in "Sum" +LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum" "" -LemmaDoc Function.comp_apply as Function.comp_apply in "Function" +LemmaDoc Function.comp_apply as "Function.comp_apply" in "Function" "" -LemmaDoc not_le as not_le in "Logic" +LemmaDoc not_le as "not_le" in "Logic" "" -LemmaDoc if_pos as if_pos in "Logic" +LemmaDoc if_pos as "if_pos" in "Logic" "" -LemmaDoc if_neg as if_neg in "Logic" +LemmaDoc if_neg as "if_neg" in "Logic" "" -LemmaDoc StrictMono.injective as StrictMono.injective in "Function" +LemmaDoc StrictMono.injective as "StrictMono.injective" in "Function" "" -LemmaDoc StrictMono.add as StrictMono.add in "Function" +LemmaDoc StrictMono.add as "StrictMono.add" in "Function" "" -LemmaDoc Odd.strictMono_pow as Odd.strictMono_pow in "Function" +LemmaDoc Odd.strictMono_pow as "Odd.strictMono_pow" in "Function" "" -LemmaDoc Exists.choose as Exists.choose in "Function" +LemmaDoc Exists.choose as "Exists.choose" in "Function" "" -LemmaDoc Exists.choose_spec as Exists.choose_spec in "Function" +LemmaDoc Exists.choose_spec as "Exists.choose_spec" in "Function" "" -LemmaDoc congrArg as congrArg in "Function" +LemmaDoc congrArg as "congrArg" in "Function" "" -LemmaDoc congrFun as congrFun in "Function" +LemmaDoc congrFun as "congrFun" in "Function" "" -LemmaDoc Iff.symm as Iff.symm in "Logic" +LemmaDoc Iff.symm as "Iff.symm" in "Logic" ""