{-# 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.Simplifier
import UntypedPlutusCore.Transform.Certify.Trace
import qualified UntypedPlutusCore.Transform.Certify.Hints as Hints
import FFI.CostInfo
-- VerifiedCompilation.Trace.SimplifierTag
d_SimplifierTag_4 :: ()
d_SimplifierTag_4 = ()
type T_SimplifierTag_4 = SimplifierStage
pattern $mC_floatDelayT_6 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_floatDelayT_6 :: SimplifierStage
C_floatDelayT_6 = FloatDelay
pattern $mC_forceDelayT_8 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceDelayT_8 :: SimplifierStage
C_forceDelayT_8 = ForceDelay
pattern $mC_forceCaseDelayT_10 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_forceCaseDelayT_10 :: SimplifierStage
C_forceCaseDelayT_10 = ForceCaseDelay
pattern $mC_caseOfCaseT_12 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseOfCaseT_12 :: SimplifierStage
C_caseOfCaseT_12 = CaseOfCase
pattern $mC_caseReduceT_14 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseReduceT_14 :: SimplifierStage
C_caseReduceT_14 = CaseReduce
pattern $mC_inlineT_16 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_inlineT_16 :: SimplifierStage
C_inlineT_16 = Inline
pattern $mC_cseT_18 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_cseT_18 :: SimplifierStage
C_cseT_18 = CSE
pattern $mC_applyToCaseT_20 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_applyToCaseT_20 :: SimplifierStage
C_applyToCaseT_20 = ApplyToCase
pattern $mC_letFloatOutT_22 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_letFloatOutT_22 :: SimplifierStage
C_letFloatOutT_22 = LetFloatOut
pattern $mC_unknown_24 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_unknown_24 :: SimplifierStage
C_unknown_24 = Unknown
check_floatDelayT_6 :: T_SimplifierTag_4
check_floatDelayT_6 :: SimplifierStage
check_floatDelayT_6 = SimplifierStage
FloatDelay
check_forceDelayT_8 :: T_SimplifierTag_4
check_forceDelayT_8 :: SimplifierStage
check_forceDelayT_8 = SimplifierStage
ForceDelay
check_forceCaseDelayT_10 :: T_SimplifierTag_4
check_forceCaseDelayT_10 :: SimplifierStage
check_forceCaseDelayT_10 = SimplifierStage
ForceCaseDelay
check_caseOfCaseT_12 :: T_SimplifierTag_4
check_caseOfCaseT_12 :: SimplifierStage
check_caseOfCaseT_12 = SimplifierStage
CaseOfCase
check_caseReduceT_14 :: T_SimplifierTag_4
check_caseReduceT_14 :: SimplifierStage
check_caseReduceT_14 = SimplifierStage
CaseReduce
check_inlineT_16 :: T_SimplifierTag_4
check_inlineT_16 :: SimplifierStage
check_inlineT_16 = SimplifierStage
Inline
check_cseT_18 :: T_SimplifierTag_4
check_cseT_18 :: SimplifierStage
check_cseT_18 = SimplifierStage
CSE
check_applyToCaseT_20 :: T_SimplifierTag_4
check_applyToCaseT_20 :: SimplifierStage
check_applyToCaseT_20 = SimplifierStage
ApplyToCase
check_letFloatOutT_22 :: T_SimplifierTag_4
check_letFloatOutT_22 :: SimplifierStage
check_letFloatOutT_22 = SimplifierStage
LetFloatOut
check_unknown_24 :: T_SimplifierTag_4
check_unknown_24 :: SimplifierStage
check_unknown_24 = SimplifierStage
Unknown
cover_SimplifierTag_4 :: SimplifierStage -> ()
cover_SimplifierTag_4 :: SimplifierStage -> ()
cover_SimplifierTag_4 SimplifierStage
x
  = case SimplifierStage
x of
      SimplifierStage
FloatDelay -> ()
      SimplifierStage
ForceDelay -> ()
      SimplifierStage
ForceCaseDelay -> ()
      SimplifierStage
CaseOfCase -> ()
      SimplifierStage
CaseReduce -> ()
      SimplifierStage
Inline -> ()
      SimplifierStage
CSE -> ()
      SimplifierStage
ApplyToCase -> ()
      SimplifierStage
LetFloatOut -> ()
      SimplifierStage
Unknown -> ()
-- VerifiedCompilation.Trace.InlineHints
d_InlineHints_26 :: ()
d_InlineHints_26 = ()
type T_InlineHints_26 = Hints.Inline
pattern $mC_var_28 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_var_28 :: Inline
C_var_28 = Hints.InlVar
pattern $mC_expand_30 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_expand_30 :: Inline -> Inline
C_expand_30 a0 = Hints.InlExpand a0
pattern $mC_ƛ_32 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_ƛ_32 :: Inline -> Inline
C_ƛ_32 a0 = Hints.InlLam a0
pattern $mC_ƛ'8595'_34 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_ƛ'8595'_34 :: Inline -> Inline
C_ƛ'8595'_34 a0 = Hints.InlLamDrop a0
pattern $mC__'183'__36 :: forall {r}. Inline -> (Inline -> Inline -> r) -> ((# #) -> r) -> r
$bC__'183'__36 :: Inline -> Inline -> Inline
C__'183'__36 a0 a1 = Hints.InlApply a0 a1
pattern $mC__'183''8595'_38 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC__'183''8595'_38 :: Inline -> Inline
C__'183''8595'_38 a0 = Hints.InlDrop a0
pattern $mC_force_40 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_force_40 :: Inline -> Inline
C_force_40 a0 = Hints.InlForce a0
pattern $mC_delay_42 :: forall {r}. Inline -> (Inline -> r) -> ((# #) -> r) -> r
$bC_delay_42 :: Inline -> Inline
C_delay_42 a0 = Hints.InlDelay a0
pattern $mC_con_44 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_con_44 :: Inline
C_con_44 = Hints.InlCon
pattern $mC_builtin_46 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_builtin_46 :: Inline
C_builtin_46 = Hints.InlBuiltin
pattern $mC_error_48 :: forall {r}. Inline -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_error_48 :: Inline
C_error_48 = Hints.InlError
pattern $mC_constr_50 :: forall {r}. Inline -> ([Inline] -> r) -> ((# #) -> r) -> r
$bC_constr_50 :: [Inline] -> Inline
C_constr_50 a0 = Hints.InlConstr a0
pattern $mC_case_52 :: forall {r}.
Inline -> (Inline -> [Inline] -> r) -> ((# #) -> r) -> r
$bC_case_52 :: Inline -> [Inline] -> Inline
C_case_52 a0 a1 = Hints.InlCase a0 a1
check_var_28 :: T_InlineHints_26
check_var_28 :: Inline
check_var_28 = Inline
Hints.InlVar
check_expand_30 :: T_InlineHints_26 -> T_InlineHints_26
check_expand_30 :: Inline -> Inline
check_expand_30 = Inline -> Inline
Hints.InlExpand
check_ƛ_32 :: T_InlineHints_26 -> T_InlineHints_26
check_ƛ_32 :: Inline -> Inline
check_ƛ_32 = Inline -> Inline
Hints.InlLam
check_ƛ'8595'_34 :: T_InlineHints_26 -> T_InlineHints_26
check_ƛ'8595'_34 :: Inline -> Inline
check_ƛ'8595'_34 = Inline -> Inline
Hints.InlLamDrop
check__'183'__36 ::
  T_InlineHints_26 -> T_InlineHints_26 -> T_InlineHints_26
check__'183'__36 :: Inline -> Inline -> Inline
check__'183'__36 = Inline -> Inline -> Inline
Hints.InlApply
check__'183''8595'_38 :: T_InlineHints_26 -> T_InlineHints_26
check__'183''8595'_38 :: Inline -> Inline
check__'183''8595'_38 = Inline -> Inline
Hints.InlDrop
check_force_40 :: T_InlineHints_26 -> T_InlineHints_26
check_force_40 :: Inline -> Inline
check_force_40 = Inline -> Inline
Hints.InlForce
check_delay_42 :: T_InlineHints_26 -> T_InlineHints_26
check_delay_42 :: Inline -> Inline
check_delay_42 = Inline -> Inline
Hints.InlDelay
check_con_44 :: T_InlineHints_26
check_con_44 :: Inline
check_con_44 = Inline
Hints.InlCon
check_builtin_46 :: T_InlineHints_26
check_builtin_46 :: Inline
check_builtin_46 = Inline
Hints.InlBuiltin
check_error_48 :: T_InlineHints_26
check_error_48 :: Inline
check_error_48 = Inline
Hints.InlError
check_constr_50 ::
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_26 ->
  T_InlineHints_26
check_constr_50 :: [Inline] -> Inline
check_constr_50 = [Inline] -> Inline
Hints.InlConstr
check_case_52 ::
  T_InlineHints_26 ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_InlineHints_26 ->
  T_InlineHints_26
check_case_52 :: Inline -> [Inline] -> Inline
check_case_52 = Inline -> [Inline] -> Inline
Hints.InlCase
cover_InlineHints_26 :: Hints.Inline -> ()
cover_InlineHints_26 :: Inline -> ()
cover_InlineHints_26 Inline
x
  = case Inline
x of
      Inline
Hints.InlVar -> ()
      Hints.InlExpand Inline
_ -> ()
      Hints.InlLam Inline
_ -> ()
      Hints.InlLamDrop 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_54 :: ()
d_Hints_54 = ()
type T_Hints_54 = Hints.Hints
pattern $mC_inline_56 :: forall {r}. Hints -> (Inline -> r) -> ((# #) -> r) -> r
$bC_inline_56 :: Inline -> Hints
C_inline_56 a0 = Hints.Inline a0
pattern $mC_none_58 :: forall {r}. Hints -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_none_58 :: Hints
C_none_58 = Hints.NoHints
check_inline_56 :: T_InlineHints_26 -> T_Hints_54
check_inline_56 :: Inline -> Hints
check_inline_56 = Inline -> Hints
Hints.Inline
check_none_58 :: T_Hints_54
check_none_58 :: Hints
check_none_58 = Hints
Hints.NoHints
cover_Hints_54 :: Hints.Hints -> ()
cover_Hints_54 :: Hints -> ()
cover_Hints_54 Hints
x
  = case Hints
x of
      Hints.Inline Inline
_ -> ()
      Hints
Hints.NoHints -> ()
-- VerifiedCompilation.Trace.Trace
d_Trace_62 :: p -> ()
d_Trace_62 p
a0 = ()
data T_Trace_62
  = C_step_66 T_SimplifierTag_4 T_Hints_54 AgdaAny T_Trace_62 |
    C_done_68 AgdaAny
-- VerifiedCompilation.Trace.head
d_head_72 :: T_Trace_62 -> AgdaAny
d_head_72 :: T_Trace_62 -> AgdaAny
d_head_72 T_Trace_62
v0
  = case T_Trace_62 -> T_Trace_62
forall a b. a -> b
coe T_Trace_62
v0 of
      C_step_66 SimplifierStage
v1 Hints
v2 AgdaAny
v3 T_Trace_62
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
      C_done_68 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Trace_62
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.Dump
d_Dump_78 :: ()
d_Dump_78 :: ()
d_Dump_78 = ()
forall a. a
erased
-- VerifiedCompilation.Trace.toTrace
d_toTrace_80 ::
  [MAlonzo.Code.Utils.T__'215'__428
     T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_54
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  Maybe T_Trace_62
d_toTrace_80 :: [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> Maybe T_Trace_62
d_toTrace_80 [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v0
  = case [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> [AgdaAny]
forall a b. a -> b
coe [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v0 of
      [] -> Maybe AgdaAny -> Maybe T_Trace_62
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe T_Trace_62
forall a b. a -> b
coe
             AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
 -> [T__'215'__428
       SimplifierStage
       (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
 -> T_Trace_62)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      SimplifierStage
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_62
du_go_90 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
      [AgdaAny]
_ -> Maybe T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace._.go
d_go_90 ::
  MAlonzo.Code.Utils.T__'215'__428
    T_SimplifierTag_4
    (MAlonzo.Code.Utils.T__'215'__428
       T_Hints_54
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__428
     T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_54
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  MAlonzo.Code.Utils.T__'215'__428
    T_SimplifierTag_4
    (MAlonzo.Code.Utils.T__'215'__428
       T_Hints_54
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__428
     T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_54
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_62
d_go_90 :: T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      SimplifierStage
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T__'215'__428
     SimplifierStage
     (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      SimplifierStage
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_62
d_go_90 ~T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v0 ~[T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v1 T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v2 [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v3 = T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      SimplifierStage
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_62
du_go_90 T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v2 [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v3
du_go_90 ::
  MAlonzo.Code.Utils.T__'215'__428
    T_SimplifierTag_4
    (MAlonzo.Code.Utils.T__'215'__428
       T_Hints_54
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.RawU.T_Untyped_208
          MAlonzo.Code.RawU.T_Untyped_208)) ->
  [MAlonzo.Code.Utils.T__'215'__428
     T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__428
        T_Hints_54
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  T_Trace_62
du_go_90 :: T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      SimplifierStage
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_62
du_go_90 T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v0 [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v1
  = case T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> (AgdaAny, AgdaAny)
forall a b. a -> b
coe T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
v0 of
      MAlonzo.Code.Utils.C__'44'__442 AgdaAny
v2 AgdaAny
v3
        -> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v3 of
             MAlonzo.Code.Utils.C__'44'__442 AgdaAny
v4 AgdaAny
v5
               -> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v5 of
                    MAlonzo.Code.Utils.C__'44'__442 AgdaAny
v6 AgdaAny
v7
                      -> case [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> [AgdaAny]
forall a b. a -> b
coe [T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v1 of
                           []
                             -> (SimplifierStage -> Hints -> AgdaAny -> T_Trace_62 -> T_Trace_62)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Trace_62
forall a b. a -> b
coe
                                  SimplifierStage -> Hints -> AgdaAny -> T_Trace_62 -> T_Trace_62
C_step_66 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) ((AgdaAny -> T_Trace_62) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Trace_62
C_done_68 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                           (:) AgdaAny
v8 [AgdaAny]
v9
                             -> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v8 of
                                  MAlonzo.Code.Utils.C__'44'__442 AgdaAny
v10 AgdaAny
v11
                                    -> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v11 of
                                         MAlonzo.Code.Utils.C__'44'__442 AgdaAny
v12 AgdaAny
v13
                                           -> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v13 of
                                                MAlonzo.Code.Utils.C__'44'__442 AgdaAny
v14 AgdaAny
v15
                                                  -> (SimplifierStage -> Hints -> AgdaAny -> T_Trace_62 -> T_Trace_62)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Trace_62
forall a b. a -> b
coe
                                                       SimplifierStage -> Hints -> AgdaAny -> T_Trace_62 -> T_Trace_62
C_step_66 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                                                       ((T__'215'__428
   SimplifierStage
   (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
 -> [T__'215'__428
       SimplifierStage
       (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
 -> T_Trace_62)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                          T__'215'__428
  SimplifierStage
  (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))
-> [T__'215'__428
      SimplifierStage
      (T__'215'__428 Hints (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Trace_62
du_go_90
                                                          ((AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny))
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                             AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__442
                                                             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10)
                                                             ((AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny))
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__442
                                                                (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12)
                                                                ((AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny))
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                   AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__442
                                                                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15))))
                                                          ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v9))
                                                (AgdaAny, AgdaAny)
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
                                         (AgdaAny, AgdaAny)
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  (AgdaAny, AgdaAny)
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
                           [AgdaAny]
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
                    (AgdaAny, AgdaAny)
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
             (AgdaAny, AgdaAny)
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
      (AgdaAny, AgdaAny)
_ -> T_Trace_62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Trace.EvalResult
d_EvalResult_116 :: ()
d_EvalResult_116 = ()
type T_EvalResult_116 = EvalResult
pattern $mC_success_118 :: forall {r}.
EvalResult -> (Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_success_118 :: Integer -> Integer -> EvalResult
C_success_118 a0 a1 = EvalSuccess a0 a1
pattern $mC_failure_120 :: forall {r}.
EvalResult
-> (EvalError -> Integer -> Integer -> r) -> ((# #) -> r) -> r
$bC_failure_120 :: EvalError -> Integer -> Integer -> EvalResult
C_failure_120 a0 a1 a2 = EvalFailure a0 a1 a2
check_success_118 :: Integer -> Integer -> T_EvalResult_116
check_success_118 :: Integer -> Integer -> EvalResult
check_success_118 = Integer -> Integer -> EvalResult
EvalSuccess
check_failure_120 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  Integer -> Integer -> T_EvalResult_116
check_failure_120 :: EvalError -> Integer -> Integer -> EvalResult
check_failure_120 = EvalError -> Integer -> Integer -> EvalResult
EvalFailure
cover_EvalResult_116 :: EvalResult -> ()
cover_EvalResult_116 :: EvalResult -> ()
cover_EvalResult_116 EvalResult
x
  = case EvalResult
x of
      EvalSuccess Integer
_ Integer
_ -> ()
      EvalFailure EvalError
_ Integer
_ Integer
_ -> ()