{-# 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.Agda.Builtin.Reflection 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Char
import qualified MAlonzo.Code.Agda.Builtin.Float
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
d_Name_6 :: a
d_Name_6
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.Name"
d_primQNameEquality_8 :: QName -> QName -> Bool
d_primQNameEquality_8
= (\ QName
x QName
y -> (QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: MAlonzo.RTE.QName -> MAlonzo.RTE.QName -> Bool) ( QName
x) ( QName
y))
d_primQNameLess_10 :: QName -> QName -> Bool
d_primQNameLess_10
= (\ QName
x QName
y -> (QName -> QName -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: MAlonzo.RTE.QName -> MAlonzo.RTE.QName -> Bool) ( QName
x) ( QName
y))
d_primShowQName_12 :: QName -> Text
d_primShowQName_12 = [Char] -> Text
Data.Text.pack ([Char] -> Text) -> (QName -> [Char]) -> QName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Char]
MAlonzo.RTE.qnameString
d_Associativity_14 :: ()
d_Associativity_14 = ()
type T_Associativity_14 = MAlonzo.RTE.Assoc
pattern $mC_left'45'assoc_16 :: forall {r}. Assoc -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_left'45'assoc_16 :: Assoc
C_left'45'assoc_16 = MAlonzo.RTE.LeftAssoc
pattern $mC_right'45'assoc_18 :: forall {r}. Assoc -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_right'45'assoc_18 :: Assoc
C_right'45'assoc_18 = MAlonzo.RTE.RightAssoc
pattern $mC_non'45'assoc_20 :: forall {r}. Assoc -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_non'45'assoc_20 :: Assoc
C_non'45'assoc_20 = MAlonzo.RTE.NonAssoc
check_left'45'assoc_16 :: T_Associativity_14
check_left'45'assoc_16 :: Assoc
check_left'45'assoc_16 = Assoc
MAlonzo.RTE.LeftAssoc
check_right'45'assoc_18 :: T_Associativity_14
check_right'45'assoc_18 :: Assoc
check_right'45'assoc_18 = Assoc
MAlonzo.RTE.RightAssoc
check_non'45'assoc_20 :: T_Associativity_14
check_non'45'assoc_20 :: Assoc
check_non'45'assoc_20 = Assoc
MAlonzo.RTE.NonAssoc
cover_Associativity_14 :: MAlonzo.RTE.Assoc -> ()
cover_Associativity_14 :: Assoc -> ()
cover_Associativity_14 Assoc
x
= case Assoc
x of
Assoc
MAlonzo.RTE.LeftAssoc -> ()
Assoc
MAlonzo.RTE.RightAssoc -> ()
Assoc
MAlonzo.RTE.NonAssoc -> ()
d_Precedence_22 :: ()
d_Precedence_22 = ()
type T_Precedence_22 = MAlonzo.RTE.Precedence
pattern $mC_related_24 :: forall {r}.
Precedence -> (PrecedenceLevel -> r) -> ((# #) -> r) -> r
$bC_related_24 :: PrecedenceLevel -> Precedence
C_related_24 a0 = MAlonzo.RTE.Related a0
pattern $mC_unrelated_26 :: forall {r}. Precedence -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_unrelated_26 :: Precedence
C_unrelated_26 = MAlonzo.RTE.Unrelated
check_related_24 ::
MAlonzo.Code.Agda.Builtin.Float.T_Float_6 -> T_Precedence_22
check_related_24 :: PrecedenceLevel -> Precedence
check_related_24 = PrecedenceLevel -> Precedence
MAlonzo.RTE.Related
check_unrelated_26 :: T_Precedence_22
check_unrelated_26 :: Precedence
check_unrelated_26 = Precedence
MAlonzo.RTE.Unrelated
cover_Precedence_22 :: MAlonzo.RTE.Precedence -> ()
cover_Precedence_22 :: Precedence -> ()
cover_Precedence_22 Precedence
x
= case Precedence
x of
MAlonzo.RTE.Related PrecedenceLevel
_ -> ()
Precedence
MAlonzo.RTE.Unrelated -> ()
d_Fixity_28 :: ()
d_Fixity_28 = ()
type T_Fixity_28 = MAlonzo.RTE.Fixity
pattern $mC_fixity_30 :: forall {r}.
Fixity -> (Assoc -> Precedence -> r) -> ((# #) -> r) -> r
$bC_fixity_30 :: Assoc -> Precedence -> Fixity
C_fixity_30 a0 a1 = MAlonzo.RTE.Fixity a0 a1
check_fixity_30 ::
T_Associativity_14 -> T_Precedence_22 -> T_Fixity_28
check_fixity_30 :: Assoc -> Precedence -> Fixity
check_fixity_30 = Assoc -> Precedence -> Fixity
MAlonzo.RTE.Fixity
cover_Fixity_28 :: MAlonzo.RTE.Fixity -> ()
cover_Fixity_28 :: Fixity -> ()
cover_Fixity_28 Fixity
x
= case Fixity
x of
MAlonzo.RTE.Fixity Assoc
_ Precedence
_ -> ()
d_primQNameFixity_32 :: QName -> Fixity
d_primQNameFixity_32 = QName -> Fixity
MAlonzo.RTE.qnameFixity
d_primQNameToWord64s_36 :: QName -> (Integer, Integer)
d_primQNameToWord64s_36
= \ QName
qn -> (QName -> Integer
MAlonzo.RTE.nameId QName
qn, QName -> Integer
MAlonzo.RTE.moduleId QName
qn)
d_Meta_38 :: a
d_Meta_38
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.Meta"
d_primMetaEquality_40 :: (Integer, Integer) -> (Integer, Integer) -> Bool
d_primMetaEquality_40
= (\ (Integer, Integer)
x (Integer, Integer)
y -> ((Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: (Integer, Integer) -> (Integer, Integer) -> Bool) ( (Integer, Integer)
x) ( (Integer, Integer)
y))
d_primMetaLess_42 :: (Integer, Integer) -> (Integer, Integer) -> Bool
d_primMetaLess_42
= (\ (Integer, Integer)
x (Integer, Integer)
y -> ((Integer, Integer) -> (Integer, Integer) -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: (Integer, Integer) -> (Integer, Integer) -> Bool) ( (Integer, Integer)
x) ( (Integer, Integer)
y))
d_primShowMeta_44 :: (Integer, Integer) -> Text
d_primShowMeta_44
= \ (Integer
m, Integer
h) -> [Char] -> Text
Data.Text.pack ([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
m :: Integer) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"@" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
h :: Integer))
d_primMetaToNat_46 :: (Integer, Integer) -> Integer
d_primMetaToNat_46
= \ (Integer
m, Integer
h) -> (Integer
h :: Integer) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
2Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
64 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
m :: Integer)
d_Visibility_48 :: ()
d_Visibility_48 = ()
data T_Visibility_48
= C_visible_50 | C_hidden_52 | C_instance'8242'_54
d_Relevance_56 :: ()
d_Relevance_56 = ()
data T_Relevance_56 = C_relevant_58 | C_irrelevant_60
d_Quantity_62 :: ()
d_Quantity_62 = ()
data T_Quantity_62 = C_quantity'45'0_64 | C_quantity'45'ω_66
d_Modality_68 :: ()
d_Modality_68 = ()
data T_Modality_68 = C_modality_74 T_Relevance_56 T_Quantity_62
d_ArgInfo_76 :: ()
d_ArgInfo_76 = ()
data T_ArgInfo_76 = C_arg'45'info_82 T_Visibility_48 T_Modality_68
d_Arg_88 :: p -> p -> ()
d_Arg_88 p
a0 p
a1 = ()
data T_Arg_88 = C_arg_98 T_ArgInfo_76 AgdaAny
d_Blocker_100 :: ()
d_Blocker_100 = ()
data T_Blocker_100
= C_blockerAny_102 [T_Blocker_100] |
C_blockerAll_104 [T_Blocker_100] | C_blockerMeta_106 AgdaAny
d_Abs_112 :: p -> p -> ()
d_Abs_112 p
a0 p
a1 = ()
data T_Abs_112
= C_abs_122 MAlonzo.Code.Agda.Builtin.String.T_String_6 AgdaAny
d_Literal_124 :: ()
d_Literal_124 = ()
data T_Literal_124
= C_nat_128 Integer | C_word64_132 MAlonzo.RTE.Word64 |
C_float_136 MAlonzo.Code.Agda.Builtin.Float.T_Float_6 |
C_char_140 MAlonzo.Code.Agda.Builtin.Char.T_Char_6 |
C_string_144 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
C_name_148 AgdaAny | C_meta_152 AgdaAny
d_Term_154 :: ()
d_Term_154 = ()
data T_Term_154
= C_var_172 Integer [T_Arg_88] | C_con_178 AgdaAny [T_Arg_88] |
C_def_184 AgdaAny [T_Arg_88] |
C_lam_190 T_Visibility_48 T_Abs_112 |
C_pat'45'lam_196 [T_Clause_160] [T_Arg_88] |
C_pi_202 T_Arg_88 T_Abs_112 | C_agda'45'sort_206 T_Sort_156 |
C_lit_210 T_Literal_124 | C_meta_214 AgdaAny [T_Arg_88] |
C_unknown_216
d_Sort_156 :: ()
d_Sort_156 = ()
data T_Sort_156
= C_set_220 T_Term_154 | C_lit_224 Integer |
C_prop_228 T_Term_154 | C_propLit_232 Integer | C_inf_236 Integer |
C_unknown_238
d_Pattern_158 :: ()
d_Pattern_158 = ()
data T_Pattern_158
= C_con_244 AgdaAny [T_Arg_88] | C_dot_248 T_Term_154 |
C_var_252 Integer | C_lit_256 T_Literal_124 | C_proj_260 AgdaAny |
C_absurd_264 Integer
d_Clause_160 :: ()
d_Clause_160 = ()
data T_Clause_160
= C_clause_272 [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] [T_Arg_88]
T_Term_154 |
C_absurd'45'clause_278 [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
[T_Arg_88]
d_Type_162 :: ()
d_Type_162 :: ()
d_Type_162 = ()
forall a. a
erased
d_Telescope_164 :: ()
d_Telescope_164 :: ()
d_Telescope_164 = ()
forall a. a
erased
d_Definition_280 :: ()
d_Definition_280 = ()
data T_Definition_280
= C_function_284 [T_Clause_160] |
C_data'45'type_290 Integer [AgdaAny] |
C_record'45'type_296 AgdaAny [T_Arg_88] |
C_data'45'cons_302 AgdaAny T_Quantity_62 | C_axiom_304 |
C_prim'45'fun_306
d_ErrorPart_308 :: ()
d_ErrorPart_308 = ()
data T_ErrorPart_308
= C_strErr_310 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
C_termErr_312 T_Term_154 | C_pattErr_314 T_Pattern_158 |
C_nameErr_316 AgdaAny
d_TC_320 :: a
d_TC_320
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.TC"
d_returnTC_326 :: a
d_returnTC_326 = a
forall a. a
erased
d_bindTC_336 :: a
d_bindTC_336 = a
forall a. a
erased
d_unify_338 :: a
d_unify_338 = a
forall a. a
erased
d_typeError_344 :: a
d_typeError_344 = a
forall a. a
erased
d_inferType_346 :: a
d_inferType_346 = a
forall a. a
erased
d_checkType_348 :: a
d_checkType_348 = a
forall a. a
erased
d_normalise_350 :: a
d_normalise_350 = a
forall a. a
erased
d_reduce_352 :: a
d_reduce_352 = a
forall a. a
erased
d_catchTC_358 :: a
d_catchTC_358 = a
forall a. a
erased
d_quoteTC_364 :: a
d_quoteTC_364 = a
forall a. a
erased
d_unquoteTC_370 :: a
d_unquoteTC_370 = a
forall a. a
erased
d_quoteωTC_374 :: a
d_quoteωTC_374 = a
forall a. a
erased
d_getContext_376 :: a
d_getContext_376 = a
forall a. a
erased
d_extendContext_382 :: a
d_extendContext_382 = a
forall a. a
erased
d_inContext_388 :: a
d_inContext_388 = a
forall a. a
erased
d_freshName_390 :: a
d_freshName_390 = a
forall a. a
erased
d_declareDef_392 :: a
d_declareDef_392 = a
forall a. a
erased
d_declarePostulate_394 :: a
d_declarePostulate_394 = a
forall a. a
erased
d_declareData_396 :: a
d_declareData_396 = a
forall a. a
erased
d_defineData_402 :: a
d_defineData_402 = a
forall a. a
erased
d_defineFun_404 :: a
d_defineFun_404 = a
forall a. a
erased
d_getType_406 :: a
d_getType_406 = a
forall a. a
erased
d_getDefinition_408 :: a
d_getDefinition_408 = a
forall a. a
erased
d_blockTC_414 :: a
d_blockTC_414 = a
forall a. a
erased
d_commitTC_416 :: a
d_commitTC_416 = a
forall a. a
erased
d_isMacro_418 :: a
d_isMacro_418 = a
forall a. a
erased
d_pragmaForeign_420 :: a
d_pragmaForeign_420 = a
forall a. a
erased
d_pragmaCompile_422 :: a
d_pragmaCompile_422 = a
forall a. a
erased
d_withNormalisation_428 :: a
d_withNormalisation_428 = a
forall a. a
erased
d_askNormalisation_430 :: a
d_askNormalisation_430 = a
forall a. a
erased
d_withReconstructed_436 :: a
d_withReconstructed_436 = a
forall a. a
erased
d_askReconstructed_438 :: a
d_askReconstructed_438 = a
forall a. a
erased
d_withExpandLast_444 :: a
d_withExpandLast_444 = a
forall a. a
erased
d_askExpandLast_446 :: a
d_askExpandLast_446 = a
forall a. a
erased
d_withReduceDefs_454 :: a
d_withReduceDefs_454 = a
forall a. a
erased
d_askReduceDefs_458 :: a
d_askReduceDefs_458 = a
forall a. a
erased
d_formatErrorParts_460 :: a
d_formatErrorParts_460 = a
forall a. a
erased
d_debugPrint_462 :: a
d_debugPrint_462 = a
forall a. a
erased
d_noConstraints_468 :: a
d_noConstraints_468 = a
forall a. a
erased
d_workOnTypes_474 :: a
d_workOnTypes_474 = a
forall a. a
erased
d_runSpeculative_482 :: a
d_runSpeculative_482 = a
forall a. a
erased
d_getInstances_484 :: a
d_getInstances_484 = a
forall a. a
erased
d_solveInstanceConstraints_486 :: a
d_solveInstanceConstraints_486 = a
forall a. a
erased
d_filter_488 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 AgdaAny -> Bool
v0 [AgdaAny]
v1
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[] -> [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1
(:) AgdaAny
v2 [AgdaAny]
v3
-> let v4 :: t
v4 = (AgdaAny -> Bool) -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> Bool
v0 AgdaAny
v2 in
AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
(if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
forall a. a
v4
then (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
(((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Bool
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
else ((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Bool
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
[AgdaAny]
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8712'__514 :: AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 :: AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 AgdaAny
v0 [AgdaAny]
v1
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[] -> Bool -> Bool
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
(:) AgdaAny
v2 [AgdaAny]
v3
-> let v4 :: t
v4 = (QName -> QName -> Bool) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe QName -> QName -> Bool
d_primQNameEquality_8 AgdaAny
v0 AgdaAny
v2 in
AgdaAny -> Bool
forall a b. a -> b
coe
(if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
forall a. a
v4 then AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4 else (AgdaAny -> [AgdaAny] -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))
[AgdaAny]
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8713'__540 :: AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 :: AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 AgdaAny
v0 [AgdaAny]
v1
= let v2 :: Bool
v2 = AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) ([AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1) in
AgdaAny -> Bool
forall a b. a -> b
coe
(if Bool -> Bool
forall a b. a -> b
coe Bool
v2
then Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
else Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
d__'43''43'__558 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 [AgdaAny]
v0 [AgdaAny]
v1
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
[] -> [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1
(:) AgdaAny
v2 [AgdaAny]
v3
-> (AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
(([AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))
[AgdaAny]
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_combineReduceDefs_574 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_combineReduceDefs_574 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_574 T_Σ_14
v0 T_Σ_14
v1
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
-> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v2
then case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
-> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v4
then (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
(((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8712'__514 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v3)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
else (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
(((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v5)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
else (case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
-> if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v4
then (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
(((AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_488 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8713'__540 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v3)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
else (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
(([AgdaAny] -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__558 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_onlyReduceDefs_602 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [AgdaAny] -> AgdaAny -> AgdaAny
d_onlyReduceDefs_602 :: () -> () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_onlyReduceDefs_602 ()
v0 ~()
v1 [AgdaAny]
v2 AgdaAny
v3 = () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_602 ()
v0 [AgdaAny]
v2 AgdaAny
v3
du_onlyReduceDefs_602 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
[AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_602 :: () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_602 ()
v0 [AgdaAny]
v1 AgdaAny
v2
= AgdaAny
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_bindTC_336 () ()
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
d_askReduceDefs_458
(\ AgdaAny
v3 ->
AgdaAny -> () -> AgdaAny -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_withReduceDefs_454 ()
v0 AgdaAny
forall a. a
erased
(T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_574
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))
(AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3))
AgdaAny
v2)
d_dontReduceDefs_608 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [AgdaAny] -> AgdaAny -> AgdaAny
d_dontReduceDefs_608 :: () -> () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_dontReduceDefs_608 ()
v0 ~()
v1 [AgdaAny]
v2 AgdaAny
v3 = () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_608 ()
v0 [AgdaAny]
v2 AgdaAny
v3
du_dontReduceDefs_608 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
[AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_608 :: () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_608 ()
v0 [AgdaAny]
v1 AgdaAny
v2
= AgdaAny
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_bindTC_336 () ()
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
d_askReduceDefs_458
(\ AgdaAny
v3 ->
AgdaAny -> () -> AgdaAny -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_withReduceDefs_454 ()
v0 AgdaAny
forall a. a
erased
(T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_574
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))
(AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3))
AgdaAny
v2)
d_blockOnMeta_626 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny -> AgdaAny
d_blockOnMeta_626 :: () -> () -> AgdaAny -> AgdaAny
d_blockOnMeta_626 ()
v0 ~()
v1 AgdaAny
v2 = () -> AgdaAny -> AgdaAny
du_blockOnMeta_626 ()
v0 AgdaAny
v2
du_blockOnMeta_626 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> AgdaAny -> AgdaAny
du_blockOnMeta_626 :: () -> AgdaAny -> AgdaAny
du_blockOnMeta_626 ()
v0 AgdaAny
v1
= AgdaAny -> () -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
d_blockTC_414 ()
v0 AgdaAny
forall a. a
erased ((AgdaAny -> T_Blocker_100) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Blocker_100
C_blockerMeta_106 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))