From d705cdf0e52e467dbbb8f6406ea474e430e70f4f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 13 Aug 2023 21:19:06 -0700 Subject: [PATCH] version bump, restructure --- Main.lean | 213 +++------------------------------------ Pantograph.lean | 207 +++++++++++++++++++++++++++++++++++++ Pantograph/Commands.lean | 13 ++- Pantograph/Serial.lean | 60 +++++++++++ Pantograph/Version.lean | 5 + README.md | 4 +- Test/Main.lean | 3 +- lean-toolchain | 2 +- 8 files changed, 304 insertions(+), 203 deletions(-) create mode 100644 Pantograph/Version.lean diff --git a/Main.lean b/Main.lean index c08014d..012ee4b 100644 --- a/Main.lean +++ b/Main.lean @@ -1,173 +1,8 @@ import Lean.Data.Json import Lean.Environment -import Pantograph.Commands -import Pantograph.Serial -import Pantograph.Meta -import Pantograph.Symbols - -namespace Pantograph - - -structure Context where - -/-- Stores state of the REPL -/ -structure State where - --environments: Array Lean.Environment := #[] - proofTrees: Array ProofTree := #[] - --- State monad -abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM) - -open Commands - -/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ -def parse_command (s: String): Except String Command := do - let s := s.trim - match s.get? 0 with - | .some '{' => -- Parse in Json mode - Lean.fromJson? (← Lean.Json.parse s) - | .some _ => -- Parse in line mode - let offset := s.posOf ' ' |> s.offsetOfPos - if offset = s.length then - return { cmd := s.take offset, payload := Lean.Json.null } - else - let payload ← s.drop offset |> Lean.Json.parse - 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" => - match Lean.fromJson? command.payload with - | .ok args => catalog args - | .error x => return errorJson x - | "inspect" => - match Lean.fromJson? command.payload with - | .ok args => inspect args - | .error x => return errorJson x - | "clear" => clear - | "expr.type" => - match Lean.fromJson? command.payload with - | .ok args => expr_type args - | .error x => return errorJson x - | "proof.start" => - match Lean.fromJson? command.payload with - | .ok args => proof_start args - | .error x => return errorJson x - | "proof.tactic" => - match Lean.fromJson? command.payload with - | .ok args => proof_tactic args - | .error x => return errorJson x - | "proof.printTree" => - match Lean.fromJson? command.payload with - | .ok args => proof_print_tree args - | .error x => return errorJson x - | cmd => - let error: InteractionError := { error := "unknown", desc := s!"Unknown command {cmd}" } - return Lean.toJson error - where - errorI (type desc: String) := Lean.toJson ({ error := type, desc := desc }: InteractionError) - errorJson := errorI "json" - errorIndex := errorI "index" - catalog (_: Catalog): Subroutine Lean.Json := do - let env ← Lean.MonadEnv.getEnv - let names := env.constants.fold (init := #[]) (λ acc name info => - match to_filtered_symbol name info with - | .some x => acc.push x - | .none => acc) - return Lean.toJson <| ({ symbols := names }: CatalogResult) - inspect (args: Inspect): Subroutine Lean.Json := do - let env ← Lean.MonadEnv.getEnv - let name := str_to_name args.name - let info? := env.find? name - match info? with - | none => return errorIndex s!"Symbol not found {args.name}" - | some info => - 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) - clear : Subroutine Lean.Json := do - let state ← get - let nTrees := state.proofTrees.size - set { state with proofTrees := #[] } - return Lean.toJson ({ nTrees := nTrees }: ClearResult) - expr_type (args: ExprType): Subroutine Lean.Json := do - let env ← Lean.MonadEnv.getEnv - match syntax_from_str env args.expr with - | .error str => return errorI "parsing" str - | .ok syn => do - match (← syntax_to_expr syn) with - | .error str => return errorI "elab" str - | .ok expr => do - try - let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr) - return Lean.toJson <| ({ - type := toString format, - roundTrip := toString <| (← Lean.Meta.ppExpr expr) - }: ExprTypeResult) - catch exception => - return errorI "typing" (← exception.toMessageData.toString) - proof_start (args: ProofStart): Subroutine Lean.Json := do - let state ← get - let env ← Lean.MonadEnv.getEnv - let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with - | .some expr, .none => - (match syntax_from_str env expr with - | .error str => return .error <| errorI "parsing" str - | .ok syn => do - (match (← syntax_to_expr syn) with - | .error str => return .error <| errorI "elab" str - | .ok expr => return .ok expr)) - | .none, .some copyFrom => - (match env.find? <| str_to_name copyFrom with - | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" - | .some cInfo => return .ok cInfo.type) - | .none, .none => - return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied" - | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}") - match expr? with - | .error error => return error - | .ok 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 } - return Lean.toJson ({ treeId := nextTreeId }: ProofStartResult) - proof_tactic (args: ProofTactic): Subroutine Lean.Json := do - let state ← get - match state.proofTrees.get? args.treeId with - | .none => return errorIndex "Invalid tree index {args.treeId}" - | .some tree => - let (result, nextTree) ← ProofTree.execute - (stateId := args.stateId) - (goalId := args.goalId.getD 0) - (tactic := args.tactic) |>.run tree - match result with - | .invalid message => return Lean.toJson <| errorIndex message - | .success nextId? goals => - set { state with proofTrees := state.proofTrees.set! args.treeId nextTree } - return Lean.toJson ({ nextId? := nextId?, goals := goals }: ProofTacticResultSuccess) - | .failure messages => - return Lean.toJson ({ tacticErrors := messages }: ProofTacticResultFailure) - proof_print_tree (args: ProofPrintTree): Subroutine Lean.Json := do - let state ← get - match state.proofTrees.get? args.treeId with - | .none => return errorIndex "Invalid tree index {args.treeId}" - | .some tree => - return Lean.toJson ({parents := tree.structure_array}: ProofPrintTreeResult) - - -end Pantograph - +import Pantograph.Version +import Pantograph -- Main IO functions open Pantograph @@ -184,38 +19,22 @@ 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 + -- NOTE: A more sophisticated scheme of command line argument handling is needed. + -- Separate imports and options + if args == ["--version"] then do + println! s!"{version}" + return + 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 options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) + |>.foldlM Lean.setOptionFromString'' Lean.Options.empty + |>.run + let options ← match options? with + | .ok options => pure options + | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}" let imports:= args.filter (λ s => ¬ (s.startsWith "--")) let env ← Lean.importModules @@ -225,11 +44,11 @@ unsafe def main (args: List String): IO Unit := do let context: Context := { } let coreContext: Lean.Core.Context := { - currNamespace := str_to_name "Aniva", + currNamespace := Lean.Name.str .anonymous "Aniva" openDecls := [], -- No 'open' directives needed fileName := "", fileMap := { source := "", positions := #[0], lines := #[1] }, - options := ← options.foldlM Lean.setOptionFromString' Lean.Options.empty + options := options } try let termElabM := loop.run context |>.run' {} diff --git a/Pantograph.lean b/Pantograph.lean index cd13b6f..045d28a 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,2 +1,209 @@ import Pantograph.Commands +import Pantograph.Serial +import Pantograph.Meta import Pantograph.Symbols + +namespace Lean +-- This is better than the default version since it handles `.` and doesn't +-- crash the program when it fails. +def setOptionFromString'' (opts : Options) (entry : String) : ExceptT String IO Options := do + let ps := (entry.splitOn "=").map String.trim + let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form ' = '" + let key := Pantograph.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 s!"invalid Bool option value '{val}'" + | DataValue.ofName _ => pure $ opts.setName key val.toName + | DataValue.ofNat _ => + match val.toNat? with + | none => throw s!"invalid Nat option value '{val}'" + | some v => pure $ opts.setNat key v + | DataValue.ofInt _ => + match val.toInt? with + | none => throw s!"invalid Int option value '{val}'" + | some v => pure $ opts.setInt key v + | DataValue.ofSyntax _ => throw s!"invalid Syntax option value" +end Lean + +namespace Pantograph + +structure Context where + +/-- Stores state of the REPL -/ +structure State where + --environments: Array Lean.Environment := #[] + proofTrees: Array ProofTree := #[] + +-- State monad +abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM) + +/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ +def parse_command (s: String): Except String Commands.Command := do + let s := s.trim + match s.get? 0 with + | .some '{' => -- Parse in Json mode + Lean.fromJson? (← Lean.Json.parse s) + | .some _ => -- Parse in line mode + let offset := s.posOf ' ' |> s.offsetOfPos + if offset = s.length then + return { cmd := s.take offset, payload := Lean.Json.null } + else + let payload ← s.drop offset |> Lean.Json.parse + return { cmd := s.take offset, payload := payload } + | .none => throw "Command is empty" + +def execute (command: Commands.Command): Subroutine Lean.Json := do + match command.cmd with + | "option.set" => + match Lean.fromJson? command.payload with + | .ok args => option_set args + | .error x => return errorJson x + | "catalog" => + match Lean.fromJson? command.payload with + | .ok args => catalog args + | .error x => return errorJson x + | "inspect" => + match Lean.fromJson? command.payload with + | .ok args => inspect args + | .error x => return errorJson x + | "clear" => clear + | "expr.type" => + match Lean.fromJson? command.payload with + | .ok args => expr_type args + | .error x => return errorJson x + | "proof.start" => + match Lean.fromJson? command.payload with + | .ok args => proof_start args + | .error x => return errorJson x + | "proof.tactic" => + match Lean.fromJson? command.payload with + | .ok args => proof_tactic args + | .error x => return errorJson x + | "proof.printTree" => + match Lean.fromJson? command.payload with + | .ok args => proof_print_tree args + | .error x => return errorJson x + | cmd => + let error: Commands.InteractionError := + { error := "unknown", desc := s!"Unknown command {cmd}" } + return Lean.toJson error + where + errorI (type desc: String) := Lean.toJson ( + { error := type, desc := desc }: Commands.InteractionError) + errorJson := errorI "json" + errorIndex := errorI "index" + option_set (args: Commands.OptionSet): Subroutine Lean.Json := do + let options? ← args.options.foldlM Lean.setOptionFromString'' Lean.Options.empty + |>.run + match options? with + | .ok options => + withTheReader Lean.Core.Context + (λ coreContext => { coreContext with options }) + (pure $ Lean.toJson <| ({ }: Commands.OptionSetResult)) + | .error e => + return errorI "parsing" e + catalog (_: Commands.Catalog): Subroutine Lean.Json := do + let env ← Lean.MonadEnv.getEnv + let names := env.constants.fold (init := #[]) (λ acc name info => + match to_filtered_symbol name info with + | .some x => acc.push x + | .none => acc) + return Lean.toJson <| ({ symbols := names }: Commands.CatalogResult) + inspect (args: Commands.Inspect): Subroutine Lean.Json := do + let env ← Lean.MonadEnv.getEnv + let name := str_to_name args.name + let info? := env.find? name + match info? with + | none => return errorIndex s!"Symbol not found {args.name}" + | some info => + 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 Option.none -- TODO: Temporary override, enable expression dissection in options. + -- return .some (← type_expr_to_bound info.toConstantVal.type) + | _ => return Option.none) + return Lean.toJson ({ + type := toString format, + boundExpr? := boundExpr?, + module? := module? + }: Commands.InspectResult) + clear : Subroutine Lean.Json := do + let state ← get + 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 + let env ← Lean.MonadEnv.getEnv + match syntax_from_str env args.expr with + | .error str => return errorI "parsing" str + | .ok syn => do + match (← syntax_to_expr syn) with + | .error str => return errorI "elab" str + | .ok expr => do + try + let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr) + return Lean.toJson <| ({ + type := toString format, + roundTrip := toString <| (← Lean.Meta.ppExpr expr) + }: Commands.ExprTypeResult) + catch exception => + return errorI "typing" (← exception.toMessageData.toString) + proof_start (args: Commands.ProofStart): Subroutine Lean.Json := do + let state ← get + let env ← Lean.MonadEnv.getEnv + let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with + | .some expr, .none => + (match syntax_from_str env expr with + | .error str => return .error <| errorI "parsing" str + | .ok syn => do + (match (← syntax_to_expr syn) with + | .error str => return .error <| errorI "elab" str + | .ok expr => return .ok expr)) + | .none, .some copyFrom => + (match env.find? <| str_to_name copyFrom with + | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" + | .some cInfo => return .ok cInfo.type) + | .none, .none => + return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied" + | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}") + match expr? with + | .error error => return error + | .ok 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 } + return Lean.toJson ({ treeId := nextTreeId }: Commands.ProofStartResult) + proof_tactic (args: Commands.ProofTactic): Subroutine Lean.Json := do + let state ← get + match state.proofTrees.get? args.treeId with + | .none => return errorIndex "Invalid tree index {args.treeId}" + | .some tree => + let (result, nextTree) ← ProofTree.execute + (stateId := args.stateId) + (goalId := args.goalId.getD 0) + (tactic := args.tactic) |>.run tree + match result with + | .invalid message => return Lean.toJson <| errorIndex message + | .success nextId? goals => + set { state with proofTrees := state.proofTrees.set! args.treeId nextTree } + return Lean.toJson ( + { nextId? := nextId?, goals := goals }: Commands.ProofTacticResultSuccess) + | .failure messages => + return Lean.toJson ( + { tacticErrors := messages }: Commands.ProofTacticResultFailure) + proof_print_tree (args: Commands.ProofPrintTree): Subroutine Lean.Json := do + let state ← get + match state.proofTrees.get? args.treeId with + | .none => return errorIndex "Invalid tree index {args.treeId}" + | .some tree => + return Lean.toJson ({parents := tree.structure_array}: Commands.ProofPrintTreeResult) + + +end Pantograph diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 4ad79b5..0b08303 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -21,7 +21,16 @@ structure InteractionError where deriving Lean.ToJson --- Individual command and return types +--- Individual command and return types --- + +-- Set Lean options supplied in the form of +-- +-- option=value +structure OptionSet where + options: Array String + deriving Lean.FromJson +structure OptionSetResult where + deriving Lean.ToJson -- Print all symbols in environment @@ -38,7 +47,7 @@ structure Inspect where structure InspectResult where type: String -- Decompose the bound expression when the type is forall. - boundExpr?: Option BoundExpression + boundExpr?: Option BoundExpression := Option.none module?: Option String deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 0d1c2d6..0851c4c 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -117,4 +117,64 @@ def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do vars := vars.reverse.toArray } +/-- 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})" + | .fvar fvarId => + let name := (← fvarId.getDecl).userName + return s!"(:fv {name})" + | .mvar _ => + -- mvarId is ignored. + return s!":mv" + | .sort u => return s!"(:sort {u.depth})" + | .const declName _ => + -- The universe level of the const expression is elided since it should be + -- inferrable from surrounding expression + return s!"(:const {declName})" + | .app fn arg => + let fn' ← serialize_expression_ast fn + let arg' ← serialize_expression_ast arg + return s!"(:app {fn'} {arg'})" + | .lam binderName binderType body binderInfo => + let binderType' ← serialize_expression_ast binderType + let body' ← serialize_expression_ast body + let binderInfo' := binderInfoToAst binderInfo + return s!"(:lam {binderName} {binderType'} {body'} :{binderInfo'})" + | .forallE binderName binderType body binderInfo => + let binderType' ← serialize_expression_ast binderType + let body' ← serialize_expression_ast body + let binderInfo' := binderInfoToAst binderInfo + return s!"(:forall {binderName} {binderType'} {body'} :{binderInfo'})" + | .letE name type value body _ => + -- Dependent boolean flag diacarded + 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'})" + | .lit v => + return (match v with + | .natVal val => toString val + | .strVal val => s!"\"{val}\"") + | .mdata _ expr => + -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter + return (← serialize_expression_ast expr) + | .proj typeName idx struct => + let struct' ← serialize_expression_ast struct + return s!"(:proj {typeName} {idx} {struct'})" + + where + binderInfoToAst : Lean.BinderInfo → String + | .default => "default" + | .implicit => "implicit" + | .strictImplicit => "strictImplicit" + | .instImplicit => "instImplicit" + +/-- Serialised expression object --/ +structure Expression where + prettyprinted?: Option String := .none + bound?: Option BoundExpression := .none + sexp?: Option String := .none + deriving ToJson + end Pantograph diff --git a/Pantograph/Version.lean b/Pantograph/Version.lean new file mode 100644 index 0000000..d667eb3 --- /dev/null +++ b/Pantograph/Version.lean @@ -0,0 +1,5 @@ +namespace Pantograph + +def version := "0.2" + +end Pantograph diff --git a/README.md b/README.md index 68ea647..1bb7f32 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantogr ## Usage ``` sh -build/bin/pantograph OPTIONS|MODULES +build/bin/pantograph MODULES|LEAN_OPTIONS ``` The REPL loop accepts commands as single-line JSON inputs and outputs either an @@ -37,7 +37,7 @@ The list of available commands can be found in `Pantograph/Commands.lean`. An empty command aborts the REPL. The `Pantograph` executable must be run with a list of modules to import. It can -also accept options of the form `--key=value` e.g. `--pp.raw=true`. +also accept lean options of the form `--key=value` e.g. `--pp.raw=true`. Example: (~5k symbols) ``` diff --git a/Test/Main.lean b/Test/Main.lean index 22d8984..54b2cb9 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,5 +1,5 @@ import LSpec -import Pantograph.Symbols +import Test.Integration import Test.Proofs import Test.Serial @@ -12,6 +12,7 @@ unsafe def main := do let suites := [ test_serial, test_proofs + --test_integration ] let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done LSpec.lspecIO $ all diff --git a/lean-toolchain b/lean-toolchain index a7041bc..1acfb77 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-05-06 +leanprover/lean4:nightly-2023-08-12