From aca7dc9811cb7fddb76faf6e895f18799583cc15 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 15 Dec 2023 13:37:55 -0500 Subject: [PATCH] refactor: env. operations into its own file --- Pantograph.lean | 73 +++------------------------------ Pantograph/Environment.lean | 82 +++++++++++++++++++++++++++++++++++++ Pantograph/Protocol.lean | 3 ++ 3 files changed, 90 insertions(+), 68 deletions(-) create mode 100644 Pantograph/Environment.lean diff --git a/Pantograph.lean b/Pantograph.lean index 2bd066e..30ac0c0 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -2,6 +2,7 @@ import Pantograph.Goal import Pantograph.Protocol import Pantograph.Serial import Pantograph.Symbol +import Pantograph.Environment import Lean.Data.HashMap namespace Pantograph @@ -59,7 +60,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } errorCommand := errorI "command" errorIndex := errorI "index" - errorExpr := errorI "expr" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -70,76 +70,13 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let state ← get let nGoals := state.goalStates.size return .ok { nGoals } - env_catalog (_: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := 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 .ok { symbols := names } + env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do + Environment.catalog args env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do let state ← get - let env ← Lean.MonadEnv.getEnv - let name := args.name.toName - let info? := env.find? name - match info? with - | none => return .error $ errorIndex s!"Symbol not found {args.name}" - | some info => - let module? := env.getModuleIdxFor? name >>= - (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString - let value? := match args.value?, info with - | .some true, _ => info.value? - | .some false, _ => .none - | .none, .defnInfo _ => info.value? - | .none, _ => .none - return .ok { - type := ← (serialize_expression state.options info.type).run', - value? := ← value?.mapM (λ v => serialize_expression state.options v |>.run'), - publicName? := Lean.privateToUserName? name |>.map (·.toString), - -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. - typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, - valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none, - module? := module? - } + Environment.inspect args state.options env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do - let env ← Lean.MonadEnv.getEnv - let tv?: Except String (Lean.Expr × Lean.Expr) ← runTermElabM (do - let type ← match syntax_from_str env args.type with - | .ok syn => do - match ← syntax_to_expr syn with - | .error e => return .error e - | .ok expr => pure expr - | .error e => return .error e - let value ← match syntax_from_str env args.value with - | .ok syn => do - try - let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) - Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing - let expr ← Lean.instantiateMVars expr - pure $ expr - catch ex => return .error (← ex.toMessageData.toString) - | .error e => return .error e - pure $ .ok (type, value) - ) - let (type, value) ← match tv? with - | .ok t => pure t - | .error e => return .error $ errorExpr e - let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx - (name := args.name.toName) - (levelParams := []) - (type := type) - (value := value) - (hints := Lean.mkReducibilityHintsRegularEx 1) - (safety := Lean.DefinitionSafety.safe) - (all := []) - let env' ← match env.addDecl constant with - | .error e => do - let options ← Lean.MonadOptions.getOptions - let errorMessage ← (e.toMessageData options).toString - return .error $ errorI "kernel" errorMessage - | .ok env' => pure env' - Lean.MonadEnv.modifyEnv (λ _ => env') - return .ok {} + Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get let env ← Lean.MonadEnv.getEnv diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean new file mode 100644 index 0000000..e9a884e --- /dev/null +++ b/Pantograph/Environment.lean @@ -0,0 +1,82 @@ +import Pantograph.Protocol +import Pantograph.Symbol +import Pantograph.Serial +import Lean + +open Lean +open Pantograph + +namespace Pantograph.Environment + +abbrev CR α := Except Protocol.InteractionError α + +def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := 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 .ok { symbols := names } +def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR Protocol.EnvInspectResult) := do + let env ← Lean.MonadEnv.getEnv + let name := args.name.toName + let info? := env.find? name + match info? with + | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}" + | some info => + let module? := env.getModuleIdxFor? name >>= + (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString + let value? := match args.value?, info with + | .some true, _ => info.value? + | .some false, _ => .none + | .none, .defnInfo _ => info.value? + | .none, _ => .none + return .ok { + type := ← (serialize_expression options info.type).run', + value? := ← value?.mapM (λ v => serialize_expression options v |>.run'), + publicName? := Lean.privateToUserName? name |>.map (·.toString), + -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. + typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, + valueDependency? := if args.dependency?.getD false then info.value?.map (·.getUsedConstants.map (λ n => name_to_ast n)) else .none, + module? := module? + } +def addDecl (args: Protocol.EnvAdd): CoreM (CR Protocol.EnvAddResult) := do + let env ← Lean.MonadEnv.getEnv + let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do + let type ← match syntax_from_str env args.type with + | .ok syn => do + match ← syntax_to_expr syn with + | .error e => return .error e + | .ok expr => pure expr + | .error e => return .error e + let value ← match syntax_from_str env args.value with + | .ok syn => do + try + let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) + Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing + let expr ← instantiateMVars expr + pure $ expr + catch ex => return .error (← ex.toMessageData.toString) + | .error e => return .error e + pure $ .ok (type, value) + let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with + | .ok t => pure t + | .error e => return .error $ Protocol.errorExpr e + let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + (name := args.name.toName) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match env.addDecl constant with + | .error e => do + let options ← Lean.MonadOptions.getOptions + let desc ← (e.toMessageData options).toString + return .error $ { error := "kernel", desc } + | .ok env' => pure env' + Lean.MonadEnv.modifyEnv (λ _ => env') + return .ok {} + +end Pantograph.Environment diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 8bf754a..c0204d0 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -79,6 +79,9 @@ structure InteractionError where desc: String deriving Lean.ToJson +def errorIndex (desc: String): InteractionError := { error := "index", desc } +def errorExpr (desc: String): InteractionError := { error := "expr", desc } + --- Individual command and return types ---