refactor: Move some functions to `Library.lean`
This commit is contained in:
parent
4706df2217
commit
ca89d671cc
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
Loading…
Reference in New Issue