From d476354a4a201a1aac438f723a32ef41dc8a6669 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 14 Aug 2023 21:43:40 -0700 Subject: [PATCH] Add expression sexp printing (2/2) --- Pantograph.lean | 19 +++---- Pantograph/Commands.lean | 13 +++-- Pantograph/Serial.lean | 38 ++++++++++---- Pantograph/{Meta.lean => Tactic.lean} | 6 +-- README.md | 2 +- Test/Integration.lean | 75 +++++++++++++++++++++++++++ Test/Main.lean | 7 ++- Test/Proofs.lean | 36 +++++++------ Test/Serial.lean | 42 ++++++++++++--- 9 files changed, 182 insertions(+), 56 deletions(-) rename Pantograph/{Meta.lean => Tactic.lean} (97%) create mode 100644 Test/Integration.lean diff --git a/Pantograph.lean b/Pantograph.lean index 086651f..e7c2c59 100644 --- a/Pantograph.lean +++ b/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 => diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 2212f96..45eca35 100644 --- a/Pantograph/Commands.lean +++ b/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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 3daf93a..67fb107 100644 --- a/Pantograph/Serial.lean +++ b/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) diff --git a/Pantograph/Meta.lean b/Pantograph/Tactic.lean similarity index 97% rename from Pantograph/Meta.lean rename to Pantograph/Tactic.lean index 09f6d93..c051f3c 100644 --- a/Pantograph/Meta.lean +++ b/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}" diff --git a/README.md b/README.md index 46d818d..309303b 100644 --- a/README.md +++ b/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": }`: Determine the type of an expression and round-trip it +- `expr.echo {"expr": }`: Determine the type of an expression and round-trip it - `proof.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol - `proof.tactic {"treeId": , "stateId": , "goalId": , "tactic": string}`: Execute a tactic on a given proof state - `proof.printTree {"treeId": }`: Print the topological structure of a proof tree diff --git a/Test/Integration.lean b/Test/Integration.lean new file mode 100644 index 0000000..d22eadf --- /dev/null +++ b/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 := "", + 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 diff --git a/Test/Main.lean b/Test/Main.lean index 9bf8e8a..84d686d 100644 --- a/Test/Main.lean +++ b/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 diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 52854d4..9df7c84 100644 --- a/Test/Proofs.lean +++ b/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") [ diff --git a/Test/Serial.lean b/Test/Serial.lean index febf489..f84e3e4 100644 --- a/Test/Serial.lean +++ b/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 := "", + fileName := "", 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 := "", + 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