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