Main.lean

@@ -1,37 +1,195 @@
 import Lean.Data.Json
 import Lean.Environment
 
-import Pantograph.Version
-import Pantograph
+import Pantograph.Commands
+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 : MainM Unit := do
-  let state ← get
+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)
-    -- Using `Lean.Json.compress` here to prevent newline
-    IO.println error.compress
+    IO.println (toString error)
   | .ok command =>
     let ret ← execute command
-    let str := match state.options.printJsonPretty with
-      | true => ret.pretty
-      | false => ret.compress
-    IO.println str
+    IO.println <| toString <| ret
   loop
 
 namespace Lean
-
-/-- 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
+-- 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 "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := Pantograph.str_to_name key
+  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
@@ -39,37 +197,25 @@ def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO O
     match val with
     | "true" => pure $ opts.setBool key true
     | "false" => pure $ opts.setBool key false
-    | _ => throw  s!"invalid Bool option value '{val}'"
+    | _ => 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 s!"invalid Nat option value '{val}'"
+    | 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 s!"invalid Int option value '{val}'"
+    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
     | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
-
+  | DataValue.ofSyntax _ => throw (IO.userError 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)
 
-  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}"
+  -- 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
@@ -77,14 +223,13 @@ unsafe def main (args: List String): IO Unit := do
     (opts := {})
     (trustLevel := 1)
   let context: Context := {
-    imports
   }
   let coreContext: Lean.Core.Context := {
-    currNamespace := Lean.Name.str .anonymous "Aniva"
+    currNamespace := str_to_name "Aniva",
     openDecls := [],     -- No 'open' directives needed
     fileName := "<Pantograph>",
     fileMap := { source := "", positions := #[0], lines := #[1] },
-    options := options
+    options := ← options.foldlM Lean.setOptionFromString' Lean.Options.empty
   }
   try
     let termElabM := loop.run context |>.run' {}

Pantograph.lean

@@ -1,179 +1,2 @@
 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,64 +6,10 @@ 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
@@ -75,57 +21,39 @@ structure InteractionError where
   deriving Lean.ToJson
 
 
---- Individual command and return types ---
+-- Individual command and return types
 
 
-structure Reset where
-  deriving Lean.FromJson
-structure ResetResult where
-  nTrees: Nat
-  deriving Lean.ToJson
-
--- Return the type of an expression
-structure ExprEcho where
-  expr: String
-  deriving Lean.FromJson
-structure ExprEchoResult where
-  expr: Expression
-  type: Expression
-  deriving Lean.ToJson
-
 -- Print all symbols in environment
-structure LibCatalog where
+structure Catalog where
   deriving Lean.FromJson
-structure LibCatalogResult where
+structure CatalogResult where
   symbols: Array String
   deriving Lean.ToJson
+
 -- Print the type of a symbol
-structure LibInspect where
+structure Inspect 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
+structure InspectResult where
+  type: String
+  -- Decompose the bound expression when the type is forall.
+  boundExpr?: Option BoundExpression
   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
+structure ClearResult where
+  nTrees: Nat
   deriving Lean.ToJson
-structure OptionsPrint where
+
+-- Get the type of an expression
+structure ExprType where
+  expr: String
   deriving Lean.FromJson
-abbrev OptionsPrintResult := Options
+structure ExprTypeResult where
+  type: String
+  roundTrip: String
+  deriving Lean.ToJson
 
 structure ProofStart where
   name: Option String     -- Identifier of the proof
@@ -136,6 +64,7 @@ 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
@@ -143,14 +72,14 @@ structure ProofTactic where
   goalId: Option Nat
   tactic: String
   deriving Lean.FromJson
-structure ProofTacticResult where
-  -- Existence of this field shows success
-  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
+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

Pantograph/Meta.lean

@@ -16,9 +16,7 @@ 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
@@ -85,14 +83,12 @@ inductive TacticResult where
   -- Invalid id
   | invalid (message: String): TacticResult
   -- Goes to next state
-  | success (nextId?: Option Nat) (goals: Array Commands.Goal)
+  | 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):
-    Commands.OptionsT StateRefT ProofTree M TacticResult := do
-  let options ← read
+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}"
@@ -115,10 +111,9 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String):
             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 options mvarDecl (parentDecl? := parentDecl?)
+          | .some mvarDecl => serialize_goal mvarDecl
           | .none => throwError mvarId
         return .success (.some nextId) goals.toArray
 

Pantograph/Serial.lean

@@ -3,20 +3,15 @@ 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)
@@ -44,164 +39,82 @@ def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
     return .ok expr
   catch ex => return .error (← ex.toMessageData.toString)
 
-
---- Output Functions ---
-
-def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do
+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) }
 
-/--
- 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'})"
 
-  where
-  -- Elides all unhygenic names
-  nameToAst: Lean.Name → String
-    | .anonymous
-    | .num _ _ => ":anon"
-    | n@(.str _ _) => toString n
-  binderInfoToAst : Lean.BinderInfo → String
-    | .default => ""
-    | .implicit => " :implicit"
-    | .strictImplicit => " :strictImplicit"
-    | .instImplicit => " :instImplicit"
-
-def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do
-  let pp := toString (← Meta.ppExpr e)
-  let pp?: Option String := match options.printExprPretty with
-      | true => .some pp
-      | 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?
-  }
+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 (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
-      : MetaM Commands.Goal := do
+def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do
   -- Options for printing; See Meta.ppGoal for details
-  let showLetValues  := true
-  let ppAuxDecls     := options.printAuxDecls
-  let ppImplDetailHyps := options.printImplementationDetailHyps
+  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 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
+    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? := .some varName.isInaccessibleUserName
-          type? := .some (← serialize_expression options type)
+          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 (← serialize_expression options val)
+          pure $ .some <| toString <| (← Meta.ppExpr val)
         else
           pure $ .none
         return {
           name := toString varName,
-          isInaccessible? := .some varName.isInaccessibleUserName
-          type? := .some (← serialize_expression options type)
+          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 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
+       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 := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
+      target := toString <| (← Meta.ppExpr (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }
 
-
-
 end Pantograph

Pantograph/Version.lean

@@ -1,5 +0,0 @@
-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 MODULES|LEAN_OPTIONS
+build/bin/pantograph OPTIONS|MODULES
 ```
 
 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` and below. An
+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 lean options of the form `--key=value` e.g. `--pp.raw=true`.
+also accept options of the form `--key=value` e.g. `--pp.raw=true`.
 
 Example: (~5k symbols)
 ```
 $ build/bin/Pantograph Init
-lib.catalog
-lib.inspect {"name": "Nat.le_add_left"}
+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
-lib.catalog
+catalog
 ```
 Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
 ```
@@ -65,15 +65,10 @@ 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.
-- `reset`: Delete all cached expressions and proof trees
-- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
-- `lib.catalog`: Display a list of all safe Lean symbols in the current context
-- `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
+- `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
@@ -91,3 +86,4 @@ The tests are based on `LSpec`. To run tests,
 ``` sh
 test/all.sh
 ```
+

Test/Integration.lean

@@ -1,76 +0,0 @@
-/- 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 Test.Integration
+import Pantograph.Symbols
 import Test.Proofs
 import Test.Serial
 
@@ -10,9 +10,8 @@ unsafe def main := do
   Lean.initSearchPath (← Lean.findSysroot)
 
   let suites := [
-    test_integration,
-    test_proofs,
-    test_serial
+    test_serial,
+    test_proofs
   ]
   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.Tactic
+import Pantograph.Meta
 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 := ReaderT Commands.Options StateRefT ProofTree M
+abbrev TestM := StateRefT ProofTree M
 
 def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
   let env ← Lean.MonadEnv.getEnv
@@ -47,16 +47,13 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
           (expr := expr)
         return (testSeq, Option.some state)
 
-deriving instance DecidableEq, Repr for Commands.Expression
-deriving instance DecidableEq, Repr for Commands.Variable
-deriving instance DecidableEq, Repr for Commands.Goal
+deriving instance DecidableEq, Repr for Variable
+deriving instance DecidableEq, Repr for 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 options ← read
-  let result: TacticResult ← ProofTree.execute stateId goalId tactic |>.run options
+  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
@@ -66,17 +63,16 @@ 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) (options: Commands.Options) (start: Start) (steps: List (TestM LSpec.TestSeq)): IO LSpec.TestSeq := do
+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 options |>.run' state
+    | .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run' state
 
   let coreContext: Lean.Core.Context := {
     currNamespace := str_to_name "Aniva",
@@ -94,22 +90,21 @@ def proof_runner (env: Lean.Environment) (options: Commands.Options) (start: Sta
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
   | .ok a            => return a
 
-def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
+def build_goal (nameType: List (String × String)) (target: String): Goal :=
   {
-    target := { pp? := .some target},
-    vars := (nameType.map fun x => ({
-      name := x.fst,
-      type? := .some { pp? := .some x.snd },
-      isInaccessible? := .some false
-    })).toArray
+    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: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-  proof_runner env {} (.copy "Nat.add_comm") [
+  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"
@@ -118,8 +113,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: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
-  proof_runner env {} (.expr "∀ (a b: Nat), a + b = b + a") [
+  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"
@@ -144,17 +139,16 @@ 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 typeProp: Commands.Expression := { pp? := .some "Prop" }
-  let branchGoal (caseName name: String): Commands.Goal := {
+  let branchGoal (caseName name: String): Goal := {
     caseName? := .some caseName,
-    target := { pp? := .some "q ∨ p" },
+    target := "q ∨ p",
     vars := #[
-      { name := "p", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "q", type? := .some typeProp, isInaccessible? := .some false },
-      { name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
+      { 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_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"
@@ -177,7 +171,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 *"
@@ -186,25 +180,6 @@ 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 }))
@@ -215,8 +190,7 @@ 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 "Delta variable" $ (← proof_delta_variable env))
+    (LSpec.group "Arithmetic 1" $ (← proof_arith_1 env))
 
 end Pantograph.Test
 

Test/Serial.lean

@@ -7,25 +7,22 @@ namespace Pantograph.Test
 open Pantograph
 open Lean
 
-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")
+deriving instance Repr, DecidableEq for BoundExpression
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
-  let entries: List (String × Commands.BoundExpression) := [
+  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 := entries.foldlM (λ suites (symbol, target) => do
+  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 := Lean.Name.str .anonymous "Aniva"
+    currNamespace := str_to_name "Aniva",
     openDecls := [],     -- No 'open' directives needed
-    fileName := "<Pantograph/Test>",
+    fileName := "<Pantograph>",
     fileMap := { source := "", positions := #[0], lines := #[1] }
   }
   match ← (coreM.run' coreContext { env := env }).toBaseIO with
@@ -33,32 +30,6 @@ 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 }))
@@ -66,8 +37,7 @@ 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.group "Sexp from symbol" (← test_sexp_of_symbol env))
+    LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
 
 end Pantograph.Test

lean-toolchain

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