The persistent @[param] constant database

The term-level translator ParamTranslate.translate consumes a db : NameMap (Expr × Expr) mapping an abstract constant c to its transferred counterpart c' together with a witness wᶜ : RArrow PA PB c c'. Without an ambient store that database must be assembled and passed by hand at each call site.

This module makes the database persistent and ambient:

• a persistent environment extension (paramExt) whose state is a NameMap (Name × Name) — abstract const name ↦ (transferred const, witness lemma). Built with Lean.registerSimplePersistentEnvExtension; the addImportedFn re-folds entries from imported modules, so registrations survive across files.
• an attribute @[param] that, given a lemma cR : RArrow PA PB c c', peels the RArrow application from the lemma's type (the last two of its eight application arguments are the abstract const c and the transferred const c') and stores c.constName ↦ (c'.constName, lemmaName).
• getParamDB : MetaM (NameMap (Expr × Expr)) — materialises the extension state into the NameMap (Expr × Expr) that translate consumes, turning each (c', lemmaName) into (Expr.const c' [], Expr.const lemmaName []).
• a driver command #param_translate t that runs translate {} (← getParamDB) t against the ambient registry and logs the transferred term and the proof's type.

A witness is registered once with @[param], and the translator resolves the constant from the registry with no explicit db argument.

The persistent @[param] database

opaque Transfer.Param.paramExt : Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name × Lean.Name) (Lean.NameMap (Lean.Name × Lean.Name))

The persistent environment extension backing @[param]. Its state maps an abstract constant's name to (transferred const name, witness lemma name). addEntryFn inserts a single registration; addImportedFn re-folds all entries contributed by imported modules so the database is cross-file.

def Transfer.Param.peelRArrow (ty : Lean.Expr) : Lean.MetaM (Lean.Name × Lean.Name)

Peel RArrow PA PB c c' from a lemma's type. RArrow has four implicit type arguments {A A' B B'}, two relation arguments PA PB, and the two function arguments f f' — eight application arguments in total. The abstract constant c and its transferred counterpart c' are the last two; their head-constant names are returned.

Equations

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

def Transfer.Param.getParamDB : Lean.MetaM (Lean.NameMap (Lean.Expr × Lean.Expr))

Materialise the persistent @[param] registry into the NameMap (Expr × Expr) that ParamTranslate.translate consumes: each stored (c', lemmaName) becomes (Expr.const c' [], Expr.const lemmaName []).

Equations

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

Driver command

def Transfer.Param.«command#param_translate_» : Lean.ParserDescr

#param_translate t runs the term-level parametricity translation ⟦t⟧ against the ambient @[param] registry (no explicit database), logging the transferred term and the type of the relatedness proof.

Equations

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