{-# 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.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.List
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Data.Vec.Base

-- Cost.Base.CostingNat
d_CostingNat_4 :: ()
d_CostingNat_4 :: ()
d_CostingNat_4 = ()
forall a. a
erased
-- Cost.Base.StepKind
d_StepKind_6 :: ()
d_StepKind_6 = ()
data T_StepKind_6
  = C_BConst_8 | C_BVar_10 | C_BLamAbs_12 | C_BApply_14 |
    C_BDelay_16 | C_BForce_18 | C_BBuiltin_20 | C_BConstr_22 |
    C_BCase_24
-- Cost.Base.showStepKind'
d_showStepKind''_26 ::
  T_StepKind_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showStepKind''_26 :: T_StepKind_6 -> Text
d_showStepKind''_26 T_StepKind_6
v0
  = case T_StepKind_6 -> T_StepKind_6
forall a b. a -> b
coe T_StepKind_6
v0 of
      T_StepKind_6
C_BConst_8 -> Text -> Text
forall a b. a -> b
coe (Text
"BConst" :: Data.Text.Text)
      T_StepKind_6
C_BVar_10 -> Text -> Text
forall a b. a -> b
coe (Text
"BVar" :: Data.Text.Text)
      T_StepKind_6
C_BLamAbs_12 -> Text -> Text
forall a b. a -> b
coe (Text
"BLamAbs" :: Data.Text.Text)
      T_StepKind_6
C_BApply_14 -> Text -> Text
forall a b. a -> b
coe (Text
"BApply" :: Data.Text.Text)
      T_StepKind_6
C_BDelay_16 -> Text -> Text
forall a b. a -> b
coe (Text
"BDelay" :: Data.Text.Text)
      T_StepKind_6
C_BForce_18 -> Text -> Text
forall a b. a -> b
coe (Text
"BForce" :: Data.Text.Text)
      T_StepKind_6
C_BBuiltin_20 -> Text -> Text
forall a b. a -> b
coe (Text
"BBuiltin" :: Data.Text.Text)
      T_StepKind_6
C_BConstr_22 -> Text -> Text
forall a b. a -> b
coe (Text
"BConstr" :: Data.Text.Text)
      T_StepKind_6
C_BCase_24 -> Text -> Text
forall a b. a -> b
coe (Text
"BCase" :: Data.Text.Text)
      T_StepKind_6
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Base.showStepKind
d_showStepKind_28 ::
  T_StepKind_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showStepKind_28 :: T_StepKind_6 -> Text
d_showStepKind_28 T_StepKind_6
v0
  = (Any -> Maybe Any -> Any) -> Text -> Any -> Text
forall a b. a -> b
coe
      Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_fromMaybe_46 (Text
"" :: Data.Text.Text)
      ((Text -> Maybe Text) -> Text -> Any
forall a b. a -> b
coe
         Text -> Maybe Text
MAlonzo.Code.Data.String.Base.d_tail_14
         (T_StepKind_6 -> Text
d_showStepKind''_26 (T_StepKind_6 -> T_StepKind_6
forall a b. a -> b
coe T_StepKind_6
v0)))
-- Cost.Base.stepKindList
d_stepKindList_32 :: [T_StepKind_6]
d_stepKindList_32 :: [T_StepKind_6]
d_stepKindList_32
  = (Any -> [Any] -> [Any]) -> Any -> Any -> [T_StepKind_6]
forall a b. a -> b
coe
      Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BConst_8)
      ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BVar_10)
         ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
            Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BLamAbs_12)
            ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
               Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BApply_14)
               ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                  Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BDelay_16)
                  ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                     Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BForce_18)
                     ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                        Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BBuiltin_20)
                        ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                           Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BConstr_22)
                           ((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
                              Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BCase_24)
                              ([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))))))))
-- Cost.Base.ExBudgetCategory
d_ExBudgetCategory_34 :: ()
d_ExBudgetCategory_34 = ()
data T_ExBudgetCategory_34
  = C_BStep_36 T_StepKind_6 |
    C_BBuiltinApp_40 MAlonzo.Code.Builtin.T_Builtin_2
                     MAlonzo.Code.Data.Vec.Base.T_Vec_28 |
    C_BStartup_42
-- Cost.Base.MachineParameters
d_MachineParameters_46 :: p -> ()
d_MachineParameters_46 p
a0 = ()
data T_MachineParameters_46
  = C_MachineParameters'46'constructor_359 (T_ExBudgetCategory_34 ->
                                            AgdaAny)
                                           AgdaAny (AgdaAny -> AgdaAny -> AgdaAny)
                                           MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
-- Cost.Base.MachineParameters.cekMachineCost
d_cekMachineCost_58 ::
  T_MachineParameters_46 -> T_ExBudgetCategory_34 -> AgdaAny
d_cekMachineCost_58 :: T_MachineParameters_46 -> T_ExBudgetCategory_34 -> Any
d_cekMachineCost_58 T_MachineParameters_46
v0
  = case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
      C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_686
v4 -> (T_ExBudgetCategory_34 -> Any) -> T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34 -> Any
v1
      T_MachineParameters_46
_ -> T_ExBudgetCategory_34 -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Base.MachineParameters.ε
d_ε_60 :: T_MachineParameters_46 -> AgdaAny
d_ε_60 :: T_MachineParameters_46 -> Any
d_ε_60 T_MachineParameters_46
v0
  = case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
      C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_686
v4 -> Any -> Any
forall a b. a -> b
coe Any
v2
      T_MachineParameters_46
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Base.MachineParameters._∙_
d__'8729'__62 ::
  T_MachineParameters_46 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__62 :: T_MachineParameters_46 -> Any -> Any -> Any
d__'8729'__62 T_MachineParameters_46
v0
  = case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
      C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_686
v4 -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
v3
      T_MachineParameters_46
_ -> Any -> Any -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Base.MachineParameters.costMonoid
d_costMonoid_64 ::
  T_MachineParameters_46 ->
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_costMonoid_64 :: T_MachineParameters_46 -> T_IsMonoid_686
d_costMonoid_64 T_MachineParameters_46
v0
  = case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
      C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_686
v4 -> T_IsMonoid_686 -> T_IsMonoid_686
forall a b. a -> b
coe T_IsMonoid_686
v4
      T_MachineParameters_46
_ -> T_IsMonoid_686
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Base.MachineParameters.startupCost
d_startupCost_66 :: () -> T_MachineParameters_46 -> AgdaAny
d_startupCost_66 :: () -> T_MachineParameters_46 -> Any
d_startupCost_66 ~()
v0 T_MachineParameters_46
v1 = T_MachineParameters_46 -> Any
du_startupCost_66 T_MachineParameters_46
v1
du_startupCost_66 :: T_MachineParameters_46 -> AgdaAny
du_startupCost_66 :: T_MachineParameters_46 -> Any
du_startupCost_66 T_MachineParameters_46
v0
  = (T_MachineParameters_46 -> T_ExBudgetCategory_34 -> Any)
-> T_MachineParameters_46 -> Any -> Any
forall a b. a -> b
coe T_MachineParameters_46 -> T_ExBudgetCategory_34 -> Any
d_cekMachineCost_58 T_MachineParameters_46
v0 (T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34
C_BStartup_42)