{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Builtin.List qualified
import MAlonzo.Code.Agda.Builtin.Maybe qualified
import MAlonzo.Code.Agda.Builtin.Nat qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Builtin.String qualified
import MAlonzo.Code.Builtin qualified
import MAlonzo.Code.Builtin.Constant.AtomicType qualified
import MAlonzo.Code.Builtin.Signature qualified
import MAlonzo.Code.Cost.Raw qualified
import MAlonzo.Code.Cost.Size qualified
import MAlonzo.Code.Data.Bool.Base qualified
import MAlonzo.Code.Data.Char.Properties qualified
import MAlonzo.Code.Data.Fin.Base qualified
import MAlonzo.Code.Data.List.Base qualified
import MAlonzo.Code.Data.List.NonEmpty.Base qualified
import MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties qualified
import MAlonzo.Code.Data.Maybe.Base qualified
import MAlonzo.Code.Data.Nat.Base qualified
import MAlonzo.Code.Data.String.Properties qualified
import MAlonzo.Code.Data.Vec.Base qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.Code.Untyped.CEK qualified
import MAlonzo.Code.Utils qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- Cost.Model.Intercept
d_Intercept_4 :: ()
d_Intercept_4 :: ()
d_Intercept_4 = ()
forall a. a
erased
-- Cost.Model.Slope
d_Slope_6 :: ()
d_Slope_6 :: ()
d_Slope_6 = ()
forall a. a
erased
-- Cost.Model.CostingModel
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 |
    C_threeArgumentsExpModCost_58 Integer Integer Integer
-- Cost.Model.BuiltinModel
d_BuiltinModel_62 :: p -> ()
d_BuiltinModel_62 p
a0 = ()
data T_BuiltinModel_62
  = C_BuiltinModel'46'constructor_607 T_CostingModel_8
                                      T_CostingModel_8
-- Cost.Model.BuiltinModel.costingCPU
d_costingCPU_70 :: T_BuiltinModel_62 -> T_CostingModel_8
d_costingCPU_70 :: T_BuiltinModel_62 -> T_CostingModel_8
d_costingCPU_70 T_BuiltinModel_62
v0
  = case T_BuiltinModel_62 -> T_BuiltinModel_62
forall a b. a -> b
coe T_BuiltinModel_62
v0 of
      C_BuiltinModel'46'constructor_607 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_62
_                                       -> T_CostingModel_8
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Model.BuiltinModel.costingMem
d_costingMem_72 :: T_BuiltinModel_62 -> T_CostingModel_8
d_costingMem_72 :: T_BuiltinModel_62 -> T_CostingModel_8
d_costingMem_72 T_BuiltinModel_62
v0
  = case T_BuiltinModel_62 -> T_BuiltinModel_62
forall a b. a -> b
coe T_BuiltinModel_62
v0 of
      C_BuiltinModel'46'constructor_607 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_62
_                                       -> T_CostingModel_8
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Model.prod
d_prod_76 ::
  Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_prod_76 :: Integer -> T_Vec_28 -> Integer
d_prod_76 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))
-- Cost.Model.maximum
d_maximum_80 ::
  Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_maximum_80 :: Integer -> T_Vec_28 -> Integer
d_maximum_80 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
-- Cost.Model.minimum
d_minimum_84 ::
  Integer -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_minimum_84 :: Integer -> T_Vec_28 -> Integer
d_minimum_84 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
-- Cost.Model.runModel
d_runModel_96 ::
  Integer ->
  T_CostingModel_8 -> MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_runModel_96 :: Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer
d_runModel_96 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_56
                   ((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_56
                         ((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_56
                      ((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_56
                      ((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_56
                                     ((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_56
                                  ((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_56
                                     ((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_56
                                  ((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_56
                                  ((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_56
                               ((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_56
                            ((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_56
                         ((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 :: Any
v6
                 = (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) in
           Any -> Integer
forall a b. a -> b
coe
             (let v7 :: Integer
v7 = Integer -> T_CostingModel_8 -> T_Vec_28 -> Integer
d_runModel_96 (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
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_56) (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_76 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_56) (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_84 (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_56) (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_80 (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_56) (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_56 (Any -> T_Value_14
forall a b. a -> b
coe Any
v7))
                                    (T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56 (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_56 (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_56 (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_96 (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_56 (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_56 (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_96 (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_56 (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_56 (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_96 (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_56
                                           (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_56
                                           (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_80 (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_56
                                              (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_56
                                                 (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
      C_threeArgumentsExpModCost_58 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
                             -> (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
v14)
                                  ((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_56
                                           (Any -> Any
forall a b. a -> b
coe Any
v13))
                                        ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                           T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                           (Any -> Any
forall a b. a -> b
coe Any
v7)))
                                     ((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
MAlonzo.Code.Data.Nat.Base.du__'47'__314
                                                 ((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 -> 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_56
                                                                   (Any -> Any
forall a b. a -> b
coe Any
v10)))
                                                             ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                                T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                                (Any -> Any
forall a b. a -> b
coe Any
v13)))
                                                          ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                             T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                             (Any -> Any
forall a b. a -> b
coe Any
v13)))
                                                       ((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
v4)
                                                             ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                                T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                                (Any -> Any
forall a b. a -> b
coe Any
v10)))
                                                          ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                             T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                             (Any -> Any
forall a b. a -> b
coe Any
v13))))
                                                    (Integer -> Any
forall a b. a -> b
coe Integer
v3))
                                                 (Integer -> Any
forall a b. a -> b
coe (Integer
2 :: Integer)))
                                              ((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 -> 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_56
                                                          (Any -> Any
forall a b. a -> b
coe Any
v10)))
                                                    ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                       T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                       (Any -> Any
forall a b. a -> b
coe Any
v13)))
                                                 ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                    T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                    (Any -> Any
forall a b. a -> b
coe Any
v13))))
                                           ((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
v4)
                                                 ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                    T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                    (Any -> Any
forall a b. a -> b
coe Any
v10)))
                                              ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                 T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                 (Any -> Any
forall a b. a -> b
coe Any
v13))))
                                        (Integer -> Any
forall a b. a -> b
coe Integer
v3))
                                     ((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 -> 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_56
                                                       (Any -> Any
forall a b. a -> b
coe Any
v10)))
                                                 ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                    T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                    (Any -> Any
forall a b. a -> b
coe Any
v13)))
                                              ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                 T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                 (Any -> Any
forall a b. a -> b
coe Any
v13)))
                                           ((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
v4)
                                                 ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                    T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                    (Any -> Any
forall a b. a -> b
coe Any
v10)))
                                              ((T_Value_14 -> Integer) -> Any -> Any
forall a b. a -> b
coe
                                                 T_Value_14 -> Integer
MAlonzo.Code.Cost.Size.d_defaultValueMeasure_56
                                                 (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
      T_CostingModel_8
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Model.convertRawModel
d_convertRawModel_292 ::
  Integer ->
  MAlonzo.Code.Cost.Raw.T_RawModel_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 :: Integer -> T_RawModel_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 Integer
v0 T_RawModel_124
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_124 -> T_RawModel_124
forall a b. a -> b
coe T_RawModel_124
v1 of
         MAlonzo.Code.Cost.Raw.C_ConstantCost_126 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_128 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_130 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_132 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_134 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_136 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_138 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_140 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_142 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_144 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_146 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_148 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_150 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_152 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_154 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_156 Integer
v3 T_RawModel_124
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_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_RawModel_124 -> T_RawModel_124
forall a b. a -> b
coe T_RawModel_124
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_158 Integer
v3 T_RawModel_124
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_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_RawModel_124 -> T_RawModel_124
forall a b. a -> b
coe T_RawModel_124
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_160 Integer
v3 T_RawModel_124
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_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (T_RawModel_124 -> T_RawModel_124
forall a b. a -> b
coe T_RawModel_124
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_ExpModCost_162 ExpModCostingFunction
v3
           -> case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
                Integer
3 -> case ExpModCostingFunction -> ExpModCostingFunction
forall a b. a -> b
coe ExpModCostingFunction
v3 of
                       MAlonzo.Code.Cost.Raw.C_mkExpModCostingFunction_122 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_threeArgumentsExpModCost_58 (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))
                       ExpModCostingFunction
_ -> 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
         T_RawModel_124
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Cost.Model.convertCpuAndMemoryModel
d_convertCpuAndMemoryModel_408 ::
  Integer ->
  MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_164 ->
  Maybe T_BuiltinModel_62
d_convertCpuAndMemoryModel_408 :: Integer -> T_CpuAndMemoryModel_164 -> Maybe T_BuiltinModel_62
d_convertCpuAndMemoryModel_408 Integer
v0 T_CpuAndMemoryModel_164
v1
  = case T_CpuAndMemoryModel_164 -> T_CpuAndMemoryModel_164
forall a b. a -> b
coe T_CpuAndMemoryModel_164
v1 of
      MAlonzo.Code.Cost.Raw.C_mkCpuAndMemoryModel_174 T_RawModel_124
v2 T_RawModel_124
v3
        -> let v4 :: Maybe T_CostingModel_8
v4 = Integer -> T_RawModel_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T_RawModel_124 -> T_RawModel_124
forall a b. a -> b
coe T_RawModel_124
v2) in
           Any -> Maybe T_BuiltinModel_62
forall a b. a -> b
coe
             (let v5 :: Maybe T_CostingModel_8
v5 = Integer -> T_RawModel_124 -> Maybe T_CostingModel_8
d_convertRawModel_292 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T_RawModel_124 -> T_RawModel_124
forall a b. a -> b
coe T_RawModel_124
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_62)
-> Any -> Any -> Any
forall a b. a -> b
coe T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_62
C_BuiltinModel'46'constructor_607 (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_164
_ -> Maybe T_BuiltinModel_62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Model.getModel
d_getModel_432 ::
  MAlonzo.Code.Builtin.T_Builtin_2 ->
  MAlonzo.Code.Utils.T_List_384
    (MAlonzo.Code.Utils.T__'215'__366
       MAlonzo.Code.Agda.Builtin.String.T_String_6
       MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_164) ->
  Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_getModel_432 :: T_Builtin_2
-> T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
-> Maybe T_Σ_14
d_getModel_432 T_Builtin_2
v0 T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
v1
  = case T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
-> [Any]
forall a b. a -> b
coe T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
v1 of
      [Any]
MAlonzo.Code.Utils.C_'91''93'_388
        -> 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'__390 Any
v2 [Any]
v3
        -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v2 of
             MAlonzo.Code.Utils.C__'44'__380 Any
v4 Any
v5
               -> let v6 :: Any
v6
                        = (T_Dec_20 -> Bool) -> Any -> Any
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_406 (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_406 (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
v6
                       then ((Any -> Any) -> Maybe Any -> Maybe Any)
-> (Any -> Any) -> Maybe T_BuiltinModel_62 -> 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_164 -> Maybe T_BuiltinModel_62
d_convertCpuAndMemoryModel_408
                                 ((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_280 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v0))))))
                                 (Any -> T_CpuAndMemoryModel_164
forall a b. a -> b
coe Any
v5))
                       else (T_Builtin_2
 -> T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
 -> Maybe T_Σ_14)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Builtin_2
-> T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
-> Maybe T_Σ_14
d_getModel_432 (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
-- Cost.Model.dummyModel
d_dummyModel_468 :: Integer -> T_BuiltinModel_62
d_dummyModel_468 :: Integer -> T_BuiltinModel_62
d_dummyModel_468 ~Integer
v0 = T_BuiltinModel_62
du_dummyModel_468
du_dummyModel_468 :: T_BuiltinModel_62
du_dummyModel_468 :: T_BuiltinModel_62
du_dummyModel_468
  = (T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_62)
-> Any -> Any -> T_BuiltinModel_62
forall a b. a -> b
coe
      T_CostingModel_8 -> T_CostingModel_8 -> T_BuiltinModel_62
C_BuiltinModel'46'constructor_607
      ((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))
-- Cost.Model.lookupModel
d_lookupModel_474 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Builtin.T_Builtin_2 -> T_BuiltinModel_62
d_lookupModel_474 :: [T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_62
d_lookupModel_474 [T_Σ_14]
v0 T_Builtin_2
v1
  = case [T_Σ_14] -> [Any]
forall a b. a -> b
coe [T_Σ_14]
v0 of
      [] -> T_BuiltinModel_62 -> T_BuiltinModel_62
forall a b. a -> b
coe T_BuiltinModel_62
du_dummyModel_468
      (:) 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_404 (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_62
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_62) -> Any -> Any -> Any
forall a b. a -> b
coe [T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_62
d_lookupModel_474 ([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_62
forall a. a
MAlonzo.RTE.mazUnreachableError
      [Any]
_ -> T_BuiltinModel_62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Cost.Model.allJust
d_allJust_510 :: () -> [Maybe AgdaAny] -> Maybe [AgdaAny]
d_allJust_510 :: () -> [Maybe Any] -> Maybe [Any]
d_allJust_510 ~()
v0 [Maybe Any]
v1 = [Maybe Any] -> Maybe [Any]
du_allJust_510 [Maybe Any]
v1
du_allJust_510 :: [Maybe AgdaAny] -> Maybe [AgdaAny]
du_allJust_510 :: [Maybe Any] -> Maybe [Any]
du_allJust_510 [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 :: Any
v4 = ([Maybe Any] -> Maybe [Any]) -> Any -> Any
forall a b. a -> b
coe [Maybe Any] -> Maybe [Any]
du_allJust_510 ([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
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
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
-- Cost.Model.ModelAssignment
d_ModelAssignment_532 :: ()
d_ModelAssignment_532 :: ()
d_ModelAssignment_532 = ()
forall a. a
erased
-- Cost.Model.createMap
d_createMap_536 ::
  MAlonzo.Code.Utils.T_List_384
    (MAlonzo.Code.Utils.T__'215'__366
       MAlonzo.Code.Agda.Builtin.String.T_String_6
       MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_164) ->
  Maybe (MAlonzo.Code.Builtin.T_Builtin_2 -> T_BuiltinModel_62)
d_createMap_536 :: T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
-> Maybe (T_Builtin_2 -> T_BuiltinModel_62)
d_createMap_536 T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
v0
  = ((Any -> Any) -> Maybe Any -> Maybe Any)
-> ([T_Σ_14] -> T_Builtin_2 -> T_BuiltinModel_62)
-> Any
-> Maybe (T_Builtin_2 -> T_BuiltinModel_62)
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_62
d_lookupModel_474
      (([Maybe Any] -> Maybe [Any]) -> Any -> Any
forall a b. a -> b
coe
         [Maybe Any] -> Maybe [Any]
du_allJust_510
         (((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_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
-> Maybe T_Σ_14
d_getModel_432 (Any -> T_Builtin_2
forall a b. a -> b
coe Any
v1) (T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
-> T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
forall a b. a -> b
coe T_List_384 (T__'215'__366 T_String_6 T_CpuAndMemoryModel_164)
v0)))
            ([T_Builtin_2] -> Any
forall a b. a -> b
coe [T_Builtin_2]
MAlonzo.Code.Builtin.d_builtinList_408)))