reorganise gameserver and add docstrings
This commit is contained in:
Jon Eugster
@@ -1,32 +1,28 @@
|
||||
import Lean
|
||||
|
||||
import GameServer.EnvExtensions
|
||||
|
||||
open Lean Meta
|
||||
open Lean Meta Elab Command
|
||||
|
||||
set_option autoImplicit false
|
||||
|
||||
/-! ## Easy metadata -/
|
||||
/-! # Game metadata -/
|
||||
|
||||
section metadata
|
||||
|
||||
open Lean Meta Elab Command Term
|
||||
|
||||
/-- Create a game with the given identifier as name. -/
|
||||
/-- 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 World -/
|
||||
/-- 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. -/
|
||||
/-- 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
|
||||
@@ -46,99 +42,6 @@ elab "Introduction" t:str : command => do
|
||||
| .World => modifyCurWorld fun world => pure {world with introduction := t.getString}
|
||||
| .Game => modifyCurGame fun game => pure {game with introduction := t.getString}
|
||||
|
||||
-- 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 _ kind args =>
|
||||
match args.toList.filterMap reprintCore with
|
||||
| [] => none
|
||||
| [arg] => arg
|
||||
| args => Format.group <| Format.nest 2 <| Format.joinSep args " "
|
||||
|
||||
def reprint (stx : Syntax) : Format :=
|
||||
reprintCore stx |>.getD ""
|
||||
|
||||
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 =>
|
||||
logInfo k
|
||||
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] $ ← 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 defined below:
|
||||
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
|
||||
let msgs ← Core.getMessageLog
|
||||
b.restore
|
||||
Core.setMessageLog msgs
|
||||
|
||||
/-- Define the conclusion of the current game or current level if some
|
||||
building a level. -/
|
||||
elab "Conclusion" t:str : command => do
|
||||
@@ -147,20 +50,14 @@ elab "Conclusion" t:str : command => do
|
||||
| .World => modifyCurWorld fun world => pure {world with conclusion := t.getString}
|
||||
| .Game => modifyCurGame fun game => pure {game with conclusion := t.getString}
|
||||
|
||||
-- /-- 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
|
||||
/-! ## 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
|
||||
@@ -172,71 +69,21 @@ elab "Path" s:Parser.path : command => do
|
||||
pure {game with worlds := {game.worlds with edges := game.worlds.edges.push (l, stx.getId)}}
|
||||
last := some stx.getId
|
||||
|
||||
end metadata
|
||||
|
||||
/-! ## Hints -/
|
||||
|
||||
open Lean Meta Elab Command Term
|
||||
/-! # Inventory
|
||||
|
||||
/-- From a term `s` and a list of pairs `(i, t) ; Ident × Term`, create the syntax
|
||||
where `s` is preceded with universal quantifiers `∀ i : t`. -/
|
||||
def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
|
||||
| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
|
||||
| [] => return s
|
||||
|
||||
-- def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
|
||||
-- (goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
|
||||
-- liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
|
||||
-- let (g, decls) ← elabBinders binders fun xs => do
|
||||
-- let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
|
||||
-- synthesizeSyntheticMVarsNoPostponing false
|
||||
-- return (← instantiateMVars g, ← xs.mapM (fun x => x.fvarId!.getDecl))
|
||||
-- let varsName := `vars
|
||||
-- let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
|
||||
-- let mut msg ← `(m! $msg)
|
||||
-- for i in [:decls.size] do
|
||||
-- msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
|
||||
-- return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
|
||||
|
||||
-- if g.hasMVar then throwError m!"Goal contains metavariables: {g}"
|
||||
|
||||
-- modifyCurLevel fun level => pure {level with hints := level.hints.push {
|
||||
-- goal := g,
|
||||
-- intros := decls.size,
|
||||
-- hidden := hidden,
|
||||
-- text := msg }}
|
||||
|
||||
/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/
|
||||
local elab "Hint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command =>
|
||||
-- elabHint false binders goal msg
|
||||
pure ()
|
||||
|
||||
/--
|
||||
Declare a hint. This version doesn't prevent the unused linter variable from running.
|
||||
A hidden hint is only displayed if explicitly requested by the user.
|
||||
The inventory contains docs for tactics, lemmas, and definitions. These are all disabled
|
||||
in the first level and get enabled during the game.
|
||||
-/
|
||||
local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
|
||||
-- elabHint true binders goal msg
|
||||
pure ()
|
||||
|
||||
/-- Declare a hint in reaction to a given tactic state in the current level. -/
|
||||
macro "Hint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
|
||||
`(set_option linter.unusedVariables false in Hint' $decls* : $goal => $msg)
|
||||
|
||||
/-- Declare a hidden hint in reaction to a given tactic state in the current level. -/
|
||||
macro "HiddenHint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
|
||||
`(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg)
|
||||
|
||||
|
||||
/-! ## Inventory -/
|
||||
/-! ## 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}"
|
||||
|
||||
/-! ### Tactics -/
|
||||
| throwError "Missing {type} Documentation: {name} (add `{type}Doc {name}` in your game's docs section)"
|
||||
|
||||
/-- Documentation entry of a tactic. Example:
|
||||
|
||||
@@ -255,26 +102,25 @@ elab "TacticDoc" name:ident content:str : command =>
|
||||
displayName := name.getId.toString,
|
||||
content := content.getString })
|
||||
|
||||
/-- 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}}
|
||||
/-- Documentation entry of a lemma. Example:
|
||||
|
||||
/-- 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}}
|
||||
```
|
||||
LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
|
||||
```
|
||||
|
||||
/-- 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}}
|
||||
|
||||
/-! ### Definitions -/
|
||||
* 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:
|
||||
|
||||
@@ -295,18 +141,58 @@ elab "DefinitionDoc" name:ident "as" displayName:str content:str : command =>
|
||||
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
|
||||
@@ -314,16 +200,32 @@ elab "OnlyDefinition" args:ident* : command => do
|
||||
for name in names do checkInventoryDoc .Definition name
|
||||
modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
|
||||
|
||||
|
||||
/-! ### Lemmas -/
|
||||
/-- 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}
|
||||
|
||||
|
||||
/-- Define the statement of the current level.
|
||||
|
||||
Arguments:
|
||||
- ident: (Optional) The name of the statemtent.
|
||||
- descr: (Optional) The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
|
||||
-/
|
||||
/-! # 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
|
||||
|
||||
-- Check that the statement name is a lemma in the doc
|
||||
@@ -389,71 +291,118 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
|
||||
} -- Format.pretty <| format thmStatement.raw }
|
||||
|
||||
|
||||
/-- Documentation entry of a lemma. Example:
|
||||
|
||||
```
|
||||
LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
|
||||
```
|
||||
/-! # Hints -/
|
||||
|
||||
* 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 })
|
||||
syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
|
||||
|
||||
/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
|
||||
/-- 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⟩ ""
|
||||
|
||||
If omitted, the first tab will be open by default. -/
|
||||
elab "LemmaTab" category:str : command =>
|
||||
modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
|
||||
/-- 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
|
||||
|
||||
/-- 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}}
|
||||
-- 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
|
||||
|
||||
/-- 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}}
|
||||
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
|
||||
|
||||
/-- 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}}
|
||||
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)
|
||||
|
||||
/-! ## Make Game -/
|
||||
/-- 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
|
||||
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}}
|
||||
|
||||
/-- Make the final Game. This command will precompute various things about the game, such as which
|
||||
/-- 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 has loops!"
|
||||
throwError "World graph must not contain loops! Check your `Path` declarations."
|
||||
|
||||
-- Compute which inventory items are available in which level:
|
||||
for inventoryType in open InventoryType in #[Tactic, Definition, Lemma] do
|
||||
@@ -523,3 +472,19 @@ elab "MakeGame" : command => do
|
||||
|
||||
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
|
||||
|
||||
@@ -8,7 +8,6 @@ The game framework stores almost all its game building data in environment exten
|
||||
defined in this file.
|
||||
-/
|
||||
|
||||
|
||||
open Lean
|
||||
|
||||
/-! ## Hints -/
|
||||
@@ -20,9 +19,9 @@ 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 -/
|
||||
/-- 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 -/
|
||||
/-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
|
||||
strict : Bool := false
|
||||
|
||||
instance : Repr GoalHintEntry := {
|
||||
@@ -40,14 +39,45 @@ instance : ToString InventoryType := ⟨fun t => match t with
|
||||
| .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 {
|
||||
@@ -120,15 +150,6 @@ structure LevelId where
|
||||
level : Nat
|
||||
deriving Inhabited
|
||||
|
||||
structure ComputedInventoryItem where
|
||||
name : Name
|
||||
displayName : String
|
||||
category : String
|
||||
locked : Bool
|
||||
-- items that are temporarily blocked in this level.
|
||||
disabled : Bool := false
|
||||
deriving ToJson, FromJson, Repr, Inhabited
|
||||
|
||||
structure InventoryInfo where
|
||||
-- new inventory items introduced by this level:
|
||||
new : Array Name
|
||||
@@ -148,35 +169,41 @@ instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
|
||||
|
||||
structure GameLevel where
|
||||
index: Nat
|
||||
/-- The title of the level. -/
|
||||
title: String := default
|
||||
/-- introduction: Theory block shown all the time -/
|
||||
/-- Introduction text shown all the time. (markdown) -/
|
||||
introduction: String := default
|
||||
/-- The mathematical statemtent in mathematician-readable form -/
|
||||
description: String := default
|
||||
/-- conclusion displayed when level is completed. -/
|
||||
conclusion: String := default
|
||||
tactics: InventoryInfo := default
|
||||
definitions: InventoryInfo := default
|
||||
lemmas: InventoryInfo := default
|
||||
lemmaTab: Option String := none
|
||||
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 module to be imported when playing this level:
|
||||
/-- 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
|
||||
title: String := ""
|
||||
introduction: String := ""
|
||||
conclusion : String := ""
|
||||
levels: HashMap Nat GameLevel := {}
|
||||
/-- 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 := ⟨
|
||||
@@ -189,12 +216,17 @@ instance : ToJson World := ⟨
|
||||
/-! ## Game -/
|
||||
|
||||
structure Game where
|
||||
/-- Internal name of the game. -/
|
||||
name : Name
|
||||
title : String := ""
|
||||
introduction : String := ""
|
||||
conclusion : String := ""
|
||||
authors : List String := []
|
||||
worlds : Graph Name World := {}
|
||||
/-- 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 -/
|
||||
|
||||
Reference in New Issue
Block a user