From fd536da55ca798cd67ba1b7bdeeddbfed80b6482 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 24 May 2023 00:54:48 -0700 Subject: [PATCH] Add expression binding printing and import Lean --- Main.lean | 51 +++++++++++++++++++++++------ Pantograph/Commands.lean | 4 +++ Pantograph/Meta.lean | 70 +++++++++++++++++----------------------- Pantograph/Serial.lean | 41 +++++++++++++++++------ Test/Proofs.lean | 20 ++++++------ Test/Serial.lean | 35 +++++++++++++++++++- 6 files changed, 151 insertions(+), 70 deletions(-) diff --git a/Main.lean b/Main.lean index 4593164..7db7233 100644 --- a/Main.lean +++ b/Main.lean @@ -14,7 +14,7 @@ structure Context where /-- Stores state of the REPL -/ structure State where --environments: Array Lean.Environment := #[] - proofTrees: Array Meta.ProofTree := #[] + proofTrees: Array ProofTree := #[] -- State monad abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM) @@ -36,8 +36,6 @@ def parse_command (s: String): Except String Command := do 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" => @@ -83,8 +81,12 @@ def execute (command: Command): Subroutine Lean.Json := do 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) proof_start (args: ProofStart): Subroutine Lean.Json := do @@ -92,10 +94,10 @@ def execute (command: Command): Subroutine Lean.Json := do let env ← Lean.MonadEnv.getEnv let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with | .some expr, .none => - (match Serial.syntax_from_str env expr with + (match syntax_from_str env expr with | .error str => return .error <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError) | .ok syn => do - (match (← Meta.syntax_to_expr syn) with + (match (← syntax_to_expr syn) with | .error str => return .error <| Lean.toJson ({ error := "elab", desc := str }: InteractionError) | .ok expr => return .ok expr)) | .none, .some copyFrom => @@ -108,7 +110,7 @@ def execute (command: Command): Subroutine Lean.Json := do match expr? with | .error error => return error | .ok expr => - let tree ← Meta.ProofTree.create (str_to_name <| args.name.getD "Untitled") 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 } @@ -118,7 +120,7 @@ def execute (command: Command): Subroutine Lean.Json := do match state.proofTrees.get? args.treeId with | .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}" | .some tree => - let (result, nextTree) ← Meta.ProofTree.execute + let (result, nextTree) ← ProofTree.execute (stateId := args.stateId) (goalId := args.goalId.getD 0) (tactic := args.tactic) |>.run tree @@ -155,12 +157,42 @@ 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 ' = '" + 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 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 imports:= args.filter (λ s => ¬ (s.startsWith "--")) + let env ← Lean.importModules - (imports := args.map (λ str => { module := str_to_name str, runtimeOnly := false })) + (imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false })) (opts := {}) (trustLevel := 1) let context: Context := { @@ -169,7 +201,8 @@ unsafe def main (args: List String): IO Unit := do currNamespace := str_to_name "Aniva", openDecls := [], -- No 'open' directives needed fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] } + fileMap := { source := "", positions := #[0], lines := #[1] }, + options := ← options.foldlM Lean.setOptionFromString' Lean.Options.empty } try let termElabM := loop.run context |>.run' {} diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 9d87942..51d08fd 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -1,6 +1,8 @@ -- All the command input/output structures are stored here import Lean.Data.Json +import Pantograph.Serial + namespace Pantograph.Commands structure Command where @@ -30,6 +32,8 @@ structure Inspect where deriving Lean.FromJson structure InspectResult where type: String + -- Decompose the bound expression when the type is forall. + boundExpr?: Option BoundExpression module?: Option String deriving Lean.ToJson diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean index 736ba73..9072195 100644 --- a/Pantograph/Meta.lean +++ b/Pantograph/Meta.lean @@ -7,38 +7,39 @@ import Pantograph.Symbols The proof state manipulation system A proof state is launched by providing -1. Environment: `Lean.Environment` -2. Expression: `Lean.Expr` +1. Environment: `Environment` +2. Expression: `Expr` The expression becomes the first meta variable in the saved tactic state -`Lean.Elab.Tactic.SavedState`. +`Elab.Tactic.SavedState`. From this point on, any proof which extends -`Lean.Elab.Term.Context` and +`Elab.Term.Context` and -/ -def Lean.MessageLog.getErrorMessages (log : Lean.MessageLog) : Lean.MessageLog := -{ msgs := log.msgs.filter fun m => match m.severity with | Lean.MessageSeverity.error => true | _ => false } +def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := +{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false } -namespace Pantograph.Meta +namespace Pantograph +open Lean structure ProofState where - goals : List Lean.MVarId - savedState : Lean.Elab.Tactic.SavedState + goals : List MVarId + savedState : Elab.Tactic.SavedState parent : Option Nat := none parentGoalId : Nat := 0 structure ProofTree where -- All parameters needed to run a `TermElabM` monad - name: Lean.Name + name: Name -- Set of proof states states : Array ProofState := #[] -abbrev M := Lean.Elab.TermElabM +abbrev M := Elab.TermElabM -def ProofTree.create (name: Lean.Name) (expr: Lean.Expr): M ProofTree := do - let expr ← Lean.instantiateMVars expr - let goal := (← Lean.Meta.mkFreshExprMVar expr (kind := Lean.MetavarKind.synthetic)) - let savedStateMonad: Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.SavedState := Lean.MonadBacktrack.saveState +def ProofTree.create (name: Name) (expr: Expr): M ProofTree := do + let expr ← instantiateMVars expr + let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic)) + let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]} return { name := name, @@ -54,42 +55,31 @@ def ProofTree.structure_array (tree: ProofTree): Array String := | .none => "" | .some parent => s!"{parent}.{state.parentGoalId}" --- Parsing syntax under the environment -def syntax_to_expr (syn: Lean.Syntax): Lean.Elab.TermElabM (Except String Lean.Expr) := do - try - let expr ← Lean.Elab.Term.elabType syn - -- Immediately synthesise all metavariables if we need to leave the elaboration context. - -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 - --Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing - let expr ← Lean.instantiateMVars expr - return .ok expr - catch ex => return .error (← ex.toMessageData.toString) - -def execute_tactic (state: Lean.Elab.Tactic.SavedState) (goal: Lean.MVarId) (tactic: String) : - M (Except (Array String) (Lean.Elab.Tactic.SavedState × List Lean.MVarId)):= do - let tacticM (stx: Lean.Syntax): Lean.Elab.Tactic.TacticM (Except (Array String) (Lean.Elab.Tactic.SavedState × List Lean.MVarId)) := do +def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) : + M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do + let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do state.restore - Lean.Elab.Tactic.setGoals [goal] + Elab.Tactic.setGoals [goal] try - Lean.Elab.Tactic.evalTactic stx - if (← getThe Lean.Core.State).messages.hasErrors then - let messages := (← getThe Lean.Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString + Elab.Tactic.evalTactic stx + if (← getThe Core.State).messages.hasErrors then + let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray + let errors ← (messages.map Message.data).mapM fun md => md.toString return .error errors else - return .ok (← Lean.MonadBacktrack.saveState, ← Lean.Elab.Tactic.getUnsolvedGoals) + return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals) catch exception => return .error #[← exception.toMessageData.toString] - match Lean.Parser.runParserCategory - (env := ← Lean.MonadEnv.getEnv) + match Parser.runParserCategory + (env := ← MonadEnv.getEnv) (catName := `tactic) (input := tactic) (fileName := "") with | Except.error err => return .error #[err] | Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic -def goals_to_string (goals: List Lean.MVarId): M (Array String) := do - let goals ← goals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g) +def goals_to_string (goals: List MVarId): M (Array String) := do + let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g) pure goals.toArray @@ -128,4 +118,4 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P modify fun s => { s with states := s.states.push proofState } return .success (.some nextId) (← goals_to_string nextGoals) -end Pantograph.Meta +end Pantograph diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 67393f7..8304665 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -1,23 +1,44 @@ +/- +All serialisation functions +-/ import Lean -/- -Expression IO --/ - - -namespace Pantograph.Serial +namespace Pantograph +open Lean /-- Read a theorem from the environment -/ -def expr_from_const (env: Lean.Environment) (name: Lean.Name): Except String Lean.Expr := +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 -def syntax_from_str (env: Lean.Environment) (s: String): Except String Lean.Syntax := - Lean.Parser.runParserCategory +def syntax_from_str (env: Environment) (s: String): Except String Syntax := + Parser.runParserCategory (env := env) (catName := `term) (input := s) (fileName := "") -end Pantograph.Serial + +def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do + try + let expr ← Elab.Term.elabType syn + -- Immediately synthesise all metavariables if we need to leave the elaboration context. + -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070 + --Elab.Term.synthesizeSyntheticMVarsNoPostponing + let expr ← instantiateMVars expr + 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 + 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) } + + +end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 0e401fa..46c8c6a 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -4,15 +4,15 @@ import Pantograph.Serial namespace Pantograph.Test open Pantograph +open Lean inductive Start where | copy (name: String) -- Start from some name in the environment | expr (expr: String) -- Start from some expression -abbrev M := Meta.M -abbrev TestM := StateRefT Meta.ProofTree M +abbrev TestM := StateRefT ProofTree M -def start_proof (start: Start): M (LSpec.TestSeq × Option Meta.ProofTree) := do +def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do let env ← Lean.MonadEnv.getEnv let mut testSeq := LSpec.TestSeq.done match start with @@ -21,37 +21,37 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option Meta.ProofTree) := do testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome match cInfo? with | .some cInfo => - let state ← Meta.ProofTree.create + let state ← ProofTree.create (name := str_to_name "TestExample") (expr := cInfo.type) return (testSeq, Option.some state) | .none => return (testSeq, Option.none) | .expr expr => - let syn? := Serial.syntax_from_str env expr + let syn? := syntax_from_str env expr testSeq := testSeq ++ LSpec.check s!"Parsing {expr}" (syn?.isOk) match syn? with | .error error => IO.println error return (testSeq, Option.none) | .ok syn => - let expr? ← Meta.syntax_to_expr syn + let expr? ← syntax_to_expr syn testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk match expr? with | .error error => IO.println error return (testSeq, Option.none) | .ok expr => - let state ← Meta.ProofTree.create + let state ← ProofTree.create (name := str_to_name "TestExample") (expr := expr) return (testSeq, Option.some state) -deriving instance DecidableEq, Repr for Meta.TacticResult +deriving instance DecidableEq, Repr for TacticResult def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) - (expected: Meta.TacticResult) : TestM LSpec.TestSeq := do - let result: Meta.TacticResult ← Meta.ProofTree.execute stateId goalId tactic + (expected: TacticResult) : TestM LSpec.TestSeq := do + let result: TacticResult ← ProofTree.execute stateId goalId tactic match expected, result with | .success (.some i) #[], .success (.some _) goals => -- If the goals are omitted but the next state is specified, we imply that diff --git a/Test/Serial.lean b/Test/Serial.lean index ce4114a..febf489 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -1,10 +1,43 @@ import LSpec +import Pantograph.Serial import Pantograph.Symbols namespace Pantograph.Test +open Pantograph +open Lean + +deriving instance Repr, DecidableEq for BoundExpression + +def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do + let cases: List (String × 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 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", + 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 })) + (opts := {}) + (trustLevel := 1) + return LSpec.group "Serialisation" $ - LSpec.test "Symbol parsing" (Lean.Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run") + (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") end Pantograph.Test