basic inline hints

server/leanserver/GameServer/Commands.lean

@@ -63,6 +63,20 @@ def reprint (stx : Syntax) : Format :=
 
 -- macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
 
+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))
+
 /-- Define the statement of the current level.
 
 Arguments:
@@ -74,15 +88,40 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
   let lvlIdx ← getCurLevelIdx
   let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
     ("level" ++ toString lvlIdx : String)
+
+  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+
   let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
   -- let thmStatement' ← match statementName with
   -- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
   -- | some name => `(lemma $name $sig $val)
+  elabCommand thmStatement
+
+  let msgs := (← get).messages
+
+  let mut hints := #[]
+  for msg in msgs.msgs do
+    -- TODO: mark the hints in a unique way to recognize them here
+    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
+          text := ← instantiateMVars (mkMVar text)
+        }
+      hints := hints.push hint
+
+  modify fun st => { st with
+    messages := initMsgs ++ msgs
+  }
 
   let scope ← getScope
   let env ← getEnv
 
-  elabCommand thmStatement
   modifyCurLevel fun level => pure {level with
     module := env.header.mainModule
     goal := sig,
@@ -91,6 +130,7 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
     descrFormat := match statementName with
     | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
     | some name => (Format.join ["lemma ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10  -- "lemma "  ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
+    hints := hints
   } -- Format.pretty <| format thmStatement.raw }
 
 /-- Define the conclusion of the current game or current level if some

server/leanserver/GameServer/RpcHandlers.lean

@@ -25,6 +25,46 @@ def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option G
     | return none
   return ← getLevel? levelId
 
+
+/-- 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
+  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
+  | .const n1 ls1, .const n2 ls2 =>
+    return n1 == n2 && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
+  | .app f1 a1, .app f2 a2 =>
+    return (← matchExprAux f1 f2) && (← matchExprAux a1 a2)
+  | .lam _ t1 b1 _, .lam _ t2 b2 _ =>
+    return (← matchExprAux t1 t2) && (← matchExprAux b1 b2)
+  | .forallE _ t1 b1 _, .forallE _ t2 b2 _ =>
+    return (← matchExprAux t1 t2) && (← matchExprAux b1 b2)
+  | .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ =>
+    return (← matchExprAux t1 t2) && (← matchExprAux v1 v2)  && (← matchExprAux b1 b2)
+  | .lit l1, .lit l2 =>
+    return l1 == l2
+  | .proj i1 n1 e1, .proj i2 n2 e2 =>
+    return i1 == i2 && n1 == n2 && (← matchExprAux e1 e2)
+  -- ignore mdata:
+  | .mdata _ pattern', _ =>
+    return ← matchExprAux pattern' e
+  | _, .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
+
+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
   -- We iterate through the array backwards hoping that this will find us faster results
@@ -38,7 +78,7 @@ def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool :=
       let declFvar := declFvars[declFvars.size - j - 1]!
       let usedFvar := usedFvars[declFvars.size - j - 1]!
       if ¬ usedFvar then
-        if ← isDefEq declMvar declFvar then
+        if ← matchExpr declMvar declFvar then
           usedFvars := usedFvars.set! (declFvars.size - j - 1) true
           found := true
           break
@@ -64,7 +104,7 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array
     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 ← isDefEq hintGoal (← inferType $ mkMVar goal)
+      if ← matchExpr hintGoal (← inferType $ mkMVar goal)
       then
         let lctx ← getLCtx -- Local context of the `goal`
         if ← matchDecls declMvars lctx.getFVars

server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean

@@ -21,6 +21,7 @@ Du siehst Robo hilflos an.
 Statement ""
     (A B C : Prop) :
     ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
+  Hint "Hello? {A}"
   tauto
 
 Hint  (A B C : Prop) :