PyPantograph/src/Pantograph/Protocol.lean

/-
All the command input/output structures are stored here

Note that no command other than `InteractionError` may have `error` as one of
its field names to avoid confusion with error messages generated by the REPL.
-/
import Pantograph.Goal

import Lean.Data.Json
import Lean.Data.Position
import Lean.Message

namespace Pantograph.Protocol

open Lean (Json ToJson FromJson Position Name)

/-- Main Option structure, placed here to avoid name collision -/
structure Options where
  -- When false, suppress newlines in Json objects. Useful for machine-to-machine interaction.
  -- This should be  false` by default to avoid any surprises with parsing.
  printJsonPretty: Bool    := false
  -- When enabled, pretty print every expression
  printExprPretty: Bool    := true
  -- When enabled, print the raw AST of expressions
  printExprAST: Bool       := false
  printDependentMVars: Bool := false
  -- When enabled, the types and values of persistent variables in a goal
  -- are not shown unless they are new to the proof step. Reduces overhead.
  -- NOTE: that this assumes the type and assignment of variables can never change.
  noRepeat: Bool := false
  -- See `pp.auxDecls`
  printAuxDecls: Bool      := false
  -- See `pp.implementationDetailHyps`
  printImplementationDetailHyps: Bool := false
  -- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
  automaticMode: Bool := true
  -- Timeout for tactics and operations that could potentially execute a tactic
  timeout: Nat := 0
  deriving ToJson

abbrev OptionsT := ReaderT Options

/-- Set options; See `Options` struct above for meanings -/
structure OptionsSet where
  printJsonPretty?: Option Bool := .none
  printExprPretty?: Option Bool := .none
  printExprAST?: Option Bool := .none
  printDependentMVars?: Option Bool := .none
  noRepeat?: Option Bool := .none
  printAuxDecls?: Option Bool := .none
  printImplementationDetailHyps?: Option Bool := .none
  automaticMode?: Option Bool := .none
  timeout?: Option Nat := .none
  deriving FromJson
structure OptionsSetResult where
  deriving ToJson
structure OptionsPrint where
  deriving FromJson

--- Expression Objects ---

structure BoundExpression where
  binders: Array (String × String)
  target: String
  deriving ToJson
structure Expression where
  -- Pretty printed expression
  pp?: Option String             := .none
  -- AST structure
  sexp?: Option String           := .none
  dependentMVars?: Option (Array Name) := .none
  deriving ToJson

structure Variable where
  /-- The internal name used in raw expressions -/
  name: Name := .anonymous
  /-- The name displayed to the user -/
  userName: Name
  /-- Does the name contain a dagger -/
  isInaccessible: Bool := false
  type?: Option Expression  := .none
  value?: Option Expression := .none
  deriving ToJson
inductive Fragment where
  | tactic
  | conv
  | calc
  deriving BEq, DecidableEq, Repr, ToJson
structure Goal where
  /-- Name of the metavariable -/
  name : Name := .anonymous
  /-- User-facing name -/
  userName? : Option Name := .none
  fragment : Fragment := .tactic
  /-- target expression type -/
  target : Expression
  /-- Variables -/
  vars : Array Variable := #[]
  deriving ToJson

--- Individual Commands and return types ---

structure Command where
  cmd: String
  payload: Json
  deriving FromJson

structure InteractionError where
  error: String
  desc: String
  deriving ToJson

namespace InteractionError

def errorIndex (desc : String) : InteractionError := { error := "index", desc }
def errorCommand (desc : String) : InteractionError := { error := "command", desc }
def errorExpr (desc : String) : InteractionError := { error := "expr", desc }
def errorParse (desc : String) : InteractionError := { error := "parse", desc }
def errorIO (desc : String) : InteractionError := { error := "io", desc }
def errorException (desc : String) : InteractionError := { error := "exception", desc }

end InteractionError

structure Reset where
  deriving FromJson
structure Stat where
  deriving FromJson
structure StatResult where
  -- Number of goals states
  nGoals: Nat
  deriving ToJson

-- Return the type of an expression
structure ExprEcho where
  expr: String
  type?: Option String := .none
  -- universe levels
  levels?: Option (Array Name) := .none
  deriving FromJson
structure ExprEchoResult where
  expr: Expression
  type: Expression
  deriving ToJson

-- Describe the current state of the environment
structure EnvDescribe where
  deriving FromJson
structure EnvDescribeResult where
  imports : Array Name
  modules : Array Name
  deriving ToJson

-- Describe a module
structure EnvModuleRead where
  module : Name
  deriving FromJson
structure EnvModuleReadResult where
  imports: Array Name
  constNames: Array Name
  extraConstNames: Array Name
  deriving ToJson

-- Print all symbols in environment
structure EnvCatalog where
  filename : String
  modulePrefix? : Option String := .none
  invertFilter : Bool := false
  deriving FromJson
structure EnvCatalogResult where
  nSymbols : Nat
  deriving ToJson

-- Print the type of a symbol
structure EnvInspect where
  name: Name
  -- Show the value expressions; By default definitions values are shown and
  -- theorem values are hidden.
  value?: Option Bool := .some false
  -- Show the type and value dependencies
  dependency?: Option Bool := .some false
  -- Show source location
  source?: Option Bool := .some false
  deriving FromJson
-- See `InductiveVal`
structure InductInfo where
  numParams: Nat
  numIndices: Nat
  all: Array Name
  ctors: Array Name
  isRec:       Bool := false
  isReflexive: Bool := false
  isNested:    Bool := false
  deriving ToJson
-- See `ConstructorVal`
structure ConstructorInfo where
  induct: Name
  cidx: Nat
  numParams: Nat
  numFields: Nat
  deriving ToJson

/-- See `Lean/Declaration.lean` -/
structure RecursorRule where
  ctor: Name
  nFields: Nat
  rhs: Expression
  deriving ToJson
structure RecursorInfo where
  all: Array Name
  numParams: Nat
  numIndices: Nat
  numMotives: Nat
  numMinors: Nat
  rules: Array RecursorRule
  k: Bool
  deriving ToJson
structure EnvInspectResult where
  type: Expression
  isUnsafe: Bool            := false
  value?: Option Expression := .none
  module?: Option Name      := .none
  -- If the name is private, displays the public facing name
  publicName?: Option Name  := .none
  typeDependency?: Option (Array Name) := .none
  valueDependency?: Option (Array Name) := .none
  inductInfo?:      Option InductInfo      := .none
  constructorInfo?: Option ConstructorInfo := .none
  recursorInfo?:    Option RecursorInfo    := .none

  -- Location in source
  sourceUri?: Option String := .none
  sourceStart?: Option Position := .none
  sourceEnd?: Option Position := .none
  deriving ToJson

structure EnvAdd where
  name: Name
  levels?: Option (Array Name) := .none
  type?: Option String := .none
  value: String
  isTheorem: Bool := false
  deriving FromJson
structure EnvAddResult where
  deriving ToJson

structure EnvSaveLoad where
  path: System.FilePath
  deriving FromJson
structure EnvSaveLoadResult where
  deriving ToJson

structure EnvParse where
  input : String
  category : Name
  deriving FromJson
structure EnvParseResult where
  -- Byte boundary for the first syntax element
  pos : Nat
  deriving ToJson

structure GoalStart where
  -- Only one of the fields below may be populated.
  expr: Option String     -- Directly parse in an expression
  -- universe levels
  levels?: Option (Array Name) := .none
  copyFrom: Option Name := .none -- Copy the type from a theorem in the environment
  deriving FromJson
structure GoalStartResult where
  stateId: Nat := 0
  -- Name of the root metavariable
  root: Name
  deriving ToJson
structure GoalTactic where
  stateId: Nat
  -- If omitted, act on the first goal
  goalId?: Option Nat := .none
  -- If set to true, goal will not go dormant. Defaults to `automaticMode`
  autoResume?: Option Bool := .none
  -- One of the fields here must be filled
  tactic?: Option String := .none
  -- Changes the current category to {"tactic", "calc", "conv"}
  mode?: Option String := .none
  -- Assigns an expression to the current goal
  expr?: Option String := .none
  have?: Option String := .none
  let?: Option String := .none
  draft?: Option String := .none

  -- In case of the `have` and `let` tactics, the new free variable name is
  -- provided here
  binderName?: Option Name := .none

  deriving FromJson
structure GoalTacticResult where
  -- The next goal state id. Existence of this field shows success
  nextStateId?: Option Nat          := .none
  -- If the array is empty, it shows the goals have been fully resolved. If this
  -- is .none, there has been a tactic error.
  goals?: Option (Array Goal)       := .none

  messages? : Option (Array Lean.SerialMessage) := .some #[]

  -- Existence of this field shows the tactic parsing has failed
  parseError? : Option String       := .none

  hasSorry : Bool := false
  hasUnsafe : Bool := false
  deriving ToJson
structure GoalContinue where
  -- State from which the continuation acquires the context
  target: Nat

  -- One of the following must be supplied
  -- The state which is an ancestor of `target` where goals will be extracted from
  branch?: Option Nat := .none
  -- Or, the particular goals that should be brought back into scope
  goals?: Option (Array Name) := .none
  deriving FromJson
structure GoalContinueResult where
  nextStateId: Nat
  goals: (Array Goal)
  deriving ToJson

structure GoalSubsume where
  stateId : Nat
  goal : Name
  srcStateId? : Option Nat := .none
  candidates : Array Name
  deriving FromJson
deriving instance ToJson for Subsumption
/-- To reconstruct the state, remove `goal` from the `stateId` in the input -/
structure GoalSubsumeResult where
  result : Subsumption
  stateId? : Option Nat := .none
  subsumptor? : Option Name := .none
  deriving ToJson

-- Remove goal states
structure GoalDelete where
  -- This is ok being a List because it doesn't show up in the ABI
  stateIds: List Nat
  deriving FromJson
structure GoalDeleteResult where
  deriving ToJson

structure GoalPrint where
  stateId: Nat

  -- Print root?
  rootExpr?: Option Bool := .some False
  -- Print the parent expressions
  parentExprs?: Option Bool := .some False
  -- Print goals?
  goals?: Option Bool := .some False
  -- Print values of extra mvars?
  extraMVars?: Option (Array Name) := .none
  deriving FromJson
structure GoalPrintResult where
  -- The root expression
  root?: Option Expression := .none
  -- The filling expression of the parent goal
  parentExprs?: Option (List (Option Expression)) := .none
  goals: Array Goal := #[]
  extraMVars: Array Expression := #[]

  rootHasSorry : Bool := false
  rootHasUnsafe : Bool := false
  rootHasMVar : Bool := true
  deriving ToJson

-- Diagnostic Options, not available in REPL
structure GoalDiag where
  printContext: Bool := true
  printValue: Bool := true
  printNewMVars: Bool := false
  -- Print all mvars
  printAll: Bool := false
  instantiate: Bool := true
  printSexp: Bool := false

structure GoalSave where
  id: Nat
  path: System.FilePath
  deriving FromJson
structure GoalSaveResult where
  deriving ToJson
structure GoalLoad where
  path: System.FilePath
  deriving FromJson
structure GoalLoadResult where
  id: Nat
  deriving ToJson

/-- Executes the Lean compiler on a single file -/
structure FrontendProcess where
  -- At least one of these two must be supplied
  fileName?: Option String := .none
  file?: Option String := .none
  -- Whether to read the header
  readHeader : Bool := false
  -- Alter the REPL environment after the compilation units.
  inheritEnv : Bool := false
  -- collect tactic invocations and output to a given file
  invocations?: Option String := .none
  -- list new constants from each compilation step
  newConstants: Bool := false
  deriving FromJson
structure InvokedTactic where
  goalBefore: String
  goalAfter: String
  tactic: String

  -- List of used constants
  usedConstants: Array Name
  deriving ToJson

structure CompilationUnit where
  -- String boundaries of compilation units
  boundary: (Nat × Nat)
  messages: Array Lean.SerialMessage := #[]
  -- Number of tactic invocations
  nInvocations?: Option Nat := .none

  -- New constants defined in compilation unit
  newConstants?: Option (Array Name) := .none
  deriving ToJson
structure FrontendProcessResult where
  units: List CompilationUnit
  deriving ToJson

/-- Frontend Process's side output going into a file -/
structure FrontendDataUnit where
  invocations? : Option (List Protocol.InvokedTactic) := .none
  deriving ToJson
structure FrontendData where
  units : List FrontendDataUnit
  deriving ToJson

structure FrontendDistil where
  file : String
  /-- If true, override default binder name which is generated from definition
  names -/
  binderName? : Option Name := .none
  /-- If set to true, the values of search targets are discarded. Otherwise they
  will be incorporated into the generated goal state. -/
  ignoreValues : Bool := true
  deriving FromJson
structure FrontendDistilSearchTarget where
  stateId : Nat
  goals : Array Goal
  deriving ToJson
structure FrontendDistilResult where
  targets : List FrontendDistilSearchTarget
  deriving ToJson

structure FrontendTrack where
  src : String
  dst : String
  deriving FromJson
structure FrontendTrackResult where
  failure? : Option String := .none
  srcMessages : Array Lean.SerialMessage := #[]
  dstMessages : Array Lean.SerialMessage := #[]
  deriving ToJson

structure FrontendRefactor where
  file : String
  coreOptions : Array String
  deriving FromJson
structure FrontendRefactorResult where
  file : String
  deriving ToJson

abbrev FallibleT := ExceptT InteractionError

abbrev throw {m : Type v → Type w} [MonadExceptOf InteractionError m] {α : Type v} (e : InteractionError) : m α :=
  throwThe InteractionError e