feat: Expose TermElab context and state

This commit is contained in:
Leni Aniva 2024-07-22 17:34:14 -07:00
parent 94c7b021f7
commit eb5ee8c57c
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 18 additions and 9 deletions

View File

@ -13,14 +13,14 @@ construct hash maps for Lean names.
@[export pantograph_str_to_name] @[export pantograph_str_to_name]
def strToName (s: String) : Name := s.toName def strToName (s: String) : Name := s.toName
@[export pantograph_name_to_str] @[export pantograph_name_to_str]
def nameToStr (s: String) : Name := s.toName def nameToStr (s: Name) : String := s.toString
@[export pantograph_name_is_inaccessible] @[export pantograph_name_is_inaccessible]
def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
@[export pantograph_mk_app_meta_m] @[export pantograph_mk_app_m]
def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr := Meta.mkAppM constName xs
@[export pantograph_pp_expr_meta_m] @[export pantograph_pp_expr_m]
def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e def ppExpr (e: Expr): MetaM String := toString <$> Meta.ppExpr e
@ -44,6 +44,18 @@ structure Goal where
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
-- 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]
def elabContext: Meta.Context := {}
@[export pantograph_elab_state]
def elabState (levelNames: Array Name): Elab.Term.State := {
levelNames := levelNames.toList,
}
end Pantograph.Condensed end Pantograph.Condensed

View File

@ -78,11 +78,6 @@ def createCoreState (imports: Array String): IO Core.State := do
(trustLevel := 1) (trustLevel := 1)
return { env := env } return { env := env }
@[export pantograph_meta_context]
def metaContext: Lean.Meta.Context := {}
@[export pantograph_meta_state]
def metaState: Lean.Meta.State := {}
@[export pantograph_env_catalog_m] @[export pantograph_env_catalog_m]
def envCatalog: CoreM Protocol.EnvCatalogResult := def envCatalog: CoreM Protocol.EnvCatalogResult :=
Environment.catalog ({}: Protocol.EnvCatalog) Environment.catalog ({}: Protocol.EnvCatalog)
@ -99,6 +94,7 @@ def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
CoreM (Protocol.CR Protocol.EnvAddResult) := CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem } Environment.addDecl { name, type, value, isTheorem }
@[export pantograph_parse_elab_type_m]
def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let syn ← match parseTerm env type with let syn ← match parseTerm env type with
@ -109,6 +105,7 @@ def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
| .ok expr => return .ok (← instantiateMVars expr) | .ok expr => return .ok (← instantiateMVars expr)
/-- This must be a TermElabM since the parsed expr contains extra information -/ /-- This must be a TermElabM since the parsed expr contains extra information -/
@[export pantograph_parse_elab_expr_m]
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let expectedType? ← match ← expectedType?.mapM parseElabType with let expectedType? ← match ← expectedType?.mapM parseElabType with