{-# 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 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.Float
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Cost.Base
import qualified MAlonzo.Code.Cost.Model
import qualified MAlonzo.Code.Cost.Raw
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Nat.Show
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Data.String.Properties
import qualified MAlonzo.Code.Data.Tree.AVL
import qualified MAlonzo.Code.Data.Tree.AVL.Map
import qualified MAlonzo.Code.Data.Tree.AVL.Value
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Text.Printf
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Utils

-- Cost.AVL.Map
d_Map_6 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Map_6 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Map_6 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Cost.AVL.empty
d_empty_10 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_empty_10 :: T_Level_18 -> T_Level_18 -> T_Tree_240
d_empty_10 T_Level_18
v0 T_Level_18
v1 = T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
MAlonzo.Code.Data.Tree.AVL.Map.du_empty_182
-- Cost.AVL.singleton
d_singleton_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_singleton_36 :: T_Level_18 -> T_Level_18 -> Text -> AgdaAny -> T_Tree_240
d_singleton_36 T_Level_18
v0 T_Level_18
v1
  = (AgdaAny -> AgdaAny -> T_Tree_240) -> Text -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.Map.du_singleton_184
-- Cost.AVL.unionWith
d_unionWith_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_unionWith_44 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_unionWith_44 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v4
  = (T_StrictTotalOrder_864
 -> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe
      T_StrictTotalOrder_864
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.Map.du_unionWith_216
      (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe
         T_StrictTotalOrder_864
MAlonzo.Code.Data.String.Properties.d_'60''45'strictTotalOrder'45''8776'_76)
      AgdaAny -> Maybe AgdaAny -> AgdaAny
v4
-- Cost.ExBudget
d_ExBudget_50 :: T_Level_18
d_ExBudget_50 = ()
data T_ExBudget_50 = C_mkExBudget_60 Integer Integer
-- Cost.ExBudget.ExCPU
d_ExCPU_56 :: T_ExBudget_50 -> Integer
d_ExCPU_56 :: T_ExBudget_50 -> Integer
d_ExCPU_56 T_ExBudget_50
v0
  = case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0 of
      C_mkExBudget_60 Integer
v1 Integer
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T_ExBudget_50
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.ExBudget.ExMem
d_ExMem_58 :: T_ExBudget_50 -> Integer
d_ExMem_58 :: T_ExBudget_50 -> Integer
d_ExMem_58 T_ExBudget_50
v0
  = case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0 of
      C_mkExBudget_60 Integer
v1 Integer
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v2
      T_ExBudget_50
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.fromHExBudget
d_fromHExBudget_62 ::
  MAlonzo.Code.Cost.Raw.T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62 :: T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62 T_HExBudget_6
v0
  = (Integer -> Integer -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
      Integer -> Integer -> T_ExBudget_50
C_mkExBudget_60 ((T_HExBudget_6 -> Integer) -> T_HExBudget_6 -> AgdaAny
forall a b. a -> b
coe T_HExBudget_6 -> Integer
MAlonzo.Code.Cost.Raw.d_getCPUCost_28 T_HExBudget_6
v0)
      ((T_HExBudget_6 -> Integer) -> T_HExBudget_6 -> AgdaAny
forall a b. a -> b
coe T_HExBudget_6 -> Integer
MAlonzo.Code.Cost.Raw.d_getMemoryCost_30 T_HExBudget_6
v0)
-- Cost.ε€
d_ε'8364'_66 :: T_ExBudget_50
d_ε'8364'_66 :: T_ExBudget_50
d_ε'8364'_66
  = (Integer -> Integer -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe Integer -> Integer -> T_ExBudget_50
C_mkExBudget_60 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))
-- Cost._∙€_
d__'8729''8364'__68 ::
  T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68 :: T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68 T_ExBudget_50
v0 T_ExBudget_50
v1
  = case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0 of
      C_mkExBudget_60 Integer
v2 Integer
v3
        -> case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v1 of
             C_mkExBudget_60 Integer
v4 Integer
v5
               -> (Integer -> Integer -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
                    Integer -> Integer -> T_ExBudget_50
C_mkExBudget_60 ((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
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
                    ((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
v3) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5))
             T_ExBudget_50
_ -> T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ExBudget_50
_ -> T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.isMonoidExBudget
d_isMonoidExBudget_78 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_isMonoidExBudget_78 :: T_IsMonoid_358
d_isMonoidExBudget_78
  = (T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> T_IsMonoid_358
forall a b. a -> b
coe
      T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
      ((T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
         ((T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
            (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
            AgdaAny
forall a. a
erased)
         AgdaAny
forall a. a
erased)
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
-- Cost.builtinCost
d_builtinCost_94 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Cost.Model.T_BuiltinModel_60 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> T_ExBudget_50
d_builtinCost_94 :: T_Builtin_2 -> T_BuiltinModel_60 -> T_Vec_24 -> T_ExBudget_50
d_builtinCost_94 T_Builtin_2
v0 T_BuiltinModel_60
v1 T_Vec_24
v2
  = (Integer -> Integer -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
      Integer -> Integer -> T_ExBudget_50
C_mkExBudget_60
      ((Integer -> T_CostingModel_8 -> T_Vec_24 -> Integer)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Integer -> T_CostingModel_8 -> T_Vec_24 -> Integer
MAlonzo.Code.Cost.Model.d_runModel_94
         ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v0))
         ((T_BuiltinModel_60 -> T_CostingModel_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_BuiltinModel_60 -> T_CostingModel_8
MAlonzo.Code.Cost.Model.d_costingCPU_68 (T_BuiltinModel_60 -> AgdaAny
forall a b. a -> b
coe T_BuiltinModel_60
v1)) (T_Vec_24 -> AgdaAny
forall a b. a -> b
coe T_Vec_24
v2))
      ((Integer -> T_CostingModel_8 -> T_Vec_24 -> Integer)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Integer -> T_CostingModel_8 -> T_Vec_24 -> Integer
MAlonzo.Code.Cost.Model.d_runModel_94
         ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v0))
         ((T_BuiltinModel_60 -> T_CostingModel_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_BuiltinModel_60 -> T_CostingModel_8
MAlonzo.Code.Cost.Model.d_costingMem_70 (T_BuiltinModel_60 -> AgdaAny
forall a b. a -> b
coe T_BuiltinModel_60
v1)) (T_Vec_24 -> AgdaAny
forall a b. a -> b
coe T_Vec_24
v2))
-- Cost.CostModel
d_CostModel_102 :: ()
d_CostModel_102 :: T_Level_18
d_CostModel_102 = T_Level_18
forall a. a
erased
-- Cost.cekMachineCostFunction
d_cekMachineCostFunction_104 ::
  MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4 ->
  MAlonzo.Code.Cost.Base.T_StepKind_6 -> T_ExBudget_50
d_cekMachineCostFunction_104 :: T_HCekMachineCosts_4 -> T_StepKind_6 -> T_ExBudget_50
d_cekMachineCostFunction_104 T_HCekMachineCosts_4
v0 T_StepKind_6
v1
  = case T_StepKind_6 -> T_StepKind_6
forall a b. a -> b
coe T_StepKind_6
v1 of
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BConst_8
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekConstCost_12 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BVar_10
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekVarCost_10 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BLamAbs_12
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekLamCost_14 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BApply_14
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekApplyCost_20 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BDelay_16
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekDelayCost_16 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BForce_18
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekForceCost_18 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BBuiltin_20
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekBuiltinCost_22 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BConstr_22
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekConstCost_12 T_HCekMachineCosts_4
v0)
      T_StepKind_6
MAlonzo.Code.Cost.Base.C_BCase_24
        -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekCaseCost_26 T_HCekMachineCosts_4
v0)
      T_StepKind_6
_ -> T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.exBudgetCategoryCost
d_exBudgetCategoryCost_124 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Builtin.T_Builtin_2 ->
     MAlonzo.Code.Cost.Model.T_BuiltinModel_60) ->
  MAlonzo.Code.Cost.Base.T_ExBudgetCategory_34 -> T_ExBudget_50
d_exBudgetCategoryCost_124 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_50
d_exBudgetCategoryCost_124 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0 T_ExBudgetCategory_34
v1
  = case T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> (AgdaAny, AgdaAny)
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0 of
      MAlonzo.Code.Utils.C__'44'__378 AgdaAny
v2 AgdaAny
v3
        -> case T_ExBudgetCategory_34 -> T_ExBudgetCategory_34
forall a b. a -> b
coe T_ExBudgetCategory_34
v1 of
             MAlonzo.Code.Cost.Base.C_BStep_36 T_StepKind_6
v4
               -> (T_HCekMachineCosts_4 -> T_StepKind_6 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_StepKind_6 -> T_ExBudget_50
d_cekMachineCostFunction_104 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_StepKind_6 -> AgdaAny
forall a b. a -> b
coe T_StepKind_6
v4)
             MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 T_Builtin_2
v4 T_Vec_24
v5
               -> (T_Builtin_2 -> T_BuiltinModel_60 -> T_Vec_24 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe T_Builtin_2 -> T_BuiltinModel_60 -> T_Vec_24 -> T_ExBudget_50
d_builtinCost_94 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v4) (AgdaAny -> T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3 T_Builtin_2
v4) (T_Vec_24 -> AgdaAny
forall a b. a -> b
coe T_Vec_24
v5)
             T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStartup_42
               -> (T_HExBudget_6 -> T_ExBudget_50) -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
                    T_HExBudget_6 -> T_ExBudget_50
d_fromHExBudget_62
                    ((T_HCekMachineCosts_4 -> T_HExBudget_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekStartupCost_8 AgdaAny
v2)
             T_ExBudgetCategory_34
_ -> T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
      (AgdaAny, AgdaAny)
_ -> T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.machineParameters
d_machineParameters_138 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Builtin.T_Builtin_2 ->
     MAlonzo.Code.Cost.Model.T_BuiltinModel_60) ->
  MAlonzo.Code.Cost.Base.T_MachineParameters_46
d_machineParameters_138 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_MachineParameters_46
d_machineParameters_138 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0
  = ((T_ExBudgetCategory_34 -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMonoid_358
 -> T_MachineParameters_46)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_MachineParameters_46
forall a b. a -> b
coe
      (T_ExBudgetCategory_34 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMonoid_358
-> T_MachineParameters_46
MAlonzo.Code.Cost.Base.C_MachineParameters'46'constructor_359
      ((T__'215'__364
   T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
 -> T_ExBudgetCategory_34 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_50
d_exBudgetCategoryCost_124 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> AgdaAny
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0)) (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
d_ε'8364'_66)
      ((T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50) -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68) (T_IsMonoid_358 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_358
d_isMonoidExBudget_78)
-- Cost.countingReport
d_countingReport_142 ::
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_countingReport_142 :: T_ExBudget_50 -> Text
d_countingReport_142 T_ExBudget_50
v0
  = case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0 of
      C_mkExBudget_60 Integer
v1 Integer
v2
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"\nCPU budget:    " :: Data.Text.Text)
             ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
"\nMemory budget: " :: Data.Text.Text)
                   (Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v2))))
      T_ExBudget_50
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.mkKeyFromExBudgetCategory
d_mkKeyFromExBudgetCategory_148 ::
  MAlonzo.Code.Cost.Base.T_ExBudgetCategory_34 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_mkKeyFromExBudgetCategory_148 :: T_ExBudgetCategory_34 -> Text
d_mkKeyFromExBudgetCategory_148 T_ExBudgetCategory_34
v0
  = case T_ExBudgetCategory_34 -> T_ExBudgetCategory_34
forall a b. a -> b
coe T_ExBudgetCategory_34
v0 of
      MAlonzo.Code.Cost.Base.C_BStep_36 T_StepKind_6
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
"0" :: Data.Text.Text)
             (T_StepKind_6 -> Text
MAlonzo.Code.Cost.Base.d_showStepKind_28 (T_StepKind_6 -> T_StepKind_6
forall a b. a -> b
coe T_StepKind_6
v1))
      MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 T_Builtin_2
v1 T_Vec_24
v2
        -> (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
"1" :: Data.Text.Text)
             (T_Builtin_2 -> Text
MAlonzo.Code.Builtin.d_showBuiltin_400 (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v1))
      T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStartup_42 -> Text -> Text
forall a b. a -> b
coe (Text
"2" :: Data.Text.Text)
      T_ExBudgetCategory_34
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.TallyingBudget
d_TallyingBudget_154 :: ()
d_TallyingBudget_154 :: T_Level_18
d_TallyingBudget_154 = T_Level_18
forall a. a
erased
-- Cost.lookup
d_lookup_156 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Cost.Base.T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156 :: T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156 T_Tree_240
v0 T_ExBudgetCategory_34
v1
  = let v2 :: t
v2
          = (T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
              T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.du_lookup_298
              (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe
                 T_StrictTotalOrder_864
MAlonzo.Code.Data.String.Properties.d_'60''45'strictTotalOrder'45''8776'_76)
              (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
              ((T_ExBudgetCategory_34 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_ExBudgetCategory_34 -> Text
d_mkKeyFromExBudgetCategory_148 (T_ExBudgetCategory_34 -> AgdaAny
forall a b. a -> b
coe T_ExBudgetCategory_34
v1)) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v0) in
    AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
         Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
d_ε'8364'_66
         Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Cost.εT
d_εT_176 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_240 T_ExBudget_50
d_εT_176 :: T__'215'__364 T_Tree_240 T_ExBudget_50
d_εT_176
  = (AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny))
-> AgdaAny -> AgdaAny -> T__'215'__364 T_Tree_240 T_ExBudget_50
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
      (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
MAlonzo.Code.Data.Tree.AVL.Map.du_empty_182)
      (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
d_ε'8364'_66)
-- Cost._∙T_
d__'8729'T__178 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_240 T_ExBudget_50 ->
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_240 T_ExBudget_50 ->
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_240 T_ExBudget_50
d__'8729'T__178 :: T__'215'__364 T_Tree_240 T_ExBudget_50
-> T__'215'__364 T_Tree_240 T_ExBudget_50
-> T__'215'__364 T_Tree_240 T_ExBudget_50
d__'8729'T__178 T__'215'__364 T_Tree_240 T_ExBudget_50
v0 T__'215'__364 T_Tree_240 T_ExBudget_50
v1
  = case T__'215'__364 T_Tree_240 T_ExBudget_50 -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe T__'215'__364 T_Tree_240 T_ExBudget_50
v0 of
      MAlonzo.Code.Utils.C__'44'__378 AgdaAny
v2 AgdaAny
v3
        -> case T__'215'__364 T_Tree_240 T_ExBudget_50 -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe T__'215'__364 T_Tree_240 T_ExBudget_50
v1 of
             MAlonzo.Code.Utils.C__'44'__378 AgdaAny
v4 AgdaAny
v5
               -> (AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny))
-> AgdaAny -> AgdaAny -> T__'215'__364 T_Tree_240 T_ExBudget_50
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
                    ((T_StrictTotalOrder_864
 -> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240
 -> T_Tree_240)
-> T_StrictTotalOrder_864
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                       T_StrictTotalOrder_864
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.Map.du_unionWith_216
                       T_StrictTotalOrder_864
MAlonzo.Code.Data.String.Properties.d_'60''45'strictTotalOrder'45''8776'_76
                       ((T_ExBudget_50 -> Maybe T_ExBudget_50 -> T_ExBudget_50) -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50 -> Maybe T_ExBudget_50 -> T_ExBudget_50
du_u_192) AgdaAny
v2 AgdaAny
v4)
                    ((T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             (AgdaAny, AgdaAny)
_ -> T__'215'__364 T_Tree_240 T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
      (AgdaAny, AgdaAny)
_ -> T__'215'__364 T_Tree_240 T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.u
d_u_192 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  T_ExBudget_50 -> Maybe T_ExBudget_50 -> T_ExBudget_50
d_u_192 :: T_Tree_240
-> T_ExBudget_50
-> T_Tree_240
-> T_ExBudget_50
-> T_ExBudget_50
-> Maybe T_ExBudget_50
-> T_ExBudget_50
d_u_192 ~T_Tree_240
v0 ~T_ExBudget_50
v1 ~T_Tree_240
v2 ~T_ExBudget_50
v3 T_ExBudget_50
v4 Maybe T_ExBudget_50
v5 = T_ExBudget_50 -> Maybe T_ExBudget_50 -> T_ExBudget_50
du_u_192 T_ExBudget_50
v4 Maybe T_ExBudget_50
v5
du_u_192 :: T_ExBudget_50 -> Maybe T_ExBudget_50 -> T_ExBudget_50
du_u_192 :: T_ExBudget_50 -> Maybe T_ExBudget_50 -> T_ExBudget_50
du_u_192 T_ExBudget_50
v0 Maybe T_ExBudget_50
v1
  = case Maybe T_ExBudget_50 -> Maybe AgdaAny
forall a b. a -> b
coe Maybe T_ExBudget_50
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
        -> (T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68 (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0
      Maybe AgdaAny
_ -> T_ExBudget_50
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.TallyingBudget-assoc
d_TallyingBudget'45'assoc_200 :: a
d_TallyingBudget'45'assoc_200
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Cost.TallyingBudget-assoc"
-- Cost.Tallying-budget-identityʳ
d_Tallying'45'budget'45'identity'691'_202 :: a
d_Tallying'45'budget'45'identity'691'_202
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Cost.Tallying-budget-identity\691"
-- Cost.isMonoidTallyingBudget
d_isMonoidTallyingBudget_204 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_isMonoidTallyingBudget_204 :: T_IsMonoid_358
d_isMonoidTallyingBudget_204
  = (T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358)
-> AgdaAny -> AgdaAny -> T_IsMonoid_358
forall a b. a -> b
coe
      T_IsSemigroup_194 -> T_Σ_14 -> T_IsMonoid_358
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_7687
      ((T_IsMagma_86
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsMagma_86
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_IsSemigroup_194
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_4001
         ((T_IsEquivalence_26
 -> (AgdaAny
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMagma_86)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26
-> (AgdaAny
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMagma_86
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_553
            (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe
               T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_242)
            AgdaAny
forall a. a
erased)
         AgdaAny
forall a. a
erased)
      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
-- Cost.tallyingCekMachineCost
d_tallyingCekMachineCost_210 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Builtin.T_Builtin_2 ->
     MAlonzo.Code.Cost.Model.T_BuiltinModel_60) ->
  MAlonzo.Code.Cost.Base.T_ExBudgetCategory_34 ->
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_240 T_ExBudget_50
d_tallyingCekMachineCost_210 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T__'215'__364 T_Tree_240 T_ExBudget_50
d_tallyingCekMachineCost_210 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0 T_ExBudgetCategory_34
v1
  = (AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny))
-> AgdaAny -> AgdaAny -> T__'215'__364 T_Tree_240 T_ExBudget_50
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> (AgdaAny, AgdaAny)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
      ((AgdaAny -> AgdaAny -> T_Tree_240)
-> Text -> T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.Map.du_singleton_184
         (T_ExBudgetCategory_34 -> Text
d_mkKeyFromExBudgetCategory_148 (T_ExBudgetCategory_34 -> T_ExBudgetCategory_34
forall a b. a -> b
coe T_ExBudgetCategory_34
v1))
         (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_50
d_exBudgetCategoryCost_124 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T__'215'__364
     T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0) (T_ExBudgetCategory_34 -> T_ExBudgetCategory_34
forall a b. a -> b
coe T_ExBudgetCategory_34
v1)))
      ((T__'215'__364
   T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
 -> T_ExBudgetCategory_34 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_50
d_exBudgetCategoryCost_124 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> AgdaAny
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0) (T_ExBudgetCategory_34 -> AgdaAny
forall a b. a -> b
coe T_ExBudgetCategory_34
v1))
-- Cost.tallyingMachineParameters
d_tallyingMachineParameters_218 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
    (MAlonzo.Code.Builtin.T_Builtin_2 ->
     MAlonzo.Code.Cost.Model.T_BuiltinModel_60) ->
  MAlonzo.Code.Cost.Base.T_MachineParameters_46
d_tallyingMachineParameters_218 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_MachineParameters_46
d_tallyingMachineParameters_218 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0
  = ((T_ExBudgetCategory_34 -> AgdaAny)
 -> AgdaAny
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsMonoid_358
 -> T_MachineParameters_46)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_MachineParameters_46
forall a b. a -> b
coe
      (T_ExBudgetCategory_34 -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsMonoid_358
-> T_MachineParameters_46
MAlonzo.Code.Cost.Base.C_MachineParameters'46'constructor_359
      ((T__'215'__364
   T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
 -> T_ExBudgetCategory_34 -> T__'215'__364 T_Tree_240 T_ExBudget_50)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T__'215'__364 T_Tree_240 T_ExBudget_50
d_tallyingCekMachineCost_210 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> AgdaAny
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0)) (T__'215'__364 T_Tree_240 T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T__'215'__364 T_Tree_240 T_ExBudget_50
d_εT_176)
      ((T__'215'__364 T_Tree_240 T_ExBudget_50
 -> T__'215'__364 T_Tree_240 T_ExBudget_50
 -> T__'215'__364 T_Tree_240 T_ExBudget_50)
-> AgdaAny
forall a b. a -> b
coe T__'215'__364 T_Tree_240 T_ExBudget_50
-> T__'215'__364 T_Tree_240 T_ExBudget_50
-> T__'215'__364 T_Tree_240 T_ExBudget_50
d__'8729'T__178) (T_IsMonoid_358 -> AgdaAny
forall a b. a -> b
coe T_IsMonoid_358
d_isMonoidTallyingBudget_204)
-- Cost.tallyingReport
d_tallyingReport_222 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_240 T_ExBudget_50 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_tallyingReport_222 :: T__'215'__364 T_Tree_240 T_ExBudget_50 -> Text
d_tallyingReport_222 T__'215'__364 T_Tree_240 T_ExBudget_50
v0
  = case T__'215'__364 T_Tree_240 T_ExBudget_50 -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe T__'215'__364 T_Tree_240 T_ExBudget_50
v0 of
      MAlonzo.Code.Utils.C__'44'__378 AgdaAny
v1 AgdaAny
v2
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (T_ExBudget_50 -> Text
d_countingReport_142 (AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe AgdaAny
v2))
             ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Text
"\n" :: Data.Text.Text)
                ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
"\n" :: Data.Text.Text)
                   ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      ((T_Tree_240 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_240 -> Text
du_printStepReport_258 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                      ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                         (Text
"\n" :: Data.Text.Text)
                         ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                            (Text
"startup    " :: Data.Text.Text)
                            ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                               ((T_ExBudget_50 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T_ExBudget_50 -> Text
du_budgetToString_246
                                  ((T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                                     (T_ExBudgetCategory_34 -> AgdaAny
forall a b. a -> b
coe T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStartup_42)))
                               ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                  (Text
"\n" :: Data.Text.Text)
                                  ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                     (Text
"compute    " :: Data.Text.Text)
                                     ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                        ((T_ExBudget_50 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_ExBudget_50 -> Text
du_budgetToString_246
                                           ((T_Tree_240 -> T_ExBudget_50) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_240 -> T_ExBudget_50
du_totalComputeCost_232 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
                                        ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                           (Text
"\n" :: Data.Text.Text)
                                           ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                              (Text
"\n\n" :: Data.Text.Text)
                                              ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                 ((T_Tree_240 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_240 -> Text
du_printBuiltinReport_274 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                                                 ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                    (Text
"\n" :: Data.Text.Text)
                                                    ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                       Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                       (Text
"Total builtin costs:   " :: Data.Text.Text)
                                                       ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                          Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                          ((T_ExBudget_50 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                             T_ExBudget_50 -> Text
du_budgetToString_246
                                                             ((T_Tree_240 -> T_ExBudget_50) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                T_Tree_240 -> T_ExBudget_50
du_totalBuiltinCosts_234 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))
                                                          ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                             (Text
"\n" :: Data.Text.Text)
                                                             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                ((Text -> AgdaAny) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                   Text -> AgdaAny
MAlonzo.Code.Text.Printf.d_printf_24
                                                                   (Text
"Time spent executing builtins:  %f%%\n"
                                                                    ::
                                                                    Data.Text.Text)
                                                                   ((Double -> Double -> Double) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                      Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54
                                                                      ((Double -> Double -> Double) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                         Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatTimes_52
                                                                         ((Integer -> Double) -> Integer -> AgdaAny
forall a b. a -> b
coe
                                                                            Integer -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primNatToFloat_24
                                                                            (Integer
100 :: Integer))
                                                                         ((T_ExBudget_50 -> Double) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                            T_ExBudget_50 -> Double
du_getCPU_242
                                                                            ((T_Tree_240 -> T_ExBudget_50) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                               T_Tree_240 -> T_ExBudget_50
du_totalBuiltinCosts_234
                                                                               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
                                                                      ((T_ExBudget_50 -> Double) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50 -> Double
du_getCPU_242 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))))
                                                                ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                   (Text
"\n" :: Data.Text.Text)
                                                                   ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                      (Text
"\n" :: Data.Text.Text)
                                                                      ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                         (Text
"Total budget spent:    "
                                                                          ::
                                                                          Data.Text.Text)
                                                                         ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                            ((T_ExBudget_50 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                               T_ExBudget_50 -> Text
du_budgetToString_246
                                                                               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
                                                                            ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                               Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                               (Text
"\n"
                                                                                ::
                                                                                Data.Text.Text)
                                                                               ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                                  Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                                  (Text
"Predicted execution time: "
                                                                                   ::
                                                                                   Data.Text.Text)
                                                                                  ((Double -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                                     Double -> Text
du_formatTimePicoseconds_282
                                                                                     ((T_ExBudget_50 -> Double) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                                        T_ExBudget_50 -> Double
du_getCPU_242
                                                                                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                                           AgdaAny
v2))))))))))))))))))))))))))
      (AgdaAny, AgdaAny)
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.totalComputeCost
d_totalComputeCost_232 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 -> T_ExBudget_50
d_totalComputeCost_232 :: T_Tree_240 -> T_ExBudget_50 -> T_ExBudget_50
d_totalComputeCost_232 T_Tree_240
v0 ~T_ExBudget_50
v1 = T_Tree_240 -> T_ExBudget_50
du_totalComputeCost_232 T_Tree_240
v0
du_totalComputeCost_232 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> T_ExBudget_50
du_totalComputeCost_232 :: T_Tree_240 -> T_ExBudget_50
du_totalComputeCost_232 T_Tree_240
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      ((AgdaAny -> T_ExBudget_50 -> T_ExBudget_50) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68
              ((T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
                 T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156 (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v0)
                 ((T_StepKind_6 -> T_ExBudgetCategory_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StepKind_6 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStep_36 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))))
      (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
d_ε'8364'_66) ([T_StepKind_6] -> AgdaAny
forall a b. a -> b
coe [T_StepKind_6]
MAlonzo.Code.Cost.Base.d_stepKindList_32)
-- Cost._.totalBuiltinCosts
d_totalBuiltinCosts_234 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 -> T_ExBudget_50
d_totalBuiltinCosts_234 :: T_Tree_240 -> T_ExBudget_50 -> T_ExBudget_50
d_totalBuiltinCosts_234 T_Tree_240
v0 ~T_ExBudget_50
v1 = T_Tree_240 -> T_ExBudget_50
du_totalBuiltinCosts_234 T_Tree_240
v0
du_totalBuiltinCosts_234 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> T_ExBudget_50
du_totalBuiltinCosts_234 :: T_Tree_240 -> T_ExBudget_50
du_totalBuiltinCosts_234 T_Tree_240
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_ExBudget_50
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240 ((T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50) -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50 -> T_ExBudget_50 -> T_ExBudget_50
d__'8729''8364'__68)
      (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
d_ε'8364'_66)
      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
         ((AgdaAny -> T_ExBudget_50) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156
                 (T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v0)
                 ((T_Builtin_2 -> T_Vec_24 -> T_ExBudgetCategory_34)
-> AgdaAny -> AgdaAny -> T_ExBudgetCategory_34
forall a b. a -> b
coe
                    T_Builtin_2 -> T_Vec_24 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                    ((Integer -> AgdaAny -> T_Vec_24) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> AgdaAny -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490
                       ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                       ((T__'8866''9839'_4 -> AgdaAny -> T_Value_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T__'8866''9839'_4 -> AgdaAny -> T_Value_14
MAlonzo.Code.Untyped.CEK.C_V'45'con_50
                          ((T_AtomicTyCon_6 -> T__'8866''9839'_4) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T_AtomicTyCon_6 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_atomic_12
                             (T_AtomicTyCon_6 -> AgdaAny
forall a b. a -> b
coe T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14))
                          (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))))
         ([T_Builtin_2] -> AgdaAny
forall a b. a -> b
coe [T_Builtin_2]
MAlonzo.Code.Builtin.d_builtinList_402))
-- Cost._.getCPU
d_getCPU_242 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.Float.T_Float_6
d_getCPU_242 :: T_Tree_240 -> T_ExBudget_50 -> T_ExBudget_50 -> Double
d_getCPU_242 ~T_Tree_240
v0 ~T_ExBudget_50
v1 T_ExBudget_50
v2 = T_ExBudget_50 -> Double
du_getCPU_242 T_ExBudget_50
v2
du_getCPU_242 ::
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.Float.T_Float_6
du_getCPU_242 :: T_ExBudget_50 -> Double
du_getCPU_242 T_ExBudget_50
v0
  = (Integer -> Double) -> Integer -> Double
forall a b. a -> b
coe
      Integer -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primNatToFloat_24
      (T_ExBudget_50 -> Integer
d_ExCPU_56 (T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0))
-- Cost._.budgetToString
d_budgetToString_246 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_budgetToString_246 :: T_Tree_240 -> T_ExBudget_50 -> T_ExBudget_50 -> Text
d_budgetToString_246 ~T_Tree_240
v0 ~T_ExBudget_50
v1 T_ExBudget_50
v2 = T_ExBudget_50 -> Text
du_budgetToString_246 T_ExBudget_50
v2
du_budgetToString_246 ::
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_budgetToString_246 :: T_ExBudget_50 -> Text
du_budgetToString_246 T_ExBudget_50
v0
  = case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v0 of
      C_mkExBudget_60 Integer
v1 Integer
v2
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Char -> Integer -> Text -> Text
MAlonzo.Code.Data.String.Base.d_padLeft_56
                (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
15 :: Integer))
                ((Integer -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)))
             ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Text
"  " :: Data.Text.Text)
                (Char -> Integer -> Text -> Text
MAlonzo.Code.Data.String.Base.d_padLeft_56
                   (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
15 :: Integer))
                   ((Integer -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2))))
      T_ExBudget_50
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.printStepCost
d_printStepCost_252 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  MAlonzo.Code.Cost.Base.T_StepKind_6 ->
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printStepCost_252 :: T_Tree_240
-> T_ExBudget_50 -> T_StepKind_6 -> T_ExBudget_50 -> Text
d_printStepCost_252 ~T_Tree_240
v0 ~T_ExBudget_50
v1 T_StepKind_6
v2 T_ExBudget_50
v3 = T_StepKind_6 -> T_ExBudget_50 -> Text
du_printStepCost_252 T_StepKind_6
v2 T_ExBudget_50
v3
du_printStepCost_252 ::
  MAlonzo.Code.Cost.Base.T_StepKind_6 ->
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printStepCost_252 :: T_StepKind_6 -> T_ExBudget_50 -> Text
du_printStepCost_252 T_StepKind_6
v0 T_ExBudget_50
v1
  = (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
      (Char -> Integer -> Text -> Text
MAlonzo.Code.Data.String.Base.d_padRight_82
         (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
10 :: Integer))
         ((T_StepKind_6 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_StepKind_6 -> Text
MAlonzo.Code.Cost.Base.d_showStepKind_28 (T_StepKind_6 -> AgdaAny
forall a b. a -> b
coe T_StepKind_6
v0)))
      ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
         (Text
" " :: Data.Text.Text)
         ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
            (Char -> Integer -> Text -> Text
MAlonzo.Code.Data.String.Base.d_padLeft_56
               (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
20 :: Integer))
               ((T_ExBudget_50 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_ExBudget_50 -> Text
du_budgetToString_246 (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
v1)))
            (Text
"\n" :: Data.Text.Text)))
-- Cost._.printStepReport
d_printStepReport_258 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printStepReport_258 :: T_Tree_240 -> T_ExBudget_50 -> T_Tree_240 -> Text
d_printStepReport_258 ~T_Tree_240
v0 ~T_ExBudget_50
v1 T_Tree_240
v2 = T_Tree_240 -> Text
du_printStepReport_258 T_Tree_240
v2
du_printStepReport_258 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printStepReport_258 :: T_Tree_240 -> Text
du_printStepReport_258 T_Tree_240
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (Text -> Text -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
              ((T_StepKind_6 -> T_ExBudget_50 -> Text)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_StepKind_6 -> T_ExBudget_50 -> Text
du_printStepCost_252 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                 ((T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156 (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v0)
                    ((T_StepKind_6 -> T_ExBudgetCategory_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StepKind_6 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStep_36 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))))
      (Text -> AgdaAny
forall a b. a -> b
coe (Text
"" :: Data.Text.Text))
      ([T_StepKind_6] -> AgdaAny
forall a b. a -> b
coe [T_StepKind_6]
MAlonzo.Code.Cost.Base.d_stepKindList_32)
-- Cost._.printBuiltinCost
d_printBuiltinCost_266 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printBuiltinCost_266 :: T_Tree_240 -> T_ExBudget_50 -> T_Builtin_2 -> T_ExBudget_50 -> Text
d_printBuiltinCost_266 ~T_Tree_240
v0 ~T_ExBudget_50
v1 T_Builtin_2
v2 T_ExBudget_50
v3
  = T_Builtin_2 -> T_ExBudget_50 -> Text
du_printBuiltinCost_266 T_Builtin_2
v2 T_ExBudget_50
v3
du_printBuiltinCost_266 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  T_ExBudget_50 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printBuiltinCost_266 :: T_Builtin_2 -> T_ExBudget_50 -> Text
du_printBuiltinCost_266 T_Builtin_2
v0 T_ExBudget_50
v1
  = case T_ExBudget_50 -> T_ExBudget_50
forall a b. a -> b
coe T_ExBudget_50
v1 of
      C_mkExBudget_60 Integer
v2 Integer
v3
        -> let v4 :: t
v4
                 = (Text -> Text -> Text) -> Text -> AgdaAny -> t
forall a b. a -> b
coe
                     Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                     (Char -> Integer -> Text -> Text
MAlonzo.Code.Data.String.Base.d_padRight_82
                        (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
22 :: Integer))
                        ((T_Builtin_2 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_Builtin_2 -> Text
MAlonzo.Code.Builtin.d_showBuiltin_400 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v0)))
                     ((Text -> Text -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                        (Text
" " :: Data.Text.Text)
                        ((Text -> Text -> Text) -> AgdaAny -> Text -> AgdaAny
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           ((T_ExBudget_50 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50 -> Text
du_budgetToString_246 (T_ExBudget_50 -> AgdaAny
forall a b. a -> b
coe T_ExBudget_50
v1)) (Text
"\n" :: Data.Text.Text))) in
           AgdaAny -> Text
forall a b. a -> b
coe
             (case Integer -> Integer
forall a b. a -> b
coe Integer
v2 of
                Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
                       Integer
0 -> Text -> AgdaAny
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
                       Integer
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4
                Integer
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)
      T_ExBudget_50
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.printBuiltinReport
d_printBuiltinReport_274 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printBuiltinReport_274 :: T_Tree_240 -> T_ExBudget_50 -> T_Tree_240 -> Text
d_printBuiltinReport_274 ~T_Tree_240
v0 ~T_ExBudget_50
v1 T_Tree_240
v2 = T_Tree_240 -> Text
du_printBuiltinReport_274 T_Tree_240
v2
du_printBuiltinReport_274 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printBuiltinReport_274 :: T_Tree_240 -> Text
du_printBuiltinReport_274 T_Tree_240
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v1 ->
            (Text -> Text -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
              ((T_Builtin_2 -> T_ExBudget_50 -> Text)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_Builtin_2 -> T_ExBudget_50 -> Text
du_printBuiltinCost_266 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                 ((T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T_Tree_240 -> T_ExBudgetCategory_34 -> T_ExBudget_50
d_lookup_156 (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v0)
                    ((T_Builtin_2 -> T_Vec_24 -> T_ExBudgetCategory_34)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Builtin_2 -> T_Vec_24 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
                       ((Integer -> AgdaAny -> T_Vec_24) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          Integer -> AgdaAny -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490
                          ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
                          ((T__'8866''9839'_4 -> AgdaAny -> T_Value_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                             T__'8866''9839'_4 -> AgdaAny -> T_Value_14
MAlonzo.Code.Untyped.CEK.C_V'45'con_50
                             ((T_AtomicTyCon_6 -> T__'8866''9839'_4) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                T_AtomicTyCon_6 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_atomic_12
                                (T_AtomicTyCon_6 -> AgdaAny
forall a b. a -> b
coe T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14))
                             (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))))))
      (Text -> AgdaAny
forall a b. a -> b
coe (Text
"" :: Data.Text.Text))
      ([T_Builtin_2] -> AgdaAny
forall a b. a -> b
coe [T_Builtin_2]
MAlonzo.Code.Builtin.d_builtinList_402)
-- Cost._.formatTimePicoseconds
d_formatTimePicoseconds_282 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
  T_ExBudget_50 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_formatTimePicoseconds_282 :: T_Tree_240 -> T_ExBudget_50 -> Double -> Text
d_formatTimePicoseconds_282 ~T_Tree_240
v0 ~T_ExBudget_50
v1 Double
v2
  = Double -> Text
du_formatTimePicoseconds_282 Double
v2
du_formatTimePicoseconds_282 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_formatTimePicoseconds_282 :: Double -> Text
du_formatTimePicoseconds_282 Double
v0
  = (Bool -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
      Bool -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Bool.Base.du_if_then_else__42
      ((Double -> Double -> Bool) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
         Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
         (Double
1.0e12 :: Double) Double
v0)
      ((Text -> AgdaAny) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Text -> AgdaAny
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f s" :: Data.Text.Text)
         ((Double -> Double -> Double) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
            Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
            (Double
1.0e12 :: Double)))
      ((Bool -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Bool.Base.du_if_then_else__42
         ((Double -> Double -> Bool) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
            Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
            (Double
1.0e9 :: Double) Double
v0)
         ((Text -> AgdaAny) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            Text -> AgdaAny
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f ms" :: Data.Text.Text)
            ((Double -> Double -> Double) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
               Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
               (Double
1.0e9 :: Double)))
         ((Bool -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            Bool -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Bool.Base.du_if_then_else__42
            ((Double -> Double -> Bool) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
               Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
               (Double
1000000.0 :: Double) Double
v0)
            ((Text -> AgdaAny) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               Text -> AgdaAny
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f \956s" :: Data.Text.Text)
               ((Double -> Double -> Double) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
                  Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
                  (Double
1000000.0 :: Double)))
            ((Bool -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               Bool -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Bool.Base.du_if_then_else__42
               ((Double -> Double -> Bool) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
                  Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
                  (Double
1000.0 :: Double) Double
v0)
               ((Text -> AgdaAny) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  Text -> AgdaAny
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f ns" :: Data.Text.Text)
                  ((Double -> Double -> Double) -> Double -> Double -> AgdaAny
forall a b. a -> b
coe
                     Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
                     (Double
1000.0 :: Double)))
               ((Text -> AgdaAny) -> Text -> Double -> AgdaAny
forall a b. a -> b
coe
                  Text -> AgdaAny
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f ps" :: Data.Text.Text)
                  Double
v0))))