Main.lean

@@ -1,173 +1,8 @@
 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
@@ -184,38 +19,22 @@ unsafe def loop : Subroutine Unit := do
     IO.println <| toString <| ret
   loop
 
-namespace Lean
--- This is better than the default version since it handles `.`
-def setOptionFromString' (opts : Options) (entry : String) : IO Options := do
-  let ps := (entry.splitOn "=").map String.trim
-  let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := str_to_name key
-  let defValue ← getOptionDefaultValue key
-  match defValue with
-  | DataValue.ofString _ => pure $ opts.setString key val
-  | DataValue.ofBool _   =>
-    match val with
-    | "true" => pure $ opts.setBool key true
-    | "false" => pure $ opts.setBool key false
-    | _ => throw $ IO.userError s!"invalid Bool option value '{val}'"
-  | DataValue.ofName _   => pure $ opts.setName key val.toName
-  | DataValue.ofNat _    =>
-    match val.toNat? with
-    | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
-    | some v => pure $ opts.setNat key v
-  | DataValue.ofInt _    =>
-    match val.toInt? with
-    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
-    | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")
-end Lean
-
 unsafe def main (args: List String): IO Unit := do
+  -- 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
@@ -225,11 +44,11 @@ unsafe def main (args: List String): IO Unit := do
   let context: Context := {
   }
   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,209 @@
 import Pantograph.Commands
+import Pantograph.Serial
+import Pantograph.Meta
 import Pantograph.Symbols
+
+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
+  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 defValue ← getOptionDefaultValue key
+  match defValue with
+  | DataValue.ofString _ => pure $ opts.setString key val
+  | DataValue.ofBool _   =>
+    match val with
+    | "true" => pure $ opts.setBool key true
+    | "false" => pure $ opts.setBool key false
+    | _ => throw  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}'"
+    | some v => pure $ opts.setNat key v
+  | DataValue.ofInt _    =>
+    match val.toInt? with
+    | none   => throw s!"invalid Int option value '{val}'"
+    | some v => pure $ opts.setInt key v
+  | DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
+end Lean
+
+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)
+
+/-- 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): Subroutine Lean.Json := do
+  match command.cmd with
+  | "option.set" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => option_set args
+    | .error x => return errorJson x
+  | "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: Commands.InteractionError :=
+      { error := "unknown", desc := s!"Unknown command {cmd}" }
+    return Lean.toJson error
+  where
+  errorI (type desc: String) := Lean.toJson (
+    { error := type, desc := desc }: Commands.InteractionError)
+  errorJson := errorI "json"
+  errorIndex := errorI "index"
+  option_set (args: Commands.OptionSet): Subroutine Lean.Json := do
+    let options? ← args.options.foldlM Lean.setOptionFromString'' Lean.Options.empty
+      |>.run
+    match options? with
+    | .ok options =>
+      withTheReader Lean.Core.Context
+        (λ coreContext => { coreContext with options })
+        (pure $ Lean.toJson <| ({ }: Commands.OptionSetResult))
+    | .error e =>
+      return errorI "parsing" e
+  catalog (_: Commands.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 }: Commands.CatalogResult)
+  inspect (args: Commands.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 Option.none -- TODO: Temporary override, enable expression dissection in options.
+          -- return .some (← type_expr_to_bound info.toConstantVal.type)
+        | _ => return Option.none)
+      return Lean.toJson ({
+        type := toString format,
+        boundExpr? := boundExpr?,
+        module? := module?
+      }: Commands.InspectResult)
+  clear : Subroutine Lean.Json := do
+    let state ← get
+    let nTrees := state.proofTrees.size
+    set { state with proofTrees := #[] }
+    return Lean.toJson ({ nTrees := nTrees }: Commands.ClearResult)
+  expr_type (args: Commands.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)
+          }: Commands.ExprTypeResult)
+        catch exception =>
+          return errorI "typing" (← exception.toMessageData.toString)
+  proof_start (args: Commands.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 }: Commands.ProofStartResult)
+  proof_tactic (args: Commands.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 }: Commands.ProofTacticResultSuccess)
+      | .failure messages =>
+        return Lean.toJson (
+          { tacticErrors := messages }: Commands.ProofTacticResultFailure)
+  proof_print_tree (args: Commands.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}: Commands.ProofPrintTreeResult)
+
+
+end Pantograph

Pantograph/Commands.lean

@@ -21,7 +21,16 @@ structure InteractionError where
   deriving Lean.ToJson
 
 
--- Individual command and return types
+--- Individual command and return types ---
+
+-- Set Lean options supplied in the form of
+--
+-- option=value
+structure OptionSet where
+  options: Array String
+  deriving Lean.FromJson
+structure OptionSetResult where
+  deriving Lean.ToJson
 
 
 -- Print all symbols in environment
@@ -38,7 +47,7 @@ structure Inspect where
 structure InspectResult where
   type: String
   -- Decompose the bound expression when the type is forall.
-  boundExpr?: Option BoundExpression
+  boundExpr?: Option BoundExpression := Option.none
   module?: Option String
   deriving Lean.ToJson
 

Pantograph/Serial.lean

@@ -117,4 +117,64 @@ def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do
       vars := vars.reverse.toArray
     }
 
+/-- 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 => return s!"(:bv {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!"(:const {declName})"
+  | .app fn arg =>
+    let fn' ← serialize_expression_ast fn
+    let arg' ← serialize_expression_ast arg
+    return s!"(:app {fn'} {arg'})"
+  | .lam binderName binderType body binderInfo =>
+    let binderType' ← serialize_expression_ast binderType
+    let body' ← serialize_expression_ast body
+    let binderInfo' := binderInfoToAst binderInfo
+    return s!"(:lam {binderName} {binderType'} {body'} :{binderInfo'})"
+  | .forallE binderName binderType body binderInfo =>
+    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 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 =>
+    return (match v with
+      | .natVal val => toString val
+      | .strVal val => s!"\"{val}\"")
+  | .mdata _ expr =>
+    -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
+    return (← serialize_expression_ast expr)
+  | .proj typeName idx struct =>
+    let struct' ← serialize_expression_ast struct
+    return s!"(:proj {typeName} {idx} {struct'})"
+
+  where
+  binderInfoToAst : Lean.BinderInfo → String
+    | .default => "default"
+    | .implicit => "implicit"
+    | .strictImplicit => "strictImplicit"
+    | .instImplicit => "instImplicit"
+
+/-- Serialised expression object --/
+structure Expression where
+  prettyprinted?: Option String := .none
+  bound?: Option BoundExpression := .none
+  sexp?: Option String := .none
+  deriving ToJson
+
 end Pantograph

Pantograph/Version.lean

@@ -0,0 +1,5 @@
+namespace Pantograph
+
+def version := "0.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
@@ -37,7 +37,7 @@ The list of available commands can be found in `Pantograph/Commands.lean`. An
 empty command aborts the REPL.
 
 The `Pantograph` executable must be run with a list of modules to import. It can
-also accept options of the form `--key=value` e.g. `--pp.raw=true`.
+also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
 
 Example: (~5k symbols)
 ```

Test/Main.lean

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

lean-toolchain

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