Lean 4 Elaboration: TermElabM, MetaM, and the CoreM Stack

open Lean Core in
-- Read the global environment
#check (getEnv : CoreM Environment)

-- Modify the environment
#check (modifyEnv : (Environment → Environment) → CoreM Unit)

-- Get compiler options
#check (getOptions : CoreM Options)

-- Throw a structured error
#check (throwError : MessageData → CoreM α)

-- Log informational messages
#check (logInfo : MessageData → CoreM Unit)
#check (logWarning : MessageData → CoreM Unit)

open Lean in
def lookupConst (name : Name) : CoreM (Option ConstantInfo) := do
  return (← getEnv).find? name

-- ConstantInfo variants: defnInfo, thmInfo, axiomInfo, opaqueInfo, quotInfo, inductInfo, ctorInfo, recInfo
open Lean in
def getConstType (name : Name) : CoreM Expr := do
  let env ← getEnv
  match env.find? name with
  | some ci => return ci.type
  | none    => throwError "unknown constant: {name}"

open Lean Meta in
example : MetaM Unit := do
  -- Create a metavariable of type Nat
  let mvar ← mkFreshExprMVar (mkConst ``Nat) .synthetic .anonymous
  -- Inspect its type
  let ty ← inferType mvar
  logInfo m!"mvar type: {ty}"

open Lean Meta in
def tryUnify (t s : Expr) : MetaM Bool := do
  isDefEq t s

-- isDefEq is the basis of all unification in elaboration.
-- It respects β-reduction, δ-reduction, ι-reduction, and ζ-reduction.

open Lean Meta in
def reduceToHead (e : Expr) : MetaM Expr := do
  whnf e

-- Example: whnf `(Nat.succ (Nat.succ 0))` → `Nat.succ (Nat.succ 0)` (already WHNF)
-- Example: whnf `(List.length [1,2,3])` → reduces the definition

open Lean Meta in
def checkType (e : Expr) : MetaM Expr := do
  inferType e

open Lean Meta in
example : MetaM Expr := do
  -- mkAppN: apply a function to multiple arguments
  let f := mkConst ``Nat.add
  let a := mkNatLit 3
  let b := mkNatLit 4
  let app := mkAppN f #[a, b]  -- Nat.add 3 4

  -- mkForallFVars: abstract over free variables to form a ∀-type
  withLocalDecl `n .default (mkConst ``Nat) fun nFVar => do
    let body := mkApp2 (mkConst ``Nat.succ) nFVar nFVar
    let forallExpr ← mkForallFVars #[nFVar] body  -- ∀ (n : Nat), Nat.succ n

  -- mkLambdaFVars: abstract over free variables to form a λ
  withLocalDecl `x .default (mkConst ``Nat) fun xFVar => do
    let body := mkApp (mkConst ``Nat.succ) xFVar
    let lam ← mkLambdaFVars #[xFVar] body  -- fun (x : Nat) => Nat.succ x

  return mkNatLit 0  -- placeholder

open Lean Meta in
def analyzeType (ty : Expr) : MetaM Unit :=
  forallTelescope ty fun params resultType => do
    logInfo m!"Parameters: {params}"
    logInfo m!"Result type: {resultType}"

-- Also: lambdaTelescope, forallTelescopeReducing

open Lean Elab Term in
-- The main entry point: elaborate a syntax node with an optional expected type
def myElab (stx : Syntax) : TermElabM Expr := do
  elabTerm stx none  -- no expected type
  -- or: elabTerm stx (some expectedType)

open Lean Meta in
example : MetaM Expr :=
  -- withLocalDecl: introduce a hypothesis into the local context
  withLocalDecl `h .default (mkConst ``Nat) fun hFVar => do
    -- hFVar is a free variable of type Nat in scope here
    return hFVar

-- withLocalDeclD: same but with "default" binder info (explicit)
-- withLetDecl: introduce a let-binding

open Lean Elab Term in
-- Register with elab_rules
elab_rules : term
  | `(myTerm $n:num) => do
      return mkNatLit n.getNat

-- Or with the low-level @[term_elab] attribute
@[term_elab myTermSyntaxKind]
def myTermElabFn : TermElab := fun stx expectedType? => do
  -- stx is the matched syntax, expectedType? is the expected type if known
  elabTerm stx[1] expectedType?

open Lean Elab Command in
-- Lift a MetaM action into CommandElabM
def myCommand : CommandElabM Unit := do
  liftTermElabM do
    let ty ← inferType (mkConst ``Nat.add)
    logInfo m!"Nat.add has type {ty}"

open Lean in
-- addDecl: add a declaration to the environment (kernel-checked)
-- addAndCompile: add and also compile to bytecode/native

def addSimpleDef (name : Name) (value type : Expr) : CoreM Unit := do
  let decl := Declaration.defnDecl {
    name        := name
    levelParams := []
    type        := type
    value       := value
    hints       := .regular (getReducibilityHintsNumHeartbeats (← getOptions))
    safety      := .safe
  }
  addDecl decl

open Lean in
-- addAndCompile (decl : Declaration) : CoreM Unit
-- Same as addDecl but also runs the compiler

import Lean
open Lean Elab Command Meta

syntax (name := showType) "#showType" ident : command

@[command_elab showType]
def elabShowType : CommandElab
  | `(#showType $id:ident) => do
      let name ← resolveGlobalConstNoOverload id
      let ty ← liftTermElabM <| do
        let ci ← getConstInfo name
        return ci.type
      logInfo m!"{name} : {ty}"
  | _ => throwUnsupportedSyntax

#showType Nat.add
-- Nat.add : Nat → Nat → Nat

open Lean in
example : CoreM Unit := do
  -- Informational message (shown in VS Code info widget)
  logInfo m!"Found {42} things"

  -- Warning (shown as yellow squiggle)
  logWarning m!"This looks suspicious"

  -- Error that aborts the current elaboration
  throwError "Expected a Nat literal, got something else"

  -- Error attached to a specific syntax node
  throwErrorAt stx "This token is invalid here"

open Lean in
example (e : Expr) (n : Name) : CoreM Unit := do
  logInfo m!"Expression: {e}"   -- pretty-printed
  logInfo m!"Name: {n}"         -- dotted name
  logInfo m!"Indented: {indentExpr e}"