lean4game/server/GameServer/RpcHandlers.lean

import GameServer.EnvExtensions
import GameServer.InteractiveGoal
import GameServer.Hints
import I18n

open Lean
open Server
open Widget
open RequestM
open Meta

/-! ## GameGoal -/

namespace GameServer

def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String) : Option LevelId := Id.run do
  let fileParts := fileName.splitOn "/"
  if fileParts.length == 3 then
    if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then
      return some {game, world := fileParts[1]!, level := level}
  return none

def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do
  let some levelId := levelIdFromFileName? initParams fileName
    | return none
  return ← getLevel? levelId

structure FVarBijection :=
  (forward : HashMap FVarId FVarId)
  (backward : HashMap FVarId FVarId)

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 => 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 =>
    if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
  | .app f1 a1, .app f2 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 _ =>
    some bij
      |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
      |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
  | .forallE _ t1 b1 _, .forallE _ t2 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 _ =>
    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 =>
    if l1 == l2 then bij else none
  | .proj i1 n1 e1, .proj i2 n2 e2 =>
    if i1 == i2 && n1 == n2 then matchExpr e1 e2 bij else none
  -- ignore mdata:
  | .mdata _ pattern', _ =>
    matchExpr pattern' e bij
  | _, .mdata _ e' =>
    matchExpr pattern e' bij
  | _, _ => 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
  -- We iterate through the array backwards hoping that this will find us faster results
  -- TODO: implement backtracking
  let mut bij := initBij
  for i in [:patterns.size] do
    let pattern := patterns[patterns.size - i - 1]!
    if bij.forward.contains pattern.fvarId! then
      continue
    for j in [:fvars.size] do
      let fvar := fvars[fvars.size - j - 1]!
      if bij.backward.contains fvar.fvarId! then
        continue

      if let some bij' := matchExpr
          (← instantiateMVars $ ← inferType pattern)
          (← instantiateMVars $ ← inferType fvar) bij then
        -- usedFvars := usedFvars.set! (fvars.size - j - 1) true
        bij := bij'.insert pattern.fvarId! fvar.fvarId!
        break
    if ! bij.forward.contains pattern.fvarId! then return none

  if !strict || fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
  then return some bij
  else return none

open Meta in
/-- Find all hints whose trigger matches the current goal -/
def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
  goal.withContext do
    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
      | 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)
        then

          -- NOTE: This code for `hintFVarsNames` is also duplicated in the
          -- "Statement" command, where `hint.rawText` is created. They need to be matching.
          -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
          -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
          -- and we wrap them in `«{}»` here since I don't know how to do it later.
          let mut hintFVarsNames : Array Expr := #[]
          for fvar in hintFVars do
            let name₁ ← fvar.fvarId!.getUserName
            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩

          let lctx := (← goal.getDecl).lctx -- the player's local context
          if let some bij ← matchDecls hintFVars lctx.getFVars
            (strict := hint.strict) (initBij := fvarBij)
          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.
            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
            let text ← (MessageData.withContext ctx text).toString

            -- Here we map the goal's variable names to the player's variable names.
            let mut varNames : Array <| Name × Name := #[]
            for (fvar₁, fvar₂) in bij.forward.toArray do
              -- get the `userName` of the fvar in the opened local context of the hint.
              let name₁ ← fvar₁.getUserName
              -- get the `userName` in the player's local context.
              let name₂ := (lctx.get! fvar₂).userName
              varNames := varNames.push (name₁, name₂)

            return some {
              text := text,
              hidden := hint.hidden,
              rawText := hint.rawText,
              varNames := varNames }

          else return none
        else
          return none
    return hints

def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
    Array InteractiveDiagnostic :=
  a.filter (fun d => match d.message with
  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
  | _ => true)

-- TODO: no need to have `RequestM`, just anything where `mut` works
/-- Add custom diagnostics about whether the level is completed. -/
def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : Bool)
    (completedWithWarnings : Bool) (pos : Lsp.Position)
    (startDiags : Array InteractiveDiagnostic := #[]) :
    RequestM <| Array InteractiveDiagnostic := do
  let mut out : Array InteractiveDiagnostic := startDiags
  if goalCount == 0 then
    if completed then
      out := out.push {
        -- TODO: marking these with `t!` has the implication that every game
        -- needs to translate these messages again,
        -- but cannot think of another option
        -- that would not involve manually adding them somewhere in the translation files.
        message := .text t!"level completed! 🎉"
        range := {
          start := pos
          «end» := pos
          }
        severity? := Lsp.DiagnosticSeverity.information }
    else if completedWithWarnings then
      out := out.push {
        message := .text t!"level completed with warnings… 🎭"
        range := {
          start := pos
          «end» := pos
          }
        severity? := Lsp.DiagnosticSeverity.information }
    else
      pure ()
  else if goalCount < prevGoalCount then
    -- If there is any errors, goals might vanish without being 'solved'
    -- so showing the message "intermediate goal solved" would be confusing.
    if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then
      out := out.push {
        message := .text t!"intermediate goal solved! 🎉"
        range := {
          start := pos
          «end» := pos
          }
        severity? := Lsp.DiagnosticSeverity.information
      }

  return out


/-- Request that returns the goals at the end of each line of the tactic proof
plus the diagnostics (i.e. warnings/errors) for the proof.
 -/
def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option ProofState)) := do
  let doc ← readDoc
  let rc ← readThe RequestContext
  let text := doc.meta.text

  withWaitFindSnap
    doc
    -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking
    -- for the first snap with goals here.
    -- NOTE (Jon): The entire proof is in one snap, so hoped that Position `0` is good enough.
    (fun snap => ¬ (snap.infoTree.goalsAt? doc.meta.text 0).isEmpty)
    (notFoundX := return none)
    fun snap => do
      -- `snap` is the one snapshot containing the entire proof.
      let mut steps : Array <| InteractiveGoalsWithHints := #[]

      -- Question: Is there a difference between the diags of this snap and the last snap?
      -- Should we get the diags from there?
      -- Answer: The last snap only copied the diags from the end of this snap
      let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray

      -- Level is completed if there are no errors or warnings
      let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
      let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)

      let mut intermediateGoalCount := 0

      -- only the positions that have non-whitespace characters since the last position
      -- should add a new proof step.
      let positionsWithSource : Array (String.Pos × String) :=
        text.positions.zipWithIndex.filterMap (
          fun (pos, i) => match i with
          | 0 => some (pos, "")
          | i' + 1 =>
            let source : String := Substring.toString ⟨text.source, text.positions.get! i', pos⟩
            if source.trim.length == 0 then
              none
            else
              some (pos, source))

      -- Drop the last position as we ensured that there is always a newline at the end
      for ((pos, source), i) in positionsWithSource.zipWithIndex do
        -- iterate over all steps in the proof and get the goals and hints at each position

        -- diags are labeled in Lsp-positions, which differ from the lean-internal
        -- positions by `1`.
        let lspPosAt := text.utf8PosToLspPos pos

        let mut diagsAtPos : Array InteractiveDiagnostic := filterUnsolvedGoal <|
          -- `+1` for getting the errors after the line.
          match i with
          | 0 =>
            -- `lspPosAt` is `(0, 0)`
            diag.filter (fun d => d.range.start == lspPosAt )
          | i' + 1 =>
            diag.filter (fun d =>
              ((text.utf8PosToLspPos <| (positionsWithSource.get! i').1) ≤ d.range.start) ∧
              d.range.start < lspPosAt )

        if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text pos then
          let goalsAtPos' : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
            fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
              -- TODO: What does this function body do?
              -- let ciAfter := { ci with mctx := ti.mctxAfter }
              let ci := if useAfter then
                  { ci with mctx := tacticInfo.mctxAfter }
                else
                  { ci with mctx := tacticInfo.mctxBefore }
              -- compute the interactive goals
              let goalMvars : List MVarId ← ci.runMetaM {} do
                return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore

              let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
                goalMvars.mapM fun goal => do
                  let hints ← findHints goal doc.meta rc.initParams
                  let interactiveGoal ← goalToInteractive goal
                  return ⟨interactiveGoal, hints⟩
              -- TODO: This code is way old, can it be deleted?
              -- compute the goal diff
              -- let goals ← ciAfter.runMetaM {} (do
              --     try
              --       Widget.diffInteractiveGoals useAfter ti goals
              --     catch _ =>
              --       -- fail silently, since this is just a bonus feature
              --       return goals
              -- )
              return interactiveGoals
          let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalsAtPos'.foldl (· ++ ·) []⟩

          diagsAtPos ← completionDiagnostics goalsAtPos.size intermediateGoalCount
            completed completedWithWarnings lspPosAt diagsAtPos

          intermediateGoalCount := goalsAtPos.size

          steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩
        else
          -- No goals present
          steps := steps.push ⟨#[], source, diagsAtPos, lspPosAt.line, none⟩

      -- Filter out the "unsolved goals" message
      diag := filterUnsolvedGoal diag

      let lastPos := text.utf8PosToLspPos positionsWithSource.back.1
      let remainingDiags : Array InteractiveDiagnostic :=
        diag.filter (fun d => lastPos ≤ d.range.start)

      return some {
        steps := steps,
        diagnostics := remainingDiags,
        completed := completed,
        completedWithWarnings := completedWithWarnings,
        lastPos := lastPos.line
        }

open RequestM in

-- The editor apparently uses this
def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do
  let doc ← readDoc
  -- let rc ← readThe RequestContext
  let text := doc.meta.text
  let hoverPos := text.lspPosToUtf8Pos p.position
  -- TODO: I couldn't find a good condition to find the correct snap. So we are looking
  -- for the first snap with goals here:
  withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
    (notFoundX := return none) fun snap => do
      if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
        let goals : List <| Array InteractiveGoal ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
          let ciAfter := { ci with mctx := ti.mctxAfter }
          let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
          -- compute the interactive goals
          let goals ← ci.runMetaM {} do
            return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
          let goals ← ci.runMetaM {} do
             goals.mapM fun goal => do
              -- let hints ← findHints goal doc.meta rc.initParams
              return ← goalToInteractive goal
          -- compute the goal diff
          -- let goals ← ciAfter.runMetaM {} (do
          --     try
          --       Widget.diffInteractiveGoals useAfter ti goals
          --     catch _ =>
          --       -- fail silently, since this is just a bonus feature
          --       return goals
          -- )
          return goals
        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
      else
        return none

builtin_initialize
  registerBuiltinRpcProcedure
    `Game.getInteractiveGoals
    Lsp.PlainGoalParams
    (Option <| InteractiveGoals
    )
    getInteractiveGoals

builtin_initialize
  registerBuiltinRpcProcedure
    `Game.getProofState
    Lsp.PlainGoalParams
    (Option ProofState)
    getProofState


end GameServer