feat(lib): Catalog command FFI

This commit is contained in:
Leni Aniva 2024-03-09 16:50:36 -08:00
parent 021d0b5b7d
commit 863c6d9e7d
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
4 changed files with 72 additions and 52 deletions

View File

@ -2,6 +2,7 @@ import Lean.Data.Json
import Lean.Environment import Lean.Environment
import Pantograph.Version import Pantograph.Version
import Pantograph.Library
import Pantograph import Pantograph
-- Main IO functions -- Main IO functions
@ -39,35 +40,6 @@ partial def loop : MainM Unit := do
IO.println str IO.println str
loop loop
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := key.toName
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>
match val with
| "true" => pure $ opts.setBool key true
| "false" => pure $ opts.setBool key false
| _ => throw s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
unsafe def main (args: List String): IO Unit := do unsafe def main (args: List String): IO Unit := do
-- NOTE: A more sophisticated scheme of command line argument handling is needed. -- NOTE: A more sophisticated scheme of command line argument handling is needed.
@ -79,32 +51,17 @@ unsafe def main (args: List String): IO Unit := do
Lean.enableInitializersExecution Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
|>.foldlM Lean.setOptionFromString' Lean.Options.empty |>.toArray |> createCoreContext
|>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
let imports:= args.filter (λ s => ¬ (s.startsWith "--")) let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
let coreState ← createCoreState imports.toArray
let env ← Lean.importModules
(imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let context: Context := { let context: Context := {
imports imports
} }
let coreContext: Lean.Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] },
options := options
}
try try
let coreM := loop.run context |>.run' {} let coreM := loop.run context |>.run' {}
IO.println "ready." IO.println "ready."
discard <| coreM.toIO coreContext { env := env } discard <| coreM.toIO coreContext coreState
catch ex => catch ex =>
IO.println "Uncaught IO exception" IO.println "Uncaught IO exception"
IO.println ex.toString IO.println ex.toString

View File

@ -71,7 +71,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
return .ok { nGoals } return .ok { nGoals }
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
Environment.catalog args let result ← Environment.catalog args
return .ok result
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
let state ← get let state ← get
Environment.inspect args state.options Environment.inspect args state.options

View File

@ -30,13 +30,13 @@ def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :
if is_symbol_unsafe_or_internal n info if is_symbol_unsafe_or_internal n info
then Option.none then Option.none
else Option.some <| to_compact_symbol_name n info else Option.some <| to_compact_symbol_name n info
def catalog (_: Protocol.EnvCatalog): CoreM (Protocol.CR Protocol.EnvCatalogResult) := do def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => acc.push x | .some x => acc.push x
| .none => acc) | .none => acc)
return .ok { symbols := names } return { symbols := names }
def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let name := args.name.toName let name := args.name.toName

View File

@ -1,8 +1,70 @@
import Pantograph.Version import Pantograph.Version
import Pantograph.Environment
import Pantograph.Protocol
import Lean
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := key.toName
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>
match val with
| "true" => pure $ opts.setBool key true
| "false" => pure $ opts.setBool key false
| _ => throw s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
namespace Pantograph namespace Pantograph
@[export pantograph_version] @[export pantograph_version]
def pantograph_version: String := version def pantographVersion: String := version
/-- Creates a Core.Context object needed to run all monads -/
@[export pantograph_create_core_context]
def createCoreContext (options: Array String): IO Lean.Core.Context := do
let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
return {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] },
options := options
}
@[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Lean.Core.State := do
let env ← Lean.importModules
(imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return { env := env }
@[export pantograph_catalog]
def catalog (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
end Pantograph end Pantograph