{-# 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.VerifiedCompilation.UForceDelay 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.RenamingSubstitution
import qualified MAlonzo.Code.VerifiedCompilation.Certificate
import qualified MAlonzo.Code.VerifiedCompilation.Equality
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews
d_pureFD_8 :: p -> p -> p -> p -> ()
d_pureFD_8 p
a0 p
a1 p
a2 p
a3 = ()
data T_pureFD_8
= C_forcedelay_18 T_pureFD_8 | C_pushfd_28 T_pureFD_8 T_pureFD_8 |
C__'10814'__36 MAlonzo.Code.Untyped.T__'8866'_14 T_pureFD_8
T_pureFD_8 |
C_translationfd_42 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 |
C_appfd_50 | C_appfd'8315''185'_58
d_forceappdelay_62 :: T_pureFD_8
d_forceappdelay_62 :: T_pureFD_8
d_forceappdelay_62
= (T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8)
-> Any -> Any -> Any -> T_pureFD_8
forall a b. a -> b
coe
T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C__'10814'__36
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26
((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))))
((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)))
((T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8) -> Any -> Any -> Any
forall a b. a -> b
coe
T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C_pushfd_28
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_TransMatch_24) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_delay_62
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
(T_TransMatch_24 -> Any
forall a b. a -> b
coe
T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_34)))))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
((Any -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.d_EmptyEq_128)))))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_Translation_16 -> T_TransMatch_24)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_50
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_TransMatch_24) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_40
((Any -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_100
((T_pureFD_8 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_pureFD_8 -> T_pureFD_8
C_forcedelay_18
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
(T_TransMatch_24 -> Any
forall a b. a -> b
coe
T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_34)))))))
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
(T_TransMatch_24 -> Any
forall a b. a -> b
coe
T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_34)))))
d_test4_78 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> T_pureFD_8
d_test4_78 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T_pureFD_8
d_test4_78 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 T__'8866'_14
v4 = T_DecEq_6
-> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14 -> T_pureFD_8
du_test4_78 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 T__'8866'_14
v4
du_test4_78 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> T_pureFD_8
du_test4_78 :: T_DecEq_6
-> T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14 -> T_pureFD_8
du_test4_78 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2 T__'8866'_14
v3
= (T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8)
-> Any -> Any -> Any -> T_pureFD_8
forall a b. a -> b
coe
T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C__'10814'__36
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)))
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2)))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_TransMatch_24) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_force_56
((Any -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_100
(T_pureFD_8 -> Any
forall a b. a -> b
coe T_pureFD_8
C_appfd_50)))))
((T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C__'10814'__36
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)))
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3)))))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
((T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8) -> Any -> Any -> Any
forall a b. a -> b
coe
T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C_pushfd_28
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)))
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3)))
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0))))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0))))
((T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C__'10814'__36
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1))))
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_Translation_16 -> T_TransMatch_24)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_50
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_TransMatch_24) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_40
((Any -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_100
((T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8) -> Any -> Any -> Any
forall a b. a -> b
coe
T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C_pushfd_28
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1))
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)))))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0))))))))
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)))))
((T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_pureFD_8 -> T_pureFD_8 -> T_pureFD_8
C__'10814'__36
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1))
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_Translation_16 -> T_TransMatch_24)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_50
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_TransMatch_24) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_40
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_Translation_16 -> T_TransMatch_24)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_50
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
((T_Translation_16 -> T_TransMatch_24) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_40
((Any -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_100
((T_pureFD_8 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_pureFD_8 -> T_pureFD_8
C_forcedelay_18
((T_Translation_16 -> T_pureFD_8) -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_pureFD_8
C_translationfd_42
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)))))))))
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.RenamingSubstitution.du_weaken_88
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)))))))
((T__'8866'_14 -> T_DecEq_6 -> T_Translation_16)
-> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_DecEq_6 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1756
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)))))
(T_pureFD_8 -> Any
forall a b. a -> b
coe T_pureFD_8
C_appfd'8315''185'_58))))
d_FD_84 :: p -> p -> p -> p -> p -> p -> ()
d_FD_84 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_FD_84
= C_forcefd_98 T_FD_84 | C_delayfd_108 T_FD_84 |
C_lastdelay_118 Integer Integer
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 |
C_multiappliedfd_132 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
T_FD_84 |
C_multiabstractfd_142 T_FD_84
d_ForceDelay_160 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_ForceDelay_160 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_ForceDelay_160 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
d_t_162 :: MAlonzo.Code.Untyped.T__'8866'_14
d_t_162 :: T__'8866'_14
d_t_162
= (T__'8866'_14 -> T__'8866'_14) -> Any -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46))))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46))
d_t''_164 :: MAlonzo.Code.Untyped.T__'8866'_14
d_t''_164 :: T__'8866'_14
d_t''_164
= (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
MAlonzo.Code.Untyped.C_error_46)
d_test'45'ffdd_166 :: T_FD_84
d_test'45'ffdd_166 :: T_FD_84
d_test'45'ffdd_166
= (T_FD_84 -> T_FD_84) -> Any -> T_FD_84
forall a b. a -> b
coe
T_FD_84 -> T_FD_84
C_forcefd_98
((T_FD_84 -> T_FD_84) -> Any -> Any
forall a b. a -> b
coe
T_FD_84 -> T_FD_84
C_forcefd_98
((T_FD_84 -> T_FD_84) -> Any -> Any
forall a b. a -> b
coe
T_FD_84 -> T_FD_84
C_delayfd_108
((Integer -> Integer -> T_Translation_16 -> T_FD_84)
-> Integer -> Integer -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Translation_16 -> T_FD_84
C_lastdelay_118 (Integer
0 :: Integer) (Integer
0 :: Integer)
((T_TransMatch_24 -> T_Translation_16) -> Any -> Any
forall a b. a -> b
coe
T_TransMatch_24 -> T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_106
(T_TransMatch_24 -> Any
forall a b. a -> b
coe
T_TransMatch_24
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_error_90)))))
d_isForceDelay'63'_176 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isForceDelay'63'_176 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isForceDelay'63'_176 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isForceDelay'63'_176 T_DecEq_6
v1
du_isForceDelay'63'_176 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isForceDelay'63'_176 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isForceDelay'63'_176 T_DecEq_6
v0
= (()
-> T_DecEq_6
-> T_SimplifierTag_4
-> (()
-> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26)
-> Any
-> Any
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
forall a b. a -> b
coe
()
-> T_DecEq_6
-> T_SimplifierTag_4
-> (()
-> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_178
Any
forall a. a
erased (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)
(T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 ->
(T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186 (Any -> Any
forall a b. a -> b
coe Any
v2) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))))
d_isFD'63'_186 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isFD'63'_186 :: ()
-> T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
d_isFD'63'_186 ~()
v0 T_DecEq_6
v1 Integer
v2 Integer
v3 T__'8866'_14
v4 T__'8866'_14
v5 = T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186 T_DecEq_6
v1 Integer
v2 Integer
v3 T__'8866'_14
v4 T__'8866'_14
v5
du_isFD'63'_186 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isFD'63'_186 :: T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186 T_DecEq_6
v0 Integer
v1 Integer
v2 T__'8866'_14
v3 T__'8866'_14
v4
= let v5 :: t
v5
= (()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
() -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isForce'63'_284
Any
forall a. a
erased
(\ Any
v5 Any
v6 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3) in
Any -> T_ProofOrCE_26
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v7 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v8
-> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v8 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v10
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v11
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v10)
(let v12 :: t
v12
= (()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
Any
forall a. a
erased
(\ Any
v12 Any
v13 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(\ Any
v12 Any
v13 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v12 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v13 T_Reflects_16
v14
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v13
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v14 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v15
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v15 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v18 Any
v19
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v20 T__'8866'_14
v21
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v18)
((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe Any
v19)
(let v22 :: t
v22
= (()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
Any
forall a. a
erased
(\ Any
v22
Any
v23 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(\ Any
v22
Any
v23 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v4) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe
Any
forall a. a
v22 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v23 T_Reflects_16
v24
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v23
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v24 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v25
-> case Any -> T_isApp_142
forall a b. a -> b
coe
Any
v25 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v28 Any
v29
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v4 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v30 T__'8866'_14
v31
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v28)
((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v29)
(let v32 :: t
v32
= (T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0)
(Integer -> Any
forall a b. a -> b
coe
Integer
v1)
((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 -> Any
forall a b. a -> b
coe
Integer
v2))
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v20))
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v30) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
Any
forall a. a
v32 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v33
-> let v34 :: t
v34
= (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> t
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isForceDelay'63'_176
T_DecEq_6
v0
T__'8866'_14
v21
T__'8866'_14
v31 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
Any
forall a. a
v34 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v35
-> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
((T_Translation_16 -> T_FD_84 -> T_FD_84) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Translation_16 -> T_FD_84 -> T_FD_84
C_multiappliedfd_132
Any
v35
Any
v33)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v38 Any
v39 Any
v40
-> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
T_SimplifierTag_4
v38
Any
v39
Any
v40
T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v36 Any
v37 Any
v38
-> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
T_SimplifierTag_4
v36
Any
v37
Any
v38
T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v24)
((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
(T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8)
T__'8866'_14
v3
T__'8866'_14
v4)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v14)
(let v15 :: t
v15
= ((() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
(() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
(\ Any
v15 Any
v16 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v15 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v16 T_Reflects_16
v17
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v16
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v17 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v18
-> case Any -> T_isLambda_54
forall a b. a -> b
coe
Any
v18 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 Any
v20
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v11 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v21
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v20)
(case Integer -> Integer
forall a b. a -> b
coe
Integer
v2 of
Integer
0 -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
(T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8)
T__'8866'_14
v3
T__'8866'_14
v4
Integer
_ -> let v22 :: Integer
v22
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe
Integer
v2)
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer)) in
Any -> Any
forall a b. a -> b
coe
(let v23 :: t
v23
= ((() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
(() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
(\ Any
v23
Any
v24 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v4) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe
Any
forall a. a
v23 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v24 T_Reflects_16
v25
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v24
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v25 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v26
-> case Any -> T_isLambda_54
forall a b. a -> b
coe
Any
v26 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 Any
v28
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v4 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v29
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v28)
(let v30 :: t
v30
= (T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0))
(Integer -> Any
forall a b. a -> b
coe
Integer
v1)
(Integer -> Any
forall a b. a -> b
coe
Integer
v22)
((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v21))
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v29) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
Any
forall a. a
v30 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v31
-> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
((T_FD_84 -> T_FD_84) -> Any -> Any
forall a b. a -> b
coe
T_FD_84 -> T_FD_84
C_multiabstractfd_142
Any
v31)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v34 Any
v35 Any
v36
-> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
T_SimplifierTag_4
v34
Any
v35
Any
v36
T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_54
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v25)
((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
(T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8)
T__'8866'_14
v3
T__'8866'_14
v4)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_54
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v17)
(let v18 :: t
v18
= (T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0)
((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 -> Any
forall a b. a -> b
coe
Integer
v1))
(Integer -> Any
forall a b. a -> b
coe
Integer
v2)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v11)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v4) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
Any
forall a. a
v18 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v19
-> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
((T_FD_84 -> T_FD_84) -> Any -> Any
forall a b. a -> b
coe
T_FD_84 -> T_FD_84
C_forcefd_98
Any
v19)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v22 Any
v23 Any
v24
-> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
T_SimplifierTag_4
v22
Any
v23
Any
v24
T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v7)
(case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
(T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8)
T__'8866'_14
v3 T__'8866'_14
v4
Integer
_ -> let v8 :: Integer
v8 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(let v9 :: t
v9
= (()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any -> t
forall a b. a -> b
coe
() -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isDelay'63'_370
Any
forall a. a
erased
(\ Any
v9 Any
v10 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v9 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v10 T_Reflects_16
v11
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v10
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v11 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v12
-> case Any -> T_isDelay_354
forall a b. a -> b
coe Any
v12 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 Any
v14
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v15
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v14)
(let v16 :: t
v16
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> t
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
(Integer -> Any
forall a b. a -> b
coe Integer
v8)
(Integer -> Any
forall a b. a -> b
coe
(Integer
0 ::
Integer)))
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
(Integer -> Any
forall a b. a -> b
coe Integer
v2)
(Integer -> Any
forall a b. a -> b
coe
(Integer
0 ::
Integer))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v16 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v17 T_Reflects_16
v18
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v17
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v18 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v19
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v19)
(let v20 :: t
v20
= (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> t
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isForceDelay'63'_176
T_DecEq_6
v0
T__'8866'_14
v15
T__'8866'_14
v4 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
Any
forall a. a
v20 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v21
-> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
((Integer -> Integer -> T_Translation_16 -> T_FD_84)
-> Integer -> Integer -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Translation_16 -> T_FD_84
C_lastdelay_118
(Integer
0 ::
Integer)
(Integer
0 ::
Integer)
Any
v21)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v24 Any
v25 Any
v26
-> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
T_SimplifierTag_4
v24
Any
v25
Any
v26
T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v18)
(let v19 :: t
v19
= (T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
du_isFD'63'_186
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0)
(Integer -> Any
forall a b. a -> b
coe
Integer
v8)
(Integer -> Any
forall a b. a -> b
coe
Integer
v2)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v15)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v4) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
Any
forall a. a
v19 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v20
-> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
((T_FD_84 -> T_FD_84) -> Any -> Any
forall a b. a -> b
coe
T_FD_84 -> T_FD_84
C_delayfd_108
Any
v20)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v23 Any
v24 Any
v25
-> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
T_SimplifierTag_4
v23
Any
v24
Any
v25
T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isDelay_354
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v11)
((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
(T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8)
T__'8866'_14
v3 T__'8866'_14
v4)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'46'extendedlambda0_208 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_208 :: ()
-> T__'8866'_14
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda0_208 = ()
-> T__'8866'_14
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda1_246 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_354 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_246 :: ()
-> T__'8866'_14
-> (T_isDelay_354 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda1_246 = ()
-> T__'8866'_14
-> (T_isDelay_354 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda2_322 ::
Integer ->
Integer ->
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda2_322 :: Integer
-> Integer
-> ()
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_Σ_14 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda2_322 = Integer
-> Integer
-> ()
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_Σ_14 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda3_384 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda3_384 :: ()
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda3_384 = ()
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda4_456 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer -> T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda4_456 :: ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda4_456 = ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda5_510 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer ->
(T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda5_510 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda5_510 = ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda6_568 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
Integer ->
Integer ->
T_FD_84 -> T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda6_568 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> Integer
-> T_FD_84
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda6_568 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_16 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> Integer
-> T_FD_84
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda7_646 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer -> T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda7_646 :: ()
-> T__'8866'_14
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> Integer
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda7_646 = ()
-> T__'8866'_14
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> Integer
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda8_694 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer ->
(T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda8_694 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda8_694 = ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda9_728 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda9_728 :: ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda9_728 = ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> Integer
-> T__'8866'_14
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda10_786 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Integer ->
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_FD_84 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda10_786 :: ()
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_isLambda_54 -> T_Irrelevant_20)
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
d_'46'extendedlambda10_786 = ()
-> T__'8866'_14
-> T_DecEq_6
-> Integer
-> Integer
-> T__'8866'_14
-> (T_FD_84 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> (T_isLambda_54 -> T_Irrelevant_20)
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_FD_84
-> T_Irrelevant_20
forall a. a
erased