Main.lean

@@ -19,6 +19,36 @@ unsafe def loop : Subroutine Unit := do
     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
+  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
+
+
 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
@@ -30,7 +60,7 @@ unsafe def main (args: List String): IO Unit := do
   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
+    |>.foldlM Lean.setOptionFromString' Lean.Options.empty
     |>.run
   let options ← match options? with
     | .ok options => pure options
@@ -42,6 +72,7 @@ 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"

Pantograph.lean

@@ -3,39 +3,14 @@ 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
+  imports: List String
 
 /-- Stores state of the REPL -/
 structure State where
+  options: Commands.Options := {}
   --environments: Array Lean.Environment := #[]
   proofTrees:   Array ProofTree := #[]
 
@@ -59,9 +34,13 @@ def parse_command (s: String): Except String Commands.Command := do
 
 def execute (command: Commands.Command): Subroutine Lean.Json := do
   match command.cmd with
-  | "option.set" =>
+  | "options.set" =>
     match Lean.fromJson? command.payload with
-    | .ok args => option_set args
+    | .ok args => options_set args
+    | .error x => return errorJson x
+  | "options.print" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => options_print args
     | .error x => return errorJson x
   | "catalog" =>
     match Lean.fromJson? command.payload with
@@ -97,16 +76,19 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
     { 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
+  -- Command Functions
+  options_set (args: Commands.OptionsSet): Subroutine Lean.Json := do
+    let state ← get
+    set { state with
+      options := {
+        printExprPretty := args.printExprPretty?.getD true,
+        printExprAST := args.printExprAST?.getD true,
+        proofVariableDelta := args.proofVariableDelta?.getD false
+      }
+    }
+    return Lean.toJson ({ }: Commands.OptionsSetResult)
+  options_print (_: Commands.OptionsPrint): Subroutine Lean.Json := do
+    return Lean.toJson (← get).options
   catalog (_: Commands.Catalog): Subroutine Lean.Json := do
     let env ← Lean.MonadEnv.getEnv
     let names := env.constants.fold (init := #[]) (λ acc name info =>
@@ -115,22 +97,23 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
       | .none => acc)
     return Lean.toJson <| ({ symbols := names }: Commands.CatalogResult)
   inspect (args: Commands.Inspect): Subroutine Lean.Json := 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  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)
+      let value? := match args.value?, info with
+        | .some true, _ => info.value?
+        | .some false, _ => .none
+        | .none, .defnInfo _ => info.value?
+        | .none, _ => .none
       return Lean.toJson ({
-        type := toString format,
-        boundExpr? := boundExpr?,
+        type := ← serialize_expression state.options info.type,
+        value? := ← value?.mapM (λ v => serialize_expression state.options v),
         module? := module?
       }: Commands.InspectResult)
   clear : Subroutine Lean.Json := do

Pantograph/Commands.lean

@@ -6,10 +6,55 @@ 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 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
+  deriving Lean.ToJson
+
+--- 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: Bool      := false
+  type: Expression
+  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
@@ -23,15 +68,19 @@ structure InteractionError where
 
 --- Individual command and return types ---
 
--- Set Lean options supplied in the form of
---
--- option=value
-structure OptionSet where
-  options: Array String
+/-- Set options; See `Options` struct above for meanings -/
+structure OptionsSet where
+  printExprPretty?: Option Bool
+  printExprAST?: Option Bool
+  proofVariableDelta?: Option Bool
   deriving Lean.FromJson
-structure OptionSetResult where
+structure OptionsSetResult where
   deriving Lean.ToJson
 
+structure OptionsPrint where
+  deriving Lean.FromJson
+abbrev OptionsPrintResult := Options
+
 
 -- Print all symbols in environment
 structure Catalog where
@@ -43,11 +92,13 @@ structure CatalogResult where
 -- Print the type of a symbol
 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 InspectResult where
-  type: String
-  -- Decompose the bound expression when the type is forall.
-  boundExpr?: Option BoundExpression := Option.none
+  type: Expression
+  value?: Option Expression := .none
   module?: Option String
   deriving Lean.ToJson
 

Pantograph/Meta.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
+  -- TODO: Replace with actual options
+  let options: Commands.Options := {}
   let tree ← get
   match tree.states.get? stateId with
   | .none => return .invalid s!"Invalid state id {stateId}"
@@ -113,7 +117,7 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P
           modify fun s => { s with states := s.states.push proofState }
         let goals ← nextGoals.mapM fun mvarId => do
           match (← MonadMCtx.getMCtx).findDecl? mvarId with
-          | .some mvarDecl => serialize_goal mvarDecl
+          | .some mvarDecl => serialize_goal options mvarDecl
           | .none => throwError mvarId
         return .success (.some nextId) goals.toArray
 

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,84 +44,15 @@ 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)
-  target: String
-  deriving ToJson
-def type_expr_to_bound (expr: Expr): MetaM BoundExpression := do
+
+--- Output Functions ---
+
+def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do
   Meta.forallTelescope expr fun arr body => do
     let binders ← arr.mapM fun fvar => do
       return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
     return { binders, target := toString (← Meta.ppExpr body) }
 
-
-structure Variable where
-  name: String
-  /-- Does the name contain a dagger -/
-  isInaccessible: Bool      := false
-  type: String
-  value?: Option String     := .none
-  deriving ToJson
-structure Goal where
-  /-- String case id -/
-  caseName?: Option String  := .none
-  /-- Is the goal in conversion mode -/
-  isConversion: Bool        := false
-  /-- target expression type -/
-  target: String
-  /-- Variables -/
-  vars: Array Variable      := #[]
-  deriving ToJson
-
-/-- Adapted from ppGoal -/
-def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do
-  -- Options for printing; See Meta.ppGoal for details
-  let showLetValues  := True
-  let ppAuxDecls     := false
-  let ppImplDetailHyps := false
-  let lctx           := mvarDecl.lctx
-  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx mvarDecl.localInstances do
-    let rec ppVars (localDecl : LocalDecl) : MetaM Variable := do
-      match localDecl with
-      | .cdecl _ _ varName type _ _ =>
-        let varName := varName.simpMacroScopes
-        let type ← instantiateMVars type
-        return {
-          name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
-          type := toString <| ← Meta.ppExpr type
-        }
-      | .ldecl _ _ varName type val _ _ => do
-        let varName := varName.simpMacroScopes
-        let type ← instantiateMVars type
-        let value? ← if showLetValues then
-          let val ← instantiateMVars val
-          pure $ .some <| toString <| (← Meta.ppExpr val)
-        else
-          pure $ .none
-        return {
-          name := toString varName,
-          isInaccessible := varName.isInaccessibleUserName,
-          type := toString <| ← Meta.ppExpr type
-          value? := value?
-        }
-    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
-       let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail
-       if skip then
-         return acc
-       else
-         let var ← ppVars localDecl
-         return var::acc
-    return {
-      caseName? := match mvarDecl.userName with
-        | Name.anonymous => .none
-        | name => .some <| toString name,
-      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
-      target := toString <| (← Meta.ppExpr (← instantiateMVars mvarDecl.type)),
-      vars := vars.reverse.toArray
-    }
-
 /-- Completely serialises an expression tree. Json not used due to compactness -/
 def serialize_expression_ast (expr: Expr): MetaM String := do
   match expr with
@@ -131,16 +67,16 @@ def serialize_expression_ast (expr: Expr): MetaM String := do
   | .const declName _ =>
     -- The universe level of the const expression is elided since it should be
     -- inferrable from surrounding expression
-    return s!"(:const {declName})"
+    return s!"(:c {declName})"
   | .app fn arg =>
     let fn' ← serialize_expression_ast fn
     let arg' ← serialize_expression_ast arg
-    return s!"(:app {fn'} {arg'})"
+    return s!"({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'})"
+    return s!"(:lambda {binderName} {binderType'} {body'} :{binderInfo'})"
   | .forallE binderName binderType body binderInfo =>
     let binderType' ← serialize_expression_ast binderType
     let body' ← serialize_expression_ast body
@@ -170,11 +106,69 @@ def serialize_expression_ast (expr: Expr): MetaM String := do
     | .strictImplicit => "strictImplicit"
     | .instImplicit => "instImplicit"
 
-/-- Serialised expression object --/
-structure Expression where
-  prettyprinted?: Option String := .none
-  bound?: Option BoundExpression := .none
-  sexp?: Option String := .none
-  deriving ToJson
+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?
+  }
+
+/-- Adapted from ppGoal -/
+def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) : MetaM Commands.Goal := do
+  -- Options for printing; See Meta.ppGoal for details
+  let showLetValues  := True
+  let ppAuxDecls     := false
+  let ppImplDetailHyps := false
+  let lctx           := mvarDecl.lctx
+  let lctx           := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let rec ppVars (localDecl : LocalDecl) : MetaM Commands.Variable := do
+      match localDecl with
+      | .cdecl _ _ varName type _ _ =>
+        let varName := varName.simpMacroScopes
+        let type ← instantiateMVars type
+        return {
+          name := toString varName,
+          isInaccessible := varName.isInaccessibleUserName,
+          type := (← 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 (← serialize_expression options val)
+        else
+          pure $ .none
+        return {
+          name := toString varName,
+          isInaccessible := varName.isInaccessibleUserName,
+          type := (← serialize_expression options type)
+          value? := value?
+        }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+       let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail
+       if skip then
+         return acc
+       else
+         let var ← ppVars localDecl
+         return var::acc
+    return {
+      caseName? := match mvarDecl.userName with
+        | Name.anonymous => .none
+        | name => .some <| toString name,
+      isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
+      target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
+      vars := vars.reverse.toArray
+    }
+
+
 
 end Pantograph

README.md

@@ -33,7 +33,7 @@ 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
@@ -65,8 +65,13 @@ 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.
+- `options.set { key: value, ... }`: Set one or more options (not Lean options; those
+  have to be set via command line arguments.)
+- `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
+- `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.
 - `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
@@ -86,4 +91,3 @@ The tests are based on `LSpec`. To run tests,
 ``` sh
 test/all.sh
 ```
-

Test/Main.lean

@@ -9,6 +9,7 @@ unsafe def main := do
   Lean.enableInitializersExecution
   Lean.initSearchPath (← Lean.findSysroot)
 
+	-- TODO: Add proper testing
   let suites := [
     test_serial,
     test_proofs