{-# 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 MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Algorithmic
import qualified MAlonzo.Code.Algorithmic.CEK
import qualified MAlonzo.Code.Algorithmic.CK
import qualified MAlonzo.Code.Algorithmic.Evaluation
import qualified MAlonzo.Code.Check
import qualified MAlonzo.Code.Cost
import qualified MAlonzo.Code.Cost.Model
import qualified MAlonzo.Code.Cost.Raw
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Evaluator.Base
import qualified MAlonzo.Code.Raw
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Scoped.Extrication
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Untyped.CEKWithCost
import qualified MAlonzo.Code.Utils
import Data.Bifunctor
import Data.Functor
import Data.Either
import Control.Monad.Trans.Except
import Raw
import PlutusCore
import PlutusCore.DeBruijn
import qualified UntypedPlutusCore as U
import qualified UntypedPlutusCore.Parser as U
import qualified Untyped 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_476 ->
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_476 -> T_Either_6 T_ERROR_12 ()
checkKindAgda = (T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ())
-> T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ()
forall a b. a -> b
coe T_Type_16 -> T_Kind_476 -> T_Either_6 T_ERROR_12 ()
d_checkKindX_50
d_checkKindX_50 ::
T_Type_16 ->
MAlonzo.Code.Utils.T_Kind_476 ->
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_476 -> T_Either_6 T_ERROR_12 ()
d_checkKindX_50 T_Type_16
v0 T_Kind_476
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_476 -> T_Kind_476 -> T_TypeError_12)
-> T_Kind_476 -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_TypeError_12
MAlonzo.Code.Check.C_kindMismatch_18 T_Kind_476
v1 Any
v4))))
((T_Dec_32 -> T_Either_6 (Any -> T_'8869'_4) Any) -> Any -> Any
forall a b. a -> b
coe
T_Dec_32 -> T_Either_6 (Any -> T_'8869'_4) Any
MAlonzo.Code.Utils.du_dec2Either_294
((T_Kind_476 -> T_Kind_476 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Dec_32
MAlonzo.Code.Check.d_decKind_138 (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
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_476
inferKindAgda :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
inferKindAgda = (T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476)
-> T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
forall a b. a -> b
coe T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
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_476
d_inferKind'8709'_68 :: T_Type_16 -> T_Either_6 T_ERROR_12 T_Kind_476
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_476
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_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
MAlonzo.Code.Scoped.Extrication.d_extricateNf'8902'_26
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (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_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14
MAlonzo.Code.Scoped.Extrication.d_extricateNf'8902'_26
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
(T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (Any -> Any
forall a b. a -> b
coe Any
v3)))))
T_Σ_14
_ -> Any
forall 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_476
-> 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_476
-> 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_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
((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_1180 -> T_Either_6 RuntimeError T_State_1180)
-> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_State_1180 -> T_Either_6 RuntimeError T_State_1180
MAlonzo.Code.Algorithmic.CEK.du_stepper_1532
(Integer -> Any
forall a b. a -> b
coe Integer
MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
((T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Stack_1166
-> T_Env_26
-> T__'8866'__168
-> T_State_1180)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Stack_1166
-> T_Env_26
-> T__'8866'__168
-> T_State_1180
MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1188
(T_Ctx_2 -> Any
forall a b. a -> b
coe T_Ctx_2
MAlonzo.Code.Algorithmic.C_'8709'_4) (Any -> Any
forall a b. a -> b
coe Any
v3)
(T_Stack_1166 -> Any
forall a b. a -> b
coe T_Stack_1166
MAlonzo.Code.Algorithmic.CEK.C_ε_1170)
(T_Env_26 -> Any
forall a b. a -> b
coe T_Env_26
MAlonzo.Code.Algorithmic.CEK.C_'91''93'_202) (Any -> Any
forall a b. a -> b
coe Any
v4))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v5 ->
case Any -> T_State_1180
forall a b. a -> b
coe Any
v5 of
MAlonzo.Code.Algorithmic.CEK.C__'894'_'9659'__1188 T_Ctx_2
v6 T__'8866'Nf'8902'__4
v7 T_Stack_1166
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'__1192 T__'8866'Nf'8902'__4
v6 T_Stack_1166
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'_1194 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'_1196 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_1180
_ -> 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_1202
(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'__364
MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
(MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Agda.Builtin.String.T_String_6
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146)) ->
T_TermU_24 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
(MAlonzo.Code.Utils.T__'215'__364
T_TermU_24 (MAlonzo.Code.Utils.T__'215'__364 Integer Integer))
runUCountingAgda :: T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
runUCountingAgda = (T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer)))
-> T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
forall a b. a -> b
coe T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
d_runUCounting_202
d_runUCounting_202 ::
MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
(MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Agda.Builtin.String.T_String_6
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146)) ->
T_TermU_24 ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Evaluator.Base.T_ERROR_12
(MAlonzo.Code.Utils.T__'215'__364
T_TermU_24 (MAlonzo.Code.Utils.T__'215'__364 Integer Integer))
d_runUCounting_202 :: T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> T_TermU_24
-> T_Either_6
T_ERROR_12
(T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
d_runUCounting_202 T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v0 T_TermU_24
v1
= case T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
-> (Any, Any)
forall a b. a -> b
coe T__'215'__364
T_HCekMachineCosts_4
(T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146))
v0 of
MAlonzo.Code.Utils.C__'44'__378 Any
v2 Any
v3
-> let v4 :: Maybe (DefaultFun -> T_BuiltinModel_60)
v4 = T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
-> Maybe (DefaultFun -> T_BuiltinModel_60)
MAlonzo.Code.Cost.Model.d_createMap_508 (Any -> T_List_382 (T__'215'__364 Text T_CpuAndMemoryModel_146)
forall a b. a -> b
coe Any
v3) in
Any
-> T_Either_6
T_ERROR_12
(T__'215'__364 T_TermU_24 (T__'215'__364 Integer Integer))
forall a b. a -> b
coe
(case Maybe (DefaultFun -> T_BuiltinModel_60) -> Maybe Any
forall a b. a -> b
coe Maybe (DefaultFun -> T_BuiltinModel_60)
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'__364
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
T__'215'__364
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_138
((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378 (Any -> Any
forall a b. a -> b
coe Any
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'__378
((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'__378
((T_ExBudget_50 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_ExBudget_50 -> Integer
MAlonzo.Code.Cost.d_ExCPU_56
((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'__364
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
T__'215'__364
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_138
((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
(Any -> Any
forall a b. a -> b
coe Any
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_50 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_ExBudget_50 -> Integer
MAlonzo.Code.Cost.d_ExMem_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'__364
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46)
-> Any -> Any
forall a b. a -> b
coe
T__'215'__364
T_HCekMachineCosts_4 (DefaultFun -> T_BuiltinModel_60)
-> T_MachineParameters_46
MAlonzo.Code.Cost.d_machineParameters_138
((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
(Any -> Any
forall a b. a -> b
coe Any
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'__364 T_TermU_24 (T__'215'__364 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 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
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 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
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
forall a. a
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
forall a. a
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: t
v6 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
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 :: t
v7 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
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
forall a. a
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
forall a. a
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 :: t
v1 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> t
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
forall a. a
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 :: t
v3 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16) -> Any -> t
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
forall a. a
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 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> t
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 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TypeN_20) -> Text -> t
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
forall a. a
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
forall a. a
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: t
v6 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16) -> Any -> t
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 :: t
v7 = (T_TypeN_20 -> T_Either_6 FreeVariableError T_Type_16) -> Any -> t
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
forall a. a
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
forall a. a
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 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
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 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermN_18) -> Text -> t
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
forall a. a
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
forall a. a
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: t
v6 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
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 :: t
v7 = (T_TermN_18 -> T_Either_6 FreeVariableError T_Term_14) -> Any -> t
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
forall a. a
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
forall a. a
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 :: t
v2 = (Text -> T_Either_6 T_ParseError_4 T_TermNU_22) -> Text -> t
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 :: t
v3 = (Text -> T_Either_6 T_ParseError_4 T_TermNU_22) -> Text -> t
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
forall a. a
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
forall a. a
v3 of
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: t
v6 = (T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24)
-> Any -> t
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 :: t
v7 = (T_TermNU_22 -> T_Either_6 FreeVariableError T_TermU_24)
-> Any -> t
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
forall a. a
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
forall a. a
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))