{-# 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_letFloatOutT_8 :: forall {r}.
UncertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_letFloatOutT_8 :: UncertifiedOptStage
C_letFloatOutT_8 = LetFloatOut
pattern $mC_caseReduceT_10 :: forall {r}.
UncertifiedOptStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseReduceT_10 :: UncertifiedOptStage
C_caseReduceT_10 = CaseReduce
check_caseOfCaseT_6 :: T_UncertifiedOptTag_4
check_caseOfCaseT_6 :: UncertifiedOptStage
check_caseOfCaseT_6 = UncertifiedOptStage
CaseOfCase
check_letFloatOutT_8 :: T_UncertifiedOptTag_4
check_letFloatOutT_8 :: UncertifiedOptStage
check_letFloatOutT_8 = UncertifiedOptStage
LetFloatOut
check_caseReduceT_10 :: T_UncertifiedOptTag_4
check_caseReduceT_10 :: UncertifiedOptStage
check_caseReduceT_10 = UncertifiedOptStage
CaseReduce
cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> ()
cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> ()
cover_UncertifiedOptTag_4 UncertifiedOptStage
x
  = case UncertifiedOptStage
x of
      UncertifiedOptStage
CaseOfCase -> ()
      UncertifiedOptStage
LetFloatOut -> ()
      UncertifiedOptStage
CaseReduce -> ()
-- 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
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
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 -> ()
-- VerifiedCompilation.Trace.OptTag
d_OptTag_26 :: ()
d_OptTag_26 :: ()
d_OptTag_26 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.FloatDelayT
d_FloatDelayT_28 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_FloatDelayT_28 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_FloatDelayT_28
  = (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_30 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ForceDelayT_30 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ForceDelayT_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_forceDelayT_16)
-- VerifiedCompilation.Trace.ForceCaseDelayT
d_ForceCaseDelayT_32 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ForceCaseDelayT_32 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ForceCaseDelayT_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_forceCaseDelayT_18)
-- VerifiedCompilation.Trace.InlineT
d_InlineT_34 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_InlineT_34 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_InlineT_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_inlineT_20)
-- VerifiedCompilation.Trace.CseT
d_CseT_36 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_CseT_36 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CseT_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_cseT_22)
-- VerifiedCompilation.Trace.ApplyToCaseT
d_ApplyToCaseT_38 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_ApplyToCaseT_38 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_ApplyToCaseT_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_applyToCaseT_24)
-- VerifiedCompilation.Trace.CaseOfCaseT
d_CaseOfCaseT_40 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
d_CaseOfCaseT_40 :: T_Either_6 UncertifiedOptStage CertifiedOptStage
d_CaseOfCaseT_40
  = (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.LetFloatOutT
d_LetFloatOutT_42 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
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}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (UncertifiedOptStage -> Any
forall a b. a -> b
coe UncertifiedOptStage
C_letFloatOutT_8)
-- VerifiedCompilation.Trace.CaseReduceT
d_CaseReduceT_44 ::
  MAlonzo.Code.Utils.T_Either_6
    T_UncertifiedOptTag_4 T_CertifiedOptTag_12
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}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12 (UncertifiedOptStage -> Any
forall a b. a -> b
coe UncertifiedOptStage
C_caseReduceT_10)
-- VerifiedCompilation.Trace.InlineHints
d_InlineHints_46 :: ()
d_InlineHints_46 = ()
type T_InlineHints_46 = Hints.Inline
pattern $mC_var_48 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_var_48 :: Inline
C_var_48 = Hints.InlVar
pattern $mC_expand_50 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_expand_50 :: Inline -> Inline
C_expand_50 a0 = Hints.InlExpand a0
pattern $mC_ƛ_52 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_ƛ_52 :: Inline -> Inline
C_ƛ_52 a0 = Hints.InlLam a0
pattern $mC__'183'__54 :: forall {r}. Inline -> (Inline -> Inline -> r) -> ((# #) -> r) -> r
$bC__'183'__54 :: Inline -> Inline -> Inline
C__'183'__54 a0 a1 = Hints.InlApply a0 a1
pattern $mC__'183''8595'_56 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC__'183''8595'_56 :: Inline -> Inline
C__'183''8595'_56 a0 = Hints.InlDrop a0
pattern $mC_force_58 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_force_58 :: Inline -> Inline
C_force_58 a0 = Hints.InlForce a0
pattern $mC_delay_60 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_delay_60 :: Inline -> Inline
C_delay_60 a0 = Hints.InlDelay a0
pattern $mC_con_62 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_con_62 :: Inline
C_con_62 = Hints.InlCon
pattern $mC_builtin_64 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_builtin_64 :: Inline
C_builtin_64 = Hints.InlBuiltin
pattern $mC_error_66 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_error_66 :: Inline
C_error_66 = Hints.InlError
pattern $mC_constr_68 :: forall {r}. Inline -> ([Inline] -> r) -> ((# #) -> r) -> r
$bC_constr_68 :: [Inline] -> Inline
C_constr_68 a0 = Hints.InlConstr a0
pattern $mC_case_70 :: forall {r}.
Inline -> (Inline -> [Inline] -> r) -> ((# #) -> r) -> r
$bC_case_70 :: Inline -> [Inline] -> Inline
C_case_70 a0 a1 = Hints.InlCase a0 a1
check_var_48 :: T_InlineHints_46
check_var_48 :: Inline
check_var_48 = Inline
Hints.InlVar
check_expand_50 :: T_InlineHints_46 -> T_InlineHints_46
check_expand_50 :: Inline -> Inline
check_expand_50 = Inline -> Inline
Hints.InlExpand
check_ƛ_52 :: T_InlineHints_46 -> T_InlineHints_46
check_ƛ_52 :: Inline -> Inline
check_ƛ_52 = Inline -> Inline
Hints.InlLam
check__'183'__54 ::
  T_InlineHints_46 -> T_InlineHints_46 -> T_InlineHints_46
check__'183'__54 :: Inline -> Inline -> Inline
check__'183'__54 = Inline -> Inline -> Inline
Hints.InlApply
check__'183''8595'_56 :: T_InlineHints_46 -> T_InlineHints_46
check__'183''8595'_56 :: Inline -> Inline
check__'183''8595'_56 = Inline -> Inline
Hints.InlDrop
check_force_58 :: T_InlineHints_46 -> T_InlineHints_46
check_force_58 :: Inline -> Inline
check_force_58 = Inline -> Inline
Hints.InlForce
check_delay_60 :: T_InlineHints_46 -> T_InlineHints_46
check_delay_60 :: Inline -> Inline
check_delay_60 = Inline -> Inline
Hints.InlDelay
check_con_62 :: T_InlineHints_46
check_con_62 :: Inline
check_con_62 = Inline
Hints.InlCon
check_builtin_64 :: T_InlineHints_46
check_builtin_64 :: Inline
check_builtin_64 = Inline
Hints.InlBuiltin
check_error_66 :: T_InlineHints_46
check_error_66 :: Inline
check_error_66 = Inline
Hints.InlError
check_constr_68 ::
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_46 ->
  T_InlineHints_46
check_constr_68 :: [Inline] -> Inline
check_constr_68 = [Inline] -> Inline
Hints.InlConstr
check_case_70 ::
  T_InlineHints_46 ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_46 ->
  T_InlineHints_46
check_case_70 :: Inline -> [Inline] -> Inline
check_case_70 = Inline -> [Inline] -> Inline
Hints.InlCase
cover_InlineHints_46 :: Hints.Inline -> ()
cover_InlineHints_46 :: Inline -> ()
cover_InlineHints_46 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_72 :: ()
d_Hints_72 = ()
type T_Hints_72 = Hints.Hints
pattern $mC_inline_74 :: forall {r}. Hints -> (Inline -> r) -> ((# #) -> r) -> r
$bC_inline_74 :: Inline -> Hints
C_inline_74 a0 = Hints.Inline a0
pattern $mC_none_76 :: forall {r}. Hints -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_none_76 :: Hints
C_none_76 = Hints.NoHints
check_inline_74 :: T_InlineHints_46 -> T_Hints_72
check_inline_74 :: Inline -> Hints
check_inline_74 = Inline -> Hints
Hints.Inline
check_none_76 :: T_Hints_72
check_none_76 :: Hints
check_none_76 = Hints
Hints.NoHints
cover_Hints_72 :: Hints.Hints -> ()
cover_Hints_72 :: Hints -> ()
cover_Hints_72 Hints
x
  = case Hints
x of
      Hints.Inline Inline
_ -> ()
      Hints
Hints.NoHints -> ()
-- VerifiedCompilation.Trace.Trace
d_Trace_80 :: p -> ()
d_Trace_80 p
a0 = ()
data T_Trace_80
  = C_step_84 (MAlonzo.Code.Utils.T_Either_6
                 T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
              T_Hints_72 AgdaAny T_Trace_80 |
    C_done_86 AgdaAny
-- VerifiedCompilation.Trace.head
d_head_90 :: T_Trace_80 -> AgdaAny
d_head_90 :: T_Trace_80 -> Any
d_head_90 T_Trace_80
v0
  = case T_Trace_80 -> T_Trace_80
forall a b. a -> b
coe T_Trace_80
v0 of
      C_step_84 T_Either_6 UncertifiedOptStage CertifiedOptStage
v1 Hints
v2 Any
v3 T_Trace_80
v4 -> Any -> Any
forall a b. a -> b
coe Any
v3
      C_done_86 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_Trace_80
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.Dump
d_Dump_96 :: ()
d_Dump_96 :: ()
d_Dump_96 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.toTrace
d_toTrace_98 ::
  [MAlonzo.Code.Utils.T__'215'__428
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_72
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  Maybe T_Trace_80
d_toTrace_98 :: [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> Maybe T_Trace_80
d_toTrace_98 [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v0
  = case [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> [Any]
forall a b. a -> b
coe [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v0 of
      [] -> Maybe Any -> Maybe T_Trace_80
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_80
forall a b. a -> b
coe
             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
 -> [T__'215'__428
       (T_Either_6 UncertifiedOptStage CertifiedOptStage)
       (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
 -> T_Trace_80)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_80
du_go_108 (Any -> Any
forall a b. a -> b
coe Any
v1) ([Any] -> Any
forall a b. a -> b
coe [Any]
v2))
      [Any]
_ -> Maybe T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace._.go
d_go_108 ::
  MAlonzo.Code.Utils.T__'215'__428
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
    (MAlonzo.Code.Utils.T__'215'__428
       T_Hints_72
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__428
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_72
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  MAlonzo.Code.Utils.T__'215'__428
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
    (MAlonzo.Code.Utils.T__'215'__428
       T_Hints_72
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__428
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_72
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_80
d_go_108 :: T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T__'215'__428
     (T_Either_6 UncertifiedOptStage CertifiedOptStage)
     (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_80
d_go_108 ~T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v0 ~[T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v1 T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v2 [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v3 = T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_80
du_go_108 T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v2 [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v3
du_go_108 ::
  MAlonzo.Code.Utils.T__'215'__428
    (MAlonzo.Code.Utils.T_Either_6
       T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
    (MAlonzo.Code.Utils.T__'215'__428
       T_Hints_72
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__428
     (MAlonzo.Code.Utils.T_Either_6
        T_UncertifiedOptTag_4 T_CertifiedOptTag_12)
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_72
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_80
du_go_108 :: T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_80
du_go_108 T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v0 [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v1
  = case T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> (Any, Any)
forall a b. a -> b
coe T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v0 of
      MAlonzo.Code.Utils.C__'44'__442 Any
v2 Any
v3
        -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v3 of
             MAlonzo.Code.Utils.C__'44'__442 Any
v4 Any
v5
               -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v5 of
                    MAlonzo.Code.Utils.C__'44'__442 Any
v6 Any
v7
                      -> case [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> [Any]
forall a b. a -> b
coe [T__'215'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v1 of
                           []
                             -> (T_Either_6 UncertifiedOptStage CertifiedOptStage
 -> Hints -> Any -> T_Trace_80 -> T_Trace_80)
-> Any -> Any -> Any -> Any -> T_Trace_80
forall a b. a -> b
coe
                                  T_Either_6 UncertifiedOptStage CertifiedOptStage
-> Hints -> Any -> T_Trace_80 -> T_Trace_80
C_step_84 (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_80) -> Any -> Any
forall a b. a -> b
coe Any -> T_Trace_80
C_done_86 (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'__442 Any
v10 Any
v11
                                    -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v11 of
                                         MAlonzo.Code.Utils.C__'44'__442 Any
v12 Any
v13
                                           -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v13 of
                                                MAlonzo.Code.Utils.C__'44'__442 Any
v14 Any
v15
                                                  -> (T_Either_6 UncertifiedOptStage CertifiedOptStage
 -> Hints -> Any -> T_Trace_80 -> T_Trace_80)
-> Any -> Any -> Any -> Any -> T_Trace_80
forall a b. a -> b
coe
                                                       T_Either_6 UncertifiedOptStage CertifiedOptStage
-> Hints -> Any -> T_Trace_80 -> T_Trace_80
C_step_84 (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'__428
   (T_Either_6 UncertifiedOptStage CertifiedOptStage)
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
 -> [T__'215'__428
       (T_Either_6 UncertifiedOptStage CertifiedOptStage)
       (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
 -> T_Trace_80)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T__'215'__428
  (T_Either_6 UncertifiedOptStage CertifiedOptStage)
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      (T_Either_6 UncertifiedOptStage CertifiedOptStage)
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_80
du_go_108
                                                          ((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'__442
                                                             (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'__442
                                                                (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'__442
                                                                   (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_80
forall a. a
MAlonzo.RTE.mazUnreachableError
                                         (Any, Any)
_ -> T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  (Any, Any)
_ -> T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
                           [Any]
_ -> T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
                    (Any, Any)
_ -> T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
             (Any, Any)
_ -> T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
      (Any, Any)
_ -> T_Trace_80
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.EvalResult
d_EvalResult_134 :: ()
d_EvalResult_134 = ()
type T_EvalResult_134 = EvalResult
pattern $mC_success_136 :: forall {r}.
EvalResult -> (Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_success_136 :: Integer -> Integer -> EvalResult
C_success_136 a0 a1 = EvalSuccess a0 a1
pattern $mC_failure_138 :: forall {r}.
EvalResult
-> (EvalError -> Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_failure_138 :: EvalError -> Integer -> Integer -> EvalResult
C_failure_138 a0 a1 a2 = EvalFailure a0 a1 a2
check_success_136 :: Integer -> Integer -> T_EvalResult_134
check_success_136 :: Integer -> Integer -> EvalResult
check_success_136 = Integer -> Integer -> EvalResult
EvalSuccess
check_failure_138 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  Integer -> Integer -> T_EvalResult_134
check_failure_138 :: EvalError -> Integer -> Integer -> EvalResult
check_failure_138 = EvalError -> Integer -> Integer -> EvalResult
EvalFailure
cover_EvalResult_134 :: EvalResult -> ()
cover_EvalResult_134 :: EvalResult -> ()
cover_EvalResult_134 EvalResult
x
  = case EvalResult
x of
      EvalSuccess Integer
_ Integer
_ -> ()
      EvalFailure EvalError
_ Integer
_ Integer
_ -> ()