From 3cbb4774f145770f345570a07bb44f4dd5f0459d Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Fri, 3 Mar 2023 15:55:15 +0100 Subject: [PATCH] hints with variable names --- server/leanserver/GameServer/Commands.lean | 50 +++++++++---------- .../leanserver/GameServer/EnvExtensions.lean | 9 ++-- server/leanserver/GameServer/RpcHandlers.lean | 13 ++++- .../Levels/Proposition/L00_Tauto.lean | 2 +- 4 files changed, 40 insertions(+), 34 deletions(-) diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index 8d08e6e..1b4127a 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -132,54 +132,50 @@ end metadata open Lean Meta Elab Command Term -declare_syntax_cat mydecl -syntax "(" ident ":" term ")" : mydecl - -def getIdent : TSyntax `mydecl → Ident -| `(mydecl| ($n:ident : $_t:term)) => n -| _ => default - -def getType : TSyntax `mydecl → Term -| `(mydecl| ($_n:ident : $t:term)) => t -| _ => default - /-- 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 -/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/ -local elab "Hint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do - let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList - let g ← liftTermElabM do (return ← elabTermAndSynthesize g none) +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 + return (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 modifyCurLevel fun level => pure {level with hints := level.hints.push { goal := g, intros := decls.size, - text := msg.getString }} + 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 /-- 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. -/ -local elab "HiddenHint'" decls:mydecl* ":" goal:term "=>" msg:str : command => do - let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList - let g ← liftTermElabM do (return ← elabTermAndSynthesize g none) - modifyCurLevel fun level => pure {level with hints := level.hints.push { - goal := g, - intros := decls.size, - hidden := true, - text := msg.getString }} - +local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do + elabHint true binders goal msg /-- Declare a hint in reaction to a given tactic state in the current level. -/ -macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do +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:mydecl* ":" goal:term "=>" msg:str : command => do +macro "HiddenHint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do `(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg) + /-! ## Inventory -/ /-- Throw an error if inventory doc does not exist -/ diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index 16fed62..1d248a7 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -14,15 +14,14 @@ open Lean /-- A hint to help the user with a specific goal state - -Fields - (TODO) - hidden: If true, then hint should be hidden by default -/ structure GoalHintEntry where goal : Expr + /-- Number of variables to intro in the beginning of goal -/ intros : Nat - text : String + /-- Text of the hint as an expression of type `Array Expr → MessageData` -/ + text : Expr + /-- If true, then hint should be hidden by default -/ hidden : Bool := false deriving Repr diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index d9c5726..9176aca 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -47,6 +47,14 @@ def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := if ¬ found then return false 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) : MetaM (Array GameHint) := do @@ -61,7 +69,10 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array let lctx ← getLCtx -- Local context of the `goal` if ← matchDecls declMvars lctx.getFVars then - return some { text := hint.text, hidden := hint.hidden } + let text := (← evalHintMessage hint.text) declMvars + 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 diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 4c09230..a46e273 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -43,7 +43,7 @@ $$ ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by tauto -HiddenHint (A : Prop) (B : Prop) (C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) => +Hint (A B C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) => "Man schreibt eine Taktik pro Zeile, also gib `tauto` ein und geh mit Enter ⏎ auf eine neue Zeile." Conclusion ""