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 '<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
   -- 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 := "<Pantograph>",
-    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

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

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

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 '<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
 
 @[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