diff --git a/Main.lean b/Main.lean index de73033..eb5240d 100644 --- a/Main.lean +++ b/Main.lean @@ -4,6 +4,7 @@ import Lean.Environment import Pantograph.Version import Pantograph.Library import Pantograph +import Repl -- Main IO functions open Pantograph diff --git a/Pantograph.lean b/Pantograph.lean index 004c63f..09327e8 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,4 +1,3 @@ -import Lean.Data.HashMap import Pantograph.Compile import Pantograph.Condensed import Pantograph.Environment @@ -6,224 +5,4 @@ import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol import Pantograph.Serial - -namespace Pantograph - -structure Context where - imports: List String - -/-- Stores state of the REPL -/ -structure State where - options: Protocol.Options := {} - nextId: Nat := 0 - goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty - -/-- Main state monad for executing commands -/ -abbrev MainM := ReaderT Context (StateT State Lean.CoreM) - --- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables --- certain monadic features in `MainM` -abbrev CR α := Except Protocol.InteractionError α - -def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := - metaM.run' -def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := - termElabM.run' (ctx := Condensed.elabContext) |>.run' - -def execute (command: Protocol.Command): MainM Lean.Json := do - let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := - match Lean.fromJson? command.payload with - | .ok args => do - match (← comm args) with - | .ok result => return Lean.toJson result - | .error ierror => return Lean.toJson ierror - | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" - match command.cmd with - | "reset" => run reset - | "stat" => run stat - | "expr.echo" => run expr_echo - | "env.catalog" => run env_catalog - | "env.inspect" => run env_inspect - | "env.add" => run env_add - | "options.set" => run options_set - | "options.print" => run options_print - | "goal.start" => run goal_start - | "goal.tactic" => run goal_tactic - | "goal.continue" => run goal_continue - | "goal.delete" => run goal_delete - | "goal.print" => run goal_print - | "compile.unit" => run compile_unit - | cmd => - let error: Protocol.InteractionError := - errorCommand s!"Unknown command {cmd}" - return Lean.toJson error - where - errorCommand := errorI "command" - errorIndex := errorI "index" - -- Command Functions - reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do - let state ← get - let nGoals := state.goalStates.size - set { state with nextId := 0, goalStates := Lean.HashMap.empty } - return .ok { nGoals } - stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do - let state ← get - let nGoals := state.goalStates.size - return .ok { nGoals } - env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do - let result ← Environment.catalog args - return .ok result - env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do - let state ← get - Environment.inspect args state.options - env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do - Environment.addDecl args - expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do - let state ← get - exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options) - options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do - let state ← get - let options := state.options - set { state with - options := { - -- FIXME: This should be replaced with something more elegant - printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, - printExprPretty := args.printExprPretty?.getD options.printExprPretty, - printExprAST := args.printExprAST?.getD options.printExprAST, - printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars, - noRepeat := args.noRepeat?.getD options.noRepeat, - printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, - printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps - automaticMode := args.automaticMode?.getD options.automaticMode, - } - } - return .ok { } - options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do - return .ok (← get).options - goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do - let state ← get - let env ← Lean.MonadEnv.getEnv - let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with - | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) - | .none, .some copyFrom => - (match env.find? <| copyFrom.toName with - | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" - | .some cInfo => return .ok (← GoalState.create cInfo.type)) - | _, _ => - return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") - match expr? with - | .error error => return .error error - | .ok goalState => - let stateId := state.nextId - set { state with - goalStates := state.goalStates.insert stateId goalState, - nextId := state.nextId + 1 - } - return .ok { stateId, root := goalState.root.name.toString } - goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do - let state ← get - let .some goalState := state.goalStates.find? args.stateId | - return .error $ errorIndex s!"Invalid state index {args.stateId}" - let .some goal := goalState.goals.get? args.goalId | - return .error $ errorIndex s!"Invalid goal index {args.goalId}" - let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do - match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with - | .some tactic, .none, .none, .none, .none => do - pure <| Except.ok <| ← goalState.tryTactic goal tactic - | .none, .some expr, .none, .none, .none => do - pure <| Except.ok <| ← goalState.tryAssign goal expr - | .none, .none, .some type, .none, .none => do - let binderName := args.binderName?.getD "" - pure <| Except.ok <| ← goalState.tryHave goal binderName type - | .none, .none, .none, .some pred, .none => do - pure <| Except.ok <| ← goalState.tryCalc goal pred - | .none, .none, .none, .none, .some true => do - pure <| Except.ok <| ← goalState.conv goal - | .none, .none, .none, .none, .some false => do - pure <| Except.ok <| ← goalState.convExit - | _, _, _, _, _ => - let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" - pure $ Except.error $ error - match nextGoalState? with - | .error error => return .error error - | .ok (.success nextGoalState) => do - let nextGoalState ← match state.options.automaticMode, args.conv? with - | true, .none => do - let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" - pure result - | true, .some true => pure nextGoalState - | true, .some false => do - let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" - let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals" - pure result - | false, _ => pure nextGoalState - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert state.nextId nextGoalState, - nextId := state.nextId + 1, - } - let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' - return .ok { - nextStateId? := .some nextStateId, - goals? := .some goals, - } - | .ok (.parseError message) => - return .ok { parseError? := .some message } - | .ok (.invalidAction message) => - return .error $ errorI "invalid" message - | .ok (.failure messages) => - return .ok { tacticErrors? := .some messages } - goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do - let state ← get - match state.goalStates.find? args.target with - | .none => return .error $ errorIndex s!"Invalid state index {args.target}" - | .some target => do - let nextState? ← match args.branch?, args.goals? with - | .some branchId, .none => do - match state.goalStates.find? branchId with - | .none => return .error $ errorIndex s!"Invalid state index {branchId}" - | .some branch => pure $ goalContinue target branch - | .none, .some goals => - pure $ goalResume target goals - | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" - match nextState? with - | .error error => return .error <| errorI "structure" error - | .ok nextGoalState => - let nextStateId := state.nextId - set { state with - goalStates := state.goalStates.insert nextStateId nextGoalState, - nextId := state.nextId + 1 - } - let goals ← goalSerialize nextGoalState (options := state.options) - return .ok { - nextStateId, - goals, - } - goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do - let state ← get - let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates - set { state with goalStates } - return .ok {} - goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do - let state ← get - match state.goalStates.find? args.stateId with - | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" - | .some goalState => runMetaM <| do - return .ok (← goalPrint goalState state.options) - compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do - let module := args.module.toName - try - let steps ← Compile.processSource module - let units? := if args.compilationUnits then - .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) - else - .none - let invocations? ← if args.invocations then - pure $ .some (← Compile.collectTacticsFromCompilation steps) - else - pure .none - return .ok { units?, invocations? } - catch e => - return .error $ errorI "compile" (← e.toMessageData.toString) - -end Pantograph +import Pantograph.Version diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7486103..225b8ac 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -307,7 +307,7 @@ protected def GoalState.convExit (state: GoalState): return .failure #[← exception.toMessageData.toString] protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do - let (mvarId, rhs ) ← state.calcPrevRhs? + let (mvarId, rhs) ← state.calcPrevRhs? if mvarId == goal then .some rhs else @@ -352,9 +352,8 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) (userName := tag ++ `calc) let mvarBranch := proof.mvarId! - let calcPrevRhs? := Option.some (goal, rhs) let mut proofType ← Meta.inferType proof - let mut remainder := Option.none + let mut remainder? := Option.none -- The calc tactic either solves the main goal or leaves another relation. -- Replace the main goal, and save the new goal if necessary @@ -367,10 +366,11 @@ protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String) let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep unless ← Meta.isDefEq proofType target do throwFailed - remainder := .some lastStepGoal.mvarId! + remainder? := .some lastStepGoal.mvarId! goal.assign proof - let goals := [ mvarBranch ] ++ remainder.toList + let goals := [ mvarBranch ] ++ remainder?.toList + let calcPrevRhs? := remainder?.map $ λ g => (g, rhs) return .success { root := state.root, savedState := { diff --git a/Repl.lean b/Repl.lean new file mode 100644 index 0000000..da594e3 --- /dev/null +++ b/Repl.lean @@ -0,0 +1,223 @@ +import Lean.Data.HashMap +import Pantograph + +namespace Pantograph + +structure Context where + imports: List String + +/-- Stores state of the REPL -/ +structure State where + options: Protocol.Options := {} + nextId: Nat := 0 + goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty + +/-- Main state monad for executing commands -/ +abbrev MainM := ReaderT Context (StateT State Lean.CoreM) + +-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables +-- certain monadic features in `MainM` +abbrev CR α := Except Protocol.InteractionError α + +def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α := + metaM.run' +def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α := + termElabM.run' (ctx := Condensed.elabContext) |>.run' + +def execute (command: Protocol.Command): MainM Lean.Json := do + let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := + match Lean.fromJson? command.payload with + | .ok args => do + match (← comm args) with + | .ok result => return Lean.toJson result + | .error ierror => return Lean.toJson ierror + | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" + match command.cmd with + | "reset" => run reset + | "stat" => run stat + | "expr.echo" => run expr_echo + | "env.catalog" => run env_catalog + | "env.inspect" => run env_inspect + | "env.add" => run env_add + | "options.set" => run options_set + | "options.print" => run options_print + | "goal.start" => run goal_start + | "goal.tactic" => run goal_tactic + | "goal.continue" => run goal_continue + | "goal.delete" => run goal_delete + | "goal.print" => run goal_print + | "compile.unit" => run compile_unit + | cmd => + let error: Protocol.InteractionError := + errorCommand s!"Unknown command {cmd}" + return Lean.toJson error + where + errorCommand := errorI "command" + errorIndex := errorI "index" + -- Command Functions + reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do + let state ← get + let nGoals := state.goalStates.size + set { state with nextId := 0, goalStates := Lean.HashMap.empty } + return .ok { nGoals } + stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do + let state ← get + let nGoals := state.goalStates.size + return .ok { nGoals } + env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do + let result ← Environment.catalog args + return .ok result + env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do + let state ← get + Environment.inspect args state.options + env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do + Environment.addDecl args + expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do + let state ← get + exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options) + options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do + let state ← get + let options := state.options + set { state with + options := { + -- FIXME: This should be replaced with something more elegant + printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, + printExprPretty := args.printExprPretty?.getD options.printExprPretty, + printExprAST := args.printExprAST?.getD options.printExprAST, + printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars, + noRepeat := args.noRepeat?.getD options.noRepeat, + printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, + printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps + automaticMode := args.automaticMode?.getD options.automaticMode, + } + } + return .ok { } + options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do + return .ok (← get).options + goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do + let state ← get + let env ← Lean.MonadEnv.getEnv + let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with + | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) + | .none, .some copyFrom => + (match env.find? <| copyFrom.toName with + | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" + | .some cInfo => return .ok (← GoalState.create cInfo.type)) + | _, _ => + return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied") + match expr? with + | .error error => return .error error + | .ok goalState => + let stateId := state.nextId + set { state with + goalStates := state.goalStates.insert stateId goalState, + nextId := state.nextId + 1 + } + return .ok { stateId, root := goalState.root.name.toString } + goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do + let state ← get + let .some goalState := state.goalStates.find? args.stateId | + return .error $ errorIndex s!"Invalid state index {args.stateId}" + let .some goal := goalState.goals.get? args.goalId | + return .error $ errorIndex s!"Invalid goal index {args.goalId}" + let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do + match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with + | .some tactic, .none, .none, .none, .none => do + pure <| Except.ok <| ← goalState.tryTactic goal tactic + | .none, .some expr, .none, .none, .none => do + pure <| Except.ok <| ← goalState.tryAssign goal expr + | .none, .none, .some type, .none, .none => do + let binderName := args.binderName?.getD "" + pure <| Except.ok <| ← goalState.tryHave goal binderName type + | .none, .none, .none, .some pred, .none => do + pure <| Except.ok <| ← goalState.tryCalc goal pred + | .none, .none, .none, .none, .some true => do + pure <| Except.ok <| ← goalState.conv goal + | .none, .none, .none, .none, .some false => do + pure <| Except.ok <| ← goalState.convExit + | _, _, _, _, _ => + let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied" + pure $ Except.error $ error + match nextGoalState? with + | .error error => return .error error + | .ok (.success nextGoalState) => do + let nextGoalState ← match state.options.automaticMode, args.conv? with + | true, .none => do + let .ok result := nextGoalState.resume goalState.goals | throwError "Resuming known goals" + pure result + | true, .some true => pure nextGoalState + | true, .some false => do + let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail" + let .ok result := nextGoalState.resume dormantGoals | throwError "Resuming known goals" + pure result + | false, _ => pure nextGoalState + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert state.nextId nextGoalState, + nextId := state.nextId + 1, + } + let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run' + return .ok { + nextStateId? := .some nextStateId, + goals? := .some goals, + } + | .ok (.parseError message) => + return .ok { parseError? := .some message } + | .ok (.invalidAction message) => + return .error $ errorI "invalid" message + | .ok (.failure messages) => + return .ok { tacticErrors? := .some messages } + goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do + let state ← get + match state.goalStates.find? args.target with + | .none => return .error $ errorIndex s!"Invalid state index {args.target}" + | .some target => do + let nextState? ← match args.branch?, args.goals? with + | .some branchId, .none => do + match state.goalStates.find? branchId with + | .none => return .error $ errorIndex s!"Invalid state index {branchId}" + | .some branch => pure $ goalContinue target branch + | .none, .some goals => + pure $ goalResume target goals + | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" + match nextState? with + | .error error => return .error <| errorI "structure" error + | .ok nextGoalState => + let nextStateId := state.nextId + set { state with + goalStates := state.goalStates.insert nextStateId nextGoalState, + nextId := state.nextId + 1 + } + let goals ← goalSerialize nextGoalState (options := state.options) + return .ok { + nextStateId, + goals, + } + goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do + let state ← get + let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates + set { state with goalStates } + return .ok {} + goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do + let state ← get + match state.goalStates.find? args.stateId with + | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" + | .some goalState => runMetaM <| do + return .ok (← goalPrint goalState state.options) + compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do + let module := args.module.toName + try + let steps ← Compile.processSource module + let units? := if args.compilationUnits then + .some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx) + else + .none + let invocations? ← if args.invocations then + pure $ .some (← Compile.collectTacticsFromCompilation steps) + else + pure .none + return .ok { units?, invocations? } + catch e => + return .error $ errorI "compile" (← e.toMessageData.toString) + +end Pantograph diff --git a/Test/Integration.lean b/Test/Integration.lean index 931c9f2..3ccff81 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -2,6 +2,8 @@ -/ import LSpec import Pantograph +import Repl + namespace Pantograph.Test.Integration open Pantograph diff --git a/flake.nix b/flake.nix index 088f306..70c84b5 100644 --- a/flake.nix +++ b/flake.nix @@ -37,14 +37,25 @@ }; project = leanPkgs.buildLeanPackage { name = "Pantograph"; - roots = [ "Main" "Pantograph" ]; - src = pkgs.lib.cleanSourceWith { + roots = [ "Pantograph" ]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { src = ./.; filter = path: type: !(pkgs.lib.hasInfix "/Test/" path) && !(pkgs.lib.hasSuffix ".md" path) && - !(pkgs.lib.hasSuffix "Makefile" path); - }; + !(pkgs.lib.hasSuffix "Repl.lean" path); + }); + }; + repl = leanPkgs.buildLeanPackage { + name = "Repl"; + roots = [ "Main" "Repl" ]; + deps = [ project ]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + !(pkgs.lib.hasInfix "/Test/" path) && + !(pkgs.lib.hasSuffix ".md" path); + }); }; test = leanPkgs.buildLeanPackage { name = "Test"; @@ -52,18 +63,19 @@ # root begins (e.g. `import Test.Environment` and not `import # Environment`) and thats where `lakefile.lean` resides. roots = [ "Test.Main" ]; - deps = [ lspecLib project ]; - src = pkgs.lib.cleanSourceWith { + deps = [ lspecLib repl ]; + src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith { src = ./.; filter = path: type: !(pkgs.lib.hasInfix "Pantograph" path); - }; + }); }; in rec { packages = { inherit (leanPkgs) lean lean-all; - inherit (project) sharedLib executable; - default = project.executable; + inherit (project) sharedLib; + inherit (repl) executable; + default = repl.executable; }; legacyPackages = { inherit project leanPkgs; diff --git a/lakefile.lean b/lakefile.lean index c68d0db..e29fa0e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -4,11 +4,14 @@ open Lake DSL package pantograph lean_lib Pantograph { + roots := #[`Pantograph] defaultFacets := #[LeanLib.sharedFacet] } +lean_lib Repl { +} @[default_target] -lean_exe pantograph { +lean_exe repl { root := `Main -- Solves the native symbol not found problem supportInterpreter := true