{-# 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.String
import qualified MAlonzo.Code.Utils

import UntypedPlutusCore.Transform.Certify.Trace
import qualified UntypedPlutusCore.Transform.Certify.Hints as Hints
import qualified Data.List.NonEmptySep as NES
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.NonEmptySep
d_NonEmptySep_90 :: p -> p -> ()
d_NonEmptySep_90 p
a0 p
a1 = ()
type T_NonEmptySep_90 a0 a1 = NES.NonEmptySep a0 a1
pattern $mC_cons_96 :: forall {r} {sep} {a}.
NonEmptySep sep a
-> (a -> sep -> NonEmptySep sep a -> r) -> ((# #) -> r) -> r
$bC_cons_96 :: forall {sep} {a}.
a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
C_cons_96 a0 a1 a2 = NES.Cons a0 a1 a2
pattern $mC_singleton_98 :: forall {r} {sep} {a}.
NonEmptySep sep a -> (a -> r) -> ((# #) -> r) -> r
$bC_singleton_98 :: forall {sep} {a}. a -> NonEmptySep sep a
C_singleton_98 a0 = NES.Singleton a0
check_cons_96 ::
  forall xS.
    forall xA.
      xA -> xS -> T_NonEmptySep_90 xS xA -> T_NonEmptySep_90 xS xA
check_cons_96 :: forall {sep} {a}.
a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
check_cons_96 = xA -> xS -> NonEmptySep xS xA -> NonEmptySep xS xA
forall {sep} {a}.
a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
NES.Cons
check_singleton_98 ::
  forall xS. forall xA. xA -> T_NonEmptySep_90 xS xA
check_singleton_98 :: forall {sep} {a}. a -> NonEmptySep sep a
check_singleton_98 = xA -> NonEmptySep xS xA
forall {sep} {a}. a -> NonEmptySep sep a
NES.Singleton
cover_NonEmptySep_90 :: NES.NonEmptySep a1 a2 -> ()
cover_NonEmptySep_90 :: forall a1 a2. NonEmptySep a1 a2 -> ()
cover_NonEmptySep_90 NonEmptySep a1 a2
x
  = case NonEmptySep a1 a2
x of
      NES.Cons a2
_ a1
_ NonEmptySep a1 a2
_ -> ()
      NES.Singleton a2
_ -> ()
-- VerifiedCompilation.Trace.head
d_head_112 :: T_NonEmptySep_90 AgdaAny AgdaAny -> AgdaAny
d_head_112 :: T_NonEmptySep_90 Any Any -> Any
d_head_112 T_NonEmptySep_90 Any Any
v0
  = case T_NonEmptySep_90 Any Any -> T_NonEmptySep_90 Any Any
forall a b. a -> b
coe T_NonEmptySep_90 Any Any
v0 of
      C_cons_96 Any
v1 Any
v2 T_NonEmptySep_90 Any Any
v3 -> Any -> Any
forall a b. a -> b
coe Any
v1
      C_singleton_98 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonEmptySep_90 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.Trace
d_Trace_118 :: () -> ()
d_Trace_118 :: () -> ()
d_Trace_118 = () -> ()
forall a. a
erased
-- VerifiedCompilation.Trace.EvalResult
d_EvalResult_122 :: ()
d_EvalResult_122 = ()
type T_EvalResult_122 = EvalResult
pattern $mC_success_124 :: forall {r}.
EvalResult -> (Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_success_124 :: Integer -> Integer -> EvalResult
C_success_124 a0 a1 = EvalSuccess a0 a1
pattern $mC_failure_126 :: forall {r}.
EvalResult
-> (EvalError -> Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_failure_126 :: EvalError -> Integer -> Integer -> EvalResult
C_failure_126 a0 a1 a2 = EvalFailure a0 a1 a2
check_success_124 :: Integer -> Integer -> T_EvalResult_122
check_success_124 :: Integer -> Integer -> EvalResult
check_success_124 = Integer -> Integer -> EvalResult
EvalSuccess
check_failure_126 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  Integer -> Integer -> T_EvalResult_122
check_failure_126 :: EvalError -> Integer -> Integer -> EvalResult
check_failure_126 = EvalError -> Integer -> Integer -> EvalResult
EvalFailure
cover_EvalResult_122 :: EvalResult -> ()
cover_EvalResult_122 :: EvalResult -> ()
cover_EvalResult_122 EvalResult
x
  = case EvalResult
x of
      EvalSuccess Integer
_ Integer
_ -> ()
      EvalFailure EvalError
_ Integer
_ Integer
_ -> ()