{-# 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.Relation.Nullary.Decidable 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.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Function.Equality
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Function.Injection
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d_map_14 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_map_14 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_16
-> T_Dec_32
-> T_Dec_32
d_map_14 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Equivalence_16
v4 = T_Equivalence_16 -> T_Dec_32 -> T_Dec_32
du_map_14 T_Equivalence_16
v4
du_map_14 ::
MAlonzo.Code.Function.Equivalence.T_Equivalence_16 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_map_14 :: T_Equivalence_16 -> T_Dec_32 -> T_Dec_32
du_map_14 T_Equivalence_16
v0
= ((Any -> Any) -> T_Dec_32 -> T_Dec_32)
-> Any -> T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe
(Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
((T_Π_16 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
((T_Equivalence_16 -> T_Π_16) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_16 -> T_Π_16
MAlonzo.Code.Function.Equivalence.d_to_34 (T_Equivalence_16 -> Any
forall a b. a -> b
coe T_Equivalence_16
v0)))
d__'8776'__62 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
AgdaAny -> AgdaAny -> ()
d__'8776'__62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> Any
-> Any
-> T_Level_18
d__'8776'__62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> Any
-> Any
-> T_Level_18
forall a. a
erased
d__'8776'__66 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
AgdaAny -> AgdaAny -> ()
d__'8776'__66 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> Any
-> Any
-> T_Level_18
d__'8776'__66 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> Any
-> Any
-> T_Level_18
forall a. a
erased
d_via'45'injection_68 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
MAlonzo.Code.Function.Injection.T_Injection_88 ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_via'45'injection_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_44
-> T_Setoid_44
-> T_Injection_88
-> (Any -> Any -> T_Dec_32)
-> Any
-> Any
-> T_Dec_32
d_via'45'injection_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_44
v4 ~T_Setoid_44
v5 T_Injection_88
v6 Any -> Any -> T_Dec_32
v7 Any
v8 Any
v9
= T_Injection_88
-> (Any -> Any -> T_Dec_32) -> Any -> Any -> T_Dec_32
du_via'45'injection_68 T_Injection_88
v6 Any -> Any -> T_Dec_32
v7 Any
v8 Any
v9
du_via'45'injection_68 ::
MAlonzo.Code.Function.Injection.T_Injection_88 ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_via'45'injection_68 :: T_Injection_88
-> (Any -> Any -> T_Dec_32) -> Any -> Any -> T_Dec_32
du_via'45'injection_68 T_Injection_88
v0 Any -> Any -> T_Dec_32
v1 Any
v2 Any
v3
= ((Any -> Any) -> T_Dec_32 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
(Any -> Any) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
((T_Injection_88 -> Any -> Any -> Any -> Any)
-> T_Injection_88 -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_88 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Injection.d_injective_108 T_Injection_88
v0 Any
v2 Any
v3)
((Any -> Any -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Dec_32
v1
((T_Π_16 -> Any -> Any) -> T_Π_16 -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106 (T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v0)) Any
v2)
((T_Π_16 -> Any -> Any) -> T_Π_16 -> Any -> Any
forall a b. a -> b
coe
T_Π_16 -> Any -> Any
MAlonzo.Code.Function.Equality.d__'10216''36''10217'__38
(T_Injection_88 -> T_Π_16
MAlonzo.Code.Function.Injection.d_to_106 (T_Injection_88 -> T_Injection_88
forall a b. a -> b
coe T_Injection_88
v0)) Any
v3))
d_True'45''8596'_78 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
(AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Function.Bundles.T_Inverse_1048
d_True'45''8596'_78 :: T_Level_18
-> T_Level_18
-> T_Dec_32
-> (Any -> Any -> T__'8801'__12)
-> T_Inverse_1048
d_True'45''8596'_78 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 ~Any -> Any -> T__'8801'__12
v3 = T_Dec_32 -> T_Inverse_1048
du_True'45''8596'_78 T_Dec_32
v2
du_True'45''8596'_78 ::
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Function.Bundles.T_Inverse_1048
du_True'45''8596'_78 :: T_Dec_32 -> T_Inverse_1048
du_True'45''8596'_78 T_Dec_32
v0
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v1 T_Reflects_14
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then ((Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> (Any -> T__'8801'__12)
-> T_Inverse_1048)
-> Any -> Any -> Any -> Any -> T_Inverse_1048
forall a b. a -> b
coe
(Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> (Any -> T__'8801'__12)
-> T_Inverse_1048
MAlonzo.Code.Function.Bundles.du_mk'8596''8242'_1382
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20 (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)))
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v3 -> T_Level_18 -> Any
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)) Any
forall a. a
erased
Any
forall a. a
erased
else (Any -> Any -> Any) -> Any -> Any -> T_Inverse_1048
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v2)
(((Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> (Any -> T__'8801'__12)
-> T_Inverse_1048)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any)
-> (Any -> Any)
-> (Any -> T__'8801'__12)
-> (Any -> T__'8801'__12)
-> T_Inverse_1048
MAlonzo.Code.Function.Bundles.du_mk'8596''8242'_1382 Any
forall a. a
erased
((T_Reflects_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Reflects_14 -> Any
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_20
(T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
Any
forall a. a
erased Any
forall a. a
erased)
T_Dec_32
_ -> T_Inverse_1048
forall a. a
MAlonzo.RTE.mazUnreachableError