{-# 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.Bool.Base
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 qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation.Trace

-- VerifiedCompilation.Certificate.CertResult
d_CertResult_12 :: p -> p -> ()
d_CertResult_12 p
a0 p
a1 = ()
data T_CertResult_12
  = C_proof_18 AgdaAny |
    C_ce_26 (MAlonzo.Code.Utils.T_Either_6
               MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
               MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
            AgdaAny AgdaAny |
    C_abort_32 (MAlonzo.Code.Utils.T_Either_6
                  MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
                  MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
               AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.is-proof
d_is'45'proof_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_CertResult_12 -> Bool
d_is'45'proof_36 :: () -> () -> T_CertResult_12 -> Bool
d_is'45'proof_36 ~()
v0 ~()
v1 T_CertResult_12
v2 = T_CertResult_12 -> Bool
du_is'45'proof_36 T_CertResult_12
v2
du_is'45'proof_36 :: T_CertResult_12 -> Bool
du_is'45'proof_36 :: T_CertResult_12 -> Bool
du_is'45'proof_36 T_CertResult_12
v0
  = case T_CertResult_12 -> T_CertResult_12
forall a b. a -> b
coe T_CertResult_12
v0 of
      C_proof_18 AgdaAny
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      C_ce_26 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny
v5 AgdaAny
v6 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      C_abort_32 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v3 AgdaAny
v4 AgdaAny
v5 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      T_CertResult_12
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.to-witness-T
d_to'45'witness'45'T_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_CertResult_12 -> AgdaAny -> AgdaAny
d_to'45'witness'45'T_42 :: () -> () -> T_CertResult_12 -> AgdaAny -> AgdaAny
d_to'45'witness'45'T_42 ~()
v0 ~()
v1 T_CertResult_12
v2 ~AgdaAny
v3
  = T_CertResult_12 -> AgdaAny
du_to'45'witness'45'T_42 T_CertResult_12
v2
du_to'45'witness'45'T_42 :: T_CertResult_12 -> AgdaAny
du_to'45'witness'45'T_42 :: T_CertResult_12 -> AgdaAny
du_to'45'witness'45'T_42 T_CertResult_12
v0
  = case T_CertResult_12 -> T_CertResult_12
forall a b. a -> b
coe T_CertResult_12
v0 of
      C_proof_18 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_CertResult_12
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.ProofOrCE
d_ProofOrCE_50 :: p -> p -> ()
d_ProofOrCE_50 p
a0 p
a1 = ()
data T_ProofOrCE_50
  = C_proof_56 AgdaAny |
    C_ce_64 (MAlonzo.Code.Utils.T_Either_6
               MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
               MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
            AgdaAny AgdaAny
-- VerifiedCompilation.Certificate.isProof?
d_isProof'63'_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_ProofOrCE_50 -> Bool
d_isProof'63'_68 :: () -> () -> T_ProofOrCE_50 -> Bool
d_isProof'63'_68 ~()
v0 ~()
v1 T_ProofOrCE_50
v2 = T_ProofOrCE_50 -> Bool
du_isProof'63'_68 T_ProofOrCE_50
v2
du_isProof'63'_68 :: T_ProofOrCE_50 -> Bool
du_isProof'63'_68 :: T_ProofOrCE_50 -> Bool
du_isProof'63'_68 T_ProofOrCE_50
v0
  = case T_ProofOrCE_50 -> T_ProofOrCE_50
forall a b. a -> b
coe T_ProofOrCE_50
v0 of
      C_proof_56 AgdaAny
v1 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
      C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny
v5 AgdaAny
v6 -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
      T_ProofOrCE_50
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.isCE?
d_isCE'63'_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> T_ProofOrCE_50 -> Bool
d_isCE'63'_72 :: () -> () -> T_ProofOrCE_50 -> Bool
d_isCE'63'_72 ~()
v0 ~()
v1 T_ProofOrCE_50
v2 = T_ProofOrCE_50 -> Bool
du_isCE'63'_72 T_ProofOrCE_50
v2
du_isCE'63'_72 :: T_ProofOrCE_50 -> Bool
du_isCE'63'_72 :: T_ProofOrCE_50 -> Bool
du_isCE'63'_72 T_ProofOrCE_50
v0
  = (Bool -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
      Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
      ((T_ProofOrCE_50 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_ProofOrCE_50 -> Bool
du_isProof'63'_68 (T_ProofOrCE_50 -> AgdaAny
forall a b. a -> b
coe T_ProofOrCE_50
v0))
-- VerifiedCompilation.Certificate.Proof?
d_Proof'63'_78 :: p -> p -> ()
d_Proof'63'_78 p
a0 p
a1 = ()
data T_Proof'63'_78
  = C_proof_84 AgdaAny |
    C_abort_90 (MAlonzo.Code.Utils.T_Either_6
                  MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
                  MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
               AgdaAny AgdaAny
-- VerifiedCompilation.Certificate._>>=_
d__'62''62''61'__100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  () ->
  T_Proof'63'_78 -> (AgdaAny -> T_Proof'63'_78) -> T_Proof'63'_78
d__'62''62''61'__100 :: ()
-> ()
-> ()
-> ()
-> T_Proof'63'_78
-> (AgdaAny -> T_Proof'63'_78)
-> T_Proof'63'_78
d__'62''62''61'__100 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Proof'63'_78
v4 AgdaAny -> T_Proof'63'_78
v5
  = T_Proof'63'_78 -> (AgdaAny -> T_Proof'63'_78) -> T_Proof'63'_78
du__'62''62''61'__100 T_Proof'63'_78
v4 AgdaAny -> T_Proof'63'_78
v5
du__'62''62''61'__100 ::
  T_Proof'63'_78 -> (AgdaAny -> T_Proof'63'_78) -> T_Proof'63'_78
du__'62''62''61'__100 :: T_Proof'63'_78 -> (AgdaAny -> T_Proof'63'_78) -> T_Proof'63'_78
du__'62''62''61'__100 T_Proof'63'_78
v0 AgdaAny -> T_Proof'63'_78
v1
  = case T_Proof'63'_78 -> T_Proof'63'_78
forall a b. a -> b
coe T_Proof'63'_78
v0 of
      C_proof_84 AgdaAny
v2 -> (AgdaAny -> T_Proof'63'_78) -> AgdaAny -> T_Proof'63'_78
forall a b. a -> b
coe AgdaAny -> T_Proof'63'_78
v1 AgdaAny
v2
      C_abort_90 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny
v5 AgdaAny
v6 -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_Proof'63'_78)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> T_Proof'63'_78
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_Proof'63'_78
C_abort_90 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny
v5 AgdaAny
v6
      T_Proof'63'_78
_ -> T_Proof'63'_78
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.DecidableCE
d_DecidableCE_120 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_120 :: () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_DecidableCE_120 = () -> () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.Checkable
d_Checkable_138 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_138 :: () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Checkable_138 = () -> () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.Certifiable
d_Certifiable_154 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_154 :: () -> (AgdaAny -> AgdaAny -> ()) -> ()
d_Certifiable_154 = () -> (AgdaAny -> AgdaAny -> ()) -> ()
forall a. a
erased
-- VerifiedCompilation.Certificate.checker
d_checker_168 ::
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> T_Proof'63'_78) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
d_checker_168 :: ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Proof'63'_78)
-> AgdaAny
-> AgdaAny
-> T_CertResult_12
d_checker_168 ~()
v0 ~AgdaAny -> AgdaAny -> ()
v1 AgdaAny -> AgdaAny -> T_Proof'63'_78
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Proof'63'_78)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_168 AgdaAny -> AgdaAny -> T_Proof'63'_78
v2 AgdaAny
v3 AgdaAny
v4
du_checker_168 ::
  (AgdaAny -> AgdaAny -> T_Proof'63'_78) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_168 :: (AgdaAny -> AgdaAny -> T_Proof'63'_78)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_checker_168 AgdaAny -> AgdaAny -> T_Proof'63'_78
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_Proof'63'_78)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Proof'63'_78
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_CertResult_12
forall a b. a -> b
coe
      (case AgdaAny -> T_Proof'63'_78
forall a b. a -> b
coe AgdaAny
v3 of
         C_proof_84 AgdaAny
v4 -> (AgdaAny -> T_CertResult_12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_CertResult_12
C_proof_18 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
         C_abort_90 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v6 AgdaAny
v7 AgdaAny
v8 -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_CertResult_12)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_CertResult_12
C_abort_32 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v6 AgdaAny
v7 AgdaAny
v8
         T_Proof'63'_78
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decider
d_decider_204 ::
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_50) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
d_decider_204 :: ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> AgdaAny
-> AgdaAny
-> T_CertResult_12
d_decider_204 ~()
v0 ~AgdaAny -> AgdaAny -> ()
v1 AgdaAny -> AgdaAny -> T_ProofOrCE_50
v2 AgdaAny
v3 AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_204 AgdaAny -> AgdaAny -> T_ProofOrCE_50
v2 AgdaAny
v3 AgdaAny
v4
du_decider_204 ::
  (AgdaAny -> AgdaAny -> T_ProofOrCE_50) ->
  AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_204 :: (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> AgdaAny -> AgdaAny -> T_CertResult_12
du_decider_204 AgdaAny -> AgdaAny -> T_ProofOrCE_50
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: AgdaAny
v3 = (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_50
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_CertResult_12
forall a b. a -> b
coe
      (case AgdaAny -> T_ProofOrCE_50
forall a b. a -> b
coe AgdaAny
v3 of
         C_proof_56 AgdaAny
v4 -> (AgdaAny -> T_CertResult_12) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_CertResult_12
C_proof_18 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
         C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v7 AgdaAny
v8 AgdaAny
v9 -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_CertResult_12)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_CertResult_12
C_ce_26 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v7 AgdaAny
v8 AgdaAny
v9
         T_ProofOrCE_50
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.decToPCE
d_decToPCE_246 ::
  () ->
  () ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
    MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_50
d_decToPCE_246 :: ()
-> ()
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> T_Dec_20
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_50
d_decToPCE_246 ~()
v0 ~()
v1 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5 = T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50
du_decToPCE_246 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v2 T_Dec_20
v3 AgdaAny
v4 AgdaAny
v5
du_decToPCE_246 ::
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
    MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_50
du_decToPCE_246 :: T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50
du_decToPCE_246 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
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_50) -> AgdaAny -> T_ProofOrCE_50
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_50
C_proof_56 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                    T_Reflects_16
_ -> T_ProofOrCE_50
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
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) ((T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0 AgdaAny
v2 AgdaAny
v3)
      T_Dec_20
_ -> T_ProofOrCE_50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.pceToDec
d_pceToDec_260 ::
  () ->
  T_ProofOrCE_50 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pceToDec_260 :: () -> T_ProofOrCE_50 -> T_Dec_20
d_pceToDec_260 ~()
v0 T_ProofOrCE_50
v1 = T_ProofOrCE_50 -> T_Dec_20
du_pceToDec_260 T_ProofOrCE_50
v1
du_pceToDec_260 ::
  T_ProofOrCE_50 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pceToDec_260 :: T_ProofOrCE_50 -> T_Dec_20
du_pceToDec_260 T_ProofOrCE_50
v0
  = case T_ProofOrCE_50 -> T_ProofOrCE_50
forall a b. a -> b
coe T_ProofOrCE_50
v0 of
      C_proof_56 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_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
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_50
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.Certificate.matchOrCE
d_matchOrCE_274 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
    MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_50
d_matchOrCE_274 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_50
d_matchOrCE_274 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
  = T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_50
du_matchOrCE_274 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_matchOrCE_274 ::
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
    MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny -> AgdaAny -> T_ProofOrCE_50
du_matchOrCE_274 :: T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_ProofOrCE_50
du_matchOrCE_274 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = let v4 :: AgdaAny
v4 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3 in
    AgdaAny -> T_ProofOrCE_50
forall a b. a -> b
coe
      (case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
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_50) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_ProofOrCE_50
C_proof_56 (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) ((T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0 AgdaAny
v2 AgdaAny
v3)
         T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.Certificate.pcePointwise
d_pcePointwise_316 ::
  () ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
    MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_50) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_50
d_pcePointwise_316 :: ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_50
d_pcePointwise_316 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> AgdaAny -> ()
v3 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_50
v5 [AgdaAny]
v6 [AgdaAny]
v7
  = T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_50
du_pcePointwise_316 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4 AgdaAny -> AgdaAny -> T_ProofOrCE_50
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_pcePointwise_316 ::
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
    MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
  (AgdaAny -> AgdaAny -> T_ProofOrCE_50) ->
  [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_50
du_pcePointwise_316 :: T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_50
du_pcePointwise_316 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0 AgdaAny -> AgdaAny -> T_ProofOrCE_50
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_50) -> AgdaAny -> T_ProofOrCE_50
forall a b. a -> b
coe
                    AgdaAny -> T_ProofOrCE_50
C_proof_56
                    (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 -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_50
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0 [AgdaAny]
v2 [AgdaAny]
v5
             [AgdaAny]
_ -> T_ProofOrCE_50
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             [] -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_50
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0 [AgdaAny]
v5 [AgdaAny]
v3
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_50
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_ProofOrCE_50
forall a b. a -> b
coe
                    (case AgdaAny -> T_ProofOrCE_50
forall a b. a -> b
coe AgdaAny
v8 of
                       C_proof_56 AgdaAny
v9
                         -> let v10 :: AgdaAny
v10
                                  = (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_ProofOrCE_50)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> [AgdaAny]
-> [AgdaAny]
-> T_ProofOrCE_50
du_pcePointwise_316 (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 -> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v0) ((AgdaAny -> AgdaAny -> T_ProofOrCE_50) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_ProofOrCE_50
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_50
forall a b. a -> b
coe AgdaAny
v10 of
                                 C_proof_56 AgdaAny
v11
                                   -> (AgdaAny -> T_ProofOrCE_50) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_ProofOrCE_50
C_proof_56
                                        ((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_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v14 AgdaAny
v15 AgdaAny
v16 -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v14 AgdaAny
v15 AgdaAny
v16
                                 T_ProofOrCE_50
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v12 AgdaAny
v13 AgdaAny
v14 -> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> AgdaAny -> AgdaAny -> T_ProofOrCE_50
C_ce_64 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v12 AgdaAny
v13 AgdaAny
v14
                       T_ProofOrCE_50
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_ProofOrCE_50
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_ProofOrCE_50
forall a. a
MAlonzo.RTE.mazUnreachableError