Compiler-owned call.rs constructors/drop queries. All keys use canonical shared type IDs and complete instances. Absent evidence remains an error.

structure Miri.Input.CompilerRuntimeQueries.TypeEntry : Type

• typeId : Nat
• pointerType : Nat
• referenceType : Nat
• dropGlue : Except String Interpreter.CallInstance

structure Miri.Input.CompilerRuntimeQueries.VirtualEntry : Type

• original : Interpreter.CallInstance
• methodDefinition : MIR.DefId
• parentTrait : MIR.DefId
• concreteType : Nat
• rebasedArgs : Array MIR.GenericArg
• resolved : Except String Interpreter.CallInstance

structure Miri.Input.CompilerRuntimeQueries.Prepared : Type

• program : LoweredProgram
• types : Array TypeEntry
• callerLocation : Array (Interpreter.CallInstance × Bool)
• virtualQueries : Array VirtualEntry

def Miri.Input.CompilerRuntimeQueries.prepare (program : LoweredProgram) : Except String Prepared

Equations

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

def Miri.Input.CompilerRuntimeQueries.mutPointerType (prepared : Prepared) (id : Nat) : Except String Nat

Equations

• Miri.Input.CompilerRuntimeQueries.mutPointerType prepared id = do let __do_lift ← Miri.Input.CompilerRuntimeQueries.entry✝ prepared id pure __do_lift.pointerType

def Miri.Input.CompilerRuntimeQueries.mutReferenceType (prepared : Prepared) (id : Nat) : Except String Nat

Equations

• Miri.Input.CompilerRuntimeQueries.mutReferenceType prepared id = do let __do_lift ← Miri.Input.CompilerRuntimeQueries.entry✝ prepared id pure __do_lift.referenceType

def Miri.Input.CompilerRuntimeQueries.resolveDropGlue (prepared : Prepared) (id : Nat) : Except String Interpreter.CallInstance

Equations

• Miri.Input.CompilerRuntimeQueries.resolveDropGlue prepared id = do let __do_lift ← Miri.Input.CompilerRuntimeQueries.entry✝ prepared id __do_lift.dropGlue

def Miri.Input.CompilerRuntimeQueries.requiresCallerLocation (prepared : Prepared) (callee : Interpreter.CallInstance) : Except String Bool

Equations

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

def Miri.Input.CompilerRuntimeQueries.parentTrait (prepared : Prepared) (method : MIR.DefId) : Except String MIR.DefId

Equations

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

def Miri.Input.CompilerRuntimeQueries.rebaseVirtualArgs (prepared : Prepared) (args : Array MIR.GenericArg) (parent : MIR.DefId) (concrete : Nat) : Except String (Array MIR.GenericArg)

Equations

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

def Miri.Input.CompilerRuntimeQueries.expectResolveForVTable (prepared : Prepared) (method : MIR.DefId) (args : Array MIR.GenericArg) : Except String Interpreter.CallInstance

Equations

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

def Miri.Input.CompilerRuntimeQueries.hooks {S C : Type} (prepared : Prepared) (base : Interpreter.VirtualCalls.CompilerHooks S C) : Interpreter.VirtualCalls.CompilerHooks S C

Equations

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