{-# 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 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.Builtin.IO
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation.Equality
import qualified MAlonzo.Code.VerifiedCompilation.UCaseOfCase
import qualified MAlonzo.Code.VerifiedCompilation.UForceDelay
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation

import qualified Data.Text.IO as TextIO
import qualified System.IO as IO
import qualified Data.Text as Text
-- VerifiedCompilation.Trace
d_Trace_8 :: p -> p -> p -> p -> ()
d_Trace_8 p
a0 p
a1 p
a2 p
a3 = ()
data T_Trace_8 = C_empty_16 | C_cons_28 AgdaAny T_Trace_8
-- VerifiedCompilation.IsTransformation
d_IsTransformation_30 :: p -> p -> p -> p -> ()
d_IsTransformation_30 p
a0 p
a1 p
a2 p
a3 = ()
data T_IsTransformation_30
  = C_isCoC_40 MAlonzo.Code.VerifiedCompilation.UCaseOfCase.T_CoC_4 |
    C_isFD_50 MAlonzo.Code.VerifiedCompilation.UForceDelay.T_FD_84
-- VerifiedCompilation.isTrace?
d_isTrace'63'_58 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  (() ->
   MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  (MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_isTrace'63'_58 :: ()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32
d_isTrace'63'_58 ~()
v0 ~T_DecEq_6
v1 ~() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
v2 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v3 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v4 = (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_58 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v3 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v4
du_isTrace'63'_58 ::
  (MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_isTrace'63'_58 :: (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_58 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1
  = case T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> [Any]
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386
        -> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (T_Trace_8 -> Any
forall a b. a -> b
coe T_Trace_8
C_empty_16))
      MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
        -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v2 of
             MAlonzo.Code.Utils.C__'44'__378 Any
v4 Any
v5
               -> let v6 :: t
v6 = ((T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
 -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
 -> T_Dec_32)
-> Any -> Any -> t
forall a b. a -> b
coe (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_58 ((T__'8866'_14 -> T__'8866'_14 -> T_Dec_32) -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3) in
                  Any -> T_Dec_32
forall a b. a -> b
coe
                    (case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v6 of
                       MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
v8
                         -> if Bool -> Bool
forall a b. a -> b
coe Bool
v7
                              then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v8 of
                                     MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v9
                                       -> let v10 :: t
v10 = (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32) -> Any -> Any -> t
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v0 Any
v4 Any
v5 in
                                          Any -> Any
forall a b. a -> b
coe
                                            (case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v10 of
                                               MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v11 T_Reflects_14
v12
                                                 -> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
                                                      then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v12 of
                                                             MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v13
                                                               -> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                    Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                                    (Bool -> Any
forall a b. a -> b
coe Bool
v11)
                                                                    ((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
                                                                       Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                                                                       ((Any -> T_Trace_8 -> T_Trace_8) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> T_Trace_8 -> T_Trace_8
C_cons_28 Any
v13 Any
v9))
                                                             T_Reflects_14
_ -> Any
forall {t}. t
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_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v12)
                                                             ((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                                (Bool -> Any
forall a b. a -> b
coe Bool
v11)
                                                                (T_Reflects_14 -> Any
forall a b. a -> b
coe
                                                                   T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
                                               T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
                                     T_Reflects_14
_ -> Any
forall {t}. t
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_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v8)
                                     ((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                        Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> Any
forall a b. a -> b
coe Bool
v7)
                                        (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
                       T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
             (Any, Any)
_ -> T_Dec_32
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      [Any]
_ -> T_Dec_32
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.isTransformation?
d_isTransformation'63'_162 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_isTransformation'63'_162 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
d_isTransformation'63'_162 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
  = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_162 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isTransformation'63'_162 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_isTransformation'63'_162 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_162 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = let v3 :: t
v3
          = (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> Any -> Any -> Any -> t
forall a b. a -> b
coe
              T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
MAlonzo.Code.VerifiedCompilation.UCaseOfCase.du_isCoC'63'_266
              (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
    Any -> T_Dec_32
forall a b. a -> b
coe
      (let v4 :: t
v4
             = (T_DecEq_6
 -> Integer -> Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> Any -> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
                 T_DecEq_6
-> Integer -> Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
MAlonzo.Code.VerifiedCompilation.UForceDelay.du_isFD'63'_186
                 (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)
                 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
       Any -> Any
forall a b. a -> b
coe
         (case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v4 of
            MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v5 T_Reflects_14
v6
              -> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
                   then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v6 of
                          MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v7
                            -> case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v3 of
                                 MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v8 T_Reflects_14
v9
                                   -> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
                                        then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v9 of
                                               MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v10
                                                 -> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                      (Bool -> Any
forall a b. a -> b
coe Bool
v8)
                                                      ((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
                                                         Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                                                         ((T_CoC_4 -> T_IsTransformation_30) -> Any -> Any
forall a b. a -> b
coe T_CoC_4 -> T_IsTransformation_30
C_isCoC_40 Any
v10))
                                               T_Reflects_14
_ -> Any
forall {t}. t
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_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v9)
                                               ((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                  (Bool -> Any
forall a b. a -> b
coe Bool
v5)
                                                  ((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
                                                     Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                                                     ((T_FD_84 -> T_IsTransformation_30) -> Any -> Any
forall a b. a -> b
coe T_FD_84 -> T_IsTransformation_30
C_isFD_50 Any
v7)))
                                 T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
                          T_Reflects_14
_ -> Any
forall {t}. t
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_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v6)
                          (case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v3 of
                             MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
v8
                               -> if Bool -> Bool
forall a b. a -> b
coe Bool
v7
                                    then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v8 of
                                           MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v9
                                             -> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                  Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                                                  (Bool -> Any
forall a b. a -> b
coe Bool
v7)
                                                  ((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
                                                     Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
                                                     ((T_CoC_4 -> T_IsTransformation_30) -> Any -> Any
forall a b. a -> b
coe T_CoC_4 -> T_IsTransformation_30
C_isCoC_40 Any
v9))
                                           T_Reflects_14
_ -> Any
forall {t}. t
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_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v8)
                                           ((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
                                              Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> Any
forall a b. a -> b
coe Bool
v7)
                                              (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
                             T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
            T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
-- VerifiedCompilation.showTranslation
d_showTranslation_228 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTranslation_228 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_16
-> Text
d_showTranslation_228 ~()
v0 ~T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 T_Translation_16
v4
  = T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 T__'8866'_14
v2 T__'8866'_14
v3 T_Translation_16
v4
du_showTranslation_228 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showTranslation_228 :: T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 T__'8866'_14
v0 T__'8866'_14
v1 T_Translation_16
v2
  = case T_Translation_16 -> T_Translation_16
forall a b. a -> b
coe T_Translation_16
v2 of
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_28 Any
v5
        -> Text -> Text
forall a b. a -> b
coe (Text
"istranslation TODO" :: Data.Text.Text)
      T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_32
        -> Text -> Text
forall a b. a -> b
coe (Text
"var" :: Data.Text.Text)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_38 T_Translation_16
v5
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
             MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v6
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                    MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v7
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(\411 " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v6) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T_Translation_16 -> Any
forall a b. a -> b
coe T_Translation_16
v5))
                              (Text
")" :: Data.Text.Text))
                    T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_48 T_Translation_16
v7 T_Translation_16
v8
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
             MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v9 T__'8866'_14
v10
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                    MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v11 T__'8866'_14
v12
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(app " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v9) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T_Translation_16 -> Any
forall a b. a -> b
coe T_Translation_16
v7))
                              ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                 (Text
" " :: Data.Text.Text)
                                 ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                    ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v10) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v12) (T_Translation_16 -> Any
forall a b. a -> b
coe T_Translation_16
v8))
                                    (Text
")" :: Data.Text.Text))))
                    T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_force_54 T_Translation_16
v5
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
             MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v6
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                    MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v7
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(force " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v6) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T_Translation_16 -> Any
forall a b. a -> b
coe T_Translation_16
v5))
                              (Text
")" :: Data.Text.Text))
                    T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_delay_60 T_Translation_16
v5
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
             MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v6
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                    MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v7
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(delay " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v6) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T_Translation_16 -> Any
forall a b. a -> b
coe T_Translation_16
v5))
                              (Text
")" :: Data.Text.Text))
                    T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_con_64
        -> Text -> Text
forall a b. a -> b
coe (Text
"con" :: Data.Text.Text)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_constr_72 T_Pointwise_48
v6
        -> Text -> Text
forall a b. a -> b
coe (Text
"(constr TODO)" :: Data.Text.Text)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_case_82 T_Pointwise_48
v7 T_Translation_16
v8
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
             MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v9 [T__'8866'_14]
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
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(case TODO " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v9) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T_Translation_16 -> Any
forall a b. a -> b
coe T_Translation_16
v8))
                              (Text
")" :: Data.Text.Text))
                    T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_builtin_86
        -> Text -> Text
forall a b. a -> b
coe (Text
"builtin" :: Data.Text.Text)
      T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_error_88
        -> Text -> Text
forall a b. a -> b
coe (Text
"error" :: Data.Text.Text)
      T_Translation_16
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.showTrace
d_showTrace_254 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14) ->
  T_Trace_8 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTrace_254 :: ()
-> T_DecEq_6
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_8
-> Text
d_showTrace_254 ~()
v0 ~T_DecEq_6
v1 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v2 T_Trace_8
v3 = T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_8 -> Text
du_showTrace_254 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v2 T_Trace_8
v3
du_showTrace_254 ::
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14) ->
  T_Trace_8 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showTrace_254 :: T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_8 -> Text
du_showTrace_254 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 T_Trace_8
v1
  = case T_Trace_8 -> T_Trace_8
forall a b. a -> b
coe T_Trace_8
v1 of
      T_Trace_8
C_empty_16 -> Text -> Text
forall a b. a -> b
coe (Text
"empty" :: Data.Text.Text)
      C_cons_28 Any
v7 T_Trace_8
v8
        -> case T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> [Any]
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 of
             MAlonzo.Code.Utils.C__'8759'__388 Any
v9 [Any]
v10
               -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v9 of
                    MAlonzo.Code.Utils.C__'44'__378 Any
v11 Any
v12
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"(cons " :: Data.Text.Text)
                           ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              ((T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_16 -> Text
du_showTranslation_228 (Any -> Any
forall a b. a -> b
coe Any
v11) (Any -> Any
forall a b. a -> b
coe Any
v12) (Any -> Any
forall a b. a -> b
coe Any
v7))
                              ((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                 ((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
 -> T_Trace_8 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_8 -> Text
du_showTrace_254 ([Any] -> Any
forall a b. a -> b
coe [Any]
v10) (T_Trace_8 -> Any
forall a b. a -> b
coe T_Trace_8
v8)) (Text
")" :: Data.Text.Text)))
                    (Any, Any)
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             [Any]
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      T_Trace_8
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.serializeTraceProof
d_serializeTraceProof_266 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_serializeTraceProof_266 :: ()
-> T_DecEq_6
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32
-> Text
d_serializeTraceProof_266 ~()
v0 ~T_DecEq_6
v1 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v2 T_Dec_32
v3
  = T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_266 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v2 T_Dec_32
v3
du_serializeTraceProof_266 ::
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14) ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_serializeTraceProof_266 :: T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_266 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 T_Dec_32
v1
  = case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v1 of
      MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v2 T_Reflects_14
v3
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
             then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v3 of
                    MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v4
                      -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"yes " :: Data.Text.Text) ((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
 -> T_Trace_8 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_8 -> Text
du_showTrace_254 (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0) (Any -> Any
forall a b. a -> b
coe Any
v4))
                    T_Reflects_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             else (Any -> Any -> Any) -> Any -> Any -> Text
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v3) (Text -> Any
forall a b. a -> b
coe (Text
"no" :: Data.Text.Text))
      T_Dec_32
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.FileHandle
type T_FileHandle_272 = IO.Handle
d_FileHandle_272 :: a
d_FileHandle_272
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: VerifiedCompilation.FileHandle"
-- VerifiedCompilation.writeFile
d_writeFile_274 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.IO.T_IO_8
    () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_writeFile_274 :: Text -> Text -> T_IO_8 () ()
d_writeFile_274 = \Text
f -> [Char] -> Text -> T_IO_8 () ()
TextIO.writeFile (Text -> [Char]
Text.unpack Text
f)
-- VerifiedCompilation.stderr
d_stderr_276 :: T_FileHandle_272
d_stderr_276 :: T_FileHandle_272
d_stderr_276 = T_FileHandle_272
IO.stderr
-- VerifiedCompilation.hPutStrLn
d_hPutStrLn_278 ::
  T_FileHandle_272 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.IO.T_IO_8
    () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_hPutStrLn_278 :: T_FileHandle_272 -> Text -> T_IO_8 () ()
d_hPutStrLn_278 = T_FileHandle_272 -> Text -> T_IO_8 () ()
TextIO.hPutStr
-- VerifiedCompilation.buildPairs
d_buildPairs_282 ::
  () ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14)
d_buildPairs_282 :: ()
-> [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
d_buildPairs_282 ~()
v0 [T__'8866'_14]
v1 = [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_282 [T__'8866'_14]
v1
du_buildPairs_282 ::
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Utils.T_List_382
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Untyped.T__'8866'_14
       MAlonzo.Code.Untyped.T__'8866'_14)
du_buildPairs_282 :: [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_282 [T__'8866'_14]
v0
  = case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v0 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall a b. a -> b
coe [T__'8866'_14]
v0
      MAlonzo.Code.Utils.C__'8759'__388 Any
v1 [Any]
v2
        -> case [Any] -> [Any]
forall a b. a -> b
coe [Any]
v2 of
             [Any]
MAlonzo.Code.Utils.C_'91''93'_386
               -> (Any -> [Any] -> [Any])
-> Any
-> Any
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall a b. a -> b
coe
                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
                    ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378 (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v1)) ([Any] -> Any
forall a b. a -> b
coe [Any]
v2)
             MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
               -> (Any -> [Any] -> [Any])
-> Any
-> Any
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall a b. a -> b
coe
                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
                    ((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378 (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
                    (([T__'8866'_14]
 -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_282 ([Any] -> Any
forall a b. a -> b
coe [Any]
v2))
             [Any]
_ -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      [Any]
_ -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.traverseEitherList
d_traverseEitherList_298 ::
  () ->
  () ->
  () ->
  (AgdaAny -> MAlonzo.Code.Utils.T_Either_6 AgdaAny AgdaAny) ->
  MAlonzo.Code.Utils.T_List_382 AgdaAny ->
  MAlonzo.Code.Utils.T_Either_6
    AgdaAny (MAlonzo.Code.Utils.T_List_382 AgdaAny)
d_traverseEitherList_298 :: ()
-> ()
-> ()
-> (Any -> T_Either_6 Any Any)
-> [Any]
-> T_Either_6 Any [Any]
d_traverseEitherList_298 ~()
v0 ~()
v1 ~()
v2 Any -> T_Either_6 Any Any
v3 [Any]
v4
  = (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_298 Any -> T_Either_6 Any Any
v3 [Any]
v4
du_traverseEitherList_298 ::
  (AgdaAny -> MAlonzo.Code.Utils.T_Either_6 AgdaAny AgdaAny) ->
  MAlonzo.Code.Utils.T_List_382 AgdaAny ->
  MAlonzo.Code.Utils.T_Either_6
    AgdaAny (MAlonzo.Code.Utils.T_List_382 AgdaAny)
du_traverseEitherList_298 :: (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_298 Any -> T_Either_6 Any Any
v0 [Any]
v1
  = case [Any] -> [Any]
forall a b. a -> b
coe [Any]
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_386
        -> (Any -> T_Either_6 Any Any) -> Any -> T_Either_6 Any [Any]
forall a b. a -> b
coe Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ([Any] -> Any
forall a b. a -> b
coe [Any]
v1)
      MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
        -> let v4 :: t
v4 = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe Any -> T_Either_6 Any Any
v0 Any
v2 in
           Any -> T_Either_6 Any [Any]
forall a b. a -> b
coe
             (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v4 of
                MAlonzo.Code.Utils.C_inj'8321'_12 Any
v5 -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v4
                MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
                  -> let v6 :: t
v6 = ((Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any])
-> Any -> Any -> t
forall a b. a -> b
coe (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_298 ((Any -> T_Either_6 Any Any) -> Any
forall a b. a -> b
coe Any -> T_Either_6 Any Any
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3) in
                     Any -> Any
forall a b. a -> b
coe
                       (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v6 of
                          MAlonzo.Code.Utils.C_inj'8321'_12 Any
v7 -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6
                          MAlonzo.Code.Utils.C_inj'8322'_14 Any
v7
                            -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                 Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388 (Any -> Any
forall a b. a -> b
coe Any
v5) (Any -> Any
forall a b. a -> b
coe Any
v7))
                          T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
                T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
      [Any]
_ -> T_Either_6 Any [Any]
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.certifier
d_certifier_354 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
  (MAlonzo.Code.Utils.T_List_382
     (MAlonzo.Code.Utils.T__'215'__364
        MAlonzo.Code.Untyped.T__'8866'_14
        MAlonzo.Code.Untyped.T__'8866'_14) ->
   MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_certifier_354 :: ()
-> T_DecEq_6
-> T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
    -> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
d_certifier_354 ~()
v0 ~T_DecEq_6
v1 T_List_382 T_Untyped_146
v2 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v3 = T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
    -> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
du_certifier_354 T_List_382 T_Untyped_146
v2 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v3
du_certifier_354 ::
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
  (MAlonzo.Code.Utils.T_List_382
     (MAlonzo.Code.Utils.T__'215'__364
        MAlonzo.Code.Untyped.T__'8866'_14
        MAlonzo.Code.Untyped.T__'8866'_14) ->
   MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_ScopeError_576
    MAlonzo.Code.Agda.Builtin.String.T_String_6
du_certifier_354 :: T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
    -> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
du_certifier_354 T_List_382 T_Untyped_146
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v1
  = let v2 :: t
v2
          = ((Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any])
-> Any -> Any -> t
forall a b. a -> b
coe
              (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_298
              ((T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14) -> Any
forall a b. a -> b
coe T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
MAlonzo.Code.Untyped.du_toWellScoped_358) (T_List_382 T_Untyped_146 -> Any
forall a b. a -> b
coe T_List_382 T_Untyped_146
v0) in
    Any -> T_Either_6 T_ScopeError_576 Text
forall a b. a -> b
coe
      (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v2 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v3 -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v3
           -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                ((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
 -> T_Dec_32 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe
                   T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_266 (([T__'8866'_14]
 -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_282 (Any -> Any
forall a b. a -> b
coe Any
v3))
                   ((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32)
-> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v1 (([T__'8866'_14]
 -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_282 (Any -> Any
forall a b. a -> b
coe Any
v3))))
         T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.runCertifier
runCertifier ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Agda.Builtin.IO.T_IO_8
    () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
runCertifier :: Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
runCertifier = (Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ())
-> Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
forall a b. a -> b
coe Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
d_runCertifier_384
d_runCertifier_384 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Agda.Builtin.IO.T_IO_8
    AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_runCertifier_384 :: Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
d_runCertifier_384 Text
v0 T_List_382 T_Untyped_146
v1
  = let v2 :: t
v2
          = (T_List_382 T_Untyped_146
 -> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
     -> T_Dec_32)
 -> T_Either_6 T_ScopeError_576 Text)
-> Any -> Any -> t
forall a b. a -> b
coe
              T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
    -> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
du_certifier_354 (T_List_382 T_Untyped_146 -> Any
forall a b. a -> b
coe T_List_382 T_Untyped_146
v1)
              (((T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
 -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
 -> T_Dec_32)
-> Any -> Any
forall a b. a -> b
coe
                 (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_58
                 ((()
 -> T_DecEq_6
 -> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
 -> T__'8866'_14
 -> T__'8866'_14
 -> T_Dec_32)
-> Any -> Any -> (Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                    ()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_32
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_100
                    Any
forall {t}. t
erased
                    ((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
                       T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
                       (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.d_EmptyEq_128))
                    (\ Any
v2 Any
v3 Any
v4 Any
v5 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_162 Any
v3 Any
v4 Any
v5))) in
    Any -> T_IO_8 () ()
forall a b. a -> b
coe
      (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v2 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v3
           -> (T_FileHandle_272 -> Text -> T_IO_8 () ())
-> T_FileHandle_272 -> Text -> Any
forall a b. a -> b
coe T_FileHandle_272 -> Text -> T_IO_8 () ()
d_hPutStrLn_278 T_FileHandle_272
d_stderr_276 (Text
"error" :: Data.Text.Text)
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v3
           -> (Text -> Text -> T_IO_8 () ()) -> Any -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> T_IO_8 () ()
d_writeFile_274
                ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Text
v0
                   (Text
".agda" :: Data.Text.Text))
                Any
v3
         T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)