{-# 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
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
d_ExBudget_52 :: T_Level_18
d_ExBudget_52 = ()
data T_ExBudget_52 = C_mkExBudget_62 Integer Integer
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
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
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)
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))
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
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)
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))
d_CostModel_104 :: ()
d_CostModel_104 :: T_Level_18
d_CostModel_104 = T_Level_18
forall a. a
erased
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
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
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)
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
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
d_TallyingBudget_156 :: ()
d_TallyingBudget_156 :: T_Level_18
d_TallyingBudget_156 = T_Level_18
forall a. a
erased
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)
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)
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
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
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"
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"
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)
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))
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)
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
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)
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))
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))
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
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)))
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)
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
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)
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))))