From ca89d671cc1b83acff63247b688eb92acb7c7398 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 9 Mar 2024 20:33:36 -0800 Subject: [PATCH] refactor: Move some functions to `Library.lean` --- Pantograph.lean | 28 +------------------- Pantograph/Library.lean | 57 +++++++++++++++++++++++++++++++++++++--- Pantograph/Protocol.lean | 2 +- Pantograph/Serial.lean | 2 +- 4 files changed, 57 insertions(+), 32 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index f1f194c..f9b5dc5 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -22,14 +22,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM) -- certain monadic features in `MainM` abbrev CR α := Except Protocol.InteractionError α -def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := - metaM.run' -def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := - termElabM.run' (ctx := { - declName? := .none, - errToSorry := false, - }) |>.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 @@ -57,9 +49,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do errorCommand s!"Unknown command {cmd}" return Lean.toJson error where - errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } - errorCommand := errorI "command" - errorIndex := errorI "index" -- Command Functions reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do let state ← get @@ -80,22 +69,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - let env ← Lean.MonadEnv.getEnv - let syn ← match syntax_from_str env args.expr with - | .error str => return .error $ errorI "parsing" str - | .ok syn => pure syn - runTermElabM (do - match ← syntax_to_expr syn with - | .error str => return .error $ errorI "elab" str - | .ok expr => do - try - let type ← Lean.Meta.inferType expr - return .ok { - type := (← serialize_expression (options := state.options) type), - expr := (← serialize_expression (options := state.options) expr) - } - catch exception => - return .error $ errorI "typing" (← exception.toMessageData.toString)) + exprEcho args state.options options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do let state ← get let options := state.options diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 07e4656..cdc112f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -3,7 +3,6 @@ import Pantograph.Environment import Pantograph.Protocol import Lean - namespace Lean /-- This is better than the default version since it handles `.` and doesn't @@ -35,6 +34,18 @@ end Lean namespace Pantograph +def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := + metaM.run' +def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := + termElabM.run' (ctx := { + declName? := .none, + errToSorry := false, + }) |>.run' + +def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } +def errorCommand := errorI "command" +def errorIndex := errorI "index" + @[export pantograph_version] def pantographVersion: String := version @@ -67,10 +78,50 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do (trustLevel := 1) return { env := env } -@[export pantograph_catalog] -def catalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do +@[export pantograph_env_catalog] +def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog) let (result, _) ← coreM.toIO cc cs return result +@[export pantograph_env_inspect] +def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State) + (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do + let coreM: Lean.CoreM _ := Environment.inspect ({ + name, value? := .some value, dependency?:= .some dependency + }: Protocol.EnvInspect) options + let (result, _) ← coreM.toIO cc cs + return result + +@[export pantograph_env_add] +def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State) + (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do + let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem } + let (result, _) ← coreM.toIO cc cs + return result + +def exprEcho (args: Protocol.ExprEcho) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do + let env ← Lean.MonadEnv.getEnv + let syn ← match syntax_from_str env args.expr with + | .error str => return .error $ errorI "parsing" str + | .ok syn => pure syn + runTermElabM (do + match ← syntax_to_expr syn with + | .error str => return .error $ errorI "elab" str + | .ok expr => do + try + let type ← Lean.Meta.inferType expr + return .ok { + type := (← serialize_expression options type), + expr := (← serialize_expression options expr) + } + catch exception => + return .error $ errorI "typing" (← exception.toMessageData.toString)) + +@[export pantograph_expr_echo] +def exprEchoExport (cc: Lean.Core.Context) (cs: Lean.Core.State) (expr: String) (options: @&Protocol.Options): IO (Protocol.CR Protocol.ExprEchoResult) := do + let coreM: Lean.CoreM _ := exprEcho { expr } options + let (result, _) ← coreM.toIO cc cs + return result + end Pantograph diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 84e0cc2..5015ad1 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -163,7 +163,7 @@ structure EnvAdd where name: String type: String value: String - isTheorem?: Bool + isTheorem: Bool deriving Lean.FromJson structure EnvAddResult where deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 38d1f14..547b3dc 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -157,7 +157,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta | .instImplicit => " :instImplicit" of_name (name: Name) := name_to_ast name sanitize -def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do +def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do let pp := toString (← Meta.ppExpr e) let pp?: Option String := match options.printExprPretty with | true => .some pp