{-# 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.Cost.Size 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.Int
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Cost.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Utils
import PlutusCore.Evaluation.Machine.ExMemoryUsage
import PlutusCore.Evaluation.Machine.CostStream
import Data.SatInt
size :: a -> c
size = SatInt -> c
forall a. Num a => SatInt -> a
fromSatInt (SatInt -> c) -> (a -> SatInt) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostStream -> SatInt
sumCostStream (CostStream -> SatInt) -> (a -> CostStream) -> a -> SatInt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CostRose -> CostStream
flattenCostRose (CostRose -> CostStream) -> (a -> CostRose) -> a -> CostStream
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CostRose
forall a. ExMemoryUsage a => a -> CostRose
memoryUsage
d_integerSize_4 :: Integer -> Integer
d_integerSize_4 :: Integer -> Integer
d_integerSize_4 = Integer -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_byteStringSize_6 ::
MAlonzo.Code.Utils.T_ByteString_356 -> Integer
d_byteStringSize_6 :: T_ByteString_356 -> Integer
d_byteStringSize_6 = T_ByteString_356 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_g1ElementSize_8 ::
MAlonzo.Code.Utils.T_Bls12'45'381'45'G1'45'Element_464 -> Integer
d_g1ElementSize_8 :: T_Bls12'45'381'45'G1'45'Element_464 -> Integer
d_g1ElementSize_8 = T_Bls12'45'381'45'G1'45'Element_464 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_g2ElementSize_10 ::
MAlonzo.Code.Utils.T_Bls12'45'381'45'G2'45'Element_468 -> Integer
d_g2ElementSize_10 :: T_Bls12'45'381'45'G2'45'Element_468 -> Integer
d_g2ElementSize_10 = T_Bls12'45'381'45'G2'45'Element_468 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_mlResultElementSize_12 ::
MAlonzo.Code.Utils.T_Bls12'45'381'45'MlResult_472 -> Integer
d_mlResultElementSize_12 :: T_Bls12'45'381'45'MlResult_472 -> Integer
d_mlResultElementSize_12 = T_Bls12'45'381'45'MlResult_472 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_dataSize_14 :: MAlonzo.Code.Utils.T_DATA_450 -> Integer
d_dataSize_14 :: T_DATA_450 -> Integer
d_dataSize_14 = T_DATA_450 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_boolSize_16 :: Bool -> Integer
d_boolSize_16 :: Bool -> Integer
d_boolSize_16 = Bool -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_unitSize_18 ::
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 -> Integer
d_unitSize_18 :: T_'8868'_6 -> Integer
d_unitSize_18 = T_'8868'_6 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_stringSize_20 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Integer
d_stringSize_20 :: T_String_6 -> Integer
d_stringSize_20 = T_String_6 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
d_defaultConstantMeasure_22 ::
MAlonzo.Code.RawU.T_TmCon_198 -> Integer
d_defaultConstantMeasure_22 :: T_TmCon_198 -> Integer
d_defaultConstantMeasure_22 T_TmCon_198
v0
= case T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v0 of
MAlonzo.Code.RawU.C_tmCon_202 T__'8866''9839'_4
v1 AgdaAny
v2
-> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v1 of
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v4
-> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v4 of
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
-> (Integer -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe Integer -> Integer
d_integerSize_4 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBytestring_10
-> (T_ByteString_356 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_ByteString_356 -> Integer
d_byteStringSize_6 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aString_12
-> (T_String_6 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_String_6 -> Integer
d_stringSize_20 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14
-> (T_'8868'_6 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_'8868'_6 -> Integer
d_unitSize_18 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBool_16
-> (Bool -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe Bool -> Integer
d_boolSize_16 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
-> (T_DATA_450 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_DATA_450 -> Integer
d_dataSize_14 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_20
-> (T_Bls12'45'381'45'G1'45'Element_464 -> Integer)
-> AgdaAny -> Integer
forall a b. a -> b
coe T_Bls12'45'381'45'G1'45'Element_464 -> Integer
d_g1ElementSize_8 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g2'45'element_22
-> (T_Bls12'45'381'45'G2'45'Element_468 -> Integer)
-> AgdaAny -> Integer
forall a b. a -> b
coe T_Bls12'45'381'45'G2'45'Element_468 -> Integer
d_g2ElementSize_10 AgdaAny
v2
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'mlresult_24
-> (T_Bls12'45'381'45'MlResult_472 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_Bls12'45'381'45'MlResult_472 -> Integer
d_mlResultElementSize_12 AgdaAny
v2
T_AtomicTyCon_6
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v4
-> case AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v2 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_386 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
MAlonzo.Code.Utils.C__'8759'__388 AgdaAny
v5 [AgdaAny]
v6
-> (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
3 :: Integer))
((T_TmCon_198 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TmCon_198 -> Integer
d_defaultConstantMeasure_22
((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202
((T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6))))
((T_TmCon_198 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TmCon_198 -> Integer
d_defaultConstantMeasure_22
((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
[AgdaAny]
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_pair_20 T__'8866''9839'_4
v4 T__'8866''9839'_4
v5
-> case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v2 of
MAlonzo.Code.Utils.C__'44'__378 AgdaAny
v6 AgdaAny
v7
-> (Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
((T_TmCon_198 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TmCon_198 -> Integer
d_defaultConstantMeasure_22
((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
((T_TmCon_198 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TmCon_198 -> Integer
d_defaultConstantMeasure_22
((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)))
(AgdaAny, AgdaAny)
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866''9839'_4
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_TmCon_198
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_defaultValueMeasure_58 ::
MAlonzo.Code.Untyped.CEK.T_Value_14 -> Integer
d_defaultValueMeasure_58 :: T_Value_14 -> Integer
d_defaultValueMeasure_58 T_Value_14
v0
= let v1 :: Integer
v1 = Integer
0 :: Integer in
AgdaAny -> Integer
forall a b. a -> b
coe
(case T_Value_14 -> T_Value_14
forall a b. a -> b
coe T_Value_14
v0 of
MAlonzo.Code.Untyped.CEK.C_V'45'con_50 T__'8866''9839'_4
v2 AgdaAny
v3
-> (T_TmCon_198 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_TmCon_198 -> Integer
d_defaultConstantMeasure_22
((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_198
MAlonzo.Code.RawU.C_tmCon_202 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
T_Value_14
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)