{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.VerifiedCompilation.Trace where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Utils

import UntypedPlutusCore.Transform.Certify.Trace
import qualified UntypedPlutusCore.Transform.Certify.Hints as Hints
import FFI.CostInfo
-- VerifiedCompilation.Trace.UncertifiedOptTag
d_UncertifiedOptTag_4 :: ()
d_UncertifiedOptTag_4 = ()
type T_UncertifiedOptTag_4 = UncertifiedOptStage
pattern $mC_caseOfCaseT_6 :: forall {r}.
UncertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseOfCaseT_6 :: UncertifiedOptStage
C_caseOfCaseT_6 = CaseOfCase
pattern $mC_constantFoldingT_8 :: forall {r}.
UncertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_constantFoldingT_8 :: UncertifiedOptStage
C_constantFoldingT_8 = ConstantFolding
pattern $mC_polyBuiltinT_10 :: forall {r}.
UncertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_polyBuiltinT_10 :: UncertifiedOptStage
C_polyBuiltinT_10 = PolyBuiltin
check_caseOfCaseT_6 :: T_UncertifiedOptTag_4
check_caseOfCaseT_6 :: UncertifiedOptStage
check_caseOfCaseT_6 = UncertifiedOptStage
CaseOfCase
check_constantFoldingT_8 :: T_UncertifiedOptTag_4
check_constantFoldingT_8 :: UncertifiedOptStage
check_constantFoldingT_8 = UncertifiedOptStage
ConstantFolding
check_polyBuiltinT_10 :: T_UncertifiedOptTag_4
check_polyBuiltinT_10 :: UncertifiedOptStage
check_polyBuiltinT_10 = UncertifiedOptStage
PolyBuiltin
cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> ()
cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> ()
cover_UncertifiedOptTag_4 UncertifiedOptStage
x
  = case UncertifiedOptStage
x of
      UncertifiedOptStage
CaseOfCase -> ()
      UncertifiedOptStage
ConstantFolding -> ()
      UncertifiedOptStage
PolyBuiltin -> ()
-- VerifiedCompilation.Trace.CertifiedOptTag
d_CertifiedOptTag_12 :: ()
d_CertifiedOptTag_12 = ()
type T_CertifiedOptTag_12 = CertifiedOptStage
pattern $mC_floatDelayT_14 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_floatDelayT_14 :: CertifiedOptStage
C_floatDelayT_14 = FloatDelay
pattern $mC_forceDelayT_16 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceDelayT_16 :: CertifiedOptStage
C_forceDelayT_16 = ForceDelay
pattern $mC_forceCaseDelayT_18 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceCaseDelayT_18 :: CertifiedOptStage
C_forceCaseDelayT_18 = ForceCaseDelay
pattern $mC_inlineT_20 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_inlineT_20 :: CertifiedOptStage
C_inlineT_20 = Inline
pattern $mC_cseT_22 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_cseT_22 :: CertifiedOptStage
C_cseT_22 = CSE
pattern $mC_applyToCaseT_24 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_applyToCaseT_24 :: CertifiedOptStage
C_applyToCaseT_24 = ApplyToCase
pattern $mC_caseReduceT_26 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseReduceT_26 :: CertifiedOptStage
C_caseReduceT_26 = CaseReduce
pattern $mC_letFloatOutT_28 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_letFloatOutT_28 :: CertifiedOptStage
C_letFloatOutT_28 = LetFloatOut
check_floatDelayT_14 :: T_CertifiedOptTag_12
check_floatDelayT_14 :: CertifiedOptStage
check_floatDelayT_14 = CertifiedOptStage
FloatDelay
check_forceDelayT_16 :: T_CertifiedOptTag_12
check_forceDelayT_16 :: CertifiedOptStage
check_forceDelayT_16 = CertifiedOptStage
ForceDelay
check_forceCaseDelayT_18 :: T_CertifiedOptTag_12
check_forceCaseDelayT_18 :: CertifiedOptStage
check_forceCaseDelayT_18 = CertifiedOptStage
ForceCaseDelay
check_inlineT_20 :: T_CertifiedOptTag_12
check_inlineT_20 :: CertifiedOptStage
check_inlineT_20 = CertifiedOptStage
Inline
check_cseT_22 :: T_CertifiedOptTag_12
check_cseT_22 :: CertifiedOptStage
check_cseT_22 = CertifiedOptStage
CSE
check_applyToCaseT_24 :: T_CertifiedOptTag_12
check_applyToCaseT_24 :: CertifiedOptStage
check_applyToCaseT_24 = CertifiedOptStage
ApplyToCase
check_caseReduceT_26 :: T_CertifiedOptTag_12
check_caseReduceT_26 :: CertifiedOptStage
check_caseReduceT_26 = CertifiedOptStage
CaseReduce
check_letFloatOutT_28 :: T_CertifiedOptTag_12
check_letFloatOutT_28 :: CertifiedOptStage
check_letFloatOutT_28 = CertifiedOptStage
LetFloatOut
cover_CertifiedOptTag_12 :: CertifiedOptStage -> ()
cover_CertifiedOptTag_12 :: CertifiedOptStage -> ()
cover_CertifiedOptTag_12 CertifiedOptStage
x
  = case CertifiedOptStage
x of
      CertifiedOptStage
FloatDelay -> ()
      CertifiedOptStage
ForceDelay -> ()
      CertifiedOptStage
ForceCaseDelay -> ()
      CertifiedOptStage
Inline -> ()
      CertifiedOptStage
CSE -> ()
      CertifiedOptStage
ApplyToCase -> ()
      CertifiedOptStage
CaseReduce -> ()
      CertifiedOptStage
LetFloatOut -> ()
-- VerifiedCompilation.Trace.OptTag
d_OptTag_30 :: ()
d_OptTag_30 :: ()
d_OptTag_30 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.FloatDelayT
d_FloatDelayT_32 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_FloatDelayT_32 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_FloatDelayT_32
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_floatDelayT_14)
-- VerifiedCompilation.Trace.ForceDelayT
d_ForceDelayT_34 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ForceDelayT_34 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ForceDelayT_34
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_forceDelayT_16)
-- VerifiedCompilation.Trace.ForceCaseDelayT
d_ForceCaseDelayT_36 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ForceCaseDelayT_36 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ForceCaseDelayT_36
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_forceCaseDelayT_18)
-- VerifiedCompilation.Trace.InlineT
d_InlineT_38 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_InlineT_38 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_InlineT_38
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_inlineT_20)
-- VerifiedCompilation.Trace.CseT
d_CseT_40 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_CseT_40 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CseT_40 = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_cseT_22)
-- VerifiedCompilation.Trace.ApplyToCaseT
d_ApplyToCaseT_42 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ApplyToCaseT_42 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ApplyToCaseT_42
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_applyToCaseT_24)
-- VerifiedCompilation.Trace.LetFloatOutT
d_LetFloatOutT_44 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_LetFloatOutT_44 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_LetFloatOutT_44
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_letFloatOutT_28)
-- VerifiedCompilation.Trace.CaseReduceT
d_CaseReduceT_46 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_CaseReduceT_46 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CaseReduceT_46
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (CertifiedOptStage -> Any
forall a b. a -> b
coe CertifiedOptStage
C_caseReduceT_26)
-- VerifiedCompilation.Trace.CaseOfCaseT
d_CaseOfCaseT_48 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_CaseOfCaseT_48 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CaseOfCaseT_48
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (UncertifiedOptStage -> Any
forall a b. a -> b
coe UncertifiedOptStage
C_caseOfCaseT_6)
-- VerifiedCompilation.Trace.ConstantFoldingT
d_ConstantFoldingT_50 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ConstantFoldingT_50 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ConstantFoldingT_50
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (UncertifiedOptStage -> Any
forall a b. a -> b
coe UncertifiedOptStage
C_constantFoldingT_8)
-- VerifiedCompilation.Trace.PolyBuiltinT
d_PolyBuiltinT_52 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_PolyBuiltinT_52 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_PolyBuiltinT_52
  = (Any -> Either Any Any)
-> Any -> T_Either_6 UncertifiedOptStage CertifiedOptStage
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (UncertifiedOptStage -> Any
forall a b. a -> b
coe UncertifiedOptStage
C_polyBuiltinT_10)
-- VerifiedCompilation.Trace.InlineHints
d_InlineHints_54 :: ()
d_InlineHints_54 = ()
type T_InlineHints_54 = Hints.Inline
pattern $mC_var_56 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_var_56 :: Inline
C_var_56 = Hints.InlVar
pattern $mC_expand_58 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_expand_58 :: Inline -> Inline
C_expand_58 a0 = Hints.InlExpand a0
pattern $mC_ƛ_60 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_ƛ_60 :: Inline -> Inline
C_ƛ_60 a0 = Hints.InlLam a0
pattern $mC__'183'__62 :: forall {r}. Inline -> (Inline -> Inline -> r) -> ((# #) -> r) -> r
$bC__'183'__62 :: Inline -> Inline -> Inline
C__'183'__62 a0 a1 = Hints.InlApply a0 a1
pattern $mC__'183''8595'_64 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC__'183''8595'_64 :: Inline -> Inline
C__'183''8595'_64 a0 = Hints.InlDrop a0
pattern $mC_force_66 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_force_66 :: Inline -> Inline
C_force_66 a0 = Hints.InlForce a0
pattern $mC_delay_68 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_delay_68 :: Inline -> Inline
C_delay_68 a0 = Hints.InlDelay a0
pattern $mC_con_70 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_con_70 :: Inline
C_con_70 = Hints.InlCon
pattern $mC_builtin_72 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_builtin_72 :: Inline
C_builtin_72 = Hints.InlBuiltin
pattern $mC_error_74 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_error_74 :: Inline
C_error_74 = Hints.InlError
pattern $mC_constr_76 :: forall {r}. Inline -> ([Inline] -> r) -> ((# #) -> r) -> r
$bC_constr_76 :: [Inline] -> Inline
C_constr_76 a0 = Hints.InlConstr a0
pattern $mC_case_78 :: forall {r}.
Inline -> (Inline -> [Inline] -> r) -> ((# #) -> r) -> r
$bC_case_78 :: Inline -> [Inline] -> Inline
C_case_78 a0 a1 = Hints.InlCase a0 a1
check_var_56 :: T_InlineHints_54
check_var_56 :: Inline
check_var_56 = Inline
Hints.InlVar
check_expand_58 :: T_InlineHints_54 -> T_InlineHints_54
check_expand_58 :: Inline -> Inline
check_expand_58 = Inline -> Inline
Hints.InlExpand
check_ƛ_60 :: T_InlineHints_54 -> T_InlineHints_54
check_ƛ_60 :: Inline -> Inline
check_ƛ_60 = Inline -> Inline
Hints.InlLam
check__'183'__62 ::
  T_InlineHints_54 -> T_InlineHints_54 -> T_InlineHints_54
check__'183'__62 :: Inline -> Inline -> Inline
check__'183'__62 = Inline -> Inline -> Inline
Hints.InlApply
check__'183''8595'_64 :: T_InlineHints_54 -> T_InlineHints_54
check__'183''8595'_64 :: Inline -> Inline
check__'183''8595'_64 = Inline -> Inline
Hints.InlDrop
check_force_66 :: T_InlineHints_54 -> T_InlineHints_54
check_force_66 :: Inline -> Inline
check_force_66 = Inline -> Inline
Hints.InlForce
check_delay_68 :: T_InlineHints_54 -> T_InlineHints_54
check_delay_68 :: Inline -> Inline
check_delay_68 = Inline -> Inline
Hints.InlDelay
check_con_70 :: T_InlineHints_54
check_con_70 :: Inline
check_con_70 = Inline
Hints.InlCon
check_builtin_72 :: T_InlineHints_54
check_builtin_72 :: Inline
check_builtin_72 = Inline
Hints.InlBuiltin
check_error_74 :: T_InlineHints_54
check_error_74 :: Inline
check_error_74 = Inline
Hints.InlError
check_constr_76 ::
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_54 ->
  T_InlineHints_54
check_constr_76 :: [Inline] -> Inline
check_constr_76 = [Inline] -> Inline
Hints.InlConstr
check_case_78 ::
  T_InlineHints_54 ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_54 ->
  T_InlineHints_54
check_case_78 :: Inline -> [Inline] -> Inline
check_case_78 = Inline -> [Inline] -> Inline
Hints.InlCase
cover_InlineHints_54 :: Hints.Inline -> ()
cover_InlineHints_54 :: Inline -> ()
cover_InlineHints_54 Inline
x
  = case Inline
x of
      Inline
Hints.InlVar -> ()
      Hints.InlExpand Inline
_ -> ()
      Hints.InlLam Inline
_ -> ()
      Hints.InlApply Inline
_ Inline
_ -> ()
      Hints.InlDrop Inline
_ -> ()
      Hints.InlForce Inline
_ -> ()
      Hints.InlDelay Inline
_ -> ()
      Inline
Hints.InlCon -> ()
      Inline
Hints.InlBuiltin -> ()
      Inline
Hints.InlError -> ()
      Hints.InlConstr [Inline]
_ -> ()
      Hints.InlCase Inline
_ [Inline]
_ -> ()
-- VerifiedCompilation.Trace.Hints
d_Hints_80 :: ()
d_Hints_80 = ()
type T_Hints_80 = Hints.Hints
pattern $mC_inline_82 :: forall {r}. Hints -> (Inline -> r) -> ((# #) -> r) -> r
$bC_inline_82 :: Inline -> Hints
C_inline_82 a0 = Hints.Inline a0
pattern $mC_none_84 :: forall {r}. Hints -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_none_84 :: Hints
C_none_84 = Hints.NoHints
check_inline_82 :: T_InlineHints_54 -> T_Hints_80
check_inline_82 :: Inline -> Hints
check_inline_82 = Inline -> Hints
Hints.Inline
check_none_84 :: T_Hints_80
check_none_84 :: Hints
check_none_84 = Hints
Hints.NoHints
cover_Hints_80 :: Hints.Hints -> ()
cover_Hints_80 :: Hints -> ()
cover_Hints_80 Hints
x
  = case Hints
x of
      Hints.Inline Inline
_ -> ()
      Hints
Hints.NoHints -> ()
-- VerifiedCompilation.Trace.Trace
d_Trace_88 :: p -> ()
d_Trace_88 p
a0 = ()
data T_Trace_88
  = C_step_92 (MAlonzo.Code.Utils.T_Either_6
                 T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
              T_Hints_80 AgdaAny T_Trace_88 |
    C_done_94 AgdaAny
-- VerifiedCompilation.Trace.head
d_head_98 :: T_Trace_88 -> AgdaAny
d_head_98 :: T_Trace_88 -> Any
d_head_98 T_Trace_88
v0
  = case T_Trace_88 -> T_Trace_88
forall a b. a -> b
coe T_Trace_88
v0 of
      C_step_92 T_Either_6 UncertifiedOptStage CertifiedOptStage
v1 Hints
v2 Any
v3 T_Trace_88
v4 -> Any -> Any
forall a b. a -> b
coe Any
v3
      C_done_94 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_Trace_88
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.Dump
d_Dump_104 :: ()
d_Dump_104 :: ()
d_Dump_104 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.toTrace
d_toTrace_106 ::
  [MAlonzo.Code.Utils.T__'215'__436
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_80
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  Maybe T_Trace_88
d_toTrace_106 :: [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> Maybe T_Trace_88
d_toTrace_106 [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v0
  = case [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> [Any]
forall a b. a -> b
coe [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v0 of
      [] -> Maybe Any -> Maybe T_Trace_88
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      (:) Any
v1 [Any]
v2
        -> (Any -> Maybe Any) -> Any -> Maybe T_Trace_88
forall a b. a -> b
coe
             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
 -> [T__'215'__436
       (T_Either_6 UncertifiedOptStage CertifiedOptStage)
       (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
 -> T_Trace_88)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> [T__'215'__436
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> T_Trace_88
du_go_116 (Any -> Any
forall a b. a -> b
coe Any
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v2))
      [Any]
_ -> Maybe T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace._.go
d_go_116 ::
  MAlonzo.Code.Utils.T__'215'__436
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
    (MAlonzo.Code.Utils.T__'215'__436
       T_Hints_80
       (MAlonzo.Code.Utils.T__'215'__436
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__436
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_80
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  MAlonzo.Code.Utils.T__'215'__436
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
    (MAlonzo.Code.Utils.T__'215'__436
       T_Hints_80
       (MAlonzo.Code.Utils.T__'215'__436
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__436
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_80
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_88
d_go_116 :: T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> [T__'215'__436
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> T__'215'__436
     (T_Either_6 UncertifiedOptStage CertifiedOptStage)
     (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> [T__'215'__436
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> T_Trace_88
d_go_116 ~T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
v0 ~[T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v1 T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
v2 [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v3 = T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> [T__'215'__436
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> T_Trace_88
du_go_116 T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
v2 [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v3
du_go_116 ::
  MAlonzo.Code.Utils.T__'215'__436
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
    (MAlonzo.Code.Utils.T__'215'__436
       T_Hints_80
       (MAlonzo.Code.Utils.T__'215'__436
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__436
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_80
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_88
du_go_116 :: T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> [T__'215'__436
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> T_Trace_88
du_go_116 T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
v0 [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v1
  = case T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> (Any, Any)
forall a b. a -> b
coe T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
v0 of
      MAlonzo.Code.Utils.C__'44'__450 Any
v2 Any
v3
        -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v3 of
             MAlonzo.Code.Utils.C__'44'__450 Any
v4 Any
v5
               -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v5 of
                    MAlonzo.Code.Utils.C__'44'__450 Any
v6 Any
v7
                      -> case [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> [Any]
forall a b. a -> b
coe [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
v1 of
                           []
                             -> (T_Either_6 UncertifiedOptStage CertifiedOptStage
 -> Hints -> Any -> T_Trace_88 -> T_Trace_88)
-> Any -> Any -> Any -> Any -> T_Trace_88
forall a b. a -> b
coe
                                  T_Either_6 UncertifiedOptStage CertifiedOptStage
-> Hints -> Any -> T_Trace_88 -> T_Trace_88
C_step_92 (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v6) ((Any -> T_Trace_88) -> Any -> Any
forall a b. a -> b
coe Any -> T_Trace_88
C_done_94 (Any -> Any
forall a b. a -> b
coe Any
v7))
                           (:) Any
v8 [Any]
v9
                             -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v8 of
                                  MAlonzo.Code.Utils.C__'44'__450 Any
v10 Any
v11
                                    -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v11 of
                                         MAlonzo.Code.Utils.C__'44'__450 Any
v12 Any
v13
                                           -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v13 of
                                                MAlonzo.Code.Utils.C__'44'__450 Any
v14 Any
v15
                                                  -> (T_Either_6 UncertifiedOptStage CertifiedOptStage
 -> Hints -> Any -> T_Trace_88 -> T_Trace_88)
-> Any -> Any -> Any -> Any -> T_Trace_88
forall a b. a -> b
coe
                                                       T_Either_6 UncertifiedOptStage CertifiedOptStage
-> Hints -> Any -> T_Trace_88 -> T_Trace_88
C_step_92 (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v4) (Any -> Any
forall a b. a -> b
coe Any
v6)
                                                       ((T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
 -> [T__'215'__436
       (T_Either_6 UncertifiedOptStage CertifiedOptStage)
       (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
 -> T_Trace_88)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T__'215'__436
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))
-> [T__'215'__436
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> T_Trace_88
du_go_116
                                                          ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                             Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__450
                                                             (Any -> Any
forall a b. a -> b
coe Any
v10)
                                                             ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__450
                                                                (Any -> Any
forall a b. a -> b
coe Any
v12)
                                                                ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                   Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__450
                                                                   (Any -> Any
forall a b. a -> b
coe Any
v7) (Any -> Any
forall a b. a -> b
coe Any
v15))))
                                                          ([Any] -> Any
forall a b. a -> b
coe [Any]
v9))
                                                (Any, Any)
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
                                         (Any, Any)
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  (Any, Any)
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
                           [Any]
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
                    (Any, Any)
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
             (Any, Any)
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
      (Any, Any)
_ -> T_Trace_88
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.EvalResult
d_EvalResult_142 :: ()
d_EvalResult_142 = ()
type T_EvalResult_142 = EvalResult
pattern $mC_success_144 :: forall {r}.
EvalResult -> (Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_success_144 :: Integer -> Integer -> EvalResult
C_success_144 a0 a1 = EvalSuccess a0 a1
pattern $mC_failure_146 :: forall {r}.
EvalResult
-> (EvalError -> Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_failure_146 :: EvalError -> Integer -> Integer -> EvalResult
C_failure_146 a0 a1 a2 = EvalFailure a0 a1 a2
check_success_144 :: Integer -> Integer -> T_EvalResult_142
check_success_144 :: Integer -> Integer -> EvalResult
check_success_144 = Integer -> Integer -> EvalResult
EvalSuccess
check_failure_146 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  Integer -> Integer -> T_EvalResult_142
check_failure_146 :: EvalError -> Integer -> Integer -> EvalResult
check_failure_146 = EvalError -> Integer -> Integer -> EvalResult
EvalFailure
cover_EvalResult_142 :: EvalResult -> ()
cover_EvalResult_142 :: EvalResult -> ()
cover_EvalResult_142 EvalResult
x
  = case EvalResult
x of
      EvalSuccess Integer
_ Integer
_ -> ()
      EvalFailure EvalError
_ Integer
_ Integer
_ -> ()