{-# 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.Certificate 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.Bool
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

import UntypedPlutusCore.Transform.Simplifier
-- VerifiedCompilation.Certificate.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_caseOfCaseT_10 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseOfCaseT_10 :: SimplifierStage
C_caseOfCaseT_10 = CaseOfCase
pattern $mC_caseReduceT_12 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_caseReduceT_12 :: SimplifierStage
C_caseReduceT_12 = CaseReduce
pattern $mC_inlineT_14 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_inlineT_14 :: SimplifierStage
C_inlineT_14 = Inline
pattern $mC_cseT_16 :: forall {r}. SimplifierStage -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_cseT_16 :: SimplifierStage
C_cseT_16 = CSE
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_caseOfCaseT_10 :: T_SimplifierTag_4
check_caseOfCaseT_10 :: SimplifierStage
check_caseOfCaseT_10 = SimplifierStage
CaseOfCase
check_caseReduceT_12 :: T_SimplifierTag_4
check_caseReduceT_12 :: SimplifierStage
check_caseReduceT_12 = SimplifierStage
CaseReduce
check_inlineT_14 :: T_SimplifierTag_4
check_inlineT_14 :: SimplifierStage
check_inlineT_14 = SimplifierStage
Inline
check_cseT_16 :: T_SimplifierTag_4
check_cseT_16 :: SimplifierStage
check_cseT_16 = SimplifierStage
CSE
cover_SimplifierTag_4 :: SimplifierStage -> ()
cover_SimplifierTag_4 :: SimplifierStage -> ()
cover_SimplifierTag_4 SimplifierStage
x
  = case SimplifierStage
x of
      SimplifierStage
FloatDelay -> ()
      SimplifierStage
ForceDelay -> ()
      SimplifierStage
CaseOfCase -> ()
      SimplifierStage
CaseReduce -> ()
      SimplifierStage
Inline -> ()
      SimplifierStage
CSE -> ()
-- VerifiedCompilation.Certificate.ProofOrCE
d_ProofOrCE_26 :: p -> p -> ()
d_ProofOrCE_26 p
a0 p
a1 = ()
data T_ProofOrCE_26
  = C_proof_32 AgdaAny | C_ce_40 T_SimplifierTag_4 AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.decToPCE
d_decToPCE_50 ::
  () ->
  () ->
  T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_26
d_decToPCE_50 :: ()
-> ()
-> SimplifierStage
-> T_Dec_20
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_26
d_decToPCE_50 ~()
v0 ~()
v1 SimplifierStage
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5 = SimplifierStage -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
du_decToPCE_50 SimplifierStage
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5
du_decToPCE_50 ::
  T_SimplifierTag_4 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_26
du_decToPCE_50 :: SimplifierStage -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
du_decToPCE_50 SimplifierStage
v0 T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 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 AgdaAny
v6
                      -> (AgdaAny -> T_ProofOrCE_26) -> AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_26
C_proof_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                    T_Reflects_16
_ -> T_ProofOrCE_26
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5) ((SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
C_ce_40 SimplifierStage
v0 AgdaAny
v2 AgdaAny
v3)
      T_Dec_20
_ -> T_ProofOrCE_26
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.pceToDec
d_pceToDec_64 ::
  () ->
  T_ProofOrCE_26 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pceToDec_64 :: () -> T_ProofOrCE_26 -> T_Dec_20
d_pceToDec_64 ~()
v0 T_ProofOrCE_26
v1 = T_ProofOrCE_26 -> T_Dec_20
du_pceToDec_64 T_ProofOrCE_26
v1
du_pceToDec_64 ::
  T_ProofOrCE_26 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pceToDec_64 :: T_ProofOrCE_26 -> T_Dec_20
du_pceToDec_64 T_ProofOrCE_26
v0
  = case T_ProofOrCE_26 -> T_ProofOrCE_26
forall a b. a -> b
coe T_ProofOrCE_26
v0 of
      C_proof_32 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
             Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
      C_ce_40 SimplifierStage
v4 AgdaAny
v5 AgdaAny
v6
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
             Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
      T_ProofOrCE_26
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.MatchOrCE
d_MatchOrCE_78 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> ()
d_MatchOrCE_78 :: () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_MatchOrCE_78 = () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.matchOrCE
d_matchOrCE_98 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_26
d_matchOrCE_98 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> SimplifierStage
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_26
d_matchOrCE_98 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
  = SimplifierStage
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_26
du_matchOrCE_98 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_matchOrCE_98 ::
  T_SimplifierTag_4 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_26
du_matchOrCE_98 :: SimplifierStage
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_26
du_matchOrCE_98 SimplifierStage
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = let v4 :: t
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3 in
    AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe
      (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v4 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v7
                         -> (AgdaAny -> T_ProofOrCE_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_26
C_proof_32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)
                       T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6) ((SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
C_ce_40 SimplifierStage
v0 AgdaAny
v2 AgdaAny
v3)
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.pcePointwise
d_pcePointwise_140 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_26) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_26
d_pcePointwise_140 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_26
d_pcePointwise_140 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_26
v5 [AgdaAny]
v6 [AgdaAny]
v7
  = SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_26
du_pcePointwise_140 SimplifierStage
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_26
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_pcePointwise_140 ::
  T_SimplifierTag_4 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_26) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_26
du_pcePointwise_140 :: SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_26
du_pcePointwise_140 SimplifierStage
v0 AgdaAny -> AgdaAny -> T_ProofOrCE_26
v1 [AgdaAny]
v2 [AgdaAny]
v3
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T_ProofOrCE_26) -> AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe
                    AgdaAny -> T_ProofOrCE_26
C_proof_32
                    (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe
                       T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
             (:) AgdaAny
v4 [AgdaAny]
v5 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> SimplifierStage -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_26
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
C_ce_40 SimplifierStage
v0 [AgdaAny]
v2 [AgdaAny]
v5
             [AgdaAny]
_ -> T_ProofOrCE_26
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             [] -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> SimplifierStage -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_26
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
C_ce_40 SimplifierStage
v0 [AgdaAny]
v5 [AgdaAny]
v3
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: t
v8 = (AgdaAny -> AgdaAny -> T_ProofOrCE_26) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_26
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe
                    (case AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
                       C_proof_32 AgdaAny
v9
                         -> let v10 :: t
v10
                                  = (SimplifierStage
 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_26)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_ProofOrCE_26)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe SimplifierStage
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_26
du_pcePointwise_140 (SimplifierStage -> AgdaAny
forall a b. a -> b
coe SimplifierStage
v0) ((AgdaAny -> AgdaAny -> T_ProofOrCE_26) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_26
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_ProofOrCE_26
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
                                 C_proof_32 AgdaAny
v11
                                   -> (AgdaAny -> T_ProofOrCE_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_ProofOrCE_26
C_proof_32
                                        ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                           AgdaAny
v9 AgdaAny
v11)
                                 C_ce_40 SimplifierStage
v14 AgdaAny
v15 AgdaAny
v16 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
C_ce_40 SimplifierStage
v14 AgdaAny
v15 AgdaAny
v16
                                 T_ProofOrCE_26
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       C_ce_40 SimplifierStage
v12 AgdaAny
v13 AgdaAny
v14 -> (SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26)
-> SimplifierStage -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe SimplifierStage -> AgdaAny -> AgdaAny -> T_ProofOrCE_26
C_ce_40 SimplifierStage
v12 AgdaAny
v13 AgdaAny
v14
                       T_ProofOrCE_26
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_ProofOrCE_26
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_ProofOrCE_26
forall a. a
MAlonzo.RTE.mazUnreachableError