Pantograph/Condensed.lean

@@ -19,13 +19,15 @@ def strToName (s: String) : Name := s.toName
 @[export pantograph_name_to_str]
 def nameToStr (s: Name) : String := s.toString
 @[export pantograph_name_is_inaccessible]
-def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
+def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName || n.hasMacroScopes
 
 @[export pantograph_mk_app_m]
 def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
 
 @[export pantograph_pp_expr_m]
 def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
+@[export pantograph_get_used_constants]
+def getUsedConstants (e: Expr) := e.getUsedConstants
 
 
 -- Mirrors Lean's LocalDecl

Pantograph/Environment.lean

@@ -7,15 +7,31 @@ open Pantograph
 
 namespace Pantograph.Environment
 
-def isNameInternal (n: Lean.Name): Bool :=
+@[export pantograph_is_name_internal]
+def isNameInternal (n: Name): Bool :=
   -- Returns true if the name is an implementation detail which should not be shown to the user.
   isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
   where
-  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
+  isLeanSymbol (name: Name): Bool := match name.getRoot with
     | .str _ name => name == "Lean"
     | _ => true
 
-def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+/-- Catalog all the non-internal names -/
+@[export pantograph_environment_catalog]
+def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
+  match isNameInternal name with
+  | true => acc.push name
+  | false => acc)
+
+@[export pantograph_environment_module_of_name]
+def module_of_name (env: Environment) (name: Name): Option Name := do
+  let moduleId ←  env.getModuleIdxFor? name
+  return env.allImportedModuleNames.get! moduleId.toNat
+
+@[export pantograph_constant_info_is_unsafe_or_partial]
+def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
+
+def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
   let pref := match info with
   | .axiomInfo  _ => "a"
   | .defnInfo   _ => "d"

Pantograph/Expr.lean

@@ -7,6 +7,7 @@ namespace Pantograph
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+@[export pantograph_unfold_aux_lemmas]
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma