{-# 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.Data.List.NonEmpty 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Properties
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.NonEmpty.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
d_split_20 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> Bool) ->
[AgdaAny] -> [MAlonzo.Code.Data.Sum.Base.T__'8846'__30]
d_split_20 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30]
d_split_20 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> Bool
v2 [AgdaAny]
v3 = (AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30]
du_split_20 AgdaAny -> Bool
v2 [AgdaAny]
v3
du_split_20 ::
(AgdaAny -> Bool) ->
[AgdaAny] -> [MAlonzo.Code.Data.Sum.Base.T__'8846'__30]
du_split_20 :: (AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30]
du_split_20 AgdaAny -> Bool
v0 [AgdaAny]
v1
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[] -> [AgdaAny] -> [T__'8846'__30]
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 -> [T__'8846'__30]
forall a b. a -> b
coe
(let v5 :: t
v5 = ((AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30])
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe (AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30]
du_split_20 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Bool
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4
then let v6 :: t
v6
= (AgdaAny -> [AgdaAny] -> [AgdaAny]) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
((AgdaAny -> T_List'8314'_24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du_'91'_'93'_44
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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)
((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
((Bool -> T_Equivalence_16) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
Bool -> T_Equivalence_16
MAlonzo.Code.Data.Bool.Properties.d_T'45''8801'_2190
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4)))
AgdaAny
forall {t}. t
erased))))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v5) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
forall {t}. t
v5 of
(:) AgdaAny
v7 [AgdaAny]
v8
-> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9
-> (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 -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
((AgdaAny -> T_List'8314'_24 -> T_List'8314'_24)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_List'8314'_24 -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du__'8759''8314'__48
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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)
((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
((Bool -> T_Equivalence_16) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
Bool -> T_Equivalence_16
MAlonzo.Code.Data.Bool.Properties.d_T'45''8801'_2190
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4)))
AgdaAny
forall {t}. t
erased))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)))
([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v8)
T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v6
[AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v6)
else (let v6 :: t
v6
= (AgdaAny -> [AgdaAny] -> [AgdaAny]) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((AgdaAny -> T_List'8314'_24) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du_'91'_'93'_44
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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)
((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
((Bool -> T_Equivalence_16) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
Bool -> T_Equivalence_16
MAlonzo.Code.Data.Bool.Properties.d_T'45'not'45''8801'_2194
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4)))
AgdaAny
forall {t}. t
erased))))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v5) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
forall {t}. t
v5 of
(:) AgdaAny
v7 [AgdaAny]
v8
-> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
-> (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 -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((AgdaAny -> T_List'8314'_24 -> T_List'8314'_24)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_List'8314'_24 -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du__'8759''8314'__48
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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)
((T_Π_16 -> AgdaAny -> AgdaAny) -> T_Π_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Π_16 -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_from_36
((Bool -> T_Equivalence_16) -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
Bool -> T_Equivalence_16
MAlonzo.Code.Data.Bool.Properties.d_T'45'not'45''8801'_2194
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v4)))
AgdaAny
forall {t}. t
erased))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)))
([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v8)
T__'8846'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v6
[AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall {t}. t
v6))))
[AgdaAny]
_ -> [T__'8846'__30]
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_flatten_86 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
[MAlonzo.Code.Data.Sum.Base.T__'8846'__30] -> [AgdaAny]
d_flatten_86 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> [T__'8846'__30]
-> [AgdaAny]
d_flatten_86 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 [T__'8846'__30]
v6 = [T__'8846'__30] -> [AgdaAny]
du_flatten_86 [T__'8846'__30]
v6
du_flatten_86 ::
[MAlonzo.Code.Data.Sum.Base.T__'8846'__30] -> [AgdaAny]
du_flatten_86 :: [T__'8846'__30] -> [AgdaAny]
du_flatten_86 [T__'8846'__30]
v0
= ([[AgdaAny]] -> [AgdaAny]) -> AgdaAny -> [AgdaAny]
forall a b. a -> b
coe
[[AgdaAny]] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_concat_268
(((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 ->
(T_List'8314'_24 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_List'8314'_24 -> [AgdaAny]
MAlonzo.Code.Data.List.NonEmpty.Base.du_toList_62
(((AgdaAny -> AgdaAny) -> T_List'8314'_24 -> T_List'8314'_24)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_List'8314'_24 -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du_map_100
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 ->
(T_List'8314'_24 -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_List'8314'_24 -> [AgdaAny]
MAlonzo.Code.Data.List.NonEmpty.Base.du_toList_62
(((AgdaAny -> AgdaAny) -> T_List'8314'_24 -> T_List'8314'_24)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_List'8314'_24 -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du_map_100
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)))))
([T__'8846'__30] -> AgdaAny
forall a b. a -> b
coe [T__'8846'__30]
v0))
d_flatten'45'split_92 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> Bool) ->
[AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_flatten'45'split_92 :: T_Level_18
-> T_Level_18 -> (AgdaAny -> Bool) -> [AgdaAny] -> T__'8801'__12
d_flatten'45'split_92 = T_Level_18
-> T_Level_18 -> (AgdaAny -> Bool) -> [AgdaAny] -> T__'8801'__12
forall {t}. t
erased
d_wordsBy_154 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> Bool) ->
[AgdaAny] -> [MAlonzo.Code.Data.List.NonEmpty.Base.T_List'8314'_24]
d_wordsBy_154 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> Bool)
-> [AgdaAny]
-> [T_List'8314'_24]
d_wordsBy_154 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> Bool
v2 [AgdaAny]
v3 = (AgdaAny -> Bool) -> [AgdaAny] -> [T_List'8314'_24]
du_wordsBy_154 AgdaAny -> Bool
v2 [AgdaAny]
v3
du_wordsBy_154 ::
(AgdaAny -> Bool) ->
[AgdaAny] -> [MAlonzo.Code.Data.List.NonEmpty.Base.T_List'8314'_24]
du_wordsBy_154 :: (AgdaAny -> Bool) -> [AgdaAny] -> [T_List'8314'_24]
du_wordsBy_154 AgdaAny -> Bool
v0 [AgdaAny]
v1
= ((AgdaAny -> Maybe AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_List'8314'_24]
forall a b. a -> b
coe
(AgdaAny -> Maybe AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_mapMaybe_32
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> AgdaAny
MAlonzo.Code.Data.Sum.Base.du_'91'_'44'_'93'_52
(let v2 :: b
v2 = Maybe AgdaAny -> b
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
forall {t}. t
v2)))
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
((AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16)
(((AgdaAny -> AgdaAny) -> T_List'8314'_24 -> T_List'8314'_24)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_List'8314'_24 -> T_List'8314'_24
MAlonzo.Code.Data.List.NonEmpty.Base.du_map_100
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v2 -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2))))))
(((AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> Bool) -> [AgdaAny] -> [T__'8846'__30]
du_split_20 ((AgdaAny -> Bool) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Bool
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v1))