{-# 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_300 AgdaAny | C_axiom_302 | C_prim'45'fun_304
d_ErrorPart_306 :: ()
d_ErrorPart_306 = ()
data T_ErrorPart_306
= C_strErr_308 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
C_termErr_310 T_Term_154 | C_pattErr_312 T_Pattern_158 |
C_nameErr_314 AgdaAny
d_TC_318 :: a
d_TC_318
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.TC"
d_returnTC_324 :: a
d_returnTC_324 = a
forall a. a
erased
d_bindTC_334 :: a
d_bindTC_334 = a
forall a. a
erased
d_unify_336 :: a
d_unify_336 = a
forall a. a
erased
d_typeError_342 :: a
d_typeError_342 = a
forall a. a
erased
d_inferType_344 :: a
d_inferType_344 = a
forall a. a
erased
d_checkType_346 :: a
d_checkType_346 = a
forall a. a
erased
d_normalise_348 :: a
d_normalise_348 = a
forall a. a
erased
d_reduce_350 :: a
d_reduce_350 = a
forall a. a
erased
d_catchTC_356 :: a
d_catchTC_356 = a
forall a. a
erased
d_quoteTC_362 :: a
d_quoteTC_362 = a
forall a. a
erased
d_unquoteTC_368 :: a
d_unquoteTC_368 = a
forall a. a
erased
d_quoteωTC_372 :: a
d_quoteωTC_372 = a
forall a. a
erased
d_getContext_374 :: a
d_getContext_374 = a
forall a. a
erased
d_extendContext_380 :: a
d_extendContext_380 = a
forall a. a
erased
d_inContext_386 :: a
d_inContext_386 = a
forall a. a
erased
d_freshName_388 :: a
d_freshName_388 = a
forall a. a
erased
d_declareDef_390 :: a
d_declareDef_390 = a
forall a. a
erased
d_declarePostulate_392 :: a
d_declarePostulate_392 = a
forall a. a
erased
d_declareData_394 :: a
d_declareData_394 = a
forall a. a
erased
d_defineData_398 :: a
d_defineData_398 = a
forall a. a
erased
d_defineFun_400 :: a
d_defineFun_400 = a
forall a. a
erased
d_getType_402 :: a
d_getType_402 = a
forall a. a
erased
d_getDefinition_404 :: a
d_getDefinition_404 = a
forall a. a
erased
d_blockTC_410 :: a
d_blockTC_410 = a
forall a. a
erased
d_commitTC_412 :: a
d_commitTC_412 = a
forall a. a
erased
d_isMacro_414 :: a
d_isMacro_414 = a
forall a. a
erased
d_pragmaForeign_416 :: a
d_pragmaForeign_416 = a
forall a. a
erased
d_pragmaCompile_418 :: a
d_pragmaCompile_418 = a
forall a. a
erased
d_withNormalisation_424 :: a
d_withNormalisation_424 = a
forall a. a
erased
d_askNormalisation_426 :: a
d_askNormalisation_426 = a
forall a. a
erased
d_withReconstructed_432 :: a
d_withReconstructed_432 = a
forall a. a
erased
d_askReconstructed_434 :: a
d_askReconstructed_434 = a
forall a. a
erased
d_withExpandLast_440 :: a
d_withExpandLast_440 = a
forall a. a
erased
d_askExpandLast_442 :: a
d_askExpandLast_442 = a
forall a. a
erased
d_withReduceDefs_450 :: a
d_withReduceDefs_450 = a
forall a. a
erased
d_askReduceDefs_454 :: a
d_askReduceDefs_454 = a
forall a. a
erased
d_formatErrorParts_456 :: a
d_formatErrorParts_456 = a
forall a. a
erased
d_debugPrint_458 :: a
d_debugPrint_458 = a
forall a. a
erased
d_noConstraints_464 :: a
d_noConstraints_464 = a
forall a. a
erased
d_runSpeculative_472 :: a
d_runSpeculative_472 = a
forall a. a
erased
d_getInstances_474 :: a
d_getInstances_474 = a
forall a. a
erased
d_filter_476 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_476 :: (AgdaAny -> Bool) -> [AgdaAny] -> [AgdaAny]
d_filter_476 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_476 ((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_476 ((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'__502 :: AgdaAny -> [AgdaAny] -> Bool
d__'8712'__502 :: AgdaAny -> [AgdaAny] -> Bool
d__'8712'__502 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'__502 (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'__528 :: AgdaAny -> [AgdaAny] -> Bool
d__'8713'__528 :: AgdaAny -> [AgdaAny] -> Bool
d__'8713'__528 AgdaAny
v0 [AgdaAny]
v1
= let v2 :: Bool
v2 = AgdaAny -> [AgdaAny] -> Bool
d__'8712'__502 (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'__546 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__546 :: [AgdaAny] -> [AgdaAny] -> [AgdaAny]
d__'43''43'__546 [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'__546 ([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_562 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_combineReduceDefs_562 :: T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_562 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_476 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8712'__502 (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_476 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8713'__528 (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_476 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny -> [AgdaAny] -> Bool
d__'8713'__528 (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'__546 (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_590 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [AgdaAny] -> AgdaAny -> AgdaAny
d_onlyReduceDefs_590 :: () -> () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_onlyReduceDefs_590 ()
v0 ~()
v1 [AgdaAny]
v2 AgdaAny
v3 = () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_590 ()
v0 [AgdaAny]
v2 AgdaAny
v3
du_onlyReduceDefs_590 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
[AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_590 :: () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_onlyReduceDefs_590 ()
v0 [AgdaAny]
v1 AgdaAny
v2
= AgdaAny
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_bindTC_334 () ()
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
d_askReduceDefs_454
(\ AgdaAny
v3 ->
AgdaAny -> () -> AgdaAny -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_withReduceDefs_450 ()
v0 AgdaAny
forall a. a
erased
(T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_562
((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_596 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> [AgdaAny] -> AgdaAny -> AgdaAny
d_dontReduceDefs_596 :: () -> () -> [AgdaAny] -> AgdaAny -> AgdaAny
d_dontReduceDefs_596 ()
v0 ~()
v1 [AgdaAny]
v2 AgdaAny
v3 = () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_596 ()
v0 [AgdaAny]
v2 AgdaAny
v3
du_dontReduceDefs_596 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
[AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_596 :: () -> [AgdaAny] -> AgdaAny -> AgdaAny
du_dontReduceDefs_596 ()
v0 [AgdaAny]
v1 AgdaAny
v2
= AgdaAny
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_bindTC_334 () ()
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny
forall a. a
d_askReduceDefs_454
(\ AgdaAny
v3 ->
AgdaAny -> () -> AgdaAny -> T_Σ_14 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
d_withReduceDefs_450 ()
v0 AgdaAny
forall a. a
erased
(T_Σ_14 -> T_Σ_14 -> T_Σ_14
d_combineReduceDefs_562
((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_614 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny -> AgdaAny
d_blockOnMeta_614 :: () -> () -> AgdaAny -> AgdaAny
d_blockOnMeta_614 ()
v0 ~()
v1 AgdaAny
v2 = () -> AgdaAny -> AgdaAny
du_blockOnMeta_614 ()
v0 AgdaAny
v2
du_blockOnMeta_614 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> AgdaAny -> AgdaAny
du_blockOnMeta_614 :: () -> AgdaAny -> AgdaAny
du_blockOnMeta_614 ()
v0 AgdaAny
v1
= AgdaAny -> () -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
d_blockTC_410 ()
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))