{-# 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.Model 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Cost.Raw
import qualified MAlonzo.Code.Cost.Size
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Char.Properties
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.NonEmpty.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.String.Properties
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Utils
d_Intercept_4 :: ()
d_Intercept_4 :: ()
d_Intercept_4 = ()
forall a. a
erased
d_Slope_6 :: ()
d_Slope_6 :: ()
d_Slope_6 = ()
forall a. a
erased
d_CostingModel_8 :: p -> ()
d_CostingModel_8 p
a0 = ()
data T_CostingModel_8
= C_constantCost_12 Integer |
C_linearCostIn_16 MAlonzo.Code.Data.Fin.Base.T_Fin_10 Integer
Integer |
C_quadraticCostIn1_20 MAlonzo.Code.Data.Fin.Base.T_Fin_10 Integer
Integer Integer |
C_quadraticCostIn2_24 MAlonzo.Code.Data.Fin.Base.T_Fin_10
MAlonzo.Code.Data.Fin.Base.T_Fin_10 Integer Integer Integer Integer
Integer Integer Integer |
C_literalCostIn_28 MAlonzo.Code.Data.Fin.Base.T_Fin_10
T_CostingModel_8 |
C_addedSizes_32 Integer Integer |
C_multipliedSizes_36 Integer Integer |
C_minSize_40 Integer Integer | C_maxSize_44 Integer Integer |
C_twoArgumentsSubtractedSizes_46 Integer Integer Integer |
C_twoArgumentsConstAboveDiagonal_48 Integer T_CostingModel_8 |
C_twoArgumentsConstBelowDiagonal_50 Integer T_CostingModel_8 |
C_twoArgumentsConstOffDiagonal_52 Integer T_CostingModel_8 |
C_twoArgumentsLinearInYAndZ_54 Integer Integer Integer |
C_twoArgumentsLinearInMaxYZ_56 Integer Integer
d_BuiltinModel_60 :: p -> ()
d_BuiltinModel_60 p
a0 = ()
data T_BuiltinModel_60
= C_BuiltinModel'46'constructor_581 T_CostingModel_8
T_CostingModel_8
d_costingCPU_68 :: T_BuiltinModel_60 -> T_CostingModel_8
d_costingCPU_68 :: T_BuiltinModel_60 -> T_CostingModel_8
d_costingCPU_68 T_BuiltinModel_60
v0
= case T_BuiltinModel_60 -> T_BuiltinModel_60
forall a b. a -> b
coe T_BuiltinModel_60
v0 of
C_BuiltinModel'46'constructor_581 T_CostingModel_8
v1 T_CostingModel_8
v2 -> T_CostingModel_8 -> T_CostingModel_8
forall a b. a -> b
coe T_CostingModel_8
v1
T_BuiltinModel_60
_ -> T_CostingModel_8
forall a. a
MAlonzo.RTE.mazUnreachableError
d_costingMem_70 :: T_BuiltinModel_60 -> T_CostingModel_8
d_costingMem_70 :: T_BuiltinModel_60 -> T_CostingModel_8
d_costingMem_70 T_BuiltinModel_60
v0
= case T_BuiltinModel_60 -> T_BuiltinModel_60
forall a b. a -> b
coe T_BuiltinModel_60
v0 of
C_BuiltinModel'46'constructor_581 T_CostingModel_8
v1 T_CostingModel_8
v2 -> T_CostingModel_8 -> T_CostingModel_8
forall a b. a -> b
coe T_CostingModel_8
v2
T_BuiltinModel_60
_ -> T_CostingModel_8
forall a. a
MAlonzo.RTE.mazUnreachableError
d_prod_74 ::
Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_prod_74 :: Integer -> T_Vec_28 -> Integer
d_prod_74 Integer
v0
= (Integer
-> (Integer -> Any -> Any -> Any) -> Any -> T_Vec_28 -> Any)
-> Any -> Any -> Any -> T_Vec_28 -> Integer
forall a b. a -> b
coe
Integer -> (Integer -> Any -> Any -> Any) -> Any -> T_Vec_28 -> Any
MAlonzo.Code.Data.Vec.Base.du_foldr_352 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Any -> Integer -> Integer -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v1 -> Integer -> Integer -> Integer
mulInt)) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
d_maximum_78 ::
Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_maximum_78 :: Integer -> T_Vec_28 -> Integer
d_maximum_78 Integer
v0 T_Vec_28
v1
= case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v1 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v3 T_Vec_28
v4
-> (Integer
-> (Integer -> Any -> Any -> Any) -> Any -> T_Vec_28 -> Any)
-> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> (Integer -> Any -> Any -> Any) -> Any -> T_Vec_28 -> Any
MAlonzo.Code.Data.Vec.Base.du_foldr_352 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Any -> Integer -> Integer -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v5 -> Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8852'__204)) (Any -> Any
forall a b. a -> b
coe Any
v3)
(T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v4)
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_minimum_82 ::
Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_minimum_82 :: Integer -> T_Vec_28 -> Integer
d_minimum_82 Integer
v0 T_Vec_28
v1
= case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v1 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v3 T_Vec_28
v4
-> (Integer
-> (Integer -> Any -> Any -> Any) -> Any -> T_Vec_28 -> Any)
-> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> (Integer -> Any -> Any -> Any) -> Any -> T_Vec_28 -> Any
MAlonzo.Code.Data.Vec.Base.du_foldr_352 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Any -> Integer -> Integer -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v5 -> Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8851'__232)) (Any -> Any
forall a b. a -> b
coe Any
v3)
(T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v4)
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_runModel_94 ::
Integer ->
T_CostingModel_8 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_runModel_94 :: Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer
d_runModel_94 Integer
v0 T_CostingModel_8
v1 T_Vec_28
v2
= case T_CostingModel_8 -> T_CostingModel_8
forall a b. a -> b
coe T_CostingModel_8
v1 of
C_constantCost_12 Integer
v4 -> Integer -> Integer
forall a b. a -> b
coe Integer
v4
C_linearCostIn_16 T_Fin_10
v4 Integer
v5 Integer
v6
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v6)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))))
(Integer -> Any
forall a b. a -> b
coe Integer
v5)
C_quadraticCostIn1_20 T_Fin_10
v4 Integer
v5 Integer
v6 Integer
v7
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v7)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v6)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4)))))
(Integer -> Any
forall a b. a -> b
coe Integer
v5)
C_quadraticCostIn2_24 T_Fin_10
v4 T_Fin_10
v5 Integer
v6 Integer
v7 Integer
v8 Integer
v9 Integer
v10 Integer
v11 Integer
v12
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d__'8852'__204 (Integer -> Any
forall a b. a -> b
coe Integer
v6)
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v10)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v11)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4))))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5)))))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v12)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5))))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5)))))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v8)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4)))))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v9)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
((T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v5)))))
(Integer -> Any
forall a b. a -> b
coe Integer
v7))
C_literalCostIn_28 T_Fin_10
v4 T_CostingModel_8
v5
-> let v6 :: t
v6
= (T_Vec_28 -> T_Fin_10 -> Any) -> Any -> Any -> t
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> Any
MAlonzo.Code.Data.Vec.Base.du_lookup_82 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4) in
Any -> Integer
forall a b. a -> b
coe
(let v7 :: Integer
v7 = Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer
d_runModel_94 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T_CostingModel_8 -> T_CostingModel_8
forall a b. a -> b
coe T_CostingModel_8
v5) (T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Value_14
forall a b. a -> b
coe Any
forall a. a
v6 of
MAlonzo.Code.Untyped.CEK.C_V'45'con_50 T__'8866''9839'_4
v8 Any
v9
-> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v8 of
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v11
-> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v11 of
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
-> case Any -> Integer
forall a b. a -> b
coe Any
v9 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Any -> Any
forall a b. a -> b
coe Any
v9) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Any -> Integer
forall a b. a -> b
coe Any
v9) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
((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
1 :: Integer))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__314
(Integer -> Any
forall a b. a -> b
coe Integer
v12) (Integer -> Any
forall a b. a -> b
coe (Integer
8 :: Integer))))
Integer
0 -> Integer -> Any
forall a b. a -> b
coe Integer
v7
Integer
_ -> Integer -> Any
forall a b. a -> b
coe Integer
v7
T_AtomicTyCon_6
_ -> Integer -> Any
forall a b. a -> b
coe Integer
v7
T__'8866''9839'_4
_ -> Integer -> Any
forall a b. a -> b
coe Integer
v7
T_Value_14
_ -> Integer -> Any
forall a b. a -> b
coe Integer
v7))
C_addedSizes_32 Integer
v4 Integer
v5
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v5)
((Integer -> T_Vec_28 -> Integer) -> Integer -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Vec_28 -> Integer
MAlonzo.Code.Data.Vec.Base.d_sum_420 Integer
v0
(((Any -> Any) -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_map_178
((T_Value_14 -> Integer) -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2))))
(Integer -> Any
forall a b. a -> b
coe Integer
v4)
C_multipliedSizes_36 Integer
v4 Integer
v5
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v5)
((Integer -> T_Vec_28 -> Integer) -> Integer -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Vec_28 -> Integer
d_prod_74 Integer
v0
(((Any -> Any) -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_map_178
((T_Value_14 -> Integer) -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2))))
(Integer -> Any
forall a b. a -> b
coe Integer
v4)
C_minSize_40 Integer
v4 Integer
v5
-> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v5)
((Integer -> T_Vec_28 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Vec_28 -> Integer
d_minimum_82 (Integer -> Any
forall a b. a -> b
coe Integer
v6)
(((Any -> Any) -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_map_178
((T_Value_14 -> Integer) -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2))))
(Integer -> Any
forall a b. a -> b
coe Integer
v4))
C_maxSize_44 Integer
v4 Integer
v5
-> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Integer
forall a b. a -> b
coe
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v5)
((Integer -> T_Vec_28 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Vec_28 -> Integer
d_maximum_78 (Integer -> Any
forall a b. a -> b
coe Integer
v6)
(((Any -> Any) -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_map_178
((T_Value_14 -> Integer) -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v2))))
(Integer -> Any
forall a b. a -> b
coe Integer
v4))
C_twoArgumentsSubtractedSizes_46 Integer
v3 Integer
v4 Integer
v5
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v7 T_Vec_28
v8
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v8 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v10 T_Vec_28
v11
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (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
MAlonzo.Code.Data.Nat.Base.d__'8852'__204 (Integer -> Any
forall a b. a -> b
coe Integer
v5)
((Integer -> Integer -> Integer) -> Integer -> Integer -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22
(T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> T_Value_14
forall a b. a -> b
coe Any
v7))
(T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> T_Value_14
forall a b. a -> b
coe Any
v10)))))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
C_twoArgumentsConstAboveDiagonal_48 Integer
v3 T_CostingModel_8
v4
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6 T_Vec_28
v7
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v7 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9 T_Vec_28
v10
-> (Any -> Any -> Any) -> Any -> Any -> Integer
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v10)
((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
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
ltInt
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> Any
forall a b. a -> b
coe Any
v6))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> Any
forall a b. a -> b
coe Any
v9)))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)
((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
d_runModel_94 (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_CostingModel_8 -> Any
forall a b. a -> b
coe T_CostingModel_8
v4)
((Any -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6
((Any -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9
(T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32)))))
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
C_twoArgumentsConstBelowDiagonal_50 Integer
v3 T_CostingModel_8
v4
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6 T_Vec_28
v7
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v7 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9 T_Vec_28
v10
-> (Any -> Any -> Any) -> Any -> Any -> Integer
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v10)
((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
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
ltInt
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> Any
forall a b. a -> b
coe Any
v9))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> Any
forall a b. a -> b
coe Any
v6)))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)
((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
d_runModel_94 (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_CostingModel_8 -> Any
forall a b. a -> b
coe T_CostingModel_8
v4)
((Any -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6
((Any -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9
(T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32)))))
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
C_twoArgumentsConstOffDiagonal_52 Integer
v3 T_CostingModel_8
v4
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6 T_Vec_28
v7
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v7 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9 T_Vec_28
v10
-> (Any -> Any -> Any) -> Any -> Any -> Integer
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v10)
((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
((Bool -> Bool) -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
((Integer -> Integer -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Bool
eqInt
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> Any
forall a b. a -> b
coe Any
v6))
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58 (Any -> Any
forall a b. a -> b
coe Any
v9))))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)
((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
d_runModel_94 (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_CostingModel_8 -> Any
forall a b. a -> b
coe T_CostingModel_8
v4)
((Any -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6
((Any -> T_Vec_28 -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9
(T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32)))))
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
C_twoArgumentsLinearInYAndZ_54 Integer
v3 Integer
v4 Integer
v5
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v7 T_Vec_28
v8
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v8 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v10 T_Vec_28
v11
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v11 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v13 T_Vec_28
v14
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
(Any -> Any
forall a b. a -> b
coe Any
v10)))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v5)
((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
(Any -> Any
forall a b. a -> b
coe Any
v13))))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
C_twoArgumentsLinearInMaxYZ_56 Integer
v3 Integer
v4
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v6 T_Vec_28
v7
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v7 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v9 T_Vec_28
v10
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v10 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v12 T_Vec_28
v13
-> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
mulInt (Integer -> Any
forall a b. a -> b
coe Integer
v4)
((Integer -> T_Vec_28 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Vec_28 -> Integer
d_maximum_78 (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
((Any -> T_Vec_28 -> T_Vec_28) -> Integer -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38
(T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
(Any -> T_Value_14
forall a b. a -> b
coe Any
v9))
((Any -> T_Vec_28 -> T_Vec_28) -> Integer -> Any -> Any
forall a b. a -> b
coe
Any -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.C__'8759'__38
(T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_58
(Any -> T_Value_14
forall a b. a -> b
coe Any
v12))
(T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32)))))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Vec_28
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
T_CostingModel_8
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_convertRawModel_270 ::
Integer ->
MAlonzo.Code.Cost.Raw.T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 :: Integer -> T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 Integer
v0 T_RawModel_108
v1
= let v2 :: b
v2 = Maybe Any -> b
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in
Any -> Maybe T_CostingModel_8
forall a b. a -> b
coe
(case T_RawModel_108 -> T_RawModel_108
forall a b. a -> b
coe T_RawModel_108
v1 of
MAlonzo.Code.Cost.Raw.C_ConstantCost_110 Integer
v3
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> T_CostingModel_8) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_CostingModel_8
C_constantCost_12 Integer
v3)
MAlonzo.Code.Cost.Raw.C_AddedSizes_112 LinearFunction
v3
-> case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> T_CostingModel_8)
-> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> T_CostingModel_8
C_addedSizes_32 Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Cost.Raw.C_MultipliedSizes_114 LinearFunction
v3
-> case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> T_CostingModel_8)
-> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> T_CostingModel_8
C_multipliedSizes_36 Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Cost.Raw.C_MinSize_116 LinearFunction
v3
-> case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 ((Integer -> Integer -> T_CostingModel_8)
-> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> T_CostingModel_8
C_minSize_40 Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Any
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_MaxSize_118 LinearFunction
v3
-> case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 ((Integer -> Integer -> T_CostingModel_8)
-> Integer -> Integer -> Any
forall a b. a -> b
coe Integer -> Integer -> T_CostingModel_8
C_maxSize_44 Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Any
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_LinearInX_120 LinearFunction
v3
-> case Integer -> Any
forall a b. a -> b
coe Integer
v0 of
Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10 -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Integer -> Integer -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer -> T_CostingModel_8
C_linearCostIn_16 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Any
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_LinearInY_122 LinearFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) ->
case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10 -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Integer -> Integer -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer -> T_CostingModel_8
C_linearCostIn_16
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_LinearInZ_124 LinearFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer)) ->
case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10 -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Integer -> Integer -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer -> T_CostingModel_8
C_linearCostIn_16
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)))
Integer
v4 Integer
v5)
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
2 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_LiteralInYOrLinearInZ_126 LinearFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer)) ->
case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10 -> T_CostingModel_8 -> T_CostingModel_8)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_CostingModel_8 -> T_CostingModel_8
C_literalCostIn_28
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((T_Fin_10 -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Integer -> Integer -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer -> T_CostingModel_8
C_linearCostIn_16
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)))
Integer
v4 Integer
v5))
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
2 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_LinearInMaxYZ_128 LinearFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
3 -> case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v4 Integer
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> T_CostingModel_8) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_CostingModel_8
C_twoArgumentsLinearInMaxYZ_56 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5))
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer)) -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
2 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_LinearInYAndZ_130 TwoVariableLinearFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
3 -> case TwoVariableLinearFunction -> TwoVariableLinearFunction
forall a b. a -> b
coe TwoVariableLinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkTwoVariableLinearFunction_74 Integer
v4 Integer
v5 Integer
v6
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer -> T_CostingModel_8
C_twoArgumentsLinearInYAndZ_54 (Integer -> Any
forall a b. a -> b
coe Integer
v4) (Integer -> Any
forall a b. a -> b
coe Integer
v5) (Integer -> Any
forall a b. a -> b
coe Integer
v6))
TwoVariableLinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer)) -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
2 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_QuadraticInY_132 OneVariableQuadraticFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) ->
case OneVariableQuadraticFunction -> OneVariableQuadraticFunction
forall a b. a -> b
coe OneVariableQuadraticFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkOneVariableQuadraticFunction_58 Integer
v4 Integer
v5 Integer
v6
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10 -> Integer -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer -> Integer -> T_CostingModel_8
C_quadraticCostIn1_20
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
Integer
v4 Integer
v5 Integer
v6)
OneVariableQuadraticFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_QuadraticInZ_134 OneVariableQuadraticFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
3 :: Integer)) ->
case OneVariableQuadraticFunction -> OneVariableQuadraticFunction
forall a b. a -> b
coe OneVariableQuadraticFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkOneVariableQuadraticFunction_58 Integer
v4 Integer
v5 Integer
v6
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10 -> Integer -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Integer -> Integer -> Integer -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer -> Integer -> T_CostingModel_8
C_quadraticCostIn1_20
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)))
Integer
v4 Integer
v5 Integer
v6)
OneVariableQuadraticFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
2 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_QuadraticInXAndY_136 TwoVariableQuadraticFunction
v3
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) ->
case TwoVariableQuadraticFunction -> TwoVariableQuadraticFunction
forall a b. a -> b
coe TwoVariableQuadraticFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkTwoVariableQuadraticFunction_106 Integer
v4 Integer
v5 Integer
v6 Integer
v7 Integer
v8 Integer
v9 Integer
v10
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Fin_10
-> T_Fin_10
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T_CostingModel_8)
-> Any
-> Any
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Any
forall a b. a -> b
coe
T_Fin_10
-> T_Fin_10
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> T_CostingModel_8
C_quadraticCostIn2_24 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((T_Fin_10 -> T_Fin_10) -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
Integer
v4 Integer
v5 Integer
v6 Integer
v7 Integer
v8 Integer
v9 Integer
v10)
TwoVariableQuadraticFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_SubtractedSizes_138 LinearFunction
v3 Integer
v4
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
2 -> case LinearFunction -> LinearFunction
forall a b. a -> b
coe LinearFunction
v3 of
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 Integer
v5 Integer
v6
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> Integer -> T_CostingModel_8)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer -> T_CostingModel_8
C_twoArgumentsSubtractedSizes_46 (Integer -> Any
forall a b. a -> b
coe Integer
v5) (Integer -> Any
forall a b. a -> b
coe Integer
v6) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
LinearFunction
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_ConstAboveDiagonal_140 Integer
v3 T_RawModel_108
v4
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
2 -> ((Any -> Any) -> Maybe Any -> Maybe Any)
-> Any -> Maybe T_CostingModel_8 -> Any
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64
((Integer -> T_CostingModel_8 -> T_CostingModel_8) -> Any -> Any
forall a b. a -> b
coe Integer -> T_CostingModel_8 -> T_CostingModel_8
C_twoArgumentsConstAboveDiagonal_48 (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(Integer -> T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_RawModel_108 -> T_RawModel_108
forall a b. a -> b
coe T_RawModel_108
v4))
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_ConstBelowDiagonal_142 Integer
v3 T_RawModel_108
v4
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
2 -> ((Any -> Any) -> Maybe Any -> Maybe Any)
-> Any -> Maybe T_CostingModel_8 -> Any
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64
((Integer -> T_CostingModel_8 -> T_CostingModel_8) -> Any -> Any
forall a b. a -> b
coe Integer -> T_CostingModel_8 -> T_CostingModel_8
C_twoArgumentsConstBelowDiagonal_50 (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(Integer -> T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_RawModel_108 -> T_RawModel_108
forall a b. a -> b
coe T_RawModel_108
v4))
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
MAlonzo.Code.Cost.Raw.C_ConstOffDiagonal_144 Integer
v3 T_RawModel_108
v4
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
2 -> ((Any -> Any) -> Maybe Any -> Maybe Any)
-> Any -> Maybe T_CostingModel_8 -> Any
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64
((Integer -> T_CostingModel_8 -> T_CostingModel_8) -> Any -> Any
forall a b. a -> b
coe Integer -> T_CostingModel_8 -> T_CostingModel_8
C_twoArgumentsConstOffDiagonal_52 (Integer -> Any
forall a b. a -> b
coe Integer
v3))
(Integer -> T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_RawModel_108 -> T_RawModel_108
forall a b. a -> b
coe T_RawModel_108
v4))
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)) -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
1 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2
T_RawModel_108
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_convertCpuAndMemoryModel_380 ::
Integer ->
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146 ->
Maybe T_BuiltinModel_60
d_convertCpuAndMemoryModel_380 :: Integer -> T_CpuAndMemoryModel_146 -> Maybe T_BuiltinModel_60
d_convertCpuAndMemoryModel_380 Integer
v0 T_CpuAndMemoryModel_146
v1
= case T_CpuAndMemoryModel_146 -> T_CpuAndMemoryModel_146
forall a b. a -> b
coe T_CpuAndMemoryModel_146
v1 of
MAlonzo.Code.Cost.Raw.C_mkCpuAndMemoryModel_156 T_RawModel_108
v2 T_RawModel_108
v3
-> let v4 :: Maybe T_CostingModel_8
v4 = Integer -> T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T_RawModel_108 -> T_RawModel_108
forall a b. a -> b
coe T_RawModel_108
v2) in
Any -> Maybe T_BuiltinModel_60
forall a b. a -> b
coe
(let v5 :: Maybe T_CostingModel_8
v5 = Integer -> T_RawModel_108 -> Maybe T_CostingModel_8
d_convertRawModel_270 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T_RawModel_108 -> T_RawModel_108
forall a b. a -> b
coe T_RawModel_108
v3) in
Any -> Any
forall a b. a -> b
coe
(case Maybe T_CostingModel_8 -> Maybe Any
forall a b. a -> b
coe Maybe T_CostingModel_8
v4 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v6
-> case Maybe T_CostingModel_8 -> Maybe Any
forall a b. a -> b
coe Maybe T_CostingModel_8
v5 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v7
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_60)
-> Any -> Any -> Any
forall a b. a -> b
coe T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_60
C_BuiltinModel'46'constructor_581 (Any -> Any
forall a b. a -> b
coe Any
v6) (Any -> Any
forall a b. a -> b
coe Any
v7))
Maybe Any
_ -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
Maybe Any
_ -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
T_CpuAndMemoryModel_146
_ -> Maybe T_BuiltinModel_60
forall a. a
MAlonzo.RTE.mazUnreachableError
d_getModel_404 ::
MAlonzo.Code.Builtin.T_Builtin_2 ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Agda.Builtin.String.T_String_6
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146) ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_getModel_404 :: T_Builtin_2
-> T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
d_getModel_404 T_Builtin_2
v0 T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
v1
= case T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> [Any]
forall a b. a -> b
coe T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
v1 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> Maybe Any -> Maybe T_Σ_14
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
-> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Utils.C__'44'__378 Any
v4 Any
v5
-> let v6 :: t
v6
= (T_Dec_20 -> Bool) -> Any -> t
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_isYes_122
(((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> (Any -> Any) -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
Any
forall a. a
erased
(\ Any
v6 ->
(T_String_6 -> T_Pointwise_48) -> Any -> Any
forall a b. a -> b
coe
T_String_6 -> T_Pointwise_48
MAlonzo.Code.Data.String.Properties.du_'8776''45'reflexive_8
((T_Builtin_2 -> T_String_6) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_String_6
MAlonzo.Code.Builtin.d_showBuiltin_400 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0)))
(((Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
MAlonzo.Code.Data.Char.Properties.d__'8799'__14)
((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe
T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12
(T_Builtin_2 -> T_String_6
MAlonzo.Code.Builtin.d_showBuiltin_400 (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v0)))
((T_String_6 -> String) -> Any -> Any
forall a b. a -> b
coe
T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 Any
v4))) in
Any -> Maybe T_Σ_14
forall a b. a -> b
coe
(if Any -> Bool
forall a b. a -> b
coe Any
forall a. a
v6
then ((Any -> Any) -> Maybe Any -> Maybe Any)
-> (Any -> Any) -> Maybe T_BuiltinModel_60 -> Any
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64
(\ Any
v7 ->
(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 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0) (Any -> Any
forall a b. a -> b
coe Any
v7))
(Integer -> T_CpuAndMemoryModel_146 -> Maybe T_BuiltinModel_60
d_convertCpuAndMemoryModel_380
((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
((Any -> Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v7 Any
v8 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Any -> Integer
forall a b. a -> b
coe Any
v8)))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((T_List'8314'_22 -> [Any]) -> Any -> Any
forall a b. a -> b
coe
T_List'8314'_22 -> [Any]
MAlonzo.Code.Data.List.NonEmpty.Base.d_tail_32
((T_Sig_68 -> T_List'8314'_22) -> Any -> Any
forall a b. a -> b
coe
T_Sig_68 -> T_List'8314'_22
MAlonzo.Code.Builtin.Signature.d_args_82
((T_Builtin_2 -> T_Sig_68) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_278 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0))))))
(Any -> T_CpuAndMemoryModel_146
forall a b. a -> b
coe Any
v5))
else (T_Builtin_2
-> T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Builtin_2
-> T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
d_getModel_404 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
(Any, Any)
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_dummyModel_440 :: Integer -> T_BuiltinModel_60
d_dummyModel_440 :: Integer -> T_BuiltinModel_60
d_dummyModel_440 ~Integer
v0 = T_BuiltinModel_60
du_dummyModel_440
du_dummyModel_440 :: T_BuiltinModel_60
du_dummyModel_440 :: T_BuiltinModel_60
du_dummyModel_440
= (T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_60)
-> Any -> Any -> T_BuiltinModel_60
forall a b. a -> b
coe
T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_60
C_BuiltinModel'46'constructor_581
((Integer -> T_CostingModel_8) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_CostingModel_8
C_constantCost_12 (Integer
0 :: Integer))
((Integer -> T_CostingModel_8) -> Integer -> Any
forall a b. a -> b
coe Integer -> T_CostingModel_8
C_constantCost_12 (Integer
0 :: Integer))
d_lookupModel_446 ::
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Builtin.T_Builtin_2 -> T_BuiltinModel_60
d_lookupModel_446 :: [T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_60
d_lookupModel_446 [T_Σ_14]
v0 T_Builtin_2
v1
= case [T_Σ_14] -> [Any]
forall a b. a -> b
coe [T_Σ_14]
v0 of
[] -> T_BuiltinModel_60 -> T_BuiltinModel_60
forall a b. a -> b
coe T_BuiltinModel_60
du_dummyModel_440
(:) Any
v2 [Any]
v3
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v4 Any
v5
-> let v6 :: T_Dec_20
v6
= T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_398 (Any -> T_Builtin_2
forall a b. a -> b
coe Any
v4) (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v1) in
Any -> T_BuiltinModel_60
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v6 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v7 T_Reflects_16
v8
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v7
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v8) (Any -> Any
forall a b. a -> b
coe Any
v5)
else ([T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_60) -> Any -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_60
d_lookupModel_446 ([Any] -> Any
forall a b. a -> b
coe [Any]
v3) (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v1)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Σ_14
_ -> T_BuiltinModel_60
forall a. a
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> T_BuiltinModel_60
forall a. a
MAlonzo.RTE.mazUnreachableError
d_allJust_482 :: () -> [Maybe AgdaAny] -> Maybe [AgdaAny]
d_allJust_482 :: () -> [Maybe Any] -> Maybe [Any]
d_allJust_482 ~()
v0 [Maybe Any]
v1 = [Maybe Any] -> Maybe [Any]
du_allJust_482 [Maybe Any]
v1
du_allJust_482 :: [Maybe AgdaAny] -> Maybe [AgdaAny]
du_allJust_482 :: [Maybe Any] -> Maybe [Any]
du_allJust_482 [Maybe Any]
v0
= case [Maybe Any] -> [Any]
forall a b. a -> b
coe [Maybe Any]
v0 of
[] -> (Any -> Maybe Any) -> Any -> Maybe [Any]
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 ([Maybe Any] -> Any
forall a b. a -> b
coe [Maybe Any]
v0)
(:) Any
v1 [Any]
v2
-> case Any -> Maybe Any
forall a b. a -> b
coe Any
v1 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v3
-> let v4 :: t
v4 = ([Maybe Any] -> Maybe [Any]) -> Any -> t
forall a b. a -> b
coe [Maybe Any] -> Maybe [Any]
du_allJust_482 ([Any] -> Any
forall a b. a -> b
coe [Any]
v2) in
Any -> Maybe [Any]
forall a b. a -> b
coe
(case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v4 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v5
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_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 (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v5))
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4
Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> Any -> Maybe [Any]
forall a b. a -> b
coe Any
v1
Maybe Any
_ -> Maybe [Any]
forall a. a
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> Maybe [Any]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_ModelAssignment_504 :: ()
d_ModelAssignment_504 :: ()
d_ModelAssignment_504 = ()
forall a. a
erased
d_createMap_508 ::
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Agda.Builtin.String.T_String_6
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_146) ->
Maybe (MAlonzo.Code.Builtin.T_Builtin_2 -> T_BuiltinModel_60)
d_createMap_508 :: T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> Maybe (T_Builtin_2 -> T_BuiltinModel_60)
d_createMap_508 T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
v0
= ((Any -> Any) -> Maybe Any -> Maybe Any)
-> ([T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_60)
-> Any
-> Maybe (T_Builtin_2 -> T_BuiltinModel_60)
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64 [T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_60
d_lookupModel_446
(([Maybe Any] -> Maybe [Any]) -> Any -> Any
forall a b. a -> b
coe
[Maybe Any] -> Maybe [Any]
du_allJust_482
(((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 -> Maybe T_Σ_14) -> Any
forall a b. a -> b
coe (\ Any
v1 -> T_Builtin_2
-> T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> Maybe T_Σ_14
d_getModel_404 (Any -> T_Builtin_2
forall a b. a -> b
coe Any
v1) (T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
-> T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
forall a b. a -> b
coe T_List_382 (T__'215'__364 T_String_6 T_CpuAndMemoryModel_146)
v0)))
([T_Builtin_2] -> Any
forall a b. a -> b
coe [T_Builtin_2]
MAlonzo.Code.Builtin.d_builtinList_402)))