{-# 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
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
cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> ()
cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> ()
cover_UncertifiedOptTag_4 UncertifiedOptStage
x
  = case UncertifiedOptStage
x of
      UncertifiedOptStage
CaseOfCase -> ()
      UncertifiedOptStage
ConstantFolding -> ()
-- VerifiedCompilation.Trace.CertifiedOptTag
d_CertifiedOptTag_10 :: ()
d_CertifiedOptTag_10 = ()
type T_CertifiedOptTag_10 = CertifiedOptStage
pattern $mC_floatDelayT_12 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_floatDelayT_12 :: CertifiedOptStage
C_floatDelayT_12 = FloatDelay
pattern $mC_forceDelayT_14 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceDelayT_14 :: CertifiedOptStage
C_forceDelayT_14 = ForceDelay
pattern $mC_forceCaseDelayT_16 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceCaseDelayT_16 :: CertifiedOptStage
C_forceCaseDelayT_16 = ForceCaseDelay
pattern $mC_inlineT_18 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_inlineT_18 :: CertifiedOptStage
C_inlineT_18 = Inline
pattern $mC_cseT_20 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_cseT_20 :: CertifiedOptStage
C_cseT_20 = CSE
pattern $mC_applyToCaseT_22 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_applyToCaseT_22 :: CertifiedOptStage
C_applyToCaseT_22 = ApplyToCase
pattern $mC_caseReduceT_24 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseReduceT_24 :: CertifiedOptStage
C_caseReduceT_24 = CaseReduce
pattern $mC_letFloatOutT_26 :: forall {r}. CertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_letFloatOutT_26 :: CertifiedOptStage
C_letFloatOutT_26 = LetFloatOut
check_floatDelayT_12 :: T_CertifiedOptTag_10
check_floatDelayT_12 :: CertifiedOptStage
check_floatDelayT_12 = CertifiedOptStage
FloatDelay
check_forceDelayT_14 :: T_CertifiedOptTag_10
check_forceDelayT_14 :: CertifiedOptStage
check_forceDelayT_14 = CertifiedOptStage
ForceDelay
check_forceCaseDelayT_16 :: T_CertifiedOptTag_10
check_forceCaseDelayT_16 :: CertifiedOptStage
check_forceCaseDelayT_16 = CertifiedOptStage
ForceCaseDelay
check_inlineT_18 :: T_CertifiedOptTag_10
check_inlineT_18 :: CertifiedOptStage
check_inlineT_18 = CertifiedOptStage
Inline
check_cseT_20 :: T_CertifiedOptTag_10
check_cseT_20 :: CertifiedOptStage
check_cseT_20 = CertifiedOptStage
CSE
check_applyToCaseT_22 :: T_CertifiedOptTag_10
check_applyToCaseT_22 :: CertifiedOptStage
check_applyToCaseT_22 = CertifiedOptStage
ApplyToCase
check_caseReduceT_24 :: T_CertifiedOptTag_10
check_caseReduceT_24 :: CertifiedOptStage
check_caseReduceT_24 = CertifiedOptStage
CaseReduce
check_letFloatOutT_26 :: T_CertifiedOptTag_10
check_letFloatOutT_26 :: CertifiedOptStage
check_letFloatOutT_26 = CertifiedOptStage
LetFloatOut
cover_CertifiedOptTag_10 :: CertifiedOptStage -> ()
cover_CertifiedOptTag_10 :: CertifiedOptStage -> ()
cover_CertifiedOptTag_10 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_28 :: ()
d_OptTag_28 :: ()
d_OptTag_28 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.FloatDelayT
d_FloatDelayT_30 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_FloatDelayT_30 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_FloatDelayT_30
  = (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_12)
-- VerifiedCompilation.Trace.ForceDelayT
d_ForceDelayT_32 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_ForceDelayT_32 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ForceDelayT_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_forceDelayT_14)
-- VerifiedCompilation.Trace.ForceCaseDelayT
d_ForceCaseDelayT_34 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_ForceCaseDelayT_34 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ForceCaseDelayT_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_forceCaseDelayT_16)
-- VerifiedCompilation.Trace.InlineT
d_InlineT_36 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_InlineT_36 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_InlineT_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_inlineT_18)
-- VerifiedCompilation.Trace.CseT
d_CseT_38 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_CseT_38 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CseT_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_cseT_20)
-- VerifiedCompilation.Trace.ApplyToCaseT
d_ApplyToCaseT_40 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_ApplyToCaseT_40 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ApplyToCaseT_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_applyToCaseT_22)
-- VerifiedCompilation.Trace.LetFloatOutT
d_LetFloatOutT_42 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_LetFloatOutT_42 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_LetFloatOutT_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_letFloatOutT_26)
-- VerifiedCompilation.Trace.CaseReduceT
d_CaseReduceT_44 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_CaseReduceT_44 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CaseReduceT_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_caseReduceT_24)
-- VerifiedCompilation.Trace.CaseOfCaseT
d_CaseOfCaseT_46 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_CaseOfCaseT_46 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CaseOfCaseT_46
  = (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_48 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_10
d_ConstantFoldingT_48 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ConstantFoldingT_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_constantFoldingT_8)
-- VerifiedCompilation.Trace.InlineHints
d_InlineHints_50 :: ()
d_InlineHints_50 = ()
type T_InlineHints_50 = Hints.Inline
pattern $mC_var_52 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_var_52 :: Inline
C_var_52 = Hints.InlVar
pattern $mC_expand_54 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_expand_54 :: Inline -> Inline
C_expand_54 a0 = Hints.InlExpand a0
pattern $mC_ƛ_56 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_ƛ_56 :: Inline -> Inline
C_ƛ_56 a0 = Hints.InlLam a0
pattern $mC__'183'__58 :: forall {r}. Inline -> (Inline -> Inline -> r) -> ((# #) -> r) -> r
$bC__'183'__58 :: Inline -> Inline -> Inline
C__'183'__58 a0 a1 = Hints.InlApply a0 a1
pattern $mC__'183''8595'_60 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC__'183''8595'_60 :: Inline -> Inline
C__'183''8595'_60 a0 = Hints.InlDrop a0
pattern $mC_force_62 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_force_62 :: Inline -> Inline
C_force_62 a0 = Hints.InlForce a0
pattern $mC_delay_64 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_delay_64 :: Inline -> Inline
C_delay_64 a0 = Hints.InlDelay a0
pattern $mC_con_66 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_con_66 :: Inline
C_con_66 = Hints.InlCon
pattern $mC_builtin_68 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_builtin_68 :: Inline
C_builtin_68 = Hints.InlBuiltin
pattern $mC_error_70 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_error_70 :: Inline
C_error_70 = Hints.InlError
pattern $mC_constr_72 :: forall {r}. Inline -> ([Inline] -> r) -> ((# #) -> r) -> r
$bC_constr_72 :: [Inline] -> Inline
C_constr_72 a0 = Hints.InlConstr a0
pattern $mC_case_74 :: forall {r}.
Inline -> (Inline -> [Inline] -> r) -> ((# #) -> r) -> r
$bC_case_74 :: Inline -> [Inline] -> Inline
C_case_74 a0 a1 = Hints.InlCase a0 a1
check_var_52 :: T_InlineHints_50
check_var_52 :: Inline
check_var_52 = Inline
Hints.InlVar
check_expand_54 :: T_InlineHints_50 -> T_InlineHints_50
check_expand_54 :: Inline -> Inline
check_expand_54 = Inline -> Inline
Hints.InlExpand
check_ƛ_56 :: T_InlineHints_50 -> T_InlineHints_50
check_ƛ_56 :: Inline -> Inline
check_ƛ_56 = Inline -> Inline
Hints.InlLam
check__'183'__58 ::
  T_InlineHints_50 -> T_InlineHints_50 -> T_InlineHints_50
check__'183'__58 :: Inline -> Inline -> Inline
check__'183'__58 = Inline -> Inline -> Inline
Hints.InlApply
check__'183''8595'_60 :: T_InlineHints_50 -> T_InlineHints_50
check__'183''8595'_60 :: Inline -> Inline
check__'183''8595'_60 = Inline -> Inline
Hints.InlDrop
check_force_62 :: T_InlineHints_50 -> T_InlineHints_50
check_force_62 :: Inline -> Inline
check_force_62 = Inline -> Inline
Hints.InlForce
check_delay_64 :: T_InlineHints_50 -> T_InlineHints_50
check_delay_64 :: Inline -> Inline
check_delay_64 = Inline -> Inline
Hints.InlDelay
check_con_66 :: T_InlineHints_50
check_con_66 :: Inline
check_con_66 = Inline
Hints.InlCon
check_builtin_68 :: T_InlineHints_50
check_builtin_68 :: Inline
check_builtin_68 = Inline
Hints.InlBuiltin
check_error_70 :: T_InlineHints_50
check_error_70 :: Inline
check_error_70 = Inline
Hints.InlError
check_constr_72 ::
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_50 ->
  T_InlineHints_50
check_constr_72 :: [Inline] -> Inline
check_constr_72 = [Inline] -> Inline
Hints.InlConstr
check_case_74 ::
  T_InlineHints_50 ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_50 ->
  T_InlineHints_50
check_case_74 :: Inline -> [Inline] -> Inline
check_case_74 = Inline -> [Inline] -> Inline
Hints.InlCase
cover_InlineHints_50 :: Hints.Inline -> ()
cover_InlineHints_50 :: Inline -> ()
cover_InlineHints_50 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_76 :: ()
d_Hints_76 = ()
type T_Hints_76 = Hints.Hints
pattern $mC_inline_78 :: forall {r}. Hints -> (Inline -> r) -> ((# #) -> r) -> r
$bC_inline_78 :: Inline -> Hints
C_inline_78 a0 = Hints.Inline a0
pattern $mC_none_80 :: forall {r}. Hints -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_none_80 :: Hints
C_none_80 = Hints.NoHints
check_inline_78 :: T_InlineHints_50 -> T_Hints_76
check_inline_78 :: Inline -> Hints
check_inline_78 = Inline -> Hints
Hints.Inline
check_none_80 :: T_Hints_76
check_none_80 :: Hints
check_none_80 = Hints
Hints.NoHints
cover_Hints_76 :: Hints.Hints -> ()
cover_Hints_76 :: Hints -> ()
cover_Hints_76 Hints
x
  = case Hints
x of
      Hints.Inline Inline
_ -> ()
      Hints
Hints.NoHints -> ()
-- VerifiedCompilation.Trace.Trace
d_Trace_84 :: p -> ()
d_Trace_84 p
a0 = ()
data T_Trace_84
  = C_step_88 (MAlonzo.Code.Utils.T_Either_6
                 T_UncertifiedOptTag_4 T_CertifiedOptTag_10)
              T_Hints_76 AgdaAny T_Trace_84 |
    C_done_90 AgdaAny
-- VerifiedCompilation.Trace.head
d_head_94 :: T_Trace_84 -> AgdaAny
d_head_94 :: T_Trace_84 -> Any
d_head_94 T_Trace_84
v0
  = case T_Trace_84 -> T_Trace_84
forall a b. a -> b
coe T_Trace_84
v0 of
      C_step_88 T_Either_6 UncertifiedOptStage CertifiedOptStage
v1 Hints
v2 Any
v3 T_Trace_84
v4 -> Any -> Any
forall a b. a -> b
coe Any
v3
      C_done_90 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_Trace_84
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.Dump
d_Dump_100 :: ()
d_Dump_100 :: ()
d_Dump_100 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.toTrace
d_toTrace_102 ::
  [MAlonzo.Code.Utils.T__'215'__436
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_10)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_76
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  Maybe T_Trace_84
d_toTrace_102 :: [T__'215'__436
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__436 Hints (T__'215'__436 T_Untyped_208 T_Untyped_208))]
-> Maybe T_Trace_84
d_toTrace_102 [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_84
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_84
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_84)
-> 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_84
du_go_112 (Any -> Any
forall a b. a -> b
coe Any
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v2))
      [Any]
_ -> Maybe T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace._.go
d_go_112 ::
  MAlonzo.Code.Utils.T__'215'__436
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_10)
    (MAlonzo.Code.Utils.T__'215'__436
       T_Hints_76
       (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_10)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_76
        (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_10)
    (MAlonzo.Code.Utils.T__'215'__436
       T_Hints_76
       (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_10)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_76
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_84
d_go_112 :: 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_84
d_go_112 ~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_84
du_go_112 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_112 ::
  MAlonzo.Code.Utils.T__'215'__436
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_10)
    (MAlonzo.Code.Utils.T__'215'__436
       T_Hints_76
       (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_10)
     (MAlonzo.Code.Utils.T__'215'__436
        T_Hints_76
        (MAlonzo.Code.Utils.T__'215'__436
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_84
du_go_112 :: 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_84
du_go_112 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_84 -> T_Trace_84)
-> Any -> Any -> Any -> Any -> T_Trace_84
forall a b. a -> b
coe
                                  T_Either_6 UncertifiedOptStage CertifiedOptStage
-> Hints -> Any -> T_Trace_84 -> T_Trace_84
C_step_88 (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_84) -> Any -> Any
forall a b. a -> b
coe Any -> T_Trace_84
C_done_90 (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_84 -> T_Trace_84)
-> Any -> Any -> Any -> Any -> T_Trace_84
forall a b. a -> b
coe
                                                       T_Either_6 UncertifiedOptStage CertifiedOptStage
-> Hints -> Any -> T_Trace_84 -> T_Trace_84
C_step_88 (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_84)
-> 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_84
du_go_112
                                                          ((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_84
forall a. a
MAlonzo.RTE.mazUnreachableError
                                         (Any, Any)
_ -> T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  (Any, Any)
_ -> T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
                           [Any]
_ -> T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
                    (Any, Any)
_ -> T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
             (Any, Any)
_ -> T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
      (Any, Any)
_ -> T_Trace_84
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.EvalResult
d_EvalResult_138 :: ()
d_EvalResult_138 = ()
type T_EvalResult_138 = EvalResult
pattern $mC_success_140 :: forall {r}.
EvalResult -> (Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_success_140 :: Integer -> Integer -> EvalResult
C_success_140 a0 a1 = EvalSuccess a0 a1
pattern $mC_failure_142 :: forall {r}.
EvalResult
-> (EvalError -> Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_failure_142 :: EvalError -> Integer -> Integer -> EvalResult
C_failure_142 a0 a1 a2 = EvalFailure a0 a1 a2
check_success_140 :: Integer -> Integer -> T_EvalResult_138
check_success_140 :: Integer -> Integer -> EvalResult
check_success_140 = Integer -> Integer -> EvalResult
EvalSuccess
check_failure_142 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  Integer -> Integer -> T_EvalResult_138
check_failure_142 :: EvalError -> Integer -> Integer -> EvalResult
check_failure_142 = EvalError -> Integer -> Integer -> EvalResult
EvalFailure
cover_EvalResult_138 :: EvalResult -> ()
cover_EvalResult_138 :: EvalResult -> ()
cover_EvalResult_138 EvalResult
x
  = case EvalResult
x of
      EvalSuccess Integer
_ Integer
_ -> ()
      EvalFailure EvalError
_ Integer
_ Integer
_ -> ()