use fvars instead of mvars for hints

server/leanserver/GameServer/AbstractCtx.lean

@@ -0,0 +1,24 @@
+import Lean
+
+section AbstractCtx
+open Lean
+open Meta
+
+structure AbstractCtxResult :=
+  (abstractMVarsResult : AbstractMVarsResult)
+
+/-- Abstract LCtx and MCtx to transport an expression into different contexts -/
+def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do
+  let goalDecl ← goal.getDecl
+  let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (mkFVar ·.fvarId)
+  let goal ← mkLambdaFVars (usedLetOnly := false) fvars goalDecl.type
+  let goal ← abstractMVars goal
+  return {
+    abstractMVarsResult := goal
+  }
+
+def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+  let (mvars, binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult
+  lambdaLetTelescope (← instantiateMVars expr) k
+
+end AbstractCtx

server/leanserver/GameServer/Commands.lean

@@ -65,17 +65,18 @@ def reprint (stx : Syntax) : Format :=
 
 elab "Hint" msg:interpolatedStr(term) : tactic => do
   let goal ← Tactic.getMainGoal
-  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 mvar ← mkFreshExprMVar none
-  guard $ ← isDefEq mvar text
-  logInfo (.compose (.ofGoal mvar.mvarId!) (.ofGoal goal))
+  goal.withContext do
+    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 mvar ← mkFreshExprMVar none
+    guard $ ← isDefEq mvar text
+    logInfo (.compose (.ofGoal mvar.mvarId!) (.ofGoal goal))
 
 /-- Define the statement of the current level.
 
@@ -105,12 +106,8 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
     if let (MessageData.withNamingContext nctx (MessageData.withContext ctx
         (.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 (mkFVar ·.fvarId)
-        let goal ← mkForallFVars fvars goalDecl.type
         return {
-          goal := goal
-          intros := fvars.size
+          goal := ← abstractCtx goal
           text := ← instantiateMVars (mkMVar text)
         }
       hints := hints.push hint
@@ -178,38 +175,40 @@ 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
+-- 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}"
+--   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 }}
+  -- 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
+  -- 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.
 -/
 local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
-  elabHint true binders goal msg
+  -- 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

server/leanserver/GameServer/EnvExtensions.lean

@@ -1,5 +1,6 @@
 import Lean
 import GameServer.Graph
+import GameServer.AbstractCtx
 
 /-! # Environment extensions
 
@@ -16,15 +17,15 @@ open Lean
 A hint to help the user with a specific goal state
 -/
 structure GoalHintEntry where
-  goal : Expr
-  /-- Number of variables to intro in the beginning of goal -/
-  intros : Nat
+  goal : AbstractCtxResult
   /-- 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
 
+instance : Repr GoalHintEntry := {
+  reprPrec := fun a n => reprPrec a.text n
+}
 
 /-! ## Tactic/Definition/Lemma documentation -/
 

server/leanserver/GameServer/RpcHandlers.lean

@@ -25,67 +25,82 @@ def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option G
     | return none
   return ← getLevel? levelId
 
+structure FVarBijection :=
+  (forward : HashMap FVarId FVarId)
+  (backward : HashMap FVarId FVarId)
 
-/-- Checks if `pattern` and `e` are equal up to mvars in `pattern` that may be assigned to fvars in `e`. -/
-partial def matchExprAux (pattern : Expr) (e : Expr) : MetaM Bool := do
+instance : EmptyCollection FVarBijection := ⟨{},{}⟩
+
+def FVarBijection.insert (bij : FVarBijection) (a b : FVarId) : FVarBijection :=
+  ⟨bij.forward.insert a b, bij.backward.insert b a⟩
+
+def FVarBijection.insert? (bij : FVarBijection) (a b : FVarId) : Option FVarBijection :=
+  let a' := bij.forward.find? a
+  let b' := bij.forward.find? b
+  if (a' == none || a' == some b) && (b' == none || b' == some a)
+  then some $ bij.insert a b
+  else none
+
+/-- Checks if `pattern` and `e` are equal up to FVar identities. -/
+partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) : Option FVarBijection :=
   match pattern, e with
-  | .bvar i1, .bvar i2 => return i1 == i2
-  | .fvar i1, .fvar i2 => return i1 == i2
-  | .mvar _, .mvar _ => return true
-  | .sort u1, .sort u2 => Meta.isLevelDefEq u1 u2
+  | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
+  | .fvar i1, .fvar i2 => bij.insert? i1 i2
+  | .mvar _, .mvar _ => bij
+  | .sort u1, .sort u2 => bij -- TODO?
   | .const n1 ls1, .const n2 ls2 =>
-    return n1 == n2 && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
+    if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
   | .app f1 a1, .app f2 a2 =>
-    return (← matchExprAux f1 f2) && (← matchExprAux a1 a2)
+    some bij
+      |> (Option.bind · (fun bij => matchExpr f1 f2 bij))
+      |> (Option.bind · (fun bij => matchExpr a1 a2 bij))
   | .lam _ t1 b1 _, .lam _ t2 b2 _ =>
-    return (← matchExprAux t1 t2) && (← matchExprAux b1 b2)
+    some bij
+      |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
+      |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
   | .forallE _ t1 b1 _, .forallE _ t2 b2 _ =>
-    return (← matchExprAux t1 t2) && (← matchExprAux b1 b2)
+    some bij
+      |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
+      |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
   | .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ =>
-    return (← matchExprAux t1 t2) && (← matchExprAux v1 v2)  && (← matchExprAux b1 b2)
+    some bij
+      |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
+      |> (Option.bind · (fun bij => matchExpr v1 v2 bij))
+      |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
   | .lit l1, .lit l2 =>
-    return l1 == l2
+    if l1 == l2 then bij else none
   | .proj i1 n1 e1, .proj i2 n2 e2 =>
-    return i1 == i2 && n1 == n2 && (← matchExprAux e1 e2)
+    if i1 == i2 && n1 == n2 then matchExpr e1 e2 bij else none
   -- ignore mdata:
   | .mdata _ pattern', _ =>
-    return ← matchExprAux pattern' e
+    matchExpr pattern' e bij
   | _, .mdata _ e' =>
-    return ← matchExprAux pattern e'
-  -- assign fvars to mvars:
-  | .mvar i1, .fvar _ =>
-    match ← getExprMVarAssignment? i1 with
-    | some pattern' => matchExprAux pattern' e
-    | none =>
-      i1.assign e
-      return true
-  | _, _ => return false
+    matchExpr pattern e' bij
+  | _, _ => none
 
-def matchExpr (pattern : Expr) (e : Expr) : MetaM Bool := do
-  checkpointDefEq (mayPostpone := true) do
-    matchExprAux pattern e
-
-/-- Check if each meta variable in `declMvars` has a matching fvar in `declFvars` -/
-def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := do
+/-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) : Bool :=
   -- We iterate through the array backwards hoping that this will find us faster results
   -- TODO: implement backtracking
-  let mut usedFvars := (List.replicate declFvars.size false).toArray
-  -- `usedFvars` keeps track of the fvars that were already used to match an mvar.
-  for i in [:declMvars.size] do
-    let declMvar := declMvars[declMvars.size - i - 1]!
-    let mut found := false
-    for j in [:declFvars.size] do
-      let declFvar := declFvars[declFvars.size - j - 1]!
-      let usedFvar := usedFvars[declFvars.size - j - 1]!
-      if ¬ usedFvar then
-        if ← matchExpr declMvar declFvar then
-          usedFvars := usedFvars.set! (declFvars.size - j - 1) true
-          found := true
-          break
-      else
-        continue
-    if ¬ found then return false
-  return true
+  -- TODO: reimplement this
+  patterns.size = fvars.size
+  -- let mut usedFvars := (List.replicate declFvars.size false).toArray
+  -- -- `usedFvars` keeps track of the fvars that were already used to match an mvar.
+  -- for i in [:declMvars.size] do
+  --   let declMvar := declMvars[declMvars.size - i - 1]!
+  --   let mut found := false
+  --   for j in [:declFvars.size] do
+  --     let declFvar := declFvars[declFvars.size - j - 1]!
+  --     let usedFvar := usedFvars[declFvars.size - j - 1]!
+  --     if ¬ usedFvar then
+  --       if let some _ := matchExpr declMvar declFvar then
+  --         usedFvars := usedFvars.set! (declFvars.size - j - 1) true
+  --         found := true
+  --         break
+  --     else
+  --       continue
+  --   if ¬ found then return false
+  -- return true
 
 unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
   evalExpr (Array Expr → MessageData)
@@ -102,19 +117,19 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array
     let some level ← getLevelByFileName? doc.meta.mkInputContext.fileName
       | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
     let hints ← level.hints.filterMapM fun hint => do
-      let (declMvars, binderInfo, hintGoal) ← forallMetaBoundedTelescope hint.goal hint.intros
-      -- TODO: Protect mvars in the type of `goal` to be instantiated?
-      if ← matchExpr hintGoal (← inferType $ mkMVar goal)
-      then
-        let lctx ← getLCtx -- Local context of the `goal`
-        if ← matchDecls declMvars lctx.getFVars
+      openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
+        if let some _ := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
         then
-          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
+          let lctx := (← goal.getDecl).lctx
+          if matchDecls hintFVars lctx.getFVars
+          then
+            let text := (← evalHintMessage hint.text) hintFVars
+            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
 
 open RequestM in