{-# 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.UFloatDelay 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.Data.Fin.Base
import qualified MAlonzo.Code.Data.Fin.Properties
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
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.Purity
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation.Certificate
import qualified MAlonzo.Code.VerifiedCompilation.Trace
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews
d_subs'45'delay_18 ::
Integer ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14
d_subs'45'delay_18 :: Integer -> T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
d_subs'45'delay_18 ~Integer
v0 T_Fin_10
v1 T__'8866'_14
v2 = T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 T_Fin_10
v1 T__'8866'_14
v2
du_subs'45'delay_18 ::
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14
du_subs'45'delay_18 :: T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 T_Fin_10
v0 T__'8866'_14
v1
= case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v2
-> let v3 :: Any
v3
= (T_Fin_10 -> T_Fin_10 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10 -> T_Dec_20
MAlonzo.Code.Data.Fin.Properties.du__'8799'__50 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0)
(T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v2) in
Any -> T__'8866'_14
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then (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
v5)
((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_Fin_10 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0)))
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
v5) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v2
-> (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_ƛ_20
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 ((T_Fin_10 -> T_Fin_10) -> T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v0)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v2 T__'8866'_14
v3
-> (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_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v2
-> (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_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v2
-> (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_delay_26
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
MAlonzo.Code.Untyped.C_con_28 T_TmCon_202
v2 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
MAlonzo.Code.Untyped.C_constr_34 Integer
v2 [T__'8866'_14]
v3
-> (Integer -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> Any
forall a b. a -> b
coe Integer
v2)
(((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0)) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v3))
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v2 [T__'8866'_14]
v3
-> (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_case_40
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
(((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18 (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v0)) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v3))
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v2 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1
T__'8866'_14
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_FlD_78 :: p -> p -> p -> ()
d_FlD_78 p
a0 p
a1 p
a2 = ()
data T_FlD_78
= C_floatdelay_90 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8
MAlonzo.Code.Untyped.Purity.T_Pure_6
d_FloatDelay_98 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_FloatDelay_98 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
d_FloatDelay_98 = Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
d_isFloatDelay'63'_102 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38
d_isFloatDelay'63'_102 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38
d_isFloatDelay'63'_102 Integer
v0
= (Integer
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_38)
-> Any
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_38
forall a b. a -> b
coe
Integer
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_160
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
(T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12 -> Any
forall a b. a -> b
coe T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_32)
((Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38) -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38
d_isFlD'63'_106)
d_isFlD'63'_106 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_38
d_isFlD'63'_106 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38
d_isFlD'63'_106 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2
= let v3 :: Any
v3
= (Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_168
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_72
(Any -> Any
forall a b. a -> b
coe Any
v3)
(\ Any
v4 Any
v5 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_784)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isDelay'63'_372
(Any -> Any
forall a b. a -> b
coe Any
v3)
(\ Any
v4 Any
v5 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_784)))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) in
Any -> T_ProofOrCE_38
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
-> case Any -> T_isApp_144
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_156 Any
v9 Any
v10
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v11 T__'8866'_14
v12
-> case Any -> T_isLambda_56
forall a b. a -> b
coe Any
v9 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_64 Any
v14
-> 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
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)
(case Any -> T_isDelay_356
forall a b. a -> b
coe Any
v10 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_364 Any
v17
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v12 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
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
v17)
(let v19 :: Any
v19
= (Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_168
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v19 ->
(Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_72
(Any -> Any
forall a b. a -> b
coe
Any
v19)
(\ Any
v20
Any
v21 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_784)))
(\ Any
v19 Any
v20 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_784)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v19 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v20 T_Reflects_16
v21
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v20
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v21 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v22
-> case Any -> T_isApp_144
forall a b. a -> b
coe
Any
v22 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_156 Any
v25 Any
v26
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v27 T__'8866'_14
v28
-> case Any -> T_isLambda_56
forall a b. a -> b
coe
Any
v25 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_64 Any
v30
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v27 of
MAlonzo.Code.Untyped.C_ƛ_20 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
v30)
((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
v26)
(let v32 :: Any
v32
= (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38)
-> Integer -> Any -> T__'8866'_14 -> Any
forall a b. a -> b
coe
Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38
d_isFloatDelay'63'_102
(Integer -> Integer -> Integer
addInt
(Integer -> Integer
forall a b. a -> b
coe
(Integer
1 ::
Integer))
(Integer -> Integer
forall a b. a -> b
coe
Integer
v0))
((T_Fin_10 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_18
(T_Fin_10 -> Any
forall a b. a -> b
coe
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
(T__'8866'_14 -> Any
forall a b. a -> b
coe
T__'8866'_14
v15))
T__'8866'_14
v31 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_38
forall a b. a -> b
coe
Any
v32 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_44 Any
v33
-> let v34 :: Any
v34
= (Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38)
-> Integer -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
Integer -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_38
d_isFloatDelay'63'_102
Integer
v0
T__'8866'_14
v18
T__'8866'_14
v28 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_ProofOrCE_38
forall a b. a -> b
coe
Any
v34 of
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_44 Any
v35
-> let v36 :: T_Dec_20
v36
= Integer -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.Untyped.Purity.d_isPure'63'_72
(Integer -> Integer
forall a b. a -> b
coe
Integer
v0)
(T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v28) in
Any -> Any
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
T_Dec_20
v36 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v37 T_Reflects_16
v38
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v37
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v38 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v39
-> (Any -> T_ProofOrCE_38) -> Any -> Any
forall a b. a -> b
coe
Any -> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_44
((T_Translation_8 -> T_Translation_8 -> T_Pure_6 -> T_FlD_78)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Translation_8 -> T_Translation_8 -> T_Pure_6 -> T_FlD_78
C_floatdelay_90
Any
v33
Any
v35
Any
v39)
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
v38)
((T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> T__'8866'_14
-> T__'8866'_14
-> Any
forall a b. a -> b
coe
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_32
T__'8866'_14
v1
T__'8866'_14
v2)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v38 Any
v39 Any
v40
-> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v38
Any
v39
Any
v40
T_ProofOrCE_38
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v36 Any
v37 Any
v38
-> (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any
-> Any
-> Any
forall a b. a -> b
coe
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v36
Any
v37
Any
v38
T_ProofOrCE_38
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_56
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_144
_ -> 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
v21)
((T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> T__'8866'_14
-> T__'8866'_14
-> Any
forall a b. a -> b
coe
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_32
T__'8866'_14
v1
T__'8866'_14
v2)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isDelay_356
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_56
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_144
_ -> 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
v5)
((T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38)
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> T__'8866'_14
-> T__'8866'_14
-> Any
forall a b. a -> b
coe
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any -> Any -> T_ProofOrCE_38
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_52
T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
MAlonzo.Code.VerifiedCompilation.Trace.d_FloatDelayT_32 T__'8866'_14
v1 T__'8866'_14
v2)
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'46'extendedlambda0_122 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_144 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FlD_78 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_122 :: Integer
-> T__'8866'_14
-> (T_isApp_144 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_FlD_78
-> T_Irrelevant_20
d_'46'extendedlambda0_122 = Integer
-> T__'8866'_14
-> (T_isApp_144 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_FlD_78
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda1_152 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_144 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FlD_78 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_152 :: Integer
-> T__'8866'_14
-> (T_isApp_144 -> T_Irrelevant_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_FlD_78
-> T_Irrelevant_20
d_'46'extendedlambda1_152 = Integer
-> T__'8866'_14
-> (T_isApp_144 -> T_Irrelevant_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_FlD_78
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda2_196 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FlD_78 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda2_196 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_8 -> T_Irrelevant_20)
-> ()
-> ()
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_FlD_78
-> T_Irrelevant_20
d_'46'extendedlambda2_196 = Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_8 -> T_Irrelevant_20)
-> ()
-> ()
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_FlD_78
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda3_244 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
() ->
() ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8 ->
T_FlD_78 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda3_244 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_8 -> T_Irrelevant_20)
-> ()
-> ()
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_8
-> T_FlD_78
-> T_Irrelevant_20
d_'46'extendedlambda3_244 = Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Translation_8 -> T_Irrelevant_20)
-> ()
-> ()
-> T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
-> Any
-> Any
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_8
-> T_FlD_78
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda4_290 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Untyped.Purity.T_Pure_6 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_8 ->
T_FlD_78 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda4_290 :: Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Translation_8
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_8
-> T_FlD_78
-> T_Irrelevant_20
d_'46'extendedlambda4_290 = Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Translation_8
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_8
-> T_FlD_78
-> T_Irrelevant_20
forall a. a
erased