From 19c57ada1e7856e59dcbf2bb84f01dc14cecc0d3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 14 Aug 2023 17:07:53 -0700 Subject: [PATCH] Add expression sexp printing (1/2, tests pending) --- Main.lean | 33 +++++++- Pantograph.lean | 75 +++++++------------ Pantograph/Commands.lean | 73 +++++++++++++++--- Pantograph/Meta.lean | 10 ++- Pantograph/Serial.lean | 158 +++++++++++++++++++-------------------- README.md | 10 ++- Test/Main.lean | 1 + 7 files changed, 214 insertions(+), 146 deletions(-) diff --git a/Main.lean b/Main.lean index 012ee4b..9b8bedb 100644 --- a/Main.lean +++ b/Main.lean @@ -19,6 +19,36 @@ unsafe def loop : Subroutine Unit := do IO.println <| toString <| ret loop +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 + + 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 @@ -30,7 +60,7 @@ unsafe def main (args: List String): IO Unit := do Lean.initSearchPath (← Lean.findSysroot) let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) - |>.foldlM Lean.setOptionFromString'' Lean.Options.empty + |>.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run let options ← match options? with | .ok options => pure options @@ -42,6 +72,7 @@ unsafe def main (args: List String): IO Unit := do (opts := {}) (trustLevel := 1) let context: Context := { + imports } let coreContext: Lean.Core.Context := { currNamespace := Lean.Name.str .anonymous "Aniva" diff --git a/Pantograph.lean b/Pantograph.lean index 045d28a..086651f 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -3,39 +3,14 @@ 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 + imports: List String /-- Stores state of the REPL -/ structure State where + options: Commands.Options := {} --environments: Array Lean.Environment := #[] proofTrees: Array ProofTree := #[] @@ -59,9 +34,13 @@ def parse_command (s: String): Except String Commands.Command := do def execute (command: Commands.Command): Subroutine Lean.Json := do match command.cmd with - | "option.set" => + | "options.set" => match Lean.fromJson? command.payload with - | .ok args => option_set args + | .ok args => options_set args + | .error x => return errorJson x + | "options.print" => + match Lean.fromJson? command.payload with + | .ok args => options_print args | .error x => return errorJson x | "catalog" => match Lean.fromJson? command.payload with @@ -97,16 +76,19 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do { 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 + -- Command Functions + options_set (args: Commands.OptionsSet): Subroutine Lean.Json := do + let state ← get + set { state with + options := { + printExprPretty := args.printExprPretty?.getD true, + printExprAST := args.printExprAST?.getD true, + proofVariableDelta := args.proofVariableDelta?.getD false + } + } + return Lean.toJson ({ }: Commands.OptionsSetResult) + options_print (_: Commands.OptionsPrint): Subroutine Lean.Json := do + return Lean.toJson (← get).options catalog (_: Commands.Catalog): Subroutine Lean.Json := do let env ← Lean.MonadEnv.getEnv let names := env.constants.fold (init := #[]) (λ acc name info => @@ -115,22 +97,23 @@ def execute (command: Commands.Command): Subroutine Lean.Json := do | .none => acc) return Lean.toJson <| ({ symbols := names }: Commands.CatalogResult) inspect (args: Commands.Inspect): Subroutine Lean.Json := do + let state ← get 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) + let value? := match args.value?, info with + | .some true, _ => info.value? + | .some false, _ => .none + | .none, .defnInfo _ => info.value? + | .none, _ => .none return Lean.toJson ({ - type := toString format, - boundExpr? := boundExpr?, + type := ← serialize_expression state.options info.type, + value? := ← value?.mapM (λ v => serialize_expression state.options v), module? := module? }: Commands.InspectResult) clear : Subroutine Lean.Json := do diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 0b08303..2212f96 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -6,10 +6,55 @@ its field names to avoid confusion with error messages generated by the REPL. -/ import Lean.Data.Json -import Pantograph.Serial - namespace Pantograph.Commands + +/-- Main Option structure, placed here to avoid name collision -/ +structure Options where + -- When enabled, pretty print every expression + printExprPretty: Bool := true + -- When enabled, print the raw AST of expressions + 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 + proofVariableDelta: Bool := false + deriving Lean.ToJson + +--- Expression Objects --- + +structure BoundExpression where + binders: Array (String × String) + target: String + deriving Lean.ToJson +structure Expression where + -- Pretty printed expression + pp?: Option String := .none + -- AST structure + sexp?: Option String := .none + deriving Lean.ToJson + +structure Variable where + name: String + /-- Does the name contain a dagger -/ + isInaccessible: Bool := false + type: Expression + value?: Option Expression := .none + deriving Lean.ToJson +structure Goal where + /-- String case id -/ + caseName?: Option String := .none + /-- Is the goal in conversion mode -/ + isConversion: Bool := false + /-- target expression type -/ + target: Expression + /-- Variables -/ + vars: Array Variable := #[] + deriving Lean.ToJson + + + +--- Individual Commands and return types --- + structure Command where cmd: String payload: Lean.Json @@ -23,15 +68,19 @@ structure InteractionError where --- Individual command and return types --- --- Set Lean options supplied in the form of --- --- option=value -structure OptionSet where - options: Array String +/-- Set options; See `Options` struct above for meanings -/ +structure OptionsSet where + printExprPretty?: Option Bool + printExprAST?: Option Bool + proofVariableDelta?: Option Bool deriving Lean.FromJson -structure OptionSetResult where +structure OptionsSetResult where deriving Lean.ToJson +structure OptionsPrint where + deriving Lean.FromJson +abbrev OptionsPrintResult := Options + -- Print all symbols in environment structure Catalog where @@ -43,11 +92,13 @@ structure CatalogResult where -- Print the type of a symbol structure Inspect where name: String + -- If true/false, show/hide the value expressions; By default definitions + -- values are shown and theorem values are hidden. + value?: Option Bool := .some false deriving Lean.FromJson structure InspectResult where - type: String - -- Decompose the bound expression when the type is forall. - boundExpr?: Option BoundExpression := Option.none + type: Expression + value?: Option Expression := .none module?: Option String deriving Lean.ToJson diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean index 3426628..09f6d93 100644 --- a/Pantograph/Meta.lean +++ b/Pantograph/Meta.lean @@ -16,7 +16,9 @@ From this point on, any proof which extends -/ def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := -{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false } + { + msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false + } namespace Pantograph @@ -83,12 +85,14 @@ inductive TacticResult where -- Invalid id | invalid (message: String): TacticResult -- Goes to next state - | success (nextId?: Option Nat) (goals: Array Goal) + | success (nextId?: Option Nat) (goals: Array Commands.Goal) -- Fails with messages | 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 := {} let tree ← get match tree.states.get? stateId with | .none => return .invalid s!"Invalid state id {stateId}" @@ -113,7 +117,7 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P modify fun s => { s with states := s.states.push proofState } let goals ← nextGoals.mapM fun mvarId => do match (← MonadMCtx.getMCtx).findDecl? mvarId with - | .some mvarDecl => serialize_goal mvarDecl + | .some mvarDecl => serialize_goal options mvarDecl | .none => throwError mvarId return .success (.some nextId) goals.toArray diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 0851c4c..3daf93a 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -3,15 +3,20 @@ All serialisation functions -/ import Lean +import Pantograph.Commands + namespace Pantograph open Lean +--- Input Functions --- + /-- Read a theorem from the environment -/ 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 +/-- Read syntax object from string -/ def syntax_from_str (env: Environment) (s: String): Except String Syntax := Parser.runParserCategory (env := env) @@ -39,84 +44,15 @@ def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do 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 + +--- Output Functions --- + +def type_expr_to_bound (expr: Expr): MetaM Commands.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) } - -structure Variable where - name: String - /-- Does the name contain a dagger -/ - isInaccessible: Bool := false - type: String - value?: Option String := .none - deriving ToJson -structure Goal where - /-- String case id -/ - caseName?: Option String := .none - /-- Is the goal in conversion mode -/ - isConversion: Bool := false - /-- target expression type -/ - target: String - /-- Variables -/ - vars: Array Variable := #[] - deriving ToJson - -/-- Adapted from ppGoal -/ -def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do - -- Options for printing; See Meta.ppGoal for details - let showLetValues := True - let ppAuxDecls := false - let ppImplDetailHyps := false - let lctx := mvarDecl.lctx - let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } - Meta.withLCtx lctx mvarDecl.localInstances do - let rec ppVars (localDecl : LocalDecl) : MetaM Variable := do - match localDecl with - | .cdecl _ _ varName type _ _ => - let varName := varName.simpMacroScopes - let type ← instantiateMVars type - return { - name := toString varName, - isInaccessible := varName.isInaccessibleUserName, - type := toString <| ← Meta.ppExpr type - } - | .ldecl _ _ varName type val _ _ => do - let varName := varName.simpMacroScopes - let type ← instantiateMVars type - let value? ← if showLetValues then - let val ← instantiateMVars val - pure $ .some <| toString <| (← Meta.ppExpr val) - else - pure $ .none - return { - name := toString varName, - isInaccessible := varName.isInaccessibleUserName, - type := toString <| ← Meta.ppExpr type - value? := value? - } - let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do - let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail - if skip then - return acc - else - let var ← ppVars localDecl - return var::acc - return { - caseName? := match mvarDecl.userName with - | Name.anonymous => .none - | name => .some <| toString name, - isConversion := "| " == (Meta.getGoalPrefix mvarDecl) - target := toString <| (← Meta.ppExpr (← instantiateMVars mvarDecl.type)), - 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 @@ -131,16 +67,16 @@ def serialize_expression_ast (expr: Expr): MetaM String := do | .const declName _ => -- The universe level of the const expression is elided since it should be -- inferrable from surrounding expression - return s!"(:const {declName})" + return s!"(:c {declName})" | .app fn arg => let fn' ← serialize_expression_ast fn let arg' ← serialize_expression_ast arg - return s!"(:app {fn'} {arg'})" + return s!"({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'})" + return s!"(:lambda {binderName} {binderType'} {body'} :{binderInfo'})" | .forallE binderName binderType body binderInfo => let binderType' ← serialize_expression_ast binderType let body' ← serialize_expression_ast body @@ -170,11 +106,69 @@ def serialize_expression_ast (expr: Expr): MetaM String := do | .strictImplicit => "strictImplicit" | .instImplicit => "instImplicit" -/-- Serialised expression object --/ -structure Expression where - prettyprinted?: Option String := .none - bound?: Option BoundExpression := .none - sexp?: Option String := .none - deriving ToJson +def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do + let pp := toString (← Meta.ppExpr e) + let pp?: Option String := match options.printExprPretty with + | true => .some pp + | false => .none + let sexp: String := (← serialize_expression_ast e) + let sexp?: Option String := match options.printExprAST with + | true => .some sexp + | false => .none + return { + pp?, + sexp? + } + +/-- Adapted from ppGoal -/ +def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) : MetaM Commands.Goal := do + -- Options for printing; See Meta.ppGoal for details + let showLetValues := True + let ppAuxDecls := false + let ppImplDetailHyps := false + let lctx := mvarDecl.lctx + let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } + Meta.withLCtx lctx mvarDecl.localInstances do + let rec ppVars (localDecl : LocalDecl) : MetaM Commands.Variable := do + match localDecl with + | .cdecl _ _ varName type _ _ => + let varName := varName.simpMacroScopes + let type ← instantiateMVars type + return { + name := toString varName, + isInaccessible := varName.isInaccessibleUserName, + type := (← serialize_expression options type) + } + | .ldecl _ _ varName type val _ _ => do + let varName := varName.simpMacroScopes + let type ← instantiateMVars type + let value? ← if showLetValues then + let val ← instantiateMVars val + pure $ .some (← serialize_expression options val) + else + pure $ .none + return { + name := toString varName, + isInaccessible := varName.isInaccessibleUserName, + type := (← serialize_expression options type) + value? := value? + } + let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do + let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail + if skip then + return acc + else + let var ← ppVars localDecl + return var::acc + return { + caseName? := match mvarDecl.userName with + | Name.anonymous => .none + | name => .some <| toString name, + isConversion := "| " == (Meta.getGoalPrefix mvarDecl) + target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), + vars := vars.reverse.toArray + } + + end Pantograph diff --git a/README.md b/README.md index 1bb7f32..46d818d 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ result of a command execution. The command can be passed in one of two formats command { ... } { "cmd": command, "payload": ... } ``` -The list of available commands can be found in `Pantograph/Commands.lean`. An +The list of available commands can be found in `Pantograph/Commands.lean` and below. An empty command aborts the REPL. The `Pantograph` executable must be run with a list of modules to import. It can @@ -65,8 +65,13 @@ where the application of `assumption` should lead to a failure. ## Commands See `Pantograph/Commands.lean` for a description of the parameters and return values in Json. +- `options.set { key: value, ... }`: Set one or more options (not Lean options; those + have to be set via command line arguments.) +- `options.print`: Display the current set of options - `catalog`: Display a list of all safe Lean symbols in the current context -- `inspect {"name": }`: Show the type and package of a given symbol +- `inspect {"name": , "value": }`: Show the type and package of a + 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 - `proof.start {["name": ], ["expr": ], ["copyFrom": ]}`: Start a new proof state from a given expression or symbol @@ -86,4 +91,3 @@ The tests are based on `LSpec`. To run tests, ``` sh test/all.sh ``` - diff --git a/Test/Main.lean b/Test/Main.lean index 54b2cb9..9bf8e8a 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -9,6 +9,7 @@ unsafe def main := do Lean.enableInitializersExecution Lean.initSearchPath (← Lean.findSysroot) + -- TODO: Add proper testing let suites := [ test_serial, test_proofs