import Lean.Widget.InteractiveGoal
import Lean.Widget.InteractiveDiagnostic
import Lean.Data.Lsp.Diagnostics

/-!
This file contains the custom data structures use by the server.

Some of them overwrite built-in structures from Lean.

In particular, the structures from `Lean.Widget.InteractiveGoal` are duplicated with
the following extension:

* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.

NOTE: Changes here need to be reflected in  the corresponding `interface` in `rcp_api.ts`
on the client-side.
-/

open Lean Server Widget

namespace GameServer

/-- Extend the interactive hypothesis bundle with an option to distinguish
"assumptions" from "objects". "Assumptions" are hypotheses of type `Prop`. -/
-- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
  /-- The hypothesis's type is of type `Prop` -/
  isAssumption? : Option Bool := none
deriving RpcEncodable

-- duplicated but with custom `InteractiveHypothesisBundle`
@[inherit_doc Lean.Widget.InteractiveGoalCore]
structure InteractiveGoalCore where
  hyps : Array InteractiveHypothesisBundle
  type : CodeWithInfos
  ctx : WithRpcRef Elab.ContextInfo

-- duplicated but with custom `InteractiveGoalCore`
@[inherit_doc Lean.Widget.InteractiveGoal]
structure InteractiveGoal extends InteractiveGoalCore where
  userName? : Option String
  goalPrefix : String
  mvarId : MVarId
  isInserted? : Option Bool := none
  isRemoved? : Option Bool := none
deriving RpcEncodable

-- duplicated with custom `InteractiveGoalCore`
@[inherit_doc Lean.Widget.InteractiveTermGoal]
structure InteractiveTermGoal extends InteractiveGoalCore where
  range : Lsp.Range
  term : WithRpcRef Elab.TermInfo
deriving RpcEncodable

/-- A hint in the game at the corresponding goal. -/
structure GameHint where
  /-- The text with the variable names already inserted.

  Note: This is in theory superfluous and will be completely replaced by `rawText`. We just left
  it in for debugging for now. -/
  text : String
  /-- Flag whether the hint should be hidden initially. -/
  hidden : Bool
  /-- The text with the variables not inserted yet. -/
  rawText : String
  /-- The assignment of variable names in the `rawText` to the ones the player used. -/
  varNames : Array <| Name × Name
deriving FromJson, ToJson

/-- Bundled `InteractiveGoal` together with an array of hints that apply at this stage. -/
structure InteractiveGoalWithHints where
  goal : InteractiveGoal
  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
  hints : Array GameHint
deriving RpcEncodable

structure InteractiveGoalsWithHints where
  goals : Array InteractiveGoalWithHints
  /-- The content of the line evaluated. -/
  command : String
  diags : Array InteractiveDiagnostic := default
  line : Option Nat -- only for debugging
  column : Option Nat -- only for debugging

deriving RpcEncodable

instance : Inhabited InteractiveGoalsWithHints := ⟨default, default, default, none, none⟩

/-- Collected goals throughout the proof. Used for communication with the game client. -/
structure ProofState where
  /-- goals after each line. includes the hints. -/
  steps : Array <| InteractiveGoalsWithHints
  /-- diagnostics contains all errors and warnings.

  TODO: I think they contain information about which line they belong to. Verify this.
  -/
  diagnostics : Array InteractiveDiagnostic := default
  /-- Whether the level is considered solved. -/
  completed : Bool
  completedWithWarnings : Bool
  lastPos : Nat -- only for debugging
deriving RpcEncodable