refactor: Move some functions to `Library.lean`

This commit is contained in:
Leni Aniva 2024-03-09 20:33:36 -08:00
parent eeb149a32c
commit f18a9dd1d5
4 changed files with 57 additions and 32 deletions

View File

@ -22,14 +22,6 @@ abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- certain monadic features in `MainM` -- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α 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 def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with
@ -57,9 +49,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
errorCommand s!"Unknown command {cmd}" errorCommand s!"Unknown command {cmd}"
return Lean.toJson error return Lean.toJson error
where where
errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
errorCommand := errorI "command"
errorIndex := errorI "index"
-- Command Functions -- Command Functions
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
@ -80,22 +69,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
Environment.addDecl args Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv exprEcho args state.options
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))
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get let state ← get
let options := state.options let options := state.options

View File

@ -3,7 +3,6 @@ import Pantograph.Environment
import Pantograph.Protocol import Pantograph.Protocol
import Lean import Lean
namespace Lean namespace Lean
/-- This is better than the default version since it handles `.` and doesn't /-- This is better than the default version since it handles `.` and doesn't
@ -35,6 +34,18 @@ end Lean
namespace Pantograph 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] @[export pantograph_version]
def pantographVersion: String := version def pantographVersion: String := version
@ -67,10 +78,50 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
(trustLevel := 1) (trustLevel := 1)
return { env := env } return { env := env }
@[export pantograph_catalog] @[export pantograph_env_catalog]
def catalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do
let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog) let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog)
let (result, _) ← coreM.toIO cc cs let (result, _) ← coreM.toIO cc cs
return result 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 end Pantograph

View File

@ -163,7 +163,7 @@ structure EnvAdd where
name: String name: String
type: String type: String
value: String value: String
isTheorem?: Bool isTheorem: Bool
deriving Lean.FromJson deriving Lean.FromJson
structure EnvAddResult where structure EnvAddResult where
deriving Lean.ToJson deriving Lean.ToJson

View File

@ -157,7 +157,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
| .instImplicit => " :instImplicit" | .instImplicit => " :instImplicit"
of_name (name: Name) := name_to_ast name sanitize 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 := toString (← Meta.ppExpr e)
let pp?: Option String := match options.printExprPretty with let pp?: Option String := match options.printExprPretty with
| true => .some pp | true => .some pp