change folder structure
This commit is contained in:
Jon Eugster
@@ -0,0 +1,26 @@
|
||||
import Lean
|
||||
|
||||
section AbstractCtx
|
||||
open Lean
|
||||
open Meta
|
||||
|
||||
structure AbstractCtxResult :=
|
||||
(abstractMVarsResult : AbstractMVarsResult)
|
||||
|
||||
/-- Abstract LCtx and MCtx to transport an expression into different contexts -/
|
||||
def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do
|
||||
let goalDecl ← goal.getDecl
|
||||
let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (mkFVar ·.fvarId)
|
||||
let goal ← mkLambdaFVars (usedLetOnly := false) fvars goalDecl.type
|
||||
let goal ← abstractMVars goal
|
||||
return {
|
||||
abstractMVarsResult := goal
|
||||
}
|
||||
|
||||
def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do
|
||||
let (mvars, binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult
|
||||
lambdaLetTelescope (← instantiateMVars expr) k
|
||||
-- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments.
|
||||
-- If the goal is a function, this will not work.
|
||||
|
||||
end AbstractCtx
|
||||
@@ -0,0 +1,564 @@
|
||||
import GameServer.EnvExtensions
|
||||
|
||||
open Lean Meta Elab Command
|
||||
|
||||
set_option autoImplicit false
|
||||
|
||||
/-! # Game metadata -/
|
||||
|
||||
/-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
|
||||
elab "Game" n:str : command => do
|
||||
let name := n.getString
|
||||
setCurGameId name
|
||||
if (← getGame? name).isNone then
|
||||
insertGame name {name}
|
||||
|
||||
/-- Create a new world in the active game. Example: `World "Addition"` -/
|
||||
elab "World" n:str : command => do
|
||||
let name := n.getString
|
||||
setCurWorldId name
|
||||
if ¬ (← getCurGame).worlds.nodes.contains name then
|
||||
addWorld {name}
|
||||
|
||||
/-- Define the current level number. Levels inside a world must be
|
||||
numbered consecutive starting with `1`. Example: `Level 1` -/
|
||||
elab "Level" level:num : command => do
|
||||
let level := level.getNat
|
||||
setCurLevelIdx level
|
||||
addLevel {index := level}
|
||||
|
||||
/-- Define the title of the current game/world/level. -/
|
||||
elab "Title" t:str : command => do
|
||||
match ← getCurLayer with
|
||||
| .Level => modifyCurLevel fun level => pure {level with title := t.getString}
|
||||
| .World => modifyCurWorld fun world => pure {world with title := t.getString}
|
||||
| .Game => modifyCurGame fun game => pure {game with title := t.getString}
|
||||
|
||||
/-- Define the introduction of the current game/world/level. -/
|
||||
elab "Introduction" t:str : command => do
|
||||
match ← getCurLayer with
|
||||
| .Level => modifyCurLevel fun level => pure {level with introduction := t.getString}
|
||||
| .World => modifyCurWorld fun world => pure {world with introduction := t.getString}
|
||||
| .Game => modifyCurGame fun game => pure {game with introduction := t.getString}
|
||||
|
||||
/-- Define the conclusion of the current game or current level if some
|
||||
building a level. -/
|
||||
elab "Conclusion" t:str : command => do
|
||||
match ← getCurLayer with
|
||||
| .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString}
|
||||
| .World => modifyCurWorld fun world => pure {world with conclusion := t.getString}
|
||||
| .Game => modifyCurGame fun game => pure {game with conclusion := t.getString}
|
||||
|
||||
/-! ## World Paths -/
|
||||
|
||||
/-- The worlds of a game are joint by paths. These are defined with the syntax
|
||||
`Path World₁ → World₂ → World₃`. -/
|
||||
def Parser.path := Parser.sepBy1Indent Parser.ident "→"
|
||||
|
||||
/-- The worlds of a game are joint by paths. These are defined with the syntax
|
||||
`Path World₁ → World₂ → World₃`. -/
|
||||
elab "Path" s:Parser.path : command => do
|
||||
let mut last : Option Name := none
|
||||
for stx in s.raw.getArgs.getEvenElems do
|
||||
let some l := last
|
||||
| do
|
||||
last := some stx.getId
|
||||
continue
|
||||
modifyCurGame fun game =>
|
||||
pure {game with worlds := {game.worlds with edges := game.worlds.edges.push (l, stx.getId)}}
|
||||
last := some stx.getId
|
||||
|
||||
|
||||
|
||||
/-! # Inventory
|
||||
|
||||
The inventory contains docs for tactics, lemmas, and definitions. These are all disabled
|
||||
in the first level and get enabled during the game.
|
||||
-/
|
||||
|
||||
/-! ## Doc entries -/
|
||||
|
||||
/-- 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} (add `{type}Doc {name}` in your game's docs section)"
|
||||
|
||||
/-- 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
|
||||
displayName := name.getId.toString
|
||||
content := content.getString })
|
||||
|
||||
/-- 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
|
||||
displayName := displayName.getString,
|
||||
category := category.getString,
|
||||
content := content.getString })
|
||||
|
||||
/-- 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,
|
||||
displayName := displayName.getString,
|
||||
content := content.getString })
|
||||
|
||||
/-! ## Add inventory items -/
|
||||
|
||||
/-- Declare tactics that are introduced by this level. -/
|
||||
elab "NewTactic" args:ident* : command => do
|
||||
let names := args.map (·.getId)
|
||||
for name in names do checkInventoryDoc .Tactic name
|
||||
modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
|
||||
|
||||
/-- Declare lemmas that are introduced by this level. -/
|
||||
elab "NewLemma" 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}}
|
||||
|
||||
/-- Declare definitions that are introduced by this level. -/
|
||||
elab "NewDefinition" 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 tactics that are temporarily disabled in this level.
|
||||
This is ignored if `OnlyTactic` is set. -/
|
||||
elab "DisabledTactic" args:ident* : command => do
|
||||
let names := args.map (·.getId)
|
||||
-- for name in names do checkInventoryDoc .Tactic name
|
||||
modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
|
||||
|
||||
/-- Declare lemmas that are temporarily disabled in this level.
|
||||
This is ignored if `OnlyLemma` is set. -/
|
||||
elab "DisabledLemma" 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 definitions that are temporarily disabled in this level -/
|
||||
elab "DisabledDefinition" 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 tactics except the ones declared here -/
|
||||
elab "OnlyTactic" args:ident* : command => do
|
||||
let names := args.map (·.getId)
|
||||
for name in names do checkInventoryDoc .Tactic name
|
||||
modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
|
||||
|
||||
/-- Temporarily disable all lemmas except the ones declared here -/
|
||||
elab "OnlyLemma" 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}}
|
||||
|
||||
/-- Temporarily disable all definitions except the ones declared here.
|
||||
This is ignored if `OnlyDefinition` is set. -/
|
||||
elab "OnlyDefinition" 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}}
|
||||
|
||||
/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
|
||||
If omitted, the current tab will remain open. -/
|
||||
elab "LemmaTab" category:str : command =>
|
||||
modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
|
||||
|
||||
/-! # Exercise Statement -/
|
||||
|
||||
-- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
|
||||
-- us highlighting on the client side.
|
||||
partial def reprintCore : Syntax → Option Format
|
||||
| Syntax.missing => none
|
||||
| Syntax.atom _ val => val.trim
|
||||
| Syntax.ident _ rawVal _ _ => rawVal.toString
|
||||
| Syntax.node _ _ args =>
|
||||
match args.toList.filterMap reprintCore with
|
||||
| [] => none
|
||||
| [arg] => arg
|
||||
| args => Format.group <| Format.nest 2 <| Format.joinSep args " "
|
||||
|
||||
/-- `reprint` is used to display the Lean-statement to the user-/
|
||||
def reprint (stx : Syntax) : Format :=
|
||||
reprintCore stx |>.getD ""
|
||||
|
||||
/-- Define the statement of the current level. -/
|
||||
elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
|
||||
let lvlIdx ← getCurLevelIdx
|
||||
|
||||
-- Save the messages before evaluation of the proof.
|
||||
let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
|
||||
|
||||
-- Check that statement has a docs entry.
|
||||
match statementName with
|
||||
| some name => checkInventoryDoc .Lemma name.getId
|
||||
| none => pure ()
|
||||
|
||||
-- The default name of the statement is `[Game].[World].level[no.]`, e.g. `NNG.Addition.level1`
|
||||
-- However, this should not be used when designing the game.
|
||||
let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
|
||||
("level" ++ toString lvlIdx : String)
|
||||
|
||||
-- Add theorem to context.
|
||||
match statementName with
|
||||
| some name =>
|
||||
let env ← getEnv
|
||||
if env.contains name.getId then
|
||||
let origType := (env.constants.map₁.find! name.getId).type
|
||||
-- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
|
||||
-- in that case.
|
||||
logWarningAt name m!"Environment already contains {name.getId}!
|
||||
Only the existing statement will be available in later levels:
|
||||
|
||||
{origType}"
|
||||
-- let (binders, typeStx) := expandDeclSig sig
|
||||
-- --let type ← Term.elabType typeStx
|
||||
-- runTermElabM (fun vars =>
|
||||
-- Term.elabBinders binders.getArgs (fun xs => do
|
||||
-- let type ← Term.elabType typeStx
|
||||
-- --Term.synthesizeSyntheticMVarsNoPostponing
|
||||
-- --let type ← instantiateMVars type
|
||||
-- --let type ← mkForallFVars xs type
|
||||
-- ))
|
||||
--let newType := Term.elabTerm sig.raw
|
||||
--dbg_trace newType
|
||||
--logInfo origType
|
||||
-- dbg_trace sig
|
||||
-- dbg_trace origType
|
||||
--dbg_trace (env.constants.map₁.find! name.getId).value! -- that's the proof
|
||||
--let newType := Lean.Elab.Term.elabTerm sig none
|
||||
|
||||
let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
|
||||
elabCommand thmStatement
|
||||
else
|
||||
let thmStatement ← `(theorem $(mkIdent name.getId) $sig $val)
|
||||
elabCommand thmStatement
|
||||
| none =>
|
||||
let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
|
||||
elabCommand thmStatement
|
||||
|
||||
let msgs := (← get).messages
|
||||
|
||||
let mut hints := #[]
|
||||
let mut nonHintMsgs := #[]
|
||||
for msg in msgs.msgs do
|
||||
-- Look for messages produced by the `Hint` tactic. They are used to pass information about the
|
||||
-- intermediate goal state
|
||||
if let MessageData.withNamingContext _ $ MessageData.withContext ctx $
|
||||
.tagged `Hint $
|
||||
.nest strict $
|
||||
.nest hidden $
|
||||
.compose (.ofGoal text) (.ofGoal goal) := msg.data then
|
||||
let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
|
||||
return {
|
||||
goal := ← abstractCtx goal
|
||||
text := ← instantiateMVars (mkMVar text)
|
||||
strict := strict == 1
|
||||
hidden := hidden == 1
|
||||
}
|
||||
hints := hints.push hint
|
||||
else
|
||||
nonHintMsgs := nonHintMsgs.push msg
|
||||
|
||||
-- restore saved messages and non-hint messages
|
||||
modify fun st => { st with
|
||||
messages := initMsgs ++ ⟨nonHintMsgs.toPArray'⟩
|
||||
}
|
||||
|
||||
let scope ← getScope
|
||||
let env ← getEnv
|
||||
|
||||
modifyCurLevel fun level => pure {level with
|
||||
module := env.header.mainModule
|
||||
goal := sig,
|
||||
scope := scope,
|
||||
descrText := match descr with
|
||||
| none => ""
|
||||
| some s => s.getString
|
||||
statementName := match statementName with
|
||||
| none => default
|
||||
| some name => name.getId
|
||||
descrFormat := match statementName with
|
||||
| none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
|
||||
| some name => (Format.join ["theorem ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10 -- "lemma " ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
|
||||
hints := hints
|
||||
} -- Format.pretty <| format thmStatement.raw }
|
||||
|
||||
|
||||
|
||||
/-! # Hints -/
|
||||
|
||||
syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
|
||||
|
||||
/-- Remove any spaces at the beginning of a new line -/
|
||||
partial def removeIndentation (s : String) : String :=
|
||||
let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
|
||||
let c := s.get i
|
||||
let i := s.next i
|
||||
if s.atEnd i then
|
||||
acc.push c
|
||||
else if removeSpaces && c == ' ' then
|
||||
loop i acc (removeSpaces := true)
|
||||
else if c == '\n' then
|
||||
loop i (acc.push c) (removeSpaces := true)
|
||||
else
|
||||
loop i (acc.push c)
|
||||
loop ⟨0⟩ ""
|
||||
|
||||
/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
|
||||
see hints. The tactic does not affect the goal state.
|
||||
-/
|
||||
elab "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
|
||||
let mut strict := false
|
||||
let mut hidden := false
|
||||
|
||||
-- remove spaces at the beginngng of new lines
|
||||
let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
|
||||
match m with
|
||||
| Syntax.node info k args =>
|
||||
if k == interpolatedStrLitKind && args.size == 1 then
|
||||
match args.get! 0 with
|
||||
| (Syntax.atom info' val) =>
|
||||
let val := removeIndentation val
|
||||
return Syntax.node info k #[Syntax.atom info' val]
|
||||
| _ => return m
|
||||
else
|
||||
return m
|
||||
| _ => return m
|
||||
|
||||
for arg in args do
|
||||
match arg with
|
||||
| `(hintArg| (strict := true)) => strict := true
|
||||
| `(hintArg| (strict := false)) => strict := false
|
||||
| `(hintArg| (hidden := true)) => hidden := true
|
||||
| `(hintArg| (hidden := false)) => hidden := false
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
let goal ← Tactic.getMainGoal
|
||||
goal.withContext do
|
||||
-- We construct an expression that can produce the hint text. The difficulty is that we
|
||||
-- want the text to possibly contain quotation of the local variables which might have been
|
||||
-- named differently by the player.
|
||||
let varsName := `vars
|
||||
let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
|
||||
let mut text ← `(m! $msg)
|
||||
let goalDecl ← goal.getDecl
|
||||
let decls := goalDecl.lctx.decls.toArray.filterMap id
|
||||
for i in [:decls.size] do
|
||||
text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
|
||||
return ← mkLambdaFVars #[vars] $ ← Term.elabTermAndSynthesize text none
|
||||
let textmvar ← mkFreshExprMVar none
|
||||
guard $ ← isDefEq textmvar text -- Store the text in a mvar.
|
||||
-- The information about the hint is logged as a message using `logInfo` to transfer it to the
|
||||
-- `Statement` command:
|
||||
logInfo $
|
||||
.tagged `Hint $
|
||||
.nest (if strict then 1 else 0) $
|
||||
.nest (if hidden then 1 else 0) $
|
||||
.compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
|
||||
|
||||
/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
|
||||
proof state. We use it to define Hints for alternative proof methods or dead ends. -/
|
||||
elab "Branch" t:tacticSeq : tactic => do
|
||||
let b ← saveState
|
||||
Tactic.evalTactic t
|
||||
|
||||
-- Show an info whether the branch proofs all remaining goals.
|
||||
let gs ← Tactic.getUnsolvedGoals
|
||||
if gs.isEmpty then
|
||||
logInfo "This branch finishes the proof."
|
||||
else
|
||||
logInfo "This branch leaves open goals."
|
||||
|
||||
let msgs ← Core.getMessageLog
|
||||
b.restore
|
||||
Core.setMessageLog msgs
|
||||
|
||||
|
||||
|
||||
/-! # 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 ComputedInventoryItem → 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}}
|
||||
|
||||
/-- Build the game. This command will precompute various things about the game, such as which
|
||||
tactics are available in each level etc. -/
|
||||
elab "MakeGame" : command => do
|
||||
let game ← getCurGame
|
||||
|
||||
-- Check for loops in world graph
|
||||
if game.worlds.hasLoops then
|
||||
throwError "World graph must not contain loops! Check your `Path` declarations."
|
||||
|
||||
-- Compute which inventory items are available in which level:
|
||||
for inventoryType in #[.Tactic, .Definition, .Lemma] do
|
||||
let mut newItemsInWorld : HashMap Name (HashSet Name) := {}
|
||||
let mut lemmaStatements : HashMap (Name × Nat) Name := {}
|
||||
let mut allItems : HashSet Name := {}
|
||||
for (worldId, world) in game.worlds.nodes.toArray do
|
||||
let mut newItems : HashSet Name := {}
|
||||
for (levelId, level) in world.levels.toArray do
|
||||
let newLemmas := (level.getInventory inventoryType).new
|
||||
newItems := newItems.insertMany newLemmas
|
||||
allItems := allItems.insertMany newLemmas
|
||||
if inventoryType == .Lemma then
|
||||
-- For levels `2, 3, …` we check if the previous level was named
|
||||
-- in which case we add it as available lemma.
|
||||
match levelId with
|
||||
| 0 => pure ()
|
||||
| 1 => pure () -- level ids start with 1, so we need to skip 1, too.
|
||||
| i₀ + 1 =>
|
||||
-- add named statement from previous level to the available lemmas.
|
||||
match (world.levels.find! (i₀)).statementName with
|
||||
| .anonymous => pure ()
|
||||
| .num _ _ => panic "Did not expect to get a numerical statement name!"
|
||||
| .str pre s =>
|
||||
let name := Name.str pre s
|
||||
newItems := newItems.insert name
|
||||
allItems := allItems.insert name
|
||||
lemmaStatements := lemmaStatements.insert (worldId, levelId) name
|
||||
if inventoryType == .Lemma then
|
||||
-- if named, add the lemma from the last level of the world to the inventory
|
||||
let i₀ := world.levels.size
|
||||
match (world.levels.find! (i₀)).statementName with
|
||||
| .anonymous => pure ()
|
||||
| .num _ _ => panic "Did not expect to get a numerical statement name!"
|
||||
| .str pre s =>
|
||||
let name := Name.str pre s
|
||||
newItems := newItems.insert name
|
||||
allItems := allItems.insert name
|
||||
newItemsInWorld := newItemsInWorld.insert worldId newItems
|
||||
|
||||
-- Basic inventory item availability: all locked.
|
||||
let Availability₀ : HashMap Name ComputedInventoryItem :=
|
||||
HashMap.ofList $
|
||||
← allItems.toList.mapM fun item => do
|
||||
let data := (← getInventoryDoc? item inventoryType).get!
|
||||
return (item, {
|
||||
name := item
|
||||
displayName := data.displayName
|
||||
category := data.category
|
||||
locked := true })
|
||||
|
||||
-- Availability after a given world
|
||||
let mut itemsInWorld : HashMap Name (HashMap Name ComputedInventoryItem) := {}
|
||||
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
|
||||
let data := (← getInventoryDoc? item inventoryType).get!
|
||||
items := items.insert item {
|
||||
name := item
|
||||
displayName := data.displayName
|
||||
category := data.category
|
||||
locked := 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
|
||||
let levelInfo := level.getInventory inventoryType
|
||||
|
||||
-- add items in `levelInfo.new` permanently as unlocked
|
||||
for item in levelInfo.new do
|
||||
let data := (← getInventoryDoc? item inventoryType).get!
|
||||
items := items.insert item {
|
||||
name := item
|
||||
displayName := data.displayName
|
||||
category := data.category
|
||||
locked := false }
|
||||
|
||||
-- add the statement from the previous level permanently as unlocked
|
||||
if inventoryType == .Lemma then
|
||||
match lemmaStatements.find? (worldId, levelId) with
|
||||
| none => pure ()
|
||||
| some name =>
|
||||
let data := (← getInventoryDoc? name inventoryType).get!
|
||||
items := items.insert name {
|
||||
name := name
|
||||
displayName := data.displayName
|
||||
category := data.category
|
||||
locked := false }
|
||||
|
||||
let itemsArray := items.toArray
|
||||
|>.insertionSort (fun a b => a.1.toString < b.1.toString)
|
||||
|>.map (·.2)
|
||||
|>.map (fun item => { item with
|
||||
-- if `levelInfo.only` is set, disable everything not in there,
|
||||
-- otherwise disable all in `levelInfo.disabled`
|
||||
disabled := if levelInfo.only.size == 0 then
|
||||
levelInfo.disabled.contains item.name
|
||||
else
|
||||
not (levelInfo.only.contains item.name)
|
||||
})
|
||||
|
||||
modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
|
||||
return level.setComputedInventory inventoryType itemsArray
|
||||
|
||||
|
||||
|
||||
/-! # Debugging tools -/
|
||||
|
||||
-- /-- Print current game for debugging purposes. -/
|
||||
-- elab "PrintCurGame" : command => do
|
||||
-- logInfo (toJson (← getCurGame))
|
||||
|
||||
/-- Print current level for debugging purposes. -/
|
||||
elab "PrintCurLevel" : command => do
|
||||
logInfo (repr (← getCurLevel))
|
||||
|
||||
/-- Print levels for debugging purposes. -/
|
||||
elab "PrintLevels" : command => do
|
||||
logInfo $ repr $ (← getCurWorld).levels.toArray
|
||||
@@ -0,0 +1,344 @@
|
||||
import GameServer.AbstractCtx
|
||||
import GameServer.Graph
|
||||
|
||||
/-! # Environment extensions
|
||||
|
||||
The game framework stores almost all its game building data in environment extensions
|
||||
defined in this file.
|
||||
-/
|
||||
|
||||
open Lean
|
||||
|
||||
/-! ## Hints -/
|
||||
|
||||
/--
|
||||
A hint to help the user with a specific goal state
|
||||
-/
|
||||
structure GoalHintEntry where
|
||||
goal : AbstractCtxResult
|
||||
/-- Text of the hint as an expression of type `Array Expr → MessageData` -/
|
||||
text : Expr
|
||||
/-- If true, then hint should be hidden and only be shown on player's request -/
|
||||
hidden : Bool := false
|
||||
/-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
|
||||
strict : Bool := false
|
||||
|
||||
instance : Repr GoalHintEntry := {
|
||||
reprPrec := fun a n => reprPrec a.text n
|
||||
}
|
||||
|
||||
/-! ## Tactic/Definition/Lemma documentation -/
|
||||
|
||||
inductive InventoryType := | Tactic | Lemma | Definition
|
||||
deriving ToJson, FromJson, Repr, BEq, Hashable, Inhabited
|
||||
|
||||
instance : ToString InventoryType := ⟨fun t => match t with
|
||||
| .Tactic => "Tactic"
|
||||
| .Lemma => "Lemma"
|
||||
| .Definition => "Definition"
|
||||
⟩
|
||||
|
||||
/-- An inventory item represents the documentation of a tactic/lemma/definitions. -/
|
||||
structure InventoryDocEntry where
|
||||
/--
|
||||
The name of the item. The restrictions are:
|
||||
|
||||
* for Tactics: The name of the tactic.
|
||||
* for Lemmas: *Fully qualified* lemma name.
|
||||
* for Definitions: no restrictions.
|
||||
-/
|
||||
name : Name
|
||||
/-- One of `Tactic`, `Lemma` and `Definition`. -/
|
||||
type : InventoryType
|
||||
/-- The display name shown in the inventory. This can be free-text. -/
|
||||
displayName : String
|
||||
/-- Category to group inventory items by. (currently only used for lemmas) -/
|
||||
category : String
|
||||
/-- The description (doc) of the item. (free-text) -/
|
||||
content : String
|
||||
deriving ToJson, Repr, Inhabited
|
||||
|
||||
structure ComputedInventoryItem where
|
||||
/--
|
||||
The name of the item. The restrictions are:
|
||||
|
||||
* for Tactics: The name of the tactic.
|
||||
* for Lemmas: *Fully qualified* lemma name.
|
||||
* for Definitions: no restrictions.
|
||||
-/
|
||||
name : Name
|
||||
/-- The display name shown in the inventory. This can be free-text. -/
|
||||
displayName : String
|
||||
/-- Category to group inventory items by (currently only used for lemmas). -/
|
||||
category : String
|
||||
/-- If `true` then the item only gets unlocked in a later level. -/
|
||||
locked : Bool
|
||||
/-- If `true` then the item is blocked for this level. -/
|
||||
disabled : Bool := false
|
||||
deriving ToJson, FromJson, Repr, Inhabited
|
||||
|
||||
/-- Environment extension for inventory documentation. -/
|
||||
initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
|
||||
registerSimplePersistentEnvExtension {
|
||||
name := `inventory_doc
|
||||
addEntryFn := Array.push
|
||||
addImportedFn := Array.concatMap id
|
||||
}
|
||||
|
||||
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 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-/
|
||||
|
||||
/-- Register a (non-persistent) environment extension to hold the current level -/
|
||||
initialize curGameExt : EnvExtension (Option Name) ← registerEnvExtension (pure none)
|
||||
/-- Register a (non-persistent) environment extension to hold the current level -/
|
||||
initialize curWorldExt : EnvExtension (Option Name) ← registerEnvExtension (pure none)
|
||||
/-- Register a (non-persistent) environment extension to hold the current level -/
|
||||
initialize curLevelExt : EnvExtension (Option Nat) ← registerEnvExtension (pure none)
|
||||
|
||||
inductive Layer :=
|
||||
| Game | World | Level
|
||||
|
||||
variable {m: Type → Type} [Monad m] [MonadEnv m]
|
||||
|
||||
def setCurGameId (game : Name) : m Unit :=
|
||||
modifyEnv (curGameExt.setState · (some game))
|
||||
|
||||
def setCurWorldId (world : Name) : m Unit :=
|
||||
modifyEnv (curWorldExt.setState · (some world))
|
||||
|
||||
def setCurLevelIdx (level : Nat) : m Unit :=
|
||||
modifyEnv (curLevelExt.setState · (some level))
|
||||
|
||||
def getCurLayer [MonadError m] : m Layer := do
|
||||
match curGameExt.getState (← getEnv), curWorldExt.getState (← getEnv), curLevelExt.getState (← getEnv) with
|
||||
| some _, some _, some _ => return Layer.Level
|
||||
| some _, some _, none => return Layer.World
|
||||
| some _, none, none => return Layer.Game
|
||||
| _, _, _ => throwError "Invalid Layer"
|
||||
|
||||
def getCurGameId [MonadError m] : m Name := do
|
||||
match curGameExt.getState (← getEnv) with
|
||||
| some game => return game
|
||||
| none => throwError "Current game not set"
|
||||
|
||||
def getCurWorldId [MonadError m] : m Name := do
|
||||
match curWorldExt.getState (← getEnv) with
|
||||
| some world => return world
|
||||
| none => throwError "Current world not set"
|
||||
|
||||
def getCurLevelIdx [MonadError m] : m Nat := do
|
||||
match curLevelExt.getState (← getEnv) with
|
||||
| some level => return level
|
||||
| none => throwError "Current level not set"
|
||||
|
||||
/-! ## Levels -/
|
||||
|
||||
structure LevelId where
|
||||
game : Name
|
||||
world : Name
|
||||
level : Nat
|
||||
deriving 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 ComputedInventoryItem
|
||||
deriving ToJson, FromJson, Repr, Inhabited
|
||||
|
||||
def getCurLevelId [MonadError m] : m LevelId := do
|
||||
return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
|
||||
|
||||
/-- Instance to make GameLevel Repr work -/
|
||||
instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
|
||||
|
||||
structure GameLevel where
|
||||
index: Nat
|
||||
/-- The title of the level. -/
|
||||
title: String := default
|
||||
/-- Introduction text shown all the time. (markdown) -/
|
||||
introduction: String := default
|
||||
conclusion: String := default
|
||||
/-- The name of the exercise proven. If provided this lemma will be available in
|
||||
future levels. -/
|
||||
statementName: Name := default
|
||||
hints: Array GoalHintEntry := default
|
||||
/-- The statement in Lean. -/
|
||||
goal : TSyntax `Lean.Parser.Command.declSig := default
|
||||
scope : Elab.Command.Scope := default
|
||||
/-- The mathematical statement in mathematician-readable form. (markdown) -/
|
||||
descrText: String := default
|
||||
descrFormat : String := default
|
||||
/-- The `category` of lemmas to be open by default -/
|
||||
lemmaTab: Option String := none
|
||||
/-- The module to be imported when playing this level -/
|
||||
module : Name := default
|
||||
tactics: InventoryInfo := default
|
||||
definitions: InventoryInfo := default
|
||||
lemmas: InventoryInfo := default
|
||||
deriving Inhabited, Repr
|
||||
|
||||
|
||||
/-! ## World -/
|
||||
|
||||
/-- A world is a collection of levels, like a chapter. -/
|
||||
structure World where
|
||||
/- Internal name of the world. Not visible to the player. -/
|
||||
name: Name
|
||||
/-- Display title of the world. -/
|
||||
title: String := default
|
||||
/-- World introduction to be shown before the first level is loaded. (markdown) -/
|
||||
introduction: String := default
|
||||
/-- TODO: This is currently unused. -/
|
||||
conclusion : String := default
|
||||
/-- The levels of the world. -/
|
||||
levels: HashMap Nat GameLevel := default
|
||||
deriving Inhabited
|
||||
|
||||
instance : ToJson World := ⟨
|
||||
fun world => Json.mkObj [
|
||||
("name", toJson world.name),
|
||||
("title", world.title),
|
||||
("introduction", world.introduction)]
|
||||
⟩
|
||||
|
||||
/-! ## Game -/
|
||||
|
||||
structure Game where
|
||||
/-- Internal name of the game. -/
|
||||
name : Name
|
||||
/-- TODO: currently unused. -/
|
||||
title : String := default
|
||||
/-- Text displayed on the main landing page of the game. -/
|
||||
introduction : String := default
|
||||
/-- TODO: currently unused. -/
|
||||
conclusion : String := default
|
||||
/-- TODO: currently unused. -/
|
||||
authors : List String := default
|
||||
worlds : Graph Name World := default
|
||||
deriving Inhabited, ToJson
|
||||
|
||||
/-! ## Game environment extension -/
|
||||
|
||||
def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) :
|
||||
HashMap α β :=
|
||||
new.fold (fun acc a b =>
|
||||
if let some bOld := acc.find? a
|
||||
then acc.insert a (merge bOld b)
|
||||
else acc.insert a b) old
|
||||
|
||||
def GameLevel.merge (old : GameLevel) (new : GameLevel) : GameLevel :=
|
||||
new -- simply override old level
|
||||
|
||||
def World.merge (old : World) (new : World) : World :=
|
||||
{ new with
|
||||
levels := HashMap.merge old.levels new.levels GameLevel.merge}
|
||||
|
||||
def Game.merge (old : Game) (new : Game) : Game :=
|
||||
{ new with
|
||||
worlds := {
|
||||
nodes := HashMap.merge old.worlds.nodes new.worlds.nodes World.merge
|
||||
edges := Id.run do
|
||||
let mut res := old.worlds.edges
|
||||
for e in new.worlds.edges do
|
||||
if ¬ res.contains e then
|
||||
res := res.push e
|
||||
return res
|
||||
} }
|
||||
|
||||
initialize gameExt : PersistentEnvExtension (Name × Game) (Name × Game) (HashMap Name Game) ←
|
||||
do registerPersistentEnvExtension {
|
||||
name := `gameExt,
|
||||
mkInitial := pure {},
|
||||
addImportedFn := fun ess => do
|
||||
let mut games := {}
|
||||
for es in ess do
|
||||
for (name, game) in es do
|
||||
match games.find? name with
|
||||
| some oldgame =>
|
||||
games := games.insert name (Game.merge oldgame game)
|
||||
| none =>
|
||||
games := games.insert name game
|
||||
return games
|
||||
addEntryFn := (λ s n => s.insert n.1 n.2),
|
||||
exportEntriesFn := HashMap.toArray,
|
||||
statsFn := fun s => format "number of local entries: " ++ format s.size
|
||||
}
|
||||
|
||||
def getGame? (n : Name) : m (Option Game) := do
|
||||
return (gameExt.getState (← getEnv)).find? n
|
||||
|
||||
def insertGame (n : Name) (g : Game) : m Unit := do
|
||||
modifyEnv (gameExt.addEntry · (n, g))
|
||||
|
||||
def getLevel? (levelId : LevelId) : m (Option GameLevel) := do
|
||||
let some game ← getGame? levelId.game
|
||||
| return none
|
||||
let some world := game.worlds.nodes.find? levelId.world
|
||||
| return none
|
||||
let some level := world.levels.find? levelId.level
|
||||
| return none
|
||||
return level
|
||||
|
||||
def getCurGame [MonadError m] : m Game := do
|
||||
let some game ← getGame? (← getCurGameId)
|
||||
| throwError m!"Game {← getCurGameId} does not exist"
|
||||
return game
|
||||
|
||||
def modifyCurGame (fn : Game → m Game) [MonadError m] : m Unit := do
|
||||
let game ← getCurGame
|
||||
insertGame game.name (← fn game)
|
||||
|
||||
def addWorld (world : World) [MonadError m] : m Unit := do
|
||||
modifyCurGame fun game => do
|
||||
return {game with worlds := game.worlds.insertNode world.name world}
|
||||
|
||||
def getCurWorld [MonadError m] : m World := do
|
||||
let some world := (← getCurGame).worlds.nodes.find? (← getCurWorldId)
|
||||
| throwError m!"World {← getCurWorldId} does not exist"
|
||||
return world
|
||||
|
||||
def modifyCurWorld (fn : World → m World) [MonadError m] : m Unit := do
|
||||
modifyCurGame fun game => do
|
||||
let world ← getCurWorld
|
||||
return {game with worlds := {game.worlds with nodes := game.worlds.nodes.insert world.name (← fn world) }}
|
||||
|
||||
def addLevel (level : GameLevel) [MonadError m] : m Unit := do
|
||||
modifyCurWorld fun world => do
|
||||
return {world with levels := world.levels.insert level.index level}
|
||||
|
||||
def getCurLevel [MonadError m] : m GameLevel := do
|
||||
let some level := (← getCurWorld).levels.find? (← getCurLevelIdx)
|
||||
| throwError m!"Level {← getCurLevelIdx} does not exist"
|
||||
return level
|
||||
|
||||
def modifyCurLevel (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
|
||||
modifyCurWorld fun world => do
|
||||
let level ← getCurLevel
|
||||
return {world with levels := world.levels.insert level.index (← fn level)}
|
||||
|
||||
def modifyLevel (levelId : LevelId) (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
|
||||
let some game ← getGame? levelId.game
|
||||
| throwError m!"Game {levelId.game} does not exist"
|
||||
let some world := (← getCurGame).worlds.nodes.find? levelId.world
|
||||
| throwError m!"World {levelId.world} does not exist"
|
||||
let some level := world.levels.find? levelId.level
|
||||
| throwError m!"Level {levelId.level} does not exist"
|
||||
let level' ← fn level
|
||||
let world' := {world with levels := world.levels.insert levelId.level level'}
|
||||
let game' := {game with worlds := game.worlds.insertNode levelId.world world'}
|
||||
insertGame levelId.game game'
|
||||
@@ -0,0 +1,561 @@
|
||||
/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
|
||||
import Lean.Server.FileWorker
|
||||
import GameServer.Game
|
||||
|
||||
namespace MyModule
|
||||
open Lean
|
||||
open Elab
|
||||
open Parser
|
||||
|
||||
private def mkErrorMessage (c : InputContext) (pos : String.Pos) (errorMsg : String) : Message :=
|
||||
let pos := c.fileMap.toPosition pos
|
||||
{ fileName := c.fileName, pos := pos, data := errorMsg }
|
||||
|
||||
private def mkEOI (pos : String.Pos) : Syntax :=
|
||||
let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""
|
||||
mkNode ``Command.eoi #[atom]
|
||||
|
||||
partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
|
||||
(mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
|
||||
Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
|
||||
let mut pos := mps.pos
|
||||
let mut recovering := mps.recovering
|
||||
let mut messages := messages
|
||||
let mut stx := Syntax.missing -- will always be assigned below
|
||||
|
||||
let tokens := getTokenTable pmctx.env
|
||||
|
||||
let s := whitespace.run inputCtx pmctx tokens { cache := initCacheForInput inputCtx.input, pos }
|
||||
let endOfWhitespace := s.pos
|
||||
|
||||
let p := (Tactic.sepByIndentSemicolon tacticParser).fn
|
||||
let s := p.run inputCtx pmctx tokens { cache := initCacheForInput inputCtx.input, pos }
|
||||
|
||||
pos := s.pos
|
||||
match s.errorMsg with
|
||||
| none =>
|
||||
stx := s.stxStack.back
|
||||
recovering := false
|
||||
| some errorMsg =>
|
||||
messages := messages.add <| mkErrorMessage inputCtx s.pos (toString errorMsg)
|
||||
recovering := true
|
||||
stx := s.stxStack.back
|
||||
if ¬ inputCtx.input.atEnd s.pos then
|
||||
messages := messages.add <| mkErrorMessage inputCtx s.pos "end of input"
|
||||
return (stx, { pos := inputCtx.input.endPos, recovering }, messages, endOfWhitespace)
|
||||
|
||||
end MyModule
|
||||
|
||||
namespace MyServer.FileWorker
|
||||
open Lean
|
||||
open Lean.Server
|
||||
open Lean.Server.FileWorker
|
||||
open Lsp
|
||||
open IO
|
||||
open Snapshots
|
||||
open JsonRpc
|
||||
|
||||
section Elab
|
||||
|
||||
-- TODO: use HashSet for allowed tactics?
|
||||
/-- Find all tactics in syntax object that are forbidden according to a
|
||||
set `allowed` of allowed tactics. -/
|
||||
partial def findForbiddenTactics (inputCtx : Parser.InputContext)
|
||||
(levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
|
||||
Elab.Command.CommandElabM Unit := do
|
||||
match stx with
|
||||
| .missing => return ()
|
||||
| .node info kind args =>
|
||||
for arg in args do
|
||||
findForbiddenTactics inputCtx levelParams arg
|
||||
| .atom info val =>
|
||||
-- ignore syntax elements that do not start with a letter
|
||||
-- and ignore "with" keyword
|
||||
let allowed := ["with", "fun", "at", "only"]
|
||||
if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
|
||||
let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
|
||||
match levelParams.tactics.find? (fun t => t.name.toString == val) with
|
||||
| none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
|
||||
| some tac =>
|
||||
if tac.locked then
|
||||
addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
|
||||
else if tac.disabled then
|
||||
addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
|
||||
| .ident info rawVal val preresolved =>
|
||||
let ns ←
|
||||
try resolveGlobalConst (mkIdent val)
|
||||
catch | _ => pure [] -- catch "unknown constant" error
|
||||
for n in ns do
|
||||
let some (.thmInfo ..) := (← getEnv).find? n
|
||||
| return () -- not a theroem -> ignore
|
||||
let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
|
||||
match lemmasAndDefs.find? (fun l => l.name == n) with
|
||||
| none => addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
|
||||
| some lem =>
|
||||
if lem.locked then
|
||||
addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
|
||||
else if lem.disabled then
|
||||
addErrorMessage info s!"The lemma/definition '{n}' is disabled in this level!"
|
||||
where addErrorMessage (info : SourceInfo) (s : MessageData) :=
|
||||
modify fun st => { st with
|
||||
messages := st.messages.add {
|
||||
fileName := inputCtx.fileName
|
||||
severity := MessageSeverity.error
|
||||
pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
|
||||
data := s
|
||||
}
|
||||
}
|
||||
|
||||
open Elab Meta Expr in
|
||||
def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
|
||||
(couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams): IO Snapshot := do
|
||||
-- Recognize end snap
|
||||
if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
|
||||
let endSnap : Snapshot := {
|
||||
beginPos := snap.mpState.pos
|
||||
stx := MyModule.mkEOI snap.mpState.pos
|
||||
mpState := snap.mpState
|
||||
cmdState := snap.cmdState
|
||||
interactiveDiags := ← withNewInteractiveDiags snap.msgLog
|
||||
tacticCache := snap.tacticCache
|
||||
}
|
||||
return endSnap
|
||||
|
||||
let parseResultRef ← IO.mkRef (Syntax.missing, snap.mpState)
|
||||
|
||||
let cmdStateRef ← IO.mkRef snap.cmdState
|
||||
/- The same snapshot may be executed by different tasks. So, to make sure `elabCommandTopLevel` has exclusive
|
||||
access to the cache, we create a fresh reference here. Before this change, the
|
||||
following `snap.tacticCache.modify` would reset the tactic post cache while another snapshot was still using it. -/
|
||||
let tacticCacheNew ← IO.mkRef (← snap.tacticCache.get)
|
||||
let cmdCtx : Elab.Command.Context := {
|
||||
cmdPos := snap.endPos
|
||||
fileName := inputCtx.fileName
|
||||
fileMap := inputCtx.fileMap
|
||||
tacticCache? := some tacticCacheNew
|
||||
}
|
||||
let (output, _) ← IO.FS.withIsolatedStreams (isolateStderr := server.stderrAsMessages.get snap.cmdState.scopes.head!.opts) <| liftM (m := BaseIO) do
|
||||
Elab.Command.catchExceptions
|
||||
(getResetInfoTrees *> do
|
||||
let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
|
||||
| throwError "Level not found: {inputCtx.fileName}"
|
||||
let scope := level.scope
|
||||
|
||||
-- use open namespaces and options as in the level file
|
||||
Elab.Command.withScope (fun _ => scope) do
|
||||
for od in scope.openDecls do
|
||||
let .simple ns _ := od
|
||||
| pure ()
|
||||
activateScoped ns
|
||||
activateScoped scope.currNamespace
|
||||
|
||||
-- parse tactics
|
||||
let pmctx := {
|
||||
env := ← getEnv,
|
||||
options := scope.opts,
|
||||
currNamespace := scope.currNamespace,
|
||||
openDecls := scope.openDecls }
|
||||
let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
|
||||
MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
|
||||
modify (fun s => { s with messages := msgLog })
|
||||
parseResultRef.set (tacticStx, cmdParserState)
|
||||
|
||||
-- Check for forbidden tactics
|
||||
findForbiddenTactics inputCtx levelParams tacticStx
|
||||
|
||||
-- Insert invisible `skip` command to make sure we always display the initial goal
|
||||
let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
|
||||
-- Insert final `done` command to display unsolved goal error in the end
|
||||
let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
|
||||
let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
|
||||
let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
|
||||
|
||||
let cmdStx ← `(command|
|
||||
theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
|
||||
Elab.Command.elabCommandTopLevel cmdStx)
|
||||
cmdCtx cmdStateRef
|
||||
let postNew := (← tacticCacheNew.get).post
|
||||
snap.tacticCache.modify fun _ => { pre := postNew, post := {} }
|
||||
let mut postCmdState ← cmdStateRef.get
|
||||
if !output.isEmpty then
|
||||
postCmdState := {
|
||||
postCmdState with
|
||||
messages := postCmdState.messages.add {
|
||||
fileName := inputCtx.fileName
|
||||
severity := MessageSeverity.information
|
||||
pos := inputCtx.fileMap.toPosition snap.endPos
|
||||
data := output
|
||||
}
|
||||
}
|
||||
|
||||
let (tacticStx, cmdParserState) ← parseResultRef.get
|
||||
|
||||
let postCmdSnap : Snapshot := {
|
||||
beginPos := tacticStx.getPos?.getD 0
|
||||
stx := tacticStx
|
||||
mpState := cmdParserState
|
||||
cmdState := postCmdState
|
||||
interactiveDiags := ← withNewInteractiveDiags postCmdState.messages
|
||||
tacticCache := (← IO.mkRef {})
|
||||
}
|
||||
return postCmdSnap
|
||||
|
||||
where
|
||||
/-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent
|
||||
snapshot. We need to do this because unlike the `MessageLog` itself, interactive diags are not
|
||||
part of the command state. -/
|
||||
withNewInteractiveDiags (msgLog : MessageLog) : IO (PersistentArray Widget.InteractiveDiagnostic) := do
|
||||
let newMsgCount := msgLog.msgs.size - snap.msgLog.msgs.size
|
||||
let mut ret := snap.interactiveDiags
|
||||
for i in List.iota newMsgCount do
|
||||
let newMsg := msgLog.msgs.get! (msgLog.msgs.size - i)
|
||||
ret := ret.push (← Widget.msgToInteractiveDiagnostic inputCtx.fileMap newMsg hasWidgets)
|
||||
return ret
|
||||
|
||||
private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
|
||||
(snaps : Array Snapshot) : IO Unit := do
|
||||
let trees := snaps.map fun snap => snap.infoTree
|
||||
let references := findModuleRefs m.text trees (localVars := true)
|
||||
let param := { version := m.version, references : LeanIleanInfoParams }
|
||||
hOut.writeLspNotification { method, param }
|
||||
|
||||
private def publishIleanInfoUpdate : DocumentMeta → FS.Stream → Array Snapshot → IO Unit :=
|
||||
publishIleanInfo "$/lean/ileanInfoUpdate"
|
||||
|
||||
private def publishIleanInfoFinal : DocumentMeta → FS.Stream → Array Snapshot → IO Unit :=
|
||||
publishIleanInfo "$/lean/ileanInfoFinal"
|
||||
|
||||
structure GameCompletedParams where
|
||||
uri : String
|
||||
deriving ToJson, FromJson
|
||||
|
||||
/-- Checks whether game level has been completed and sends a notification to the client -/
|
||||
def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
|
||||
-- check if there is any error or warning
|
||||
for snap in snaps do
|
||||
if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
|
||||
then return
|
||||
let param := { uri := m.uri : GameCompletedParams}
|
||||
hOut.writeLspNotification { method := "$/game/completed", param }
|
||||
|
||||
/-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
|
||||
private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
|
||||
(levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
|
||||
: AsyncElabM (Option Snapshot) := do
|
||||
cancelTk.check
|
||||
let s ← get
|
||||
let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
|
||||
if lastSnap.isAtEnd then
|
||||
publishGameCompleted m ctx.hOut s.snaps
|
||||
publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
|
||||
publishProgressDone m ctx.hOut
|
||||
-- This will overwrite existing ilean info for the file, in case something
|
||||
-- went wrong during the incremental updates.
|
||||
publishIleanInfoFinal m ctx.hOut s.snaps
|
||||
return none
|
||||
publishProgressAtPos m lastSnap.endPos ctx.hOut
|
||||
-- Make sure that there is at least one snap after the head snap, so that
|
||||
-- we can see the current goal even on an empty document
|
||||
let couldBeEndSnap := s.snaps.size > 1
|
||||
let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
|
||||
levelParams initParams
|
||||
set { s with snaps := s.snaps.push snap }
|
||||
-- TODO(MH): check for interrupt with increased precision
|
||||
cancelTk.check
|
||||
/- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
|
||||
while prefering newer versions over old ones. The former is necessary because we do
|
||||
not explicitly clear older diagnostics, while the latter is necessary because we do
|
||||
not guarantee that diagnostics are emitted in order. Specifically, it may happen that
|
||||
we interrupted this elaboration task right at this point and a newer elaboration task
|
||||
emits diagnostics, after which we emit old diagnostics because we did not yet detect
|
||||
the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
|
||||
because we cannot guarantee that no further diagnostics are emitted after clearing
|
||||
them. -/
|
||||
-- NOTE(WN): this is *not* redundent even if there are no new diagnostics in this snapshot
|
||||
-- because empty diagnostics clear existing error/information squiggles. Therefore we always
|
||||
-- want to publish in case there was previously a message at this position.
|
||||
publishDiagnostics m snap.diagnostics.toArray ctx.hOut
|
||||
publishIleanInfoUpdate m ctx.hOut #[snap]
|
||||
return some snap
|
||||
|
||||
/-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
|
||||
def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
|
||||
(startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
|
||||
: ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
|
||||
let ctx ← read
|
||||
let some headerSnap := snaps[0]? | panic! "empty snapshots"
|
||||
if headerSnap.msgLog.hasErrors then
|
||||
-- Treat header processing errors as fatal so users aren't swamped with
|
||||
-- followup errors
|
||||
publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
|
||||
publishIleanInfoFinal m ctx.hOut #[headerSnap]
|
||||
return AsyncList.ofList [headerSnap]
|
||||
else
|
||||
-- This will overwrite existing ilean info for the file since this has a
|
||||
-- higher version number.
|
||||
publishIleanInfoUpdate m ctx.hOut snaps
|
||||
return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
|
||||
IO.sleep startAfterMs
|
||||
AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps })
|
||||
|
||||
end Elab
|
||||
|
||||
section Updates
|
||||
|
||||
/-- Given the new document, updates editable doc state. -/
|
||||
def updateDocument (newMeta : DocumentMeta) (levelParams : Game.DidOpenLevelParams) : WorkerM Unit := do
|
||||
let ctx ← read
|
||||
let oldDoc := (←get).doc
|
||||
oldDoc.cancelTk.set
|
||||
let initHeaderStx := (← get).initHeaderStx
|
||||
let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
|
||||
let cancelTk ← CancelToken.new
|
||||
let headSnapTask := oldDoc.cmdSnaps.waitHead?
|
||||
let newSnaps ← if initHeaderStx != newHeaderStx then
|
||||
EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
|
||||
IO.sleep ctx.initParams.editDelay.toUInt32
|
||||
cancelTk.check
|
||||
IO.Process.exit 2
|
||||
else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
|
||||
-- There is always at least one snapshot absent exceptions
|
||||
let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
|
||||
let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
|
||||
let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
|
||||
-- Ignore exceptions, we are only interested in the successful snapshots
|
||||
let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
|
||||
-- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
|
||||
-- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
|
||||
let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
|
||||
if h : validSnaps.length ≤ 1 then
|
||||
validSnaps := [newHeaderSnap]
|
||||
else
|
||||
/- When at least one valid non-header snap exists, it may happen that a change does not fall
|
||||
within the syntactic range of that last snap but still modifies it by appending tokens.
|
||||
We check for this here. We do not currently handle crazy grammars in which an appended
|
||||
token can merge two or more previous commands into one. To do so would require reparsing
|
||||
the entire file. -/
|
||||
have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
|
||||
let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
|
||||
let preLastSnap :=
|
||||
have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
|
||||
have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
|
||||
validSnaps[validSnaps.length - 2]
|
||||
let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
|
||||
if newLastStx != lastSnap.stx then
|
||||
validSnaps := validSnaps.dropLast
|
||||
-- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
|
||||
-- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
|
||||
unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
|
||||
(startAfterMs := ctx.initParams.editDelay.toUInt32)
|
||||
modify fun st => { st with doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk } }
|
||||
|
||||
end Updates
|
||||
|
||||
section Initialization
|
||||
|
||||
def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
|
||||
input := "" -- No header!
|
||||
fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
|
||||
fileMap := default
|
||||
|
||||
def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
|
||||
(levelModule : Name) (initParams : InitializeParams): IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
|
||||
let some gameDir := GameServer.gameDirFromInitParams initParams
|
||||
| throwServerError s!"Invalid rootUri: {initParams.rootUri?}"
|
||||
|
||||
-- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
|
||||
let out ← IO.Process.output
|
||||
{ cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
|
||||
if out.exitCode != 0 then
|
||||
throwServerError s!"Error while running Lake: {out.stderr}"
|
||||
|
||||
-- Make the paths relative to the current directory
|
||||
let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
|
||||
let currentDir ← IO.currentDir
|
||||
let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
|
||||
|
||||
-- Set the search path
|
||||
Lean.searchPathRef.set paths
|
||||
|
||||
let env ← importModules [{ module := `Init : Import }, { module := levelModule : Import }] {} 0
|
||||
-- return (env, paths)
|
||||
|
||||
-- use empty header
|
||||
let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
|
||||
{m.mkInputContext with
|
||||
input := ""
|
||||
fileMap := FileMap.ofString ""}
|
||||
(headerStx, ·) <$> EIO.asTask do
|
||||
let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
|
||||
let headerEnv := env
|
||||
let mut headerEnv := headerEnv
|
||||
try
|
||||
if let some path := System.Uri.fileUriToPath? m.uri then
|
||||
headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
|
||||
catch _ => pure ()
|
||||
let cmdState := Elab.Command.mkState headerEnv {} opts
|
||||
let cmdState := { cmdState with infoState := {
|
||||
enabled := true
|
||||
trees := #[Elab.InfoTree.context ({
|
||||
env := headerEnv
|
||||
fileMap := m.text
|
||||
ngen := { namePrefix := `_worker }
|
||||
}) (Elab.InfoTree.node
|
||||
(Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
|
||||
(headerStx[1].getArgs.toList.map (fun importStx =>
|
||||
Elab.InfoTree.node (Elab.Info.ofCommandInfo {
|
||||
elaborator := `import
|
||||
stx := importStx
|
||||
}) #[].toPArray'
|
||||
)).toPArray'
|
||||
)].toPArray'
|
||||
}}
|
||||
let headerSnap := {
|
||||
beginPos := 0
|
||||
stx := headerStx
|
||||
mpState := {}
|
||||
cmdState := cmdState
|
||||
interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
|
||||
tacticCache := (← IO.mkRef {})
|
||||
}
|
||||
publishDiagnostics m headerSnap.diagnostics.toArray hOut
|
||||
return (headerSnap, srcSearchPath)
|
||||
|
||||
def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
|
||||
(levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
|
||||
let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
|
||||
let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
|
||||
levelParams.levelModule initParams
|
||||
let cancelTk ← CancelToken.new
|
||||
let ctx :=
|
||||
{ hIn := i
|
||||
hOut := o
|
||||
hLog := e
|
||||
headerTask
|
||||
initParams
|
||||
clientHasWidgets
|
||||
}
|
||||
let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
|
||||
| Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
|
||||
| Except.error e => throw (e : ElabTaskError))
|
||||
let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
|
||||
return (ctx,
|
||||
{ doc := doc
|
||||
initHeaderStx := headerStx
|
||||
pendingRequests := RBMap.empty
|
||||
rpcSessions := RBMap.empty
|
||||
})
|
||||
|
||||
end Initialization
|
||||
|
||||
section NotificationHandling
|
||||
|
||||
def handleDidChange (levelParams : Game.DidOpenLevelParams) (p : DidChangeTextDocumentParams) : WorkerM Unit := do
|
||||
let docId := p.textDocument
|
||||
let changes := p.contentChanges
|
||||
let oldDoc := (←get).doc
|
||||
let some newVersion ← pure docId.version?
|
||||
| throwServerError "Expected version number"
|
||||
if newVersion ≤ oldDoc.meta.version then
|
||||
-- TODO(WN): This happens on restart sometimes.
|
||||
IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
|
||||
else if ¬ changes.isEmpty then
|
||||
let newDocText := foldDocumentChanges changes oldDoc.meta.text
|
||||
updateDocument ⟨docId.uri, newVersion, newDocText⟩ levelParams
|
||||
|
||||
end NotificationHandling
|
||||
|
||||
section MessageHandling
|
||||
|
||||
def handleNotification (method : String) (params : Json) (levelParams : Game.DidOpenLevelParams) : WorkerM Unit := do
|
||||
let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
|
||||
parseParams paramType params >>= handler
|
||||
match method with
|
||||
| "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange levelParams)
|
||||
| "$/cancelRequest" => handle CancelParams handleCancelRequest
|
||||
| "$/lean/rpc/release" => handle RpcReleaseParams handleRpcRelease
|
||||
| "$/lean/rpc/keepAlive" => handle RpcKeepAliveParams handleRpcKeepAlive
|
||||
| _ => throwServerError s!"Got unsupported notification method: {method}"
|
||||
|
||||
end MessageHandling
|
||||
|
||||
section MainLoop
|
||||
partial def mainLoop (levelParams : Game.DidOpenLevelParams) : WorkerM Unit := do
|
||||
let ctx ← read
|
||||
let mut st ← get
|
||||
let msg ← ctx.hIn.readLspMessage
|
||||
let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
|
||||
: IO PendingRequestMap := do
|
||||
if (← hasFinished task) then
|
||||
/- Handler tasks are constructed so that the only possible errors here
|
||||
are failures of writing a response into the stream. -/
|
||||
if let Except.error e := task.get then
|
||||
throwServerError s!"Failed responding to request {id}: {e}"
|
||||
pure <| acc.erase id
|
||||
else pure acc
|
||||
let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
|
||||
st := { st with pendingRequests }
|
||||
|
||||
-- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
|
||||
for (id, seshRef) in st.rpcSessions do
|
||||
let sesh ← seshRef.get
|
||||
if (← sesh.hasExpired) then
|
||||
st := { st with rpcSessions := st.rpcSessions.erase id }
|
||||
|
||||
set st
|
||||
match msg with
|
||||
| Message.request id method (some params) =>
|
||||
if method == "Game.getInteractiveGoals" then throwServerError "HELLO"
|
||||
handleRequest id method (toJson params)
|
||||
mainLoop levelParams
|
||||
| Message.notification "exit" none =>
|
||||
let doc := st.doc
|
||||
doc.cancelTk.set
|
||||
return ()
|
||||
| Message.notification method (some params) =>
|
||||
handleNotification method (toJson params) levelParams
|
||||
mainLoop levelParams
|
||||
| _ => throwServerError "Got invalid JSON-RPC message"
|
||||
end MainLoop
|
||||
|
||||
def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
|
||||
let i ← maybeTee "fwIn.txt" false i
|
||||
let o ← maybeTee "fwOut.txt" true o
|
||||
let initParams ← i.readLspRequestAs "initialize" InitializeParams
|
||||
let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
|
||||
let ⟨_, levelParams⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams
|
||||
|
||||
let doc := param.textDocument
|
||||
/- NOTE(WN): `toFileMap` marks line beginnings as immediately following
|
||||
"\n", which should be enough to handle both LF and CRLF correctly.
|
||||
This is because LSP always refers to characters by (line, column),
|
||||
so if we get the line number correct it shouldn't matter that there
|
||||
is a CR there. -/
|
||||
let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
|
||||
let e := e.withPrefix s!"[{param.textDocument.uri}] "
|
||||
let _ ← IO.setStderr e
|
||||
try
|
||||
let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
|
||||
let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) (mainLoop levelParams)
|
||||
return (0 : UInt32)
|
||||
catch e =>
|
||||
IO.eprintln e
|
||||
publishDiagnostics meta #[{ range := ⟨⟨0, 0⟩, ⟨0, 0⟩⟩, severity? := DiagnosticSeverity.error, message := e.toString }] o
|
||||
return (1 : UInt32)
|
||||
|
||||
def workerMain (opts : Options) : IO UInt32 := do
|
||||
let i ← IO.getStdin
|
||||
let o ← IO.getStdout
|
||||
let e ← IO.getStderr
|
||||
try
|
||||
let exitCode ← initAndRunWorker i o e opts
|
||||
-- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
|
||||
-- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
|
||||
o.flush
|
||||
e.flush
|
||||
IO.Process.exit exitCode.toUInt8
|
||||
catch err =>
|
||||
e.putStrLn s!"worker initialization error: {err}"
|
||||
return (1 : UInt32)
|
||||
|
||||
end MyServer.FileWorker
|
||||
@@ -0,0 +1,162 @@
|
||||
import GameServer.RpcHandlers
|
||||
|
||||
open Lean
|
||||
|
||||
structure GameServerState :=
|
||||
(env : Lean.Environment)
|
||||
(game : Name)
|
||||
|
||||
abbrev GameServerM := StateT GameServerState Server.Watchdog.ServerM
|
||||
|
||||
instance : MonadEnv GameServerM := {
|
||||
getEnv := do return (← get).env
|
||||
modifyEnv := fun f => do
|
||||
let s ← get
|
||||
set {s with env := f s.env}
|
||||
}
|
||||
|
||||
namespace Game
|
||||
open Server
|
||||
open Watchdog
|
||||
open Lsp
|
||||
open JsonRpc
|
||||
open IO
|
||||
|
||||
def getGame (game : Name): GameServerM Json := do
|
||||
let some game ← getGame? game
|
||||
| throwServerError "Game not found"
|
||||
let gameJson : Json := toJson game
|
||||
-- Add world sizes to Json object
|
||||
let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size))
|
||||
let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)])
|
||||
return gameJson
|
||||
|
||||
/--
|
||||
Fields:
|
||||
- description: Lemma in mathematical language.
|
||||
- descriptionGoal: Lemma printed as Lean-Code.
|
||||
-/
|
||||
structure LevelInfo where
|
||||
index : Nat
|
||||
title : String
|
||||
tactics : Array ComputedInventoryItem
|
||||
lemmas : Array ComputedInventoryItem
|
||||
definitions : Array ComputedInventoryItem
|
||||
introduction : String
|
||||
conclusion : String
|
||||
descrText : String := ""
|
||||
descrFormat : String := ""
|
||||
lemmaTab : Option String
|
||||
statementName : Option String
|
||||
deriving ToJson, FromJson
|
||||
|
||||
structure LoadLevelParams where
|
||||
world : Name
|
||||
level : Nat
|
||||
deriving ToJson, FromJson
|
||||
|
||||
structure DidOpenLevelParams where
|
||||
uri : String
|
||||
levelModule : Name
|
||||
tactics : Array ComputedInventoryItem
|
||||
lemmas : Array ComputedInventoryItem
|
||||
definitions : Array ComputedInventoryItem
|
||||
deriving ToJson, FromJson
|
||||
|
||||
structure Doc where
|
||||
name: String
|
||||
displayName: String
|
||||
text: String
|
||||
deriving ToJson
|
||||
|
||||
structure LoadDocParams where
|
||||
name : Name
|
||||
type : InventoryType
|
||||
deriving ToJson, FromJson
|
||||
|
||||
def handleDidOpenLevel (params : Json) : GameServerM Unit := do
|
||||
let p ← parseParams _ params
|
||||
let m := p.textDocument
|
||||
-- Execute the regular handling of the `didOpen` event
|
||||
handleDidOpen p
|
||||
let fw ← findFileWorker! m.uri
|
||||
-- let s ← get
|
||||
let c ← read
|
||||
let some lvl ← GameServer.getLevelByFileName? c.initParams ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
|
||||
| do
|
||||
c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}"
|
||||
c.hLog.flush
|
||||
-- Send an extra notification to the file worker to inform it about the level data
|
||||
fw.stdin.writeLspNotification {
|
||||
method := "$/game/didOpenLevel"
|
||||
param := {
|
||||
uri := m.uri
|
||||
levelModule := lvl.module
|
||||
tactics := lvl.tactics.computed
|
||||
lemmas := lvl.lemmas.computed
|
||||
definitions := lvl.definitions.computed
|
||||
: DidOpenLevelParams
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
|
||||
match ev with
|
||||
| ServerEvent.clientMsg msg =>
|
||||
match msg with
|
||||
| Message.request id "info" _ =>
|
||||
let s ← get
|
||||
let c ← read
|
||||
c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩
|
||||
return true
|
||||
| Message.request id "loadLevel" params =>
|
||||
let p ← parseParams LoadLevelParams (toJson params)
|
||||
let s ← get
|
||||
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
|
||||
|
||||
let env ← getEnv
|
||||
|
||||
let levelInfo : LevelInfo :=
|
||||
{ index := lvl.index,
|
||||
title := lvl.title,
|
||||
tactics := lvl.tactics.computed,
|
||||
lemmas := lvl.lemmas.computed,
|
||||
definitions := lvl.definitions.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
|
||||
conclusion := lvl.conclusion
|
||||
lemmaTab := lvl.lemmaTab
|
||||
statementName := match lvl.statementName with
|
||||
| .anonymous => none
|
||||
| name => match (inventoryDocExt.getState env).find?
|
||||
(fun x => x.name == name && x.type == .Lemma) with
|
||||
| some n => n.displayName
|
||||
| none => name.toString
|
||||
-- Note: we could call `.find!` because we check in `Statement` that the
|
||||
-- lemma doc must exist.
|
||||
}
|
||||
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 ← 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
|
||||
displayName := doc.displayName
|
||||
text := doc.content }
|
||||
c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩
|
||||
return true
|
||||
| _ => return false
|
||||
| _ => return false
|
||||
|
||||
end Game
|
||||
@@ -0,0 +1,69 @@
|
||||
import Lean
|
||||
|
||||
open Lean Meta
|
||||
|
||||
/-! ## Graph -/
|
||||
|
||||
variable [inst : BEq α] [inst : Hashable α]
|
||||
|
||||
structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
|
||||
nodes: HashMap α β := {}
|
||||
edges: Array (α × α) := {}
|
||||
deriving Inhabited
|
||||
|
||||
instance [ToJson β] : ToJson (Graph Name β) := {
|
||||
toJson := fun graph => Json.mkObj [
|
||||
("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
|
||||
("edges", toJson graph.edges)
|
||||
]
|
||||
}
|
||||
|
||||
instance : EmptyCollection (Graph α β) := ⟨default⟩
|
||||
|
||||
def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=
|
||||
{g with nodes := g.nodes.insert a b}
|
||||
|
||||
/-- Check if graph contains loops -/
|
||||
partial def Graph.hasLoops (g : Graph α β) (visited0 : HashSet α := {}): Bool := Id.run do
|
||||
let mut visited : HashSet α := visited0
|
||||
let all : Array α := g.nodes.toArray.map (·.1)
|
||||
|
||||
-- find some node that we haven't visited
|
||||
let some x := all.find? fun x => ¬ visited.contains x
|
||||
| return false -- We have visted all nodes and found no loops
|
||||
visited := visited.insert x
|
||||
|
||||
match visitSuccessors x x visited with -- visit all recursive successors of x
|
||||
| some visited' => visited := visited'
|
||||
| none => return true -- none means a loop has been found
|
||||
|
||||
g.hasLoops visited -- continue looking for unvisited nodes
|
||||
|
||||
where
|
||||
visitSuccessors (x : α) (x0 : α) (visited0 : HashSet α) : Option (HashSet α) := Id.run do
|
||||
let mut visited : HashSet α := visited0
|
||||
|
||||
let directSuccessors := (g.edges.filter (·.1 == x)).map (·.2)
|
||||
for y in directSuccessors do
|
||||
if y == x0 then
|
||||
return none -- loop found
|
||||
if visited.contains y then
|
||||
continue -- no loop possible here because the visited nodes do not lead to x0
|
||||
visited := visited.insert y
|
||||
match visitSuccessors y x0 visited with
|
||||
| some visited' => visited := visited'
|
||||
| none => return none
|
||||
|
||||
return some visited
|
||||
|
||||
-- #eval Graph.hasLoops ⟨HashMap.ofList [(2,2), (1,1)], #[(2,1)]⟩
|
||||
|
||||
partial def Graph.predecessors (g : Graph α β) (x : α) (acc : HashSet α := {}) : HashSet α := Id.run do
|
||||
let mut res := acc
|
||||
let directPredecessors := (g.edges.filter (·.2 == x)).map (·.1)
|
||||
for y in directPredecessors do
|
||||
if ¬ res.contains y then
|
||||
res := res.insert y
|
||||
res := g.predecessors y res
|
||||
|
||||
return res
|
||||
@@ -0,0 +1,200 @@
|
||||
/- This file is mostly copied from `Lean/Widget/InteractiveGoal.lean`. -/
|
||||
|
||||
import Lean.Widget.InteractiveGoal
|
||||
|
||||
/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
|
||||
|
||||
namespace GameServer
|
||||
open Lean Lean.Widget Lean.Server
|
||||
|
||||
structure GameHint where
|
||||
text : String
|
||||
hidden : Bool
|
||||
deriving FromJson, ToJson
|
||||
|
||||
/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
|
||||
as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
|
||||
booleans to save space in the json encoding. -/
|
||||
structure InteractiveHypothesisBundle where
|
||||
/-- The user-friendly name for each hypothesis. -/
|
||||
names : Array Name
|
||||
/-- The ids for each variable. Should have the same length as `names`. -/
|
||||
fvarIds : Array FVarId
|
||||
type : CodeWithInfos
|
||||
/-- The value, in the case the hypothesis is a `let`-binder. -/
|
||||
val? : Option CodeWithInfos := none
|
||||
/-- The hypothesis is a typeclass instance. -/
|
||||
isInstance? : Option Bool := none
|
||||
/-- The hypothesis is a type. -/
|
||||
isType? : Option Bool := none
|
||||
/-- The hypothesis's type is of type `Prop` -/
|
||||
isAssumption? : Option Bool := none
|
||||
/-- If true, the hypothesis was not present on the previous tactic state.
|
||||
Only present in tactic-mode goals. -/
|
||||
isInserted? : Option Bool := none
|
||||
/-- If true, the hypothesis will be removed in the next tactic state.
|
||||
Only present in tactic-mode goals. -/
|
||||
isRemoved? : Option Bool := none
|
||||
deriving Inhabited, RpcEncodable
|
||||
|
||||
/-- The shared parts of interactive term-mode and tactic-mode goals. -/
|
||||
structure InteractiveGoalCore where
|
||||
hyps : Array InteractiveHypothesisBundle
|
||||
/-- The target type. -/
|
||||
type : CodeWithInfos
|
||||
/-- Metavariable context that the goal is well-typed in. -/
|
||||
ctx : WithRpcRef Elab.ContextInfo
|
||||
|
||||
/-- An interactive tactic-mode goal. -/
|
||||
structure InteractiveGoal extends InteractiveGoalCore where
|
||||
/-- The name `foo` in `case foo`, if any. -/
|
||||
userName? : Option String
|
||||
/-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ `
|
||||
and it could be extended. -/
|
||||
goalPrefix : String
|
||||
/-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/
|
||||
mvarId : MVarId
|
||||
/-- If true, the goal was not present on the previous tactic state. -/
|
||||
isInserted? : Option Bool := none
|
||||
/-- If true, the goal will be removed on the next tactic state. -/
|
||||
isRemoved? : Option Bool := none
|
||||
hints : Array GameHint := #[]
|
||||
deriving RpcEncodable
|
||||
|
||||
/-- An interactive term-mode goal. -/
|
||||
structure InteractiveTermGoal extends InteractiveGoalCore where
|
||||
/-- Syntactic range of the term. -/
|
||||
range : Lsp.Range
|
||||
/-- Information about the term whose type is the term-mode goal. -/
|
||||
term : WithRpcRef Elab.TermInfo
|
||||
deriving RpcEncodable
|
||||
|
||||
def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
|
||||
(goalPrefix : String) : Format := Id.run do
|
||||
let indent := 2 -- Use option
|
||||
let mut ret := match userName? with
|
||||
| some userName => f!"case {userName}"
|
||||
| none => Format.nil
|
||||
for hyp in g.hyps do
|
||||
ret := addLine ret
|
||||
let names := hyp.names
|
||||
|>.toList
|
||||
|>.filter (not ∘ Name.isAnonymous)
|
||||
|>.map toString
|
||||
|> " ".intercalate
|
||||
match names with
|
||||
| "" =>
|
||||
ret := ret ++ Format.group f!":{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
|
||||
| _ =>
|
||||
match hyp.val? with
|
||||
| some val =>
|
||||
ret := ret ++ Format.group f!"{names} : {hyp.type.stripTags} :={Format.nest indent (Format.line ++ val.stripTags)}"
|
||||
| none =>
|
||||
ret := ret ++ Format.group f!"{names} :{Format.nest indent (Format.line ++ hyp.type.stripTags)}"
|
||||
ret := addLine ret
|
||||
ret ++ f!"{goalPrefix}{Format.nest indent g.type.stripTags}"
|
||||
where
|
||||
addLine (fmt : Format) : Format :=
|
||||
if fmt.isNil then fmt else fmt ++ Format.line
|
||||
|
||||
def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
|
||||
g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
|
||||
|
||||
def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
|
||||
g.toInteractiveGoalCore.pretty none "⊢ "
|
||||
|
||||
structure InteractiveGoals where
|
||||
goals : Array InteractiveGoal
|
||||
deriving RpcEncodable
|
||||
|
||||
def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
|
||||
goals := l.goals ++ r.goals
|
||||
|
||||
instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
|
||||
instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
|
||||
|
||||
open Meta in
|
||||
/-- Extend an array of hypothesis bundles with another bundle. -/
|
||||
def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
|
||||
(ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) :
|
||||
MetaM (Array InteractiveHypothesisBundle) := do
|
||||
if ids.size == 0 then
|
||||
throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
|
||||
let fvarIds := ids.map Prod.snd
|
||||
let names := ids.map Prod.fst
|
||||
return hyps.push {
|
||||
names
|
||||
fvarIds
|
||||
type := (← ppExprTagged type)
|
||||
val? := (← value?.mapM ppExprTagged)
|
||||
isInstance? := if (← isClass? type).isSome then true else none
|
||||
isType? := if (← instantiateMVars type).isSort then true else none
|
||||
isAssumption? := if (← inferType type).isProp then true else none
|
||||
}
|
||||
|
||||
open Meta in
|
||||
variable [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadOptions n] [MonadMCtx n] in
|
||||
def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α) : n α := do
|
||||
let mctx ← getMCtx
|
||||
let some mvarDecl := mctx.findDecl? goal
|
||||
| throwError "unknown goal {goal.name}"
|
||||
let lctx := mvarDecl.lctx |>.sanitizeNames.run' {options := (← getOptions)}
|
||||
withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
|
||||
|
||||
open Meta in
|
||||
/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
|
||||
def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
|
||||
let ppAuxDecls := pp.auxDecls.get (← getOptions)
|
||||
let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
|
||||
let showLetValues := pp.showLetValues.get (← getOptions)
|
||||
withGoalCtx mvarId fun lctx mvarDecl => do
|
||||
let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
|
||||
: MetaM (Array InteractiveHypothesisBundle) :=
|
||||
if ids.isEmpty then
|
||||
pure hyps
|
||||
else
|
||||
match type? with
|
||||
| none => pure hyps
|
||||
| some type => addInteractiveHypothesisBundle hyps ids type
|
||||
let mut varNames : Array (Name × FVarId) := #[]
|
||||
let mut prevType? : Option Expr := none
|
||||
let mut hyps : Array InteractiveHypothesisBundle := #[]
|
||||
for localDecl in lctx do
|
||||
if !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail then
|
||||
continue
|
||||
else
|
||||
match localDecl with
|
||||
| LocalDecl.cdecl _index fvarId varName type _ _ =>
|
||||
let varName := varName.simpMacroScopes
|
||||
let type ← instantiateMVars type
|
||||
if prevType? == none || prevType? == some type then
|
||||
varNames := varNames.push (varName, fvarId)
|
||||
else
|
||||
hyps ← pushPending varNames prevType? hyps
|
||||
varNames := #[(varName, fvarId)]
|
||||
prevType? := some type
|
||||
| LocalDecl.ldecl _index fvarId varName type val _ _ => do
|
||||
let varName := varName.simpMacroScopes
|
||||
hyps ← pushPending varNames prevType? hyps
|
||||
let type ← instantiateMVars type
|
||||
let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
|
||||
hyps ← addInteractiveHypothesisBundle hyps #[(varName, fvarId)] type val?
|
||||
varNames := #[]
|
||||
prevType? := none
|
||||
hyps ← pushPending varNames prevType? hyps
|
||||
let goalTp ← instantiateMVars mvarDecl.type
|
||||
let goalFmt ← ppExprTagged goalTp
|
||||
let userName? := match mvarDecl.userName with
|
||||
| Name.anonymous => none
|
||||
| name => some <| toString name.eraseMacroScopes
|
||||
return {
|
||||
hyps
|
||||
type := goalFmt
|
||||
ctx := ⟨← Elab.ContextInfo.save⟩
|
||||
userName?
|
||||
goalPrefix := getGoalPrefix mvarDecl
|
||||
mvarId
|
||||
hints
|
||||
}
|
||||
|
||||
end GameServer
|
||||
@@ -0,0 +1,188 @@
|
||||
import GameServer.EnvExtensions
|
||||
import GameServer.InteractiveGoal
|
||||
|
||||
open Lean
|
||||
open Server
|
||||
open Widget
|
||||
open RequestM
|
||||
open Meta
|
||||
|
||||
|
||||
/-! ## GameGoal -/
|
||||
|
||||
namespace GameServer
|
||||
|
||||
def splitRootUri (initParams : Lsp.InitializeParams) (i : Nat): Option String := Id.run do
|
||||
let some rootUri := initParams.rootUri?
|
||||
| return none
|
||||
let rootUriParts := rootUri.splitOn "/"
|
||||
if rootUriParts.length == 3 then
|
||||
return rootUriParts[i]?
|
||||
return none
|
||||
|
||||
def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String) : Option LevelId := Id.run do
|
||||
let fileParts := fileName.splitOn "/"
|
||||
if fileParts.length == 3 then
|
||||
if let (some level, some game) := (fileParts[2]!.toNat?, splitRootUri initParams 2) then
|
||||
return some {game, world := fileParts[1]!, level := level}
|
||||
return none
|
||||
|
||||
def gameDirFromInitParams (initParams : Lsp.InitializeParams) : Option String :=
|
||||
(splitRootUri initParams 0).map (s!"../../{·}")
|
||||
|
||||
def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
|
||||
let some levelId := levelIdFromFileName? initParams fileName
|
||||
| return none
|
||||
return ← getLevel? levelId
|
||||
|
||||
structure FVarBijection :=
|
||||
(forward : HashMap FVarId FVarId)
|
||||
(backward : HashMap FVarId FVarId)
|
||||
|
||||
instance : EmptyCollection FVarBijection := ⟨{},{}⟩
|
||||
|
||||
def FVarBijection.insert (bij : FVarBijection) (a b : FVarId) : FVarBijection :=
|
||||
⟨bij.forward.insert a b, bij.backward.insert b a⟩
|
||||
|
||||
def FVarBijection.insert? (bij : FVarBijection) (a b : FVarId) : Option FVarBijection :=
|
||||
let a' := bij.forward.find? a
|
||||
let b' := bij.forward.find? b
|
||||
if (a' == none || a' == some b) && (b' == none || b' == some a)
|
||||
then some $ bij.insert a b
|
||||
else none
|
||||
|
||||
/-- Checks if `pattern` and `e` are equal up to FVar identities. -/
|
||||
partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) : Option FVarBijection :=
|
||||
match pattern, e with
|
||||
| .bvar i1, .bvar i2 => if i1 == i2 then bij else none
|
||||
| .fvar i1, .fvar i2 => bij.insert? i1 i2
|
||||
| .mvar _, .mvar _ => bij
|
||||
| .sort u1, .sort u2 => bij -- TODO?
|
||||
| .const n1 ls1, .const n2 ls2 =>
|
||||
if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
|
||||
| .app f1 a1, .app f2 a2 =>
|
||||
some bij
|
||||
|> (Option.bind · (fun bij => matchExpr f1 f2 bij))
|
||||
|> (Option.bind · (fun bij => matchExpr a1 a2 bij))
|
||||
| .lam _ t1 b1 _, .lam _ t2 b2 _ =>
|
||||
some bij
|
||||
|> (Option.bind · (fun bij => matchExpr t1 t2 bij))
|
||||
|> (Option.bind · (fun bij => matchExpr b1 b2 bij))
|
||||
| .forallE _ t1 b1 _, .forallE _ t2 b2 _ =>
|
||||
some bij
|
||||
|> (Option.bind · (fun bij => matchExpr t1 t2 bij))
|
||||
|> (Option.bind · (fun bij => matchExpr b1 b2 bij))
|
||||
| .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ =>
|
||||
some bij
|
||||
|> (Option.bind · (fun bij => matchExpr t1 t2 bij))
|
||||
|> (Option.bind · (fun bij => matchExpr v1 v2 bij))
|
||||
|> (Option.bind · (fun bij => matchExpr b1 b2 bij))
|
||||
| .lit l1, .lit l2 =>
|
||||
if l1 == l2 then bij else none
|
||||
| .proj i1 n1 e1, .proj i2 n2 e2 =>
|
||||
if i1 == i2 && n1 == n2 then matchExpr e1 e2 bij else none
|
||||
-- ignore mdata:
|
||||
| .mdata _ pattern', _ =>
|
||||
matchExpr pattern' e bij
|
||||
| _, .mdata _ e' =>
|
||||
matchExpr pattern e' bij
|
||||
| _, _ => none
|
||||
|
||||
/-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
|
||||
def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do
|
||||
-- We iterate through the array backwards hoping that this will find us faster results
|
||||
-- TODO: implement backtracking
|
||||
let mut bij := initBij
|
||||
for i in [:patterns.size] do
|
||||
let pattern := patterns[patterns.size - i - 1]!
|
||||
if bij.forward.contains pattern.fvarId! then
|
||||
continue
|
||||
for j in [:fvars.size] do
|
||||
let fvar := fvars[fvars.size - j - 1]!
|
||||
if bij.backward.contains fvar.fvarId! then
|
||||
continue
|
||||
|
||||
if let some bij' := matchExpr
|
||||
(← instantiateMVars $ ← inferType pattern)
|
||||
(← instantiateMVars $ ← inferType fvar) bij then
|
||||
-- usedFvars := usedFvars.set! (fvars.size - j - 1) true
|
||||
bij := bij'.insert pattern.fvarId! fvar.fvarId!
|
||||
break
|
||||
if ! bij.forward.contains pattern.fvarId! then return false
|
||||
|
||||
if strict then
|
||||
return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
|
||||
return true
|
||||
|
||||
unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
|
||||
evalExpr (Array Expr → MessageData)
|
||||
(.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
|
||||
(mkConst ``MessageData) .default)
|
||||
|
||||
@[implemented_by evalHintMessageUnsafe]
|
||||
def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
|
||||
|
||||
open Meta in
|
||||
/-- Find all hints whose trigger matches the current goal -/
|
||||
def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
|
||||
goal.withContext do
|
||||
let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
|
||||
| throwError "Level not found: {doc.meta.mkInputContext.fileName}"
|
||||
let hints ← level.hints.filterMapM fun hint => do
|
||||
openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
|
||||
if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
|
||||
then
|
||||
let lctx := (← goal.getDecl).lctx
|
||||
if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
|
||||
then
|
||||
let text := (← evalHintMessage hint.text) hintFVars
|
||||
let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
|
||||
let text ← (MessageData.withContext ctx text).toString
|
||||
return some { text := text, hidden := hint.hidden }
|
||||
else return none
|
||||
else
|
||||
return none
|
||||
return hints
|
||||
|
||||
open RequestM in
|
||||
def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
|
||||
let doc ← readDoc
|
||||
let rc ← readThe RequestContext
|
||||
let text := doc.meta.text
|
||||
let hoverPos := text.lspPosToUtf8Pos p.position
|
||||
-- TODO: I couldn't find a good condition to find the correct snap. So we are looking
|
||||
-- for the first snap with goals here:
|
||||
withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
|
||||
(notFoundX := return none) fun snap => do
|
||||
if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
|
||||
let goals : List InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
|
||||
let ciAfter := { ci with mctx := ti.mctxAfter }
|
||||
let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
|
||||
-- compute the interactive goals
|
||||
let goals ← ci.runMetaM {} do
|
||||
return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
|
||||
let goals ← ci.runMetaM {} do
|
||||
goals.mapM fun goal => do
|
||||
let hints ← findHints goal doc rc.initParams
|
||||
return ← goalToInteractive goal hints
|
||||
-- compute the goal diff
|
||||
-- let goals ← ciAfter.runMetaM {} (do
|
||||
-- try
|
||||
-- Widget.diffInteractiveGoals useAfter ti goals
|
||||
-- catch _ =>
|
||||
-- -- fail silently, since this is just a bonus feature
|
||||
-- return goals
|
||||
-- )
|
||||
return {goals}
|
||||
return some <| goals.foldl (· ++ ·) ⟨#[]⟩
|
||||
else
|
||||
return none
|
||||
|
||||
builtin_initialize
|
||||
registerBuiltinRpcProcedure
|
||||
`Game.getInteractiveGoals
|
||||
Lsp.PlainGoalParams
|
||||
(Option InteractiveGoals)
|
||||
getInteractiveGoals
|
||||
|
||||
end GameServer
|
||||
@@ -0,0 +1,153 @@
|
||||
/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
|
||||
import Lean.Server.Watchdog
|
||||
import GameServer.Game
|
||||
|
||||
namespace MyServer.Watchdog
|
||||
open Lean
|
||||
open Server
|
||||
open Watchdog
|
||||
open IO
|
||||
open Lsp
|
||||
open JsonRpc
|
||||
open System.Uri
|
||||
|
||||
partial def mainLoop (clientTask : Task ServerEvent) : GameServerM Unit := do
|
||||
let st ← read
|
||||
let workers ← st.fileWorkersRef.get
|
||||
let mut workerTasks := #[]
|
||||
for (_, fw) in workers do
|
||||
if let WorkerState.running := fw.state then
|
||||
workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
|
||||
|
||||
let ev ← IO.waitAny (clientTask :: workerTasks.toList)
|
||||
|
||||
if ← Game.handleServerEvent ev then -- handle Game requests
|
||||
mainLoop (←runClientTask)
|
||||
else
|
||||
match ev with
|
||||
| ServerEvent.clientMsg msg =>
|
||||
match msg with
|
||||
| Message.request id "shutdown" _ =>
|
||||
shutdown
|
||||
st.hOut.writeLspResponse ⟨id, Json.null⟩
|
||||
| Message.request id method (some params) =>
|
||||
handleRequest id method (toJson params)
|
||||
mainLoop (←runClientTask)
|
||||
| Message.response .. =>
|
||||
-- TODO: handle client responses
|
||||
mainLoop (←runClientTask)
|
||||
| Message.responseError _ _ e .. =>
|
||||
throwServerError s!"Unhandled response error: {e}"
|
||||
| Message.notification method (some params) =>
|
||||
if method == "textDocument/didOpen" then
|
||||
-- for lean4game, we need to pass in extra information when a level is opened:
|
||||
Game.handleDidOpenLevel (← parseParams _ (toJson params))
|
||||
else
|
||||
handleNotification method (toJson params)
|
||||
mainLoop (←runClientTask)
|
||||
| _ => throwServerError "Got invalid JSON-RPC message"
|
||||
| ServerEvent.clientError e => throw e
|
||||
| ServerEvent.workerEvent fw ev =>
|
||||
match ev with
|
||||
| WorkerEvent.ioError e =>
|
||||
throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
|
||||
| WorkerEvent.crashed _ =>
|
||||
handleCrash fw.doc.uri #[]
|
||||
mainLoop clientTask
|
||||
| WorkerEvent.terminated =>
|
||||
throwServerError "Internal server error: got termination event for worker that should have been removed"
|
||||
| .importsChanged =>
|
||||
startFileWorker fw.doc
|
||||
mainLoop clientTask
|
||||
|
||||
def initAndRunWatchdogAux : GameServerM Unit := do
|
||||
let st ← read
|
||||
try
|
||||
discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
|
||||
let clientTask ← runClientTask
|
||||
mainLoop clientTask
|
||||
catch err =>
|
||||
shutdown
|
||||
throw err
|
||||
/- NOTE(WN): It looks like instead of sending the `exit` notification,
|
||||
VSCode just closes the stream. In that case, pretend we got an `exit`. -/
|
||||
let Message.notification "exit" none ←
|
||||
try st.hIn.readLspMessage
|
||||
catch _ => pure (Message.notification "exit" none)
|
||||
| throwServerError "Got `shutdown` request, expected an `exit` notification"
|
||||
|
||||
def createEnv (gameDir : String) (module : String) : IO Environment := do
|
||||
-- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
|
||||
let out ← IO.Process.output
|
||||
{ cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
|
||||
if out.exitCode != 0 then
|
||||
throwServerError s!"Error while running Lake: {out.stderr}"
|
||||
|
||||
-- Make the paths relative to the current directory
|
||||
let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
|
||||
let currentDir ← IO.currentDir
|
||||
let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
|
||||
|
||||
-- Set the search path
|
||||
Lean.searchPathRef.set paths
|
||||
|
||||
let env ← importModules [{ module := `Init : Import }, { module := module : Import }] {} 0
|
||||
return env
|
||||
|
||||
def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
|
||||
if args.length < 4 then
|
||||
throwServerError s!"Expected 3 command line arguments in addition to `--server`:
|
||||
game directory, the name of the main module, and the name of the game"
|
||||
let gameId := args[1]!
|
||||
let gameDir := s!"../../{gameId}"
|
||||
let module := args[2]!
|
||||
let gameName := args[3]!
|
||||
let workerPath := "./gameserver"
|
||||
-- TODO: Do the following commands slow us down?
|
||||
let srcSearchPath ← initSrcSearchPath (← getBuildDir)
|
||||
let references ← IO.mkRef (← loadReferences)
|
||||
let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
|
||||
let i ← maybeTee "wdIn.txt" false i
|
||||
let o ← maybeTee "wdOut.txt" true o
|
||||
let e ← maybeTee "wdErr.txt" true e
|
||||
let state := {env := ← createEnv gameDir module, game := gameName}
|
||||
let initRequest ← i.readLspRequestAs "initialize" InitializeParams
|
||||
-- We misuse the `rootUri` field to store gameId, module, and gameName
|
||||
let rootUri? := s!"{gameId}/{module}/{gameName}"
|
||||
let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
|
||||
o.writeLspResponse {
|
||||
id := initRequest.id
|
||||
result := {
|
||||
capabilities := mkLeanServerCapabilities
|
||||
serverInfo? := some {
|
||||
name := "Lean 4 Game Server"
|
||||
version? := "0.1.1"
|
||||
}
|
||||
: InitializeResult
|
||||
}
|
||||
}
|
||||
let context : ServerContext := {
|
||||
hIn := i
|
||||
hOut := o
|
||||
hLog := e
|
||||
args := args
|
||||
fileWorkersRef := fileWorkersRef
|
||||
initParams := initRequest.param
|
||||
workerPath
|
||||
srcSearchPath
|
||||
references
|
||||
}
|
||||
discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
|
||||
|
||||
def watchdogMain (args : List String) : IO UInt32 := do
|
||||
let i ← IO.getStdin
|
||||
let o ← IO.getStdout
|
||||
let e ← IO.getStderr
|
||||
try
|
||||
initAndRunWatchdog args i o e
|
||||
return 0
|
||||
catch err =>
|
||||
e.putStrLn s!"Watchdog error: {err}"
|
||||
return 1
|
||||
|
||||
end MyServer.Watchdog
|
||||
Reference in New Issue
Block a user