Merge branch 'main' of github.com:leanprover-community/lean4game
This commit is contained in:
Jon Eugster
@@ -19,7 +19,7 @@ function Inventory({ tactics, lemmas } :
|
||||
<h2>Tactics</h2>
|
||||
<div className="inventory-list">
|
||||
{ tactics.map(tac =>
|
||||
<InventoryItem key={tac.name} showDoc={() => {setDocName(tac.name); setDocType("tactic")}}
|
||||
<InventoryItem key={tac.name} showDoc={() => {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 } :
|
||||
<h2>Lemmas</h2>
|
||||
<div className="inventory-list">
|
||||
{ lemmas.map(lem =>
|
||||
<InventoryItem key={lem.name} showDoc={() => {setDocName(lem.name); setDocType("lemma")}}
|
||||
<InventoryItem key={lem.name} showDoc={() => {setDocName(lem.name); setDocType("Lemma")}}
|
||||
name={lem.name} locked={lem.locked} disabled={lem.disabled} />) }
|
||||
</div>
|
||||
|
||||
|
||||
@@ -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 })
|
||||
|
||||
instance : Quote LemmaDocEntry `term :=
|
||||
⟨λ entry => Syntax.mkCApp ``LemmaDocEntry.mk #[quote entry.name, quote entry.userName, quote entry.category, quote entry.content]⟩
|
||||
|
||||
/-- 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. -/
|
||||
/-- Declare lemmas that are introduced by this level. -/
|
||||
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}
|
||||
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}}
|
||||
|
||||
/-- 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}}
|
||||
|
||||
/-- 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
|
||||
-- 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 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})
|
||||
-- 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 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
|
||||
-- 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 tactics := tacticsInWorld.find! worldId
|
||||
let mut lemmas := lemmasInWorld.find! worldId
|
||||
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
|
||||
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}
|
||||
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 tacticArray := tactics.toArray
|
||||
|>.insertionSort (fun a b => a.1.toString < b.1.toString)
|
||||
|>.map (·.2)
|
||||
let itemsArray := items.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}
|
||||
modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
|
||||
return level.setComputedInventory inventoryType itemsArray
|
||||
|
||||
@@ -26,77 +26,43 @@ structure GoalHintEntry where
|
||||
hidden : Bool := false
|
||||
deriving Repr
|
||||
|
||||
/-! ## Tactic documentation -/
|
||||
|
||||
structure TacticDocEntry where
|
||||
name : Name
|
||||
content : String
|
||||
deriving ToJson, Repr
|
||||
|
||||
/-- Environment extension for tactic documentation. -/
|
||||
initialize tacticDocExt : SimplePersistentEnvExtension TacticDocEntry (Array TacticDocEntry) ←
|
||||
registerSimplePersistentEnvExtension {
|
||||
name := `tactic_doc
|
||||
addEntryFn := Array.push
|
||||
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
|
||||
for entry in tacticDocExt.getState (← getEnv) do
|
||||
dbg_trace "{entry.name} : {entry.content}"
|
||||
|
||||
/-! ## Lemma documentation -/
|
||||
|
||||
structure LemmaDocEntry where
|
||||
/-! ## Tactic/Definition/Lemma documentation -/
|
||||
|
||||
inductive InventoryType := | Tactic | Lemma | Definition
|
||||
deriving ToJson, FromJson, Repr, BEq, Hashable
|
||||
|
||||
instance : ToString InventoryType := ⟨fun t => match t with
|
||||
| .Tactic => "Tactic"
|
||||
| .Lemma => "Lemma"
|
||||
| .Definition => "Definition"
|
||||
⟩
|
||||
|
||||
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
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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"
|
||||
""
|
||||
|
||||
|
||||
Reference in New Issue
Block a user