diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 5f9e51d..1761b4d 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -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 diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index 2cdbc47..ddafbdc 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -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. diff --git a/server/GameServer/Helpers.lean b/server/GameServer/Helpers.lean index 4a59e75..debd3c2 100644 --- a/server/GameServer/Helpers.lean +++ b/server/GameServer/Helpers.lean @@ -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)`? diff --git a/server/GameServer/Hints.lean b/server/GameServer/Hints.lean new file mode 100644 index 0000000..0605e27 --- /dev/null +++ b/server/GameServer/Hints.lean @@ -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) diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index c815abf..2714f07 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -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