check trigger for messages

server/leanserver/GameServer/Commands.lean

@@ -116,16 +116,10 @@ def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
 /-- Declare a message. This version doesn't prevent the unused linter variable from running. -/
 local elab "Message'" 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 ← instantiateMVars (← elabTerm g none))
+  let g ← liftTermElabM do (return ← elabTermAndSynthesize g none)
-  let (ctx_size, normalized_goal) ← liftTermElabM do
-    let msg_mvar ← mkFreshExprMVar g MetavarKind.syntheticOpaque
-    msg_mvar.mvarId!.withContext do
-      let (_, msg_mvar) ← msg_mvar.mvarId!.introNP decls.size
-      return ((← msg_mvar.getDecl).lctx.size,  (← normalizedRevertExpr msg_mvar))
   modifyCurLevel fun level => pure {level with messages := level.messages.push {
-    ctx_size := ctx_size,
+    goal := g,
-    normalized_goal := normalized_goal,
+    intros := decls.size,
-    intro_nb := decls.size,
     message := msg.getString }}
 
 /-- Declare a message in reaction to a given tactic state in the current level. -/

server/leanserver/GameServer/EnvExtensions.lean

@@ -11,9 +11,8 @@ open Lean
 /-! ## Messages -/
 
 structure GoalMessageEntry where
-  ctx_size : Nat
+  goal : Expr
-  normalized_goal : Expr
+  intros : Nat
-  intro_nb : Nat
   message : String
   deriving Repr
 

server/leanserver/GameServer/RpcHandlers.lean

@@ -73,10 +73,18 @@ def getLevelByFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String)
     | throwError "Level not found"
   return level
 
+open Meta in
+/-- Find all messages whose trigger matches the current goal -/
 def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array String) := do
   let level ← getLevelByFileName doc.meta.mkInputContext.fileName
-  return level.messages.map GoalMessageEntry.message
+  let messages ← level.messages.filterMapM fun message => do
+    let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
+    if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
+    then return some message.message
+    else return none
+  return messages
 
+/-- Get goals and messages at a given position -/
 def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal)) := do
   let doc ← readDoc
   let text := doc.meta.text

server/leanserver/GameServer/Utils.lean

@@ -2,29 +2,13 @@ import Lean
 
 open Lean
 
-def Lean.Expr.getFVars (e : Expr) : Array FVarId :=
-  (Lean.collectFVars {} e).fvarIds
-
-
-/-- Returns the type of the goal after reverting all free variables in the order
-where they appear in the goal type. -/
-partial def normalizedRevertExpr (goal : MVarId) : MetaM Expr := do
-  goal.withContext do
-    let (_, new) ← goal.revert (← goal.getType).getFVars true
-    let e ← new.getType
-    if e.hasFVar then 
-      return ← normalizedRevertExpr new
-    else
-      return (← new.getType)
-
-
 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
 { msgs := log.msgs.filter (·.severity matches .error) }
 
 /-- A version of `println!` that actually does its job by flushing stdout. -/
 def output {α : Type} [ToString α] (s : α) : IO Unit := do
   println! s
-  IO.FS.Stream.flush (← IO.getStdout)  
+  IO.FS.Stream.flush (← IO.getStdout)
 
 def Lean.LocalDecl.toJson (decl : LocalDecl) : MetaM Json :=
   return Lean.ToJson.toJson [toString decl.userName, toString (← Meta.ppExpr decl.type)]