Public source-facing compiler symbol hooks. The metadata parser and lookup policy live in the lower-level CompilerForeignSymbolTables module, allowing CompilerProviders to retain one immutable preparation result without a module cycle.

@[reducible, inline]

abbrev Miri.Input.CompilerForeignSymbols.Candidate : Type

Equations

• Miri.Input.CompilerForeignSymbols.Candidate = Miri.Input.CompilerForeignSymbolTables.Candidate

@[reducible, inline]

abbrev Miri.Input.CompilerForeignSymbols.AllocatorTarget : Type

Equations

• Miri.Input.CompilerForeignSymbols.AllocatorTarget = Miri.Input.CompilerForeignSymbolTables.AllocatorTarget

@[reducible, inline]

abbrev Miri.Input.CompilerForeignSymbols.AllocatorEntry : Type

Equations

• Miri.Input.CompilerForeignSymbols.AllocatorEntry = Miri.Input.CompilerForeignSymbolTables.AllocatorEntry

@[reducible, inline]

abbrev Miri.Input.CompilerForeignSymbols.Prepared : Type

Equations

• Miri.Input.CompilerForeignSymbols.Prepared = Miri.Input.CompilerForeignSymbolTables.Prepared

def Miri.Input.CompilerForeignSymbols.prepare (instances : CompilerVTableRuntime.Prepared) : Except String Prepared

Equations

• Miri.Input.CompilerForeignSymbols.prepare instances = Miri.Input.CompilerForeignSymbolTables.prepare instances

def Miri.Input.CompilerForeignSymbols.lookup (prepared : Prepared) (symbol : String) : Except Interpreter.StepError (Option Candidate)

Equations

• Miri.Input.CompilerForeignSymbols.lookup prepared symbol = Miri.Input.CompilerForeignSymbolTables.lookup prepared symbol

def Miri.Input.CompilerForeignSymbols.lookupFunction {S : Type} (prepared : Prepared) (loadMir : Interpreter.CallInstance → EStateM Interpreter.StepError S Interpreter.LoadedBody) (symbol : String) : EStateM Interpreter.StepError S (Option (Interpreter.LoadedBody × Interpreter.CallInstance))

Equations

• Miri.Input.CompilerForeignSymbols.lookupFunction prepared loadMir symbol = Miri.Input.CompilerForeignSymbolTables.lookupFunction prepared loadMir symbol

def Miri.Input.CompilerForeignSymbols.allocatorSymbol (prepared : Prepared) (symbol : String) : Option (Interpreter.ForeignItems.AllocatorSymbol Interpreter.CallInstance)

Equations

• Miri.Input.CompilerForeignSymbols.allocatorSymbol prepared symbol = Miri.Input.CompilerForeignSymbolTables.allocatorSymbol prepared symbol

def Miri.Input.CompilerForeignSymbols.checkSymbolClash (prepared : Prepared) (symbol : String) : Except Interpreter.StepError Unit

Equations

• Miri.Input.CompilerForeignSymbols.checkSymbolClash prepared symbol = Miri.Input.CompilerForeignSymbolTables.checkSymbolClash prepared symbol

def Miri.Input.CompilerForeignSymbols.options (prepared : Prepared) (base : EvalForeignConstruction.Options) : EvalForeignConstruction.Options

Equations

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

def Miri.Input.CompilerForeignSymbols.hooks {S : Type} (prepared : Prepared) (calls : CompilerCallPipeline.Prepared) : EvalForeignConstruction.Symbols S

Equations

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