{-# 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.UCaseReduce 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Untyped.Reduction
import qualified MAlonzo.Code.VerifiedCompilation.Certificate
import qualified MAlonzo.Code.VerifiedCompilation.Equality
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews

-- VerifiedCompilation.UCaseReduce.CaseReduce
d_CaseReduce_4 :: p -> p -> p -> p -> ()
d_CaseReduce_4 p
a0 p
a1 p
a2 p
a3 = ()
data T_CaseReduce_4
  = C_casereduce_20 MAlonzo.Code.Untyped.T__'8866'_14
                    MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
-- VerifiedCompilation.UCaseReduce.isCaseReduce?
d_isCaseReduce'63'_30 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isCaseReduce'63'_30 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isCaseReduce'63'_30 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseReduce'63'_30 T_DecEq_6
v1
du_isCaseReduce'63'_30 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isCaseReduce'63'_30 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseReduce'63'_30 T_DecEq_6
v0
  = (()
 -> T_DecEq_6
 -> T_SimplifierTag_4
 -> (()
     -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
 -> T__'8866'_14
 -> T__'8866'_14
 -> T_ProofOrCE_26)
-> Any
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
forall a b. a -> b
coe
      ()
-> T_DecEq_6
-> T_SimplifierTag_4
-> (()
    -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_178
      Any
forall a. a
erased (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)
      (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_12)
      (\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCR'63'_48 Any
v2 Any
v3 Any
v4)
-- VerifiedCompilation.UCaseReduce.justEq
d_justEq_38 ::
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_justEq_38 :: () -> Any -> Any -> T__'8801'__12 -> T__'8801'__12
d_justEq_38 = () -> Any -> Any -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- VerifiedCompilation.UCaseReduce.isCR?
d_isCR'63'_48 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isCR'63'_48 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isCR'63'_48 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCR'63'_48 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isCR'63'_48 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isCR'63'_48 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCR'63'_48 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = let v3 :: t
v3
          = (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> [T__'8866'_14] -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
              ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isCase'63'_598
              Any
forall a. a
erased
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    (()
 -> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                      ()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
                      Any
forall a. a
erased
                      (\ Any
v4 Any
v5 ->
                         T_Dec_20 -> Any
forall a b. a -> b
coe
                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))
              (\ Any
v3 Any
v4 ->
                 T_Dec_20 -> Any
forall a b. a -> b
coe
                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)
              (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) in
    Any -> T_ProofOrCE_26
forall a b. a -> b
coe
      (case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v3 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
                         -> case Any -> T_isCase_574
forall a b. a -> b
coe Any
v6 of
                              MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v9 Any
v10
                                -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                                     MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v11 [T__'8866'_14]
v12
                                       -> case Any -> T_isConstr_478
forall a b. a -> b
coe Any
v9 of
                                            MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v15
                                              -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
                                                   MAlonzo.Code.Untyped.C_constr_34 Integer
v16 [T__'8866'_14]
v17
                                                     -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v15)
                                                          ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                             Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v10)
                                                             (let v18 :: t
v18
                                                                    = (Integer -> [Any] -> Maybe Any) -> Any -> Any -> t
forall a b. a -> b
coe
                                                                        Integer -> [Any] -> Maybe Any
MAlonzo.Code.Untyped.CEK.du_lookup'63'_954
                                                                        (Integer -> Any
forall a b. a -> b
coe Integer
v16) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v12) in
                                                              Any -> Any
forall a b. a -> b
coe
                                                                (case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v18 of
                                                                   MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v19
                                                                     -> let v20 :: t
v20
                                                                              = (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T_DecEq_6 -> Any -> T__'8866'_14 -> t
forall a b. a -> b
coe
                                                                                  T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseReduce'63'_30
                                                                                  T_DecEq_6
v0
                                                                                  ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                     T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.Reduction.du_iterApp_242
                                                                                     (Any -> Any
forall a b. a -> b
coe Any
v19)
                                                                                     ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v17))
                                                                                  T__'8866'_14
v2 in
                                                                        Any -> Any
forall a b. a -> b
coe
                                                                          (case Any -> T_ProofOrCE_26
forall a b. a -> b
coe Any
forall a. a
v20 of
                                                                             MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v21
                                                                               -> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
                                                                                    Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
                                                                                    ((T__'8866'_14 -> T_Translation_16 -> T_CaseReduce_4)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                       T__'8866'_14 -> T_Translation_16 -> T_CaseReduce_4
C_casereduce_20
                                                                                       Any
v19 Any
v21)
                                                                             MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v24 Any
v25 Any
v26
                                                                               -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                    T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                                    T_SimplifierTag_4
v24 Any
v25 Any
v26
                                                                             T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                   Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                                                                     -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                          (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
                                                                             T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_12)
                                                                          T__'8866'_14
v1 T__'8866'_14
v2
                                                                   Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
                                                   T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                            T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
                       ((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                          (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_12)
                          T__'8866'_14
v1 T__'8866'_14
v2)
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCaseReduce..extendedlambda0
d_'46'extendedlambda0_64 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isCase_574 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  T_CaseReduce_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_64 :: ()
-> T__'8866'_14
-> (T_isCase_574 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_4
-> T_Irrelevant_20
d_'46'extendedlambda0_64 = ()
-> T__'8866'_14
-> (T_isCase_574 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce..extendedlambda1
d_'46'extendedlambda1_92 ::
  () ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  T_CaseReduce_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_92 :: ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_4
-> T_Irrelevant_20
d_'46'extendedlambda1_92 = ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T_CaseReduce_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce..extendedlambda2
d_'46'extendedlambda2_96 ::
  () ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda2_96 :: ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> T_Translation_16
-> T__'8801'__12
-> T_Irrelevant_20
d_'46'extendedlambda2_96 = ()
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8801'__12
-> T_Translation_16
-> T__'8801'__12
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce..extendedlambda3
d_'46'extendedlambda3_148 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T_CaseReduce_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda3_148 :: ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> T_CaseReduce_4
-> T_Irrelevant_20
d_'46'extendedlambda3_148 = ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> Integer
-> T__'8801'__12
-> T_CaseReduce_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseReduce.UCaseReduce
d_UCaseReduce_156 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_UCaseReduce_156 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_UCaseReduce_156 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
-- VerifiedCompilation.UCaseReduce.integer
d_integer_158 :: MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_integer_158 :: T__'8866''9839'_4
d_integer_158
  = (T_Tag_28 Any -> T__'8866''9839'_4) -> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
      T_Tag_28 Any -> T__'8866''9839'_4
MAlonzo.Code.RawU.du_tag2TyTag_206
      (DefaultUni (Esc Integer) -> Any
forall a b. a -> b
coe DefaultUni (Esc Integer)
forall {a}. (a ~ Esc Integer) => DefaultUni a
MAlonzo.Code.RawU.C_integer_30)
-- VerifiedCompilation.UCaseReduce.con-integer
d_con'45'integer_162 ::
  () -> Integer -> MAlonzo.Code.Untyped.T__'8866'_14
d_con'45'integer_162 :: () -> Integer -> T__'8866'_14
d_con'45'integer_162 ~()
v0 Integer
v1 = Integer -> T__'8866'_14
du_con'45'integer_162 Integer
v1
du_con'45'integer_162 ::
  Integer -> MAlonzo.Code.Untyped.T__'8866'_14
du_con'45'integer_162 :: Integer -> T__'8866'_14
du_con'45'integer_162 Integer
v0
  = (T_TmCon_198 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T_TmCon_198 -> T__'8866'_14
MAlonzo.Code.Untyped.C_con_28
      ((T__'8866''9839'_4 -> Any -> T_TmCon_198) -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''9839'_4 -> Any -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> Any
forall a b. a -> b
coe T__'8866''9839'_4
d_integer_158) (Integer -> Any
forall a b. a -> b
coe Integer
v0))
-- VerifiedCompilation.UCaseReduce.ast₁
d_ast'8321'_166 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast'8321'_166 :: T__'8866'_14
d_ast'8321'_166
  = (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
      ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
         ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
            Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
            ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))))
      ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
         Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
         ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
            (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))
-- VerifiedCompilation.UCaseReduce.ast₁'
d_ast'8321'''_168 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast'8321'''_168 :: T__'8866'_14
d_ast'8321'''_168
  = (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
      ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
         Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
         (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))
-- VerifiedCompilation.UCaseReduce.ast
d_ast_172 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast_172 :: T__'8866'_14
d_ast_172
  = (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
      ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
            ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
12 :: Integer)))
            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
               ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
42 :: Integer)))
               ([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))
      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
         ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
            ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
               T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
               ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                  Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                  ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                     Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                     (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
            ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
               T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
               ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                  T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
                  ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                     T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
                     ((Integer -> [T__'8866'_14] -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                        Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                        ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
                           Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
                           ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))))
                     ((Any -> [Any]) -> Any -> Any
forall a b. a -> b
coe
                        Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_286
                        ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                           Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                           (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))))
            ([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))
-- VerifiedCompilation.UCaseReduce.ast'
d_ast''_174 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ast''_174 :: T__'8866'_14
d_ast''_174
  = (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
42 :: Integer)))
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
99 :: Integer)))
-- VerifiedCompilation.UCaseReduce.ex1
d_ex1_176 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ex1_176 :: T__'8866'_14
d_ex1_176
  = (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
      ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
         ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
            ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
               T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
               ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                  T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                  ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                     T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                     ((T_Builtin_2 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                        T_Builtin_2 -> T__'8866'_14
MAlonzo.Code.Untyped.C_builtin_44
                        (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
MAlonzo.Code.Builtin.C_subtractInteger_6))
                     ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                        Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                        (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))
                  ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                     Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                     ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                        Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                        (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))))
         ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer))))
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer)))
-- VerifiedCompilation.UCaseReduce.ex2
d_ex2_178 :: MAlonzo.Code.Untyped.T__'8866'_14
d_ex2_178 :: T__'8866'_14
d_ex2_178
  = (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
      T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
      ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
         T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
         ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
            T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
            ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
               T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
               ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                  T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                  ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                     T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                     ((T_Builtin_2 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                        T_Builtin_2 -> T__'8866'_14
MAlonzo.Code.Untyped.C_builtin_44
                        (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
MAlonzo.Code.Builtin.C_subtractInteger_6))
                     ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                        Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                        ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                           Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                           (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))))
                  ((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                     Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
                     (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
         ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer))))
      ((Integer -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14
du_con'45'integer_162 (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)))