add defeq-hints #45

server/GameServer/Commands.lean

@@ -4,7 +4,7 @@ import GameServer.Options
 import GameServer.SaveData
 import GameServer.Hints
 import GameServer.Tactic.LetIntros
-import GameServer.RpcHandlers -- only needed to collect the translations of "level completed" msgs
+-- import GameServer.RpcHandlers -- only needed to collect the translations of "level completed" msgs
 import I18n
 
 open Lean Meta Elab Command
@@ -437,6 +437,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
         .tagged `Hint $
         .nest strict $
         .nest hidden $
+        .nest defeq $
         .compose (.ofGoal text) (.ofGoal goal) := msg.data then
       let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
 
@@ -467,6 +468,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
           rawText := rawText
           strict := strict == 1
           hidden := hidden == 1
+          defeq := defeq == 1
         }
 
       -- Note: The current setup for hints is a bit convoluted, but for now we need to
@@ -522,6 +524,7 @@ 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
+  let mut defeq := false
 
   -- remove spaces at the beginning of new lines
   let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
@@ -543,6 +546,8 @@ elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(t
     | `(hintArg| (strict := false)) => strict := false
     | `(hintArg| (hidden := true)) => hidden := true
     | `(hintArg| (hidden := false)) => hidden := false
+    | `(hintArg| (defeq := true)) => defeq := true
+    | `(hintArg| (defeq := false)) => defeq := false
     | _ => throwUnsupportedSyntax
 
   let goal ← Tactic.getMainGoal
@@ -566,6 +571,7 @@ elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(t
       .tagged `Hint $
       .nest (if strict then 1 else 0) $
       .nest (if hidden then 1 else 0) $
+      .nest (if defeq 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

server/GameServer/Hints.lean

@@ -8,7 +8,7 @@ open Lean Meta Elab
 
 namespace GameServer
 
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden" <|> &"defeq") " := " withoutPosition(term) ")")
 
 /-- A hint to help the user with a specific goal state -/
 structure GoalHintEntry where
@@ -20,6 +20,7 @@ structure GoalHintEntry where
   hidden : Bool := false
   /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
   strict : Bool := false
+  defeq : Bool := false
 
 instance : Repr GoalHintEntry := {
   reprPrec := fun a n => reprPrec a.text n

server/GameServer/RpcHandlers.lean

@@ -79,7 +79,9 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) :
   | _, _ => 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 (Option FVarBijection) := do
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true)
+    (initBij : FVarBijection := {}) (defeq := false) : MetaM (Option FVarBijection) := do
+  let reducer := if defeq then whnf else pure
   -- We iterate through the array backwards hoping that this will find us faster results
   -- TODO: implement backtracking
   let mut bij := initBij
@@ -93,8 +95,8 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
         continue
 
       if let some bij' := matchExpr
-          (← instantiateMVars $ ← inferType pattern)
-          (← instantiateMVars $ ← inferType fvar) bij then
+          (← reducer <| ← instantiateMVars $ ← inferType pattern)
+          (← reducer <| ← instantiateMVars $ ← inferType fvar) bij then
         -- usedFvars := usedFvars.set! (fvars.size - j - 1) true
         bij := bij'.insert pattern.fvarId! fvar.fvarId!
         break
@@ -112,7 +114,10 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
       | throwError "Level not found: {m.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)
+        let reducer := if hint.defeq then whnf else pure
+        if let some fvarBij := matchExpr
+          (← reducer <| ← instantiateMVars $ hintGoal)
+          (← reducer <| ← instantiateMVars $ ← inferType $ mkMVar goal)
         then
 
           -- NOTE: This code for `hintFVarsNames` is also duplicated in the
@@ -127,7 +132,7 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
 
           let lctx := (← goal.getDecl).lctx -- the player's local context
           if let some bij ← matchDecls hintFVars lctx.getFVars
-            (strict := hint.strict) (initBij := fvarBij)
+            (strict := hint.strict) (initBij := fvarBij) (defeq := hint.defeq)
           then
             let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
             -- Evaluate the text in the player's context to get the new variable names.