{-# 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.ExBudget
d_ExBudget_52 :: T_Level_18
d_ExBudget_52 = ()
data T_ExBudget_52 = C_mkExBudget_62 Integer Integer
-- Cost.ExBudget.ExCPU
d_ExCPU_58 :: T_ExBudget_52 -> Integer
d_ExCPU_58 :: T_ExBudget_52 -> Integer
d_ExCPU_58 T_ExBudget_52
v0
  = case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0 of
      C_mkExBudget_62 Integer
v1 Integer
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v1
      T_ExBudget_52
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.ExBudget.ExMem
d_ExMem_60 :: T_ExBudget_52 -> Integer
d_ExMem_60 :: T_ExBudget_52 -> Integer
d_ExMem_60 T_ExBudget_52
v0
  = case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0 of
      C_mkExBudget_62 Integer
v1 Integer
v2 -> Integer -> Integer
forall a b. a -> b
coe Integer
v2
      T_ExBudget_52
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.fromHExBudget
d_fromHExBudget_64 ::
  MAlonzo.Code.Cost.Raw.T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64 :: T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64 T_HExBudget_6
v0
  = (Integer -> Integer -> T_ExBudget_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe
      Integer -> Integer -> T_ExBudget_52
C_mkExBudget_62 ((T_HExBudget_6 -> Integer) -> T_HExBudget_6 -> Any
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 -> Any
forall a b. a -> b
coe T_HExBudget_6 -> Integer
MAlonzo.Code.Cost.Raw.d_getMemoryCost_30 T_HExBudget_6
v0)
-- Cost.ε€
d_ε'8364'_68 :: T_ExBudget_52
d_ε'8364'_68 :: T_ExBudget_52
d_ε'8364'_68
  = (Integer -> Integer -> T_ExBudget_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe Integer -> Integer -> T_ExBudget_52
C_mkExBudget_62 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
-- Cost._∙€_
d__'8729''8364'__70 ::
  T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70 :: T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70 T_ExBudget_52
v0 T_ExBudget_52
v1
  = case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0 of
      C_mkExBudget_62 Integer
v2 Integer
v3
        -> case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v1 of
             C_mkExBudget_62 Integer
v4 Integer
v5
               -> (Integer -> Integer -> T_ExBudget_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe
                    Integer -> Integer -> T_ExBudget_52
C_mkExBudget_62 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                    ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v5))
             T_ExBudget_52
_ -> T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ExBudget_52
_ -> T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.isMonoidExBudget
d_isMonoidExBudget_80 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_isMonoidExBudget_80 :: T_IsMonoid_686
d_isMonoidExBudget_80
  = (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> Any -> Any -> T_IsMonoid_686
forall a b. a -> b
coe
      T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
      ((T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472)
-> Any -> Any -> Any
forall a b. a -> b
coe
         T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
         ((T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsMagma_176)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any) -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
            (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
               T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
            Any
forall a. a
erased)
         Any
forall a. a
erased)
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased)
-- Cost.builtinCost
d_builtinCost_96 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Cost.Model.T_BuiltinModel_60 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> T_ExBudget_52
d_builtinCost_96 :: T_Builtin_2 -> T_BuiltinModel_60 -> T_Vec_28 -> T_ExBudget_52
d_builtinCost_96 T_Builtin_2
v0 T_BuiltinModel_60
v1 T_Vec_28
v2
  = (Integer -> Integer -> T_ExBudget_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe
      Integer -> Integer -> T_ExBudget_52
C_mkExBudget_62
      ((Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer
MAlonzo.Code.Cost.Model.d_runModel_94
         ((T_Builtin_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0))
         ((T_BuiltinModel_60 -> T_CostingModel_8) -> Any -> Any
forall a b. a -> b
coe T_BuiltinModel_60 -> T_CostingModel_8
MAlonzo.Code.Cost.Model.d_costingCPU_68 (T_BuiltinModel_60 -> Any
forall a b. a -> b
coe T_BuiltinModel_60
v1)) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2))
      ((Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer
MAlonzo.Code.Cost.Model.d_runModel_94
         ((T_Builtin_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0))
         ((T_BuiltinModel_60 -> T_CostingModel_8) -> Any -> Any
forall a b. a -> b
coe T_BuiltinModel_60 -> T_CostingModel_8
MAlonzo.Code.Cost.Model.d_costingMem_70 (T_BuiltinModel_60 -> Any
forall a b. a -> b
coe T_BuiltinModel_60
v1)) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2))
-- Cost.CostModel
d_CostModel_104 :: ()
d_CostModel_104 :: T_Level_18
d_CostModel_104 = T_Level_18
forall a. a
erased
-- Cost.cekMachineCostFunction
d_cekMachineCostFunction_106 ::
  MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4 ->
  MAlonzo.Code.Cost.Base.T_StepKind_6 -> T_ExBudget_52
d_cekMachineCostFunction_106 :: T_HCekMachineCosts_4 -> T_StepKind_6 -> T_ExBudget_52
d_cekMachineCostFunction_106 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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
             T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
             ((T_HCekMachineCosts_4 -> T_HExBudget_6)
-> T_HCekMachineCosts_4 -> Any
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_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.exBudgetCategoryCost
d_exBudgetCategoryCost_126 ::
  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_52
d_exBudgetCategoryCost_126 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_52
d_exBudgetCategoryCost_126 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)
-> (Any, Any)
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 Any
v2 Any
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_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_StepKind_6 -> T_ExBudget_52
d_cekMachineCostFunction_106 (Any -> Any
forall a b. a -> b
coe Any
v2) (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
v4)
             MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 T_Builtin_2
v4 T_Vec_28
v5
               -> (T_Builtin_2 -> T_BuiltinModel_60 -> T_Vec_28 -> T_ExBudget_52)
-> Any -> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe T_Builtin_2 -> T_BuiltinModel_60 -> T_Vec_28 -> T_ExBudget_52
d_builtinCost_96 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v4) (Any -> T_Builtin_2 -> Any
forall a b. a -> b
coe Any
v3 T_Builtin_2
v4) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v5)
             T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStartup_42
               -> (T_HExBudget_6 -> T_ExBudget_52) -> Any -> T_ExBudget_52
forall a b. a -> b
coe
                    T_HExBudget_6 -> T_ExBudget_52
d_fromHExBudget_64
                    ((T_HCekMachineCosts_4 -> T_HExBudget_6) -> Any -> Any
forall a b. a -> b
coe T_HCekMachineCosts_4 -> T_HExBudget_6
MAlonzo.Code.Cost.Raw.d_getCekStartupCost_8 Any
v2)
             T_ExBudgetCategory_34
_ -> T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      (Any, Any)
_ -> T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.machineParameters
d_machineParameters_140 ::
  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_140 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_MachineParameters_46
d_machineParameters_140 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0
  = ((T_ExBudgetCategory_34 -> Any)
 -> Any
 -> (Any -> Any -> Any)
 -> T_IsMonoid_686
 -> T_MachineParameters_46)
-> Any -> Any -> Any -> Any -> T_MachineParameters_46
forall a b. a -> b
coe
      (T_ExBudgetCategory_34 -> Any)
-> Any
-> (Any -> Any -> Any)
-> T_IsMonoid_686
-> 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_52)
-> Any -> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_52
d_exBudgetCategoryCost_126 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0)) (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
d_ε'8364'_68)
      ((T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52) -> Any
forall a b. a -> b
coe T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70) (T_IsMonoid_686 -> Any
forall a b. a -> b
coe T_IsMonoid_686
d_isMonoidExBudget_80)
-- Cost.countingReport
d_countingReport_144 ::
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_countingReport_144 :: T_ExBudget_52 -> Text
d_countingReport_144 T_ExBudget_52
v0
  = case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0 of
      C_mkExBudget_62 Integer
v1 Integer
v2
        -> (Text -> Text -> Text) -> Text -> Any -> 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) -> Any -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                ((Integer -> Text) -> Integer -> Any
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
                ((Text -> Text -> Text) -> Text -> Any -> Any
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) -> Integer -> Any
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v2)))
      T_ExBudget_52
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.mkKeyFromExBudgetCategory
d_mkKeyFromExBudgetCategory_150 ::
  MAlonzo.Code.Cost.Base.T_ExBudgetCategory_34 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_mkKeyFromExBudgetCategory_150 :: T_ExBudgetCategory_34 -> Text
d_mkKeyFromExBudgetCategory_150 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_28
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_156 :: ()
d_TallyingBudget_156 :: T_Level_18
d_TallyingBudget_156 = T_Level_18
forall a. a
erased
-- Cost.lookup
d_lookup_158 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  MAlonzo.Code.Cost.Base.T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158 :: T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158 T_Tree_254
v0 T_ExBudgetCategory_34
v1
  = let v2 :: t
v2
          = (T_StrictTotalOrder_1036
 -> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any)
-> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
              T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
MAlonzo.Code.Data.Tree.AVL.du_lookup_312
              (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe
                 T_StrictTotalOrder_1036
MAlonzo.Code.Data.String.Properties.d_'60''45'strictTotalOrder'45''8776'_76)
              (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v0)
              ((T_ExBudgetCategory_34 -> Text) -> Any -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34 -> Text
d_mkKeyFromExBudgetCategory_150 (T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34
v1)) in
    Any -> T_ExBudget_52
forall a b. a -> b
coe
      (case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v2 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v3 -> Any -> Any
forall a b. a -> b
coe Any
v3
         Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
d_ε'8364'_68
         Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Cost.εT
d_εT_178 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_254 T_ExBudget_52
d_εT_178 :: T__'215'__364 T_Tree_254 T_ExBudget_52
d_εT_178
  = (Any -> Any -> (Any, Any))
-> Any -> Any -> T__'215'__364 T_Tree_254 T_ExBudget_52
forall a b. a -> b
coe
      Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
      (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
MAlonzo.Code.Data.Tree.AVL.Map.du_empty_198)
      (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
d_ε'8364'_68)
-- Cost._∙T_
d__'8729'T__180 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_254 T_ExBudget_52 ->
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_254 T_ExBudget_52 ->
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_254 T_ExBudget_52
d__'8729'T__180 :: T__'215'__364 T_Tree_254 T_ExBudget_52
-> T__'215'__364 T_Tree_254 T_ExBudget_52
-> T__'215'__364 T_Tree_254 T_ExBudget_52
d__'8729'T__180 T__'215'__364 T_Tree_254 T_ExBudget_52
v0 T__'215'__364 T_Tree_254 T_ExBudget_52
v1
  = case T__'215'__364 T_Tree_254 T_ExBudget_52 -> (Any, Any)
forall a b. a -> b
coe T__'215'__364 T_Tree_254 T_ExBudget_52
v0 of
      MAlonzo.Code.Utils.C__'44'__378 Any
v2 Any
v3
        -> case T__'215'__364 T_Tree_254 T_ExBudget_52 -> (Any, Any)
forall a b. a -> b
coe T__'215'__364 T_Tree_254 T_ExBudget_52
v1 of
             MAlonzo.Code.Utils.C__'44'__378 Any
v4 Any
v5
               -> (Any -> Any -> (Any, Any))
-> Any -> Any -> T__'215'__364 T_Tree_254 T_ExBudget_52
forall a b. a -> b
coe
                    Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
                    ((T_StrictTotalOrder_1036
 -> (Any -> Maybe Any -> Any)
 -> T_Tree_254
 -> T_Tree_254
 -> T_Tree_254)
-> T_StrictTotalOrder_1036 -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_StrictTotalOrder_1036
-> (Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.Map.du_unionWith_232
                       T_StrictTotalOrder_1036
MAlonzo.Code.Data.String.Properties.d_'60''45'strictTotalOrder'45''8776'_76
                       ((T_ExBudget_52 -> Maybe T_ExBudget_52 -> T_ExBudget_52) -> Any
forall a b. a -> b
coe T_ExBudget_52 -> Maybe T_ExBudget_52 -> T_ExBudget_52
du_u_194) Any
v2 Any
v4)
                    ((T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52)
-> Any -> Any -> Any
forall a b. a -> b
coe T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70 (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v5))
             (Any, Any)
_ -> T__'215'__364 T_Tree_254 T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
      (Any, Any)
_ -> T__'215'__364 T_Tree_254 T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.u
d_u_194 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  T_ExBudget_52 -> Maybe T_ExBudget_52 -> T_ExBudget_52
d_u_194 :: T_Tree_254
-> T_ExBudget_52
-> T_Tree_254
-> T_ExBudget_52
-> T_ExBudget_52
-> Maybe T_ExBudget_52
-> T_ExBudget_52
d_u_194 ~T_Tree_254
v0 ~T_ExBudget_52
v1 ~T_Tree_254
v2 ~T_ExBudget_52
v3 T_ExBudget_52
v4 Maybe T_ExBudget_52
v5 = T_ExBudget_52 -> Maybe T_ExBudget_52 -> T_ExBudget_52
du_u_194 T_ExBudget_52
v4 Maybe T_ExBudget_52
v5
du_u_194 :: T_ExBudget_52 -> Maybe T_ExBudget_52 -> T_ExBudget_52
du_u_194 :: T_ExBudget_52 -> Maybe T_ExBudget_52 -> T_ExBudget_52
du_u_194 T_ExBudget_52
v0 Maybe T_ExBudget_52
v1
  = case Maybe T_ExBudget_52 -> Maybe Any
forall a b. a -> b
coe Maybe T_ExBudget_52
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v2
        -> (T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70 (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
v0) (Any -> Any
forall a b. a -> b
coe Any
v2)
      Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0
      Maybe Any
_ -> T_ExBudget_52
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.TallyingBudget-assoc
d_TallyingBudget'45'assoc_202 :: a
d_TallyingBudget'45'assoc_202
  = [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'_204 :: a
d_Tallying'45'budget'45'identity'691'_204
  = [Char] -> a
forall a. HasCallStack => [Char] -> a
error
      [Char]
"MAlonzo Runtime Error: postulate evaluated: Cost.Tallying-budget-identity\691"
-- Cost.isMonoidTallyingBudget
d_isMonoidTallyingBudget_206 ::
  MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
d_isMonoidTallyingBudget_206 :: T_IsMonoid_686
d_isMonoidTallyingBudget_206
  = (T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686)
-> Any -> Any -> T_IsMonoid_686
forall a b. a -> b
coe
      T_IsSemigroup_472 -> T_Σ_14 -> T_IsMonoid_686
MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
      ((T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472)
-> Any -> Any -> Any
forall a b. a -> b
coe
         T_IsMagma_176 -> (Any -> Any -> Any -> Any) -> T_IsSemigroup_472
MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
         ((T_IsEquivalence_26
 -> (Any -> Any -> Any -> Any -> Any -> Any -> Any)
 -> T_IsMagma_176)
-> Any -> Any -> Any
forall a b. a -> b
coe
            T_IsEquivalence_26
-> (Any -> Any -> Any -> Any -> Any -> Any -> Any) -> T_IsMagma_176
MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
            (T_IsEquivalence_26 -> Any
forall a b. a -> b
coe
               T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
            Any
forall a. a
erased)
         Any
forall a. a
erased)
      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
forall a. a
erased Any
forall a. a
erased)
-- Cost.tallyingCekMachineCost
d_tallyingCekMachineCost_212 ::
  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_254 T_ExBudget_52
d_tallyingCekMachineCost_212 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T__'215'__364 T_Tree_254 T_ExBudget_52
d_tallyingCekMachineCost_212 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0 T_ExBudgetCategory_34
v1
  = (Any -> Any -> (Any, Any))
-> Any -> Any -> T__'215'__364 T_Tree_254 T_ExBudget_52
forall a b. a -> b
coe
      Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378
      ((Any -> Any -> T_Tree_254) -> Text -> T_ExBudget_52 -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.Map.du_singleton_200
         (T_ExBudgetCategory_34 -> Text
d_mkKeyFromExBudgetCategory_150 (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_52
d_exBudgetCategoryCost_126 (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_52)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_ExBudgetCategory_34 -> T_ExBudget_52
d_exBudgetCategoryCost_126 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0) (T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34
v1))
-- Cost.tallyingMachineParameters
d_tallyingMachineParameters_220 ::
  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_220 :: T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> T_MachineParameters_46
d_tallyingMachineParameters_220 T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0
  = ((T_ExBudgetCategory_34 -> Any)
 -> Any
 -> (Any -> Any -> Any)
 -> T_IsMonoid_686
 -> T_MachineParameters_46)
-> Any -> Any -> Any -> Any -> T_MachineParameters_46
forall a b. a -> b
coe
      (T_ExBudgetCategory_34 -> Any)
-> Any
-> (Any -> Any -> Any)
-> T_IsMonoid_686
-> 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_254 T_ExBudget_52)
-> Any -> Any
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_254 T_ExBudget_52
d_tallyingCekMachineCost_212 (T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
-> Any
forall a b. a -> b
coe T__'215'__364
  T_HCekMachineCosts_4 (T_Builtin_2 -> T_BuiltinModel_60)
v0)) (T__'215'__364 T_Tree_254 T_ExBudget_52 -> Any
forall a b. a -> b
coe T__'215'__364 T_Tree_254 T_ExBudget_52
d_εT_178)
      ((T__'215'__364 T_Tree_254 T_ExBudget_52
 -> T__'215'__364 T_Tree_254 T_ExBudget_52
 -> T__'215'__364 T_Tree_254 T_ExBudget_52)
-> Any
forall a b. a -> b
coe T__'215'__364 T_Tree_254 T_ExBudget_52
-> T__'215'__364 T_Tree_254 T_ExBudget_52
-> T__'215'__364 T_Tree_254 T_ExBudget_52
d__'8729'T__180) (T_IsMonoid_686 -> Any
forall a b. a -> b
coe T_IsMonoid_686
d_isMonoidTallyingBudget_206)
-- Cost.tallyingReport
d_tallyingReport_224 ::
  MAlonzo.Code.Utils.T__'215'__364
    MAlonzo.Code.Data.Tree.AVL.T_Tree_254 T_ExBudget_52 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_tallyingReport_224 :: T__'215'__364 T_Tree_254 T_ExBudget_52 -> Text
d_tallyingReport_224 T__'215'__364 T_Tree_254 T_ExBudget_52
v0
  = case T__'215'__364 T_Tree_254 T_ExBudget_52 -> (Any, Any)
forall a b. a -> b
coe T__'215'__364 T_Tree_254 T_ExBudget_52
v0 of
      MAlonzo.Code.Utils.C__'44'__378 Any
v1 Any
v2
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (T_ExBudget_52 -> Text
d_countingReport_144 (Any -> T_ExBudget_52
forall a b. a -> b
coe Any
v2))
             ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      ((T_Tree_254 -> Text) -> Any -> Any
forall a b. a -> b
coe T_Tree_254 -> Text
du_printStepReport_260 (Any -> Any
forall a b. a -> b
coe Any
v1))
                      ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                               Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                               ((T_ExBudget_52 -> Text) -> Any -> Any
forall a b. a -> b
coe
                                  T_ExBudget_52 -> Text
du_budgetToString_248
                                  ((T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                     T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158 (Any -> Any
forall a b. a -> b
coe Any
v1)
                                     (T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStartup_42)))
                               ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                                        Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                        ((T_ExBudget_52 -> Text) -> Any -> Any
forall a b. a -> b
coe
                                           T_ExBudget_52 -> Text
du_budgetToString_248
                                           ((T_Tree_254 -> T_ExBudget_52) -> Any -> Any
forall a b. a -> b
coe T_Tree_254 -> T_ExBudget_52
du_totalComputeCost_234 (Any -> Any
forall a b. a -> b
coe Any
v1)))
                                        ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                 ((T_Tree_254 -> Text) -> Any -> Any
forall a b. a -> b
coe T_Tree_254 -> Text
du_printBuiltinReport_276 (Any -> Any
forall a b. a -> b
coe Any
v1))
                                                 ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                          Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                          ((T_ExBudget_52 -> Text) -> Any -> Any
forall a b. a -> b
coe
                                                             T_ExBudget_52 -> Text
du_budgetToString_248
                                                             ((T_Tree_254 -> T_ExBudget_52) -> Any -> Any
forall a b. a -> b
coe
                                                                T_Tree_254 -> T_ExBudget_52
du_totalBuiltinCosts_236 (Any -> Any
forall a b. a -> b
coe Any
v1)))
                                                          ((Text -> Text -> Text) -> Text -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                ((Text -> Any) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                                   Text -> Any
MAlonzo.Code.Text.Printf.d_printf_24
                                                                   (Text
"Time spent executing builtins:  %f%%\n"
                                                                    ::
                                                                    Data.Text.Text)
                                                                   ((Double -> Double -> Double) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                      Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54
                                                                      ((Double -> Double -> Double) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                         Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatTimes_52
                                                                         ((Integer -> Double) -> Integer -> Any
forall a b. a -> b
coe
                                                                            Integer -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primNatToFloat_24
                                                                            (Integer
100 :: Integer))
                                                                         ((T_ExBudget_52 -> Double) -> Any -> Any
forall a b. a -> b
coe
                                                                            T_ExBudget_52 -> Double
du_getCPU_244
                                                                            ((T_Tree_254 -> T_ExBudget_52) -> Any -> Any
forall a b. a -> b
coe
                                                                               T_Tree_254 -> T_ExBudget_52
du_totalBuiltinCosts_236
                                                                               (Any -> Any
forall a b. a -> b
coe Any
v1))))
                                                                      ((T_ExBudget_52 -> Double) -> Any -> Any
forall a b. a -> b
coe T_ExBudget_52 -> Double
du_getCPU_244 (Any -> Any
forall a b. a -> b
coe Any
v2))))
                                                                ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                            ((T_ExBudget_52 -> Text) -> Any -> Any
forall a b. a -> b
coe
                                                                               T_ExBudget_52 -> Text
du_budgetToString_248
                                                                               (Any -> Any
forall a b. a -> b
coe Any
v2))
                                                                            ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any -> Any
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) -> Any -> Any
forall a b. a -> b
coe
                                                                                     Double -> Text
du_formatTimePicoseconds_284
                                                                                     ((T_ExBudget_52 -> Double) -> Any -> Any
forall a b. a -> b
coe
                                                                                        T_ExBudget_52 -> Double
du_getCPU_244
                                                                                        (Any -> Any
forall a b. a -> b
coe
                                                                                           Any
v2))))))))))))))))))))))))))
      (Any, Any)
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.totalComputeCost
d_totalComputeCost_234 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 -> T_ExBudget_52
d_totalComputeCost_234 :: T_Tree_254 -> T_ExBudget_52 -> T_ExBudget_52
d_totalComputeCost_234 T_Tree_254
v0 ~T_ExBudget_52
v1 = T_Tree_254 -> T_ExBudget_52
du_totalComputeCost_234 T_Tree_254
v0
du_totalComputeCost_234 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> T_ExBudget_52
du_totalComputeCost_234 :: T_Tree_254 -> T_ExBudget_52
du_totalComputeCost_234 T_Tree_254
v0
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((Any -> T_ExBudget_52 -> T_ExBudget_52) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70
              ((T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52)
-> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe
                 T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158 (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v0)
                 ((T_StepKind_6 -> T_ExBudgetCategory_34) -> Any -> Any
forall a b. a -> b
coe T_StepKind_6 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStep_36 (Any -> Any
forall a b. a -> b
coe Any
v1)))))
      (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
d_ε'8364'_68) ([T_StepKind_6] -> Any
forall a b. a -> b
coe [T_StepKind_6]
MAlonzo.Code.Cost.Base.d_stepKindList_32)
-- Cost._.totalBuiltinCosts
d_totalBuiltinCosts_236 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 -> T_ExBudget_52
d_totalBuiltinCosts_236 :: T_Tree_254 -> T_ExBudget_52 -> T_ExBudget_52
d_totalBuiltinCosts_236 T_Tree_254
v0 ~T_ExBudget_52
v1 = T_Tree_254 -> T_ExBudget_52
du_totalBuiltinCosts_236 T_Tree_254
v0
du_totalBuiltinCosts_236 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> T_ExBudget_52
du_totalBuiltinCosts_236 :: T_Tree_254 -> T_ExBudget_52
du_totalBuiltinCosts_236 T_Tree_254
v0
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> T_ExBudget_52
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216 ((T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52) -> Any
forall a b. a -> b
coe T_ExBudget_52 -> T_ExBudget_52 -> T_ExBudget_52
d__'8729''8364'__70)
      (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
d_ε'8364'_68)
      (((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
         ((Any -> T_ExBudget_52) -> Any
forall a b. a -> b
coe
            (\ Any
v1 ->
               T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158
                 (T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v0)
                 ((T_Builtin_2 -> T_Vec_28 -> T_ExBudgetCategory_34)
-> Any -> Any -> T_ExBudgetCategory_34
forall a b. a -> b
coe
                    T_Builtin_2 -> T_Vec_28 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 (Any -> Any
forall a b. a -> b
coe Any
v1)
                    ((Integer -> Any -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Integer -> Any -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444
                       ((T_Builtin_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (Any -> Any
forall a b. a -> b
coe Any
v1))
                       ((T__'8866''9839'_4 -> Any -> T_Value_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                          T__'8866''9839'_4 -> Any -> T_Value_14
MAlonzo.Code.Untyped.CEK.C_V'45'con_50
                          ((T_AtomicTyCon_6 -> T__'8866''9839'_4) -> Any -> Any
forall a b. a -> b
coe
                             T_AtomicTyCon_6 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_atomic_12
                             (T_AtomicTyCon_6 -> Any
forall a b. a -> b
coe T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14))
                          (T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))))
         ([T_Builtin_2] -> Any
forall a b. a -> b
coe [T_Builtin_2]
MAlonzo.Code.Builtin.d_builtinList_402))
-- Cost._.getCPU
d_getCPU_244 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.Float.T_Float_6
d_getCPU_244 :: T_Tree_254 -> T_ExBudget_52 -> T_ExBudget_52 -> Double
d_getCPU_244 ~T_Tree_254
v0 ~T_ExBudget_52
v1 T_ExBudget_52
v2 = T_ExBudget_52 -> Double
du_getCPU_244 T_ExBudget_52
v2
du_getCPU_244 ::
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.Float.T_Float_6
du_getCPU_244 :: T_ExBudget_52 -> Double
du_getCPU_244 T_ExBudget_52
v0
  = (Integer -> Double) -> Integer -> Double
forall a b. a -> b
coe
      Integer -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primNatToFloat_24
      (T_ExBudget_52 -> Integer
d_ExCPU_58 (T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0))
-- Cost._.budgetToString
d_budgetToString_248 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_budgetToString_248 :: T_Tree_254 -> T_ExBudget_52 -> T_ExBudget_52 -> Text
d_budgetToString_248 ~T_Tree_254
v0 ~T_ExBudget_52
v1 T_ExBudget_52
v2 = T_ExBudget_52 -> Text
du_budgetToString_248 T_ExBudget_52
v2
du_budgetToString_248 ::
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_budgetToString_248 :: T_ExBudget_52 -> Text
du_budgetToString_248 T_ExBudget_52
v0
  = case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v0 of
      C_mkExBudget_62 Integer
v1 Integer
v2
        -> (Text -> Text -> Text) -> Text -> Any -> 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_60
                (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
15 :: Integer))
                ((Integer -> Text) -> Integer -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1))
             ((Text -> Text -> Text) -> Text -> Text -> Any
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_60
                   (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
15 :: Integer))
                   ((Integer -> Text) -> Integer -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v2)))
      T_ExBudget_52
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.printStepCost
d_printStepCost_254 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  MAlonzo.Code.Cost.Base.T_StepKind_6 ->
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printStepCost_254 :: T_Tree_254
-> T_ExBudget_52 -> T_StepKind_6 -> T_ExBudget_52 -> Text
d_printStepCost_254 ~T_Tree_254
v0 ~T_ExBudget_52
v1 T_StepKind_6
v2 T_ExBudget_52
v3 = T_StepKind_6 -> T_ExBudget_52 -> Text
du_printStepCost_254 T_StepKind_6
v2 T_ExBudget_52
v3
du_printStepCost_254 ::
  MAlonzo.Code.Cost.Base.T_StepKind_6 ->
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printStepCost_254 :: T_StepKind_6 -> T_ExBudget_52 -> Text
du_printStepCost_254 T_StepKind_6
v0 T_ExBudget_52
v1
  = (Text -> Text -> Text) -> Text -> Any -> 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_70
         (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
10 :: Integer))
         ((T_StepKind_6 -> Text) -> Any -> Text
forall a b. a -> b
coe T_StepKind_6 -> Text
MAlonzo.Code.Cost.Base.d_showStepKind_28 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
v0)))
      ((Text -> Text -> Text) -> Text -> Any -> Any
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 -> Any
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_60
               (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
20 :: Integer))
               ((T_ExBudget_52 -> Text) -> Any -> Text
forall a b. a -> b
coe T_ExBudget_52 -> Text
du_budgetToString_248 (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
v1)))
            (Text
"\n" :: Data.Text.Text)))
-- Cost._.printStepReport
d_printStepReport_260 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printStepReport_260 :: T_Tree_254 -> T_ExBudget_52 -> T_Tree_254 -> Text
d_printStepReport_260 ~T_Tree_254
v0 ~T_ExBudget_52
v1 T_Tree_254
v2 = T_Tree_254 -> Text
du_printStepReport_260 T_Tree_254
v2
du_printStepReport_260 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printStepReport_260 :: T_Tree_254 -> Text
du_printStepReport_260 T_Tree_254
v0
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Text
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (Text -> Text -> Text) -> Any -> Any
forall a b. a -> b
coe
              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
              ((T_StepKind_6 -> T_ExBudget_52 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                 T_StepKind_6 -> T_ExBudget_52 -> Text
du_printStepCost_254 (Any -> Any
forall a b. a -> b
coe Any
v1)
                 ((T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158 (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v0)
                    ((T_StepKind_6 -> T_ExBudgetCategory_34) -> Any -> Any
forall a b. a -> b
coe T_StepKind_6 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BStep_36 (Any -> Any
forall a b. a -> b
coe Any
v1))))))
      (Text -> Any
forall a b. a -> b
coe (Text
"" :: Data.Text.Text))
      ([T_StepKind_6] -> Any
forall a b. a -> b
coe [T_StepKind_6]
MAlonzo.Code.Cost.Base.d_stepKindList_32)
-- Cost._.printBuiltinCost
d_printBuiltinCost_268 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printBuiltinCost_268 :: T_Tree_254 -> T_ExBudget_52 -> T_Builtin_2 -> T_ExBudget_52 -> Text
d_printBuiltinCost_268 ~T_Tree_254
v0 ~T_ExBudget_52
v1 T_Builtin_2
v2 T_ExBudget_52
v3
  = T_Builtin_2 -> T_ExBudget_52 -> Text
du_printBuiltinCost_268 T_Builtin_2
v2 T_ExBudget_52
v3
du_printBuiltinCost_268 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  T_ExBudget_52 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printBuiltinCost_268 :: T_Builtin_2 -> T_ExBudget_52 -> Text
du_printBuiltinCost_268 T_Builtin_2
v0 T_ExBudget_52
v1
  = case T_ExBudget_52 -> T_ExBudget_52
forall a b. a -> b
coe T_ExBudget_52
v1 of
      C_mkExBudget_62 Integer
v2 Integer
v3
        -> let v4 :: t
v4
                 = (Text -> Text -> Text) -> Text -> Any -> 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_70
                        (Char -> Char
forall a b. a -> b
coe Char
' ') (Integer -> Integer
forall a b. a -> b
coe (Integer
22 :: Integer))
                        ((T_Builtin_2 -> Text) -> Any -> Text
forall a b. a -> b
coe T_Builtin_2 -> Text
MAlonzo.Code.Builtin.d_showBuiltin_400 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0)))
                     ((Text -> Text -> Text) -> Text -> Any -> Any
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) -> Any -> Text -> Any
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           ((T_ExBudget_52 -> Text) -> Any -> Any
forall a b. a -> b
coe T_ExBudget_52 -> Text
du_budgetToString_248 (T_ExBudget_52 -> Any
forall a b. a -> b
coe T_ExBudget_52
v1)) (Text
"\n" :: Data.Text.Text))) in
           Any -> 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 -> Any
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
                       Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4
                Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
      T_ExBudget_52
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost._.printBuiltinReport
d_printBuiltinReport_276 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_printBuiltinReport_276 :: T_Tree_254 -> T_ExBudget_52 -> T_Tree_254 -> Text
d_printBuiltinReport_276 ~T_Tree_254
v0 ~T_ExBudget_52
v1 T_Tree_254
v2 = T_Tree_254 -> Text
du_printBuiltinReport_276 T_Tree_254
v2
du_printBuiltinReport_276 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_printBuiltinReport_276 :: T_Tree_254 -> Text
du_printBuiltinReport_276 T_Tree_254
v0
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Text
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (Text -> Text -> Text) -> Any -> Any
forall a b. a -> b
coe
              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
              ((T_Builtin_2 -> T_ExBudget_52 -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                 T_Builtin_2 -> T_ExBudget_52 -> Text
du_printBuiltinCost_268 (Any -> Any
forall a b. a -> b
coe Any
v1)
                 ((T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52)
-> Any -> Any -> Any
forall a b. a -> b
coe
                    T_Tree_254 -> T_ExBudgetCategory_34 -> T_ExBudget_52
d_lookup_158 (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v0)
                    ((T_Builtin_2 -> T_Vec_28 -> T_ExBudgetCategory_34)
-> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Builtin_2 -> T_Vec_28 -> T_ExBudgetCategory_34
MAlonzo.Code.Cost.Base.C_BBuiltinApp_40 (Any -> Any
forall a b. a -> b
coe Any
v1)
                       ((Integer -> Any -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Integer -> Any -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444
                          ((T_Builtin_2 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_arity_280 (Any -> Any
forall a b. a -> b
coe Any
v1))
                          ((T__'8866''9839'_4 -> Any -> T_Value_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                             T__'8866''9839'_4 -> Any -> T_Value_14
MAlonzo.Code.Untyped.CEK.C_V'45'con_50
                             ((T_AtomicTyCon_6 -> T__'8866''9839'_4) -> Any -> Any
forall a b. a -> b
coe
                                T_AtomicTyCon_6 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_atomic_12
                                (T_AtomicTyCon_6 -> Any
forall a b. a -> b
coe T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14))
                             (T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))))))))
      (Text -> Any
forall a b. a -> b
coe (Text
"" :: Data.Text.Text))
      ([T_Builtin_2] -> Any
forall a b. a -> b
coe [T_Builtin_2]
MAlonzo.Code.Builtin.d_builtinList_402)
-- Cost._.formatTimePicoseconds
d_formatTimePicoseconds_284 ::
  MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
  T_ExBudget_52 ->
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_formatTimePicoseconds_284 :: T_Tree_254 -> T_ExBudget_52 -> Double -> Text
d_formatTimePicoseconds_284 ~T_Tree_254
v0 ~T_ExBudget_52
v1 Double
v2
  = Double -> Text
du_formatTimePicoseconds_284 Double
v2
du_formatTimePicoseconds_284 ::
  MAlonzo.Code.Agda.Builtin.Float.T_Float_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_formatTimePicoseconds_284 :: Double -> Text
du_formatTimePicoseconds_284 Double
v0
  = (Bool -> Any -> Any -> Any) -> Any -> Any -> Any -> Text
forall a b. a -> b
coe
      Bool -> Any -> Any -> Any
MAlonzo.Code.Data.Bool.Base.du_if_then_else__44
      ((Double -> Double -> Bool) -> Double -> Double -> Any
forall a b. a -> b
coe
         Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
         (Double
1.0e12 :: Double) Double
v0)
      ((Text -> Any) -> Text -> Any -> Any
forall a b. a -> b
coe
         Text -> Any
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f s" :: Data.Text.Text)
         ((Double -> Double -> Double) -> Double -> Double -> Any
forall a b. a -> b
coe
            Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
            (Double
1.0e12 :: Double)))
      ((Bool -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         Bool -> Any -> Any -> Any
MAlonzo.Code.Data.Bool.Base.du_if_then_else__44
         ((Double -> Double -> Bool) -> Double -> Double -> Any
forall a b. a -> b
coe
            Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
            (Double
1.0e9 :: Double) Double
v0)
         ((Text -> Any) -> Text -> Any -> Any
forall a b. a -> b
coe
            Text -> Any
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f ms" :: Data.Text.Text)
            ((Double -> Double -> Double) -> Double -> Double -> Any
forall a b. a -> b
coe
               Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
               (Double
1.0e9 :: Double)))
         ((Bool -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            Bool -> Any -> Any -> Any
MAlonzo.Code.Data.Bool.Base.du_if_then_else__44
            ((Double -> Double -> Bool) -> Double -> Double -> Any
forall a b. a -> b
coe
               Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
               (Double
1000000.0 :: Double) Double
v0)
            ((Text -> Any) -> Text -> Any -> Any
forall a b. a -> b
coe
               Text -> Any
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f \956s" :: Data.Text.Text)
               ((Double -> Double -> Double) -> Double -> Double -> Any
forall a b. a -> b
coe
                  Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
                  (Double
1000000.0 :: Double)))
            ((Bool -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
               Bool -> Any -> Any -> Any
MAlonzo.Code.Data.Bool.Base.du_if_then_else__44
               ((Double -> Double -> Bool) -> Double -> Double -> Any
forall a b. a -> b
coe
                  Double -> Double -> Bool
MAlonzo.Code.Agda.Builtin.Float.d_primFloatInequality_8
                  (Double
1000.0 :: Double) Double
v0)
               ((Text -> Any) -> Text -> Any -> Any
forall a b. a -> b
coe
                  Text -> Any
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f ns" :: Data.Text.Text)
                  ((Double -> Double -> Double) -> Double -> Double -> Any
forall a b. a -> b
coe
                     Double -> Double -> Double
MAlonzo.Code.Agda.Builtin.Float.d_primFloatDiv_54 Double
v0
                     (Double
1000.0 :: Double)))
               ((Text -> Any) -> Text -> Double -> Any
forall a b. a -> b
coe
                  Text -> Any
MAlonzo.Code.Text.Printf.d_printf_24 (Text
"%f ps" :: Data.Text.Text)
                  Double
v0))))