Compiler shape/query adapters for Cast and ValidityVisitor. Definition and TypeConst IDs are appended to the existing shared bundle, never source indices. Dynamic-predicate tokens index an explicit shared table of original compiler predicate arrays; vtable consumers must use this same table and still discharge normalization/stable-comparison queries.

@[reducible, inline]

abbrev Miri.Input.CompilerFactAdapters.Result (α : Type u_1) : Type u_1

Equations

• Miri.Input.CompilerFactAdapters.Result = Except String

inductive Miri.Input.CompilerFactAdapters.PatternIdentity : Type

Canonical source pattern identities; range constants share the program's TypeConst table and Or children share this pattern table.

• range (start finish : MIR.TypeConstId) : PatternIdentity
• or (children : Array Nat) : PatternIdentity
• notNull : PatternIdentity

def Miri.Input.CompilerFactAdapters.instReprPatternIdentity.repr : PatternIdentity → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Miri.Input.CompilerFactAdapters.instReprPatternIdentity : Repr PatternIdentity

Equations

• Miri.Input.CompilerFactAdapters.instReprPatternIdentity = { reprPrec := Miri.Input.CompilerFactAdapters.instReprPatternIdentity.repr }

def Miri.Input.CompilerFactAdapters.instDecidableEqPatternIdentity.decEq (x✝ x✝¹ : PatternIdentity) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Miri.Input.CompilerFactAdapters.instDecidableEqPatternIdentity.decEq Miri.Input.CompilerFactAdapters.PatternIdentity.notNull Miri.Input.CompilerFactAdapters.PatternIdentity.notNull = isTrue ⋯

@[instance_reducible]

instance Miri.Input.CompilerFactAdapters.instDecidableEqPatternIdentity : DecidableEq PatternIdentity

Equations

• Miri.Input.CompilerFactAdapters.instDecidableEqPatternIdentity = Miri.Input.CompilerFactAdapters.instDecidableEqPatternIdentity.decEq

structure Miri.Input.CompilerFactAdapters.Prepared : Type

• context : CompilerFacts.Context
• dynamicPredicates : Array Lean.Json
• patterns : Array PatternIdentity
• castTypes : Array (TypeId × Result Interpreter.CastTypeInfo)
• obligations : Array Obligation

def Miri.Input.CompilerFactAdapters.prepare (context : CompilerFacts.Context) : Result Prepared

Equations

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

def Miri.Input.CompilerFactAdapters.castTypeInfo (prepared : Prepared) (id : TypeId) : Result Interpreter.CastTypeInfo

Equations

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

def Miri.Input.CompilerFactAdapters.validityKind (prepared : Prepared) (id : TypeId) : Result Interpreter.ValidityVisitor.TypeKind

Equations

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

def Miri.Input.CompilerFactAdapters.metadataTail (prepared : Prepared) (id : TypeId) : Result Interpreter.ValidityVisitor.MetadataTail

Equations

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

def Miri.Input.CompilerFactAdapters.castHooks {P S C V : Type} (prepared : Prepared) (machine : Interpreter.CastHooks P S C V) : Interpreter.CastHooks P S C V

Equations

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

def Miri.Input.CompilerFactAdapters.validityHooks {P S C E Fn Abi Pad : Type} (prepared : Prepared) (machine : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad) : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad

Equations

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

theorem Miri.Input.CompilerFactAdapters.validity_typeName_of_node {P S C E Fn Abi Pad : Type} (prepared : Prepared) (machine : Interpreter.ValidityVisitor.Hooks P S C E Fn Abi Pad) (choice : C) (ty : TypeId) (node : TypeNode) (found : prepared.context.runtime.node ty = Except.ok node) : (validityHooks prepared machine).typeName choice ty = pure node.display

The diagnostic type name is a pure compiler-node projection.