{-# 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.Term where
import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Bool qualified
import MAlonzo.Code.Agda.Builtin.List qualified
import MAlonzo.Code.Agda.Builtin.Maybe qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Builtin.String qualified
import MAlonzo.Code.Agda.Builtin.Unit qualified
import MAlonzo.Code.Algorithmic qualified
import MAlonzo.Code.Algorithmic.CEK qualified
import MAlonzo.Code.Algorithmic.CK qualified
import MAlonzo.Code.Algorithmic.Evaluation qualified
import MAlonzo.Code.Builtin qualified
import MAlonzo.Code.Check qualified
import MAlonzo.Code.Cost qualified
import MAlonzo.Code.Cost.Model qualified
import MAlonzo.Code.Cost.Raw qualified
import MAlonzo.Code.Data.List.Base qualified
import MAlonzo.Code.Data.Maybe.Base qualified
import MAlonzo.Code.Data.String.Base qualified
import MAlonzo.Code.Evaluator.Base qualified
import MAlonzo.Code.Raw qualified
import MAlonzo.Code.RawU qualified
import MAlonzo.Code.Scoped qualified
import MAlonzo.Code.Scoped.Extrication qualified
import MAlonzo.Code.Type qualified
import MAlonzo.Code.Untyped qualified
import MAlonzo.Code.Untyped.CEK qualified
import MAlonzo.Code.Untyped.CEKWithCost qualified
import MAlonzo.Code.Utils qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
word64ToNat)
import MAlonzo.RTE qualified
import Control.Monad.Trans.Except
import Data.Bifunctor
import Data.Either
import Data.Functor
import FFI.Untyped qualified as U
import PlutusCore
import PlutusCore.DeBruijn
import Raw
import UntypedPlutusCore qualified as U
import UntypedPlutusCore.Parser qualified as U
type T_Term_14 =
PlutusCore.Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
d_Term_14 :: a
d_Term_14
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.Term"
type T_Type_16 = PlutusCore.Type NamedTyDeBruijn DefaultUni ()
d_Type_16 :: a
d_Type_16
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.Type"
type T_TermN_18 =
PlutusCore.Term TyName Name DefaultUni DefaultFun PlutusCore.SrcSpan
d_TermN_18 :: a
d_TermN_18
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TermN"
type T_TypeN_20 =
PlutusCore.Type TyName DefaultUni PlutusCore.SrcSpan
d_TypeN_20 :: a
d_TypeN_20
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TypeN"
type T_TermNU_22 =
U.Term Name DefaultUni DefaultFun PlutusCore.SrcSpan
d_TermNU_22 :: a
d_TermNU_22
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TermNU"
type T_TermU_24 = U.Term NamedDeBruijn DefaultUni DefaultFun ()
d_TermU_24 :: a
d_TermU_24
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Term.TermU"
d_parseTm_26 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ParseError_4 T_TermN_18
d_parseTm_26 :: Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 = QuoteT (Either T_ParseError_4) T_TermN_18
-> T_Either_6 T_ParseError_4 T_TermN_18
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT (Either T_ParseError_4) T_TermN_18
-> T_Either_6 T_ParseError_4 T_TermN_18)
-> (Text -> QuoteT (Either T_ParseError_4) T_TermN_18)
-> Text
-> T_Either_6 T_ParseError_4 T_TermN_18
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> QuoteT (Either T_ParseError_4) T_TermN_18
forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m T_TermN_18
parseTerm
d_parseTmU_28 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ParseError_4 T_TermNU_22
d_parseTmU_28 :: Text -> T_Either_6 T_ParseError_4 T_TermNU_22
d_parseTmU_28 = QuoteT (Either T_ParseError_4) T_TermNU_22
-> T_Either_6 T_ParseError_4 T_TermNU_22
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT (Either T_ParseError_4) T_TermNU_22
-> T_Either_6 T_ParseError_4 T_TermNU_22)
-> (Text -> QuoteT (Either T_ParseError_4) T_TermNU_22)
-> Text
-> T_Either_6 T_ParseError_4 T_TermNU_22
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> QuoteT (Either T_ParseError_4) T_TermNU_22
forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m T_TermNU_22
U.parseTerm
d_parseTy_30 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ParseError_4 T_TypeN_20
d_parseTy_30 :: Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 = QuoteT (Either T_ParseError_4) T_TypeN_20
-> T_Either_6 T_ParseError_4 T_TypeN_20
forall (m :: * -> *) a. Monad m => QuoteT m a -> m a
runQuoteT (QuoteT (Either T_ParseError_4) T_TypeN_20
-> T_Either_6 T_ParseError_4 T_TypeN_20)
-> (Text -> QuoteT (Either T_ParseError_4) T_TypeN_20)
-> Text
-> T_Either_6 T_ParseError_4 T_TypeN_20
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> QuoteT (Either T_ParseError_4) T_TypeN_20
forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m T_TypeN_20
parseType
d_deBruijnifyTm_32 ::
T_TermN_18 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Scoped.T_FreeVariableError_574 T_Term_14
d_deBruijnifyTm_32 :: T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 = (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_Term_14)
-> Either
FreeVariableError
(Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_Term_14
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 Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan
-> T_Term_14
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either
FreeVariableError
(Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_Term_14)
-> (T_TermN_18
-> Either
FreeVariableError
(Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermN_18
-> T_Either_6 FreeVariableError T_Term_14
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)
-> Either
FreeVariableError
(Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> (T_TermN_18
-> Except
FreeVariableError
(Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermN_18
-> Either
FreeVariableError
(Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_TermN_18
-> 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
d_deBruijnifyTy_34 ::
T_TypeN_20 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Scoped.T_FreeVariableError_574 T_Type_16
d_deBruijnifyTy_34 :: T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 = (Type NamedTyDeBruijn DefaultUni SrcSpan -> T_Type_16)
-> Either
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
-> T_Either_6 FreeVariableError T_Type_16
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 Type NamedTyDeBruijn DefaultUni SrcSpan -> T_Type_16
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
-> T_Either_6 FreeVariableError T_Type_16)
-> (T_TypeN_20
-> Either
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan))
-> T_TypeN_20
-> T_Either_6 FreeVariableError T_Type_16
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Except FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
-> Either
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
forall e a. Except e a -> Either e a
runExcept (Except FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
-> Either
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan))
-> (T_TypeN_20
-> Except
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan))
-> T_TypeN_20
-> Either
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_TypeN_20
-> Except
FreeVariableError (Type NamedTyDeBruijn DefaultUni SrcSpan)
forall e (m :: * -> *) (uni :: * -> *) ann.
(AsFreeVariableError e, MonadError e m) =>
Type TyName uni ann -> m (Type NamedTyDeBruijn uni ann)
deBruijnTy
d_deBruijnifyTmU_36 ::
T_TermNU_22 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Scoped.T_FreeVariableError_574 T_TermU_24
d_deBruijnifyTmU_36 :: T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24
d_deBruijnifyTmU_36 = (Term NamedDeBruijn DefaultUni DefaultFun SrcSpan -> T_TermU_24)
-> Either
FreeVariableError
(Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_TermU_24
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 Term NamedDeBruijn DefaultUni DefaultFun SrcSpan -> T_TermU_24
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Either
FreeVariableError
(Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
-> T_Either_6 FreeVariableError T_TermU_24)
-> (T_TermNU_22
-> Either
FreeVariableError
(Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermNU_22
-> T_Either_6 FreeVariableError T_TermU_24
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)
-> Either
FreeVariableError
(Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> (T_TermNU_22
-> Except
FreeVariableError
(Term NamedDeBruijn DefaultUni DefaultFun SrcSpan))
-> T_TermNU_22
-> Either
FreeVariableError
(Term NamedDeBruijn DefaultUni DefaultFun SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_TermNU_22
-> 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
d_convTm_38 :: T_Term_14 -> MAlonzo.Code.Raw.T_RawTm_30
d_convTm_38 :: T_Term_14 -> T_RawTm_30
d_convTm_38 = T_Term_14 -> T_RawTm_30
forall a.
Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun a
-> T_RawTm_30
conv
d_unconvTm_40 :: MAlonzo.Code.Raw.T_RawTm_30 -> T_Term_14
d_unconvTm_40 :: T_RawTm_30 -> T_Term_14
d_unconvTm_40 = Int -> T_RawTm_30 -> T_Term_14
unconv Int
0
d_convTy_42 :: T_Type_16 -> MAlonzo.Code.Raw.T_RawTy_2
d_convTy_42 :: T_Type_16 -> T_RawTy_2
d_convTy_42 = T_Type_16 -> T_RawTy_2
forall a. Type NamedTyDeBruijn DefaultUni a -> T_RawTy_2
convT
d_unconvTy_44 :: MAlonzo.Code.Raw.T_RawTy_2 -> T_Type_16
d_unconvTy_44 :: T_RawTy_2 -> T_Type_16
d_unconvTy_44 = Int -> T_RawTy_2 -> T_Type_16
unconvT Int
0
d_convTmU_46 :: T_TermU_24 -> MAlonzo.Code.RawU.T_Untyped_146
d_convTmU_46 :: T_TermU_24 -> T_Untyped_146
d_convTmU_46 = T_TermU_24 -> T_Untyped_146
forall a.
Term NamedDeBruijn DefaultUni DefaultFun a -> T_Untyped_146
U.conv
d_unconvTmU_48 :: MAlonzo.Code.RawU.T_Untyped_146 -> T_TermU_24
d_unconvTmU_48 :: T_Untyped_146 -> T_TermU_24
d_unconvTmU_48 = Int -> T_Untyped_146 -> T_TermU_24
U.uconv Int
0
checkKindAgda ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Kind_636 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
checkKindAgda :: T_Type_16 -> T_Kind_636 -> T_Either_6 T_ERROR_12 ()
checkKindAgda = (T_Type_16 -> T_Kind_636 -> T_Either_6 T_ERROR_12 ())
-> T_Type_16 -> T_Kind_636 -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe T_Type_16 -> T_Kind_636 -> T_Either_6 T_ERROR_12 ()
d_checkKindX_50
d_checkKindX_50 ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Kind_636 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_checkKindX_50 :: T_Type_16 -> T_Kind_636 -> T_Either_6 T_ERROR_12 ()
d_checkKindX_50 T_Type_16
v0 T_Kind_636
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 ()
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
((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
((Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (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_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
v0))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(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
v3 ->
(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
v3))))
((T_Ctx'8902'_2
-> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferKind_562
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v2)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
case Any -> T_Σ_14
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v4 Any
v5
-> (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
v6 ->
(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
((T_Kind_636 -> T_Kind_636 -> T_TypeError_12)
-> T_Kind_636 -> Any -> Any
forall a b. a -> b
coe T_Kind_636 -> T_Kind_636 -> T_TypeError_12
MAlonzo.Code.Check.C_kindMismatch_18 T_Kind_636
v1 Any
v4))))
((T_Dec_20 -> T_Either_6 (Any -> T_Irrelevant_20) Any) -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> T_Either_6 (Any -> T_Irrelevant_20) Any
MAlonzo.Code.Utils.du_dec2Either_294
((T_Kind_636 -> T_Kind_636 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_636 -> T_Kind_636 -> T_Dec_20
MAlonzo.Code.Check.d_decKind_138 (T_Kind_636 -> Any
forall a b. a -> b
coe T_Kind_636
v1) (Any -> Any
forall a b. a -> b
coe Any
v4))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v6 ->
(Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
(() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
inferKindAgda ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Utils.T_Kind_636
inferKindAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_636
inferKindAgda = (T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_636)
-> T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_636
forall a b. a -> b
coe T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_636
d_inferKind'8709'_68
d_inferKind'8709'_68 ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Utils.T_Kind_636
d_inferKind'8709'_68 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_636
d_inferKind'8709'_68 T_Type_16
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_Kind_636
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
((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
((Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (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_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
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_Ctx'8902'_2
-> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferKind_562
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (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 (Any -> Any
forall a b. a -> b
coe Any
v3)
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
normalizeTypeAgda ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
normalizeTypeAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
normalizeTypeAgda = (T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16)
-> T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
forall a b. a -> b
coe T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
d_normalizeType_80
d_normalizeType_80 ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
d_normalizeType_80 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Type_16
d_normalizeType_80 T_Type_16
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_Type_16
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
((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
((Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (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_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
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_Ctx'8902'_2
-> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> T_ScopedTy_14 -> T_Either_6 T_TypeError_12 T_Σ_14
MAlonzo.Code.Check.d_inferKind_562
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (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 -> T_Type_16) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
T_RawTy_2 -> T_Type_16
d_unconvTy_44
(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_636 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_636 -> 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) (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v4)))))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
inferTypeAgda ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
inferTypeAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
inferTypeAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
d_inferType'8709'_92
d_inferType'8709'_92 ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Type_16
d_inferType'8709'_92 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Type_16
d_inferType'8709'_92 T_Term_14
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_Type_16
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
((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_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
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_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
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) (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 -> T_Type_16) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
T_RawTy_2 -> T_Type_16
d_unconvTy_44
(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_636 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_636 -> 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_636 -> Any
forall a b. a -> b
coe T_Kind_636
MAlonzo.Code.Utils.C_'42'_638) (Any -> Any
forall a b. a -> b
coe Any
v3)))))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
checkTypeAgda ::
T_Type_16 ->
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
checkTypeAgda :: T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
checkTypeAgda = (T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ())
-> T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
d_checkType'8709'_104
d_checkType'8709'_104 ::
T_Type_16 ->
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_checkType'8709'_104 :: T_Type_16 -> T_Term_14 -> T_Either_6 T_ERROR_12 ()
d_checkType'8709'_104 T_Type_16
v0 T_Term_14
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 ()
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
((ScopeError -> T_ERROR_12) -> Any
forall a b. a -> b
coe ScopeError -> T_ERROR_12
MAlonzo.Code.Evaluator.Base.C_scopeError_18)
((Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_RawTy_2 -> T_Either_6 ScopeError T_ScopedTy_14
MAlonzo.Code.Scoped.d_scopeCheckTy_616
((T_Ctx'8902'_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2 -> Integer
MAlonzo.Code.Check.d_len'8902'_106
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4))
((Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Weirdâ„•_42 -> T_RawTy_2 -> T_RawTy_2
MAlonzo.Code.Scoped.d_shifterTy_194 (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_Type_16 -> T_RawTy_2) -> T_Type_16 -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 T_Type_16
v0))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(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
v3 ->
(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
v3))))
((T_Ctx'8902'_2
-> T_ScopedTy_14
-> T_Kind_636
-> T_Either_6 T_TypeError_12 T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_ScopedTy_14
-> T_Kind_636
-> T_Either_6 T_TypeError_12 T__'8866'Nf'8902'__4
MAlonzo.Code.Check.d_checkKind_554
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v2)
(T_Kind_636 -> Any
forall a b. a -> b
coe T_Kind_636
MAlonzo.Code.Utils.C_'42'_638)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(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
((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_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
v1))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 ->
(T_Monad_186 -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Monad_186 -> Any -> Any -> Any
MAlonzo.Code.Utils.du__'62''62'__214
(T_Monad_186 -> Any
forall a b. a -> b
coe T_Monad_186
MAlonzo.Code.Utils.du_EitherP_274)
(((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
v5 ->
(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
v5))))
((T_Ctx'8902'_2
-> T_Ctx_2
-> T_ScopedTm_522
-> T__'8866'Nf'8902'__4
-> T_Either_6 T_TypeError_12 T__'8866'__168)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Ctx_2
-> T_ScopedTm_522
-> T__'8866'Nf'8902'__4
-> T_Either_6 T_TypeError_12 T__'8866'__168
MAlonzo.Code.Check.d_checkType_1148
(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
v4) (Any -> Any
forall a b. a -> b
coe Any
v3)))
((Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
(() -> Any
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))))))
normalizeTypeTermAgda ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
normalizeTypeTermAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
normalizeTypeTermAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_normalizeTypeTerm_120
d_normalizeTypeTerm_120 ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_normalizeTypeTerm_120 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_normalizeTypeTerm_120 T_Term_14
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_Term_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
((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_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
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_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
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) (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_RawTm_30 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_Term_14
d_unconvTm_40
(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
v4)))))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
runTLAgda ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
runTLAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
runTLAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTL_132
d_runTL_132 ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_runTL_132 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTL_132 T_Term_14
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_Term_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
((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_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
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_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
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) (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
-> (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)))
((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 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_Term_14
d_unconvTm_40
(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 a. a
MAlonzo.RTE.mazUnreachableError))))
runTCKAgda ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
runTCKAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
runTCKAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCK_146
d_runTCK_146 ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_runTCK_146 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCK_146 T_Term_14
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_Term_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
((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_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
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_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
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) (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
-> (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 ->
case Any -> T_State_34
forall a b. a -> b
coe Any
v5 of
MAlonzo.Code.Algorithmic.CK.C__'9659'__40 T__'8866'Nf'8902'__4
v6 T_Stack_18
v7 T__'8866'__168
v8
-> (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_gasError_350))
MAlonzo.Code.Algorithmic.CK.C__'9669'__46 T__'8866'Nf'8902'__4
v6 T_Stack_18
v7 T__'8866'__168
v8 T_Value_28
v9
-> (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_gasError_350))
MAlonzo.Code.Algorithmic.CK.C_'9633'_50 T__'8866'__168
v6 T_Value_28
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 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_Term_14
d_unconvTm_40
(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
v6)))))
MAlonzo.Code.Algorithmic.CK.C_'9670'_54 T__'8866'Nf'8902'__4
v6
-> (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 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_Term_14
d_unconvTm_40
(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
(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_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
MAlonzo.Code.Algorithmic.C_error_258)))))
T_State_34
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
runTCEKAgda ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
runTCEKAgda :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
runTCEKAgda = (T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14)
-> T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
forall a b. a -> b
coe T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCEK_166
d_runTCEK_166 ::
T_Term_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_Term_14
d_runTCEK_166 :: T_Term_14 -> T_Either_6 T_ERROR_12 T_Term_14
d_runTCEK_166 T_Term_14
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_Term_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
((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_Term_14 -> T_RawTm_30) -> T_Term_14 -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 T_Term_14
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_Ctx'8902'_2
-> T_Ctx_2 -> T_ScopedTm_522 -> T_Either_6 T_TypeError_12 T_Σ_14)
-> Any -> Any -> Any -> Any
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) (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
-> (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_1186 -> T_Either_6 RuntimeError T_State_1186)
-> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_State_1186 -> T_Either_6 RuntimeError T_State_1186
MAlonzo.Code.Algorithmic.CEK.du_stepper_1538
(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_1172
-> T_Env_26
-> T__'8866'__168
-> T_State_1186)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Stack_1172
-> T_Env_26
-> T__'8866'__168
-> T_State_1186
MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1194
(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_1172 -> Any
forall a b. a -> b
coe T_Stack_1172
MAlonzo.Code.Algorithmic.CEK.C_ε_1176)
(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 ->
case Any -> T_State_1186
forall a b. a -> b
coe Any
v5 of
MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1194 T_Ctx_2
v6 T__'8866'Nf'8902'__4
v7 T_Stack_1172
v8 T_Env_26
v9 T__'8866'__168
v10
-> (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_gasError_350))
MAlonzo.Code.Algorithmic.CEK.C__'9669'__1198 T__'8866'Nf'8902'__4
v6 T_Stack_1172
v7 T_Value_52
v8
-> (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_gasError_350))
MAlonzo.Code.Algorithmic.CEK.C_'9633'_1200 T_Value_52
v6
-> (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 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_Term_14
d_unconvTm_40
(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
v6))))))
MAlonzo.Code.Algorithmic.CEK.C_'9670'_1202 T__'8866'Nf'8902'__4
v6
-> (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 -> T_Term_14) -> T_RawTm_30 -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_Term_14
d_unconvTm_40
(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
(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_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
MAlonzo.Code.Algorithmic.C_error_258)))))
T_State_1186
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))))
d_runUValue_186 ::
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
MAlonzo.Code.Untyped.CEK.T_Value_14
d_runUValue_186 :: T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14
d_runUValue_186 T__'8866'_14
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_Value_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
((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_1242
(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
v0)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 ->
let v2 :: t
v2
= (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
v1 of
MAlonzo.Code.Untyped.CEK.C_'9633'_226 T_Value_14
v3
-> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (T_Value_14 -> Any
forall a b. a -> b
coe T_Value_14
v3)
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 a. a
v2)))
runUAgda ::
T_TermU_24 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_TermU_24
runUAgda :: T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
runUAgda = (T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24)
-> T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
forall a b. a -> b
coe T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
d_runU_194
d_runU_194 ::
T_TermU_24 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12 T_TermU_24
d_runU_194 :: T_TermU_24 -> T_Either_6 T_ERROR_12 T_TermU_24
d_runU_194 T_TermU_24
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_TermU_24
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
((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_TermU_24 -> T_Untyped_146) -> T_TermU_24 -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 T_TermU_24
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 ((T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Either_6 T_ERROR_12 T_Value_14
d_runUValue_186 (Any -> Any
forall a b. a -> b
coe Any
v1))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
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 -> T_TermU_24) -> T_Untyped_146 -> Any
forall a b. a -> b
coe
T_Untyped_146 -> T_TermU_24
d_unconvTmU_48
(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 (Any -> Any
forall a b. a -> b
coe Any
v2))))))))
runUCountingAgda ::
MAlonzo.Code.Utils.T__'215'__366
MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
(MAlonzo.Code.Utils.T_List_384
(MAlonzo.Code.Utils.T__'215'__366
MAlonzo.Code.Agda.Builtin.String.T_String_6
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_164)) ->
T_TermU_24 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
(MAlonzo.Code.Utils.T__'215'__366
T_TermU_24 (MAlonzo.Code.Utils.T__'215'__366 Integer Integer))
runUCountingAgda :: T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer))
runUCountingAgda = (T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer)))
-> T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer))
forall a b. a -> b
coe T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer))
d_runUCounting_202
d_runUCounting_202 ::
MAlonzo.Code.Utils.T__'215'__366
MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
(MAlonzo.Code.Utils.T_List_384
(MAlonzo.Code.Utils.T__'215'__366
MAlonzo.Code.Agda.Builtin.String.T_String_6
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_164)) ->
T_TermU_24 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
(MAlonzo.Code.Utils.T__'215'__366
T_TermU_24 (MAlonzo.Code.Utils.T__'215'__366 Integer Integer))
d_runUCounting_202 :: T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer))
d_runUCounting_202 T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
v0 T_TermU_24
v1
= case T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
-> (Any, Any)
forall a b. a -> b
coe T__'215'__366
T_HCekMachineCosts_4
(T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164))
v0 of
MAlonzo.Code.Utils.C__'44'__380 Any
v2 Any
v3
-> let v4 :: Any
v4
= ((Any -> Any) -> Any -> Maybe Any -> Any)
-> Any -> Any -> Any -> Any
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
v4 ->
(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_62) -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> DefaultFun -> T_BuiltinModel_62
MAlonzo.Code.Cost.Model.d_lookupModel_474 (Any -> Any
forall a b. a -> b
coe Any
v4))))
(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_510
((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_384 (T__'215'__366 Text T_CpuAndMemoryModel_164)
-> Maybe T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
DefaultFun
-> T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164)
-> Maybe T_Σ_14
MAlonzo.Code.Cost.Model.d_getModel_432
(DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
MAlonzo.Code.Builtin.C_addInteger_4) (Any -> Any
forall a b. a -> b
coe Any
v3))
(((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
v4 -> DefaultFun
-> T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164)
-> Maybe T_Σ_14
MAlonzo.Code.Cost.Model.d_getModel_432 (Any -> DefaultFun
forall a b. a -> b
coe Any
v4) (Any -> T_List_384 (T__'215'__366 Text T_CpuAndMemoryModel_164)
forall a b. a -> b
coe Any
v3)))
((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] -> [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_dropList_180)
([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
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer))
forall a b. a -> b
coe
(case Any -> Maybe Any
forall a b. a -> b
coe Any
v4 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v5
-> (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
((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_TermU_24 -> T_Untyped_146) -> T_TermU_24 -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 T_TermU_24
v1)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v6 ->
(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'__366
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_62)
-> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
T__'215'__366
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_62)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140
((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'__380 (Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v5)))
(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 -> Any -> 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) Any
v6))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v7 ->
let v8 :: t
v8
= (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
v7 of
MAlonzo.Code.Untyped.CEK.C_'9633'_226 T_Value_14
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
((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'__380
((T_Untyped_146 -> T_TermU_24) -> T_Untyped_146 -> Any
forall a b. a -> b
coe
T_Untyped_146 -> T_TermU_24
d_unconvTmU_48
(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
v9))))
((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'__380
((T_ExBudget_52 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_ExBudget_52 -> Integer
MAlonzo.Code.Cost.d_ExCPU_58
((T_Writer_304 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Writer_304 -> Any
MAlonzo.Code.Utils.d_accum_316
((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'__366
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_62)
-> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
T__'215'__366
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_62)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140
((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'__380
(Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v5)))
(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 -> Any -> 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)
Any
v6))))
((T_ExBudget_52 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_ExBudget_52 -> Integer
MAlonzo.Code.Cost.d_ExMem_60
((T_Writer_304 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Writer_304 -> Any
MAlonzo.Code.Utils.d_accum_316
((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'__366
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_62)
-> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
T__'215'__366
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_62)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_140
((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'__380
(Any -> Any
forall a b. a -> b
coe Any
v2) (Any -> Any
forall a b. a -> b
coe Any
v5)))
(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 -> Any -> 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)
Any
v6))))))
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 a. a
v8)))))
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 a. a
MAlonzo.RTE.mazUnreachableError)
(Any, Any)
_ -> T_Either_6
T_ERROR_12
(T__'215'__366 T_TermU_24 (T__'215'__366 Integer Integer))
forall a. a
MAlonzo.RTE.mazUnreachableError
blah ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
blah :: Text -> Text -> Text
blah = (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe Text -> Text -> Text
d_blah_240
d_blah_240 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_blah_240 :: Text -> Text -> Text
d_blah_240 Text
v0 Text
v1
= let v2 :: Any
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v0 in
Any -> Text
forall a b. a -> b
coe
(let v3 :: Any
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v1 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: Any
v6 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14)
-> Any -> Any
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v4 in
Any -> Any
forall a b. a -> b
coe
(let v7 :: Any
v7 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14)
-> Any -> Any
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v5 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
-> (Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(T_RawTm_30 -> Text
MAlonzo.Code.Raw.d_rawPrinter_344
((T_Term_14 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v8))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" || " :: Data.Text.Text)
(T_RawTm_30 -> Text
MAlonzo.Code.Raw.d_rawPrinter_344
((T_Term_14 -> T_RawTm_30) -> Any -> T_RawTm_30
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v9)))
T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"deBruijnifying failed" :: Data.Text.Text)
T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"deBruijnifying failed" :: Data.Text.Text)))
T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"parsing failed" :: Data.Text.Text)
T_Either_6 Any Any
_ -> Text -> Any
forall a b. a -> b
coe (Text
"parsing failed" :: Data.Text.Text)))
printTy ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
printTy :: Text -> Text
printTy = (Text -> Text) -> Text -> Text
forall a b. a -> b
coe Text -> Text
d_printTy_286
d_printTy_286 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printTy_286 :: Text -> Text
d_printTy_286 Text
v0
= let v1 :: Any
v1 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 Text
v0 in
Any -> Text
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v1 of
MAlonzo.Code.Utils.C_inj'8321'_12 Any
v2
-> Text -> Any
forall a b. a -> b
coe (Text
"parseTy error" :: Data.Text.Text)
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v2
-> let v3 :: Any
v3 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16)
-> Any -> Any
forall a b. a -> b
coe T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 Any
v2 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Utils.C_inj'8321'_12 Any
v4
-> Text -> Any
forall a b. a -> b
coe (Text
"deBruinjifyTy error" :: Data.Text.Text)
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
-> (T_RawTy_2 -> Text) -> Any -> Any
forall a b. a -> b
coe T_RawTy_2 -> Text
MAlonzo.Code.Raw.d_rawTyPrinter_294 ((T_Type_16 -> T_RawTy_2) -> Any -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 Any
v4)
T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
alphaTy ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
alphaTy :: Text -> Text -> Bool
alphaTy = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b. a -> b
coe Text -> Text -> Bool
d_alphaTy_314
d_alphaTy_314 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d_alphaTy_314 :: Text -> Text -> Bool
d_alphaTy_314 Text
v0 Text
v1
= let v2 :: Any
v2 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 Text
v0 in
Any -> Bool
forall a b. a -> b
coe
(let v3 :: Any
v3 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TypeN_20
d_parseTy_30 Text
v1 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: Any
v6 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16)
-> Any -> Any
forall a b. a -> b
coe T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 Any
v4 in
Any -> Any
forall a b. a -> b
coe
(let v7 :: Any
v7 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16)
-> Any -> Any
forall a b. a -> b
coe T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16
d_deBruijnifyTy_34 Any
v5 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
-> (T_RawTy_2 -> T_RawTy_2 -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawTy_2 -> T_RawTy_2 -> Bool
MAlonzo.Code.Raw.d_decRTy_100 ((T_Type_16 -> T_RawTy_2) -> Any -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 Any
v8)
((T_Type_16 -> T_RawTy_2) -> Any -> Any
forall a b. a -> b
coe T_Type_16 -> T_RawTy_2
d_convTy_42 Any
v9)
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
alphaTm ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
alphaTm :: Text -> Text -> Bool
alphaTm = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b. a -> b
coe Text -> Text -> Bool
d_alphaTm_360
d_alphaTm_360 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d_alphaTm_360 :: Text -> Text -> Bool
d_alphaTm_360 Text
v0 Text
v1
= let v2 :: Any
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v0 in
Any -> Bool
forall a b. a -> b
coe
(let v3 :: Any
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermN_18
d_parseTm_26 Text
v1 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: Any
v6 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14)
-> Any -> Any
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v4 in
Any -> Any
forall a b. a -> b
coe
(let v7 :: Any
v7 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14)
-> Any -> Any
forall a b. a -> b
coe T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14
d_deBruijnifyTm_32 Any
v5 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
-> (T_RawTm_30 -> T_RawTm_30 -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
T_RawTm_30 -> T_RawTm_30 -> Bool
MAlonzo.Code.Raw.d_decRTm_186 ((T_Term_14 -> T_RawTm_30) -> Any -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v8)
((T_Term_14 -> T_RawTm_30) -> Any -> Any
forall a b. a -> b
coe T_Term_14 -> T_RawTm_30
d_convTm_38 Any
v9)
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
alphaU ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
alphaU :: Text -> Text -> Bool
alphaU = (Text -> Text -> Bool) -> Text -> Text -> Bool
forall a b. a -> b
coe Text -> Text -> Bool
d_alphaU_406
d_alphaU_406 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Bool
d_alphaU_406 :: Text -> Text -> Bool
d_alphaU_406 Text
v0 Text
v1
= let v2 :: Any
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermNU_22) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermNU_22
d_parseTmU_28 Text
v0 in
Any -> Bool
forall a b. a -> b
coe
(let v3 :: Any
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermNU_22) -> Text -> Any
forall a b. a -> b
coe Text -> T_Either_6 T_ParseError_4 T_TermNU_22
d_parseTmU_28 Text
v1 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v4
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: Any
v6 = (T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24)
-> Any -> Any
forall a b. a -> b
coe T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24
d_deBruijnifyTmU_36 Any
v4 in
Any -> Any
forall a b. a -> b
coe
(let v7 :: Any
v7 = (T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24)
-> Any -> Any
forall a b. a -> b
coe T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24
d_deBruijnifyTmU_36 Any
v5 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v8
-> case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v9
-> (T_Untyped_146 -> T_Untyped_146 -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Untyped_146 -> T_Untyped_146 -> Bool
MAlonzo.Code.Untyped.d_decUTm_314
((T_TermU_24 -> T_Untyped_146) -> Any -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 Any
v8) ((T_TermU_24 -> T_Untyped_146) -> Any -> Any
forall a b. a -> b
coe T_TermU_24 -> T_Untyped_146
d_convTmU_46 Any
v9)
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
T_Either_6 Any Any
_ -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))