cleanup code surrounding hints
This commit is contained in:
Jon Eugster
@@ -2,6 +2,7 @@ import GameServer.Helpers
|
||||
import GameServer.Inventory
|
||||
import GameServer.Options
|
||||
import GameServer.SaveData
|
||||
import GameServer.Hints
|
||||
|
||||
open Lean Meta Elab Command
|
||||
|
||||
@@ -396,9 +397,32 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
|
||||
.nest hidden $
|
||||
.compose (.ofGoal text) (.ofGoal goal) := msg.data then
|
||||
let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
|
||||
|
||||
let goalDecl ← goal.getDecl
|
||||
let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (·.fvarId)
|
||||
|
||||
-- NOTE: This code about `hintFVarsNames` is duplicated from `RpcHandlers`
|
||||
-- where the variable bijection is constructed, and they
|
||||
-- need to be matching.
|
||||
-- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
|
||||
-- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
|
||||
-- and we wrap them in `«{}»` here since I don't know how to do it later.
|
||||
let mut hintFVarsNames : Array Expr := #[]
|
||||
for fvar in fvars do
|
||||
let name₁ ← fvar.getUserName
|
||||
hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
|
||||
|
||||
let text ← instantiateMVars (mkMVar text)
|
||||
|
||||
-- Evaluate the text in the `Hint`'s context to get the old variable names.
|
||||
let rawText := (← GameServer.evalHintMessage text) hintFVarsNames
|
||||
let ctx₂ := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
|
||||
let rawText : String ← (MessageData.withContext ctx₂ rawText).toString
|
||||
|
||||
return {
|
||||
goal := ← abstractCtx goal
|
||||
text := ← instantiateMVars (mkMVar text)
|
||||
text := text
|
||||
rawText := rawText
|
||||
strict := strict == 1
|
||||
hidden := hidden == 1
|
||||
}
|
||||
@@ -440,58 +464,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
|
||||
|
||||
/-! # Hints -/
|
||||
|
||||
/-- 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 (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
|
||||
let mut strict := false
|
||||
let mut hidden := false
|
||||
|
||||
-- remove spaces at the beginning 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 (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do
|
||||
|
||||
@@ -1,7 +1,8 @@
|
||||
import GameServer.AbstractCtx
|
||||
import GameServer.Graph
|
||||
import GameServer.Hints
|
||||
|
||||
|
||||
open GameServer
|
||||
|
||||
/-- The default game name if `Game "MyGame"` is not used. -/
|
||||
def defaultGameName: String := "MyGame"
|
||||
@@ -18,22 +19,6 @@ 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
|
||||
}
|
||||
|
||||
/-! ## Inventory (documentation)
|
||||
|
||||
The inventory contains documentation that the user can access.
|
||||
|
||||
@@ -4,8 +4,6 @@ import Lean
|
||||
|
||||
open Lean Meta Elab Command
|
||||
|
||||
syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
|
||||
|
||||
/-! ## Doc Comment Parsing -/
|
||||
|
||||
/-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
|
||||
@@ -85,23 +83,6 @@ def getStatementString (name : Name) : CommandElabM String := do
|
||||
syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
|
||||
-- TODO
|
||||
|
||||
|
||||
/-- 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⟩ ""
|
||||
|
||||
|
||||
/-! ## Loops in Graph-like construct
|
||||
|
||||
TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?
|
||||
|
||||
@@ -0,0 +1,106 @@
|
||||
import GameServer.AbstractCtx
|
||||
|
||||
/-!
|
||||
This file contains anything related to the `Hint` tactic used to add hints to a game level.
|
||||
-/
|
||||
|
||||
open Lean Meta Elab
|
||||
|
||||
namespace GameServer
|
||||
|
||||
syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
|
||||
|
||||
/-- 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
|
||||
rawText : String
|
||||
/-- 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
|
||||
}
|
||||
|
||||
/-- For a hint `(hint : GoalHintEntry)` one uses `(← evalHintMessage hint.text) x`
|
||||
where `(x : Array Expr)` contains the names of all the variables that should be inserted
|
||||
in the text.
|
||||
|
||||
TODO: explain better. -/
|
||||
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 _ => "")
|
||||
|
||||
/-- 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 (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
|
||||
let mut strict := false
|
||||
let mut hidden := false
|
||||
|
||||
-- remove spaces at the beginning 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)
|
||||
@@ -1,6 +1,7 @@
|
||||
import GameServer.EnvExtensions
|
||||
import GameServer.InteractiveGoal
|
||||
import Std.Data.Array.Init.Basic
|
||||
import GameServer.Hints
|
||||
|
||||
open Lean
|
||||
open Server
|
||||
@@ -103,14 +104,6 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
|
||||
then return some bij
|
||||
else return none
|
||||
|
||||
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) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
|
||||
@@ -122,6 +115,8 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
|
||||
if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
|
||||
then
|
||||
|
||||
-- NOTE: This code for `hintFVarsNames` is also duplicated in the
|
||||
-- "Statement" command, where `hint.rawText` is created. They need to be matching.
|
||||
-- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
|
||||
-- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
|
||||
-- and we wrap them in `«{}»` here since I don't know how to do it later.
|
||||
@@ -140,11 +135,6 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
|
||||
let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
|
||||
let text ← (MessageData.withContext ctx text).toString
|
||||
|
||||
-- Evaluate the text in the `Hint`'s context to get the old variable names.
|
||||
let rawText := (← evalHintMessage hint.text) hintFVarsNames
|
||||
let ctx₂ := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
|
||||
let rawText ← (MessageData.withContext ctx₂ rawText).toString
|
||||
|
||||
-- Here we map the goal's variable names to the player's variable names.
|
||||
let mut varNames : Array <| Name × Name := #[]
|
||||
for (fvar₁, fvar₂) in bij.forward.toArray do
|
||||
@@ -157,7 +147,7 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
|
||||
return some {
|
||||
text := text,
|
||||
hidden := hint.hidden,
|
||||
rawText := rawText,
|
||||
rawText := hint.rawText,
|
||||
varNames := varNames }
|
||||
|
||||
else return none
|
||||
|
||||
Reference in New Issue
Block a user