{-# 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.UCSE 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.Sigma
import qualified MAlonzo.Code.Data.Irrelevant
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.Equality
import qualified MAlonzo.Code.VerifiedCompilation.Purity
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews
d_UCSE_4 :: p -> p -> p -> p -> ()
d_UCSE_4 p
a0 p
a1 p
a2 p
a3 = ()
data T_UCSE_4
= C_cse_16 MAlonzo.Code.VerifiedCompilation.Purity.T_UPure_6
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
d_UntypedCSE_26 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_UntypedCSE_26 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_UntypedCSE_26 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
d_isUntypedCSE'63'_32 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isUntypedCSE'63'_32 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_isUntypedCSE'63'_32 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isUntypedCSE'63'_32 T_DecEq_6
v1
du_isUntypedCSE'63'_32 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isUntypedCSE'63'_32 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isUntypedCSE'63'_32 T_DecEq_6
v0
= (()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_20)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_20
forall a b. a -> b
coe
()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_100
Any
forall a. a
erased (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isUCSE'63'_38 Any
v2 Any
v3 Any
v4)
d_isUCSE'63'_38 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isUCSE'63'_38 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_isUCSE'63'_38 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isUCSE'63'_38 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isUCSE'63'_38 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isUCSE'63'_38 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isUCSE'63'_38 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
= let v3 :: t
v3
= (()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> 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 -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
((() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> (Any -> Any -> Any) -> Any
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
v4 Any
v5 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
(\ Any
v3 Any
v4 ->
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
v2) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
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_142
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v9 Any
v10
-> 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
v11 T__'8866'_14
v12
-> case Any -> T_isLambda_54
forall a b. a -> b
coe Any
v9 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 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)
((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 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
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> T_DecEq_6 -> T__'8866'_14 -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isUntypedCSE'63'_32 T_DecEq_6
v0
T__'8866'_14
v1
((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.RenamingSubstitution.du__'91'_'93'_468
(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
v12)))
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v4)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_UPure_6 -> Any
forall a b. a -> b
coe
T_UPure_6
MAlonzo.Code.VerifiedCompilation.Purity.C_FIXME_12))) 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
-> case Any -> T_Σ_14
forall a b. a -> b
coe
Any
v19 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v20 Any
v21
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v17)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_UPure_6 -> T_Translation_16 -> T_UCSE_4) -> Any -> Any -> Any
forall a b. a -> b
coe
T_UPure_6 -> T_Translation_16 -> T_UCSE_4
C_cse_16
Any
v21
Any
v20))
T_Σ_14
_ -> 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)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v17)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
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__'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
v5)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'46'extendedlambda0_54 ::
() ->
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 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_UCSE_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_54 :: ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_UCSE_4
-> T_Irrelevant_20
d_'46'extendedlambda0_54 = ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_UCSE_4
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda1_82 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_UCSE_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_82 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_UCSE_4
-> T_Irrelevant_20
d_'46'extendedlambda1_82 = ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_UCSE_4
-> T_Irrelevant_20
forall a. a
erased