{-# 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 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.Data.Irrelevant
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.RenamingSubstitution
import qualified MAlonzo.Code.VerifiedCompilation.Certificate
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews

-- VerifiedCompilation.UCSE.UCSE
d_UCSE_4 :: p -> p -> p -> ()
d_UCSE_4 p
a0 p
a1 p
a2 = ()
newtype T_UCSE_4
  = C_cse_14 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12
-- VerifiedCompilation.UCSE.UntypedCSE
d_UntypedCSE_22 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_UntypedCSE_22 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
d_UntypedCSE_22 = Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
-- VerifiedCompilation.UCSE.isUntypedCSE?
d_isUntypedCSE'63'_26 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_54
d_isUntypedCSE'63'_26 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54
d_isUntypedCSE'63'_26 Integer
v0
  = (Integer
 -> T_SimplifierTag_4
 -> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54)
 -> T__'8866'_14
 -> T__'8866'_14
 -> T_ProofOrCE_54)
-> Any
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_54
forall a b. a -> b
coe
      Integer
-> T_SimplifierTag_4
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_54
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_164
      (Integer -> Any
forall a b. a -> b
coe Integer
v0)
      (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_18)
      ((Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54) -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54
d_isUCSE'63'_30)
-- VerifiedCompilation.UCSE.isUCSE?
d_isUCSE'63'_30 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_54
d_isUCSE'63'_30 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54
d_isUCSE'63'_30 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = let v3 :: Any
v3
          = (Integer
 -> (Integer -> T__'8866'_14 -> T_Dec_20)
 -> (Integer -> 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
              Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
              (Integer -> Any
forall a b. a -> b
coe Integer
v0)
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v3 ->
                    (Integer
 -> (Integer -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                      Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
                      (Any -> Any
forall a b. a -> b
coe Any
v3)
                      (\ 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_54
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
                                                                    = (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                        Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_54
d_isUntypedCSE'63'_26 Integer
v0 T__'8866'_14
v1
                                                                        (Integer -> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.d__'91'_'93'_468
                                                                           (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v15)
                                                                           (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v12)) in
                                                              Any -> Any
forall a b. a -> b
coe
                                                                (case Any -> T_ProofOrCE_54
forall a b. a -> b
coe Any
v16 of
                                                                   MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_60 Any
v17
                                                                     -> (Any -> T_ProofOrCE_54) -> Any -> Any
forall a b. a -> b
coe
                                                                          Any -> T_ProofOrCE_54
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_60
                                                                          ((T_Translation_12 -> T_UCSE_4) -> Any -> Any
forall a b. a -> b
coe T_Translation_12 -> T_UCSE_4
C_cse_14 Any
v17)
                                                                   MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_68 T_SimplifierTag_4
v20 Any
v21 Any
v22
                                                                     -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_54)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_54
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_68
                                                                          T_SimplifierTag_4
v20 Any
v21 Any
v22
                                                                   T_ProofOrCE_54
_ -> 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_54)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_54
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_68
                          (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_18) T__'8866'_14
v1 T__'8866'_14
v2)
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCSE..extendedlambda0
d_'46'extendedlambda0_46 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  T_UCSE_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_46 :: Integer
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_UCSE_4
-> T_Irrelevant_20
d_'46'extendedlambda0_46 = Integer
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_UCSE_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCSE..extendedlambda1
d_'46'extendedlambda1_78 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
   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_78 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_12 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T_UCSE_4
-> T_Irrelevant_20
d_'46'extendedlambda1_78 = Integer
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_12 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T_UCSE_4
-> T_Irrelevant_20
forall a. a
erased