{-# 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.Data.Nat.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
-- Cost.Size.integerSize
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
-- Cost.Size.byteStringSize
d_byteStringSize_6 ::
  MAlonzo.Code.Utils.T_ByteString_426 -> Integer
d_byteStringSize_6 :: T_ByteString_426 -> Integer
d_byteStringSize_6 = T_ByteString_426 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.g1ElementSize
d_g1ElementSize_8 ::
  MAlonzo.Code.Utils.T_Bls12'45'381'45'G1'45'Element_764 -> Integer
d_g1ElementSize_8 :: T_Bls12'45'381'45'G1'45'Element_764 -> Integer
d_g1ElementSize_8 = T_Bls12'45'381'45'G1'45'Element_764 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.g2ElementSize
d_g2ElementSize_10 ::
  MAlonzo.Code.Utils.T_Bls12'45'381'45'G2'45'Element_768 -> Integer
d_g2ElementSize_10 :: T_Bls12'45'381'45'G2'45'Element_768 -> Integer
d_g2ElementSize_10 = T_Bls12'45'381'45'G2'45'Element_768 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.mlResultElementSize
d_mlResultElementSize_12 ::
  MAlonzo.Code.Utils.T_Bls12'45'381'45'MlResult_772 -> Integer
d_mlResultElementSize_12 :: T_Bls12'45'381'45'MlResult_772 -> Integer
d_mlResultElementSize_12 = T_Bls12'45'381'45'MlResult_772 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.dataSize
d_dataSize_14 :: MAlonzo.Code.Utils.T_DATA_618 -> Integer
d_dataSize_14 :: T_DATA_618 -> Integer
d_dataSize_14 = T_DATA_618 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.dataNodeCount
d_dataNodeCount_16 :: MAlonzo.Code.Utils.T_DATA_618 -> Integer
d_dataNodeCount_16 :: T_DATA_618 -> Integer
d_dataNodeCount_16 = DataNodeCount -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size (DataNodeCount -> Integer)
-> (T_DATA_618 -> DataNodeCount) -> T_DATA_618 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_DATA_618 -> DataNodeCount
DataNodeCount
-- Cost.Size.boolSize
d_boolSize_18 :: Bool -> Integer
d_boolSize_18 :: Bool -> Integer
d_boolSize_18 = Bool -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.unitSize
d_unitSize_20 ::
  MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 -> Integer
d_unitSize_20 :: T_'8868'_6 -> Integer
d_unitSize_20 = T_'8868'_6 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.stringSize
d_stringSize_22 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Integer
d_stringSize_22 :: T_String_6 -> Integer
d_stringSize_22 = T_String_6 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.valueSize
d_valueSize_24 :: MAlonzo.Code.Utils.T_Value_776 -> Integer
d_valueSize_24 :: T_Value_776 -> Integer
d_valueSize_24 = T_Value_776 -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size
-- Cost.Size.valueMaxDepth
d_valueMaxDepth_26 :: MAlonzo.Code.Utils.T_Value_776 -> Integer
d_valueMaxDepth_26 :: T_Value_776 -> Integer
d_valueMaxDepth_26 = ValueMaxDepth -> Integer
forall {c} {a}. (Num c, ExMemoryUsage a) => a -> c
size (ValueMaxDepth -> Integer)
-> (T_Value_776 -> ValueMaxDepth) -> T_Value_776 -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T_Value_776 -> ValueMaxDepth
ValueMaxDepth
-- Cost.Size.defaultConstantMeasure
d_defaultConstantMeasure_28 ::
  MAlonzo.Code.RawU.T_TmCon_204 -> Integer
d_defaultConstantMeasure_28 :: T_TmCon_204 -> Integer
d_defaultConstantMeasure_28 T_TmCon_204
v0
  = case T_TmCon_204 -> T_TmCon_204
forall a b. a -> b
coe T_TmCon_204
v0 of
      MAlonzo.Code.RawU.C_tmCon_208 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_426 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_ByteString_426 -> 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_22 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_20 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_18 AgdaAny
v2
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
                      -> (T_DATA_618 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_DATA_618 -> Integer
d_dataSize_14 AgdaAny
v2
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aValue_20
                      -> (T_Value_776 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_Value_776 -> Integer
d_valueSize_24 AgdaAny
v2
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_22
                      -> (T_Bls12'45'381'45'G1'45'Element_764 -> Integer)
-> AgdaAny -> Integer
forall a b. a -> b
coe T_Bls12'45'381'45'G1'45'Element_764 -> Integer
d_g1ElementSize_8 AgdaAny
v2
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g2'45'element_24
                      -> (T_Bls12'45'381'45'G2'45'Element_768 -> Integer)
-> AgdaAny -> Integer
forall a b. a -> b
coe T_Bls12'45'381'45'G2'45'Element_768 -> Integer
d_g2ElementSize_10 AgdaAny
v2
                    T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'mlresult_26
                      -> (T_Bls12'45'381'45'MlResult_772 -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_Bls12'45'381'45'MlResult_772 -> 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
               -> (T_List_454 AgdaAny -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe T_List_454 AgdaAny -> Integer
MAlonzo.Code.Utils.du_length_490 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
             MAlonzo.Code.Builtin.Signature.C_array_20 T__'8866''9839'_4
v4
               -> let v5 :: AgdaAny
v5
                        = (T_'8868'_6 -> T_Array_602 AgdaAny -> Integer)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_'8868'_6 -> T_Array_602 AgdaAny -> Integer
forall xA. T_'8868'_6 -> T_Array_602 xA -> Integer
MAlonzo.Code.Utils.d_HSlengthOfArray_606 AgdaAny
forall a. a
erased AgdaAny
v2 in
                  AgdaAny -> Integer
forall a b. a -> b
coe
                    (case AgdaAny -> Integer
forall a b. a -> b
coe AgdaAny
v5 of
                       Integer
0 -> Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)
                       Integer
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
                       Integer
_ -> Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
             MAlonzo.Code.Builtin.Signature.C_pair_24 T__'8866''9839'_4
v4 T__'8866''9839'_4
v5
               -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
             T__'8866''9839'_4
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_TmCon_204
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Size.defaultValueMeasure
d_defaultValueMeasure_86 ::
  MAlonzo.Code.Untyped.CEK.T_Value_14 -> Integer
d_defaultValueMeasure_86 :: T_Value_14 -> Integer
d_defaultValueMeasure_86 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_204 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_TmCon_204 -> Integer
d_defaultConstantMeasure_28
                ((T__'8866''9839'_4 -> AgdaAny -> T_TmCon_204)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> T_TmCon_204
MAlonzo.Code.RawU.C_tmCon_208 (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)
-- Cost.Size.valueMaxDepthMeasure
d_valueMaxDepthMeasure_92 ::
  MAlonzo.Code.Untyped.CEK.T_Value_14 -> Integer
d_valueMaxDepthMeasure_92 :: T_Value_14 -> Integer
d_valueMaxDepthMeasure_92 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
           -> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v2 of
                MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v5
                  -> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v5 of
                       T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aValue_20
                         -> (T_Value_776 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_776 -> Integer
d_valueMaxDepth_26 AgdaAny
v3
                       T_AtomicTyCon_6
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
                T__'8866''9839'_4
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
         T_Value_14
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
-- Cost.Size.dataNodeCountMeasure
d_dataNodeCountMeasure_96 ::
  MAlonzo.Code.Untyped.CEK.T_Value_14 -> Integer
d_dataNodeCountMeasure_96 :: T_Value_14 -> Integer
d_dataNodeCountMeasure_96 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
           -> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v2 of
                MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v5
                  -> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v5 of
                       T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
                         -> (T_DATA_618 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DATA_618 -> Integer
d_dataNodeCount_16 AgdaAny
v3
                       T_AtomicTyCon_6
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
                T__'8866''9839'_4
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
         T_Value_14
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
-- Cost.Size.numBytesAsWords
d_numBytesAsWords_100 ::
  MAlonzo.Code.Untyped.CEK.T_Value_14 -> Integer
d_numBytesAsWords_100 :: T_Value_14 -> Integer
d_numBytesAsWords_100 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
           -> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v2 of
                MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v5
                  -> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v5 of
                       T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
                         -> case AgdaAny -> Integer
forall a b. a -> b
coe AgdaAny
v3 of
                              Integer
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                  let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (AgdaAny -> Integer
forall a b. a -> b
coe AgdaAny
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                  AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    ((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))
                                       ((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                          Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__318 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6)
                                          (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
8 :: Integer))))
                              Integer
0 -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
                              Integer
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
                       T_AtomicTyCon_6
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
                T__'8866''9839'_4
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1
         T_Value_14
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)