{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Cost.Model where

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

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