{-# 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_6 :: p -> p -> p -> ()
d_Trace_6 p
a0 p
a1 p
a2 = ()
data T_Trace_6 = C_empty_12 | C_cons_22 AgdaAny T_Trace_6
-- VerifiedCompilation.IsTransformation
d_IsTransformation_24 :: p -> p -> p -> ()
d_IsTransformation_24 p
a0 p
a1 p
a2 = ()
data T_IsTransformation_24
  = C_isCoC_32 MAlonzo.Code.VerifiedCompilation.UCaseOfCase.T_CoC_4 |
    C_isFD_40 MAlonzo.Code.VerifiedCompilation.UForceDelay.T_FD_48
-- VerifiedCompilation.isTrace?
d_isTrace'63'_46 ::
  () ->
  (() ->
   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'_46 :: ()
-> (() -> 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'_46 ~()
v0 ~() -> T__'8866'_14 -> T__'8866'_14 -> ()
v1 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v2 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v3 = (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'_46 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v2 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v3
du_isTrace'63'_46 ::
  (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'_46 :: (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'_46 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_6 -> Any
forall a b. a -> b
coe T_Trace_6
C_empty_12))
      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'_46 ((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_6 -> T_Trace_6) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> T_Trace_6 -> T_Trace_6
C_cons_22 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'_150 ::
  () ->
  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'_150 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
d_isTransformation'63'_150 ~()
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'_150 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isTransformation'63'_150 ::
  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'_150 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_150 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'_264
              (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'_138
                 (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_24) -> Any -> Any
forall a b. a -> b
coe T_CoC_4 -> T_IsTransformation_24
C_isCoC_32 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_48 -> T_IsTransformation_24) -> Any -> Any
forall a b. a -> b
coe T_FD_48 -> T_IsTransformation_24
C_isFD_40 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_24) -> Any -> Any
forall a b. a -> b
coe T_CoC_4 -> T_IsTransformation_24
C_isCoC_32 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_214 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTranslation_214 :: () -> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
d_showTranslation_214 ~()
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v3
  = T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v3
du_showTranslation_214 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showTranslation_214 :: T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 T__'8866'_14
v0 T__'8866'_14
v1 T_Translation_12
v2
  = case T_Translation_12 -> T_Translation_12
forall a b. a -> b
coe T_Translation_12
v2 of
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_22 Any
v6
        -> Text -> Text
forall a b. a -> b
coe (Text
"istranslation TODO" :: Data.Text.Text)
      T_Translation_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_28
        -> Text -> Text
forall a b. a -> b
coe (Text
"var" :: Data.Text.Text)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_36 T_Translation_12
v6
        -> 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
v7
               -> 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
v8
                      -> (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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v8) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v6))
                              (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_12
v8 T_Translation_12
v9
        -> 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
v10 T__'8866'_14
v11
               -> 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
v12 T__'8866'_14
v13
                      -> (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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (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_12 -> Any
forall a b. a -> b
coe T_Translation_12
v8))
                              ((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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v13) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v9))
                                    (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_56 T_Translation_12
v6
        -> 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
v7
               -> 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
v8
                      -> (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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v8) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v6))
                              (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_64 T_Translation_12
v6
        -> 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
v7
               -> 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
v8
                      -> (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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v8) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v6))
                              (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_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_con_70
        -> Text -> Text
forall a b. a -> b
coe (Text
"con" :: Data.Text.Text)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_constr_80 T_Pointwise_48
v7
        -> Text -> Text
forall a b. a -> b
coe (Text
"(constr TODO)" :: Data.Text.Text)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_case_92 T_Pointwise_48
v8 T_Translation_12
v9
        -> 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
v10 [T__'8866'_14]
v11
               -> 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
v12 [T__'8866'_14]
v13
                      -> (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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (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_12 -> Any
forall a b. a -> b
coe T_Translation_12
v9))
                              (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_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_builtin_98
        -> Text -> Text
forall a b. a -> b
coe (Text
"builtin" :: Data.Text.Text)
      T_Translation_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_error_102
        -> Text -> Text
forall a b. a -> b
coe (Text
"error" :: Data.Text.Text)
      T_Translation_12
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.showTrace
d_showTrace_238 ::
  () ->
  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_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTrace_238 :: ()
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6
-> Text
d_showTrace_238 ~()
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Trace_6
v2 = T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Trace_6
v2
du_showTrace_238 ::
  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_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showTrace_238 :: T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 T_Trace_6
v1
  = case T_Trace_6 -> T_Trace_6
forall a b. a -> b
coe T_Trace_6
v1 of
      T_Trace_6
C_empty_12 -> Text -> Text
forall a b. a -> b
coe (Text
"empty" :: Data.Text.Text)
      C_cons_22 Any
v6 T_Trace_6
v7
        -> 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
v8 [Any]
v9
               -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v8 of
                    MAlonzo.Code.Utils.C__'44'__378 Any
v10 Any
v11
                      -> (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_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (Any -> Any
forall a b. a -> b
coe Any
v10) (Any -> Any
forall a b. a -> b
coe Any
v11) (Any -> Any
forall a b. a -> b
coe Any
v6))
                              ((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_6 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 ([Any] -> Any
forall a b. a -> b
coe [Any]
v9) (T_Trace_6 -> Any
forall a b. a -> b
coe T_Trace_6
v7)) (Text
")" :: Data.Text.Text)))
                    (Any, Any)
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
             [Any]
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
      T_Trace_6
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- VerifiedCompilation.serializeTraceProof
d_serializeTraceProof_248 ::
  () ->
  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_248 :: ()
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32
-> Text
d_serializeTraceProof_248 ~()
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Dec_32
v2
  = T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_248 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Dec_32
v2
du_serializeTraceProof_248 ::
  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_248 :: T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_248 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_6 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 (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_254 = IO.Handle
d_FileHandle_254 :: a
d_FileHandle_254
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: VerifiedCompilation.FileHandle"
-- VerifiedCompilation.writeFile
d_writeFile_256 ::
  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_256 :: Text -> Text -> T_IO_8 () ()
d_writeFile_256 = \Text
f -> [Char] -> Text -> T_IO_8 () ()
TextIO.writeFile (Text -> [Char]
Text.unpack Text
f)
-- VerifiedCompilation.stderr
d_stderr_258 :: T_FileHandle_254
d_stderr_258 :: T_FileHandle_254
d_stderr_258 = T_FileHandle_254
IO.stderr
-- VerifiedCompilation.hPutStrLn
d_hPutStrLn_260 ::
  T_FileHandle_254 ->
  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_260 :: T_FileHandle_254 -> Text -> T_IO_8 () ()
d_hPutStrLn_260 = T_FileHandle_254 -> Text -> T_IO_8 () ()
TextIO.hPutStr
-- VerifiedCompilation.buildPairs
d_buildPairs_264 ::
  () ->
  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_264 :: ()
-> [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
d_buildPairs_264 ~()
v0 [T__'8866'_14]
v1 = [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 [T__'8866'_14]
v1
du_buildPairs_264 ::
  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_264 :: [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 [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_264 ([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_280 ::
  () ->
  () ->
  () ->
  (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_280 :: ()
-> ()
-> ()
-> (Any -> T_Either_6 Any Any)
-> [Any]
-> T_Either_6 Any [Any]
d_traverseEitherList_280 ~()
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_280 Any -> T_Either_6 Any Any
v3 [Any]
v4
du_traverseEitherList_280 ::
  (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_280 :: (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_280 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_280 ((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_334 ::
  () ->
  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_334 :: ()
-> 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_334 ~()
v0 T_List_382 T_Untyped_146
v1 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
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
du_certifier_334 T_List_382 T_Untyped_146
v1 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v2
du_certifier_334 ::
  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_334 :: 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_334 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_280
              ((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_248 (([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_264 (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_264 (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_364
d_runCertifier_364 ::
  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_364 :: Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
d_runCertifier_364 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_334 (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'_46
                 ((()
 -> 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'_114
                    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'_150 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_254 -> Text -> T_IO_8 () ())
-> T_FileHandle_254 -> Text -> Any
forall a b. a -> b
coe T_FileHandle_254 -> Text -> T_IO_8 () ()
d_hPutStrLn_260 T_FileHandle_254
d_stderr_258 (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_256
                ((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)