Pantograph.lean

@@ -1,7 +1,7 @@
 import Pantograph.Commands
 import Pantograph.Serial
-import Pantograph.Meta
 import Pantograph.Symbols
+import Pantograph.Tactic
 
 namespace Pantograph
 
@@ -51,9 +51,9 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
     | .ok args => inspect args
     | .error x => return errorJson x
   | "clear" => clear
-  | "expr.type" =>
+  | "expr.echo" =>
     match Lean.fromJson? command.payload with
-    | .ok args => expr_type args
+    | .ok args => expr_echo args
     | .error x => return errorJson x
   | "proof.start" =>
     match Lean.fromJson? command.payload with
@@ -121,7 +121,8 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
     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
+  expr_echo (args: Commands.ExprEcho): Subroutine Lean.Json := do
+    let state ← get
     let env ← Lean.MonadEnv.getEnv
     match syntax_from_str env args.expr with
     | .error str => return errorI "parsing" str
@@ -130,11 +131,11 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
       | .error str => return errorI "elab" str
       | .ok expr => do
         try
-          let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr)
+          let type ← Lean.Meta.inferType expr
           return Lean.toJson <| ({
-              type := toString format,
-              roundTrip := toString <| (← Lean.Meta.ppExpr expr)
-          }: Commands.ExprTypeResult)
+              type := (← serialize_expression (options := state.options) type),
+              expr := (← serialize_expression (options := state.options) expr)
+          }: Commands.ExprEchoResult)
         catch exception =>
           return errorI "typing" (← exception.toMessageData.toString)
   proof_start (args: Commands.ProofStart): Subroutine Lean.Json := do
@@ -171,7 +172,7 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do
       let (result, nextTree) ← ProofTree.execute
         (stateId := args.stateId)
         (goalId := args.goalId.getD 0)
-        (tactic := args.tactic) |>.run tree
+        (tactic := args.tactic) |>.run state.options |>.run tree
       match result with
       | .invalid message => return Lean.toJson <| errorIndex message
       | .success nextId? goals =>

Pantograph/Commands.lean

@@ -17,9 +17,12 @@ structure Options where
   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
+  -- TODO: Not implemented yet.
   proofVariableDelta: Bool := false
   deriving Lean.ToJson
 
+abbrev OptionsT := ReaderT Options
+
 --- Expression Objects ---
 
 structure BoundExpression where
@@ -106,13 +109,13 @@ structure ClearResult where
   nTrees: Nat
   deriving Lean.ToJson
 
--- Get the type of an expression
-structure ExprType where
+-- Return the type of an expression
+structure ExprEcho where
   expr: String
   deriving Lean.FromJson
-structure ExprTypeResult where
-  type: String
-  roundTrip: String
+structure ExprEchoResult where
+  expr: Expression
+  type: Expression
   deriving Lean.ToJson
 
 structure ProofStart where

Pantograph/Serial.lean

@@ -53,10 +53,14 @@ def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := 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 -/
+/--
+ 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})"
+  | .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})"
@@ -73,38 +77,50 @@ def serialize_expression_ast (expr: Expr): MetaM String := do
     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'})"
+    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'})"
+    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'})"
+    return s!"(:let {name'} {type'} {value'} {body'})"
   | .lit v =>
-    return (match v with
+    -- 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}\"")
+      | .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 => "default"
-    | .implicit => "implicit"
-    | .strictImplicit => "strictImplicit"
-    | .instImplicit => "instImplicit"
+    | .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)

Pantograph/Tactic.lean

@@ -90,9 +90,9 @@ inductive TacticResult where
   | 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 := {}
+def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String):
+    Commands.OptionsT StateRefT ProofTree M TacticResult := do
+  let options ← read
   let tree ← get
   match tree.states.get? stateId with
   | .none => return .invalid s!"Invalid state id {stateId}"

README.md

@@ -73,7 +73,7 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
   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
+- `expr.echo {"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

Test/Integration.lean

@@ -0,0 +1,75 @@
+/- 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): Subroutine 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 (Subroutine 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: Subroutine 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"
+  subroutine_runner [
+    subroutine_step "inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp? }, module? }:
+      Commands.InspectResult)),
+    subroutine_step "options.set"
+      [("printExprAST", .bool true)]
+     (Lean.toJson ({ }:
+      Commands.OptionsSetResult)),
+    subroutine_step "inspect"
+      [("name", .str "Nat.add_one")]
+     (Lean.toJson ({
+       type := { pp?, sexp? }, module? }:
+      Commands.InspectResult)),
+    subroutine_step "options.print"
+      []
+     (Lean.toJson ({ 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

@@ -9,11 +9,10 @@ unsafe def main := do
   Lean.enableInitializersExecution
   Lean.initSearchPath (← Lean.findSysroot)
 
-	-- TODO: Add proper testing
   let suites := [
-    test_serial,
-    test_proofs
-    --test_integration
+    test_integration,
+    test_proofs,
+    test_serial
   ]
   let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
   LSpec.lspecIO $ all

Test/Proofs.lean

@@ -1,5 +1,5 @@
 import LSpec
-import Pantograph.Meta
+import Pantograph.Tactic
 import Pantograph.Serial
 
 namespace Pantograph.Test
@@ -47,13 +47,15 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
           (expr := expr)
         return (testSeq, Option.some state)
 
-deriving instance DecidableEq, Repr for Variable
-deriving instance DecidableEq, Repr for Goal
+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 TacticResult
 
+/-- Check the output of each proof step -/
 def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
     (expected: TacticResult) : TestM LSpec.TestSeq := do
-  let result: TacticResult ← ProofTree.execute stateId goalId tactic
+  let result: TacticResult ← ProofTree.execute stateId goalId tactic |>.run {}
   match expected, result with
   | .success (.some i) #[], .success (.some _) goals =>
     -- If the goals are omitted but the next state is specified, we imply that
@@ -63,6 +65,7 @@ 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)
@@ -90,20 +93,18 @@ def proof_runner (env: Lean.Environment) (start: Start) (steps: List (TestM LSpe
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
   | .ok a            => return a
 
-def build_goal (nameType: List (String × String)) (target: String): Goal :=
+def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
   {
-    target := target,
-    vars := (nameType.map fun x => ({ name := x.fst, type := x.snd }: Variable)).toArray
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      name := x.fst, type := { pp? := .some x.snd } })).toArray
   }
 
 example: ∀ (a b: Nat), a + b = b + a := by
   intro n m
   rw [Nat.add_comm]
 def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
-  let goal1: Goal := {
-    target := "n + m = m + n",
-    vars := #[{ name := "n", type := "Nat" }, { name := "m", type := "Nat" }]
-  }
+  let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
   proof_runner env (.copy "Nat.add_comm") [
     proof_step 0 0 "intro n m"
       (.success (.some 1) #[goal1]),
@@ -113,7 +114,7 @@ def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
       (.success .none #[])
   ]
 def proof_nat_add_comm_manual (env: Lean.Environment): IO LSpec.TestSeq := do
-  let goal1: Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
+  let goal1: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
   proof_runner env (.expr "∀ (a b: Nat), a + b = b + a") [
     proof_step 0 0 "intro n m"
       (.success (.some 1) #[goal1]),
@@ -139,13 +140,14 @@ example: ∀ (p q: Prop), p ∨ q → q ∨ p := by
   . apply Or.inl
     assumption
 def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
-  let branchGoal (caseName name: String): Goal := {
+  let typeProp: Commands.Expression := { pp? := .some "Prop" }
+  let branchGoal (caseName name: String): Commands.Goal := {
     caseName? := .some caseName,
-    target := "q ∨ p",
+    target := { pp? := .some "q ∨ p" },
     vars := #[
-      { name := "p", type := "Prop" },
-      { name := "q", type := "Prop" },
-      { name := "h✝", type := name, isInaccessible := true }
+      { name := "p", type := typeProp },
+      { name := "q", type := typeProp },
+      { name := "h✝", type := { pp? := .some name }, isInaccessible := true }
     ]
   }
   proof_runner env (.expr "∀ (p q: Prop), p ∨ q → q ∨ p") [

Test/Serial.lean

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