{-# 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.Evaluator.Program 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.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Algorithmic
import qualified MAlonzo.Code.Algorithmic.CEK
import qualified MAlonzo.Code.Algorithmic.CK
import qualified MAlonzo.Code.Algorithmic.Erasure
import qualified MAlonzo.Code.Algorithmic.Evaluation
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Check
import qualified MAlonzo.Code.Cost
import qualified MAlonzo.Code.Cost.Base
import qualified MAlonzo.Code.Cost.Model
import qualified MAlonzo.Code.Cost.Raw
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Evaluator.Base
import qualified MAlonzo.Code.Raw
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Scoped.Extrication
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Untyped.CEKWithCost
import qualified MAlonzo.Code.Utils

import PlutusCore.Executable.Common
import PlutusCore.Executable.Parsers
import PlutusCore.DeBruijn
import qualified UntypedPlutusCore as U
import qualified UntypedPlutusCore.Parser as U
import qualified Untyped as U
import Raw
import PlutusCore
import Data.Bifunctor
import Data.Functor
import Data.Either
import Control.Monad.Trans.Except
import Opts
-- Evaluator.Program.Format
type T_Format_14 = Format
d_Format_14 :: a
d_Format_14
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Program.Format"
-- Evaluator.Program.Input
type T_Input_16 = Input
d_Input_16 :: a
d_Input_16
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Program.Input"
-- Evaluator.Program.ProgramN
type T_ProgramN_18 =
  PlutusCore.Program TyName Name DefaultUni DefaultFun PlutusCore.SrcSpan
d_ProgramN_18 :: a
d_ProgramN_18
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Program.ProgramN"
-- Evaluator.Program.Program
type T_Program_20 =
  PlutusCore.Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
d_Program_20 :: a
d_Program_20
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Program.Program"
-- Evaluator.Program.convP
d_convP_22 :: T_Program_20 -> MAlonzo.Code.Raw.T_RawTm_30
d_convP_22 :: T_Program_20 -> T_RawTm_30
d_convP_22 = T_Program_20 -> T_RawTm_30
forall a.
Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
-> T_RawTm_30
convP
-- Evaluator.Program.deBruijnify
d_deBruijnify_24 ::
  T_ProgramN_18 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_FreeVariableError_574 T_Program_20
d_deBruijnify_24 :: T_ProgramN_18 -> T_Either_6 FreeVariableError T_Program_20
d_deBruijnify_24
  = \ (Program SrcSpan
ann Version
ver Term TyName Name DefaultUni DefaultFun SrcSpan
tm) -> (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
 -> T_Program_20)
-> Either
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_Program_20
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Program NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_Program_20
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Program
   NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
 -> T_Program_20)
-> (Term
      NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
    -> Program
         NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_Program_20
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan
-> Version
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> Program
     NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program SrcSpan
ann Version
ver) (Either
   FreeVariableError
   (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> T_Either_6 FreeVariableError T_Program_20)
-> (Except
      FreeVariableError
      (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
    -> Either
         FreeVariableError
         (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> Except
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_Program_20
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except
  FreeVariableError
  (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> Either
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e a. Except e a -> Either e a
runExcept (Except
   FreeVariableError
   (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> T_Either_6 FreeVariableError T_Program_20)
-> Except
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_Program_20
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun SrcSpan
-> Except
     FreeVariableError
     (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term TyName Name uni fun ann
-> m (Term NamedTyDeBruijn NamedDeBruijn uni fun ann)
deBruijnTerm Term TyName Name DefaultUni DefaultFun SrcSpan
tm
-- Evaluator.Program.ProgramNU
type T_ProgramNU_26 =
  U.Program Name DefaultUni DefaultFun PlutusCore.SrcSpan
d_ProgramNU_26 :: a
d_ProgramNU_26
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Program.ProgramNU"
-- Evaluator.Program.ProgramU
type T_ProgramU_28 =
  U.Program NamedDeBruijn DefaultUni DefaultFun ()
d_ProgramU_28 :: a
d_ProgramU_28
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Program.ProgramU"
-- Evaluator.Program.deBruijnifyU
d_deBruijnifyU_30 ::
  T_ProgramNU_26 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Scoped.T_FreeVariableError_574 T_ProgramU_28
d_deBruijnifyU_30 :: T_ProgramNU_26 -> T_Either_6 FreeVariableError T_ProgramU_28
d_deBruijnifyU_30
  = \ (U.Program SrcSpan
ann Version
ver Term Name DefaultUni DefaultFun SrcSpan
tm) -> (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan -> T_ProgramU_28)
-> Either
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_ProgramU_28
forall b c a. (b -> c) -> Either a b -> Either a c
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Program NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_ProgramU_28
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Program NamedDeBruijn DefaultUni DefaultFun SrcSpan
 -> T_ProgramU_28)
-> (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan
    -> Program NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> Term NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_ProgramU_28
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan
-> Version
-> Term NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> Program NamedDeBruijn DefaultUni DefaultFun SrcSpan
forall name (uni :: * -> *) fun ann.
ann -> Version -> Term name uni fun ann -> Program name uni fun ann
U.Program SrcSpan
ann Version
ver) (Either
   FreeVariableError
   (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> T_Either_6 FreeVariableError T_ProgramU_28)
-> (Except
      FreeVariableError
      (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
    -> Either
         FreeVariableError
         (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> Except
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_ProgramU_28
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except
  FreeVariableError
  (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> Either
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e a. Except e a -> Either e a
runExcept (Except
   FreeVariableError
   (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
 -> T_Either_6 FreeVariableError T_ProgramU_28)
-> Except
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_ProgramU_28
forall a b. (a -> b) -> a -> b
$ Term Name DefaultUni DefaultFun SrcSpan
-> Except
     FreeVariableError
     (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall e (m :: * -> *) (uni :: * -> *) fun ann.
(AsFreeVariableError e, MonadError e m) =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
U.deBruijnTerm Term Name DefaultUni DefaultFun SrcSpan
tm
-- Evaluator.Program.convPU
d_convPU_32 :: T_ProgramU_28 -> MAlonzo.Code.RawU.T_Untyped_146
d_convPU_32 :: T_ProgramU_28 -> T_Untyped_146
d_convPU_32 = T_ProgramU_28 -> T_Untyped_146
forall a.
Program NamedDeBruijn DefaultUni DefaultFun a -> T_Untyped_146
U.convP
-- Evaluator.Program.BudgetMode
d_BudgetMode_36 :: p -> ()
d_BudgetMode_36 p
a0 = ()
type T_BudgetMode_36 a0 = BudgetMode a0
pattern $mC_Silent_40 :: forall {r} {a}. BudgetMode a -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_Silent_40 :: forall {a}. BudgetMode a
C_Silent_40 = Silent
pattern $mC_Counting_42 :: forall {r} {a}. BudgetMode a -> (a -> r) -> ((# #) -> r) -> r
$bC_Counting_42 :: forall {a}. a -> BudgetMode a
C_Counting_42 a0 = Counting a0
pattern $mC_Tallying_44 :: forall {r} {a}. BudgetMode a -> (a -> r) -> ((# #) -> r) -> r
$bC_Tallying_44 :: forall {a}. a -> BudgetMode a
C_Tallying_44 a0 = Tallying a0
check_Silent_40 :: forall xA. T_BudgetMode_36 xA
check_Silent_40 :: forall {a}. BudgetMode a
check_Silent_40 = BudgetMode xA
forall {a}. BudgetMode a
Silent
check_Counting_42 :: forall xA. xA -> T_BudgetMode_36 xA
check_Counting_42 :: forall {a}. a -> BudgetMode a
check_Counting_42 = xA -> BudgetMode xA
forall {a}. a -> BudgetMode a
Counting
check_Tallying_44 :: forall xA. xA -> T_BudgetMode_36 xA
check_Tallying_44 :: forall {a}. a -> BudgetMode a
check_Tallying_44 = xA -> BudgetMode xA
forall {a}. a -> BudgetMode a
Tallying
cover_BudgetMode_36 :: BudgetMode a1 -> ()
cover_BudgetMode_36 :: forall a1. BudgetMode a1 -> ()
cover_BudgetMode_36 BudgetMode a1
x
  = case BudgetMode a1
x of
      BudgetMode a1
Silent -> ()
      Counting a1
_ -> ()
      Tallying a1
_ -> ()
-- Evaluator.Program.EvalMode
d_EvalMode_46 :: ()
d_EvalMode_46 = ()
type T_EvalMode_46 = EvalMode
pattern $mC_U_48 :: forall {r}. EvalMode -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_U_48 :: EvalMode
C_U_48 = U
pattern $mC_TL_50 :: forall {r}. EvalMode -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_TL_50 :: EvalMode
C_TL_50 = TL
pattern $mC_TCK_52 :: forall {r}. EvalMode -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_TCK_52 :: EvalMode
C_TCK_52 = TCK
pattern $mC_TCEK_54 :: forall {r}. EvalMode -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_TCEK_54 :: EvalMode
C_TCEK_54 = TCEK
check_U_48 :: T_EvalMode_46
check_U_48 :: EvalMode
check_U_48 = EvalMode
U
check_TL_50 :: T_EvalMode_46
check_TL_50 :: EvalMode
check_TL_50 = EvalMode
TL
check_TCK_52 :: T_EvalMode_46
check_TCK_52 :: EvalMode
check_TCK_52 = EvalMode
TCK
check_TCEK_54 :: T_EvalMode_46
check_TCEK_54 :: EvalMode
check_TCEK_54 = EvalMode
TCEK
cover_EvalMode_46 :: EvalMode -> ()
cover_EvalMode_46 :: EvalMode -> ()
cover_EvalMode_46 EvalMode
x
  = case EvalMode
x of
      EvalMode
U -> ()
      EvalMode
TL -> ()
      EvalMode
TCK -> ()
      EvalMode
TCEK -> ()
-- Evaluator.Program.parsePLC
d_parsePLC_56 ::
  T_ProgramN_18 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Scoped.T_ScopedTm_522
d_parsePLC_56 :: T_ProgramN_18 -> T_Either_6 T_ERROR_12 T_ScopedTm_522
d_parsePLC_56 T_ProgramN_18
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T_ScopedTm_522
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 ->
               (ScopeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                 ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18
                 ((FreeVariableError -> ScopeError) -> Any -> Any
forall a b. a -> b
coe FreeVariableError -> ScopeError
MAlonzo.Code.Scoped.C_freeVariableError_580 (Any -> Any
forall a b. a -> b
coe Any
v1))))
         ((T_ProgramN_18 -> T_Either_6 FreeVariableError T_Program_20)
-> T_ProgramN_18 -> Any
forall a b. a -> b
coe T_ProgramN_18 -> T_Either_6 FreeVariableError T_Program_20
d_deBruijnify_24 T_ProgramN_18
v0))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            ((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
              ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
              ((Integer
 -> T_Weirdℕ_42
 -> T_RawTm_30
 -> T_Either_6 ScopeError T_ScopedTm_522)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                 Integer
-> T_Weirdℕ_42
-> T_RawTm_30
-> T_Either_6 ScopeError T_ScopedTm_522
MAlonzo.Code.Scoped.d_scopeCheckTm_686 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                 (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                 ((Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                    Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_shifter_272 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                    (T_Weirdℕ_42 -> Any
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44) ((T_Program_20 -> T_RawTm_30) -> Any -> Any
forall a b. a -> b
coe T_Program_20 -> T_RawTm_30
d_convP_22 Any
v1)))))
-- Evaluator.Program.parseUPLC
d_parseUPLC_62 ::
  T_ProgramNU_26 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Untyped.T__'8866'_14
d_parseUPLC_62 :: T_ProgramNU_26 -> T_Either_6 T_ERROR_12 T__'8866'_14
d_parseUPLC_62 T_ProgramNU_26
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 T__'8866'_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
      (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
         ((Any -> Any) -> Any
forall a b. a -> b
coe
            (\ Any
v1 ->
               (ScopeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                 ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18
                 ((FreeVariableError -> ScopeError) -> Any -> Any
forall a b. a -> b
coe FreeVariableError -> ScopeError
MAlonzo.Code.Scoped.C_freeVariableError_580 (Any -> Any
forall a b. a -> b
coe Any
v1))))
         ((T_ProgramNU_26 -> T_Either_6 FreeVariableError T_ProgramU_28)
-> T_ProgramNU_26 -> Any
forall a b. a -> b
coe T_ProgramNU_26 -> T_Either_6 FreeVariableError T_ProgramU_28
d_deBruijnifyU_30 T_ProgramNU_26
v0))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            ((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
              ((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
              ((T_Untyped_146 -> T_Either_6 ScopeError T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                 T_Untyped_146 -> T_Either_6 ScopeError T__'8866'_14
MAlonzo.Code.Untyped.d_scopeCheckU0_304 ((T_ProgramU_28 -> T_Untyped_146) -> Any -> Any
forall a b. a -> b
coe T_ProgramU_28 -> T_Untyped_146
d_convPU_32 Any
v1))))
-- Evaluator.Program.typeCheckPLC
d_typeCheckPLC_70 ::
  MAlonzo.Code.Scoped.T_ScopedTm_522 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Check.T_TypeError_12
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_typeCheckPLC_70 :: T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
d_typeCheckPLC_70 T_ScopedTm_522
v0
  = (T_Ctx'8902'_2
 -> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> T_Either_6 T_TypeError_12 T_Σ_14
forall a b. a -> b
coe
      T_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferType_1156
      (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
      (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v0)
-- Evaluator.Program.checkError
d_checkError_76 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Algorithmic.T__'8866'__168
d_checkError_76 :: T__'8866'Nf'8902'__4
-> T__'8866'__168 -> T_Either_6 T_ERROR_12 T__'8866'__168
d_checkError_76 ~T__'8866'Nf'8902'__4
v0 T__'8866'__168
v1 = T__'8866'__168 -> T_Either_6 T_ERROR_12 T__'8866'__168
du_checkError_76 T__'8866'__168
v1
du_checkError_76 ::
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Algorithmic.T__'8866'__168
du_checkError_76 :: T__'8866'__168 -> T_Either_6 T_ERROR_12 T__'8866'__168
du_checkError_76 T__'8866'__168
v0
  = let v1 :: t
v1 = (Any -> T_Either_6 Any Any) -> Any -> t
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__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v0) in
    Any -> T_Either_6 T_ERROR_12 T__'8866'__168
forall a b. a -> b
coe
      (case T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v0 of
         T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258
           -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                   RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                   (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
         T__'8866'__168
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)
-- Evaluator.Program.executePLC
d_executePLC_80 ::
  T_EvalMode_46 ->
  MAlonzo.Code.Scoped.T_ScopedTm_522 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_executePLC_80 :: EvalMode -> T_ScopedTm_522 -> T_Either_6 T_ERROR_12 Text
d_executePLC_80 EvalMode
v0 T_ScopedTm_522
v1
  = case EvalMode -> EvalMode
forall a b. a -> b
coe EvalMode
v0 of
      EvalMode
C_U_48
        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                ((Any -> Any) -> Any
forall a b. a -> b
coe
                   (\ Any
v2 ->
                      (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                        Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                        ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                ((T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
d_typeCheckPLC_70 (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v1)))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v2 ->
                   case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                     MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                       -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                            T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                            (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                               ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                               ((Integer -> T_State_218 -> T_Either_6 RuntimeError T_State_218)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  Integer -> T_State_218 -> T_Either_6 RuntimeError T_State_218
MAlonzo.Code.Untyped.CEK.d_stepper_1234
                                  (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                  ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                     T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                                     (T_Stack_6 -> Any
forall a b. a -> b
coe T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                                     (T_Env_16 -> Any
forall a b. a -> b
coe T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18)
                                     (T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'_14
MAlonzo.Code.Algorithmic.Erasure.d_erase_48
                                        (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                        (T_Ctx_2 -> T_Ctx_2
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe Any
v3)
                                        (Any -> T__'8866'__168
forall a b. a -> b
coe Any
v4)))))
                            ((Any -> Any) -> Any
forall a b. a -> b
coe
                               (\ Any
v5 ->
                                  let v6 :: t
v6
                                        = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350)) in
                                  Any -> Any
forall a b. a -> b
coe
                                    (case Any -> T_State_218
forall a b. a -> b
coe Any
v5 of
                                       MAlonzo.Code.Untyped.CEK.C_'9633'_226 T_Value_14
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
                                              ((T_Untyped_146 -> Text) -> T_Untyped_146 -> Any
forall a b. a -> b
coe
                                                 T_Untyped_146 -> Text
MAlonzo.Code.Evaluator.Base.d_prettyPrintUTm_10
                                                 (T__'8866'_14 -> T_Untyped_146
MAlonzo.Code.Untyped.d_extricateU0_218
                                                    ((T_Value_14 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe
                                                       T_Value_14 -> T__'8866'_14
MAlonzo.Code.Untyped.CEK.d_discharge_126
                                                       (T_Value_14 -> Any
forall a b. a -> b
coe T_Value_14
v7))))
                                       T_State_218
MAlonzo.Code.Untyped.CEK.C_'9670'_228
                                         -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                              Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                              ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                                 RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                                 (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
                                       T_State_218
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6)))
                     T_Σ_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
      EvalMode
C_TL_50
        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                ((Any -> Any) -> Any
forall a b. a -> b
coe
                   (\ Any
v2 ->
                      (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                        Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                        ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                ((T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
d_typeCheckPLC_70 (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v1)))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v2 ->
                   case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                     MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                       -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                            T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                            ((T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                               (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                                  ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                                  ((T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> Integer
 -> T_Either_6 RuntimeError T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                     T__'8866'Nf'8902'__4
-> T__'8866'__168
-> Integer
-> T_Either_6 RuntimeError T__'8866'__168
MAlonzo.Code.Algorithmic.Evaluation.d_stepper_86 (Any -> Any
forall a b. a -> b
coe Any
v3)
                                     (Any -> Any
forall a b. a -> b
coe Any
v4) (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)))
                               ((T__'8866'__168 -> T_Either_6 T_ERROR_12 T__'8866'__168) -> Any
forall a b. a -> b
coe T__'8866'__168 -> T_Either_6 T_ERROR_12 T__'8866'__168
du_checkError_76))
                            ((Any -> Any) -> Any
forall a b. a -> b
coe
                               (\ Any
v5 ->
                                  (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_RawTm_30 -> Text) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                       T_RawTm_30 -> Text
MAlonzo.Code.Evaluator.Base.d_prettyPrintTm_6
                                       (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                          (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                          ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                             Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                             ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                                (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                             ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                                (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                             ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3)
                                                (Any -> Any
forall a b. a -> b
coe Any
v5)))))))
                     T_Σ_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
      EvalMode
C_TCK_52
        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                ((Any -> Any) -> Any
forall a b. a -> b
coe
                   (\ Any
v2 ->
                      (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                        Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                        ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                ((T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
d_typeCheckPLC_70 (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v1)))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v2 ->
                   case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                     MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                       -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                            T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                            (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                               ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                               ((Integer -> T_State_34 -> T_Either_6 RuntimeError T_State_34)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  Integer -> T_State_34 -> T_Either_6 RuntimeError T_State_34
MAlonzo.Code.Algorithmic.CK.du_stepper_372
                                  (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                  ((T__'8866'Nf'8902'__4
 -> T_Stack_18 -> T__'8866'__168 -> T_State_34)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                     T__'8866'Nf'8902'__4 -> T_Stack_18 -> T__'8866'__168 -> T_State_34
MAlonzo.Code.Algorithmic.CK.C__'9659'__40 (Any -> Any
forall a b. a -> b
coe Any
v3)
                                     (T_Stack_18 -> Any
forall a b. a -> b
coe T_Stack_18
MAlonzo.Code.Algorithmic.CK.C_ε_22) (Any -> Any
forall a b. a -> b
coe Any
v4))))
                            ((Any -> Any) -> Any
forall a b. a -> b
coe
                               (\ Any
v5 ->
                                  let v6 :: t
v6
                                        = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350)) in
                                  Any -> Any
forall a b. a -> b
coe
                                    (case Any -> T_State_34
forall a b. a -> b
coe Any
v5 of
                                       MAlonzo.Code.Algorithmic.CK.C_'9633'_50 T__'8866'__168
v7 T_Value_28
v8
                                         -> (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_RawTm_30 -> Text) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                                 T_RawTm_30 -> Text
MAlonzo.Code.Evaluator.Base.d_prettyPrintTm_6
                                                 (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                    (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                    ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                                       Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                                       ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                                       ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                          (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                                       ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                          (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4)
                                                          (Any -> Any
forall a b. a -> b
coe Any
v3) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v7)))))
                                       MAlonzo.Code.Algorithmic.CK.C_'9670'_54 T__'8866'Nf'8902'__4
v7
                                         -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                              Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                              ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                                 RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                                 (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
                                       T_State_34
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6)))
                     T_Σ_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
      EvalMode
C_TCEK_54
        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                ((Any -> Any) -> Any
forall a b. a -> b
coe
                   (\ Any
v2 ->
                      (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                        Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                        ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                ((T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
d_typeCheckPLC_70 (T_ScopedTm_522 -> Any
forall a b. a -> b
coe T_ScopedTm_522
v1)))
             ((Any -> Any) -> Any
forall a b. a -> b
coe
                (\ Any
v2 ->
                   case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                     MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                       -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                            T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                            (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                               ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                               ((Integer -> T_State_1180 -> T_Either_6 RuntimeError T_State_1180)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                  Integer -> T_State_1180 -> T_Either_6 RuntimeError T_State_1180
MAlonzo.Code.Algorithmic.CEK.du_stepper_1532
                                  (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                  ((T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T_Stack_1166
 -> T_Env_26
 -> T__'8866'__168
 -> T_State_1180)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                     T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Stack_1166
-> T_Env_26
-> T__'8866'__168
-> T_State_1180
MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1188
                                     (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3)
                                     (T_Stack_1166 -> Any
forall a b. a -> b
coe T_Stack_1166
MAlonzo.Code.Algorithmic.CEK.C_ε_1170)
                                     (T_Env_26 -> Any
forall a b. a -> b
coe T_Env_26
MAlonzo.Code.Algorithmic.CEK.C_'91''93'_202) (Any -> Any
forall a b. a -> b
coe Any
v4))))
                            ((Any -> Any) -> Any
forall a b. a -> b
coe
                               (\ Any
v5 ->
                                  let v6 :: t
v6
                                        = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe
                                            Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                            ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                               RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                               (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350)) in
                                  Any -> Any
forall a b. a -> b
coe
                                    (case Any -> T_State_1180
forall a b. a -> b
coe Any
v5 of
                                       MAlonzo.Code.Algorithmic.CEK.C_'9633'_1194 T_Value_52
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
                                              ((T_RawTm_30 -> Text) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
                                                 T_RawTm_30 -> Text
MAlonzo.Code.Evaluator.Base.d_prettyPrintTm_6
                                                 (Integer -> T_Weirdℕ_42 -> T_RawTm_30 -> T_RawTm_30
MAlonzo.Code.Scoped.d_unshifter_434
                                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer))
                                                    (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                                    ((Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30)
-> Any -> Any -> Any -> T_RawTm_30
forall a b. a -> b
coe
                                                       Integer -> T_Weirdℕ_42 -> T_ScopedTm_522 -> T_RawTm_30
MAlonzo.Code.Scoped.d_extricateScope_828
                                                       ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                                       ((T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2 -> T_Ctx_2 -> T_Weirdℕ_42
MAlonzo.Code.Scoped.Extrication.d_len_94
                                                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                          (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4))
                                                       ((T_Ctx'8902'_2
 -> T_Ctx_2
 -> T__'8866'Nf'8902'__4
 -> T__'8866'__168
 -> T_ScopedTm_522)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T_ScopedTm_522
MAlonzo.Code.Scoped.Extrication.d_extricate_140
                                                          (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                                          (T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4)
                                                          (Any -> Any
forall a b. a -> b
coe Any
v3)
                                                          ((T__'8866'Nf'8902'__4 -> T_Value_52 -> T__'8866'__168)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                             T__'8866'Nf'8902'__4 -> T_Value_52 -> T__'8866'__168
MAlonzo.Code.Algorithmic.CEK.d_discharge_228
                                                             (Any -> Any
forall a b. a -> b
coe Any
v3) (T_Value_52 -> Any
forall a b. a -> b
coe T_Value_52
v7))))))
                                       MAlonzo.Code.Algorithmic.CEK.C_'9670'_1196 T__'8866'Nf'8902'__4
v7
                                         -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                                              Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                                              ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                                                 RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                                                 (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
                                       T_State_1180
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6)))
                     T_Σ_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
      EvalMode
_ -> T_Either_6 T_ERROR_12 Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- Evaluator.Program.showUPLCResult
d_showUPLCResult_138 ::
  MAlonzo.Code.Untyped.CEK.T_State_218 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showUPLCResult_138 :: T_State_218 -> T_Either_6 T_ERROR_12 Text
d_showUPLCResult_138 T_State_218
v0
  = let v1 :: t
v1
          = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe
              Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
              ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                 RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                 (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_gasError_350)) in
    Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
      (case T_State_218 -> T_State_218
forall a b. a -> b
coe T_State_218
v0 of
         MAlonzo.Code.Untyped.CEK.C_'9633'_226 T_Value_14
v2
           -> (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_Untyped_146 -> Text) -> T_Untyped_146 -> Any
forall a b. a -> b
coe
                   T_Untyped_146 -> Text
MAlonzo.Code.Evaluator.Base.d_prettyPrintUTm_10
                   (T__'8866'_14 -> T_Untyped_146
MAlonzo.Code.Untyped.d_extricateU0_218
                      ((T_Value_14 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe T_Value_14 -> T__'8866'_14
MAlonzo.Code.Untyped.CEK.d_discharge_126 (T_Value_14 -> Any
forall a b. a -> b
coe T_Value_14
v2))))
         T_State_218
MAlonzo.Code.Untyped.CEK.C_'9670'_228
           -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                ((RuntimeError -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                   RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20
                   (RuntimeError -> Any
forall a b. a -> b
coe RuntimeError
MAlonzo.Code.Utils.C_userError_352))
         T_State_218
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v1)
-- Evaluator.Program.executeUPLCwithMP
d_executeUPLCwithMP_144 ::
  () ->
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Utils.T_List_382
       (MAlonzo.Code.Utils.T__'215'__364
          MAlonzo.Code.Agda.Builtin.String.T_String_6
          MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146)) ->
  (MAlonzo.Code.Utils.T__'215'__364
     MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
     (MAlonzo.Code.Builtin.T_Builtin_2 ->
      MAlonzo.Code.Cost.Model.T_BuiltinModel_60) ->
   MAlonzo.Code.Cost.Base.T_MachineParameters_46) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_executeUPLCwithMP_144 :: ()
-> T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (T__'215'__364
      T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
    -> T_MachineParameters_46)
-> (Any -> Text)
-> T__'8866'_14
-> T_Either_6 T_ERROR_12 Text
d_executeUPLCwithMP_144 ~()
v0 T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v1 T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
v2 Any -> Text
v3 T__'8866'_14
v4
  = T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (T__'215'__364
      T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
    -> T_MachineParameters_46)
-> (Any -> Text)
-> T__'8866'_14
-> T_Either_6 T_ERROR_12 Text
du_executeUPLCwithMP_144 T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v1 T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
v2 Any -> Text
v3 T__'8866'_14
v4
du_executeUPLCwithMP_144 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Utils.T_List_382
       (MAlonzo.Code.Utils.T__'215'__364
          MAlonzo.Code.Agda.Builtin.String.T_String_6
          MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146)) ->
  (MAlonzo.Code.Utils.T__'215'__364
     MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
     (MAlonzo.Code.Builtin.T_Builtin_2 ->
      MAlonzo.Code.Cost.Model.T_BuiltinModel_60) ->
   MAlonzo.Code.Cost.Base.T_MachineParameters_46) ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
du_executeUPLCwithMP_144 :: T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (T__'215'__364
      T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
    -> T_MachineParameters_46)
-> (Any -> Text)
-> T__'8866'_14
-> T_Either_6 T_ERROR_12 Text
du_executeUPLCwithMP_144 T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v0 T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
v1 Any -> Text
v2 T__'8866'_14
v3
  = case T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (Any, Any)
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v0 of
      MAlonzo.Code.Utils.C__'44'__378 Any
v4 Any
v5
        -> let v6 :: t
v6
                 = ((Any -> Any) -> Any -> Maybe Any -> Any) -> Any -> Any -> Any -> t
forall a b. a -> b
coe
                     (Any -> Any) -> Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_maybe_32
                     ((Any -> Any) -> Any
forall a b. a -> b
coe
                        (\ Any
v6 ->
                           (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                             (([T_Σ_14] -> DefaultFun -> T_BuiltinModel_60) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> DefaultFun -> T_BuiltinModel_60
MAlonzo.Code.Cost.Model.d_lookupModel_446 (Any -> Any
forall a b. a -> b
coe Any
v6))))
                     (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                     (([Maybe Any] -> Maybe [Any]) -> Any -> Any
forall a b. a -> b
coe
                        [Maybe Any] -> Maybe [Any]
MAlonzo.Code.Cost.Model.du_allJust_482
                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                           ((DefaultFun
 -> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
 -> Maybe T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                              DefaultFun
-> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
MAlonzo.Code.Cost.Model.d_getModel_404
                              (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_addInteger_4) (Any -> Any
forall a b. a -> b
coe Any
v5))
                           (((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                              (Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
                              ((Any -> Maybe T_Σ_14) -> Any
forall a b. a -> b
coe
                                 (\ Any
v6 -> DefaultFun
-> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
MAlonzo.Code.Cost.Model.d_getModel_404 (Any -> DefaultFun
forall a b. a -> b
coe Any
v6) (Any -> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
forall a b. a -> b
coe Any
v5)))
                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                 (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_subtractInteger_6)
                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                    (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_multiplyInteger_8)
                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                       (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_divideInteger_10)
                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                          (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_quotientInteger_12)
                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                             (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_remainderInteger_14)
                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_modInteger_16)
                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                   (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_equalsInteger_18)
                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                         DefaultFun
MAlonzo.Code.Builtin.C_lessThanInteger_20)
                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                            DefaultFun
MAlonzo.Code.Builtin.C_lessThanEqualsInteger_22)
                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                               DefaultFun
MAlonzo.Code.Builtin.C_appendByteString_24)
                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                  DefaultFun
MAlonzo.Code.Builtin.C_consByteString_26)
                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                     DefaultFun
MAlonzo.Code.Builtin.C_sliceByteString_28)
                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                        DefaultFun
MAlonzo.Code.Builtin.C_lengthOfByteString_30)
                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                           DefaultFun
MAlonzo.Code.Builtin.C_indexByteString_32)
                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                              DefaultFun
MAlonzo.Code.Builtin.C_equalsByteString_34)
                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_lessThanByteString_36)
                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_lessThanEqualsByteString_38)
                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_sha2'45'256_40)
                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_sha3'45'256_42)
                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_blake2b'45'256_44)
                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_verifyEd25519Signature_46)
                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_verifyEcdsaSecp256k1Signature_48)
                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_verifySchnorrSecp256k1Signature_50)
                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_appendString_52)
                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_equalsString_54)
                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_encodeUtf8_56)
                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_decodeUtf8_58)
                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_ifThenElse_60)
                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_chooseUnit_62)
                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_trace_64)
                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_fstPair_66)
                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_sndPair_68)
                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_chooseList_70)
                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_mkCons_72)
                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_headList_74)
                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_tailList_76)
                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_nullList_78)
                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_chooseData_80)
                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_constrData_82)
                                                                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_mapData_84)
                                                                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_listData_86)
                                                                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_iData_88)
                                                                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_bData_90)
                                                                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_unConstrData_92)
                                                                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_unMapData_94)
                                                                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_unListData_96)
                                                                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_unIData_98)
                                                                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_unBData_100)
                                                                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_equalsData_102)
                                                                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_serialiseData_104)
                                                                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_mkPairData_106)
                                                                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_mkNilData_108)
                                                                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_mkNilPairData_110)
                                                                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'add_112)
                                                                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'neg_114)
                                                                                                                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'scalarMul_116)
                                                                                                                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'equal_118)
                                                                                                                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'hashToGroup_120)
                                                                                                                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'compress_122)
                                                                                                                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G1'45'uncompress_124)
                                                                                                                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'add_126)
                                                                                                                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'neg_128)
                                                                                                                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'scalarMul_130)
                                                                                                                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'equal_132)
                                                                                                                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'hashToGroup_134)
                                                                                                                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'compress_136)
                                                                                                                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'G2'45'uncompress_138)
                                                                                                                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'millerLoop_140)
                                                                                                                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'mulMlResult_142)
                                                                                                                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_bls12'45'381'45'finalVerify_144)
                                                                                                                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_keccak'45'256_146)
                                                                                                                                                                                                                                                   ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                      (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                         DefaultFun
MAlonzo.Code.Builtin.C_blake2b'45'224_148)
                                                                                                                                                                                                                                                      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                         (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                            DefaultFun
MAlonzo.Code.Builtin.C_byteStringToInteger_150)
                                                                                                                                                                                                                                                         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                            (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                               DefaultFun
MAlonzo.Code.Builtin.C_integerToByteString_152)
                                                                                                                                                                                                                                                            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                               (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                  DefaultFun
MAlonzo.Code.Builtin.C_andByteString_154)
                                                                                                                                                                                                                                                               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                  (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                     DefaultFun
MAlonzo.Code.Builtin.C_orByteString_156)
                                                                                                                                                                                                                                                                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                     (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                        DefaultFun
MAlonzo.Code.Builtin.C_xorByteString_158)
                                                                                                                                                                                                                                                                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                        (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                           DefaultFun
MAlonzo.Code.Builtin.C_complementByteString_160)
                                                                                                                                                                                                                                                                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                           (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                              DefaultFun
MAlonzo.Code.Builtin.C_readBit_162)
                                                                                                                                                                                                                                                                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                              (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                 DefaultFun
MAlonzo.Code.Builtin.C_writeBits_164)
                                                                                                                                                                                                                                                                              ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                 Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                 (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                    DefaultFun
MAlonzo.Code.Builtin.C_replicateByte_166)
                                                                                                                                                                                                                                                                                 ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                    Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                    (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                       DefaultFun
MAlonzo.Code.Builtin.C_shiftByteString_168)
                                                                                                                                                                                                                                                                                    ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                       Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                       (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                          DefaultFun
MAlonzo.Code.Builtin.C_rotateByteString_170)
                                                                                                                                                                                                                                                                                       ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                          Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                          (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                             DefaultFun
MAlonzo.Code.Builtin.C_countSetBits_172)
                                                                                                                                                                                                                                                                                          ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                             Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                             (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                DefaultFun
MAlonzo.Code.Builtin.C_findFirstSetBit_174)
                                                                                                                                                                                                                                                                                             ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                                (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                   DefaultFun
MAlonzo.Code.Builtin.C_ripemd'45'160_176)
                                                                                                                                                                                                                                                                                                ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                   Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                                                                                                                                                                                                                                                                                                   (DefaultFun -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                      DefaultFun
MAlonzo.Code.Builtin.C_expModInteger_178)
                                                                                                                                                                                                                                                                                                   ([Any] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                                                                                      [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
           Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             (case Any -> Maybe Any
forall a b. a -> b
coe Any
forall {t}. t
v6 of
                MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v7
                  -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                       (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                          (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                          ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                          ((T_Writer_304 -> Any) -> Any -> Any
forall a b. a -> b
coe
                             T_Writer_304 -> Any
MAlonzo.Code.Utils.d_wrvalue_314
                             ((T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
                                ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
v1 ((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
v4) (Any -> Any
forall a b. a -> b
coe Any
v7)))
                                (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                   T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                                   (T_Stack_6 -> Any
forall a b. a -> b
coe T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                                   (T_Env_16 -> Any
forall a b. a -> b
coe T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18) T__'8866'_14
v3))))
                       ((Any -> Any) -> Any
forall a b. a -> b
coe
                          (\ Any
v8 ->
                             (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                               T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
                               ((T_State_218 -> T_Either_6 T_ERROR_12 Text) -> Any -> Any
forall a b. a -> b
coe T_State_218 -> T_Either_6 T_ERROR_12 Text
d_showUPLCResult_138 (Any -> Any
forall a b. a -> b
coe Any
v8))
                               ((Any -> Any) -> Any
forall a b. a -> b
coe
                                  (\ Any
v9 ->
                                     (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
                                       ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                                          Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Any
v9
                                          ((Any -> Text) -> Any -> Any
forall a b. a -> b
coe
                                             Any -> Text
v2
                                             (T_Writer_304 -> Any
MAlonzo.Code.Utils.d_accum_316
                                                ((T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304)
-> Any -> Any -> Any -> T_Writer_304
forall a b. a -> b
coe
                                                   T_MachineParameters_46 -> Integer -> T_State_218 -> T_Writer_304
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
                                                   ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
                                                      T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
v1
                                                      ((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
v4)
                                                         (Any -> Any
forall a b. a -> b
coe Any
v7)))
                                                   (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                                                   ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                      T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                                                      (T_Stack_6 -> Any
forall a b. a -> b
coe T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                                                      (T_Env_16 -> Any
forall a b. a -> b
coe T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18)
                                                      T__'8866'_14
v3)))))))))
                Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                  -> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                       Any -> T_Either_6 Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                       ((Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                          Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_jsonError_22
                          (Text -> Any
forall a b. a -> b
coe (Text
"while processing parameters." :: Data.Text.Text)))
                Maybe Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
      (Any, Any)
_ -> T_Either_6 T_ERROR_12 Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- Evaluator.Program.executeUPLC
d_executeUPLC_192 ::
  T_BudgetMode_36
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
       (MAlonzo.Code.Utils.T_List_382
          (MAlonzo.Code.Utils.T__'215'__364
             MAlonzo.Code.Agda.Builtin.String.T_String_6
             MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146))) ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_executeUPLC_192 :: T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
-> T__'8866'_14 -> T_Either_6 T_ERROR_12 Text
d_executeUPLC_192 T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
v0 T__'8866'_14
v1
  = case T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
-> BudgetMode Any
forall a b. a -> b
coe T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
v0 of
      BudgetMode Any
C_Silent_40
        -> (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
             (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                ((RuntimeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe RuntimeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
                ((Integer -> T_State_218 -> T_Either_6 RuntimeError T_State_218)
-> Any -> Any -> Any
forall a b. a -> b
coe
                   Integer -> T_State_218 -> T_Either_6 RuntimeError T_State_218
MAlonzo.Code.Untyped.CEK.d_stepper_1234
                   (Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
                   ((T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218)
-> Any -> Any -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                      T_Stack_6 -> T_Env_16 -> T__'8866'_14 -> T_State_218
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
                      (T_Stack_6 -> Any
forall a b. a -> b
coe T_Stack_6
MAlonzo.Code.Untyped.CEK.C_ε_10)
                      (T_Env_16 -> Any
forall a b. a -> b
coe T_Env_16
MAlonzo.Code.Untyped.CEK.C_'91''93'_18) T__'8866'_14
v1)))
             ((T_State_218 -> T_Either_6 T_ERROR_12 Text) -> Any
forall a b. a -> b
coe T_State_218 -> T_Either_6 T_ERROR_12 Text
d_showUPLCResult_138)
      C_Counting_42 Any
v2
        -> (T__'215'__364
   T_HCekMachineCosts_4
   (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
 -> (T__'215'__364
       T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
     -> T_MachineParameters_46)
 -> (Any -> Text)
 -> T__'8866'_14
 -> T_Either_6 T_ERROR_12 Text)
-> Any -> Any -> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (T__'215'__364
      T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
    -> T_MachineParameters_46)
-> (Any -> Text)
-> T__'8866'_14
-> T_Either_6 T_ERROR_12 Text
du_executeUPLCwithMP_144 (Any -> Any
forall a b. a -> b
coe Any
v2)
             ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140)
             ((T_ExBudget_52 -> Text) -> Any
forall a b. a -> b
coe T_ExBudget_52 -> Text
MAlonzo.Code.Cost.d_countingReport_144) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)
      C_Tallying_44 Any
v2
        -> (T__'215'__364
   T_HCekMachineCosts_4
   (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
 -> (T__'215'__364
       T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
     -> T_MachineParameters_46)
 -> (Any -> Text)
 -> T__'8866'_14
 -> T_Either_6 T_ERROR_12 Text)
-> Any -> Any -> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
             T__'215'__364
  T_HCekMachineCosts_4
  (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (T__'215'__364
      T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
    -> T_MachineParameters_46)
-> (Any -> Text)
-> T__'8866'_14
-> T_Either_6 T_ERROR_12 Text
du_executeUPLCwithMP_144 (Any -> Any
forall a b. a -> b
coe Any
v2)
             ((T__'215'__364
   T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
 -> T_MachineParameters_46)
-> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_tallyingMachineParameters_220)
             ((T__'215'__364 T_Tree_254 T_ExBudget_52 -> Text) -> Any
forall a b. a -> b
coe T__'215'__364 T_Tree_254 T_ExBudget_52 -> Text
MAlonzo.Code.Cost.d_tallyingReport_224) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)
      BudgetMode Any
_ -> T_Either_6 T_ERROR_12 Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
-- Evaluator.Program.evalProgramNU
d_evalProgramNU_204 ::
  T_BudgetMode_36
    (MAlonzo.Code.Utils.T__'215'__364
       MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
       (MAlonzo.Code.Utils.T_List_382
          (MAlonzo.Code.Utils.T__'215'__364
             MAlonzo.Code.Agda.Builtin.String.T_String_6
             MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146))) ->
  T_ProgramNU_26 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_evalProgramNU_204 :: T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
-> T_ProgramNU_26 -> T_Either_6 T_ERROR_12 Text
d_evalProgramNU_204 T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
v0 T_ProgramNU_26
v1
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42 ((T_ProgramNU_26 -> T_Either_6 T_ERROR_12 T__'8866'_14)
-> Any -> Any
forall a b. a -> b
coe T_ProgramNU_26 -> T_Either_6 T_ERROR_12 T__'8866'_14
d_parseUPLC_62 (T_ProgramNU_26 -> Any
forall a b. a -> b
coe T_ProgramNU_26
v1))
      ((T_BudgetMode_36
   (T__'215'__364
      T_HCekMachineCosts_4
      (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
 -> T__'8866'_14 -> T_Either_6 T_ERROR_12 Text)
-> Any -> Any
forall a b. a -> b
coe T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
-> T__'8866'_14 -> T_Either_6 T_ERROR_12 Text
d_executeUPLC_192 (T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
-> Any
forall a b. a -> b
coe T_BudgetMode_36
  (T__'215'__364
     T_HCekMachineCosts_4
     (T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)))
v0))
-- Evaluator.Program.evalProgramN
d_evalProgramN_212 ::
  T_EvalMode_46 ->
  T_ProgramN_18 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_evalProgramN_212 :: EvalMode -> T_ProgramN_18 -> T_Either_6 T_ERROR_12 Text
d_evalProgramN_212 EvalMode
v0 T_ProgramN_18
v1
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42 ((T_ProgramN_18 -> T_Either_6 T_ERROR_12 T_ScopedTm_522)
-> Any -> Any
forall a b. a -> b
coe T_ProgramN_18 -> T_Either_6 T_ERROR_12 T_ScopedTm_522
d_parsePLC_56 (T_ProgramN_18 -> Any
forall a b. a -> b
coe T_ProgramN_18
v1))
      ((EvalMode -> T_ScopedTm_522 -> T_Either_6 T_ERROR_12 Text)
-> Any -> Any
forall a b. a -> b
coe EvalMode -> T_ScopedTm_522 -> T_Either_6 T_ERROR_12 Text
d_executePLC_80 (EvalMode -> Any
forall a b. a -> b
coe EvalMode
v0))
-- Evaluator.Program.typeCheckProgramN
d_typeCheckProgramN_220 ::
  T_ProgramN_18 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Evaluator.Base.T_ERROR_12
    MAlonzo.Code.Agda.Builtin.String.T_String_6
d_typeCheckProgramN_220 :: T_ProgramN_18 -> T_Either_6 T_ERROR_12 Text
d_typeCheckProgramN_220 T_ProgramN_18
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_ERROR_12 Text
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42 ((T_ProgramN_18 -> T_Either_6 T_ERROR_12 T_ScopedTm_522)
-> Any -> Any
forall a b. a -> b
coe T_ProgramN_18 -> T_Either_6 T_ERROR_12 T_ScopedTm_522
d_parsePLC_56 (T_ProgramN_18 -> Any
forall a b. a -> b
coe T_ProgramN_18
v0))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_42
              (((Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
                 (Any -> Any) -> T_Either_6 Any Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_withE_282
                 ((Any -> Any) -> Any
forall a b. a -> b
coe
                    (\ Any
v2 ->
                       (Text -> T_ERROR_12) -> Any -> Any
forall a b. a -> b
coe
                         Text -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_typeError_14
                         ((T_TypeError_12 -> Text) -> Any -> Any
forall a b. a -> b
coe T_TypeError_12 -> Text
MAlonzo.Code.Evaluator.Base.d_uglyTypeError_24 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                 ((T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14) -> Any -> Any
forall a b. a -> b
coe T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14
d_typeCheckPLC_70 (Any -> Any
forall a b. a -> b
coe Any
v1)))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v3 Any
v4
                        -> (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_RawTy_2 -> Text) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
                                T_RawTy_2 -> Text
MAlonzo.Code.Evaluator.Base.d_prettyPrintTy_8
                                (Integer -> T_Weirdℕ_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_unshifterTy_360
                                   (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (T_Weirdℕ_42 -> T_Weirdℕ_42
forall a b. a -> b
coe T_Weirdℕ_42
MAlonzo.Code.Scoped.C_Z_44)
                                   ((Integer -> T_ScopedTy_14 -> T_RawTy_2) -> Any -> Any -> T_RawTy_2
forall a b. a -> b
coe
                                      Integer -> T_ScopedTy_14 -> T_RawTy_2
MAlonzo.Code.Scoped.d_extricateScopeTy_780
                                      ((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Scoped.Extrication.d_len'8902'_4
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
                                      ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                         T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
MAlonzo.Code.Scoped.Extrication.d_extricateNf'8902'_26
                                         (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
                                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (Any -> Any
forall a b. a -> b
coe Any
v3)))))
                      T_Σ_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))))