{-# 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
-- 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_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
-- Cost.Size.g1ElementSize
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
-- Cost.Size.g2ElementSize
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
-- Cost.Size.mlResultElementSize
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
-- Cost.Size.dataSize
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
-- Cost.Size.boolSize
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
-- Cost.Size.unitSize
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
-- Cost.Size.stringSize
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
-- Cost.Size.defaultConstantMeasure
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
-- Cost.Size.defaultValueMeasure
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)