{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 */}
@@ -28,7 +28,7 @@ function Inventory({ tactics, lemmas } :
Lemmas
{ lemmas.map(lem =>
- {setDocName(lem.name); setDocType("lemma")}}
+ {setDocName(lem.name); setDocType("Lemma")}}
name={lem.name} locked={lem.locked} disabled={lem.disabled} />) }
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 0b6b924..97c131e 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -180,92 +180,119 @@ macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
macro "HiddenHint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
`(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg)
-/-! ## Tactics -/
+/-! ## Inventory -/
+
+/-- Throw an error if inventory doc does not exist -/
+def checkInventoryDoc (type : InventoryType) (name : Name) : CommandElabM Unit := do
+ let some _ := (inventoryDocExt.getState (← getEnv)).find?
+ (fun x => x.name == name && x.type == type)
+ | throwError "Missing {type} Documentation: {name}"
+
+/-! ### Tactics -/
/-- Declare a documentation entry for some tactic.
Expect an identifier and then a string literal. -/
elab "TacticDoc" name:ident content:str : command =>
- modifyEnv (tacticDocExt.addEntry · {
+ modifyEnv (inventoryDocExt.addEntry · {
+ category := default
+ type := .Tactic
name := name.getId,
+ userName := name.getId,
content := content.getString })
-instance : Quote TacticDocEntry `term :=
-⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
-
-/-- Throw an error if tactic doc does not exist -/
-def checkTacticDoc (name : Name) : CommandElabM Unit := do
- let some _ := (tacticDocExt.getState (← getEnv)).find? (·.name = name)
- | throwError "Missing Tactic Documentation: {name}"
-
/-- Declare tactics that are introduced by this level. -/
elab "NewTactics" args:ident* : command => do
let names := args.map (·.getId)
- for name in names do checkTacticDoc name
- modifyCurLevel fun level => pure {level with newTactics := names}
+ for name in names do checkInventoryDoc .Tactic name
+ modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
/-- Declare tactics that are temporarily disabled in this level -/
elab "DisabledTactics" args:ident* : command => do
let names := args.map (·.getId)
- for name in names do checkTacticDoc name
- modifyCurLevel fun level => pure {level with disabledTactics := names}
+ for name in names do checkInventoryDoc .Tactic name
+ modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
/-- Temporarily disable all tactics except the ones declared here -/
elab "OnlyTactics" args:ident* : command => do
let names := args.map (·.getId)
- for name in names do checkTacticDoc name
- modifyCurLevel fun level => pure {level with onlyTactics := names}
+ for name in names do checkInventoryDoc .Tactic name
+ modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
-/-! ## Lemmas -/
+/-! ### Definitions -/
+
+/-- Declare a documentation entry for some definition.
+Expect an identifier and then a string literal. -/
+elab "DefinitionDoc" name:ident content:str : command =>
+ modifyEnv (inventoryDocExt.addEntry · {
+ category := default
+ type := .Definition
+ name := name.getId,
+ userName := name.getId,
+ content := content.getString })
+
+/-- Declare definitions that are introduced by this level. -/
+elab "NewDefinitions" args:ident* : command => do
+ let names := args.map (·.getId)
+ for name in names do checkInventoryDoc .Definition name
+ modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := names}}
+
+/-- Declare definitions that are temporarily disabled in this level -/
+elab "DisabledDefinitions" args:ident* : command => do
+ let names := args.map (·.getId)
+ for name in names do checkInventoryDoc .Definition name
+ modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := names}}
+
+/-- Temporarily disable all definitions except the ones declared here -/
+elab "OnlyDefinitions" args:ident* : command => do
+ let names := args.map (·.getId)
+ for name in names do checkInventoryDoc .Definition name
+ modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
+
+
+/-! ### 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 =>
- modifyEnv (lemmaDocExt.addEntry · {
+ modifyEnv (inventoryDocExt.addEntry · {
name := name.getId,
+ type := .Lemma
userName := userName.getId,
category := category.getString,
content := content.getString })
-/-- Declare a set of lemma documentation entries.
-Expect an identifier used as the set name then `:=` and a
-space separated list of identifiers. -/
-elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
- let docs := lemmaDocExt.getState (← getEnv)
- let mut entries : Array Name := #[]
- for arg in args do
- let name := arg.getId
- match docs.find? (·.userName = name) with
- | some doc => entries := entries.push name
- | none => throwError "Lemma doc {name} wasn't found."
- modifyEnv (lemmaSetExt.addEntry · {
- name := name.getId,
- title := title.getString,
- lemmas := entries })
+/-- Declare lemmas that are introduced by this level. -/
+elab "NewLemmas" args:ident* : command => do
+ let names := args.map (·.getId)
+ for name in names do checkInventoryDoc .Lemma name
+ modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
-instance : Quote LemmaDocEntry `term :=
-⟨λ entry => Syntax.mkCApp ``LemmaDocEntry.mk #[quote entry.name, quote entry.userName, quote entry.category, quote entry.content]⟩
+/-- Declare lemmas that are temporarily disabled in this level -/
+elab "DisabledLemmas" args:ident* : command => do
+ let names := args.map (·.getId)
+ for name in names do checkInventoryDoc .Lemma name
+ modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
-/-- Declare the list of lemmas that will be displayed in the current level.
-Expects a space separated list of identifiers that refer to either a lemma doc
-entry or a lemma doc set. -/
-elab "NewLemmas" args:ident* : command => do
- let env ← getEnv
- let docs := lemmaDocExt.getState env
- let sets := lemmaSetExt.getState env
- let mut lemmas : Array Name := #[]
- for arg in args do
- let name := arg.getId
- match docs.find? (·.userName = name) with
- | some entry => lemmas := lemmas.push name
- | none => match sets.find? (·.name = name) with
- | some entry => lemmas := lemmas ++ entry.lemmas
- | none => throwError "Lemma doc or lemma set {name} wasn't found."
- modifyCurLevel fun level => pure {level with newLemmas := lemmas}
+/-- Temporarily disable all lemmas except the ones declared here -/
+elab "OnlyLemmas" args:ident* : command => do
+ let names := args.map (·.getId)
+ for name in names do checkInventoryDoc .Lemma name
+ modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
/-! ## Make Game -/
+def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
+| .Tactic => level.tactics
+| .Definition => level.definitions
+| .Lemma => level.lemmas
+
+def GameLevel.setComputedInventory (level : GameLevel) : InventoryType → Array Availability → GameLevel
+| .Tactic, v => {level with tactics := {level.tactics with computed := v}}
+| .Definition, v => {level with definitions := {level.definitions with computed := v}}
+| .Lemma, v => {level with lemmas := {level.lemmas with computed := v}}
+
/-- 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
@@ -275,72 +302,47 @@ elab "MakeGame" : command => do
if game.worlds.hasLoops then
throwError "World graph has loops!"
- -- 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
-
- -- 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 := 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
-
- for (levelId, level) in levels do
- 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 := tacticArray
- lemmas := lemmaArray}
+ -- Compute which inventory items are available in which level:
+ for inventoryType in open InventoryType in #[Tactic, Definition, Lemma] do
+ let mut newItemsInWorld : HashMap Name (HashSet Name) := {}
+ let mut allItems : HashSet Name := {}
+ for (worldId, world) in game.worlds.nodes.toArray do
+ let mut newItems : HashSet Name := {}
+ for (_, level) in world.levels.toArray do
+ newItems := newItems.insertMany (level.getInventory inventoryType).new
+ allItems := allItems.insertMany (level.getInventory inventoryType).new
+ newItemsInWorld := newItemsInWorld.insert worldId newItems
+
+ -- Basic inventory item availability: all locked, none disabled.
+ let Availability₀ : HashMap Name Availability :=
+ HashMap.ofList $
+ allItems.toList.map fun name =>
+ (name, {name, locked := true, disabled := false})
+
+ -- Availability after a given world
+ let mut itemsInWorld : HashMap Name (HashMap Name Availability) := {}
+ for (worldId, _) in game.worlds.nodes.toArray do
+ let mut items := Availability₀
+ let predecessors := game.worlds.predecessors worldId
+ for predWorldId in predecessors do
+ for item in newItemsInWorld.find! predWorldId do
+ items := items.insert item {name := item, locked := false, disabled := false}
+ itemsInWorld := itemsInWorld.insert worldId items
+
+ for (worldId, world) in game.worlds.nodes.toArray do
+ let mut items := itemsInWorld.find! worldId
+
+ let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
+
+ for (levelId, level) in levels do
+ for item in (level.getInventory inventoryType).new do
+ items := items.insert item {name := item, locked := false, disabled := false}
+ for item in (level.getInventory inventoryType).disabled do
+ items := items.insert item {name := item, locked := false, disabled := true}
+
+ let itemsArray := items.toArray
+ |>.insertionSort (fun a b => a.1.toString < b.1.toString)
+ |>.map (·.2)
+
+ modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
+ return level.setComputedInventory inventoryType itemsArray
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 55fe713..1469780 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -26,77 +26,43 @@ structure GoalHintEntry where
hidden : Bool := false
deriving Repr
-/-! ## Tactic documentation -/
-structure TacticDocEntry where
- name : Name
- content : String
- deriving ToJson, Repr
+/-! ## Tactic/Definition/Lemma documentation -/
-/-- Environment extension for tactic documentation. -/
-initialize tacticDocExt : SimplePersistentEnvExtension TacticDocEntry (Array TacticDocEntry) ←
- registerSimplePersistentEnvExtension {
- name := `tactic_doc
- addEntryFn := Array.push
- addImportedFn := Array.concatMap id
- }
+inductive InventoryType := | Tactic | Lemma | Definition
+deriving ToJson, FromJson, Repr, BEq, Hashable
-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
- for entry in tacticDocExt.getState (← getEnv) do
- dbg_trace "{entry.name} : {entry.content}"
-
-/-! ## Lemma documentation -/
+instance : ToString InventoryType := ⟨fun t => match t with
+| .Tactic => "Tactic"
+| .Lemma => "Lemma"
+| .Definition => "Definition"
+⟩
-structure LemmaDocEntry where
+structure InventoryDocEntry where
name : Name
+ type : InventoryType
userName : Name
category : String
content : String
deriving ToJson, Repr
-/-- Environment extension for lemma documentation. -/
-initialize lemmaDocExt : SimplePersistentEnvExtension LemmaDocEntry (Array LemmaDocEntry) ←
+/-- Environment extension for inventory documentation. -/
+initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
registerSimplePersistentEnvExtension {
- name := `lemma_doc
+ name := `inventory_doc
addEntryFn := Array.push
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)
+def getInventoryDoc? {m : Type → Type} [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) :
+ m (Option InventoryDocEntry) := do
+ return (inventoryDocExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type)
open Elab Command in
-/-- Print a lemma doc for debugging purposes. -/
-elab "#print_lemma_doc" : command => do
- for entry in lemmaDocExt.getState (← getEnv) do
- dbg_trace "{entry.userName} ({entry.name}) in {entry.category}: {entry.content}"
-
-structure LemmaSetEntry where
- name : Name
- title : String
- lemmas : Array Name
- deriving ToJson, Repr
-
-/-- Environment extension for lemma sets. -/
-initialize lemmaSetExt : SimplePersistentEnvExtension LemmaSetEntry (Array LemmaSetEntry) ←
- registerSimplePersistentEnvExtension {
- name := `lemma_set
- addEntryFn := Array.push
- addImportedFn := Array.concatMap id
- }
-
-open Elab Command in
-/-- Print all registered lemma sets for debugging purposes. -/
-elab "#print_lemma_set" : command => do
- for entry in lemmaSetExt.getState (← getEnv) do
- dbg_trace "{entry.name} : {entry.lemmas}"
+/-- Print a registered tactic doc for debugging purposes. -/
+elab "#print_doc" : command => do
+ for entry in inventoryDocExt.getState (← getEnv) do
+ dbg_trace "[{entry.type}] {entry.name} : {entry.content}"
/-! ## Environment extensions for game specification-/
@@ -156,7 +122,18 @@ structure Availability where
name : Name
locked : Bool
disabled : Bool
-deriving ToJson, FromJson, Repr
+deriving ToJson, FromJson, Repr, Inhabited
+
+structure InventoryInfo where
+ -- new inventory items introduced by this level:
+ new : Array Name
+ -- inventory items exceptionally forbidden in this level:
+ disabled : Array Name
+ -- only these inventory items are allowed in this level (ignored if empty):
+ only : Array Name
+ -- inventory items in this level (computed by `MakeGame`):
+ computed : Array Availability
+deriving ToJson, FromJson, Repr, Inhabited
def getCurLevelId [MonadError m] : m LevelId := do
return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
@@ -164,37 +141,20 @@ def getCurLevelId [MonadError m] : m LevelId := do
/-- Instance to make GameLevel Repr work -/
instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
-/--
-Fields:
-- TODO
-- introduction: Theory block shown all the time.
-- description: The mathematical statemtent in mathematician-readable form.
-- goal: The statement in Lean.
-- conclusion: Displayed when level is completed.
--/
structure GameLevel where
index: Nat
title: String := default
+ /-- introduction: Theory block shown all the time -/
introduction: String := default
+ /-- The mathematical statemtent in mathematician-readable form -/
description: String := default
+ /-- conclusion displayed when level is completed. -/
conclusion: String := default
- -- new tactics introduces by this level:
- newTactics: Array Name := default
- -- tactics exceptionally forbidden in this level:
- disabledTactics: Array Name := default
- -- only these tactics are allowed in this level (ignore if empty):
- onlyTactics: Array Name := default
- -- tactics in this level (computed by `MakeGame`):
- tactics: Array Availability := default
- -- new lemmas introduces by this level:
- newLemmas: Array Name := default
- -- lemmas exceptionally forbidden in this level:
- disabledLemmas: Array Name := default
- -- only these lemmas are allowed in this level (ignore if empty):
- onlyLemmas: Array Name := default
- -- lemmas in this level (computed by `MakeGame`):
- lemmas: Array Availability := default
+ tactics: InventoryInfo := default
+ definitions: InventoryInfo := default
+ lemmas: InventoryInfo := default
hints: Array GoalHintEntry := default
+ /-- The statement in Lean. -/
goal : TSyntax `Lean.Parser.Command.declSig := default
scope : Elab.Command.Scope := default
descrText: String := default
diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean
index a546350..b16cc9b 100644
--- a/server/leanserver/GameServer/Game.lean
+++ b/server/leanserver/GameServer/Game.lean
@@ -66,27 +66,11 @@ structure Doc where
text: String
deriving ToJson
-inductive TacOrLem := | tactic | «lemma»
-deriving ToJson, FromJson
-
structure LoadDocParams where
name : Name
- type : TacOrLem
+ type : InventoryType
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 }
-
def handleDidOpenLevel (params : Json) : GameServerM Unit := do
let p ← parseParams _ params
let m := p.textDocument
@@ -105,8 +89,8 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do
param := {
uri := m.uri
levelModule := lvl.module
- tactics := lvl.tactics
- lemmas := lvl.lemmas
+ tactics := lvl.tactics.computed
+ lemmas := lvl.lemmas.computed
: DidOpenLevelParams
}
}
@@ -133,8 +117,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
let levelInfo : LevelInfo :=
{ index := lvl.index,
title := lvl.title,
- tactics := lvl.tactics,
- lemmas := lvl.lemmas,
+ tactics := lvl.tactics.computed,
+ lemmas := lvl.lemmas.computed,
descrText := lvl.descrText,
descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO
introduction := lvl.introduction }
@@ -144,10 +128,13 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
let p ← parseParams LoadDocParams (toJson params)
let s ← get
let c ← read
- let some doc ← mkDoc p.name p.type
+ let some doc ← getInventoryDoc? p.name p.type
| do
c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Documentation not found: {p.name}", none⟩
return true
+ let doc : Doc :=
+ { name := doc.name.toString
+ text := doc.content }
c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
return true
| _ => return false
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index f1badf4..dfb8aa6 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -55,9 +55,6 @@ LemmaDoc add_zero as add_zero in "Addition"
LemmaDoc add_succ as add_succ in "Addition"
"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
-LemmaSet addition : "Addition lemmas" :=
-zero_add add_zero
-
LemmaDoc not_forall as not_forall in "Logic"
"`∀ (A : Prop), ¬(∀ x, A) ↔ ∃x, (¬A)`."
@@ -106,14 +103,6 @@ LemmaDoc Nat.prime_def_lt'' as Nat.prime_def_lt'' in "Nat"
""
-
-
-LemmaSet natural : "Natürliche Zahlen" :=
-Even Odd not_odd not_even
-
-LemmaSet logic : "Logik" :=
-not_not not_forall not_exists
-
LemmaDoc Finset.sum_add_distrib as Finset.sum_add_distrib in "Sum"
""