instance instParseableTuple {α : Type (max u_1 u_2)} {β : Type (max u_1 u_2)} [A : Cli.ParseableType α] [B : Cli.ParseableType β] : Cli.ParseableType (α × β)

Parse a tuple

Equations

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

@[reducible, inline]

abbrev MContext (φ : ℕ) : Type

Equations

• MContext φ = Ctxt (InstCombine.MTy φ)

@[reducible, inline]

abbrev Context : Type

Equations

• Context = MContext 0

@[reducible, inline]

abbrev MCom (φ : ℕ) : Ctxt (InstCombine.MetaLLVM φ).Ty → EffectKind → (InstCombine.MetaLLVM φ).Ty → Type

Equations

• MCom φ = Com (InstCombine.MetaLLVM φ)

@[reducible, inline]

abbrev MExpr (φ : ℕ) (Γ : Ctxt (InstCombine.MetaLLVM φ).Ty) (eff : EffectKind) (ty : (InstCombine.MetaLLVM φ).Ty) : Type

Equations

• MExpr φ = Expr (InstCombine.MetaLLVM φ)

instance instToStringContext : ToString Context

Equations

• instToStringContext = inferInstanceAs (ToString (List (InstCombine.MTy 0)))

structure CliTest : Type

• name : Lean.Name
• mvars : ℕ
• context : MContext self.mvars
• ty : InstCombine.MTy self.mvars
• eff : EffectKind
• code : MCom self.mvars self.context self.eff self.ty

def CliTest.signature (test : CliTest) : List (InstCombine.MTy test.mvars) × InstCombine.MTy test.mvars

Equations

• test.signature = (test.context, test.ty)

theorem natParamsTup (n : ℕ) : n > 0 → natParams (n + 1) = (ℕ × natParams n)

def instParseableNatParams {n : ℕ} : Cli.ParseableType (natParams n)

instance instParseableTypeNatParams {n : ℕ} : Cli.ParseableType (natParams n)

Equations

• instParseableTypeNatParams = instParseableNatParams

def CliTest.params : CliTest → Type

Equations

• x.params = natParams x.mvars

def CliTest.paramsParseable (test : CliTest) : Cli.ParseableType test.params

Equations

• test.paramsParseable = instParseableNatParams

instance instParseableTypeBitVec_sSA {n : ℕ} : Cli.ParseableType (BitVec n)

Equations

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

def CliTest.concrete : CliTest → Prop

We can only execute tests that are concrete. This property ensures that they are concrete, i.e. have no metavariables (mvars = 0)

Equations

• test.concrete = (test.mvars = 0)

instance instDecidableConcrete {test : CliTest} : Decidable test.concrete

Equations

• instDecidableConcrete = inferInstanceAs (DecidableEq ℕ) test.mvars 0

structure ConcreteCliTest : Type

• name : Lean.Name
• context : Context
• ty : InstCombine.Ty
• code : MCom 0 self.context EffectKind.pure self.ty

def InstCombine.MTy.cast_concrete (mvars : ℕ) (ty : InstCombine.MTy mvars) (hMvars : mvars = 0) : InstCombine.MTy 0

Equations

• InstCombine.MTy.cast_concrete mvars ty hMvars = hMvars ▸ ty

def InstCombine.MTy.cast_concrete? (mvars : ℕ) (ty : InstCombine.MTy mvars) : Option (InstCombine.MTy 0)

Equations

• InstCombine.MTy.cast_concrete? mvars ty = if h : mvars = 0 then some (InstCombine.MTy.cast_concrete mvars ty h) else none

def MLIR.AST.Context.cast_concrete (mvars : ℕ) (ctxt : MContext mvars) (hMVars : mvars = 0) : MContext 0

Equations

• MLIR.AST.Context.cast_concrete mvars ctxt hMVars = hMVars ▸ ctxt

def MLIR.AST.Context.cast_concrete? (mvars : ℕ) (ctxt : MContext mvars) : Option (MContext 0)

Equations

• MLIR.AST.Context.cast_concrete? mvars ctxt = if h : mvars = 0 then some (MLIR.AST.Context.cast_concrete mvars ctxt h) else none

def InstCombine.mkValuation (ctxt : MContext 0) (values : Mathlib.Vector (Option ℤ) (List.length ctxt)) : Ctxt.Valuation ctxt

Equations

• InstCombine.mkValuation [] ⟨[], property⟩ = Ctxt.Valuation.nil
• InstCombine.mkValuation (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w) :: tys) ⟨val :: vals, hlen_2⟩ = (InstCombine.mkValuation tys ⟨vals, ⋯⟩::ᵥOption.map (BitVec.ofInt w) val)

def ConcreteCliTest.eval (test : ConcreteCliTest) (values : Mathlib.Vector (Option ℤ) (List.length test.context)) : IO ⟦test.ty⟧

Equations

• test.eval values = pure (Com.denote test.code (InstCombine.mkValuation test.context values.reverse))

def ConcreteCliTest.eval? (test : ConcreteCliTest) (values : Array (Option ℤ)) : IO (Except String ⟦test.ty⟧)

Equations

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

def ConcreteCliTest.parseableInputs (test : ConcreteCliTest) : Cli.ParseableType (Mathlib.Vector ℤ (List.length test.context))

Equations

• test.parseableInputs = inferInstance

def CocreteCliTest.signature (test : ConcreteCliTest) : List (InstCombine.MTy 0) × InstCombine.MTy 0

Equations

• CocreteCliTest.signature test = (List.reverse test.context, test.ty)

def ConcreteCliTest.printSignature (test : ConcreteCliTest) : String

Equations

• test.printSignature = toString "" ++ toString (List.reverse test.context) ++ toString " → " ++ toString test.ty ++ toString ""

instance instToStringToTypeTyTy {test : ConcreteCliTest} : ToString ⟦test.ty⟧

Equations

• instToStringToTypeTyTy = { toString := match (motive := (x : InstCombine.Ty) → ⟦x⟧ → String) test.ty with | InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w) => toString }

@[reducible, inline]

abbrev NameExt : Type

Equations

• NameExt = Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name)

def llvmTest : Lean.ParserDescr

Equations

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

opaque llvmExtension : NameExt

def termLlvmTests! : Lean.ParserDescr

Equations

• termLlvmTests! = Lean.ParserDescr.node `termLlvmTests! 1024 (Lean.ParserDescr.symbol "llvmTests!")