Monomorphize Procedures

The MonomorphizeProcedures program transformation monomorphizes every polymorphic procedure so that no procedure's types mention type variables.

Where it runs

This pass runs in corePipelinePhases immediately before typeCheckPhase (and therefore after CallElim in transformPipelinePhases). Two consequences of this position matter:

• CallElim has already run, so no procedure body contains a call and each procedure can be monomorphized independently of the others.
• typeCheckPhase which runs after MonomorphizeProcedures clears header.typeArgs and instantiates the signature to fresh internal type variables such as $__ty0, so running before it lets each procedure still carry its declared type parameters in header.typeArgs under their original source names (e.g. a).

The subsequent typeCheckPhase then re-checks the now-monomorphic procedure against its opaque-typed signature, propagating the opaque types through the body.

How it works

For each procedure whose header.typeArgs is x₁, …, xₖ:

1. A fresh, globally-unique opaque type is minted per type parameter, named $__opaque_{procName}_{xᵢ}_N (the $__ prefix reserves the internal namespace so the name cannot collide with a user-declared type; the trailing _N is a fresh counter from the shared CoreGenState, guaranteeing uniqueness). Each becomes a nullary top-level type declaration type {name}; emitted immediately before the procedure.
2. A type substitution mapping each xᵢ to its opaque nullary type constructor is applied to the whole procedure: input/output signatures, precondition and postcondition expressions, and every expression and local declaration type in the body (LExpr.applySubst for expression annotations, LMonoTy.subst for signature and declaration types).
3. header.typeArgs is cleared, so the procedure is now monomorphic.

The statement-level substitution reuses the type checker's Core.Statement.subst (StatementType.lean, which in turn uses Command.subst and Lambda.LTy.subst). Only structured bodies are monomorphized: a CFG body is reported as an error.

Applying the type substitution

The statement / command / declared-type substitution is the type checker's existing Core.Statement.subst (which uses Command.subst and Lambda.LTy.subst, in StatementType.lean / LTyUnify.lean). Here we only assemble the whole-procedure substitution on top of it.

def Core.MonomorphizeProcedures.substProc (S : Lambda.Subst) (proc : Procedure) : Transform.CoreTransformM Procedure

Apply S to a whole procedure: its signature, spec clauses, and body, and clear header.typeArgs. Throws if the body is a CFG (unsupported). The body substitution reuses Statement.subst.

Equations

• One or more equations did not get rendered due to their size.

The transformation

def Core.MonomorphizeProcedures.monomorphizeProc (proc : Procedure) (md : Imperative.MetaData Expression) : Transform.CoreTransformM (List Decl)

Monomorphize a single procedure. One fresh opaque type is minted per declared type parameter (header.typeArgs); the opaque type declarations are returned first, followed by the substituted procedure. A procedure with no type parameters is returned unchanged.

Equations

• One or more equations did not get rendered due to their size.

def Core.MonomorphizeProcedures.run (p : Program) : Transform.CoreTransformM Program

Monomorphize every procedure in the program, introducing opaque types for the free type variables of each polymorphic procedure.

Equations

• One or more equations did not get rendered due to their size.

def Core.monomorphizeProcedures (p : Program) : Transform.CoreTransformM (Bool × Program)

CoreTransformM runner for MonomorphizeProcedures, suitable for use with Core.Transform.run. Reports whether any opaque type declaration was introduced (which happens iff some procedure was monomorphized).

Equations

• Core.monomorphizeProcedures p = do let p' ← Core.MonomorphizeProcedures.run p pure (List.length p'.decls != List.length p.decls, p')

def Core.monomorphizeProceduresPipelinePhase : PipelinePhase

Pipeline phase for MonomorphizeProcedures. Model-preserving: replacing an implicitly universally-quantified type variable with a fresh, arbitrary opaque type is universal generalization (∀-introduction), which preserves the proof obligation and introduces no spurious models.

Equations

• Core.monomorphizeProceduresPipelinePhase = Core.modelPreservingPipelinePhase "monomorphizeProcedures" fun (prog : Core.Program) => Core.monomorphizeProcedures prog