{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Cost.Base where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Algebra.Structures
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Data.Vec.Base
d_CostingNat_4 :: ()
d_CostingNat_4 :: ()
d_CostingNat_4 = ()
forall a. a
erased
d_StepKind_6 :: ()
d_StepKind_6 = ()
data T_StepKind_6
= C_BConst_8 | C_BVar_10 | C_BLamAbs_12 | C_BApply_14 |
C_BDelay_16 | C_BForce_18 | C_BBuiltin_20 | C_BConstr_22 |
C_BCase_24
d_showStepKind''_26 ::
T_StepKind_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showStepKind''_26 :: T_StepKind_6 -> Text
d_showStepKind''_26 T_StepKind_6
v0
= case T_StepKind_6 -> T_StepKind_6
forall a b. a -> b
coe T_StepKind_6
v0 of
T_StepKind_6
C_BConst_8 -> Text -> Text
forall a b. a -> b
coe (Text
"BConst" :: Data.Text.Text)
T_StepKind_6
C_BVar_10 -> Text -> Text
forall a b. a -> b
coe (Text
"BVar" :: Data.Text.Text)
T_StepKind_6
C_BLamAbs_12 -> Text -> Text
forall a b. a -> b
coe (Text
"BLamAbs" :: Data.Text.Text)
T_StepKind_6
C_BApply_14 -> Text -> Text
forall a b. a -> b
coe (Text
"BApply" :: Data.Text.Text)
T_StepKind_6
C_BDelay_16 -> Text -> Text
forall a b. a -> b
coe (Text
"BDelay" :: Data.Text.Text)
T_StepKind_6
C_BForce_18 -> Text -> Text
forall a b. a -> b
coe (Text
"BForce" :: Data.Text.Text)
T_StepKind_6
C_BBuiltin_20 -> Text -> Text
forall a b. a -> b
coe (Text
"BBuiltin" :: Data.Text.Text)
T_StepKind_6
C_BConstr_22 -> Text -> Text
forall a b. a -> b
coe (Text
"BConstr" :: Data.Text.Text)
T_StepKind_6
C_BCase_24 -> Text -> Text
forall a b. a -> b
coe (Text
"BCase" :: Data.Text.Text)
T_StepKind_6
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
d_showStepKind_28 ::
T_StepKind_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showStepKind_28 :: T_StepKind_6 -> Text
d_showStepKind_28 T_StepKind_6
v0
= (Any -> Maybe Any -> Any) -> Text -> Any -> Text
forall a b. a -> b
coe
Any -> Maybe Any -> Any
MAlonzo.Code.Data.Maybe.Base.du_fromMaybe_50 (Text
"" :: Data.Text.Text)
((Text -> Maybe Text) -> Text -> Any
forall a b. a -> b
coe
Text -> Maybe Text
MAlonzo.Code.Data.String.Base.d_tail_14
(T_StepKind_6 -> Text
d_showStepKind''_26 (T_StepKind_6 -> T_StepKind_6
forall a b. a -> b
coe T_StepKind_6
v0)))
d_stepKindList_32 :: [T_StepKind_6]
d_stepKindList_32 :: [T_StepKind_6]
d_stepKindList_32
= (Any -> [Any] -> [Any]) -> Any -> Any -> [T_StepKind_6]
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BConst_8)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BVar_10)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BLamAbs_12)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BApply_14)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BDelay_16)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BForce_18)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BBuiltin_20)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BConstr_22)
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_StepKind_6 -> Any
forall a b. a -> b
coe T_StepKind_6
C_BCase_24)
([Any] -> Any
forall a b. a -> b
coe [Any]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))))))))
d_ExBudgetCategory_34 :: ()
d_ExBudgetCategory_34 = ()
data T_ExBudgetCategory_34
= C_BStep_36 T_StepKind_6 |
C_BBuiltinApp_40 MAlonzo.Code.Builtin.T_Builtin_2
MAlonzo.Code.Data.Vec.Base.T_Vec_24 |
C_BStartup_42
d_MachineParameters_46 :: p -> ()
d_MachineParameters_46 p
a0 = ()
data T_MachineParameters_46
= C_MachineParameters'46'constructor_359 (T_ExBudgetCategory_34 ->
AgdaAny)
AgdaAny (AgdaAny -> AgdaAny -> AgdaAny)
MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_cekMachineCost_58 ::
T_MachineParameters_46 -> T_ExBudgetCategory_34 -> AgdaAny
d_cekMachineCost_58 :: T_MachineParameters_46 -> T_ExBudgetCategory_34 -> Any
d_cekMachineCost_58 T_MachineParameters_46
v0
= case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_358
v4 -> (T_ExBudgetCategory_34 -> Any) -> T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34 -> Any
v1
T_MachineParameters_46
_ -> T_ExBudgetCategory_34 -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_ε_60 :: T_MachineParameters_46 -> AgdaAny
d_ε_60 :: T_MachineParameters_46 -> Any
d_ε_60 T_MachineParameters_46
v0
= case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_358
v4 -> Any -> Any
forall a b. a -> b
coe Any
v2
T_MachineParameters_46
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8729'__62 ::
T_MachineParameters_46 -> AgdaAny -> AgdaAny -> AgdaAny
d__'8729'__62 :: T_MachineParameters_46 -> Any -> Any -> Any
d__'8729'__62 T_MachineParameters_46
v0
= case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_358
v4 -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
v3
T_MachineParameters_46
_ -> Any -> Any -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_costMonoid_64 ::
T_MachineParameters_46 ->
MAlonzo.Code.Algebra.Structures.T_IsMonoid_358
d_costMonoid_64 :: T_MachineParameters_46 -> T_IsMonoid_358
d_costMonoid_64 T_MachineParameters_46
v0
= case T_MachineParameters_46 -> T_MachineParameters_46
forall a b. a -> b
coe T_MachineParameters_46
v0 of
C_MachineParameters'46'constructor_359 T_ExBudgetCategory_34 -> Any
v1 Any
v2 Any -> Any -> Any
v3 T_IsMonoid_358
v4 -> T_IsMonoid_358 -> T_IsMonoid_358
forall a b. a -> b
coe T_IsMonoid_358
v4
T_MachineParameters_46
_ -> T_IsMonoid_358
forall a. a
MAlonzo.RTE.mazUnreachableError
d_startupCost_66 :: () -> T_MachineParameters_46 -> AgdaAny
d_startupCost_66 :: () -> T_MachineParameters_46 -> Any
d_startupCost_66 ~()
v0 T_MachineParameters_46
v1 = T_MachineParameters_46 -> Any
du_startupCost_66 T_MachineParameters_46
v1
du_startupCost_66 :: T_MachineParameters_46 -> AgdaAny
du_startupCost_66 :: T_MachineParameters_46 -> Any
du_startupCost_66 T_MachineParameters_46
v0
= (T_MachineParameters_46 -> T_ExBudgetCategory_34 -> Any)
-> T_MachineParameters_46 -> Any -> Any
forall a b. a -> b
coe T_MachineParameters_46 -> T_ExBudgetCategory_34 -> Any
d_cekMachineCost_58 T_MachineParameters_46
v0 (T_ExBudgetCategory_34 -> Any
forall a b. a -> b
coe T_ExBudgetCategory_34
C_BStartup_42)