aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat(lib): CoreM execution function

This commit is contained in:
Leni Aniva 2024-03-10 06:41:35 -07:00
parent ca89d671cc
commit d958dbed9d
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 40 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Pantograph.lean
View File

@ -69,7 +69,10 @@ 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
exprEcho args state.options let expr ← match ← exprParse args.expr with
| .ok expr => pure $ expr
| .error e => return .error e
exprPrint expr state.options
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

63
Pantograph/Library.lean
View File

@ -1,6 +1,7 @@
import Pantograph.Version
import Pantograph.Environment import Pantograph.Environment
import Pantograph.Goal
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Version
import Lean import Lean
namespace Lean namespace Lean
@ -70,6 +71,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do
options := options options := options
} }
/-- Creates a Core.State object needed to run all monads -/
@[export pantograph_create_core_state] @[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Lean.Core.State := do def createCoreState (imports: Array String): IO Lean.Core.State := do
let env ← Lean.importModules let env ← Lean.importModules
@ -78,11 +80,14 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
(trustLevel := 1) (trustLevel := 1)
return { env := env } return { env := env }
/-- Execute a `CoreM` monad -/
@[export pantograph_exec_core]
def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): IO (α × Lean.Core.State) :=
coreM.toIO context state
@[export pantograph_env_catalog] @[export pantograph_env_catalog]
def envCatalog (cc: Lean.Core.Context) (cs: Lean.Core.State): IO Protocol.EnvCatalogResult := do def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
let coreM: Lean.CoreM _ := Environment.catalog ({}: Protocol.EnvCatalog) Environment.catalog ({}: Protocol.EnvCatalog)
let (result, _) ← coreM.toIO cc cs
return result
@[export pantograph_env_inspect] @[export pantograph_env_inspect]
def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State) def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State)
@ -100,28 +105,32 @@ def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State)
let (result, _) ← coreM.toIO cc cs let (result, _) ← coreM.toIO cc cs
return result return result
def exprEcho (args: Protocol.ExprEcho) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do @[export pantograph_expr_parse]
let env ← Lean.MonadEnv.getEnv def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
let syn ← match syntax_from_str env args.expr with let env ← Lean.MonadEnv.getEnv
| .error str => return .error $ errorI "parsing" str let syn ← match syntax_from_str env s with
| .ok syn => pure syn | .error str => return .error $ errorI "parsing" str
runTermElabM (do | .ok syn => pure syn
match ← syntax_to_expr syn with runTermElabM (do
| .error str => return .error $ errorI "elab" str match ← syntax_to_expr syn with
| .ok expr => do | .error str => return .error $ errorI "elab" str
try | .ok expr => return .ok expr)
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] @[export pantograph_expr_print]
def exprEchoExport (cc: Lean.Core.Context) (cs: Lean.Core.State) (expr: String) (options: @&Protocol.Options): IO (Protocol.CR Protocol.ExprEchoResult) := do def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
let coreM: Lean.CoreM _ := exprEcho { expr } options let termElabM: Lean.Elab.TermElabM _ :=
let (result, _) ← coreM.toIO cc cs try
return result 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)
runTermElabM termElabM
@[export pantograph_goal_start]
def goalStart (expr: Lean.Expr): Lean.CoreM GoalState :=
runTermElabM (GoalState.create expr)
end Pantograph end Pantograph