{-# 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.UCSE where

import Data.Text qualified
import MAlonzo.Code.Data.Irrelevant qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.Code.Relation.Nullary.Reflects qualified
import MAlonzo.Code.Untyped qualified
import MAlonzo.Code.Untyped.RenamingSubstitution qualified
import MAlonzo.Code.VerifiedCompilation.Certificate qualified
import MAlonzo.Code.VerifiedCompilation.Equality qualified
import MAlonzo.Code.VerifiedCompilation.UntypedTranslation qualified
import MAlonzo.Code.VerifiedCompilation.UntypedViews qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- VerifiedCompilation.UCSE.UCSE
d_UCSE_4 :: p -> p -> p -> p -> ()
d_UCSE_4 p
a0 p
a1 p
a2 p
a3 = ()
newtype T_UCSE_4
  = C_cse_16 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
-- VerifiedCompilation.UCSE.UntypedCSE
d_UntypedCSE_26 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_UntypedCSE_26 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_UntypedCSE_26 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
-- VerifiedCompilation.UCSE.isUntypedCSE?
d_isUntypedCSE'63'_32 ::
  () ->
  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_isUntypedCSE'63'_32 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isUntypedCSE'63'_32 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isUntypedCSE'63'_32 T_DecEq_6
v1
du_isUntypedCSE'63'_32 ::
  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_isUntypedCSE'63'_32 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isUntypedCSE'63'_32 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_cseT_16)
      (\ 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_isUCSE'63'_38 Any
v2 Any
v3 Any
v4)
-- VerifiedCompilation.UCSE.isUCSE?
d_isUCSE'63'_38 ::
  () ->
  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_isUCSE'63'_38 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isUCSE'63'_38 ~()
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_isUCSE'63'_38 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isUCSE'63'_38 ::
  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_isUCSE'63'_38 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isUCSE'63'_38 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = let v3 :: Any
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 -> Any
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_isApp'63'_166
              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
forall a b. a -> b
coe
                      (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
                      (\ Any
v4 Any
v5 ->
                         T_Dec_20 -> Any
forall a b. a -> b
coe
                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
              (\ Any
v3 Any
v4 ->
                 T_Dec_20 -> Any
forall a b. a -> b
coe
                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
              (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
    Any -> T_ProofOrCE_26
forall a b. a -> b
coe
      (case Any -> T_Dec_20
forall a b. a -> b
coe Any
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_isApp_142
forall a b. a -> b
coe Any
v6 of
                              MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v9 Any
v10
                                -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
                                     MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v11 T__'8866'_14
v12
                                       -> case Any -> T_isLambda_54
forall a b. a -> b
coe Any
v9 of
                                            MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 Any
v14
                                              -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
                                                   MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
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
v14)
                                                          ((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 v16 :: Any
v16
                                                                    = (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T_DecEq_6 -> T__'8866'_14 -> Any -> Any
forall a b. a -> b
coe
                                                                        T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isUntypedCSE'63'_32 T_DecEq_6
v0 T__'8866'_14
v1
                                                                        ((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.RenamingSubstitution.du__'91'_'93'_468
                                                                           (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v15) (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 -> T_ProofOrCE_26
forall a b. a -> b
coe Any
v16 of
                                                                   MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v17
                                                                     -> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
                                                                          Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
                                                                          ((T_Translation_16 -> T_UCSE_4) -> Any -> Any
forall a b. a -> b
coe T_Translation_16 -> T_UCSE_4
C_cse_16 Any
v17)
                                                                   MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v20 Any
v21 Any
v22
                                                                     -> (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
v20 Any
v21 Any
v22
                                                                   T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
                                                   T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                            T_isLambda_54
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_isApp_142
_ -> 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_cseT_16) T__'8866'_14
v1 T__'8866'_14
v2)
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCSE..extendedlambda0
d_'46'extendedlambda0_54 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  T_UCSE_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_54 :: ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_UCSE_4
-> T_Irrelevant_20
d_'46'extendedlambda0_54 = ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_UCSE_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCSE..extendedlambda1
d_'46'extendedlambda1_86 ::
  () ->
  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 -> T_UCSE_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_86 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T_UCSE_4
-> T_Irrelevant_20
d_'46'extendedlambda1_86 = ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T_UCSE_4
-> T_Irrelevant_20
forall a. a
erased