{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
{-# LANGUAGE TypeApplications #-}

module MAlonzo.Code.Evaluator.Base 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.String
import qualified MAlonzo.Code.Check
import qualified MAlonzo.Code.Data.String.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.Utils

import PlutusCore.Pretty
import qualified Data.Text as T
import PlutusCore.Error
import qualified Untyped as U
import Raw
-- Evaluator.Base.ParseError
type T_ParseError_4 = PlutusCore.Error.ParserErrorBundle
d_ParseError_4 :: a
d_ParseError_4
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Evaluator.Base.ParseError"
-- Evaluator.Base.prettyPrintTm
d_prettyPrintTm_6 ::
  MAlonzo.Code.Raw.T_RawTm_30 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_prettyPrintTm_6 :: T_RawTm_30 -> Text
d_prettyPrintTm_6 = forall str a. (Pretty a, Render str) => a -> str
display @T.Text (Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
 -> Text)
-> (T_RawTm_30
    -> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ())
-> T_RawTm_30
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> T_RawTm_30
-> Term NamedTyDeBruijn NamedDeBruijn DefaultUni DefaultFun ()
unconv Int
0
-- Evaluator.Base.prettyPrintTy
d_prettyPrintTy_8 ::
  MAlonzo.Code.Raw.T_RawTy_2 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_prettyPrintTy_8 :: T_RawTy_2 -> Text
d_prettyPrintTy_8 = forall str a. (Pretty a, Render str) => a -> str
display @T.Text (Type NamedTyDeBruijn DefaultUni () -> Text)
-> (T_RawTy_2 -> Type NamedTyDeBruijn DefaultUni ())
-> T_RawTy_2
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> T_RawTy_2 -> Type NamedTyDeBruijn DefaultUni ()
unconvT Int
0
-- Evaluator.Base.prettyPrintUTm
d_prettyPrintUTm_10 ::
  MAlonzo.Code.RawU.T_Untyped_146 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_prettyPrintUTm_10 :: T_Untyped_146 -> Text
d_prettyPrintUTm_10 = forall str a. (Pretty a, Render str) => a -> str
display @T.Text (Term NamedDeBruijn DefaultUni DefaultFun () -> Text)
-> (T_Untyped_146 -> Term NamedDeBruijn DefaultUni DefaultFun ())
-> T_Untyped_146
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> T_Untyped_146 -> Term NamedDeBruijn DefaultUni DefaultFun ()
U.uconv Int
0
-- Evaluator.Base.ERROR
d_ERROR_12 :: ()
d_ERROR_12 = ()
type T_ERROR_12 = ERROR
pattern $mC_typeError_14 :: forall {r}. ERROR -> (Text -> r) -> ((# #) -> r) -> r
$bC_typeError_14 :: Text -> ERROR
C_typeError_14 a0 = TypeError a0
pattern $mC_parseError_16 :: forall {r}. ERROR -> (ParserErrorBundle -> r) -> ((# #) -> r) -> r
$bC_parseError_16 :: ParserErrorBundle -> ERROR
C_parseError_16 a0 = ParseError a0
pattern $mC_scopeError_18 :: forall {r}. ERROR -> (ScopeError -> r) -> ((# #) -> r) -> r
$bC_scopeError_18 :: ScopeError -> ERROR
C_scopeError_18 a0 = ScopeError a0
pattern $mC_runtimeError_20 :: forall {r}. ERROR -> (RuntimeError -> r) -> ((# #) -> r) -> r
$bC_runtimeError_20 :: RuntimeError -> ERROR
C_runtimeError_20 a0 = RuntimeError a0
pattern $mC_jsonError_22 :: forall {r}. ERROR -> (Text -> r) -> ((# #) -> r) -> r
$bC_jsonError_22 :: Text -> ERROR
C_jsonError_22 a0 = JsonError a0
check_typeError_14 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> T_ERROR_12
check_typeError_14 :: Text -> ERROR
check_typeError_14 = Text -> ERROR
TypeError
check_parseError_16 :: T_ParseError_4 -> T_ERROR_12
check_parseError_16 :: ParserErrorBundle -> ERROR
check_parseError_16 = ParserErrorBundle -> ERROR
ParseError
check_scopeError_18 ::
  MAlonzo.Code.Scoped.T_ScopeError_576 -> T_ERROR_12
check_scopeError_18 :: ScopeError -> ERROR
check_scopeError_18 = ScopeError -> ERROR
ScopeError
check_runtimeError_20 ::
  MAlonzo.Code.Utils.T_RuntimeError_348 -> T_ERROR_12
check_runtimeError_20 :: RuntimeError -> ERROR
check_runtimeError_20 = RuntimeError -> ERROR
RuntimeError
check_jsonError_22 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> T_ERROR_12
check_jsonError_22 :: Text -> ERROR
check_jsonError_22 = Text -> ERROR
JsonError
cover_ERROR_12 :: ERROR -> ()
cover_ERROR_12 :: ERROR -> ()
cover_ERROR_12 ERROR
x
  = case ERROR
x of
      TypeError Text
_ -> ()
      ParseError ParserErrorBundle
_ -> ()
      ScopeError ScopeError
_ -> ()
      RuntimeError RuntimeError
_ -> ()
      JsonError Text
_ -> ()
-- Evaluator.Base.uglyTypeError
d_uglyTypeError_24 ::
  MAlonzo.Code.Check.T_TypeError_12 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_uglyTypeError_24 :: T_TypeError_12 -> Text
d_uglyTypeError_24 T_TypeError_12
v0
  = case T_TypeError_12 -> T_TypeError_12
forall a b. a -> b
coe T_TypeError_12
v0 of
      MAlonzo.Code.Check.C_kindMismatch_18 T_Kind_476
v1 T_Kind_476
v2
        -> Text -> Text
forall a b. a -> b
coe (Text
"kindMismatch" :: Data.Text.Text)
      MAlonzo.Code.Check.C_notFunKind_26 T_Kind_476
v1
        -> Text -> Text
forall a b. a -> b
coe (Text
"NotFunKind" :: Data.Text.Text)
      MAlonzo.Code.Check.C_notPat_32 T_Kind_476
v1
        -> Text -> Text
forall a b. a -> b
coe (Text
"notPat" :: Data.Text.Text)
      T_TypeError_12
MAlonzo.Code.Check.C_UnknownType_34
        -> Text -> Text
forall a b. a -> b
coe (Text
"UnknownType" :: Data.Text.Text)
      MAlonzo.Code.Check.C_notPi_44 T_Ctx'8902'_2
v1 T__'8866'Nf'8902'__4
v2
        -> Text -> Text
forall a b. a -> b
coe (Text
"notPi" :: Data.Text.Text)
      MAlonzo.Code.Check.C_notMu_56 T_Ctx'8902'_2
v1 T__'8866'Nf'8902'__4
v2
        -> Text -> Text
forall a b. a -> b
coe (Text
"notMu" :: Data.Text.Text)
      MAlonzo.Code.Check.C_notFunType_66 T_Ctx'8902'_2
v1 T__'8866'Nf'8902'__4
v2
        -> Text -> Text
forall a b. a -> b
coe (Text
"notFunType" :: Data.Text.Text)
      MAlonzo.Code.Check.C_notSOP_76 T_Ctx'8902'_2
v1 T__'8866'Nf'8902'__4
v2
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"notSOP" :: Data.Text.Text)
             ((T_RawTy_2 -> Text) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
                T_RawTy_2 -> Text
d_prettyPrintTy_8
                (Integer -> T_ScopedTy_14 -> T_RawTy_2
MAlonzo.Code.Scoped.d_extricateScopeTy_780
                   ((T_Ctx'8902'_2 -> Integer) -> Any -> Integer
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
v1))
                   ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> T_ScopedTy_14
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
v1)
                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2))))
      MAlonzo.Code.Check.C_IndexOutOfBounds_82 Integer
v1 Integer
v2
        -> Text -> Text
forall a b. a -> b
coe (Text
"IndexOutOfBounds" :: Data.Text.Text)
      T_TypeError_12
MAlonzo.Code.Check.C_TooManyConstrArgs_84
        -> Text -> Text
forall a b. a -> b
coe (Text
"TooManyConstrArgs" :: Data.Text.Text)
      T_TypeError_12
MAlonzo.Code.Check.C_TooFewConstrArgs_86
        -> Text -> Text
forall a b. a -> b
coe (Text
"TooFewConstrArgs" :: Data.Text.Text)
      T_TypeError_12
MAlonzo.Code.Check.C_TooFewCases_88
        -> Text -> Text
forall a b. a -> b
coe (Text
"TooFewCases" :: Data.Text.Text)
      T_TypeError_12
MAlonzo.Code.Check.C_TooManyCases_90
        -> Text -> Text
forall a b. a -> b
coe (Text
"TooManyCases" :: Data.Text.Text)
      MAlonzo.Code.Check.C_typeMismatch_100 T_Ctx'8902'_2
v1 T_Kind_476
v2 T__'8866'Nf'8902'__4
v3 T__'8866'Nf'8902'__4
v4
        -> (Text -> Text -> Text) -> Any -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             ((T_RawTy_2 -> Text) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
                T_RawTy_2 -> Text
d_prettyPrintTy_8
                (Integer -> T_ScopedTy_14 -> T_RawTy_2
MAlonzo.Code.Scoped.d_extricateScopeTy_780
                   ((T_Ctx'8902'_2 -> Integer) -> Any -> Integer
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
v1))
                   ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> T_ScopedTy_14
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
v1)
                      (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v2) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v3))))
             ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Text
" doesn't match " :: Data.Text.Text)
                ((T_RawTy_2 -> Text) -> T_RawTy_2 -> Any
forall a b. a -> b
coe
                   T_RawTy_2 -> Text
d_prettyPrintTy_8
                   (Integer -> T_ScopedTy_14 -> T_RawTy_2
MAlonzo.Code.Scoped.d_extricateScopeTy_780
                      ((T_Ctx'8902'_2 -> Integer) -> Any -> Integer
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
v1))
                      ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T_ScopedTy_14)
-> Any -> Any -> Any -> T_ScopedTy_14
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
v1)
                         (T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
v2) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4)))))
      T_TypeError_12
MAlonzo.Code.Check.C_builtinError_102
        -> Text -> Text
forall a b. a -> b
coe (Text
"builtinError" :: Data.Text.Text)
      MAlonzo.Code.Check.C_Unimplemented_104 Text
v1
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"Feature " :: Data.Text.Text)
             ((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
v1
                (Text
" not implemented" :: Data.Text.Text))
      T_TypeError_12
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Evaluator.Base.reportError
d_reportError_66 ::
  T_ERROR_12 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_reportError_66 :: ERROR -> Text
d_reportError_66 ERROR
v0
  = case ERROR -> ERROR
forall a b. a -> b
coe ERROR
v0 of
      C_typeError_14 Text
v1
        -> (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"typeError: " :: Data.Text.Text) Text
v1
      C_parseError_16 ParserErrorBundle
v1 -> Text -> Text
forall a b. a -> b
coe (Text
"parseError" :: Data.Text.Text)
      C_scopeError_18 ScopeError
v1 -> Text -> Text
forall a b. a -> b
coe (Text
"scopeError" :: Data.Text.Text)
      C_runtimeError_20 RuntimeError
v1
        -> case RuntimeError -> RuntimeError
forall a b. a -> b
coe RuntimeError
v1 of
             RuntimeError
MAlonzo.Code.Utils.C_gasError_350
               -> Text -> Text
forall a b. a -> b
coe (Text
"gasError" :: Data.Text.Text)
             RuntimeError
MAlonzo.Code.Utils.C_userError_352
               -> Text -> Text
forall a b. a -> b
coe (Text
"userError" :: Data.Text.Text)
             RuntimeError
MAlonzo.Code.Utils.C_runtimeTypeError_354
               -> Text -> Text
forall a b. a -> b
coe (Text
"runtimeTypeError" :: Data.Text.Text)
             RuntimeError
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      C_jsonError_22 Text
v1
        -> (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"jsonError: " :: Data.Text.Text) Text
v1
      ERROR
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Evaluator.Base.maxsteps
d_maxsteps_72 :: Integer
d_maxsteps_72 :: Integer
d_maxsteps_72 = Integer -> Integer
forall a b. a -> b
coe (Integer
10000000000 :: Integer)