Add documentation; Remove mathlib dependency

Clean up README

.gitignore

@@ -1,2 +1,5 @@
+.*
+!.gitignore
+
 /build
 /lake-packages

Main.lean

@@ -1,4 +1,244 @@
-import Pantograph
+import Lean.Data.Json
+import Lean.Environment
 
-def main : IO Unit :=
+import Pantograph.Commands
-  IO.println s!"Hello, {hello}!"
+import Pantograph.Serial
+import Pantograph.Meta
+import Pantograph.Symbols
+
+namespace Pantograph
+
+
+structure Context where
+
+/-- Stores state of the REPL -/
+structure State where
+  --environments: Array Lean.Environment := #[]
+  proofTrees:   Array ProofTree := #[]
+
+-- State monad
+abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM)
+
+open Commands
+
+/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
+def parse_command (s: String): Except String Command := do
+  let s := s.trim
+  match s.get? 0 with
+  | .some '{' => -- Parse in Json mode
+    Lean.fromJson? (← Lean.Json.parse s)
+  | .some _ => -- Parse in line mode
+    let offset := s.posOf ' ' |> s.offsetOfPos
+    if offset = s.length then
+      return { cmd := s.take offset, payload := Lean.Json.null }
+    else
+      let payload ← s.drop offset |> Lean.Json.parse
+      return { cmd := s.take offset, payload := payload }
+  | .none => throw "Command is empty"
+
+def execute (command: Command): Subroutine Lean.Json := do
+  match command.cmd with
+  | "catalog" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => catalog args
+    | .error x => return errorJson x
+  | "inspect" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => inspect args
+    | .error x => return errorJson x
+  | "clear" => clear
+  | "expr.type" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => expr_type args
+    | .error x => return errorJson x
+  | "proof.start" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => proof_start args
+    | .error x => return errorJson x
+  | "proof.tactic" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => proof_tactic args
+    | .error x => return errorJson x
+  | "proof.printTree" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => proof_print_tree args
+    | .error x => return errorJson x
+  | cmd =>
+    let error: InteractionError := { error := "unknown", desc := s!"Unknown command {cmd}" }
+      return Lean.toJson error
+  where
+  errorI (type desc: String) := Lean.toJson ({ error := type, desc := desc }: InteractionError)
+  errorJson := errorI "json"
+  errorIndex := errorI "index"
+  catalog (_: Catalog): Subroutine Lean.Json := do
+    let env ← Lean.MonadEnv.getEnv
+    let names := env.constants.fold (init := #[]) (λ acc name info =>
+      match to_filtered_symbol name info with
+      | .some x => acc.push x
+      | .none => acc)
+    return Lean.toJson <| ({ symbols := names }: CatalogResult)
+  inspect (args: Inspect): Subroutine Lean.Json := do
+    let env ← Lean.MonadEnv.getEnv
+    let name := str_to_name args.name
+    let info? := env.find? name
+    match info? with
+    | none => return  errorIndex s!"Symbol not found {args.name}"
+    | some info =>
+      let format ← Lean.Meta.ppExpr info.toConstantVal.type
+      let module? := env.getModuleIdxFor? name >>=
+        (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+      let boundExpr? ← (match info.toConstantVal.type with
+        | .forallE _ _ _ _ => return .some (← type_expr_to_bound info.toConstantVal.type)
+        | _ => return Option.none)
+      return Lean.toJson ({
+        type := toString format,
+        boundExpr? := boundExpr?,
+        module? := module?
+      }: InspectResult)
+  clear : Subroutine Lean.Json := do
+    let state ← get
+    let nTrees := state.proofTrees.size
+    set { state with proofTrees := #[] }
+    return Lean.toJson ({ nTrees := nTrees }: ClearResult)
+  expr_type (args: ExprType): Subroutine Lean.Json := do
+    let env ← Lean.MonadEnv.getEnv
+    match syntax_from_str env args.expr with
+    | .error str => return errorI "parsing" str
+    | .ok syn => do
+      match (← syntax_to_expr syn) with
+      | .error str => return errorI "elab" str
+      | .ok expr => do
+        try
+          let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr)
+          return Lean.toJson <| ({
+              type := toString format,
+              roundTrip := toString <| (← Lean.Meta.ppExpr expr)
+          }: ExprTypeResult)
+        catch exception =>
+          return errorI "typing" (← exception.toMessageData.toString)
+  proof_start (args: ProofStart): Subroutine Lean.Json := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with
+      | .some expr, .none =>
+        (match syntax_from_str env expr with
+        | .error str => return .error <| errorI "parsing" str
+        | .ok syn => do
+          (match (← syntax_to_expr syn) with
+          | .error str => return .error <| errorI "elab" str
+          | .ok expr => return .ok expr))
+      | .none, .some copyFrom =>
+        (match env.find? <| str_to_name copyFrom with
+        | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
+        | .some cInfo => return .ok cInfo.type)
+      | .none, .none =>
+        return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
+      | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
+    match expr? with
+    | .error error => return error
+    | .ok expr =>
+      let tree ← ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
+      -- Put the new tree in the environment
+      let nextTreeId := state.proofTrees.size
+      set { state with proofTrees := state.proofTrees.push tree }
+      return Lean.toJson ({ treeId := nextTreeId }: ProofStartResult)
+  proof_tactic (args: ProofTactic): Subroutine Lean.Json := do
+    let state ← get
+    match state.proofTrees.get? args.treeId with
+    | .none => return errorIndex "Invalid tree index {args.treeId}"
+    | .some tree =>
+      let (result, nextTree) ← ProofTree.execute
+        (stateId := args.stateId)
+        (goalId := args.goalId.getD 0)
+        (tactic := args.tactic) |>.run tree
+      match result with
+      | .invalid message => return Lean.toJson <| errorIndex message
+      | .success nextId? goals =>
+        set { state with proofTrees := state.proofTrees.set! args.treeId nextTree }
+        return Lean.toJson ({ nextId? := nextId?, goals := goals }: ProofTacticResultSuccess)
+      | .failure messages =>
+        return Lean.toJson ({ tacticErrors := messages }: ProofTacticResultFailure)
+  proof_print_tree (args: ProofPrintTree): Subroutine Lean.Json := do
+    let state ← get
+    match state.proofTrees.get? args.treeId with
+    | .none => return errorIndex "Invalid tree index {args.treeId}"
+    | .some tree =>
+      return Lean.toJson ({parents := tree.structure_array}: ProofPrintTreeResult)
+
+
+end Pantograph
+
+
+-- Main IO functions
+open Pantograph
+
+unsafe def loop : Subroutine Unit := do
+  let command ← (← IO.getStdin).getLine
+  if command.trim.length = 0 then return ()
+  match parse_command command with
+  | .error error =>
+    let error  := Lean.toJson ({ error := "json", desc := error }: Commands.InteractionError)
+    IO.println (toString error)
+  | .ok command =>
+    let ret ← execute command
+    IO.println <| toString <| ret
+  loop
+
+namespace Lean
+-- This is better than the default version since it handles `.`
+def setOptionFromString' (opts : Options) (entry : String) : IO Options := do
+  let ps := (entry.splitOn "=").map String.trim
+  let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
+  let key := str_to_name key
+  let defValue ← getOptionDefaultValue key
+  match defValue with
+  | DataValue.ofString _ => pure $ opts.setString key val
+  | DataValue.ofBool _   =>
+    match val with
+    | "true" => pure $ opts.setBool key true
+    | "false" => pure $ opts.setBool key false
+    | _ => throw $ IO.userError s!"invalid Bool option value '{val}'"
+  | DataValue.ofName _   => pure $ opts.setName key val.toName
+  | DataValue.ofNat _    =>
+    match val.toNat? with
+    | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
+    | some v => pure $ opts.setNat key v
+  | DataValue.ofInt _    =>
+    match val.toInt? with
+    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
+    | some v => pure $ opts.setInt key v
+  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")
+end Lean
+
+unsafe def main (args: List String): IO Unit := do
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot)
+
+  -- Separate imports and options
+  let options := args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+  let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
+
+  let env ← Lean.importModules
+    (imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  let context: Context := {
+  }
+  let coreContext: Lean.Core.Context := {
+    currNamespace := str_to_name "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] },
+    options := ← options.foldlM Lean.setOptionFromString' Lean.Options.empty
+  }
+  try
+    let termElabM := loop.run context |>.run' {}
+    let metaM := termElabM.run' (ctx := {
+      declName? := some "_pantograph",
+      errToSorry := false
+    })
+    let coreM := metaM.run'
+    discard <| coreM.toIO coreContext { env := env }
+  catch ex =>
+    IO.println "Uncaught IO exception"
+    IO.println ex.toString

Pantograph.lean

@@ -1 +1,2 @@
-def hello := "world"
+import Pantograph.Commands
+import Pantograph.Symbols

Pantograph/Commands.lean

@@ -0,0 +1,91 @@
+/-
+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 Lean.Data.Json
+
+import Pantograph.Serial
+
+namespace Pantograph.Commands
+
+structure Command where
+  cmd: String
+  payload: Lean.Json
+  deriving Lean.FromJson
+
+structure InteractionError where
+  error: String
+  desc: String
+  deriving Lean.ToJson
+
+
+-- Individual command and return types
+
+
+-- Print all symbols in environment
+structure Catalog where
+  deriving Lean.FromJson
+structure CatalogResult where
+  symbols: Array String
+  deriving Lean.ToJson
+
+-- Print the type of a symbol
+structure Inspect where
+  name: String
+  deriving Lean.FromJson
+structure InspectResult where
+  type: String
+  -- Decompose the bound expression when the type is forall.
+  boundExpr?: Option BoundExpression
+  module?: Option String
+  deriving Lean.ToJson
+
+structure ClearResult where
+  nTrees: Nat
+  deriving Lean.ToJson
+
+-- Get the type of an expression
+structure ExprType where
+  expr: String
+  deriving Lean.FromJson
+structure ExprTypeResult where
+  type: String
+  roundTrip: String
+  deriving Lean.ToJson
+
+structure ProofStart where
+  name: Option String     -- Identifier of the proof
+  -- Only one of the fields below may be populated.
+  expr: Option String     -- Proof expression
+  copyFrom: Option String -- Theorem name
+  deriving Lean.FromJson
+structure ProofStartResult where
+  treeId: Nat := 0 -- Proof tree id
+  deriving Lean.ToJson
+
+structure ProofTactic where
+  -- Identifiers for tree, state, and goal
+  treeId: Nat
+  stateId: Nat
+  goalId: Option Nat
+  tactic: String
+  deriving Lean.FromJson
+structure ProofTacticResultSuccess where
+  goals: Array Goal
+  nextId?: Option Nat -- Next proof state id
+  deriving Lean.ToJson
+structure ProofTacticResultFailure where
+  tacticErrors: Array String -- Error messages generated by tactic
+  deriving Lean.ToJson
+
+structure ProofPrintTree where
+  treeId: Nat
+  deriving Lean.FromJson
+structure ProofPrintTreeResult where
+  -- "" if no parents, otherwise "parentId.goalId"
+  parents: Array String
+  deriving Lean.ToJson
+
+end Pantograph.Commands

Pantograph/Meta.lean

@@ -0,0 +1,120 @@
+import Lean
+
+import Pantograph.Symbols
+import Pantograph.Serial
+
+/-
+The proof state manipulation system
+
+A proof state is launched by providing
+1. Environment: `Environment`
+2. Expression: `Expr`
+The expression becomes the first meta variable in the saved tactic state
+`Elab.Tactic.SavedState`.
+From this point on, any proof which extends
+`Elab.Term.Context` and
+-/
+
+def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
+{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false }
+
+
+namespace Pantograph
+open Lean
+
+structure ProofState where
+  goals : List MVarId
+  savedState : Elab.Tactic.SavedState
+  parent : Option Nat := none
+  parentGoalId : Nat  := 0
+structure ProofTree where
+  -- All parameters needed to run a `TermElabM` monad
+  name: Name
+
+  -- Set of proof states
+  states : Array ProofState := #[]
+
+abbrev M := Elab.TermElabM
+
+def ProofTree.create (name: Name) (expr: Expr): M ProofTree := do
+  let expr ← instantiateMVars expr
+  let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
+  let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
+  let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
+  return {
+    name := name,
+    states := #[{
+      savedState := savedState,
+      goals := [goal.mvarId!]
+    }]
+  }
+
+-- Print the tree structures in readable form
+def ProofTree.structure_array (tree: ProofTree): Array String :=
+  tree.states.map λ state => match state.parent with
+    | .none => ""
+    | .some parent => s!"{parent}.{state.parentGoalId}"
+
+def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) :
+    M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
+  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
+    state.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      Elab.Tactic.evalTactic stx
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .error errors
+      else
+        return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
+    catch exception =>
+      return .error #[← exception.toMessageData.toString]
+  match Parser.runParserCategory
+    (env := ← MonadEnv.getEnv)
+    (catName := `tactic)
+    (input := tactic)
+    (fileName := "<stdin>") with
+  | Except.error err => return .error #[err]
+  | Except.ok stx    => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
+
+/-- Response for executing a tactic -/
+inductive TacticResult where
+  -- Invalid id
+  | invalid (message: String): TacticResult
+  -- Goes to next state
+  | success (nextId?: Option Nat) (goals: Array Goal)
+  -- Fails with messages
+  | failure (messages: Array String)
+
+/-- Execute tactic on given state -/
+def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT ProofTree M TacticResult := do
+  let tree ← get
+  match tree.states.get? stateId with
+  | .none => return .invalid s!"Invalid state id {stateId}"
+  | .some state =>
+    match state.goals.get? goalId with
+    | .none => return .invalid s!"Invalid goal id {goalId}"
+    | .some goal =>
+      match (← execute_tactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
+      | .error errors =>
+        return .failure errors
+      | .ok (nextState, nextGoals) =>
+        let nextId := tree.states.size
+        if nextGoals.isEmpty then
+          return .success .none #[]
+        else
+          let proofState: ProofState := {
+            savedState := nextState,
+            goals := nextGoals,
+            parent := stateId,
+            parentGoalId := goalId
+          }
+          modify fun s => { s with states := s.states.push proofState }
+        let goals ← nextGoals.mapM fun mvarId => do
+          match (← MonadMCtx.getMCtx).findDecl? mvarId with
+          | .some mvarDecl => serialize_goal mvarDecl
+          | .none => throwError mvarId
+        return .success (.some nextId) goals.toArray
+
+end Pantograph

Pantograph/Serial.lean

@@ -0,0 +1,120 @@
+/-
+All serialisation functions
+-/
+import Lean
+
+namespace Pantograph
+open Lean
+
+
+/-- Read a theorem from the environment -/
+def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
+  match env.find? name with
+  | none       => throw s!"Symbol not found: {name}"
+  | some cInfo => return cInfo.type
+def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
+  Parser.runParserCategory
+    (env := env)
+    (catName := `term)
+    (input := s)
+    (fileName := "<stdin>")
+
+
+def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabType syn
+    -- Immediately synthesise all metavariables if we need to leave the elaboration context.
+    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
+    --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let expr ← instantiateMVars expr
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
+  try
+    let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
+    -- Immediately synthesise all metavariables if we need to leave the elaboration context.
+    -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
+    --Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let expr ← instantiateMVars expr
+    return .ok expr
+  catch ex => return .error (← ex.toMessageData.toString)
+
+structure BoundExpression where
+  binders: Array (String × String)
+  target: String
+  deriving ToJson
+def type_expr_to_bound (expr: Expr): MetaM BoundExpression := do
+  Meta.forallTelescope expr fun arr body => do
+    let binders ← arr.mapM fun fvar => do
+      return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
+    return { binders, target := toString (← Meta.ppExpr body) }
+
+
+structure Variable where
+  name: String
+  /-- Does the name contain a dagger -/
+  isInaccessible: Bool      := false
+  type: String
+  value?: Option String     := .none
+  deriving ToJson
+structure Goal where
+  /-- String case id -/
+  caseName?: Option String  := .none
+  /-- Is the goal in conversion mode -/
+  isConversion: Bool        := false
+  /-- target expression type -/
+  target: String
+  /-- Variables -/
+  vars: Array Variable      := #[]
+  deriving ToJson
+
+/-- Adapted from ppGoal -/
+def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do
+  -- Options for printing; See Meta.ppGoal for details
+  let showLetValues  := True
+  let ppAuxDecls     := false
+  let ppImplDetailHyps := false
+  let lctx           := mvarDecl.lctx
+  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let rec ppVars (localDecl : LocalDecl) : MetaM Variable := do
+      match localDecl with
+      | .cdecl _ _ varName type _ _ =>
+        let varName := varName.simpMacroScopes
+        let type ← instantiateMVars type
+        return {
+          name := toString varName,
+          isInaccessible := varName.isInaccessibleUserName,
+          type := toString <| ← Meta.ppExpr type
+        }
+      | .ldecl _ _ varName type val _ _ => do
+        let varName := varName.simpMacroScopes
+        let type ← instantiateMVars type
+        let value? ← if showLetValues then
+          let val ← instantiateMVars val
+          pure $ .some <| toString <| (← Meta.ppExpr val)
+        else
+          pure $ .none
+        return {
+          name := toString varName,
+          isInaccessible := varName.isInaccessibleUserName,
+          type := toString <| ← Meta.ppExpr type
+          value? := value?
+        }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+       let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail
+       if skip then
+         return acc
+       else
+         let var ← ppVars localDecl
+         return var::acc
+    return {
+      caseName? := match mvarDecl.userName with
+        | Name.anonymous => .none
+        | name => .some <| toString name,
+      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
+      target := toString <| (← Meta.ppExpr (← instantiateMVars mvarDecl.type)),
+      vars := vars.reverse.toArray
+    }
+
+end Pantograph

Pantograph/Symbols.lean

@@ -0,0 +1,38 @@
+/-
+ - Manages the visibility status of symbols
+ -/
+import Lean.Declaration
+
+namespace Pantograph
+
+def str_to_name (s: String): Lean.Name :=
+  (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
+
+def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
+  let nameDeduce: Bool := match n.getRoot with
+  | .str _ name => name.startsWith "_" ∨ name == "Lean"
+  | _ => true
+  let stemDeduce: Bool := match n with
+  | .anonymous => true
+  | .str _ name => name.startsWith "_"
+  | .num _ _ => true
+  nameDeduce ∨ stemDeduce ∨ info.isUnsafe
+
+def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+  let pref := match info with
+  | .axiomInfo  _ => "axiom"
+  | .defnInfo   _ => "defn"
+  | .thmInfo    _ => "thm"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo   _ => "quot"
+  | .inductInfo _ => "induct"
+  | .ctorInfo   _ => "ctor"
+  | .recInfo    _ => "rec"
+  s!"{pref}|{toString n}"
+
+def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
+  if is_symbol_unsafe_or_internal n info
+  then Option.none
+  else Option.some <| to_compact_symbol_name n info
+
+end Pantograph

README.md

@@ -0,0 +1,89 @@
+# Pantograph
+
+An interaction system for Lean 4.
+
+![Pantograph](doc/icon.svg)
+
+## Installation
+
+Install `elan` and `lean4`. Then, execute
+``` sh
+lake build
+```
+Then, setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
+``` sh
+LIB="../lib"
+LIB_MATHLIB="$LIB/mathlib4/lake-packages"
+export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
+
+LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
+```
+Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantograph! This is because Pantograph taps into Lean's internals.
+
+## Usage
+
+``` sh
+build/bin/pantograph OPTIONS|MODULES
+```
+
+The REPL loop accepts commands as single-line JSON inputs and outputs either an
+`Error:` (indicating malformed command) or a json return value indicating the
+result of a command execution.  The command can be passed in one of two formats
+```
+command { ... }
+{ "cmd": command, "payload": ... }
+```
+The list of available commands can be found in `Pantograph/Commands.lean`. An
+empty command aborts the REPL.
+
+The `Pantograph` executable must be run with a list of modules to import. It can
+also accept options of the form `--key=value` e.g. `--pp.raw=true`.
+
+Example: (~5k symbols)
+```
+$ build/bin/Pantograph Init
+catalog
+inspect {"name": "Nat.le_add_left"}
+```
+Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
+```
+$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
+catalog
+```
+Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
+```
+$ env build/bin/Pantograph Init
+proof.start {"expr": "∀ (n m : Nat), n + m = m + n"}
+proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"}
+proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}
+proof.printTree {"treeId": 0}
+proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
+proof.printTree {"treeId": 0}
+```
+where the application of `assumption` should lead to a failure.
+
+## Commands
+
+See `Pantograph/Commands.lean` for a description of the parameters and return values in Json.
+- `catalog`: Display a list of all safe Lean symbols in the current context
+- `inspect {"name": <name>}`: Show the type and package of a given symbol
+- `clear`: Delete all cached expressions and proof trees
+- `expr.type {"expr": <expr>}`: Determine the type of an expression and round-trip it
+- `proof.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new proof state from a given expression or symbol
+- `proof.tactic {"treeId": <id>, "stateId": <id>, "goalId": <id>, "tactic": string}`: Execute a tactic on a given proof state
+- `proof.printTree {"treeId": <id>}`: Print the topological structure of a proof tree
+
+## Troubleshooting
+
+If lean encounters stack overflow problems when printing catalog, execute this before running lean:
+```sh
+ulimit -s unlimited
+```
+
+## Testing
+
+The tests are based on `LSpec`. To run tests,
+``` sh
+test/all.sh
+```
+

Test/Main.lean

@@ -0,0 +1,17 @@
+import LSpec
+import Pantograph.Symbols
+import Test.Proofs
+import Test.Serial
+
+open Pantograph.Test
+
+unsafe def main := do
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot)
+
+  let suites := [
+    test_serial,
+    test_proofs
+  ]
+  let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
+  LSpec.lspecIO $ all

Test/Proofs.lean

@@ -0,0 +1,196 @@
+import LSpec
+import Pantograph.Meta
+import Pantograph.Serial
+
+namespace Pantograph.Test
+open Pantograph
+open Lean
+
+inductive Start where
+  | copy (name: String) -- Start from some name in the environment
+  | expr (expr: String) -- Start from some expression
+
+abbrev TestM := StateRefT ProofTree M
+
+def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
+  let env ← Lean.MonadEnv.getEnv
+  let mut testSeq := LSpec.TestSeq.done
+  match start with
+  | .copy name =>
+    let cInfo? := str_to_name name |> env.find?
+    testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
+    match cInfo? with
+    | .some cInfo =>
+      let state ← ProofTree.create
+        (name := str_to_name "TestExample")
+        (expr := cInfo.type)
+      return (testSeq, Option.some state)
+    | .none =>
+      return (testSeq, Option.none)
+  | .expr expr =>
+    let syn? := syntax_from_str env expr
+    testSeq := testSeq ++ LSpec.check s!"Parsing {expr}" (syn?.isOk)
+    match syn? with
+    | .error error =>
+      IO.println error
+      return (testSeq, Option.none)
+    | .ok syn =>
+      let expr? ← syntax_to_expr syn
+      testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk
+      match expr? with
+      | .error error =>
+        IO.println error
+        return (testSeq, Option.none)
+      | .ok expr =>
+        let state ← ProofTree.create
+          (name := str_to_name "TestExample")
+          (expr := expr)
+        return (testSeq, Option.some state)
+
+deriving instance DecidableEq, Repr for Variable
+deriving instance DecidableEq, Repr for Goal
+deriving instance DecidableEq, Repr for TacticResult
+
+def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
+    (expected: TacticResult) : TestM LSpec.TestSeq := do
+  let result: TacticResult ← ProofTree.execute stateId goalId tactic
+  match expected, result with
+  | .success (.some i) #[], .success (.some _) goals =>
+    -- If the goals are omitted but the next state is specified, we imply that
+    -- the tactic succeeded.
+    let expected := .success (.some i) goals
+    return LSpec.test s!"{stateId}.{goalId} {tactic}"   (result = expected)
+  | _, _ =>
+    return LSpec.test s!"{stateId}.{goalId} {tactic}"   (result = expected)
+
+def proof_inspect (expected: Array String) : TestM LSpec.TestSeq := do
+  let result := (← get).structure_array
+  return LSpec.test s!"tree structure" (result = expected)
+
+def proof_runner (env: Lean.Environment) (start: Start) (steps: List (TestM LSpec.TestSeq)): IO LSpec.TestSeq := do
+  let termElabM := do
+    let (testSeq, state?) ← start_proof start
+    match state? with
+    | .none => return testSeq
+    | .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run' state
+
+  let coreContext: Lean.Core.Context := {
+    currNamespace := str_to_name "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
+  let coreM := metaM.run'
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok a            => return a
+
+def build_goal (nameType: List (String × String)) (target: String): Goal :=
+  {
+    target := target,
+    vars := (nameType.map fun x => ({ name := x.fst, type := x.snd }: Variable)).toArray
+  }
+
+example: ∀ (a b: Nat), a + b = b + a := by
+  intro n m
+  rw [Nat.add_comm]
+def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
+  let goal1: Goal := {
+    target := "n + m = m + n",
+    vars := #[{ name := "n", type := "Nat" }, { name := "m", type := "Nat" }]
+  }
+  proof_runner env (.copy "Nat.add_comm") [
+    proof_step 0 0 "intro n m"
+      (.success (.some 1) #[goal1]),
+    proof_step 1 0 "assumption"
+      (.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]),
+    proof_step 1 0 "rw [Nat.add_comm]"
+      (.success .none #[])
+  ]
+def proof_nat_add_comm_manual (env: Lean.Environment): IO LSpec.TestSeq := do
+  let goal1: Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
+  proof_runner env (.expr "∀ (a b: Nat), a + b = b + a") [
+    proof_step 0 0 "intro n m"
+      (.success (.some 1) #[goal1]),
+    proof_step 1 0 "assumption"
+      (.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]),
+    proof_step 1 0 "rw [Nat.add_comm]"
+      (.success .none #[])
+  ]
+
+-- Two ways to write the same theorem
+example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
+  intro p q h
+  cases h
+  apply Or.inr
+  assumption
+  apply Or.inl
+  assumption
+example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
+  intro p q h
+  cases h
+  . apply Or.inr
+    assumption
+  . apply Or.inl
+    assumption
+def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
+  let branchGoal (caseName name: String): Goal := {
+    caseName? := .some caseName,
+    target := "q ∨ p",
+    vars := #[
+      { name := "p", type := "Prop" },
+      { name := "q", type := "Prop" },
+      { name := "h✝", type := name, isInaccessible := true }
+    ]
+  }
+  proof_runner env (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [
+    proof_step 0 0 "intro p q h"
+      (.success (.some 1) #[build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]),
+    proof_step 1 0 "cases h"
+      (.success (.some 2) #[branchGoal "inl" "p", branchGoal "inr" "q"]),
+    proof_inspect #["", "0.0", "1.0"],
+    proof_step 2 0 "apply Or.inr"
+      (.success (.some 3) #[]),
+    proof_inspect #["", "0.0", "1.0", "2.0"],
+    proof_step 3 0 "assumption"
+      (.success .none #[]),
+    proof_step 2 1 "apply Or.inl"
+      (.success (.some 4) #[]),
+    proof_step 4 0 "assumption"
+      (.success .none #[]),
+    proof_inspect #["", "0.0", "1.0", "2.0", "2.1"]
+  ]
+
+example (w x y z : Nat) (p : Nat → Prop)
+        (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
+  simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
+  assumption
+def proof_arith_1 (env: Lean.Environment): IO LSpec.TestSeq := do
+  proof_runner env (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") [
+    proof_step 0 0 "intros"
+      (.success (.some 1) #[]),
+    proof_step 1 0 "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *"
+      (.success (.some 2) #[]),
+    proof_step 2 0 "assumption"
+      (.success .none #[])
+  ]
+
+def test_proofs : IO LSpec.TestSeq := do
+  let env: Lean.Environment ← Lean.importModules
+    (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+
+  return LSpec.group "Proofs" $
+    (LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm env)) ++
+    (LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual env)) ++
+    (LSpec.group "Or.comm" $ (← proof_or_comm env)) ++
+    (LSpec.group "Arithmetic 1" $ (← proof_arith_1 env))
+
+end Pantograph.Test
+

Test/Serial.lean

@@ -0,0 +1,43 @@
+import LSpec
+import Pantograph.Serial
+import Pantograph.Symbols
+
+namespace Pantograph.Test
+
+open Pantograph
+open Lean
+
+deriving instance Repr, DecidableEq for BoundExpression
+
+def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
+  let cases: List (String × BoundExpression) := [
+    ("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
+    ("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
+  ]
+  let coreM := cases.foldlM (λ suites (symbol, target) => do
+    let env ← MonadEnv.getEnv
+    let expr := str_to_name symbol |> env.find? |>.get! |>.type
+    let test := LSpec.check symbol ((← type_expr_to_bound expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+  let coreContext: Core.Context := {
+    currNamespace := str_to_name "Aniva",
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok a            => return a
+
+def test_serial: IO LSpec.TestSeq := do
+  let env: Environment ← importModules
+    (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+
+  return LSpec.group "Serialisation" $
+    (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
+    LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
+
+end Pantograph.Test

Test/all.sh

@@ -0,0 +1,3 @@
+#!/bin/bash
+
+lake build test && lake env build/bin/test

doc/icon.svg

@@ -0,0 +1,73 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- Created with Inkscape (http://www.inkscape.org/) -->
+
+<svg
+   width="256"
+   height="256"
+   viewBox="0 0 55.900957 55.900957"
+   version="1.1"
+   id="svg21534"
+   xml:space="preserve"
+   inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
+   sodipodi:docname="icon.svg"
+   xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+   xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+   xmlns="http://www.w3.org/2000/svg"
+   xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
+     id="namedview21536"
+     pagecolor="#ffffff"
+     bordercolor="#111111"
+     borderopacity="1"
+     inkscape:showpageshadow="0"
+     inkscape:pageopacity="0"
+     inkscape:pagecheckerboard="1"
+     inkscape:deskcolor="#d1d1d1"
+     inkscape:document-units="px"
+     showgrid="true"
+     inkscape:zoom="5.1754899"
+     inkscape:cx="158.82554"
+     inkscape:cy="91.682142"
+     inkscape:window-width="3777"
+     inkscape:window-height="2093"
+     inkscape:window-x="0"
+     inkscape:window-y="0"
+     inkscape:window-maximized="1"
+     inkscape:current-layer="layer1"><inkscape:grid
+       type="xygrid"
+       id="grid23833"
+       spacingx="3.4938098"
+       spacingy="3.4938098"
+       empspacing="4" /></sodipodi:namedview><defs
+     id="defs21531" /><g
+     inkscape:label="Layer 1"
+     inkscape:groupmode="layer"
+     id="layer1"><rect
+       style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:1.78013;stroke-miterlimit:3.4;stroke-dasharray:none"
+       id="rect26805"
+       width="11.502316"
+       height="2.2512667"
+       x="33.344425"
+       y="7.6690259"
+       ry="0.28140834"
+       rx="0.47926313" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="m 35.764667,9.9513013 c 0,0 -26.8581417,13.7987337 -28.0863506,14.9501437 -1.250042,1.171878 3.2347846,3.945325 3.2347846,3.945325 l 21.34979,14.934062 6.624567,0.453105 -27.599216,-17.304358 c 0,0 -0.603209,-0.08927 -0.600411,-0.762283 0.0028,-0.673015 27.32022,-16.4227356 27.32022,-16.4227356 z"
+       id="path27381"
+       sodipodi:nodetypes="csccccscc" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="M 10.97848,26.985751 40.537772,9.7943227 41.921795,9.7005084 11.210626,27.421377 Z"
+       id="path27479" /><path
+       style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
+       d="m 7.0509847,25.522367 c -0.8266141,1.386819 -2.4011783,4.48805 -2.4706357,4.90223 -0.069458,0.414182 0.4434324,0.513474 0.8491061,0.757041 C 5.835129,31.425204 19.33424,43.917182 19.33424,43.917182 l 0.324562,-0.539228 c 0,0 -14.2055729,-12.369493 -14.0644435,-12.868167 0.1411292,-0.498672 3.544896,-3.777392 3.544896,-3.777392 L 7.4596884,25.117508 Z"
+       id="path27481" /><rect
+       style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:2.11692;stroke-miterlimit:3.4;stroke-dasharray:none;stroke-opacity:1"
+       id="rect27483"
+       width="36.38942"
+       height="3.6217353"
+       x="13.953447"
+       y="43.009739"
+       rx="0.43672624"
+       ry="0.43672624" /><path
+       style="fill:none;stroke:#000000;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+       d="M -2.1119274,7.666599 H 64.179192"
+       id="path27487" /></g></svg>

lake-manifest.json

@@ -0,0 +1,33 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/lurk-lab/LSpec.git",
+    "subDir?": null,
+    "rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
+    "name": "LSpec",
+    "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "8e5a00a8afc8913c0584cb85f37951995275fd87",
+    "name": "mathlib",
+    "inputRev?": "8e5a00a8afc8913c0584cb85f37951995275fd87"}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
+    "name": "std",
+    "inputRev?": "main"}}]}

lakefile.lean

@@ -1,19 +1,24 @@
 import Lake
 open Lake DSL
 
-
+package pantograph
-package pantograph {
-  -- add package configuration options here
-}
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @  "8e5a00a8afc8913c0584cb85f37951995275fd87"
 
 lean_lib Pantograph {
-  -- add library configuration options here
 }
 
 @[default_target]
 lean_exe pantograph {
   root := `Main
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
+}
+
+require LSpec from git
+  "https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
+lean_lib Test {
+}
+lean_exe test {
+  root := `Test.Main
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
 }