Add expression sexp printing (2/2)

This commit is contained in:
Leni Aniva 2023-08-14 21:43:40 -07:00
parent 19c57ada1e
commit d476354a4a
9 changed files with 182 additions and 56 deletions

View File

@ -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 =>

View File

@ -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

View File

@ -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)

View File

@ -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}"

View File

@ -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

75
Test/Integration.lean Normal file
View File

@ -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

View File

@ -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

View File

@ -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") [

View File

@ -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