{-# 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.InlineHints⁺
d_InlineHints'8314'_82 :: p -> ()
d_InlineHints'8314'_82 p
a0 = ()
type T_InlineHints'8314'_82 a0 = Hints.InlinePlus a0
pattern $mC__'8593''7511'_86 :: forall {r} {term}.
InlinePlus term -> (Inline -> r) -> ((# #) -> r) -> r
$bC__'8593''7511'_86 :: forall {term}. Inline -> InlinePlus term
C__'8593''7511'_86 a0 = Hints.InlOne a0
pattern $mC__'10814''91'_'93'__88 :: forall {r} {term}.
InlinePlus term
-> (Inline -> term -> InlinePlus term -> r) -> ((# #) -> r) -> r
$bC__'10814''91'_'93'__88 :: forall {term}. Inline -> term -> InlinePlus term -> InlinePlus term
C__'10814''91'_'93'__88 a0 a1 a2 = Hints.InlSeq a0 a1 a2
check__'8593''7511'_86 ::
  forall xA. T_InlineHints_54 -> T_InlineHints'8314'_82 xA
check__'8593''7511'_86 :: forall {term}. Inline -> InlinePlus term
check__'8593''7511'_86 = Inline -> InlinePlus xA
forall {term}. Inline -> InlinePlus term
Hints.InlOne
check__'10814''91'_'93'__88 ::
  forall xA.
    T_InlineHints_54 ->
    xA -> T_InlineHints'8314'_82 xA -> T_InlineHints'8314'_82 xA
check__'10814''91'_'93'__88 :: forall {term}. Inline -> term -> InlinePlus term -> InlinePlus term
check__'10814''91'_'93'__88 = Inline -> xA -> InlinePlus xA -> InlinePlus xA
forall {term}. Inline -> term -> InlinePlus term -> InlinePlus term
Hints.InlSeq
cover_InlineHints'8314'_82 :: Hints.InlinePlus a1 -> ()
cover_InlineHints'8314'_82 :: forall a1. InlinePlus a1 -> ()
cover_InlineHints'8314'_82 InlinePlus a1
x
  = case InlinePlus a1
x of
      Hints.InlOne Inline
_ -> ()
      Hints.InlSeq Inline
_ a1
_ InlinePlus a1
_ -> ()
-- VerifiedCompilation.Trace.Hints
d_Hints_92 :: p -> ()
d_Hints_92 p
a0 = ()
type T_Hints_92 a0 = Hints.Hints a0
pattern $mC_inline_96 :: forall {r} {term}.
Hints term -> (InlinePlus term -> r) -> ((# #) -> r) -> r
$bC_inline_96 :: forall {term}. InlinePlus term -> Hints term
C_inline_96 a0 = Hints.Inline a0
pattern $mC_none_98 :: forall {r} {term}. Hints term -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_none_98 :: forall {term}. Hints term
C_none_98 = Hints.NoHints
check_inline_96 ::
  forall xA. T_InlineHints'8314'_82 xA -> T_Hints_92 xA
check_inline_96 :: forall {term}. InlinePlus term -> Hints term
check_inline_96 = InlinePlus xA -> Hints xA
forall {term}. InlinePlus term -> Hints term
Hints.Inline
check_none_98 :: forall xA. T_Hints_92 xA
check_none_98 :: forall {term}. Hints term
check_none_98 = Hints xA
forall {term}. Hints term
Hints.NoHints
cover_Hints_92 :: Hints.Hints a1 -> ()
cover_Hints_92 :: forall a1. Hints a1 -> ()
cover_Hints_92 Hints a1
x
  = case Hints a1
x of
      Hints.Inline InlinePlus a1
_ -> ()
      Hints a1
Hints.NoHints -> ()
-- VerifiedCompilation.Trace.NonEmptySep
d_NonEmptySep_104 :: p -> p -> ()
d_NonEmptySep_104 p
a0 p
a1 = ()
type T_NonEmptySep_104 a0 a1 = NES.NonEmptySep a0 a1
pattern $mC_cons_110 :: forall {r} {sep} {a}.
NonEmptySep sep a
-> (a -> sep -> NonEmptySep sep a -> r) -> ((# #) -> r) -> r
$bC_cons_110 :: forall {sep} {a}.
a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
C_cons_110 a0 a1 a2 = NES.Cons a0 a1 a2
pattern $mC_singleton_112 :: forall {r} {sep} {a}.
NonEmptySep sep a -> (a -> r) -> ((# #) -> r) -> r
$bC_singleton_112 :: forall {sep} {a}. a -> NonEmptySep sep a
C_singleton_112 a0 = NES.Singleton a0
check_cons_110 ::
  forall xS.
    forall xA.
      xA -> xS -> T_NonEmptySep_104 xS xA -> T_NonEmptySep_104 xS xA
check_cons_110 :: forall {sep} {a}.
a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
check_cons_110 = xA -> xS -> NonEmptySep xS xA -> NonEmptySep xS xA
forall {sep} {a}.
a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
NES.Cons
check_singleton_112 ::
  forall xS. forall xA. xA -> T_NonEmptySep_104 xS xA
check_singleton_112 :: forall {sep} {a}. a -> NonEmptySep sep a
check_singleton_112 = xA -> NonEmptySep xS xA
forall {sep} {a}. a -> NonEmptySep sep a
NES.Singleton
cover_NonEmptySep_104 :: NES.NonEmptySep a1 a2 -> ()
cover_NonEmptySep_104 :: forall a1 a2. NonEmptySep a1 a2 -> ()
cover_NonEmptySep_104 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_126 :: T_NonEmptySep_104 AgdaAny AgdaAny -> AgdaAny
d_head_126 :: T_NonEmptySep_104 Any Any -> Any
d_head_126 T_NonEmptySep_104 Any Any
v0
  = case T_NonEmptySep_104 Any Any -> T_NonEmptySep_104 Any Any
forall a b. a -> b
coe T_NonEmptySep_104 Any Any
v0 of
      C_cons_110 Any
v1 Any
v2 T_NonEmptySep_104 Any Any
v3 -> Any -> Any
forall a b. a -> b
coe Any
v1
      C_singleton_112 Any
v1 -> Any -> Any
forall a b. a -> b
coe Any
v1
      T_NonEmptySep_104 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.Trace
d_Trace_132 :: () -> ()
d_Trace_132 :: () -> ()
d_Trace_132 = () -> ()
forall a. a
erased
-- VerifiedCompilation.Trace.EvalResult
d_EvalResult_136 :: ()
d_EvalResult_136 = ()
type T_EvalResult_136 = EvalResult
pattern $mC_success_138 :: forall {r}.
EvalResult -> (Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_success_138 :: Integer -> Integer -> EvalResult
C_success_138 a0 a1 = EvalSuccess a0 a1
pattern $mC_failure_140 :: forall {r}.
EvalResult
-> (EvalError -> Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_failure_140 :: EvalError -> Integer -> Integer -> EvalResult
C_failure_140 a0 a1 a2 = EvalFailure a0 a1 a2
check_success_138 :: Integer -> Integer -> T_EvalResult_136
check_success_138 :: Integer -> Integer -> EvalResult
check_success_138 = Integer -> Integer -> EvalResult
EvalSuccess
check_failure_140 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  Integer -> Integer -> T_EvalResult_136
check_failure_140 :: EvalError -> Integer -> Integer -> EvalResult
check_failure_140 = EvalError -> Integer -> Integer -> EvalResult
EvalFailure
cover_EvalResult_136 :: EvalResult -> ()
cover_EvalResult_136 :: EvalResult -> ()
cover_EvalResult_136 EvalResult
x
  = case EvalResult
x of
      EvalSuccess Integer
_ Integer
_ -> ()
      EvalFailure EvalError
_ Integer
_ Integer
_ -> ()