refactor: Remove export of Lean functions

If the user wishes to use Lean functions, they should add the bindings manually.
This commit is contained in:
Leni Aniva 2024-08-14 01:20:56 -07:00
parent caac70f0cf
commit 0bc7bc5856
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 1 additions and 45 deletions

View File

@ -9,39 +9,6 @@ open Lean
namespace Pantograph namespace Pantograph
namespace Condensed namespace Condensed
/-
These two functions are for user defiend names. For internal names such as
`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to
construct hash maps for Lean names.
-/
@[export pantograph_str_to_name]
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 || n.hasMacroScopes
@[export pantograph_mk_app_m]
def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
@[export pantograph_mk_app_expr_m]
def mkAppM' (f: Expr) (xs : Array Expr) : MetaM Expr := Meta.mkAppM' f xs
-- Copies same function in `Meta/AppBuilder.lean`
@[export pantograph_mk_fun_m]
def mkFun (constName : Name) : MetaM (Expr × Expr) := do
let cinfo ← getConstInfo constName
let us ← cinfo.levelParams.mapM fun _ => Meta.mkFreshLevelMVar
let f := mkConst constName us
let fType ← Meta.instantiateTypeLevelParams cinfo us
return (f, fType)
@[export pantograph_expr_to_string]
def exprToString (e: Expr): String := toString e
@[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 -- Mirrors Lean's LocalDecl
structure LocalDecl where structure LocalDecl where
-- Default value is for testing -- Default value is for testing
@ -61,20 +28,11 @@ structure Goal where
@[export pantograph_goal_is_lhs] @[export pantograph_goal_is_lhs]
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
-- Functions for creating contexts and states -- Functions for creating contexts and states
@[export pantograph_meta_context]
def metaContext: Meta.Context := {}
@[export pantograph_meta_state]
def metaState: Meta.State := {}
@[export pantograph_elab_context] @[export pantograph_elab_context]
def elabContext: Elab.Term.Context := { def elabContext: Elab.Term.Context := {
errToSorry := false errToSorry := false
} }
@[export pantograph_elab_state]
def elabState (levelNames: Array Name): Elab.Term.State := {
levelNames := levelNames.toList,
}
end Condensed end Condensed

View File

@ -63,10 +63,8 @@
packages = { packages = {
inherit (leanPkgs) lean lean-all; inherit (leanPkgs) lean lean-all;
inherit (project) sharedLib executable; inherit (project) sharedLib executable;
default = project.executable;
};
dependencies = {
inherit project leanPkgs; inherit project leanPkgs;
default = project.executable;
}; };
checks = { checks = {
test = pkgs.runCommand "test" { test = pkgs.runCommand "test" {