Theorem: run_denoteOp (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
name : String
res args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
⊢ run (denoteOp Δ (Op.mk name res args regions attrs)) env =
    run
      (do
        let args ← denoteOpArgs Δ args
        let ret ←
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
              (Semantics.semantics_op (IOp.mk name (List.map Prod.snd res) args (OpM.denoteRegions regions 0) attrs))
        match res with
          | [] => pure ret
          | [res] =>
            match ret with
            | [{ fst := τ, snd := v }] => do
              TopM.set τ res.fst v
              pure ret
            | x => do
              TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString ret ++ toString "'")
              pure ret
          | x => do
            TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'")
            pure ret)
      env
Tactic:
simp [denoteOp]
State after:
no goals