From 863c6d9e7d8342f833a05091758ffb30c2f7bc8f Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 9 Mar 2024 16:50:36 -0800 Subject: [PATCH] feat(lib): Catalog command FFI --- Main.lean | 53 +++--------------------------- Pantograph.lean | 3 +- Pantograph/Environment.lean | 4 +-- Pantograph/Library.lean | 64 ++++++++++++++++++++++++++++++++++++- 4 files changed, 72 insertions(+), 52 deletions(-) diff --git a/Main.lean b/Main.lean index 68d1a3e..7c36db2 100644 --- a/Main.lean +++ b/Main.lean @@ -2,6 +2,7 @@ import Lean.Data.Json import Lean.Environment import Pantograph.Version +import Pantograph.Library import Pantograph -- Main IO functions @@ -39,35 +40,6 @@ partial def loop : MainM Unit := do IO.println str 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 ' = '" - 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 -- 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.initSearchPath (← Lean.findSysroot) - let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) - |>.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}" + let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none) + |>.toArray |> createCoreContext let imports:= args.filter (λ s => ¬ (s.startsWith "--")) - - let env ← Lean.importModules - (imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false })) - (opts := {}) - (trustLevel := 1) + let coreState ← createCoreState imports.toArray let context: Context := { imports } - let coreContext: Lean.Core.Context := { - currNamespace := Lean.Name.str .anonymous "Aniva" - openDecls := [], -- No 'open' directives needed - fileName := "", - fileMap := { source := "", positions := #[0], lines := #[1] }, - options := options - } try let coreM := loop.run context |>.run' {} IO.println "ready." - discard <| coreM.toIO coreContext { env := env } + discard <| coreM.toIO coreContext coreState catch ex => IO.println "Uncaught IO exception" IO.println ex.toString diff --git a/Pantograph.lean b/Pantograph.lean index 90ce2d2..f1f194c 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -71,7 +71,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do let nGoals := state.goalStates.size return .ok { nGoals } 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 let state ← get Environment.inspect args state.options diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index b823e8f..df0bc7f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -30,13 +30,13 @@ def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String : if is_symbol_unsafe_or_internal n info then Option.none 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 names := env.constants.fold (init := #[]) (λ acc name info => match to_filtered_symbol name info with | .some x => acc.push x | .none => acc) - return .ok { symbols := names } + return { symbols := names } def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do let env ← Lean.MonadEnv.getEnv let name := args.name.toName diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 330d84d..5b5e954 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,8 +1,70 @@ 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 ' = '" + 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 @[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 := "", + 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