Add compressed json print option; Rearrange commands into hierarchy

Main.lean

@@ -1,195 +1,37 @@
 import Lean.Data.Json
 import Lean.Environment
 
-import Pantograph.Commands
+import Pantograph.Version
-import Pantograph.Serial
+import Pantograph
-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
+unsafe def loop : MainM Unit := do
+  let state ← get
   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)
+    -- Using `Lean.Json.compress` here to prevent newline
+    IO.println error.compress
   | .ok command =>
     let ret ← execute command
-    IO.println <| toString <| ret
+    let str := match state.options.printJsonPretty with
+      | true => ret.pretty
+      | false => ret.compress
+    IO.println str
   loop
 
 namespace Lean
--- This is better than the default version since it handles `.`
+
-def setOptionFromString' (opts : Options) (entry : String) : IO Options := do
+/-- This is better than the default version since it handles `.` and doesn't
+ crash the program when it fails. -/
+def setOptionFromString' (opts : Options) (entry : String) : ExceptT 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, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := str_to_name key
+  let key := Pantograph.str_to_name key
   let defValue ← getOptionDefaultValue key
   match defValue with
   | DataValue.ofString _ => pure $ opts.setString key val
@@ -197,25 +39,37 @@ def setOptionFromString' (opts : Options) (entry : String) : IO Options := do
     match val with
     | "true" => pure $ opts.setBool key true
     | "false" => pure $ opts.setBool key false
-    | _ => throw $ IO.userError s!"invalid Bool option value '{val}'"
+    | _ => throw  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}'")
+    | none   => throw 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}'")
+    | none   => throw s!"invalid Int option value '{val}'"
     | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")
+  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
+
 end Lean
 
+
 unsafe def main (args: List String): IO Unit := do
+  -- NOTE: A more sophisticated scheme of command line argument handling is needed.
+  -- Separate imports and options
+  if args == ["--version"] then do
+    println! s!"{version}"
+    return
+
   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 options := args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
+    |>.foldlM Lean.setOptionFromString' Lean.Options.empty
+    |>.run
+  let options ← match options? with
+    | .ok options => pure options
+    | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
   let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
 
   let env ← Lean.importModules
@@ -223,13 +77,14 @@ unsafe def main (args: List String): IO Unit := do
     (opts := {})
     (trustLevel := 1)
   let context: Context := {
+    imports
   }
   let coreContext: Lean.Core.Context := {
-    currNamespace := str_to_name "Aniva",
+    currNamespace := Lean.Name.str .anonymous "Aniva"
     openDecls := [],     -- No 'open' directives needed
     fileName := "<Pantograph>",
     fileMap := { source := "", positions := #[0], lines := #[1] },
-    options := ← options.foldlM Lean.setOptionFromString' Lean.Options.empty
+    options := options
   }
   try
     let termElabM := loop.run context |>.run' {}

Pantograph.lean

@@ -1,2 +1,179 @@
 import Pantograph.Commands
+import Pantograph.Serial
 import Pantograph.Symbols
+import Pantograph.Tactic
+
+namespace Pantograph
+
+structure Context where
+  imports: List String
+
+/-- Stores state of the REPL -/
+structure State where
+  options: Commands.Options := {}
+  --environments: Array Lean.Environment := #[]
+  proofTrees:   Array ProofTree := #[]
+
+-- State monad
+abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
+-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
+-- monadic features in `MainM`
+abbrev CR α := Except Commands.InteractionError α
+
+/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
+def parse_command (s: String): Except String Commands.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: Commands.Command): MainM Lean.Json := do
+  let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
+    match Lean.fromJson? command.payload with
+    | .ok args => do
+      match (← comm args) with
+      | .ok result =>  return Lean.toJson result
+      | .error ierror => return Lean.toJson ierror
+    | .error error => pure $ error
+  match command.cmd with
+  | "reset"           => run reset
+  | "expr.echo"       => run expr_echo
+  | "lib.catalog"     => run lib_catalog
+  | "lib.inspect"     => run lib_inspect
+  | "options.set"     => run options_set
+  | "options.print"   => run options_print
+  | "proof.start"     => run proof_start
+  | "proof.tactic"    => run proof_tactic
+  | "proof.printTree" => run proof_print_tree
+  | cmd =>
+    let error: Commands.InteractionError :=
+      { error := "unknown", desc := s!"Unknown command {cmd}" }
+    return Lean.toJson error
+  where
+  errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
+  errorIndex := errorI "index"
+  -- Command Functions
+  reset (_: Commands.Reset): MainM (CR Commands.ResetResult) := do
+    let state ← get
+    let nTrees := state.proofTrees.size
+    set { state with proofTrees := #[] }
+    return .ok { nTrees := nTrees }
+  lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := 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 .ok { symbols := names }
+  lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    let name := str_to_name args.name
+    let info? := env.find? name
+    match info? with
+    | none => return .error $ errorIndex s!"Symbol not found {args.name}"
+    | some info =>
+      let module? := env.getModuleIdxFor? name >>=
+        (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
+      let value? := match args.value?, info with
+        | .some true, _ => info.value?
+        | .some false, _ => .none
+        | .none, .defnInfo _ => info.value?
+        | .none, _ => .none
+      return .ok {
+        type := ← serialize_expression state.options info.type,
+        value? := ← value?.mapM (λ v => serialize_expression state.options v),
+        module? := module?
+      }
+  expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    match syntax_from_str env args.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 => do
+        try
+          let type ← Lean.Meta.inferType expr
+          return .ok {
+              type := (← serialize_expression (options := state.options) type),
+              expr := (← serialize_expression (options := state.options) expr)
+          }
+        catch exception =>
+          return .error $ errorI "typing" (← exception.toMessageData.toString)
+  options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
+    let state ← get
+    let options := state.options
+    set { state with
+      options := {
+        -- FIXME: This should be replaced with something more elegant
+        printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
+        printExprPretty := args.printExprPretty?.getD options.printExprPretty,
+        printExprAST := args.printExprAST?.getD options.printExprAST,
+        proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
+        printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
+        printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
+      }
+    }
+    return .ok {  }
+  options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
+    return .ok (← get).options
+  proof_start (args: Commands.ProofStart): MainM (CR Commands.ProofStartResult) := do
+    let state ← get
+    let env ← Lean.MonadEnv.getEnv
+    let expr?: Except _ 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 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 .ok { treeId := nextTreeId }
+  proof_tactic (args: Commands.ProofTactic): MainM (CR Commands.ProofTacticResult) := do
+    let state ← get
+    match state.proofTrees.get? args.treeId with
+    | .none => return .error $ 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 state.options |>.run tree
+      match result with
+      | .invalid message => return .error $  errorIndex message
+      | .success nextId? goals =>
+        set { state with proofTrees := state.proofTrees.set! args.treeId nextTree }
+        return .ok { nextId? := nextId?, goals? := .some goals }
+      | .failure messages =>
+        return .ok { tacticErrors? := .some messages }
+  proof_print_tree (args: Commands.ProofPrintTree): MainM (CR Commands.ProofPrintTreeResult) := do
+    let state ← get
+    match state.proofTrees.get? args.treeId with
+    | .none => return .error $ errorIndex "Invalid tree index {args.treeId}"
+    | .some tree =>
+      return .ok { parents := tree.structure_array }
+
+end Pantograph

Pantograph/Commands.lean

@@ -6,10 +6,64 @@ its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
 
-import Pantograph.Serial
-
 namespace Pantograph.Commands
 
+
+/-- 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
+  -- When enabled, the types and values of persistent variables in a proof goal
+  -- are not shown unless they are new to the proof step. Reduces overhead
+  proofVariableDelta: Bool := false
+  -- See `pp.auxDecls`
+  printAuxDecls: Bool      := false
+  -- See `pp.implementationDetailHyps`
+  printImplementationDetailHyps: Bool := false
+  deriving Lean.ToJson
+
+abbrev OptionsT := ReaderT Options
+
+--- Expression Objects ---
+
+structure BoundExpression where
+  binders: Array (String × String)
+  target: String
+  deriving Lean.ToJson
+structure Expression where
+  -- Pretty printed expression
+  pp?: Option String             := .none
+  -- AST structure
+  sexp?: Option String           := .none
+  deriving Lean.ToJson
+
+structure Variable where
+  name: String
+  /-- Does the name contain a dagger -/
+  isInaccessible?: Option Bool := .none
+  type?: Option Expression  := .none
+  value?: Option Expression := .none
+  deriving Lean.ToJson
+structure Goal where
+  /-- String case id -/
+  caseName?: Option String  := .none
+  /-- Is the goal in conversion mode -/
+  isConversion: Bool        := false
+  /-- target expression type -/
+  target: Expression
+  /-- Variables -/
+  vars: Array Variable      := #[]
+  deriving Lean.ToJson
+
+
+
+--- Individual Commands and return types ---
+
 structure Command where
   cmd: String
   payload: Lean.Json
@@ -21,40 +75,58 @@ structure InteractionError where
   deriving Lean.ToJson
 
 
--- Individual command and return types
+--- Individual command and return types ---
 
 
--- Print all symbols in environment
+structure Reset where
-structure Catalog where
   deriving Lean.FromJson
-structure CatalogResult where
+structure ResetResult 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
+-- Return the type of an expression
-structure ExprType where
+structure ExprEcho where
   expr: String
   deriving Lean.FromJson
-structure ExprTypeResult where
+structure ExprEchoResult where
-  type: String
+  expr: Expression
-  roundTrip: String
+  type: Expression
   deriving Lean.ToJson
 
+-- Print all symbols in environment
+structure LibCatalog where
+  deriving Lean.FromJson
+structure LibCatalogResult where
+  symbols: Array String
+  deriving Lean.ToJson
+-- Print the type of a symbol
+structure LibInspect where
+  name: String
+  -- If true/false, show/hide the value expressions; By default definitions
+  -- values are shown and theorem values are hidden.
+  value?: Option Bool := .some false
+  deriving Lean.FromJson
+structure LibInspectResult where
+  type: Expression
+  value?: Option Expression := .none
+  module?: Option String
+  deriving Lean.ToJson
+
+/-- Set options; See `Options` struct above for meanings -/
+structure OptionsSet where
+  printJsonPretty?: Option Bool
+  printExprPretty?: Option Bool
+  printExprAST?: Option Bool
+  proofVariableDelta?: Option Bool
+  printAuxDecls?: Option Bool
+  printImplementationDetailHyps?: Option Bool
+  deriving Lean.FromJson
+structure OptionsSetResult where
+  deriving Lean.ToJson
+structure OptionsPrint where
+  deriving Lean.FromJson
+abbrev OptionsPrintResult := Options
+
 structure ProofStart where
   name: Option String     -- Identifier of the proof
   -- Only one of the fields below may be populated.
@@ -64,7 +136,6 @@ structure ProofStart where
 structure ProofStartResult where
   treeId: Nat := 0 -- Proof tree id
   deriving Lean.ToJson
-
 structure ProofTactic where
   -- Identifiers for tree, state, and goal
   treeId: Nat
@@ -72,14 +143,14 @@ structure ProofTactic where
   goalId: Option Nat
   tactic: String
   deriving Lean.FromJson
-structure ProofTacticResultSuccess where
+structure ProofTacticResult where
-  goals: Array Goal
+  -- Existence of this field shows success
-  nextId?: Option Nat -- Next proof state id
+  goals?: Option (Array Goal)          := .none
+  -- Next proof state id, if successful
+  nextId?: Option Nat                  := .none
+  -- Existence of this field shows failure
+  tacticErrors?: Option (Array String) := .none
   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

Pantograph/Serial.lean

@@ -3,15 +3,20 @@ All serialisation functions
 -/
 import Lean
 
+import Pantograph.Commands
+
 namespace Pantograph
 open Lean
 
+--- Input Functions ---
+
 
 /-- 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
+/-- Read syntax object from string -/
 def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
   Parser.runParserCategory
     (env := env)
@@ -39,82 +44,164 @@ def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 
-structure BoundExpression where
+
-  binders: Array (String × String)
+--- Output Functions ---
-  target: String
+
-  deriving ToJson
+def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do
-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) }
 
+/--
+ Completely serialises an expression tree. Json not used due to compactness
+-/
+def serialize_expression_ast (expr: Expr): MetaM String := do
+  match expr with
+  | .bvar deBruijnIndex =>
+    -- This is very common so the index alone is shown. Literals are handled below.
+    return s!"{deBruijnIndex}"
+  | .fvar fvarId =>
+    let name := (← fvarId.getDecl).userName
+    return s!"(:fv {name})"
+  | .mvar _ =>
+    -- mvarId is ignored.
+    return s!":mv"
+  | .sort u => return s!"(:sort {u.depth})"
+  | .const declName _ =>
+    -- The universe level of the const expression is elided since it should be
+    -- inferrable from surrounding expression
+    return s!"(:c {declName})"
+  | .app fn arg =>
+    let fn' ← serialize_expression_ast fn
+    let arg' ← serialize_expression_ast arg
+    return s!"({fn'} {arg'})"
+  | .lam binderName binderType body binderInfo =>
+    let binderName' := nameToAst binderName
+    let binderType' ← serialize_expression_ast binderType
+    let body' ← serialize_expression_ast body
+    let binderInfo' := binderInfoToAst binderInfo
+    return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+  | .forallE binderName binderType body binderInfo =>
+    let binderName' := nameToAst binderName
+    let binderType' ← serialize_expression_ast binderType
+    let body' ← serialize_expression_ast body
+    let binderInfo' := binderInfoToAst binderInfo
+    return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+  | .letE name type value body _ =>
+    -- Dependent boolean flag diacarded
+    let name' := nameToAst name
+    let type' ← serialize_expression_ast type
+    let value' ← serialize_expression_ast value
+    let body' ← serialize_expression_ast body
+    return s!"(:let {name'} {type'} {value'} {body'})"
+  | .lit v =>
+    -- To not burden the downstream parser who needs to handle this, the literal
+    -- is wrapped in a :lit sexp.
+    let v' := match v with
+      | .natVal val => toString val
+      | .strVal val => s!"\"{val}\""
+    return s!"(:lit {v'})"
+  | .mdata _ expr =>
+    -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
+    -- It may become necessary to incorporate the metadata.
+    return (← serialize_expression_ast expr)
+  | .proj typeName idx struct =>
+    let struct' ← serialize_expression_ast struct
+    return s!"(:proj {typeName} {idx} {struct'})"
 
-structure Variable where
+  where
-  name: String
+  -- Elides all unhygenic names
-  /-- Does the name contain a dagger -/
+  nameToAst: Lean.Name → String
-  isInaccessible: Bool      := false
+    | .anonymous
-  type: String
+    | .num _ _ => ":anon"
-  value?: Option String     := .none
+    | n@(.str _ _) => toString n
-  deriving ToJson
+  binderInfoToAst : Lean.BinderInfo → String
-structure Goal where
+    | .default => ""
-  /-- String case id -/
+    | .implicit => " :implicit"
-  caseName?: Option String  := .none
+    | .strictImplicit => " :strictImplicit"
-  /-- Is the goal in conversion mode -/
+    | .instImplicit => " :instImplicit"
-  isConversion: Bool        := false
+
-  /-- target expression type -/
+def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do
-  target: String
+  let pp := toString (← Meta.ppExpr e)
-  /-- Variables -/
+  let pp?: Option String := match options.printExprPretty with
-  vars: Array Variable      := #[]
+      | true => .some pp
-  deriving ToJson
+      | false => .none
+  let sexp: String := (← serialize_expression_ast e)
+  let sexp?: Option String := match options.printExprAST with
+      | true => .some sexp
+      | false => .none
+  return {
+    pp?,
+    sexp?
+  }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do
+def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+      : MetaM Commands.Goal := do
   -- Options for printing; See Meta.ppGoal for details
-  let showLetValues  := True
+  let showLetValues  := true
-  let ppAuxDecls     := false
+  let ppAuxDecls     := options.printAuxDecls
-  let ppImplDetailHyps := false
+  let ppImplDetailHyps := options.printImplementationDetailHyps
   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
+    let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
+      match localDecl with
+      | .cdecl _ _ varName _ _ _ =>
+        let varName := varName.simpMacroScopes
+        return {
+          name := toString varName,
+        }
+      | .ldecl _ _ varName _ _ _ _ => do
+        return {
+          name := toString varName,
+        }
+    let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
       match localDecl with
       | .cdecl _ _ varName type _ _ =>
         let varName := varName.simpMacroScopes
         let type ← instantiateMVars type
         return {
           name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
+          isInaccessible? := .some varName.isInaccessibleUserName
-          type := toString <| ← Meta.ppExpr type
+          type? := .some (← serialize_expression options 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)
+          pure $ .some (← serialize_expression options val)
         else
           pure $ .none
         return {
           name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
+          isInaccessible? := .some varName.isInaccessibleUserName
-          type := toString <| ← Meta.ppExpr type
+          type? := .some (← serialize_expression options type)
           value? := value?
         }
     let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
-       let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
-       if skip then
+        !ppImplDetailHyps && localDecl.isImplementationDetail
-         return acc
+      if skip then
-       else
+        return acc
-         let var ← ppVars localDecl
+      else
-         return var::acc
+        let nameOnly := options.proofVariableDelta && (parentDecl?.map
+          (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
+        let var ← match nameOnly with
+          | true => ppVarNameOnly localDecl
+          | false => ppVar 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)),
+      target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }
 
+
+
 end Pantograph

Pantograph/Tactic.lean

@@ -16,7 +16,9 @@ From this point on, any proof which extends
 -/
 
 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
-{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false }
+  {
+    msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
+  }
 
 
 namespace Pantograph
@@ -83,12 +85,14 @@ inductive TacticResult where
   -- Invalid id
   | invalid (message: String): TacticResult
   -- Goes to next state
-  | success (nextId?: Option Nat) (goals: Array Goal)
+  | success (nextId?: Option Nat) (goals: Array Commands.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
+def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String):
+    Commands.OptionsT StateRefT ProofTree M TacticResult := do
+  let options ← read
   let tree ← get
   match tree.states.get? stateId with
   | .none => return .invalid s!"Invalid state id {stateId}"
@@ -111,9 +115,10 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P
             parentGoalId := goalId
           }
           modify fun s => { s with states := s.states.push proofState }
+        let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal
         let goals ← nextGoals.mapM fun mvarId => do
           match (← MonadMCtx.getMCtx).findDecl? mvarId with
-          | .some mvarDecl => serialize_goal mvarDecl
+          | .some mvarDecl => serialize_goal options mvarDecl (parentDecl? := parentDecl?)
           | .none => throwError mvarId
         return .success (.some nextId) goals.toArray
 

Pantograph/Version.lean

@@ -0,0 +1,5 @@
+namespace Pantograph
+
+def version := "0.2.2"
+
+end Pantograph

README.md

@@ -23,7 +23,7 @@ Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantogr
 ## Usage
 
 ``` sh
-build/bin/pantograph OPTIONS|MODULES
+build/bin/pantograph MODULES|LEAN_OPTIONS
 ```
 
 The REPL loop accepts commands as single-line JSON inputs and outputs either an
@@ -33,22 +33,22 @@ 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
+The list of available commands can be found in `Pantograph/Commands.lean` and below. 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`.
+also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
 
 Example: (~5k symbols)
 ```
 $ build/bin/Pantograph Init
-catalog
+lib.catalog
-inspect {"name": "Nat.le_add_left"}
+lib.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
+lib.catalog
 ```
 Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
 ```
@@ -65,10 +65,15 @@ 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
+- `reset`: Delete all cached expressions and proof trees
-- `inspect {"name": <name>}`: Show the type and package of a given symbol
+- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
-- `clear`: Delete all cached expressions and proof trees
+- `lib.catalog`: Display a list of all safe Lean symbols in the current context
-- `expr.type {"expr": <expr>}`: Determine the type of an expression and round-trip it
+- `lib.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
+  given symbol; If value flag is set, the value is printed or hidden. By default
+  only the values of definitions are printed.
+- `options.set { key: value, ... }`: Set one or more options (not Lean options; those
+  have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
+- `options.print`: Display the current set of options
 - `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
@@ -86,4 +91,3 @@ The tests are based on `LSpec`. To run tests,
 ``` sh
 test/all.sh
 ```
-

Test/Integration.lean

@@ -0,0 +1,76 @@
+/- Integration test for the REPL
+ -/
+import LSpec
+import Pantograph
+namespace Pantograph.Test
+open Pantograph
+
+def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
+    (expected: Lean.Json): MainM LSpec.TestSeq := do
+  let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
+  return LSpec.test s!"{cmd}" (toString result = toString expected)
+
+def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
+  -- Setup the environment for execution
+  let env ← Lean.importModules
+    (imports := [{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
+    (opts := {})
+    (trustLevel := 1)
+  let context: Context := {
+    imports := ["Init"]
+  }
+  let coreContext: Lean.Core.Context := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],
+    fileName := "<Test>",
+    fileMap := { source := "", positions := #[0], lines := #[1] },
+    options := Lean.Options.empty
+  }
+  let commands: MainM LSpec.TestSeq :=
+    steps.foldlM (λ suite step => do
+      let result ← step
+      return suite ++ result) LSpec.TestSeq.done
+  try
+    let termElabM := commands.run context |>.run' {}
+    let metaM := termElabM.run' (ctx := {
+      declName? := some "_pantograph",
+      errToSorry := false
+    })
+    let coreM := metaM.run'
+    return Prod.fst $ (← coreM.toIO coreContext { env := env })
+  catch ex =>
+    return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
+
+def test_option_print : IO LSpec.TestSeq :=
+  let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
+  let sexp? := Option.some "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"
+  let module? := Option.some "Init.Data.Nat.Basic"
+  let options: Commands.Options := {}
+  subroutine_runner [
+    subroutine_step "lib.inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp? }, module? }:
+      Commands.LibInspectResult)),
+    subroutine_step "options.set"
+      [("printExprAST", .bool true)]
+     (Lean.toJson ({ }:
+      Commands.OptionsSetResult)),
+    subroutine_step "lib.inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp?, sexp? }, module? }:
+      Commands.LibInspectResult)),
+    subroutine_step "options.print"
+      []
+     (Lean.toJson ({ options with printExprAST := true }:
+      Commands.OptionsPrintResult))
+  ]
+
+def test_integration: IO LSpec.TestSeq := do
+
+  return LSpec.group "Integration" $
+    (LSpec.group "Option modify" (← test_option_print))
+
+
+end Pantograph.Test

Test/Main.lean

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

Test/Proofs.lean

@@ -1,5 +1,5 @@
 import LSpec
-import Pantograph.Meta
+import Pantograph.Tactic
 import Pantograph.Serial
 
 namespace Pantograph.Test
@@ -10,7 +10,7 @@ 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
+abbrev TestM := ReaderT Commands.Options StateRefT ProofTree M
 
 def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
   let env ← Lean.MonadEnv.getEnv
@@ -47,13 +47,16 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
           (expr := expr)
         return (testSeq, Option.some state)
 
-deriving instance DecidableEq, Repr for Variable
+deriving instance DecidableEq, Repr for Commands.Expression
-deriving instance DecidableEq, Repr for Goal
+deriving instance DecidableEq, Repr for Commands.Variable
+deriving instance DecidableEq, Repr for Commands.Goal
 deriving instance DecidableEq, Repr for TacticResult
 
+/-- Check the output of each proof step -/
 def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
     (expected: TacticResult) : TestM LSpec.TestSeq := do
-  let result: TacticResult ← ProofTree.execute stateId goalId tactic
+  let options ← read
+  let result: TacticResult ← ProofTree.execute stateId goalId tactic |>.run options
   match expected, result with
   | .success (.some i) #[], .success (.some _) goals =>
     -- If the goals are omitted but the next state is specified, we imply that
@@ -63,16 +66,17 @@ def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
   | _, _ =>
     return LSpec.test s!"{stateId}.{goalId} {tactic}"   (result = expected)
 
+/-- Check that the tree structure is correct -/
 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
+def proof_runner (env: Lean.Environment) (options: Commands.Options) (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
+    | .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run options |>.run' state
 
   let coreContext: Lean.Core.Context := {
     currNamespace := str_to_name "Aniva",
@@ -90,21 +94,22 @@ def proof_runner (env: Lean.Environment) (start: Start) (steps: List (TestM LSpe
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
   | .ok a            => return a
 
-def build_goal (nameType: List (String × String)) (target: String): Goal :=
+def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
   {
-    target := target,
+    target := { pp? := .some target},
-    vars := (nameType.map fun x => ({ name := x.fst, type := x.snd }: Variable)).toArray
+    vars := (nameType.map fun x => ({
+      name := x.fst,
+      type? := .some { pp? := .some x.snd },
+      isInaccessible? := .some false
+    })).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 := {
+  let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-    target := "n + m = m + n",
+  proof_runner env {} (.copy "Nat.add_comm") [
-    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"
@@ -113,8 +118,8 @@ def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
       (.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"
+  let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-  proof_runner env (.expr "∀ (a b: Nat), a + b = b + a") [
+  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"
@@ -139,16 +144,17 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
   . apply Or.inl
     assumption
 def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
-  let branchGoal (caseName name: String): Goal := {
+  let typeProp: Commands.Expression := { pp? := .some "Prop" }
+  let branchGoal (caseName name: String): Commands.Goal := {
     caseName? := .some caseName,
-    target := "q ∨ p",
+    target := { pp? := .some "q ∨ p" },
     vars := #[
-      { name := "p", type := "Prop" },
+      { name := "p", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "q", type := "Prop" },
+      { name := "q", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "h✝", type := name, isInaccessible := true }
+      { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
     ]
   }
-  proof_runner env (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [
+  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"
@@ -171,7 +177,7 @@ example (w x y z : Nat) (p : Nat → Prop)
   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_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 *"
@@ -180,6 +186,25 @@ def proof_arith_1 (env: Lean.Environment): IO LSpec.TestSeq := do
       (.success .none #[])
   ]
 
+def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
+  {
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      name := x.fst,
+      type? := x.snd.map (λ type => { pp? := type }),
+      isInaccessible? := x.snd.map (λ _ => false)
+    })).toArray
+  }
+def proof_delta_variable (env: Lean.Environment): IO LSpec.TestSeq := do
+  let goal1: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
+  let goal2: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
+  proof_runner env { proofVariableDelta := true } (.expr "∀ (a b: Nat), a + b = b + a") [
+    proof_step 0 0 "intro n"
+      (.success (.some 1) #[goal1]),
+    proof_step 1 0 "intro m"
+      (.success (.some 2) #[goal2])
+  ]
+
 def test_proofs : IO LSpec.TestSeq := do
   let env: Lean.Environment ← Lean.importModules
     (imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
@@ -190,7 +215,8 @@ def test_proofs : IO LSpec.TestSeq := do
     (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))
+    (LSpec.group "Arithmetic 1" $ (← proof_arith_1 env)) ++
+    (LSpec.group "Delta variable" $ (← proof_delta_variable env))
 
 end Pantograph.Test
 

Test/Serial.lean

@@ -7,22 +7,25 @@ namespace Pantograph.Test
 open Pantograph
 open Lean
 
-deriving instance Repr, DecidableEq for BoundExpression
+deriving instance Repr, DecidableEq for Commands.BoundExpression
+
+def test_str_to_name: LSpec.TestSeq :=
+    LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
-  let cases: List (String × BoundExpression) := [
+  let entries: List (String × Commands.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 coreM := entries.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",
+    currNamespace := Lean.Name.str .anonymous "Aniva"
     openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph>",
+    fileName := "<Pantograph/Test>",
     fileMap := { source := "", positions := #[0], lines := #[1] }
   }
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
@@ -30,6 +33,32 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
   | .ok a            => return a
 
+def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
+  let entries: List (String × String) := [
+    -- This one contains unhygienic variable names which must be suppressed
+    ("Nat.add", "(:forall :anon (:c Nat) (:forall :anon (:c Nat) (:c Nat)))"),
+    -- These ones are normal and easy
+    ("Nat.add_one", "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"),
+    ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)")
+  ]
+  let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
+    let env ← MonadEnv.getEnv
+    let expr := str_to_name symbol |> env.find? |>.get! |>.type
+    let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
+  let coreM := metaM.run'
+  let coreContext: Core.Context := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph/Test>",
+    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 }))
@@ -37,7 +66,8 @@ def test_serial: IO LSpec.TestSeq := do
     (trustLevel := 1)
 
   return LSpec.group "Serialisation" $
+    (LSpec.group "str_to_name" test_str_to_name) ++
     (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")
+    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
 
 end Pantograph.Test

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-06
+leanprover/lean4:nightly-2023-08-12